/[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 3404 - (hide annotations) (download)
Sun Sep 23 07:25:28 2001 UTC (19 years, 10 months ago) by xiny
File size: 123630 byte(s)
1. Minor changes in czf_itt_group;
2. Define subgroup and abelian group;
3. Define cyclic subgroup and cyclic group. However, there are
   problems with the proofs in czf_itt_cyclic_subgroup.

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     P p1 Number 19
9     O o1 location p p1
10     NSummary!parent parent parent Summary
11     O o2 parent
12     P p2 String Czf_itt_set
13     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     P p5 String Czf_itt_comment
23     O o5 parent p5
24     T t6 o5
25     B b6 t6
26     T t7 o b6 b4
27     B b7 t7
28     P p7 String Itt_theory
29     O o7 parent p7
30     T t8 o7
31     B b8 t8
32     T t9 o b8 b4
33     B b9 t9
34     P p9 String Itt_fset
35     O o9 parent p9
36     T t10 o9
37     B b10 t10
38     T t11 o b10 b4
39     B b11 t11
40     P p11 String Itt_prop_decide
41     O o11 parent p11
42     T t12 o11
43     B b12 t12
44     T t13 o b12 b4
45     B b13 t13
46     P p13 String Itt_derive
47     O o13 parent p13
48     T t14 o13
49     B b14 t14
50     T t15 o b14 b4
51     B b15 t15
52     P p15 String Itt_list2
53     O o15 parent p15
54     T t16 o15
55     B b16 t16
56     T t17 o b16 b4
57     B b17 t17
58     P p17 String Itt_list
59     O o17 parent p17
60     T t18 o17
61     B b18 t18
62     T t19 o b18 b4
63     B b19 t19
64     P p19 String Itt_quotient
65     O o19 parent p19
66     T t20 o19
67     B b20 t20
68     T t21 o b20 b4
69     B b21 t21
70     P p21 String Itt_esquash
71     O o21 parent p21
72     T t22 o21
73     B b22 t22
74     T t23 o b22 b4
75     B b23 t23
76     P p23 String Itt_srec
77     O o23 parent p23
78     T t24 o23
79     B b24 t24
80     T t25 o b24 b4
81     B b25 t25
82     P p25 String Itt_prec
83     O o25 parent p25
84     T t26 o25
85     B b26 t26
86     T t27 o b26 b4
87     B b27 t27
88     P p27 String Itt_w
89     O o27 parent p27
90     T t28 o27
91     B b28 t28
92     T t29 o b28 b4
93     B b29 t29
94     P p29 String Itt_bunion
95     O o29 parent p29
96     T t30 o29
97     B b30 t30
98     T t31 o b30 b4
99     B b31 t31
100     P p31 String Itt_bisect
101     O o31 parent p31
102     T t32 o31
103     B b32 t32
104     T t33 o b32 b4
105     B b33 t33
106     P p33 String Itt_tunion
107     O o33 parent p33
108     T t34 o33
109     B b34 t34
110     T t35 o b34 b4
111     B b35 t35
112     P p35 String Itt_isect
113     O o35 parent p35
114     T t36 o35
115     B b36 t36
116     T t37 o b36 b4
117     B b37 t37
118     P p37 String Itt_struct2
119     O o37 parent p37
120     T t38 o37
121     B b38 t38
122     T t39 o b38 b4
123     B b39 t39
124     P p39 String Itt_well_founded
125     O o39 parent p39
126     T t40 o39
127     B b40 t40
128     T t41 o b40 b4
129     B b41 t41
130     P p41 String Itt_int_arith
131     O o41 parent p41
132     T t42 o41
133     B b42 t42
134     T t43 o b42 b4
135     B b43 t43
136     P p43 String Itt_int_ext
137     O o43 parent p43
138     T t44 o43
139     B b44 t44
140     T t45 o b44 b4
141     B b45 t45
142     P p45 String Itt_int_base
143     O o45 parent p45
144     T t46 o45
145     B b46 t46
146     T t47 o b46 b4
147     B b47 t47
148     P p47 String Itt_atom_bool
149     O o47 parent p47
150     T t48 o47
151     B b48 t48
152     T t49 o b48 b4
153     B b49 t49
154     P p49 String Itt_atom
155     O o49 parent p49
156     T t50 o49
157     B b50 t50
158     T t51 o b50 b4
159     B b51 t51
160     P p51 String Itt_bool
161     O o51 parent p51
162     T t52 o51
163     B b52 t52
164     T t53 o b52 b4
165     B b53 t53
166     P p53 String Itt_decidable
167     O o53 parent p53
168     T t54 o53
169     B b54 t54
170     T t55 o b54 b4
171     B b55 t55
172     P p55 String Itt_logic
173     O o55 parent p55
174     T t56 o55
175     B b56 t56
176     T t57 o b56 b4
177     B b57 t57
178     P p57 String Itt_prod
179     O o57 parent p57
180     T t58 o57
181     B b58 t58
182     T t59 o b58 b4
183     B b59 t59
184     P p59 String Itt_dprod
185     O o59 parent p59
186     T t60 o59
187     B b60 t60
188     T t61 o b60 b4
189     B b61 t61
190     P p61 String Itt_fun
191     O o61 parent p61
192     T t62 o61
193     B b62 t62
194     T t63 o b62 b4
195     B b63 t63
196     P p63 String Itt_dfun
197     O o63 parent p63
198     T t64 o63
199     B b64 t64
200     T t65 o b64 b4
201     B b65 t65
202     P p65 String Itt_rfun
203     O o65 parent p65
204     T t66 o65
205     B b66 t66
206     T t67 o b66 b4
207     B b67 t67
208     P p67 String Itt_set
209     O o67 parent p67
210     T t68 o67
211     B b68 t68
212     T t69 o b68 b4
213     B b69 t69
214     P p69 String Itt_unit
215     O o69 parent p69
216     T t70 o69
217     B b70 t70
218     T t71 o b70 b4
219     B b71 t71
220     P p71 String Itt_squiggle
221     O o71 parent p71
222     T t72 o71
223     B b72 t72
224     T t73 o b72 b4
225     B b73 t73
226     P p73 String Itt_squash
227     O o73 parent p73
228     T t74 o73
229     B b74 t74
230     T t75 o b74 b4
231     B b75 t75
232     P p75 String Itt_union
233     O o75 parent p75
234     T t76 o75
235     B b76 t76
236     T t77 o b76 b4
237     B b77 t77
238     P p77 String Itt_void
239     O o77 parent p77
240     T t78 o77
241     B b78 t78
242     T t79 o b78 b4
243     B b79 t79
244     P p79 String Itt_subtype
245     O o79 parent p79
246     T t80 o79
247     B b80 t80
248     T t81 o b80 b4
249     B b81 t81
250     P p81 String Itt_struct
251     O o81 parent p81
252     T t82 o81
253     B b82 t82
254     T t83 o b82 b4
255     B b83 t83
256     P p83 String Itt_equal
257     O o83 parent p83
258     T t84 o83
259     B b84 t84
260     T t85 o b84 b4
261     B b85 t85
262     P p85 String Itt_comment
263     O o85 parent p85
264     T t86 o85
265     B b86 t86
266     T t87 o b86 b4
267     B b87 t87
268     P p87 String Base_theory
269     O o87 parent p87
270     T t88 o87
271     B b88 t88
272     T t89 o b88 b4
273     B b89 t89
274     P p89 String Base_meta
275     O o89 parent p89
276     T t90 o89
277     B b90 t90
278     T t91 o b90 b4
279     B b91 t91
280     P p91 String Base_cache
281     O o91 parent p91
282     T t92 o91
283     B b92 t92
284     T t93 o b92 b4
285     B b93 t93
286     P p93 String Tactic_cache
287     O o93 parent p93
288     T t94 o93
289     B b94 t94
290     T t95 o b94 b4
291     B b95 t95
292     P p95 String Typeinf
293     O o95 parent p95
294     T t96 o95
295     B b96 t96
296     T t97 o b96 b4
297     B b97 t97
298     P p97 String Ocaml_df
299     O o97 parent p97
300     T t98 o97
301     B b98 t98
302     T t99 o b98 b4
303     B b99 t99
304     P p99 String Ocaml_str_df
305     O o99 parent p99
306     T t100 o99
307     B b100 t100
308     T t101 o b100 b4
309     B b101 t101
310     P p101 String Ocaml_sig_df
311     O o101 parent p101
312     T t102 o101
313     B b102 t102
314     T t103 o b102 b4
315     B b103 t103
316     P p103 String Ocaml_me_df
317     O o103 parent p103
318     T t104 o103
319     B b104 t104
320     T t105 o b104 b4
321     B b105 t105
322     P p105 String Ocaml_mt_df
323     O o105 parent p105
324     T t106 o105
325     B b106 t106
326     T t107 o b106 b4
327     B b107 t107
328     P p107 String Ocaml_type_df
329     O o107 parent p107
330     T t108 o107
331     B b108 t108
332     T t109 o b108 b4
333     B b109 t109
334     P p109 String Ocaml_patt_df
335     O o109 parent p109
336     T t110 o109
337     B b110 t110
338     T t111 o b110 b4
339     B b111 t111
340     P p111 String Ocaml_expr_df
341     O o111 parent p111
342     T t112 o111
343     B b112 t112
344     T t113 o b112 b4
345     B b113 t113
346     P p113 String Ocaml_base_df
347     O o113 parent p113
348     T t114 o113
349     B b114 t114
350     T t115 o b114 b4
351     B b115 t115
352     P p115 String Ocaml
353     O o115 parent p115
354     T t116 o115
355     B b116 t116
356     T t117 o b116 b4
357     B b117 t117
358     P p117 String Base_rewrite
359     O o117 parent p117
360     T t118 o117
361     B b118 t118
362     T t119 o b118 b4
363     B b119 t119
364     P p119 String Base_dtactic
365     O o119 parent p119
366     T t120 o119
367     B b120 t120
368     T t121 o b120 b4
369     B b121 t121
370     P p121 String Base_auto_tactic
371     O o121 parent p121
372     T t122 o121
373     B b122 t122
374     T t123 o b122 b4
375     B b123 t123
376     P p123 String Base_trivial
377     O o123 parent p123
378     T t124 o123
379     B b124 t124
380     T t125 o b124 b4
381     B b125 t125
382     P p125 String Top_conversionals
383     O o125 parent p125
384     T t126 o125
385     B b126 t126
386     T t127 o b126 b4
387     B b127 t127
388     P p127 String Top_tacticals
389     O o127 parent p127
390     T t128 o127
391     B b128 t128
392     T t129 o b128 b4
393     B b129 t129
394     P p129 String Var
395     O o129 parent p129
396     T t130 o129
397     B b130 t130
398     T t131 o b130 b4
399     B b131 t131
400     P p131 String Mptop
401     O o131 parent p131
402     T t132 o131
403     B b132 t132
404     T t133 o b132 b4
405     B b133 t133
406     P p133 String Summary
407     O o133 parent p133
408     T t134 o133
409     B b134 t134
410     T t135 o b134 b4
411     B b135 t135
412     P p135 String Comment
413     O o135 parent p135
414     T t136 o135
415     B b136 t136
416     T t137 o b136 b4
417     B b137 t137
418     P p137 String Base_dform
419     O o137 parent p137
420     T t138 o137
421     B b138 t138
422     T t139 o b138 b4
423     B b139 t139
424     P p139 String Nuprl_font
425     O o139 parent p139
426     T t140 o139
427     B b140 t140
428     T t141 o b140 b4
429     B b141 t141
430     P p141 String Perv
431     O o141 parent p141
432     T t142 o141
433     B b142 t142
434     T t143 o b142 b4
435     B b143 t143
436     T t144 o b143 b4
437     B b144 t144
438     T t145 o b141 b144
439     B b145 t145
440     T t146 o b139 b145
441     B b146 t146
442     T t147 o b137 b146
443     B b147 t147
444     T t148 o b135 b147
445     B b148 t148
446     T t149 o b133 b148
447     B b149 t149
448     T t150 o b131 b149
449     B b150 t150
450     T t151 o b129 b150
451     B b151 t151
452     T t152 o b127 b151
453     B b152 t152
454     T t153 o b125 b152
455     B b153 t153
456     T t154 o b123 b153
457     B b154 t154
458     T t155 o b121 b154
459     B b155 t155
460     T t156 o b119 b155
461     B b156 t156
462     T t157 o b117 b156
463     B b157 t157
464     T t158 o b115 b157
465     B b158 t158
466     T t159 o b113 b158
467     B b159 t159
468     T t160 o b111 b159
469     B b160 t160
470     T t161 o b109 b160
471     B b161 t161
472     T t162 o b107 b161
473     B b162 t162
474     T t163 o b105 b162
475     B b163 t163
476     T t164 o b103 b163
477     B b164 t164
478     T t165 o b101 b164
479     B b165 t165
480     T t166 o b99 b165
481     B b166 t166
482     T t167 o b97 b166
483     B b167 t167
484     T t168 o b95 b167
485     B b168 t168
486     T t169 o b93 b168
487     B b169 t169
488     T t170 o b91 b169
489     B b170 t170
490     T t171 o b89 b170
491     B b171 t171
492     T t172 o b87 b171
493     B b172 t172
494     T t173 o b85 b172
495     B b173 t173
496     T t174 o b83 b173
497     B b174 t174
498     T t175 o b81 b174
499     B b175 t175
500     T t176 o b79 b175
501     B b176 t176
502     T t177 o b77 b176
503     B b177 t177
504     T t178 o b75 b177
505     B b178 t178
506     T t179 o b73 b178
507     B b179 t179
508     T t180 o b71 b179
509     B b180 t180
510     T t181 o b69 b180
511     B b181 t181
512     T t182 o b67 b181
513     B b182 t182
514     T t183 o b65 b182
515     B b183 t183
516     T t184 o b63 b183
517     B b184 t184
518     T t185 o b61 b184
519     B b185 t185
520     T t186 o b59 b185
521     B b186 t186
522     T t187 o b57 b186
523     B b187 t187
524     T t188 o b55 b187
525     B b188 t188
526     T t189 o b53 b188
527     B b189 t189
528     T t190 o b51 b189
529     B b190 t190
530     T t191 o b49 b190
531     B b191 t191
532     T t192 o b47 b191
533     B b192 t192
534     T t193 o b45 b192
535     B b193 t193
536     T t194 o b43 b193
537     B b194 t194
538     T t195 o b41 b194
539     B b195 t195
540     T t196 o b39 b195
541     B b196 t196
542     T t197 o b37 b196
543     B b197 t197
544     T t198 o b35 b197
545     B b198 t198
546     T t199 o b33 b198
547     B b199 t199
548     T t200 o b31 b199
549     B b200 t200
550     T t201 o b29 b200
551     B b201 t201
552     T t202 o b27 b201
553     B b202 t202
554     T t203 o b25 b202
555     B b203 t203
556     T t204 o b23 b203
557     B b204 t204
558     T t205 o b21 b204
559     B b205 t205
560     T t206 o b19 b205
561     B b206 t206
562     T t207 o b17 b206
563     B b207 t207
564     T t208 o b15 b207
565     B b208 t208
566     T t209 o b13 b208
567     B b209 t209
568     T t210 o b11 b209
569     B b210 t210
570     T t211 o b9 b210
571     B b211 t211
572     T t212 o b7 b211
573     B b212 t212
574     T t213 o b5 b212
575     B b213 t213
576     NSummary!resource resource resource Summary
577     P p213 String auto
578     O o213 resource p213
579     NOcaml Ocaml Ocaml NIL
580     NOcaml!type_lid type_lid type_lid Ocaml
581     P p214 Number 2332
582     P p215 Number 2341
583     O o215 type_lid p214 p215
584     P p216 String auto_info
585     O o216 type_lid p216
586     T t216 o216
587     B b216 t216
588     T t217 o215 b216
589     B b217 t217
590     NOcaml!type_prod type_prod type_prod Ocaml
591     P p217 Number 2343
592 xiny 3404 P p218 Number 2367
593 xiny 3379 O o218 type_prod p217 p218
594     P p219 Number 2349
595     O o219 type_lid p217 p219
596     P p220 String tactic
597     O o220 type_lid p220
598     T t220 o220
599     B b220 t220
600     T t221 o219 b220
601     B b221 t221
602     P p221 Number 2352
603 xiny 3404 P p222 Number 2358
604     O o222 type_lid p221 p222
605     T t222 o222 b220
606 xiny 3379 B b222 t222
607 xiny 3404 P p223 Number 2361
608     O o223 type_lid p223 p218
609     T t223 o223 b220
610 xiny 3379 B b223 t223
611 xiny 3404 T t224 o b223 b4
612 xiny 3379 B b224 t224
613 xiny 3404 T t225 o b222 b224
614 xiny 3379 B b225 t225
615 xiny 3404 T t226 o b221 b225
616 xiny 3379 B b226 t226
617 xiny 3404 T t227 o218 b226
618     B b227 t227
619     T t228 o213 b217 b227
620     B b228 t228
621     P p228 String cache
622     O o228 resource p228
623     P p229 Number 1424
624     P p230 Number 1434
625     O o230 type_lid p229 p230
626     P p231 String cache_rule
627     O o231 type_lid p231
628     T t231 o231
629     B b231 t231
630     T t232 o230 b231
631 xiny 3379 B b232 t232
632 xiny 3404 P p232 Number 1436
633     P p233 Number 1441
634     O o233 type_lid p232 p233
635     O o234 type_lid p228
636     T t234 o234
637 xiny 3379 B b234 t234
638 xiny 3404 T t235 o233 b234
639     B b235 t235
640     T t236 o228 b232 b235
641     B b236 t236
642     P p236 String elim
643     O o236 resource p236
644     P p237 Number 1761
645     P p238 Number 1783
646     O o238 type_prod p237 p238
647     P p239 Number 1765
648     O o239 type_lid p237 p239
649     P p240 String term
650     O o240 type_lid p240
651     T t240 o240
652     B b240 t240
653     T t241 o239 b240
654     B b241 t241
655 xiny 3379 NOcaml!type_fun type_fun type_fun Ocaml
656 xiny 3404 P p241 Number 1769
657     P p242 Number 1782
658     O o242 type_fun p241 p242
659     P p243 Number 1772
660     O o243 type_lid p241 p243
661     P p244 String int
662     O o244 type_lid p244
663     T t244 o244
664 xiny 3379 B b244 t244
665 xiny 3404 T t245 o243 b244
666 xiny 3379 B b245 t245
667 xiny 3404 P p245 Number 1776
668     O o245 type_lid p245 p242
669     T t246 o245 b220
670 xiny 3379 B b246 t246
671 xiny 3404 T t247 o242 b245 b246
672 xiny 3379 B b247 t247
673 xiny 3404 T t248 o b247 b4
674 xiny 3379 B b248 t248
675 xiny 3404 T t249 o b241 b248
676     B b249 t249
677     T t250 o238 b249
678 xiny 3379 B b250 t250
679 xiny 3404 P p250 Number 1785
680     P p251 Number 1798
681     O o251 type_fun p250 p251
682     P p252 Number 1788
683     O o252 type_lid p250 p252
684     T t252 o252 b244
685 xiny 3379 B b252 t252
686 xiny 3404 P p253 Number 1792
687     O o253 type_lid p253 p251
688     T t253 o253 b220
689 xiny 3379 B b253 t253
690 xiny 3404 T t254 o251 b252 b253
691     B b254 t254
692     T t255 o236 b250 b254
693     B b255 t255
694     P p255 String eqcd
695     O o255 resource p255
696     P p256 Number 6168
697     P p257 Number 6181
698     O o257 type_prod p256 p257
699     P p258 Number 6172
700     O o258 type_lid p256 p258
701     T t258 o258 b240
702 xiny 3379 B b258 t258
703 xiny 3404 P p259 Number 6175
704     O o259 type_lid p259 p257
705     T t259 o259 b220
706 xiny 3379 B b259 t259
707 xiny 3404 T t260 o b259 b4
708 xiny 3379 B b260 t260
709 xiny 3404 T t261 o b258 b260
710 xiny 3379 B b261 t261
711 xiny 3404 T t262 o257 b261
712 xiny 3379 B b262 t262
713 xiny 3404 P p262 Number 6183
714     P p263 Number 6189
715     O o263 type_lid p262 p263
716     T t263 o263 b220
717     B b263 t263
718     T t264 o255 b262 b263
719     B b264 t264
720     P p264 String intro
721     O o264 resource p264
722     P p265 Number 1815
723     P p266 Number 1852
724     O o266 type_prod p265 p266
725     P p267 Number 1819
726     O o267 type_lid p265 p267
727     T t267 o267 b240
728     B b267 t267
729     P p268 Number 1823
730     P p269 Number 1851
731     O o269 type_prod p268 p269
732     P p270 Number 1829
733     O o270 type_lid p268 p270
734     P p271 String string
735     O o271 type_lid p271
736     T t271 o271
737     B b271 t271
738     T t272 o270 b271
739     B b272 t272
740 xiny 3379 NOcaml!type_apply type_apply type_apply Ocaml
741 xiny 3404 P p272 Number 1832
742     P p273 Number 1842
743     O o273 type_apply p272 p273
744     P p274 Number 1836
745     O o274 type_lid p274 p273
746     P p275 String option
747     O o275 type_lid p275
748     T t275 o275
749 xiny 3379 B b275 t275
750 xiny 3404 T t276 o274 b275
751 xiny 3379 B b276 t276
752 xiny 3404 P p276 Number 1835
753     O o276 type_lid p272 p276
754     T t277 o276 b244
755 xiny 3379 B b277 t277
756 xiny 3404 T t278 o273 b276 b277
757 xiny 3379 B b278 t278
758 xiny 3404 P p278 Number 1845
759     O o278 type_lid p278 p269
760     T t279 o278 b220
761 xiny 3379 B b279 t279
762 xiny 3404 T t280 o b279 b4
763 xiny 3379 B b280 t280
764 xiny 3404 T t281 o b278 b280
765 xiny 3379 B b281 t281
766 xiny 3404 T t282 o b272 b281
767 xiny 3379 B b282 t282
768 xiny 3404 T t283 o269 b282
769 xiny 3379 B b283 t283
770 xiny 3404 T t284 o b283 b4
771 xiny 3379 B b284 t284
772 xiny 3404 T t285 o b267 b284
773 xiny 3379 B b285 t285
774 xiny 3404 T t286 o266 b285
775 xiny 3379 B b286 t286
776 xiny 3404 P p286 Number 1854
777     P p287 Number 1860
778     O o287 type_lid p286 p287
779     T t287 o287 b220
780     B b287 t287
781     T t288 o264 b286 b287
782     B b288 t288
783     P p288 String reduce
784     O o288 resource p288
785     P p289 Number 2920
786     P p290 Number 2931
787     O o290 type_prod p289 p290
788     P p291 Number 2924
789     O o291 type_lid p289 p291
790     T t291 o291 b240
791 xiny 3379 B b291 t291
792 xiny 3404 P p292 Number 2927
793     O o292 type_lid p292 p290
794     P p293 String conv
795     O o293 type_lid p293
796     T t293 o293
797 xiny 3379 B b293 t293
798 xiny 3404 T t294 o292 b293
799 xiny 3379 B b294 t294
800 xiny 3404 T t295 o b294 b4
801 xiny 3379 B b295 t295
802 xiny 3404 T t296 o b291 b295
803 xiny 3379 B b296 t296
804 xiny 3404 T t297 o290 b296
805 xiny 3379 B b297 t297
806 xiny 3404 P p297 Number 2933
807     P p298 Number 2937
808     O o298 type_lid p297 p298
809     T t298 o298 b293
810     B b298 t298
811     T t299 o288 b297 b298
812     B b299 t299
813     P p299 String squash
814     O o299 resource p299
815     P p300 Number 4017
816     P p301 Number 4028
817     O o301 type_lid p300 p301
818     P p302 String squash_info
819     O o302 type_lid p302
820     T t302 o302
821     B b302 t302
822     T t303 o301 b302
823 xiny 3379 B b303 t303
824 xiny 3404 P p303 Number 4030
825     P p304 Number 4043
826     O o304 type_fun p303 p304
827     P p305 Number 4033
828     O o305 type_lid p303 p305
829     T t305 o305 b244
830 xiny 3379 B b305 t305
831 xiny 3404 P p306 Number 4037
832     O o306 type_lid p306 p304
833     T t306 o306 b220
834 xiny 3379 B b306 t306
835 xiny 3404 T t307 o304 b305 b306
836     B b307 t307
837     T t308 o299 b303 b307
838     B b308 t308
839     P p308 String sub
840     O o308 resource p308
841     P p309 Number 4882
842     P p310 Number 4899
843     O o310 type_lid p309 p310
844     P p311 String sub_resource_info
845     O o311 type_lid p311
846     T t311 o311
847 xiny 3379 B b311 t311
848 xiny 3404 T t312 o310 b311
849 xiny 3379 B b312 t312
850 xiny 3404 P p312 Number 4901
851     P p313 Number 4907
852     O o313 type_lid p312 p313
853     T t313 o313 b220
854     B b313 t313
855     T t314 o308 b312 b313
856     B b314 t314
857     P p314 String toploop
858     O o314 resource p314
859     P p315 Number 2445
860     P p316 Number 2467
861     O o316 type_prod p315 p316
862     P p317 Number 2451
863     O o317 type_lid p315 p317
864     T t317 o317 b271
865 xiny 3379 B b317 t317
866 xiny 3404 P p318 Number 2454
867     P p319 Number 2460
868     O o319 type_lid p318 p319
869     T t319 o319 b271
870 xiny 3379 B b319 t319
871 xiny 3404 P p320 Number 2463
872     O o320 type_lid p320 p316
873     P p321 String expr
874     O o321 type_lid p321
875     T t321 o321
876 xiny 3379 B b321 t321
877 xiny 3404 T t322 o320 b321
878 xiny 3379 B b322 t322
879 xiny 3404 T t323 o b322 b4
880 xiny 3379 B b323 t323
881 xiny 3404 T t324 o b319 b323
882 xiny 3379 B b324 t324
883 xiny 3404 T t325 o b317 b324
884     B b325 t325
885     T t326 o316 b325
886 xiny 3379 B b326 t326
887 xiny 3404 P p326 Number 2469
888     P p327 Number 2478
889     O o327 type_lid p326 p327
890     P p328 String top_table
891     O o328 type_lid p328
892     T t328 o328
893 xiny 3379 B b328 t328
894 xiny 3404 T t329 o327 b328
895     B b329 t329
896     T t330 o314 b326 b329
897     B b330 t330
898     P p330 String typeinf
899     O o330 resource p330
900     P p331 Number 2151
901     P p332 Number 2172
902     O o332 type_lid p331 p332
903     P p333 String typeinf_resource_info
904     O o333 type_lid p333
905     T t333 o333
906     B b333 t333
907     T t334 o332 b333
908 xiny 3379 B b334 t334
909 xiny 3404 P p334 Number 2174
910     P p335 Number 2186
911     O o335 type_lid p334 p335
912     P p336 String typeinf_func
913     O o336 type_lid p336
914     T t336 o336
915 xiny 3379 B b336 t336
916 xiny 3404 T t337 o335 b336
917     B b337 t337
918     T t338 o330 b334 b337
919     B b338 t338
920     P p338 String typeinf_subst
921     O o338 resource p338
922     P p339 Number 1825
923     P p340 Number 1843
924     O o340 type_lid p339 p340
925     P p341 String typeinf_subst_info
926 xiny 3379 O o341 type_lid p341
927     T t341 o341
928     B b341 t341
929     T t342 o340 b341
930     B b342 t342
931 xiny 3404 P p342 Number 1862
932     O o342 type_lid p278 p342
933     P p343 String typeinf_subst_fun
934     O o343 type_lid p343
935     T t343 o343
936 xiny 3379 B b343 t343
937 xiny 3404 T t344 o342 b343
938 xiny 3379 B b344 t344
939 xiny 3404 T t345 o338 b342 b344
940 xiny 3379 B b345 t345
941 xiny 3404 T t346 o b345 b4
942 xiny 3379 B b346 t346
943 xiny 3404 T t347 o b338 b346
944 xiny 3379 B b347 t347
945 xiny 3404 T t348 o b330 b347
946 xiny 3379 B b348 t348
947 xiny 3404 T t349 o b314 b348
948 xiny 3379 B b349 t349
949 xiny 3404 T t350 o b308 b349
950 xiny 3379 B b350 t350
951 xiny 3404 T t351 o b299 b350
952 xiny 3379 B b351 t351
953 xiny 3404 T t352 o b288 b351
954 xiny 3379 B b352 t352
955 xiny 3404 T t353 o b264 b352
956 xiny 3379 B b353 t353
957 xiny 3404 T t354 o b255 b353
958 xiny 3379 B b354 t354
959 xiny 3404 T t355 o b236 b354
960 xiny 3379 B b355 t355
961 xiny 3404 T t356 o b228 b355
962 xiny 3379 B b356 t356
963 xiny 3404 T t357 o2 b5 b213 b356
964     B b357 t357
965     T t358 o1 b357
966 xiny 3379 B b358 t358
967 xiny 3404 P p358 Number 20
968     P p359 Number 42
969     O o359 location p358 p359
970     P p360 String Czf_itt_member
971     O o360 parent p360
972     T t360 o360
973 xiny 3379 B b360 t360
974     T t361 o b360 b4
975     B b361 t361
976 xiny 3404 P p361 String Czf_itt_eq
977     O o361 parent p361
978     T t362 o361
979 xiny 3379 B b362 t362
980 xiny 3404 T t363 o b362 b4
981 xiny 3379 B b363 t363
982 xiny 3404 T t364 o b363 b4
983 xiny 3379 B b364 t364
984 xiny 3404 T t365 o b361 b364
985 xiny 3379 B b365 t365
986 xiny 3404 T t366 o2 b361 b365 b356
987 xiny 3379 B b366 t366
988 xiny 3404 T t367 o359 b366
989 xiny 3379 B b367 t367
990 xiny 3404 P p367 Number 43
991     P p368 Number 61
992 xiny 3379 O o368 location p367 p368
993 xiny 3404 T t368 o2 b363 b4 b356
994     B b368 t368
995     T t369 o368 b368
996 xiny 3379 B b369 t369
997 xiny 3404 P p369 Number 62
998     P p370 Number 82
999     O o370 location p369 p370
1000     P p371 String Czf_itt_dall
1001     O o371 parent p371
1002     T t371 o371
1003 xiny 3379 B b371 t371
1004     T t372 o b371 b4
1005     B b372 t372
1006 xiny 3404 P p372 String Czf_itt_set_ind
1007 xiny 3379 O o372 parent p372
1008     T t373 o372
1009     B b373 t373
1010     T t374 o b373 b4
1011     B b374 t374
1012 xiny 3404 P p374 String Czf_itt_all
1013 xiny 3379 O o374 parent p374
1014     T t375 o374
1015     B b375 t375
1016     T t376 o b375 b4
1017     B b376 t376
1018 xiny 3404 P p376 String Czf_itt_sep
1019     O o376 parent p376
1020     T t377 o376
1021 xiny 3379 B b377 t377
1022 xiny 3404 T t378 o b377 b4
1023 xiny 3379 B b378 t378
1024 xiny 3404 T t379 o b378 b4
1025 xiny 3379 B b379 t379
1026 xiny 3404 T t380 o b376 b379
1027 xiny 3379 B b380 t380
1028 xiny 3404 T t381 o b374 b380
1029 xiny 3379 B b381 t381
1030 xiny 3404 T t382 o b372 b381
1031 xiny 3379 B b382 t382
1032 xiny 3404 T t383 o2 b372 b382 b356
1033     B b383 t383
1034     T t384 o370 b383
1035 xiny 3379 B b384 t384
1036 xiny 3404 P p384 Number 83
1037     P p385 Number 102
1038     O o385 location p384 p385
1039     P p386 String Czf_itt_and
1040     O o386 parent p386
1041     T t386 o386
1042 xiny 3379 B b386 t386
1043 xiny 3404 T t387 o b386 b4
1044 xiny 3379 B b387 t387
1045 xiny 3404 T t388 o b387 b4
1046 xiny 3379 B b388 t388
1047 xiny 3404 T t389 o2 b387 b388 b356
1048     B b389 t389
1049     T t390 o385 b389
1050     B b390 t390
1051     P p390 Number 104
1052     P p391 Number 115
1053     O o391 location p390 p391
1054 xiny 3379 NSummary!summary_item summary_item summary_item Summary
1055 xiny 3404 O o392 summary_item
1056 xiny 3379 NOcaml!str_open str_open str_open Ocaml
1057 xiny 3404 O o393 str_open p390 p391
1058 xiny 3379 NOcaml!string string string Ocaml
1059 xiny 3404 P p393 String Printf
1060     O o394 string p393
1061     T t394 o394
1062 xiny 3379 B b394 t394
1063 xiny 3404 T t395 o b394 b4
1064 xiny 3379 B b395 t395
1065 xiny 3404 T t396 o393 b395
1066 xiny 3379 B b396 t396
1067 xiny 3404 T t397 o392 b396
1068     B b397 t397
1069     T t398 o391 b397
1070     B b398 t398
1071     P p398 Number 116
1072     P p399 Number 129
1073     O o399 location p398 p399
1074     O o400 str_open p398 p399
1075     P p400 String Mp_debug
1076     O o401 string p400
1077     T t401 o401
1078 xiny 3379 B b401 t401
1079 xiny 3404 T t402 o b401 b4
1080 xiny 3379 B b402 t402
1081 xiny 3404 T t403 o400 b402
1082 xiny 3379 B b403 t403
1083 xiny 3404 T t404 o392 b403
1084     B b404 t404
1085     T t405 o399 b404
1086     B b405 t405
1087     P p405 Number 130
1088     P p406 Number 159
1089     O o406 location p405 p406
1090     O o407 str_open p405 p406
1091     P p407 String Refiner
1092     O o408 string p407
1093     T t408 o408
1094 xiny 3379 B b408 t408
1095 xiny 3404 P p408 String TermType
1096     O o409 string p408
1097     T t409 o409
1098 xiny 3379 B b409 t409
1099 xiny 3404 T t410 o b409 b4
1100 xiny 3379 B b410 t410
1101 xiny 3404 T t411 o b408 b410
1102 xiny 3379 B b411 t411
1103 xiny 3404 T t412 o b408 b411
1104 xiny 3379 B b412 t412
1105 xiny 3404 T t413 o407 b412
1106 xiny 3379 B b413 t413
1107 xiny 3404 T t414 o392 b413
1108     B b414 t414
1109     T t415 o406 b414
1110     B b415 t415
1111     P p415 Number 160
1112     P p416 Number 185
1113     O o416 location p415 p416
1114     O o417 str_open p415 p416
1115     P p417 String Term
1116     O o418 string p417
1117     T t418 o418
1118 xiny 3379 B b418 t418
1119 xiny 3404 T t419 o b418 b4
1120 xiny 3379 B b419 t419
1121 xiny 3404 T t420 o b408 b419
1122 xiny 3379 B b420 t420
1123 xiny 3404 T t421 o b408 b420
1124 xiny 3379 B b421 t421
1125 xiny 3404 T t422 o417 b421
1126 xiny 3379 B b422 t422
1127 xiny 3404 T t423 o392 b422
1128     B b423 t423
1129     T t424 o416 b423
1130     B b424 t424
1131     P p424 Number 186
1132     P p425 Number 213
1133     O o425 location p424 p425
1134     O o426 str_open p424 p425
1135     P p426 String TermOp
1136     O o427 string p426
1137     T t427 o427
1138 xiny 3379 B b427 t427
1139 xiny 3404 T t428 o b427 b4
1140 xiny 3379 B b428 t428
1141 xiny 3404 T t429 o b408 b428
1142 xiny 3379 B b429 t429
1143 xiny 3404 T t430 o b408 b429
1144 xiny 3379 B b430 t430
1145 xiny 3404 T t431 o426 b430
1146 xiny 3379 B b431 t431
1147 xiny 3404 T t432 o392 b431
1148     B b432 t432
1149     T t433 o425 b432
1150     B b433 t433
1151     P p433 Number 214
1152     P p434 Number 243
1153     O o434 location p433 p434
1154     O o435 str_open p433 p434
1155     P p435 String TermAddr
1156     O o436 string p435
1157     T t436 o436
1158 xiny 3379 B b436 t436
1159 xiny 3404 T t437 o b436 b4
1160 xiny 3379 B b437 t437
1161 xiny 3404 T t438 o b408 b437
1162 xiny 3379 B b438 t438
1163 xiny 3404 T t439 o b408 b438
1164 xiny 3379 B b439 t439
1165 xiny 3404 T t440 o435 b439
1166 xiny 3379 B b440 t440
1167 xiny 3404 T t441 o392 b440
1168     B b441 t441
1169     T t442 o434 b441
1170     B b442 t442
1171     P p442 Number 244
1172     P p443 Number 272
1173     O o443 location p442 p443
1174     O o444 str_open p442 p443
1175     P p444 String TermMan
1176     O o445 string p444
1177     T t445 o445
1178 xiny 3379 B b445 t445
1179 xiny 3404 T t446 o b445 b4
1180 xiny 3379 B b446 t446
1181 xiny 3404 T t447 o b408 b446
1182 xiny 3379 B b447 t447
1183 xiny 3404 T t448 o b408 b447
1184 xiny 3379 B b448 t448
1185 xiny 3404 T t449 o444 b448
1186 xiny 3379 B b449 t449
1187 xiny 3404 T t450 o392 b449
1188     B b450 t450
1189     T t451 o443 b450
1190     B b451 t451
1191     P p451 Number 273
1192     P p452 Number 303
1193     O o452 location p451 p452
1194     O o453 str_open p451 p452
1195     P p453 String TermSubst
1196     O o454 string p453
1197     T t454 o454
1198 xiny 3379 B b454 t454
1199 xiny 3404 T t455 o b454 b4
1200 xiny 3379 B b455 t455
1201 xiny 3404 T t456 o b408 b455
1202 xiny 3379 B b456 t456
1203 xiny 3404 T t457 o b408 b456
1204 xiny 3379 B b457 t457
1205 xiny 3404 T t458 o453 b457
1206 xiny 3379 B b458 t458
1207 xiny 3404 T t459 o392 b458
1208     B b459 t459
1209     T t460 o452 b459
1210     B b460 t460
1211     P p460 Number 304
1212     P p461 Number 331
1213     O o461 location p460 p461
1214     O o462 str_open p460 p461
1215     P p462 String Refine
1216     O o463 string p462
1217     T t463 o463
1218 xiny 3379 B b463 t463
1219 xiny 3404 T t464 o b463 b4
1220 xiny 3379 B b464 t464
1221 xiny 3404 T t465 o b408 b464
1222 xiny 3379 B b465 t465
1223 xiny 3404 T t466 o b408 b465
1224 xiny 3379 B b466 t466
1225 xiny 3404 T t467 o462 b466
1226 xiny 3379 B b467 t467
1227 xiny 3404 T t468 o392 b467
1228     B b468 t468
1229     T t469 o461 b468
1230     B b469 t469
1231     P p469 Number 332
1232     P p470 Number 364
1233     O o470 location p469 p470
1234     O o471 str_open p469 p470
1235     P p471 String RefineError
1236     O o472 string p471
1237     T t472 o472
1238 xiny 3379 B b472 t472
1239 xiny 3404 T t473 o b472 b4
1240 xiny 3379 B b473 t473
1241 xiny 3404 T t474 o b408 b473
1242 xiny 3379 B b474 t474
1243 xiny 3404 T t475 o b408 b474
1244 xiny 3379 B b475 t475
1245 xiny 3404 T t476 o471 b475
1246 xiny 3379 B b476 t476
1247 xiny 3404 T t477 o392 b476
1248     B b477 t477
1249     T t478 o470 b477
1250     B b478 t478
1251     P p478 Number 365
1252     P p479 Number 381
1253     O o479 location p478 p479
1254     O o480 str_open p478 p479
1255     P p480 String Mp_resource
1256     O o481 string p480
1257     T t481 o481
1258 xiny 3379 B b481 t481
1259 xiny 3404 T t482 o b481 b4
1260 xiny 3379 B b482 t482
1261 xiny 3404 T t483 o480 b482
1262 xiny 3379 B b483 t483
1263 xiny 3404 T t484 o392 b483
1264     B b484 t484
1265     T t485 o479 b484
1266     B b485 t485
1267     P p485 Number 382
1268     P p486 Number 399
1269     O o486 location p485 p486
1270     O o487 str_open p485 p486
1271     P p487 String Simple_print
1272     O o488 string p487
1273     T t488 o488
1274 xiny 3379 B b488 t488
1275 xiny 3404 T t489 o b488 b4
1276 xiny 3379 B b489 t489
1277 xiny 3404 T t490 o487 b489
1278 xiny 3379 B b490 t490
1279 xiny 3404 T t491 o392 b490
1280     B b491 t491
1281     T t492 o486 b491
1282     B b492 t492
1283     P p492 Number 401
1284     P p493 Number 417
1285     O o493 location p492 p493
1286     O o494 str_open p492 p493
1287     P p494 String Tactic_type
1288     O o495 string p494
1289     T t495 o495
1290 xiny 3379 B b495 t495
1291 xiny 3404 T t496 o b495 b4
1292 xiny 3379 B b496 t496
1293 xiny 3404 T t497 o494 b496
1294 xiny 3379 B b497 t497
1295 xiny 3404 T t498 o392 b497
1296     B b498 t498
1297     T t499 o493 b498
1298     B b499 t499
1299     P p499 Number 418
1300     P p500 Number 444
1301     O o500 location p499 p500
1302     O o501 str_open p499 p500
1303     P p501 String Tacticals
1304     O o502 string p501
1305     T t502 o502
1306 xiny 3379 B b502 t502
1307 xiny 3404 T t503 o b502 b4
1308 xiny 3379 B b503 t503
1309 xiny 3404 T t504 o b495 b503
1310 xiny 3379 B b504 t504
1311 xiny 3404 T t505 o501 b504
1312 xiny 3379 B b505 t505
1313 xiny 3404 T t506 o392 b505
1314     B b506 t506
1315     T t507 o500 b506
1316     B b507 t507
1317     P p507 Number 445
1318     P p508 Number 469
1319     O o508 location p507 p508
1320     O o509 str_open p507 p508
1321     P p509 String Sequent
1322     O o510 string p509
1323     T t510 o510
1324 xiny 3379 B b510 t510
1325 xiny 3404 T t511 o b510 b4
1326 xiny 3379 B b511 t511
1327 xiny 3404 T t512 o b495 b511
1328 xiny 3379 B b512 t512
1329 xiny 3404 T t513 o509 b512
1330 xiny 3379 B b513 t513
1331 xiny 3404 T t514 o392 b513
1332     B b514 t514
1333     T t515 o508 b514
1334     B b515 t515
1335     P p515 Number 470
1336     P p516 Number 500
1337     O o516 location p515 p516
1338     O o517 str_open p515 p516
1339     P p517 String Conversionals
1340     O o518 string p517
1341     T t518 o518
1342 xiny 3379 B b518 t518
1343 xiny 3404 T t519 o b518 b4
1344 xiny 3379 B b519 t519
1345 xiny 3404 T t520 o b495 b519
1346 xiny 3379 B b520 t520
1347 xiny 3404 T t521 o517 b520
1348 xiny 3379 B b521 t521
1349 xiny 3404 T t522 o392 b521
1350     B b522 t522
1351     T t523 o516 b522
1352     B b523 t523
1353     P p523 Number 501
1354     P p524 Number 511
1355     O o524 location p523 p524
1356     O o525 str_open p523 p524
1357     O o526 string p131
1358     T t526 o526
1359 xiny 3379 B b526 t526
1360 xiny 3404 T t527 o b526 b4
1361 xiny 3379 B b527 t527
1362 xiny 3404 T t528 o525 b527
1363 xiny 3379 B b528 t528
1364 xiny 3404 T t529 o392 b528
1365     B b529 t529
1366     T t530 o524 b529
1367     B b530 t530
1368     P p530 Number 512
1369     P p531 Number 520
1370     O o531 location p530 p531
1371     O o532 str_open p530 p531
1372     O o533 string p129
1373     T t533 o533
1374 xiny 3379 B b533 t533
1375 xiny 3404 T t534 o b533 b4
1376 xiny 3379 B b534 t534
1377 xiny 3404 T t535 o532 b534
1378 xiny 3379 B b535 t535
1379 xiny 3404 T t536 o392 b535
1380     B b536 t536
1381     T t537 o531 b536
1382     B b537 t537
1383     P p537 Number 522
1384     P p538 Number 539
1385     O o538 location p537 p538
1386     O o539 str_open p537 p538
1387     O o540 string p119
1388     T t540 o540
1389 xiny 3379 B b540 t540
1390 xiny 3404 T t541 o b540 b4
1391 xiny 3379 B b541 t541
1392 xiny 3404 T t542 o539 b541
1393 xiny 3379 B b542 t542
1394 xiny 3404 T t543 o392 b542
1395     B b543 t543
1396     T t544 o538 b543
1397     B b544 t544
1398     P p544 Number 540
1399     P p545 Number 561
1400     O o545 location p544 p545
1401     O o546 str_open p544 p545
1402     O o547 string p121
1403     T t547 o547
1404 xiny 3379 B b547 t547
1405 xiny 3404 T t548 o b547 b4
1406 xiny 3379 B b548 t548
1407 xiny 3404 T t549 o546 b548
1408 xiny 3379 B b549 t549
1409 xiny 3404 T t550 o392 b549
1410     B b550 t550
1411     T t551 o545 b550
1412     B b551 t551
1413     P p551 Number 563
1414     P p552 Number 574
1415     O o552 location p551 p552
1416 xiny 3379 NSummary!opname opname opname Summary
1417 xiny 3404 P p553 String car
1418     O o553 opname p553
1419 xiny 3379 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1420     NCzf_itt_group!car car car Czf_itt_group
1421 xiny 3404 O o554 car
1422     T t554 o554
1423 xiny 3379 B b554 t554
1424 xiny 3404 T t555 o553 b554
1425     B b555 t555
1426     T t556 o552 b555
1427     B b556 t556
1428     P p556 Number 615
1429     P p557 Number 635
1430     O o557 location p556 p557
1431     P p558 String op
1432     O o558 opname p558
1433 xiny 3379 NCzf_itt_group!op op op Czf_itt_group
1434 xiny 3404 O o559 op
1435 xiny 3379 Nvar var var NIL
1436 xiny 3404 P p559 Var s1
1437     O o560 var p559
1438     T t560 o560
1439 xiny 3379 B b560 t560
1440 xiny 3404 P p560 Var s2
1441     O o561 var p560
1442     T t561 o561
1443 xiny 3379 B b561 t561
1444 xiny 3404 T t562 o559 b560 b561
1445 xiny 3379 B b562 t562
1446 xiny 3404 T t563 o558 b562
1447     B b563 t563
1448     T t564 o557 b563
1449     B b564 t564
1450     P p564 Number 636
1451     P p565 Number 646
1452     O o565 location p564 p565
1453     P p566 String id
1454     O o566 opname p566
1455 xiny 3379 NCzf_itt_group!id id id Czf_itt_group
1456 xiny 3404 O o567 id
1457     T t567 o567
1458 xiny 3379 B b567 t567
1459 xiny 3404 T t568 o566 b567
1460     B b568 t568
1461     T t569 o565 b568
1462     B b569 t569
1463     P p569 Number 647
1464     P p570 Number 662
1465     O o570 location p569 p570
1466     P p571 String inv
1467     O o571 opname p571
1468 xiny 3379 NCzf_itt_group!inv inv inv Czf_itt_group
1469 xiny 3404 O o572 inv
1470     P p572 Var s
1471     O o573 var p572
1472     T t573 o573
1473 xiny 3379 B b573 t573
1474 xiny 3404 T t574 o572 b573
1475 xiny 3379 B b574 t574
1476 xiny 3404 T t575 o571 b574
1477     B b575 t575
1478     T t576 o570 b575
1479     B b576 t576
1480     P p576 Number 664
1481     P p577 Number 713
1482     O o577 location p576 p577
1483 xiny 3379 NSummary!dform dform dform Summary
1484 xiny 3404 P p578 String car_df
1485     O o578 dform p578
1486 xiny 3379 NSummary!except_mode_df except_mode_df except_mode_df Summary
1487 xiny 3404 P p579 String src
1488     O o579 except_mode_df p579
1489 xiny 3379 T t579 o579
1490     B b579 t579
1491     T t580 o b579 b4
1492     B b580 t580
1493 xiny 3404 NSummary!df_term df_term df_term Summary
1494     O o580 df_term
1495     NPerv!string string580 string Perv
1496     P p580 String G
1497     O o581 string580 p580
1498     T t581 o581
1499 xiny 3379 B b581 t581
1500 xiny 3404 T t582 o b581 b4
1501 xiny 3379 B b582 t582
1502 xiny 3404 T t583 o580 b582
1503 xiny 3379 B b583 t583
1504 xiny 3404 T t584 o578 b580 b554 b583
1505     B b584 t584
1506     T t585 o577 b584
1507     B b585 t585
1508     P p585 Number 715
1509     P p586 Number 762
1510     O o586 location p585 p586
1511     P p587 String id_df
1512     O o587 dform p587
1513     P p588 String e
1514     O o588 string580 p588
1515     T t588 o588
1516 xiny 3379 B b588 t588
1517 xiny 3404 T t589 o b588 b4
1518 xiny 3379 B b589 t589
1519 xiny 3404 T t590 o580 b589
1520 xiny 3379 B b590 t590
1521 xiny 3404 T t591 o587 b580 b567 b590
1522     B b591 t591
1523     T t592 o586 b591
1524     B b592 t592
1525     P p592 Number 765
1526     P p593 Number 866
1527     O o593 location p592 p593
1528     P p594 String op_df
1529     O o594 dform p594
1530 xiny 3379 NSummary!parens_df parens_df parens_df Summary
1531 xiny 3404 O o595 parens_df
1532     T t595 o595
1533 xiny 3379 B b595 t595
1534 xiny 3404 T t596 o b595 b4
1535 xiny 3379 B b596 t596
1536 xiny 3404 T t597 o b579 b596
1537 xiny 3379 B b597 t597
1538 xiny 3404 Nslot slot slot NIL
1539     P p597 String le
1540     O o597 slot p597
1541     T t598 o597 b560
1542 xiny 3379 B b598 t598
1543 xiny 3404 P p598 String " * "
1544     O o598 string580 p598
1545     T t599 o598
1546 xiny 3379 B b599 t599
1547 xiny 3404 T t600 o597 b561
1548 xiny 3379 B b600 t600
1549 xiny 3404 T t601 o b600 b4
1550 xiny 3379 B b601 t601
1551 xiny 3404 T t602 o b599 b601
1552 xiny 3379 B b602 t602
1553 xiny 3404 T t603 o b598 b602
1554 xiny 3379 B b603 t603
1555 xiny 3404 T t604 o580 b603
1556 xiny 3379 B b604 t604
1557 xiny 3404 T t605 o594 b597 b562 b604
1558     B b605 t605
1559     T t606 o593 b605
1560 xiny 3379 B b606 t606
1561 xiny 3404 P p606 Number 868
1562     P p607 Number 946
1563     O o607 location p606 p607
1564     P p608 String inv_df
1565     O o608 dform p608
1566     T t608 o597 b573
1567 xiny 3379 B b608 t608
1568 xiny 3404 P p609 String '
1569     O o609 string580 p609
1570     T t609 o609
1571 xiny 3379 B b609 t609
1572 xiny 3404 T t610 o b609 b4
1573 xiny 3379 B b610 t610
1574 xiny 3404 T t611 o b608 b610
1575 xiny 3379 B b611 t611
1576 xiny 3404 T t612 o580 b611
1577 xiny 3379 B b612 t612
1578 xiny 3404 T t613 o608 b597 b574 b612
1579     B b613 t613
1580     T t614 o607 b613
1581     B b614 t614
1582     P p614 Number 961
1583     P p615 Number 1037
1584     O o615 location p614 p615
1585 xiny 3379 NSummary!rule rule rule Summary
1586 xiny 3404 P p616 String car_wf
1587     O o616 rule p616
1588 xiny 3379 NSummary!context_param context_param context_param Summary
1589 xiny 3404 P p617 String H
1590     O o617 context_param p617
1591 xiny 3379 T t617 o617
1592     B b617 t617
1593     T t618 o b617 b4
1594 xiny 3404 B b618 t618
1595     NSummary!meta_theorem meta_theorem meta_theorem Summary
1596     O o618 meta_theorem
1597     P p618 Var ext
1598     O o619 var p618
1599     T t619 o619
1600     B b619 t619
1601     T t620 o b619 b4
1602 xiny 3379 C h H
1603     NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1604     NCzf_itt_set!isset isset isset Czf_itt_set
1605 xiny 3404 O o620 isset
1606     T t621 o620 b554
1607     S s t620 h
1608     G s t621
1609     B b621 s
1610     T t622 o618 b621
1611     B b622 t622
1612 xiny 3379 NSummary!incomplete incomplete incomplete Summary
1613 xiny 3404 O o622 incomplete
1614     T t623 o622
1615     B b623 t623
1616 xiny 3379 NSummary!resource_defs resource_defs resource_defs Summary
1617 xiny 3404 P p623 Number 983
1618     P p624 Number 990
1619     O o624 resource_defs p623 p624 p264
1620 xiny 3379 NOcaml!uid uid uid Ocaml
1621 xiny 3404 P p625 Number 988
1622     O o625 uid p625 p624
1623     P p626 String []
1624     O o626 uid p626
1625     T t626 o626
1626 xiny 3379 B b626 t626
1627 xiny 3404 T t627 o625 b626
1628 xiny 3379 B b627 t627
1629     T t628 o b627 b4
1630     B b628 t628
1631 xiny 3404 T t629 o624 b628
1632 xiny 3379 B b629 t629
1633 xiny 3404 T t630 o b629 b4
1634 xiny 3379 B b630 t630
1635 xiny 3404 T t631 o616 b618 b622 b623 b630
1636     B b631 t631
1637     T t632 o615 b631
1638     B b632 t632
1639     P p632 Number 1039
1640     P p633 Number 1214
1641     O o633 location p632 p633
1642     P p634 String op_wf1
1643     O o634 rule p634
1644 xiny 3379 NSummary!meta_implies meta_implies meta_implies Summary
1645 xiny 3404 O o635 meta_implies
1646 xiny 3379 NBase_trivial Base_trivial Base_trivial NIL
1647     NBase_trivial!squash squash squash Base_trivial
1648 xiny 3404 O o636 squash
1649     T t636 o636
1650     B b636 t636
1651     T t637 o b636 b4
1652     T t638 o620 b560
1653     S s638 t637 h
1654 xiny 3379 G s638 t638
1655     B b638 s638
1656 xiny 3404 T t639 o618 b638
1657 xiny 3379 B b639 t639
1658 xiny 3404 T t640 o620 b561
1659     S s640 t637 h
1660 xiny 3379 G s640 t640
1661     B b640 s640
1662 xiny 3404 T t641 o618 b640
1663 xiny 3379 B b641 t641
1664 xiny 3404 T t642 o620 b562
1665     S s642 t620 h
1666     G s642 t642
1667     B b642 s642
1668     T t643 o618 b642
1669 xiny 3379 B b643 t643
1670 xiny 3404 T t644 o635 b641 b643
1671     B b644 t644
1672     T t645 o635 b639 b644
1673 xiny 3379 B b645 t645
1674 xiny 3404 P p645 Number 1061
1675     P p646 Number 1068
1676     O o646 resource_defs p645 p646 p264
1677     P p647 Number 1066
1678     O o647 uid p647 p646
1679     T t647 o647 b626
1680 xiny 3379 B b647 t647
1681     T t648 o b647 b4
1682     B b648 t648
1683 xiny 3404 T t649 o646 b648
1684 xiny 3379 B b649 t649
1685 xiny 3404 T t650 o b649 b4
1686 xiny 3379 B b650 t650
1687 xiny 3404 T t651 o634 b618 b645 b623 b650
1688     B b651 t651
1689     T t652 o633 b651
1690     B b652 t652
1691     P p652 Number 1216
1692     P p653 Number 1486
1693     O o653 location p652 p653
1694     P p654 String op_wf2
1695     O o654 rule p654
1696 xiny 3379 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1697     NCzf_itt_member!mem mem mem Czf_itt_member
1698 xiny 3404 O o655 mem
1699     T t655 o655 b560 b554
1700     S s655 t620 h
1701 xiny 3379 G s655 t655
1702     B b655 s655
1703 xiny 3404 T t656 o618 b655
1704 xiny 3379 B b656 t656
1705 xiny 3404 T t657 o655 b561 b554
1706     S s657 t620 h
1707 xiny 3379 G s657 t657
1708     B b657 s657
1709 xiny 3404 T t658 o618 b657
1710 xiny 3379 B b658 t658
1711 xiny 3404 T t659 o655 b562 b554
1712     S s659 t620 h
1713     G s659 t659
1714     B b659 s659
1715     T t660 o618 b659
1716 xiny 3379 B b660 t660
1717 xiny 3404 T t661 o635 b658 b660
1718 xiny 3379 B b661 t661
1719 xiny 3404 T t662 o635 b656 b661
1720 xiny 3379 B b662 t662
1721 xiny 3404 T t663 o635 b641 b662
1722     B b663 t663
1723     T t664 o635 b639 b663
1724 xiny 3379 B b664 t664
1725 xiny 3404 P p664 Number 1238
1726     P p665 Number 1245
1727     O o665 resource_defs p664 p665 p264
1728     P p666 Number 1243
1729     O o666 uid p666 p665
1730     T t666 o666 b626
1731 xiny 3379 B b666 t666
1732     T t667 o b666 b4
1733     B b667 t667
1734 xiny 3404 T t668 o665 b667
1735 xiny 3379 B b668 t668
1736 xiny 3404 T t669 o b668 b4
1737 xiny 3379 B b669 t669
1738 xiny 3404 T t670 o654 b618 b664 b623 b669
1739     B b670 t670
1740     T t671 o653 b670
1741     B b671 t671
1742     P p671 Number 1488
1743     P p672 Number 1766
1744     O o672 location p671 p672
1745     P p673 String op_eq1
1746     O o673 rule p673
1747     P p674 Var s3
1748     O o674 var p674
1749     T t674 o674
1750 xiny 3379 B b674 t674
1751 xiny 3404 T t675 o620 b674
1752     S s675 t637 h
1753 xiny 3379 G s675 t675
1754     B b675 s675
1755 xiny 3404 T t676 o618 b675
1756 xiny 3379 B b676 t676
1757 xiny 3404 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1758     NCzf_itt_eq!eq eq eq Czf_itt_eq
1759     O o676 eq
1760     T t677 o676 b560 b561
1761     S s677 t620 h
1762     G s677 t677
1763     B b677 s677
1764     T t678 o618 b677
1765 xiny 3379 B b678 t678
1766 xiny 3404 T t679 o559 b674 b560
1767     B b679 t679
1768     T t680 o559 b674 b561
1769 xiny 3379 B b680 t680
1770 xiny 3404 T t681 o676 b679 b680
1771     S s681 t620 h
1772     G s681 t681
1773     B b681 s681
1774     T t682 o618 b681
1775 xiny 3379 B b682 t682
1776 xiny 3404 T t683 o635 b678 b682
1777 xiny 3379 B b683 t683
1778 xiny 3404 T t684 o635 b676 b683
1779 xiny 3379 B b684 t684
1780 xiny 3404 T t685 o635 b641 b684
1781     B b685 t685
1782     T t686 o635 b639 b685
1783 xiny 3379 B b686 t686
1784 xiny 3404 P p686 Number 1510
1785     P p687 Number 1517
1786     O o687 resource_defs p686 p687 p264
1787     P p688 Number 1515
1788     O o688 uid p688 p687
1789     T t688 o688 b626
1790 xiny 3379 B b688 t688
1791     T t689 o b688 b4
1792     B b689 t689
1793 xiny 3404 T t690 o687 b689
1794 xiny 3379 B b690 t690
1795 xiny 3404 T t691 o b690 b4
1796 xiny 3379 B b691 t691
1797 xiny 3404 T t692 o673 b618 b686 b623 b691
1798     B b692 t692
1799     T t693 o672 b692
1800 xiny 3379 B b693 t693
1801 xiny 3404 P p693 Number 1768
1802     P p694 Number 2046
1803     O o694 location p693 p694
1804     P p695 String op_eq2
1805     O o695 rule p695
1806     T t695 o559 b560 b674
1807     B b695 t695
1808     T t696 o559 b561 b674
1809 xiny 3379 B b696 t696
1810 xiny 3404 T t697 o676 b695 b696
1811     S s697 t620 h
1812     G s697 t697
1813     B b697 s697
1814     T t698 o618 b697
1815 xiny 3379 B b698 t698
1816 xiny 3404 T t699 o635 b678 b698
1817 xiny 3379 B b699 t699
1818 xiny 3404 T t700 o635 b676 b699
1819 xiny 3379 B b700 t700
1820 xiny 3404 T t701 o635 b641 b700
1821     B b701 t701
1822     T t702 o635 b639 b701
1823 xiny 3379 B b702 t702
1824 xiny 3404 P p702 Number 1790
1825     P p703 Number 1797
1826     O o703 resource_defs p702 p703 p264
1827     P p704 Number 1795
1828     O o704 uid p704 p703
1829     T t704 o704 b626
1830 xiny 3379 B b704 t704
1831     T t705 o b704 b4
1832     B b705 t705
1833 xiny 3404 T t706 o703 b705
1834 xiny 3379 B b706 t706
1835 xiny 3404 T t707 o b706 b4
1836 xiny 3379 B b707 t707
1837 xiny 3404 T t708 o695 b618 b702 b623 b707
1838     B b708 t708
1839     T t709 o694 b708
1840     B b709 t709
1841     P p709 Number 2048
1842     P p710 Number 2181
1843     O o710 location p709 p710
1844     P p711 String op_fun1
1845     O o711 rule p711
1846     T t711 o620 b573
1847     S s711 t637 h
1848     G s711 t711
1849     B b711 s711
1850     T t712 o618 b711
1851     B b712 t712
1852 xiny 3379 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1853 xiny 3404 O o712 fun_set
1854     P p712 Var z
1855     O o713 var p712
1856     T t713 o713
1857     B b713 t713
1858     T t714 o559 b713 b573
1859     B b714 t714 z
1860     T t715 o712 b714
1861     S s715 t620 h
1862     G s715 t715
1863     B b715 s715
1864     T t716 o618 b715
1865     B b716 t716
1866     T t717 o635 b712 b716
1867 xiny 3379 B b717 t717
1868 xiny 3404 P p717 Number 2071
1869     P p718 Number 2078
1870     O o718 resource_defs p717 p718 p264
1871     P p719 Number 2076
1872     O o719 uid p719 p718
1873     T t719 o719 b626
1874 xiny 3379 B b719 t719
1875     T t720 o b719 b4
1876     B b720 t720
1877 xiny 3404 T t721 o718 b720
1878 xiny 3379 B b721 t721
1879 xiny 3404 T t722 o b721 b4
1880 xiny 3379 B b722 t722
1881 xiny 3404 T t723 o711 b618 b717 b623 b722
1882     B b723 t723
1883     T t724 o710 b723
1884     B b724 t724
1885     P p724 Number 2183
1886     P p725 Number 2316
1887     O o725 location p724 p725
1888     P p726 String op_fun2
1889     O o726 rule p726
1890     T t726 o559 b573 b713
1891     B b726 t726 z
1892     T t727 o712 b726
1893     S s727 t620 h
1894     G s727 t727
1895     B b727 s727
1896     T t728 o618 b727
1897     B b728 t728
1898     T t729 o635 b712 b728
1899 xiny 3379 B b729 t729
1900 xiny 3404 P p729 Number 2206
1901     P p730 Number 2213
1902     O o730 resource_defs p729 p730 p264
1903     P p731 Number 2211
1904     O o731 uid p731 p730
1905     T t731 o731 b626
1906 xiny 3379 B b731 t731
1907     T t732 o b731 b4
1908     B b732 t732
1909 xiny 3404 T t733 o730 b732
1910 xiny 3379 B b733 t733
1911 xiny 3404 T t734 o b733 b4
1912 xiny 3379 B b734 t734
1913 xiny 3404 T t735 o726 b618 b729 b623 b734
1914     B b735 t735
1915     T t736 o725 b735
1916     B b736 t736
1917     P p736 Number 2506
1918     P p737 Number 2899
1919     O o737 location p736 p737
1920     P p738 String op_assoc1
1921     O o738 rule p738
1922     T t738 o655 b674 b554
1923     S s738 t620 h
1924     G s738 t738
1925     B b738 s738
1926     T t739 o618 b738
1927     B b739 t739
1928 xiny 3379 NCzf_itt_eq!equal equal equal Czf_itt_eq
1929 xiny 3404 O o739 equal
1930     T t740 o559 b562 b674
1931     B b740 t740
1932     T t741 o559 b560 b696
1933 xiny 3379 B b741 t741
1934 xiny 3404 T t742 o739 b740 b741
1935     S s742 t620 h
1936     G s742 t742
1937     B b742 s742
1938     T t743 o618 b742
1939 xiny 3379 B b743 t743
1940 xiny 3404 T t744 o635 b739 b743
1941 xiny 3379 B b744 t744
1942 xiny 3404 T t745 o635 b658 b744
1943 xiny 3379 B b745 t745
1944 xiny 3404 T t746 o635 b656 b745
1945 xiny 3379 B b746 t746
1946 xiny 3404 T t747 o635 b676 b746
1947 xiny 3379 B b747 t747
1948 xiny 3404 T t748 o635 b641 b747
1949     B b748 t748
1950     T t749 o635 b639 b748
1951 xiny 3379 B b749 t749
1952 xiny 3404 P p749 Number 2531
1953     P p750 Number 2538
1954     O o750 resource_defs p749 p750 p264
1955     P p751 Number 2536
1956     O o751 uid p751 p750
1957     T t751 o751 b626
1958 xiny 3379 B b751 t751
1959     T t752 o b751 b4
1960     B b752 t752
1961 xiny 3404 T t753 o750 b752
1962 xiny 3379 B b753 t753
1963 xiny 3404 T t754 o b753 b4
1964 xiny 3379 B b754 t754
1965 xiny 3404 T t755 o738 b618 b749 b623 b754
1966     B b755 t755
1967     T t756 o737 b755
1968     B b756 t756
1969     P p756 Number 2972
1970     P p757 Number 3365
1971     O o757 location p756 p757
1972     P p758 String op_assoc2
1973     O o758 rule p758
1974     T t758 o739 b741 b740
1975     S s758 t620 h
1976     G s758 t758
1977     B b758 s758
1978     T t759 o618 b758
1979 xiny 3379 B b759 t759
1980 xiny 3404 T t760 o635 b739 b759
1981 xiny 3379 B b760 t760
1982 xiny 3404 T t761 o635 b658 b760
1983 xiny 3379 B b761 t761
1984 xiny 3404 T t762 o635 b656 b761
1985 xiny 3379 B b762 t762
1986 xiny 3404 T t763 o635 b676 b762
1987 xiny 3379 B b763 t763
1988 xiny 3404 T t764 o635 b641 b763
1989     B b764 t764
1990     T t765 o635 b639 b764
1991 xiny 3379 B b765 t765
1992 xiny 3404 P p765 Number 2997
1993     P p766 Number 3004
1994     O o766 resource_defs p765 p766 p264
1995     P p767 Number 3002
1996     O o767 uid p767 p766
1997     T t767 o767 b626
1998 xiny 3379 B b767 t767
1999     T t768 o b767 b4
2000     B b768 t768
2001 xiny 3404 T t769 o766 b768
2002 xiny 3379 B b769 t769
2003 xiny 3404 T t770 o b769 b4
2004 xiny 3379 B b770 t770
2005 xiny 3404 T t771 o758 b618 b765 b623 b770
2006     B b771 t771
2007     T t772 o757 b771
2008     B b772 t772
2009     P p772 Number 3438
2010     P p773 Number 3514
2011     O o773 location p772 p773
2012     P p774 String id_wf1
2013     O o774 rule p774
2014     T t774 o620 b567
2015     S s774 t620 h
2016     G s774 t774
2017     B b774 s774
2018     T t775 o618 b774
2019 xiny 3379 B b775 t775
2020 xiny 3404 P p775 Number 3460
2021     P p776 Number 3468
2022     O o776 resource_defs p775 p776 p264
2023     P p777 Number 3466
2024     O o777 uid p777 p776
2025     T t777 o777 b626
2026 xiny 3379 B b777 t777
2027     T t778 o b777 b4
2028     B b778 t778
2029 xiny 3404 T t779 o776 b778
2030 xiny 3379 B b779 t779
2031 xiny 3404 T t780 o b779 b4
2032 xiny 3379 B b780 t780
2033 xiny 3404 T t781 o774 b618 b775 b623 b780
2034     B b781 t781
2035     T t782 o773 b781
2036     B b782 t782
2037     P p782 Number 3517
2038     P p783 Number 3595
2039     O o783 location p782 p783
2040     P p784 String id_wf2
2041     O o784 rule p784
2042     T t784 o655 b567 b554
2043     S s784 t620 h
2044     G s784 t784
2045     B b784 s784
2046     T t785 o618 b784
2047 xiny 3379 B b785 t785
2048 xiny 3404 P p785 Number 3539
2049     P p786 Number 3546
2050     O o786 resource_defs p785 p786 p264
2051     P p787 Number 3544
2052     O o787 uid p787 p786
2053     T t787 o787 b626
2054 xiny 3379 B b787 t787
2055     T t788 o b787 b4
2056     B b788 t788
2057 xiny 3404 T t789 o786 b788
2058 xiny 3379 B b789 t789
2059 xiny 3404 T t790 o b789 b4
2060 xiny 3379 B b790 t790
2061 xiny 3404 T t791 o784 b618 b785 b623 b790
2062     B b791 t791
2063     T t792 o783 b791
2064     B b792 t792
2065     P p792 Number 3684
2066     P p793 Number 3860
2067     O o793 location p792 p793
2068     P p794 String id_eq1
2069     O o794 rule p794
2070     T t794 o655 b573 b554
2071     S s794 t620 h
2072     G s794 t794
2073     B b794 s794
2074     T t795 o618 b794
2075     B b795 t795
2076     T t796 o559 b567 b573
2077 xiny 3379 B b796 t796
2078 xiny 3404 T t797 o739 b796 b573
2079     S s797 t620 h
2080     G s797 t797
2081     B b797 s797
2082     T t798 o618 b797
2083 xiny 3379 B b798 t798
2084 xiny 3404 T t799 o635 b795 b798
2085     B b799 t799
2086     T t800 o635 b712 b799
2087 xiny 3379 B b800 t800
2088 xiny 3404 P p800 Number 3706
2089     P p801 Number 3713
2090     O o801 resource_defs p800 p801 p264
2091     P p802 Number 3711
2092     O o802 uid p802 p801
2093     T t802 o802 b626
2094 xiny 3379 B b802 t802
2095     T t803 o b802 b4
2096     B b803 t803
2097 xiny 3404 T t804 o801 b803
2098 xiny 3379 B b804 t804
2099 xiny 3404 T t805 o b804 b4
2100 xiny 3379 B b805 t805
2101 xiny 3404 T t806 o794 b618 b800 b623 b805
2102 xiny 3379 B b806 t806
2103 xiny 3404 T t807 o793 b806
2104     B b807 t807
2105     P p807 Number 3862
2106     P p808 Number 4038
2107     O o808 location p807 p808
2108     P p809 String id_eq2
2109     O o809 rule p809
2110     T t809 o559 b573 b567
2111 xiny 3379 B b809 t809
2112 xiny 3404 T t810 o739 b809 b573
2113     S s810 t620 h
2114     G s810 t810
2115     B b810 s810
2116     T t811 o618 b810
2117     B b811 t811
2118     T t812 o635 b795 b811
2119 xiny 3379 B b812 t812
2120 xiny 3404 T t813 o635 b712 b812
2121 xiny 3379 B b813 t813
2122 xiny 3404 P p813 Number 3884
2123     P p814 Number 3891
2124     O o814 resource_defs p813 p814 p264
2125     P p815 Number 3889
2126     O o815 uid p815 p814
2127     T t815 o815 b626
2128 xiny 3379 B b815 t815
2129 xiny 3404 T t816 o b815 b4
2130 xiny 3379 B b816 t816
2131 xiny 3404 T t817 o814 b816
2132 xiny 3379 B b817 t817
2133 xiny 3404 T t818 o b817 b4
2134     B b818 t818
2135     T t819 o809 b618 b813 b623 b818
2136     B b819 t819
2137     T t820 o808 b819
2138     B b820 t820
2139     P p820 Number 4040
2140     P p821 Number 4097
2141     O o821 location p820 p821
2142 xiny 3379 NOcaml!str_let str_let str_let Ocaml
2143 xiny 3404 O o822 str_let p820 p821
2144 xiny 3379 NOcaml!patt_var patt_var patt_var Ocaml
2145 xiny 3404 P p822 Number 4044
2146     O o823 patt_var p822 p821
2147 xiny 3379 NOcaml!patt_done patt_done patt_done Ocaml
2148 xiny 3404 O o824 patt_done p820 p821
2149     T t824 o824
2150     B b824 t824 id_elim2T
2151     T t825 o823 b824
2152     B b825 t825
2153 xiny 3379 NOcaml!fun fun fun Ocaml
2154 xiny 3404 O o825 fun p822 p821
2155 xiny 3379 NOcaml!patt_if patt_if patt_if Ocaml
2156 xiny 3404 O o826 patt_if p822 p821
2157     P p826 Number 4054
2158     P p827 Number 4055
2159     O o827 patt_var p826 p827
2160 xiny 3379 NOcaml!patt_body patt_body patt_body Ocaml
2161 xiny 3404 O o828 patt_body p822 p821
2162 xiny 3379 NOcaml!apply apply apply Ocaml
2163 xiny 3404 P p828 Number 4061
2164     O o829 apply p828 p821
2165     P p829 Number 4095
2166     O o830 apply p828 p829
2167 xiny 3379 NOcaml!lid lid lid Ocaml
2168 xiny 3404 P p830 Number 4067
2169     O o831 lid p828 p830
2170     O o832 lid p794
2171     T t832 o832
2172     B b832 t832
2173     T t833 o831 b832
2174     B b833 t833
2175     P p833 Number 4069
2176     P p834 Number 4094
2177     O o834 apply p833 p834
2178 xiny 3379 NOcaml!proj proj proj Ocaml
2179 xiny 3404 P p835 Number 4092
2180     O o835 proj p833 p835
2181     O o836 uid p833 p835
2182     O o837 uid p509
2183     T t837 o837
2184 xiny 3379 B b837 t837
2185 xiny 3404 T t838 o836 b837
2186 xiny 3379 B b838 t838
2187 xiny 3404 P p838 Number 4078
2188     O o838 lid p838 p835
2189     P p839 String hyp_count_addr
2190     O o839 lid p839
2191 xiny 3379 T t839 o839
2192     B b839 t839
2193     T t840 o838 b839
2194     B b840 t840
2195 xiny 3404 T t841 o835 b838 b840
2196 xiny 3379 B b841 t841
2197 xiny 3404 P p841 Number 4093
2198     O o841 lid p841 p834
2199     P p842 Var p
2200     O o842 var p842
2201     T t842 o842
2202 xiny 3379 B b842 t842
2203 xiny 3404 T t843 o841 b842
2204 xiny 3379 B b843 t843
2205 xiny 3404 T t844 o834 b841 b843
2206 xiny 3379 B b844 t844
2207 xiny 3404 T t845 o830 b833 b844
2208     B b845 t845
2209     P p845 Number 4096
2210     O o845 lid p845 p821
2211     T t846 o845 b842
2212 xiny 3379 B b846 t846
2213 xiny 3404 T t847 o829 b845 b846
2214 xiny 3379 B b847 t847
2215 xiny 3404 T t848 o828 b847
2216     B b848 t848 p
2217     T t849 o827 b848
2218 xiny 3379 B b849 t849
2219 xiny 3404 T t850 o826 b849
2220 xiny 3379 B b850 t850
2221 xiny 3404 T t851 o825 b850
2222 xiny 3379 B b851 t851
2223 xiny 3404 T t852 o822 b825 b851
2224 xiny 3379 B b852 t852
2225 xiny 3404 T t853 o b852 b4
2226 xiny 3379 B b853 t853
2227 xiny 3404 T t854 o822 b853
2228     B b854 t854
2229     T t855 o392 b854
2230 xiny 3379 B b855 t855
2231 xiny 3404 T t856 o821 b855
2232     B b856 t856
2233     P p856 Number 4099
2234     P p857 Number 4272
2235     O o857 location p856 p857
2236     P p858 String inv_wf1
2237     O o858 rule p858
2238     T t858 o572 b560
2239 xiny 3379 B b858 t858
2240 xiny 3404 T t859 o620 b858
2241     S s859 t620 h
2242     G s859 t859
2243     B b859 s859
2244     T t860 o618 b859
2245     B b860 t860
2246     T t861 o635 b656 b860
2247 xiny 3379 B b861 t861
2248 xiny 3404 T t862 o635 b639 b861
2249 xiny 3379 B b862 t862
2250 xiny 3404 P p862 Number 4122
2251     P p863 Number 4129
2252     O o863 resource_defs p862 p863 p264
2253     P p864 Number 4127
2254     O o864 uid p864 p863
2255     T t864 o864 b626
2256 xiny 3379 B b864 t864
2257 xiny 3404 T t865 o b864 b4
2258 xiny 3379 B b865 t865
2259 xiny 3404 T t866 o863 b865
2260 xiny 3379 B b866 t866
2261 xiny 3404 T t867 o b866 b4
2262     B b867 t867
2263     T t868 o858 b618 b862 b623 b867
2264     B b868 t868
2265     T t869 o857 b868
2266 xiny 3379 B b869 t869
2267 xiny 3404 P p869 Number 4274
2268     P p870 Number 4450
2269     O o870 location p869 p870
2270     P p871 String inv_wf2
2271     O o871 rule p871
2272     T t871 o655 b858 b554
2273     S s871 t620 h
2274     G s871 t871
2275     B b871 s871
2276     T t872 o618 b871
2277     B b872 t872
2278     T t873 o635 b656 b872
2279 xiny 3379 B b873 t873
2280 xiny 3404 T t874 o635 b639 b873
2281 xiny 3379 B b874 t874
2282 xiny 3404 P p874 Number 4297
2283     P p875 Number 4304
2284     O o875 resource_defs p874 p875 p264
2285     P p876 Number 4302
2286     O o876 uid p876 p875
2287     T t876 o876 b626
2288 xiny 3379 B b876 t876
2289 xiny 3404 T t877 o b876 b4
2290 xiny 3379 B b877 t877
2291 xiny 3404 T t878 o875 b877
2292 xiny 3379 B b878 t878
2293 xiny 3404 T t879 o b878 b4
2294     B b879 t879
2295     T t880 o871 b618 b874 b623 b879
2296 xiny 3379 B b880 t880
2297 xiny 3404 T t881 o870 b880
2298     B b881 t881
2299     P p881 Number 4452
2300     P p882 Number 4539
2301     O o882 location p881 p882
2302     P p883 String inv_fun1
2303     O o883 rule p883
2304     T t883 o572 b713
2305     B b883 t883 z
2306     T t884 o712 b883
2307     S s884 t620 h
2308     G s884 t884
2309     B b884 s884
2310     T t885 o618 b884
2311     B b885 t885
2312     P p885 Number 4476
2313     P p886 Number 4483
2314     O o886 resource_defs p885 p886 p264
2315     P p887 Number 4481
2316     O o887 uid p887 p886
2317     T t887 o887 b626
2318 xiny 3379 B b887 t887
2319 xiny 3404 T t888 o b887 b4
2320 xiny 3379 B b888 t888
2321 xiny 3404 T t889 o886 b888
2322 xiny 3379 B b889 t889
2323 xiny 3404 T t890 o b889 b4
2324 xiny 3379 B b890 t890
2325 xiny 3404 T t891 o883 b618 b885 b623 b890
2326 xiny 3379 B b891 t891
2327 xiny 3404 T t892 o882 b891
2328     B b892 t892
2329     P p892 Number 4541
2330     P p893 Number 4727
2331     O o893 location p892 p893
2332     P p894 String inv_id1
2333     O o894 rule p894
2334     T t894 o559 b858 b560
2335     B b894 t894
2336     T t895 o739 b894 b567
2337     S s895 t620 h
2338     G s895 t895
2339     B b895 s895
2340     T t896 o618 b895
2341 xiny 3379 B b896 t896
2342 xiny 3404 T t897 o635 b656 b896
2343 xiny 3379 B b897 t897
2344 xiny 3404 T t898 o635 b639 b897
2345     B b898 t898
2346     P p898 Number 4564
2347     P p899 Number 4571
2348     O o899 resource_defs p898 p899 p264
2349     P p900 Number 4569
2350     O o900 uid p900 p899
2351     T t900 o900 b626
2352 xiny 3379 B b900 t900
2353 xiny 3404 T t901 o b900 b4
2354 xiny 3379 B b901 t901
2355 xiny 3404 T t902 o899 b901
2356 xiny 3379 B b902 t902
2357 xiny 3404 T t903 o b902 b4
2358 xiny 3379 B b903 t903
2359 xiny 3404 T t904 o894 b618 b898 b623 b903
2360 xiny 3379 B b904 t904
2361 xiny 3404 T t905 o893 b904
2362     B b905 t905
2363     P p905 Number 4729
2364     P p906 Number 4915
2365     O o906 location p905 p906
2366     P p907 String inv_id2
2367     O o907 rule p907
2368     T t907 o559 b560 b858
2369 xiny 3379 B b907 t907
2370 xiny 3404 T t908 o739 b907 b567
2371     S s908 t620 h
2372     G s908 t908
2373     B b908 s908
2374     T t909 o618 b908
2375 xiny 3379 B b909 t909
2376 xiny 3404 T t910 o635 b656 b909
2377     B b910 t910
2378     T t911 o635 b639 b910
2379 xiny 3379 B b911 t911
2380 xiny 3404 P p911 Number 4752
2381     P p912 Number 4759
2382     O o912 resource_defs p911 p912 p264
2383     P p913 Number 4757
2384     O o913 uid p913 p912
2385     T t913 o913 b626
2386 xiny 3379 B b913 t913
2387 xiny 3404 T t914 o b913 b4
2388 xiny 3379 B b914 t914
2389 xiny 3404 T t915 o912 b914
2390 xiny 3379 B b915 t915
2391 xiny 3404 T t916 o b915 b4
2392 xiny 3379 B b916 t916
2393 xiny 3404 T t917 o907 b618 b911 b623 b916
2394 xiny 3379 B b917 t917
2395 xiny 3404 T t918 o906 b917
2396 xiny 3379 B b918 t918
2397 xiny 3404 P p918 Number 5376
2398     P p919 Number 5802
2399     O o919 location p918 p919
2400     P p920 String cancel1
2401     O o920 rule p920
2402     NSummary!term_param term_param term_param Summary
2403     O o921 term_param
2404     T t921 o921 b560
2405     B b921 t921
2406     T t922 o b921 b4
2407 xiny 3379 B b922 t922
2408 xiny 3404 T t923 o b617 b922
2409     B b923 t923
2410     T t924 o739 b562 b695
2411     S s924 t620 h
2412     G s924 t924
2413     B b924 s924
2414     T t925 o618 b924
2415 xiny 3379 B b925 t925
2416 xiny 3404 T t926 o739 b561 b674
2417     S s926 t620 h
2418     G s926 t926
2419     B b926 s926
2420     T t927 o618 b926
2421 xiny 3379 B b927 t927
2422 xiny 3404 T t928 o635 b925 b927
2423 xiny 3379 B b928 t928
2424 xiny 3404 T t929 o635 b739 b928
2425 xiny 3379 B b929 t929
2426 xiny 3404 T t930 o635 b658 b929
2427 xiny 3379 B b930 t930
2428 xiny 3404 T t931 o635 b656 b930
2429 xiny 3379 B b931 t931
2430 xiny 3404 T t932 o635 b676 b931
2431 xiny 3379 B b932 t932
2432 xiny 3404 T t933 o635 b641 b932
2433 xiny 3379 B b933 t933
2434 xiny 3404 T t934 o635 b639 b933
2435 xiny 3379 B b934 t934
2436 xiny 3404 NSummary!interactive interactive interactive Summary
2437     O o934 interactive
2438     NSummary!ext_rule ext_rule ext_rule Summary
2439     P p934 String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2440     O o935 ext_rule p934
2441     NSummary!status_incomplete status_incomplete status_incomplete Summary
2442     O o936 status_incomplete
2443     T t936 o936
2444 xiny 3379 B b936 t936
2445 xiny 3404 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2446     O o937 ext_unjustified
2447     NSummary!tactic_arg tactic_arg tactic_arg Summary
2448     P p937 String main
2449     O o938 tactic_arg p937
2450     NSummary!msequent msequent msequent Summary
2451     O o939 msequent
2452     T t939 o b924 b4
2453     B b939 t939
2454     T t940 o b738 b939
2455     B b940 t940
2456     T t941 o b657 b940
2457     B b941 t941
2458     T t942 o b655 b941
2459     B b942 t942
2460     T t943 o b675 b942
2461     B b943 t943
2462     T t944 o b640 b943
2463     B b944 t944
2464     T t945 o b638 b944
2465     B b945 t945
2466     T t946 o939 b926 b945
2467     B b946 t946
2468     NSummary!parent_none parent_none parent_none Summary
2469     O o946 parent_none
2470     T t947 o946
2471     B b947 t947
2472     T t948 o938 b946 b4 b947
2473     B b948 t948
2474     P p948 String assertion
2475     O o948 tactic_arg p948
2476     H h948 v t924
2477     T t949 o559 b858 b562
2478     B b949 t949
2479     T t950 o559 b858 b695
2480     B b950 t950
2481     T t951 o739 b949 b950
2482     S s951 t620 h h948
2483     G s951 t951
2484     B b951 s951
2485     T t952 o939 b951 b945
2486     B b952 t952
2487     S s952 t620 h h948
2488     G s952 t926
2489     B b953 s952
2490     T t953 o939 b953 b945
2491     B b954 t953
2492     T t954 o2 b948
2493     B b955 t954
2494     T t955 o938 b954 b4 b955
2495     B b956 t955
2496     T t956 o2 b956
2497     B b957 t956
2498     T t957 o948 b952 b4 b957
2499     B b958 t957
2500     H h958 v_1 t951
2501     S s958 t620 h h948 h958
2502     G s958 t926
2503     B b959 s958
2504     T t959 o939 b959 b945
2505     B b960 t959
2506     T t960 o938 b960 b4 b957
2507     B b961 t960
2508     T t961 o b961 b4
2509     B b962 t961
2510     T t962 o b958 b962
2511 xiny 3379 B b963 t962
2512 xiny 3404 T t963 o937 b948 b963
2513     B b964 t963
2514     P p964 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2515     O o964 ext_rule p964
2516     T t964 o937 b958 b4
2517     B b965 t964
2518     T t965 o964 b936 b965 b4 b4
2519     B b966 t965
2520     P p966 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2521     O o966 ext_rule p966
2522     P p967 String eq
2523     O o967 tactic_arg p967
2524     T t967 o559 b894 b561
2525 xiny 3379 B b967 t967
2526 xiny 3404 T t968 o739 b949 b967
2527     S s968 t620 h h948 h958
2528     G s968 t968
2529     B b968 s968
2530     T t969 o939 b968 b945
2531 xiny 3379 B b969 t969
2532 xiny 3404 T t970 o2 b961
2533 xiny 3379 B b970 t970
2534 xiny 3404 T t971 o967 b969 b4 b970
2535 xiny 3379 B b971 t971
2536 xiny 3404 T t972 o739 b967 b950
2537     H h972 v_2 t972
2538     S s972 t620 h h948 h958 h972
2539     G s972 t926
2540     B b972 s972
2541     T t973 o939 b972 b945
2542 xiny 3379 B b973 t973
2543 xiny 3404 T t974 o938 b973 b4 b970
2544 xiny 3379 B b974 t974
2545 xiny 3404 P p974 String wf
2546     O o974 tactic_arg p974
2547     B b975 t950 v_2
2548     T t975 o712 b975
2549     S s975 t620 h h948 h958
2550     G s975 t975
2551     B b976 s975
2552     T t976 o939 b976 b945
2553     B b977 t976
2554     NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2555     O o977 fun_prop
2556     P p977 Var v_2
2557     O o978 var p977
2558     T t978 o978
2559 xiny 3379 B b978 t978
2560 xiny 3404 T t979 o739 b978 b950
2561     B b979 t979 v_2
2562     T t980 o977 b979
2563     S s980 t620 h h948 h958
2564     G s980 t980
2565     B b980 s980
2566     T t981 o939 b980 b945
2567     B b981 t981
2568     NSummary!arg_named arg_named arg_named Summary
2569     P p981 String d_auto
2570     O o981 arg_named p981
2571     NSummary!arg_bool arg_bool arg_bool Summary
2572     P p982 String true
2573     O o982 arg_bool p982
2574     T t982 o982
2575 xiny 3379 B b982 t982
2576 xiny 3404 T t983 o981 b982
2577 xiny 3379 B b983 t983
2578 xiny 3404 T t984 o b983 b4
2579 xiny 3379 B b984 t984
2580 xiny 3404 T t985 o974 b981 b984 b970
2581     B b985 t985
2582     T t986 o2 b985
2583 xiny 3379 B b986 t986
2584 xiny 3404 T t987 o974 b977 b4 b986
2585 xiny 3379 B b987 t987
2586 xiny 3404 T t988 o b987 b4
2587     B b988 t988
2588     T t989 o b974 b988
2589     B b989 t989
2590     T t990 o b971 b989
2591     B b990 t990
2592     T t991 o937 b961 b990
2593     B b991 t991
2594     P p991 String autoT
2595     O o991 ext_rule p991
2596     T t992 o937 b971 b4
2597     B b992 t992
2598     T t993 o991 b936 b992 b4 b4
2599     B b993 t993
2600     P p993 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2601     O o993 ext_rule p993
2602     T t994 o559 b894 b674
2603     B b994 t994
2604     T t995 o739 b950 b994
2605     S s995 t620 h h948 h958 h972
2606     G s995 t995
2607     B b995 s995
2608     T t996 o939 b995 b945
2609     B b996 t996
2610     T t997 o2 b974
2611     B b997 t997
2612     T t998 o967 b996 b4 b997
2613     B b998 t998
2614     T t999 o739 b967 b994
2615     H h999 v_3 t999
2616     S s999 t620 h h948 h958 h972 h999
2617     G s999 t926
2618     B b999 s999
2619     T t1000 o939 b999 b945
2620     B b1000 t1000
2621     T t1001 o938 b1000 b4 b997
2622     B b1001 t1001
2623     B b1002 t967 v_3
2624     T t1002 o712 b1002
2625     S s1002 t620 h h948 h958 h972
2626     G s1002 t1002
2627     B b1003 s1002
2628     T t1003 o939 b1003 b945
2629 xiny 3379 B b1004 t1003
2630 xiny 3404 P p1004 Var v_3
2631     O o1004 var p1004
2632     T t1004 o1004
2633 xiny 3379 B b1005 t1004
2634 xiny 3404 T t1005 o739 b967 b1005
2635     B b1006 t1005 v_3
2636     T t1006 o977 b1006
2637     S s1006 t620 h h948 h958 h972
2638     G s1006 t1006
2639     B b1007 s1006
2640     T t1007 o939 b1007 b945
2641 xiny 3379 B b1008 t1007
2642 xiny 3404 T t1008 o974 b1008 b984 b997
2643 xiny 3379 B b1009 t1008
2644 xiny 3404 T t1009 o2 b1009
2645 xiny 3379 B b1010 t1009
2646 xiny 3404 T t1010 o974 b1004 b4 b1010
2647 xiny 3379 B b1011 t1010
2648 xiny 3404 T t1011 o b1011 b4
2649     B b1012 t1011
2650     T t1012 o b1001 b1012
2651 xiny 3379 B b1013 t1012
2652 xiny 3404 T t1013 o b998 b1013
2653 xiny 3379 B b1014 t1013
2654 xiny 3404 T t1014 o937 b974 b1014
2655 xiny 3379 B b1015 t1014
2656 xiny 3404 T t1015 o937 b998 b4
2657     B b1016 t1015
2658     T t1016 o991 b936 b1016 b4 b4
2659     B b1017 t1016
2660     P p1017 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2661     O o1017 ext_rule p1017
2662     T t1017 o559 b567 b561
2663 xiny 3379 B b1018 t1017
2664 xiny 3404 T t1018 o559 b567 b674
2665 xiny 3379 B b1019 t1018
2666 xiny 3404 T t1019 o739 b1018 b1019
2667     H h1019 v_4 t1019
2668     S s1019 t620 h h948 h958 h972 h999 h1019
2669     G s1019 t926
2670     B b1020 s1019
2671     T t1020 o939 b1020 b945
2672     B b1021 t1020
2673     T t1021 o2 b1001
2674 xiny 3379 B b1022 t1021
2675 xiny 3404 T t1022 o938 b1021 b4 b1022
2676 xiny 3379 B b1023 t1022
2677 xiny 3404 T t1023 o b1023 b4
2678 xiny 3379 B b1024 t1023
2679 xiny 3404 T t1024 o937 b1001 b1024
2680 xiny 3379 B b1025 t1024
2681 xiny 3404 P p1025 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2682     O o1025 ext_rule p1025
2683     T t1025 o739 b561 b1019
2684     H h1025 v_5 t1025
2685     S s1025 t620 h h948 h958 h972 h999 h1019 h1025
2686     G s1025 t926
2687     B b1026 s1025
2688     T t1026 o939 b1026 b945
2689 xiny 3379 B b1027 t1026
2690 xiny 3404 T t1027 o2 b1023
2691 xiny 3379 B b1028 t1027
2692 xiny 3404 T t1028 o938 b1027 b4 b1028
2693     B b1029 t1028
2694     B b1030 t1018 v_5
2695     T t1030 o712 b1030
2696     S s1030 t620 h h948 h958 h972 h999 h1019
2697     G s1030 t1030
2698     B b1031 s1030
2699     T t1031 o939 b1031 b945
2700 xiny 3379 B b1032 t1031
2701 xiny 3404 P p1032 Var v_5
2702     O o1032 var p1032
2703     T t1032 o1032
2704 xiny 3379 B b1033 t1032
2705 xiny 3404 T t1033 o739 b1033 b1019
2706     B b1034 t1033 v_5
2707     T t1034 o977 b1034
2708     S s1034 t620 h h948 h958 h972 h999 h1019
2709     G s1034 t1034
2710     B b1035 s1034
2711     T t1035 o939 b1035 b945
2712 xiny 3379 B b1036 t1035
2713 xiny 3404 T t1036 o974 b1036 b984 b1028
2714 xiny 3379 B b1037 t1036
2715 xiny 3404 T t1037 o2 b1037
2716 xiny 3379 B b1038 t1037
2717 xiny 3404 T t1038 o974 b1032 b4 b1038
2718 xiny 3379 B b1039 t1038
2719 xiny 3404 T t1039 o b1039 b4
2720 xiny 3379 B b1040 t1039
2721 xiny 3404 T t1040 o b1029 b1040
2722 xiny 3379 B b1041 t1040
2723 xiny 3404 T t1041 o937 b1023 b1041
2724 xiny 3379 B b1042 t1041
2725 xiny 3404 P p1042 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2726     O o1042 ext_rule p1042
2727     H h1042 v_6 t926
2728     S s1042 t620 h h948 h958 h972 h999 h1019 h1025 h1042
2729     G s1042 t926
2730     B b1043 s1042
2731     T t1043 o939 b1043 b945
2732 xiny 3379 B b1044 t1043
2733 xiny 3404 T t1044 o2 b1029
2734 xiny 3379 B b1045 t1044
2735 xiny 3404 T t1045 o938 b1044 b4 b1045
2736 xiny 3379 B b1046 t1045
2737 xiny 3404 T t1046 o b1046 b4
2738 xiny 3379 B b1047 t1046
2739 xiny 3404 T t1047 o937 b1029 b1047
2740 xiny 3379 B b1048 t1047
2741 xiny 3404 P p1048 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2742     O o1048 ext_rule p1048
2743     T t1048 o937 b1046 b4
2744 xiny 3379 B b1049 t1048
2745 xiny 3404 T t1049 o1048 b936 b1049 b4 b4
2746 xiny 3379 B b1050 t1049
2747 xiny 3404 T t1050 o b1050 b4
2748 xiny 3379 B b1051 t1050
2749 xiny 3404 P p1051 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2750     O o1051 ext_rule p1051
2751     B b1052 t1017 v_6
2752     T t1052 o712 b1052
2753     S s1052 t620 h h948 h958 h972 h999 h1019 h1025
2754     G s1052 t1052
2755     B b1053 s1052
2756     T t1053 o939 b1053 b945
2757 xiny 3379 B b1054 t1053
2758 xiny 3404 P p1054 Var v_6
2759     O o1054 var p1054
2760     T t1054 o1054
2761 xiny 3379 B b1055 t1054
2762 xiny 3404 T t1055 o739 b1018 b1055
2763     B b1056 t1055 v_6
2764     T t1056 o977 b1056
2765     S s1056 t620 h h948 h958 h972 h999 h1019 h1025
2766     G s1056 t1056
2767     B b1057 s1056
2768     T t1057 o939 b1057 b945
2769 xiny 3379 B b1058 t1057
2770 xiny 3404 T t1058 o974 b1058 b984 b1045
2771 xiny 3379 B b1059 t1058
2772 xiny 3404 T t1059 o2 b1059
2773 xiny 3379 B b1060 t1059
2774 xiny 3404 T t1060 o974 b1054 b4 b1060
2775 xiny 3379 B b1061 t1060
2776 xiny 3404 T t1061 o937 b1061 b4
2777     B b1062 t1061
2778     T t1062 o1051 b936 b1062 b4 b4
2779     B b1063 t1062
2780     T t1063 o b1063 b4
2781     B b1064 t1063
2782     T t1064 o1042 b936 b1048 b1051 b1064
2783     B b1065 t1064
2784     T t1065 o937 b1039 b4
2785     B b1066 t1065
2786     T t1066 o1051 b936 b1066 b4 b4
2787     B b1067 t1066
2788     T t1067 o b1067 b4
2789     B b1068 t1067
2790     T t1068 o b1065 b1068
2791     B b1069 t1068
2792     T t1069 o1025 b936 b1042 b1069 b4
2793     B b1070 t1069
2794     T t1070 o b1070 b4
2795     B b1071 t1070
2796     T t1071 o1017 b936 b1025 b1071 b4
2797     B b1072 t1071
2798     P p1072 String "rwh unfold_fun_set 0 thenT autoT"
2799     O o1072 ext_rule p1072
2800     T t1072 o937 b1011 b4
2801     B b1073 t1072
2802     T t1073 o1072 b936 b1073 b4 b4
2803     B b1074 t1073
2804     T t1074 o b1074 b4
2805     B b1075 t1074
2806     T t1075 o b1072 b1075
2807     B b1076 t1075
2808     T t1076 o b1017 b1076
2809     B b1077 t1076
2810     T t1077 o993 b936 b1015 b1077 b4
2811     B b1078 t1077
2812     T t1078 o937 b987 b4
2813     B b1079 t1078
2814     T t1079 o1072 b936 b1079 b4 b4
2815     B b1080 t1079
2816     T t1080 o b1080 b4
2817     B b1081 t1080
2818     T t1081 o b1078 b1081
2819     B b1082 t1081
2820     T t1082 o b993 b1082
2821     B b1083 t1082
2822     T t1083 o966 b936 b991 b1083 b4
2823     B b1084 t1083
2824     T t1084 o b1084 b4
2825     B b1085 t1084
2826     T t1085 o b966 b1085
2827     B b1086 t1085
2828     NSummary!ext_goal ext_goal ext_goal Summary
2829     O o1086 ext_goal
2830     S s1086 t620 h
2831     G s1086 t951
2832     B b1087 s1086
2833     T t1087 o939 b1087 b945
2834     B b1088 t1087
2835     T t1088 o948 b1088 b4 b955
2836     B b1089 t1088
2837     T t1089 o1086 b1089
2838     B b1090 t1089
2839     T t1090 o b1090 b4
2840     B b1091 t1090
2841     T t1091 o964 b936 b1090 b1091 b4
2842     B b1092 t1091
2843     P p1092 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2844     O o1092 ext_rule p1092
2845     H h1092 v t951
2846     S s1092 t620 h h1092
2847     G s1092 t926
2848     B b1093 s1092
2849     T t1093 o939 b1093 b945
2850     B b1094 t1093
2851     T t1094 o938 b1094 b4 b955
2852     B b1095 t1094
2853     T t1095 o1086 b1095
2854     B b1096 t1095
2855     P p1096 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2856     O o1096 ext_rule p1096
2857     P p1097 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2858     O o1097 ext_rule p1097
2859     T t1097 o b1096 b4
2860 xiny 3379 B b1097 t1097
2861 xiny 3404 H h1097 x t924
2862     H h1098 v_1 t972
2863     H h1099 v_2 t999
2864     H h1100 v_3 t1019
2865     H h1101 v_4 t1025
2866     B b1101 t1017 v_5
2867     T t1101 o712 b1101
2868     S s1101 t620 h h1097 h1092 h1098 h1099 h1100 h1101
2869     G s1101 t1101
2870     B b1102 s1101
2871     T t1102 o b738 b4
2872 xiny 3379 B b1103 t1102
2873 xiny 3404 T t1103 o b657 b1103
2874     B b1104 t1103
2875     T t1104 o b655 b1104
2876 xiny 3379 B b1105 t1104
2877 xiny 3404 T t1105 o b675 b1105
2878 xiny 3379 B b1106 t1105
2879 xiny 3404 T t1106 o b640 b1106
2880 xiny 3379 B b1107 t1106
2881 xiny 3404 T t1107 o b638 b1107
2882 xiny 3379 B b1108 t1107
2883 xiny 3404 T t1108 o939 b1102 b1108
2884 xiny 3379 B b1109 t1108
2885 xiny 3404 T t1109 o739 b1018 b1033
2886     B b1110 t1109 v_5
2887     T t1110 o977 b1110
2888     S s1110 t620 h h1097 h1092 h1098 h1099 h1100 h1101
2889     G s1110 t1110
2890     B b1111 s1110
2891     T t1111 o939 b1111 b1108
2892 xiny 3379 B b1112 t1111
2893 xiny 3404 S s1112 t620 h h1097 h1092 h1098 h1099 h1100 h1101
2894     G s1112 t926
2895     B b1113 s1112
2896     T t1113 o939 b1113 b1108
2897     B b1114 t1113
2898     S s1114 t620 h h1097 h1092 h1098 h1099 h1100
2899     G s1114 t926
2900     B b1115 s1114
2901     T t1115 o939 b1115 b1108
2902 xiny 3379 B b1116 t1115
2903 xiny 3404 S s1116 t620 h h1097 h1092 h1098 h1099
2904     G s1116 t926
2905     B b1117 s1116
2906     T t1117 o939 b1117 b1108
2907     B b1118 t1117
2908     S s1118 t620 h h1097 h1092 h1098
2909     G s1118 t926
2910 xiny 3379 B b1119 s1118
2911 xiny 3404 T t1119 o939 b1119 b1108
2912 xiny 3379 B b1120 t1119
2913 xiny 3404 S s1120 t620 h h1097 h1092
2914     G s1120 t926
2915     B b1121 s1120
2916     T t1121 o939 b1121 b1108
2917     B b1122 t1121
2918     S s1122 t620 h h1097
2919     G s1122 t926
2920     B b1123 s1122
2921     T t1123 o939 b1123 b1108
2922 xiny 3379 B b1124 t1123
2923 xiny 3404 T t1124 o938 b1124 b4 b947
2924 xiny 3379 B b1125 t1124
2925 xiny 3404 T t1125 o2 b1125
2926 xiny 3379 B b1126 t1125
2927 xiny 3404 T t1126 o938 b1122 b4 b1126
2928 xiny 3379 B b1127 t1126
2929 xiny 3404 T t1127 o2 b1127
2930 xiny 3379 B b1128 t1127
2931 xiny 3404 T t1128 o938 b1120 b4 b1128
2932 xiny 3379 B b1129 t1128
2933 xiny 3404 T t1129 o2 b1129
2934 xiny 3379 B b1130 t1129
2935 xiny 3404 T t1130 o938 b1118 b4 b1130
2936     B b1131 t1130
2937     T t1131 o2 b1131
2938 xiny 3379 B b1132 t1131
2939 xiny 3404 T t1132 o938 b1116 b4 b1132
2940 xiny 3379 B b1133 t1132
2941 xiny 3404 T t1133 o2 b1133
2942 xiny 3379 B b1134 t1133
2943 xiny 3404 T t1134 o938 b1114 b4 b1134
2944     B b1135 t1134
2945     T t1135 o2 b1135
2946     B b1136 t1135
2947     T t1136 o974 b1112 b984 b1136
2948 xiny 3379 B b1137 t1136
2949 xiny 3404 T t1137 o2 b1137
2950     B b1138 t1137
2951     T t1138 o974 b1109 b4 b1138
2952     B b1139 t1138
2953     T t1139 o937 b1139 b4
2954 xiny 3379 B b1140 t1139
2955 xiny 3404 T t1140 o1051 b936 b1140 b4 b4
2956 xiny 3379 B b1141 t1140
2957 xiny 3404 T t1141 o b1141 b4
2958 xiny 3379 B b1142 t1141
2959 xiny 3404 T t1142 o1097 b936 b1096 b1097 b1142
2960 xiny 3379 B b1143 t1142
2961     T t1143 o b1143 b4
2962     B b1144 t1143
2963 xiny 3404 B b1145 t1018 v_4
2964     T t1145 o712 b1145
2965     S s1145 t620 h h1097 h1092 h1098 h1099 h1100
2966     G s1145 t1145
2967     B b1146 s1145
2968     T t1146 o939 b1146 b1108
2969 xiny 3379 B b1147 t1146
2970 xiny 3404 P p1147 Var v_4
2971     O o1147 var p1147
2972     T t1147 o1147
2973 xiny 3379 B b1148 t1147
2974 xiny 3404 T t1148 o739 b1148 b1019
2975     B b1149 t1148 v_4
2976     T t1149 o977 b1149
2977     S s1149 t620 h h1097 h1092 h1098 h1099 h1100
2978     G s1149 t1149
2979     B b1150 s1149
2980     T t1150 o939 b1150 b1108
2981 xiny 3379 B b1151 t1150
2982 xiny 3404 T t1151 o974 b1151 b984 b1134
2983 xiny 3379 B b1152 t1151
2984 xiny 3404 T t1152 o2 b1152
2985 xiny 3379 B b1153 t1152
2986 xiny 3404 T t1153 o974 b1147 b4 b1153
2987 xiny 3379 B b1154 t1153
2988 xiny 3404 T t1154 o937 b1154 b4
2989     B b1155 t1154
2990     T t1155 o1051 b936 b1155 b4 b4
2991 xiny 3379 B b1156 t1155
2992 xiny 3404 T t1156 o b1156 b4
2993 xiny 3379 B b1157 t1156
2994 xiny 3404 T t1157 o1025 b936 b1096 b1144 b1157
2995 xiny 3379 B b1158 t1157
2996 xiny 3404 T t1158 o b1158 b4
2997     B b1159 t1158
2998     T t1159 o1017 b936 b1096 b1159 b4
2999     B b1160 t1159
3000     T t1160 o b1160 b4
3001 xiny 3379 B b1161 t1160
3002 xiny 3404 S s1161 t620 h h1097 h1092 h1098
3003     G s1161 t995
3004     B b1162 s1161
3005     T t1162 o939 b1162 b1108
3006     B b1163 t1162
3007     T t1163 o967 b1163 b4 b1130
3008 xiny 3379 B b1164 t1163
3009 xiny 3404 T t1164 o937 b1164 b4
3010 xiny 3379 B b1165 t1164
3011 xiny 3404 T t1165 o991 b936 b1165 b4 b4
3012 xiny 3379 B b1166 t1165
3013 xiny 3404 P p1166 String "rwh unfold_fun_prop 0 thenT autoT"
3014     O o1166 ext_rule p1166
3015     T t1166 o739 b967 b978
3016     B b1167 t1166 v_2
3017     T t1167 o977 b1167
3018     S s1167 t620 h h1097 h1092 h1098
3019     G s1167 t1167
3020     B b1168 s1167
3021     T t1168 o939 b1168 b1108
3022 xiny 3379 B b1169 t1168
3023 xiny 3404 T t1169 o974 b1169 b4 b1130
3024 xiny 3379 B b1170 t1169
3025 xiny 3404 NCzf_itt_set!set set set Czf_itt_set
3026     O o1170 set
3027     T t1170 o1170
3028     H h1170 s1_1 t1170
3029     H h1171 s2_1 t1170
3030     P p1171 Var s1_1
3031     O o1171 var p1171
3032     T t1171 o1171
3033     B b1171 t1171
3034     P p1172 Var s2_1
3035     O o1172 var p1172
3036     T t1172 o1172
3037     B b1172 t1172
3038     T t1173 o739 b1171 b1172
3039     H h1173 x_1 t1173
3040     T t1174 o739 b967 b1171
3041     H h1174 x_2 t1174
3042     T t1175 o676 b967 b1172
3043     S s1175 t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174
3044     G s1175 t1175
3045     B b1175 s1175
3046     T t1176 o939 b1175 b1108
3047     B b1176 t1176
3048     T t1177 o739 b967 b1172
3049     S s1177 t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174
3050     G s1177 t1177
3051     B b1177 s1177
3052     T t1178 o939 b1177 b1108
3053     B b1178 t1178
3054     NItt_logic Itt_logic Itt_logic NIL
3055     NItt_logic!implies implies implies Itt_logic
3056     O o1178 implies
3057     B b1179 t1174
3058     B b1180 t1177
3059     T t1180 o1178 b1179 b1180
3060     S s1180 t620 h h1097 h1092 h1098 h1170 h1171 h1173
3061     G s1180 t1180
3062     B b1181 s1180
3063     T t1181 o939 b1181 b1108
3064 xiny 3379 B b1182 t1181
3065 xiny 3404 B b1183 t1173
3066     B b1184 t1180
3067     T t1184 o1178 b1183 b1184
3068     S s1184 t620 h h1097 h1092 h1098 h1170 h1171
3069     G s1184 t1184
3070     B b1185 s1184
3071     T t1185 o939 b1185 b1108
3072 xiny 3379 B b1186 t1185
3073 xiny 3404 NItt_logic!all all all Itt_logic
3074     O o1186 all
3075     B b1187 t1170
3076     B b1188 t1184 s2_1
3077     T t1188 o1186 b1187 b1188
3078     S s1188 t620 h h1097 h1092 h1098 h1170
3079     G s1188 t1188
3080 xiny 3379 B b1189 s1188
3081 xiny 3404 T t1189 o939 b1189 b1108
3082 xiny 3379 B b1190 t1189
3083 xiny 3404 B b1191 t1188 s1_1
3084     T t1191 o1186 b1187 b1191
3085     S s1191 t620 h h1097 h1092 h1098
3086     G s1191 t1191
3087     B b1192 s1191
3088     T t1192 o939 b1192 b1108
3089 xiny 3379 B b1193 t1192
3090 xiny 3404 T t1193 o2 b1170
3091     B b1194 t1193
3092     T t1194 o974 b1193 b984 b1194
3093 xiny 3379 B b1195 t1194
3094 xiny 3404 T t1195 o2 b1195
3095 xiny 3379 B b1196 t1195
3096 xiny 3404 T t1196 o938 b1190 b984 b1196
3097 xiny 3379 B b1197 t1196
3098 xiny 3404 T t1197 o2 b1197
3099 xiny 3379 B b1198 t1197
3100 xiny 3404 T t1198 o938 b1186 b984 b1198
3101 xiny 3379 B b1199 t1198
3102 xiny 3404 T t1199 o2 b1199
3103 xiny 3379 B b1200 t1199
3104 xiny 3404 T t1200 o938 b1182 b984 b1200
3105 xiny 3379 B b1201 t1200
3106 xiny 3404 T t1201 o2 b1201
3107 xiny 3379 B b1202 t1201
3108 xiny 3404 T t1202 o938 b1178 b984 b1202
3109 xiny 3379 B b1203 t1202
3110 xiny 3404 T t1203 o2 b1203
3111     B b1204 t1203
3112     T t1204 o938 b1176 b4 b1204
3113 xiny 3379 B b1205 t1204
3114 xiny 3404 T t1205 o b1205 b4
3115 xiny 3379 B b1206 t1205
3116 xiny 3404 T t1206 o937 b1170 b1206
3117 xiny 3379 B b1207 t1206
3118 xiny 3404 P p1207 String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3119     O o1207 ext_rule p1207
3120     T t1207 o937 b1205 b4
3121 xiny 3379 B b1208 t1207
3122 xiny 3404 T t1208 o1207 b936 b1208 b4 b4
3123 xiny 3379 B b1209 t1208
3124 xiny 3404 T t1209 o b1209 b4
3125     B b1210 t1209
3126     T t1210 o1166 b936 b1207 b1210 b4
3127 xiny 3379 B b1211 t1210
3128 xiny 3404 T t1211 o b1211 b4
3129 xiny 3379 B b1212 t1211
3130 xiny 3404 T t1212 o b1166 b1212
3131 xiny 3379 B b1213 t1212
3132 xiny 3404 T t1213 o1096 b936 b1096 b1161 b1213
3133 xiny 3379 B b1214 t1213
3134 xiny 3404 T t1214 o b1214 b4
3135 xiny 3379 B b1215 t1214
3136 xiny 3404 S s1215 t620 h h1097 h1092
3137     G s1215 t968
3138     B b1216 s1215
3139     T t1216 o939 b1216 b1108
3140 xiny 3379 B b1217 t1216
3141 xiny 3404 T t1217 o967 b1217 b4 b1128
3142 xiny 3379 B b1218 t1217
3143 xiny 3404 T t1218 o937 b1218 b4
3144 xiny 3379 B b1219 t1218
3145 xiny 3404 T t1219 o991 b936 b1219 b4 b4
3146 xiny 3379 B b1220 t1219
3147 xiny 3404 P p1220 Var v_1
3148     O o1220 var p1220
3149     T t1220 o1220
3150 xiny 3379 B b1221 t1220
3151 xiny 3404 T t1221 o739 b1221 b950
3152     B b1222 t1221 v_1
3153     T t1222 o977 b1222
3154     S s1222 t620 h h1097 h1092
3155     G s1222 t1222
3156     B b1223 s1222
3157     T t1223 o939 b1223 b1108
3158 xiny 3379 B b1224 t1223
3159 xiny 3404 T t1224 o974 b1224 b4 b1128
3160 xiny 3379 B b1225 t1224
3161 xiny 3404 H h1225 s2 t1170
3162     T t1225 o739 b1171 b561
3163     H h1226 x_1 t1225
3164     T t1226 o739 b1171 b950
3165     H h1227 x_2 t1226
3166     T t1227 o676 b561 b950
3167     S s1227 t620 h h1097 h1092 h1170 h1225 h1226 h1227
3168     G s1227 t1227
3169     B b1227 s1227
3170     T t1228 o939 b1227 b1108
3171     B b1228 t1228
3172     T t1229 o739 b561 b950
3173     S s1229 t620 h h1097 h1092 h1170 h1225 h1226 h1227
3174     G s1229 t1229
3175     B b1229 s1229
3176     T t1230 o939 b1229 b1108
3177 xiny 3379 B b1230 t1230
3178 xiny 3404 B b1231 t1226
3179     B b1232 t1229
3180     T t1232 o1178 b1231 b1232
3181     S s1232 t620 h h1097 h1092 h1170 h1225 h1226
3182 xiny 3379 G s1232 t1232
3183 xiny 3404 B b1233 s1232
3184     T t1233 o939 b1233 b1108
3185     B b1234 t1233
3186     B b1235 t1225
3187     B b1236 t1232
3188     T t1236 o1178 b1235 b1236
3189     S s1236 t620 h h1097 h1092 h1170 h1225
3190     G s1236 t1236
3191     B b1237 s1236
3192     T t1237 o939 b1237 b1108
3193     B b1238 t1237
3194     B b1239 t1236 s2
3195     T t1239 o1186 b1187 b1239
3196     S s1239 t620 h h1097 h1092 h1170
3197 xiny 3379 G s1239 t1239
3198     B b1240 s1239
3199 xiny 3404 T t1240 o939 b1240 b1108
3200 xiny 3379 B b1241 t1240
3201     B b1242 t1239 s1_1
3202 xiny 3404 T t1242 o1186 b1187 b1242
3203     S s1242 t620 h h1097 h1092
3204 xiny 3379 G s1242 t1242
3205     B b1243 s1242
3206 xiny 3404 T t1243 o939 b1243 b1108
3207 xiny 3379 B b1244 t1243
3208 xiny 3404 T t1244 o2 b1225
3209 xiny 3379 B b1245 t1244
3210 xiny 3404 T t1245 o974 b1244 b984 b1245
3211 xiny 3379 B b1246 t1245
3212     T t1246 o2 b1246
3213     B b1247 t1246
3214 xiny 3404 T t1247 o938 b1241 b984 b1247
3215 xiny 3379 B b1248 t1247
3216     T t1248 o2 b1248
3217     B b1249 t1248
3218 xiny 3404 T t1249 o938 b1238 b984 b1249
3219 xiny 3379 B b1250 t1249
3220     T t1250 o2 b1250
3221     B b1251 t1250
3222 xiny 3404 T t1251 o938 b1234 b984 b1251
3223 xiny 3379 B b1252 t1251
3224 xiny 3404 T t1252 o2 b1252
3225 xiny 3379 B b1253 t1252
3226 xiny 3404 T t1253 o938 b1230 b984 b1253
3227 xiny 3379 B b1254 t1253
3228 xiny 3404 T t1254 o2 b1254
3229 xiny 3379 B b1255 t1254
3230 xiny 3404 T t1255 o938 b1228 b4 b1255
3231 xiny 3379 B b1256 t1255
3232 xiny 3404 T t1256 o b1256 b4
3233 xiny 3379 B b1257 t1256
3234 xiny 3404 T t1257 o937 b1225 b1257
3235 xiny 3379 B b1258 t1257
3236 xiny 3404 P p1258 String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3237     O o1258 ext_rule p1258
3238     T t1258 o937 b1256 b4
3239 xiny 3379 B b1259 t1258
3240 xiny 3404 T t1259 o1258 b936 b1259 b4 b4
3241 xiny 3379 B b1260 t1259
3242     T t1260 o b1260 b4
3243     B b1261 t1260
3244 xiny 3404 T t1261 o1166 b936 b1258 b1261 b4
3245 xiny 3379 B b1262 t1261
3246     T t1262 o b1262 b4
3247     B b1263 t1262
3248 xiny 3404 T t1263 o b1220 b1263
3249 xiny 3379 B b1264 t1263
3250 xiny 3404 T t1264 o1092 b936 b1096 b1215 b1264
3251 xiny 3379 B b1265 t1264
3252 xiny 3404 P p1265 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3253     O o1265 ext_rule p1265
3254     H h1265 y_1 t642
3255     T t1265 o620 b695
3256     H h1266 z_1 t1265
3257     T t1266 o676 b562 b695
3258     H h1267 z t1266
3259     T t1267 o676 b949 b950
3260     H h1268 v t1267
3261     T t1268 o676 b561 b674
3262     S s1268 t620 h h1265 h1266 h1267 h1268
3263     G s1268 t1268
3264     B b1268 s1268
3265     T t1269 o939 b1268 b1108
3266 xiny 3379 B b1269 t1269
3267 xiny 3404 S s1269 t620 h h1265 h1266 h1267 h1268
3268     G s1269 t926
3269     B b1270 s1269
3270     T t1270 o939 b1270 b1108
3271     B b1271 t1270
3272     NItt_logic!and and and Itt_logic
3273     O o1271 and
3274     B b1272 t642
3275     B b1273 t1265
3276     T t1273 o1271 b1272 b1273
3277     H h1273 y t1273
3278     S s1273 t620 h h1273 h1267 h1268
3279     G s1273 t926
3280     B b1274 s1273
3281     T t1274 o939 b1274 b1108
3282     B b1275 t1274
3283     B b1276 t1273
3284     B b1277 t1266
3285     T t1277 o1271 b1276 b1277
3286     H h1277 x t1277
3287     S s1277 t620 h h1277 h1268
3288     G s1277 t926
3289     B b1278 s1277
3290     T t1278 o939 b1278 b1108
3291     B b1279 t1278
3292     S s1279 t620 h h1277
3293     G s1279 t926
3294     B b1280 s1279
3295     T t1280 o939 b1280 b1108
3296     B b1281 t1280
3297     T t1281 o938 b1281 b4 b1126
3298     B b1282 t1281
3299     T t1282 o2 b1282
3300     B b1283 t1282
3301     T t1283 o938 b1279 b4 b1283
3302     B b1284 t1283
3303     T t1284 o2 b1284
3304     B b1285 t1284
3305     T t1285 o938 b1275 b4 b1285
3306     B b1286 t1285
3307     T t1286 o2 b1286
3308     B b1287 t1286
3309     T t1287 o938 b1271 b984 b1287
3310     B b1288 t1287
3311     T t1288 o2 b1288
3312     B b1289 t1288
3313     T t1289 o938 b1269 b4 b1289
3314     B b1290 t1289
3315     T t1290 o676 b967 b950
3316     H h1290 v_1 t1290
3317     S s1290 t620 h h1265 h1266 h1267 h1268 h1290
3318     G s1290 t1268
3319     B b1291 s1290
3320     T t1291 o939 b1291 b1108
3321     B b1292 t1291
3322     T t1292 o2 b1290
3323     B b1293 t1292
3324     T t1293 o938 b1292 b4 b1293
3325     B b1294 t1293
3326     B b1295 t950 v_1
3327     T t1295 o712 b1295
3328     S s1295 t620 h h1265 h1266 h1267 h1268
3329     G s1295 t1295
3330     B b1296 s1295
3331     T t1296 o939 b1296 b1108
3332     B b1297 t1296
3333     T t1297 o676 b1221 b950
3334     B b1298 t1297 v_1
3335     T t1298 o977 b1298
3336     S s1298 t620 h h1265 h1266 h1267 h1268
3337     G s1298 t1298
3338     B b1299 s1298
3339     T t1299 o939 b1299 b1108
3340     B b1300 t1299
3341     T t1300 o974 b1300 b984 b1293
3342     B b1301 t1300
3343     T t1301 o2 b1301
3344     B b1302 t1301
3345     T t1302 o974 b1297 b4 b1302
3346     B b1303 t1302
3347     T t1303 o b1303 b4
3348     B b1304 t1303
3349     T t1304 o b1294 b1304
3350     B b1305 t1304
3351     T t1305 o937 b1290 b1305
3352     B b1306 t1305
3353     P p1306 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3354     O o1306 ext_rule p1306
3355     T t1306 o676 b967 b994
3356     H h1306 v_2 t1306
3357     S s1306 t620 h h1265 h1266 h1267 h1268 h1290 h1306
3358     G s1306 t1268
3359     B b1307 s1306
3360     T t1307 o939 b1307 b1108
3361     B b1308 t1307
3362     T t1308 o2 b1294
3363     B b1309 t1308
3364     T t1309 o938 b1308 b4 b1309
3365     B b1310 t1309
3366     B b1311 t967 v_2
3367     T t1311 o712 b1311
3368     S s1311 t620 h h1265 h1266 h1267 h1268 h1290
3369     G s1311 t1311
3370     B b1312 s1311
3371     T t1312 o939 b1312 b1108
3372     B b1313 t1312
3373     T t1313 o676 b967 b978
3374     B b1314 t1313 v_2
3375     T t1314 o977 b1314
3376     S s1314 t620 h h1265 h1266 h1267 h1268 h1290
3377     G s1314 t1314
3378     B b1315 s1314
3379     T t1315 o939 b1315 b1108
3380     B b1316 t1315
3381     T t1316 o974 b1316 b984 b1309
3382     B b1317 t1316
3383     T t1317 o2 b1317
3384     B b1318 t1317
3385     T t1318 o974 b1313 b4 b1318
3386     B b1319 t1318
3387     T t1319 o b1319 b4
3388     B b1320 t1319
3389     T t1320 o b1310 b1320
3390     B b1321 t1320
3391     T t1321 o937 b1294 b1321
3392     B b1322 t1321
3393     P p1322 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3394     O o1322 ext_rule p1322
3395     T t1322 o676 b1018 b1019
3396     H h1322 v_3 t1322
3397     S s1322 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3398     G s1322 t1268
3399     B b1323 s1322
3400     T t1323 o939 b1323 b1108
3401     B b1324 t1323
3402     T t1324 o2 b1310
3403     B b1325 t1324
3404     T t1325 o938 b1324 b4 b1325
3405     B b1326 t1325
3406     T t1326 o b1326 b4
3407     B b1327 t1326
3408     T t1327 o937 b1310 b1327
3409     B b1328 t1327
3410     P p1328 String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"
3411     O o1328 ext_rule p1328
3412     T t1328 o676 b561 b1019
3413     H h1328 v_4 t1328
3414     S s1328 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1328
3415     G s1328 t1268
3416     B b1329 s1328
3417     T t1329 o939 b1329 b1108
3418     B b1330 t1329
3419     T t1330 o2 b1326
3420     B b1331 t1330
3421     T t1331 o938 b1330 b4 b1331
3422     B b1332 t1331
3423     S s1332 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3424     G s1332 t1145
3425     B b1333 s1332
3426     T t1333 o939 b1333 b1108
3427     B b1334 t1333
3428     T t1334 o676 b1148 b1019
3429     B b1335 t1334 v_4
3430     T t1335 o977 b1335
3431     S s1335 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3432     G s1335 t1335
3433     B b1336 s1335
3434     T t1336 o939 b1336 b1108
3435     B b1337 t1336
3436     T t1337 o974 b1337 b984 b1331
3437     B b1338 t1337
3438     T t1338 o2 b1338
3439     B b1339 t1338
3440     T t1339 o974 b1334 b4 b1339
3441     B b1340 t1339
3442     T t1340 o b1340 b4
3443     B b1341 t1340
3444     T t1341 o b1332 b1341
3445     B b1342 t1341
3446     T t1342 o937 b1326 b1342
3447     B b1343 t1342
3448     P p1343 String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3449     O o1343 ext_rule p1343
3450     T t1343 o937 b1332 b4
3451     B b1344 t1343
3452     T t1344 o1343 b936 b1344 b4 b4
3453     B b1345 t1344
3454     H h1345 s1 t1170
3455     T t1345 o739 b560 b561
3456     H h1346 x t1345
3457     T t1346 o739 b1019 b1019
3458     S s1346 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345 h1225 h1346
3459     G s1346 t1346
3460     B b1346 s1346
3461     T t1347 o939 b1346 b1108
3462 xiny 3379 B b1347 t1347
3463 xiny 3404 B b1348 t1345
3464     B b1349 t1346
3465     T t1349 o1178 b1348 b1349
3466     S s1349 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345 h1225
3467     G s1349 t1349
3468     B b1350 s1349
3469     T t1350 o939 b1350 b1108
3470     B b1351 t1350
3471     B b1352 t1349 s2
3472     T t1352 o1186 b1187 b1352
3473     S s1352 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345
3474     G s1352 t1352
3475     B b1353 s1352
3476     T t1353 o939 b1353 b1108
3477     B b1354 t1353
3478     B b1355 t1352 s1
3479     T t1355 o1186 b1187 b1355
3480     S s1355 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3481     G s1355 t1355
3482     B b1356 s1355
3483     T t1356 o939 b1356 b1108
3484     B b1357 t1356
3485     T t1357 o2 b1340
3486     B b1358 t1357
3487     T t1358 o974 b1357 b984 b1358
3488     B b1359 t1358
3489     T t1359 o2 b1359
3490     B b1360 t1359
3491     T t1360 o938 b1354 b984 b1360
3492     B b1361 t1360
3493     T t1361 o2 b1361
3494     B b1362 t1361
3495     T t1362 o938 b1351 b984 b1362
3496     B b1363 t1362
3497     T t1363 o2 b1363
3498     B b1364 t1363
3499     T t1364 o938 b1347 b4 b1364
3500     B b1365 t1364
3501     T t1365 o b1365 b4
3502     B b1366 t1365
3503     T t1366 o937 b1340 b1366
3504     B b1367 t1366
3505     T t1367 o1086 b1365
3506     B b1368 t1367
3507     T t1368 o b1368 b4
3508     B b1369 t1368
3509     T t1369 o1072 b936 b1367 b1369 b4
3510     B b1370 t1369
3511     T t1370 o b1370 b4
3512     B b1371 t1370
3513     T t1371 o b1345 b1371
3514     B b1372 t1371
3515     T t1372 o1328 b936 b1343 b1372 b4
3516     B b1373 t1372
3517     T t1373 o b1373 b4
3518     B b1374 t1373
3519     T t1374 o1322 b936 b1328 b1374 b4
3520     B b1375 t1374
3521     T t1375 o937 b1319 b4
3522     B b1376 t1375
3523     T t1376 o1072 b936 b1376 b4 b4
3524     B b1377 t1376
3525     T t1377 o b1377 b4
3526     B b1378 t1377
3527     T t1378 o b1375 b1378
3528     B b1379 t1378
3529     P p1379 String "eqSetSymT thenT autoT"
3530     O o1379 ext_rule p1379
3531     T t1379 o676 b950 b994
3532     S s1379 t620 h h1265 h1266 h1267 h1268 h1290
3533     G s1379 t1379
3534     B b1380 s1379
3535     T t1380 o939 b1380 b1108
3536     B b1381 t1380
3537     S s1381 t620 h h1265 h1266 h1267 h1268 h1290
3538     G s1381 t995
3539     B b1382 s1381
3540     T t1382 o939 b1382 b1108
3541     B b1383 t1382
3542     T t1383 o967 b1383 b984 b1309
3543 xiny 3379 B b1384 t1383
3544 xiny 3404 T t1384 o2 b1384
3545     B b1385 t1384
3546     T t1385 o967 b1381 b4 b1385
3547     B b1386 t1385
3548     T t1386 o676 b994 b950
3549     S s1386 t620 h h1265 h1266 h1267 h1268 h1290
3550     G s1386 t1386
3551     B b1387 s1386
3552     T t1387 o939 b1387 b1108
3553     B b1388 t1387
3554     T t1388 o2 b1386
3555     B b1389 t1388
3556     T t1389 o967 b1388 b4 b1389
3557     B b1390 t1389
3558     T t1390 o b1390 b4
3559     B b1391 t1390
3560     T t1391 o937 b1386 b1391
3561     B b1392 t1391
3562     T t1392 o1086 b1390
3563     B b1393 t1392
3564     T t1393 o b1393 b4
3565     B b1394 t1393
3566     T t1394 o1379 b936 b1392 b1394 b4
3567     B b1395 t1394
3568     T t1395 o b1395 b4
3569     B b1396 t1395
3570     T t1396 o1306 b936 b1322 b1379 b1396
3571     B b1397 t1396
3572     T t1397 o937 b1303 b4
3573     B b1398 t1397
3574     T t1398 o1072 b936 b1398 b4 b4
3575     B b1399 t1398
3576     T t1399 o b1399 b4
3577 xiny 3379 B b1400 t1399
3578 xiny 3404 T t1400 o b1397 b1400
3579 xiny 3379 B b1401 t1400
3580 xiny 3404 T t1401 o676 b949 b967
3581     S s1401 t620 h h1265 h1266 h1267 h1268
3582     G s1401 t1401
3583     B b1402 s1401
3584     T t1402 o939 b1402 b1108
3585 xiny 3379 B b1403 t1402
3586 xiny 3404 S s1403 t620 h h1265 h1266 h1267 h1268
3587     G s1403 t968
3588     B b1404 s1403
3589     T t1404 o939 b1404 b1108
3590 xiny 3379 B b1405 t1404
3591 xiny 3404 T t1405 o967 b1405 b984 b1293
3592 xiny 3379 B b1406 t1405
3593     T t1406 o2 b1406
3594     B b1407 t1406
3595 xiny 3404 T t1407 o967 b1403 b4 b1407
3596 xiny 3379 B b1408 t1407
3597 xiny 3404 T t1408 o676 b967 b949
3598     S s1408 t620 h h1265 h1266 h1267 h1268
3599     G s1408 t1408
3600     B b1409 s1408
3601     T t1409 o939 b1409 b1108
3602 xiny 3379 B b1410 t1409
3603 xiny 3404 T t1410 o2 b1408
3604     B b1411 t1410
3605     T t1411 o967 b1410 b4 b1411
3606 xiny 3379 B b1412 t1411
3607 xiny 3404 T t1412 o b1412 b4
3608 xiny 3379 B b1413 t1412
3609 xiny 3404 T t1413 o937 b1408 b1413
3610 xiny 3379 B b1414 t1413
3611 xiny 3404 T t1414 o1086 b1412
3612 xiny 3379 B b1415 t1414
3613 xiny 3404 T t1415 o b1415 b4
3614 xiny 3379 B b1416 t1415
3615 xiny 3404 T t1416 o1379 b936 b1414 b1416 b4
3616 xiny 3379 B b1417 t1416
3617     T t1417 o b1417 b4
3618     B b1418 t1417
3619 xiny 3404 T t1418 o1265 b936 b1306 b1401 b1418
3620 xiny 3379 B b1419 t1418
3621 xiny 3404 T t1419 o b1419 b4
3622     B b1420 t1419
3623     T t1420 o b1265 b1420
3624     B b1421 t1420
3625     T t1421 o b1092 b1421
3626     B b1422 t1421
3627     T t1422 o935 b936 b964 b1086 b1422
3628     B b1423 t1422
3629     T t1423 o934 b1423
3630     B b1424 t1423
3631     P p1424 Number 5399
3632     P p1425 Number 5407
3633     O o1425 resource_defs p1424 p1425 p264
3634     P p1426 Number 5405
3635     O o1426 uid p1426 p1425
3636     T t1426 o1426 b626
3637     B b1426 t1426
3638     T t1427 o b1426 b4
3639 xiny 3379 B b1427 t1427
3640 xiny 3404 T t1428 o1425 b1427
3641 xiny 3379 B b1428 t1428
3642 xiny 3404 T t1429 o b1428 b4
3643 xiny 3379 B b1429 t1429
3644 xiny 3404 T t1430 o920 b923 b934 b1424 b1429
3645 xiny 3379 B b1430 t1430
3646 xiny 3404 T t1431 o919 b1430
3647 xiny 3379 B b1431 t1431
3648 xiny 3404 P p1431 Number 5847
3649     P p1432 Number 6273
3650     O o1432 location p1431 p1432
3651     P p1433 String cancel2
3652     O o1433 rule p1433
3653     T t1433 o921 b674
3654     B b1433 t1433
3655     T t1434 o b1433 b4
3656 xiny 3379 B b1434 t1434
3657 xiny 3404 T t1435 o b617 b1434
3658 xiny 3379 B b1435 t1435
3659 xiny 3404 T t1436 o739 b695 b696
3660     S s1436 t620 h
3661     G s1436 t1436
3662     B b1436 s1436
3663     T t1437 o618 b1436
3664     B b1437 t1437
3665     S s1437 t620 h
3666     G s1437 t1345
3667     B b1438 s1437
3668     T t1438 o618 b1438
3669     B b1439 t1438
3670     T t1439 o635 b1437 b1439
3671     B b1440 t1439
3672     T t1440 o635 b739 b1440
3673 xiny 3379 B b1441 t1440
3674 xiny 3404 T t1441 o635 b658 b1441
3675     B b1442 t1441
3676     T t1442 o635 b656 b1442
3677     B b1443 t1442
3678     T t1443 o635 b676 b1443
3679 xiny 3379 B b1444 t1443
3680 xiny 3404 T t1444 o635 b641 b1444
3681 xiny 3379 B b1445 t1444
3682 xiny 3404 T t1445 o635 b639 b1445
3683 xiny 3379 B b1446 t1445
3684 xiny 3404 P p1446 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"
3685     O o1446 ext_rule p1446
3686     T t1446 o b1436 b4
3687 xiny 3379 B b1447 t1446
3688 xiny 3404 T t1447 o b738 b1447
3689 xiny 3379 B b1448 t1447
3690 xiny 3404 T t1448 o b657 b1448
3691 xiny 3379 B b1449 t1448
3692 xiny 3404 T t1449 o b655 b1449
3693 xiny 3379 B b1450 t1449
3694 xiny 3404 T t1450 o b675 b1450
3695 xiny 3379 B b1451 t1450
3696 xiny 3404 T t1451 o b640 b1451
3697 xiny 3379 B b1452 t1451
3698 xiny 3404 T t1452 o b638 b1452
3699 xiny 3379 B b1453 t1452
3700 xiny 3404 T t1453 o939 b1438 b1453
3701 xiny 3379 B b1454 t1453
3702 xiny 3404 T t1454 o938 b1454 b4 b947
3703 xiny 3379 B b1455 t1454
3704 xiny 3404 H h1455 v t1436
3705     T t1455 o572 b674
3706 xiny 3379 B b1456 t1455
3707 xiny 3404 T t1456 o559 b695 b1456
3708 xiny 3379 B b1457 t1456
3709 xiny 3404 T t1457 o559 b696 b1456
3710 xiny 3379 B b1458 t1457
3711 xiny 3404 T t1458 o739 b1457 b1458
3712     S s1458 t620 h h1455
3713     G s1458 t1458
3714     B b1459 s1458
3715     T t1459 o939 b1459 b1453
3716 xiny 3379 B b1460 t1459
3717 xiny 3404 S s1460 t620 h h1455
3718     G s1460 t1345
3719     B b1461 s1460
3720     T t1461 o939 b1461 b1453
3721 xiny 3379 B b1462 t1461
3722 xiny 3404 T t1462 o2 b1455
3723 xiny 3379 B b1463 t1462
3724 xiny 3404 T t1463 o938 b1462 b4 b1463
3725 xiny 3379 B b1464 t1463
3726 xiny 3404 T t1464 o2 b1464
3727 xiny 3379 B b1465 t1464
3728 xiny 3404 T t1465 o948 b1460 b4 b1465
3729 xiny 3379 B b1466 t1465
3730 xiny 3404 H h1466 v_1 t1458
3731     S s1466 t620 h h1455 h1466
3732     G s1466 t1345
3733     B b1467 s1466
3734     T t1467 o939 b1467 b1453
3735     B b1468 t1467
3736     T t1468 o938 b1468 b4 b1465
3737     B b1469 t1468
3738     T t1469 o b1469 b4
3739     B b1470 t1469
3740     T t1470 o b1466 b1470
3741     B b1471 t1470
3742     T t1471 o937 b1455 b1471
3743     B b1472 t1471
3744     T t1472 o937 b1466 b4
3745     B b1473 t1472
3746     T t1473 o964 b936 b1473 b4 b4
3747     B b1474 t1473
3748     P p1474 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
3749     O o1474 ext_rule p1474
3750     T t1474 o559 b674 b1456
3751     B b1475 t1474
3752     T t1475 o559 b560 b1475
3753     B b1476 t1475
3754     T t1476 o739 b1476 b1458
3755     H h1476 v_2 t1476
3756     S s1476 t620 h h1455 h1466 h1476
3757     G s1476 t1345
3758     B b1477 s1476
3759     T t1477 o939 b1477 b1453
3760     B b1478 t1477
3761     T t1478 o2 b1469
3762     B b1479 t1478
3763     T t1479 o938 b1478 b4 b1479
3764     B b1480 t1479
3765     B b1481 t1457 v_2
3766     T t1481 o712 b1481
3767     S s1481 t620 h h1455 h1466
3768     G s1481 t1481
3769     B b1482 s1481
3770     T t1482 o939 b1482 b1453
3771     B b1483 t1482
3772     T t1483 o739 b978 b1458
3773     B b1484 t1483 v_2
3774     T t1484 o977 b1484
3775     S s1484 t620 h h1455 h1466
3776     G s1484 t1484
3777     B b1485 s1484
3778     T t1485 o939 b1485 b1453
3779     B b1486 t1485
3780     T t1486 o974 b1486 b984 b1479
3781     B b1487 t1486
3782     T t1487 o2 b1487
3783