/[mojave]/metaprl/theories/czf/czf_itt_group.prla
ViewVC logotype

Annotation of /metaprl/theories/czf/czf_itt_group.prla

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3527 - (hide annotations) (download)
Mon Mar 4 02:20:01 2002 UTC (19 years, 4 months ago) by xiny
File size: 120257 byte(s)
1. Replaced equality relations with equivalence relations in
   the definition axioms for "op", "inv", and "id".
2. Defined the equivalence functionality for "op" and "inv".
3. Changed the tactics for "left and right cancellation laws"
   (i.e., groupCancelLeftT and groupCancelRightT) to make it
   easier to use.
4. Re-proved all properties.

1 xiny 3379 #PRL version 1.0.0 ASCII term
2     NPerv Perv Perv NIL
3     NPerv!cons cons cons Perv
4     O o cons
5     NSummary Summary Summary NIL
6     NSummary!location location location Summary
7     P p Number 0
8 xiny 3498 P p1 Number 25
9 xiny 3379 O o1 location p p1
10     NSummary!parent parent parent Summary
11     O o2 parent
12 xiny 3498 P p2 String Itt_record_label0
13 xiny 3379 O o3 parent p2
14     T t o3
15     B b t
16     NPerv!nil nil3 nil Perv
17     O o4 nil3
18     T t4 o4
19     B b4 t4
20     T t5 o b b4
21     B b5 t5
22 xiny 3498 P p5 String Itt_nat
23 xiny 3379 O o5 parent p5
24     T t6 o5
25     B b6 t6
26     T t7 o b6 b4
27     B b7 t7
28 xiny 3498 P p7 String Itt_int_ext
29 xiny 3379 O o7 parent p7
30     T t8 o7
31     B b8 t8
32     T t9 o b8 b4
33     B b9 t9
34 xiny 3498 P p9 String Itt_int_base
35 xiny 3379 O o9 parent p9
36     T t10 o9
37     B b10 t10
38     T t11 o b10 b4
39     B b11 t11
40 xiny 3498 P p11 String Itt_bool
41 xiny 3379 O o11 parent p11
42     T t12 o11
43     B b12 t12
44     T t13 o b12 b4
45     B b13 t13
46 xiny 3498 P p13 String Itt_decidable
47 xiny 3379 O o13 parent p13
48     T t14 o13
49     B b14 t14
50     T t15 o b14 b4
51     B b15 t15
52 xiny 3498 P p15 String Itt_logic
53 xiny 3379 O o15 parent p15
54     T t16 o15
55     B b16 t16
56     T t17 o b16 b4
57     B b17 t17
58 xiny 3498 P p17 String Itt_union
59 xiny 3379 O o17 parent p17
60     T t18 o17
61     B b18 t18
62     T t19 o b18 b4
63     B b19 t19
64 xiny 3498 P p19 String Itt_prod
65 xiny 3379 O o19 parent p19
66     T t20 o19
67     B b20 t20
68     T t21 o b20 b4
69     B b21 t21
70 xiny 3498 P p21 String Itt_dprod
71 xiny 3379 O o21 parent p21
72     T t22 o21
73     B b22 t22
74     T t23 o b22 b4
75     B b23 t23
76 xiny 3498 P p23 String Itt_fun
77 xiny 3379 O o23 parent p23
78     T t24 o23
79     B b24 t24
80     T t25 o b24 b4
81     B b25 t25
82 xiny 3498 P p25 String Itt_dfun
83 xiny 3379 O o25 parent p25
84     T t26 o25
85     B b26 t26
86     T t27 o b26 b4
87     B b27 t27
88 xiny 3498 P p27 String Itt_rfun
89 xiny 3379 O o27 parent p27
90     T t28 o27
91     B b28 t28
92     T t29 o b28 b4
93     B b29 t29
94 xiny 3498 P p29 String Itt_void
95 xiny 3379 O o29 parent p29
96     T t30 o29
97     B b30 t30
98     T t31 o b30 b4
99     B b31 t31
100 xiny 3498 P p31 String Itt_set
101 xiny 3379 O o31 parent p31
102     T t32 o31
103     B b32 t32
104     T t33 o b32 b4
105     B b33 t33
106 xiny 3498 P p33 String Itt_unit
107 xiny 3379 O o33 parent p33
108     T t34 o33
109     B b34 t34
110     T t35 o b34 b4
111     B b35 t35
112 xiny 3498 P p35 String Itt_squiggle
113 xiny 3379 O o35 parent p35
114     T t36 o35
115     B b36 t36
116     T t37 o b36 b4
117     B b37 t37
118 xiny 3498 P p37 String Itt_subtype
119 xiny 3379 O o37 parent p37
120     T t38 o37
121     B b38 t38
122     T t39 o b38 b4
123     B b39 t39
124 xiny 3498 P p39 String Itt_squash
125 xiny 3379 O o39 parent p39
126     T t40 o39
127     B b40 t40
128     T t41 o b40 b4
129     B b41 t41
130 xiny 3498 P p41 String Itt_struct
131 xiny 3379 O o41 parent p41
132     T t42 o41
133     B b42 t42
134     T t43 o b42 b4
135     B b43 t43
136 xiny 3498 P p43 String Itt_equal
137 xiny 3379 O o43 parent p43
138     T t44 o43
139     B b44 t44
140     T t45 o b44 b4
141     B b45 t45
142 xiny 3498 P p45 String Itt_comment
143 xiny 3379 O o45 parent p45
144     T t46 o45
145     B b46 t46
146     T t47 o b46 b4
147     B b47 t47
148 xiny 3498 P p47 String Base_theory
149 xiny 3379 O o47 parent p47
150     T t48 o47
151     B b48 t48
152     T t49 o b48 b4
153     B b49 t49
154 xiny 3498 P p49 String Base_meta
155 xiny 3379 O o49 parent p49
156     T t50 o49
157     B b50 t50
158     T t51 o b50 b4
159     B b51 t51
160 xiny 3498 P p51 String Base_cache
161 xiny 3379 O o51 parent p51
162     T t52 o51
163     B b52 t52
164     T t53 o b52 b4
165     B b53 t53
166 xiny 3498 P p53 String Tactic_cache
167 xiny 3379 O o53 parent p53
168     T t54 o53
169     B b54 t54
170     T t55 o b54 b4
171     B b55 t55
172 xiny 3498 P p55 String Typeinf
173 xiny 3379 O o55 parent p55
174     T t56 o55
175     B b56 t56
176     T t57 o b56 b4
177     B b57 t57
178 xiny 3498 P p57 String Ocaml_df
179 xiny 3379 O o57 parent p57
180     T t58 o57
181     B b58 t58
182     T t59 o b58 b4
183     B b59 t59
184 xiny 3498 P p59 String Ocaml_str_df
185 xiny 3379 O o59 parent p59
186     T t60 o59
187     B b60 t60
188     T t61 o b60 b4
189     B b61 t61
190 xiny 3498 P p61 String Ocaml_sig_df
191 xiny 3379 O o61 parent p61
192     T t62 o61
193     B b62 t62
194     T t63 o b62 b4
195     B b63 t63
196 xiny 3498 P p63 String Ocaml_me_df
197 xiny 3379 O o63 parent p63
198     T t64 o63
199     B b64 t64
200     T t65 o b64 b4
201     B b65 t65
202 xiny 3498 P p65 String Ocaml_mt_df
203 xiny 3379 O o65 parent p65
204     T t66 o65
205     B b66 t66
206     T t67 o b66 b4
207     B b67 t67
208 xiny 3498 P p67 String Ocaml_type_df
209 xiny 3379 O o67 parent p67
210     T t68 o67
211     B b68 t68
212     T t69 o b68 b4
213     B b69 t69
214 xiny 3498 P p69 String Ocaml_patt_df
215 xiny 3379 O o69 parent p69
216     T t70 o69
217     B b70 t70
218     T t71 o b70 b4
219     B b71 t71
220 xiny 3498 P p71 String Ocaml_expr_df
221 xiny 3379 O o71 parent p71
222     T t72 o71
223     B b72 t72
224     T t73 o b72 b4
225     B b73 t73
226 xiny 3498 P p73 String Ocaml_base_df
227 xiny 3379 O o73 parent p73
228     T t74 o73
229     B b74 t74
230     T t75 o b74 b4
231     B b75 t75
232 xiny 3498 P p75 String Ocaml
233 xiny 3379 O o75 parent p75
234     T t76 o75
235     B b76 t76
236     T t77 o b76 b4
237     B b77 t77
238 xiny 3498 P p77 String Base_rewrite
239 xiny 3379 O o77 parent p77
240     T t78 o77
241     B b78 t78
242     T t79 o b78 b4
243     B b79 t79
244 xiny 3498 P p79 String Base_dtactic
245 xiny 3379 O o79 parent p79
246     T t80 o79
247     B b80 t80
248     T t81 o b80 b4
249     B b81 t81
250 xiny 3498 P p81 String Base_auto_tactic
251 xiny 3379 O o81 parent p81
252     T t82 o81
253     B b82 t82
254     T t83 o b82 b4
255     B b83 t83
256 xiny 3498 P p83 String Base_trivial
257 xiny 3379 O o83 parent p83
258     T t84 o83
259     B b84 t84
260     T t85 o b84 b4
261     B b85 t85
262 xiny 3498 P p85 String Top_conversionals
263 xiny 3379 O o85 parent p85
264     T t86 o85
265     B b86 t86
266     T t87 o b86 b4
267     B b87 t87
268 xiny 3498 P p87 String Top_tacticals
269 xiny 3379 O o87 parent p87
270     T t88 o87
271     B b88 t88
272     T t89 o b88 b4
273     B b89 t89
274 xiny 3498 P p89 String Var
275 xiny 3379 O o89 parent p89
276     T t90 o89
277     B b90 t90
278     T t91 o b90 b4
279     B b91 t91
280 xiny 3498 P p91 String Mptop
281 xiny 3379 O o91 parent p91
282     T t92 o91
283     B b92 t92
284     T t93 o b92 b4
285     B b93 t93
286 xiny 3498 P p93 String Summary
287 xiny 3379 O o93 parent p93
288     T t94 o93
289     B b94 t94
290     T t95 o b94 b4
291     B b95 t95
292 xiny 3498 P p95 String Comment
293 xiny 3379 O o95 parent p95
294     T t96 o95
295     B b96 t96
296     T t97 o b96 b4
297     B b97 t97
298 xiny 3498 P p97 String Base_dform
299 xiny 3379 O o97 parent p97
300     T t98 o97
301     B b98 t98
302     T t99 o b98 b4
303     B b99 t99
304 xiny 3498 P p99 String Nuprl_font
305 xiny 3379 O o99 parent p99
306     T t100 o99
307     B b100 t100
308     T t101 o b100 b4
309     B b101 t101
310 xiny 3498 P p101 String Perv
311 xiny 3379 O o101 parent p101
312     T t102 o101
313     B b102 t102
314     T t103 o b102 b4
315     B b103 t103
316 xiny 3498 T t104 o b103 b4
317 xiny 3379 B b104 t104
318 xiny 3498 T t105 o b101 b104
319 xiny 3379 B b105 t105
320 xiny 3498 T t106 o b99 b105
321 xiny 3379 B b106 t106
322 xiny 3498 T t107 o b97 b106
323 xiny 3379 B b107 t107
324 xiny 3498 T t108 o b95 b107
325 xiny 3379 B b108 t108
326 xiny 3498 T t109 o b93 b108
327 xiny 3379 B b109 t109
328 xiny 3498 T t110 o b91 b109
329 xiny 3379 B b110 t110
330 xiny 3498 T t111 o b89 b110
331 xiny 3379 B b111 t111
332 xiny 3498 T t112 o b87 b111
333 xiny 3379 B b112 t112
334 xiny 3498 T t113 o b85 b112
335 xiny 3379 B b113 t113
336 xiny 3498 T t114 o b83 b113
337 xiny 3379 B b114 t114
338 xiny 3498 T t115 o b81 b114
339 xiny 3379 B b115 t115
340 xiny 3498 T t116 o b79 b115
341 xiny 3379 B b116 t116
342 xiny 3498 T t117 o b77 b116
343 xiny 3379 B b117 t117
344 xiny 3498 T t118 o b75 b117
345 xiny 3379 B b118 t118
346 xiny 3498 T t119 o b73 b118
347 xiny 3379 B b119 t119
348 xiny 3498 T t120 o b71 b119
349 xiny 3379 B b120 t120
350 xiny 3498 T t121 o b69 b120
351 xiny 3379 B b121 t121
352 xiny 3498 T t122 o b67 b121
353 xiny 3379 B b122 t122
354 xiny 3498 T t123 o b65 b122
355 xiny 3379 B b123 t123
356 xiny 3498 T t124 o b63 b123
357 xiny 3379 B b124 t124
358 xiny 3498 T t125 o b61 b124
359 xiny 3379 B b125 t125
360 xiny 3498 T t126 o b59 b125
361 xiny 3379 B b126 t126
362 xiny 3498 T t127 o b57 b126
363 xiny 3379 B b127 t127
364 xiny 3498 T t128 o b55 b127
365 xiny 3379 B b128 t128
366 xiny 3498 T t129 o b53 b128
367 xiny 3379 B b129 t129
368 xiny 3498 T t130 o b51 b129
369 xiny 3379 B b130 t130
370 xiny 3498 T t131 o b49 b130
371 xiny 3379 B b131 t131
372 xiny 3498 T t132 o b47 b131
373 xiny 3379 B b132 t132
374 xiny 3498 T t133 o b45 b132
375 xiny 3379 B b133 t133
376 xiny 3498 T t134 o b43 b133
377 xiny 3379 B b134 t134
378 xiny 3498 T t135 o b41 b134
379 xiny 3379 B b135 t135
380 xiny 3498 T t136 o b39 b135
381 xiny 3379 B b136 t136
382 xiny 3498 T t137 o b37 b136
383 xiny 3379 B b137 t137
384 xiny 3498 T t138 o b35 b137
385 xiny 3379 B b138 t138
386 xiny 3498 T t139 o b33 b138
387 xiny 3379 B b139 t139
388 xiny 3498 T t140 o b31 b139
389 xiny 3379 B b140 t140
390 xiny 3498 T t141 o b29 b140
391 xiny 3379 B b141 t141
392 xiny 3498 T t142 o b27 b141
393 xiny 3379 B b142 t142
394 xiny 3498 T t143 o b25 b142
395 xiny 3379 B b143 t143
396 xiny 3498 T t144 o b23 b143
397 xiny 3379 B b144 t144
398 xiny 3498 T t145 o b21 b144
399 xiny 3379 B b145 t145
400 xiny 3498 T t146 o b19 b145
401 xiny 3379 B b146 t146
402 xiny 3498 T t147 o b17 b146
403 xiny 3379 B b147 t147
404 xiny 3498 T t148 o b15 b147
405 xiny 3379 B b148 t148
406 xiny 3498 T t149 o b13 b148
407 xiny 3379 B b149 t149
408 xiny 3498 T t150 o b11 b149
409 xiny 3379 B b150 t150
410 xiny 3498 T t151 o b9 b150
411 xiny 3379 B b151 t151
412 xiny 3498 T t152 o b7 b151
413 xiny 3379 B b152 t152
414 xiny 3498 T t153 o b5 b152
415 xiny 3379 B b153 t153
416 xiny 3498 NSummary!resource resource resource Summary
417     P p153 String auto
418     O o153 resource p153
419     NOcaml Ocaml Ocaml NIL
420     NOcaml!type_lid type_lid type_lid Ocaml
421     P p154 Number 2332
422     P p155 Number 2341
423     O o155 type_lid p154 p155
424     P p156 String auto_info
425     O o156 type_lid p156
426     T t156 o156
427 xiny 3379 B b156 t156
428 xiny 3498 T t157 o155 b156
429 xiny 3379 B b157 t157
430 xiny 3498 NOcaml!type_prod type_prod type_prod Ocaml
431     P p157 Number 2343
432     P p158 Number 2367
433     O o158 type_prod p157 p158
434     P p159 Number 2349
435     O o159 type_lid p157 p159
436     P p160 String tactic
437     O o160 type_lid p160
438     T t160 o160
439 xiny 3379 B b160 t160
440 xiny 3498 T t161 o159 b160
441 xiny 3379 B b161 t161
442 xiny 3498 P p161 Number 2352
443     P p162 Number 2358
444     O o162 type_lid p161 p162
445     T t162 o162 b160
446 xiny 3379 B b162 t162
447 xiny 3498 P p163 Number 2361
448     O o163 type_lid p163 p158
449     T t163 o163 b160
450 xiny 3379 B b163 t163
451 xiny 3498 T t164 o b163 b4
452 xiny 3379 B b164 t164
453 xiny 3498 T t165 o b162 b164
454 xiny 3379 B b165 t165
455 xiny 3498 T t166 o b161 b165
456 xiny 3379 B b166 t166
457 xiny 3498 T t167 o158 b166
458 xiny 3379 B b167 t167
459 xiny 3498 T t168 o153 b157 b167
460 xiny 3379 B b168 t168
461 xiny 3498 P p168 String cache
462     O o168 resource p168
463     P p169 Number 1424
464     P p170 Number 1434
465     O o170 type_lid p169 p170
466     P p171 String cache_rule
467     O o171 type_lid p171
468     T t171 o171
469 xiny 3379 B b171 t171
470 xiny 3498 T t172 o170 b171
471 xiny 3379 B b172 t172
472 xiny 3498 P p172 Number 1436
473     P p173 Number 1441
474     O o173 type_lid p172 p173
475     O o174 type_lid p168
476     T t174 o174
477 xiny 3379 B b174 t174
478 xiny 3498 T t175 o173 b174
479 xiny 3379 B b175 t175
480 xiny 3498 T t176 o168 b172 b175
481 xiny 3379 B b176 t176
482 xiny 3498 P p176 String elim
483     O o176 resource p176
484     P p177 Number 1761
485     P p178 Number 1783
486     O o178 type_prod p177 p178
487     P p179 Number 1765
488     O o179 type_lid p177 p179
489     P p180 String term
490     O o180 type_lid p180
491     T t180 o180
492 xiny 3379 B b180 t180
493 xiny 3498 T t181 o179 b180
494 xiny 3379 B b181 t181
495 xiny 3498 NOcaml!type_fun type_fun type_fun Ocaml
496     P p181 Number 1769
497     P p182 Number 1782
498     O o182 type_fun p181 p182
499     P p183 Number 1772
500     O o183 type_lid p181 p183
501     P p184 String int
502     O o184 type_lid p184
503     T t184 o184
504 xiny 3379 B b184 t184
505 xiny 3498 T t185 o183 b184
506 xiny 3379 B b185 t185
507 xiny 3498 P p185 Number 1776
508     O o185 type_lid p185 p182
509     T t186 o185 b160
510 xiny 3379 B b186 t186
511 xiny 3498 T t187 o182 b185 b186
512 xiny 3379 B b187 t187
513 xiny 3498 T t188 o b187 b4
514 xiny 3379 B b188 t188
515 xiny 3498 T t189 o b181 b188
516 xiny 3379 B b189 t189
517 xiny 3498 T t190 o178 b189
518 xiny 3379 B b190 t190
519 xiny 3498 P p190 Number 1785
520     P p191 Number 1798
521     O o191 type_fun p190 p191
522     P p192 Number 1788
523     O o192 type_lid p190 p192
524     T t192 o192 b184
525 xiny 3379 B b192 t192
526 xiny 3498 P p193 Number 1792
527     O o193 type_lid p193 p191
528     T t193 o193 b160
529 xiny 3379 B b193 t193
530 xiny 3498 T t194 o191 b192 b193
531 xiny 3379 B b194 t194
532 xiny 3498 T t195 o176 b190 b194
533 xiny 3379 B b195 t195
534 xiny 3498 P p195 String eqcd
535     O o195 resource p195
536     P p196 Number 6168
537     P p197 Number 6181
538     O o197 type_prod p196 p197
539     P p198 Number 6172
540     O o198 type_lid p196 p198
541     T t198 o198 b180
542 xiny 3379 B b198 t198
543 xiny 3498 P p199 Number 6175
544     O o199 type_lid p199 p197
545     T t199 o199 b160
546 xiny 3379 B b199 t199
547 xiny 3498 T t200 o b199 b4
548 xiny 3379 B b200 t200
549 xiny 3498 T t201 o b198 b200
550 xiny 3379 B b201 t201
551 xiny 3498 T t202 o197 b201
552 xiny 3379 B b202 t202
553 xiny 3498 P p202 Number 6183
554     P p203 Number 6189
555     O o203 type_lid p202 p203
556     T t203 o203 b160
557 xiny 3379 B b203 t203
558 xiny 3498 T t204 o195 b202 b203
559 xiny 3379 B b204 t204
560 xiny 3498 P p204 String intro
561     O o204 resource p204
562     P p205 Number 1815
563     P p206 Number 1852
564     O o206 type_prod p205 p206
565     P p207 Number 1819
566     O o207 type_lid p205 p207
567     T t207 o207 b180
568 xiny 3379 B b207 t207
569 xiny 3498 P p208 Number 1823
570     P p209 Number 1851
571     O o209 type_prod p208 p209
572     P p210 Number 1829
573     O o210 type_lid p208 p210
574     P p211 String string
575     O o211 type_lid p211
576     T t211 o211
577 xiny 3379 B b211 t211
578 xiny 3498 T t212 o210 b211
579 xiny 3379 B b212 t212
580 xiny 3498 NOcaml!type_apply type_apply type_apply Ocaml
581     P p212 Number 1832
582     P p213 Number 1842
583     O o213 type_apply p212 p213
584     P p214 Number 1836
585     O o214 type_lid p214 p213
586     P p215 String option
587     O o215 type_lid p215
588     T t215 o215
589     B b215 t215
590     T t216 o214 b215
591 xiny 3379 B b216 t216
592 xiny 3498 P p216 Number 1835
593     O o216 type_lid p212 p216
594     T t217 o216 b184
595 xiny 3379 B b217 t217
596 xiny 3498 T t218 o213 b216 b217
597     B b218 t218
598     P p218 Number 1845
599     O o218 type_lid p218 p209
600     T t219 o218 b160
601     B b219 t219
602     T t220 o b219 b4
603 xiny 3379 B b220 t220
604 xiny 3498 T t221 o b218 b220
605 xiny 3379 B b221 t221
606 xiny 3498 T t222 o b212 b221
607 xiny 3379 B b222 t222
608 xiny 3498 T t223 o209 b222
609 xiny 3379 B b223 t223
610 xiny 3404 T t224 o b223 b4
611 xiny 3379 B b224 t224
612 xiny 3498 T t225 o b207 b224
613 xiny 3379 B b225 t225
614 xiny 3498 T t226 o206 b225
615 xiny 3379 B b226 t226
616 xiny 3498 P p226 Number 1854
617     P p227 Number 1860
618     O o227 type_lid p226 p227
619     T t227 o227 b160
620 xiny 3404 B b227 t227
621 xiny 3498 T t228 o204 b226 b227
622 xiny 3404 B b228 t228
623 xiny 3498 P p228 String reduce
624 xiny 3404 O o228 resource p228
625 xiny 3498 P p229 Number 2920
626     P p230 Number 2931
627     O o230 type_prod p229 p230
628     P p231 Number 2924
629     O o231 type_lid p229 p231
630     T t231 o231 b180
631 xiny 3404 B b231 t231
632 xiny 3498 P p232 Number 2927
633     O o232 type_lid p232 p230
634     P p233 String conv
635     O o233 type_lid p233
636     T t233 o233
637     B b233 t233
638     T t234 o232 b233
639 xiny 3379 B b234 t234
640 xiny 3498 T t235 o b234 b4
641 xiny 3404 B b235 t235
642 xiny 3498 T t236 o b231 b235
643 xiny 3404 B b236 t236
644 xiny 3498 T t237 o230 b236
645     B b237 t237
646     P p237 Number 2933
647     P p238 Number 2937
648     O o238 type_lid p237 p238
649     T t238 o238 b233
650     B b238 t238
651     T t239 o228 b237 b238
652     B b239 t239
653     P p239 String squash
654     O o239 resource p239
655     P p240 Number 4017
656     P p241 Number 4028
657     O o241 type_lid p240 p241
658     P p242 String squash_info
659     O o242 type_lid p242
660     T t242 o242
661     B b242 t242
662     T t243 o241 b242
663     B b243 t243
664     P p243 Number 4030
665     P p244 Number 4043
666     O o244 type_fun p243 p244
667     P p245 Number 4033
668     O o245 type_lid p243 p245
669     T t245 o245 b184
670 xiny 3379 B b245 t245
671 xiny 3498 P p246 Number 4037
672     O o246 type_lid p246 p244
673     T t246 o246 b160
674 xiny 3379 B b246 t246
675 xiny 3498 T t247 o244 b245 b246
676 xiny 3379 B b247 t247
677 xiny 3498 T t248 o239 b243 b247
678 xiny 3379 B b248 t248
679 xiny 3498 P p248 String sub
680     O o248 resource p248
681     P p249 Number 4882
682     P p250 Number 4899
683     O o250 type_lid p249 p250
684     P p251 String sub_resource_info
685     O o251 type_lid p251
686     T t251 o251
687     B b251 t251
688     T t252 o250 b251
689 xiny 3379 B b252 t252
690 xiny 3498 P p252 Number 4901
691     P p253 Number 4907
692     O o253 type_lid p252 p253
693     T t253 o253 b160
694 xiny 3379 B b253 t253
695 xiny 3498 T t254 o248 b252 b253
696 xiny 3404 B b254 t254
697 xiny 3498 P p254 String toploop
698     O o254 resource p254
699     P p255 Number 2445
700     P p256 Number 2467
701     O o256 type_prod p255 p256
702     P p257 Number 2451
703     O o257 type_lid p255 p257
704     T t257 o257 b211
705     B b257 t257
706     P p258 Number 2454
707     P p259 Number 2460
708     O o259 type_lid p258 p259
709     T t259 o259 b211
710 xiny 3379 B b259 t259
711 xiny 3498 P p260 Number 2463
712     O o260 type_lid p260 p256
713     P p261 String expr
714     O o261 type_lid p261
715     T t261 o261
716 xiny 3379 B b261 t261
717 xiny 3498 T t262 o260 b261
718 xiny 3379 B b262 t262
719 xiny 3498 T t263 o b262 b4
720 xiny 3404 B b263 t263
721 xiny 3498 T t264 o b259 b263
722 xiny 3404 B b264 t264
723 xiny 3498 T t265 o b257 b264
724     B b265 t265
725     T t266 o256 b265
726     B b266 t266
727     P p266 Number 2469
728     P p267 Number 2478
729     O o267 type_lid p266 p267
730     P p268 String top_table
731     O o268 type_lid p268
732     T t268 o268
733     B b268 t268
734     T t269 o267 b268
735     B b269 t269
736     T t270 o254 b266 b269
737     B b270 t270
738     P p270 String typeinf
739     O o270 resource p270
740     P p271 Number 2151
741     P p272 Number 2172
742     O o272 type_lid p271 p272
743     P p273 String typeinf_resource_info
744     O o273 type_lid p273
745     T t273 o273
746     B b273 t273
747     T t274 o272 b273
748     B b274 t274
749     P p274 Number 2174
750     P p275 Number 2186
751     O o275 type_lid p274 p275
752     P p276 String typeinf_func
753     O o276 type_lid p276
754     T t276 o276
755 xiny 3379 B b276 t276
756 xiny 3498 T t277 o275 b276
757 xiny 3379 B b277 t277
758 xiny 3498 T t278 o270 b274 b277
759 xiny 3379 B b278 t278
760 xiny 3498 P p278 String typeinf_subst
761     O o278 resource p278
762     P p279 Number 1825
763     P p280 Number 1843
764     O o280 type_lid p279 p280
765     P p281 String typeinf_subst_info
766     O o281 type_lid p281
767     T t281 o281
768 xiny 3379 B b281 t281
769 xiny 3498 T t282 o280 b281
770 xiny 3379 B b282 t282
771 xiny 3498 P p282 Number 1862
772     O o282 type_lid p218 p282
773     P p283 String typeinf_subst_fun
774     O o283 type_lid p283
775     T t283 o283
776 xiny 3379 B b283 t283
777 xiny 3498 T t284 o282 b283
778 xiny 3379 B b284 t284
779 xiny 3498 T t285 o278 b282 b284
780 xiny 3379 B b285 t285
781 xiny 3498 T t286 o b285 b4
782 xiny 3379 B b286 t286
783 xiny 3498 T t287 o b278 b286
784 xiny 3404 B b287 t287
785 xiny 3498 T t288 o b270 b287
786 xiny 3404 B b288 t288
787 xiny 3498 T t289 o b254 b288
788     B b289 t289
789     T t290 o b248 b289
790     B b290 t290
791     T t291 o b239 b290
792 xiny 3379 B b291 t291
793 xiny 3498 T t292 o b228 b291
794     B b292 t292
795     T t293 o b204 b292
796 xiny 3379 B b293 t293
797 xiny 3498 T t294 o b195 b293
798 xiny 3379 B b294 t294
799 xiny 3498 T t295 o b176 b294
800 xiny 3379 B b295 t295
801 xiny 3498 T t296 o b168 b295
802 xiny 3379 B b296 t296
803 xiny 3498 T t297 o2 b5 b153 b296
804 xiny 3379 B b297 t297
805 xiny 3498 T t298 o1 b297
806 xiny 3404 B b298 t298
807 xiny 3498 P p298 Number 26
808     P p299 Number 45
809     O o299 location p298 p299
810     P p300 String Czf_itt_set
811     O o300 parent p300
812     T t300 o300
813     B b300 t300
814     T t301 o b300 b4
815     B b301 t301
816     P p301 String Czf_itt_comment
817     O o301 parent p301
818     T t302 o301
819 xiny 3404 B b302 t302
820 xiny 3498 T t303 o b302 b4
821 xiny 3379 B b303 t303
822 xiny 3498 P p303 String Itt_theory
823     O o303 parent p303
824     T t304 o303
825     B b304 t304
826     T t305 o b304 b4
827 xiny 3379 B b305 t305
828 xiny 3498 P p305 String Itt_fset
829     O o305 parent p305
830     T t306 o305
831 xiny 3379 B b306 t306
832 xiny 3498 T t307 o b306 b4
833 xiny 3404 B b307 t307
834 xiny 3498 P p307 String Itt_prop_decide
835     O o307 parent p307
836     T t308 o307
837 xiny 3404 B b308 t308
838 xiny 3498 T t309 o b308 b4
839     B b309 t309
840     P p309 String Itt_derive
841     O o309 parent p309
842     T t310 o309
843     B b310 t310
844     T t311 o b310 b4
845 xiny 3379 B b311 t311
846 xiny 3498 P p311 String Itt_list2
847     O o311 parent p311
848     T t312 o311
849 xiny 3379 B b312 t312
850 xiny 3498 T t313 o b312 b4
851 xiny 3404 B b313 t313
852 xiny 3498 P p313 String Itt_list
853     O o313 parent p313
854     T t314 o313
855 xiny 3404 B b314 t314
856 xiny 3498 T t315 o b314 b4
857     B b315 t315
858     P p315 String Itt_quotient
859     O o315 parent p315
860     T t316 o315
861     B b316 t316
862     T t317 o b316 b4
863 xiny 3379 B b317 t317
864 xiny 3498 P p317 String Itt_esquash
865     O o317 parent p317
866     T t318 o317
867     B b318 t318
868     T t319 o b318 b4
869 xiny 3379 B b319 t319
870 xiny 3498 P p319 String Itt_srec
871     O o319 parent p319
872     T t320 o319
873     B b320 t320
874     T t321 o b320 b4
875 xiny 3379 B b321 t321
876 xiny 3498 P p321 String Itt_prec
877     O o321 parent p321
878     T t322 o321
879 xiny 3379 B b322 t322
880 xiny 3404 T t323 o b322 b4
881 xiny 3379 B b323 t323
882 xiny 3498 P p323 String Itt_w
883     O o323 parent p323
884     T t324 o323
885 xiny 3379 B b324 t324
886 xiny 3498 T t325 o b324 b4
887 xiny 3404 B b325 t325
888 xiny 3498 P p325 String Itt_bunion
889     O o325 parent p325
890     T t326 o325
891 xiny 3379 B b326 t326
892 xiny 3498 T t327 o b326 b4
893     B b327 t327
894     P p327 String Itt_bisect
895     O o327 parent p327
896     T t328 o327
897 xiny 3379 B b328 t328
898 xiny 3498 T t329 o b328 b4
899 xiny 3404 B b329 t329
900 xiny 3498 P p329 String Itt_tunion
901     O o329 parent p329
902     T t330 o329
903 xiny 3404 B b330 t330
904 xiny 3498 T t331 o b330 b4
905     B b331 t331
906     P p331 String Itt_isect
907     O o331 parent p331
908     T t332 o331
909     B b332 t332
910     T t333 o b332 b4
911 xiny 3404 B b333 t333
912 xiny 3498 P p333 String Itt_struct2
913     O o333 parent p333
914     T t334 o333
915 xiny 3379 B b334 t334
916 xiny 3498 T t335 o b334 b4
917     B b335 t335
918     P p335 String Itt_well_founded
919     O o335 parent p335
920     T t336 o335
921 xiny 3379 B b336 t336
922 xiny 3498 T t337 o b336 b4
923 xiny 3404 B b337 t337
924 xiny 3498 P p337 String Itt_int_arith
925     O o337 parent p337
926     T t338 o337
927 xiny 3404 B b338 t338
928 xiny 3498 T t339 o b338 b4
929     B b339 t339
930     P p339 String Itt_atom_bool
931     O o339 parent p339
932     T t340 o339
933     B b340 t340
934     T t341 o b340 b4
935 xiny 3379 B b341 t341
936 xiny 3498 P p341 String Itt_atom
937     O o341 parent p341
938     T t342 o341
939 xiny 3379 B b342 t342
940 xiny 3498 T t343 o b342 b4
941 xiny 3379 B b343 t343
942 xiny 3498 T t344 o b343 b4
943 xiny 3379 B b344 t344
944 xiny 3498 T t345 o b341 b344
945 xiny 3379 B b345 t345
946 xiny 3498 T t346 o b339 b345
947 xiny 3379 B b346 t346
948 xiny 3498 T t347 o b337 b346
949 xiny 3379 B b347 t347
950 xiny 3498 T t348 o b335 b347
951 xiny 3379 B b348 t348
952 xiny 3498 T t349 o b333 b348
953 xiny 3379 B b349 t349
954 xiny 3498 T t350 o b331 b349
955 xiny 3379 B b350 t350
956 xiny 3498 T t351 o b329 b350
957 xiny 3379 B b351 t351
958 xiny 3498 T t352 o b327 b351
959 xiny 3379 B b352 t352
960 xiny 3498 T t353 o b325 b352
961 xiny 3379 B b353 t353
962 xiny 3498 T t354 o b323 b353
963 xiny 3379 B b354 t354
964 xiny 3498 T t355 o b321 b354
965 xiny 3379 B b355 t355
966 xiny 3498 T t356 o b319 b355
967 xiny 3379 B b356 t356
968 xiny 3498 T t357 o b317 b356
969 xiny 3404 B b357 t357
970 xiny 3498 T t358 o b315 b357
971 xiny 3379 B b358 t358
972 xiny 3498 T t359 o b313 b358
973     B b359 t359
974     T t360 o b311 b359
975 xiny 3379 B b360 t360
976 xiny 3498 T t361 o b309 b360
977 xiny 3379 B b361 t361
978 xiny 3498 T t362 o b307 b361
979 xiny 3379 B b362 t362
980 xiny 3498 T t363 o b305 b362
981 xiny 3379 B b363 t363
982 xiny 3498 T t364 o b303 b363
983 xiny 3379 B b364 t364
984 xiny 3498 T t365 o b301 b364
985 xiny 3379 B b365 t365
986 xiny 3498 T t366 o2 b301 b365 b296
987 xiny 3379 B b366 t366
988 xiny 3498 T t367 o299 b366
989 xiny 3379 B b367 t367
990 xiny 3498 P p367 Number 46
991     P p368 Number 68
992 xiny 3379 O o368 location p367 p368
993 xiny 3498 P p369 String Czf_itt_member
994     O o369 parent p369
995     T t369 o369
996 xiny 3379 B b369 t369
997 xiny 3498 T t370 o b369 b4
998     B b370 t370
999     P p370 String Czf_itt_eq
1000     O o370 parent p370
1001     T t371 o370
1002 xiny 3379 B b371 t371
1003     T t372 o b371 b4
1004     B b372 t372
1005 xiny 3498 T t373 o b372 b4
1006 xiny 3379 B b373 t373
1007 xiny 3498 T t374 o b370 b373
1008 xiny 3379 B b374 t374
1009 xiny 3498 T t375 o2 b370 b374 b296
1010 xiny 3379 B b375 t375
1011 xiny 3498 T t376 o368 b375
1012 xiny 3379 B b376 t376
1013 xiny 3498 P p376 Number 69
1014     P p377 Number 87
1015     O o377 location p376 p377
1016     T t377 o2 b372 b4 b296
1017 xiny 3379 B b377 t377
1018 xiny 3498 T t378 o377 b377
1019 xiny 3379 B b378 t378
1020 xiny 3498 P p378 Number 88
1021     P p379 Number 108
1022     O o379 location p378 p379
1023     P p380 String Czf_itt_dall
1024     O o380 parent p380
1025     T t380 o380
1026 xiny 3379 B b380 t380
1027 xiny 3498 T t381 o b380 b4
1028 xiny 3379 B b381 t381
1029 xiny 3498 P p381 String Czf_itt_set_ind
1030     O o381 parent p381
1031     T t382 o381
1032 xiny 3379 B b382 t382
1033 xiny 3498 T t383 o b382 b4
1034 xiny 3404 B b383 t383
1035 xiny 3498 P p383 String Czf_itt_all
1036     O o383 parent p383
1037     T t384 o383
1038 xiny 3379 B b384 t384
1039 xiny 3498 T t385 o b384 b4
1040     B b385 t385
1041     P p385 String Czf_itt_sep
1042     O o385 parent p385
1043     T t386 o385
1044 xiny 3379 B b386 t386
1045 xiny 3404 T t387 o b386 b4
1046 xiny 3379 B b387 t387
1047 xiny 3404 T t388 o b387 b4
1048 xiny 3379 B b388 t388
1049 xiny 3498 T t389 o b385 b388
1050 xiny 3404 B b389 t389
1051 xiny 3498 T t390 o b383 b389
1052 xiny 3404 B b390 t390
1053 xiny 3498 T t391 o b381 b390
1054     B b391 t391
1055     T t392 o2 b381 b391 b296
1056     B b392 t392
1057     T t393 o379 b392
1058     B b393 t393
1059     P p393 Number 109
1060     P p394 Number 128
1061     O o394 location p393 p394
1062     P p395 String Czf_itt_and
1063     O o395 parent p395
1064     T t395 o395
1065 xiny 3379 B b395 t395
1066 xiny 3498 T t396 o b395 b4
1067 xiny 3379 B b396 t396
1068 xiny 3498 T t397 o b396 b4
1069 xiny 3404 B b397 t397
1070 xiny 3498 T t398 o2 b396 b397 b296
1071 xiny 3404 B b398 t398
1072 xiny 3498 T t399 o394 b398
1073     B b399 t399
1074 xiny 3527 P p399 Number 129
1075     P p400 Number 150
1076     O o400 location p399 p400
1077     P p401 String Czf_itt_equiv
1078     O o401 parent p401
1079     T t401 o401
1080     B b401 t401
1081     T t402 o b401 b4
1082 xiny 3516 B b402 t402
1083 xiny 3527 P p402 String Czf_itt_pair
1084     O o402 parent p402
1085     T t403 o402
1086 xiny 3379 B b403 t403
1087 xiny 3498 T t404 o b403 b4
1088 xiny 3404 B b404 t404
1089 xiny 3527 P p404 String Czf_itt_singleton
1090     O o404 parent p404
1091     T t405 o404
1092     B b405 t405
1093     T t406 o b405 b4
1094     B b406 t406
1095     P p406 String Czf_itt_union
1096     O o406 parent p406
1097     T t407 o406
1098     B b407 t407
1099     T t408 o b407 b4
1100     B b408 t408
1101     P p408 String Czf_itt_subset
1102     O o408 parent p408
1103     T t409 o408
1104     B b409 t409
1105     T t410 o b409 b4
1106 xiny 3379 B b410 t410
1107 xiny 3527 P p410 String Czf_itt_dexists
1108     O o410 parent p410
1109     T t411 o410
1110 xiny 3379 B b411 t411
1111 xiny 3527 T t412 o b411 b4
1112     B b412 t412
1113     T t413 o b412 b4
1114     B b413 t413
1115     T t414 o b410 b413
1116     B b414 t414
1117     T t415 o b408 b414
1118     B b415 t415
1119     T t416 o b406 b415
1120     B b416 t416
1121     T t417 o b404 b416
1122 xiny 3498 B b417 t417
1123 xiny 3527 T t418 o b402 b417
1124 xiny 3379 B b418 t418
1125 xiny 3527 T t419 o2 b402 b418 b296
1126 xiny 3379 B b419 t419
1127 xiny 3527 T t420 o400 b419
1128 xiny 3379 B b420 t420
1129 xiny 3527 P p420 Number 152
1130     P p421 Number 163
1131     O o421 location p420 p421
1132     NSummary!summary_item summary_item summary_item Summary
1133     O o422 summary_item
1134     NOcaml!str_open str_open str_open Ocaml
1135     O o423 str_open p420 p421
1136     NOcaml!string string string Ocaml
1137     P p423 String Printf
1138     O o424 string p423
1139     T t424 o424
1140     B b424 t424
1141     T t425 o b424 b4
1142     B b425 t425
1143     T t426 o423 b425
1144     B b426 t426
1145     T t427 o422 b426
1146 xiny 3379 B b427 t427
1147 xiny 3527 T t428 o421 b427
1148 xiny 3379 B b428 t428
1149 xiny 3527 P p428 Number 164
1150     P p429 Number 177
1151     O o429 location p428 p429
1152     O o430 str_open p428 p429
1153     P p430 String Mp_debug
1154     O o431 string p430
1155     T t431 o431
1156     B b431 t431
1157     T t432 o b431 b4
1158     B b432 t432
1159     T t433 o430 b432
1160     B b433 t433
1161     T t434 o422 b433
1162     B b434 t434
1163     T t435 o429 b434
1164     B b435 t435
1165     P p435 Number 178
1166     P p436 Number 207
1167     O o436 location p435 p436
1168     O o437 str_open p435 p436
1169     P p437 String Refiner
1170     O o438 string p437
1171     T t438 o438
1172 xiny 3379 B b438 t438
1173 xiny 3527 P p438 String TermType
1174     O o439 string p438
1175     T t439 o439
1176 xiny 3379 B b439 t439
1177 xiny 3527 T t440 o b439 b4
1178     B b440 t440
1179     T t441 o b438 b440
1180     B b441 t441
1181     T t442 o b438 b441
1182     B b442 t442
1183     T t443 o437 b442
1184     B b443 t443
1185     T t444 o422 b443
1186     B b444 t444
1187     T t445 o436 b444
1188 xiny 3379 B b445 t445
1189 xiny 3527 P p445 Number 208
1190     P p446 Number 233
1191     O o446 location p445 p446
1192     O o447 str_open p445 p446
1193     P p447 String Term
1194     O o448 string p447
1195     T t448 o448
1196 xiny 3379 B b448 t448
1197 xiny 3527 T t449 o b448 b4
1198     B b449 t449
1199     T t450 o b438 b449
1200     B b450 t450
1201     T t451 o b438 b450
1202     B b451 t451
1203     T t452 o447 b451
1204     B b452 t452
1205     T t453 o422 b452
1206     B b453 t453
1207     T t454 o446 b453
1208 xiny 3379 B b454 t454
1209 xiny 3527 P p454 Number 234
1210     P p455 Number 261
1211     O o455 location p454 p455
1212     O o456 str_open p454 p455
1213     P p456 String TermOp
1214     O o457 string p456
1215     T t457 o457
1216 xiny 3379 B b457 t457
1217 xiny 3527 T t458 o b457 b4
1218     B b458 t458
1219     T t459 o b438 b458
1220     B b459 t459
1221     T t460 o b438 b459
1222     B b460 t460
1223     T t461 o456 b460
1224     B b461 t461
1225     T t462 o422 b461
1226     B b462 t462
1227     T t463 o455 b462
1228 xiny 3379 B b463 t463
1229 xiny 3527 P p463 Number 262
1230     P p464 Number 291
1231     O o464 location p463 p464
1232     O o465 str_open p463 p464
1233     P p465 String TermAddr
1234     O o466 string p465
1235     T t466 o466
1236 xiny 3379 B b466 t466
1237 xiny 3527 T t467 o b466 b4
1238     B b467 t467
1239     T t468 o b438 b467
1240     B b468 t468
1241     T t469 o b438 b468
1242     B b469 t469
1243     T t470 o465 b469
1244     B b470 t470
1245     T t471 o422 b470
1246     B b471 t471
1247     T t472 o464 b471
1248 xiny 3379 B b472 t472
1249 xiny 3527 P p472 Number 292
1250     P p473 Number 320
1251     O o473 location p472 p473
1252     O o474 str_open p472 p473
1253     P p474 String TermMan
1254     O o475 string p474
1255     T t475 o475
1256 xiny 3379 B b475 t475
1257 xiny 3527 T t476 o b475 b4
1258     B b476 t476
1259     T t477 o b438 b476
1260     B b477 t477
1261     T t478 o b438 b477
1262     B b478 t478
1263     T t479 o474 b478
1264     B b479 t479
1265     T t480 o422 b479
1266     B b480 t480
1267     T t481 o473 b480
1268 xiny 3379 B b481 t481
1269 xiny 3527 P p481 Number 321
1270     P p482 Number 351
1271     O o482 location p481 p482
1272     O o483 str_open p481 p482
1273     P p483 String TermSubst
1274     O o484 string p483
1275     T t484 o484
1276 xiny 3404 B b484 t484
1277 xiny 3527 T t485 o b484 b4
1278     B b485 t485
1279     T t486 o b438 b485
1280     B b486 t486
1281     T t487 o b438 b486
1282     B b487 t487
1283     T t488 o483 b487
1284     B b488 t488
1285     T t489 o422 b488
1286     B b489 t489
1287     T t490 o482 b489
1288 xiny 3379 B b490 t490
1289 xiny 3527 P p490 Number 352
1290     P p491 Number 379
1291     O o491 location p490 p491
1292     O o492 str_open p490 p491
1293     P p492 String Refine
1294     O o493 string p492
1295     T t493 o493
1296     B b493 t493
1297     T t494 o b493 b4
1298     B b494 t494
1299     T t495 o b438 b494
1300     B b495 t495
1301     T t496 o b438 b495
1302     B b496 t496
1303     T t497 o492 b496
1304 xiny 3379 B b497 t497
1305 xiny 3527 T t498 o422 b497
1306 xiny 3404 B b498 t498
1307 xiny 3527 T t499 o491 b498
1308     B b499 t499
1309     P p499 Number 380
1310     P p500 Number 412
1311     O o500 location p499 p500
1312     O o501 str_open p499 p500
1313     P p501 String RefineError
1314     O o502 string p501
1315     T t502 o502
1316     B b502 t502
1317     T t503 o b502 b4
1318     B b503 t503
1319     T t504 o b438 b503
1320 xiny 3379 B b504 t504
1321 xiny 3527 T t505 o b438 b504
1322 xiny 3379 B b505 t505
1323 xiny 3527 T t506 o501 b505
1324     B b506 t506
1325     T t507 o422 b506
1326     B b507 t507
1327     T t508 o500 b507
1328     B b508 t508
1329     P p508 Number 413
1330     P p509 Number 429
1331     O o509 location p508 p509
1332     O o510 str_open p508 p509
1333     P p510 String Mp_resource
1334 xiny 3498 O o511 string p510
1335     T t511 o511
1336 xiny 3379 B b511 t511
1337 xiny 3498 T t512 o b511 b4
1338 xiny 3379 B b512 t512
1339 xiny 3527 T t513 o510 b512
1340 xiny 3379 B b513 t513
1341 xiny 3527 T t514 o422 b513
1342     B b514 t514
1343     T t515 o509 b514
1344     B b515 t515
1345     P p515 Number 430
1346     P p516 Number 447
1347     O o516 location p515 p516
1348     O o517 str_open p515 p516
1349     P p517 String Simple_print
1350     O o518 string p517
1351     T t518 o518
1352     B b518 t518
1353     T t519 o b518 b4
1354 xiny 3379 B b519 t519
1355 xiny 3527 T t520 o517 b519
1356 xiny 3379 B b520 t520
1357 xiny 3527 T t521 o422 b520
1358 xiny 3379 B b521 t521
1359 xiny 3527 T t522 o516 b521
1360     B b522 t522
1361     P p522 Number 449
1362     P p523 Number 465
1363     O o523 location p522 p523
1364     O o524 str_open p522 p523
1365     P p524 String Tactic_type
1366     O o525 string p524
1367     T t525 o525
1368     B b525 t525
1369     T t526 o b525 b4
1370     B b526 t526
1371     T t527 o524 b526
1372 xiny 3379 B b527 t527
1373 xiny 3527 T t528 o422 b527
1374 xiny 3379 B b528 t528
1375 xiny 3527 T t529 o523 b528
1376 xiny 3404 B b529 t529
1377 xiny 3527 P p529 Number 466
1378     P p530 Number 492
1379     O o530 location p529 p530
1380     O o531 str_open p529 p530
1381     P p531 String Tacticals
1382     O o532 string p531
1383     T t532 o532
1384     B b532 t532
1385     T t533 o b532 b4
1386     B b533 t533
1387     T t534 o b525 b533
1388     B b534 t534
1389     T t535 o531 b534
1390 xiny 3379 B b535 t535
1391 xiny 3527 T t536 o422 b535
1392 xiny 3404 B b536 t536
1393 xiny 3527 T t537 o530 b536
1394     B b537 t537
1395     P p537 Number 493
1396     P p538 Number 517
1397     O o538 location p537 p538
1398     O o539 str_open p537 p538
1399     P p539 String Sequent
1400     O o540 string p539
1401     T t540 o540
1402     B b540 t540
1403     T t541 o b540 b4
1404     B b541 t541
1405     T t542 o b525 b541
1406 xiny 3379 B b542 t542
1407 xiny 3527 T t543 o539 b542
1408 xiny 3404 B b543 t543
1409 xiny 3527 T t544 o422 b543
1410     B b544 t544
1411     T t545 o538 b544
1412     B b545 t545
1413     P p545 Number 518
1414 xiny 3498 P p546 Number 548
1415 xiny 3527 O o546 location p545 p546
1416     O o547 str_open p545 p546
1417     P p547 String Conversionals
1418     O o548 string p547
1419     T t548 o548
1420     B b548 t548
1421     T t549 o b548 b4
1422 xiny 3379 B b549 t549
1423 xiny 3527 T t550 o b525 b549
1424 xiny 3404 B b550 t550
1425 xiny 3527 T t551 o547 b550
1426     B b551 t551
1427     T t552 o422 b551
1428     B b552 t552
1429     T t553 o546 b552
1430     B b553 t553
1431     P p553 Number 549
1432     P p554 Number 559
1433     O o554 location p553 p554
1434     O o555 str_open p553 p554
1435     O o556 string p91
1436 xiny 3498 T t556 o556
1437     B b556 t556
1438     T t557 o b556 b4
1439     B b557 t557
1440 xiny 3527 T t558 o555 b557
1441     B b558 t558
1442     T t559 o422 b558
1443     B b559 t559
1444     T t560 o554 b559
1445     B b560 t560
1446     P p560 Number 560
1447     P p561 Number 568
1448     O o561 location p560 p561
1449     O o562 str_open p560 p561
1450     O o563 string p89
1451     T t563 o563
1452     B b563 t563
1453     T t564 o b563 b4
1454 xiny 3404 B b564 t564
1455 xiny 3527 T t565 o562 b564
1456 xiny 3498 B b565 t565
1457 xiny 3527 T t566 o422 b565
1458 xiny 3498 B b566 t566
1459 xiny 3527 T t567 o561 b566
1460     B b567 t567
1461     P p567 Number 570
1462     P p568 Number 587
1463     O o568 location p567 p568
1464     O o569 str_open p567 p568
1465     O o570 string p79
1466     T t570 o570
1467 xiny 3498 B b570 t570
1468 xiny 3527 T t571 o b570 b4
1469 xiny 3498 B b571 t571
1470 xiny 3527 T t572 o569 b571
1471     B b572 t572
1472     T t573 o422 b572
1473     B b573 t573
1474     T t574 o568 b573
1475     B b574 t574
1476     P p574 Number 588
1477     P p575 Number 609
1478     O o575 location p574 p575
1479     O o576 str_open p574 p575
1480     O o577 string p81
1481 xiny 3498 T t577 o577
1482     B b577 t577
1483 xiny 3527 T t578 o b577 b4
1484 xiny 3498 B b578 t578
1485 xiny 3527 T t579 o576 b578
1486     B b579 t579
1487     T t580 o422 b579
1488     B b580 t580
1489     T t581 o575 b580
1490     B b581 t581
1491     P p581 Number 611
1492     P p582 Number 628
1493     O o582 location p581 p582
1494     NSummary!opname opname opname Summary
1495     P p583 String group
1496     O o583 opname p583
1497     NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1498     NCzf_itt_group!group group group Czf_itt_group
1499     O o584 group
1500     Nvar var var NIL
1501     P p584 Var g
1502     O o585 var p584
1503     T t585 o585
1504     B b585 t585
1505     T t586 o584 b585
1506     B b586 t586
1507     T t587 o583 b586
1508     B b587 t587
1509     T t588 o582 b587
1510     B b588 t588
1511     P p588 Number 629
1512     P p589 Number 644
1513     O o589 location p588 p589
1514     P p590 String car
1515     O o590 opname p590
1516     NCzf_itt_group!car car car Czf_itt_group
1517     O o591 car
1518     T t591 o591 b585
1519     B b591 t591
1520     T t592 o590 b591
1521     B b592 t592
1522     T t593 o589 b592
1523     B b593 t593
1524     P p593 Number 685
1525     P p594 Number 707
1526     O o594 location p593 p594
1527     P p595 String op
1528     O o595 opname p595
1529     NCzf_itt_group!op op op Czf_itt_group
1530     O o596 op
1531     P p596 Var a
1532     O o597 var p596
1533     T t597 o597
1534     B b597 t597
1535     P p597 Var b
1536     O o598 var p597
1537     T t598 o598
1538     B b598 t598
1539     T t599 o596 b585 b597 b598
1540     B b599 t599
1541     T t600 o595 b599
1542 xiny 3379 B b600 t600
1543 xiny 3527 T t601 o594 b600
1544 xiny 3379 B b601 t601
1545 xiny 3527 P p601 Number 708
1546     P p602 Number 722
1547     O o602 location p601 p602
1548     P p603 String id
1549     O o603 opname p603
1550     NCzf_itt_group!id id id Czf_itt_group
1551     O o604 id
1552     T t604 o604 b585
1553 xiny 3379 B b604 t604
1554 xiny 3527 T t605 o603 b604
1555 xiny 3404 B b605 t605
1556 xiny 3527 T t606 o602 b605
1557 xiny 3379 B b606 t606
1558 xiny 3527 P p606 Number 723
1559     P p607 Number 742
1560     O o607 location p606 p607
1561     P p608 String inv
1562     O o608 opname p608
1563     NCzf_itt_group!inv inv inv Czf_itt_group
1564     O o609 inv
1565     T t609 o609 b585 b597
1566     B b609 t609
1567     T t610 o608 b609
1568     B b610 t610
1569     T t611 o607 b610
1570 xiny 3379 B b611 t611
1571 xiny 3527 P p611 Number 744
1572     P p612 Number 756
1573     O o612 location p611 p612
1574     NSummary!prec prec prec Summary
1575     P p613 String prec_op
1576     O o613 prec p613
1577     T t613 o613
1578 xiny 3404 B b613 t613
1579 xiny 3527 T t614 o612 b613
1580 xiny 3404 B b614 t614
1581 xiny 3527 P p614 Number 758
1582     P p615 Number 828
1583     O o615 location p614 p615
1584     NSummary!dform dform dform Summary
1585     P p616 String group_df
1586     O o616 dform p616
1587     NSummary!except_mode_df except_mode_df except_mode_df Summary
1588     P p617 String src
1589     O o617 except_mode_df p617
1590     T t617 o617
1591 xiny 3379 B b617 t617
1592 xiny 3527 T t618 o b617 b4
1593     B b618 t618
1594     NSummary!df_term df_term df_term Summary
1595     O o618 df_term
1596     Nslot slot slot NIL
1597     O o619 slot
1598     T t619 o619 b585
1599     B b619 t619
1600     NPerv!string string619 string Perv
1601     P p619 String " group"
1602     O o620 string619 p619
1603     T t620 o620
1604     B b620 t620
1605     T t621 o b620 b4
1606 xiny 3498 B b621 t621
1607 xiny 3527 T t622 o b619 b621
1608 xiny 3404 B b622 t622
1609 xiny 3527 T t623 o618 b622
1610 xiny 3404 B b623 t623
1611 xiny 3527 T t624 o616 b618 b586 b623
1612 xiny 3498 B b624 t624
1613 xiny 3527 T t625 o615 b624
1614     B b625 t625
1615     P p625 Number 830
1616     P p626 Number 899
1617     O o626 location p625 p626
1618     P p627 String car_df
1619 xiny 3498 O o627 dform p627
1620 xiny 3527 P p628 String car(
1621     O o628 string619 p628
1622 xiny 3498 T t628 o628
1623     B b628 t628
1624 xiny 3527 P p629 String )
1625     O o629 string619 p629
1626     T t629 o629
1627 xiny 3498 B b629 t629
1628 xiny 3527 T t630 o b629 b4
1629 xiny 3498 B b630 t630
1630 xiny 3527 T t631 o b619 b630
1631 xiny 3498 B b631 t631
1632 xiny 3527 T t632 o b628 b631
1633 xiny 3498 B b632 t632
1634 xiny 3527 T t633 o618 b632
1635     B b633 t633
1636     T t634 o627 b618 b591 b633
1637     B b634 t634
1638     T t635 o626 b634
1639     B b635 t635
1640     P p635 Number 901
1641     P p636 Number 967
1642     O o636 location p635 p636
1643     P p637 String id_df
1644     O o637 dform p637
1645     P p638 String id(
1646     O o638 string619 p638
1647     T t638 o638
1648     B b638 t638
1649     T t639 o b638 b631
1650     B b639 t639
1651     T t640 o618 b639
1652     B b640 t640
1653     T t641 o637 b618 b604 b640
1654     B b641 t641
1655     T t642 o636 b641
1656     B b642 t642
1657     P p642 Number 969
1658     P p643 Number 1103
1659     O o643 location p642 p643
1660     P p644 String op_df
1661     O o644 dform p644
1662     NSummary!prec_df prec_df prec_df Summary
1663     O o645 prec_df p613
1664     T t645 o645
1665     B b645 t645
1666     NSummary!parens_df parens_df parens_df Summary
1667     O o646 parens_df
1668 xiny 3498 T t646 o646
1669     B b646 t646
1670 xiny 3527 T t647 o b646 b4
1671     B b647 t647
1672     T t648 o b645 b647
1673     B b648 t648
1674     T t649 o b617 b648
1675     B b649 t649
1676     P p649 String op(
1677     O o649 string619 p649
1678     T t650 o649
1679     B b650 t650
1680     P p650 String "; "
1681     O o650 string619 p650
1682     T t651 o650
1683     B b651 t651
1684     T t652 o619 b597
1685     B b652 t652
1686     T t653 o619 b598
1687     B b653 t653
1688     T t654 o b653 b630
1689     B b654 t654
1690     T t655 o b651 b654
1691     B b655 t655
1692     T t656 o b652 b655
1693     B b656 t656
1694     T t657 o b651 b656
1695     B b657 t657
1696     T t658 o b619 b657
1697     B b658 t658
1698     T t659 o b650 b658
1699     B b659 t659
1700     T t660 o618 b659
1701     B b660 t660
1702     T t661 o644 b649 b599 b660
1703     B b661 t661
1704     T t662 o643 b661
1705     B b662 t662
1706     P p662 Number 1105
1707     P p663 Number 1203
1708     O o663 location p662 p663
1709     P p664 String inv_df
1710     O o664 dform p664
1711     T t664 o b617 b647
1712     B b664 t664
1713     P p665 String inv(
1714     O o665 string619 p665
1715     T t665 o665
1716     B b665 t665
1717     T t666 o b652 b630
1718     B b666 t666
1719     T t667 o b651 b666
1720     B b667 t667
1721     T t668 o b619 b667
1722     B b668 t668
1723     T t669 o b665 b668
1724     B b669 t669
1725     T t670 o618 b669
1726     B b670 t670
1727     T t671 o664 b664 b609 b670
1728     B b671 t671
1729     T t672 o663 b671
1730     B b672 t672
1731     P p672 Number 1222
1732     P p673 Number 1356
1733     O o673 location p672 p673
1734 xiny 3498 NSummary!rule rule rule Summary
1735 xiny 3527 P p674 String group_type
1736     O o674 rule p674
1737 xiny 3498 NSummary!context_param context_param context_param Summary
1738 xiny 3527 P p675 String H
1739     O o675 context_param p675
1740     T t675 o675
1741     B b675 t675
1742     T t676 o b675 b4
1743     B b676 t676
1744 xiny 3498 NSummary!meta_implies meta_implies meta_implies Summary
1745 xiny 3527 O o676 meta_implies
1746 xiny 3498 NSummary!meta_theorem meta_theorem meta_theorem Summary
1747 xiny 3527 O o677 meta_theorem
1748 xiny 3498 NBase_trivial Base_trivial Base_trivial NIL
1749     NBase_trivial!squash squash squash Base_trivial
1750 xiny 3527 O o678 squash
1751     T t678 o678
1752     B b678 t678
1753     T t679 o b678 b4
1754 xiny 3498 C h H
1755     NItt_equal Itt_equal Itt_equal NIL
1756     NItt_equal!equal equal equal Itt_equal
1757 xiny 3527 O o679 equal
1758 xiny 3498 NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1759     NItt_record_label0!label label label Itt_record_label0
1760 xiny 3527 O o680 label
1761     T t680 o680
1762     B b680 t680
1763     T t681 o679 b680 b585 b585
1764     S s t679 h
1765     G s t681
1766     B b681 s
1767     T t682 o677 b681
1768     B b682 t682
1769     P p682 Var ext
1770     O o682 var p682
1771     T t683 o682
1772     B b683 t683
1773     T t684 o b683 b4
1774 xiny 3498 NItt_equal!type type type Itt_equal
1775 xiny 3527 O o684 type
1776     T t685 o684 b586
1777     S s685 t684 h
1778     G s685 t685
1779     B b685 s685
1780     T t686 o677 b685
1781     B b686 t686
1782     T t687 o676 b682 b686
1783     B b687 t687
1784 xiny 3498 NSummary!incomplete incomplete incomplete Summary
1785 xiny 3527 O o687 incomplete
1786     T t688 o687
1787     B b688 t688
1788 xiny 3498 NSummary!resource_defs resource_defs resource_defs Summary
1789 xiny 3527 P p688 Number 1248
1790     P p689 Number 1256
1791     O o689 resource_defs p688 p689 p204
1792 xiny 3498 NOcaml!uid uid uid Ocaml
1793 xiny 3527 P p690 Number 1254
1794     O o690 uid p690 p689
1795     P p691 String []
1796     O o691 uid p691
1797     T t691 o691
1798     B b691 t691
1799     T t692 o690 b691
1800     B b692 t692
1801     T t693 o b692 b4
1802     B b693 t693
1803     T t694 o689 b693
1804     B b694 t694
1805     T t695 o b694 b4
1806     B b695 t695
1807     T t696 o674 b676 b687 b688 b695
1808     B b696 t696
1809     T t697 o673 b696
1810     B b697 t697
1811     P p697 Number 1358
1812     P p698 Number 1526
1813     O o698 location p697 p698
1814     P p699 String car_wf
1815     O o699 rule p699
1816     S s699 t684 h
1817     G s699 t586
1818     B b699 s699
1819     T t699 o677 b699
1820     B b700 t699
1821 xiny 3498 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1822     NCzf_itt_set!isset isset isset Czf_itt_set
1823 xiny 3527 O o700 isset
1824     T t700 o700 b591
1825     S s700 t684 h
1826     G s700 t700
1827     B b701 s700
1828     T t701 o677 b701
1829     B b702 t701
1830     T t702 o676 b700 b702
1831     B b703 t702
1832     T t703 o676 b682 b703
1833     B b704 t703
1834     P p704 Number 1380
1835     P p705 Number 1387
1836     O o705 resource_defs p704 p705 p204
1837     P p706 Number 1385
1838     O o706 uid p706 p705
1839     T t706 o706 b691
1840     B b706 t706
1841     T t707 o b706 b4
1842 xiny 3494 B b707 t707
1843 xiny 3527 T t708 o705 b707
1844 xiny 3494 B b708 t708
1845 xiny 3527 T t709 o b708 b4
1846 xiny 3498 B b709 t709
1847 xiny 3527 T t710 o699 b676 b704 b688 b709
1848 xiny 3498 B b710 t710
1849 xiny 3527 T t711 o698 b710
1850 xiny 3498 B b711 t711
1851 xiny 3527 P p711 Number 1528
1852     P p712 Number 1795
1853     O o712 location p711 p712
1854     P p713 String op_wf1
1855     O o713 rule p713
1856     P p714 Var s1
1857     O o714 var p714
1858     T t714 o714
1859     B b714 t714
1860     T t715 o700 b714
1861     S s715 t679 h
1862     G s715 t715
1863     B b715 s715
1864     T t716 o677 b715
1865     B b716 t716
1866     P p716 Var s2
1867     O o716 var p716
1868     T t717 o716
1869     B b717 t717
1870     T t718 o700 b717
1871     S s718 t679 h
1872     G s718 t718
1873     B b718 s718
1874     T t719 o677 b718
1875     B b719 t719
1876     T t720 o596 b585 b714 b717
1877     B b720 t720
1878     T t721 o700 b720
1879     S s721 t684 h
1880 xiny 3498 G s721 t721
1881     B b721 s721
1882 xiny 3527 T t722 o677 b721
1883 xiny 3494 B b722 t722
1884 xiny 3527 T t723 o676 b719 b722
1885     B b723 t723
1886     T t724 o676 b716 b723
1887 xiny 3498 B b724 t724
1888 xiny 3527 T t725 o676 b700 b724
1889     B b725 t725
1890     T t726 o676 b682 b725
1891 xiny 3498 B b726 t726
1892 xiny 3527 P p726 Number 1550
1893     P p727 Number 1557
1894     O o727 resource_defs p726 p727 p204
1895     P p728 Number 1555
1896     O o728 uid p728 p727
1897     T t728 o728 b691
1898 xiny 3498 B b728 t728
1899 xiny 3527 T t729 o b728 b4
1900 xiny 3498 B b729 t729
1901 xiny 3527 T t730 o727 b729
1902 xiny 3494 B b730 t730
1903 xiny 3527 T t731 o b730 b4
1904 xiny 3494 B b731 t731
1905 xiny 3527 T t732 o713 b676 b726 b688 b731
1906 xiny 3494 B b732 t732
1907 xiny 3527 T t733 o712 b732
1908     B b733 t733
1909     P p733 Number 1797
1910     P p734 Number 2171
1911     O o734 location p733 p734
1912     P p735 String op_wf2
1913     O o735 rule p735
1914     NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1915     NCzf_itt_member!mem mem mem Czf_itt_member
1916     O o736 mem
1917     T t736 o736 b714 b591
1918     S s736 t684 h
1919     G s736 t736
1920     B b736 s736
1921     T t737 o677 b736
1922     B b737 t737
1923     T t738 o736 b717 b591
1924     S s738 t684 h
1925     G s738 t738
1926     B b738 s738
1927     T t739 o677 b738
1928     B b739 t739
1929     T t740 o736 b720 b591
1930     S s740 t684 h
1931     G s740 t740
1932     B b740 s740
1933     T t741 o677 b740
1934     B b741 t741
1935     T t742 o676 b739 b741
1936 xiny 3498 B b742 t742
1937 xiny 3527 T t743 o676 b737 b742
1938     B b743 t743
1939     T t744 o676 b700 b743
1940 xiny 3498 B b744 t744
1941 xiny 3527 T t745 o676 b682 b744
1942     B b745 t745
1943     T t746 o676 b719 b745
1944     B b746 t746
1945     T t747 o676 b716 b746
1946 xiny 3498 B b747 t747
1947 xiny 3527 P p747 Number 1826
1948     O o747 resource_defs p207 p747 p204
1949     P p748 Number 1824
1950     O o748 uid p748 p747
1951     T t748 o748 b691
1952 xiny 3498 B b748 t748
1953 xiny 3527 T t749 o b748 b4
1954     B b749 t749
1955     T t750 o747 b749
1956     B b750 t750
1957     T t751 o b750 b4
1958     B b751 t751
1959     T t752 o735 b676 b747 b688 b751
1960     B b752 t752
1961     T t753 o734 b752
1962     B b753 t753
1963     P p753 Number 2173
1964     P p754 Number 2825
1965     O o754 location p753 p754
1966     P p755 String op_equiv1
1967     O o755 rule p755
1968     P p756 Var s3
1969     O o756 var p756
1970     T t756 o756
1971     B b756 t756
1972     T t757 o700 b756
1973     S s757 t679 h
1974     G s757 t757
1975     B b757 s757
1976     T t758 o677 b757
1977     B b758 t758
1978     P p758 Var R
1979     O o758 var p758
1980     T t759 o758
1981     B b759 t759
1982     T t760 o700 b759
1983     S s760 t679 h
1984     G s760 t760
1985     B b760 s760
1986     T t761 o677 b760
1987     B b761 t761
1988     NCzf_itt_equiv Czf_itt_equiv Czf_itt_equiv NIL
1989     NCzf_itt_equiv!equiv equiv equiv Czf_itt_equiv
1990     O o761 equiv
1991     T t762 o761 b591 b759
1992     S s762 t684 h
1993     G s762 t762
1994     B b762 s762
1995     T t763 o677 b762
1996     B b763 t763
1997     T t764 o736 b756 b591
1998     S s764 t684 h
1999     G s764 t764
2000     B b764 s764
2001     T t765 o677 b764
2002 xiny 3498 B b765 t765
2003 xiny 3527 T t766 o761 b591 b759 b714 b717
2004     S s766 t684 h
2005     G s766 t766
2006     B b766 s766
2007     T t767 o677 b766
2008     B b767 t767
2009     T t768 o596 b585 b756 b714
2010     B b768 t768
2011     T t769 o596 b585 b756 b717
2012     B b769 t769
2013     T t770 o761 b591 b759 b768 b769
2014     S s770 t684 h
2015     G s770 t770
2016     B b770 s770
2017     T t771 o677 b770
2018     B b771 t771
2019     T t772 o676 b767 b771
2020     B b772 t772
2021     T t773 o676 b765 b772
2022     B b773 t773
2023     T t774 o676 b739 b773
2024     B b774 t774
2025     T t775 o676 b737 b774
2026     B b775 t775
2027     T t776 o676 b763 b775
2028     B b776 t776
2029     T t777 o676 b700 b776
2030     B b777 t777
2031     T t778 o676 b682 b777
2032     B b778 t778
2033     T t779 o676 b761 b778
2034     B b779 t779
2035     T t780 o676 b758 b779
2036     B b780 t780
2037     T t781 o676 b719 b780
2038     B b781 t781
2039     T t782 o676 b716 b781
2040     B b782 t782
2041     P p782 Number 2198
2042     P p783 Number 2205
2043     O o783 resource_defs p782 p783 p204
2044     P p784 Number 2203
2045     O o784 uid p784 p783
2046     T t784 o784 b691
2047 xiny 3405 B b784 t784
2048 xiny 3527 T t785 o b784 b4
2049 xiny 3498 B b785 t785
2050 xiny 3527 T t786 o783 b785
2051     B b786 t786
2052     T t787 o b786 b4
2053     B b787 t787
2054     T t788 o755 b676 b782 b688 b787
2055 xiny 3498 B b788 t788
2056 xiny 3527 T t789 o754 b788
2057 xiny 3498 B b789 t789
2058 xiny 3527 P p789 Number 2827
2059     P p790 Number 3479
2060     O o790 location p789 p790
2061     P p791 String op_equiv2
2062     O o791 rule p791
2063     T t791 o596 b585 b714 b756
2064     B b791 t791
2065     T t792 o596 b585 b717 b756
2066     B b792 t792
2067     T t793 o761 b591 b759 b791 b792
2068     S s793 t684 h
2069     G s793 t793
2070     B b793 s793
2071     T t794 o677 b793
2072     B b794 t794
2073     T t795 o676 b767 b794
2074     B b795 t795
2075     T t796 o676 b765 b795
2076     B b796 t796
2077     T t797 o676 b739 b796
2078     B b797 t797
2079     T t798 o676 b737 b797
2080     B b798 t798
2081     T t799 o676 b763 b798
2082     B b799 t799
2083     T t800 o676 b700 b799
2084 xiny 3498 B b800 t800
2085 xiny 3527 T t801 o676 b682 b800
2086 xiny 3494 B b801 t801
2087 xiny 3527 T t802 o676 b761 b801
2088     B b802 t802
2089     T t803 o676 b758 b802
2090     B b803 t803
2091     T t804 o676 b719 b803
2092     B b804 t804
2093     T t805 o676 b716 b804
2094     B b805 t805
2095     P p805 Number 2852
2096     P p806 Number 2859
2097     O o806 resource_defs p805 p806 p204
2098     P p807 Number 2857
2099     O o807 uid p807 p806
2100     T t807 o807 b691
2101     B b807 t807
2102     T t808 o b807 b4
2103     B b808 t808
2104     T t809 o806 b808
2105     B b809 t809
2106     T t810 o b809 b4
2107     B b810 t810
2108     T t811 o791 b676 b805 b688 b810
2109 xiny 3498 B b811 t811
2110 xiny 3527 T t812 o790 b811
2111 xiny 3498 B b812 t812
2112 xiny 3527 P p812 Number 3481
2113     P p813 Number 3826
2114     O o813 location p812 p813
2115     P p814 String op_equiv_fun1
2116     O o814 rule p814
2117     P p815 Var s
2118     O o815 var p815
2119     T t815 o815
2120     B b815 t815
2121     T t816 o700 b815
2122     S s816 t679 h
2123     G s816 t816
2124     B b816 s816
2125     T t817 o677 b816
2126     B b817 t817
2127     NCzf_itt_equiv!equiv_fun_set equiv_fun_set equiv_fun_set Czf_itt_equiv
2128     O o817 equiv_fun_set
2129     P p817 Var z
2130     O o818 var p817
2131     T t818 o818
2132     B b818 t818
2133     T t819 o596 b585 b818 b815
2134     B b819 t819 z
2135     T t820 o817 b591 b759 b819
2136     S s820 t684 h
2137     G s820 t820
2138     B b820 s820
2139     T t821 o677 b820
2140     B b821 t821
2141     T t822 o676 b763 b821
2142     B b822 t822
2143     T t823 o676 b700 b822
2144     B b823 t823
2145     T t824 o676 b682 b823
2146     B b824 t824
2147     T t825 o676 b761 b824
2148     B b825 t825
2149     T t826 o676 b817 b825
2150     B b826 t826
2151     P p826 Number 3510
2152     P p827 Number 3517
2153     O o827 resource_defs p826 p827 p204
2154     P p828 Number 3515
2155     O o828 uid p828 p827
2156     T t828 o828 b691
2157     B b828 t828
2158     T t829 o b828 b4
2159     B b829 t829
2160     T t830 o827 b829
2161     B b830 t830
2162     T t831 o b830 b4
2163     B b831 t831
2164     T t832 o814 b676 b826 b688 b831
2165     B b832 t832
2166     T t833 o813 b832
2167     B b833 t833
2168     P p833 Number 3828
2169     P p834 Number 4173
2170     O o834 location p833 p834
2171     P p835 String op_equiv_fun2
2172     O o835 rule p835
2173     T t835 o596 b585 b815 b818
2174     B b835 t835 z
2175     T t836 o817 b591 b759 b835
2176     S s836 t684 h
2177     G s836 t836
2178     B b836 s836
2179     T t837 o677 b836
2180     B b837 t837
2181     T t838 o676 b763 b837
2182     B b838 t838
2183     T t839 o676 b700 b838
2184     B b839 t839
2185     T t840 o676 b682 b839
2186     B b840 t840
2187     T t841 o676 b761 b840
2188     B b841 t841
2189     T t842 o676 b817 b841
2190     B b842 t842
2191     P p842 Number 3857
2192     P p843 Number 3864
2193     O o843 resource_defs p842 p843 p204
2194     P p844 Number 3862
2195     O o844 uid p844 p843
2196     T t844 o844 b691
2197     B b844 t844
2198     T t845 o b844 b4
2199     B b845 t845
2200     T t846 o843 b845
2201     B b846 t846
2202     T t847 o b846 b4
2203     B b847 t847
2204     T t848 o835 b676 b842 b688 b847
2205     B b848 t848
2206     T t849 o834 b848
2207     B b849 t849
2208     P p849 Number 4175
2209     P p850 Number 4403
2210     O o850 location p849 p850
2211     P p851 String op_eq_fun1
2212     O o851 rule p851
2213     NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
2214     NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
2215     O o852 fun_set
2216     T t852 o852 b819
2217     S s852 t684 h
2218     G s852 t852
2219     B b852 s852
2220     T t853 o677 b852
2221 xiny 3498 B b853 t853
2222 xiny 3527 T t854 o676 b700 b853
2223     B b854 t854
2224     T t855 o676 b682 b854
2225     B b855 t855
2226     T t856 o676 b817 b855
2227     B b856 t856
2228     P p856 Number 4201
2229     P p857 Number 4208
2230     O o857 resource_defs p856 p857 p204
2231     P p858 Number 4206
2232     O o858 uid p858 p857
2233     T t858 o858 b691
2234     B b858 t858
2235     T t859 o b858 b4
2236     B b859 t859
2237     T t860 o857 b859
2238     B b860 t860
2239     T t861 o b860 b4
2240     B b861 t861
2241     T t862 o851 b676 b856 b688 b861
2242     B b862 t862
2243     T t863 o850 b862
2244 xiny 3494 B b863 t863
2245 xiny 3527 P p863 Number 4405
2246     P p864 Number 4633
2247     O o864 location p863 p864
2248     P p865 String op_eq_fun2
2249     O o865 rule p865
2250     T t865 o852 b835
2251     S s865 t684 h
2252     G s865 t865
2253     B b865 s865
2254     T t866 o677 b865
2255     B b866 t866
2256     T t867 o676 b700 b866
2257     B b867 t867
2258     T t868 o676 b682 b867
2259     B b868 t868
2260     T t869 o676 b817 b868
2261     B b869 t869
2262     P p869 Number 4431
2263     P p870 Number 4438
2264     O o870 resource_defs p869 p870 p204
2265     P p871 Number 4436
2266     O o871 uid p871 p870
2267     T t871 o871 b691
2268     B b871 t871
2269     T t872 o b871 b4
2270     B b872 t872
2271     T t873 o870 b872
2272     B b873 t873
2273     T t874 o b873 b4
2274     B b874 t874
2275     T t875 o865 b676 b869 b688 b874
2276 xiny 3494 B b875 t875
2277 xiny 3527 T t876 o864 b875
2278 xiny 3494 B b876 t876
2279 xiny 3527 P p876 Number 4635
2280     P p877 Number 5252
2281     O o877 location p876 p877
2282     P p878 String op_assoc1
2283     O o878 rule p878
2284     T t878 o596 b585 b720 b756
2285     B b878 t878
2286     T t879 o596 b585 b714 b792
2287     B b879 t879
2288     T t880 o761 b591 b759 b878 b879
2289     S s880 t684 h
2290     G s880 t880
2291     B b880 s880
2292     T t881 o677 b880
2293     B b881 t881
2294     T t882 o676 b765 b881
2295     B b882 t882
2296     T t883 o676 b739 b882
2297     B b883 t883
2298     T t884 o676 b737 b883
2299     B b884 t884
2300     T t885 o676 b763 b884
2301     B b885 t885
2302     T t886 o676 b700 b885
2303     B b886 t886
2304     T t887 o676 b682 b886
2305     B b887 t887
2306     T t888 o676 b761 b887
2307     B b888 t888
2308     T t889 o676 b758 b888
2309     B b889 t889
2310     T t890 o676 b719 b889
2311     B b890 t890
2312     T t891 o676 b716 b890
2313 xiny 3498 B b891 t891
2314 xiny 3527 P p891 Number 4660
2315     P p892 Number 4667
2316     O o892 resource_defs p891 p892 p204
2317     P p893 Number 4665
2318     O o893 uid p893 p892
2319     T t893 o893 b691
2320     B b893 t893
2321     T t894 o b893 b4
2322     B b894 t894
2323     T t895 o892 b894
2324     B b895 t895
2325     T t896 o b895 b4
2326     B b896 t896
2327     T t897 o878 b676 b891 b688 b896
2328     B b897 t897
2329     T t898 o877 b897
2330     B b898 t898
2331     P p898 Number 5254
2332     P p899 Number 5871
2333     O o899 location p898 p899
2334     P p900 String op_assoc2
2335     O o900 rule p900
2336     T t900 o761 b591 b759 b879 b878
2337     S s900 t684 h
2338     G s900 t900
2339     B b900 s900
2340     T t901 o677 b900
2341     B b901 t901
2342     T t902 o676 b765 b901
2343     B b902 t902
2344     T t903 o676 b739 b902
2345     B b903 t903
2346     T t904 o676 b737 b903
2347     B b904 t904
2348     T t905 o676 b763 b904
2349     B b905 t905
2350     T t906 o676 b700 b905
2351 xiny 3405 B b906 t906
2352 xiny 3527 T t907 o676 b682 b906
2353     B b907 t907
2354     T t908 o676 b761 b907
2355 xiny 3405 B b908 t908
2356 xiny 3527 T t909 o676 b758 b908
2357 xiny 3379 B b909 t909
2358 xiny 3527 T t910 o676 b719 b909
2359 xiny 3404 B b910 t910
2360 xiny 3527 T t911 o676 b716 b910
2361 xiny 3498 B b911 t911
2362 xiny 3527 P p911 Number 5279
2363     P p912 Number 5286
2364     O o912 resource_defs p911 p912 p204
2365     P p913 Number 5284
2366     O o913 uid p913 p912
2367     T t913 o913 b691
2368     B b913 t913
2369     T t914 o b913 b4
2370     B b914 t914
2371     T t915 o912 b914
2372     B b915 t915
2373     T t916 o b915 b4
2374     B b916 t916
2375     T t917 o900 b676 b911 b688 b916
2376     B b917 t917
2377     T t918 o899 b917
2378     B b918 t918
2379     P p918 Number 5873
2380     P p919 Number 6041
2381     O o919 location p918 p919
2382     P p920 String id_wf1
2383     O o920 rule p920
2384     T t920 o700 b604
2385     S s920 t684 h
2386     G s920 t920
2387     B b920 s920
2388     T t921 o677 b920
2389     B b921 t921
2390     T t922 o676 b700 b921
2391 xiny 3379 B b922 t922
2392 xiny 3527 T t923 o676 b682 b922
2393 xiny 3498 B b923 t923
2394 xiny 3527 P p923 Number 5895
2395     P p924 Number 5903
2396     O o924 resource_defs p923 p924 p204
2397     P p925 Number 5901
2398     O o925 uid p925 p924
2399     T t925 o925 b691
2400 xiny 3498 B b925 t925
2401 xiny 3527 T t926 o b925 b4
2402 xiny 3405 B b926 t926
2403 xiny 3527 T t927 o924 b926
2404     B b927 t927
2405     T t928 o b927 b4
2406     B b928 t928
2407     T t929 o920 b676 b923 b688 b928
2408     B b929 t929
2409     T t930 o919 b929
2410     B b930 t930
2411     P p930 Number 6043
2412     P p931 Number 6217
2413     O o931 location p930 p931
2414     P p932 String id_wf2
2415     O o932 rule p932
2416     T t932 o736 b604 b591
2417     S s932 t684 h
2418     G s932 t932
2419     B b932 s932
2420     T t933 o677 b932
2421     B b933 t933
2422     T t934 o676 b700 b933
2423     B b934 t934
2424     T t935 o676 b682 b934
2425     B b935 t935
2426     P p935 Number 6065
2427     P p936 Number 6072
2428     O o936 resource_defs p935 p936 p204
2429     P p937 Number 6070
2430     O o937 uid p937 p936
2431     T t937 o937 b691
2432 xiny 3498 B b937 t937
2433 xiny 3527 T t938 o b937 b4
2434 xiny 3405 B b938 t938
2435 xiny 3527 T t939 o936 b938
2436 xiny 3404 B b939 t939
2437 xiny 3527 T t940 o b939 b4
2438     B b940 t940
2439     T t941 o932 b676 b935 b688 b940
2440     B b941 t941
2441     T t942 o931 b941
2442     B b942 t942
2443     P p942 Number 6219
2444     P p943 Number 6603
2445     O o943 location p942 p943
2446     P p944 String id_eq1
2447     O o944 rule p944
2448     T t944 o736 b815 b591
2449     S s944 t684 h
2450     G s944 t944
2451     B b944 s944
2452     T t945 o677 b944
2453     B b945 t945
2454     T t946 o596 b585 b604 b815
2455     B b946 t946
2456     T t947 o761 b591 b759 b946 b815
2457     S s947 t684 h
2458     G s947 t947
2459     B b947 s947
2460     T t948 o677 b947
2461 xiny 3498 B b948 t948
2462 xiny 3527 T t949 o676 b945 b948
2463     B b949 t949
2464     T t950 o676 b763 b949
2465     B b950 t950
2466     T t951 o676 b700 b950
2467     B b951 t951
2468     T t952 o676 b682 b951
2469     B b952 t952
2470     T t953 o676 b761 b952
2471     B b953 t953
2472     T t954 o676 b817 b953
2473     B b954 t954
2474     P p954 Number 6241
2475     P p955 Number 6248
2476     O o955 resource_defs p954 p955 p204
2477     P p956 Number 6246
2478     O o956 uid p956 p955
2479     T t956 o956 b691
2480     B b956 t956
2481     T t957 o b956 b4
2482     B b957 t957
2483     T t958 o955 b957
2484     B b958 t958
2485     T t959 o b958 b4
2486     B b959 t959
2487     T t960 o944 b676 b954 b688 b959
2488     B b960 t960
2489     T t961 o943 b960
2490     B b961 t961
2491     P p961 Number 6605
2492     P p962 Number 6989
2493     O o962 location p961 p962
2494     P p963 String id_eq2
2495 xiny 3498 O o963 rule p963
2496 xiny 3527 T t963 o596 b585 b815 b604
2497 xiny 3498 B b963 t963
2498 xiny 3527 T t964 o761 b591 b759 b963 b815
2499     S s964 t684 h
2500     G s964 t964
2501     B b964 s964
2502     T t965 o677 b964
2503     B b965 t965
2504     T t966 o676 b945 b965
2505     B b966 t966
2506     T t967 o676 b763 b966
2507     B b967 t967
2508     T t968 o676 b700 b967
2509     B b968 t968
2510     T t969 o676 b682 b968
2511     B b969 t969
2512     T t970 o676 b761 b969
2513     B b970 t970
2514     T t971 o676 b817 b970
2515     B b971 t971
2516     P p971 Number 6627
2517     P p972 Number 6634
2518     O o972 resource_defs p971 p972 p204
2519     P p973 Number 6632
2520     O o973 uid p973 p972
2521     T t973 o973 b691
2522     B b973 t973
2523     T t974 o b973 b4
2524     B b974 t974
2525     T t975 o972 b974
2526     B b975 t975
2527     T t976 o b975 b4
2528     B b976 t976
2529     T t977 o963 b676 b971 b688 b976
2530     B b977 t977
2531     T t978 o962 b977
2532     B b978 t978
2533     P p978 Number 6991
2534     P p979 Number 7260
2535     O o979 location p978 p979
2536     P p980 String inv_wf1
2537     O o980 rule p980
2538     T t980 o609 b585 b714
2539 xiny 3405 B b980 t980
2540 xiny 3527 T t981 o700 b980
2541     S s981 t684 h
2542     G s981 t981
2543     B b981 s981
2544     T t982 o677 b981
2545 xiny 3379 B b982 t982
2546 xiny 3527 T t983 o676 b737 b982
2547 xiny 3379 B b983 t983
2548 xiny 3527 T t984 o676 b700 b983
2549     B b984 t984
2550     T t985 o676 b682 b984
2551     B b985 t985
2552     T t986 o676 b716 b985
2553     B b986 t986
2554     P p986 Number 7014
2555     P p987 Number 7021
2556     O o987 resource_defs p986 p987 p204
2557     P p988 Number 7019
2558     O o988 uid p988 p987
2559     T t988 o988 b691
2560     B b988 t988
2561     T t989 o b988 b4
2562     B b989 t989
2563     T t990 o987 b989
2564     B b990 t990
2565     T t991 o b990 b4
2566     B b991 t991
2567     T t992 o980 b676 b986 b688 b991
2568     B b992 t992
2569     T t993 o979 b992
2570     B b993 t993
2571     P p993 Number 7262
2572     P p994 Number 7538
2573     O o994 location p993 p994
2574     P p995 String inv_wf2
2575     O o995 rule p995
2576     T t995 o736 b980 b591
2577     S s995 t684 h
2578     G s995 t995
2579     B b995 s995
2580     T t996 o677 b995
2581     B b996 t996
2582     T t997 o676 b737 b996
2583     B b997 t997
2584     T t998 o676 b700 b997
2585 xiny 3498 B b998 t998
2586 xiny 3527 T t999 o676 b682 b998
2587     B b999 t999
2588     T t1000 o676 b716 b999
2589     B b1000 t1000
2590     P p1000 Number 7285
2591     P p1001 Number 7292
2592     O o1001 resource_defs p1000 p1001 p204
2593     P p1002 Number 7290
2594     O o1002 uid p1002 p1001
2595     T t1002 o1002 b691
2596 xiny 3498 B b1002 t1002
2597 xiny 3527 T t1003 o b1002 b4
2598 xiny 3498 B b1003 t1003
2599 xiny 3527 T t1004 o1001 b1003
2600 xiny 3498 B b1004 t1004
2601 xiny 3527 T t1005 o b1004 b4
2602 xiny 3498 B b1005 t1005
2603 xiny 3527 T t1006 o995 b676 b1000 b688 b1005
2604 xiny 3498 B b1006 t1006
2605 xiny 3527 T t1007 o994 b1006
2606 xiny 3498 B b1007 t1007
2607 xiny 3527 P p1007 Number 7540
2608     P p1008 Number 7839
2609     O o1008 location p1007 p1008
2610     P p1009 String inv_equiv_fun1
2611     O o1009 rule p1009
2612     T t1009 o609 b585 b818
2613     B b1009 t1009 z
2614     T t1010 o817 b591 b759 b1009
2615     S s1010 t684 h
2616     G s1010 t1010
2617     B b1010 s1010
2618     T t1011 o677 b1010
2619 xiny 3498 B b1011 t1011
2620 xiny 3527 T t1012 o676 b763 b1011
2621 xiny 3498 B b1012 t1012
2622 xiny 3527 T t1013 o676 b700 b1012
2623 xiny 3498 B b1013 t1013
2624 xiny 3527 T t1014 o676 b682 b1013
2625 xiny 3498 B b1014 t1014
2626 xiny 3527 T t1015 o676 b761 b1014
2627     B b1015 t1015
2628     P p1015 Number 7570
2629     P p1016 Number 7577
2630     O o1016 resource_defs p1015 p1016 p204
2631     P p1017 Number 7575
2632     O o1017 uid p1017 p1016
2633     T t1017 o1017 b691
2634     B b1017 t1017
2635     T t1018 o b1017 b4
2636     B b1018 t1018
2637     T t1019 o1016 b1018
2638     B b1019 t1019
2639     T t1020 o b1019 b4
2640     B b1020 t1020
2641     T t1021 o1009 b676 b1015 b688 b1020
2642     B b1021 t1021
2643     T t1022 o1008 b1021
2644     B b1022 t1022
2645     P p1022 Number 7841
2646     P p1023 Number 8023
2647     O o1023 location p1022 p1023
2648     P p1024 String inv_eq_fun1
2649     O o1024 rule p1024
2650     T t1024 o852 b1009
2651     S s1024 t684 h
2652     G s1024 t1024
2653     B b1024 s1024
2654     T t1025 o677 b1024
2655     B b1025 t1025
2656     T t1026 o676 b700 b1025
2657     B b1026 t1026
2658     T t1027 o676 b682 b1026
2659     B b1027 t1027
2660     P p1027 Number 7868
2661     P p1028 Number 7875
2662     O o1028 resource_defs p1027 p1028 p204
2663     P p1029 Number 7873
2664     O o1029 uid p1029 p1028
2665     T t1029 o1029 b691
2666     B b1029 t1029
2667     T t1030 o b1029 b4
2668     B b1030 t1030
2669     T t1031 o1028 b1030
2670     B b1031 t1031
2671     T t1032 o b1031 b4
2672     B b1032 t1032
2673     T t1033 o1024 b676 b1027 b688 b1032
2674     B b1033 t1033
2675     T t1034 o1023 b1033
2676     B b1034 t1034
2677     P p1034 Number 8025
2678     P p1035 Number 8423
2679     O o1035 location p1034 p1035
2680     P p1036 String inv_id1
2681     O o1036 rule p1036
2682     T t1036 o596 b585 b980 b714
2683     B b1036 t1036
2684     T t1037 o761 b591 b759 b1036 b604
2685     S s1037 t684 h
2686     G s1037 t1037
2687     B b1037 s1037
2688     T t1038 o677 b1037
2689     B b1038 t1038
2690     T t1039 o676 b737 b1038
2691     B b1039 t1039
2692     T t1040 o676 b763 b1039
2693     B b1040 t1040
2694     T t1041 o676 b700 b1040
2695     B b1041 t1041
2696     T t1042 o676 b682 b1041
2697     B b1042 t1042
2698     T t1043 o676 b761 b1042
2699     B b1043 t1043
2700     T t1044 o676 b716 b1043
2701     B b1044 t1044
2702     P p1044 Number 8048
2703     P p1045 Number 8055
2704     O o1045 resource_defs p1044 p1045 p204
2705     P p1046 Number 8053
2706     O o1046 uid p1046 p1045
2707     T t1046 o1046 b691
2708     B b1046 t1046
2709     T t1047 o b1046 b4
2710     B b1047 t1047
2711     T t1048 o1045 b1047
2712     B b1048 t1048
2713     T t1049 o b1048 b4
2714     B b1049 t1049
2715     T t1050 o1036 b676 b1044 b688 b1049
2716     B b1050 t1050
2717     T t1051 o1035 b1050
2718     B b1051 t1051
2719     P p1051 Number 8425
2720     P p1052 Number 8823
2721     O o1052 location p1051 p1052
2722     P p1053 String inv_id2
2723     O o1053 rule p1053
2724     T t1053 o596 b585 b714 b980
2725     B b1053 t1053
2726     T t1054 o761 b591 b759 b1053 b604
2727     S s1054 t684 h
2728     G s1054 t1054
2729     B b1054 s1054
2730     T t1055 o677 b1054
2731     B b1055 t1055
2732     T t1056 o676 b737 b1055
2733     B b1056 t1056
2734     T t1057 o676 b763 b1056
2735     B b1057 t1057
2736     T t1058 o676 b700 b1057
2737     B b1058 t1058
2738     T t1059 o676 b682 b1058
2739     B b1059 t1059
2740     T t1060 o676 b761 b1059
2741     B b1060 t1060
2742     T t1061 o676 b716 b1060
2743     B b1061 t1061
2744     P p1061 Number 8448
2745     P p1062 Number 8455
2746     O o1062 resource_defs p1061 p1062 p204
2747     P p1063 Number 8453
2748     O o1063 uid p1063 p1062
2749     T t1063 o1063 b691
2750     B b1063 t1063
2751     T t1064 o b1063 b4
2752     B b1064 t1064
2753     T t1065 o1062 b1064
2754     B b1065 t1065
2755     T t1066 o b1065 b4
2756     B b1066 t1066
2757     T t1067 o1053 b676 b1061 b688 b1066
2758     B b1067 t1067
2759     T t1068 o1052 b1067
2760     B b1068 t1068
2761     P p1068 Number 8845
2762     P p1069 Number 9369
2763     O o1069 location p1068 p1069
2764     P p1070 String equiv_op_fun1
2765     O o1070 rule p1070
2766     T t1070 o700 b597
2767     S s1070 t679 h
2768     G s1070 t1070
2769     B b1070 s1070
2770     T t1071 o677 b1070
2771     B b1071 t1071
2772     T t1072 o700 b598
2773     S s1072 t679 h
2774     G s1072 t1072
2775     B b1072 s1072
2776     T t1073 o677 b1072
2777     B b1073 t1073
2778     T t1074 o736 b597 b591
2779     S s1074 t684 h
2780     G s1074 t1074
2781     B b1074 s1074
2782     T t1075 o677 b1074
2783     B b1075 t1075
2784     T t1076 o736 b598 b591
2785     S s1076 t684 h
2786     G s1076 t1076
2787     B b1076 s1076
2788     T t1077 o677 b1076
2789     B b1077 t1077
2790     NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
2791     O o1077 equiv_fun_prop
2792     T t1078 o596 b585 b818 b597
2793     B b1078 t1078
2794     T t1079 o596 b585 b818 b598
2795     B b1079 t1079
2796     T t1080 o761 b591 b759 b1078 b1079
2797     B b1080 t1080 z
2798     T t1081 o1077 b591 b759 b1080
2799     S s1081 t684 h
2800     G s1081 t1081
2801     B b1081 s1081
2802     T t1082 o677 b1081
2803 xiny 3498 B b1082 t1082
2804 xiny 3527 T t1083 o676 b1077 b1082
2805 xiny 3498 B b1083 t1083
2806 xiny 3527 T t1084 o676 b1075 b1083
2807 xiny 3498 B b1084 t1084
2808 xiny 3527 T t1085 o676 b763 b1084
2809     B b1085 t1085
2810     T t1086 o676 b700 b1085
2811     B b1086 t1086
2812     T t1087 o676 b682 b1086
2813     B b1087 t1087
2814     T t1088 o676 b761 b1087
2815     B b1088 t1088
2816     T t1089 o676 b1073 b1088
2817     B b1089 t1089
2818     T t1090 o676 b1071 b1089
2819     B b1090 t1090
2820     NSummary!interactive interactive interactive Summary
2821     O o1090 interactive
2822     NSummary!ext_rule ext_rule ext_rule Summary
2823     P p1090 String "rwh unfold_equiv_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
2824     O o1091 ext_rule p1090
2825     NSummary!status_incomplete status_incomplete status_incomplete Summary
2826     O o1092 status_incomplete
2827     T t1092 o1092
2828     B b1092 t1092
2829     NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2830     O o1093 ext_unjustified
2831     NSummary!tactic_arg tactic_arg tactic_arg Summary
2832     P p1093 String main
2833     O o1094 tactic_arg p1093
2834     NSummary!msequent msequent msequent Summary
2835     O o1095 msequent
2836     T t1095 o b1076 b4
2837     B b1095 t1095
2838     T t1096 o b1074 b1095
2839     B b1096 t1096
2840     T t1097 o b762 b1096
2841     B b1097 t1097
2842     T t1098 o b699 b1097
2843 xiny 3498 B b1098 t1098
2844 xiny 3527 T t1099 o b681 b1098
2845 xiny 3498 B b1099 t1099
2846 xiny 3527 T t1100 o b760 b1099
2847 xiny 3498 B b1100 t1100
2848 xiny 3527 T t1101 o b1072 b1100
2849 xiny 3498 B b1101 t1101
2850 xiny 3527 T t1102 o b1070 b1101
2851 xiny 3498 B b1102 t1102
2852 xiny 3527 T t1103 o1095 b1081 b1102
2853 xiny 3498 B b1103 t1103
2854 xiny 3527 NSummary!parent_none parent_none parent_none Summary
2855     O o1103 parent_none
2856     T t1104 o1103
2857 xiny 3498 B b1104 t1104
2858 xiny 3527 T t1105 o1094 b1103 b4 b1104
2859 xiny 3498 B b1105 t1105
2860 xiny 3527 NCzf_itt_set!set set set Czf_itt_set
2861     O o1105 set
2862     T t1106 o1105
2863     H h1106 a_1 t1106
2864     H h1107 b_1 t1106
2865     H h1108 x t762
2866     P p1108 Var a_1
2867     O o1108 var p1108
2868     T t1108 o1108
2869 xiny 3498 B b1108 t1108
2870 xiny 3527 P p1109 Var b_1
2871     O o1109 var p1109
2872     T t1109 o1109
2873 xiny 3498 B b1109 t1109
2874 xiny 3527 T t1110 o761 b591 b759 b1108 b1109
2875     H h1110 x_1 t1110
2876     T t1111 o596 b585 b1108 b597
2877 xiny 3498 B b1111 t1111
2878 xiny 3527 T t1112 o596 b585 b1108 b598
2879     B b1112 t1112
2880     T t1113 o761 b591 b759 b1111 b1112
2881     H h1113 x_2 t1113
2882     T t1114 o596 b585 b1109 b597
2883     B b1114 t1114
2884     T t1115 o596 b585 b1109 b598
2885     B b1115 t1115
2886     T t1116 o761 b591 b759 b1114 b1115
2887     S s1116 t684 h h1106 h1107 h1108 h1110 h1113
2888     G s1116 t1116
2889     B b1116 s1116
2890     T t1117 o1095 b1116 b1102
2891     B b1117 t1117
2892     NItt_logic Itt_logic Itt_logic NIL
2893     NItt_logic!implies implies implies Itt_logic
2894     O o1117 implies
2895     B b1118 t1113
2896     B b1119 t1116
2897     T t1119 o1117 b1118 b1119
2898     S s1119 t684 h h1106 h1107 h1108 h1110
2899     G s1119 t1119
2900 xiny 3405 B b1120 s1119
2901 xiny 3527 T t1120 o1095 b1120 b1102
2902 xiny 3405 B b1121 t1120
2903 xiny 3527 B b1122 t1110
2904     B b1123 t1119
2905     T t1123 o1117 b1122 b1123
2906     S s1123 t684 h h1106 h1107 h1108
2907     G s1123 t1123
2908     B b1124 s1123
2909     T t1124 o1095 b1124 b1102
2910 xiny 3379 B b1125 t1124
2911 xiny 3527 B b1126 t762
2912     B b1127 t1123
2913     T t1127 o1117 b1126 b1127
2914     S s1127 t684 h h1106 h1107
2915     G s1127 t1127
2916     B b1128 s1127
2917     T t1128 o1095 b1128 b1102
2918 xiny 3379 B b1129 t1128
2919 xiny 3527 NItt_logic!all all all Itt_logic
2920     O o1129 all
2921     B b1130 t1106
2922     B b1131 t1127 b_1
2923     T t1131 o1129 b1130 b1131
2924     S s1131 t684 h h1106
2925     G s1131 t1131
2926     B b1132 s1131
2927     T t1132 o1095 b1132 b1102
2928 xiny 3379 B b1133 t1132
2929 xiny 3527 B b1134 t1131 a_1
2930     T t1134 o1129 b1130 b1134
2931     S s1134 t684 h
2932     G s1134 t1134
2933     B b1135 s1134
2934     T t1135 o1095 b1135 b1102
2935 xiny 3404 B b1136 t1135
2936 xiny 3527 T t1136 o2 b1105
2937     B b1137 t1136
2938     T t1137 o1094 b1136 b4 b1137
2939 xiny 3404 B b1138 t1137
2940 xiny 3527 T t1138 o2 b1138
2941 xiny 3404 B b1139 t1138
2942 xiny 3527 T t1139 o1094 b1133 b4 b1139
2943 xiny 3379 B b1140 t1139
2944 xiny 3527 T t1140 o2 b1140
2945 xiny 3379 B b1141 t1140
2946 xiny 3527 T t1141 o1094 b1129 b4 b1141
2947 xiny 3379 B b1142 t1141
2948 xiny 3527 T t1142 o2 b1142
2949 xiny 3379 B b1143 t1142
2950 xiny 3527 T t1143 o1094 b1125 b4 b1143
2951 xiny 3498 B b1144 t1143
2952 xiny 3527 T t1144 o2 b1144
2953     B b1145 t1144
2954     T t1145 o1094 b1121 b4 b1145
2955 xiny 3405 B b1146 t1145
2956 xiny 3527 T t1146 o2 b1146
2957 xiny 3379 B b1147 t1146
2958 xiny 3527 T t1147 o1094 b1117 b4 b1147
2959 xiny 3498 B b1148 t1147
2960     T t1148 o b1148 b4
2961     B b1149 t1148
2962 xiny 3527 T t1149 o1093 b1105 b1149
2963 xiny 3405 B b1150 t1149
2964 xiny 3527 P p1150 String "equivTransT << op{'g; 'b_1; 'a} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
2965 xiny 3498 O o1150 ext_rule p1150
2966 xiny 3527 NItt_logic!and and and Itt_logic
2967     O o1151 and
2968     B b1151 t700
2969     B b1152 t760
2970     T t1152 o700 b1111
2971 xiny 3379 B b1153 t1152
2972 xiny 3527 T t1153 o700 b1112
2973 xiny 3379 B b1154 t1153
2974 xiny 3527 T t1154 o1151 b1153 b1154
2975 xiny 3404 B b1155 t1154
2976 xiny 3527 T t1155 o1151 b1152 b1155
2977 xiny 3379 B b1156 t1155
2978 xiny 3527 T t1156 o1151 b1151 b1156
2979 xiny 3379 B b1157 t1156
2980 xiny 3527 T t1157 o736 b1111 b591
2981 xiny 3379 B b1158 t1157
2982 xiny 3527 T t1158 o736 b1112 b591
2983 xiny 3404 B b1159 t1158
2984 xiny 3527 T t1159 o1151 b1158 b1159
2985 xiny 3404 B b1160 t1159
2986 xiny 3527 T t1160 o1151 b1157 b1160
2987 xiny 3498 B b1161 t1160
2988 xiny 3527 NCzf_itt_pair Czf_itt_pair Czf_itt_pair NIL
2989     NCzf_itt_pair!pair pair pair Czf_itt_pair
2990     O o1161 pair
2991     T t1161 o1161 b1111 b1112
2992 xiny 3405 B b1162 t1161
2993 xiny 3527 T t1162 o736 b1162 b759
2994 xiny 3404 B b1163 t1162
2995 xiny 3527 T t1163 o1151 b1161 b1163
2996     H h1163 x_2 t1163
2997     T t1164 o736 b1114 b591
2998     S s1164 t684 h h1106 h1107 h1108 h1110 h1163
2999     G s1164 t1164
3000     B b1164 s1164
3001     T t1165 o1095 b1164 b1102
3002     B b1165 t1165
3003     S s1165 t684 h h1106 h1107 h1108 h1110 h1113
3004     G s1165 t1164
3005     B b1166 s1165
3006     T t1166 o1095 b1166 b1102
3007 xiny 3498 B b1167 t1166
3008 xiny 3527 T t1167 o2 b1148
3009 xiny 3405 B b1168 t1167
3010 xiny 3527 T t1168 o1094 b1167 b4 b1168
3011 xiny 3379 B b1169 t1168
3012 xiny 3527 T t1169 o2 b1169
3013 xiny 3498 B b1170 t1169
3014 xiny 3527 T t1170 o1094 b1165 b4 b1170
3015     B b1171 t1170
3016     T t1171 o761 b591 b759 b1111 b1114
3017     H h1171 u t1171
3018     T t1172 o761 b591 b759 b1114 b1112
3019     H h1172 v t1172
3020     S s1172 t684 h h1106 h1107 h1108 h1110 h1163 h1171 h1172
3021     G s1172 t1116
3022     B b1172 s1172
3023     T t1173 o1095 b1172 b1102
3024     B b1173 t1173
3025     S s1173 t684 h h1106 h1107 h1108 h1110 h1113 h1171 h1172
3026     G s1173 t1116
3027     B b1174 s1173
3028     T t1174 o1095 b1174 b1102
3029     B b1175 t1174
3030     T t1175 o1094 b1175 b4 b1168
3031     B b1176 t1175
3032     T t1176 o2 b1176
3033     B b1177 t1176
3034     T t1177 o1094 b1173 b4 b1177
3035     B b1178 t1177
3036     T t1178 o b1178 b4
3037     B b1179 t1178
3038     T t1179 o b1171 b1179
3039     B b1180 t1179
3040     T t1180 o1093 b1148 b1180
3041     B b1181 t1180
3042     P p1181 String "autoT thenT rwh unfold_equiv 5 ttca"
3043     O o1181 ext_rule p1181
3044     T t1181 o1093 b1171 b4
3045     B b1182 t1181
3046     T t1182 o1181 b1092 b1182 b4 b4
3047     B b1183 t1182
3048     P p1183 String "equivTransT << op{'g; 'b_1; 'b} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3049     O o1183 ext_rule p1183
3050     T t1183 o1093 b1178 b4
3051     B b1184 t1183
3052     T t1184 o1183 b1092 b1184 b4 b4
3053     B b1185 t1184
3054     T t1185 o b1185 b4
3055     B b1186 t1185
3056     T t1186 o b1183 b1186
3057     B b1187 t1186
3058     T t1187 o1150 b1092 b1181 b1187 b4
3059     B b1188 t1187
3060     T t1188 o b1188 b4
3061     B b1189 t1188
3062     T t1189 o1091 b1092 b1150 b1189 b4
3063     B b1190 t1189
3064     T t1190 o1090 b1190
3065     B b1191 t1190
3066     P p1191 Number 8874
3067     P p1192 Number 8881
3068     O o1192 resource_defs p1191 p1192 p204
3069     P p1193 Number 8879
3070     O o1193 uid p1193 p1192
3071     T t1193 o1193 b691
3072     B b1193 t1193
3073     T t1194 o b1193 b4
3074 xiny 3498 B b1194 t1194
3075 xiny 3527 T t1195 o1192 b1194
3076     B b1195 t1195
3077     T t1196 o b1195 b4
3078     B b1196 t1196
3079     T t1197 o1070 b676 b1090 b1191 b1196
3080     B b1197 t1197
3081     T t1198 o1069 b1197
3082     B b1198 t1198
3083     P p1198 Number 9371
3084     P p1199 Number 9895
3085     O o1199 location p1198 p1199
3086     P p1200 String equiv_op_fun2
3087     O o1200 rule p1200
3088     T t1200 o596 b585 b597 b818
3089     B b1200 t1200
3090     T t1201 o596 b585 b598 b818
3091 xiny 3498 B b1201 t1201
3092 xiny 3527 T t1202 o761 b591 b759 b1200 b1201
3093     B b1202 t1202 z
3094     T t1203 o1077 b591 b759 b1202
3095     S s1203 t684 h
3096     G s1203 t1203
3097     B b1203 s1203
3098     T t1204 o677 b1203
3099 xiny 3498 B b1204 t1204
3100 xiny 3527 T t1205 o676 b1077 b1204
3101     B b1205 t1205
3102     T t1206 o676 b1075 b1205
3103     B b1206 t1206
3104     T t1207 o676 b763 b1206
3105     B b1207 t1207
3106     T t1208 o676 b700 b1207
3107 xiny 3498 B b1208 t1208
3108 xiny 3527 T t1209 o676 b682 b1208
3109     B b1209 t1209
3110     T t1210 o676 b761 b1209
3111     B b1210 t1210
3112     T t1211 o676 b1073 b1210
3113 xiny 3498 B b1211 t1211
3114 xiny 3527 T t1212 o676 b1071 b1211
3115     B b1212 t1212
3116     T t1213 o1095 b1203 b1102
3117     B b1213 t1213
3118     T t1214 o1094 b1213 b4 b1104
3119     B b1214 t1214
3120     T t1215 o596 b585 b597 b1108
3121     B b1215 t1215
3122     T t1216 o596 b585 b598 b1108
3123     B b1216 t1216
3124     T t1217 o761 b591 b759 b1215 b1216
3125     H h1217 x_2 t1217
3126     T t1218 o596 b585 b597 b1109
3127     B b1218 t1218
3128     T t1219 o596 b585 b598 b1109
3129     B b1219 t1219
3130     T t1220 o761 b591 b759 b1218 b1219
3131     S s1220 t684 h h1106 h1107 h1108 h1110 h1217
3132     G s1220 t1220
3133     B b1220 s1220
3134     T t1221 o1095 b1220 b1102
3135     B b1221 t1221
3136     B b1222 t1217
3137     B b1223 t1220
3138     T t1223 o1117 b1222 b1223
3139     S s1223 t684 h h1106 h1107 h1108 h1110
3140     G s1223 t1223
3141     B b1224 s1223
3142     T t1224 o1095 b1224 b1102
3143     B b1225 t1224
3144     B b1226 t1223
3145     T t1226 o1117 b1122 b1226
3146     S s1226 t684 h h1106 h1107 h1108
3147     G s1226 t1226
3148     B b1227 s1226
3149     T t1227 o1095 b1227 b1102
3150     B b1228 t1227
3151     B b1229 t1226
3152     T t1229 o1117 b1126 b1229
3153     S s1229 t684 h h1106 h1107
3154     G s1229 t1229
3155     B b1230 s1229
3156     T t1230 o1095 b1230 b1102
3157     B b1231 t1230
3158     B b1232 t1229 b_1
3159     T t1232 o1129 b1130 b1232
3160     S s1232 t684 h h1106
3161     G s1232 t1232
3162     B b1233 s1232
3163     T t1233 o1095 b1233 b1102
3164     B b1234 t1233
3165     B b1235 t1232 a_1
3166     T t1235 o1129 b1130 b1235
3167     S s1235 t684 h
3168     G s1235 t1235
3169     B b1236 s1235
3170     T t1236 o1095 b1236 b1102
3171     B b1237 t1236
3172     T t1237 o2 b1214
3173     B b1238 t1237
3174     T t1238 o1094 b1237 b4 b1238
3175     B b1239 t1238
3176     T t1239 o2 b1239
3177     B b1240 t1239
3178     T t1240 o1094 b1234 b4 b1240
3179     B b1241 t1240
3180     T t1241 o2 b1241
3181     B b1242 t1241
3182     T t1242 o1094 b1231 b4 b1242
3183     B b1243 t1242
3184     T t1243 o2 b1243
3185     B b1244 t1243
3186     T t1244 o1094 b1228 b4 b1244
3187     B b1245 t1244
3188     T t1245 o2 b1245
3189     B b1246 t1245
3190     T t1246 o1094 b1225 b4 b1246
3191     B b1247 t1246
3192     T t1247 o2 b1247
3193     B b1248 t1247
3194     T t1248 o1094 b1221 b4 b1248
3195     B b1249 t1248
3196     T t1249 o b1249 b4
3197     B b1250 t1249
3198     T t1250 o1093 b1214 b1250
3199     B b1251 t1250
3200     P p1251 String "equivTransT << op{'g; 'a; 'b_1} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
3201     O o1251 ext_rule p1251
3202     T t1251 o700 b1215
3203     B b1252 t1251
3204     T t1252 o700 b1216
3205     B b1253 t1252
3206     T t1253 o1151 b1252 b1253
3207     B b1254 t1253
3208     T t1254 o1151 b1152 b1254
3209     B b1255 t1254
3210     T t1255 o1151 b1151 b1255
3211     B b1256 t1255
3212     T t1256 o736 b1215 b591
3213     B b1257 t1256
3214     T t1257 o736 b1216 b591
3215     B b1258 t1257
3216     T t1258 o1151 b1257 b1258
3217     B b1259 t1258
3218     T t1259 o1151 b1256 b1259
3219     B b1260 t1259
3220     T t1260 o1161 b1215 b1216
3221     B b1261 t1260
3222     T t1261 o736 b1261 b759
3223     B b1262 t1261
3224     T t1262 o1151 b1260 b1262
3225     H h1262 x_2 t1262
3226     T t1263 o736 b1218 b591
3227     S s1263 t684 h h1106 h1107 h1108 h1110 h1262
3228     G s1263 t1263
3229     B b1263 s1263
3230     T t1264 o1095 b1263 b1102
3231     B b1264 t1264
3232     S s1264 t684 h h1106 h1107 h1108 h1110 h1217
3233     G s1264 t1263
3234     B b1265 s1264
3235     T t1265 o1095 b1265 b1102
3236     B b1266 t1265
3237     T t1266 o2 b1249
3238     B b1267 t1266
3239     T t1267 o1094 b1266 b4 b1267
3240     B b1268 t1267
3241     T t1268 o2 b1268
3242     B b1269 t1268
3243     T t1269 o1094 b1264 b4 b1269
3244     B b1270 t1269
3245     T t1270 o761 b591 b759 b1215 b1218
3246     H h1270 u t1270
3247     T t1271 o761 b591 b759 b1218 b1216
3248     H h1271 v t1271
3249     S s1271 t684 h h1106 h1107 h1108 h1110 h1262 h1270 h1271
3250     G s1271 t1220
3251     B b1271 s1271
3252     T t1272 o1095 b1271 b1102
3253     B b1272 t1272
3254     S s1272 t684 h h1106 h1107 h1108 h1110 h1217 h1270 h1271
3255     G s1272 t1220
3256     B b1273 s1272
3257     T t1273 o1095 b1273 b1102
3258     B b1274 t1273
3259     T t1274 o1094 b1274 b4 b1267
3260     B b1275 t1274
3261     T t1275 o2 b1275
3262     B b1276 t1275
3263     T t1276 o1094 b1272 b4 b1276
3264     B b1277 t1276
3265     T t1277 o b1277 b4
3266     B b1278 t1277
3267     T t1278 o b1270 b1278
3268     B b1279 t1278
3269     T t1279 o1093 b1249 b1279
3270     B b1280 t1279
3271     T t1280 o1093 b1270 b4
3272     B b1281 t1280
3273     T t1281 o1181 b1092 b1281 b4 b4
3274     B b1282 t1281
3275     P p1282 String "equivTransT << op{'g; 'b; 'b_1} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3276     O o1282 ext_rule p1282
3277     T t1282 o1093 b1277 b4
3278     B b1283 t1282
3279     T t1283 o1282 b1092 b1283 b4 b4
3280     B b1284 t1283
3281     T t1284 o b1284 b4
3282     B b1285 t1284
3283     T t1285 o b1282 b1285
3284     B b1286 t1285
3285     T t1286 o1251 b1092 b1280 b1286 b4
3286     B b1287 t1286
3287     T t1287 o b1287 b4
3288     B b1288 t1287
3289     T t1288 o1091 b1092 b1251 b1288 b4
3290     B b1289 t1288
3291     T t1289 o1090 b1289
3292     B b1290 t1289
3293     P p1290 Number 9400
3294     P p1291 Number 9407
3295     O o1291 resource_defs p1290 p1291 p204
3296     P p1292 Number 9405
3297     O o1292 uid p1292 p1291
3298     T t1292 o1292 b691
3299 xiny 3498 B b1292 t1292
3300 xiny 3527 T t1293 o b1292 b4
3301     B b1293 t1293
3302     T t1294 o1291 b1293
3303     B b1294 t1294
3304     T t1295 o b1294 b4
3305     B b1295 t1295
3306     T t1296 o1200 b676 b1212 b1290 b1295
3307     B b1296 t1296
3308     T t1297 o1199 b1296
3309     B b1297 t1297
3310     P p1297 Number 11515
3311     P p1298 Number 12822
3312     O o1298 location p1297 p1298
3313     P p1299 String cancel1
3314     O o1299 rule p1299
3315     P p1300 String J
3316     O o1300 context_param p1300
3317     T t1300 o1300
3318     B b1300 t1300
3319     T t1301 o b1300 b4
3320     B b1301 t1301
3321     T t1302 o b675 b1301
3322     B b1302 t1302
3323     T t1303 o761 b591 b759 b720 b791
3324     H h1303 x t1303
3325     P p1303 Var x
3326     O o1303 var p1303
3327     T t1304 o1303
3328     C h1304 J t1304
3329     S s1304 t679 h h1303 h1304
3330     G s1304 t715
3331     B b1304 s1304
3332     T t1305 o677 b1304
3333 xiny 3498 B b1305 t1305
3334 xiny 3527 S s1305 t679 h h1303 h1304
3335     G s1305 t718
3336     B b1306 s1305
3337     T t1306 o677 b1306
3338     B b1307 t1306
3339     S s1307 t679 h h1303 h1304
3340     G s1307 t757
3341     B b1308 s1307
3342     T t1308 o677 b1308
3343     B b1309 t1308
3344     S s1309 t679 h h1303 h1304
3345     G s1309 t760
3346     B b1310 s1309
3347     T t1310 o677 b1310
3348     B b1311 t1310
3349     S s1311 t679 h h1303 h1304
3350     G s1311 t681
3351     B b1312 s1311
3352     T t1312 o677 b1312
3353     B b1313 t1312
3354     S s1313 t684 h h1303 h1304
3355     G s1313 t586
3356     B b1314 s1313
3357     T t1314 o677 b1314
3358     B b1315 t1314
3359     S s1315 t684 h h1303 h1304
3360     G s1315 t762
3361     B b1316 s1315
3362     T t1316 o677 b1316
3363     B b1317 t1316
3364     S s1317 t684 h h1303 h1304
3365     G s1317 t736
3366     B b1318 s1317
3367     T t1318 o677 b1318
3368     B b1319 t1318
3369     S s1319 t684 h h1303 h1304
3370     G s1319 t738
3371     B b1320 s1319
3372     T t1320 o677 b1320
3373     B b1321 t1320
3374     S s1321 t684 h h1303 h1304
3375     G s1321 t764
3376     B b1322 s1321
3377     T t1322 o677 b1322
3378     B b1323 t1322
3379     T t1323 o761 b591 b759 b717 b756
3380     S s1323 t684 h h1303 h1304
3381     G s1323 t1323
3382     B b1324 s1323
3383     T t1324 o677 b1324
3384     B b1325 t1324
3385     T t1325 o676 b1323 b1325
3386     B b1326 t1325
3387     T t1326 o676 b1321 b1326
3388     B b1327 t1326
3389     T t1327 o676 b1319 b1327
3390     B b1328 t1327
3391     T t1328 o676 b1317 b1328
3392     B b1329 t1328
3393     T t1329 o676 b1315 b1329
3394     B b1330 t1329
3395     T t1330 o676 b1313 b1330
3396     B b1331 t1330
3397     T t1331 o676 b1311 b1331
3398     B b1332 t1331
3399     T t1332 o676 b1309 b1332
3400     B b1333 t1332
3401     T t1333 o676 b1307 b1333
3402     B b1334 t1333
3403     T t1334 o676 b1305 b1334
3404     B b1335 t1334
3405     P p1335 String "assertT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenAT autoT"
3406     O o1335 ext_rule p1335
3407     T t1335 o b1322 b4
3408     B b1336 t1335
3409     T t1336 o b1320 b1336
3410     B b1337 t1336
3411     T t1337 o b1318 b1337
3412     B b1338 t1337
3413     T t1338 o b1316 b1338
3414     B b1339 t1338
3415     T t1339 o b1314 b1339
3416     B b1340 t1339
3417     T t1340 o b1312 b1340
3418     B b1341 t1340
3419     T t1341 o b1310 b1341
3420     B b1342 t1341
3421     T t1342 o b1308 b1342
3422     B b1343 t1342
3423     T t1343 o b1306 b1343
3424     B b1344 t1343
3425     T t1344 o b1304 b1344
3426     B b1345 t1344
3427     T t1345 o1095 b1324 b1345
3428     B b1346 t1345
3429     T t1346 o1094 b1346 b4 b1104
3430     B b1347 t1346
3431     T t1347 o596 b585 b980 b720
3432     B b1348 t1347
3433     T t1348 o596 b585 b980 b791
3434     B b1349 t1348
3435     T t1349 o761 b591 b759 b1348 b1349
3436     H h1349 v t1349
3437     S s1349 t684 h h1303 h1304 h1349
3438     G s1349 t1323
3439     B b1350 s1349
3440     T t1350 o1095 b1350 b1345
3441     B b1351 t1350
3442     T t1351 o2 b1347
3443     B b1352 t1351
3444     T t1352 o1094 b1351 b4 b1352
3445     B b1353 t1352
3446     T t1353 o b1353 b4
3447 xiny 3498 B b1354 t1353
3448 xiny 3527 T t1354 o1093 b1347 b1354
3449 xiny 3498 B b1355 t1354
3450 xiny 3527 P p1355 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 4 ttca"
3451     O o1355 ext_rule p1355
3452     T t1355 o596 b585 b1036 b717
3453 xiny 3498 B b1356 t1355
3454 xiny 3527 T t1356 o761 b591 b759 b1356 b1349
3455     H h1356 z t1356
3456     S s1356 t684 h h1303 h1304 h1349 h1356
3457     G s1356 t1323
3458     B b1357 s1356
3459     T t1357 o1095 b1357 b1345
3460 xiny 3498 B b1358 t1357
3461 xiny 3527 T t1358 o2 b1353
3462 xiny 3498 B b1359 t1358
3463 xiny 3527 T t1359 o1094 b1358 b4 b1359
3464 xiny 3498 B b1360 t1359
3465 xiny 3527 T t1360 o b1360 b4
3466     B b1361 t1360
3467     T t1361 o1093 b1353 b1361
3468 xiny 3498 B b1362 t1361
3469 xiny 3527 P p1362 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 5 ttca"
3470     O o1362 ext_rule p1362
3471     T t1362 o596 b585 b1036 b756
3472 xiny 3498 B b1363 t1362
3473 xiny 3527 T t1363 o761 b591 b759 b1356 b1363
3474     H h1363 z_1 t1363
3475     S s1363 t684 h h1303 h1304 h1349 h1356 h1363
3476     G s1363 t1323
3477     B b1364 s1363
3478     T t1364 o1095 b1364 b1345
3479 xiny 3498 B b1365 t1364
3480 xiny 3527 T t1365 o2 b1360
3481 xiny 3498 B b1366 t1365
3482 xiny 3527 T t1366 o1094 b1365 b4 b1366
3483     B b1367 t1366
3484     T t1367 o b1367 b4
3485 xiny 3498 B b1368 t1367
3486 xiny 3527 T t1368 o1093 b1360 b1368
3487 xiny 3498 B b1369 t1368
3488 xiny 3527 P p1369 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"
3489     O o1369 ext_rule p1369
3490     T t1369 o596 b585 b604 b717
3491 xiny 3498 B b1370 t1369
3492 xiny 3527 T t1370 o596 b585 b604 b756
3493 xiny 3498 B b1371 t1370
3494 xiny 3527 T t1371 o761 b591 b759 b1370 b1371
3495     H h1371 z_2 t1371
3496     S s1371 t684 h h1303 h1304 h1349 h1356 h1363 h1371
3497     G s1371 t1323
3498     B b1372 s1371
3499     T t1372 o1095 b1372 b1345
3500 xiny 3498 B b1373 t1372
3501 xiny 3527 T t1373 o2 b1367
3502 xiny 3498 B b1374 t1373
3503 xiny 3527 T t1374 o1094 b1373 b4 b1374
3504 xiny 3404 B b1375 t1374
3505 xiny 3498 T t1375 o b1375 b4
3506 xiny 3404 B b1376 t1375
3507 xiny 3527 T t1376 o1093 b1367 b1376
3508 xiny 3498 B b1377 t1376
3509 xiny 3527 P p1377 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"
3510     O o1377 ext_rule p1377
3511     T t1377 o761 b591 b759 b717 b1371
3512     H h1377 z_3 t1377
3513     S s1377 t684 h h1303 h1304 h1349 h1356 h1363 h1371 h1377
3514     G s1377 t1323
3515     B b1378 s1377
3516     T t1378 o1095 b1378 b1345
3517 xiny 3498 B b1379 t1378
3518 xiny 3527 T t1379 o2 b1375
3519 xiny 3405 B b1380 t1379
3520 xiny 3527 T t1380 o1094 b1379 b4 b1380
3521     B b1381 t1380
3522     T t1381 o b1381 b4
3523     B b1382 t1381
3524     T t1382 o1093 b1375 b1382
3525     B b1383 t1382
3526     P p1383 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"
3527     O o1383 ext_rule p1383
3528     T t1383 o1093 b1381 b4
3529     B b1384 t1383
3530     T t1384 o1383 b1092 b1384 b4 b4
3531     B b1385 t1384
3532     T t1385 o b1385 b4
3533     B b1386 t1385
3534     T t1386 o1377 b1092 b1383 b1386 b4
3535     B b1387 t1386
3536     T t1387 o b1387 b4
3537     B b1388 t1387
3538     T t1388 o1369 b1092 b1377 b1388 b4
3539     B b1389 t1388
3540     T t1389 o b1389 b4
3541     B b1390 t1389
3542     T t1390 o1362 b1092 b1369 b1390 b4
3543     B b1391 t1390
3544     T t1391 o b1391 b4
3545     B b1392 t1391
3546     T t1392 o1355 b1092 b1362 b1392 b4
3547     B b1393 t1392
3548     T t1393 o b1393 b4
3549     B b1394 t1393
3550     P p1394 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 3 ttca"
3551     O o1394 ext_rule p1394
3552     H h1394 v t1303
3553     H h1395 v_1 t1349
3554     S s1395 t684 h h1394 h1395
3555     G s1395 t1323
3556     B b1395 s1395
3557     S s1396 t684 h
3558     G s1396 t1303
3559     B b1396 s1396
3560     T t1396 o b1396 b4
3561     B b1397 t1396
3562     T t1397 o b764 b1397
3563     B b1398 t1397
3564     T t1398 o b738 b1398
3565     B b1399 t1398
3566     T t1399 o b736 b1399
3567     B b1400 t1399
3568     T t1400 o b762 b1400
3569     B b1401 t1400
3570     T t1401 o b699 b1401
3571     B b1402 t1401
3572     T t1402 o b681 b1402
3573     B b1403 t1402
3574     T t1403 o b760 b1403
3575     B b1404 t1403
3576     T t1404 o b757 b1404
3577     B b1405 t1404
3578     T t1405 o b718 b1405
3579     B b1406 t1405
3580     T t1406 o b715 b1406
3581     B b1407 t1406
3582     T t1407 o1095 b1395 b1407
3583     B b1408 t1407
3584     S s1408 t684 h h1394
3585     G s1408 t1323
3586     B b1409 s1408
3587     T t1409 o1095 b1409 b1407
3588     B b1410 t1409
3589     S s1410 t684 h
3590     G s1410 t1323
3591     B b1411 s1410
3592     T t1411 o1095 b1411 b1407
3593     B b1412 t1411
3594     T t1412 o1094 b1412 b4 b1104
3595     B b1413 t1412
3596     T t1413 o2 b1413
3597     B b1414 t1413
3598     T t1414 o1094 b1410 b4 b1414
3599     B b1415 t1414
3600     T t1415 o2 b1415
3601     B b1416 t1415
3602     T t1416 o1094 b1408 b4 b1416
3603     B b1417 t1416
3604     S s1417 t684 h h1394 h1395 h1356
3605     G s1417 t1323
3606     B b1418 s1417
3607     T t1418 o1095 b1418 b1407
3608     B b1419 t1418
3609     T t1419 o2 b1417
3610     B b1420 t1419
3611     T t1420 o1094 b1419 b4 b1420
3612     B b1421 t1420
3613     T t1421 o b1421 b4
3614     B b1422 t1421
3615     T t1422 o1093 b1417 b1422
3616     B b1423 t1422
3617     P p1423 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 4 ttca"
3618     O o1423 ext_rule p1423
3619     S s1423 t684 h h1394 h1395 h1356 h1363
3620     G s1423 t1323
3621     B b1424 s1423
3622     T t1424 o1095 b1424 b1407
3623     B b1425 t1424
3624     T t1425 o2 b1421
3625     B b1426 t1425
3626     T t1426 o1094 b1425 b4 b1426
3627     B b1427 t1426
3628     T t1427 o b1427 b4
3629     B b1428 t1427
3630     T t1428 o1093 b1421 b1428
3631     B b1429 t1428
3632     P p1429 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 ttca"
3633     O o1429 ext_rule p1429
3634     S s1429 t684 h h1394 h1395 h1356 h1363 h1371
3635     G s1429 t1323
3636     B b1430 s1429
3637     T t1430 o1095 b1430 b1407
3638     B b1431 t1430
3639     T t1431 o2 b1427
3640     B b1432 t1431
3641     T t1432 o1094 b1431 b4 b1432
3642     B b1433 t1432
3643     T t1433 o b1433 b4
3644     B b1434 t1433
3645     T t1434 o1093 b1427 b1434
3646     B b1435 t1434
3647     P p1435 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 6 ttca"
3648     O o1435 ext_rule p1435
3649     S s1435 t684 h h1394 h1395 h1356 h1363 h1371 h1377
3650     G s1435 t1323
3651     B b1436 s1435
3652     T t1436 o1095 b1436 b1407
3653     B b1437 t1436
3654     T t1437 o2 b1433
3655     B b1438 t1437
3656     T t1438 o1094 b1437 b4 b1438
3657     B b1439 t1438
3658     T t1439 o b1439 b4
3659     B b1440 t1439
3660     T t1440 o1093 b1433 b1440
3661     B b1441 t1440
3662     P p1441 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 7 ttca"
3663     O o1441 ext_rule p1441
3664     T t1441 o1093 b1439 b4
3665     B b1442 t1441
3666     T t1442 o1441 b1092 b1442 b4 b4
3667     B b1443 t1442
3668     T t1443 o b1443 b4
3669     B b1444 t1443
3670     T t1444 o1435 b1092 b1441 b1444 b4
3671     B b1445 t1444
3672     T t1445 o b1445 b4
3673     B b1446 t1445
3674     T t1446 o1429 b1092 b1435 b1446 b4
3675     B b1447 t1446
3676     T t1447 o b1447 b4
3677     B b1448 t1447
3678     T t1448 o1423 b1092 b1429 b1448 b4
3679     B b1449 t1448
3680     T t1449 o b1449 b4
3681     B b1450 t1449
3682     T t1450 o1394 b1092 b1423 b1450 b4
3683     B b1451 t1450
3684     T t1451 o b1451 b4
3685     B b1452 t1451
3686     T t1452 o1335 b1092 b1355 b1394 b1452
3687     B b1453 t1452
3688     T t1453 o1090 b1453
3689     B b1454 t1453
3690     T t1454 o1299 b1302 b1335 b1454 b4
3691     B b1455 t1454
3692     T t1455 o1298 b1455
3693     B b1456 t1455
3694     P p1456 Number 12867
3695     P p1457 Number 14174
3696     O o1457 location p1456 p1457
3697     P p1458 String cancel2
3698     O o1458 rule p1458
3699     H h1458 x t793
3700     S s1458 t679 h h1458 h1304
3701     G s1458 t715
3702     B b1458 s1458
3703     T t1458 o677 b1458
3704     B b1459 t1458
3705     S s1459 t679 h h1458 h1304
3706     G s1459 t718
3707     B b1460 s1459
3708     T t1460 o677 b1460
3709     B b1461 t1460
3710     S s1461 t679 h h1458 h1304
3711     G s1461 t757
3712     B b1462 s1461
3713     T t1462 o677 b1462
3714 xiny 3379 B b1463 t1462
3715 xiny 3527 S s1463 t679 h h1458 h1304
3716     G s1463 t760
3717     B b1464 s1463
3718     T t1464 o677 b1464
3719 xiny 3379 B b1465 t1464
3720 xiny 3527 S s1465 t679 h h1458 h1304
3721     G s1465 t681
3722     B b1466 s1465
3723     T t1466 o677 b1466
3724 xiny 3405 B b1467 t1466
3725 xiny 3527 S s1467 t684 h h1458 h1304
3726     G s1467 t586
3727     B b1468 s1467
3728     T t1468 o677 b1468
3729     B b1469 t1468
3730     S s1469 t684 h h1458 h1304
3731     G s1469 t762
3732     B b1470 s1469
3733     T t1470 o677 b1470
3734 xiny 3404 B b1471 t1470
3735 xiny 3527 S s1471 t684 h h1458 h1304
3736     G s1471 t736
3737     B b1472 s1471
3738     T t1472 o677 b1472
3739 xiny 3404 B b