/[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 3535 - (hide annotations) (download)
Mon Mar 11 09:57:39 2002 UTC (19 years, 4 months ago) by xiny
File size: 138414 byte(s)
Added the elimination form of the unique inverse rule.

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