/[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 3379 - (hide annotations) (download)
Fri Sep 14 07:00:13 2001 UTC (19 years, 10 months ago) by xiny
File size: 103995 byte(s)
Definition of algebraic group.

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     P p218 Number 2358
593     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     O o221 type_lid p221 p218
604     T t222 o221 b220
605     B b222 t222
606     T t223 o b222 b4
607     B b223 t223
608     T t224 o b221 b223
609     B b224 t224
610     T t225 o218 b224
611     B b225 t225
612     T t226 o213 b217 b225
613     B b226 t226
614     P p226 String cache
615     O o226 resource p226
616     P p227 Number 1424
617     P p228 Number 1434
618     O o228 type_lid p227 p228
619     P p229 String cache_rule
620     O o229 type_lid p229
621     T t229 o229
622     B b229 t229
623     T t230 o228 b229
624     B b230 t230
625     P p230 Number 1436
626     P p231 Number 1441
627     O o231 type_lid p230 p231
628     O o232 type_lid p226
629     T t232 o232
630     B b232 t232
631     T t233 o231 b232
632     B b233 t233
633     T t234 o226 b230 b233
634     B b234 t234
635     P p234 String elim
636     O o234 resource p234
637     P p235 Number 1761
638     P p236 Number 1783
639     O o236 type_prod p235 p236
640     P p237 Number 1765
641     O o237 type_lid p235 p237
642     P p238 String term
643     O o238 type_lid p238
644     T t238 o238
645     B b238 t238
646     T t239 o237 b238
647     B b239 t239
648     NOcaml!type_fun type_fun type_fun Ocaml
649     P p239 Number 1769
650     P p240 Number 1782
651     O o240 type_fun p239 p240
652     P p241 Number 1772
653     O o241 type_lid p239 p241
654     P p242 String int
655     O o242 type_lid p242
656     T t242 o242
657     B b242 t242
658     T t243 o241 b242
659     B b243 t243
660     P p243 Number 1776
661     O o243 type_lid p243 p240
662     T t244 o243 b220
663     B b244 t244
664     T t245 o240 b243 b244
665     B b245 t245
666     T t246 o b245 b4
667     B b246 t246
668     T t247 o b239 b246
669     B b247 t247
670     T t248 o236 b247
671     B b248 t248
672     P p248 Number 1785
673     P p249 Number 1798
674     O o249 type_fun p248 p249
675     P p250 Number 1788
676     O o250 type_lid p248 p250
677     T t250 o250 b242
678     B b250 t250
679     P p251 Number 1792
680     O o251 type_lid p251 p249
681     T t251 o251 b220
682     B b251 t251
683     T t252 o249 b250 b251
684     B b252 t252
685     T t253 o234 b248 b252
686     B b253 t253
687     P p253 String eqcd
688     O o253 resource p253
689     P p254 Number 6168
690     P p255 Number 6181
691     O o255 type_prod p254 p255
692     P p256 Number 6172
693     O o256 type_lid p254 p256
694     T t256 o256 b238
695     B b256 t256
696     P p257 Number 6175
697     O o257 type_lid p257 p255
698     T t257 o257 b220
699     B b257 t257
700     T t258 o b257 b4
701     B b258 t258
702     T t259 o b256 b258
703     B b259 t259
704     T t260 o255 b259
705     B b260 t260
706     P p260 Number 6183
707     P p261 Number 6189
708     O o261 type_lid p260 p261
709     T t261 o261 b220
710     B b261 t261
711     T t262 o253 b260 b261
712     B b262 t262
713     P p262 String intro
714     O o262 resource p262
715     P p263 Number 1815
716     P p264 Number 1852
717     O o264 type_prod p263 p264
718     P p265 Number 1819
719     O o265 type_lid p263 p265
720     T t265 o265 b238
721     B b265 t265
722     P p266 Number 1823
723     P p267 Number 1851
724     O o267 type_prod p266 p267
725     P p268 Number 1829
726     O o268 type_lid p266 p268
727     P p269 String string
728     O o269 type_lid p269
729     T t269 o269
730     B b269 t269
731     T t270 o268 b269
732     B b270 t270
733     NOcaml!type_apply type_apply type_apply Ocaml
734     P p270 Number 1832
735     P p271 Number 1842
736     O o271 type_apply p270 p271
737     P p272 Number 1836
738     O o272 type_lid p272 p271
739     P p273 String option
740     O o273 type_lid p273
741     T t273 o273
742     B b273 t273
743     T t274 o272 b273
744     B b274 t274
745     P p274 Number 1835
746     O o274 type_lid p270 p274
747     T t275 o274 b242
748     B b275 t275
749     T t276 o271 b274 b275
750     B b276 t276
751     P p276 Number 1845
752     O o276 type_lid p276 p267
753     T t277 o276 b220
754     B b277 t277
755     T t278 o b277 b4
756     B b278 t278
757     T t279 o b276 b278
758     B b279 t279
759     T t280 o b270 b279
760     B b280 t280
761     T t281 o267 b280
762     B b281 t281
763     T t282 o b281 b4
764     B b282 t282
765     T t283 o b265 b282
766     B b283 t283
767     T t284 o264 b283
768     B b284 t284
769     P p284 Number 1854
770     P p285 Number 1860
771     O o285 type_lid p284 p285
772     T t285 o285 b220
773     B b285 t285
774     T t286 o262 b284 b285
775     B b286 t286
776     P p286 String reduce
777     O o286 resource p286
778     P p287 Number 2920
779     P p288 Number 2931
780     O o288 type_prod p287 p288
781     P p289 Number 2924
782     O o289 type_lid p287 p289
783     T t289 o289 b238
784     B b289 t289
785     P p290 Number 2927
786     O o290 type_lid p290 p288
787     P p291 String conv
788     O o291 type_lid p291
789     T t291 o291
790     B b291 t291
791     T t292 o290 b291
792     B b292 t292
793     T t293 o b292 b4
794     B b293 t293
795     T t294 o b289 b293
796     B b294 t294
797     T t295 o288 b294
798     B b295 t295
799     P p295 Number 2933
800     P p296 Number 2937
801     O o296 type_lid p295 p296
802     T t296 o296 b291
803     B b296 t296
804     T t297 o286 b295 b296
805     B b297 t297
806     P p297 String squash
807     O o297 resource p297
808     P p298 Number 4017
809     P p299 Number 4028
810     O o299 type_lid p298 p299
811     P p300 String squash_info
812     O o300 type_lid p300
813     T t300 o300
814     B b300 t300
815     T t301 o299 b300
816     B b301 t301
817     P p301 Number 4030
818     P p302 Number 4043
819     O o302 type_fun p301 p302
820     P p303 Number 4033
821     O o303 type_lid p301 p303
822     T t303 o303 b242
823     B b303 t303
824     P p304 Number 4037
825     O o304 type_lid p304 p302
826     T t304 o304 b220
827     B b304 t304
828     T t305 o302 b303 b304
829     B b305 t305
830     T t306 o297 b301 b305
831     B b306 t306
832     P p306 String sub
833     O o306 resource p306
834     P p307 Number 4871
835     P p308 Number 4888
836     O o308 type_lid p307 p308
837     P p309 String sub_resource_info
838     O o309 type_lid p309
839     T t309 o309
840     B b309 t309
841     T t310 o308 b309
842     B b310 t310
843     P p310 Number 4890
844     P p311 Number 4896
845     O o311 type_lid p310 p311
846     T t311 o311 b220
847     B b311 t311
848     T t312 o306 b310 b311
849     B b312 t312
850     P p312 String toploop
851     O o312 resource p312
852     P p313 Number 2445
853     P p314 Number 2467
854     O o314 type_prod p313 p314
855     P p315 Number 2451
856     O o315 type_lid p313 p315
857     T t315 o315 b269
858     B b315 t315
859     P p316 Number 2454
860     P p317 Number 2460
861     O o317 type_lid p316 p317
862     T t317 o317 b269
863     B b317 t317
864     P p318 Number 2463
865     O o318 type_lid p318 p314
866     P p319 String expr
867     O o319 type_lid p319
868     T t319 o319
869     B b319 t319
870     T t320 o318 b319
871     B b320 t320
872     T t321 o b320 b4
873     B b321 t321
874     T t322 o b317 b321
875     B b322 t322
876     T t323 o b315 b322
877     B b323 t323
878     T t324 o314 b323
879     B b324 t324
880     P p324 Number 2469
881     P p325 Number 2478
882     O o325 type_lid p324 p325
883     P p326 String top_table
884     O o326 type_lid p326
885     T t326 o326
886     B b326 t326
887     T t327 o325 b326
888     B b327 t327
889     T t328 o312 b324 b327
890     B b328 t328
891     P p328 String typeinf
892     O o328 resource p328
893     P p329 Number 2151
894     P p330 Number 2172
895     O o330 type_lid p329 p330
896     P p331 String typeinf_resource_info
897     O o331 type_lid p331
898     T t331 o331
899     B b331 t331
900     T t332 o330 b331
901     B b332 t332
902     P p332 Number 2174
903     P p333 Number 2186
904     O o333 type_lid p332 p333
905     P p334 String typeinf_func
906     O o334 type_lid p334
907     T t334 o334
908     B b334 t334
909     T t335 o333 b334
910     B b335 t335
911     T t336 o328 b332 b335
912     B b336 t336
913     P p336 String typeinf_subst
914     O o336 resource p336
915     P p337 Number 1825
916     P p338 Number 1843
917     O o338 type_lid p337 p338
918     P p339 String typeinf_subst_info
919     O o339 type_lid p339
920     T t339 o339
921     B b339 t339
922     T t340 o338 b339
923     B b340 t340
924     P p340 Number 1862
925     O o340 type_lid p276 p340
926     P p341 String typeinf_subst_fun
927     O o341 type_lid p341
928     T t341 o341
929     B b341 t341
930     T t342 o340 b341
931     B b342 t342
932     T t343 o336 b340 b342
933     B b343 t343
934     T t344 o b343 b4
935     B b344 t344
936     T t345 o b336 b344
937     B b345 t345
938     T t346 o b328 b345
939     B b346 t346
940     T t347 o b312 b346
941     B b347 t347
942     T t348 o b306 b347
943     B b348 t348
944     T t349 o b297 b348
945     B b349 t349
946     T t350 o b286 b349
947     B b350 t350
948     T t351 o b262 b350
949     B b351 t351
950     T t352 o b253 b351
951     B b352 t352
952     T t353 o b234 b352
953     B b353 t353
954     T t354 o b226 b353
955     B b354 t354
956     T t355 o2 b5 b213 b354
957     B b355 t355
958     T t356 o1 b355
959     B b356 t356
960     P p356 Number 20
961     P p357 Number 42
962     O o357 location p356 p357
963     P p358 String Czf_itt_member
964     O o358 parent p358
965     T t358 o358
966     B b358 t358
967     T t359 o b358 b4
968     B b359 t359
969     P p359 String Czf_itt_eq
970     O o359 parent p359
971     T t360 o359
972     B b360 t360
973     T t361 o b360 b4
974     B b361 t361
975     T t362 o b361 b4
976     B b362 t362
977     T t363 o b359 b362
978     B b363 t363
979     T t364 o2 b359 b363 b354
980     B b364 t364
981     T t365 o357 b364
982     B b365 t365
983     P p365 Number 43
984     P p366 Number 61
985     O o366 location p365 p366
986     T t366 o2 b361 b4 b354
987     B b366 t366
988     T t367 o366 b366
989     B b367 t367
990     P p367 Number 62
991     P p368 Number 82
992     O o368 location p367 p368
993     P p369 String Czf_itt_dall
994     O o369 parent p369
995     T t369 o369
996     B b369 t369
997     T t370 o b369 b4
998     B b370 t370
999     P p370 String Czf_itt_set_ind
1000     O o370 parent p370
1001     T t371 o370
1002     B b371 t371
1003     T t372 o b371 b4
1004     B b372 t372
1005     P p372 String Czf_itt_all
1006     O o372 parent p372
1007     T t373 o372
1008     B b373 t373
1009     T t374 o b373 b4
1010     B b374 t374
1011     P p374 String Czf_itt_sep
1012     O o374 parent p374
1013     T t375 o374
1014     B b375 t375
1015     T t376 o b375 b4
1016     B b376 t376
1017     T t377 o b376 b4
1018     B b377 t377
1019     T t378 o b374 b377
1020     B b378 t378
1021     T t379 o b372 b378
1022     B b379 t379
1023     T t380 o b370 b379
1024     B b380 t380
1025     T t381 o2 b370 b380 b354
1026     B b381 t381
1027     T t382 o368 b381
1028     B b382 t382
1029     P p382 Number 83
1030     P p383 Number 102
1031     O o383 location p382 p383
1032     P p384 String Czf_itt_and
1033     O o384 parent p384
1034     T t384 o384
1035     B b384 t384
1036     T t385 o b384 b4
1037     B b385 t385
1038     T t386 o b385 b4
1039     B b386 t386
1040     T t387 o2 b385 b386 b354
1041     B b387 t387
1042     T t388 o383 b387
1043     B b388 t388
1044     P p388 Number 104
1045     P p389 Number 115
1046     O o389 location p388 p389
1047     NSummary!summary_item summary_item summary_item Summary
1048     O o390 summary_item
1049     NOcaml!str_open str_open str_open Ocaml
1050     O o391 str_open p388 p389
1051     NOcaml!string string string Ocaml
1052     P p391 String Printf
1053     O o392 string p391
1054     T t392 o392
1055     B b392 t392
1056     T t393 o b392 b4
1057     B b393 t393
1058     T t394 o391 b393
1059     B b394 t394
1060     T t395 o390 b394
1061     B b395 t395
1062     T t396 o389 b395
1063     B b396 t396
1064     P p396 Number 116
1065     P p397 Number 129
1066     O o397 location p396 p397
1067     O o398 str_open p396 p397
1068     P p398 String Mp_debug
1069     O o399 string p398
1070     T t399 o399
1071     B b399 t399
1072     T t400 o b399 b4
1073     B b400 t400
1074     T t401 o398 b400
1075     B b401 t401
1076     T t402 o390 b401
1077     B b402 t402
1078     T t403 o397 b402
1079     B b403 t403
1080     P p403 Number 130
1081     P p404 Number 159
1082     O o404 location p403 p404
1083     O o405 str_open p403 p404
1084     P p405 String Refiner
1085     O o406 string p405
1086     T t406 o406
1087     B b406 t406
1088     P p406 String TermType
1089     O o407 string p406
1090     T t407 o407
1091     B b407 t407
1092     T t408 o b407 b4
1093     B b408 t408
1094     T t409 o b406 b408
1095     B b409 t409
1096     T t410 o b406 b409
1097     B b410 t410
1098     T t411 o405 b410
1099     B b411 t411
1100     T t412 o390 b411
1101     B b412 t412
1102     T t413 o404 b412
1103     B b413 t413
1104     P p413 Number 160
1105     P p414 Number 185
1106     O o414 location p413 p414
1107     O o415 str_open p413 p414
1108     P p415 String Term
1109     O o416 string p415
1110     T t416 o416
1111     B b416 t416
1112     T t417 o b416 b4
1113     B b417 t417
1114     T t418 o b406 b417
1115     B b418 t418
1116     T t419 o b406 b418
1117     B b419 t419
1118     T t420 o415 b419
1119     B b420 t420
1120     T t421 o390 b420
1121     B b421 t421
1122     T t422 o414 b421
1123     B b422 t422
1124     P p422 Number 186
1125     P p423 Number 213
1126     O o423 location p422 p423
1127     O o424 str_open p422 p423
1128     P p424 String TermOp
1129     O o425 string p424
1130     T t425 o425
1131     B b425 t425
1132     T t426 o b425 b4
1133     B b426 t426
1134     T t427 o b406 b426
1135     B b427 t427
1136     T t428 o b406 b427
1137     B b428 t428
1138     T t429 o424 b428
1139     B b429 t429
1140     T t430 o390 b429
1141     B b430 t430
1142     T t431 o423 b430
1143     B b431 t431
1144     P p431 Number 214
1145     P p432 Number 243
1146     O o432 location p431 p432
1147     O o433 str_open p431 p432
1148     P p433 String TermAddr
1149     O o434 string p433
1150     T t434 o434
1151     B b434 t434
1152     T t435 o b434 b4
1153     B b435 t435
1154     T t436 o b406 b435
1155     B b436 t436
1156     T t437 o b406 b436
1157     B b437 t437
1158     T t438 o433 b437
1159     B b438 t438
1160     T t439 o390 b438
1161     B b439 t439
1162     T t440 o432 b439
1163     B b440 t440
1164     P p440 Number 244
1165     P p441 Number 272
1166     O o441 location p440 p441
1167     O o442 str_open p440 p441
1168     P p442 String TermMan
1169     O o443 string p442
1170     T t443 o443
1171     B b443 t443
1172     T t444 o b443 b4
1173     B b444 t444
1174     T t445 o b406 b444
1175     B b445 t445
1176     T t446 o b406 b445
1177     B b446 t446
1178     T t447 o442 b446
1179     B b447 t447
1180     T t448 o390 b447
1181     B b448 t448
1182     T t449 o441 b448
1183     B b449 t449
1184     P p449 Number 273
1185     P p450 Number 303
1186     O o450 location p449 p450
1187     O o451 str_open p449 p450
1188     P p451 String TermSubst
1189     O o452 string p451
1190     T t452 o452
1191     B b452 t452
1192     T t453 o b452 b4
1193     B b453 t453
1194     T t454 o b406 b453
1195     B b454 t454
1196     T t455 o b406 b454
1197     B b455 t455
1198     T t456 o451 b455
1199     B b456 t456
1200     T t457 o390 b456
1201     B b457 t457
1202     T t458 o450 b457
1203     B b458 t458
1204     P p458 Number 304
1205     P p459 Number 331
1206     O o459 location p458 p459
1207     O o460 str_open p458 p459
1208     P p460 String Refine
1209     O o461 string p460
1210     T t461 o461
1211     B b461 t461
1212     T t462 o b461 b4
1213     B b462 t462
1214     T t463 o b406 b462
1215     B b463 t463
1216     T t464 o b406 b463
1217     B b464 t464
1218     T t465 o460 b464
1219     B b465 t465
1220     T t466 o390 b465
1221     B b466 t466
1222     T t467 o459 b466
1223     B b467 t467
1224     P p467 Number 332
1225     P p468 Number 364
1226     O o468 location p467 p468
1227     O o469 str_open p467 p468
1228     P p469 String RefineError
1229     O o470 string p469
1230     T t470 o470
1231     B b470 t470
1232     T t471 o b470 b4
1233     B b471 t471
1234     T t472 o b406 b471
1235     B b472 t472
1236     T t473 o b406 b472
1237     B b473 t473
1238     T t474 o469 b473
1239     B b474 t474
1240     T t475 o390 b474
1241     B b475 t475
1242     T t476 o468 b475
1243     B b476 t476
1244     P p476 Number 365
1245     P p477 Number 381
1246     O o477 location p476 p477
1247     O o478 str_open p476 p477
1248     P p478 String Mp_resource
1249     O o479 string p478
1250     T t479 o479
1251     B b479 t479
1252     T t480 o b479 b4
1253     B b480 t480
1254     T t481 o478 b480
1255     B b481 t481
1256     T t482 o390 b481
1257     B b482 t482
1258     T t483 o477 b482
1259     B b483 t483
1260     P p483 Number 382
1261     P p484 Number 399
1262     O o484 location p483 p484
1263     O o485 str_open p483 p484
1264     P p485 String Simple_print
1265     O o486 string p485
1266     T t486 o486
1267     B b486 t486
1268     T t487 o b486 b4
1269     B b487 t487
1270     T t488 o485 b487
1271     B b488 t488
1272     T t489 o390 b488
1273     B b489 t489
1274     T t490 o484 b489
1275     B b490 t490
1276     P p490 Number 401
1277     P p491 Number 417
1278     O o491 location p490 p491
1279     O o492 str_open p490 p491
1280     P p492 String Tactic_type
1281     O o493 string p492
1282     T t493 o493
1283     B b493 t493
1284     T t494 o b493 b4
1285     B b494 t494
1286     T t495 o492 b494
1287     B b495 t495
1288     T t496 o390 b495
1289     B b496 t496
1290     T t497 o491 b496
1291     B b497 t497
1292     P p497 Number 418
1293     P p498 Number 444
1294     O o498 location p497 p498
1295     O o499 str_open p497 p498
1296     P p499 String Tacticals
1297     O o500 string p499
1298     T t500 o500
1299     B b500 t500
1300     T t501 o b500 b4
1301     B b501 t501
1302     T t502 o b493 b501
1303     B b502 t502
1304     T t503 o499 b502
1305     B b503 t503
1306     T t504 o390 b503
1307     B b504 t504
1308     T t505 o498 b504
1309     B b505 t505
1310     P p505 Number 445
1311     P p506 Number 469
1312     O o506 location p505 p506
1313     O o507 str_open p505 p506
1314     P p507 String Sequent
1315     O o508 string p507
1316     T t508 o508
1317     B b508 t508
1318     T t509 o b508 b4
1319     B b509 t509
1320     T t510 o b493 b509
1321     B b510 t510
1322     T t511 o507 b510
1323     B b511 t511
1324     T t512 o390 b511
1325     B b512 t512
1326     T t513 o506 b512
1327     B b513 t513
1328     P p513 Number 470
1329     P p514 Number 500
1330     O o514 location p513 p514
1331     O o515 str_open p513 p514
1332     P p515 String Conversionals
1333     O o516 string p515
1334     T t516 o516
1335     B b516 t516
1336     T t517 o b516 b4
1337     B b517 t517
1338     T t518 o b493 b517
1339     B b518 t518
1340     T t519 o515 b518
1341     B b519 t519
1342     T t520 o390 b519
1343     B b520 t520
1344     T t521 o514 b520
1345     B b521 t521
1346     P p521 Number 501
1347     P p522 Number 511
1348     O o522 location p521 p522
1349     O o523 str_open p521 p522
1350     O o524 string p131
1351     T t524 o524
1352     B b524 t524
1353     T t525 o b524 b4
1354     B b525 t525
1355     T t526 o523 b525
1356     B b526 t526
1357     T t527 o390 b526
1358     B b527 t527
1359     T t528 o522 b527
1360     B b528 t528
1361     P p528 Number 512
1362     P p529 Number 520
1363     O o529 location p528 p529
1364     O o530 str_open p528 p529
1365     O o531 string p129
1366     T t531 o531
1367     B b531 t531
1368     T t532 o b531 b4
1369     B b532 t532
1370     T t533 o530 b532
1371     B b533 t533
1372     T t534 o390 b533
1373     B b534 t534
1374     T t535 o529 b534
1375     B b535 t535
1376     P p535 Number 522
1377     P p536 Number 539
1378     O o536 location p535 p536
1379     O o537 str_open p535 p536
1380     O o538 string p119
1381     T t538 o538
1382     B b538 t538
1383     T t539 o b538 b4
1384     B b539 t539
1385     T t540 o537 b539
1386     B b540 t540
1387     T t541 o390 b540
1388     B b541 t541
1389     T t542 o536 b541
1390     B b542 t542
1391     P p542 Number 540
1392     P p543 Number 561
1393     O o543 location p542 p543
1394     O o544 str_open p542 p543
1395     O o545 string p121
1396     T t545 o545
1397     B b545 t545
1398     T t546 o b545 b4
1399     B b546 t546
1400     T t547 o544 b546
1401     B b547 t547
1402     T t548 o390 b547
1403     B b548 t548
1404     T t549 o543 b548
1405     B b549 t549
1406     P p549 Number 563
1407     P p550 Number 574
1408     O o550 location p549 p550
1409     NSummary!opname opname opname Summary
1410     P p551 String car
1411     O o551 opname p551
1412     NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1413     NCzf_itt_group!car car car Czf_itt_group
1414     O o552 car
1415     T t552 o552
1416     B b552 t552
1417     T t553 o551 b552
1418     B b553 t553
1419     T t554 o550 b553
1420     B b554 t554
1421     P p554 Number 615
1422     P p555 Number 635
1423     O o555 location p554 p555
1424     P p556 String op
1425     O o556 opname p556
1426     NCzf_itt_group!op op op Czf_itt_group
1427     O o557 op
1428     Nvar var var NIL
1429     P p557 Var s1
1430     O o558 var p557
1431     T t558 o558
1432     B b558 t558
1433     P p558 Var s2
1434     O o559 var p558
1435     T t559 o559
1436     B b559 t559
1437     T t560 o557 b558 b559
1438     B b560 t560
1439     T t561 o556 b560
1440     B b561 t561
1441     T t562 o555 b561
1442     B b562 t562
1443     P p562 Number 636
1444     P p563 Number 646
1445     O o563 location p562 p563
1446     P p564 String id
1447     O o564 opname p564
1448     NCzf_itt_group!id id id Czf_itt_group
1449     O o565 id
1450     T t565 o565
1451     B b565 t565
1452     T t566 o564 b565
1453     B b566 t566
1454     T t567 o563 b566
1455     B b567 t567
1456     P p567 Number 647
1457     P p568 Number 662
1458     O o568 location p567 p568
1459     P p569 String inv
1460     O o569 opname p569
1461     NCzf_itt_group!inv inv inv Czf_itt_group
1462     O o570 inv
1463     P p570 Var s
1464     O o571 var p570
1465     T t571 o571
1466     B b571 t571
1467     T t572 o570 b571
1468     B b572 t572
1469     T t573 o569 b572
1470     B b573 t573
1471     T t574 o568 b573
1472     B b574 t574
1473     P p574 Number 664
1474     P p575 Number 713
1475     O o575 location p574 p575
1476     NSummary!dform dform dform Summary
1477     P p576 String car_df
1478     O o576 dform p576
1479     NSummary!except_mode_df except_mode_df except_mode_df Summary
1480     P p577 String src
1481     O o577 except_mode_df p577
1482     T t577 o577
1483     B b577 t577
1484     T t578 o b577 b4
1485     B b578 t578
1486     NSummary!df_term df_term df_term Summary
1487     O o578 df_term
1488     NPerv!string string578 string Perv
1489     P p578 String S
1490     O o579 string578 p578
1491     T t579 o579
1492     B b579 t579
1493     T t580 o b579 b4
1494     B b580 t580
1495     T t581 o578 b580
1496     B b581 t581
1497     T t582 o576 b578 b552 b581
1498     B b582 t582
1499     T t583 o575 b582
1500     B b583 t583
1501     P p583 Number 715
1502     P p584 Number 762
1503     O o584 location p583 p584
1504     P p585 String id_df
1505     O o585 dform p585
1506     P p586 String e
1507     O o586 string578 p586
1508     T t586 o586
1509     B b586 t586
1510     T t587 o b586 b4
1511     B b587 t587
1512     T t588 o578 b587
1513     B b588 t588
1514     T t589 o585 b578 b565 b588
1515     B b589 t589
1516     T t590 o584 b589
1517     B b590 t590
1518     P p590 Number 765
1519     P p591 Number 866
1520     O o591 location p590 p591
1521     P p592 String op_df
1522     O o592 dform p592
1523     NSummary!parens_df parens_df parens_df Summary
1524     O o593 parens_df
1525     T t593 o593
1526     B b593 t593
1527     T t594 o b593 b4
1528     B b594 t594
1529     T t595 o b577 b594
1530     B b595 t595
1531     Nslot slot slot NIL
1532     P p595 String le
1533     O o595 slot p595
1534     T t596 o595 b558
1535     B b596 t596
1536     P p596 String " * "
1537     O o596 string578 p596
1538     T t597 o596
1539     B b597 t597
1540     T t598 o595 b559
1541     B b598 t598
1542     T t599 o b598 b4
1543     B b599 t599
1544     T t600 o b597 b599
1545     B b600 t600
1546     T t601 o b596 b600
1547     B b601 t601
1548     T t602 o578 b601
1549     B b602 t602
1550     T t603 o592 b595 b560 b602
1551     B b603 t603
1552     T t604 o591 b603
1553     B b604 t604
1554     P p604 Number 868
1555     P p605 Number 946
1556     O o605 location p604 p605
1557     P p606 String inv_df
1558     O o606 dform p606
1559     T t606 o595 b571
1560     B b606 t606
1561     P p607 String '
1562     O o607 string578 p607
1563     T t607 o607
1564     B b607 t607
1565     T t608 o b607 b4
1566     B b608 t608
1567     T t609 o b606 b608
1568     B b609 t609
1569     T t610 o578 b609
1570     B b610 t610
1571     T t611 o606 b595 b572 b610
1572     B b611 t611
1573     T t612 o605 b611
1574     B b612 t612
1575     P p612 Number 961
1576     P p613 Number 1037
1577     O o613 location p612 p613
1578     NSummary!rule rule rule Summary
1579     P p614 String car_wf
1580     O o614 rule p614
1581     NSummary!context_param context_param context_param Summary
1582     P p615 String H
1583     O o615 context_param p615
1584     T t615 o615
1585     B b615 t615
1586     T t616 o b615 b4
1587     B b616 t616
1588     NSummary!meta_theorem meta_theorem meta_theorem Summary
1589     O o616 meta_theorem
1590     P p616 Var ext
1591     O o617 var p616
1592     T t617 o617
1593     B b617 t617
1594     T t618 o b617 b4
1595     C h H
1596     NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1597     NCzf_itt_set!isset isset isset Czf_itt_set
1598     O o618 isset
1599     T t619 o618 b552
1600     S s t618 h
1601     G s t619
1602     B b619 s
1603     T t620 o616 b619
1604     B b620 t620
1605     NSummary!incomplete incomplete incomplete Summary
1606     O o620 incomplete
1607     T t621 o620
1608     B b621 t621
1609     NSummary!resource_defs resource_defs resource_defs Summary
1610     P p621 Number 983
1611     P p622 Number 990
1612     O o622 resource_defs p621 p622 p262
1613     NOcaml!uid uid uid Ocaml
1614     P p623 Number 988
1615     O o623 uid p623 p622
1616     P p624 String []
1617     O o624 uid p624
1618     T t624 o624
1619     B b624 t624
1620     T t625 o623 b624
1621     B b625 t625
1622     T t626 o b625 b4
1623     B b626 t626
1624     T t627 o622 b626
1625     B b627 t627
1626     T t628 o b627 b4
1627     B b628 t628
1628     T t629 o614 b616 b620 b621 b628
1629     B b629 t629
1630     T t630 o613 b629
1631     B b630 t630
1632     P p630 Number 1039
1633     P p631 Number 1214
1634     O o631 location p630 p631
1635     P p632 String op_wf1
1636     O o632 rule p632
1637     NSummary!meta_implies meta_implies meta_implies Summary
1638     O o633 meta_implies
1639     NBase_trivial Base_trivial Base_trivial NIL
1640     NBase_trivial!squash squash squash Base_trivial
1641     O o634 squash
1642     T t634 o634
1643     B b634 t634
1644     T t635 o b634 b4
1645     T t636 o618 b558
1646     S s636 t635 h
1647     G s636 t636
1648     B b636 s636
1649     T t637 o616 b636
1650     B b637 t637
1651     T t638 o618 b559
1652     S s638 t635 h
1653     G s638 t638
1654     B b638 s638
1655     T t639 o616 b638
1656     B b639 t639
1657     T t640 o618 b560
1658     S s640 t618 h
1659     G s640 t640
1660     B b640 s640
1661     T t641 o616 b640
1662     B b641 t641
1663     T t642 o633 b639 b641
1664     B b642 t642
1665     T t643 o633 b637 b642
1666     B b643 t643
1667     P p643 Number 1061
1668     P p644 Number 1068
1669     O o644 resource_defs p643 p644 p262
1670     P p645 Number 1066
1671     O o645 uid p645 p644
1672     T t645 o645 b624
1673     B b645 t645
1674     T t646 o b645 b4
1675     B b646 t646
1676     T t647 o644 b646
1677     B b647 t647
1678     T t648 o b647 b4
1679     B b648 t648
1680     T t649 o632 b616 b643 b621 b648
1681     B b649 t649
1682     T t650 o631 b649
1683     B b650 t650
1684     P p650 Number 1216
1685     P p651 Number 1486
1686     O o651 location p650 p651
1687     P p652 String op_wf2
1688     O o652 rule p652
1689     NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1690     NCzf_itt_member!mem mem mem Czf_itt_member
1691     O o653 mem
1692     T t653 o653 b558 b552
1693     S s653 t618 h
1694     G s653 t653
1695     B b653 s653
1696     T t654 o616 b653
1697     B b654 t654
1698     T t655 o653 b559 b552
1699     S s655 t618 h
1700     G s655 t655
1701     B b655 s655
1702     T t656 o616 b655
1703     B b656 t656
1704     T t657 o653 b560 b552
1705     S s657 t618 h
1706     G s657 t657
1707     B b657 s657
1708     T t658 o616 b657
1709     B b658 t658
1710     T t659 o633 b656 b658
1711     B b659 t659
1712     T t660 o633 b654 b659
1713     B b660 t660
1714     T t661 o633 b639 b660
1715     B b661 t661
1716     T t662 o633 b637 b661
1717     B b662 t662
1718     P p662 Number 1238
1719     P p663 Number 1245
1720     O o663 resource_defs p662 p663 p262
1721     P p664 Number 1243
1722     O o664 uid p664 p663
1723     T t664 o664 b624
1724     B b664 t664
1725     T t665 o b664 b4
1726     B b665 t665
1727     T t666 o663 b665
1728     B b666 t666
1729     T t667 o b666 b4
1730     B b667 t667
1731     T t668 o652 b616 b662 b621 b667
1732     B b668 t668
1733     T t669 o651 b668
1734     B b669 t669
1735     P p669 Number 1488
1736     P p670 Number 1766
1737     O o670 location p669 p670
1738     P p671 String op_eq1
1739     O o671 rule p671
1740     P p672 Var s3
1741     O o672 var p672
1742     T t672 o672
1743     B b672 t672
1744     T t673 o618 b672
1745     S s673 t635 h
1746     G s673 t673
1747     B b673 s673
1748     T t674 o616 b673
1749     B b674 t674
1750     NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1751     NCzf_itt_eq!eq eq eq Czf_itt_eq
1752     O o674 eq
1753     T t675 o674 b558 b559
1754     S s675 t618 h
1755     G s675 t675
1756     B b675 s675
1757     T t676 o616 b675
1758     B b676 t676
1759     T t677 o557 b672 b558
1760     B b677 t677
1761     T t678 o557 b672 b559
1762     B b678 t678
1763     T t679 o674 b677 b678
1764     S s679 t618 h
1765     G s679 t679
1766     B b679 s679
1767     T t680 o616 b679
1768     B b680 t680
1769     T t681 o633 b676 b680
1770     B b681 t681
1771     T t682 o633 b674 b681
1772     B b682 t682
1773     T t683 o633 b639 b682
1774     B b683 t683
1775     T t684 o633 b637 b683
1776     B b684 t684
1777     P p684 Number 1510
1778     P p685 Number 1517
1779     O o685 resource_defs p684 p685 p262
1780     P p686 Number 1515
1781     O o686 uid p686 p685
1782     T t686 o686 b624
1783     B b686 t686
1784     T t687 o b686 b4
1785     B b687 t687
1786     T t688 o685 b687
1787     B b688 t688
1788     T t689 o b688 b4
1789     B b689 t689
1790     T t690 o671 b616 b684 b621 b689
1791     B b690 t690
1792     T t691 o670 b690
1793     B b691 t691
1794     P p691 Number 1768
1795     P p692 Number 2046
1796     O o692 location p691 p692
1797     P p693 String op_eq2
1798     O o693 rule p693
1799     T t693 o557 b558 b672
1800     B b693 t693
1801     T t694 o557 b559 b672
1802     B b694 t694
1803     T t695 o674 b693 b694
1804     S s695 t618 h
1805     G s695 t695
1806     B b695 s695
1807     T t696 o616 b695
1808     B b696 t696
1809     T t697 o633 b676 b696
1810     B b697 t697
1811     T t698 o633 b674 b697
1812     B b698 t698
1813     T t699 o633 b639 b698
1814     B b699 t699
1815     T t700 o633 b637 b699
1816     B b700 t700
1817     P p700 Number 1790
1818     P p701 Number 1797
1819     O o701 resource_defs p700 p701 p262
1820     P p702 Number 1795
1821     O o702 uid p702 p701
1822     T t702 o702 b624
1823     B b702 t702
1824     T t703 o b702 b4
1825     B b703 t703
1826     T t704 o701 b703
1827     B b704 t704
1828     T t705 o b704 b4
1829     B b705 t705
1830     T t706 o693 b616 b700 b621 b705
1831     B b706 t706
1832     T t707 o692 b706
1833     B b707 t707
1834     P p707 Number 2048
1835     P p708 Number 2181
1836     O o708 location p707 p708
1837     P p709 String op_fun1
1838     O o709 rule p709
1839     T t709 o618 b571
1840     S s709 t635 h
1841     G s709 t709
1842     B b709 s709
1843     T t710 o616 b709
1844     B b710 t710
1845     NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1846     O o710 fun_set
1847     P p710 Var z
1848     O o711 var p710
1849     T t711 o711
1850     B b711 t711
1851     T t712 o557 b711 b571
1852     B b712 t712 z
1853     T t713 o710 b712
1854     S s713 t618 h
1855     G s713 t713
1856     B b713 s713
1857     T t714 o616 b713
1858     B b714 t714
1859     T t715 o633 b710 b714
1860     B b715 t715
1861     P p715 Number 2071
1862     P p716 Number 2078
1863     O o716 resource_defs p715 p716 p262
1864     P p717 Number 2076
1865     O o717 uid p717 p716
1866     T t717 o717 b624
1867     B b717 t717
1868     T t718 o b717 b4
1869     B b718 t718
1870     T t719 o716 b718
1871     B b719 t719
1872     T t720 o b719 b4
1873     B b720 t720
1874     T t721 o709 b616 b715 b621 b720
1875     B b721 t721
1876     T t722 o708 b721
1877     B b722 t722
1878     P p722 Number 2183
1879     P p723 Number 2316
1880     O o723 location p722 p723
1881     P p724 String op_fun2
1882     O o724 rule p724
1883     T t724 o557 b571 b711
1884     B b724 t724 z
1885     T t725 o710 b724
1886     S s725 t618 h
1887     G s725 t725
1888     B b725 s725
1889     T t726 o616 b725
1890     B b726 t726
1891     T t727 o633 b710 b726
1892     B b727 t727
1893     P p727 Number 2206
1894     P p728 Number 2213
1895     O o728 resource_defs p727 p728 p262
1896     P p729 Number 2211
1897     O o729 uid p729 p728
1898     T t729 o729 b624
1899     B b729 t729
1900     T t730 o b729 b4
1901     B b730 t730
1902     T t731 o728 b730
1903     B b731 t731
1904     T t732 o b731 b4
1905     B b732 t732
1906     T t733 o724 b616 b727 b621 b732
1907     B b733 t733
1908     T t734 o723 b733
1909     B b734 t734
1910     P p734 Number 2506
1911     P p735 Number 2899
1912     O o735 location p734 p735
1913     P p736 String op_assoc1
1914     O o736 rule p736
1915     T t736 o653 b672 b552
1916     S s736 t618 h
1917     G s736 t736
1918     B b736 s736
1919     T t737 o616 b736
1920     B b737 t737
1921     NCzf_itt_eq!equal equal equal Czf_itt_eq
1922     O o737 equal
1923     T t738 o557 b560 b672
1924     B b738 t738
1925     T t739 o557 b558 b694
1926     B b739 t739
1927     T t740 o737 b738 b739
1928     S s740 t618 h
1929     G s740 t740
1930     B b740 s740
1931     T t741 o616 b740
1932     B b741 t741
1933     T t742 o633 b737 b741
1934     B b742 t742
1935     T t743 o633 b656 b742
1936     B b743 t743
1937     T t744 o633 b654 b743
1938     B b744 t744
1939     T t745 o633 b674 b744
1940     B b745 t745
1941     T t746 o633 b639 b745
1942     B b746 t746
1943     T t747 o633 b637 b746
1944     B b747 t747
1945     P p747 Number 2531
1946     P p748 Number 2538
1947     O o748 resource_defs p747 p748 p262
1948     P p749 Number 2536
1949     O o749 uid p749 p748
1950     T t749 o749 b624
1951     B b749 t749
1952     T t750 o b749 b4
1953     B b750 t750
1954     T t751 o748 b750
1955     B b751 t751
1956     T t752 o b751 b4
1957     B b752 t752
1958     T t753 o736 b616 b747 b621 b752
1959     B b753 t753
1960     T t754 o735 b753
1961     B b754 t754
1962     P p754 Number 2972
1963     P p755 Number 3365
1964     O o755 location p754 p755
1965     P p756 String op_assoc2
1966     O o756 rule p756
1967     T t756 o737 b739 b738
1968     S s756 t618 h
1969     G s756 t756
1970     B b756 s756
1971     T t757 o616 b756
1972     B b757 t757
1973     T t758 o633 b737 b757
1974     B b758 t758
1975     T t759 o633 b656 b758
1976     B b759 t759
1977     T t760 o633 b654 b759
1978     B b760 t760
1979     T t761 o633 b674 b760
1980     B b761 t761
1981     T t762 o633 b639 b761
1982     B b762 t762
1983     T t763 o633 b637 b762
1984     B b763 t763
1985     P p763 Number 2997
1986     P p764 Number 3004
1987     O o764 resource_defs p763 p764 p262
1988     P p765 Number 3002
1989     O o765 uid p765 p764
1990     T t765 o765 b624
1991     B b765 t765
1992     T t766 o b765 b4
1993     B b766 t766
1994     T t767 o764 b766
1995     B b767 t767
1996     T t768 o b767 b4
1997     B b768 t768
1998     T t769 o756 b616 b763 b621 b768
1999     B b769 t769
2000     T t770 o755 b769
2001     B b770 t770
2002     P p770 Number 3438
2003     P p771 Number 3514
2004     O o771 location p770 p771
2005     P p772 String id_wf1
2006     O o772 rule p772
2007     T t772 o618 b565
2008     S s772 t618 h
2009     G s772 t772
2010     B b772 s772
2011     T t773 o616 b772
2012     B b773 t773
2013     P p773 Number 3460
2014     P p774 Number 3468
2015     O o774 resource_defs p773 p774 p262
2016     P p775 Number 3466
2017     O o775 uid p775 p774
2018     T t775 o775 b624
2019     B b775 t775
2020     T t776 o b775 b4
2021     B b776 t776
2022     T t777 o774 b776
2023     B b777 t777
2024     T t778 o b777 b4
2025     B b778 t778
2026     T t779 o772 b616 b773 b621 b778
2027     B b779 t779
2028     T t780 o771 b779
2029     B b780 t780
2030     P p780 Number 3517
2031     P p781 Number 3595
2032     O o781 location p780 p781
2033     P p782 String id_wf2
2034     O o782 rule p782
2035     T t782 o653 b565 b552
2036     S s782 t618 h
2037     G s782 t782
2038     B b782 s782
2039     T t783 o616 b782
2040     B b783 t783
2041     P p783 Number 3539
2042     P p784 Number 3546
2043     O o784 resource_defs p783 p784 p262
2044     P p785 Number 3544
2045     O o785 uid p785 p784
2046     T t785 o785 b624
2047     B b785 t785
2048     T t786 o b785 b4
2049     B b786 t786
2050     T t787 o784 b786
2051     B b787 t787
2052     T t788 o b787 b4
2053     B b788 t788
2054     T t789 o782 b616 b783 b621 b788
2055     B b789 t789
2056     T t790 o781 b789
2057     B b790 t790
2058     P p790 Number 3683
2059     P p791 Number 3859
2060     O o791 location p790 p791
2061     P p792 String id_eq1
2062     O o792 rule p792
2063     T t792 o653 b571 b552
2064     S s792 t618 h
2065     G s792 t792
2066     B b792 s792
2067     T t793 o616 b792
2068     B b793 t793
2069     T t794 o557 b565 b571
2070     B b794 t794
2071     T t795 o737 b794 b571
2072     S s795 t618 h
2073     G s795 t795
2074     B b795 s795
2075     T t796 o616 b795
2076     B b796 t796
2077     T t797 o633 b793 b796
2078     B b797 t797
2079     T t798 o633 b710 b797
2080     B b798 t798
2081     P p798 Number 3705
2082     P p799 Number 3712
2083     O o799 resource_defs p798 p799 p262
2084     P p800 Number 3710
2085     O o800 uid p800 p799
2086     T t800 o800 b624
2087     B b800 t800
2088     T t801 o b800 b4
2089     B b801 t801
2090     T t802 o799 b801
2091     B b802 t802
2092     T t803 o b802 b4
2093     B b803 t803
2094     T t804 o792 b616 b798 b621 b803
2095     B b804 t804
2096     T t805 o791 b804
2097     B b805 t805
2098     P p805 Number 3861
2099     O o805 location p805 p304
2100     P p806 String id_eq2
2101     O o806 rule p806
2102     T t806 o557 b571 b565
2103     B b806 t806
2104     T t807 o737 b806 b571
2105     S s807 t618 h
2106     G s807 t807
2107     B b807 s807
2108     T t808 o616 b807
2109     B b808 t808
2110     T t809 o633 b793 b808
2111     B b809 t809
2112     T t810 o633 b710 b809
2113     B b810 t810
2114     P p810 Number 3883
2115     P p811 Number 3890
2116     O o811 resource_defs p810 p811 p262
2117     P p812 Number 3888
2118     O o812 uid p812 p811
2119     T t812 o812 b624
2120     B b812 t812
2121     T t813 o b812 b4
2122     B b813 t813
2123     T t814 o811 b813
2124     B b814 t814
2125     T t815 o b814 b4
2126     B b815 t815
2127     T t816 o806 b616 b810 b621 b815
2128     B b816 t816
2129     T t817 o805 b816
2130     B b817 t817
2131     P p817 Number 4039
2132     P p818 Number 4096
2133     O o818 location p817 p818
2134     NOcaml!str_let str_let str_let Ocaml
2135     O o819 str_let p817 p818
2136     NOcaml!patt_var patt_var patt_var Ocaml
2137     O o820 patt_var p302 p818
2138     NOcaml!patt_done patt_done patt_done Ocaml
2139     O o821 patt_done p817 p818
2140     T t821 o821
2141     B b821 t821 id_elim2T
2142     T t822 o820 b821
2143     B b822 t822
2144     NOcaml!fun fun fun Ocaml
2145     O o822 fun p302 p818
2146     NOcaml!patt_if patt_if patt_if Ocaml
2147     O o823 patt_if p302 p818
2148     P p823 Number 4053
2149     P p824 Number 4054
2150     O o824 patt_var p823 p824
2151     NOcaml!patt_body patt_body patt_body Ocaml
2152     O o825 patt_body p302 p818
2153     NOcaml!apply apply apply Ocaml
2154     P p825 Number 4060
2155     O o826 apply p825 p818
2156     P p826 Number 4094
2157     O o827 apply p825 p826
2158     NOcaml!lid lid lid Ocaml
2159     P p827 Number 4066
2160     O o828 lid p825 p827
2161     O o829 lid p792
2162     T t829 o829
2163     B b829 t829
2164     T t830 o828 b829
2165     B b830 t830
2166     P p830 Number 4068
2167     P p831 Number 4093
2168     O o831 apply p830 p831
2169     NOcaml!proj proj proj Ocaml
2170     P p832 Number 4091
2171     O o832 proj p830 p832
2172     O o833 uid p830 p832
2173     O o834 uid p507
2174     T t834 o834
2175     B b834 t834
2176     T t835 o833 b834
2177     B b835 t835
2178     P p835 Number 4077
2179     O o835 lid p835 p832
2180     P p836 String hyp_count_addr
2181     O o836 lid p836
2182     T t836 o836
2183     B b836 t836
2184     T t837 o835 b836
2185     B b837 t837
2186     T t838 o832 b835 b837
2187     B b838 t838
2188     P p838 Number 4092
2189     O o838 lid p838 p831
2190     P p839 Var p
2191     O o839 var p839
2192     T t839 o839
2193     B b839 t839
2194     T t840 o838 b839
2195     B b840 t840
2196     T t841 o831 b838 b840
2197     B b841 t841
2198     T t842 o827 b830 b841
2199     B b842 t842
2200     P p842 Number 4095
2201     O o842 lid p842 p818
2202     T t843 o842 b839
2203     B b843 t843
2204     T t844 o826 b842 b843
2205     B b844 t844
2206     T t845 o825 b844
2207     B b845 t845 p
2208     T t846 o824 b845
2209     B b846 t846
2210     T t847 o823 b846
2211     B b847 t847
2212     T t848 o822 b847
2213     B b848 t848
2214     T t849 o819 b822 b848
2215     B b849 t849
2216     T t850 o b849 b4
2217     B b850 t850
2218     T t851 o819 b850
2219     B b851 t851
2220     T t852 o390 b851
2221     B b852 t852
2222     T t853 o818 b852
2223     B b853 t853
2224     P p853 Number 4098
2225     P p854 Number 4271
2226     O o854 location p853 p854
2227     P p855 String inv_wf1
2228     O o855 rule p855
2229     T t855 o570 b558
2230     B b855 t855
2231     T t856 o618 b855
2232     S s856 t618 h
2233     G s856 t856
2234     B b856 s856
2235     T t857 o616 b856
2236     B b857 t857
2237     T t858 o633 b654 b857
2238     B b858 t858
2239     T t859 o633 b637 b858
2240     B b859 t859
2241     P p859 Number 4121
2242     P p860 Number 4128
2243     O o860 resource_defs p859 p860 p262
2244     P p861 Number 4126
2245     O o861 uid p861 p860
2246     T t861 o861 b624
2247     B b861 t861
2248     T t862 o b861 b4
2249     B b862 t862
2250     T t863 o860 b862
2251     B b863 t863
2252     T t864 o b863 b4
2253     B b864 t864
2254     T t865 o855 b616 b859 b621 b864
2255     B b865 t865
2256     T t866 o854 b865
2257     B b866 t866
2258     P p866 Number 4273
2259     P p867 Number 4449
2260     O o867 location p866 p867
2261     P p868 String inv_wf2
2262     O o868 rule p868
2263     T t868 o653 b855 b552
2264     S s868 t618 h
2265     G s868 t868
2266     B b868 s868
2267     T t869 o616 b868
2268     B b869 t869
2269     T t870 o633 b654 b869
2270     B b870 t870
2271     T t871 o633 b637 b870
2272     B b871 t871
2273     P p871 Number 4296
2274     P p872 Number 4303
2275     O o872 resource_defs p871 p872 p262
2276     P p873 Number 4301
2277     O o873 uid p873 p872
2278     T t873 o873 b624
2279     B b873 t873
2280     T t874 o b873 b4
2281     B b874 t874
2282     T t875 o872 b874
2283     B b875 t875
2284     T t876 o b875 b4
2285     B b876 t876
2286     T t877 o868 b616 b871 b621 b876
2287     B b877 t877
2288     T t878 o867 b877
2289     B b878 t878
2290     P p878 Number 4451
2291     P p879 Number 4637
2292     O o879 location p878 p879
2293     P p880 String inv_id1
2294     O o880 rule p880
2295     T t880 o557 b855 b558
2296     B b880 t880
2297     T t881 o737 b880 b565
2298     S s881 t618 h
2299     G s881 t881
2300     B b881 s881
2301     T t882 o616 b881
2302     B b882 t882
2303     T t883 o633 b654 b882
2304     B b883 t883
2305     T t884 o633 b637 b883
2306     B b884 t884
2307     P p884 Number 4474
2308     P p885 Number 4481
2309     O o885 resource_defs p884 p885 p262
2310     P p886 Number 4479
2311     O o886 uid p886 p885
2312     T t886 o886 b624
2313     B b886 t886
2314     T t887 o b886 b4
2315     B b887 t887
2316     T t888 o885 b887
2317     B b888 t888
2318     T t889 o b888 b4
2319     B b889 t889
2320     T t890 o880 b616 b884 b621 b889
2321     B b890 t890
2322     T t891 o879 b890
2323     B b891 t891
2324     P p891 Number 4639
2325     P p892 Number 4825
2326     O o892 location p891 p892
2327     P p893 String inv_id2
2328     O o893 rule p893
2329     T t893 o557 b558 b855
2330     B b893 t893
2331     T t894 o737 b893 b565
2332     S s894 t618 h
2333     G s894 t894
2334     B b894 s894
2335     T t895 o616 b894
2336     B b895 t895
2337     T t896 o633 b654 b895
2338     B b896 t896
2339     T t897 o633 b637 b896
2340     B b897 t897
2341     P p897 Number 4662
2342     P p898 Number 4669
2343     O o898 resource_defs p897 p898 p262
2344     P p899 Number 4667
2345     O o899 uid p899 p898
2346     T t899 o899 b624
2347     B b899 t899
2348     T t900 o b899 b4
2349     B b900 t900
2350     T t901 o898 b900
2351     B b901 t901
2352     T t902 o b901 b4
2353     B b902 t902
2354     T t903 o893 b616 b897 b621 b902
2355     B b903 t903
2356     T t904 o892 b903
2357     B b904 t904
2358     P p904 Number 4885
2359     P p905 Number 5314
2360     O o905 location p904 p905
2361     P p906 String cancelLeft
2362     O o906 rule p906
2363     NSummary!term_param term_param term_param Summary
2364     O o907 term_param
2365     T t907 o907 b558
2366     B b907 t907
2367     T t908 o b907 b4
2368     B b908 t908
2369     T t909 o b615 b908
2370     B b909 t909
2371     T t910 o737 b560 b693
2372     S s910 t618 h
2373     G s910 t910
2374     B b910 s910
2375     T t911 o616 b910
2376     B b911 t911
2377     T t912 o737 b559 b672
2378     S s912 t618 h
2379     G s912 t912
2380     B b912 s912
2381     T t913 o616 b912
2382     B b913 t913
2383     T t914 o633 b911 b913
2384     B b914 t914
2385     T t915 o633 b737 b914
2386     B b915 t915
2387     T t916 o633 b656 b915
2388     B b916 t916
2389     T t917 o633 b654 b916
2390     B b917 t917
2391     T t918 o633 b674 b917
2392     B b918 t918
2393     T t919 o633 b639 b918
2394     B b919 t919
2395     T t920 o633 b637 b919
2396     B b920 t920
2397     NSummary!interactive interactive interactive Summary
2398     O o920 interactive
2399     NSummary!ext_rule ext_rule ext_rule Summary
2400     P p920 String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2401     O o921 ext_rule p920
2402     NSummary!status_incomplete status_incomplete status_incomplete Summary
2403     O o922 status_incomplete
2404     T t922 o922
2405     B b922 t922
2406     NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2407     O o923 ext_unjustified
2408     NSummary!tactic_arg tactic_arg tactic_arg Summary
2409     P p923 String main
2410     O o924 tactic_arg p923
2411     NSummary!msequent msequent msequent Summary
2412     O o925 msequent
2413     T t925 o b910 b4
2414     B b925 t925
2415     T t926 o b736 b925
2416     B b926 t926
2417     T t927 o b655 b926
2418     B b927 t927
2419     T t928 o b653 b927
2420     B b928 t928
2421     T t929 o b673 b928
2422     B b929 t929
2423     T t930 o b638 b929
2424     B b930 t930
2425     T t931 o b636 b930
2426     B b931 t931
2427     T t932 o925 b912 b931
2428     B b932 t932
2429     NSummary!parent_none parent_none parent_none Summary
2430     O o932 parent_none
2431     T t933 o932
2432     B b933 t933
2433     T t934 o924 b932 b4 b933
2434     B b934 t934
2435     P p934 String assertion
2436     O o934 tactic_arg p934
2437     H h934 v t910
2438     T t935 o557 b855 b560
2439     B b935 t935
2440     T t936 o557 b855 b693
2441     B b936 t936
2442     T t937 o737 b935 b936
2443     S s937 t618 h h934
2444     G s937 t937
2445     B b937 s937
2446     T t938 o925 b937 b931
2447     B b938 t938
2448     S s938 t618 h h934
2449     G s938 t912
2450     B b939 s938
2451     T t939 o925 b939 b931
2452     B b940 t939
2453     T t940 o2 b934
2454     B b941 t940
2455     T t941 o924 b940 b4 b941
2456     B b942 t941
2457     T t942 o2 b942
2458     B b943 t942
2459     T t943 o934 b938 b4 b943
2460     B b944 t943
2461     H h944 v_1 t937
2462     S s944 t618 h h934 h944
2463     G s944 t912
2464     B b945 s944
2465     T t945 o925 b945 b931
2466     B b946 t945
2467     T t946 o924 b946 b4 b943
2468     B b947 t946
2469     T t947 o b947 b4
2470     B b948 t947
2471     T t948 o b944 b948
2472     B b949 t948
2473     T t949 o923 b934 b949
2474     B b950 t949
2475     P p950 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2476     O o950 ext_rule p950
2477     T t950 o923 b944 b4
2478     B b951 t950
2479     T t951 o950 b922 b951 b4 b4
2480     B b952 t951
2481     P p952 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2482     O o952 ext_rule p952
2483     P p953 String eq
2484     O o953 tactic_arg p953
2485     T t953 o557 b880 b559
2486     B b953 t953
2487     T t954 o737 b935 b953
2488     S s954 t618 h h934 h944
2489     G s954 t954
2490     B b954 s954
2491     T t955 o925 b954 b931
2492     B b955 t955
2493     T t956 o2 b947
2494     B b956 t956
2495     T t957 o953 b955 b4 b956
2496     B b957 t957
2497     T t958 o737 b953 b936
2498     H h958 v_2 t958
2499     S s958 t618 h h934 h944 h958
2500     G s958 t912
2501     B b958 s958
2502     T t959 o925 b958 b931
2503     B b959 t959
2504     T t960 o924 b959 b4 b956
2505     B b960 t960
2506     P p960 String wf
2507     O o960 tactic_arg p960
2508     B b961 t936 v_2
2509     T t961 o710 b961
2510     S s961 t618 h h934 h944
2511     G s961 t961
2512     B b962 s961
2513     T t962 o925 b962 b931
2514     B b963 t962
2515     NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2516     O o963 fun_prop
2517     P p963 Var v_2
2518     O o964 var p963
2519     T t964 o964
2520     B b964 t964
2521     T t965 o737 b964 b936
2522     B b965 t965 v_2
2523     T t966 o963 b965
2524     S s966 t618 h h934 h944
2525     G s966 t966
2526     B b966 s966
2527     T t967 o925 b966 b931
2528     B b967 t967
2529     NSummary!arg_named arg_named arg_named Summary
2530     P p967 String d_auto
2531     O o967 arg_named p967
2532     NSummary!arg_bool arg_bool arg_bool Summary
2533     P p968 String true
2534     O o968 arg_bool p968
2535     T t968 o968
2536     B b968 t968
2537     T t969 o967 b968
2538     B b969 t969
2539     T t970 o b969 b4
2540     B b970 t970
2541     T t971 o960 b967 b970 b956
2542     B b971 t971
2543     T t972 o2 b971
2544     B b972 t972
2545     T t973 o960 b963 b4 b972
2546     B b973 t973
2547     T t974 o b973 b4
2548     B b974 t974
2549     T t975 o b960 b974
2550     B b975 t975
2551     T t976 o b957 b975
2552     B b976 t976
2553     T t977 o923 b947 b976
2554     B b977 t977
2555     P p977 String autoT
2556     O o977 ext_rule p977
2557     T t978 o923 b957 b4
2558     B b978 t978
2559     T t979 o977 b922 b978 b4 b4
2560     B b979 t979
2561     P p979 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2562     O o979 ext_rule p979
2563     T t980 o557 b880 b672
2564     B b980 t980
2565     T t981 o737 b936 b980
2566     S s981 t618 h h934 h944 h958
2567     G s981 t981
2568     B b981 s981
2569     T t982 o925 b981 b931
2570     B b982 t982
2571     T t983 o2 b960
2572     B b983 t983
2573     T t984 o953 b982 b4 b983
2574     B b984 t984
2575     T t985 o737 b953 b980
2576     H h985 v_3 t985
2577     S s985 t618 h h934 h944 h958 h985
2578     G s985 t912
2579     B b985 s985
2580     T t986 o925 b985 b931
2581     B b986 t986
2582     T t987 o924 b986 b4 b983
2583     B b987 t987
2584     B b988 t953 v_3
2585     T t988 o710 b988
2586     S s988 t618 h h934 h944 h958
2587     G s988 t988
2588     B b989 s988
2589     T t989 o925 b989 b931
2590     B b990 t989
2591     P p990 Var v_3
2592     O o990 var p990
2593     T t990 o990
2594     B b991 t990
2595     T t991 o737 b953 b991
2596     B b992 t991 v_3
2597     T t992 o963 b992
2598     S s992 t618 h h934 h944 h958
2599     G s992 t992
2600     B b993 s992
2601     T t993 o925 b993 b931
2602     B b994 t993
2603     T t994 o960 b994 b970 b983
2604     B b995 t994
2605     T t995 o2 b995
2606     B b996 t995
2607     T t996 o960 b990 b4 b996
2608     B b997 t996
2609     T t997 o b997 b4
2610     B b998 t997
2611     T t998 o b987 b998
2612     B b999 t998
2613     T t999 o b984 b999
2614     B b1000 t999
2615     T t1000 o923 b960 b1000
2616     B b1001 t1000
2617     T t1001 o923 b984 b4
2618     B b1002 t1001
2619     T t1002 o977 b922 b1002 b4 b4
2620     B b1003 t1002
2621     P p1003 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2622     O o1003 ext_rule p1003
2623     T t1003 o557 b565 b559
2624     B b1004 t1003
2625     T t1004 o557 b565 b672
2626     B b1005 t1004
2627     T t1005 o737 b1004 b1005
2628     H h1005 v_4 t1005
2629     S s1005 t618 h h934 h944 h958 h985 h1005
2630     G s1005 t912
2631     B b1006 s1005
2632     T t1006 o925 b1006 b931
2633     B b1007 t1006
2634     T t1007 o2 b987
2635     B b1008 t1007
2636     T t1008 o924 b1007 b4 b1008
2637     B b1009 t1008
2638     T t1009 o b1009 b4
2639     B b1010 t1009
2640     T t1010 o923 b987 b1010
2641     B b1011 t1010
2642     P p1011 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2643     O o1011 ext_rule p1011
2644     T t1011 o737 b559 b1005
2645     H h1011 v_5 t1011
2646     S s1011 t618 h h934 h944 h958 h985 h1005 h1011
2647     G s1011 t912
2648     B b1012 s1011
2649     T t1012 o925 b1012 b931
2650     B b1013 t1012
2651     T t1013 o2 b1009
2652     B b1014 t1013
2653     T t1014 o924 b1013 b4 b1014
2654     B b1015 t1014
2655     B b1016 t1004 v_5
2656     T t1016 o710 b1016
2657     S s1016 t618 h h934 h944 h958 h985 h1005
2658     G s1016 t1016
2659     B b1017 s1016
2660     T t1017 o925 b1017 b931
2661     B b1018 t1017
2662     P p1018 Var v_5
2663     O o1018 var p1018
2664     T t1018 o1018
2665     B b1019 t1018
2666     T t1019 o737 b1019 b1005
2667     B b1020 t1019 v_5
2668     T t1020 o963 b1020
2669     S s1020 t618 h h934 h944 h958 h985 h1005
2670     G s1020 t1020
2671     B b1021 s1020
2672     T t1021 o925 b1021 b931
2673     B b1022 t1021
2674     T t1022 o960 b1022 b970 b1014
2675     B b1023 t1022
2676     T t1023 o2 b1023
2677     B b1024 t1023
2678     T t1024 o960 b1018 b4 b1024
2679     B b1025 t1024
2680     T t1025 o b1025 b4
2681     B b1026 t1025
2682     T t1026 o b1015 b1026
2683     B b1027 t1026
2684     T t1027 o923 b1009 b1027
2685     B b1028 t1027
2686     P p1028 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2687     O o1028 ext_rule p1028
2688     H h1028 v_6 t912
2689     S s1028 t618 h h934 h944 h958 h985 h1005 h1011 h1028
2690     G s1028 t912
2691     B b1029 s1028
2692     T t1029 o925 b1029 b931
2693     B b1030 t1029
2694     T t1030 o2 b1015
2695     B b1031 t1030
2696     T t1031 o924 b1030 b4 b1031
2697     B b1032 t1031
2698     T t1032 o b1032 b4
2699     B b1033 t1032
2700     T t1033 o923 b1015 b1033
2701     B b1034 t1033
2702     P p1034 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2703     O o1034 ext_rule p1034
2704     T t1034 o923 b1032 b4
2705     B b1035 t1034
2706     T t1035 o1034 b922 b1035 b4 b4
2707     B b1036 t1035
2708     T t1036 o b1036 b4
2709     B b1037 t1036
2710     T t1037 o1028 b922 b1034 b1037 b4
2711     B b1038 t1037
2712     P p1038 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2713     O o1038 ext_rule p1038
2714     T t1038 o923 b1025 b4
2715     B b1039 t1038
2716     T t1039 o1038 b922 b1039 b4 b4
2717     B b1040 t1039
2718     T t1040 o b1040 b4
2719     B b1041 t1040
2720     T t1041 o b1038 b1041
2721     B b1042 t1041
2722     T t1042 o1011 b922 b1028 b1042 b4
2723     B b1043 t1042
2724     T t1043 o b1043 b4
2725     B b1044 t1043
2726     T t1044 o1003 b922 b1011 b1044 b4
2727     B b1045 t1044
2728     T t1045 o923 b997 b4
2729     B b1046 t1045
2730     T t1046 o1038 b922 b1046 b4 b4
2731     B b1047 t1046
2732     T t1047 o b1047 b4
2733     B b1048 t1047
2734     T t1048 o b1045 b1048
2735     B b1049 t1048
2736     T t1049 o b1003 b1049
2737     B b1050 t1049
2738     T t1050 o979 b922 b1001 b1050 b4
2739     B b1051 t1050
2740     T t1051 o923 b973 b4
2741     B b1052 t1051
2742     T t1052 o1038 b922 b1052 b4 b4
2743     B b1053 t1052
2744     T t1053 o b1053 b4
2745     B b1054 t1053
2746     T t1054 o b1051 b1054
2747     B b1055 t1054
2748     T t1055 o b979 b1055
2749     B b1056 t1055
2750     T t1056 o952 b922 b977 b1056 b4
2751     B b1057 t1056
2752     T t1057 o b1057 b4
2753     B b1058 t1057
2754     T t1058 o b952 b1058
2755     B b1059 t1058
2756     T t1059 o921 b922 b950 b1059 b4
2757     B b1060 t1059
2758     T t1060 o920 b1060
2759     B b1061 t1060
2760     P p1061 Number 4911
2761     P p1062 Number 4919
2762     O o1062 resource_defs p1061 p1062 p262
2763     P p1063 Number 4917
2764     O o1063 uid p1063 p1062
2765     T t1063 o1063 b624
2766     B b1063 t1063
2767     T t1064 o b1063 b4
2768     B b1064 t1064
2769     T t1065 o1062 b1064
2770     B b1065 t1065
2771     T t1066 o b1065 b4
2772     B b1066 t1066
2773     T t1067 o906 b909 b920 b1061 b1066
2774     B b1067 t1067
2775     T t1068 o905 b1067
2776     B b1068 t1068
2777     P p1068 Number 5359
2778     P p1069 Number 5789
2779     O o1069 location p1068 p1069
2780     P p1070 String cancelRight
2781     O o1070 rule p1070
2782     T t1070 o907 b672
2783     B b1070 t1070
2784     T t1071 o b1070 b4
2785     B b1071 t1071
2786     T t1072 o b615 b1071
2787     B b1072 t1072
2788     T t1073 o737 b693 b694
2789     S s1073 t618 h
2790     G s1073 t1073
2791     B b1073 s1073
2792     T t1074 o616 b1073
2793     B b1074 t1074
2794     T t1075 o737 b558 b559
2795     S s1075 t618 h
2796     G s1075 t1075
2797     B b1075 s1075
2798     T t1076 o616 b1075
2799     B b1076 t1076
2800     T t1077 o633 b1074 b1076
2801     B b1077 t1077
2802     T t1078 o633 b737 b1077
2803     B b1078 t1078
2804     T t1079 o633 b656 b1078
2805     B b1079 t1079
2806     T t1080 o633 b654 b1079
2807     B b1080 t1080
2808     T t1081 o633 b674 b1080
2809     B b1081 t1081
2810     T t1082 o633 b639 b1081
2811     B b1082 t1082
2812     T t1083 o633 b637 b1082
2813     B b1083 t1083
2814     P p1083 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenWT autoT"
2815     O o1083 ext_rule p1083
2816     T t1084 o b1073 b4
2817     B b1084 t1084
2818     T t1085 o b736 b1084
2819     B b1085 t1085
2820     T t1086 o b655 b1085
2821     B b1086 t1086
2822     T t1087 o b653 b1086
2823     B b1087 t1087
2824     T t1088 o b673 b1087
2825     B b1088 t1088
2826     T t1089 o b638 b1088
2827     B b1089 t1089
2828     T t1090 o b636 b1089
2829     B b1090 t1090
2830     T t1091 o925 b1075 b1090
2831     B b1091 t1091
2832     T t1092 o924 b1091 b4 b933
2833     B b1092 t1092
2834     H h1092 v t1073
2835     T t1093 o570 b672
2836     B b1093 t1093
2837     T t1094 o557 b693 b1093
2838     B b1094 t1094
2839     T t1095 o557 b694 b1093
2840     B b1095 t1095
2841     T t1096 o737 b1094 b1095
2842     S s1096 t618 h h1092
2843     G s1096 t1096
2844     B b1096 s1096
2845     T t1097 o925 b1096 b1090
2846     B b1097 t1097
2847     S s1097 t618 h h1092
2848     G s1097 t1075
2849     B b1098 s1097
2850     T t1098 o925 b1098 b1090
2851     B b1099 t1098
2852     T t1099 o2 b1092
2853     B b1100 t1099
2854     T t1100 o924 b1099 b4 b1100
2855     B b1101 t1100
2856     T t1101 o2 b1101
2857     B b1102 t1101
2858     T t1102 o934 b1097 b4 b1102
2859     B b1103 t1102
2860     H h1103 v_1 t1096
2861     S s1103 t618 h h1092 h1103
2862     G s1103 t1075
2863     B b1104 s1103
2864     T t1104 o925 b1104 b1090
2865     B b1105 t1104
2866     T t1105 o924 b1105 b4 b1102
2867     B b1106 t1105
2868     T t1106 o b1106 b4
2869     B b1107 t1106
2870     T t1107 o b1103 b1107
2871     B b1108 t1107
2872     T t1108 o923 b1092 b1108
2873     B b1109 t1108
2874     T t1109 o923 b1103 b4
2875     B b1110 t1109
2876     T t1110 o950 b922 b1110 b4 b4
2877     B b1111 t1110
2878     P p1111 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
2879     O o1111 ext_rule p1111
2880     T t1111 o557 b672 b1093
2881     B b1112 t1111
2882     T t1112 o557 b558 b1112
2883     B b1113 t1112
2884     T t1113 o737 b1113 b1095
2885     H h1113 v_2 t1113
2886     S s1113 t618 h h1092 h1103 h1113
2887     G s1113 t1075
2888     B b1114 s1113
2889     T t1114 o925 b1114 b1090
2890     B b1115 t1114
2891     T t1115 o2 b1106
2892     B b1116 t1115
2893     T t1116 o924 b1115 b4 b1116
2894     B b1117 t1116
2895     B b1118 t1095 v_2
2896     T t1118 o710 b1118
2897     S s1118 t618 h h1092 h1103
2898     G s1118 t1118
2899     B b1119 s1118
2900     T t1119 o925 b1119 b1090
2901     B b1120 t1119
2902     T t1120 o737 b964 b1095
2903     B b1121 t1120 v_2
2904     T t1121 o963 b1121
2905     S s1121 t618 h h1092 h1103
2906     G s1121 t1121
2907     B b1122 s1121
2908     T t1122 o925 b1122 b1090
2909     B b1123 t1122
2910     T t1123 o960 b1123 b970 b1116
2911     B b1124 t1123
2912     T t1124 o2 b1124
2913     B b1125 t1124
2914     T t1125 o960 b1120 b4 b1125
2915     B b1126 t1125
2916     T t1126 o b1126 b4
2917     B b1127 t1126
2918     T t1127 o b1117 b1127
2919     B b1128 t1127
2920     T t1128 o923 b1106 b1128
2921     B b1129 t1128
2922     P p1129 String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
2923     O o1129 ext_rule p1129
2924     T t1129 o557 b559 b1112
2925     B b1130 t1129
2926     T t1130 o737 b1113 b1130
2927     H h1130 v_3 t1130
2928     S s1130 t618 h h1092 h1103 h1113 h1130
2929     G s1130 t1075
2930     B b1131 s1130
2931     T t1131 o925 b1131 b1090
2932     B b1132 t1131
2933     T t1132 o2 b1117
2934     B b1133 t1132
2935     T t1133 o924 b1132 b4 b1133
2936     B b1134 t1133
2937     B b1135 t1112 v_3
2938     T t1135 o710 b1135
2939     S s1135 t618 h h1092 h1103 h1113
2940     G s1135 t1135
2941     B b1136 s1135
2942     T t1136 o925 b1136 b1090
2943     B b1137 t1136
2944     T t1137 o737 b1113 b991
2945     B b1138 t1137 v_3
2946     T t1138 o963 b1138
2947     S s1138 t618 h h1092 h1103 h1113
2948     G s1138 t1138
2949     B b1139 s1138
2950     T t1139 o925 b1139 b1090
2951     B b1140 t1139
2952     T t1140 o960 b1140 b970 b1133
2953     B b1141 t1140
2954     T t1141 o2 b1141
2955     B b1142 t1141
2956     T t1142 o960 b1137 b4 b1142
2957     B b1143 t1142
2958     T t1143 o b1143 b4
2959     B b1144 t1143
2960     T t1144 o b1134 b1144
2961     B b1145 t1144
2962     T t1145 o923 b1117 b1145
2963     B b1146 t1145
2964     P p1146 String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
2965     O o1146 ext_rule p1146
2966     T t1146 o557 b558 b565
2967     B b1147 t1146
2968     T t1147 o557 b559 b565
2969     B b1148 t1147
2970     T t1148 o737 b1147 b1148
2971     H h1148 v_4 t1148
2972     S s1148 t618 h h1092 h1103 h1113 h1130 h1148
2973     G s1148 t1075
2974     B b1149 s1148
2975     T t1149 o925 b1149 b1090
2976     B b1150 t1149
2977     T t1150 o2 b1134
2978     B b1151 t1150
2979     T t1151 o924 b1150 b4 b1151
2980     B b1152 t1151
2981     T t1152 o b1152 b4
2982     B b1153 t1152
2983     T t1153 o923 b1134 b1153
2984     B b1154 t1153
2985     P p1154 String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
2986     O o1154 ext_rule p1154
2987     T t1154 o737 b558 b1148
2988     H h1154 v_5 t1154
2989     S s1154 t618 h h1092 h1103 h1113 h1130 h1148 h1154
2990     G s1154 t1075
2991     B b1155 s1154
2992     T t1155 o925 b1155 b1090
2993     B b1156 t1155
2994     T t1156 o2 b1152
2995     B b1157 t1156
2996     T t1157 o924 b1156 b4 b1157
2997     B b1158 t1157
2998     B b1159 t1147 v_5
2999     T t1159 o710 b1159
3000     S s1159 t618 h h1092 h1103 h1113 h1130 h1148
3001     G s1159 t1159
3002     B b1160 s1159
3003     T t1160 o925 b1160 b1090
3004     B b1161 t1160
3005     T t1161 o737 b1019 b1148
3006     B b1162 t1161 v_5
3007     T t1162 o963 b1162
3008     S s1162 t618 h h1092 h1103 h1113 h1130 h1148
3009     G s1162 t1162
3010     B b1163 s1162
3011     T t1163 o925 b1163 b1090
3012     B b1164 t1163
3013     T t1164 o960 b1164 b970 b1157
3014     B b1165 t1164
3015     T t1165 o2 b1165
3016     B b1166 t1165
3017     T t1166 o960 b1161 b4 b1166
3018     B b1167 t1166
3019     T t1167 o b1167 b4
3020     B b1168 t1167
3021     T t1168 o b1158 b1168
3022     B b1169 t1168
3023     T t1169 o923 b1152 b1169
3024     B b1170 t1169
3025     P p1170 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3026     O o1170 ext_rule p1170
3027     T t1170 o923 b1158 b4
3028     B b1171 t1170
3029     T t1171 o1170 b922 b1171 b4 b4
3030     B b1172 t1171
3031     P p1172 String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
3032     O o1172 ext_rule p1172
3033     T t1172 o923 b1167 b4
3034     B b1173 t1172
3035     T t1173 o1172 b922 b1173 b4 b4
3036     B b1174 t1173
3037     T t1174 o b1174 b4
3038     B b1175 t1174
3039     T t1175 o b1172 b1175
3040     B b1176 t1175
3041     T t1176 o1154 b922 b1170 b1176 b4
3042     B b1177 t1176
3043     T t1177 o b1177 b4
3044     B b1178 t1177
3045     T t1178 o1146 b922 b1154 b1178 b4
3046     B b1179 t1178
3047     T t1179 o923 b1143 b4
3048     B b1180 t1179
3049     T t1180 o1172 b922 b1180 b4 b4
3050     B b1181 t1180
3051     T t1181 o b1181 b4
3052     B b1182 t1181
3053     T t1182 o b1179 b1182
3054     B b1183 t1182
3055     T t1183 o1129 b922 b1146 b1183 b4
3056     B b1184 t1183
3057     T t1184 o923 b1126 b4
3058     B b1185 t1184
3059     T t1185 o1172 b922 b1185 b4 b4
3060     B b1186 t1185
3061     T t1186 o b1186 b4
3062     B b1187 t1186
3063     T t1187 o b1184 b1187
3064     B b1188 t1187
3065     S s1188 t618 h h1092 h1103 h1113
3066     G s1188 t675
3067     B b1189 s1188
3068     T t1189 o925 b1189 b1090
3069     B b1190 t1189
3070     T t1190 o924 b1115 b970 b1116
3071     B b1191 t1190
3072     T t1191 o2 b1191
3073     B b1192 t1191
3074     T t1192 o924 b1190 b4 b1192
3075     B b1193 t1192
3076     S s1193 t618 h h1092 h1103 h1113 h1130
3077     G s1193 t675
3078     B b1194 s1193
3079     T t1194 o925 b1194 b1090
3080     B b1195 t1194
3081     T t1195 o2 b1193
3082     B b1196 t1195
3083     T t1196 o924 b1195 b4 b1196
3084     B b1197 t1196
3085     T t1197 o960 b1140 b970 b1196
3086     B b1198 t1197
3087     T t1198 o2 b1198
3088     B b1199 t1198
3089     T t1199 o960 b1137 b4 b1199
3090     B b1200 t1199
3091     T t1200 o b1200 b4
3092     B b1201 t1200
3093     T t1201 o b1197 b1201
3094     B b1202 t1201
3095     T t1202 o923 b1193 b1202
3096     B b1203 t1202
3097     S s1203 t618 h h1092 h1103 h1113 h1130 h1148
3098     G s1203 t675
3099     B b1204 s1203
3100     T t1204 o925 b1204 b1090
3101     B b1205 t1204
3102     T t1205 o2 b1197
3103     B b1206 t1205
3104     T t1206 o924 b1205 b4 b1206
3105     B b1207 t1206
3106     T t1207 o b1207 b4
3107     B b1208 t1207
3108     T t1208 o923 b1197 b1208
3109     B b1209 t1208
3110     S s1209 t618 h h1092 h1103 h1113 h1130 h1148 h1154
3111     G s1209 t675
3112     B b1210 s1209
3113     T t1210 o925 b1210 b1090
3114     B b1211 t1210
3115     T t1211 o2 b1207
3116     B b1212 t1211
3117     T t1212 o924 b1211 b4 b1212
3118     B b1213 t1212
3119     T t1213 o960 b1164 b970 b1212
3120     B b1214 t1213
3121     T t1214 o2 b1214
3122     B b1215 t1214
3123     T t1215 o960 b1161 b4 b1215
3124     B b1216 t1215
3125     T t1216 o b1216 b4
3126     B b1217 t1216
3127     T t1217 o b1213 b1217
3128     B b1218 t1217
3129     T t1218 o923 b1207 b1218
3130     B b1219 t1218
3131     P p1219 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT thenT rwh unfold_equal 8 thenT autoT"
3132     O o1219 ext_rule p1219
3133     T t1219 o923 b1213 b4
3134     B b1220 t1219
3135     T t1220 o1219 b922 b1220 b4 b4
3136     B b1221 t1220
3137     T t1221 o923 b1216 b4
3138     B b1222 t1221
3139     T t1222 o1038 b922 b1222 b4 b4
3140     B b1223 t1222
3141     T t1223 o b1223 b4
3142     B b1224 t1223
3143     T t1224 o b1221 b1224
3144     B b1225 t1224
3145     T t1225 o1154 b922 b1219 b1225 b4
3146     B b1226 t1225
3147     T t1226 o b1226 b4
3148     B b1227 t1226
3149     T t1227 o1146 b922 b1209 b1227 b4
3150     B b1228 t1227
3151     P p1228 String "rwh unfold_fun_set 0 thenT autoT"
3152     O o1228 ext_rule p1228
3153     NCzf_itt_set!set set set Czf_itt_set
3154     O o1229 set
3155     T t1229 o1229
3156     H h1229 s1_1 t1229
3157     H h1230 s2 t1229
3158     P p1230 Var s1_1
3159     O o1230 var p1230
3160     T t1230 o1230
3161     B b1230 t1230
3162     T t1231 o737 b1230 b559
3163     H h1231 x t1231
3164     T t1232 o737 b1113 b1113
3165     S s1232 t618 h h1092 h1103 h1113 h1229 h1230 h1231
3166     G s1232 t1232
3167     B b1232 s1232
3168     T t1233 o925 b1232 b1090
3169     B b1233 t1233
3170     NItt_logic Itt_logic Itt_logic NIL
3171     NItt_logic!implies implies implies Itt_logic
3172     O o1233 implies
3173     B b1234 t1231
3174     B b1235 t1232
3175     T t1235 o1233 b1234 b1235
3176     S s1235 t618 h h1092 h1103 h1113 h1229 h1230
3177     G s1235 t1235
3178     B b1236 s1235
3179     T t1236 o925 b1236 b1090
3180     B b1237 t1236
3181     NItt_logic!all all all Itt_logic
3182     O o1237 all
3183     B b1238 t1229
3184     B b1239 t1235 s2
3185     T t1239 o1237 b1238 b1239
3186     S s1239 t618 h h1092 h1103 h1113 h1229
3187     G s1239 t1239
3188     B b1240 s1239
3189     T t1240 o925 b1240 b1090
3190     B b1241 t1240
3191     B b1242 t1239 s1_1
3192     T t1242 o1237 b1238 b1242
3193     S s1242 t618 h h1092 h1103 h1113
3194     G s1242 t1242
3195     B b1243 s1242
3196     T t1243 o925 b1243 b1090
3197     B b1244 t1243
3198     T t1244 o2 b1200
3199     B b1245 t1244
3200     T t1245 o960 b1244 b970 b1245
3201     B b1246 t1245
3202     T t1246 o2 b1246
3203     B b1247 t1246
3204     T t1247 o924 b1241 b970 b1247
3205     B b1248 t1247
3206     T t1248 o2 b1248
3207     B b1249 t1248
3208     T t1249 o924 b1237 b970 b1249
3209     B b1250 t1249
3210     T t1250 o2 b1250
3211     B b1251 t1250
3212     T t1251 o924 b1233 b4 b1251
3213     B b1252 t1251
3214     T t1252 o b1252 b4
3215     B b1253 t1252
3216     T t1253 o923 b1200 b1253
3217     B b1254 t1253
3218     NSummary!ext_goal ext_goal ext_goal Summary
3219     O o1254 ext_goal
3220     T t1254 o1254 b1252
3221     B b1255 t1254
3222     T t1255 o b1255 b4
3223     B b1256 t1255
3224     T t1256 o1228 b922 b1254 b1256 b4
3225     B b1257 t1256
3226     T t1257 o b1257 b4
3227     B b1258 t1257
3228     T t1258 o b1228 b1258
3229     B b1259 t1258
3230     T t1259 o1129 b922 b1203 b1259 b4
3231     B b1260 t1259
3232     T t1260 o b1260 b4
3233     B b1261 t1260
3234     T t1261 o1111 b922 b1129 b1188 b1261
3235     B b1262 t1261
3236     T t1262 o b1262 b4
3237     B b1263 t1262
3238     T t1263 o b1111 b1263
3239     B b1264 t1263
3240     T t1264 o1083 b922 b1109 b1264 b4
3241     B b1265 t1264
3242     T t1265 o920 b1265
3243     B b1266 t1265
3244     P p1266 Number 5386
3245     P p1267 Number 5394
3246     O o1267 resource_defs p1266 p1267 p262
3247     P p1268 Number 5392
3248     O o1268 uid p1268 p1267
3249     T t1268 o1268 b624
3250     B b1268 t1268
3251     T t1269 o b1268 b4
3252     B b1269 t1269
3253     T t1270 o1267 b1269
3254     B b1270 t1270
3255     T t1271 o b1270 b4
3256     B b1271 t1271
3257     T t1272 o1070 b1072 b1083 b1266 b1271
3258     B b1272 t1272
3259     T t1273 o1069 b1272
3260     B b1273 t1273
3261     P p1273 Number 5791
3262     P p1274 Number 5863
3263     O o1274 location p1273 p1274
3264     O o1275 str_let p1273 p1274
3265     P p1275 Number 5795
3266     O o1276 patt_var p1275 p1274
3267     O o1277 patt_done p1273 p1274
3268     T t1277 o1277
3269     B b1277 t1277 groupCancelLeftT
3270     T t1278 o1276 b1277
3271     B b1278 t1278
3272     O o1278 fun p1275 p1274
3273     O o1279 patt_if p1275 p1274
3274     P p1279 Number 5812
3275     P p1280 Number 5813
3276     O o1280 patt_var p1279 p1280
3277     O o1281 patt_body p1275 p1274
3278     P p1281 Number 5814
3279     P p1282 Number 5815
3280     O o1282 patt_var p1281 p1282
3281     P p1283 Number 5821
3282     O o1283 apply p1283 p1274
3283     P p1284 Number 5861
3284     O o1284 apply p1283 p1284
3285     P p1285 Number 5859
3286     O o1285 apply p1283 p1285
3287     P p1286 Number 5831
3288     O o1286 lid p1283 p1286
3289     O o1287 lid p906
3290     T t1287 o1287
3291     B b1287 t1287
3292     T t1288 o1286 b1287
3293     B b1288 t1288
3294     P p1288 Number 5833
3295     P p1289 Number 5858
3296     O o1289 apply p1288 p1289
3297     P p1290 Number 5856
3298     O o1290 proj p1288 p1290
3299     O o1291 uid p1288 p1290
3300     T t1291 o1291 b834
3301     B b1291 t1291
3302     P p1291 Number 5842
3303     O o1292 lid p1291 p1290
3304     T t1292 o1292 b836
3305     B b1292 t1292
3306     T t1293 o1290 b1291 b1292
3307     B b1293 t1293
3308     P p1293 Number 5857
3309     O o1293 lid p1293 p1289
3310     T t1294 o1293 b839
3311     B b1294 t1294
3312     T t1295 o1289 b1293 b1294
3313     B b1295 t1295
3314     T t1296 o1285 b1288 b1295
3315     B b1296 t1296
3316     P p1296 Number 5860
3317     O o1296 lid p1296 p1284
3318     P p1297 Var t
3319     O o1297 var p1297
3320     T t1297 o1297
3321     B b1297 t1297
3322     T t1298 o1296 b1297
3323     B b1298 t1298
3324     T t1299 o1284 b1296 b1298
3325     B b1299 t1299
3326     P p1299 Number 5862
3327     O o1299 lid p1299 p1274
3328     T t1300 o1299 b839
3329     B b1300 t1300
3330     T t1301 o1283 b1299 b1300
3331     B b1301 t1301
3332     T t1302 o1281 b1301
3333     B b1302 t1302 p
3334     T t1303 o1282 b1302
3335     B b1303 t1303
3336     T t1304 o1279 b1303
3337     B b1304 t1304
3338     T t1305 o1278 b1304
3339     B b1305 t1305
3340     T t1306 o1281 b1305
3341     B b1306 t1306 t
3342     T t1307 o1280 b1306
3343     B b1307 t1307
3344     T t1308 o1279 b1307
3345     B b1308 t1308
3346     T t1309 o1278 b1308
3347     B b1309 t1309
3348     T t1310 o1275 b1278 b1309
3349     B b1310 t1310
3350     T t1311 o b1310 b4
3351     B b1311 t1311
3352     T t1312 o1275 b1311
3353     B b1312 t1312
3354     T t1313 o390 b1312
3355     B b1313 t1313
3356     T t1314 o1274 b1313
3357     B b1314 t1314
3358     P p1314 Number 5865
3359     P p1315 Number 5939
3360     O o1315 location p1314 p1315
3361     O o1316 str_let p1314 p1315
3362     P p1316 Number 5869
3363     O o1317 patt_var p1316 p1315
3364     O o1318 patt_done p1314 p1315
3365     T t1318 o1318
3366     B b1318 t1318 groupCancelRightT
3367     T t1319 o1317 b1318
3368     B b1319 t1319
3369     O o1319 fun p1316 p1315
3370     O o1320 patt_if p1316 p1315
3371     P p1320 Number 5887
3372     P p1321 Number 5888
3373     O o1321 patt_var p1320 p1321
3374     O o1322 patt_body p1316 p1315
3375     P p1322 Number 5889
3376     P p1323 Number 5890
3377     O o1323 patt_var p1322 p1323
3378     P p1324 Number 5896
3379     O o1324 apply p1324 p1315
3380     P p1325 Number 5937
3381     O o1325 apply p1324 p1325
3382     P p1326 Number 5935
3383     O o1326 apply p1324 p1326
3384     P p1327 Number 5907
3385     O o1327 lid p1324 p1327
3386     O o1328 lid p1070
3387     T t1328 o1328
3388     B b1328 t1328
3389     T t1329 o1327 b1328
3390     B b1329 t1329
3391     P p1329 Number 5909
3392     P p1330 Number 5934
3393     O o1330 apply p1329 p1330
3394     P p1331 Number 5932
3395     O o1331 proj p1329 p1331
3396     O o1332 uid p1329 p1331
3397     T t1332 o1332 b834
3398     B b1332 t1332
3399     P p1332 Number 5918
3400     O o1333 lid p1332 p1331
3401     T t1333 o1333 b836
3402     B b1333 t1333
3403     T t1334 o1331 b1332 b1333
3404     B b1334 t1334
3405     P p1334 Number 5933
3406     O o1334 lid p1334 p1330
3407     T t1335 o1334 b839
3408     B b1335 t1335
3409     T t1336 o1330 b1334 b1335
3410     B b1336 t1336
3411     T t1337 o1326 b1329 b1336
3412     B b1337 t1337
3413     P p1337 Number 5936
3414     O o1337 lid p1337 p1325
3415     T t1338 o1337 b1297
3416     B b1338 t1338
3417     T t1339 o1325 b1337 b1338
3418     B b1339 t1339
3419     P p1339 Number 5938
3420     O o1339 lid p1339 p1315
3421     T t1340 o1339 b839
3422     B b1340 t1340
3423     T t1341 o1324 b1339 b1340
3424     B b1341 t1341
3425     T t1342 o1322 b1341
3426     B b1342 t1342 p
3427     T t1343 o1323 b1342
3428     B b1343 t1343
3429     T t1344 o1320 b1343
3430     B b1344 t1344
3431     T t1345 o1319 b1344
3432     B b1345 t1345
3433     T t1346 o1322 b1345
3434     B b1346 t1346 t
3435     T t1347 o1321 b1346
3436     B b1347 t1347
3437     T t1348 o1320 b1347
3438     B b1348 t1348
3439     T t1349 o1319 b1348
3440     B b1349 t1349
3441     T t1350 o1316 b1319 b1349
3442     B b1350 t1350
3443     T t1351 o b1350 b4
3444     B b1351 t1351
3445     T t1352 o1316 b1351
3446     B b1352 t1352
3447     T t1353 o390 b1352
3448     B b1353 t1353
3449     T t1354 o1315 b1353
3450     B b1354 t1354
3451     P p1354 Number 5957
3452     P p1355 Number 6198
3453     O o1355 location p1354 p1355
3454     P p1356 String unique_id1
3455     O o1356 rule p1356
3456     P p1357 Var e2
3457     O o1357 var p1357
3458     T t1357 o1357
3459     B b1357 t1357
3460     T t1358 o618 b1357
3461     S s1358 t635 h
3462     G s1358 t1358
3463     B b1358 s1358
3464     T t1359 o616 b1358
3465     B b1359 t1359
3466     T t1360 o653 b1357 b552
3467     S s1360 t618 h
3468     G s1360 t1360
3469     B b1360 s1360
3470     T t1361 o616 b1360
3471     B b1361 t1361
3472     NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
3473     NCzf_itt_dall!dall dall dall Czf_itt_dall
3474     O o1361 dall
3475     NItt_logic!and and and Itt_logic
3476     O o1362 and
3477     T t1362 o557 b1357 b571
3478     B b1362 t1362
3479     T t1363 o674 b1362 b571
3480     B b1363 t1363
3481     T t1364 o557 b571 b1357
3482     B b1364 t1364
3483     T t1365 o674 b1364 b571
3484     B b1365 t1365
3485     T t1366 o1362 b1363 b1365
3486     B b1366 t1366 s
3487     T t1367 o1361 b552 b1366
3488     H h1367 x t1367
3489     T t1368 o674 b1357 b565
3490     S s1368 t618 h h1367
3491     G s1368 t1368
3492     B b1368 s1368
3493     T t1369 o616 b1368
3494     B b1369 t1369
3495     T t1370 o633 b1361 b1369
3496     B b1370 t1370
3497     T t1371 o633 b1359 b1370
3498     B b1371 t1371
3499     P p1371 String "withT << id >> (dT 2) thenT autoT"
3500     O o1371 ext_rule p1371
3501     T t1372 o b1360 b4
3502     B b1372 t1372
3503     T t1373 o b1358 b1372
3504     B b1373 t1373
3505     T t1374 o925 b1368 b1373
3506     B b1374 t1374
3507     T t1375 o924 b1374 b4 b933
3508     B b1375 t1375
3509     T t1376 o557 b1357 b565
3510     B b1376 t1376
3511     T t1377 o674 b1376 b565
3512     H h1377 y t1377
3513     T t1378 o557 b565 b1357
3514     B b1378 t1378
3515     T t1379 o674 b1378 b565
3516     H h1379 z t1379
3517     S s1379 t618 h h1367 h1377 h1379
3518     G s1379 t1368
3519     B b1379 s1379
3520     T t1380 o925 b1379 b1373
3521     B b1380 t1380
3522     B b1381 t1377
3523     B b1382 t1379
3524     T t1382 o1362 b1381 b1382
3525     H h1382 w t1382
3526     S s1382 t618 h h1367 h1382
3527     G s1382 t1368
3528     B b1383 s1382
3529     T t1383 o925 b1383 b1373
3530     B b1384 t1383
3531     P p1384 String with
3532     O o1384 arg_named p1384
3533     NSummary!arg_term_list arg_term_list arg_term_list Summary
3534     O o1385 arg_term_list
3535     T t1385 o b565 b4
3536     B b1385 t1385
3537     T t1386 o1385 b1385
3538     B b1386 t1386
3539     T t1387 o1384 b1386
3540     B b1387 t1387
3541     T t1388 o b1387 b4
3542     B b1388 t1388
3543     T t1389 o924 b1374 b1388 b933
3544     B b1389 t1389
3545     T t1390 o2 b1389
3546     B b1390 t1390
3547     T t1391 o924 b1384 b4 b1390
3548     B b1391 t1391
3549     T t1392 o2 b1391
3550     B b1392 t1392
3551     T t1393 o924 b1380 b4 b1392
3552     B b1393 t1393
3553     T t1394 o b1393 b4
3554     B b1394 t1394
3555     T t1395 o923 b1375 b1394
3556     B b1395 t1395
3557     P p1395 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
3558     O o1395 ext_rule p1395
3559     T t1396 o923 b1393 b4
3560     B b1396 t1396
3561     T t1397 o1395 b922 b1396 b4 b4
3562     B b1397 t1397
3563     T t1398 o b1397 b4
3564     B b1398 t1398
3565     S s1398 t618 h
3566     G s1398 t1358
3567     B b1399 s1398
3568     T t1399 o b1399 b1372
3569     B b1400 t1399
3570     T t1400 o925 b1379 b1400
3571     B b1401 t1400
3572     T t1401 o925 b1383 b1400
3573     B b1402 t1401
3574     T t1402 o925 b1368 b1400
3575     B b1403 t1402
3576     T t1403 o924 b1403 b1388 b933
3577     B b1404 t1403
3578     T t1404 o2 b1404
3579     B b1405 t1404
3580     T t1405 o924 b1402 b4 b1405
3581     B b1406 t1405
3582     T t1406 o2 b1406
3583     B b1407 t1406
3584     T t1407 o924 b1401 b4 b1407
3585     B b1408 t1407
3586     T t1408 o923 b1408 b4
3587     B b1409 t1408
3588     T t1409 o1395 b922 b1409 b4 b4
3589     B b1410 t1409
3590     P p1410 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
3591     O o1410 ext_rule p1410
3592     H h1410 v t1368
3593     S s1410 t618 h h1367 h1377 h1379 h1410
3594     G s1410 t1368
3595     B b1411 s1410
3596     T t1411 o925 b1411 b1400
3597     B b1412 t1411
3598     T t1412 o2 b1408
3599     B b1413 t1412
3600     T t1413 o924 b1412 b4 b1413
3601     B b1414 t1413
3602     T t1414 o b1414 b4
3603     B b1415 t1414
3604     T t1415 o923 b1408 b1415
3605     B b1416 t1415
3606     T t1416 o1254 b1414
3607     B b1417 t1416
3608     T t1417 o b1417 b4
3609     B b1418 t1417
3610     T t1418 o1410 b922 b1416 b1418 b4
3611     B b1419 t1418
3612     P p1419 String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
3613     O o1419 ext_rule p1419
3614     P p1420 Var e
3615     O o1420 var p1420
3616     T t1420 o1420
3617     B b1420 t1420
3618     T t1421 o618 b1420
3619     S s1421 t635 h h1367 h1377 h1379
3620     G s1421 t1421
3621     B b1421 s1421
3622     T t1422 o925 b1421 b1400
3623     B b1422 t1422
3624     T t1423 o557 b1357 b1420
3625     B b1423 t1423
3626     T t1424 o618 b1423
3627     S s1424 t635 h h1367 h1377 h1379
3628     G s1424 t1424
3629     B b1424 s1424
3630     T t1425 o925 b1424 b1400
3631     B b1425 t1425
3632     T t1426 o737 b1423 b1357
3633     S s1426 t618 h h1367 h1377 h1379
3634     G s1426 t1426
3635     B b1426 s1426
3636     T t1427 o925 b1426 b1400
3637     B b1427 t1427
3638     T t1428 o953 b1427 b970 b1413
3639     B b1428 t1428
3640     T t1429 o2 b1428
3641     B b1429 t1429
3642     T t1430 o960 b1425 b970 b1429
3643     B b1430 t1430
3644     T t1431 o2 b1430
3645     B b1431 t1431
3646     T t1432 o960 b1422 b4 b1431
3647     B b1432 t1432
3648     T t1433 o674 b1423 b1357
3649     S s1433 t618 h h1367 h1377 h1379
3650     G s1433 t1433
3651     B b1433 s1433
3652     T t1434 o925 b1433 b1400
3653     B b1434 t1434
3654     T t1435 o953 b1434 b4 b1429
3655     B b1435 t1435
3656     H h1435 v t1377
3657     S s1435 t618 h h1367 h1377 h1379 h1435
3658     G s1435 t1368
3659     B b1436 s1435
3660     T t1436 o925 b1436 b1400
3661     B b1437 t1436
3662     T t1437 o924 b1437 b4 b1413
3663     B b1438 t1437
3664     B b1439 t1376 v
3665     T t1439 o710 b1439
3666     S s1439 t618 h h1367 h1377 h1379
3667     G s1439 t1439
3668     B b1440 s1439
3669     T t1440 o925 b1440 b1400
3670     B b1441 t1440
3671     B b1442 t1377 v
3672     T t1442 o963 b1442
3673     S s1442 t618 h h1367 h1377 h1379
3674     G s1442 t1442
3675     B b1443 s1442
3676     T t1443 o925 b1443 b1400
3677     B b1444 t1443
3678     T t1444 o960 b1444 b970 b1413
3679     B b1445 t1444
3680     T t1445 o2 b1445
3681     B b1446 t1445
3682     T t1446 o960 b1441 b4 b1446
3683     B b1447 t1446
3684     T t1447 o b1447 b4
3685     B b1448 t1447
3686     T t1448 o b1438 b1448
3687     B b1449 t1448
3688     T t1449 o b1435 b1449
3689     B b1450 t1449
3690     T t1450 o b1432 b1450
3691     B b1451 t1450
3692     T t1451 o923 b1408 b1451
3693     B b1452 t1451
3694     T t1452 o1254 b1432
3695     B b1453 t1452
3696     T t1453 o1254 b1435
3697     B b1454 t1453
3698     T t1454 o1254 b1438
3699     B b1455 t1454
3700     T t1455 o1254 b1447
3701     B b1456 t1455
3702     T t1456 o b1456 b4
3703     B b1457 t1456
3704     T t1457 o b1455 b1457
3705     B b1458 t1457
3706     T t1458 o b1454 b1458
3707     B b1459 t1458
3708     T t1459 o b1453 b1459
3709     B b1460 t1459
3710     T t1460 o1419 b922 b1452 b1460 b4
3711     B b1461 t1460
3712     T t1461 o b1461 b4
3713     B b1462 t1461
3714     T t1462 o b1461 b1462
3715     B b1463 t1462
3716     T t1463 o b1419 b1463
3717     B b1464 t1463
3718     T t1464 o b1410 b1464
3719     B b1465 t1464
3720     T t1465 o1371 b922 b1395 b1398 b1465
3721     B b1466 t1465
3722     T t1466 o920 b1466
3723     B b1467 t1466
3724     P p1467 Number 5983
3725     P p1468 Number 5991
3726     O o1468 resource_defs p1467 p1468 p262
3727     P p1469 Number 5989
3728     O o1469 uid p1469 p1468
3729     T t1469 o1469 b624
3730     B b1469 t1469
3731     T t1470 o b1469 b4
3732     B b1470 t1470
3733     T t1471 o1468 b1470
3734     B b1471 t1471
3735     T t1472 o b1471 b4
3736     B b1472 t1472
3737     T t1473 o1356 b616 b1371 b1467 b1472
3738     B b1473 t1473
3739     T t1474 o1355 b1473
3740     B b1474 t1474
3741     P p1474 Number 6221
3742     P p1475 Number 6548
3743     O o1475 location p1474 p1475
3744     P p1476 String unique_inv
3745     O o1476 rule p1476
3746     T t1476 o557 b559 b571
3747     B b1476 t1476
3748     T t1477 o737 b1476 b565
3749     H h1477 x t1477
3750     T t1478 o557 b571 b559
3751     B b1478 t1478
3752     T t1479 o737 b1478 b565
3753     H h1479 y t1479
3754     T t1480 o737 b559 b572
3755     S s1480 t618 h h1477 h1479
3756     G s1480 t1480
3757     B b1480 s1480
3758     T t1481 o616 b1480
3759     B b1481 t1481
3760     T t1482 o633 b656 b1481
3761     B b1482 t1482
3762     T t1483 o633 b793 b1482
3763     B b1483 t1483
3764     T t1484 o633 b639 b1483
3765     B b1484 t1484
3766     T t1485 o633 b710 b1484
3767     B b1485 t1485
3768     P p1485 String "assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
3769     O o1485 ext_rule p1485
3770     T t1486 o b655 b4
3771     B b1486 t1486
3772     T t1487 o b792 b1486
3773     B b1487 t1487
3774     T t1488 o b638 b1487
3775     B b1488 t1488
3776     T t1489 o b709 b1488
3777     B b1489 t1489
3778     T t1490 o925 b1480 b1489
3779     B b1490 t1490
3780     T t1491 o924 b1490 b4 b933
3781     B b1491 t1491
3782     T t1492 o557 b572 b571
3783     B b1492 t1492
3784     T t1493 o737 b1492 b565
3785     H h1493 v t1493
3786     S s1493 t618 h h1477 h1479 h1493
3787     G s1493 t1480
3788     B b1493 s1493
3789     T t1494 o925 b1493 b1489
3790     B b1494 t1494
3791     T t1495 o2 b1491
3792     B b1495 t1495
3793     T t1496 o924 b1494 b4 b1495
3794     B b1496 t1496
3795     T t1497 o b1496 b4
3796     B b1497 t1497
3797     T t1498 o923 b1491 b1497
3798     B b1498 t1498
3799     P p1498 String "setSubstT << equal{id; op{inv{'s}; 's}} >> 2 thenAT autoT"
3800     O o1498 ext_rule p1498
3801     T t1499 o674 b565 b1492
3802     S s1499 t618 h h1477 h1479 h1493
3803     G s1499 t1499
3804     B b1499 s1499
3805     T t1500 o925 b1499 b1489
3806     B b1500 t1500
3807     T t1501 o737 b565 b1492
3808     S s1501 t618 h h1477 h1479 h1493
3809     G s1501 t1501
3810     B b1501 s1501
3811     T t1502 o925 b1501 b1489
3812     B b1502 t1502
3813     T t1503 o2 b1496
3814     B b1503 t1503
3815     T t1504 o953 b1502 b970 b1503
3816     B b1504 t1504
3817     T t1505 o2 b1504
3818     B b1505 t1505
3819     T t1506 o953 b1500 b4 b1505
3820     B b1506 t1506
3821     T t1507 o737 b1476 b1492
3822     H h1507 v_1 t1507
3823     S s1507 t618 h h1477 h1479 h1493 h1507
3824     G s1507 t1480
3825     B b1507 s1507
3826     T t1508 o925 b1507 b1489
3827     B b1508 t1508
3828     T t1509 o924 b1508 b4 b1503
3829     B b1509 t1509
3830     B b1510 t1476 v_1
3831     T t1510 o710 b1510
3832     S s1510 t618 h h1477 h1479 h1493
3833     G s1510 t1510
3834     B b1511 s1510
3835     T t1511 o925 b1511 b1489
3836     B b1512 t1511
3837     P p1512 Var v_1
3838     O o1512 var p1512
3839     T t1512 o1512
3840     B b1513 t1512
3841     T t1513 o737 b1476 b1513
3842     B b1514 t1513 v_1
3843     T t1514 o963 b1514
3844     S s1514 t618 h h1477 h1479 h1493
3845     G s1514 t1514
3846     B b1515 s1514
3847     T t1515 o925 b1515 b1489
3848     B b1516 t1515
3849     T t1516 o960 b1516 b970 b1503
3850     B b1517 t1516
3851     T t1517 o2 b1517
3852     B b1518 t1517
3853     T t1518 o960 b1512 b4 b1518
3854     B b1519 t1518
3855     T t1519 o b1519 b4
3856     B b1520 t1519
3857     T t1520 o b1509 b1520
3858     B b1521 t1520
3859     T t1521 o b1506 b1521
3860     B b1522 t1521
3861     T t1522 o923 b1496 b1522
3862     B b1523 t1522
3863     P p1523 String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
3864     O o1523 ext_rule p1523
3865     T t1523 o923 b1506 b4
3866     B b1524 t1523
3867     T t1524 o1523 b922 b1524 b4 b4
3868     B b1525 t1524
3869     P p1525 String "groupCancelRightT << 's >> thenT autoT"
3870     O o1525 ext_rule p1525
3871     T t1525 o923 b1509 b4
3872     B b1526 t1525
3873     T t1526 o1525 b922 b1526 b4 b4
3874     B b1527 t1526
3875     T t1527 o923 b1519 b4
3876     B b1528 t1527
3877     T t1528 o1228 b922 b1528 b4 b4
3878     B b1529 t1528
3879     T t1529 o b1529 b4
3880     B b1530 t1529
3881     T t1530 o b1527 b1530
3882     B b1531 t1530
3883     T t1531 o b1525 b1531
3884     B b1532 t1531
3885     T t1532 o1498 b922 b1523 b1532 b4
3886     B b1533 t1532
3887     T t1533 o b1533 b4
3888     B b1534 t1533
3889     T t1534 o1485 b922 b1498 b1534 b4
3890     B b1535 t1534
3891     T t1535 o920 b1535
3892     B b1536 t1535
3893     P p1536 Number 6247
3894     P p1537 Number 6255
3895     O o1537 resource_defs p1536 p1537 p262
3896     P p1538 Number 6253
3897     O o1538 uid p1538 p1537
3898     T t1538 o1538 b624
3899     B b1538 t1538
3900     T t1539 o b1538 b4
3901     B b1539 t1539
3902     T t1540 o1537 b1539
3903     B b1540 t1540
3904     T t1541 o b1540 b4
3905     B b1541 t1541
3906     T t1542 o1476 b616 b1485 b1536 b1541
3907     B b1542 t1542
3908     T t1543 o1475 b1542
3909     B b1543 t1543
3910     P p1543 Number 6599
3911     P p1544 Number 7021
3912     O o1544 location p1543 p1544
3913     P p1545 String unique_sol1
3914     O o1545 rule p1545
3915     P p1546 Var a
3916     O o1546 var p1546
3917     T t1546 o1546
3918     B b1546 t1546
3919     T t1547 o618 b1546
3920     S s1547 t635 h
3921     G s1547 t1547
3922     B b1547 s1547
3923     T t1548 o616 b1547
3924     B b1548 t1548
3925     P p1548 Var b
3926     O o1548 var p1548
3927     T t1549 o1548
3928     B b1549 t1549
3929     T t1550 o618 b1549
3930     S s1550 t635 h
3931     G s1550 t1550
3932     B b1550 s1550
3933     T t1551 o616 b1550
3934     B b1551 t1551
3935     P p1551 Var x
3936     O o1551 var p1551
3937     T t1552 o1551
3938     B b1552 t1552
3939     T t1553 o618 b1552
3940     S s1553 t635 h
3941     G s1553 t1553
3942     B b1553 s1553
3943     T t1554 o616 b1553
3944     B b1554 t1554
3945     T t1555 o653 b1546 b552
3946     S s1555 t618 h
3947     G s1555 t1555
3948     B b1555 s1555
3949     T t1556 o616 b1555
3950     B b1556 t1556
3951     T t1557 o653 b1549 b552
3952     S s1557 t618 h
3953     G s1557 t1557
3954     B b1557 s1557
3955     T t1558 o616 b1557
3956     B b1558 t1558
3957     T t1559 o653 b1552 b552
3958     S s1559 t618 h
3959     G s1559 t1559
3960     B b1559 s1559
3961     T t1560 o616 b1559
3962     B b1560 t1560
3963     T t1561 o557 b1546 b1552
3964     B b1561 t1561
3965     T t1562 o737 b1561 b1549
3966     S s1562 t618 h
3967     G s1562 t1562
3968     B b1562 s1562
3969     T t1563 o616 b1562
3970     B b1563 t1563
3971     T t1564 o570 b1546
3972     B b1564 t1564
3973     T t1565 o557 b1564 b1549
3974     B b1565 t1565
3975     T t1566 o737 b1552 b1565
3976     S s1566 t618 h
3977     G s1566 t1566
3978     B b1566 s1566
3979     T t1567 o616 b1566
3980     B b1567 t1567
3981     T t1568 o633 b1563 b1567
3982     B b1568 t1568
3983     T t1569 o633 b1560 b1568
3984     B b1569 t1569
3985     T t1570 o633 b1558 b1569
3986     B b1570 t1570
3987     T t1571 o633 b1556 b1570
3988     B b1571 t1571
3989     T t1572 o633 b1554 b1571
3990     B b1572 t1572
3991     T t1573 o633 b1551 b1572
3992     B b1573 t1573
3993     T t1574 o633 b1548 b1573
3994     B b1574 t1574
3995     P p1574 String "assumT 7 thenT rwh unfold_equal 2 thenT autoT thenT assertT << equal{op{inv{'a}; op{'a; 'x}}; op{inv{'a}; 'b}} >> thenWT autoT"
3996     O o1574 ext_rule p1574
3997     T t1575 o b1562 b4
3998     B b1575 t1575
3999     T t1576 o b1559 b1575
4000     B b1576 t1576
4001     T t1577 o b1557 b1576
4002     B b1577 t1577
4003     T t1578 o b1555 b1577
4004     B b1578 t1578
4005     T t1579 o b1553 b1578
4006     B b1579 t1579
4007     T t1580 o b1550 b1579
4008     B b1580 t1580
4009     T t1581 o b1547 b1580
4010     B b1581 t1581
4011     T t1582 o925 b1566 b1581
4012     B b1582 t1582
4013     T t1583 o924 b1582 b4 b933
4014     B b1583 t1583
4015     T t1584 o618 b1561
4016