/[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 3516 - (hide annotations) (download)
Mon Feb 25 02:24:42 2002 UTC (19 years, 5 months ago) by xiny
File size: 96837 byte(s)
Replaced equality relations with equivalence relations everywhere in the
context of groups, and re-proved the rules.

1 xiny 3379 #PRL version 1.0.0 ASCII term
2     NPerv Perv Perv NIL
3     NPerv!cons cons cons Perv
4     O o cons
5     NSummary Summary Summary NIL
6     NSummary!location location location Summary
7     P p Number 0
8 xiny 3498 P p1 Number 25
9 xiny 3379 O o1 location p p1
10     NSummary!parent parent parent Summary
11     O o2 parent
12 xiny 3498 P p2 String Itt_record_label0
13 xiny 3379 O o3 parent p2
14     T t o3
15     B b t
16     NPerv!nil nil3 nil Perv
17     O o4 nil3
18     T t4 o4
19     B b4 t4
20     T t5 o b b4
21     B b5 t5
22 xiny 3498 P p5 String Itt_nat
23 xiny 3379 O o5 parent p5
24     T t6 o5
25     B b6 t6
26     T t7 o b6 b4
27     B b7 t7
28 xiny 3498 P p7 String Itt_int_ext
29 xiny 3379 O o7 parent p7
30     T t8 o7
31     B b8 t8
32     T t9 o b8 b4
33     B b9 t9
34 xiny 3498 P p9 String Itt_int_base
35 xiny 3379 O o9 parent p9
36     T t10 o9
37     B b10 t10
38     T t11 o b10 b4
39     B b11 t11
40 xiny 3498 P p11 String Itt_bool
41 xiny 3379 O o11 parent p11
42     T t12 o11
43     B b12 t12
44     T t13 o b12 b4
45     B b13 t13
46 xiny 3498 P p13 String Itt_decidable
47 xiny 3379 O o13 parent p13
48     T t14 o13
49     B b14 t14
50     T t15 o b14 b4
51     B b15 t15
52 xiny 3498 P p15 String Itt_logic
53 xiny 3379 O o15 parent p15
54     T t16 o15
55     B b16 t16
56     T t17 o b16 b4
57     B b17 t17
58 xiny 3498 P p17 String Itt_union
59 xiny 3379 O o17 parent p17
60     T t18 o17
61     B b18 t18
62     T t19 o b18 b4
63     B b19 t19
64 xiny 3498 P p19 String Itt_prod
65 xiny 3379 O o19 parent p19
66     T t20 o19
67     B b20 t20
68     T t21 o b20 b4
69     B b21 t21
70 xiny 3498 P p21 String Itt_dprod
71 xiny 3379 O o21 parent p21
72     T t22 o21
73     B b22 t22
74     T t23 o b22 b4
75     B b23 t23
76 xiny 3498 P p23 String Itt_fun
77 xiny 3379 O o23 parent p23
78     T t24 o23
79     B b24 t24
80     T t25 o b24 b4
81     B b25 t25
82 xiny 3498 P p25 String Itt_dfun
83 xiny 3379 O o25 parent p25
84     T t26 o25
85     B b26 t26
86     T t27 o b26 b4
87     B b27 t27
88 xiny 3498 P p27 String Itt_rfun
89 xiny 3379 O o27 parent p27
90     T t28 o27
91     B b28 t28
92     T t29 o b28 b4
93     B b29 t29
94 xiny 3498 P p29 String Itt_void
95 xiny 3379 O o29 parent p29
96     T t30 o29
97     B b30 t30
98     T t31 o b30 b4
99     B b31 t31
100 xiny 3498 P p31 String Itt_set
101 xiny 3379 O o31 parent p31
102     T t32 o31
103     B b32 t32
104     T t33 o b32 b4
105     B b33 t33
106 xiny 3498 P p33 String Itt_unit
107 xiny 3379 O o33 parent p33
108     T t34 o33
109     B b34 t34
110     T t35 o b34 b4
111     B b35 t35
112 xiny 3498 P p35 String Itt_squiggle
113 xiny 3379 O o35 parent p35
114     T t36 o35
115     B b36 t36
116     T t37 o b36 b4
117     B b37 t37
118 xiny 3498 P p37 String Itt_subtype
119 xiny 3379 O o37 parent p37
120     T t38 o37
121     B b38 t38
122     T t39 o b38 b4
123     B b39 t39
124 xiny 3498 P p39 String Itt_squash
125 xiny 3379 O o39 parent p39
126     T t40 o39
127     B b40 t40
128     T t41 o b40 b4
129     B b41 t41
130 xiny 3498 P p41 String Itt_struct
131 xiny 3379 O o41 parent p41
132     T t42 o41
133     B b42 t42
134     T t43 o b42 b4
135     B b43 t43
136 xiny 3498 P p43 String Itt_equal
137 xiny 3379 O o43 parent p43
138     T t44 o43
139     B b44 t44
140     T t45 o b44 b4
141     B b45 t45
142 xiny 3498 P p45 String Itt_comment
143 xiny 3379 O o45 parent p45
144     T t46 o45
145     B b46 t46
146     T t47 o b46 b4
147     B b47 t47
148 xiny 3498 P p47 String Base_theory
149 xiny 3379 O o47 parent p47
150     T t48 o47
151     B b48 t48
152     T t49 o b48 b4
153     B b49 t49
154 xiny 3498 P p49 String Base_meta
155 xiny 3379 O o49 parent p49
156     T t50 o49
157     B b50 t50
158     T t51 o b50 b4
159     B b51 t51
160 xiny 3498 P p51 String Base_cache
161 xiny 3379 O o51 parent p51
162     T t52 o51
163     B b52 t52
164     T t53 o b52 b4
165     B b53 t53
166 xiny 3498 P p53 String Tactic_cache
167 xiny 3379 O o53 parent p53
168     T t54 o53
169     B b54 t54
170     T t55 o b54 b4
171     B b55 t55
172 xiny 3498 P p55 String Typeinf
173 xiny 3379 O o55 parent p55
174     T t56 o55
175     B b56 t56
176     T t57 o b56 b4
177     B b57 t57
178 xiny 3498 P p57 String Ocaml_df
179 xiny 3379 O o57 parent p57
180     T t58 o57
181     B b58 t58
182     T t59 o b58 b4
183     B b59 t59
184 xiny 3498 P p59 String Ocaml_str_df
185 xiny 3379 O o59 parent p59
186     T t60 o59
187     B b60 t60
188     T t61 o b60 b4
189     B b61 t61
190 xiny 3498 P p61 String Ocaml_sig_df
191 xiny 3379 O o61 parent p61
192     T t62 o61
193     B b62 t62
194     T t63 o b62 b4
195     B b63 t63
196 xiny 3498 P p63 String Ocaml_me_df
197 xiny 3379 O o63 parent p63
198     T t64 o63
199     B b64 t64
200     T t65 o b64 b4
201     B b65 t65
202 xiny 3498 P p65 String Ocaml_mt_df
203 xiny 3379 O o65 parent p65
204     T t66 o65
205     B b66 t66
206     T t67 o b66 b4
207     B b67 t67
208 xiny 3498 P p67 String Ocaml_type_df
209 xiny 3379 O o67 parent p67
210     T t68 o67
211     B b68 t68
212     T t69 o b68 b4
213     B b69 t69
214 xiny 3498 P p69 String Ocaml_patt_df
215 xiny 3379 O o69 parent p69
216     T t70 o69
217     B b70 t70
218     T t71 o b70 b4
219     B b71 t71
220 xiny 3498 P p71 String Ocaml_expr_df
221 xiny 3379 O o71 parent p71
222     T t72 o71
223     B b72 t72
224     T t73 o b72 b4
225     B b73 t73
226 xiny 3498 P p73 String Ocaml_base_df
227 xiny 3379 O o73 parent p73
228     T t74 o73
229     B b74 t74
230     T t75 o b74 b4
231     B b75 t75
232 xiny 3498 P p75 String Ocaml
233 xiny 3379 O o75 parent p75
234     T t76 o75
235     B b76 t76
236     T t77 o b76 b4
237     B b77 t77
238 xiny 3498 P p77 String Base_rewrite
239 xiny 3379 O o77 parent p77
240     T t78 o77
241     B b78 t78
242     T t79 o b78 b4
243     B b79 t79
244 xiny 3498 P p79 String Base_dtactic
245 xiny 3379 O o79 parent p79
246     T t80 o79
247     B b80 t80
248     T t81 o b80 b4
249     B b81 t81
250 xiny 3498 P p81 String Base_auto_tactic
251 xiny 3379 O o81 parent p81
252     T t82 o81
253     B b82 t82
254     T t83 o b82 b4
255     B b83 t83
256 xiny 3498 P p83 String Base_trivial
257 xiny 3379 O o83 parent p83
258     T t84 o83
259     B b84 t84
260     T t85 o b84 b4
261     B b85 t85
262 xiny 3498 P p85 String Top_conversionals
263 xiny 3379 O o85 parent p85
264     T t86 o85
265     B b86 t86
266     T t87 o b86 b4
267     B b87 t87
268 xiny 3498 P p87 String Top_tacticals
269 xiny 3379 O o87 parent p87
270     T t88 o87
271     B b88 t88
272     T t89 o b88 b4
273     B b89 t89
274 xiny 3498 P p89 String Var
275 xiny 3379 O o89 parent p89
276     T t90 o89
277     B b90 t90
278     T t91 o b90 b4
279     B b91 t91
280 xiny 3498 P p91 String Mptop
281 xiny 3379 O o91 parent p91
282     T t92 o91
283     B b92 t92
284     T t93 o b92 b4
285     B b93 t93
286 xiny 3498 P p93 String Summary
287 xiny 3379 O o93 parent p93
288     T t94 o93
289     B b94 t94
290     T t95 o b94 b4
291     B b95 t95
292 xiny 3498 P p95 String Comment
293 xiny 3379 O o95 parent p95
294     T t96 o95
295     B b96 t96
296     T t97 o b96 b4
297     B b97 t97
298 xiny 3498 P p97 String Base_dform
299 xiny 3379 O o97 parent p97
300     T t98 o97
301     B b98 t98
302     T t99 o b98 b4
303     B b99 t99
304 xiny 3498 P p99 String Nuprl_font
305 xiny 3379 O o99 parent p99
306     T t100 o99
307     B b100 t100
308     T t101 o b100 b4
309     B b101 t101
310 xiny 3498 P p101 String Perv
311 xiny 3379 O o101 parent p101
312     T t102 o101
313     B b102 t102
314     T t103 o b102 b4
315     B b103 t103
316 xiny 3498 T t104 o b103 b4
317 xiny 3379 B b104 t104
318 xiny 3498 T t105 o b101 b104
319 xiny 3379 B b105 t105
320 xiny 3498 T t106 o b99 b105
321 xiny 3379 B b106 t106
322 xiny 3498 T t107 o b97 b106
323 xiny 3379 B b107 t107
324 xiny 3498 T t108 o b95 b107
325 xiny 3379 B b108 t108
326 xiny 3498 T t109 o b93 b108
327 xiny 3379 B b109 t109
328 xiny 3498 T t110 o b91 b109
329 xiny 3379 B b110 t110
330 xiny 3498 T t111 o b89 b110
331 xiny 3379 B b111 t111
332 xiny 3498 T t112 o b87 b111
333 xiny 3379 B b112 t112
334 xiny 3498 T t113 o b85 b112
335 xiny 3379 B b113 t113
336 xiny 3498 T t114 o b83 b113
337 xiny 3379 B b114 t114
338 xiny 3498 T t115 o b81 b114
339 xiny 3379 B b115 t115
340 xiny 3498 T t116 o b79 b115
341 xiny 3379 B b116 t116
342 xiny 3498 T t117 o b77 b116
343 xiny 3379 B b117 t117
344 xiny 3498 T t118 o b75 b117
345 xiny 3379 B b118 t118
346 xiny 3498 T t119 o b73 b118
347 xiny 3379 B b119 t119
348 xiny 3498 T t120 o b71 b119
349 xiny 3379 B b120 t120
350 xiny 3498 T t121 o b69 b120
351 xiny 3379 B b121 t121
352 xiny 3498 T t122 o b67 b121
353 xiny 3379 B b122 t122
354 xiny 3498 T t123 o b65 b122
355 xiny 3379 B b123 t123
356 xiny 3498 T t124 o b63 b123
357 xiny 3379 B b124 t124
358 xiny 3498 T t125 o b61 b124
359 xiny 3379 B b125 t125
360 xiny 3498 T t126 o b59 b125
361 xiny 3379 B b126 t126
362 xiny 3498 T t127 o b57 b126
363 xiny 3379 B b127 t127
364 xiny 3498 T t128 o b55 b127
365 xiny 3379 B b128 t128
366 xiny 3498 T t129 o b53 b128
367 xiny 3379 B b129 t129
368 xiny 3498 T t130 o b51 b129
369 xiny 3379 B b130 t130
370 xiny 3498 T t131 o b49 b130
371 xiny 3379 B b131 t131
372 xiny 3498 T t132 o b47 b131
373 xiny 3379 B b132 t132
374 xiny 3498 T t133 o b45 b132
375 xiny 3379 B b133 t133
376 xiny 3498 T t134 o b43 b133
377 xiny 3379 B b134 t134
378 xiny 3498 T t135 o b41 b134
379 xiny 3379 B b135 t135
380 xiny 3498 T t136 o b39 b135
381 xiny 3379 B b136 t136
382 xiny 3498 T t137 o b37 b136
383 xiny 3379 B b137 t137
384 xiny 3498 T t138 o b35 b137
385 xiny 3379 B b138 t138
386 xiny 3498 T t139 o b33 b138
387 xiny 3379 B b139 t139
388 xiny 3498 T t140 o b31 b139
389 xiny 3379 B b140 t140
390 xiny 3498 T t141 o b29 b140
391 xiny 3379 B b141 t141
392 xiny 3498 T t142 o b27 b141
393 xiny 3379 B b142 t142
394 xiny 3498 T t143 o b25 b142
395 xiny 3379 B b143 t143
396 xiny 3498 T t144 o b23 b143
397 xiny 3379 B b144 t144
398 xiny 3498 T t145 o b21 b144
399 xiny 3379 B b145 t145
400 xiny 3498 T t146 o b19 b145
401 xiny 3379 B b146 t146
402 xiny 3498 T t147 o b17 b146
403 xiny 3379 B b147 t147
404 xiny 3498 T t148 o b15 b147
405 xiny 3379 B b148 t148
406 xiny 3498 T t149 o b13 b148
407 xiny 3379 B b149 t149
408 xiny 3498 T t150 o b11 b149
409 xiny 3379 B b150 t150
410 xiny 3498 T t151 o b9 b150
411 xiny 3379 B b151 t151
412 xiny 3498 T t152 o b7 b151
413 xiny 3379 B b152 t152
414 xiny 3498 T t153 o b5 b152
415 xiny 3379 B b153 t153
416 xiny 3498 NSummary!resource resource resource Summary
417     P p153 String auto
418     O o153 resource p153
419     NOcaml Ocaml Ocaml NIL
420     NOcaml!type_lid type_lid type_lid Ocaml
421     P p154 Number 2332
422     P p155 Number 2341
423     O o155 type_lid p154 p155
424     P p156 String auto_info
425     O o156 type_lid p156
426     T t156 o156
427 xiny 3379 B b156 t156
428 xiny 3498 T t157 o155 b156
429 xiny 3379 B b157 t157
430 xiny 3498 NOcaml!type_prod type_prod type_prod Ocaml
431     P p157 Number 2343
432     P p158 Number 2367
433     O o158 type_prod p157 p158
434     P p159 Number 2349
435     O o159 type_lid p157 p159
436     P p160 String tactic
437     O o160 type_lid p160
438     T t160 o160
439 xiny 3379 B b160 t160
440 xiny 3498 T t161 o159 b160
441 xiny 3379 B b161 t161
442 xiny 3498 P p161 Number 2352
443     P p162 Number 2358
444     O o162 type_lid p161 p162
445     T t162 o162 b160
446 xiny 3379 B b162 t162
447 xiny 3498 P p163 Number 2361
448     O o163 type_lid p163 p158
449     T t163 o163 b160
450 xiny 3379 B b163 t163
451 xiny 3498 T t164 o b163 b4
452 xiny 3379 B b164 t164
453 xiny 3498 T t165 o b162 b164
454 xiny 3379 B b165 t165
455 xiny 3498 T t166 o b161 b165
456 xiny 3379 B b166 t166
457 xiny 3498 T t167 o158 b166
458 xiny 3379 B b167 t167
459 xiny 3498 T t168 o153 b157 b167
460 xiny 3379 B b168 t168
461 xiny 3498 P p168 String cache
462     O o168 resource p168
463     P p169 Number 1424
464     P p170 Number 1434
465     O o170 type_lid p169 p170
466     P p171 String cache_rule
467     O o171 type_lid p171
468     T t171 o171
469 xiny 3379 B b171 t171
470 xiny 3498 T t172 o170 b171
471 xiny 3379 B b172 t172
472 xiny 3498 P p172 Number 1436
473     P p173 Number 1441
474     O o173 type_lid p172 p173
475     O o174 type_lid p168
476     T t174 o174
477 xiny 3379 B b174 t174
478 xiny 3498 T t175 o173 b174
479 xiny 3379 B b175 t175
480 xiny 3498 T t176 o168 b172 b175
481 xiny 3379 B b176 t176
482 xiny 3498 P p176 String elim
483     O o176 resource p176
484     P p177 Number 1761
485     P p178 Number 1783
486     O o178 type_prod p177 p178
487     P p179 Number 1765
488     O o179 type_lid p177 p179
489     P p180 String term
490     O o180 type_lid p180
491     T t180 o180
492 xiny 3379 B b180 t180
493 xiny 3498 T t181 o179 b180
494 xiny 3379 B b181 t181
495 xiny 3498 NOcaml!type_fun type_fun type_fun Ocaml
496     P p181 Number 1769
497     P p182 Number 1782
498     O o182 type_fun p181 p182
499     P p183 Number 1772
500     O o183 type_lid p181 p183
501     P p184 String int
502     O o184 type_lid p184
503     T t184 o184
504 xiny 3379 B b184 t184
505 xiny 3498 T t185 o183 b184
506 xiny 3379 B b185 t185
507 xiny 3498 P p185 Number 1776
508     O o185 type_lid p185 p182
509     T t186 o185 b160
510 xiny 3379 B b186 t186
511 xiny 3498 T t187 o182 b185 b186
512 xiny 3379 B b187 t187
513 xiny 3498 T t188 o b187 b4
514 xiny 3379 B b188 t188
515 xiny 3498 T t189 o b181 b188
516 xiny 3379 B b189 t189
517 xiny 3498 T t190 o178 b189
518 xiny 3379 B b190 t190
519 xiny 3498 P p190 Number 1785
520     P p191 Number 1798
521     O o191 type_fun p190 p191
522     P p192 Number 1788
523     O o192 type_lid p190 p192
524     T t192 o192 b184
525 xiny 3379 B b192 t192
526 xiny 3498 P p193 Number 1792
527     O o193 type_lid p193 p191
528     T t193 o193 b160
529 xiny 3379 B b193 t193
530 xiny 3498 T t194 o191 b192 b193
531 xiny 3379 B b194 t194
532 xiny 3498 T t195 o176 b190 b194
533 xiny 3379 B b195 t195
534 xiny 3498 P p195 String eqcd
535     O o195 resource p195
536     P p196 Number 6168
537     P p197 Number 6181
538     O o197 type_prod p196 p197
539     P p198 Number 6172
540     O o198 type_lid p196 p198
541     T t198 o198 b180
542 xiny 3379 B b198 t198
543 xiny 3498 P p199 Number 6175
544     O o199 type_lid p199 p197
545     T t199 o199 b160
546 xiny 3379 B b199 t199
547 xiny 3498 T t200 o b199 b4
548 xiny 3379 B b200 t200
549 xiny 3498 T t201 o b198 b200
550 xiny 3379 B b201 t201
551 xiny 3498 T t202 o197 b201
552 xiny 3379 B b202 t202
553 xiny 3498 P p202 Number 6183
554     P p203 Number 6189
555     O o203 type_lid p202 p203
556     T t203 o203 b160
557 xiny 3379 B b203 t203
558 xiny 3498 T t204 o195 b202 b203
559 xiny 3379 B b204 t204
560 xiny 3498 P p204 String intro
561     O o204 resource p204
562     P p205 Number 1815
563     P p206 Number 1852
564     O o206 type_prod p205 p206
565     P p207 Number 1819
566     O o207 type_lid p205 p207
567     T t207 o207 b180
568 xiny 3379 B b207 t207
569 xiny 3498 P p208 Number 1823
570     P p209 Number 1851
571     O o209 type_prod p208 p209
572     P p210 Number 1829
573     O o210 type_lid p208 p210
574     P p211 String string
575     O o211 type_lid p211
576     T t211 o211
577 xiny 3379 B b211 t211
578 xiny 3498 T t212 o210 b211
579 xiny 3379 B b212 t212
580 xiny 3498 NOcaml!type_apply type_apply type_apply Ocaml
581     P p212 Number 1832
582     P p213 Number 1842
583     O o213 type_apply p212 p213
584     P p214 Number 1836
585     O o214 type_lid p214 p213
586     P p215 String option
587     O o215 type_lid p215
588     T t215 o215
589     B b215 t215
590     T t216 o214 b215
591 xiny 3379 B b216 t216
592 xiny 3498 P p216 Number 1835
593     O o216 type_lid p212 p216
594     T t217 o216 b184
595 xiny 3379 B b217 t217
596 xiny 3498 T t218 o213 b216 b217
597     B b218 t218
598     P p218 Number 1845
599     O o218 type_lid p218 p209
600     T t219 o218 b160
601     B b219 t219
602     T t220 o b219 b4
603 xiny 3379 B b220 t220
604 xiny 3498 T t221 o b218 b220
605 xiny 3379 B b221 t221
606 xiny 3498 T t222 o b212 b221
607 xiny 3379 B b222 t222
608 xiny 3498 T t223 o209 b222
609 xiny 3379 B b223 t223
610 xiny 3404 T t224 o b223 b4
611 xiny 3379 B b224 t224
612 xiny 3498 T t225 o b207 b224
613 xiny 3379 B b225 t225
614 xiny 3498 T t226 o206 b225
615 xiny 3379 B b226 t226
616 xiny 3498 P p226 Number 1854
617     P p227 Number 1860
618     O o227 type_lid p226 p227
619     T t227 o227 b160
620 xiny 3404 B b227 t227
621 xiny 3498 T t228 o204 b226 b227
622 xiny 3404 B b228 t228
623 xiny 3498 P p228 String reduce
624 xiny 3404 O o228 resource p228
625 xiny 3498 P p229 Number 2920
626     P p230 Number 2931
627     O o230 type_prod p229 p230
628     P p231 Number 2924
629     O o231 type_lid p229 p231
630     T t231 o231 b180
631 xiny 3404 B b231 t231
632 xiny 3498 P p232 Number 2927
633     O o232 type_lid p232 p230
634     P p233 String conv
635     O o233 type_lid p233
636     T t233 o233
637     B b233 t233
638     T t234 o232 b233
639 xiny 3379 B b234 t234
640 xiny 3498 T t235 o b234 b4
641 xiny 3404 B b235 t235
642 xiny 3498 T t236 o b231 b235
643 xiny 3404 B b236 t236
644 xiny 3498 T t237 o230 b236
645     B b237 t237
646     P p237 Number 2933
647     P p238 Number 2937
648     O o238 type_lid p237 p238
649     T t238 o238 b233
650     B b238 t238
651     T t239 o228 b237 b238
652     B b239 t239
653     P p239 String squash
654     O o239 resource p239
655     P p240 Number 4017
656     P p241 Number 4028
657     O o241 type_lid p240 p241
658     P p242 String squash_info
659     O o242 type_lid p242
660     T t242 o242
661     B b242 t242
662     T t243 o241 b242
663     B b243 t243
664     P p243 Number 4030
665     P p244 Number 4043
666     O o244 type_fun p243 p244
667     P p245 Number 4033
668     O o245 type_lid p243 p245
669     T t245 o245 b184
670 xiny 3379 B b245 t245
671 xiny 3498 P p246 Number 4037
672     O o246 type_lid p246 p244
673     T t246 o246 b160
674 xiny 3379 B b246 t246
675 xiny 3498 T t247 o244 b245 b246
676 xiny 3379 B b247 t247
677 xiny 3498 T t248 o239 b243 b247
678 xiny 3379 B b248 t248
679 xiny 3498 P p248 String sub
680     O o248 resource p248
681     P p249 Number 4882
682     P p250 Number 4899
683     O o250 type_lid p249 p250
684     P p251 String sub_resource_info
685     O o251 type_lid p251
686     T t251 o251
687     B b251 t251
688     T t252 o250 b251
689 xiny 3379 B b252 t252
690 xiny 3498 P p252 Number 4901
691     P p253 Number 4907
692     O o253 type_lid p252 p253
693     T t253 o253 b160
694 xiny 3379 B b253 t253
695 xiny 3498 T t254 o248 b252 b253
696 xiny 3404 B b254 t254
697 xiny 3498 P p254 String toploop
698     O o254 resource p254
699     P p255 Number 2445
700     P p256 Number 2467
701     O o256 type_prod p255 p256
702     P p257 Number 2451
703     O o257 type_lid p255 p257
704     T t257 o257 b211
705     B b257 t257
706     P p258 Number 2454
707     P p259 Number 2460
708     O o259 type_lid p258 p259
709     T t259 o259 b211
710 xiny 3379 B b259 t259
711 xiny 3498 P p260 Number 2463
712     O o260 type_lid p260 p256
713     P p261 String expr
714     O o261 type_lid p261
715     T t261 o261
716 xiny 3379 B b261 t261
717 xiny 3498 T t262 o260 b261
718 xiny 3379 B b262 t262
719 xiny 3498 T t263 o b262 b4
720 xiny 3404 B b263 t263
721 xiny 3498 T t264 o b259 b263
722 xiny 3404 B b264 t264
723 xiny 3498 T t265 o b257 b264
724     B b265 t265
725     T t266 o256 b265
726     B b266 t266
727     P p266 Number 2469
728     P p267 Number 2478
729     O o267 type_lid p266 p267
730     P p268 String top_table
731     O o268 type_lid p268
732     T t268 o268
733     B b268 t268
734     T t269 o267 b268
735     B b269 t269
736     T t270 o254 b266 b269
737     B b270 t270
738     P p270 String typeinf
739     O o270 resource p270
740     P p271 Number 2151
741     P p272 Number 2172
742     O o272 type_lid p271 p272
743     P p273 String typeinf_resource_info
744     O o273 type_lid p273
745     T t273 o273
746     B b273 t273
747     T t274 o272 b273
748     B b274 t274
749     P p274 Number 2174
750     P p275 Number 2186
751     O o275 type_lid p274 p275
752     P p276 String typeinf_func
753     O o276 type_lid p276
754     T t276 o276
755 xiny 3379 B b276 t276
756 xiny 3498 T t277 o275 b276
757 xiny 3379 B b277 t277
758 xiny 3498 T t278 o270 b274 b277
759 xiny 3379 B b278 t278
760 xiny 3498 P p278 String typeinf_subst
761     O o278 resource p278
762     P p279 Number 1825
763     P p280 Number 1843
764     O o280 type_lid p279 p280
765     P p281 String typeinf_subst_info
766     O o281 type_lid p281
767     T t281 o281
768 xiny 3379 B b281 t281
769 xiny 3498 T t282 o280 b281
770 xiny 3379 B b282 t282
771 xiny 3498 P p282 Number 1862
772     O o282 type_lid p218 p282
773     P p283 String typeinf_subst_fun
774     O o283 type_lid p283
775     T t283 o283
776 xiny 3379 B b283 t283
777 xiny 3498 T t284 o282 b283
778 xiny 3379 B b284 t284
779 xiny 3498 T t285 o278 b282 b284
780 xiny 3379 B b285 t285
781 xiny 3498 T t286 o b285 b4
782 xiny 3379 B b286 t286
783 xiny 3498 T t287 o b278 b286
784 xiny 3404 B b287 t287
785 xiny 3498 T t288 o b270 b287
786 xiny 3404 B b288 t288
787 xiny 3498 T t289 o b254 b288
788     B b289 t289
789     T t290 o b248 b289
790     B b290 t290
791     T t291 o b239 b290
792 xiny 3379 B b291 t291
793 xiny 3498 T t292 o b228 b291
794     B b292 t292
795     T t293 o b204 b292
796 xiny 3379 B b293 t293
797 xiny 3498 T t294 o b195 b293
798 xiny 3379 B b294 t294
799 xiny 3498 T t295 o b176 b294
800 xiny 3379 B b295 t295
801 xiny 3498 T t296 o b168 b295
802 xiny 3379 B b296 t296
803 xiny 3498 T t297 o2 b5 b153 b296
804 xiny 3379 B b297 t297
805 xiny 3498 T t298 o1 b297
806 xiny 3404 B b298 t298
807 xiny 3498 P p298 Number 26
808     P p299 Number 45
809     O o299 location p298 p299
810     P p300 String Czf_itt_set
811     O o300 parent p300
812     T t300 o300
813     B b300 t300
814     T t301 o b300 b4
815     B b301 t301
816     P p301 String Czf_itt_comment
817     O o301 parent p301
818     T t302 o301
819 xiny 3404 B b302 t302
820 xiny 3498 T t303 o b302 b4
821 xiny 3379 B b303 t303
822 xiny 3498 P p303 String Itt_theory
823     O o303 parent p303
824     T t304 o303
825     B b304 t304
826     T t305 o b304 b4
827 xiny 3379 B b305 t305
828 xiny 3498 P p305 String Itt_fset
829     O o305 parent p305
830     T t306 o305
831 xiny 3379 B b306 t306
832 xiny 3498 T t307 o b306 b4
833 xiny 3404 B b307 t307
834 xiny 3498 P p307 String Itt_prop_decide
835     O o307 parent p307
836     T t308 o307
837 xiny 3404 B b308 t308
838 xiny 3498 T t309 o b308 b4
839     B b309 t309
840     P p309 String Itt_derive
841     O o309 parent p309
842     T t310 o309
843     B b310 t310
844     T t311 o b310 b4
845 xiny 3379 B b311 t311
846 xiny 3498 P p311 String Itt_list2
847     O o311 parent p311
848     T t312 o311
849 xiny 3379 B b312 t312
850 xiny 3498 T t313 o b312 b4
851 xiny 3404 B b313 t313
852 xiny 3498 P p313 String Itt_list
853     O o313 parent p313
854     T t314 o313
855 xiny 3404 B b314 t314
856 xiny 3498 T t315 o b314 b4
857     B b315 t315
858     P p315 String Itt_quotient
859     O o315 parent p315
860     T t316 o315
861     B b316 t316
862     T t317 o b316 b4
863 xiny 3379 B b317 t317
864 xiny 3498 P p317 String Itt_esquash
865     O o317 parent p317
866     T t318 o317
867     B b318 t318
868     T t319 o b318 b4
869 xiny 3379 B b319 t319
870 xiny 3498 P p319 String Itt_srec
871     O o319 parent p319
872     T t320 o319
873     B b320 t320
874     T t321 o b320 b4
875 xiny 3379 B b321 t321
876 xiny 3498 P p321 String Itt_prec
877     O o321 parent p321
878     T t322 o321
879 xiny 3379 B b322 t322
880 xiny 3404 T t323 o b322 b4
881 xiny 3379 B b323 t323
882 xiny 3498 P p323 String Itt_w
883     O o323 parent p323
884     T t324 o323
885 xiny 3379 B b324 t324
886 xiny 3498 T t325 o b324 b4
887 xiny 3404 B b325 t325
888 xiny 3498 P p325 String Itt_bunion
889     O o325 parent p325
890     T t326 o325
891 xiny 3379 B b326 t326
892 xiny 3498 T t327 o b326 b4
893     B b327 t327
894     P p327 String Itt_bisect
895     O o327 parent p327
896     T t328 o327
897 xiny 3379 B b328 t328
898 xiny 3498 T t329 o b328 b4
899 xiny 3404 B b329 t329
900 xiny 3498 P p329 String Itt_tunion
901     O o329 parent p329
902     T t330 o329
903 xiny 3404 B b330 t330
904 xiny 3498 T t331 o b330 b4
905     B b331 t331
906     P p331 String Itt_isect
907     O o331 parent p331
908     T t332 o331
909     B b332 t332
910     T t333 o b332 b4
911 xiny 3404 B b333 t333
912 xiny 3498 P p333 String Itt_struct2
913     O o333 parent p333
914     T t334 o333
915 xiny 3379 B b334 t334
916 xiny 3498 T t335 o b334 b4
917     B b335 t335
918     P p335 String Itt_well_founded
919     O o335 parent p335
920     T t336 o335
921 xiny 3379 B b336 t336
922 xiny 3498 T t337 o b336 b4
923 xiny 3404 B b337 t337
924 xiny 3498 P p337 String Itt_int_arith
925     O o337 parent p337
926     T t338 o337
927 xiny 3404 B b338 t338
928 xiny 3498 T t339 o b338 b4
929     B b339 t339
930     P p339 String Itt_atom_bool
931     O o339 parent p339
932     T t340 o339
933     B b340 t340
934     T t341 o b340 b4
935 xiny 3379 B b341 t341
936 xiny 3498 P p341 String Itt_atom
937     O o341 parent p341
938     T t342 o341
939 xiny 3379 B b342 t342
940 xiny 3498 T t343 o b342 b4
941 xiny 3379 B b343 t343
942 xiny 3498 T t344 o b343 b4
943 xiny 3379 B b344 t344
944 xiny 3498 T t345 o b341 b344
945 xiny 3379 B b345 t345
946 xiny 3498 T t346 o b339 b345
947 xiny 3379 B b346 t346
948 xiny 3498 T t347 o b337 b346
949 xiny 3379 B b347 t347
950 xiny 3498 T t348 o b335 b347
951 xiny 3379 B b348 t348
952 xiny 3498 T t349 o b333 b348
953 xiny 3379 B b349 t349
954 xiny 3498 T t350 o b331 b349
955 xiny 3379 B b350 t350
956 xiny 3498 T t351 o b329 b350
957 xiny 3379 B b351 t351
958 xiny 3498 T t352 o b327 b351
959 xiny 3379 B b352 t352
960 xiny 3498 T t353 o b325 b352
961 xiny 3379 B b353 t353
962 xiny 3498 T t354 o b323 b353
963 xiny 3379 B b354 t354
964 xiny 3498 T t355 o b321 b354
965 xiny 3379 B b355 t355
966 xiny 3498 T t356 o b319 b355
967 xiny 3379 B b356 t356
968 xiny 3498 T t357 o b317 b356
969 xiny 3404 B b357 t357
970 xiny 3498 T t358 o b315 b357
971 xiny 3379 B b358 t358
972 xiny 3498 T t359 o b313 b358
973     B b359 t359
974     T t360 o b311 b359
975 xiny 3379 B b360 t360
976 xiny 3498 T t361 o b309 b360
977 xiny 3379 B b361 t361
978 xiny 3498 T t362 o b307 b361
979 xiny 3379 B b362 t362
980 xiny 3498 T t363 o b305 b362
981 xiny 3379 B b363 t363
982 xiny 3498 T t364 o b303 b363
983 xiny 3379 B b364 t364
984 xiny 3498 T t365 o b301 b364
985 xiny 3379 B b365 t365
986 xiny 3498 T t366 o2 b301 b365 b296
987 xiny 3379 B b366 t366
988 xiny 3498 T t367 o299 b366
989 xiny 3379 B b367 t367
990 xiny 3498 P p367 Number 46
991     P p368 Number 68
992 xiny 3379 O o368 location p367 p368
993 xiny 3498 P p369 String Czf_itt_member
994     O o369 parent p369
995     T t369 o369
996 xiny 3379 B b369 t369
997 xiny 3498 T t370 o b369 b4
998     B b370 t370
999     P p370 String Czf_itt_eq
1000     O o370 parent p370
1001     T t371 o370
1002 xiny 3379 B b371 t371
1003     T t372 o b371 b4
1004     B b372 t372
1005 xiny 3498 T t373 o b372 b4
1006 xiny 3379 B b373 t373
1007 xiny 3498 T t374 o b370 b373
1008 xiny 3379 B b374 t374
1009 xiny 3498 T t375 o2 b370 b374 b296
1010 xiny 3379 B b375 t375
1011 xiny 3498 T t376 o368 b375
1012 xiny 3379 B b376 t376
1013 xiny 3498 P p376 Number 69
1014     P p377 Number 87
1015     O o377 location p376 p377
1016     T t377 o2 b372 b4 b296
1017 xiny 3379 B b377 t377
1018 xiny 3498 T t378 o377 b377
1019 xiny 3379 B b378 t378
1020 xiny 3498 P p378 Number 88
1021     P p379 Number 108
1022     O o379 location p378 p379
1023     P p380 String Czf_itt_dall
1024     O o380 parent p380
1025     T t380 o380
1026 xiny 3379 B b380 t380
1027 xiny 3498 T t381 o b380 b4
1028 xiny 3379 B b381 t381
1029 xiny 3498 P p381 String Czf_itt_set_ind
1030     O o381 parent p381
1031     T t382 o381
1032 xiny 3379 B b382 t382
1033 xiny 3498 T t383 o b382 b4
1034 xiny 3404 B b383 t383
1035 xiny 3498 P p383 String Czf_itt_all
1036     O o383 parent p383
1037     T t384 o383
1038 xiny 3379 B b384 t384
1039 xiny 3498 T t385 o b384 b4
1040     B b385 t385
1041     P p385 String Czf_itt_sep
1042     O o385 parent p385
1043     T t386 o385
1044 xiny 3379 B b386 t386
1045 xiny 3404 T t387 o b386 b4
1046 xiny 3379 B b387 t387
1047 xiny 3404 T t388 o b387 b4
1048 xiny 3379 B b388 t388
1049 xiny 3498 T t389 o b385 b388
1050 xiny 3404 B b389 t389
1051 xiny 3498 T t390 o b383 b389
1052 xiny 3404 B b390 t390
1053 xiny 3498 T t391 o b381 b390
1054     B b391 t391
1055     T t392 o2 b381 b391 b296
1056     B b392 t392
1057     T t393 o379 b392
1058     B b393 t393
1059     P p393 Number 109
1060     P p394 Number 128
1061     O o394 location p393 p394
1062     P p395 String Czf_itt_and
1063     O o395 parent p395
1064     T t395 o395
1065 xiny 3379 B b395 t395
1066 xiny 3498 T t396 o b395 b4
1067 xiny 3379 B b396 t396
1068 xiny 3498 T t397 o b396 b4
1069 xiny 3404 B b397 t397
1070 xiny 3498 T t398 o2 b396 b397 b296
1071 xiny 3404 B b398 t398
1072 xiny 3498 T t399 o394 b398
1073     B b399 t399
1074 xiny 3516 P p4 Number 129
1075     P p8 Number 150
1076     O o10 location p4 p8
1077     P p10 String Czf_itt_equiv
1078     O o12 parent p10
1079     T t158 o12
1080     B b158 t158
1081     T t159 o b158 b4
1082     B b159 t159
1083     P p166 String Czf_itt_pair
1084     O o166 parent p166
1085     T t170 o166
1086     B b170 t170
1087     T t173 o b170 b4
1088     B b173 t173
1089     P p188 String Czf_itt_singleton
1090     O o188 parent p188
1091     T t196 o188
1092     B b196 t196
1093     T t197 o b196 b4
1094     B b197 t197
1095     P p201 String Czf_itt_union
1096     O o202 parent p201
1097     T t213 o202
1098     B b213 t213
1099     T t214 o b213 b4
1100     B b214 t214
1101     P p220 String Czf_itt_subset
1102     O o220 parent p220
1103     T t230 o220
1104     B b230 t230
1105     T t232 o b230 b4
1106     B b232 t232
1107     P p236 String Czf_itt_dexists
1108     O o236 parent p236
1109     T t241 o236
1110     B b241 t241
1111     T t244 o b241 b4
1112     B b244 t244
1113     T t249 o b244 b4
1114     B b249 t249
1115     T t250 o b232 b249
1116     B b250 t250
1117     T t255 o b214 b250
1118     B b255 t255
1119     T t256 o b197 b255
1120     B b256 t256
1121     T t258 o b173 b256
1122     B b258 t258
1123     T t260 o b159 b258
1124     B b260 t260
1125     T t402 o2 b159 b260 b296
1126     B b402 t402
1127     T t509 o10 b402
1128     B b509 t509
1129     P p512 Number 152
1130     P p513 Number 163
1131     O o513 location p512 p513
1132 xiny 3498 NSummary!summary_item summary_item summary_item Summary
1133     O o401 summary_item
1134     NOcaml!str_open str_open str_open Ocaml
1135 xiny 3516 O o514 str_open p512 p513
1136 xiny 3498 NOcaml!string string string Ocaml
1137     P p402 String Printf
1138     O o403 string p402
1139     T t403 o403
1140 xiny 3379 B b403 t403
1141 xiny 3498 T t404 o b403 b4
1142 xiny 3404 B b404 t404
1143 xiny 3516 T t574 o514 b404
1144     B b574 t574
1145     T t575 o401 b574
1146     B b575 t575
1147     T t581 o513 b575
1148     B b581 t581
1149     P p589 Number 164
1150     P p590 Number 177
1151     O o590 location p589 p590
1152     O o591 str_open p589 p590
1153 xiny 3498 P p409 String Mp_debug
1154     O o410 string p409
1155     T t410 o410
1156 xiny 3379 B b410 t410
1157 xiny 3498 T t411 o b410 b4
1158 xiny 3379 B b411 t411
1159 xiny 3516 T t599 o591 b411
1160     B b599 t599
1161     T t608 o401 b599
1162     B b608 t608
1163     T t618 o590 b608
1164     B b618 t618
1165     P p618 Number 178
1166     P p619 Number 207
1167     O o619 location p618 p619
1168     O o622 str_open p618 p619
1169 xiny 3498 P p416 String Refiner
1170     O o417 string p416
1171     T t417 o417
1172     B b417 t417
1173     P p417 String TermType
1174 xiny 3404 O o418 string p417
1175     T t418 o418
1176 xiny 3379 B b418 t418
1177 xiny 3404 T t419 o b418 b4
1178 xiny 3379 B b419 t419
1179 xiny 3498 T t420 o b417 b419
1180 xiny 3379 B b420 t420
1181 xiny 3498 T t421 o b417 b420
1182 xiny 3379 B b421 t421
1183 xiny 3516 T t625 o622 b421
1184     B b625 t625
1185     T t642 o401 b625
1186     B b642 t642
1187     T t643 o619 b642
1188     B b643 t643
1189     P p643 Number 208
1190     P p644 Number 233
1191     O o644 location p643 p644
1192     O o647 str_open p643 p644
1193 xiny 3498 P p426 String Term
1194 xiny 3404 O o427 string p426
1195     T t427 o427
1196 xiny 3379 B b427 t427
1197 xiny 3404 T t428 o b427 b4
1198 xiny 3379 B b428 t428
1199 xiny 3498 T t429 o b417 b428
1200 xiny 3379 B b429 t429
1201 xiny 3498 T t430 o b417 b429
1202 xiny 3379 B b430 t430
1203 xiny 3516 T t654 o647 b430
1204     B b654 t654
1205     T t661 o401 b654
1206     B b661 t661
1207     T t666 o644 b661
1208     B b666 t666
1209     P p667 Number 234
1210     P p668 Number 261
1211     O o675 location p667 p668
1212     O o677 str_open p667 p668
1213 xiny 3498 P p435 String TermOp
1214 xiny 3404 O o436 string p435
1215     T t436 o436
1216 xiny 3379 B b436 t436
1217 xiny 3404 T t437 o b436 b4
1218 xiny 3379 B b437 t437
1219 xiny 3498 T t438 o b417 b437
1220 xiny 3379 B b438 t438
1221 xiny 3498 T t439 o b417 b438
1222 xiny 3379 B b439 t439
1223 xiny 3516 T t681 o677 b439
1224     B b681 t681
1225     T t682 o401 b681
1226     B b682 t682
1227     T t683 o675 b682
1228     B b683 t683
1229     P p683 Number 262
1230     P p684 Number 291
1231     O o684 location p683 p684
1232     O o685 str_open p683 p684
1233 xiny 3498 P p444 String TermAddr
1234 xiny 3404 O o445 string p444
1235     T t445 o445
1236 xiny 3379 B b445 t445
1237 xiny 3404 T t446 o b445 b4
1238 xiny 3379 B b446 t446
1239 xiny 3498 T t447 o b417 b446
1240 xiny 3379 B b447 t447
1241 xiny 3498 T t448 o b417 b447
1242 xiny 3379 B b448 t448
1243 xiny 3516 T t685 o685 b448
1244     B b685 t685
1245     T t686 o401 b685
1246     B b686 t686
1247     T t695 o684 b686
1248     B b695 t695
1249     P p695 Number 292
1250     P p696 Number 320
1251     O o696 location p695 p696
1252     O o697 str_open p695 p696
1253 xiny 3498 P p453 String TermMan
1254 xiny 3404 O o454 string p453
1255     T t454 o454
1256 xiny 3379 B b454 t454
1257 xiny 3404 T t455 o b454 b4
1258 xiny 3379 B b455 t455
1259 xiny 3498 T t456 o b417 b455
1260 xiny 3379 B b456 t456
1261 xiny 3498 T t457 o b417 b456
1262 xiny 3379 B b457 t457
1263 xiny 3516 T t697 o697 b457
1264     B b697 t697
1265     T t698 o401 b697
1266     B b698 t698
1267     T t699 o696 b698
1268     B b699 t699
1269     P p699 Number 321
1270     P p700 Number 351
1271     O o700 location p699 p700
1272     O o701 str_open p699 p700
1273 xiny 3498 P p462 String TermSubst
1274 xiny 3404 O o463 string p462
1275     T t463 o463
1276 xiny 3379 B b463 t463
1277 xiny 3404 T t464 o b463 b4
1278 xiny 3379 B b464 t464
1279 xiny 3498 T t465 o b417 b464
1280 xiny 3379 B b465 t465
1281 xiny 3498 T t466 o b417 b465
1282 xiny 3379 B b466 t466
1283 xiny 3516 T t712 o701 b466
1284     B b713 t712
1285     T t713 o401 b713
1286     B b714 t713
1287     T t714 o700 b714
1288     B b715 t714
1289     P p718 Number 352
1290     P p719 Number 379
1291     O o719 location p718 p719
1292     O o723 str_open p718 p719
1293 xiny 3498 P p471 String Refine
1294 xiny 3404 O o472 string p471
1295     T t472 o472
1296 xiny 3379 B b472 t472
1297 xiny 3404 T t473 o b472 b4
1298 xiny 3379 B b473 t473
1299 xiny 3498 T t474 o b417 b473
1300 xiny 3379 B b474 t474
1301 xiny 3498 T t475 o b417 b474
1302 xiny 3379 B b475 t475
1303 xiny 3516 T t734 o723 b475
1304     B b734 t734
1305     T t735 o401 b734
1306     B b735 t735
1307     T t736 o719 b735
1308     B b736 t736
1309     P p736 Number 380
1310     P p737 Number 412
1311     O o737 location p736 p737
1312     O o738 str_open p736 p737
1313 xiny 3498 P p480 String RefineError
1314 xiny 3404 O o481 string p480
1315     T t481 o481
1316 xiny 3379 B b481 t481
1317 xiny 3404 T t482 o b481 b4
1318 xiny 3379 B b482 t482
1319 xiny 3498 T t483 o b417 b482
1320 xiny 3379 B b483 t483
1321 xiny 3498 T t484 o b417 b483
1322 xiny 3404 B b484 t484
1323 xiny 3516 T t738 o738 b484
1324     B b738 t738
1325     T t739 o401 b738
1326     B b739 t739
1327     T t758 o737 b739
1328     B b758 t758
1329     P p758 Number 413
1330     P p759 Number 429
1331     O o759 location p758 p759
1332     O o760 str_open p758 p759
1333 xiny 3498 P p489 String Mp_resource
1334     O o490 string p489
1335     T t490 o490
1336 xiny 3379 B b490 t490
1337 xiny 3498 T t491 o b490 b4
1338 xiny 3404 B b491 t491
1339 xiny 3516 T t760 o760 b491
1340     B b760 t760
1341     T t761 o401 b760
1342     B b761 t761
1343     T t762 o759 b761
1344     B b762 t762
1345     P p762 Number 430
1346     P p763 Number 447
1347     O o763 location p762 p763
1348     O o764 str_open p762 p763
1349 xiny 3498 P p496 String Simple_print
1350     O o497 string p496
1351     T t497 o497
1352 xiny 3379 B b497 t497
1353 xiny 3498 T t498 o b497 b4
1354 xiny 3404 B b498 t498
1355 xiny 3516 T t776 o764 b498
1356     B b776 t776
1357     T t777 o401 b776
1358     B b777 t777
1359     T t778 o763 b777
1360     B b778 t778
1361     P p781 Number 449
1362     P p782 Number 465
1363     O o782 location p781 p782
1364     O o787 str_open p781 p782
1365 xiny 3498 P p503 String Tactic_type
1366     O o504 string p503
1367     T t504 o504
1368 xiny 3379 B b504 t504
1369 xiny 3498 T t505 o b504 b4
1370 xiny 3379 B b505 t505
1371 xiny 3516 T t791 o787 b505
1372     B b791 t791
1373     T t792 o401 b791
1374     B b792 t792
1375     T t793 o782 b792
1376     B b793 t793
1377     P p793 Number 466
1378     P p794 Number 492
1379     O o794 location p793 p794
1380     O o795 str_open p793 p794
1381 xiny 3498 P p510 String Tacticals
1382     O o511 string p510
1383     T t511 o511
1384 xiny 3379 B b511 t511
1385 xiny 3498 T t512 o b511 b4
1386 xiny 3379 B b512 t512
1387 xiny 3498 T t513 o b504 b512
1388 xiny 3379 B b513 t513
1389 xiny 3516 T t795 o795 b513
1390     B b795 t795
1391     T t796 o401 b795
1392     B b796 t796
1393     T t803 o794 b796
1394     B b803 t803
1395     P p803 Number 493
1396     P p804 Number 517
1397     O o804 location p803 p804
1398     O o805 str_open p803 p804
1399 xiny 3498 P p518 String Sequent
1400     O o519 string p518
1401     T t519 o519
1402 xiny 3379 B b519 t519
1403 xiny 3498 T t520 o b519 b4
1404 xiny 3379 B b520 t520
1405 xiny 3498 T t521 o b504 b520
1406 xiny 3379 B b521 t521
1407 xiny 3516 T t805 o805 b521
1408     B b805 t805
1409     T t806 o401 b805
1410     B b806 t806
1411     T t807 o804 b806
1412     B b807 t807
1413     P p807 Number 518
1414 xiny 3498 P p526 String Conversionals
1415     O o527 string p526
1416     T t527 o527
1417 xiny 3379 B b527 t527
1418 xiny 3498 T t528 o b527 b4
1419 xiny 3379 B b528 t528
1420 xiny 3498 T t529 o b504 b528
1421 xiny 3404 B b529 t529
1422 xiny 3498 O o535 string p91
1423     T t535 o535
1424 xiny 3379 B b535 t535
1425 xiny 3498 T t536 o b535 b4
1426 xiny 3404 B b536 t536
1427 xiny 3498 O o542 string p89
1428     T t542 o542
1429 xiny 3379 B b542 t542
1430 xiny 3498 T t543 o b542 b4
1431 xiny 3404 B b543 t543
1432 xiny 3498 P p546 Number 548
1433 xiny 3516 O o807 location p807 p546
1434     O o808 str_open p807 p546
1435     T t808 o808 b529
1436     B b808 t808
1437     T t825 o401 b808
1438     B b825 t825
1439     T t826 o807 b825
1440     B b826 t826
1441     P p826 Number 549
1442     P p827 Number 559
1443     O o827 location p826 p827
1444     O o828 str_open p826 p827
1445     T t828 o828 b536
1446     B b828 t828
1447     T t829 o401 b828
1448     B b829 t829
1449     T t830 o827 b829
1450     B b830 t830
1451     P p830 Number 560
1452     P p831 Number 568
1453     O o831 location p830 p831
1454     O o834 str_open p830 p831
1455     T t843 o834 b543
1456     B b843 t843
1457     T t844 o401 b843
1458     B b844 t844
1459     T t845 o831 b844
1460     B b845 t845
1461     P p845 Number 570
1462 xiny 3498 O o549 string p79
1463     T t549 o549
1464 xiny 3379 B b549 t549
1465 xiny 3498 T t550 o b549 b4
1466 xiny 3404 B b550 t550
1467 xiny 3498 P p554 Number 587
1468 xiny 3516 O o845 location p845 p554
1469     O o846 str_open p845 p554
1470     T t846 o846 b550
1471     B b846 t846
1472     T t847 o401 b846
1473     B b847 t847
1474     T t848 o845 b847
1475     B b848 t848
1476     P p848 Number 588
1477     P p849 Number 609
1478     O o849 location p848 p849
1479     O o851 str_open p848 p849
1480 xiny 3498 O o556 string p81
1481     T t556 o556
1482     B b556 t556
1483     T t557 o b556 b4
1484     B b557 t557
1485 xiny 3516 T t855 o851 b557
1486     B b855 t855
1487     T t856 o401 b855
1488     B b856 t856
1489     T t857 o849 b856
1490     B b857 t857
1491     P p857 Number 611
1492     P p858 Number 628
1493     O o858 location p857 p858
1494 xiny 3379 NSummary!opname opname opname Summary
1495 xiny 3498 P p562 String group
1496     O o562 opname p562
1497 xiny 3379 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1498 xiny 3498 NCzf_itt_group!group group group Czf_itt_group
1499     O o563 group
1500 xiny 3379 Nvar var var NIL
1501 xiny 3498 P p563 Var g
1502     O o564 var p563
1503     T t564 o564
1504 xiny 3404 B b564 t564
1505 xiny 3498 T t565 o563 b564
1506     B b565 t565
1507     T t566 o562 b565
1508     B b566 t566
1509 xiny 3516 T t858 o858 b566
1510     B b858 t858
1511     P p859 Number 629
1512     P p860 Number 644
1513     O o860 location p859 p860
1514 xiny 3498 P p569 String car
1515     O o569 opname p569
1516     NCzf_itt_group!car car car Czf_itt_group
1517     O o570 car
1518     T t570 o570 b564
1519     B b570 t570
1520     T t571 o569 b570
1521     B b571 t571
1522 xiny 3516 T t860 o860 b571
1523     B b860 t860
1524     P p861 Number 685
1525     P p863 Number 707
1526     O o863 location p861 p863
1527 xiny 3498 P p574 String op
1528     O o574 opname p574
1529     NCzf_itt_group!op op op Czf_itt_group
1530     O o575 op
1531     P p575 Var s1
1532     O o576 var p575
1533     T t576 o576
1534 xiny 3404 B b576 t576
1535 xiny 3498 P p576 Var s2
1536     O o577 var p576
1537     T t577 o577
1538     B b577 t577
1539     T t578 o575 b564 b576 b577
1540     B b578 t578
1541     P p582 String id
1542     O o582 opname p582
1543     NCzf_itt_group!id id id Czf_itt_group
1544     O o583 id
1545     T t583 o583 b564
1546 xiny 3379 B b583 t583
1547 xiny 3498 T t584 o582 b583
1548 xiny 3404 B b584 t584
1549 xiny 3498 P p586 Number 722
1550     P p587 String inv
1551     O o587 opname p587
1552     NCzf_itt_group!inv inv inv Czf_itt_group
1553     O o588 inv
1554     P p588 Var s
1555     O o589 var p588
1556     T t589 o589
1557 xiny 3379 B b589 t589
1558 xiny 3498 T t590 o588 b564 b589
1559 xiny 3379 B b590 t590
1560 xiny 3498 P p592 Number 723
1561     NSummary!prec prec prec Summary
1562     P p6 String prec_op
1563     O o8 prec p6
1564     T t154 o8
1565     B b154 t154
1566     NSummary!dform dform dform Summary
1567     P p599 String group_df
1568     O o599 dform p599
1569     NSummary!except_mode_df except_mode_df except_mode_df Summary
1570     P p600 String src
1571     O o600 except_mode_df p600
1572     T t600 o600
1573 xiny 3379 B b600 t600
1574 xiny 3404 T t601 o b600 b4
1575 xiny 3379 B b601 t601
1576 xiny 3498 NSummary!df_term df_term df_term Summary
1577     O o601 df_term
1578     Nslot slot slot NIL
1579     O o602 slot
1580     T t602 o602 b564
1581 xiny 3379 B b602 t602
1582 xiny 3498 NPerv!string string602 string Perv
1583     P p602 String " group"
1584     O o603 string602 p602
1585     T t603 o603
1586 xiny 3379 B b603 t603
1587 xiny 3498 T t604 o b603 b4
1588 xiny 3379 B b604 t604
1589 xiny 3498 T t605 o b602 b604
1590 xiny 3404 B b605 t605
1591 xiny 3498 T t606 o601 b605
1592 xiny 3379 B b606 t606
1593 xiny 3498 T t607 o599 b601 b565 b606
1594     B b607 t607
1595     P p610 String car_df
1596     O o610 dform p610
1597     P p611 String car(
1598     O o611 string602 p611
1599     T t611 o611
1600 xiny 3379 B b611 t611
1601 xiny 3498 P p612 String )
1602     O o612 string602 p612
1603     T t612 o612
1604 xiny 3379 B b612 t612
1605 xiny 3498 T t613 o b612 b4
1606 xiny 3404 B b613 t613
1607 xiny 3498 T t614 o b602 b613
1608 xiny 3404 B b614 t614
1609 xiny 3498 T t615 o b611 b614
1610     B b615 t615
1611     T t616 o601 b615
1612     B b616 t616
1613     T t617 o610 b601 b570 b616
1614 xiny 3379 B b617 t617
1615 xiny 3498 P p620 String id_df
1616     O o620 dform p620
1617     P p621 String id(
1618     O o621 string602 p621
1619     T t621 o621
1620     B b621 t621
1621     T t622 o b621 b614
1622 xiny 3404 B b622 t622
1623 xiny 3498 T t623 o601 b622
1624 xiny 3404 B b623 t623
1625 xiny 3498 T t624 o620 b601 b583 b623
1626     B b624 t624
1627     P p627 String op_df
1628     O o627 dform p627
1629     NSummary!prec_df prec_df prec_df Summary
1630     O o201 prec_df p6
1631     T t205 o201
1632     B b205 t205
1633     NSummary!parens_df parens_df parens_df Summary
1634     O o628 parens_df
1635     T t628 o628
1636     B b628 t628
1637     T t629 o b628 b4
1638     B b629 t629
1639     T t206 o b205 b629
1640     B b206 t206
1641     T t208 o b600 b206
1642     B b208 t208
1643     T t630 o b600 b629
1644     B b630 t630
1645     P p630 String op(
1646     O o630 string602 p630
1647     T t631 o630
1648     B b631 t631
1649     P p631 String "; "
1650     O o631 string602 p631
1651     T t632 o631
1652     B b632 t632
1653     P p645 String inv_df
1654     O o645 dform p645
1655     P p646 String inv(
1656     O o646 string602 p646
1657     T t646 o646
1658     B b646 t646
1659     NSummary!rule rule rule Summary
1660     P p663 String group_type
1661     O o663 rule p663
1662     NSummary!context_param context_param context_param Summary
1663     P p664 String H
1664     O o664 context_param p664
1665     T t664 o664
1666 xiny 3379 B b664 t664
1667 xiny 3498 T t665 o b664 b4
1668 xiny 3494 B b665 t665
1669 xiny 3498 NSummary!meta_implies meta_implies meta_implies Summary
1670     O o665 meta_implies
1671     NSummary!meta_theorem meta_theorem meta_theorem Summary
1672     O o666 meta_theorem
1673     NBase_trivial Base_trivial Base_trivial NIL
1674     NBase_trivial!squash squash squash Base_trivial
1675     O o667 squash
1676     T t667 o667
1677     B b667 t667
1678     T t668 o b667 b4
1679     C h H
1680     NItt_equal Itt_equal Itt_equal NIL
1681     NItt_equal!equal equal equal Itt_equal
1682     O o668 equal
1683     NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1684     NItt_record_label0!label label label Itt_record_label0
1685     O o669 label
1686     T t669 o669
1687     B b669 t669
1688     T t670 o668 b669 b564 b564
1689     S s t668 h
1690     G s t670
1691     B b670 s
1692     T t671 o666 b670
1693     B b671 t671
1694     P p671 Var ext
1695     O o671 var p671
1696     T t672 o671
1697 xiny 3494 B b672 t672
1698 xiny 3498 T t673 o b672 b4
1699     NItt_equal!type type type Itt_equal
1700     O o673 type
1701     T t674 o673 b565
1702     S s674 t673 h
1703     G s674 t674
1704     B b674 s674
1705     T t675 o666 b674
1706     B b675 t675
1707     T t676 o665 b671 b675
1708 xiny 3379 B b676 t676
1709 xiny 3498 NSummary!incomplete incomplete incomplete Summary
1710     O o676 incomplete
1711     T t677 o676
1712     B b677 t677
1713     NSummary!resource_defs resource_defs resource_defs Summary
1714     NOcaml!uid uid uid Ocaml
1715     P p680 String []
1716     O o680 uid p680
1717     T t680 o680
1718 xiny 3379 B b680 t680
1719 xiny 3498 P p688 String car_wf
1720     O o688 rule p688
1721     S s688 t673 h
1722     G s688 t565
1723     B b688 s688
1724     T t688 o666 b688
1725     B b689 t688
1726     NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1727     NCzf_itt_set!isset isset isset Czf_itt_set
1728     O o689 isset
1729     T t689 o689 b570
1730     S s689 t673 h
1731     G s689 t689
1732     B b690 s689
1733     T t690 o666 b690
1734     B b691 t690
1735     T t691 o665 b689 b691
1736     B b692 t691
1737     T t692 o665 b671 b692
1738     B b693 t692
1739     P p287 Number 1528
1740     P p288 Number 1526
1741     P p702 String op_wf1
1742     O o702 rule p702
1743     T t702 o689 b576
1744     S s702 t668 h
1745     G s702 t702
1746     B b702 s702
1747     T t703 o666 b702
1748     B b703 t703
1749     T t704 o689 b577
1750     S s704 t668 h
1751     G s704 t704
1752     B b704 s704
1753     T t705 o666 b704
1754 xiny 3494 B b705 t705
1755 xiny 3498 T t706 o689 b578
1756     S s706 t673 h
1757     G s706 t706
1758     B b706 s706
1759     T t707 o666 b706
1760 xiny 3494 B b707 t707
1761 xiny 3498 T t708 o665 b705 b707
1762 xiny 3494 B b708 t708
1763 xiny 3498 T t709 o665 b703 b708
1764     B b709 t709
1765     T t710 o665 b689 b709
1766     B b710 t710
1767     T t711 o665 b671 b710
1768     B b711 t711
1769     P p720 String op_wf2
1770     O o720 rule p720
1771     NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1772     NCzf_itt_member!mem mem mem Czf_itt_member
1773     O o721 mem
1774     T t721 o721 b576 b570
1775     S s721 t673 h
1776     G s721 t721
1777     B b721 s721
1778     T t722 o666 b721
1779 xiny 3494 B b722 t722
1780 xiny 3498 T t723 o721 b577 b570
1781     S s723 t673 h
1782     G s723 t723
1783     B b723 s723
1784     T t724 o666 b723
1785     B b724 t724
1786     T t725 o721 b578 b570
1787     S s725 t673 h
1788     G s725 t725
1789     B b725 s725
1790     T t726 o666 b725
1791     B b726 t726
1792     T t727 o665 b724 b726
1793     B b727 t727
1794     T t728 o665 b722 b727
1795     B b728 t728
1796     T t729 o665 b689 b728
1797     B b729 t729
1798     T t730 o665 b671 b729
1799 xiny 3494 B b730 t730
1800 xiny 3498 T t731 o665 b705 b730
1801 xiny 3494 B b731 t731
1802 xiny 3498 T t732 o665 b703 b731
1803 xiny 3494 B b732 t732
1804 xiny 3498 P p742 Var s3
1805     O o742 var p742
1806     T t742 o742
1807     B b742 t742
1808     T t743 o689 b742
1809     S s743 t668 h
1810     G s743 t743
1811     B b743 s743
1812     T t744 o666 b743
1813     B b744 t744
1814     NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1815     NCzf_itt_eq!eq eq eq Czf_itt_eq
1816     O o744 eq
1817     T t747 o575 b564 b742 b576
1818     B b747 t747
1819     T t748 o575 b564 b742 b577
1820     B b748 t748
1821     T t765 o575 b564 b576 b742
1822     B b765 t765
1823     T t766 o575 b564 b577 b742
1824 xiny 3494 B b766 t766
1825 xiny 3498 P p783 String op_fun1
1826 xiny 3405 O o783 rule p783
1827 xiny 3498 T t783 o689 b589
1828     S s783 t668 h
1829 xiny 3405 G s783 t783
1830     B b783 s783
1831 xiny 3498 T t784 o666 b783
1832 xiny 3405 B b784 t784
1833 xiny 3498 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1834     O o784 fun_set
1835     P p784 Var z
1836     O o785 var p784
1837     T t785 o785
1838     B b785 t785
1839     T t786 o575 b564 b785 b589
1840     B b786 t786 z
1841     T t787 o784 b786
1842     S s787 t673 h
1843     G s787 t787
1844     B b787 s787
1845     T t788 o666 b787
1846     B b788 t788
1847     T t789 o665 b784 b788
1848     B b789 t789
1849     P p798 String op_fun2
1850     O o798 rule p798
1851     T t798 o575 b564 b589 b785
1852     B b798 t798 z
1853     T t799 o784 b798
1854     S s799 t673 h
1855     G s799 t799
1856     B b799 s799
1857     T t800 o666 b799
1858     B b800 t800
1859     T t801 o665 b784 b800
1860 xiny 3494 B b801 t801
1861 xiny 3498 P p810 String op_assoc1
1862     O o810 rule p810
1863     T t810 o721 b742 b570
1864     S s810 t673 h
1865     G s810 t810
1866     B b810 s810
1867     T t811 o666 b810
1868     B b811 t811
1869     NCzf_itt_eq!equal equal811 equal Czf_itt_eq
1870     O o811 equal811
1871     T t812 o575 b564 b578 b742
1872     B b812 t812
1873     T t813 o575 b564 b576 b766
1874     B b813 t813
1875     P p832 String op_assoc2
1876     O o832 rule p832
1877     P p850 String id_wf1
1878     O o850 rule p850
1879     T t850 o689 b583
1880     S s850 t673 h
1881     G s850 t850
1882     B b850 s850
1883     T t851 o666 b850
1884     B b851 t851
1885     T t852 o665 b689 b851
1886     B b852 t852
1887     T t853 o665 b671 b852
1888     B b853 t853
1889     P p862 String id_wf2
1890     O o862 rule p862
1891     T t862 o721 b583 b570
1892     S s862 t673 h
1893     G s862 t862
1894     B b862 s862
1895     T t863 o666 b862
1896 xiny 3494 B b863 t863
1897 xiny 3498 T t864 o665 b689 b863
1898 xiny 3494 B b864 t864
1899 xiny 3498 T t865 o665 b671 b864
1900     B b865 t865
1901     P p874 String id_eq1
1902     O o874 rule p874
1903     T t874 o721 b589 b570
1904     S s874 t673 h
1905     G s874 t874
1906     B b874 s874
1907     T t875 o666 b874
1908 xiny 3494 B b875 t875
1909 xiny 3498 T t876 o575 b564 b583 b589
1910 xiny 3494 B b876 t876
1911 xiny 3498 P p891 String id_eq2
1912     O o891 rule p891
1913     T t891 o575 b564 b589 b583
1914     B b891 t891
1915     P p906 String inv_wf1
1916 xiny 3405 O o906 rule p906
1917 xiny 3498 T t906 o588 b564 b576
1918 xiny 3405 B b906 t906
1919 xiny 3498 T t907 o689 b906
1920     S s907 t673 h
1921 xiny 3405 G s907 t907
1922     B b907 s907
1923 xiny 3498 T t908 o666 b907
1924 xiny 3405 B b908 t908
1925 xiny 3498 T t909 o665 b722 b908
1926 xiny 3379 B b909 t909
1927 xiny 3498 T t910 o665 b689 b909
1928 xiny 3404 B b910 t910
1929 xiny 3498 T t911 o665 b671 b910
1930     B b911 t911
1931     T t912 o665 b703 b911
1932     B b912 t912
1933     P p921 String inv_wf2
1934     O o921 rule p921
1935     T t921 o721 b906 b570
1936     S s921 t673 h
1937     G s921 t921
1938     B b921 s921
1939     T t922 o666 b921
1940 xiny 3379 B b922 t922
1941 xiny 3498 T t923 o665 b722 b922
1942     B b923 t923
1943     T t924 o665 b689 b923
1944 xiny 3405 B b924 t924
1945 xiny 3498 T t925 o665 b671 b924
1946     B b925 t925
1947     T t926 o665 b703 b925
1948 xiny 3405 B b926 t926
1949 xiny 3498 P p935 String inv_fun1
1950     O o935 rule p935
1951     T t935 o588 b564 b785
1952     B b935 t935 z
1953     T t936 o784 b935
1954     S s936 t673 h
1955     G s936 t936
1956     B b936 s936
1957     T t937 o666 b936
1958     B b937 t937
1959     T t938 o665 b689 b937
1960 xiny 3405 B b938 t938
1961 xiny 3498 T t939 o665 b671 b938
1962 xiny 3404 B b939 t939
1963 xiny 3498 P p948 String inv_id1
1964     O o948 rule p948
1965     T t948 o575 b564 b906 b576
1966     B b948 t948
1967     P p925 Number 6113
1968     P p963 String inv_id2
1969     O o963 rule p963
1970     T t963 o575 b564 b576 b906
1971     B b963 t963
1972     P p978 String cancel1
1973     O o978 rule p978
1974     NSummary!term_param term_param term_param Summary
1975     O o979 term_param
1976     T t979 o979 b564
1977     B b979 t979
1978     T t980 o979 b576
1979 xiny 3405 B b980 t980
1980 xiny 3498 T t981 o b980 b4
1981 xiny 3405 B b981 t981
1982 xiny 3498 T t982 o b979 b981
1983 xiny 3379 B b982 t982
1984 xiny 3498 T t983 o b664 b982
1985 xiny 3379 B b983 t983
1986 xiny 3498 T t984 o811 b578 b765
1987     S s984 t673 h
1988     G s984 t984
1989     B b984 s984
1990     T t986 o811 b577 b742
1991     S s986 t673 h
1992     G s986 t986
1993     B b986 s986
1994     NSummary!interactive interactive interactive Summary
1995     O o996 interactive
1996     NSummary!ext_rule ext_rule ext_rule Summary
1997     P p996 String "assumT 9 thenT assertT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenWT autoT"
1998     O o997 ext_rule p996
1999     NSummary!status_incomplete status_incomplete status_incomplete Summary
2000     O o998 status_incomplete
2001     T t998 o998
2002     B b998 t998
2003     NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2004     O o999 ext_unjustified
2005     NSummary!tactic_arg tactic_arg tactic_arg Summary
2006     P p999 String main
2007     O o1000 tactic_arg p999
2008     NSummary!msequent msequent msequent Summary
2009     O o1001 msequent
2010     T t1001 o b984 b4
2011     B b1001 t1001
2012     T t1002 o b810 b1001
2013     B b1002 t1002
2014     T t1003 o b723 b1002
2015     B b1003 t1003
2016     T t1004 o b721 b1003
2017     B b1004 t1004
2018     T t1005 o b688 b1004
2019     B b1005 t1005
2020     T t1006 o b670 b1005
2021     B b1006 t1006
2022     T t1007 o b743 b1006
2023     B b1007 t1007
2024     T t1008 o b704 b1007
2025     B b1008 t1008
2026     T t1009 o b702 b1008
2027     B b1009 t1009
2028     T t1010 o1001 b986 b1009
2029     B b1010 t1010
2030     NSummary!parent_none parent_none parent_none Summary
2031     O o1010 parent_none
2032     T t1011 o1010
2033     B b1011 t1011
2034     T t1012 o1000 b1010 b4 b1011
2035     B b1012 t1012
2036     P p1012 String assertion
2037     O o1012 tactic_arg p1012
2038     H h1012 v t984
2039     T t1013 o575 b564 b906 b578
2040     B b1013 t1013
2041     T t1014 o575 b564 b906 b765
2042     B b1014 t1014
2043     T t1015 o811 b1013 b1014
2044     S s1015 t673 h h1012
2045     G s1015 t1015
2046     B b1015 s1015
2047     T t1016 o1001 b1015 b1009
2048     B b1016 t1016
2049     S s1016 t673 h h1012
2050     G s1016 t986
2051     B b1017 s1016
2052     T t1017 o1001 b1017 b1009
2053 xiny 3379 B b1018 t1017
2054 xiny 3498 T t1018 o2 b1012
2055     B b1019 t1018
2056     T t1019 o1000 b1018 b4 b1019
2057 xiny 3405 B b1020 t1019
2058 xiny 3498 T t1020 o2 b1020
2059 xiny 3404 B b1021 t1020
2060 xiny 3498 T t1021 o1012 b1016 b4 b1021
2061 xiny 3379 B b1022 t1021
2062 xiny 3498 H h1022 v_1 t1015
2063     S s1022 t673 h h1012 h1022
2064     G s1022 t986
2065     B b1023 s1022
2066     T t1023 o1001 b1023 b1009
2067 xiny 3379 B b1024 t1023
2068 xiny 3498 T t1024 o1000 b1024 b4 b1021
2069     B b1025 t1024
2070     T t1025 o b1025 b4
2071 xiny 3405 B b1026 t1025
2072 xiny 3498 T t1026 o b1022 b1026
2073 xiny 3379 B b1027 t1026
2074 xiny 3498 T t1027 o999 b1012 b1027
2075 xiny 3379 B b1028 t1027
2076 xiny 3498 P p1028 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2077     O o1028 ext_rule p1028
2078     T t1028 o999 b1022 b4
2079     B b1029 t1028
2080     T t1029 o1028 b998 b1029 b4 b4
2081     B b1030 t1029
2082     P p1030 String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 3 thenAT autoT"
2083     O o1030 ext_rule p1030
2084     T t1030 o575 b564 b948 b577
2085 xiny 3405 B b1031 t1030
2086 xiny 3498 T t1031 o811 b1031 b1014
2087     H h1031 v_2 t1031
2088     S s1031 t673 h h1012 h1022 h1031
2089     G s1031 t986
2090     B b1032 s1031
2091     T t1032 o1001 b1032 b1009
2092     B b1033 t1032
2093     T t1033 o2 b1025
2094     B b1034 t1033
2095     T t1034 o1000 b1033 b4 b1034
2096 xiny 3405 B b1035 t1034
2097 xiny 3498 T t1035 o b1035 b4
2098 xiny 3379 B b1036 t1035
2099 xiny 3498 T t1036 o999 b1025 b1036
2100 xiny 3379 B b1037 t1036
2101 xiny 3498 P p1037 String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 4 thenAT autoT"
2102     O o1037 ext_rule p1037
2103     T t1037 o575 b564 b948 b742
2104 xiny 3379 B b1038 t1037
2105 xiny 3498 T t1038 o811 b1031 b1038
2106     H h1038 v_3 t1038
2107     S s1038 t673 h h1012 h1022 h1031 h1038
2108     G s1038 t986
2109     B b1039 s1038
2110     T t1039 o1001 b1039 b1009
2111     B b1040 t1039
2112     T t1040 o2 b1035
2113     B b1041 t1040
2114     T t1041 o1000 b1040 b4 b1041
2115     B b1042 t1041
2116     T t1042 o b1042 b4
2117 xiny 3405 B b1043 t1042
2118 xiny 3498 T t1043 o999 b1035 b1043
2119 xiny 3379 B b1044 t1043
2120 xiny 3498 P p1044 String "setSubstT << equal{op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 thenAT autoT"
2121     O o1044 ext_rule p1044
2122     T t1044 o575 b564 b583 b577
2123 xiny 3379 B b1045 t1044
2124 xiny 3498 T t1045 o575 b564 b583 b742
2125 xiny 3379 B b1046 t1045
2126 xiny 3498 T t1046 o811 b1045 b1046
2127     H h1046 v_4 t1046
2128     S s1046 t673 h h1012 h1022 h1031 h1038 h1046
2129     G s1046 t986
2130     B b1047 s1046
2131     T t1047 o1001 b1047 b1009
2132 xiny 3379 B b1048 t1047
2133 xiny 3498 T t1048 o2 b1042
2134 xiny 3379 B b1049 t1048
2135 xiny 3498 T t1049 o1000 b1048 b4 b1049
2136 xiny 3379 B b1050 t1049
2137 xiny 3498 T t1050 o b1050 b4
2138     B b1051 t1050
2139     T t1051 o999 b1042 b1051
2140     B b1052 t1051
2141     P p1052 String "setSubstT << equal{op{'g; id{'g}; 's2}; 's2} >> 6 thenAT autoT"
2142     O o1052 ext_rule p1052
2143     T t1052 o811 b577 b1046
2144     H h1052 v_5 t1052
2145     S s1052 t673 h h1012 h1022 h1031 h1038 h1046 h1052
2146     G s1052 t986
2147     B b1053 s1052
2148     T t1053 o1001 b1053 b1009
2149 xiny 3379 B b1054 t1053
2150 xiny 3498 T t1054 o2 b1050
2151     B b1055 t1054
2152     T t1055 o1000 b1054 b4 b1055
2153     B b1056 t1055
2154     T t1056 o b1056 b4
2155 xiny 3405 B b1057 t1056
2156 xiny 3498 T t1057 o999 b1050 b1057
2157 xiny 3379 B b1058 t1057
2158 xiny 3498 P p1058 String "setSubstT << equal{op{'g; id{'g}; 's3}; 's3} >> 7 thenT autoT"
2159     O o1058 ext_rule p1058
2160     T t1058 o999 b1056 b4
2161 xiny 3379 B b1059 t1058
2162 xiny 3498 T t1059 o1058 b998 b1059 b4 b4
2163 xiny 3379 B b1060 t1059
2164 xiny 3498 T t1060 o b1060 b4
2165 xiny 3379 B b1061 t1060
2166 xiny 3498 T t1061 o1052 b998 b1058 b1061 b4
2167 xiny 3404 B b1062 t1061
2168 xiny 3405 T t1062 o b1062 b4
2169 xiny 3404 B b1063 t1062
2170 xiny 3498 T t1063 o1044 b998 b1052 b1063 b4
2171 xiny 3404 B b1064 t1063
2172 xiny 3498 T t1064 o b1064 b4
2173 xiny 3404 B b1065 t1064
2174 xiny 3498 T t1065 o1037 b998 b1044 b1065 b4
2175 xiny 3404 B b1066 t1065
2176 xiny 3405 T t1066 o b1066 b4
2177 xiny 3404 B b1067 t1066
2178 xiny 3498 T t1067 o1030 b998 b1037 b1067 b4
2179     B b1068 t1067
2180     T t1068 o b1068 b4
2181     B b1069 t1068
2182     T t1069 o b1030 b1069
2183     B b1070 t1069
2184     T t1070 o997 b998 b1028 b1070 b4
2185     B b1071 t1070
2186     T t1071 o996 b1071
2187 xiny 3404 B b1072 t1071
2188 xiny 3498 P p1081 String cancel2
2189     O o1081 rule p1081
2190     T t1081 o979 b742
2191     B b1081 t1081
2192     T t1082 o b1081 b4
2193     B b1082 t1082
2194     T t1083 o b979 b1082
2195     B b1083 t1083
2196     T t1084 o b664 b1083
2197     B b1084 t1084
2198     T t1085 o811 b765 b766
2199     S s1085 t673 h
2200     G s1085 t1085
2201     B b1085 s1085
2202     T t1087 o811 b576 b577
2203     S s1087 t673 h
2204     G s1087 t1087
2205     B b1087 s1087
2206     P p1097 String "assumT 9 thenT assertT << equal{op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}} >> thenT autoT"
2207     O o1097 ext_rule p1097
2208     T t1098 o b1085 b4
2209     B b1098 t1098
2210     T t1099 o b810 b1098
2211     B b1099 t1099
2212     T t1100 o b723 b1099
2213     B b1100 t1100
2214     T t1101 o b721 b1100
2215     B b1101 t1101
2216     T t1102 o b688 b1101
2217     B b1102 t1102
2218     T t1103 o b670 b1102
2219     B b1103 t1103
2220     T t1104 o b743 b1103
2221     B b1104 t1104
2222     T t1105 o b704 b1104
2223     B b1105 t1105
2224     T t1106 o b702 b1105
2225     B b1106 t1106
2226     T t1107 o1001 b1087 b1106
2227     B b1107 t1107
2228     T t1108 o1000 b1107 b4 b1011
2229     B b1108 t1108
2230     H h1108 v t1085
2231     T t1109 o588 b564 b742
2232     B b1109 t1109
2233     T t1110 o575 b564 b765 b1109
2234     B b1110 t1110
2235     T t1111 o575 b564 b766 b1109
2236     B b1111 t1111
2237     T t1112 o811 b1110 b1111
2238     S s1112 t673 h h1108
2239     G s1112 t1112
2240     B b1112 s1112
2241     T t1113 o1001 b1112 b1106
2242     B b1113 t1113
2243     S s1113 t673 h h1108
2244     G s1113 t1087
2245 xiny 3405 B b1114 s1113
2246 xiny 3498 T t1114 o1001 b1114 b1106
2247 xiny 3405 B b1115 t1114
2248 xiny 3498 T t1115 o2 b1108
2249     B b1116 t1115
2250     T t1116 o1000 b1115 b4 b1116
2251 xiny 3405 B b1117 t1116
2252 xiny 3498 T t1117 o2 b1117
2253     B b1118 t1117
2254     T t1118 o1012 b1113 b4 b1118
2255 xiny 3405 B b1119 t1118
2256 xiny 3498 H h1119 v_1 t1112
2257     S s1119 t673 h h1108 h1119
2258     G s1119 t1087
2259 xiny 3405 B b1120 s1119
2260 xiny 3498 T t1120 o1001 b1120 b1106
2261 xiny 3405 B b1121 t1120
2262 xiny 3498 T t1121 o1000 b1121 b4 b1118
2263     B b1122 t1121
2264     T t1122 o b1122 b4
2265 xiny 3405 B b1123 t1122
2266 xiny 3498 T t1123 o b1119 b1123
2267 xiny 3379 B b1124 t1123
2268 xiny 3498 T t1124 o999 b1108 b1124
2269 xiny 3379 B b1125 t1124
2270 xiny 3498 T t1125 o999 b1119 b4
2271 xiny 3379 B b1126 t1125
2272 xiny 3498 T t1126 o1028 b998 b1126 b4 b4
2273 xiny 3379 B b1127 t1126
2274 xiny 3498 P p1127 String "setSubstT << equal{op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 3 thenT autoT"
2275     O o1127 ext_rule p1127
2276     T t1127 o575 b564 b742 b1109
2277 xiny 3379 B b1128 t1127
2278 xiny 3498 T t1128 o575 b564 b576 b1128
2279 xiny 3379 B b1129 t1128
2280 xiny 3498 T t1129 o811 b1129 b1111
2281     H h1129 v_2 t1129
2282     S s1129 t673 h h1108 h1119 h1129
2283     G s1129 t1087
2284     B b1130 s1129
2285     T t1130 o1001 b1130 b1106
2286 xiny 3404 B b1131 t1130
2287 xiny 3498 T t1131 o2 b1122
2288 xiny 3379 B b1132 t1131
2289 xiny 3498 T t1132 o1000 b1131 b4 b1132
2290 xiny 3379 B b1133 t1132
2291 xiny 3498 T t1133 o b1133 b4
2292 xiny 3379 B b1134 t1133
2293 xiny 3498 T t1134 o999 b1122 b1134
2294 xiny 3404 B b1135 t1134
2295 xiny 3498 P p1135 String "setSubstT << equal{op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 4 thenT autoT"
2296     O o1135 ext_rule p1135
2297     T t1135 o575 b564 b577 b1128
2298 xiny 3404 B b1136 t1135
2299 xiny 3498 T t1136 o811 b1129 b1136
2300     H h1136 v_3 t1136
2301     S s1136 t673 h h1108 h1119 h1129 h1136
2302     G s1136 t1087
2303     B b1137 s1136
2304     T t1137 o1001 b1137 b1106
2305 xiny 3404 B b1138 t1137
2306 xiny 3498 T t1138 o2 b1133
2307 xiny 3404 B b1139 t1138
2308 xiny 3498 T t1139 o1000 b1138 b4 b1139
2309 xiny 3379 B b1140 t1139
2310 xiny 3405 T t1140 o b1140 b4
2311 xiny 3379 B b1141 t1140
2312 xiny 3498 T t1141 o999 b1133 b1141
2313 xiny 3379 B b1142 t1141
2314 xiny 3498 P p1142 String "setSubstT << equal{op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 5 thenT autoT"
2315     O o1142 ext_rule p1142
2316     T t1142 o575 b564 b576 b583
2317 xiny 3379 B b1143 t1142
2318 xiny 3498 T t1143 o575 b564 b577 b583
2319     B b1144 t1143
2320     T t1144 o811 b1143 b1144
2321     H h1144 v_4 t1144
2322     S s1144 t673 h h1108 h1119 h1129 h1136 h1144
2323     G s1144 t1087
2324 xiny 3405 B b1145 s1144
2325 xiny 3498 T t1145 o1001 b1145 b1106
2326 xiny 3405 B b1146 t1145
2327 xiny 3498 T t1146 o2 b1140
2328 xiny 3379 B b1147 t1146
2329 xiny 3498 T t1147 o1000 b1146 b4 b1147
2330     B b1148 t1147
2331     T t1148 o b1148 b4
2332     B b1149 t1148
2333     T t1149 o999 b1140 b1149
2334 xiny 3405 B b1150 t1149
2335 xiny 3498 P p1150 String "setSubstT << equal{op{'g; 's1; id{'g}}; 's1} >> 6 thenT autoT"
2336     O o1150 ext_rule p1150
2337     T t1150 o811 b576 b1144
2338     H h1150 v_5 t1150
2339     S s1150 t673 h h1108 h1119 h1129 h1136 h1144 h1150
2340     G s1150 t1087
2341     B b1151 s1150
2342     T t1151 o1001 b1151 b1106
2343 xiny 3379 B b1152 t1151
2344 xiny 3498 T t1152 o2 b1148
2345 xiny 3379 B b1153 t1152
2346 xiny 3498 T t1153 o1000 b1152 b4 b1153
2347 xiny 3379 B b1154 t1153
2348 xiny 3498 T t1154 o b1154 b4
2349 xiny 3404 B b1155 t1154
2350 xiny 3498 T t1155 o999 b1148 b1155
2351 xiny 3379 B b1156 t1155
2352 xiny 3498 P p1156 String "setSubstT << equal{op{'g; 's2; id{'g}}; 's2} >> 7 thenT autoT"
2353     O o1156 ext_rule p1156
2354     T t1156 o999 b1154 b4
2355 xiny 3379 B b1157 t1156
2356 xiny 3498 T t1157 o1156 b998 b1157 b4 b4
2357 xiny 3379 B b1158 t1157
2358 xiny 3498 T t1158 o b1158 b4
2359 xiny 3404 B b1159 t1158
2360 xiny 3498 T t1159 o1150 b998 b1156 b1159 b4
2361 xiny 3404 B b1160 t1159
2362 xiny 3498 T t1160 o b1160 b4
2363     B b1161 t1160
2364     T t1161 o1142 b998 b1150 b1161 b4
2365 xiny 3405 B b1162 t1161
2366 xiny 3498 T t1162 o b1162 b4
2367 xiny 3404 B b1163 t1162
2368 xiny 3498 T t1163 o1135 b998 b1142 b1163 b4
2369 xiny 3379 B b1164 t1163
2370 xiny 3498 T t1164 o b1164 b4
2371 xiny 3379 B b1165 t1164
2372 xiny 3498 T t1165 o1127 b998 b1135 b1165 b4
2373     B b1166 t1165
2374     T t1166 o b1166 b4
2375     B b1167 t1166
2376     T t1167 o b1127 b1167
2377 xiny 3405 B b1168 t1167
2378 xiny 3498 T t1168 o1097 b998 b1125 b1168 b4
2379 xiny 3379 B b1169 t1168
2380 xiny 3498 T t1169 o996 b1169
2381     B b1170 t1169
2382     NOcaml!str_let str_let str_let Ocaml
2383     NOcaml!patt_var patt_var patt_var Ocaml
2384     NOcaml!patt_done patt_done patt_done Ocaml
2385     NOcaml!fun fun fun Ocaml
2386     NOcaml!patt_if patt_if patt_if Ocaml
2387     NOcaml!patt_body patt_body patt_body Ocaml
2388     NOcaml!apply apply apply Ocaml
2389     NOcaml!lid lid lid Ocaml
2390     O o1194 lid p978
2391     T t1194 o1194
2392     B b1194 t1194
2393     NOcaml!proj proj proj Ocaml
2394     O o1199 uid p518
2395     T t1199 o1199
2396     B b1199 t1199
2397     P p1201 String hyp_count_addr
2398     O o1201 lid p1201
2399     T t1201 o1201
2400     B b1201 t1201
2401     P p1204 Var p
2402     O o1204 var p1204
2403     T t1204 o1204
2404     B b1204 t1204
2405     P p1208 Var t1
2406     O o1208 var p1208
2407     T t1208 o1208
2408     B b1208 t1208
2409     P p1211 Var t2
2410     O o1211 var p1211
2411     T t1211 o1211
2412     B b1211 t1211
2413     O o1249 lid p1081
2414     T t1249 o1249
2415     B b1249 t1249
2416     P p1283 String unique_id1
2417     O o1283 rule p1283
2418     P p1284 Var e2
2419     O o1284 var p1284
2420     T t1284 o1284
2421     B b1284 t1284
2422     T t1285 o689 b1284
2423     S s1285 t668 h
2424     G s1285 t1285
2425     B b1285 s1285
2426     T t1286 o666 b1285
2427     B b1286 t1286
2428     T t1287 o721 b1284 b570
2429     S s1287 t673 h
2430     G s1287 t1287
2431     B b1287 s1287
2432     T t1288 o666 b1287
2433     B b1288 t1288
2434     NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
2435     NCzf_itt_dall!dall dall dall Czf_itt_dall
2436     O o1288 dall
2437 xiny 3404 NItt_logic Itt_logic Itt_logic NIL
2438     NItt_logic!and and and Itt_logic
2439 xiny 3498 O o1289 and
2440     T t1289 o575 b564 b1284 b589
2441     B b1289 t1289
2442     T t1290 o744 b1289 b589
2443     B b1290 t1290
2444     T t1291 o575 b564 b589 b1284
2445     B b1291 t1291
2446     T t1292 o744 b1291 b589
2447     B b1292 t1292
2448     T t1293 o1289 b1290 b1292
2449     B b1293 t1293 s
2450     T t1294 o1288 b570 b1293
2451     S s1294 t673 h
2452 xiny 3405 G s1294 t1294
2453 xiny 3498 B b1294 s1294
2454     T t1296 o744 b1284 b583
2455     S s1296 t673 h
2456     G s1296 t1296
2457     B b1296 s1296
2458     P p1302 String "assumT 5 thenT withT << id{'g} >> (dT 2) thenT autoT"
2459     O o1302 ext_rule p1302
2460     T t1303 o b1294 b4
2461     B b1303 t1303
2462     T t1304 o b1287 b1303
2463     B b1304 t1304
2464     T t1305 o b688 b1304
2465     B b1305 t1305
2466     T t1306 o b670 b1305
2467     B b1306 t1306
2468     T t1307 o b1285 b1306
2469     B b1307 t1307
2470     T t1308 o1001 b1296 b1307
2471     B b1308 t1308
2472     T t1309 o1000 b1308 b4 b1011
2473     B b1309 t1309
2474     H h1309 v t1294
2475     T t1310 o575 b564 b1284 b583
2476     B b1310 t1310
2477     T t1311 o744 b1310 b583
2478     H h1311 y t1311
2479     T t1312 o575 b564 b583 b1284
2480     B b1312 t1312
2481     T t1313 o744 b1312 b583
2482     H h1313 z t1313
2483     S s1313 t673 h h1309 h1311 h1313
2484     G s1313 t1296
2485     B b1313 s1313
2486     T t1314 o1001 b1313 b1307
2487     B b1314 t1314
2488     B b1315 t1311
2489     B b1316 t1313
2490     T t1316 o1289 b1315 b1316
2491     H h1316 w t1316
2492     S s1316 t673 h h1309 h1316
2493     G s1316 t1296
2494     B b1317 s1316
2495     T t1317 o1001 b1317 b1307
2496 xiny 3404 B b1318 t1317
2497 xiny 3498 S s1318 t673 h h1309
2498     G s1318 t1296
2499     B b1319 s1318
2500     T t1319 o1001 b1319 b1307
2501     B b1320 t1319
2502     NSummary!arg_named arg_named arg_named Summary
2503     P p1320 String with
2504     O o1320 arg_named p1320
2505     NSummary!arg_term_list arg_term_list arg_term_list Summary
2506     O o1321 arg_term_list
2507     T t1321 o b583 b4
2508     B b1321 t1321
2509     T t1322 o1321 b1321
2510     B b1322 t1322
2511     T t1323 o1320 b1322
2512     B b1323 t1323
2513     T t1324 o b1323 b4
2514     B b1324 t1324
2515     T t1325 o2 b1309
2516     B b1325 t1325
2517     T t1326 o1000 b1320 b1324 b1325
2518     B b1326 t1326
2519     T t1327 o2 b1326
2520     B b1327 t1327
2521     T t1328 o1000 b1318 b4 b1327
2522     B b1328 t1328
2523     T t1329 o2 b1328
2524     B b1329 t1329
2525     T t1330 o1000 b1314 b4 b1329
2526     B b1330 t1330
2527     T t1331 o b1330 b4
2528     B b1331 t1331
2529     T t1332 o999 b1309 b1331
2530     B b1332 t1332
2531     P p1332 String "setSubstT << equal{op{'g; id{'g}; 'e2}; 'e2} >> 4 thenT autoT"
2532     O o1332 ext_rule p1332
2533     T t1333 o999 b1330 b4
2534     B b1333 t1333
2535     T t1334 o1332 b998 b1333 b4 b4
2536     B b1334 t1334
2537     T t1335 o b1334 b4
2538     B b1335 t1335
2539     T t1336 o1302 b998 b1332 b1335 b4
2540     B b1336 t1336
2541     T t1337 o996 b1336
2542     B b1337 t1337
2543     P p1346 String unique_id2
2544     O o1346 rule p1346
2545     B b1346 t1290 s
2546     T t1346 o1288 b570 b1346
2547     S s1346 t673 h
2548     G s1346 t1346
2549     B b1347 s1346
2550     P p1353 String "assumT 5"
2551     O o1353 ext_rule p1353
2552     T t1353 o b1347 b4
2553     B b1354 t1353
2554     T t1354 o b1287 b1354
2555     B b1355 t1354
2556     T t1355 o b688 b1355
2557     B b1356 t1355
2558     T t1356 o b670 b1356
2559     B b1357 t1356
2560     T t1357 o b1285 b1357
2561     B b1358 t1357
2562     T t1358 o1001 b1296 b1358
2563     B b1359 t1358
2564     T t1359 o1000 b1359 b4 b1011
2565     B b1360 t1359
2566     H h1360 v t1346
2567     S s1360 t673 h h1360
2568     G s1360 t1296
2569     B b1361 s1360
2570     T t1361 o1001 b1361 b1358
2571     B b1362 t1361
2572     T t1362 o2 b1360
2573     B b1363 t1362
2574     T t1363 o1000 b1362 b4 b1363
2575     B b1364 t1363
2576     T t1364 o b1364 b4
2577     B b1365 t1364
2578     T t1365 o999 b1360 b1365
2579     B b1366 t1365
2580     P p1366 String "withT << id{'g} >> (dT 2) thenAT autoT"
2581     O o1366 ext_rule p1366
2582     H h1366 w t1311
2583     S s1366 t673 h h1360 h1366
2584     G s1366 t1296
2585     B b1367 s1366
2586     T t1367 o1001 b1367 b1358
2587     B b1368 t1367
2588     T t1368 o1000 b1362 b1324 b1363
2589     B b1369 t1368
2590     T t1369 o2 b1369
2591     B b1370 t1369
2592     T t1370 o1000 b1368 b4 b1370
2593     B b1371 t1370
2594     T t1371 o b1371 b4
2595     B b1372 t1371
2596     T t1372 o999 b1364 b1372
2597     B b1373 t1372
2598     P p1373 String "setSubstT << equal{op{'g; 'e2; id{'g}}; 'e2} >> 3 thenT autoT"
2599     O o1373 ext_rule p1373
2600     T t1373 o999 b1371 b4
2601     B b1374 t1373
2602     T t1374 o1373 b998 b1374 b4 b4
2603 xiny 3404 B b1375 t1374
2604 xiny 3498 T t1375 o b1375 b4
2605 xiny 3404 B b1376 t1375
2606 xiny 3498 T t1376 o1366 b998 b1373 b1376 b4
2607     B b1377 t1376
2608     T t1377 o b1377 b4
2609     B b1378 t1377
2610     T t1378 o1353 b998 b1366 b1378 b4
2611     B b1379 t1378
2612     T t1379 o996 b1379
2613 xiny 3405 B b1380 t1379
2614 xiny 3498 P p2068 Number 9097
2615     P p1432 String unique_inv1
2616 xiny 3405 O o1432 rule p1432
2617 xiny 3498 T t1432 o575 b564 b577 b589
2618 xiny 3405 B b1432 t1432
2619 xiny 3498 T t1433 o811 b1432 b583
2620     S s1433 t673 h
2621     G s1433 t1433
2622     B b1433 s1433
2623     T t1435 o811 b577 b590
2624     S s1435 t673 h
2625 xiny 3405 G s1435 t1435
2626     B b1435 s1435
2627 xiny 3498 P p1443 String "assumT 7 thenT setSubstT << equal{id{'g}; op{'g; inv{'g; 's}; 's}}>> 2 thenAT autoT"
2628     O o1443 ext_rule p1443
2629     T t1444 o b1433 b4
2630     B b1444 t1444
2631     T t1445 o b723 b1444
2632     B b1445 t1445
2633     T t1446 o b874 b1445
2634     B b1446 t1446
2635     T t1447 o b688 b1446
2636     B b1447 t1447
2637     T t1448 o b670 b1447
2638     B b1448 t1448
2639     T t1449 o b704 b1448
2640     B b1449 t1449
2641     T t1450 o b783 b1449
2642     B b1450 t1450
2643     T t1451 o1001 b1435 b1450
2644     B b1451 t1451
2645     T t1452 o1000 b1451 b4 b1011
2646     B b1452 t1452
2647     P p1452 String eq
2648     O o1452 tactic_arg p1452
2649     H h1452 v t1433
2650     T t1453 o575 b564 b590 b589
2651     B b1453 t1453
2652     T t1454 o744 b583 b1453
2653     S s1454 t673 h h1452
2654     G s1454 t1454
2655     B b1454 s1454
2656     T t1455 o1001 b1454 b1450
2657     B b1455 t1455
2658     T t1456 o811 b583 b1453
2659     S s1456 t673 h h1452
2660     G s1456 t1456
2661     B b1456 s1456
2662     T t1457 o1001 b1456 b1450
2663     B b1457 t1457
2664     P p1457 String d_auto
2665     O o1457 arg_named p1457
2666     NSummary!arg_bool arg_bool arg_bool Summary
2667     P p1458 String true
2668     O o1458 arg_bool p1458
2669     T t1458 o1458
2670     B b1458 t1458
2671     T t1459 o1457 b1458
2672     B b1459 t1459
2673     T t1460 o b1459 b4
2674     B b1460 t1460
2675     S s1460 t673 h h1452
2676     G s1460 t1435
2677     B b1461 s1460
2678     T t1461 o1001 b1461 b1450
2679 xiny 3379 B b1462 t1461
2680 xiny 3498 T t1462 o2 b1452
2681 xiny 3379 B b1463 t1462
2682 xiny 3498 T t1463 o1000 b1462 b4 b1463
2683 xiny 3379 B b1464 t1463
2684 xiny 3498 T t1464 o2 b1464
2685 xiny 3379 B b1465 t1464
2686 xiny 3498 T t1465 o1452 b1457 b1460 b1465
2687     B b1466 t1465
2688     T t1466 o2 b1466
2689 xiny 3405 B b1467 t1466
2690 xiny 3498 T t1467 o1452 b1455 b4 b1467
2691 xiny 3404 B b1468 t1467
2692 xiny 3498 T t1468 o811 b1432 b1453
2693     H h1468 v_1 t1468
2694     S s1468 t673 h h1452 h1468
2695     G s1468 t1435
2696     B b1469 s1468
2697     T t1469 o1001 b1469 b1450
2698 xiny 3404 B b1470 t1469
2699 xiny 3498 T t1470 o1000 b1470 b4 b1465
2700 xiny 3404 B b1471 t1470
2701 xiny 3498 T t1471 o b1471 b4
2702 xiny 3404 B b1472 t1471
2703 xiny 3498 T t1472 o b1468 b1472
2704 xiny 3404 B b1473 t1472
2705 xiny 3498 T t1473 o999 b1452 b1473
2706 xiny 3404 B b1474 t1473
2707 xiny 3498 P p1474 String "assertT << equal{op{'g; inv{'g; 's}; 's}; id{'g}}>> thenT autoT"
2708     O o1474 ext_rule p1474
2709     T t1474 o811 b1453 b583
2710     H h1474 v_1 t1474
2711     S s1474 t673 h h1452 h1474
2712     G s1474 t1454
2713     B b1475 s1474
2714     T t1475 o1001 b1475 b1450
2715     B b1476 t1475
2716     T t1476 o2 b1468
2717 xiny 3405 B b1477 t1476
2718 xiny 3498 T t1477 o1000 b1476 b4 b1477
2719 xiny 3404 B b1478 t1477
2720 xiny 3498 T t1478 o b1478 b4
2721 xiny 3404 B b1479 t1478
2722 xiny 3498 T t1479 o999 b1468 b1479
2723     B b1480 t1479
2724     P p1480 String "rwh unfold_equal 3 thenT eqSetSymT thenT autoT"
2725     O o1480 ext_rule p1480
2726     T t1480 o999 b1478 b4
2727     B b1481 t1480
2728     T t1481 o1480 b998 b1481 b4 b4
2729 xiny 3405 B b1482 t1481
2730 xiny 3498 T t1482 o b1482 b4
2731     B b1483 t1482
2732     T t1483 o1474 b998 b1480 b1483 b4
2733     B b1484 t1483
2734     P p1484 String "groupCancelRightT << 'g >> << 's >> thenT autoT"
2735     O o1484 ext_rule p1484
2736     T t1484 o999 b1471 b4
2737 xiny 3405 B b1485 t1484
2738 xiny 3498 T t1485 o1484 b998 b1485 b4 b4
2739 xiny 3404 B b1486 t1485
2740 xiny 3498 T t1486 o b1486 b4
2741 xiny 3404 B b1487 t1486
2742 xiny 3498 T t1487 o b1484 b1487
2743 xiny 3404 B b1488 t1487
2744 xiny 3498 T t1488 o1443 b998 b1474 b1488 b4
2745     B b1489 t1488
2746     T t1489 o996 b1489
2747     B b1490 t1489
2748     P p1492 Number 9099
2749     P p1499 String unique_inv2
2750     O o1499 rule p1499
2751     T t1499 o575 b564 b589 b577
2752     B b1499 t1499
2753     T t1500 o811 b1499 b583
2754     S s1500 t673 h
2755 xiny 3405 G s1500 t1500
2756 xiny 3498 B b1500 s1500
2757     P p1508 String "assumT 7 thenT setSubstT << equal{id{'g}; op{'g; 's; inv{'g; 's}}}>> 2 thenAT autoT"
2758 xiny 3405 O o1508 ext_rule p1508
2759 xiny 3498 T t1509 o b1500 b4
2760     B b1509 t1509
2761     T t1510 o b723 b1509
2762     B b1510 t1510
2763     T t1511 o b874 b1510
2764     B b1511 t1511
2765     T t1512 o b688 b1511
2766     B b1512 t1512
2767     T t1513 o b670 b1512
2768     B b1513 t1513
2769     T t1514 o b704 b1513
2770     B b1514 t1514
2771     T t1515 o b783 b1514
2772     B b1515 t1515
2773     T t1516 o1001 b1435 b1515
2774     B b1516 t1516
2775     T t1517 o1000 b1516 b4 b1011
2776     B b1517 t1517
2777     H h1517 v t1500
2778     T t1518 o575 b564 b589 b590
2779     B b1518 t1518
2780     T t1519 o744 b583 b1518
2781     S s1519 t673 h h1517
2782     G s1519 t1519
2783     B b1519 s1519
2784     T t1520 o1001 b1519 b1515
2785     B b1520 t1520
2786     T t1521 o811 b583 b1518
2787     S s1521 t673 h h1517
2788 xiny 3405 G s1521 t1521
2789 xiny 3498 B b1521 s1521
2790     T t1522 o1001 b1521 b1515
2791     B b1522 t1522
2792     S s1522 t673 h h1517
2793     G s1522 t1435
2794     B b1523 s1522
2795     T t1523 o1001 b1523 b1515
2796     B b1524 t1523
2797     T t1524 o2 b1517
2798     B b1525 t1524
2799     T t1525 o1000 b1524 b4 b1525
2800 xiny 3405 B b1526 t1525
2801 xiny 3498 T t1526 o2 b1526
2802 xiny 3379 B b1527 t1526
2803 xiny 3498 T t1527 o1452 b1522 b1460 b1527
2804 xiny 3379 B b1528 t1527
2805 xiny 3498 T t1528 o2 b1528
2806 xiny 3379 B b1529 t1528
2807 xiny 3498 T t1529 o1452 b1520 b4 b1529
2808     B b1530 t1529
2809     T t1530 o811 b1499 b1518
2810     H h1530 v_1 t1530
2811     S s1530 t673 h h1517 h1530
2812     G s1530 t1435
2813     B b1531 s1530
2814     T t1531 o1001 b1531 b1515
2815     B b1532 t1531
2816     T t1532 o1000 b1532 b4 b1527
2817 xiny 3379 B b1533 t1532
2818 xiny 3498 T t1533 o b1533 b4
2819 xiny 3379 B b1534 t1533
2820 xiny 3498 T t1534 o b1530 b1534
2821 xiny 3379 B b1535 t1534
2822 xiny 3498 T t1535 o999 b1517 b1535
2823 xiny 3379 B b1536 t1535
2824 xiny 3498 P p1536 String "assertT << equal{op{'g; 's; inv{'g; 's}}; id{'g}}>> thenT autoT"
2825     O o1536 ext_rule p1536
2826     T t1536 o811 b1518 b583
2827     H h1536 v_1 t1536
2828     S s1536 t673 h h1517 h1536
2829     G s1536 t1519
2830     B b1537 s1536
2831     T t1537 o1001 b1537 b1515
2832     B b1538 t1537
2833     T t1538 o2 b1530
2834     B b1539 t1538
2835     T t1539 o1000 b1538 b4 b1539
2836     B b1540 t1539
2837     T t1540 o b1540 b4
2838     B b1541 t1540
2839     T t1541 o999 b1530 b1541
2840 xiny 3404 B b1542 t1541
2841 xiny 3498 T t1542 o999 b1540 b4
2842 xiny 3404 B b1543 t1542
2843 xiny 3498 T t1543 o1480 b998 b1543 b4 b4
2844 xiny 3404 B b1544 t1543
2845 xiny 3498 T t1544 o b1544 b4
2846     B b1545 t1544
2847     P p1545 String "rwh unfold_equal 3 thenT eqSetSymT"
2848     O o1545 ext_rule p1545
2849     S s1545 t673 h h1517 h1474
2850     G s1545 t1519
2851     B b1546 s1545
2852     T t1546 o1001 b1546 b1515
2853 xiny 3404 B b1547 t1546
2854 xiny 3498 T t1547 o1000 b1547 b4 b1539
2855 xiny 3404 B b1548 t1547
2856 xiny 3498 P p1548 String wf
2857     O o1548 tactic_arg p1548
2858     T t1548 o689 b1453
2859 xiny 3404 B b1549 t1548
2860 xiny 3498 B b1550 t850
2861     T t1550 o1289 b1549 b1550
2862     B b1551 t1550
2863     T t1551 o744 b1453 b583
2864     B b1552 t1551
2865     T t1552 o1289 b1551 b1552
2866     H h1552 v_1 t1552
2867     S s1552 t668 h h1517 h1552
2868     G s1552 t850
2869     B b1553 s1552
2870     T t1553 o1001 b1553 b1515
2871     B b1554 t1553
2872     S s1554 t673 h h1517 h1552
2873     G s1554 t1519
2874     B b1555 s1554
2875     T t1555 o1001 b1555 b1515
2876 xiny 3404 B b1556 t1555
2877 xiny 3498 T t1556 o2 b1548
2878 xiny 3404 B b1557 t1556
2879 xiny 3498 T t1557 o1000 b1556 b4 b1557
2880 xiny 3404 B b1558 t1557
2881 xiny 3498 T t1558 o2 b1558
2882 xiny 3404 B b1559 t1558
2883 xiny 3498 T t1559 o1548 b1554 b4 b1559
2884     B b1560 t1559
2885     T t1560 o689 b1518
2886     S s1560 t668 h h1517 h1552
2887     G s1560 t1560
2888     B b1561 s1560
2889     T t1561 o1001 b1561 b1515
2890 xiny 3404 B b1562 t1561
2891 xiny 3498 T t1562 o1548 b1562 b4 b1559
2892 xiny 3404 B b1563 t1562
2893 xiny 3498 T t1563 o744 b1518 b583
2894     S s1563 t673 h h1517 h1552
2895     G s1563 t1563
2896     B b1564 s1563
2897     T t1564 o1001 b1564 b1515
2898 xiny 3404 B b1565 t1564
2899 xiny 3498 T t1565 o1000 b1565 b4 b1559
2900 xiny 3404 B b1566 t1565
2901 xiny 3498 T t1566 o b1566 b4
2902     B b1567 t1566
2903     T t1567 o b1563 b1567
2904     B b1568 t1567
2905     T t1568 o b1560 b1568
2906     B b1569 t1568
2907     T t1569 o999 b1548 b1569
2908     B b1570 t1569
2909     NSummary!ext_goal ext_goal ext_goal Summary
2910     O o1570 ext_goal
2911     T t1570 o1570 b1560
2912 xiny 3405 B b1571 t1570
2913 xiny 3498 T t1571 o1570 b1563
2914     B b1572 t1571
2915     T t1572 o1570 b1566
2916     B b1573 t1572
2917     T t1573 o b1573 b4
2918 xiny 3405 B b1574 t1573
2919 xiny 3498 T t1574 o b1572 b1574
2920     B b1575 t1574
2921     T t1575 o b1571 b1575
2922 xiny 3405 B b1576 t1575
2923 xiny 3498 T t1576 o1545 b998 b1570 b1576 b4
2924     B b1577 t1576
2925     T t1577 o b1577 b4
2926 xiny 3405 B b1578 t1577
2927 xiny 3498 T t1578 o1536 b998 b1542 b1545 b1578
2928     B b1579 t1578
2929     P p1579 String "groupCancelLeftT << 'g >> << 's >> thenT autoT"
2930     O o1579 ext_rule p1579
2931     T t1579 o999 b1533 b4
2932 xiny 3405 B b1580 t1579
2933 xiny 3498 T t1580 o1579 b998 b1580 b4 b4
2934     B b1581 t1580
2935     T t1581 o b1581 b4
2936 xiny 3405 B b1582 t1581
2937 xiny 3498 T t1582 o b1579 b1582
2938     B b1583 t1582
2939     T t1583 o1508 b998 b1536 b1583 b4
2940 xiny 3405 B b1584 t1583
2941 xiny 3498 T t1584 o996 b1584
2942 xiny 3404 B b1585 t1584
2943 xiny 3498 P p1594 String unique_sol1
2944     O o1594 rule p1594
2945     P p1595 Var a
2946     O o1595 var p1595
2947     T t1595 o1595
2948     B b1595 t1595
2949     T t1596 o689 b1595
2950     S s1596 t668 h
2951     G s1596 t1596
2952     B b1596 s1596
2953     T t1597 o666 b1596
2954     B b1597 t1597
2955     P p1597 Var b
2956     O o1597 var p1597
2957     T t1598 o1597
2958     B b1598 t1598
2959     T t1599 o689 b1598
2960     S s1599 t668 h
2961     G s1599 t1599
2962     B b1599 s1599
2963     T t1600 o666 b1599
2964     B b1600 t1600
2965     P p1600 Var x
2966     O o1600 var p1600
2967     T t1601 o1600
2968     B b1601 t1601
2969     T t1602 o689 b1601
2970     S s1602 t668 h
2971     G s1602 t1602
2972     B b1602 s1602
2973     T t1603 o666 b1602
2974     B b1603 t1603
2975     T t1604 o721 b1595 b570
2976     S s1604 t673 h
2977     G s1604 t1604
2978     B b1604 s1604
2979     T t1605 o666 b1604
2980     B b1605 t1605
2981     T t1606 o721 b1598 b570
2982     S s1606 t673 h
2983     G s1606 t1606
2984     B b1606 s1606
2985     T t1607 o666 b1606
2986     B b1607 t1607
2987     T t1608 o721 b1601 b570
2988     S s1608 t673 h
2989 xiny 3405 G s1608 t1608
2990 xiny 3498 B b1608 s1608
2991     T t1609 o666 b1608
2992     B b1609 t1609
2993     T t1610 o575 b564 b1595 b1601
2994     B b1610 t1610
2995     T t1611 o811 b1610 b1598
2996     S s1611 t673 h
2997     G s1611 t1611
2998     B b1611 s1611
2999     T t1613 o588 b564 b1595
3000     B b1613 t1613
3001     T t1614 o575 b564 b1613 b1598
3002     B b1614 t1614
3003     T t1615 o811 b1601 b1614
3004     S s1615 t673 h
3005     G s1615 t1615
3006     B b1615 s1615
3007     P p1625 String "assumT 9 thenT assertT << equal{op{'g; inv{'g; 'a}; op{'g; 'a; 'x}}; op{'g; inv{'g; 'a}; 'b}} >> thenT autoT"
3008     O o1625 ext_rule p1625
3009     T t1626 o b1611 b4
3010     B b1626 t1626
3011     T t1627 o b1608 b1626
3012     B b1627 t1627
3013     T t1628 o b1606 b1627
3014     B b1628 t1628
3015     T t1629 o b1604 b1628
3016     B b1629 t1629
3017     T t1630 o b688 b1629
3018     B b1630 t1630
3019     T t1631 o b670 b1630
3020     B b1631 t1631
3021     T t1632 o b1602 b1631
3022     B b1632 t1632
3023     T t1633 o b1599 b1632
3024     B b1633 t1633
3025     T t1634 o b1596 b1633
3026     B b1634 t1634
3027     T t1635 o1001 b1615 b1634
3028     B b1635 t1635
3029     T t1636 o1000 b1635 b4 b1011
3030     B b1636 t1636
3031     H h1636 v t1611
3032     T t1637 o744 b1610 b1598
3033     S s1637 t673 h h1636
3034     G s1637 t1637
3035     B b1637 s1637
3036     T t1638 o1001 b1637 b1634
3037     B b1638 t1638
3038     T t1639 o575 b564 b1613 b1610
3039     B b1639 t1639
3040     T t1640 o744 b1639 b1614
3041     S s1640 t673 h h1636
3042     G s1640 t1640
3043     B b1640 s1640
3044     T t1641 o1001 b1640 b1634
3045     B b1641 t1641
3046     T t1642 o811 b1639 b1614
3047     S s1642 t673 h h1636
3048     G s1642 t1642
3049     B b1642 s1642
3050     T t1643 o1001 b1642 b1634
3051 xiny 3494 B b1643 t1643
3052 xiny 3498 S s1643 t673 h h1636
3053     G s1643 t1615
3054     B b1644 s1643
3055     T t1644 o1001 b1644 b1634
3056     B b1645 t1644
3057     T t1645 o2 b1636
3058     B b1646 t1645
3059     T t1646 o1000 b1645 b4 b1646
3060     B b1647 t1646
3061     T t1647 o2 b1647
3062     B b1648 t1647
3063     T t1648 o1012 b1643 b1460 b1648
3064     B b1649 t1648
3065     T t1649 o2 b1649
3066     B b1650 t1649
3067     T t1650 o1012 b1641 b1460 b1650
3068     B b1651 t1650
3069     T t1651 o2 b1651
3070     B b1652 t1651
3071     T t1652 o1012 b1638 b4 b1652
3072     B b1653 t1652
3073     H h1653 v_1 t1642
3074     T t1653 o744 b1601 b1614
3075     S s1653 t673 h h1636 h1653
3076     G s1653 t1653
3077     B b1654 s1653
3078     T t1654 o1001 b1654 b1634
3079     B b1655 t1654
3080     S s1655 t673 h h1636 h1653
3081     G s1655 t1615
3082     B b1656 s1655
3083     T t1656 o1001 b1656 b1634
3084     B b1657 t1656
3085     T t1657 o1000 b1657 b1460 b1648
3086     B b1658 t1657
3087     T t1658 o2 b1658
3088     B b1659 t1658
3089     T t1659 o1000 b1655 b4 b1659
3090     B b1660 t1659
3091     T t1660 o b1660 b4
3092     B b1661 t1660
3093     T t1661 o b1653 b1661
3094     B b1662 t1661
3095     T t1662 o999 b1636 b1662
3096     B b1663 t1662
3097     P p1663 String "rwh unfold_equal 2 thenT autoT"
3098     O o1663 ext_rule p1663
3099     T t1663 o999 b1653 b4
3100     B b1664 t1663
3101     T t1664 o1663 b998 b1664 b4 b4
3102     B b1665 t1664
3103     P p1665 String "setSubstT << equal{op{'g; inv{'g; 'a}; op{'g; 'a; 'x}}; op{'g; op{'g; inv{'g; 'a}; 'a}; 'x}} >> 3 thenT autoT"
3104     O o1665 ext_rule p1665
3105     T t1665 o575 b564 b1613 b1595
3106     B b1666 t1665
3107     T t1666 o575 b564 b1666 b1601
3108     B b1667 t1666
3109     T t1667 o811 b1667 b1614
3110     H h1667 v_2 t1667
3111     S s1667 t673 h h1636 h1653 h1667
3112     G s1667 t1653
3113     B b1668 s1667
3114     T t1668 o1001 b1668 b1634
3115     B b1669 t1668
3116     T t1669 o2 b1660
3117     B b1670 t1669
3118     T t1670 o1000 b1669 b4 b1670
3119     B b1671 t1670
3120     T t1671 o b1671 b4
3121     B b1672 t1671
3122     T t1672 o999 b1660 b1672
3123     B b1673 t1672
3124     P p1673 String "setSubstT << equal{op{'g; inv{'g; 'a}; 'a}; id{'g}} >> 4 thenT autoT"
3125     O o1673 ext_rule p1673
3126     T t1673 o575 b564 b583 b1601
3127     B b1674 t1673
3128     T t1674 o811 b1674 b1614
3129     H h1674 v_3 t1674
3130     S s1674 t673 h h1636 h1653 h1667 h1674
3131     G s1674 t1653
3132     B b1675 s1674
3133     T t1675 o1001 b1675 b1634
3134     B b1676 t1675
3135     T t1676 o2 b1671
3136     B b1677 t1676
3137     T t1677 o1000 b1676 b4 b1677
3138     B b1678 t1677
3139     T t1678 o b1678 b4
3140     B b1679 t1678
3141     T t1679 o999 b1671 b1679
3142     B b1680 t1679
3143     P p1680 String "setSubstT << equal{op{'g; id{'g}; 'x}; 'x} >> 5 thenT autoT"
3144     O o1680 ext_rule p1680
3145     H h1680 v_4 t1615
3146     S s1680 t673 h h1636 h1653 h1667 h1674 h1680
3147     G s1680 t1653
3148     B b1681 s1680
3149     T t1681 o1001 b1681 b1634
3150     B b1682 t1681
3151     T t1682 o2 b1678
3152     B b1683 t1682
3153     T t1683 o1000 b1682 b4 b1683
3154     B b1684 t1683
3155     T t1684 o b1684 b4
3156     B b1685 t1684
3157     T t1685 o999 b1678 b1685
3158     B b1686 t1685
3159     P p1686 String "rwh unfold_equal 6 thenT autoT"
3160     O o1686 ext_rule p1686
3161     T t1686 o999 b1684 b4
3162     B b1687 t1686
3163     T t1687 o1686 b998 b1687 b4 b4
3164     B b1688 t1687
3165     T t1688 o b1688 b4
3166     B b1689 t1688
3167     T t1689 o1680 b998 b1686 b1689 b4
3168     B b1690 t1689
3169     T t1690 o b1690 b4
3170     B b1691 t1690
3171     T t1691 o1673 b998 b1680 b1691 b4
3172     B b1692 t1691
3173     T t1692 o b1692 b4
3174     B b1693 t1692
3175     T t1693 o1665 b998 b1673 b1693 b4
3176     B b1694 t1693
3177     T t1694 o b1694 b4
3178     B b1695 t1694
3179     T t1695 o b1665 b1695
3180     B b1696 t1695
3181     T t1696 o1625 b998 b1663 b1696 b4
3182     B b1697 t1696
3183     T t1697 o996 b1697
3184     B b1698 t1697
3185     O o1705 location p p
3186     P p1705 String unique_sol2
3187     O o1706 rule p1705
3188     P p1706 Var y
3189     O o1707 var p1706
3190     T t1707 o1707
3191     B b1707 t1707
3192     T t1708 o689 b1707
3193     S s1708 t668 h
3194     G s1708 t1708
3195     B b1708 s1708
3196     T t1709 o666 b1708
3197     B b1709 t1709
3198     T t1710 o721 b1707 b570
3199     S s1710 t673 h
3200     G s1710 t1710
3201     B b1710 s1710
3202     T t1711 o666 b1710
3203     B b1711 t1711
3204     T t1712 o575 b564 b1707 b1595
3205     B b1712 t1712
3206     T t1713 o811 b1712 b1598
3207     S s1713 t673 h
3208     G s1713 t1713
3209     B b1713 s1713
3210     T t1715 o575 b564 b1598 b1613
3211     B b1715 t1715
3212     T t1716 o811 b1707 b1715
3213     S s1716 t673 h
3214     G s1716 t1716
3215     B b1716 s1716
3216     P p1726 String "assumT 9 thenT assertT << equal{op{'g; op{'g; 'y; 'a}; inv{'g; 'a}}; op{'g; 'b; inv{'g; 'a}}} >> thenT autoT"
3217     O o1726 ext_rule p1726
3218     T t1727 o b1713 b4
3219     B b1727 t1727
3220     T t1728 o b1710 b1727
3221 xiny 3405 B b1728 t1728
3222 xiny 3498 T t1729 o b1606 b1728
3223     B b1729 t1729
3224     T t1730 o b1604 b1729
3225 xiny 3405 B b1730 t1730
3226 xiny 3498 T t1731 o b688 b1730
3227 xiny 3405 B b1731 t1731
3228 xiny 3498 T t1732 o b670 b1731
3229 xiny 3404 B b1732 t1732
3230 xiny 3498 T t1733 o b1708 b1732
3231 xiny 3404 B b1733 t1733
3232 xiny 3498 T t1734 o b1599 b1733
3233 xiny 3404 B b1734 t1734
3234 xiny 3498 T t1735 o b1596 b1734
3235     B b1735 t1735
3236     T t1736 o1001 b1716 b1735
3237     B b1736 t1736
3238     T t1737 o1000 b1736 b4 b1011
3239     B b1737 t1737
3240     H h1737 v t1713
3241     T t1738 o744 b1712 b1598
3242     S s1738 t673 h h1737
3243     G s1738 t1738
3244     B b1738 s1738
3245     T t1739 o1001 b1738 b1735
3246 xiny 3404 B b1739 t1739
3247 xiny 3498 T t1740 o575 b564 b1712 b1613
3248 xiny 3404 B b1740 t1740
3249 xiny 3498 T t1741 o744 b1740 b1715
3250     S s1741 t673 h h1737
3251     G s1741 t1741
3252     B b1741 s1741
3253     T t1742 o1001 b1741 b1735
3254 xiny 3404 B b1742 t1742
3255 xiny 3498 T t1743 o811 b1740 b1715
3256     S s1743 t673 h h1737
3257     G s1743 t1743
3258     B b1743 s1743
3259     T t1744 o1001 b1743 b1735
3260 xiny 3404 B b1744 t1744
3261 xiny 3498 S s1744 t673 h h1737
3262     G s1744 t1716
3263     B b1745 s1744
3264     T t1745 o1001 b1745 b1735
3265     B b1746 t1745
3266     T t1746 o2 b1737
3267     B b1747 t1746
3268     T t1747 o1000 b1746 b4 b1747
3269     B b1748 t1747
3270     T t1748 o2 b1748
3271     B b1749 t1748
3272     T t1749 o1012 b1744 b1460 b1749
3273     B b1750 t1749
3274     T t1750 o2 b1750
3275     B b1751 t1750
3276     T t1751 o1012 b1742 b1460 b1751
3277     B b1752 t1751
3278     T t1752 o2 b1752
3279 xiny 3405 B b1753 t1752
3280 xiny 3498 T t1753 o1012 b1739 b4 b1753
3281     B b1754 t1753
3282     H h1754 v_1 t1743
3283     T t1754 o744 b1707 b1715
3284     S s1754 t673 h h1737 h1754
3285     G s1754 t1754
3286     B b1755 s1754
3287     T t1755 o1001 b1755 b1735
3288     B b1756 t1755
3289     S s1756 t673 h h1737 h1754
3290     G s1756 t1716
3291     B b1757 s1756
3292     T t1757 o1001 b1757 b1735
3293     B b1758 t1757
3294     T t1758 o1000 b1758 b1460 b1749
3295     B b1759 t1758
3296     T t1759 o2 b1759
3297     B b1760 t1759
3298     T t1760 o1000 b1756 b4 b1760
3299     B b1761 t1760
3300     T t1761 o b1761 b4
3301     B b1762 t1761
3302     T t1762 o b1754 b1762
3303     B b1763 t1762
3304     T t1763 o999 b1737 b1763
3305     B b1764 t1763
3306     T t1764 o999 b1754 b4
3307     B b1765 t1764
3308     T t1765 o1663 b998 b1765 b4 b4
3309     B b1766 t1765
3310     P p1766 String "setSubstT << equal{op{'g; op{'g; 'y; 'a}; inv{'g; 'a}}; op{'g; 'y; op{'g; 'a; inv{'g; 'a}}}} >> 3 thenT autoT"
3311     O o1766 ext_rule p1766
3312     T t1766 o575 b564 b1595 b1613
3313     B b1767 t1766
3314     T t1767 o575 b564 b1707 b1767
3315     B b1768 t1767
3316     T t1768 o811 b1768 b1715
3317     H h1768 v_2 t1768
3318     S s1768 t673 h h1737 h1754 h1768
3319     G s1768 t1754
3320     B b1769 s1768
3321     T t1769 o1001 b1769 b1735
3322 xiny 3404 B b1770 t1769
3323 xiny 3498 T t1770 o2 b1761
3324 xiny 3404 B b1771 t1770
3325 xiny 3498 T t1771 o1000 b1770 b4 b1771
3326 xiny 3404 B b1772 t1771
3327 xiny 3498 T t1772 o b1772 b4
3328 xiny 3404 B b1773 t1772
3329 xiny 3498 T t1773 o999 b1761 b1773
3330 xiny 3404 B b1774 t1773
3331 xiny 3498 P p1774 String "setSubstT << equal{op{'g; 'a; inv{'g; 'a}}; id{'g}} >> 4 thenT autoT"
3332     O o1774 ext_rule p1774
3333     T t1774 o575 b564 b1707 b583
3334 xiny 3404 B b1775 t1774
3335 xiny 3498 T t1775 o811 b1775 b1715
3336     H h1775 v_3 t1775
3337     S s1775 t673 h h1737 h1754 h1768 h1775
3338     G s1775 t1754
3339     B b1776 s1775
3340     T t1776 o1001 b1776 b1735
3341 xiny 3404 B b1777 t1776
3342 xiny 3498 T t1777 o2 b1772
3343 xiny 3404 B b1778 t1777
3344 xiny 3498 T t1778 o1000 b1777 b4 b1778
3345 xiny 3404 B b1779 t1778
3346 xiny 3498 T t1779 o b1779 b4
3347     B b1780 t1779
3348     T t1780 o999 b1772 b1780
3349 xiny 3405 B b1781 t1780
3350 xiny 3498 P p1781 String "setSubstT << equal{op{'g; 'y; id{'g}}; 'y}>> 5 thenT autoT"
3351     O o1781 ext_rule p1781
3352     H h1781 v_4 t1716
3353     S s1781 t673 h h1737 h1754 h1768 h1775 h1781
3354     G s1781 t1754
3355     B b1782 s1781
3356     T t1782 o1001 b1782 b1735
3357 xiny 3404 B b1783 t1782
3358 xiny 3498 T t1783 o2 b1779
3359 xiny 3404 B b1784 t1783
3360 xiny 3498 T t1784 o1000 b1783 b4 b1784
3361 xiny 3404 B b1785 t1784
3362 xiny 3498 T t1785 o b1785 b4
3363 xiny 3404 B b1786 t1785
3364 xiny 3498 T t1786 o999 b1779 b1786
3365 xiny 3404 B b1787 t1786
3366 xiny 3498 T t1787 o999 b1785 b4
3367 xiny 3404 B b1788 t1787
3368 xiny 3498 T t1788 o1686 b998 b1788 b4 b4
3369     B b1789 t1788
3370     T t1789 o b1789 b4
3371     B b1790 t1789
3372     T t1790 o1781 b998 b1787 b1790 b4
3373     B b1791 t1790
3374     T t1791 o b1791 b4
3375     B b1792 t1791
3376     T t1792 o1774 b998 b1781 b1792 b4
3377     B b1793 t1792
3378     T t1793 o b1793 b4
3379     B b1794 t1793
3380     T t1794 o1766 b998 b1774 b1794 b4
3381     B b1795 t1794
3382     T t1795 o b1795 b4
3383     B b1796 t1795
3384     T t1796 o b1766 b1796
3385     B b1797 t1796
3386     T t1797 o1726 b998 b1764 b1797 b4
3387     B b1798 t1797
3388     T t1798 o996 b1798
3389     B b1799 t1798
3390     P p1806 String inv_simplify
3391     O o1806 rule p1806
3392     T t1807 o575 b564 b1595 b1598
3393     B b1807 t1807
3394 xiny 3516 T t867 o574 b1807
3395     B b867 t867
3396     T t868 o863 b867
3397     B b868 t868
3398     P p868 Number 708
3399     O o868 location p868 p586
3400     T t869 o868 b584
3401     B b869 t869
3402     P p869 Number 742
3403     O o869 location p592 p869
3404     T t870 o587 b1613
3405     B b870 t870
3406     T t871 o869 b870
3407     B b871 t871
3408     P p871 Number 744
3409     P p872 Number 756
3410     O o872 location p871 p872
3411     T t872 o872 b154
3412     B b872 t872
3413     P p873 Number 758
3414     P p880 Number 828
3415     O o880 location p873 p880
3416     T t884 o880 b607
3417     B b884 t884
3418     P p884 Number 830
3419     P p885 Number 899
3420     O o885 location p884 p885
3421     T t885 o885 b617
3422     B b885 t885
3423     P p886 Number 901
3424     P p887 Number 967
3425     O o887 location p886 p887
3426     T t887 o887 b624
3427     B b887 t887
3428     P p888 Number 969
3429     P p889 Number 1103
3430     O o889 location p888 p889
3431     T t889 o602 b1595
3432     B b889 t889
3433     T t899 o602 b1598
3434     B b899 t899
3435     T t900 o b899 b613
3436     B b900 t900
3437     T t901 o b632 b900
3438     B b901 t901
3439     T t902 o b889 b901
3440     B b902 t902
3441     T t903 o b632 b902
3442     B b903 t903
3443     T t904 o b602 b903
3444     B b904 t904
3445     T t914 o b631 b904
3446     B b914 t914
3447     T t915 o601 b914
3448     B b915 t915
3449     T t916 o627 b208 b1807 b915
3450     B b916 t916
3451     T t917 o889 b916
3452     B b917 t917
3453     P p917 Number 1105
3454     P p918 Number 1203
3455     O o918 location p917 p918
3456     T t918 o b889 b613
3457     B b918 t918
3458     T t919 o b632 b918
3459     B b919 t919
3460     T t927 o b602 b919
3461     B b927 t927
3462     T t928 o b646 b927
3463     B b928 t928
3464     T t929 o601 b928
3465     B b929 t929
3466     T t930 o645 b630 b1613 b929
3467     B b930 t930
3468     T t931 o918 b930
3469     B b931 t931
3470     P p931 Number 1222
3471     P p932 Number 1356
3472     O o932 location p931 p932
3473     P p933 Number 1248
3474     P p934 Number 1256
3475     O o934 resource_defs p933 p934 p204
3476     P p936 Number 1254
3477     O o936 uid p936 p934
3478     T t941 o936 b680
3479     B b941 t941
3480     T t942 o b941 b4
3481     B b942 t942
3482     T t943 o934 b942
3483     B b943 t943
3484     T t944 o b943 b4
3485     B b944 t944
3486     T t945 o663 b665 b676 b677 b944
3487     B b945 t945
3488     T t946 o932 b945
3489     B b946 t946
3490     P p946 Number 1358
3491     O o946 location p946 p288
3492     P p947 Number 1380
3493     P p949 Number 1387
3494     O o949 resource_defs p947 p949 p204
3495     P p950 Number 1385
3496     O o950 uid p950 p949
3497     T t956 o950 b680
3498     B b956 t956
3499     T t957 o b956 b4
3500     B b957 t957
3501     T t958 o949 b957
3502     B b958 t958
3503     T t959 o b958 b4
3504     B b959 t959
3505     T t960 o688 b665 b693 b677 b959
3506     B b960 t960
3507     T t961 o946 b960
3508     B b961 t961
3509     P p961 Number 1795
3510     O o961 location p287 p961
3511     P p962 Number 1550
3512     P p964 Number 1557
3513     O o964 resource_defs p962 p964 p204
3514     P p965 Number 1555
3515     O o965 uid p965 p964
3516     T t971 o965 b680
3517     B b971 t971
3518     T t972 o b971 b4
3519     B b972 t972
3520     T t973 o964 b972
3521     B b973 t973
3522     T t974 o b973 b4
3523     B b974 t974
3524     T t975 o702 b665 b711 b677 b974
3525     B b975 t975
3526     T t976 o961 b975
3527     B b976 t976
3528     P p976 Number 1797
3529     P p977 Number 2171
3530     O o977 location p976 p977
3531     P p980 Number 1826
3532     O o981 resource_defs p207 p980 p204
3533     P p981 Number 1824
3534     O o982 uid p981 p980
3535     T t1072 o982 b680
3536     B b1074 t1072
3537     T t1074 o b1074 b4
3538     B b1075 t1074
3539     T t1075 o981 b1075
3540     B b1076 t1075
3541     T t1076 o b1076 b4
3542     B b1077 t1076
3543     T t1077 o720 b665 b732 b677 b1077
3544     B b1078 t1077
3545     T t1078 o977 b1078
3546     B b1079 t1078
3547     P p1079 Number 2173
3548     P p1080 Number 2825
3549     O o1080 location p1079 p1080
3550     P p1082 String op_equiv1
3551     O o1082 rule p1082
3552     P p1083 Var R
3553     O o1083 var p1083
3554     T t1119 o1083
3555     B b1172 t1119
3556     T t1172 o689 b1172
3557     S s1172 t668 h
3558     G s1172 t1172
3559     B b1173 s1172
3560     T t1173 o666 b1173
3561     B b1174 t1173
3562     NCzf_itt_equiv Czf_itt_equiv Czf_itt_equiv NIL
3563     NCzf_itt_equiv!equiv equiv equiv Czf_itt_equiv
3564     O o1175 equiv
3565     T t1175 o1175 b570 b1172
3566     S s1175 t673 h
3567     G s1175 t1175
3568     B b1175 s1175
3569     T t1176 o666 b1175
3570     B b1176 t1176
3571     T t1177 o1175 b570 b1172 b576 b577
3572     S s1177 t673 h
3573     G s1177 t1177
3574     B b1177 s1177
3575     T t1178 o666 b1177
3576     B b1178 t1178
3577     T t1179 o1175 b570 b1172 b747 b748
3578     S s1179 t673 h
3579     G s1179 t1179
3580     B b1179 s1179
3581     T t1180 o666 b1179
3582     B b1180 t1180
3583     T t1181 o665 b1178 b1180
3584     B b1181 t1181
3585     T t1182 o665 b811 b1181
3586     B b1182 t1182
3587     T t1183 o665 b724 b1182
3588     B b1183 t1183
3589     T t1184 o665 b722 b1183
3590     B b1184 t1184
3591     T t1185 o665 b1176 b1184
3592     B b1185 t1185
3593     T t1186 o665 b689 b1185
3594     B b1186 t1186
3595     T t1193 o665 b671 b1186
3596     B b1193 t1193
3597     T t1195 o665 b1174 b1193
3598     B b1195 t1195
3599     T t1196 o665 b744 b1195
3600     B b1196 t1196
3601     T t1197 o665 b705 b1196
3602     B b1197 t1197
3603     T t1198 o665 b703 b1197
3604     B b1198 t1198
3605     P p1199 Number 2198
3606     P p1200 Number 2205
3607     O o1200 resource_defs p1199 p1200 p204
3608     P p1207 Number 2203
3609     O o1207 uid p1207 p1200
3610     T t1207 o1207 b680
3611     B b1207 t1207
3612     T t1209 o b1207 b4
3613     B b1209 t1209
3614     T t1210 o1200 b1209
3615     B b1210 t1210
3616     T t1212 o b1210 b4
3617     B b1212 t1212
3618     T t1213 o1082 b665 b1198 b677 b1212
3619     B b1213 t1213
3620     T t1214 o1080 b1213
3621     B b1214 t1214
3622     P p1214 Number 2827
3623     P p1215 Number 3479
3624     O o1215 location p1214 p1215
3625     P p1216 String op_equiv2
3626     O o1216 rule p1216
3627     T t1216 o1175 b570 b1172 b765 b766
3628     S s1216 t673 h
3629     G s1216 t1216
3630     B b1216 s1216
3631     T t1217 o666 b1216
3632     B b1217 t1217
3633     T t1218 o665 b1178 b1217
3634     B b1218 t1218
3635     T t1219 o665 b811 b1218
3636     B b1219 t1219
3637     T t1220 o665 b724 b1219
3638     B b1220 t1220
3639     T t1221 o665 b722 b1220
3640     B b1221 t1221
3641     T t1222 o665 b1176 b1221
3642     B b1222 t1222
3643     T t1223 o665 b689 b1222
3644     B b1223 t1223
3645     T t1224 o665 b671 b1223
3646     B b1224 t1224
3647     T t1225 o665 b1174 b1224
3648     B b1225 t1225
3649     T t1226 o665 b744 b1225
3650     B b1226 t1226
3651     T t1227 o665 b705 b1226
3652     B b1227 t1227
3653     T t1228 o665 b703 b1227
3654     B b1228 t1228
3655     P p1228 Number 2852
3656     P p1229 Number 2859
3657     O o1229 resource_defs p1228 p1229 p204
3658     P p1230 Number 2857
3659     O o1230 uid p1230 p1229
3660     T t1230 o1230 b680
3661     B b1230 t1230
3662     T t1231 o b1230 b4
3663     B b1231 t1231
3664     T t1232 o1229 b1231
3665     B b1232 t1232
3666     T t1236 o b1232 b4
3667     B b1236 t1236
3668     T t1237 o1216 b665 b1228 b677 b1236
3669     B b1237 t1237
3670     T t1241 o1215 b1237
3671     B b1241 t1241
3672     P p1242 Number 3481
3673     P p1244 Number 3618
3674     O o1244 location p1242 p1244
3675     P p1245 Number 3504
3676     P p1246 Number 3511
3677     O o1246 resource_defs p1245 p1246 p204
3678     P p1247 Number 3509
3679     O o1247 uid p1247 p1246
3680     T t1247 o1247 b680
3681     B b1247 t1247
3682     T t1248 o b1247 b4
3683     B b1248 t1248
3684     T t1250 o1246 b1248
3685     B b1250 t1250
3686     T t1251 o b1250 b4
3687     B b1251 t1251
3688     T t1252 o783 b665 b789 b677 b1251
3689     B b1252 t1252
3690     T t1253 o1244 b1252
3691     B b1253 t1253
3692     P p1253 Number 3620
3693     P p1256 Number 3757
3694     O o1258 location p1253 p1256
3695     P p1258 Number 3643
3696     P p1259 Number 3650
3697     O o1260 resource_defs p1258 p1259 p204
3698     P p1260 Number 3648
3699     O o1262 uid p1260 p1259
3700     T t1262 o1262 b680
3701     B b1262 t1262
3702     T t1263 o b1262 b4
3703     B b1263 t1263
3704     T t1264 o1260 b1263
3705     B b1264 t1264
3706     T t1265 o b1264 b4
3707     B b1265 t1265
3708     T t1266 o798 b665 b801 b677 b1265
3709     B b1266 t1266
3710     T t1267 o1258 b1266
3711     B b1267 t1267
3712     P p1267 Number 3759
3713     P p1268 Number 4376
3714     O o1268 location p1267 p1268
3715     T t1268 o1175 b570 b1172 b812 b813
3716     S s1268 t673 h
3717     G s1268 t1268<