/[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 3530 - (hide annotations) (download)
Thu Mar 7 23:13:10 2002 UTC (19 years, 4 months ago) by xiny
File size: 136215 byte(s)
1. Added properties that "e * a = a * e" and "a * e = e * a".
2. Changed the definition of groups to one-sided (left) definition,
   i.e., groups are defined by the left axioms, and proved the right
   axioms.
3. Removed the introduction forms of group cancellation laws which
   were put in comments in the last version.

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 xiny 3530 P p6 Number 6874
2493     O o10 location p961 p6
2494 xiny 3527 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 p980 String inv_wf1
2517     O o980 rule p980
2518     T t980 o609 b585 b714
2519 xiny 3405 B b980 t980
2520 xiny 3527 T t981 o700 b980
2521     S s981 t684 h
2522     G s981 t981
2523     B b981 s981
2524     T t982 o677 b981
2525 xiny 3379 B b982 t982
2526 xiny 3527 T t983 o676 b737 b982
2527 xiny 3379 B b983 t983
2528 xiny 3527 T t984 o676 b700 b983
2529     B b984 t984
2530     T t985 o676 b682 b984
2531     B b985 t985
2532     T t986 o676 b716 b985
2533     B b986 t986
2534 xiny 3530 P p10 Number 6628
2535     P p12 Number 6635
2536     O o12 resource_defs p10 p12 p204
2537     P p14 Number 6633
2538     O o14 uid p14 p12
2539     T t250 o14 b691
2540     B b250 t250
2541     T t255 o b250 b4
2542     B b255 t255
2543     T t256 o12 b255
2544     B b256 t256
2545     T t258 o b256 b4
2546     B b258 t258
2547     T t260 o980 b676 b986 b688 b258
2548     B b260 t260
2549     T t267 o10 b260
2550     B b267 t267
2551     P p269 Number 6876
2552     P p277 Number 7152
2553     O o277 location p269 p277
2554 xiny 3527 P p995 String inv_wf2
2555     O o995 rule p995
2556     T t995 o736 b980 b591
2557     S s995 t684 h
2558     G s995 t995
2559     B b995 s995
2560     T t996 o677 b995
2561     B b996 t996
2562     T t997 o676 b737 b996
2563     B b997 t997
2564     T t998 o676 b700 b997
2565 xiny 3498 B b998 t998
2566 xiny 3527 T t999 o676 b682 b998
2567     B b999 t999
2568     T t1000 o676 b716 b999
2569     B b1000 t1000
2570 xiny 3530 P p284 Number 6899
2571     P p285 Number 6906
2572     O o285 resource_defs p284 p285 p204
2573     P p286 Number 6904
2574     O o286 uid p286 p285
2575     T t299 o286 b691
2576     B b299 t299
2577     T t368 o b299 b4
2578     B b368 t368
2579     T t379 o285 b368
2580     B b379 t379
2581     T t394 o b379 b4
2582     B b394 t394
2583     T t400 o995 b676 b1000 b688 b394
2584     B b400 t400
2585     T t421 o277 b400
2586     B b421 t421
2587     P p422 Number 7154
2588     P p424 Number 7453
2589     O o425 location p422 p424
2590 xiny 3527 P p1009 String inv_equiv_fun1
2591     O o1009 rule p1009
2592     T t1009 o609 b585 b818
2593     B b1009 t1009 z
2594     T t1010 o817 b591 b759 b1009
2595     S s1010 t684 h
2596     G s1010 t1010
2597     B b1010 s1010
2598     T t1011 o677 b1010
2599 xiny 3498 B b1011 t1011
2600 xiny 3527 T t1012 o676 b763 b1011
2601 xiny 3498 B b1012 t1012
2602 xiny 3527 T t1013 o676 b700 b1012
2603 xiny 3498 B b1013 t1013
2604 xiny 3527 T t1014 o676 b682 b1013
2605 xiny 3498 B b1014 t1014
2606 xiny 3527 T t1015 o676 b761 b1014
2607     B b1015 t1015
2608 xiny 3530 P p425 Number 7184
2609     P p426 Number 7191
2610     O o426 resource_defs p425 p426 p204
2611     P p427 Number 7189
2612     O o427 uid p427 p426
2613     T t429 o427 b691
2614     B b429 t429
2615     T t430 o b429 b4
2616     B b430 t430
2617     T t436 o426 b430
2618     B b436 t436
2619     T t437 o b436 b4
2620     B b437 t437
2621     T t446 o1009 b676 b1015 b688 b437
2622     B b446 t446
2623     T t447 o425 b446
2624     B b447 t447
2625     P p448 Number 7455
2626     P p449 Number 7637
2627     O o449 location p448 p449
2628 xiny 3527 P p1024 String inv_eq_fun1
2629     O o1024 rule p1024
2630     T t1024 o852 b1009
2631     S s1024 t684 h
2632     G s1024 t1024
2633     B b1024 s1024
2634     T t1025 o677 b1024
2635     B b1025 t1025
2636     T t1026 o676 b700 b1025
2637     B b1026 t1026
2638     T t1027 o676 b682 b1026
2639     B b1027 t1027
2640 xiny 3530 P p450 Number 7482
2641     P p451 Number 7489
2642     O o451 resource_defs p450 p451 p204
2643     P p452 Number 7487
2644     O o452 uid p452 p451
2645     T t455 o452 b691
2646     B b455 t455
2647     T t456 o b455 b4
2648     B b456 t456
2649     T t464 o451 b456
2650     B b464 t464
2651     T t465 o b464 b4
2652     B b465 t465
2653     T t473 o1024 b676 b1027 b688 b465
2654     B b473 t473
2655     T t474 o449 b473
2656     B b474 t474
2657     P p475 Number 7639
2658     P p476 Number 8037
2659     O o476 location p475 p476
2660 xiny 3527 P p1036 String inv_id1
2661     O o1036 rule p1036
2662     T t1036 o596 b585 b980 b714
2663     B b1036 t1036
2664     T t1037 o761 b591 b759 b1036 b604
2665     S s1037 t684 h
2666     G s1037 t1037
2667     B b1037 s1037
2668     T t1038 o677 b1037
2669     B b1038 t1038
2670     T t1039 o676 b737 b1038
2671     B b1039 t1039
2672     T t1040 o676 b763 b1039
2673     B b1040 t1040
2674     T t1041 o676 b700 b1040
2675     B b1041 t1041
2676     T t1042 o676 b682 b1041
2677     B b1042 t1042
2678     T t1043 o676 b761 b1042
2679     B b1043 t1043
2680     T t1044 o676 b716 b1043
2681     B b1044 t1044
2682 xiny 3530 P p477 Number 7662
2683     P p478 Number 7669
2684     O o478 resource_defs p477 p478 p204
2685     P p479 Number 7667
2686     O o479 uid p479 p478
2687     T t482 o479 b691
2688     B b482 t482
2689     T t483 o b482 b4
2690     B b483 t483
2691     T t491 o478 b483
2692     B b491 t491
2693     T t492 o b491 b4
2694     B b492 t492
2695     T t500 o1036 b676 b1044 b688 b492
2696     B b500 t500
2697     T t501 o476 b500
2698     B b501 t501
2699 xiny 3527 P p1053 String inv_id2
2700     O o1053 rule p1053
2701     P p1070 String equiv_op_fun1
2702     O o1070 rule p1070
2703     T t1070 o700 b597
2704     S s1070 t679 h
2705     G s1070 t1070
2706     B b1070 s1070
2707     T t1071 o677 b1070
2708     B b1071 t1071
2709     T t1072 o700 b598
2710     S s1072 t679 h
2711     G s1072 t1072
2712     B b1072 s1072
2713     T t1073 o677 b1072
2714     B b1073 t1073
2715     T t1074 o736 b597 b591
2716     S s1074 t684 h
2717     G s1074 t1074
2718     B b1074 s1074
2719     T t1075 o677 b1074
2720     B b1075 t1075
2721     T t1076 o736 b598 b591
2722     S s1076 t684 h
2723     G s1076 t1076
2724     B b1076 s1076
2725     T t1077 o677 b1076
2726     B b1077 t1077
2727     NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
2728     O o1077 equiv_fun_prop
2729     T t1078 o596 b585 b818 b597
2730     B b1078 t1078
2731     T t1079 o596 b585 b818 b598
2732     B b1079 t1079
2733     T t1080 o761 b591 b759 b1078 b1079
2734     B b1080 t1080 z
2735     T t1081 o1077 b591 b759 b1080
2736     S s1081 t684 h
2737     G s1081 t1081
2738     B b1081 s1081
2739     T t1082 o677 b1081
2740 xiny 3498 B b1082 t1082
2741 xiny 3527 T t1083 o676 b1077 b1082
2742 xiny 3498 B b1083 t1083
2743 xiny 3527 T t1084 o676 b1075 b1083
2744 xiny 3498 B b1084 t1084
2745 xiny 3527 T t1085 o676 b763 b1084
2746     B b1085 t1085
2747     T t1086 o676 b700 b1085
2748     B b1086 t1086
2749     T t1087 o676 b682 b1086
2750     B b1087 t1087
2751     T t1088 o676 b761 b1087
2752     B b1088 t1088
2753     T t1089 o676 b1073 b1088
2754     B b1089 t1089
2755     T t1090 o676 b1071 b1089
2756     B b1090 t1090
2757     NSummary!interactive interactive interactive Summary
2758     O o1090 interactive
2759     NSummary!ext_rule ext_rule ext_rule Summary
2760     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"
2761     O o1091 ext_rule p1090
2762     NSummary!status_incomplete status_incomplete status_incomplete Summary
2763     O o1092 status_incomplete
2764     T t1092 o1092
2765     B b1092 t1092
2766     NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2767     O o1093 ext_unjustified
2768     NSummary!tactic_arg tactic_arg tactic_arg Summary
2769     P p1093 String main
2770     O o1094 tactic_arg p1093
2771     NSummary!msequent msequent msequent Summary
2772     O o1095 msequent
2773     T t1095 o b1076 b4
2774     B b1095 t1095
2775     T t1096 o b1074 b1095
2776     B b1096 t1096
2777     T t1097 o b762 b1096
2778     B b1097 t1097
2779     T t1098 o b699 b1097
2780 xiny 3498 B b1098 t1098
2781 xiny 3527 T t1099 o b681 b1098
2782 xiny 3498 B b1099 t1099
2783 xiny 3527 T t1100 o b760 b1099
2784 xiny 3498 B b1100 t1100
2785 xiny 3527 T t1101 o b1072 b1100
2786 xiny 3498 B b1101 t1101
2787 xiny 3527 T t1102 o b1070 b1101
2788 xiny 3498 B b1102 t1102
2789 xiny 3527 T t1103 o1095 b1081 b1102
2790 xiny 3498 B b1103 t1103
2791 xiny 3527 NSummary!parent_none parent_none parent_none Summary
2792     O o1103 parent_none
2793     T t1104 o1103
2794 xiny 3498 B b1104 t1104
2795 xiny 3527 T t1105 o1094 b1103 b4 b1104
2796 xiny 3498 B b1105 t1105
2797 xiny 3527 NCzf_itt_set!set set set Czf_itt_set
2798     O o1105 set
2799     T t1106 o1105
2800     H h1106 a_1 t1106
2801     H h1107 b_1 t1106
2802     H h1108 x t762
2803     P p1108 Var a_1
2804     O o1108 var p1108
2805     T t1108 o1108
2806 xiny 3498 B b1108 t1108
2807 xiny 3527 P p1109 Var b_1
2808     O o1109 var p1109
2809     T t1109 o1109
2810 xiny 3498 B b1109 t1109
2811 xiny 3527 T t1110 o761 b591 b759 b1108 b1109
2812     H h1110 x_1 t1110
2813     T t1111 o596 b585 b1108 b597
2814 xiny 3498 B b1111 t1111
2815 xiny 3527 T t1112 o596 b585 b1108 b598
2816     B b1112 t1112
2817     T t1113 o761 b591 b759 b1111 b1112
2818     H h1113 x_2 t1113
2819     T t1114 o596 b585 b1109 b597
2820     B b1114 t1114
2821     T t1115 o596 b585 b1109 b598
2822     B b1115 t1115
2823     T t1116 o761 b591 b759 b1114 b1115
2824     S s1116 t684 h h1106 h1107 h1108 h1110 h1113
2825     G s1116 t1116
2826     B b1116 s1116
2827     T t1117 o1095 b1116 b1102
2828     B b1117 t1117
2829     NItt_logic Itt_logic Itt_logic NIL
2830     NItt_logic!implies implies implies Itt_logic
2831     O o1117 implies
2832     B b1118 t1113
2833     B b1119 t1116
2834     T t1119 o1117 b1118 b1119
2835     S s1119 t684 h h1106 h1107 h1108 h1110
2836     G s1119 t1119
2837 xiny 3405 B b1120 s1119
2838 xiny 3527 T t1120 o1095 b1120 b1102
2839 xiny 3405 B b1121 t1120
2840 xiny 3527 B b1122 t1110
2841     B b1123 t1119
2842     T t1123 o1117 b1122 b1123
2843     S s1123 t684 h h1106 h1107 h1108
2844     G s1123 t1123
2845     B b1124 s1123
2846     T t1124 o1095 b1124 b1102
2847 xiny 3379 B b1125 t1124
2848 xiny 3527 B b1126 t762
2849     B b1127 t1123
2850     T t1127 o1117 b1126 b1127
2851     S s1127 t684 h h1106 h1107
2852     G s1127 t1127
2853     B b1128 s1127
2854     T t1128 o1095 b1128 b1102
2855 xiny 3379 B b1129 t1128
2856 xiny 3527 NItt_logic!all all all Itt_logic
2857     O o1129 all
2858     B b1130 t1106
2859     B b1131 t1127 b_1
2860     T t1131 o1129 b1130 b1131
2861     S s1131 t684 h h1106
2862     G s1131 t1131
2863     B b1132 s1131
2864     T t1132 o1095 b1132 b1102
2865 xiny 3379 B b1133 t1132
2866 xiny 3527 B b1134 t1131 a_1
2867     T t1134 o1129 b1130 b1134
2868     S s1134 t684 h
2869     G s1134 t1134
2870     B b1135 s1134
2871     T t1135 o1095 b1135 b1102
2872 xiny 3404 B b1136 t1135
2873 xiny 3527 T t1136 o2 b1105
2874     B b1137 t1136
2875     T t1137 o1094 b1136 b4 b1137
2876 xiny 3404 B b1138 t1137
2877 xiny 3527 T t1138 o2 b1138
2878 xiny 3404 B b1139 t1138
2879 xiny 3527 T t1139 o1094 b1133 b4 b1139
2880 xiny 3379 B b1140 t1139
2881 xiny 3527 T t1140 o2 b1140
2882 xiny 3379 B b1141 t1140
2883 xiny 3527 T t1141 o1094 b1129 b4 b1141
2884 xiny 3379 B b1142 t1141
2885 xiny 3527 T t1142 o2 b1142
2886 xiny 3379 B b1143 t1142
2887 xiny 3527 T t1143 o1094 b1125 b4 b1143
2888 xiny 3498 B b1144 t1143
2889 xiny 3527 T t1144 o2 b1144
2890     B b1145 t1144
2891     T t1145 o1094 b1121 b4 b1145
2892 xiny 3405 B b1146 t1145
2893 xiny 3527 T t1146 o2 b1146
2894 xiny 3379 B b1147 t1146
2895 xiny 3527 T t1147 o1094 b1117 b4 b1147
2896 xiny 3498 B b1148 t1147
2897     T t1148 o b1148 b4
2898     B b1149 t1148
2899 xiny 3527 T t1149 o1093 b1105 b1149
2900 xiny 3405 B b1150 t1149
2901 xiny 3527 P p1150 String "equivTransT << op{'g; 'b_1; 'a} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
2902 xiny 3498 O o1150 ext_rule p1150
2903 xiny 3527 NItt_logic!and and and Itt_logic
2904     O o1151 and
2905     B b1151 t700
2906     B b1152 t760
2907     T t1152 o700 b1111
2908 xiny 3379 B b1153 t1152
2909 xiny 3527 T t1153 o700 b1112
2910 xiny 3379 B b1154 t1153
2911 xiny 3527 T t1154 o1151 b1153 b1154
2912 xiny 3404 B b1155 t1154
2913 xiny 3527 T t1155 o1151 b1152 b1155
2914 xiny 3379 B b1156 t1155
2915 xiny 3527 T t1156 o1151 b1151 b1156
2916 xiny 3379 B b1157 t1156
2917 xiny 3527 T t1157 o736 b1111 b591
2918 xiny 3379 B b1158 t1157
2919 xiny 3527 T t1158 o736 b1112 b591
2920 xiny 3404 B b1159 t1158
2921 xiny 3527 T t1159 o1151 b1158 b1159
2922 xiny 3404 B b1160 t1159
2923 xiny 3527 T t1160 o1151 b1157 b1160
2924 xiny 3498 B b1161 t1160
2925 xiny 3527 NCzf_itt_pair Czf_itt_pair Czf_itt_pair NIL
2926     NCzf_itt_pair!pair pair pair Czf_itt_pair
2927     O o1161 pair
2928     T t1161 o1161 b1111 b1112
2929 xiny 3405 B b1162 t1161
2930 xiny 3527 T t1162 o736 b1162 b759
2931 xiny 3404 B b1163 t1162
2932 xiny 3527 T t1163 o1151 b1161 b1163
2933     H h1163 x_2 t1163
2934     T t1164 o736 b1114 b591
2935     S s1164 t684 h h1106 h1107 h1108 h1110 h1163
2936     G s1164 t1164
2937     B b1164 s1164
2938     T t1165 o1095 b1164 b1102
2939     B b1165 t1165
2940     S s1165 t684 h h1106 h1107 h1108 h1110 h1113
2941     G s1165 t1164
2942     B b1166 s1165
2943     T t1166 o1095 b1166 b1102
2944 xiny 3498 B b1167 t1166
2945 xiny 3527 T t1167 o2 b1148
2946 xiny 3405 B b1168 t1167
2947 xiny 3527 T t1168 o1094 b1167 b4 b1168
2948 xiny 3379 B b1169 t1168
2949 xiny 3527 T t1169 o2 b1169
2950 xiny 3498 B b1170 t1169
2951 xiny 3527 T t1170 o1094 b1165 b4 b1170
2952     B b1171 t1170
2953     T t1171 o761 b591 b759 b1111 b1114
2954     H h1171 u t1171
2955     T t1172 o761 b591 b759 b1114 b1112
2956     H h1172 v t1172
2957     S s1172 t684 h h1106 h1107 h1108 h1110 h1163 h1171 h1172
2958     G s1172 t1116
2959     B b1172 s1172
2960     T t1173 o1095 b1172 b1102
2961     B b1173 t1173
2962     S s1173 t684 h h1106 h1107 h1108 h1110 h1113 h1171 h1172
2963     G s1173 t1116
2964     B b1174 s1173
2965     T t1174 o1095 b1174 b1102
2966     B b1175 t1174
2967     T t1175 o1094 b1175 b4 b1168
2968     B b1176 t1175
2969     T t1176 o2 b1176
2970     B b1177 t1176
2971     T t1177 o1094 b1173 b4 b1177
2972     B b1178 t1177
2973     T t1178 o b1178 b4
2974     B b1179 t1178
2975     T t1179 o b1171 b1179
2976     B b1180 t1179
2977     T t1180 o1093 b1148 b1180
2978     B b1181 t1180
2979     P p1181 String "autoT thenT rwh unfold_equiv 5 ttca"
2980     O o1181 ext_rule p1181
2981     T t1181 o1093 b1171 b4
2982     B b1182 t1181
2983     T t1182 o1181 b1092 b1182 b4 b4
2984     B b1183 t1182
2985     P p1183 String "equivTransT << op{'g; 'b_1; 'b} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
2986     O o1183 ext_rule p1183
2987     T t1183 o1093 b1178 b4
2988     B b1184 t1183
2989     T t1184 o1183 b1092 b1184 b4 b4
2990     B b1185 t1184
2991     T t1185 o b1185 b4
2992     B b1186 t1185
2993     T t1186 o b1183 b1186
2994     B b1187 t1186
2995     T t1187 o1150 b1092 b1181 b1187 b4
2996     B b1188 t1187
2997     T t1188 o b1188 b4
2998     B b1189 t1188
2999     T t1189 o1091 b1092 b1150 b1189 b4
3000     B b1190 t1189
3001     T t1190 o1090 b1190
3002     B b1191 t1190
3003     P p1200 String equiv_op_fun2
3004     O o1200 rule p1200
3005     T t1200 o596 b585 b597 b818
3006     B b1200 t1200
3007     T t1201 o596 b585 b598 b818
3008 xiny 3498 B b1201 t1201
3009 xiny 3527 T t1202 o761 b591 b759 b1200 b1201
3010     B b1202 t1202 z
3011     T t1203 o1077 b591 b759 b1202
3012     S s1203 t684 h
3013     G s1203 t1203
3014     B b1203 s1203
3015     T t1204 o677 b1203
3016 xiny 3498 B b1204 t1204
3017 xiny 3527 T t1205 o676 b1077 b1204
3018     B b1205 t1205
3019     T t1206 o676 b1075 b1205
3020     B b1206 t1206
3021     T t1207 o676 b763 b1206
3022     B b1207 t1207
3023     T t1208 o676 b700 b1207
3024 xiny 3498 B b1208 t1208
3025 xiny 3527 T t1209 o676 b682 b1208
3026     B b1209 t1209
3027     T t1210 o676 b761 b1209
3028     B b1210 t1210
3029     T t1211 o676 b1073 b1210
3030 xiny 3498 B b1211 t1211
3031 xiny 3527 T t1212 o676 b1071 b1211
3032     B b1212 t1212
3033     T t1213 o1095 b1203 b1102
3034     B b1213 t1213
3035     T t1214 o1094 b1213 b4 b1104
3036     B b1214 t1214
3037     T t1215 o596 b585 b597 b1108
3038     B b1215 t1215
3039     T t1216 o596 b585 b598 b1108
3040     B b1216 t1216
3041     T t1217 o761 b591 b759 b1215 b1216
3042     H h1217 x_2 t1217
3043     T t1218 o596 b585 b597 b1109
3044     B b1218 t1218
3045     T t1219 o596 b585 b598 b1109
3046     B b1219 t1219
3047     T t1220 o761 b591 b759 b1218 b1219
3048     S s1220 t684 h h1106 h1107 h1108 h1110 h1217
3049     G s1220 t1220
3050     B b1220 s1220
3051     T t1221 o1095 b1220 b1102
3052     B b1221 t1221
3053     B b1222 t1217
3054     B b1223 t1220
3055     T t1223 o1117 b1222 b1223
3056     S s1223 t684 h h1106 h1107 h1108 h1110
3057     G s1223 t1223
3058     B b1224 s1223
3059     T t1224 o1095 b1224 b1102
3060     B b1225 t1224
3061     B b1226 t1223
3062     T t1226 o1117 b1122 b1226
3063     S s1226 t684 h h1106 h1107 h1108
3064     G s1226 t1226
3065     B b1227 s1226
3066     T t1227 o1095 b1227 b1102
3067     B b1228 t1227
3068     B b1229 t1226
3069     T t1229 o1117 b1126 b1229
3070     S s1229 t684 h h1106 h1107
3071     G s1229 t1229
3072     B b1230 s1229
3073     T t1230 o1095 b1230 b1102
3074     B b1231 t1230
3075     B b1232 t1229 b_1
3076     T t1232 o1129 b1130 b1232
3077     S s1232 t684 h h1106
3078     G s1232 t1232
3079     B b1233 s1232
3080     T t1233 o1095 b1233 b1102
3081     B b1234 t1233
3082     B b1235 t1232 a_1
3083     T t1235 o1129 b1130 b1235
3084     S s1235 t684 h
3085     G s1235 t1235
3086     B b1236 s1235
3087     T t1236 o1095 b1236 b1102
3088     B b1237 t1236
3089     T t1237 o2 b1214
3090     B b1238 t1237
3091     T t1238 o1094 b1237 b4 b1238
3092     B b1239 t1238
3093     T t1239 o2 b1239
3094     B b1240 t1239
3095     T t1240 o1094 b1234 b4 b1240
3096     B b1241 t1240
3097     T t1241 o2 b1241
3098     B b1242 t1241
3099     T t1242 o1094 b1231 b4 b1242
3100     B b1243 t1242
3101     T t1243 o2 b1243
3102     B b1244 t1243
3103     T t1244 o1094 b1228 b4 b1244
3104     B b1245 t1244
3105     T t1245 o2 b1245
3106     B b1246 t1245
3107     T t1246 o1094 b1225 b4 b1246
3108     B b1247 t1246
3109     T t1247 o2 b1247
3110     B b1248 t1247
3111     T t1248 o1094 b1221 b4 b1248
3112     B b1249 t1248
3113     T t1249 o b1249 b4
3114     B b1250 t1249
3115     T t1250 o1093 b1214 b1250
3116     B b1251 t1250
3117     P p1251 String "equivTransT << op{'g; 'a; 'b_1} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
3118     O o1251 ext_rule p1251
3119     T t1251 o700 b1215
3120     B b1252 t1251
3121     T t1252 o700 b1216
3122     B b1253 t1252
3123     T t1253 o1151 b1252 b1253
3124     B b1254 t1253
3125     T t1254 o1151 b1152 b1254
3126     B b1255 t1254
3127     T t1255 o1151 b1151 b1255
3128     B b1256 t1255
3129     T t1256 o736 b1215 b591
3130     B b1257 t1256
3131     T t1257 o736 b1216 b591
3132     B b1258 t1257
3133     T t1258 o1151 b1257 b1258
3134     B b1259 t1258
3135     T t1259 o1151 b1256 b1259
3136     B b1260 t1259
3137     T t1260 o1161 b1215 b1216
3138     B b1261 t1260
3139     T t1261 o736 b1261 b759
3140     B b1262 t1261
3141     T t1262 o1151 b1260 b1262
3142     H h1262 x_2 t1262
3143     T t1263 o736 b1218 b591
3144     S s1263 t684 h h1106 h1107 h1108 h1110 h1262
3145     G s1263 t1263
3146     B b1263 s1263
3147     T t1264 o1095 b1263 b1102
3148     B b1264 t1264
3149     S s1264 t684 h h1106 h1107 h1108 h1110 h1217
3150     G s1264 t1263
3151     B b1265 s1264
3152     T t1265 o1095 b1265 b1102
3153     B b1266 t1265
3154     T t1266 o2 b1249
3155     B b1267 t1266
3156     T t1267 o1094 b1266 b4 b1267
3157     B b1268 t1267
3158     T t1268 o2 b1268
3159     B b1269 t1268
3160     T t1269 o1094 b1264 b4 b1269
3161     B b1270 t1269
3162     T t1270 o761 b591 b759 b1215 b1218
3163     H h1270 u t1270
3164     T t1271 o761 b591 b759 b1218 b1216
3165     H h1271 v t1271
3166     S s1271 t684 h h1106 h1107 h1108 h1110 h1262 h1270 h1271
3167     G s1271 t1220
3168     B b1271 s1271
3169     T t1272 o1095 b1271 b1102
3170     B b1272 t1272
3171     S s1272 t684 h h1106 h1107 h1108 h1110 h1217 h1270 h1271
3172     G s1272 t1220
3173     B b1273 s1272
3174     T t1273 o1095 b1273 b1102
3175     B b1274 t1273
3176     T t1274 o1094 b1274 b4 b1267
3177     B b1275 t1274
3178     T t1275 o2 b1275
3179     B b1276 t1275
3180     T t1276 o1094 b1272 b4 b1276
3181     B b1277 t1276
3182     T t1277 o b1277 b4
3183     B b1278 t1277
3184     T t1278 o b1270 b1278
3185     B b1279 t1278
3186     T t1279 o1093 b1249 b1279
3187     B b1280 t1279
3188     T t1280 o1093 b1270 b4
3189     B b1281 t1280
3190     T t1281 o1181 b1092 b1281 b4 b4
3191     B b1282 t1281
3192     P p1282 String "equivTransT << op{'g; 'b; 'b_1} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3193     O o1282 ext_rule p1282
3194     T t1282 o1093 b1277 b4
3195     B b1283 t1282
3196     T t1283 o1282 b1092 b1283 b4 b4
3197     B b1284 t1283
3198     T t1284 o b1284 b4
3199     B b1285 t1284
3200     T t1285 o b1282 b1285
3201     B b1286 t1285
3202     T t1286 o1251 b1092 b1280 b1286 b4
3203     B b1287 t1286
3204     T t1287 o b1287 b4
3205     B b1288 t1287
3206     T t1288 o1091 b1092 b1251 b1288 b4
3207     B b1289 t1288
3208     T t1289 o1090 b1289
3209     B b1290 t1289
3210     P p1299 String cancel1
3211     O o1299 rule p1299
3212     P p1300 String J
3213     O o1300 context_param p1300
3214     T t1300 o1300
3215     B b1300 t1300
3216     T t1301 o b1300 b4
3217     B b1301 t1301
3218     T t1302 o b675 b1301
3219     B b1302 t1302
3220     T t1303 o761 b591 b759 b720 b791
3221     H h1303 x t1303
3222     P p1303 Var x
3223     O o1303 var p1303
3224     T t1304 o1303
3225     C h1304 J t1304
3226     S s1304 t679 h h1303 h1304
3227     G s1304 t715
3228     B b1304 s1304
3229     T t1305 o677 b1304
3230 xiny 3498 B b1305 t1305
3231 xiny 3527 S s1305 t679 h h1303 h1304
3232     G s1305 t718
3233     B b1306 s1305
3234     T t1306 o677 b1306
3235     B b1307 t1306
3236     S s1307 t679 h h1303 h1304
3237     G s1307 t757
3238     B b1308 s1307
3239     T t1308 o677 b1308
3240     B b1309 t1308
3241     S s1309 t679 h h1303 h1304
3242     G s1309 t760
3243     B b1310 s1309
3244     T t1310 o677 b1310
3245     B b1311 t1310
3246     S s1311 t679 h h1303 h1304
3247     G s1311 t681
3248     B b1312 s1311
3249     T t1312 o677 b1312
3250     B b1313 t1312
3251     S s1313 t684 h h1303 h1304
3252     G s1313 t586
3253     B b1314 s1313
3254     T t1314 o677 b1314
3255     B b1315 t1314
3256     S s1315 t684 h h1303 h1304
3257     G s1315 t762
3258     B b1316 s1315
3259     T t1316 o677 b1316
3260     B b1317 t1316
3261     S s1317 t684 h h1303 h1304
3262     G s1317 t736
3263     B b1318 s1317
3264     T t1318 o677 b1318
3265     B b1319 t1318
3266     S s1319 t684 h h1303 h1304
3267     G s1319 t738
3268     B b1320 s1319
3269     T t1320 o677 b1320
3270     B b1321 t1320
3271     S s1321 t684 h h1303 h1304
3272     G s1321 t764
3273     B b1322 s1321
3274     T t1322 o677 b1322
3275     B b1323 t1322
3276     T t1323 o761 b591 b759 b717 b756
3277     S s1323 t684 h h1303 h1304
3278     G s1323 t1323
3279     B b1324 s1323
3280     T t1324 o677 b1324
3281     B b1325 t1324
3282     T t1325 o676 b1323 b1325
3283     B b1326 t1325
3284     T t1326 o676 b1321 b1326
3285     B b1327 t1326
3286     T t1327 o676 b1319 b1327
3287     B b1328 t1327
3288     T t1328 o676 b1317 b1328
3289     B b1329 t1328
3290     T t1329 o676 b1315 b1329
3291     B b1330 t1329
3292     T t1330 o676 b1313 b1330
3293     B b1331 t1330
3294     T t1331 o676 b1311 b1331
3295     B b1332 t1331
3296     T t1332 o676 b1309 b1332
3297     B b1333 t1332
3298     T t1333 o676 b1307 b1333
3299     B b1334 t1333
3300     T t1334 o676 b1305 b1334
3301     B b1335 t1334
3302     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"
3303     O o1335 ext_rule p1335
3304     T t1335 o b1322 b4
3305     B b1336 t1335
3306     T t1336 o b1320 b1336
3307     B b1337 t1336
3308     T t1337 o b1318 b1337
3309     B b1338 t1337
3310     T t1338 o b1316 b1338
3311     B b1339 t1338
3312     T t1339 o b1314 b1339
3313     B b1340 t1339
3314     T t1340 o b1312 b1340
3315     B b1341 t1340
3316     T t1341 o b1310 b1341
3317     B b1342 t1341
3318     T t1342 o b1308 b1342
3319     B b1343 t1342
3320     T t1343 o b1306 b1343
3321     B b1344 t1343
3322     T t1344 o b1304 b1344
3323     B b1345 t1344
3324     T t1345 o1095 b1324 b1345
3325     B b1346 t1345
3326     T t1346 o1094 b1346 b4 b1104
3327     B b1347 t1346
3328     T t1347 o596 b585 b980 b720
3329     B b1348 t1347
3330     T t1348 o596 b585 b980 b791
3331     B b1349 t1348
3332     T t1349 o761 b591 b759 b1348 b1349
3333     H h1349 v t1349
3334     S s1349 t684 h h1303 h1304 h1349
3335     G s1349 t1323
3336     B b1350 s1349
3337     T t1350 o1095 b1350 b1345
3338     B b1351 t1350
3339     T t1351 o2 b1347
3340     B b1352 t1351
3341     T t1352 o1094 b1351 b4 b1352
3342     B b1353 t1352
3343     T t1353 o b1353 b4
3344 xiny 3498 B b1354 t1353
3345 xiny 3527 T t1354 o1093 b1347 b1354
3346 xiny 3498 B b1355 t1354
3347 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"
3348     O o1355 ext_rule p1355
3349     T t1355 o596 b585 b1036 b717
3350 xiny 3498 B b1356 t1355
3351 xiny 3527 T t1356 o761 b591 b759 b1356 b1349
3352     H h1356 z t1356
3353     S s1356 t684 h h1303 h1304 h1349 h1356
3354     G s1356 t1323
3355     B b1357 s1356
3356     T t1357 o1095 b1357 b1345
3357 xiny 3498 B b1358 t1357
3358 xiny 3527 T t1358 o2 b1353
3359 xiny 3498 B b1359 t1358
3360 xiny 3527 T t1359 o1094 b1358 b4 b1359
3361 xiny 3498 B b1360 t1359
3362 xiny 3527 T t1360 o b1360 b4
3363     B b1361 t1360
3364     T t1361 o1093 b1353 b1361
3365 xiny 3498 B b1362 t1361
3366 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"
3367     O o1362 ext_rule p1362
3368     T t1362 o596 b585 b1036 b756
3369 xiny 3498 B b1363 t1362
3370 xiny 3527 T t1363 o761 b591 b759 b1356 b1363
3371     H h1363 z_1 t1363
3372     S s1363 t684 h h1303 h1304 h1349 h1356 h1363
3373     G s1363 t1323
3374     B b1364 s1363
3375     T t1364 o1095 b1364 b1345
3376 xiny 3498 B b1365 t1364
3377 xiny 3527 T t1365 o2 b1360
3378 xiny 3498 B b1366 t1365
3379 xiny 3527 T t1366 o1094 b1365 b4 b1366
3380     B b1367 t1366
3381     T t1367 o b1367 b4
3382 xiny 3498 B b1368 t1367
3383 xiny 3527 T t1368 o1093 b1360 b1368
3384 xiny 3498 B b1369 t1368
3385 xiny 3527 P p1369 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"
3386     O o1369 ext_rule p1369
3387     T t1369 o596 b585 b604 b717
3388 xiny 3498 B b1370 t1369
3389 xiny 3527 T t1370 o596 b585 b604 b756
3390 xiny 3498 B b1371 t1370
3391 xiny 3527 T t1371 o761 b591 b759 b1370 b1371
3392     H h1371 z_2 t1371
3393     S s1371 t684 h h1303 h1304 h1349 h1356 h1363 h1371
3394     G s1371 t1323
3395     B b1372 s1371
3396     T t1372 o1095 b1372 b1345
3397 xiny 3498 B b1373 t1372
3398 xiny 3527 T t1373 o2 b1367
3399 xiny 3498 B b1374 t1373
3400 xiny 3527 T t1374 o1094 b1373 b4 b1374
3401 xiny 3404 B b1375 t1374
3402 xiny 3498 T t1375 o b1375 b4
3403 xiny 3404 B b1376 t1375
3404 xiny 3527 T t1376 o1093 b1367 b1376
3405 xiny 3498 B b1377 t1376
3406 xiny 3527 P p1377 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"
3407     O o1377 ext_rule p1377
3408     T t1377 o761 b591 b759 b717 b1371
3409     H h1377 z_3 t1377
3410     S s1377 t684 h h1303 h1304 h1349 h1356 h1363 h1371 h1377
3411     G s1377 t1323
3412     B b1378 s1377
3413     T t1378 o1095 b1378 b1345
3414 xiny 3498 B b1379 t1378
3415 xiny 3527 T t1379 o2 b1375
3416 xiny 3405 B b1380 t1379
3417 xiny 3527 T t1380 o1094 b1379 b4 b1380
3418     B b1381 t1380
3419     T t1381 o b1381 b4
3420     B b1382 t1381
3421     T t1382 o1093 b1375 b1382
3422     B b1383 t1382
3423     P p1383 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"
3424     O o1383 ext_rule p1383
3425     T t1383 o1093 b1381 b4
3426     B b1384 t1383
3427     T t1384 o1383 b1092 b1384 b4 b4
3428     B b1385 t1384
3429     T t1385 o b1385 b4
3430     B b1386 t1385
3431     T t1386 o1377 b1092 b1383 b1386 b4
3432     B b1387 t1386
3433     T t1387 o b1387 b4
3434     B b1388 t1387
3435     T t1388 o1369 b1092 b1377 b1388 b4
3436     B b1389 t1388
3437     T t1389 o b1389 b4
3438     B b1390 t1389
3439     T t1390 o1362 b1092 b1369 b1390 b4
3440     B b1391 t1390
3441     T t1391 o b1391 b4
3442     B b1392 t1391
3443     T t1392 o1355 b1092 b1362 b1392 b4
3444     B b1393 t1392
3445     T t1393 o b1393 b4
3446     B b1394 t1393
3447     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"
3448     O o1394 ext_rule p1394
3449     H h1394 v t1303
3450     H h1395 v_1 t1349
3451     S s1395 t684 h h1394 h1395
3452     G s1395 t1323
3453     B b1395 s1395
3454     S s1396 t684 h
3455     G s1396 t1303
3456     B b1396 s1396
3457     T t1396 o b1396 b4
3458     B b1397 t1396
3459     T t1397 o b764 b1397
3460     B b1398 t1397
3461     T t1398 o b738 b1398
3462     B b1399 t1398
3463     T t1399 o b736 b1399
3464     B b1400 t1399
3465     T t1400 o b762 b1400
3466     B b1401 t1400
3467     T t1401 o b699 b1401
3468     B b1402 t1401
3469     T t1402 o b681 b1402
3470     B b1403 t1402
3471     T t1403 o b760 b1403
3472     B b1404 t1403
3473     T t1404 o b757 b1404
3474     B b1405 t1404
3475     T t1405 o b718 b1405
3476     B b1406 t1405
3477     T t1406 o b715 b1406
3478     B b1407 t1406
3479     T t1407 o1095 b1395 b1407
3480     B b1408 t1407
3481     S s1408 t684 h h1394
3482     G s1408 t1323
3483     B b1409 s1408
3484     T t1409 o1095 b1409 b1407
3485     B b1410 t1409
3486     S s1410 t684 h
3487     G s1410 t1323
3488     B b1411 s1410
3489     T t1411 o1095 b1411 b1407
3490     B b1412 t1411
3491     T t1412 o1094 b1412 b4 b1104
3492     B b1413 t1412
3493     T t1413 o2 b1413
3494     B b1414 t1413
3495     T t1414 o1094 b1410 b4 b1414
3496     B b1415 t1414
3497     T t1415 o2 b1415
3498     B b1416 t1415
3499     T t1416 o1094 b1408 b4 b1416
3500     B b1417 t1416
3501     S s1417 t684 h h1394 h1395 h1356
3502     G s1417 t1323
3503     B b1418 s1417
3504     T t1418 o1095 b1418 b1407
3505     B b1419 t1418
3506     T t1419 o2 b1417
3507     B b1420 t1419
3508     T t1420 o1094 b1419 b4 b1420
3509     B b1421 t1420
3510     T t1421 o b1421 b4
3511     B b1422 t1421
3512     T t1422 o1093 b1417 b1422
3513     B b1423 t1422
3514     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"
3515     O o1423 ext_rule p1423
3516     S s1423 t684 h h1394 h1395 h1356 h1363
3517     G s1423 t1323
3518     B b1424 s1423
3519     T t1424 o1095 b1424 b1407
3520     B b1425 t1424
3521     T t1425 o2 b1421
3522     B b1426 t1425
3523     T t1426 o1094 b1425 b4 b1426
3524     B b1427 t1426
3525     T t1427 o b1427 b4
3526     B b1428 t1427
3527     T t1428 o1093 b1421 b1428
3528     B b1429 t1428
3529     P p1429 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 ttca"
3530     O o1429 ext_rule p1429
3531     S s1429 t684 h h1394 h1395 h1356 h1363 h1371
3532     G s1429 t1323
3533     B b1430 s1429
3534     T t1430 o1095 b1430 b1407
3535     B b1431 t1430
3536     T t1431 o2 b1427
3537     B b1432 t1431
3538     T t1432 o1094 b1431 b4 b1432
3539     B b1433 t1432
3540     T t1433 o b1433 b4
3541     B b1434 t1433
3542     T t1434 o1093 b1427 b1434
3543     B b1435 t1434
3544     P p1435 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 6 ttca"
3545     O o1435 ext_rule p1435
3546     S s1435 t684 h h1394 h1395 h1356 h1363 h1371 h1377
3547     G s1435 t1323
3548     B b1436 s1435
3549     T t1436 o1095 b1436 b1407
3550     B b1437 t1436
3551     T t1437 o2 b1433
3552     B b1438 t1437
3553     T t1438 o1094 b1437 b4 b1438
3554     B b1439 t1438
3555     T t1439 o b1439 b4
3556     B b1440 t1439
3557     T t1440 o1093 b1433 b1440
3558     B b1441 t1440
3559     P p1441 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 7 ttca"
3560     O o1441 ext_rule p1441
3561     T t1441 o1093 b1439 b4
3562     B b1442 t1441
3563     T t1442 o1441 b1092 b1442 b4 b4
3564     B b1443 t1442
3565     T t1443 o b1443 b4
3566     B b1444 t1443
3567     T t1444 o1435 b1092 b1441 b1444 b4
3568     B b1445 t1444
3569     T t1445 o b1445 b4
3570     B b1446 t1445
3571     T t1446 o1429 b1092 b1435 b1446 b4
3572     B b1447 t1446
3573     T t1447 o b1447 b4
3574     B b1448 t1447
3575     T t1448 o1423 b1092 b1429 b1448 b4
3576     B b1449 t1448
3577     T t1449 o b1449 b4
3578     B b1450 t1449
3579     T t1450 o1394 b1092 b1423 b1450 b4
3580     B b1451 t1450
3581     T t1451 o b1451 b4
3582     B b1452 t1451
3583     T t1452 o1335 b1092 b1355 b1394 b1452
3584     B b1453 t1452
3585     T t1453 o1090 b1453
3586     B b1454 t1453
3587     T t1454 o1299 b1302 b1335 b1454 b4
3588     B b1455 t1454
3589     P p1458 String cancel2
3590     O o1458 rule p1458
3591     H h1458 x t793
3592     S s1458 t679 h h1458 h1304
3593     G s1458 t715
3594     B b1458 s1458
3595     T t1458 o677 b1458
3596     B b1459 t1458
3597     S s1459 t679 h h1458 h1304
3598     G s1459 t718
3599     B b1460 s1459
3600     T t1460 o677 b1460
3601     B b1461 t1460
3602     S s1461 t679 h h1458 h1304
3603     G s1461 t757
3604     B b1462 s1461
3605     T t1462 o677 b1462
3606 xiny 3379 B b1463 t1462
3607 xiny 3527 S s1463 t679 h h1458 h1304
3608     G s1463 t760
3609     B b1464 s1463
3610     T t1464 o677 b1464
3611 xiny 3379 B b1465 t1464
3612 xiny 3527 S s1465 t679 h h1458 h1304
3613     G s1465 t681
3614     B b1466 s1465
3615     T t1466 o677 b1466
3616 xiny 3405 B b1467 t1466
3617 xiny 3527 S s1467 t684 h h1458 h1304
3618     G s1467 t586
3619     B b1468 s1467
3620     T t1468 o677 b1468
3621     B b1469 t1468
3622     S s1469 t684 h h1458 h1304
3623     G s1469 t762
3624     B b1470 s1469
3625     T t1470 o677 b1470
3626 xiny 3404 B b1471 t1470
3627 xiny 3527 S s1471 t684 h h1458 h1304
3628     G s1471 t736
3629     B b1472 s1471
3630     T t1472 o677 b1472
3631 xiny 3404 B b1473 t1472
3632 xiny 3527 S s1473 t684 h h1458 h1304
3633     G s1473 t738
3634     B b1474 s1473
3635     T t1474 o677 b1474
3636     B b1475 t1474
3637     S s1475 t684 h h1458 h1304
3638     G s1475 t764
3639     B b1476 s1475
3640     T t1476 o677 b1476
3641 xiny 3405 B b1477 t1476
3642 xiny 3527 S s1477 t684 h h1458 h1304
3643     G s1477 t766
3644     B b1478 s1477
3645     T t1478 o677 b1478
3646 xiny 3404 B b1479 t1478
3647 xiny 3527 T t1479 o676 b1477 b1479
3648 xiny 3498 B b1480 t1479
3649 xiny 3527 T t1480 o676 b1475 b1480
3650 xiny 3498 B b1481 t1480
3651 xiny 3527 T t1481 o676 b1473 b1481
3652 xiny 3405 B b1482 t1481
3653 xiny 3527 T t1482 o676 b1471 b1482
3654 xiny 3498 B b1483 t1482
3655 xiny 3527 T t1483 o676 b1469 b1483
3656 xiny 3498 B b1484 t1483
3657 xiny 3527 T t1484 o676 b1467 b1484
3658 xiny 3405 B b1485 t1484
3659 xiny 3527 T t1485 o676 b1465 b1485
3660 xiny 3404 B b1486 t1485
3661 xiny 3527 T t1486 o676 b1463 b1486
3662 xiny 3404 B b1487 t1486
3663 xiny 3527 T t1487 o676 b1461 b1487
3664 xiny 3404 B b1488 t1487
3665 xiny 3527 T t1488 o676 b1459 b1488
3666 xiny 3498 B b1489 t1488
3667 xiny 3527 P p1489 String "assertT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}} >> thenAT autoT"
3668     O o1489 ext_rule p1489
3669     T t1489 o b1476 b4
3670 xiny 3498 B b1490 t1489
3671 xiny 3527 T t1490 o b1474 b1490
3672     B b1491 t1490
3673     T t1491 o b1472 b1491
3674     B b1492 t1491
3675     T t1492 o b1470 b1492
3676     B b1493 t1492
3677     T t1493 o b1468 b1493
3678     B b1494 t1493
3679     T t1494 o b1466 b1494
3680     B b1495 t1494
3681     T t1495 o b1464 b1495
3682     B b1496 t1495
3683     T t1496 o b1462 b1496
3684     B b1497 t1496
3685     T t1497 o b1460 b1497
3686     B b1498 t1497
3687     T t1498 o b1458 b1498
3688     B b1499 t1498
3689     T t1499 o1095 b1478 b1499
3690     B b1500 t1499
3691     T t1500 o1094 b1500 b4 b1104
3692     B b1501 t1500
3693     T t1501 o609 b585 b756
3694     B b1502 t1501
3695     T t1502 o596 b585 b791 b1502
3696     B b1503 t1502
3697     T t1503 o596 b585 b792 b1502
3698     B b1504 t1503
3699     T t1504 o761 b591 b759 b1503 b1504
3700     H h1504 v t1504
3701     S s1504 t684 h h1458 h1304 h1504
3702     G s1504 t766
3703     B b1505 s1504
3704     T t1505 o1095 b1505 b1499
3705     B b1506 t1505
3706     T t1506 o2 b1501
3707     B b1507 t1506
3708     T t1507 o1094 b1506 b4 b1507
3709     B b1508 t1507
3710     T t1508 o b1508 b4
3711     B b1509 t1508
3712     T t1509 o1093 b1501 b1509
3713     B b1510 t1509
3714     P p1510 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 4 ttca"
3715     O o1510 ext_rule p1510
3716     T t1510 o596 b585 b756 b1502
3717     B b1511 t1510
3718     T t1511 o596 b585 b714 b1511
3719     B b1512 t1511
3720     T t1512 o761 b591 b759 b1512 b1504
3721     H h1512 z t1512
3722     S s1512 t684 h h1458 h1304 h1504 h1512
3723     G s1512 t766
3724     B b1513 s1512
3725     T t1513 o1095 b1513 b1499
3726     B b1514 t1513
3727     T t1514 o2 b1508
3728     B b1515 t1514
3729     T t1515 o1094 b1514 b4 b1515
3730     B b1516 t1515
3731     T t1516 o b1516 b4
3732     B b1517 t1516
3733     T t1517 o1093 b1508 b1517
3734     B b1518 t1517
3735     P p1518 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 5 ttca"
3736     O o1518 ext_rule p1518
3737     T t1518 o596 b585 b717 b1511
3738     B b1519 t1518
3739     T t1519 o761 b591 b759 b1512 b1519
3740     H h1519 z_1 t1519
3741     S s1519 t684 h h1458 h1304 h1504 h1512 h1519
3742     G s1519 t766
3743     B b1520 s1519
3744     T t1520 o1095 b1520 b1499
3745     B b1521 t1520
3746     T t1521 o2 b1516
3747     B b1522 t1521
3748     T t1522 o1094 b1521 b4 b1522
3749     B b1523 t1522
3750     T t1523 o b1523 b4
3751 xiny 3498 B b1524 t1523
3752 xiny 3527 T t1524 o1093 b1516 b1524
3753 xiny 3498 B b1525 t1524