/[mojave]/metaprl/theories/czf/czf_itt_group.prla
ViewVC logotype

Contents of /metaprl/theories/czf/czf_itt_group.prla

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3553 - (show annotations) (download)
Tue Apr 2 07:45:26 2002 UTC (19 years, 3 months ago) by xiny
File size: 151041 byte(s)
1. Added "eqG" to the definition of groups which denotes the equivalence
   relation related with the group. Every group has an equivalence
   relation, which is now explicitly described.
2. Accordingly, all rules related with equivalence relations in groups
   are updated and reproved.
3. Added tactics "uniqueInvLeftT" and "uniqueInvRightT" which might not
   be very useful though.

1 #PRL version 1.0.0 ASCII term
2 NPerv Perv Perv NIL
3 NPerv!cons cons cons Perv
4 O o cons
5 NSummary Summary Summary NIL
6 NSummary!location location location Summary
7 P p Number 0
8 P p1 Number 25
9 O o1 location p p1
10 NSummary!parent parent parent Summary
11 O o2 parent
12 P p2 String Itt_record_label0
13 O o3 parent p2
14 T t o3
15 B b t
16 NPerv!nil nil3 nil Perv
17 O o4 nil3
18 T t4 o4
19 B b4 t4
20 T t5 o b b4
21 B b5 t5
22 P p5 String Itt_nat
23 O o5 parent p5
24 T t6 o5
25 B b6 t6
26 T t7 o b6 b4
27 B b7 t7
28 P p7 String Itt_int_ext
29 O o7 parent p7
30 T t8 o7
31 B b8 t8
32 T t9 o b8 b4
33 B b9 t9
34 P p9 String Itt_int_base
35 O o9 parent p9
36 T t10 o9
37 B b10 t10
38 T t11 o b10 b4
39 B b11 t11
40 P p11 String Itt_bool
41 O o11 parent p11
42 T t12 o11
43 B b12 t12
44 T t13 o b12 b4
45 B b13 t13
46 P p13 String Itt_decidable
47 O o13 parent p13
48 T t14 o13
49 B b14 t14
50 T t15 o b14 b4
51 B b15 t15
52 P p15 String Itt_logic
53 O o15 parent p15
54 T t16 o15
55 B b16 t16
56 T t17 o b16 b4
57 B b17 t17
58 P p17 String Itt_union
59 O o17 parent p17
60 T t18 o17
61 B b18 t18
62 T t19 o b18 b4
63 B b19 t19
64 P p19 String Itt_prod
65 O o19 parent p19
66 T t20 o19
67 B b20 t20
68 T t21 o b20 b4
69 B b21 t21
70 P p21 String Itt_dprod
71 O o21 parent p21
72 T t22 o21
73 B b22 t22
74 T t23 o b22 b4
75 B b23 t23
76 P p23 String Itt_fun
77 O o23 parent p23
78 T t24 o23
79 B b24 t24
80 T t25 o b24 b4
81 B b25 t25
82 P p25 String Itt_dfun
83 O o25 parent p25
84 T t26 o25
85 B b26 t26
86 T t27 o b26 b4
87 B b27 t27
88 P p27 String Itt_rfun
89 O o27 parent p27
90 T t28 o27
91 B b28 t28
92 T t29 o b28 b4
93 B b29 t29
94 P p29 String Itt_void
95 O o29 parent p29
96 T t30 o29
97 B b30 t30
98 T t31 o b30 b4
99 B b31 t31
100 P p31 String Itt_set
101 O o31 parent p31
102 T t32 o31
103 B b32 t32
104 T t33 o b32 b4
105 B b33 t33
106 P p33 String Itt_unit
107 O o33 parent p33
108 T t34 o33
109 B b34 t34
110 T t35 o b34 b4
111 B b35 t35
112 P p35 String Itt_squiggle
113 O o35 parent p35
114 T t36 o35
115 B b36 t36
116 T t37 o b36 b4
117 B b37 t37
118 P p37 String Itt_subtype
119 O o37 parent p37
120 T t38 o37
121 B b38 t38
122 T t39 o b38 b4
123 B b39 t39
124 P p39 String Itt_squash
125 O o39 parent p39
126 T t40 o39
127 B b40 t40
128 T t41 o b40 b4
129 B b41 t41
130 P p41 String Itt_struct
131 O o41 parent p41
132 T t42 o41
133 B b42 t42
134 T t43 o b42 b4
135 B b43 t43
136 P p43 String Itt_equal
137 O o43 parent p43
138 T t44 o43
139 B b44 t44
140 T t45 o b44 b4
141 B b45 t45
142 P p45 String Itt_comment
143 O o45 parent p45
144 T t46 o45
145 B b46 t46
146 T t47 o b46 b4
147 B b47 t47
148 P p47 String Base_theory
149 O o47 parent p47
150 T t48 o47
151 B b48 t48
152 T t49 o b48 b4
153 B b49 t49
154 P p49 String Base_meta
155 O o49 parent p49
156 T t50 o49
157 B b50 t50
158 T t51 o b50 b4
159 B b51 t51
160 P p51 String Base_cache
161 O o51 parent p51
162 T t52 o51
163 B b52 t52
164 T t53 o b52 b4
165 B b53 t53
166 P p53 String Tactic_cache
167 O o53 parent p53
168 T t54 o53
169 B b54 t54
170 T t55 o b54 b4
171 B b55 t55
172 P p55 String Typeinf
173 O o55 parent p55
174 T t56 o55
175 B b56 t56
176 T t57 o b56 b4
177 B b57 t57
178 P p57 String Ocaml_df
179 O o57 parent p57
180 T t58 o57
181 B b58 t58
182 T t59 o b58 b4
183 B b59 t59
184 P p59 String Ocaml_str_df
185 O o59 parent p59
186 T t60 o59
187 B b60 t60
188 T t61 o b60 b4
189 B b61 t61
190 P p61 String Ocaml_sig_df
191 O o61 parent p61
192 T t62 o61
193 B b62 t62
194 T t63 o b62 b4
195 B b63 t63
196 P p63 String Ocaml_me_df
197 O o63 parent p63
198 T t64 o63
199 B b64 t64
200 T t65 o b64 b4
201 B b65 t65
202 P p65 String Ocaml_mt_df
203 O o65 parent p65
204 T t66 o65
205 B b66 t66
206 T t67 o b66 b4
207 B b67 t67
208 P p67 String Ocaml_type_df
209 O o67 parent p67
210 T t68 o67
211 B b68 t68
212 T t69 o b68 b4
213 B b69 t69
214 P p69 String Ocaml_patt_df
215 O o69 parent p69
216 T t70 o69
217 B b70 t70
218 T t71 o b70 b4
219 B b71 t71
220 P p71 String Ocaml_expr_df
221 O o71 parent p71
222 T t72 o71
223 B b72 t72
224 T t73 o b72 b4
225 B b73 t73
226 P p73 String Ocaml_base_df
227 O o73 parent p73
228 T t74 o73
229 B b74 t74
230 T t75 o b74 b4
231 B b75 t75
232 P p75 String Ocaml
233 O o75 parent p75
234 T t76 o75
235 B b76 t76
236 T t77 o b76 b4
237 B b77 t77
238 P p77 String Base_rewrite
239 O o77 parent p77
240 T t78 o77
241 B b78 t78
242 T t79 o b78 b4
243 B b79 t79
244 P p79 String Base_dtactic
245 O o79 parent p79
246 T t80 o79
247 B b80 t80
248 T t81 o b80 b4
249 B b81 t81
250 P p81 String Base_auto_tactic
251 O o81 parent p81
252 T t82 o81
253 B b82 t82
254 T t83 o b82 b4
255 B b83 t83
256 P p83 String Base_trivial
257 O o83 parent p83
258 T t84 o83
259 B b84 t84
260 T t85 o b84 b4
261 B b85 t85
262 P p85 String Top_conversionals
263 O o85 parent p85
264 T t86 o85
265 B b86 t86
266 T t87 o b86 b4
267 B b87 t87
268 P p87 String Top_tacticals
269 O o87 parent p87
270 T t88 o87
271 B b88 t88
272 T t89 o b88 b4
273 B b89 t89
274 P p89 String Var
275 O o89 parent p89
276 T t90 o89
277 B b90 t90
278 T t91 o b90 b4
279 B b91 t91
280 P p91 String Mptop
281 O o91 parent p91
282 T t92 o91
283 B b92 t92
284 T t93 o b92 b4
285 B b93 t93
286 P p93 String Summary
287 O o93 parent p93
288 T t94 o93
289 B b94 t94
290 T t95 o b94 b4
291 B b95 t95
292 P p95 String Comment
293 O o95 parent p95
294 T t96 o95
295 B b96 t96
296 T t97 o b96 b4
297 B b97 t97
298 P p97 String Base_dform
299 O o97 parent p97
300 T t98 o97
301 B b98 t98
302 T t99 o b98 b4
303 B b99 t99
304 P p99 String Nuprl_font
305 O o99 parent p99
306 T t100 o99
307 B b100 t100
308 T t101 o b100 b4
309 B b101 t101
310 P p101 String Perv
311 O o101 parent p101
312 T t102 o101
313 B b102 t102
314 T t103 o b102 b4
315 B b103 t103
316 T t104 o b103 b4
317 B b104 t104
318 T t105 o b101 b104
319 B b105 t105
320 T t106 o b99 b105
321 B b106 t106
322 T t107 o b97 b106
323 B b107 t107
324 T t108 o b95 b107
325 B b108 t108
326 T t109 o b93 b108
327 B b109 t109
328 T t110 o b91 b109
329 B b110 t110
330 T t111 o b89 b110
331 B b111 t111
332 T t112 o b87 b111
333 B b112 t112
334 T t113 o b85 b112
335 B b113 t113
336 T t114 o b83 b113
337 B b114 t114
338 T t115 o b81 b114
339 B b115 t115
340 T t116 o b79 b115
341 B b116 t116
342 T t117 o b77 b116
343 B b117 t117
344 T t118 o b75 b117
345 B b118 t118
346 T t119 o b73 b118
347 B b119 t119
348 T t120 o b71 b119
349 B b120 t120
350 T t121 o b69 b120
351 B b121 t121
352 T t122 o b67 b121
353 B b122 t122
354 T t123 o b65 b122
355 B b123 t123
356 T t124 o b63 b123
357 B b124 t124
358 T t125 o b61 b124
359 B b125 t125
360 T t126 o b59 b125
361 B b126 t126
362 T t127 o b57 b126
363 B b127 t127
364 T t128 o b55 b127
365 B b128 t128
366 T t129 o b53 b128
367 B b129 t129
368 T t130 o b51 b129
369 B b130 t130
370 T t131 o b49 b130
371 B b131 t131
372 T t132 o b47 b131
373 B b132 t132
374 T t133 o b45 b132
375 B b133 t133
376 T t134 o b43 b133
377 B b134 t134
378 T t135 o b41 b134
379 B b135 t135
380 T t136 o b39 b135
381 B b136 t136
382 T t137 o b37 b136
383 B b137 t137
384 T t138 o b35 b137
385 B b138 t138
386 T t139 o b33 b138
387 B b139 t139
388 T t140 o b31 b139
389 B b140 t140
390 T t141 o b29 b140
391 B b141 t141
392 T t142 o b27 b141
393 B b142 t142
394 T t143 o b25 b142
395 B b143 t143
396 T t144 o b23 b143
397 B b144 t144
398 T t145 o b21 b144
399 B b145 t145
400 T t146 o b19 b145
401 B b146 t146
402 T t147 o b17 b146
403 B b147 t147
404 T t148 o b15 b147
405 B b148 t148
406 T t149 o b13 b148
407 B b149 t149
408 T t150 o b11 b149
409 B b150 t150
410 T t151 o b9 b150
411 B b151 t151
412 T t152 o b7 b151
413 B b152 t152
414 T t153 o b5 b152
415 B b153 t153
416 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 B b156 t156
428 T t157 o155 b156
429 B b157 t157
430 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 B b160 t160
440 T t161 o159 b160
441 B b161 t161
442 P p161 Number 2352
443 P p162 Number 2358
444 O o162 type_lid p161 p162
445 T t162 o162 b160
446 B b162 t162
447 P p163 Number 2361
448 O o163 type_lid p163 p158
449 T t163 o163 b160
450 B b163 t163
451 T t164 o b163 b4
452 B b164 t164
453 T t165 o b162 b164
454 B b165 t165
455 T t166 o b161 b165
456 B b166 t166
457 T t167 o158 b166
458 B b167 t167
459 T t168 o153 b157 b167
460 B b168 t168
461 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 B b171 t171
470 T t172 o170 b171
471 B b172 t172
472 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 B b174 t174
478 T t175 o173 b174
479 B b175 t175
480 T t176 o168 b172 b175
481 B b176 t176
482 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 B b180 t180
493 T t181 o179 b180
494 B b181 t181
495 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 B b184 t184
505 T t185 o183 b184
506 B b185 t185
507 P p185 Number 1776
508 O o185 type_lid p185 p182
509 T t186 o185 b160
510 B b186 t186
511 T t187 o182 b185 b186
512 B b187 t187
513 T t188 o b187 b4
514 B b188 t188
515 T t189 o b181 b188
516 B b189 t189
517 T t190 o178 b189
518 B b190 t190
519 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 B b192 t192
526 P p193 Number 1792
527 O o193 type_lid p193 p191
528 T t193 o193 b160
529 B b193 t193
530 T t194 o191 b192 b193
531 B b194 t194
532 T t195 o176 b190 b194
533 B b195 t195
534 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 B b198 t198
543 P p199 Number 6175
544 O o199 type_lid p199 p197
545 T t199 o199 b160
546 B b199 t199
547 T t200 o b199 b4
548 B b200 t200
549 T t201 o b198 b200
550 B b201 t201
551 T t202 o197 b201
552 B b202 t202
553 P p202 Number 6183
554 P p203 Number 6189
555 O o203 type_lid p202 p203
556 T t203 o203 b160
557 B b203 t203
558 T t204 o195 b202 b203
559 B b204 t204
560 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 B b207 t207
569 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 B b211 t211
578 T t212 o210 b211
579 B b212 t212
580 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 B b216 t216
592 P p216 Number 1835
593 O o216 type_lid p212 p216
594 T t217 o216 b184
595 B b217 t217
596 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 B b220 t220
604 T t221 o b218 b220
605 B b221 t221
606 T t222 o b212 b221
607 B b222 t222
608 T t223 o209 b222
609 B b223 t223
610 T t224 o b223 b4
611 B b224 t224
612 T t225 o b207 b224
613 B b225 t225
614 T t226 o206 b225
615 B b226 t226
616 P p226 Number 1854
617 P p227 Number 1860
618 O o227 type_lid p226 p227
619 T t227 o227 b160
620 B b227 t227
621 T t228 o204 b226 b227
622 B b228 t228
623 P p228 String reduce
624 O o228 resource p228
625 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 B b231 t231
632 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 B b234 t234
640 T t235 o b234 b4
641 B b235 t235
642 T t236 o b231 b235
643 B b236 t236
644 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 B b245 t245
671 P p246 Number 4037
672 O o246 type_lid p246 p244
673 T t246 o246 b160
674 B b246 t246
675 T t247 o244 b245 b246
676 B b247 t247
677 T t248 o239 b243 b247
678 B b248 t248
679 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 B b252 t252
690 P p252 Number 4901
691 P p253 Number 4907
692 O o253 type_lid p252 p253
693 T t253 o253 b160
694 B b253 t253
695 T t254 o248 b252 b253
696 B b254 t254
697 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 B b259 t259
711 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 B b261 t261
717 T t262 o260 b261
718 B b262 t262
719 T t263 o b262 b4
720 B b263 t263
721 T t264 o b259 b263
722 B b264 t264
723 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 B b276 t276
756 T t277 o275 b276
757 B b277 t277
758 T t278 o270 b274 b277
759 B b278 t278
760 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 B b281 t281
769 T t282 o280 b281
770 B b282 t282
771 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 B b283 t283
777 T t284 o282 b283
778 B b284 t284
779 T t285 o278 b282 b284
780 B b285 t285
781 T t286 o b285 b4
782 B b286 t286
783 T t287 o b278 b286
784 B b287 t287
785 T t288 o b270 b287
786 B b288 t288
787 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 B b291 t291
793 T t292 o b228 b291
794 B b292 t292
795 T t293 o b204 b292
796 B b293 t293
797 T t294 o b195 b293
798 B b294 t294
799 T t295 o b176 b294
800 B b295 t295
801 T t296 o b168 b295
802 B b296 t296
803 T t297 o2 b5 b153 b296
804 B b297 t297
805 T t298 o1 b297
806 B b298 t298
807 P p298 Number 26
808 P p299 Number 48
809 O o299 location p298 p299
810 P p300 String Czf_itt_member
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_eq
817 O o301 parent p301
818 T t302 o301
819 B b302 t302
820 T t303 o b302 b4
821 B b303 t303
822 P p303 String Czf_itt_set
823 O o303 parent p303
824 T t304 o303
825 B b304 t304
826 T t305 o b304 b4
827 B b305 t305
828 P p305 String Czf_itt_comment
829 O o305 parent p305
830 T t306 o305
831 B b306 t306
832 T t307 o b306 b4
833 B b307 t307
834 P p307 String Itt_theory
835 O o307 parent p307
836 T t308 o307
837 B b308 t308
838 T t309 o b308 b4
839 B b309 t309
840 P p309 String Itt_fset
841 O o309 parent p309
842 T t310 o309
843 B b310 t310
844 T t311 o b310 b4
845 B b311 t311
846 P p311 String Itt_prop_decide
847 O o311 parent p311
848 T t312 o311
849 B b312 t312
850 T t313 o b312 b4
851 B b313 t313
852 P p313 String Itt_derive
853 O o313 parent p313
854 T t314 o313
855 B b314 t314
856 T t315 o b314 b4
857 B b315 t315
858 P p315 String Itt_list2
859 O o315 parent p315
860 T t316 o315
861 B b316 t316
862 T t317 o b316 b4
863 B b317 t317
864 P p317 String Itt_list
865 O o317 parent p317
866 T t318 o317
867 B b318 t318
868 T t319 o b318 b4
869 B b319 t319
870 P p319 String Itt_quotient
871 O o319 parent p319
872 T t320 o319
873 B b320 t320
874 T t321 o b320 b4
875 B b321 t321
876 P p321 String Itt_esquash
877 O o321 parent p321
878 T t322 o321
879 B b322 t322
880 T t323 o b322 b4
881 B b323 t323
882 P p323 String Itt_srec
883 O o323 parent p323
884 T t324 o323
885 B b324 t324
886 T t325 o b324 b4
887 B b325 t325
888 P p325 String Itt_prec
889 O o325 parent p325
890 T t326 o325
891 B b326 t326
892 T t327 o b326 b4
893 B b327 t327
894 P p327 String Itt_w
895 O o327 parent p327
896 T t328 o327
897 B b328 t328
898 T t329 o b328 b4
899 B b329 t329
900 P p329 String Itt_bunion
901 O o329 parent p329
902 T t330 o329
903 B b330 t330
904 T t331 o b330 b4
905 B b331 t331
906 P p331 String Itt_bisect
907 O o331 parent p331
908 T t332 o331
909 B b332 t332
910 T t333 o b332 b4
911 B b333 t333
912 P p333 String Itt_tunion
913 O o333 parent p333
914 T t334 o333
915 B b334 t334
916 T t335 o b334 b4
917 B b335 t335
918 P p335 String Itt_isect
919 O o335 parent p335
920 T t336 o335
921 B b336 t336
922 T t337 o b336 b4
923 B b337 t337
924 P p337 String Itt_struct2
925 O o337 parent p337
926 T t338 o337
927 B b338 t338
928 T t339 o b338 b4
929 B b339 t339
930 P p339 String Itt_well_founded
931 O o339 parent p339
932 T t340 o339
933 B b340 t340
934 T t341 o b340 b4
935 B b341 t341
936 P p341 String Itt_int_arith
937 O o341 parent p341
938 T t342 o341
939 B b342 t342
940 T t343 o b342 b4
941 B b343 t343
942 P p343 String Itt_atom_bool
943 O o343 parent p343
944 T t344 o343
945 B b344 t344
946 T t345 o b344 b4
947 B b345 t345
948 P p345 String Itt_atom
949 O o345 parent p345
950 T t346 o345
951 B b346 t346
952 T t347 o b346 b4
953 B b347 t347
954 T t348 o b347 b4
955 B b348 t348
956 T t349 o b345 b348
957 B b349 t349
958 T t350 o b343 b349
959 B b350 t350
960 T t351 o b341 b350
961 B b351 t351
962 T t352 o b339 b351
963 B b352 t352
964 T t353 o b337 b352
965 B b353 t353
966 T t354 o b335 b353
967 B b354 t354
968 T t355 o b333 b354
969 B b355 t355
970 T t356 o b331 b355
971 B b356 t356
972 T t357 o b329 b356
973 B b357 t357
974 T t358 o b327 b357
975 B b358 t358
976 T t359 o b325 b358
977 B b359 t359
978 T t360 o b323 b359
979 B b360 t360
980 T t361 o b321 b360
981 B b361 t361
982 T t362 o b319 b361
983 B b362 t362
984 T t363 o b317 b362
985 B b363 t363
986 T t364 o b315 b363
987 B b364 t364
988 T t365 o b313 b364
989 B b365 t365
990 T t366 o b311 b365
991 B b366 t366
992 T t367 o b309 b366
993 B b367 t367
994 T t368 o b307 b367
995 B b368 t368
996 T t369 o b305 b368
997 B b369 t369
998 T t370 o b303 b369
999 B b370 t370
1000 T t371 o b301 b370
1001 B b371 t371
1002 T t372 o2 b301 b371 b296
1003 B b372 t372
1004 T t373 o299 b372
1005 B b373 t373
1006 P p373 Number 49
1007 P p374 Number 67
1008 O o374 location p373 p374
1009 T t374 o2 b303 b4 b296
1010 B b374 t374
1011 T t375 o374 b374
1012 B b375 t375
1013 P p375 Number 68
1014 P p376 Number 88
1015 O o376 location p375 p376
1016 P p377 String Czf_itt_dall
1017 O o377 parent p377
1018 T t377 o377
1019 B b377 t377
1020 T t378 o b377 b4
1021 B b378 t378
1022 P p378 String Czf_itt_set_ind
1023 O o378 parent p378
1024 T t379 o378
1025 B b379 t379
1026 T t380 o b379 b4
1027 B b380 t380
1028 P p380 String Czf_itt_all
1029 O o380 parent p380
1030 T t381 o380
1031 B b381 t381
1032 T t382 o b381 b4
1033 B b382 t382
1034 P p382 String Czf_itt_sep
1035 O o382 parent p382
1036 T t383 o382
1037 B b383 t383
1038 T t384 o b383 b4
1039 B b384 t384
1040 T t385 o b384 b4
1041 B b385 t385
1042 T t386 o b382 b385
1043 B b386 t386
1044 T t387 o b380 b386
1045 B b387 t387
1046 T t388 o b378 b387
1047 B b388 t388
1048 T t389 o2 b378 b388 b296
1049 B b389 t389
1050 T t390 o376 b389
1051 B b390 t390
1052 P p390 Number 89
1053 P p391 Number 108
1054 O o391 location p390 p391
1055 P p392 String Czf_itt_and
1056 O o392 parent p392
1057 T t392 o392
1058 B b392 t392
1059 T t393 o b392 b4
1060 B b393 t393
1061 T t394 o b393 b4
1062 B b394 t394
1063 T t395 o2 b393 b394 b296
1064 B b395 t395
1065 T t396 o391 b395
1066 B b396 t396
1067 P p396 Number 109
1068 P p397 Number 130
1069 O o397 location p396 p397
1070 P p398 String Czf_itt_equiv
1071 O o398 parent p398
1072 T t398 o398
1073 B b398 t398
1074 T t399 o b398 b4
1075 B b399 t399
1076 P p399 String Czf_itt_pair
1077 O o399 parent p399
1078 T t400 o399
1079 B b400 t400
1080 T t401 o b400 b4
1081 B b401 t401
1082 P p401 String Czf_itt_singleton
1083 O o401 parent p401
1084 T t402 o401
1085 B b402 t402
1086 T t403 o b402 b4
1087 B b403 t403
1088 P p403 String Czf_itt_union
1089 O o403 parent p403
1090 T t404 o403
1091 B b404 t404
1092 T t405 o b404 b4
1093 B b405 t405
1094 P p405 String Czf_itt_subset
1095 O o405 parent p405
1096 T t406 o405
1097 B b406 t406
1098 T t407 o b406 b4
1099 B b407 t407
1100 P p407 String Czf_itt_dexists
1101 O o407 parent p407
1102 T t408 o407
1103 B b408 t408
1104 T t409 o b408 b4
1105 B b409 t409
1106 T t410 o b409 b4
1107 B b410 t410
1108 T t411 o b407 b410
1109 B b411 t411
1110 T t412 o b405 b411
1111 B b412 t412
1112 T t413 o b403 b412
1113 B b413 t413
1114 T t414 o b401 b413
1115 B b414 t414
1116 T t415 o b399 b414
1117 B b415 t415
1118 T t416 o2 b399 b415 b296
1119 B b416 t416
1120 T t417 o397 b416
1121 B b417 t417
1122 P p417 Number 132
1123 P p418 Number 143
1124 O o418 location p417 p418
1125 NSummary!summary_item summary_item summary_item Summary
1126 O o419 summary_item
1127 NOcaml!str_open str_open str_open Ocaml
1128 O o420 str_open p417 p418
1129 NOcaml!string string string Ocaml
1130 P p420 String Printf
1131 O o421 string p420
1132 T t421 o421
1133 B b421 t421
1134 T t422 o b421 b4
1135 B b422 t422
1136 T t423 o420 b422
1137 B b423 t423
1138 T t424 o419 b423
1139 B b424 t424
1140 T t425 o418 b424
1141 B b425 t425
1142 P p425 Number 144
1143 P p426 Number 157
1144 O o426 location p425 p426
1145 O o427 str_open p425 p426
1146 P p427 String Mp_debug
1147 O o428 string p427
1148 T t428 o428
1149 B b428 t428
1150 T t429 o b428 b4
1151 B b429 t429
1152 T t430 o427 b429
1153 B b430 t430
1154 T t431 o419 b430
1155 B b431 t431
1156 T t432 o426 b431
1157 B b432 t432
1158 P p432 Number 158
1159 P p433 Number 187
1160 O o433 location p432 p433
1161 O o434 str_open p432 p433
1162 P p434 String Refiner
1163 O o435 string p434
1164 T t435 o435
1165 B b435 t435
1166 P p435 String TermType
1167 O o436 string p435
1168 T t436 o436
1169 B b436 t436
1170 T t437 o b436 b4
1171 B b437 t437
1172 T t438 o b435 b437
1173 B b438 t438
1174 T t439 o b435 b438
1175 B b439 t439
1176 T t440 o434 b439
1177 B b440 t440
1178 T t441 o419 b440
1179 B b441 t441
1180 T t442 o433 b441
1181 B b442 t442
1182 P p442 Number 188
1183 P p443 Number 213
1184 O o443 location p442 p443
1185 O o444 str_open p442 p443
1186 P p444 String Term
1187 O o445 string p444
1188 T t445 o445
1189 B b445 t445
1190 T t446 o b445 b4
1191 B b446 t446
1192 T t447 o b435 b446
1193 B b447 t447
1194 T t448 o b435 b447
1195 B b448 t448
1196 T t449 o444 b448
1197 B b449 t449
1198 T t450 o419 b449
1199 B b450 t450
1200 T t451 o443 b450
1201 B b451 t451
1202 P p451 Number 214
1203 P p452 Number 241
1204 O o452 location p451 p452
1205 O o453 str_open p451 p452
1206 P p453 String TermOp
1207 O o454 string p453
1208 T t454 o454
1209 B b454 t454
1210 T t455 o b454 b4
1211 B b455 t455
1212 T t456 o b435 b455
1213 B b456 t456
1214 T t457 o b435 b456
1215 B b457 t457
1216 T t458 o453 b457
1217 B b458 t458
1218 T t459 o419 b458
1219 B b459 t459
1220 T t460 o452 b459
1221 B b460 t460
1222 P p460 Number 242
1223 P p461 Number 271
1224 O o461 location p460 p461
1225 O o462 str_open p460 p461
1226 P p462 String TermAddr
1227 O o463 string p462
1228 T t463 o463
1229 B b463 t463
1230 T t464 o b463 b4
1231 B b464 t464
1232 T t465 o b435 b464
1233 B b465 t465
1234 T t466 o b435 b465
1235 B b466 t466
1236 T t467 o462 b466
1237 B b467 t467
1238 T t468 o419 b467
1239 B b468 t468
1240 T t469 o461 b468
1241 B b469 t469
1242 P p469 Number 272
1243 P p470 Number 300
1244 O o470 location p469 p470
1245 O o471 str_open p469 p470
1246 P p471 String TermMan
1247 O o472 string p471
1248 T t472 o472
1249 B b472 t472
1250 T t473 o b472 b4
1251 B b473 t473
1252 T t474 o b435 b473
1253 B b474 t474
1254 T t475 o b435 b474
1255 B b475 t475
1256 T t476 o471 b475
1257 B b476 t476
1258 T t477 o419 b476
1259 B b477 t477
1260 T t478 o470 b477
1261 B b478 t478
1262 P p478 Number 301
1263 P p479 Number 331
1264 O o479 location p478 p479
1265 O o480 str_open p478 p479
1266 P p480 String TermSubst
1267 O o481 string p480
1268 T t481 o481
1269 B b481 t481
1270 T t482 o b481 b4
1271 B b482 t482
1272 T t483 o b435 b482
1273 B b483 t483
1274 T t484 o b435 b483
1275 B b484 t484
1276 T t485 o480 b484
1277 B b485 t485
1278 T t486 o419 b485
1279 B b486 t486
1280 T t487 o479 b486
1281 B b487 t487
1282 P p487 Number 332
1283 P p488 Number 359
1284 O o488 location p487 p488
1285 O o489 str_open p487 p488
1286 P p489 String Refine
1287 O o490 string p489
1288 T t490 o490
1289 B b490 t490
1290 T t491 o b490 b4
1291 B b491 t491
1292 T t492 o b435 b491
1293 B b492 t492
1294 T t493 o b435 b492
1295 B b493 t493
1296 T t494 o489 b493
1297 B b494 t494
1298 T t495 o419 b494
1299 B b495 t495
1300 T t496 o488 b495
1301 B b496 t496
1302 P p496 Number 360
1303 P p497 Number 392
1304 O o497 location p496 p497
1305 O o498 str_open p496 p497
1306 P p498 String RefineError
1307 O o499 string p498
1308 T t499 o499
1309 B b499 t499
1310 T t500 o b499 b4
1311 B b500 t500
1312 T t501 o b435 b500
1313 B b501 t501
1314 T t502 o b435 b501
1315 B b502 t502
1316 T t503 o498 b502
1317 B b503 t503
1318 T t504 o419 b503
1319 B b504 t504
1320 T t505 o497 b504
1321 B b505 t505
1322 P p505 Number 393
1323 P p506 Number 409
1324 O o506 location p505 p506
1325 O o507 str_open p505 p506
1326 P p507 String Mp_resource
1327 O o508 string p507
1328 T t508 o508
1329 B b508 t508
1330 T t509 o b508 b4
1331 B b509 t509
1332 T t510 o507 b509
1333 B b510 t510
1334 T t511 o419 b510
1335 B b511 t511
1336 T t512 o506 b511
1337 B b512 t512
1338 P p512 Number 410
1339 P p513 Number 427
1340 O o513 location p512 p513
1341 O o514 str_open p512 p513
1342 P p514 String Simple_print
1343 O o515 string p514
1344 T t515 o515
1345 B b515 t515
1346 T t516 o b515 b4
1347 B b516 t516
1348 T t517 o514 b516
1349 B b517 t517
1350 T t518 o419 b517
1351 B b518 t518
1352 T t519 o513 b518
1353 B b519 t519
1354 P p519 Number 429
1355 P p520 Number 445
1356 O o520 location p519 p520
1357 O o521 str_open p519 p520
1358 P p521 String Tactic_type
1359 O o522 string p521
1360 T t522 o522
1361 B b522 t522
1362 T t523 o b522 b4
1363 B b523 t523
1364 T t524 o521 b523
1365 B b524 t524
1366 T t525 o419 b524
1367 B b525 t525
1368 T t526 o520 b525
1369 B b526 t526
1370 P p526 Number 446
1371 P p527 Number 472
1372 O o527 location p526 p527
1373 O o528 str_open p526 p527
1374 P p528 String Tacticals
1375 O o529 string p528
1376 T t529 o529
1377 B b529 t529
1378 T t530 o b529 b4
1379 B b530 t530
1380 T t531 o b522 b530
1381 B b531 t531
1382 T t532 o528 b531
1383 B b532 t532
1384 T t533 o419 b532
1385 B b533 t533
1386 T t534 o527 b533
1387 B b534 t534
1388 P p534 Number 473
1389 P p535 Number 497
1390 O o535 location p534 p535
1391 O o536 str_open p534 p535
1392 P p536 String Sequent
1393 O o537 string p536
1394 T t537 o537
1395 B b537 t537
1396 T t538 o b537 b4
1397 B b538 t538
1398 T t539 o b522 b538
1399 B b539 t539
1400 T t540 o536 b539
1401 B b540 t540
1402 T t541 o419 b540
1403 B b541 t541
1404 T t542 o535 b541
1405 B b542 t542
1406 P p542 Number 498
1407 P p543 Number 528
1408 O o543 location p542 p543
1409 O o544 str_open p542 p543
1410 P p544 String Conversionals
1411 O o545 string p544
1412 T t545 o545
1413 B b545 t545
1414 T t546 o b545 b4
1415 B b546 t546
1416 T t547 o b522 b546
1417 B b547 t547
1418 T t548 o544 b547
1419 B b548 t548
1420 T t549 o419 b548
1421 B b549 t549
1422 T t550 o543 b549
1423 B b550 t550
1424 P p550 Number 529
1425 P p551 Number 539
1426 O o551 location p550 p551
1427 O o552 str_open p550 p551
1428 O o553 string p91
1429 T t553 o553
1430 B b553 t553
1431 T t554 o b553 b4
1432 B b554 t554
1433 T t555 o552 b554
1434 B b555 t555
1435 T t556 o419 b555
1436 B b556 t556
1437 T t557 o551 b556
1438 B b557 t557
1439 P p557 Number 540
1440 P p558 Number 548
1441 O o558 location p557 p558
1442 O o559 str_open p557 p558
1443 O o560 string p89
1444 T t560 o560
1445 B b560 t560
1446 T t561 o b560 b4
1447 B b561 t561
1448 T t562 o559 b561
1449 B b562 t562
1450 T t563 o419 b562
1451 B b563 t563
1452 T t564 o558 b563
1453 B b564 t564
1454 P p564 Number 550
1455 P p565 Number 567
1456 O o565 location p564 p565
1457 O o566 str_open p564 p565
1458 O o567 string p79
1459 T t567 o567
1460 B b567 t567
1461 T t568 o b567 b4
1462 B b568 t568
1463 T t569 o566 b568
1464 B b569 t569
1465 T t570 o419 b569
1466 B b570 t570
1467 T t571 o565 b570
1468 B b571 t571
1469 P p571 Number 568
1470 P p572 Number 589
1471 O o572 location p571 p572
1472 O o573 str_open p571 p572
1473 O o574 string p81
1474 T t574 o574
1475 B b574 t574
1476 T t575 o b574 b4
1477 B b575 t575
1478 T t576 o573 b575
1479 B b576 t576
1480 T t577 o419 b576
1481 B b577 t577
1482 T t578 o572 b577
1483 B b578 t578
1484 P p578 Number 591
1485 P p579 Number 608
1486 O o579 location p578 p579
1487 NSummary!opname opname opname Summary
1488 P p580 String group
1489 O o580 opname p580
1490 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1491 NCzf_itt_group!group group group Czf_itt_group
1492 O o581 group
1493 Nvar var var NIL
1494 P p581 Var g
1495 O o582 var p581
1496 T t582 o582
1497 B b582 t582
1498 T t583 o581 b582
1499 B b583 t583
1500 T t584 o580 b583
1501 B b584 t584
1502 T t585 o579 b584
1503 B b585 t585
1504 P p585 Number 609
1505 P p586 Number 624
1506 O o586 location p585 p586
1507 P p587 String car
1508 O o587 opname p587
1509 NCzf_itt_group!car car car Czf_itt_group
1510 O o588 car
1511 T t588 o588 b582
1512 B b588 t588
1513 T t589 o587 b588
1514 B b589 t589
1515 T t590 o586 b589
1516 B b590 t590
1517 P p590 Number 671
1518 P p591 Number 686
1519 O o591 location p590 p591
1520 P p592 String eqG
1521 O o592 opname p592
1522 NCzf_itt_group!eqG eqG eqG Czf_itt_group
1523 O o593 eqG
1524 T t593 o593 b582
1525 B b593 t593
1526 T t594 o592 b593
1527 B b594 t594
1528 T t595 o591 b594
1529 B b595 t595
1530 P p595 Number 812
1531 P p596 Number 834
1532 O o596 location p595 p596
1533 P p597 String op
1534 O o597 opname p597
1535 NCzf_itt_group!op op op Czf_itt_group
1536 O o598 op
1537 P p598 Var a
1538 O o599 var p598
1539 T t599 o599
1540 B b599 t599
1541 P p599 Var b
1542 O o600 var p599
1543 T t600 o600
1544 B b600 t600
1545 T t601 o598 b582 b599 b600
1546 B b601 t601
1547 T t602 o597 b601
1548 B b602 t602
1549 T t603 o596 b602
1550 B b603 t603
1551 P p603 Number 835
1552 P p604 Number 849
1553 O o604 location p603 p604
1554 P p605 String id
1555 O o605 opname p605
1556 NCzf_itt_group!id id id Czf_itt_group
1557 O o606 id
1558 T t606 o606 b582
1559 B b606 t606
1560 T t607 o605 b606
1561 B b607 t607
1562 T t608 o604 b607
1563 B b608 t608
1564 P p608 Number 850
1565 P p609 Number 869
1566 O o609 location p608 p609
1567 P p610 String inv
1568 O o610 opname p610
1569 NCzf_itt_group!inv inv inv Czf_itt_group
1570 O o611 inv
1571 T t611 o611 b582 b599
1572 B b611 t611
1573 T t612 o610 b611
1574 B b612 t612
1575 T t613 o609 b612
1576 B b613 t613
1577 P p613 Number 1012
1578 P p614 Number 1082
1579 O o614 location p613 p614
1580 NSummary!dform dform dform Summary
1581 P p615 String group_df
1582 O o615 dform p615
1583 NSummary!except_mode_df except_mode_df except_mode_df Summary
1584 P p616 String src
1585 O o616 except_mode_df p616
1586 T t616 o616
1587 B b616 t616
1588 T t617 o b616 b4
1589 B b617 t617
1590 NSummary!df_term df_term df_term Summary
1591 O o617 df_term
1592 Nslot slot slot NIL
1593 O o618 slot
1594 T t618 o618 b582
1595 B b618 t618
1596 NPerv!string string618 string Perv
1597 P p618 String " group"
1598 O o619 string618 p618
1599 T t619 o619
1600 B b619 t619
1601 T t620 o b619 b4
1602 B b620 t620
1603 T t621 o b618 b620
1604 B b621 t621
1605 T t622 o617 b621
1606 B b622 t622
1607 T t623 o615 b617 b583 b622
1608 B b623 t623
1609 T t624 o614 b623
1610 B b624 t624
1611 P p624 Number 1084
1612 P p625 Number 1153
1613 O o625 location p624 p625
1614 P p626 String car_df
1615 O o626 dform p626
1616 P p627 String car(
1617 O o627 string618 p627
1618 T t627 o627
1619 B b627 t627
1620 P p628 String )
1621 O o628 string618 p628
1622 T t628 o628
1623 B b628 t628
1624 T t629 o b628 b4
1625 B b629 t629
1626 T t630 o b618 b629
1627 B b630 t630
1628 T t631 o b627 b630
1629 B b631 t631
1630 T t632 o617 b631
1631 B b632 t632
1632 T t633 o626 b617 b588 b632
1633 B b633 t633
1634 T t634 o625 b633
1635 B b634 t634
1636 P p634 Number 1155
1637 P p635 Number 1225
1638 O o635 location p634 p635
1639 P p636 String eqG_df1
1640 O o636 dform p636
1641 P p637 String eqG(
1642 O o637 string618 p637
1643 T t637 o637
1644 B b637 t637
1645 T t638 o b637 b630
1646 B b638 t638
1647 T t639 o617 b638
1648 B b639 t639
1649 T t640 o636 b617 b593 b639
1650 B b640 t640
1651 T t641 o635 b640
1652 B b641 t641
1653 P p641 Number 1342
1654 P p642 Number 1408
1655 O o642 location p641 p642
1656 P p643 String id_df
1657 O o643 dform p643
1658 P p644 String id(
1659 O o644 string618 p644
1660 T t644 o644
1661 B b644 t644
1662 T t645 o b644 b630
1663 B b645 t645
1664 T t646 o617 b645
1665 B b646 t646
1666 T t647 o643 b617 b606 b646
1667 B b647 t647
1668 T t648 o642 b647
1669 B b648 t648
1670 P p648 Number 1410
1671 P p649 Number 1525
1672 O o649 location p648 p649
1673 P p650 String op_df
1674 O o650 dform p650
1675 NSummary!parens_df parens_df parens_df Summary
1676 O o651 parens_df
1677 T t651 o651
1678 B b651 t651
1679 T t652 o b651 b4
1680 B b652 t652
1681 T t653 o b616 b652
1682 B b653 t653
1683 P p653 String op(
1684 O o653 string618 p653
1685 T t654 o653
1686 B b654 t654
1687 P p654 String "; "
1688 O o654 string618 p654
1689 T t655 o654
1690 B b655 t655
1691 T t656 o618 b599
1692 B b656 t656
1693 T t657 o618 b600
1694 B b657 t657
1695 T t658 o b657 b629
1696 B b658 t658
1697 T t659 o b655 b658
1698 B b659 t659
1699 T t660 o b656 b659
1700 B b660 t660
1701 T t661 o b655 b660
1702 B b661 t661
1703 T t662 o b618 b661
1704 B b662 t662
1705 T t663 o b654 b662
1706 B b663 t663
1707 T t664 o617 b663
1708 B b664 t664
1709 T t665 o650 b653 b601 b664
1710 B b665 t665
1711 T t666 o649 b665
1712 B b666 t666
1713 P p666 Number 1527
1714 P p667 Number 1625
1715 O o667 location p666 p667
1716 P p668 String inv_df
1717 O o668 dform p668
1718 P p669 String inv(
1719 O o669 string618 p669
1720 T t669 o669
1721 B b669 t669
1722 T t670 o b656 b629
1723 B b670 t670
1724 T t671 o b655 b670
1725 B b671 t671
1726 T t672 o b618 b671
1727 B b672 t672
1728 T t673 o b669 b672
1729 B b673 t673
1730 T t674 o617 b673
1731 B b674 t674
1732 T t675 o668 b653 b611 b674
1733 B b675 t675
1734 T t676 o667 b675
1735 B b676 t676
1736 P p676 Number 1644
1737 P p677 Number 1778
1738 O o677 location p676 p677
1739 NSummary!rule rule rule Summary
1740 P p678 String group_type
1741 O o678 rule p678
1742 NSummary!context_param context_param context_param Summary
1743 P p679 String H
1744 O o679 context_param p679
1745 T t679 o679
1746 B b679 t679
1747 T t680 o b679 b4
1748 B b680 t680
1749 NSummary!meta_implies meta_implies meta_implies Summary
1750 O o680 meta_implies
1751 NSummary!meta_theorem meta_theorem meta_theorem Summary
1752 O o681 meta_theorem
1753 NBase_trivial Base_trivial Base_trivial NIL
1754 NBase_trivial!squash squash squash Base_trivial
1755 O o682 squash
1756 T t682 o682
1757 B b682 t682
1758 T t683 o b682 b4
1759 C h H
1760 NItt_equal Itt_equal Itt_equal NIL
1761 NItt_equal!equal equal equal Itt_equal
1762 O o683 equal
1763 NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1764 NItt_record_label0!label label label Itt_record_label0
1765 O o684 label
1766 T t684 o684
1767 B b684 t684
1768 T t685 o683 b684 b582 b582
1769 S s t683 h
1770 G s t685
1771 B b685 s
1772 T t686 o681 b685
1773 B b686 t686
1774 P p686 Var ext
1775 O o686 var p686
1776 T t687 o686
1777 B b687 t687
1778 T t688 o b687 b4
1779 NItt_equal!type type type Itt_equal
1780 O o688 type
1781 T t689 o688 b583
1782 S s689 t688 h
1783 G s689 t689
1784 B b689 s689
1785 T t690 o681 b689
1786 B b690 t690
1787 T t691 o680 b686 b690
1788 B b691 t691
1789 NSummary!incomplete incomplete incomplete Summary
1790 O o691 incomplete
1791 T t692 o691
1792 B b692 t692
1793 NSummary!resource_defs resource_defs resource_defs Summary
1794 P p692 Number 1670
1795 P p693 Number 1678
1796 O o693 resource_defs p692 p693 p204
1797 NOcaml!uid uid uid Ocaml
1798 P p694 Number 1676
1799 O o694 uid p694 p693
1800 P p695 String []
1801 O o695 uid p695
1802 T t695 o695
1803 B b695 t695
1804 T t696 o694 b695
1805 B b696 t696
1806 T t697 o b696 b4
1807 B b697 t697
1808 T t698 o693 b697
1809 B b698 t698
1810 T t699 o b698 b4
1811 B b699 t699
1812 T t700 o678 b680 b691 b692 b699
1813 B b700 t700
1814 T t701 o677 b700
1815 B b701 t701
1816 P p701 Number 1780
1817 P p702 Number 1906
1818 O o702 location p701 p702
1819 P p703 String car_wf
1820 O o703 rule p703
1821 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1822 NCzf_itt_set!isset isset isset Czf_itt_set
1823 O o704 isset
1824 T t704 o704 b588
1825 S s704 t688 h
1826 G s704 t704
1827 B b704 s704
1828 T t705 o681 b704
1829 B b705 t705
1830 T t706 o680 b686 b705
1831 B b706 t706
1832 P p706 Number 1802
1833 P p707 Number 1809
1834 O o707 resource_defs p706 p707 p204
1835 P p708 Number 1807
1836 O o708 uid p708 p707
1837 T t708 o708 b695
1838 B b708 t708
1839 T t709 o b708 b4
1840 B b709 t709
1841 T t710 o707 b709
1842 B b710 t710
1843 T t711 o b710 b4
1844 B b711 t711
1845 T t712 o703 b680 b706 b692 b711
1846 B b712 t712
1847 T t713 o702 b712
1848 B b713 t713
1849 P p713 Number 1908
1850 P p714 Number 2035
1851 O o714 location p713 p714
1852 P p715 String eqG_wf1
1853 O o715 rule p715
1854 T t715 o704 b593
1855 S s715 t688 h
1856 G s715 t715
1857 B b715 s715
1858 T t716 o681 b715
1859 B b716 t716
1860 T t717 o680 b686 b716
1861 B b717 t717
1862 P p717 Number 1931
1863 P p718 Number 1938
1864 O o718 resource_defs p717 p718 p204
1865 P p719 Number 1936
1866 O o719 uid p719 p718
1867 T t719 o719 b695
1868 B b719 t719
1869 T t720 o b719 b4
1870 B b720 t720
1871 T t721 o718 b720
1872 B b721 t721
1873 T t722 o b721 b4
1874 B b722 t722
1875 T t723 o715 b680 b717 b692 b722
1876 B b723 t723
1877 T t724 o714 b723
1878 B b724 t724
1879 P p724 Number 2037
1880 P p725 Number 2215
1881 O o725 location p724 p725
1882 P p726 String eqG_wf2
1883 O o726 rule p726
1884 S s726 t688 h
1885 G s726 t583
1886 B b726 s726
1887 T t726 o681 b726
1888 B b727 t726
1889 NCzf_itt_equiv Czf_itt_equiv Czf_itt_equiv NIL
1890 NCzf_itt_equiv!equiv equiv equiv Czf_itt_equiv
1891 O o727 equiv
1892 T t727 o727 b588 b593
1893 S s727 t688 h
1894 G s727 t727
1895 B b728 s727
1896 T t728 o681 b728
1897 B b729 t728
1898 T t729 o680 b727 b729
1899 B b730 t729
1900 T t730 o680 b686 b730
1901 B b731 t730
1902 P p731 Number 2060
1903 P p732 Number 2067
1904 O o732 resource_defs p731 p732 p204
1905 P p733 Number 2065
1906 O o733 uid p733 p732
1907 T t733 o733 b695
1908 B b733 t733
1909 T t734 o b733 b4
1910 B b734 t734
1911 T t735 o732 b734
1912 B b735 t735
1913 T t736 o b735 b4
1914 B b736 t736
1915 T t737 o726 b680 b731 b692 b736
1916 B b737 t737
1917 T t738 o725 b737
1918 B b738 t738
1919 P p738 Number 2910
1920 P p739 Number 3134
1921 O o739 location p738 p739
1922 P p740 String op_wf
1923 O o740 rule p740
1924 P p741 Var s1
1925 O o741 var p741
1926 T t741 o741
1927 B b741 t741
1928 T t742 o704 b741
1929 S s742 t683 h
1930 G s742 t742
1931 B b742 s742
1932 T t743 o681 b742
1933 B b743 t743
1934 P p743 Var s2
1935 O o743 var p743
1936 T t744 o743
1937 B b744 t744
1938 T t745 o704 b744
1939 S s745 t683 h
1940 G s745 t745
1941 B b745 s745
1942 T t746 o681 b745
1943 B b746 t746
1944 T t747 o598 b582 b741 b744
1945 B b747 t747
1946 T t748 o704 b747
1947 S s748 t688 h
1948 G s748 t748
1949 B b748 s748
1950 T t749 o681 b748
1951 B b749 t749
1952 T t750 o680 b746 b749
1953 B b750 t750
1954 T t751 o680 b743 b750
1955 B b751 t751
1956 T t752 o680 b686 b751
1957 B b752 t752
1958 P p752 Number 2938
1959 O o752 resource_defs p230 p752 p204
1960 P p753 Number 2936
1961 O o753 uid p753 p752
1962 T t753 o753 b695
1963 B b753 t753
1964 T t754 o b753 b4
1965 B b754 t754
1966 T t755 o752 b754
1967 B b755 t755
1968 T t756 o b755 b4
1969 B b756 t756
1970 T t757 o740 b680 b752 b692 b756
1971 B b757 t757
1972 T t758 o739 b757
1973 B b758 t758
1974 P p758 Number 3136
1975 P p759 Number 3514
1976 O o759 location p758 p759
1977 P p760 String op_closure
1978 O o760 rule p760
1979 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1980 NCzf_itt_member!mem mem mem Czf_itt_member
1981 O o761 mem
1982 T t761 o761 b741 b588
1983 S s761 t688 h
1984 G s761 t761
1985 B b761 s761
1986 T t762 o681 b761
1987 B b762 t762
1988 T t763 o761 b744 b588
1989 S s763 t688 h
1990 G s763 t763
1991 B b763 s763
1992 T t764 o681 b763
1993 B b764 t764
1994 T t765 o761 b747 b588
1995 S s765 t688 h
1996 G s765 t765
1997 B b765 s765
1998 T t766 o681 b765
1999 B b766 t766
2000 T t767 o680 b764 b766
2001 B b767 t767
2002 T t768 o680 b762 b767
2003 B b768 t768
2004 T t769 o680 b727 b768
2005 B b769 t769
2006 T t770 o680 b686 b769
2007 B b770 t770
2008 T t771 o680 b746 b770
2009 B b771 t771
2010 T t772 o680 b743 b771
2011 B b772 t772
2012 P p772 Number 3162
2013 P p773 Number 3169
2014 O o773 resource_defs p772 p773 p204
2015 P p774 Number 3167
2016 O o774 uid p774 p773
2017 T t774 o774 b695
2018 B b774 t774
2019 T t775 o b774 b4
2020 B b775 t775
2021 T t776 o773 b775
2022 B b776 t776
2023 T t777 o b776 b4
2024 B b777 t777
2025 T t778 o760 b680 b772 b692 b777
2026 B b778 t778
2027 T t779 o759 b778
2028 B b779 t779
2029 P p779 Number 3516
2030 P p780 Number 4081
2031 O o780 location p779 p780
2032 P p781 String op_eqG1
2033 O o781 rule p781
2034 P p782 Var s3
2035 O o782 var p782
2036 T t782 o782
2037 B b782 t782
2038 T t783 o704 b782
2039 S s783 t683 h
2040 G s783 t783
2041 B b783 s783
2042 T t784 o681 b783
2043 B b784 t784
2044 T t785 o761 b782 b588
2045 S s785 t688 h
2046 G s785 t785
2047 B b785 s785
2048 T t786 o681 b785
2049 B b786 t786
2050 T t787 o727 b588 b593 b741 b744
2051 S s787 t688 h
2052 G s787 t787
2053 B b787 s787
2054 T t788 o681 b787
2055 B b788 t788
2056 T t789 o598 b582 b782 b741
2057 B b789 t789
2058 T t790 o598 b582 b782 b744
2059 B b790 t790
2060 T t791 o727 b588 b593 b789 b790
2061 S s791 t688 h
2062 G s791 t791
2063 B b791 s791
2064 T t792 o681 b791
2065 B b792 t792
2066 T t793 o680 b788 b792
2067 B b793 t793
2068 T t794 o680 b786 b793
2069 B b794 t794
2070 T t795 o680 b764 b794
2071 B b795 t795
2072 T t796 o680 b762 b795
2073 B b796 t796
2074 T t797 o680 b727 b796
2075 B b797 t797
2076 T t798 o680 b686 b797
2077 B b798 t798
2078 T t799 o680 b784 b798
2079 B b799 t799
2080 T t800 o680 b746 b799
2081 B b800 t800
2082 T t801 o680 b743 b800
2083 B b801 t801
2084 P p801 Number 3539
2085 P p802 Number 3546
2086 O o802 resource_defs p801 p802 p204
2087 P p803 Number 3544
2088 O o803 uid p803 p802
2089 T t803 o803 b695
2090 B b803 t803
2091 T t804 o b803 b4
2092 B b804 t804
2093 T t805 o802 b804
2094 B b805 t805
2095 T t806 o b805 b4
2096 B b806 t806
2097 T t807 o781 b680 b801 b692 b806
2098 B b807 t807
2099 T t808 o780 b807
2100 B b808 t808
2101 P p808 Number 4083
2102 P p809 Number 4648
2103 O o809 location p808 p809
2104 P p810 String op_eqG2
2105 O o810 rule p810
2106 T t810 o598 b582 b741 b782
2107 B b810 t810
2108 T t811 o598 b582 b744 b782
2109 B b811 t811
2110 T t812 o727 b588 b593 b810 b811
2111 S s812 t688 h
2112 G s812 t812
2113 B b812 s812
2114 T t813 o681 b812
2115 B b813 t813
2116 T t814 o680 b788 b813
2117 B b814 t814
2118 T t815 o680 b786 b814
2119 B b815 t815
2120 T t816 o680 b764 b815
2121 B b816 t816
2122 T t817 o680 b762 b816
2123 B b817 t817
2124 T t818 o680 b727 b817
2125 B b818 t818
2126 T t819 o680 b686 b818
2127 B b819 t819
2128 T t820 o680 b784 b819
2129 B b820 t820
2130 T t821 o680 b746 b820
2131 B b821 t821
2132 T t822 o680 b743 b821
2133 B b822 t822
2134 P p822 Number 4106
2135 P p823 Number 4113
2136 O o823 resource_defs p822 p823 p204
2137 P p824 Number 4111
2138 O o824 uid p824 p823
2139 T t824 o824 b695
2140 B b824 t824
2141 T t825 o b824 b4
2142 B b825 t825
2143 T t826 o823 b825
2144 B b826 t826
2145 T t827 o b826 b4
2146 B b827 t827
2147 T t828 o810 b680 b822 b692 b827
2148 B b828 t828
2149 T t829 o809 b828
2150 B b829 t829
2151 P p829 Number 4650
2152 P p830 Number 4903
2153 O o830 location p829 p830
2154 P p831 String op_eqG_fun1
2155 O o831 rule p831
2156 P p832 Var s
2157 O o832 var p832
2158 T t832 o832
2159 B b832 t832
2160 T t833 o704 b832
2161 S s833 t683 h
2162 G s833 t833
2163 B b833 s833
2164 T t834 o681 b833
2165 B b834 t834
2166 NCzf_itt_equiv!equiv_fun_set equiv_fun_set equiv_fun_set Czf_itt_equiv
2167 O o834 equiv_fun_set
2168 P p834 Var z
2169 O o835 var p834
2170 T t835 o835
2171 B b835 t835
2172 T t836 o598 b582 b835 b832
2173 B b836 t836 z
2174 T t837 o834 b588 b593 b836
2175 S s837 t688 h
2176 G s837 t837
2177 B b837 s837
2178 T t838 o681 b837
2179 B b838 t838
2180 T t839 o680 b727 b838
2181 B b839 t839
2182 T t840 o680 b686 b839
2183 B b840 t840
2184 T t841 o680 b834 b840
2185 B b841 t841
2186 P p841 Number 4677
2187 P p842 Number 4684
2188 O o842 resource_defs p841 p842 p204
2189 P p843 Number 4682
2190 O o843 uid p843 p842
2191 T t843 o843 b695
2192 B b843 t843
2193 T t844 o b843 b4
2194 B b844 t844
2195 T t845 o842 b844
2196 B b845 t845
2197 T t846 o b845 b4
2198 B b846 t846
2199 T t847 o831 b680 b841 b692 b846
2200 B b847 t847
2201 T t848 o830 b847
2202 B b848 t848
2203 P p848 Number 4905
2204 P p849 Number 5160
2205 O o849 location p848 p849
2206 P p850 String op_equiv_fun2
2207 O o850 rule p850
2208 T t850 o598 b582 b832 b835
2209 B b850 t850 z
2210 T t851 o834 b588 b593 b850
2211 S s851 t688 h
2212 G s851 t851
2213 B b851 s851
2214 T t852 o681 b851
2215 B b852 t852
2216 T t853 o680 b727 b852
2217 B b853 t853
2218 T t854 o680 b686 b853
2219 B b854 t854
2220 T t855 o680 b834 b854
2221 B b855 t855
2222 P p855 Number 4934
2223 P p856 Number 4941
2224 O o856 resource_defs p855 p856 p204
2225 P p857 Number 4939
2226 O o857 uid p857 p856
2227 T t857 o857 b695
2228 B b857 t857
2229 T t858 o b857 b4
2230 B b858 t858
2231 T t859 o856 b858
2232 B b859 t859
2233 T t860 o b859 b4
2234 B b860 t860
2235 T t861 o850 b680 b855 b692 b860
2236 B b861 t861
2237 T t862 o849 b861
2238 B b862 t862
2239 P p862 Number 5162
2240 P p863 Number 5390
2241 O o863 location p862 p863
2242 P p864 String op_eq_fun1
2243 O o864 rule p864
2244 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
2245 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
2246 O o865 fun_set
2247 T t865 o865 b836
2248 S s865 t688 h
2249 G s865 t865
2250 B b865 s865
2251 T t866 o681 b865
2252 B b866 t866
2253 T t867 o680 b727 b866
2254 B b867 t867
2255 T t868 o680 b686 b867
2256 B b868 t868
2257 T t869 o680 b834 b868
2258 B b869 t869
2259 P p869 Number 5188
2260 P p870 Number 5195
2261 O o870 resource_defs p869 p870 p204
2262 P p871 Number 5193
2263 O o871 uid p871 p870
2264 T t871 o871 b695
2265 B b871 t871
2266 T t872 o b871 b4
2267 B b872 t872
2268 T t873 o870 b872
2269 B b873 t873
2270 T t874 o b873 b4
2271 B b874 t874
2272 T t875 o864 b680 b869 b692 b874
2273 B b875 t875
2274 T t876 o863 b875
2275 B b876 t876
2276 P p876 Number 5392
2277 P p877 Number 5620
2278 O o877 location p876 p877
2279 P p878 String op_eq_fun2
2280 O o878 rule p878
2281 T t878 o865 b850
2282 S s878 t688 h
2283 G s878 t878
2284 B b878 s878
2285 T t879 o681 b878
2286 B b879 t879
2287 T t880 o680 b727 b879
2288 B b880 t880
2289 T t881 o680 b686 b880
2290 B b881 t881
2291 T t882 o680 b834 b881
2292 B b882 t882
2293 P p882 Number 5418
2294 P p883 Number 5425
2295 O o883 resource_defs p882 p883 p204
2296 P p884 Number 5423
2297 O o884 uid p884 p883
2298 T t884 o884 b695
2299 B b884 t884
2300 T t885 o b884 b4
2301 B b885 t885
2302 T t886 o883 b885
2303 B b886 t886
2304 T t887 o b886 b4
2305 B b887 t887
2306 T t888 o878 b680 b882 b692 b887
2307 B b888 t888
2308 T t889 o877 b888
2309 B b889 t889
2310 P p889 Number 5622
2311 P p890 Number 6149
2312 O o890 location p889 p890
2313 P p891 String op_assoc1
2314 O o891 rule p891
2315 T t891 o598 b582 b747 b782
2316 B b891 t891
2317 T t892 o598 b582 b741 b811
2318 B b892 t892
2319 T t893 o727 b588 b593 b891 b892
2320 S s893 t688 h
2321 G s893 t893
2322 B b893 s893
2323 T t894 o681 b893
2324 B b894 t894
2325 T t895 o680 b786 b894
2326 B b895 t895
2327 T t896 o680 b764 b895
2328 B b896 t896
2329 T t897 o680 b762 b896
2330 B b897 t897
2331 T t898 o680 b727 b897
2332 B b898 t898
2333 T t899 o680 b686 b898
2334 B b899 t899
2335 T t900 o680 b784 b899
2336 B b900 t900
2337 T t901 o680 b746 b900
2338 B b901 t901
2339 T t902 o680 b743 b901
2340 B b902 t902
2341 P p902 Number 5647
2342 P p903 Number 5654
2343 O o903 resource_defs p902 p903 p204
2344 P p904 Number 5652
2345 O o904 uid p904 p903
2346 T t904 o904 b695
2347 B b904 t904
2348 T t905 o b904 b4
2349 B b905 t905
2350 T t906 o903 b905
2351 B b906 t906
2352 T t907 o b906 b4
2353 B b907 t907
2354 T t908 o891 b680 b902 b692 b907
2355 B b908 t908
2356 T t909 o890 b908
2357 B b909 t909
2358 P p909 Number 6151
2359 P p910 Number 6678
2360 O o910 location p909 p910
2361 P p911 String op_assoc2
2362 O o911 rule p911
2363 T t911 o727 b588 b593 b892 b891
2364 S s911 t688 h
2365 G s911 t911
2366 B b911 s911
2367 T t912 o681 b911
2368 B b912 t912
2369 T t913 o680 b786 b912
2370 B b913 t913
2371 T t914 o680 b764 b913
2372 B b914 t914
2373 T t915 o680 b762 b914
2374 B b915 t915
2375 T t916 o680 b727 b915
2376 B b916 t916
2377 T t917 o680 b686 b916
2378 B b917 t917
2379 T t918 o680 b784 b917
2380 B b918 t918
2381 T t919 o680 b746 b918
2382 B b919 t919
2383 T t920 o680 b743 b919
2384 B b920 t920
2385 P p920 Number 6176
2386 O o920 resource_defs p920 p202 p204
2387 O o921 uid p197 p202
2388 T t921 o921 b695
2389 B b921 t921
2390 T t922 o b921 b4
2391 B b922 t922
2392 T t923 o920 b922
2393 B b923 t923
2394 T t924 o b923 b4
2395 B b924 t924
2396 T t925 o911 b680 b920 b692 b924
2397 B b925 t925
2398 T t926 o910 b925
2399 B b926 t926
2400 P p926 Number 6680
2401 P p927 Number 6806
2402 O o927 location p926 p927
2403 P p928 String id_wf1
2404 O o928 rule p928
2405 T t928 o704 b606
2406 S s928 t688 h
2407 G s928 t928
2408 B b928 s928
2409 T t929 o681 b928
2410 B b929 t929
2411 T t930 o680 b686 b929
2412 B b930 t930
2413 P p930 Number 6702
2414 P p931 Number 6710
2415 O o931 resource_defs p930 p931 p204
2416 P p932 Number 6708
2417 O o932 uid p932 p931
2418 T t932 o932 b695
2419 B b932 t932
2420 T t933 o b932 b4
2421 B b933 t933
2422 T t934 o931 b933
2423 B b934 t934
2424 T t935 o b934 b4
2425 B b935 t935
2426 T t936 o928 b680 b930 b692 b935
2427 B b936 t936
2428 T t937 o927 b936
2429 B b937 t937
2430 P p937 Number 6808
2431 P p938 Number 6982
2432 O o938 location p937 p938
2433 P p939 String id_wf2
2434 O o939 rule p939
2435 T t939 o761 b606 b588
2436 S s939 t688 h
2437 G s939 t939
2438 B b939 s939
2439 T t940 o681 b939
2440 B b940 t940
2441 T t941 o680 b727 b940
2442 B b941 t941
2443 T t942 o680 b686 b941
2444 B b942 t942
2445 P p942 Number 6830
2446 P p943 Number 6837
2447 O o943 resource_defs p942 p943 p204
2448 P p944 Number 6835
2449 O o944 uid p944 p943
2450 T t944 o944 b695
2451 B b944 t944
2452 T t945 o b944 b4
2453 B b945 t945
2454 T t946 o943 b945
2455 B b946 t946
2456 T t947 o b946 b4
2457 B b947 t947
2458 T t948 o939 b680 b942 b692 b947
2459 B b948 t948
2460 T t949 o938 b948
2461 B b949 t949
2462 P p949 Number 6984
2463 P p950 Number 7278
2464 O o950 location p949 p950
2465 P p951 String id_eq1
2466 O o951 rule p951
2467 T t951 o761 b832 b588
2468 S s951 t688 h
2469 G s951 t951
2470 B b951 s951
2471 T t952 o681 b951
2472 B b952 t952
2473 T t953 o598 b582 b606 b832
2474 B b953 t953
2475 T t954 o727 b588 b593 b953 b832
2476 S s954 t688 h
2477 G s954 t954
2478 B b954 s954
2479 T t955 o681 b954
2480 B b955 t955
2481 T t956 o680 b952 b955
2482 B b956 t956
2483 T t957 o680 b727 b956
2484 B b957 t957
2485 T t958 o680 b686 b957
2486 B b958 t958
2487 T t959 o680 b834 b958
2488 B b959 t959
2489 P p959 Number 7006
2490 P p960 Number 7013
2491 O o960 resource_defs p959 p960 p204
2492 P p961 Number 7011
2493 O o961 uid p961 p960
2494 T t961 o961 b695
2495 B b961 t961
2496 T t962 o b961 b4
2497 B b962 t962
2498 T t963 o960 b962
2499 B b963 t963
2500 T t964 o b963 b4
2501 B b964 t964
2502 T t965 o951 b680 b959 b692 b964
2503 B b965 t965
2504 T t966 o950 b965
2505 B b966 t966
2506 P p966 Number 7280
2507 P p967 Number 7457
2508 O o967 location p966 p967
2509 P p968 String inv_wf1
2510 O o968 rule p968
2511 T t968 o611 b582 b741
2512 B b968 t968
2513 T t969 o704 b968
2514 S s969 t688 h
2515 G s969 t969
2516 B b969 s969
2517 T t970 o681 b969
2518 B b970 t970
2519 T t971 o680 b686 b970
2520 B b971 t971
2521 T t972 o680 b743 b971
2522 B b972 t972
2523 P p972 Number 7303
2524 P p973 Number 7310
2525 O o973 resource_defs p972 p973 p204
2526 P p974 Number 7308
2527 O o974 uid p974 p973
2528 T t974 o974 b695
2529 B b974 t974
2530 T t975 o b974 b4
2531 B b975 t975
2532 T t976 o973 b975
2533 B b976 t976
2534 T t977 o b976 b4
2535 B b977 t977
2536 T t978 o968 b680 b972 b692 b977
2537 B b978 t978
2538 T t979 o967 b978
2539 B b979 t979
2540 P p979 Number 7459
2541 P p980 Number 7735
2542 O o980 location p979 p980
2543 P p981 String inv_wf2
2544 O o981 rule p981
2545 T t981 o761 b968 b588
2546 S s981 t688 h
2547 G s981 t981
2548 B b981 s981
2549 T t982 o681 b981
2550 B b982 t982
2551 T t983 o680 b762 b982
2552 B b983 t983
2553 T t984 o680 b727 b983
2554 B b984 t984
2555 T t985 o680 b686 b984
2556 B b985 t985
2557 T t986 o680 b743 b985
2558 B b986 t986
2559 P p986 Number 7482
2560 P p987 Number 7489
2561 O o987 resource_defs p986 p987 p204
2562 P p988 Number 7487
2563 O o988 uid p988 p987
2564 T t988 o988 b695
2565 B b988 t988
2566 T t989 o b988 b4
2567 B b989 t989
2568 T t990 o987 b989
2569 B b990 t990
2570 T t991 o b990 b4
2571 B b991 t991
2572 T t992 o981 b680 b986 b692 b991
2573 B b992 t992
2574 T t993 o980 b992
2575 B b993 t993
2576 P p993 Number 7737
2577 P p994 Number 7946
2578 O o994 location p993 p994
2579 P p995 String inv_equiv_fun1
2580 O o995 rule p995
2581 T t995 o611 b582 b835
2582 B b995 t995 z
2583 T t996 o834 b588 b593 b995
2584 S s996 t688 h
2585 G s996 t996
2586 B b996 s996
2587 T t997 o681 b996
2588 B b997 t997
2589 T t998 o680 b727 b997
2590 B b998 t998
2591 T t999 o680 b686 b998
2592 B b999 t999
2593 P p999 Number 7767
2594 P p1000 Number 7774
2595 O o1000 resource_defs p999 p1000 p204
2596 P p1001 Number 7772
2597 O o1001 uid p1001 p1000
2598 T t1001 o1001 b695
2599 B b1001 t1001
2600 T t1002 o b1001 b4
2601 B b1002 t1002
2602 T t1003 o1000 b1002
2603 B b1003 t1003
2604 T t1004 o b1003 b4
2605 B b1004 t1004
2606 T t1005 o995 b680 b999 b692 b1004
2607 B b1005 t1005
2608 T t1006 o994 b1005
2609 B b1006 t1006
2610 P p1006 Number 7948
2611 P p1007 Number 8130
2612 O o1007 location p1006 p1007
2613 P p1008 String inv_eq_fun1
2614 O o1008 rule p1008
2615 T t1008 o865 b995
2616 S s1008 t688 h
2617 G s1008 t1008
2618 B b1008 s1008
2619 T t1009 o681 b1008
2620 B b1009 t1009
2621 T t1010 o680 b727 b1009
2622 B b1010 t1010
2623 T t1011 o680 b686 b1010
2624 B b1011 t1011
2625 P p1011 Number 7975
2626 P p1012 Number 7982
2627 O o1012 resource_defs p1011 p1012 p204
2628 P p1013 Number 7980
2629 O o1013 uid p1013 p1012
2630 T t1013 o1013 b695
2631 B b1013 t1013
2632 T t1014 o b1013 b4
2633 B b1014 t1014
2634 T t1015 o1012 b1014
2635 B b1015 t1015
2636 T t1016 o b1015 b4
2637 B b1016 t1016
2638 T t1017 o1008 b680 b1011 b692 b1016
2639 B b1017 t1017
2640 T t1018 o1007 b1017
2641 B b1018 t1018
2642 P p1018 Number 8132
2643 P p1019 Number 8440
2644 O o1019 location p1018 p1019
2645 P p1020 String inv_id1
2646 O o1020 rule p1020
2647 T t1020 o598 b582 b968 b741
2648 B b1020 t1020
2649 T t1021 o727 b588 b593 b1020 b606
2650 S s1021 t688 h
2651 G s1021 t1021
2652 B b1021 s1021
2653 T t1022 o681 b1021
2654 B b1022 t1022
2655 T t1023 o680 b762 b1022
2656 B b1023 t1023
2657 T t1024 o680 b727 b1023
2658 B b1024 t1024
2659 T t1025 o680 b686 b1024
2660 B b1025 t1025
2661 T t1026 o680 b743 b1025
2662 B b1026 t1026
2663 P p1026 Number 8155
2664 P p1027 Number 8162
2665 O o1027 resource_defs p1026 p1027 p204
2666 P p1028 Number 8160
2667 O o1028 uid p1028 p1027
2668 T t1028 o1028 b695
2669 B b1028 t1028
2670 T t1029 o b1028 b4
2671 B b1029 t1029
2672 T t1030 o1027 b1029
2673 B b1030 t1030
2674 T t1031 o b1030 b4
2675 B b1031 t1031
2676 T t1032 o1020 b680 b1026 b692 b1031
2677 B b1032 t1032
2678 T t1033 o1019 b1032
2679 B b1033 t1033
2680 P p1033 Number 8459
2681 P p1034 Number 9032
2682 O o1034 location p1033 p1034
2683 P p1035 String id_judge_elim
2684 O o1035 rule p1035
2685 P p1036 String J
2686 O o1036 context_param p1036
2687 T t1036 o1036
2688 B b1036 t1036
2689 T t1037 o b1036 b4
2690 B b1037 t1037
2691 T t1038 o b679 b1037
2692 B b1038 t1038
2693 T t1039 o598 b582 b832 b832
2694 B b1039 t1039
2695 T t1040 o727 b588 b593 b1039 b832
2696 H h1040 x t1040
2697 P p1040 Var x
2698 O o1040 var p1040
2699 T t1041 o1040
2700 C h1041 J t1041
2701 S s1041 t683 h h1040 h1041
2702 G s1041 t833
2703 B b1041 s1041
2704 T t1042 o681 b1041
2705 B b1042 t1042
2706 S s1042 t683 h h1040 h1041
2707 G s1042 t685
2708 B b1043 s1042
2709 T t1043 o681 b1043
2710 B b1044 t1043
2711 S s1044 t688 h h1040 h1041
2712 G s1044 t583
2713 B b1045 s1044
2714 T t1045 o681 b1045
2715 B b1046 t1045
2716 T t1046 o727 b588 b593 b832 b606
2717 H h1046 y t1046
2718 P p1046 Var C
2719 O o1046 var p1046
2720 B b1047 t1041
2721 T t1047 o1046 b1047
2722 S s1047 t688 h h1040 h1041 h1046
2723 G s1047 t1047
2724 B b1048 s1047
2725 T t1048 o681 b1048
2726 B b1049 t1048
2727 S s1049 t688 h h1040 h1041
2728 G s1049 t1047
2729 B b1050 s1049
2730 T t1050 o681 b1050
2731 B b1051 t1050
2732 T t1051 o680 b1049 b1051
2733 B b1052 t1051
2734 T t1052 o680 b1046 b1052
2735 B b1053 t1052
2736 T t1053 o680 b1044 b1053
2737 B b1054 t1053
2738 T t1054 o680 b1042 b1054
2739 B b1055 t1054
2740 NSummary!interactive interactive interactive Summary
2741 O o1055 interactive
2742 NSummary!ext_rule ext_rule ext_rule Summary
2743 P p1055 String "assertT << equiv{car{'g}; eqG{'g}; 's; id{'g}} >> ttca"
2744 O o1056 ext_rule p1055
2745 NSummary!status_incomplete status_incomplete status_incomplete Summary
2746 O o1057 status_incomplete
2747 T t1057 o1057
2748 B b1057 t1057
2749 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2750 O o1058 ext_unjustified
2751 NSummary!tactic_arg tactic_arg tactic_arg Summary
2752 P p1058 String main
2753 O o1059 tactic_arg p1058
2754 NSummary!msequent msequent msequent Summary
2755 O o1060 msequent
2756 T t1060 o b1048 b4
2757 B b1060 t1060
2758 T t1061 o b1045 b1060
2759 B b1061 t1061
2760 T t1062 o b1043 b1061
2761 B b1062 t1062
2762 T t1063 o b1041 b1062
2763 B b1063 t1063
2764 T t1064 o1060 b1050 b1063
2765 B b1064 t1064
2766 NSummary!parent_none parent_none parent_none Summary
2767 O o1064 parent_none
2768 T t1065 o1064
2769 B b1065 t1065
2770 T t1066 o1059 b1064 b4 b1065
2771 B b1066 t1066
2772 P p1066 String assertion
2773 O o1066 tactic_arg p1066
2774 S s1066 t688 h h1040 h1041
2775 G s1066 t1046
2776 B b1067 s1066
2777 T t1067 o1060 b1067 b1063
2778 B b1068 t1067
2779 T t1068 o2 b1066
2780 B b1069 t1068
2781 T t1069 o1066 b1068 b4 b1069
2782 B b1070 t1069
2783 T t1070 o b1070 b4
2784 B b1071 t1070
2785 T t1071 o1058 b1066 b1071
2786 B b1072 t1071
2787 P p1072 String "equivSubstT << equiv{car{'g}; eqG{'g}; 's; op{'g; id{'g}; 's}} >> 0 ttca"
2788 O o1072 ext_rule p1072
2789 T t1072 o727 b588 b593 b832 b953
2790 S s1072 t688 h h1040 h1041
2791 G s1072 t1072
2792 B b1073 s1072
2793 T t1073 o1060 b1073 b1063
2794 B b1074 t1073
2795 T t1074 o2 b1070
2796 B b1075 t1074
2797 T t1075 o1066 b1074 b4 b1075
2798 B b1076 t1075
2799 T t1076 o727 b588 b593 b953 b606
2800 S s1076 t688 h h1040 h1041
2801 G s1076 t1076
2802 B b1077 s1076
2803 T t1077 o1060 b1077 b1063
2804 B b1078 t1077
2805 T t1078 o1066 b1078 b4 b1075
2806 B b1079 t1078
2807 T t1079 o b1079 b4
2808 B b1080 t1079
2809 T t1080 o b1076 b1080
2810 B b1081 t1080
2811 T t1081 o1058 b1070 b1081
2812 B b1082 t1081
2813 P p1082 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 's}; 's} >> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
2814 O o1082 ext_rule p1082
2815 T t1082 o1058 b1076 b4
2816 B b1083 t1082
2817 T t1083 o1082 b1057 b1083 b4 b4
2818 B b1084 t1083
2819 P p1084 String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'g}; op{'g; inv{'g; 's}; 's}} >> 0 ttca"
2820 O o1084 ext_rule p1084
2821 T t1084 o611 b582 b832
2822 B b1085 t1084
2823 T t1085 o598 b582 b1085 b832
2824 B b1086 t1085
2825 T t1086 o727 b588 b593 b606 b1086
2826 S s1086 t688 h h1040 h1041
2827 G s1086 t1086
2828 B b1087 s1086
2829 T t1087 o1060 b1087 b1063
2830 B b1088 t1087
2831 T t1088 o2 b1079
2832 B b1089 t1088
2833 T t1089 o1066 b1088 b4 b1089
2834 B b1090 t1089
2835 T t1090 o598 b582 b1086 b832
2836 B b1091 t1090
2837 T t1091 o727 b588 b593 b1091 b1086
2838 S s1091 t688 h h1040 h1041
2839 G s1091 t1091
2840 B b1092 s1091
2841 T t1092 o1060 b1092 b1063
2842 B b1093 t1092
2843 T t1093 o1066 b1093 b4 b1089
2844 B b1094 t1093
2845 NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
2846 O o1094 equiv_fun_prop
2847 B b1095 t836
2848 T t1095 o727 b588 b593 b1095 b835
2849 B b1096 t1095 z
2850 T t1096 o1094 b588 b593 b1096
2851 S s1096 t688 h h1040 h1041
2852 G s1096 t1096
2853 B b1097 s1096
2854 T t1097 o1060 b1097 b1063
2855 B b1098 t1097
2856 T t1098 o1066 b1098 b4 b1089
2857 B b1099 t1098
2858 T t1099 o b1099 b4
2859 B b1100 t1099
2860 T t1100 o b1094 b1100
2861 B b1101 t1100
2862 T t1101 o b1090 b1101
2863 B b1102 t1101
2864 T t1102 o1058 b1079 b1102
2865 B b1103 t1102
2866 P p1103 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT thenT rwh unfold_equiv 2 ttca"
2867 O o1103 ext_rule p1103
2868 T t1103 o1058 b1090 b4
2869 B b1104 t1103
2870 T t1104 o1103 b1057 b1104 b4 b4
2871 B b1105 t1104
2872 P p1105 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; inv{'g; 's}; 's}; 's}; op{'g; inv{'g; 's}; op{'g; 's; 's}}}>> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
2873 O o1105 ext_rule p1105
2874 T t1105 o1058 b1094 b4
2875 B b1106 t1105
2876 T t1106 o1105 b1057 b1106 b4 b4
2877 B b1107 t1106
2878 P p1107 String "rwh unfold_equiv_fun_prop 0 thenT autoT"
2879 O o1107 ext_rule p1107
2880 NCzf_itt_set!set set set Czf_itt_set
2881 O o1108 set
2882 T t1108 o1108
2883 H h1108 a t1108
2884 H h1109 b t1108
2885 H h1110 x_1 t727
2886 T t1110 o727 b588 b593 b599 b600
2887 H h1111 x_2 t1110
2888 T t1111 o598 b582 b599 b832
2889 B b1111 t1111
2890 T t1112 o727 b588 b593 b1111 b599
2891 H h1112 x_3 t1112
2892 T t1113 o598 b582 b600 b832
2893 B b1113 t1113
2894 T t1114 o727 b588 b593 b1113 b600
2895 S s1114 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
2896 G s1114 t1114
2897 B b1114 s1114
2898 T t1115 o1060 b1114 b1063
2899 B b1115 t1115
2900 NItt_logic Itt_logic Itt_logic NIL
2901 NItt_logic!implies implies implies Itt_logic
2902 O o1115 implies
2903 B b1116 t1112
2904 B b1117 t1114
2905 T t1117 o1115 b1116 b1117
2906 S s1117 t688 h h1040 h1041 h1108 h1109 h1110 h1111
2907 G s1117 t1117
2908 B b1118 s1117
2909 T t1118 o1060 b1118 b1063
2910 B b1119 t1118
2911 NSummary!arg_named arg_named arg_named Summary
2912 P p1119 String d_auto
2913 O o1119 arg_named p1119
2914 NSummary!arg_bool arg_bool arg_bool Summary
2915 P p1120 String true
2916 O o1120 arg_bool p1120
2917 T t1120 o1120
2918 B b1120 t1120
2919 T t1121 o1119 b1120
2920 B b1121 t1121
2921 T t1122 o b1121 b4
2922 B b1122 t1122
2923 B b1123 t1110
2924 B b1124 t1117
2925 T t1124 o1115 b1123 b1124
2926 S s1124 t688 h h1040 h1041 h1108 h1109 h1110
2927 G s1124 t1124
2928 B b1125 s1124
2929 T t1125 o1060 b1125 b1063
2930 B b1126 t1125
2931 B b1127 t727
2932 B b1128 t1124
2933 T t1128 o1115 b1127 b1128
2934 S s1128 t688 h h1040 h1041 h1108 h1109
2935 G s1128 t1128
2936 B b1129 s1128
2937 T t1129 o1060 b1129 b1063
2938 B b1130 t1129
2939 NItt_logic!all all all Itt_logic
2940 O o1130 all
2941 B b1131 t1108
2942 B b1132 t1128 b
2943 T t1132 o1130 b1131 b1132
2944 S s1132 t688 h h1040 h1041 h1108
2945 G s1132 t1132
2946 B b1133 s1132
2947 T t1133 o1060 b1133 b1063
2948 B b1134 t1133
2949 B b1135 t1132 a
2950 T t1135 o1130 b1131 b1135
2951 S s1135 t688 h h1040 h1041
2952 G s1135 t1135
2953 B b1136 s1135
2954 T t1136 o1060 b1136 b1063
2955 B b1137 t1136
2956 T t1137 o2 b1099
2957 B b1138 t1137
2958 T t1138 o1066 b1137 b1122 b1138
2959 B b1139 t1138
2960 T t1139 o2 b1139
2961 B b1140 t1139
2962 T t1140 o1059 b1134 b1122 b1140
2963 B b1141 t1140
2964 T t1141 o2 b1141
2965 B b1142 t1141
2966 T t1142 o1059 b1130 b1122 b1142
2967 B b1143 t1142
2968 T t1143 o2 b1143
2969 B b1144 t1143
2970 T t1144 o1059 b1126 b1122 b1144
2971 B b1145 t1144
2972 T t1145 o2 b1145
2973 B b1146 t1145
2974 T t1146 o1059 b1119 b1122 b1146
2975 B b1147 t1146
2976 T t1147 o2 b1147
2977 B b1148 t1147
2978 T t1148 o1059 b1115 b4 b1148
2979 B b1149 t1148
2980 T t1149 o b1149 b4
2981 B b1150 t1149
2982 T t1150 o1058 b1099 b1150
2983 B b1151 t1150
2984 P p1151 String "equivTransT << op{'g; 'a; 's} >> thenT autoT thenT rwh unfold_equiv 2 thenT rwh unfold_equiv 7 ttca thenT rwh fold_equiv 2 thenT rwh fold_equiv 7"
2985 O o1151 ext_rule p1151
2986 T t1151 o727 b588 b593 b600 b599
2987 S s1151 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
2988 G s1151 t1151
2989 B b1152 s1151
2990 T t1152 o1060 b1152 b1063
2991 B b1153 t1152
2992 NItt_logic!and and and Itt_logic
2993 O o1153 and
2994 B b1154 t704
2995 B b1155 t715
2996 T t1155 o704 b599
2997 B b1156 t1155
2998 T t1156 o704 b600
2999 B b1157 t1156
3000 T t1157 o1153 b1156 b1157
3001 B b1158 t1157
3002 T t1158 o1153 b1155 b1158
3003 B b1159 t1158
3004 T t1159 o1153 b1154 b1159
3005 B b1160 t1159
3006 T t1160 o761 b599 b588
3007 B b1161 t1160
3008 T t1161 o761 b600 b588
3009 B b1162 t1161
3010 T t1162 o1153 b1161 b1162
3011 B b1163 t1162
3012 T t1163 o1153 b1160 b1163
3013 B b1164 t1163
3014 NCzf_itt_pair Czf_itt_pair Czf_itt_pair NIL
3015 NCzf_itt_pair!pair pair pair Czf_itt_pair
3016 O o1164 pair
3017 T t1164 o1164 b599 b600
3018 B b1165 t1164
3019 T t1165 o761 b1165 b593
3020 B b1166 t1165
3021 T t1166 o1153 b1164 b1166
3022 H h1166 x_2 t1166
3023 S s1166 t688 h h1040 h1041 h1108 h1109 h1110 h1166 h1112
3024 G s1166 t1151
3025 B b1167 s1166
3026 T t1167 o1060 b1167 b1063
3027 B b1168 t1167
3028 T t1168 o704 b1039
3029 B b1169 t1168
3030 B b1170 t833
3031 T t1170 o1153 b1169 b1170
3032 B b1171 t1170
3033 T t1171 o1153 b1155 b1171
3034 B b1172 t1171
3035 T t1172 o1153 b1154 b1172
3036 B b1173 t1172
3037 T t1173 o761 b1039 b588
3038 B b1174 t1173
3039 B b1175 t951
3040 T t1175 o1153 b1174 b1175
3041 B b1176 t1175
3042 T t1176 o1153 b1173 b1176
3043 B b1177 t1176
3044 T t1177 o1164 b1039 b832
3045 B b1178 t1177
3046 T t1178 o761 b1178 b593
3047 B b1179 t1178
3048 T t1179 o1153 b1177 b1179
3049 H h1179 x t1179
3050 S s1179 t688 h h1179 h1041 h1108 h1109 h1110 h1166 h1112
3051 G s1179 t1151
3052 B b1180 s1179
3053 T t1180 o1060 b1180 b1063
3054 B b1181 t1180
3055 S s1181 t688 h h1179 h1041 h1108 h1109 h1110 h1111 h1112
3056 G s1181 t1151
3057 B b1182 s1181
3058 T t1182 o1060 b1182 b1063
3059 B b1183 t1182
3060 T t1183 o727 b588 b593 b1113 b1111
3061 S s1183 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
3062 G s1183 t1183
3063 B b1184 s1183
3064 T t1184 o1060 b1184 b1063
3065 B b1185 t1184
3066 T t1185 o2 b1149
3067 B b1186 t1185
3068 T t1186 o1059 b1185 b1122 b1186
3069 B b1187 t1186
3070 T t1187 o2 b1187
3071 B b1188 t1187
3072 T t1188 o1059 b1153 b4 b1188
3073 B b1189 t1188
3074 T t1189 o2 b1189
3075 B b1190 t1189
3076 T t1190 o1059 b1183 b4 b1190
3077 B b1191 t1190
3078 T t1191 o2 b1191
3079 B b1192 t1191
3080 T t1192 o1059 b1181 b4 b1192
3081 B b1193 t1192
3082 T t1193 o2 b1193
3083 B b1194 t1193
3084 T t1194 o1059 b1168 b4 b1194
3085 B b1195 t1194
3086 T t1195 o2 b1195
3087 B b1196 t1195
3088 T t1196 o1059 b1153 b4 b1196
3089 B b1197 t1196
3090 T t1197 o727 b588 b593 b1111 b600
3091 S s1197 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
3092 G s1197 t1197
3093 B b1198 s1197
3094 T t1198 o1060 b1198 b1063
3095 B b1199 t1198
3096 S s1199 t688 h h1040 h1041 h1108 h1109 h1110 h1166 h1112
3097 G s1199 t1197
3098 B b1200 s1199
3099 T t1200 o1060 b1200 b1063
3100 B b1201 t1200
3101 S s1201 t688 h h1179 h1041 h1108 h1109 h1110 h1166 h1112
3102 G s1201 t1197
3103 B b1202 s1201
3104 T t1202 o1060 b1202 b1063
3105 B b1203 t1202
3106 S s1203 t688 h h1179 h1041 h1108 h1109 h1110 h1111 h1112
3107 G s1203 t1197
3108 B b1204 s1203
3109 T t1204 o1060 b1204 b1063
3110 B b1205 t1204
3111 T t1205 o1059 b1199 b4 b1186
3112 B b1206 t1205
3113 T t1206 o2 b1206
3114 B b1207 t1206
3115 T t1207 o1059 b1205 b4 b1207
3116 B b1208 t1207
3117 T t1208 o2 b1208
3118 B b1209 t1208
3119 T t1209 o1059 b1203 b4 b1209
3120 B b1210 t1209
3121 T t1210 o2 b1210
3122 B b1211 t1210
3123 T t1211 o1059 b1201 b4 b1211
3124 B b1212 t1211
3125 T t1212 o2 b1212
3126 B b1213 t1212
3127 T t1213 o1059 b1199 b4 b1213
3128 B b1214 t1213
3129 T t1214 o b1214 b4
3130 B b1215 t1214
3131 T t1215 o b1197 b1215
3132 B b1216 t1215
3133 T t1216 o1058 b1149 b1216
3134 B b1217 t1216
3135 P p1217 String "equivSymT ttca thenT rwh unfold_equiv 7 ttca"
3136 O o1217 ext_rule p1217
3137 T t1217 o1058 b1197 b4
3138 B b1218 t1217
3139 T t1218 o1217 b1057 b1218 b4 b4
3140 B b1219 t1218
3141 P p1219 String "equivTransT << 'a >> ttca thenT rwh unfold_equiv 7 thenT rwh unfold_equiv 8 ttca"
3142 O o1219 ext_rule p1219
3143 T t1219 o1058 b1214 b4
3144 B b1220 t1219
3145 T t1220 o1219 b1057 b1220 b4 b4
3146 B b1221 t1220
3147 T t1221 o b1221 b4
3148 B b1222 t1221
3149 T t1222 o b1219 b1222
3150 B b1223 t1222
3151 T t1223 o1151 b1057 b1217 b1223 b4
3152 B b1224 t1223
3153 T t1224 o b1224 b4
3154 B b1225 t1224
3155 T t1225 o1107 b1057 b1151 b1225 b4
3156 B b1226 t1225
3157 T t1226 o b1226 b4
3158 B b1227 t1226
3159 T t1227 o b1107 b1227
3160 B b1228 t1227
3161 T t1228 o b1105 b1228
3162 B b1229 t1228
3163 T t1229 o1084 b1057 b1103 b1229 b4
3164 B b1230 t1229
3165 T t1230 o b1230 b4
3166 B b1231 t1230
3167 T t1231 o b1084 b1231
3168 B b1232 t1231
3169 T t1232 o1072 b1057 b1082 b1232 b4
3170 B b1233 t1232
3171 T t1233 o b1233 b4
3172 B b1234 t1233
3173 T t1234 o1056 b1057 b1072 b1234 b4
3174 B b1235 t1234
3175 T t1235 o1055 b1235
3176 B b1236 t1235
3177 P p1236 Number 8488
3178 P p1237 Number 8495
3179 O o1237 resource_defs p1236 p1237 p176
3180 P p1238 Number 8493
3181 O o1238 uid p1238 p1237
3182 T t1238 o1238 b695
3183 B b1238 t1238
3184 T t1239 o b1238 b4
3185 B b1239 t1239
3186 T t1240 o1237 b1239
3187 B b1240 t1240
3188 T t1241 o b1240 b4
3189 B b1241 t1241
3190 T t1242 o1035 b1038 b1055 b1236 b1241
3191 B b1242 t1242
3192 T t1243 o1034 b1242
3193 B b1243 t1243
3194 P p1243 Number 9034
3195 P p1244 Number 9338
3196 O o1244 location p1243 p1244
3197 P p1245 String inv_id2
3198 O o1245 rule p1245
3199 T t1245 o598 b582 b832 b1085
3200 B b1245 t1245
3201 T t1246 o727 b588 b593 b1245 b606
3202 S s1246 t688 h
3203 G s1246 t1246
3204 B b1246 s1246
3205 T t1247 o681 b1246
3206 B b1247 t1247
3207 T t1248 o680 b952 b1247
3208 B b1248 t1248
3209 T t1249 o680 b727 b1248
3210 B b1249 t1249
3211 T t1250 o680 b686 b1249
3212 B b1250 t1250
3213 T t1251 o680 b834 b1250
3214 B b1251 t1251
3215 P p1251 String "assertT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's; inv{'g; 's}}; op{'g; 's; inv{'g; 's}}}; op{'g; 's; inv{'g; 's}}} >> ttca"
3216 O o1251 ext_rule p1251
3217 T t1252 o b951 b4
3218 B b1252 t1252
3219 T t1253 o b726 b1252
3220 B b1253 t1253
3221 T t1254 o b685 b1253
3222 B b1254 t1254
3223 T t1255 o b833 b1254
3224 B b1255 t1255
3225 T t1256 o1060 b1246 b1255
3226 B b1256 t1256
3227 T t1257 o1059 b1256 b4 b1065
3228 B b1257 t1257
3229 T t1258 o598 b582 b1245 b1245
3230 B b1258 t1258
3231 T t1259 o727 b588 b593 b1258 b1245
3232 S s1259 t688 h
3233 G s1259 t1259
3234 B b1259 s1259
3235 T t1260 o1060 b1259 b1255
3236 B b1260 t1260
3237 T t1261 o2 b1257
3238 B b1261 t1261
3239 T t1262 o1066 b1260 b4 b1261
3240 B b1262 t1262
3241 H h1262 v t1259
3242 S s1262 t688 h h1262
3243 G s1262 t1246
3244 B b1263 s1262
3245 T t1263 o1060 b1263 b1255
3246 B b1264 t1263
3247 T t1264 o1059 b1264 b4 b1261
3248 B b1265 t1264
3249 T t1265 o b1265 b4
3250 B b1266 t1265
3251 T t1266 o b1262 b1266
3252 B b1267 t1266
3253 T t1267 o1058 b1257 b1267
3254 B b1268 t1267
3255 P p1268 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's; inv{'g; 's}}; op{'g; 's; inv{'g; 's}}}; op{'g; 's; op{'g; inv{'g; 's}; op{'g; 's; inv{'g; 's}}}}} >> 0 ttca"
3256 O o1268 ext_rule p1268
3257 T t1268 o598 b582 b1085 b1245
3258 B b1269 t1268
3259 T t1269 o598 b582 b832 b1269
3260 B b1270 t1269
3261 T t1270 o727 b588 b593 b1270 b1245
3262 S s1270 t688 h
3263 G s1270 t1270
3264 B b1271 s1270
3265 T t1271 o1060 b1271 b1255
3266 B b1272 t1271
3267 T t1272 o2 b1262
3268 B b1273 t1272
3269 T t1273 o1066 b1272 b4 b1273
3270 B b1274 t1273
3271 T t1274 o b1274 b4
3272 B b1275 t1274
3273 T t1275 o1058 b1262 b1275
3274 B b1276 t1275
3275 P p1276 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; op{'g; inv{'g; 's}; op{'g; 's; inv{'g; 's}}}}; op{'g; 's; op{'g; op{'g; inv{'g; 's}; 's}; inv{'g; 's}}}} >> 0 ttca"
3276 O o1276 ext_rule p1276
3277 T t1276 o598 b582 b1086 b1085
3278 B b1277 t1276
3279 T t1277 o598 b582 b832 b1277
3280 B b1278 t1277
3281 T t1278 o727 b588 b593 b1278 b1245
3282 S s1278 t688 h
3283 G s1278 t1278
3284 B b1279 s1278
3285 T t1279 o1060 b1279 b1255
3286 B b1280 t1279
3287 T t1280 o2 b1274
3288 B b1281 t1280
3289 T t1281 o1066 b1280 b4 b1281
3290 B b1282 t1281
3291 T t1282 o b1282 b4
3292 B b1283 t1282
3293 T t1283 o1058 b1274 b1283
3294 B b1284 t1283
3295 P p1284 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT"
3296 O o1284 ext_rule p1284
3297 T t1284 o598 b582 b835 b1085
3298 B b1285 t1284
3299 T t1285 o598 b582 b832 b1285
3300 B b1286 t1285 z
3301 T t1286 o834 b588 b593 b1286
3302 S s1286 t688 h
3303 G s1286 t1286
3304 B b1287 s1286
3305 T t1287 o1060 b1287 b1255
3306 B b1288 t1287
3307 B b1289 t1285
3308 T t1289 o727 b588 b593 b1289 b1245
3309 B b1290 t1289 z
3310 T t1290 o1094 b588 b593 b1290
3311 S s1290 t688 h
3312 G s1290 t1290
3313 B b1291 s1290
3314 T t1291 o1060 b1291 b1255
3315 B b1292 t1291
3316 T t1292 o2 b1282
3317 B b1293 t1292
3318 T t1293 o1066 b1292 b1122 b1293
3319 B b1294 t1293
3320 T t1294 o2 b1294
3321 B b1295 t1294
3322 T t1295 o1066 b1288 b4 b1295
3323 B b1296 t1295
3324 T t1296 o b1296 b4
3325 B b1297 t1296
3326 T t1297 o1058 b1282 b1297
3327 B b1298 t1297
3328 P p1298 String "rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 5 ttca"
3329 O o1298 ext_rule p1298
3330 T t1298 o1058 b1296 b4
3331 B b1299 t1298
3332 T t1299 o1298 b1057 b1299 b4 b4
3333 B b1300 t1299
3334 T t1300 o b1300 b4
3335 B b1301 t1300
3336 T t1301 o1284 b1057 b1298 b1301 b4
3337 B b1302 t1301
3338 T t1302 o b1302 b4
3339 B b1303 t1302
3340 T t1303 o1276 b1057 b1284 b1303 b4
3341 B b1304 t1303
3342 T t1304 o b1304 b4
3343 B b1305 t1304
3344 T t1305 o1268 b1057 b1276 b1305 b4
3345 B b1306 t1305
3346 P p1306 String "dT 2 ttca"
3347 O o1306 ext_rule p1306
3348 T t1306 o1058 b1265 b4
3349 B b1307 t1306
3350 T t1307 o1306 b1057 b1307 b4 b4
3351 B b1308 t1307
3352 T t1308 o b1308 b4
3353 B b1309 t1308
3354 T t1309 o b1306 b1309
3355 B b1310 t1309
3356 T t1310 o1251 b1057 b1268 b1310 b4
3357 B b1311 t1310
3358 T t1311 o1055 b1311
3359 B b1312 t1311
3360 P p1312 Number 9057
3361 P p1313 Number 9064
3362 O o1313 resource_defs p1312 p1313 p204
3363 P p1314 Number 9062
3364 O o1314 uid p1314 p1313
3365 T t1314 o1314 b695
3366 B b1314 t1314
3367 T t1315 o b1314 b4
3368 B b1315 t1315
3369 T t1316 o1313 b1315
3370 B b1316 t1316
3371 T t1317 o b1316 b4
3372 B b1317 t1317
3373 T t1318 o1245 b680 b1251 b1312 b1317
3374 B b1318 t1318
3375 T t1319 o1244 b1318
3376 B b1319 t1319
3377 P p1319 Number 9340
3378 P p1320 Number 9634
3379 O o1320 location p1319 p1320
3380 P p1321 String id_eq2
3381 O o1321 rule p1321
3382 T t1321 o598 b582 b832 b606
3383 B b1321 t1321
3384 T t1322 o727 b588 b593 b1321 b832
3385 S s1322 t688 h
3386 G s1322 t1322
3387 B b1322 s1322
3388 T t1323 o681 b1322
3389 B b1323 t1323
3390 T t1324 o680 b952 b1323
3391 B b1324 t1324
3392 T t1325 o680 b727 b1324
3393 B b1325 t1325
3394 T t1326 o680 b686 b1325
3395 B b1326 t1326
3396 T t1327 o680 b834 b1326
3397 B b1327 t1327
3398 T t1328 o1060 b1322 b1255
3399 B b1328 t1328
3400 T t1329 o1059 b1328 b4 b1065
3401 B b1329 t1329
3402 S s1329 t688 h
3403 G s1329 t1086
3404 B b1330 s1329
3405 T t1330 o1060 b1330 b1255
3406 B b1331 t1330
3407 T t1331 o2 b1329
3408 B b1332 t1331
3409 T t1332 o1059 b1331 b4 b1332
3410 B b1333 t1332
3411 T t1333 o598 b582 b832 b1086
3412 B b1334 t1333
3413 T t1334 o727 b588 b593 b1334 b832
3414 S s1334 t688 h
3415 G s1334 t1334
3416 B b1335 s1334
3417 T t1335 o1060 b1335 b1255
3418 B b1336 t1335
3419 T t1336 o1059 b1336 b4 b1332
3420 B b1337 t1336
3421 T t1337 o b1337 b4
3422 B b1338 t1337
3423 T t1338 o b1333 b1338
3424 B b1339 t1338
3425 T t1339 o1058 b1329 b1339
3426 B b1340 t1339
3427 T t1340 o1058 b1333 b4
3428 B b1341 t1340
3429 T t1341 o1103 b1057 b1341 b4 b4
3430 B b1342 t1341
3431 P p1342 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; op{'g; inv{'g; 's}; 's}}; op{'g; op{'g; 's; inv{'g; 's}}; 's}}>> 0 ttca"
3432 O o1342 ext_rule p1342
3433 T t1342 o598 b582 b1245 b832
3434 B b1343 t1342
3435 T t1343 o727 b588 b593 b1343 b832
3436 S s1343 t688 h
3437 G s1343 t1343
3438 B b1344 s1343
3439 T t1344 o1060 b1344 b1255
3440 B b1345 t1344
3441 T t1345 o2 b1337
3442 B b1346 t1345
3443 T t1346 o1059 b1345 b4 b1346
3444 B b1347 t1346
3445 T t1347 o b1347 b4
3446 B b1348 t1347
3447 T t1348 o1058 b1337 b1348
3448 B b1349 t1348
3449 P p1349 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; inv{'g; 's}}; id{'g}} >> 0 thenT autoT"
3450 O o1349 ext_rule p1349
3451 T t1349 o1058 b1347 b4
3452 B b1350 t1349
3453 T t1350 o1349 b1057 b1350 b4 b4
3454 B b1351 t1350
3455 T t1351 o b1351 b4
3456 B b1352 t1351
3457 T t1352 o1342 b1057 b1349 b1352 b4
3458 B b1353 t1352
3459 T t1353 o b1353 b4
3460 B b1354 t1353
3461 T t1354 o b1342 b1354
3462 B b1355 t1354
3463 T t1355 o1084 b1057 b1340 b1355 b4
3464 B b1356 t1355
3465 T t1356 o1055 b1356
3466 B b1357 t1356
3467 P p1357 Number 9362
3468 P p1358 Number 9369
3469 O o1358 resource_defs p1357 p1358 p204
3470 P p1359 Number 9367
3471 O o1359 uid p1359 p1358
3472 T t1359 o1359 b695
3473 B b1359 t1359
3474 T t1360 o b1359 b4
3475 B b1360 t1360
3476 T t1361 o1358 b1360
3477 B b1361 t1361
3478 T t1362 o b1361 b4
3479 B b1362 t1362
3480 T t1363 o1321 b680 b1327 b1357 b1362
3481 B b1363 t1363
3482 T t1364 o1320 b1363
3483 B b1364 t1364
3484 P p1364 Number 9655
3485 P p1365 Number 10094
3486 O o1365 location p1364 p1365
3487 P p1366 String equiv_op_fun1
3488 O o1366 rule p1366
3489 S s1366 t683 h
3490 G s1366 t1155
3491 B b1366 s1366
3492 T t1366 o681 b1366
3493 B b1367 t1366
3494 S s1367 t683 h
3495 G s1367 t1156
3496 B b1368 s1367
3497 T t1368 o681 b1368
3498 B b1369 t1368
3499 S s1369 t688 h
3500 G s1369 t1160
3501 B b1370 s1369
3502 T t1370 o681 b1370
3503 B b1371 t1370
3504 S s1371 t688 h
3505 G s1371 t1161
3506 B b1372 s1371
3507 T t1372 o681 b1372
3508 B b1373 t1372
3509 T t1373 o598 b582 b835 b599
3510 B b1374 t1373
3511 T t1374 o598 b582 b835 b600
3512 B b1375 t1374
3513 T t1375 o727 b588 b593 b1374 b1375
3514 B b1376 t1375 z
3515 T t1376 o1094 b588 b593 b1376
3516 S s1376 t688 h
3517 G s1376 t1376
3518 B b1377 s1376
3519 T t1377 o681 b1377
3520 B b1378 t1377
3521 T t1378 o680 b1373 b1378
3522 B b1379 t1378
3523 T t1379 o680 b1371 b1379
3524 B b1380 t1379
3525 T t1380 o680 b727 b1380
3526 B b1381 t1380
3527 T t1381 o680 b686 b1381
3528 B b1382 t1381
3529 T t1382 o680 b1369 b1382
3530 B b1383 t1382
3531 T t1383 o680 b1367 b1383
3532 B b1384 t1383
3533 P p1384 String "rwh unfold_equiv_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
3534 O o1384 ext_rule p1384
3535 T t1384 o b1372 b4
3536 B b1385 t1384
3537 T t1385 o b1370 b1385
3538 B b1386 t1385
3539 T t1386 o b726 b1386
3540 B b1387 t1386
3541 T t1387 o b685 b1387
3542 B b1388 t1387
3543 T t1388 o b1368 b1388
3544 B b1389 t1388
3545 T t1389 o b1366 b1389
3546 B b1390 t1389
3547 T t1390 o1060 b1377 b1390
3548 B b1391 t1390
3549 T t1391 o1059 b1391 b4 b1065
3550 B b1392 t1391
3551 H h1392 a_1 t1108
3552 H h1393 b_1 t1108
3553 H h1394 x t727
3554 P p1394 Var a_1
3555 O o1394 var p1394
3556 T t1394 o1394
3557 B b1394 t1394
3558 P p1395 Var b_1
3559 O o1395 var p1395
3560 T t1395 o1395
3561 B b1395 t1395
3562 T t1396 o727 b588 b593 b1394 b1395
3563 H h1396 x_1 t1396
3564 T t1397 o598 b582 b1394 b599
3565 B b1397 t1397
3566 T t1398 o598 b582 b1394 b600
3567 B b1398 t1398
3568 T t1399 o727 b588 b593 b1397 b1398
3569 H h1399 x_2 t1399
3570 T t1400 o598 b582 b1395 b599
3571 B b1400 t1400
3572 T t1401 o598 b582 b1395 b600
3573 B b1401 t1401
3574 T t1402 o727 b588 b593 b1400 b1401
3575 S s1402 t688 h h1392 h1393 h1394 h1396 h1399
3576 G s1402 t1402
3577 B b1402 s1402
3578 T t1403 o1060 b1402 b1390
3579 B b1403 t1403
3580 B b1404 t1399
3581 B b1405 t1402
3582 T t1405 o1115 b1404 b1405
3583 S s1405 t688 h h1392 h1393 h1394 h1396
3584 G s1405 t1405
3585 B b1406 s1405
3586 T t1406 o1060 b1406 b1390
3587 B b1407 t1406
3588 B b1408 t1396
3589 B b1409 t1405
3590 T t1409 o1115 b1408 b1409
3591 S s1409 t688 h h1392 h1393 h1394
3592 G s1409 t1409
3593 B b1410 s1409
3594 T t1410 o1060 b1410 b1390
3595 B b1411 t1410
3596 B b1412 t1409
3597 T t1412 o1115 b1127 b1412
3598 S s1412 t688 h h1392 h1393
3599 G s1412 t1412
3600 B b1413 s1412
3601 T t1413 o1060 b1413 b1390
3602 B b1414 t1413
3603 B b1415 t1412 b_1
3604 T t1415 o1130 b1131 b1415
3605 S s1415 t688 h h1392
3606 G s1415 t1415
3607 B b1416 s1415
3608 T t1416 o1060 b1416 b1390
3609 B b1417 t1416
3610 B b1418 t1415 a_1
3611 T t1418 o1130 b1131 b1418
3612 S s1418 t688 h
3613 G s1418 t1418
3614 B b1419 s1418
3615 T t1419 o1060 b1419 b1390
3616 B b1420 t1419
3617 T t1420 o2 b1392
3618 B b1421 t1420
3619 T t1421 o1059 b1420 b4 b1421
3620 B b1422 t1421
3621 T t1422 o2 b1422
3622 B b1423 t1422
3623 T t1423 o1059 b1417 b4 b1423
3624 B b1424 t1423
3625 T t1424 o2 b1424
3626 B b1425 t1424
3627 T t1425 o1059 b1414 b4 b1425
3628 B b1426 t1425
3629 T t1426 o2 b1426
3630 B b1427 t1426
3631 T t1427 o1059 b1411 b4 b1427
3632 B b1428 t1427
3633 T t1428 o2 b1428
3634 B b1429 t1428
3635 T t1429 o1059 b1407 b4 b1429
3636 B b1430 t1429
3637 T t1430 o2 b1430
3638 B b1431 t1430
3639 T t1431 o1059 b1403 b4 b1431
3640 B b1432 t1431
3641 T t1432 o b1432 b4
3642 B b1433 t1432
3643 T t1433 o1058 b1392 b1433
3644 B b1434 t1433
3645 P p1434 String "equivTransT << op{'g; 'a_1; 'b} >> ttca thenT rwh unfold_equiv 5 thenT rwh unfold_equiv 6 ttca thenT rwh fold_equiv 5 thenT rwh fold_equiv 6"
3646 O o1434 ext_rule p1434
3647 T t1434 o727 b588 b593 b1400 b1398
3648 S s1434 t688 h h1392 h1393 h1394 h1396 h1399
3649 G s1434 t1434
3650 B b1435 s1434
3651 T t1435 o1060 b1435 b1390
3652 B b1436 t1435
3653 T t1436 o704 b1397
3654 B b1437 t1436
3655 T t1437 o704 b1398
3656 B b1438 t1437
3657 T t1438 o1153 b1437 b1438
3658 B b1439 t1438
3659 T t1439 o1153 b1155 b1439
3660 B b1440 t1439
3661 T t1440 o1153 b1154 b1440
3662 B b1441 t1440
3663 T t1441 o761 b1397 b588
3664 B b1442 t1441
3665 T t1442 o761 b1398 b588
3666 B b1443 t1442
3667 T t1443 o1153 b1442 b1443
3668 B b1444 t1443
3669 T t1444 o1153 b1441 b1444
3670 B b1445 t1444
3671 T t1445 o1164 b1397 b1398
3672 B b1446 t1445
3673 T t1446 o761 b1446 b593
3674 B b1447 t1446
3675 T t1447 o1153 b1445 b1447
3676 H h1447 x_2 t1447
3677 S s1447 t688 h h1392 h1393 h1394 h1396 h1447
3678 G s1447 t1434
3679 B b1448 s1447
3680 T t1448 o1060 b1448 b1390
3681 B b1449 t1448
3682 T t1449 o704 b1394
3683 B b1450 t1449
3684 T t1450 o704 b1395
3685 B b1451 t1450
3686 T t1451 o1153 b1450 b1451
3687 B b1452 t1451
3688 T t1452 o1153 b1155 b1452
3689 B b1453 t1452
3690 T t1453 o1153 b1154 b1453
3691 B b1454 t1453
3692 T t1454 o761 b1394 b588
3693 B b1455 t1454
3694 T t1455 o761 b1395 b588
3695 B b1456 t1455
3696 T t1456 o1153 b1455 b1456
3697 B b1457 t1456
3698 T t1457 o1153 b1454 b1457
3699 B b1458 t1457
3700 T t1458 o1164 b1394 b1395
3701 B b1459 t1458
3702 T t1459 o761 b1459 b593
3703 B b1460 t1459
3704 T t1460 o1153 b1458 b1460
3705 H h1460 x_1 t1460
3706 S s1460 t688 h h1392 h1393 h1394 h1460 h1447
3707 G s1460 t1434
3708 B b1461 s1460
3709 T t1461 o1060 b1461 b1390
3710 B b1462 t1461
3711 S s1462 t688 h h1392 h1393 h1394 h1460 h1399
3712 G s1462 t1434
3713 B b1463 s1462
3714 T t1463 o1060 b1463 b1390
3715 B b1464 t1463
3716 T t1464 o2 b1432
3717 B b1465 t1464
3718 T t1465 o1059 b1436 b4 b1465
3719 B b1466 t1465
3720 T t1466 o2 b1466
3721 B b1467 t1466
3722 T t1467 o1059 b1464 b4 b1467
3723 B b1468 t1467
3724 T t1468 o2 b1468
3725 B b1469 t1468
3726 T t1469 o1059 b1462 b4 b1469
3727 B b1470 t1469
3728 T t1470 o2 b1470
3729 B b1471 t1470
3730 T t1471 o1059 b1449 b4 b1471
3731 B b1472 t1471
3732 T t1472 o2 b1472
3733 B b1473 t1472
3734 T t1473 o1059 b1436 b4 b1473
3735 B b1474 t1473
3736 T t1474 o727 b588 b593 b1398 b1401
3737 S s1474 t688 h h1392 h1393 h1394 h1396 h1399
3738 G s1474 t1474
3739 B b1475 s1474
3740 T t1475 o1060 b1475 b1390
3741 B b1476 t1475
3742 S s1476 t688 h h1392 h1393 h1394 h1396 h1447
3743 G s1476 t1474
3744 B b1477 s1476
3745 T t1477 o1060 b1477 b1390
3746 B b1478 t1477
3747 S s1478 t688 h h1392 h1393 h1394 h1460 h1447
3748 G s1478 t1474
3749 B b1479 s1478
3750 T t1479 o1060 b1479 b1390
3751 B b1480 t1479
3752 S s1480 t688 h h1392 h1393 h1394 h1460 h1399
3753 G s1480 t1474
3754 B b1481 s1480
3755 T t1481 o1060 b1481 b1390
3756 B b1482 t1481
3757 T t1482 o1059 b1476 b4 b1465
3758 B b1483 t1482
3759 T t1483 o2 b1483
3760 B b1484 t1483
3761 T t1484 o1059 b1482 b4 b1484
3762 B b1485 t1484
3763 T t1485 o2 b1485
3764 B b1486 t1485
3765 T t1486 o1059 b1480 b4 b1486
3766 B b1487 t1486
3767 T t1487 o2 b1487
3768 B b1488 t1487
3769 T t1488 o1059 b1478 b4 b1488
3770 B b1489 t1488
3771 T t1489 o2 b1489
3772 B b1490 t1489
3773 T t1490 o1059 b1476 b4 b1490
3774 B b1491 t1490
3775 T t1491 o b1491 b4
3776 B b1492 t1491
3777 T t1492 o b1474 b1492
3778 B b1493 t1492
3779 T t1493 o1058 b1432 b1493
3780 B b1494 t1493
3781 P p1494 String "equivTransT << op{'g; 'a_1; 'a} >> thenT autoT thenT rwh unfold_equiv 5 thenT rwh unfold_equiv 6 ttca thenT rwh fold_equiv 5 thenT rwh fold_equiv 6"
3782 O o1494 ext_rule p1494
3783 T t1494 o727 b588 b593 b1395 b1394
3784 S s1494 t688 h h1392 h1393 h1394 h1396 h1399
3785 G s1494 t1494
3786 B b1495 s1494
3787 T t1495 o1060 b1495 b1390
3788 B b1496 t1495
3789 S s1496 t688 h h1392 h1393 h1394 h1396 h1447
3790 G s1496 t1494
3791 B b1497 s1496
3792 T t1497 o1060 b1497 b1390
3793 B b1498 t1497
3794 S s1498 t688 h h1392 h1393 h1394 h1460 h1447
3795 G s1498 t1494
3796 B b1499 s1498
3797 T t1499 o1060 b1499 b1390
3798 B b1500 t1499
3799 S s1500 t688 h h1392 h1393 h1394 h1460 h1399
3800 G s1500 t1494
3801 B b1501 s1500
3802 T t1501 o1060 b1501 b1390
3803 B b1502 t1501
3804 T t1502 o727 b588 b593 b1400 b1397
3805 S s1502 t688 h h1392 h1393 h1394 h1396 h1399
3806 G s1502 t1502
3807 B b1503 s1502
3808 T t1503 o1060 b1503 b1390
3809 B b1504 t1503
3810 T t1504 o2 b1474
3811 B b1505 t1504
3812 T t1505 o1059 b1504 b1122 b1505
3813 B b1506 t1505
3814 T t1506 o2 b1506
3815 B b1507 t1506
3816 T t1507 o1059 b1496 b4 b1507
3817 B b1508 t1507
3818 T t1508 o2 b1508
3819 B b1509 t1508
3820 T t1509 o1059 b1502 b4 b1509
3821 B b1510 t1509
3822 T t1510 o2 b1510
3823 B b1511 t1510
3824 T t1511 o1059 b1500 b4 b1511
3825 B b1512 t1511
3826 T t1512 o2 b1512
3827 B b1513 t1512
3828 T t1513 o1059 b1498 b4 b1513
3829 B b1514 t1513
3830 T t1514 o2 b1514
3831 B b1515 t1514
3832 T t1515 o1059 b1496 b4 b1515
3833 B b1516 t1515
3834 T t1516 o b1516 b4
3835 B b1517 t1516
3836 T t1517 o1058 b1474 b1517
3837 B b1518 t1517
3838 P p1518 String "equivSymT ttca thenT rwh unfold_equiv 5 ttca"
3839 O o1518 ext_rule p1518
3840 T t1518 o1058 b1516 b4
3841 B b1519 t1518
3842 T t1519 o1518 b1057 b1519 b4 b4
3843 B b1520 t1519
3844 T t1520 o b1520 b4
3845 B b1521 t1520
3846 T t1521 o1494 b1057 b1518 b1521 b4
3847 B b1522 t1521
3848 P p1522 String "autoT thenT rwh unfold_equiv 5 ttca"
3849 O o1522 ext_rule p1522
3850 T t1522 o1058 b1491 b4
3851 B b1523 t1522
3852 T t1523 o1522 b1057 b1523 b4 b4
3853 B b1524 t1523
3854 T t1524 o b1524 b4
3855 B b1525 t1524
3856 T t1525 o b1522 b1525
3857 B b1526 t1525
3858 T t1526 o1434 b1057 b1494 b1526 b4
3859 B b1527 t1526
3860 T t1527 o b1527 b4
3861 B b1528 t1527
3862 T t1528 o1384 b1057 b1434 b1528 b4
3863 B b1529 t1528
3864 T t1529 o1055 b1529
3865 B b1530 t1529
3866 P p1530 Number 9684
3867 P p1531 Number 9691
3868 O o1531 resource_defs p1530 p1531 p204
3869 P p1532 Number 9689
3870 O o1532 uid p1532 p1531
3871 T t1532 o1532 b695
3872 B b1532 t1532
3873 T t1533 o b1532 b4
3874 B b1533 t1533
3875 T t1534 o1531 b1533
3876 B b1534 t1534
3877 T t1535 o b1534 b4
3878 B b1535 t1535
3879 T t1536 o1366 b680 b1384 b1530 b1535
3880 B b1536 t1536
3881 T t1537 o1365 b1536
3882 B b1537 t1537
3883 P p1537 Number 10096
3884 P p1538 Number 10535
3885 O o1538 location p1537 p1538
3886 P p1539 String equiv_op_fun2
3887 O o1539 rule p1539
3888 T t1539 o598 b582 b599 b835
3889 B b1539 t1539
3890 T t1540 o598 b582 b600 b835
3891 B b1540 t1540
3892 T t1541 o727 b588 b593 b1539 b1540
3893 B b1541 t1541 z
3894 T t1542 o1094 b588 b593 b1541
3895 S s1542 t688 h
3896 G s1542 t1542
3897 B b1542 s1542
3898 T t1543 o681 b1542
3899 B b1543 t1543
3900 T t1544 o680 b1373 b1543
3901 B b1544 t1544
3902 T t1545 o680 b1371 b1544
3903 B b1545 t1545
3904 T t1546 o680 b727 b1545
3905 B b1546 t1546
3906 T t1547 o680 b686 b1546
3907 B b1547 t1547
3908 T t1548 o680 b1369 b1547
3909 B b1548 t1548
3910 T t1549 o680 b1367 b1548
3911 B b1549 t1549
3912 T t1550 o1060 b1542 b1390
3913 B b1550 t1550
3914 T t1551 o1059 b1550 b4 b1065
3915 B b1551 t1551
3916 T t1552 o598 b582 b599 b1394
3917 B b1552 t1552
3918 T t1553 o598 b582 b600 b1394
3919 B b1553 t1553
3920 T t1554 o727 b588 b593 b1552 b1553
3921 H h1554 x_2 t1554
3922 T t1555 o598 b582 b599 b1395
3923 B b1555 t1555
3924 T t1556 o598 b582 b600 b1395
3925 B b1556 t1556
3926 T t1557 o727 b588 b593 b1555 b1556
3927 S s1557 t688 h h1392 h1393 h1394 h1396 h1554
3928 G s1557 t1557
3929 B b1557 s1557
3930 T t1558 o1060 b1557 b1390
3931 B b1558 t1558
3932 B b1559 t1554
3933 B b1560 t1557
3934 T t1560 o1115 b1559 b1560
3935 S s1560 t688 h h1392 h1393 h1394 h1396
3936 G s1560 t1560
3937 B b1561 s1560
3938 T t1561 o1060 b1561 b1390
3939 B b1562 t1561
3940 B b1563 t1560
3941 T t1563 o1115 b1408 b1563
3942 S s1563 t688 h h1392 h1393 h1394
3943 G s1563 t1563
3944 B b1564 s1563
3945 T t1564 o1060 b1564 b1390
3946 B b1565 t1564
3947 B b1566 t1563
3948 T t1566 o1115 b1127 b1566
3949 S s1566 t688 h h1392 h1393
3950 G s1566 t1566
3951 B b1567 s1566
3952 T t1567 o1060 b1567 b1390
3953 B b1568 t1567
3954 B b1569 t1566 b_1
3955 T t1569 o1130 b1131 b1569
3956 S s1569 t688 h h1392
3957 G s1569 t1569
3958 B b1570 s1569
3959 T t1570 o1060 b1570 b1390
3960 B b1571 t1570
3961 B b1572 t1569 a_1
3962 T t1572 o1130 b1131 b1572
3963 S s1572 t688 h
3964 G s1572 t1572
3965 B b1573 s1572
3966 T t1573 o1060 b1573 b1390
3967 B b1574 t1573
3968 T t1574 o2 b1551
3969 B b1575 t1574
3970 T t1575 o1059 b1574 b4 b1575
3971 B b1576 t1575
3972 T t1576 o2 b1576
3973 B b1577 t1576
3974 T t1577 o1059 b1571 b4 b1577
3975 B b1578 t1577
3976 T t1578 o2 b1578
3977 B b1579 t1578
3978 T t1579 o1059 b1568 b4 b1579
3979 B b1580 t1579
3980 T t1580 o2 b1580
3981 B b1581 t1580
3982 T t1581 o1059 b1565 b4 b1581
3983 B b1582 t1581
3984 T t1582 o2 b1582
3985 B b1583 t1582
3986 T t1583 o1059 b1562 b4 b1583
3987 B b1584 t1583
3988 T t1584 o2 b1584
3989 B b1585 t1584
3990 T t1585 o1059 b1558 b4 b1585
3991 B b1586 t1585
3992 T t1586 o b1586 b4
3993 B b1587 t1586
3994 T t1587 o1058 b1551 b1587
3995 B b1588 t1587
3996 P p1588 String "equivTransT << op{'g; 'b; 'a_1} >> thenT autoT thenT rwh unfold_equiv 5 ttca"
3997 O o1588 ext_rule p1588
3998 T t1588 o727 b588 b593 b1555 b1553
3999 S s1588 t688 h h1392 h1393 h1394 h1460 h1554
4000 G s1588 t1588
4001 B b1589 s1588
4002 T t1589 o1060 b1589 b1390
4003 B b1590 t1589
4004 S s1590 t688 h h1392 h1393 h1394 h1396 h1554
4005 G s1590 t1588
4006 B b1591 s1590
4007 T t1591 o1060 b1591 b1390
4008 B b1592 t1591
4009 T t1592 o2 b1586
4010 B b1593 t1592
4011 T t1593 o1059 b1592 b4 b1593
4012 B b1594 t1593
4013 T t1594 o2 b1594
4014 B b1595 t1594
4015 T t1595 o1059 b1590 b4 b1595
4016 B b1596 t1595
4017 T t1596 o b1596 b4
4018 B b1597 t1596
4019 T t1597 o1058 b1586 b1597
4020 B b1598 t1597
4021 P p1598 String "rwh fold_equiv 5 thenT equivTransT << op{'g; 'a; 'a_1} >> thenT autoT thenT rwh unfold_equiv 5 ttca thenT rwh fold_equiv 5"
4022 O o1598 ext_rule p1598
4023 S s1598 t688 h h1392 h1393 h1394 h1396 h1554
4024 G s1598 t1494
4025 B b1599 s1598
4026 T t1599 o1060 b1599 b1390
4027 B b1600 t1599
4028 S s1600 t688 h h1392 h1393 h1394 h1460 h1554
4029 G s1600 t1494
4030 B b1601 s1600
4031 T t1601 o1060 b1601 b1390
4032 B b1602 t1601
4033 T t1602 o727 b588 b593 b1555 b1552
4034 S s1602 t688 h h1392 h1393 h1394 h1396 h1554
4035 G s1602 t1602
4036 B b1603 s1602
4037 T t1603 o1060 b1603 b1390
4038 B b1604 t1603
4039 T t1604 o2 b1596
4040 B b1605 t1604
4041 T t1605 o1059 b1592 b4 b1605
4042 B b1606 t1605
4043 T t1606 o2 b1606
4044 B b1607 t1606
4045 T t1607 o1059 b1604 b1122 b1607
4046 B b1608 t1607
4047 T t1608 o2 b1608
4048 B b1609 t1608
4049 T t1609 o1059 b1600 b4 b1609
4050 B b1610 t1609
4051 T t1610 o2 b1610
4052 B b1611 t1610
4053 T t1611 o1059 b1602 b4 b1611
4054 B b1612 t1611
4055 T t1612 o2 b1612
4056 B b1613 t1612
4057 T t1613 o1059 b1600 b4 b1613
4058 B b1614 t1613
4059 T t1614 o b1614 b4
4060 B b1615 t1614
4061 T t1615 o1058 b1596 b1615
4062 B b1616 t1615
4063 T t1616 o1058 b1614 b4
4064 B b1617 t1616
4065 T t1617 o1518 b1057 b1617 b4 b4
4066 B b1618 t1617
4067 T t1618 o b1618 b4
4068 B b1619 t1618
4069 T t1619 o1598 b1057 b1616 b1619 b4
4070 B b1620 t1619
4071 T t1620 o b1620 b4
4072 B b1621 t1620
4073 T t1621 o1588 b1057 b1598 b1621 b4
4074 B b1622 t1621
4075 T t1622 o b1622 b4
4076 B b1623 t1622
4077 T t1623 o1384 b1057 b1588 b1623 b4
4078 B b1624 t1623
4079 T t1624 o1055 b1624
4080 B b1625 t1624
4081 P p1625 Number 10125
4082 P p1626 Number 10132
4083 O o1626 resource_defs p1625 p1626 p204
4084 P p1627 Number 10130
4085 O o1627 uid p1627 p1626
4086 T t1627 o1627 b695
4087 B b1627 t1627
4088 T t1628 o b1627 b4
4089 B b1628 t1628
4090 T t1629 o1626 b1628
4091 B b1629 t1629
4092 T t1630 o b1629 b4
4093 B b1630 t1630
4094 T t1631 o1539 b680 b1549 b1625 b1630
4095 B b1631 t1631
4096 T t1632 o1538 b1631
4097 B b1632 t1632
4098 P p1632 Number 10580
4099 P p1633 Number 11708
4100 O o1633 location p1632 p1633
4101 P p1634 String cancel1
4102 O o1634 rule p1634
4103 T t1634 o727 b588 b593 b747 b810
4104 H h1634 x t1634
4105 S s1634 t683 h h1634 h1041
4106 G s1634 t742
4107 B b1634 s1634
4108 T t1635 o681 b1634
4109 B b1635 t1635
4110 S s1635 t683 h h1634 h1041
4111 G s1635 t745
4112 B b1636 s1635
4113 T t1636 o681 b1636
4114 B b1637 t1636
4115 S s1637 t683 h h1634 h1041
4116 G s1637 t783
4117 B b1638 s1637
4118 T t1638 o681 b1638
4119 B b1639 t1638
4120 S s1639 t683 h h1634 h1041
4121 G s1639 t685
4122 B b1640 s1639
4123 T t1640 o681 b1640
4124 B b1641 t1640
4125 S s1641 t688 h h1634 h1041
4126 G s1641 t583
4127 B b1642 s1641
4128 T t1642 o681 b1642
4129 B b1643 t1642
4130 S s1643 t688 h h1634 h1041
4131 G s1643 t761
4132 B b1644 s1643
4133 T t1644 o681 b1644
4134 B b1645 t1644
4135 S s1645 t688 h h1634 h1041
4136 G s1645 t763
4137 B b1646 s1645
4138 T t1646 o681 b1646
4139 B b1647 t1646
4140 S s1647 t688 h h1634 h1041
4141 G s1647 t785
4142 B b1648 s1647
4143 T t1648 o681 b1648
4144 B b1649 t1648
4145 T t1649 o727 b588 b593 b744 b782
4146 S s1649 t688 h h1634 h1041
4147 G s1649 t1649
4148 B b1650 s1649
4149 T t1650 o681 b1650
4150 B b1651 t1650
4151 T t1651 o680 b1649 b1651
4152 B b1652 t1651
4153 T t1652 o680 b1647 b1652
4154 B b1653 t1652
4155 T t1653 o680 b1645 b1653
4156 B b1654 t1653
4157 T t1654 o680 b1643 b1654
4158 B b1655 t1654
4159 T t1655 o680 b1641 b1655
4160 B b1656 t1655
4161 T t1656 o680 b1639 b1656
4162 B b1657 t1656
4163 T t1657 o680 b1637 b1657
4164 B b1658 t1657
4165 T t1658 o680 b1635 b1658
4166 B b1659 t1658
4167 P p1659 String "assertT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenT autoT"
4168 O o1659 ext_rule p1659
4169 T t1659 o b1648 b4
4170 B b1660 t1659
4171 T t1660 o b1646 b1660
4172 B b1661 t1660
4173 T t1661 o b1644 b1661
4174 B b1662 t1661
4175 T t1662 o b1642 b1662
4176 B b1663 t1662
4177 T t1663 o b1640 b1663
4178 B b1664 t1663
4179 T t1664 o b1638 b1664
4180 B b1665 t1664
4181 T t1665 o b1636 b1665
4182 B b1666 t1665
4183 T t1666 o b1634 b1666
4184 B b1667 t1666
4185 T t1667 o1060 b1650 b1667
4186 B b1668 t1667
4187 T t1668 o1059 b1668 b4 b1065
4188 B b1669 t1668
4189 T t1669 o598 b582 b968 b747
4190 B b1670 t1669
4191 T t1670 o598 b582 b968 b810
4192 B b1671 t1670
4193 T t1671 o727 b588 b593 b1670 b1671
4194 H h1671 v t1671
4195 S s1671 t688 h h1634 h1041 h1671
4196 G s1671 t1649
4197 B b1672 s1671
4198 T t1672 o1060 b1672 b1667
4199 B b1673 t1672
4200 T t1673 o2 b1669
4201 B b1674 t1673
4202 T t1674 o1059 b1673 b4 b1674
4203 B b1675 t1674
4204 T t1675 o b1675 b4
4205 B b1676 t1675
4206 T t1676 o1058 b1669 b1676
4207 B b1677 t1676
4208 P p1677 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 4 ttca"
4209 O o1677 ext_rule p1677
4210 T t1677 o598 b582 b1020 b744
4211 B b1678 t1677
4212 T t1678 o727 b588 b593 b1678 b1671
4213 H h1678 z t1678
4214 S s1678 t688 h h1634 h1041 h1671 h1678
4215 G s1678 t1649
4216 B b1679 s1678
4217 T t1679 o1060 b1679 b1667
4218 B b1680 t1679
4219 T t1680 o2 b1675
4220 B b1681 t1680
4221 T t1681 o1059 b1680 b4 b1681
4222 B b1682 t1681
4223 T t1682 o b1682 b4
4224 B b1683 t1682
4225 T t1683 o1058 b1675 b1683
4226 B b1684 t1683
4227 P p1684 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 5 ttca"
4228 O o1684 ext_rule p1684
4229 T t1684 o598 b582 b1020 b782
4230 B b1685 t1684
4231 T t1685 o727 b588 b593 b1678 b1685
4232 H h1685 z_1 t1685
4233 S s1685 t688 h h1634 h1041 h1671 h1678 h1685
4234 G s1685 t1649
4235 B b1686 s1685
4236 T t1686 o1060 b1686 b1667
4237 B b1687 t1686
4238 T t1687 o2 b1682
4239 B b1688 t1687
4240 T t1688 o1059 b1687 b4 b1688
4241 B b1689 t1688
4242 T t1689 o b1689 b4
4243 B b1690 t1689
4244 T t1690 o1058 b1682 b1690
4245 B b1691 t1690
4246 P p1691 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"
4247 O o1691 ext_rule p1691
4248 T t1691 o598 b582 b606 b744
4249 B b1692 t1691
4250 T t1692 o598 b582 b606 b782
4251 B b1693 t1692
4252 T t1693 o727 b588 b593 b1692 b1693
4253 H h1693 z_2 t1693
4254 S s1693 t688 h h1634 h1041 h1671 h1678 h1685 h1693
4255 G s1693 t1649
4256 B b1694 s1693
4257 T t1694 o1060 b1694 b1667
4258 B b1695 t1694
4259 T t1695 o2 b1689
4260 B b1696 t1695
4261 T t1696 o1059 b1695 b4 b1696
4262 B b1697 t1696
4263 T t1697 o b1697 b4
4264 B b1698 t1697
4265 T t1698 o1058 b1689 b1698
4266 B b1699 t1698
4267 P p1699 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"
4268 O o1699 ext_rule p1699
4269 T t1699 o727 b588 b593 b744 b1693
4270 H h1699 z_3 t1699
4271 S s1699 t688 h h1634 h1041 h1671 h1678 h1685 h1693 h1699
4272 G s1699 t1649
4273 B b1700 s1699
4274 T t1700 o1060 b1700 b1667
4275 B b1701 t1700
4276 T t1701 o2 b1697
4277 B b1702 t1701
4278 T t1702 o1059 b1701 b4 b1702
4279 B b1703 t1702
4280 T t1703 o b1703 b4
4281 B b1704 t1703
4282 T t1704 o1058 b1697 b1704
4283 B b1705 t1704
4284 P p1705 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"
4285 O o1705 ext_rule p1705
4286 T t1705 o1058 b1703 b4
4287 B b1706 t1705
4288 T t1706 o1705 b1057 b1706 b4 b4
4289 B b1707 t1706
4290 T t1707 o b1707 b4
4291 B b1708 t1707
4292 T t1708 o1699 b1057 b1705 b1708 b4
4293 B b1709 t1708
4294 T t1709 o b1709 b4
4295 B b1710 t1709
4296 T t1710 o1691 b1057 b1699 b1710 b4
4297 B b1711 t1710
4298 T t1711 o b1711 b4
4299 B b1712 t1711
4300 T t1712 o1684 b1057 b1691 b1712 b4
4301 B b1713 t1712
4302 T t1713 o b1713 b4
4303 B b1714 t1713
4304 T t1714 o1677 b1057 b1684 b1714 b4
4305 B b1715 t1714
4306 T t1715 o b1715 b4
4307 B b1716 t1715
4308 T t1716 o1659 b1057 b1677 b1716 b4
4309 B b1717 t1716
4310 T t1717 o1055 b1717
4311 B b1718 t1717
4312 T t1718 o1634 b1038 b1659 b1718 b4
4313 B b1719 t1718
4314 T t1719 o1633 b1719
4315 B b1720 t1719
4316 P p1720 Number 11753
4317 P p1721 Number 12881
4318 O o1721 location p1720 p1721
4319 P p1722 String cancel2
4320 O o1722 rule p1722
4321 H h1722 x t812
4322 S s1722 t683 h h1722 h1041
4323 G s1722 t742
4324 B b1722 s1722
4325 T t1722 o681 b1722
4326 B b1723 t1722
4327 S s1723 t683 h h1722 h1041
4328 G s1723 t745
4329 B b1724 s1723
4330 T t1724 o681 b1724
4331 B b1725 t1724
4332 S s1725 t683 h h1722 h1041
4333 G s1725 t783
4334 B b1726 s1725
4335 T t1726 o681 b1726
4336 B b1727 t1726
4337 S s1727 t683 h h1722 h1041
4338 G s1727 t685
4339 B b1728 s1727
4340 T t1728 o681 b1728
4341 B b1729 t1728
4342 S s1729 t688 h h1722 h1041
4343 G s1729 t583
4344 B b1730 s1729
4345 T t1730 o681 b1730
4346 B b1731 t1730
4347 S s1731 t688 h h1722 h1041
4348 G s1731 t761
4349 B b1732 s1731
4350 T t1732 o681 b1732
4351 B b1733 t1732
4352 S s1733 t688 h h1722 h1041
4353 G s1733 t763
4354 B b1734 s1733
4355 T t1734 o681 b1734
4356 B b1735 t1734
4357 S s1735 t688 h h1722 h1041
4358 G s1735 t785
4359 B b1736 s1735
4360 T t1736 o681 b1736
4361 B b1737 t1736
4362 S s1737 t688 h h1722 h1041
4363 G s1737 t787
4364 B b1738 s1737
4365 T t1738 o681 b1738
4366 B b1739 t1738
4367 T t1739 o680 b1737 b1739
4368 B b1740 t1739
4369 T t1740 o680 b1735 b1740
4370 B b1741 t1740
4371 T t1741 o680 b1733 b1741
4372 B b1742 t1741
4373 T t1742 o680 b1731 b1742
4374 B b1743 t1742
4375 T t1743 o680 b1729 b1743
4376 B b1744 t1743
4377 T t1744 o680 b1727 b1744
4378 B b1745 t1744
4379 T t1745 o680 b1725 b1745
4380 B b1746 t1745
4381 T t1746 o680 b1723 b1746
4382 B b1747 t1746
4383 P p1747 String "assertT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}} >> thenT autoT"
4384 O o1747 ext_rule p1747
4385 T t1747 o b1736 b4
4386 B b1748 t1747
4387 T t1748 o b1734 b1748
4388 B b1749 t1748
4389 T t1749 o b1732 b1749
4390 B b1750 t1749
4391 T t1750 o b1730 b1750
4392 B b1751 t1750
4393 T t1751 o b1728 b1751
4394 B b1752 t1751
4395 T t1752 o b1726 b1752
4396 B b1753 t1752
4397 T t1753 o b1724 b1753
4398 B b1754 t1753
4399 T t1754 o b1722 b1754
4400 B b1755 t1754
4401 T t1755 o1060 b1738 b1755
4402 B b1756 t1755
4403 T t1756 o1059 b1756 b4 b1065
4404 B b1757 t1756
4405 T t1757 o611 b582 b782
4406 B b1758 t1757
4407 T t1758 o598 b582 b810 b1758
4408 B b1759 t1758
4409 T t1759 o598 b582 b811 b1758
4410 B b1760 t1759
4411 T t1760 o727 b588 b593 b1759 b1760
4412 H h1760 v t1760
4413 S s1760 t688 h h1722 h1041 h1760
4414 G s1760 t787
4415 B b1761 s1760
4416 T t1761 o1060 b1761 b1755
4417 B b1762 t1761
4418 T t1762 o2 b1757
4419 B b1763 t1762
4420 T t1763 o1059 b1762 b4 b1763
4421 B b1764 t1763
4422 T t1764 o b1764 b4
4423 B b1765 t1764
4424 T t1765 o1058 b1757 b1765
4425 B b1766 t1765
4426 P p1766 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 4 ttca"
4427 O o1766 ext_rule p1766
4428 T t1766 o598 b582 b782 b1758
4429 B b1767 t1766
4430 T t1767 o598 b582 b741 b1767
4431 B b1768 t1767
4432 T t1768 o727 b588 b593 b1768 b1760
4433 H h1768 z t1768
4434 S s1768 t688 h h1722 h1041 h1760 h1768
4435 G s1768 t787
4436 B b1769 s1768
4437 T t1769 o1060 b1769 b1755
4438 B b1770 t1769
4439 T t1770 o2 b1764
4440 B b1771 t1770
4441 T t1771 o1059 b1770 b4 b1771
4442 B b1772 t1771
4443 T t1772 o b1772 b4
4444 B b1773 t1772
4445 T t1773 o1058 b1764 b1773
4446 B b1774 t1773
4447 P p1774 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 5 ttca"
4448 O o1774 ext_rule p1774
4449 T t1774 o598 b582 b744 b1767
4450 B b1775 t1774
4451 T t1775 o727 b588 b593 b1768 b1775
4452 H h1775 z_1 t1775
4453 S s1775 t688 h h1722 h1041 h1760 h1768 h1775
4454 G s1775 t787
4455 B b1776 s1775
4456 T t1776 o1060 b1776 b1755
4457 B b1777 t1776
4458 T t1777 o2 b1772
4459 B b1778 t1777
4460 T t1778 o1059 b1777 b4 b1778
4461 B b1779 t1778
4462 T t1779 o b1779 b4
4463 B b1780 t1779
4464 T t1780 o1058 b1772 b1780
4465 B b1781 t1780
4466 P p1781 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 6 ttca"
4467 O o1781 ext_rule p1781
4468 T t1781 o598 b582 b741 b606
4469 B b1782 t1781
4470 T t1782 o598 b582 b744 b606
4471 B b1783 t1782
4472 T t1783 o727 b588 b593 b1782 b1783
4473 H h1783 z_2 t1783
4474 S s1783 t688 h h1722 h1041 h1760 h1768 h1775 h1783
4475 G s1783 t787
4476 B b1784 s1783
4477 T t1784 o1060 b1784 b1755
4478 B b1785 t1784
4479 T t1785 o2 b1779
4480 B b1786 t1785
4481 T t1786 o1059 b1785 b4 b1786
4482 B b1787 t1786
4483 T t1787 o b1787 b4
4484 B b1788 t1787
4485 T t1788 o1058 b1779 b1788
4486 B b1789 t1788
4487 P p1789 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's1; id{'g}}; 's1} >> 7 ttca"
4488 O o1789 ext_rule p1789
4489 T t1789 o727 b588 b593 b741 b1783
4490 H h1789 z_3 t1789
4491 S s1789 t688 h h1722 h1041 h1760 h1768 h1775 h1783 h1789
4492 G s1789 t787
4493 B b1790 s1789
4494 T t1790 o1060 b1790 b1755
4495 B b1791 t1790
4496 T t1791 o2 b1787
4497 B b1792 t1791
4498 T t1792 o1059 b1791 b4 b1792
4499 B b1793 t1792
4500 T t1793 o b1793 b4
4501 B b1794 t1793
4502 T t1794 o1058 b1787 b1794
4503 B b1795 t1794
4504 P p1795 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's2; id{'g}}; 's2} >> 8 ttca"
4505 O o1795 ext_rule p1795
4506 T t1795 o1058 b1793 b4
4507 B b1796 t1795
4508 T t1796 o1795 b1057 b1796 b4 b4
4509 B b1797 t1796
4510 T t1797 o b1797 b4
4511 B b1798 t1797
4512 T t1798 o1789 b1057 b1795 b1798 b4
4513 B b1799 t1798
4514 T t1799 o b1799 b4
4515 B b1800 t1799
4516 T t1800 o1781 b1057 b1789 b1800 b4
4517 B b1801 t1800
4518 T t1801 o b1801 b4
4519 B b1802 t1801
4520 T t1802 o1774 b1057 b1781 b1802 b4
4521 B b1803 t1802
4522 T t1803 o b1803 b4
4523 B b1804 t1803
4524 T t1804 o1766 b1057 b1774 b1804 b4
4525 B b1805 t1804
4526 T t1805 o b1805 b4
4527 B b1806 t1805
4528 T t1806 o1747 b1057 b1766 b1806 b4
4529 B b1807 t1806
4530 T t1807 o1055 b1807
4531 B b1808 t1807
4532 T t1808 o1722 b1038 b1747 b1808 b4
4533 B b1809 t1808
4534 T t1809 o1721 b1809
4535 B b1810 t1809
4536 P p1810 Number 12883
4537 P p1811 Number 12970
4538 O o1811 location p1810 p1811
4539 NOcaml!str_let str_let str_let Ocaml
4540 O o1812 str_let p1810 p1811
4541 NOcaml!patt_var patt_var patt_var Ocaml
4542 P p1812 Number 12887
4543 O o1813 patt_var p1812 p1811
4544 NOcaml!patt_done patt_done patt_done Ocaml
4545 O o1814 patt_done p1810 p1811
4546 T t1814 o1814
4547 B b1814 t1814 groupCancelLeftT
4548 T t1815 o1813 b1814
4549 B b1815 t1815
4550 NOcaml!fun fun fun Ocaml
4551 O o1815 fun p1812 p1811
4552 NOcaml!patt_if patt_if patt_if Ocaml
4553 O o1816 patt_if p1812 p1811
4554 P p1816 Number 12904
4555 P p1817 Number 12905
4556 O o1817 patt_var p1816 p1817
4557 NOcaml!patt_body patt_body patt_body Ocaml
4558 O o1818 patt_body p1812 p1811
4559 P p1818 Number 12906
4560 P p1819 Number 12907
4561 O o1819 patt_var p1818 p1819
4562 NOcaml!let let let Ocaml
4563 P p1820 Number 12913
4564 O o1820 let p1820 p1811
4565 NOcaml!patt_tuple patt_tuple patt_tuple Ocaml
4566 P p1821 Number 12917
4567 P p1822 Number 12921
4568 O o1822 patt_tuple p1821 p1822
4569 P p1823 Number 12918
4570 O o1823 patt_var p1821 p1823
4571 NOcaml!patt_tuple_arg patt_tuple_arg patt_tuple_arg Ocaml
4572 O o1824 patt_tuple_arg p1821 p1822
4573 P p1824 Number 12920
4574 O o1825 patt_var p1824 p1822
4575 NOcaml!patt_tuple_end patt_tuple_end patt_tuple_end Ocaml
4576 O o1826 patt_tuple_end p1821 p1822
4577 NOcaml!patt_in patt_in patt_in Ocaml
4578 O o1827 patt_in p1820 p1811
4579 NOcaml!apply apply apply Ocaml
4580 P p1827 Number 12957
4581 O o1828 apply p1827 p1811
4582 P p1828 Number 12968
4583 O o1829 apply p1827 p1828
4584 P p1829 Number 12966
4585 O o1830 apply p1827 p1829
4586 NOcaml!lid lid lid Ocaml
4587 P p1830 Number 12964
4588 O o1831 lid p1827 p1830
4589 O o1832 lid p1634
4590 T t1832 o1832
4591 B b1832 t1832
4592 T t1833 o1831 b1832
4593 B b1833 t1833
4594 P p1833 Number 12965
4595 O o1833 lid p1833 p1829
4596 P p1834 Var j
4597 O o1834 var p1834
4598 T t1834 o1834
4599 B b1834 t1834
4600 T t1835 o1833 b1834
4601 B b1835 t1835
4602 T t1836 o1830 b1833 b1835
4603 B b1836 t1836
4604 P p1836 Number 12967
4605 O o1836 lid p1836 p1828
4606 P p1837 Var k
4607 O o1837 var p1837
4608 T t1837 o1837
4609 B b1837 t1837
4610 T t1838 o1836 b1837
4611 B b1838 t1838
4612 T t1839 o1829 b1836 b1838
4613 B b1839 t1839
4614 P p1839 Number 12969
4615 O o1839 lid p1839 p1811
4616 P p1840 Var p
4617 O o1840 var p1840
4618 T t1840 o1840
4619 B b1840 t1840
4620 T t1841 o1839 b1840
4621 B b1841 t1841
4622 T t1842 o1828 b1839 b1841
4623 B b1842 t1842
4624 T t1843 o1827 b1842
4625 B b1843 t1843
4626 T t1844 o1826 b1843
4627 B b1844 t1844 k
4628 T t1845 o1825 b1844
4629 B b1845 t1845
4630 T t1846 o1824 b1845
4631 B b1846 t1846 j
4632 T t1847 o1823 b1846
4633 B b1847 t1847
4634 T t1848 o1822 b1847
4635 B b1848 t1848
4636 P p1848 Number 12924
4637 P p1849 Number 12947
4638 O o1849 apply p1848 p1849
4639 P p1850 Number 12945
4640 O o1850 apply p1848 p1850
4641 NOcaml!proj proj proj Ocaml
4642 P p1851 Number 12943
4643 O o1851 proj p1848 p1851
4644 O o1852 uid p1848 p1851
4645 O o1853 uid p536
4646 T t1853 o1853
4647 B b1853 t1853
4648 T t1854 o1852 b1853
4649 B b1854 t1854
4650 P p1854 Number 12932
4651 O o1854 lid p1854 p1851
4652 P p1855 String hyp_indices
4653 O o1855 lid p1855
4654 T t1855 o1855
4655 B b1855 t1855
4656 T t1856 o1854 b1855
4657 B b1856 t1856
4658 T t1857 o1851 b1854 b1856
4659 B b1857 t1857
4660 P p1857 Number 12944
4661 O o1857 lid p1857 p1850
4662 T t1858 o1857 b1840
4663 B b1858 t1858
4664 T t1859 o1850 b1857 b1858
4665 B b1859 t1859
4666 P p1859 Number 12946
4667 O o1859 lid p1859 p1849
4668 P p1860 Var i
4669 O o1860 var p1860
4670 T t1860 o1860
4671 B b1860 t1860
4672 T t1861 o1859 b1860
4673 B b1861 t1861
4674 T t1862 o1849 b1859 b1861
4675 B b1862 t1862
4676 T t1863 o b1862 b4
4677 B b1863 t1863
4678 T t1864 o1820 b1848 b1863
4679 B b1864 t1864
4680 T t1865 o1818 b1864
4681 B b1865 t1865 p
4682 T t1866 o1819 b1865
4683 B b1866 t1866
4684 T t1867 o1816 b1866
4685 B b1867 t1867
4686 T t1868 o1815 b1867
4687 B b1868 t1868
4688 T t1869 o1818 b1868
4689 B b1869 t1869 i
4690 T t1870 o1817 b1869
4691 B b1870 t1870
4692 T t1871 o1816 b1870
4693 B b1871 t1871
4694 T t1872 o1815 b1871
4695 B b1872 t1872
4696 T t1873 o1812 b1815 b1872
4697 B b1873 t1873
4698 T t1874 o b1873 b4
4699 B b1874 t1874
4700 T t1875 o1812 b1874
4701 B b1875 t1875
4702 T t1876 o419 b1875
4703 B b1876 t1876
4704 T t1877 o1811 b1876
4705 B b1877 t1877
4706 P p1877 Number 12972
4707 P p1878 Number 13060
4708 O o1878 location p1877 p1878
4709 O o1879 str_let p1877 p1878
4710 P p1879 Number 12976
4711 O o1880 patt_var p1879 p1878
4712 O o1881 patt_done p1877 p1878
4713 T t1881 o1881
4714 B b1881 t1881 groupCancelRightT
4715 T t1882 o1880 b1881
4716 B b1882 t1882
4717 O o1882 fun p1879 p1878
4718 O o1883 patt_if p1879 p1878
4719 P p1883 Number 12994
4720 P p1884 Number 12995
4721 O o1884 patt_var p1883 p1884
4722 O o1885 patt_body p1879 p1878
4723 P p1885 Number 12996
4724 P p1886 Number 12997
4725 O o1886 patt_var p1885 p1886
4726 P p1887 Number 13003
4727 O o1887 let p1887 p1878
4728 P p1888 Number 13007
4729 P p1889 Number 13011
4730 O o1889 patt_tuple p1888 p1889
4731 P p1890 Number 13008
4732 O o1890 patt_var p1888 p1890
4733 O o1891 patt_tuple_arg p1888 p1889
4734 P p1891 Number 13010
4735 O o1892 patt_var p1891 p1889
4736 O o1893 patt_tuple_end p1888 p1889
4737 O o1894 patt_in p1887 p1878
4738 P p1894 Number 13047
4739 O o1895 apply p1894 p1878
4740 P p1895 Number 13058
4741 O o1896 apply p1894 p1895
4742 P p1896 Number 13056
4743 O o1897 apply p1894 p1896
4744 P p1897 Number 13054
4745 O o1898 lid p1894 p1897
4746 O o1899 lid p1722
4747 T t1899 o1899
4748 B b1899 t1899
4749 T t1900 o1898 b1899
4750 B b1900 t1900
4751 P p1900 Number 13055
4752 O o1900 lid p1900 p1896
4753 T t1901 o1900 b1834
4754 B b1901 t1901
4755 T t1902 o1897 b1900 b1901
4756 B b1902 t1902
4757 P p1902 Number 13057
4758 O o1902 lid p1902 p1895
4759 T t1903 o1902 b1837
4760 B b1903 t1903
4761 T t1904 o1896 b1902 b1903
4762 B b1904 t1904
4763 P p1904 Number 13059
4764 O o1904 lid p1904 p1878
4765 T t1905 o1904 b1840
4766 B b1905 t1905
4767 T t1906 o1895 b1904 b1905
4768 B b1906 t1906
4769 T t1907 o1894 b1906
4770 B b1907 t1907
4771 T t1908 o1893 b1907
4772 B b1908 t1908 k
4773 T t1909 o1892 b1908
4774 B b1909 t1909
4775 T t1910 o1891 b1909
4776 B b1910 t1910 j
4777 T t1911 o1890 b1910
4778 B b1911 t1911
4779 T t1912 o1889 b1911
4780 B b1912 t1912
4781 P p1912 Number 13014
4782 P p1913 Number 13037
4783 O o1913 apply p1912 p1913
4784 P p1914 Number 13035
4785 O o1914 apply p1912 p1914
4786 P p1915 Number 13033
4787 O o1915 proj p1912 p1915
4788 O o1916 uid p1912 p1915
4789 T t1916 o1916 b1853
4790 B b1916 t1916
4791 P p1916 Number 13022
4792 O o1917 lid p1916 p1915
4793 T t1917 o1917 b1855
4794 B b1917 t1917
4795 T t1918 o1915 b1916 b1917
4796 B b1918 t1918
4797 P p1918 Number 13034
4798 O o1918 lid p1918 p1914
4799 T t1919 o1918 b1840
4800 B b1919 t1919
4801 T t1920 o1914 b1918 b1919
4802 B b1920 t1920
4803 P p1920 Number 13036
4804 O o1920 lid p1920 p1913
4805 T t1921 o1920 b1860
4806 B b1921 t1921
4807 T t1922 o1913 b1920 b1921
4808 B b1922 t1922
4809 T t1923 o b1922 b4
4810 B b1923 t1923
4811 T t1924 o1887 b1912 b1923
4812 B b1924 t1924
4813 T t1925 o1885 b1924
4814 B b1925 t1925 p
4815 T t1926 o1886 b1925
4816 B b1926 t1926
4817 T t1927 o1883 b1926
4818 B b1927 t1927
4819 T t1928 o1882 b1927
4820 B b1928 t1928
4821 T t1929 o1885 b1928
4822 B b1929 t1929 i
4823 T t1930 o1884 b1929
4824 B b1930 t1930
4825 T t1931 o1883 b1930
4826 B b1931 t1931
4827 T t1932 o1882 b1931
4828 B b1932 t1932
4829 T t1933 o1879 b1882 b1932
4830 B b1933 t1933
4831 T t1934 o b1933 b4
4832 B b1934 t1934
4833 T t1935 o1879 b1934
4834 B b1935 t1935
4835 T t1936 o419 b1935
4836 B b1936 t1936
4837 T t1937 o1878 b1936
4838 B b1937 t1937
4839 P p1937 Number 13078
4840 P p1938 Number 13450
4841 O o1938 location p1937 p1938
4842 P p1939 String unique_id1
4843 O o1939 rule p1939
4844 P p1940 Var e2
4845 O o1940 var p1940
4846 T t1940 o1940
4847 B b1940 t1940
4848 T t1941 o704 b1940
4849 S s1941 t683 h
4850 G s1941 t1941
4851 B b1941 s1941
4852 T t1942 o681 b1941
4853 B b1942 t1942
4854 T t1943 o761 b1940 b588
4855 S s1943 t688 h
4856 G s1943 t1943
4857 B b1943 s1943
4858 T t1944 o681 b1943
4859 B b1944 t1944
4860 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4861 NCzf_itt_dall!dall dall dall Czf_itt_dall
4862 O o1944 dall
4863 T t1945 o598 b582 b1940 b832
4864 B b1945 t1945
4865 T t1946 o727 b588 b593 b1945 b832
4866 B b1946 t1946 s
4867 T t1947 o1944 b588 b1946
4868 S s1947 t688 h
4869 G s1947 t1947
4870 B b1947 s1947
4871 T t1948 o681 b1947
4872 B b1948 t1948
4873 T t1949 o727 b588 b593 b1940 b606
4874 S s1949 t688 h
4875 G s1949 t1949
4876 B b1949 s1949
4877 T t1950 o681 b1949
4878 B b1950 t1950
4879 T t1951 o680 b1948 b1950
4880 B b1951 t1951
4881 T t1952 o680 b1944 b1951
4882 B b1952 t1952
4883 T t1953 o680 b727 b1952
4884 B b1953 t1953
4885 T t1954 o680 b686 b1953
4886 B b1954 t1954
4887 T t1955 o680 b1942 b1954
4888 B b1955 t1955
4889 P p1955 String "assumT 5 thenT withT << id{'g} >> (dT 2) thenT autoT"
4890 O o1955 ext_rule p1955
4891 T t1956 o b1947 b4
4892 B b1956 t1956
4893 T t1957 o b1943 b1956
4894 B b1957 t1957
4895 T t1958 o b726 b1957
4896 B b1958 t1958
4897 T t1959 o b685 b1958
4898 B b1959 t1959
4899 T t1960 o b1941 b1959
4900 B b1960 t1960
4901 T t1961 o1060 b1949 b1960
4902 B b1961 t1961
4903 T t1962 o1059 b1961 b4 b1065
4904 B b1962 t1962
4905 P p1962 String wf
4906 O o1962 tactic_arg p1962
4907 H h1962 v t1947
4908 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
4909 O o1963 fun_prop
4910 P p1963 Var w
4911 O o1964 var p1963
4912 T t1964 o1964
4913 B b1964 t1964
4914 T t1965 o598 b582 b1940 b1964
4915 B b1965 t1965
4916 T t1966 o727 b588 b593 b1965 b1964
4917 B b1966 t1966 w
4918 T t1967 o1963 b1966
4919 S s1967 t688 h h1962
4920 G s1967 t1967
4921 B b1967 s1967
4922 T t1968 o1060 b1967 b1960
4923 B b1968 t1968
4924 S s1968 t688 h h1962
4925 G s1968 t1949
4926 B b1969 s1968
4927 T t1969 o1060 b1969 b1960
4928 B b1970 t1969
4929 P p1970 String with
4930 O o1970 arg_named p1970
4931 NSummary!arg_term_list arg_term_list arg_term_list Summary
4932 O o1971 arg_term_list
4933 T t1971 o b606 b4
4934 B b1971 t1971
4935 T t1972 o1971 b1971
4936 B b1972 t1972
4937 T t1973 o1970 b1972
4938 B b1973 t1973
4939 T t1974 o b1973 b4
4940 B b1974 t1974
4941 T t1975 o2 b1962
4942 B b1975 t1975
4943 T t1976 o1059 b1970 b1974 b1975
4944 B b1976 t1976
4945 T t1977 o2 b1976
4946 B b1977 t1977
4947 T t1978 o1962 b1968 b4 b1977
4948 B b1978 t1978
4949 T t1979 o598 b582 b1940 b606
4950 B b1979 t1979
4951 T t1980 o727 b588 b593 b1979 b606
4952 H h1980 w t1980
4953 S s1980 t688 h h1962 h1980
4954 G s1980 t1949
4955 B b1980 s1980
4956 T t1981 o1060 b1980 b1960
4957 B b1981 t1981
4958 T t1982 o1059 b1981 b4 b1977
4959 B b1982 t1982
4960 T t1983 o b1982 b4
4961 B b1983 t1983
4962 T t1984 o b1978 b1983
4963 B b1984 t1984
4964 T t1985 o1058 b1962 b1984
4965 B b1985 t1985
4966 P p1985 String "rwh unfold_fun_prop 0 thenT autoT"
4967 O o1985 ext_rule p1985
4968 H h1985 s1 t1108
4969 H h1986 s2 t1108
4970 NCzf_itt_eq!equal equal1986 equal Czf_itt_eq
4971 O o1986 equal1986
4972 T t1986 o1986 b741 b744
4973 H h1987 x t1986
4974 T t1987 o598 b582 b1940 b741
4975 B b1987 t1987
4976 T t1988 o727 b588 b593 b1987 b741
4977 H h1988 x_1 t1988
4978 T t1989 o598 b582 b1940 b744
4979 B b1989 t1989
4980 T t1990 o727 b588 b593 b1989 b744
4981 S s1990 t688 h h1962 h1985 h1986 h1987 h1988
4982 G s1990 t1990
4983 B b1990 s1990
4984 T t1991 o1060 b1990 b1960
4985 B b1991 t1991
4986 B b1992 t1988
4987 B b1993 t1990
4988 T t1993 o1115 b1992 b1993
4989 S s1993 t688 h h1962 h1985 h1986 h1987
4990 G s1993 t1993
4991 B b1994 s1993
4992 T t1994 o1060 b1994 b1960
4993 B b1995 t1994
4994 B b1996 t1986
4995 B b1997 t1993
4996 T t1997 o1115 b1996 b1997
4997 S s1997 t688 h h1962 h1985 h1986
4998 G s1997 t1997
4999 B b1998 s1997
5000 T t1998 o1060 b1998 b1960
5001 B b1999 t1998
5002 B b2000 t1997 s2
5003 T t2000 o1130 b1131 b2000
5004 S s2000 t688 h h1962 h1985
5005 G s2000 t2000
5006 B b2001 s2000
5007 T t2001 o1060 b2001 b1960
5008 B b2002 t2001
5009 B b2003 t2000 s1
5010 T t2003 o1130 b1131 b2003
5011 S s2003 t688 h h1962
5012 G s2003 t2003
5013 B b2004 s2003
5014 T t2004 o1060 b2004 b1960
5015 B b2005 t2004
5016 T t2005 o2 b1978
5017 B b2006 t2005
5018 T t2006 o1962 b2005 b1122 b2006
5019 B b2007 t2006
5020 T t2007 o2 b2007
5021 B b2008 t2007
5022 T t2008 o1059 b2002 b1122 b2008
5023 B b2009 t2008
5024 T t2009 o2 b2009
5025 B b2010 t2009
5026 T t2010 o1059 b1999 b1122 b2010
5027 B b2011 t2010
5028 T t2011 o2 b2011
5029 B b2012 t2011
5030 T t2012 o1059 b1995 b1122 b2012
5031 B b2013 t2012
5032 T t2013 o2 b2013
5033 B b2014 t2013
5034 T t2014 o1059 b1991 b4 b2014
5035 B b2015 t2014
5036 T t2015 o b2015 b4
5037 B b2016 t2015
5038 T t2016 o1058 b1978 b2016
5039 B b2017 t2016
5040 P p2017 String "equivTransT << 's1 >> thenT autoT thenT rwh unfold_equiv 6 ttca"
5041 O o2017 ext_rule p2017
5042 T t2017 o704 b1987
5043 B b2018 t2017
5044 B b2019 t742
5045 T t2019 o1153 b2018 b2019
5046 B b2020 t2019
5047 T t2020 o1153 b1155 b2020
5048 B b2021 t2020
5049 T t2021 o1153 b1154 b2021
5050 B b2022 t2021
5051 T t2022 o761 b1987 b588
5052 B b2023 t2022
5053 B b2024 t761
5054 T t2024 o1153 b2023 b2024
5055 B b2025 t2024
5056 T t2025 o1153 b2022 b2025
5057 B b2026 t2025
5058 T t2026 o1164 b1987 b741
5059 B b2027 t2026
5060 T t2027 o761 b2027 b593
5061 B b2028 t2027
5062 T t2028 o1153 b2026 b2028
5063 H h2028 x_1 t2028
5064 S s2028 t688 h h1962 h1985 h1986 h1987 h2028
5065 G s2028 t763
5066 B b2029 s2028
5067 T t2029 o1060 b2029 b1960
5068 B b2030 t2029
5069 S s2030 t688 h h1962 h1985 h1986 h1987 h1988
5070 G s2030 t763
5071 B b2031 s2030
5072 T t2031 o1060 b2031 b1960
5073 B b2032 t2031
5074 T t2032 o761 b1989 b588
5075 S s2032 t688 h h1962 h1985 h1986 h1987 h1988
5076 G s2032 t2032
5077 B b2033 s2032
5078 T t2033 o1060 b2033 b1960
5079 B b2034 t2033
5080 T t2034 o2 b2015
5081 B b2035 t2034
5082 T t2035 o1059 b2034 b1122 b2035
5083 B b2036 t2035
5084 T t2036 o2 b2036
5085 B b2037 t2036
5086 T t2037 o1059 b2032 b4 b2037
5087 B b2038 t2037
5088 T t2038 o2 b2038
5089 B b2039 t2038
5090 T t2039 o1059 b2030 b4 b2039
5091 B b2040 t2039
5092 T t2040 o727 b588 b593 b1989 b741
5093 S s2040 t688 h h1962 h1985 h1986 h1987 h2028
5094 G s2040 t2040
5095 B b2041 s2040
5096 T t2041 o1060 b2041 b1960
5097 B b2042 t2041
5098 S s2042 t688 h h1962 h1985 h1986 h1987 h1988
5099 G s2042 t2040
5100 B b2043 s2042
5101 T t2043 o1060 b2043 b1960
5102 B b2044 t2043
5103 T t2044 o1059 b2044 b4 b2035
5104 B b2045 t2044
5105 T t2045 o2 b2045
5106 B b2046 t2045
5107 T t2046 o1059 b2042 b4 b2046
5108 B b2047 t2046
5109 S s2047 t688 h h1962 h1985 h1986 h1987 h2028
5110 G s2047 t787
5111 B b2048 s2047
5112 T t2048 o1060 b2048 b1960
5113 B b2049 t2048
5114 S s2049 t688 h h1962 h1985 h1986 h1987 h1988
5115 G s2049 t787
5116 B b2050 s2049
5117 T t2050 o1060 b2050 b1960
5118 B b2051 t2050
5119 T t2051 o1059 b2051 b4 b2035
5120 B b2052 t2051
5121 T t2052 o2 b2052
5122 B b2053 t2052
5123 T t2053 o1059 b2049 b4 b2053
5124 B b2054 t2053
5125 T t2054 o b2054 b4
5126 B b2055 t2054
5127 T t2055 o b2047 b2055
5128 B b2056 t2055
5129 T t2056 o b2040 b2056
5130 B b2057 t2056
5131 T t2057 o1058 b2015 b2057
5132 B b2058 t2057
5133 P p2058 String "autoT thenT setSubstT << equal{'s1; 's2} >> 11 ttca"
5134 O o2058 ext_rule p2058
5135 T t2058 o1058 b2040 b4
5136 B b2059 t2058
5137 T t2059 o2058 b1057 b2059 b4 b4
5138 B b2060 t2059
5139 P p2060 String "equivTransT << op{'g; 'e2; 's1} >> ttca thenT rwh fold_equiv 6 thenT autoT thenT rwh unfold_equiv 6 thenT autoT"
5140 O o2060 ext_rule p2060
5141 H h2060 y_2 t704
5142 H h2061 y_1 t715
5143 H h2062 y_3 t2017
5144 H h2063 z_1 t742
5145 H h2064 y t2022
5146 H h2065 z_2 t761
5147 H h2066 z t2027
5148 S s2066 t688 h h1962 h1985 h1986 h1987 h2060 h2061 h2062 h2063 h2064 h2065 h2066
5149 G s2066 t763
5150 B b2066 s2066
5151 T t2066 o1060 b2066 b1960
5152 B b2067 t2066
5153 H h2067 z_3 t2019
5154 S s2067 t688 h h1962 h1985 h1986 h1987 h2060 h2061 h2067 h2064 h2065 h2066
5155 G s2067 t763
5156 B b2068 s2067
5157 T t2068 o1060 b2068 b1960
5158 B b2069 t2068
5159 H h2069 z_1 t2020
5160 S s2069 t688 h h1962 h1985 h1986 h1987 h2060 h2069 h2064 h2065 h2066
5161 G s2069 t763
5162 B b2070 s2069
5163 T t2070 o1060 b2070 b1960
5164 B b2071 t2070
5165 H h2071 y_1 t2021
5166 S s2071 t688 h h1962 h1985 h1986 h1987 h2071 h2064 h2065 h2066
5167 G s2071 t763
5168 B b2072 s2071
5169 T t2072 o1060 b2072 b1960
5170 B b2073 t2072
5171 H h2073 z_1 t2024
5172 S s2073 t688 h h1962 h1985 h1986 h1987 h2071 h2073 h2066
5173 G s2073 t763
5174 B b2074 s2073
5175 T t2074 o1060 b2074 b1960
5176 B b2075 t2074
5177 H h2075 y t2025
5178 S s2075 t688 h h1962 h1985 h1986 h1987 h2075 h2066
5179 G s2075 t763
5180 B b2076 s2075
5181 T t2076 o1060 b2076 b1960
5182 B b2077 t2076
5183 S s2077 t688 h h1962 h1985 h1986 h1987 h2028
5184 G s2077 t2032
5185 B b2078 s2077
5186 T t2078 o1060 b2078 b1960
5187 B b2079 t2078
5188 T t2079 o2 b2047
5189 B b2080 t2079
5190 T t2080 o1059 b2079 b4 b2080
5191 B b2081 t2080
5192 T t2081 o2 b2081
5193 B b2082 t2081
5194 T t2082 o1059 b2034 b1122 b2082
5195 B b2083 t2082
5196 T t2083 o2 b2083
5197 B b2084 t2083
5198 T t2084 o1059 b2032 b4 b2084
5199 B b2085 t2084
5200 T t2085 o2 b2085
5201 B b2086 t2085
5202 T t2086 o1059 b2030 b4 b2086
5203 B b2087 t2086
5204 T t2087 o2 b2087
5205 B b2088 t2087
5206 T t2088 o1059 b2077 b4 b2088
5207 B b2089 t2088
5208 T t2089 o2 b2089
5209 B b2090 t2089
5210 T t2090 o1059 b2075 b4 b2090
5211 B b2091 t2090
5212 T t2091 o2 b2091
5213 B b2092 t2091
5214 T t2092 o1059 b2073 b4 b2092
5215 B b2093 t2092
5216 T t2093 o2 b2093
5217 B b2094 t2093
5218 T t2094 o1059 b2071 b4 b2094
5219 B b2095 t2094
5220 T t2095 o2 b2095
5221 B b2096 t2095
5222 T t2096 o1059 b2069 b4 b2096
5223 B b2097 t2096
5224 T t2097 o2 b2097
5225 B b2098 t2097
5226 T t2098 o1059 b2067 b4 b2098
5227 B b2099 t2098
5228 T t2099 o727 b588 b593 b744 b741
5229 S s2099 t688 h h1962 h1985 h1986 h1987 h2060 h2061 h2062 h2063 h2064 h2065 h2066
5230 G s2099 t2099
5231 B b2100 s2099
5232 T t2100 o1060 b2100 b1960
5233 B b2101 t2100
5234 S s2101 t688 h h1962 h1985 h1986 h1987 h2060 h2061 h2067 h2064 h2065 h2066
5235 G s2101 t2099
5236 B b2102 s2101
5237 T t2102 o1060 b2102 b1960
5238 B b2103 t2102
5239 S s2103 t688 h h1962 h1985 h1986 h1987 h2060 h2069 h2064 h2065 h2066
5240 G s2103 t2099
5241 B b2104 s2103
5242 T t2104 o1060 b2104 b1960
5243 B b2105 t2104
5244 S s2105 t688 h h1962 h1985 h1986 h1987 h2071 h2064 h2065 h2066
5245 G s2105 t2099
5246 B b2106 s2105
5247 T t2106 o1060 b2106 b1960
5248 B b2107 t2106
5249 S s2107 t688 h h1962 h1985 h1986 h1987 h2071 h2073 h2066
5250 G s2107 t2099
5251 B b2108 s2107
5252 T t2108 o1060 b2108 b1960
5253 B b2109 t2108
5254 S s2109 t688 h h1962 h1985 h1986 h1987 h2075 h2066
5255 G s2109 t2099
5256 B b2110 s2109
5257 T t2110 o1060 b2110 b1960
5258 B b2111 t2110
5259 S s2111 t688 h h1962 h1985 h1986 h1987 h2028
5260 G s2111 t2099
5261 B b2112 s2111
5262 T t2112 o1060 b2112 b1960
5263 B b2113 t2112
5264 S s2113 t688 h h1962 h1985 h1986 h1987 h1988
5265 G s2113 t2099
5266 B b2114 s2113
5267 T t2114 o1060 b2114 b1960
5268 B b2115 t2114
5269 T t2115 o727 b588 b593 b1989 b1987
5270 S s2115 t688 h h1962 h1985 h1986 h1987 h1988
5271 G s2115 t2115
5272 B b2116 s2115
5273 T t2116 o1060 b2116 b1960
5274 B b2117 t2116
5275 S s2117 t688 h h1962 h1985 h1986 h1987 h2028
5276 G s2117 t2115
5277 B b2118 s2117
5278 T t2118 o1060 b2118 b1960
5279 B b2119 t2118
5280 T t2119 o1059 b2119 b4 b2080
5281 B b2120 t2119
5282 T t2120 o2 b2120
5283 B b2121 t2120
5284 T t2121 o1059 b2117 b1122 b2121
5285 B b2122 t2121
5286 T t2122 o2 b2122
5287 B b2123 t2122
5288 T t2123 o1059 b2115 b4 b2123
5289 B b2124 t2123
5290 T t2124 o2 b2124
5291 B b2125 t2124
5292 T t2125 o1059 b2113 b4 b2125
5293 B b2126 t2125
5294 T t2126 o2 b2126
5295 B b2127 t2126
5296 T t2127 o1059 b2111 b4 b2127
5297 B b2128 t2127
5298 T t2128 o2 b2128
5299 B b2129 t2128
5300 T t2129 o1059 b2109 b4 b2129
5301 B b2130 t2129
5302 T t2130 o2 b2130
5303 B b2131 t2130
5304 T t2131 o1059 b2107 b4 b2131
5305 B b2132 t2131
5306 T t2132 o2 b2132
5307 B b2133 t2132
5308 T t2133 o1059 b2105 b4 b2133
5309 B b2134 t2133
5310 T t2134 o2 b2134
5311 B b2135 t2134
5312 T t2135 o1059 b2103 b4 b2135
5313 B b2136 t2135
5314 T t2136 o2 b2136
5315 B b2137 t2136
5316 T t2137 o1059 b2101 b4 b2137
5317 B b2138 t2137
5318 T t2138 o b2138 b4
5319 B b2139 t2138
5320 T t2139 o b2099 b2139
5321 B b2140 t2139
5322 T t2140 o1058 b2047 b2140
5323 B b2141 t2140
5324 P p2141 String "setSubstT << equal{'s1; 's2} >> 11 ttca"
5325 O o2141 ext_rule p2141
5326 T t2141 o1058 b2099 b4
5327 B b2142 t2141
5328 T t2142 o2141 b1057 b2142 b4 b4
5329 B b2143 t2142
5330 P p2143 String "setSubstT << equal{'s1; 's2} >> 0 thenT autoT"
5331 O o2143 ext_rule p2143
5332 T t2143 o727 b588 b593 b744 b744
5333 S s2143 t688 h h1962 h1985 h1986 h1987 h2060 h2061 h2062 h2063 h2064 h2065 h2066
5334 G s2143 t2143
5335 B b2144 s2143
5336 T t2144 o1060 b2144 b1960
5337 B b2145 t2144
5338 T t2145 o2 b2138
5339 B b2146 t2145
5340 T t2146 o1059 b2145 b4 b2146
5341 B b2147 t2146
5342 T t2147 o2 b2147
5343 B b2148 t2147
5344 T t2148 o1059 b2067 b4 b2148
5345 B b2149 t2148
5346 T t2149 o b2149 b4
5347 B b2150 t2149
5348 T t2150 o1058 b2138 b2150
5349 B b2151 t2150
5350 T t2151 o1058 b2149 b4
5351 B b2152 t2151
5352 T t2152 o2141 b1057 b2152 b4 b4
5353 B b2153 t2152
5354 T t2153 o b2153 b4
5355 B b2154 t2153
5356 T t2154 o2143 b1057 b2151 b2154 b4
5357 B b2155 t2154
5358 T t2155 o b2155 b4
5359 B b2156 t2155
5360 T t2156 o b2143 b2156
5361 B b2157 t2156
5362 T t2157 o2060 b1057 b2141 b2157 b4
5363 B b2158 t2157
5364 P p2158 String "setSubstT << equal{'s1; 's2} >> 0 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 11 thenT autoT"
5365 O o2158 ext_rule p2158
5366 T t2158 o1058 b2054 b4
5367 B b2159 t2158
5368 T t2159 o2158 b1057 b2159 b4 b4
5369 B b2160 t2159
5370 T t2160 o b2160 b4
5371 B b2161 t2160
5372 T t2161 o b2158 b2161
5373 B b2162 t2161
5374 T t2162 o b2060 b2162
5375 B b2163 t2162
5376 T t2163 o2017 b1057 b2058 b2163 b4
5377 B b2164 t2163
5378 T t2164 o b2164 b4
5379 B b2165 t2164
5380 T t2165 o1985 b1057 b2017 b2165 b4
5381 B b2166 t2165
5382 P p2166 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 'e2; id{'g}}; 'e2} >> 3 thenT autoT"
5383 O o2166 ext_rule p2166
5384 T t2166 o1058 b1982 b4
5385 B b2167 t2166
5386 T t2167 o2166 b1057 b2167 b4 b4
5387 B b2168 t2167
5388 T t2168 o b2168 b4
5389 B b2169 t2168
5390 T t2169 o b2166 b2169
5391 B b2170 t2169
5392 T t2170 o1955 b1057 b1985 b2170 b4
5393 B b2171 t2170
5394 T t2171 o1055 b2171
5395 B b2172 t2171
5396 T t2172 o1939 b680 b1955 b2172 b4
5397 B b2173 t2172
5398 T t2173 o1938 b2173
5399 B b2174 t2173
5400 P p2174 Number 13452
5401 P p2175 Number 13824
5402 O o2175 location p2174 p2175
5403 P p2176 String unique_id2
5404 O o2176 rule p2176
5405 T t2176 o598 b582 b832 b1940
5406 B b2176 t2176
5407 T t2177 o727 b588 b593 b2176 b832
5408 B b2177 t2177 s
5409 T t2178 o1944 b588 b2177
5410 S s2178 t688 h
5411 G s2178 t2178
5412 B b2178 s2178
5413 T t2179 o681 b2178
5414 B b2179 t2179
5415 T t2180 o680 b2179 b1950
5416 B b2180 t2180
5417 T t2181 o680 b1944 b2180
5418 B b2181 t2181
5419 T t2182 o680 b727 b2181
5420 B b2182 t2182
5421 T t2183 o680 b686 b2182
5422 B b2183 t2183
5423 T t2184 o680 b1942 b2183
5424 B b2184 t2184
5425 P p2184 String "assumT 5 thenT withT << id{'g} >> (dT 2) ttca"
5426 O o2184 ext_rule p2184
5427 T t2185 o b2178 b4
5428 B b2185 t2185
5429 T t2186 o b1943 b2185
5430 B b2186 t2186
5431 T t2187 o b726 b2186
5432 B b2187 t2187
5433 T t2188 o b685 b2187
5434 B b2188 t2188
5435 T t2189 o b1941 b2188
5436 B b2189 t2189
5437 T t2190 o1060 b1949 b2189
5438 B b2190 t2190
5439 T t2191 o1059 b2190 b4 b1065
5440 B b2191 t2191
5441 H h2191 v t2178
5442 T t2192 o598 b582 b1964 b1940
5443 B b2192 t2192
5444 T t2193 o727 b588 b593 b2192 b1964
5445 B b2193 t2193 w
5446 T t2194 o1963 b2193
5447 S s2194 t688 h h2191
5448 G s2194 t2194
5449 B b2194 s2194
5450 T t2195 o1060 b2194 b2189
5451 B b2195 t2195
5452 S s2195 t688 h h2191
5453 G s2195 t1949
5454 B b2196 s2195
5455 T t2196 o1060 b2196 b2189
5456 B b2197 t2196
5457 T t2197 o2 b2191
5458 B b2198 t2197
5459 T t2198 o1059 b2197 b1974 b2198
5460 B b2199 t2198
5461 T t2199 o2 b2199
5462 B b2200 t2199
5463 T t2200 o1962 b2195 b4 b2200
5464 B b2201 t2200
5465 T t2201 o598 b582 b606 b1940
5466 B b2202 t2201
5467 T t2202 o727 b588 b593 b2202 b606
5468 H h2202 w t2202
5469 S s2202 t688 h h2191 h2202
5470 G s2202 t1949
5471 B b2203 s2202
5472 T t2203 o1060 b2203 b2189
5473 B b2204 t2203
5474 T t2204 o1059 b2204 b4 b2200
5475 B b2205 t2204
5476 T t2205 o b2205 b4
5477 B b2206 t2205
5478 T t2206 o b2201 b2206
5479 B b2207 t2206
5480 T t2207 o1058 b2191 b2207
5481 B b2208 t2207
5482 T t2208 o598 b582 b741 b1940
5483 B b2209 t2208
5484 T t2209 o727 b588 b593 b2209 b741
5485 H h2209 x_1 t2209
5486 T t2210 o598 b582 b744 b1940
5487 B b2210 t2210
5488 T t2211 o727 b588 b593 b2210 b744
5489 S s2211 t688 h h2191 h1985 h1986 h1987 h2209
5490 G s2211 t2211
5491 B b2211 s2211
5492 T t2212 o1060 b2211 b2189
5493 B b2212 t2212
5494 B b2213 t2209
5495 B b2214 t2211
5496 T t2214 o1115 b2213 b2214
5497 S s2214 t688 h h2191 h1985 h1986 h1987
5498 G s2214 t2214
5499 B b2215 s2214
5500 T t2215 o1060 b2215 b2189
5501 B b2216 t2215
5502 B b2217 t2214
5503 T t2217 o1115 b1996 b2217
5504 S s2217 t688 h h2191 h1985 h1986
5505 G s2217 t2217
5506 B b2218 s2217
5507 T t2218 o1060 b2218 b2189
5508 B b2219 t2218
5509 B b2220 t2217 s2
5510 T t2220 o1130 b1131 b2220
5511 S s2220 t688 h h2191 h1985
5512 G s2220 t2220
5513 B b2221 s2220
5514 T t2221 o1060 b2221 b2189
5515 B b2222 t2221
5516 B b2223 t2220 s1
5517 T t2223 o1130 b1131 b2223
5518 S s2223 t688 h h2191
5519 G s2223 t2223
5520 B b2224 s2223
5521 T t2224 o1060 b2224 b2189
5522 B b2225 t2224
5523 T t2225 o2 b2201
5524 B b2226 t2225
5525 T t2226 o1962 b2225 b1122 b2226
5526 B b2227 t2226
5527 T t2227 o2 b2227
5528 B b2228 t2227
5529 T t2228 o1059 b2222 b1122 b2228
5530 B b2229 t2228
5531 T t2229 o2 b2229
5532 B b2230 t2229
5533 T t2230 o1059 b2219 b1122 b2230
5534 B b2231 t2230
5535 T t2231 o2 b2231
5536 B b2232 t2231
5537 T t2232 o1059 b2216 b1122 b2232
5538 B b2233 t2232
5539 T t2233 o2 b2233
5540 B b2234 t2233
5541 T t2234 o1059 b2212 b4 b2234
5542 B b2235 t2234
5543 T t2235 o b2235 b4
5544 B b2236 t2235
5545 T t2236 o1058 b2201 b2236
5546 B b2237 t2236
5547 P p2237 String "equivTransT << 's1 >> thenT autoT thenT rwh unfold_equiv 6 ttca thenT rwh fold_equiv 6"
5548 O o2237 ext_rule p2237
5549 S s2237 t688 h h2191 h1985 h1986 h1987 h2209
5550 G s2237 t763
5551 B b2238 s2237
5552 T t2238 o1060 b2238 b2189
5553 B b2239 t2238
5554 T t2239 o704 b2209
5555 B b2240 t2239
5556 T t2240 o1153 b2240 b2019
5557 B b2241 t2240
5558 T t2241 o1153 b1155 b2241
5559 B b2242 t2241
5560 T t2242 o1153 b1154 b2242
5561 B b2243 t2242
5562 T t2243 o761 b2209 b588
5563 B b2244 t2243
5564 T t2244 o1153 b2244 b2024
5565 B b2245 t2244
5566 T t2245 o1153 b2243 b2245
5567 B b2246 t2245
5568 T t2246 o1164 b2209 b741
5569 B b2247 t2246
5570 T t2247 o761 b2247 b593
5571 B b2248 t2247
5572 T t2248 o1153 b2246 b2248
5573 H h2248 x_1 t2248
5574 S s2248 t688 h h2191 h1985 h1986 h1987 h2248
5575 G s2248 t763
5576 B b2249 s2248
5577 T t2249 o1060 b2249 b2189
5578 B b2250 t2249
5579 T t2250 o761 b2210 b588
5580 S s2250 t688 h h2191 h1985 h1986 h1987 h2209
5581 G s2250 t2250
5582 B b2251 s2250
5583 T t2251 o1060 b2251 b2189
5584 B b2252 t2251
5585 T t2252 o2 b2235
5586 B b2253 t2252
5587 T t2253 o1059 b2252 b1122 b2253
5588 B b2254 t2253
5589 T t2254 o2 b2254
5590 B b2255 t2254
5591 T t2255 o1059 b2239 b4 b2255
5592 B b2256 t2255
5593 T t2256 o2 b2256
5594 B b2257 t2256
5595 T t2257 o1059 b2250 b4 b2257
5596 B b2258 t2257
5597 T t2258 o2 b2258
5598 B b2259 t2258
5599 T t2259 o1059 b2239 b4 b2259
5600 B b2260 t2259
5601 T t2260 o727 b588 b593 b2210 b741
5602 S s2260 t688 h h2191 h1985 h1986 h1987 h2209
5603 G s2260 t2260
5604 B b2261 s2260
5605 T t2261 o1060 b2261 b2189
5606 B b2262 t2261
5607 S s2262 t688 h h2191 h1985 h1986 h1987 h2248
5608 G s2262 t2260
5609 B b2263 s2262
5610 T t2263 o1060 b2263 b2189
5611 B b2264 t2263
5612 T t2264 o1059 b2262 b4 b2253
5613 B b2265 t2264
5614 T t2265 o2 b2265
5615 B b2266 t2265
5616 T t2266 o1059 b2264 b4 b2266
5617 B b2267 t2266
5618 T t2267 o2 b2267
5619 B b2268 t2267
5620 T t2268 o1059 b2262 b4 b2268
5621 B b2269 t2268
5622 S s2269 t688 h h2191 h1985 h1986 h1987 h2209
5623 G s2269 t787
5624 B b2270 s2269
5625 T t2270 o1060 b2270 b2189
5626 B b2271 t2270
5627 S s2271 t688 h h2191 h1985 h1986 h1987 h2248
5628 G s2271 t787
5629 B b2272 s2271
5630 T t2272 o1060 b2272 b2189
5631 B b2273 t2272
5632 T t2273 o1059 b2271 b4 b2253
5633 B b2274 t2273
5634 T t2274 o2 b2274
5635 B b2275 t2274
5636 T t2275 o1059 b2273 b4 b2275
5637 B b2276 t2275
5638 T t2276 o2 b2276
5639 B b2277 t2276
5640 T t2277 o1059 b2271 b4 b2277
5641 B b2278 t2277
5642 T t2278 o b2278 b4
5643 B b2279 t2278
5644 T t2279 o b2269 b2279
5645 B b2280 t2279
5646 T t2280 o b2260 b2280
5647 B b2281 t2280
5648 T t2281 o1058 b2235 b2281
5649 B b2282 t2281
5650 P p2282 String "rwh unfold_equiv 6 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 11 thenT autoT"
5651 O o2282 ext_rule p2282
5652 T t2282 o1058 b2260 b4
5653 B b2283 t2282
5654 T t2283 o2282 b1057 b2283 b4 b4
5655 B b2284 t2283
5656 P p2284 String "equivTransT << op{'g; 's1; 'e2} >> thenT autoT thenT rwh unfold_equiv 6 thenT autoT"
5657 O o2284 ext_rule p2284
5658 H h2284 y_3 t2239
5659 H h2285 y t2243
5660 H h2286 z t2247
5661 S s2286 t688 h h2191 h1985 h1986 h1987 h2060 h2061 h2284 h2063 h2285 h2065 h2286
5662 G s2286 t763
5663 B b2286 s2286
5664 T t2286 o1060 b2286 b2189
5665 B b2287 t2286
5666 H h2287 z_3 t2240
5667 S s2287 t688 h h2191 h1985 h1986 h1987 h2060 h2061 h2287 h2285 h2065 h2286
5668 G s2287 t763
5669 B b2288 s2287
5670 T t2288 o1060 b2288 b2189
5671 B b2289 t2288
5672 H h2289 z_1 t2241
5673 S s2289 t688 h h2191 h1985 h1986 h1987 h2060 h2289 h2285 h2065 h2286
5674 G s2289 t763
5675 B b2290 s2289
5676 T t2290 o1060 b2290 b2189
5677 B b2291 t2290
5678 H h2291 y_1 t2242
5679 S s2291 t688 h h2191 h1985 h1986 h1987 h2291 h2285 h2065 h2286
5680 G s2291 t763
5681 B b2292 s2291
5682 T t2292 o1060 b2292 b2189
5683 B b2293 t2292
5684 H h2293 z_1 t2244
5685 S s2293 t688 h h2191 h1985 h1986 h1987 h2291 h2293 h2286
5686 G s2293 t763
5687 B b2294 s2293
5688 T t2294 o1060 b2294 b2189
5689 B b2295 t2294
5690 H h2295 y t2245
5691 S s2295 t688 h h2191 h1985 h1986 h1987 h2295 h2286
5692 G s2295 t763
5693 B b2296 s2295
5694 T t2296 o1060 b2296 b2189
5695 B b2297 t2296
5696 T t2297 o2 b2269
5697 B b2298 t2297
5698 T t2298 o1059 b2252 b1122 b2298
5699 B b2299 t2298
5700 T t2299 o2 b2299
5701 B b2300 t2299
5702 T t2300 o1059 b2239 b4 b2300
5703 B b2301 t2300
5704 T t2301 o2 b2301
5705 B b2302 t2301
5706 T t2302 o1059 b2250 b4 b2302
5707 B b2303 t2302
5708 T t2303 o2 b2303
5709 B b2304 t2303
5710 T t2304 o1059 b2297 b4 b2304
5711 B b2305 t2304
5712 T t2305 o2 b2305
5713 B b2306 t2305
5714 T t2306 o1059 b2295 b4 b2306
5715 B b2307 t2306
5716 T t2307 o2 b2307
5717 B b2308 t2307
5718 T t2308 o1059 b2293 b4 b2308
5719 B b2309 t2308
5720 T t2309 o2 b2309
5721 B b2310 t2309
5722 T t2310 o1059 b2291 b4 b2310
5723 B b2311 t2310
5724 T t2311 o2 b2311
5725 B b2312 t2311
5726 T t2312 o1059 b2289 b4 b2312
5727 B b2313 t2312
5728 T t2313 o2 b2313
5729 B b2314 t2313
5730 T t2314 o1059 b2287 b4 b2314
5731 B b2315 t2314
5732 S s2315 t688 h h2191 h1985 h1986 h1987 h2060 h2061 h2284 h2063 h2285 h2065 h2286
5733 G s2315 t2099
5734 B b2316 s2315
5735 T t2316 o1060 b2316 b2189
5736 B b2317 t2316
5737 S s2317 t688 h h2191 h1985 h1986 h1987 h2060 h2061 h2287 h2285 h2065 h2286
5738 G s2317 t2099
5739 B b2318 s2317
5740 T t2318 o1060 b2318 b2189
5741 B b2319 t2318
5742 S s2319 t688 h h2191 h1985 h1986 h1987 h2060 h2289 h2285 h2065 h2286
5743 G s2319 t2099
5744 B b2320 s2319
5745 T t2320 o1060 b2320 b2189
5746 B b2321 t2320
5747 S s2321 t688 h h2191 h1985 h1986 h1987 h2291 h2285 h2065 h2286
5748 G s2321 t2099
5749 B b2322 s2321
5750 T t2322 o1060 b2322 b2189
5751 B b2323 t2322
5752 S s2323 t688 h h2191 h1985 h1986 h1987 h2291 h2293 h2286
5753 G s2323 t2099
5754 B b2324 s2323
5755 T t2324 o1060 b2324 b2189
5756 B b2325 t2324
5757 S s2325 t688 h h2191 h1985 h1986 h1987 h2295 h2286
5758 G s2325 t2099
5759 B b2326 s2325
5760 T t2326 o1060 b2326 b2189
5761 B b2327 t2326
5762 S s2327 t688 h h2191 h1985 h1986 h1987 h2248
5763 G s2327 t2099
5764 B b2328 s2327
5765 T t2328 o1060 b2328 b2189
5766 B b2329 t2328
5767 S s2329 t688 h h2191 h1985 h1986 h1987 h2209
5768 G s2329 t2099
5769 B b2330 s2329
5770 T t2330 o1060 b2330 b2189
5771 B b2331 t2330
5772 T t2331 o727 b588 b593 b2210 b2209
5773 S s2331 t688 h h2191 h1985 h1986 h1987 h2209
5774 G s2331 t2331
5775 B b2332 s2331
5776 T t2332 o1060 b2332 b2189
5777 B b2333 t2332
5778 T t2333 o1059 b2333 b1122 b2298
5779 B b2334 t2333
5780 T t2334 o2 b2334
5781 B b2335 t2334
5782 T t2335 o1059 b2331 b4 b2335
5783 B b2336 t2335
5784 T t2336 o2 b2336
5785 B b2337 t2336
5786 T t2337 o1059 b2329 b4 b2337
5787 B b2338 t2337
5788 T t2338 o2 b2338
5789 B b2339 t2338
5790 T t2339 o1059 b2327 b4 b2339
5791 B b2340 t2339
5792 T t2340 o2 b2340
5793 B b2341 t2340
5794 T t2341 o1059 b2325 b4 b2341
5795 B b2342 t2341
5796 T t2342 o2 b2342
5797 B b2343 t2342
5798 T t2343 o1059 b2323 b4 b2343
5799 B b2344 t2343
5800 T t2344 o2 b2344
5801 B b2345 t2344
5802 T t2345 o1059 b2321 b4 b2345
5803 B b2346 t2345
5804 T t2346 o2 b2346
5805 B b2347 t2346
5806 T t2347 o1059 b2319 b4 b2347
5807 B b2348 t2347
5808 T t2348 o2 b2348
5809 B b2349 t2348
5810 T t2349 o1059 b2317 b4 b2349
5811 B b2350 t2349
5812 T t2350 o b2350 b4
5813 B b2351 t2350
5814 T t2351 o b2315 b2351
5815 B b2352 t2351
5816 T t2352 o1058 b2269 b2352
5817 B b2353 t2352
5818 T t2353 o1058 b2315 b4
5819 B b2354 t2353
5820 T t2354 o2141 b1057 b2354 b4 b4
5821 B b2355 t2354
5822 T t2355 o1058 b2350 b4
5823 B b2356 t2355
5824 T t2356 o2158 b1057 b2356 b4 b4
5825 B b2357 t2356
5826 T t2357 o b2357 b4
5827 B b2358 t2357
5828 T t2358 o b2355 b2358
5829 B b2359 t2358
5830 T t2359 o2284 b1057 b2353 b2359 b4
5831 B b2360 t2359
5832 P p2360 String "setSubstT << equal{'s1; 's2} >> 0 thenT autoT thenT rwh unfold_equiv 6 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 11 thenT autoT"
5833 O o2360 ext_rule p2360
5834 T t2360 o1058 b2278 b4
5835 B b2361 t2360
5836 T t2361 o2360 b1057 b2361 b4 b4
5837 B b2362 t2361
5838 T t2362 o b2362 b4
5839 B b2363 t2362
5840 T t2363 o b2360 b2363
5841 B b2364 t2363
5842 T t2364 o b2284 b2364
5843 B b2365 t2364
5844 T t2365 o2237 b1057 b2282 b2365 b4
5845 B b2366 t2365
5846 T t2366 o b2366 b4
5847 B b2367 t2366
5848 T t2367 o1985 b1057 b2237 b2367 b4
5849 B b2368 t2367
5850 P p2368 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 'e2}; 'e2} >> 3 ttca"
5851 O o2368 ext_rule p2368
5852 T t2368 o1058 b2205 b4
5853 B b2369 t2368
5854 T t2369 o2368 b1057 b2369 b4 b4
5855 B b2370 t2369
5856 T t2370 o b2370 b4
5857 B b2371 t2370
5858 T t2371 o b2368 b2371
5859 B b2372 t2371
5860 P p2372 String "withT << 'a >> (dT 2) thenT autoT"
5861 O o2372 ext_rule p2372
5862 H h2372 b t1160
5863 T t2372 o598 b582 b1940 b599
5864 B b2373 t2372
5865 T t2373 o727 b588 b593 b2373 b599
5866 S s2373 t688 h h2191 h2202 h1108 h2372
5867 G s2373 t2373
5868 B b2374 s2373
5869 T t2374 o1060 b2374 b2189
5870 B b2375 t2374
5871 S s2375 t688 h h2191 h2202
5872 G s2375 t1947
5873 B b2376 s2375
5874 T t2376 o1060 b2376 b2189
5875 B b2377 t2376
5876 T t2377 o1059 b2204 b1122 b2200
5877 B b2378 t2377
5878 T t2378 o2 b2378
5879 B b2379 t2378
5880 T t2379 o1059 b2377 b1122 b2379
5881 B b2380 t2379
5882 T t2380 o2 b2380
5883 B b2381 t2380
5884 T t2381 o1059 b2375 b4 b2381
5885 B b2382 t2381
5886 P p2382 Var w_1
5887 O o2382 var p2382
5888 T t2382 o2382
5889 B b2383 t2382
5890 T t2383 o598 b582 b2383 b1940
5891 B b2384 t2383
5892 T t2384 o727 b588 b593 b2384 b2383
5893 B b2385 t2384 w_1
5894 T t2385 o1963 b2385
5895 S s2385 t688 h h2191 h2202 h1108 h2372
5896 G s2385 t2385
5897 B b2386 s2385
5898 T t2386 o1060 b2386 b2189
5899 B b2387 t2386
5900 T t2387 o b599 b4
5901 B b2388 t2387
5902 T t2388 o1971 b2388
5903 B b2389 t2388
5904 T t2389 o1970 b2389
5905 B b2390 t2389
5906 T t2390 o b2390 b4
5907 B b2391 t2390
5908 T t2391 o1059 b2375 b2391 b2381
5909 B b2392 t2391
5910 T t2392 o2 b2392
5911 B b2393 t2392
5912 T t2393 o1962 b2387 b4 b2393
5913 B b2394 t2393
5914 T t2394 o598 b582 b599 b1940
5915 B b2395 t2394
5916 T t2395 o727 b588 b593 b2395 b599
5917 H h2395 w_1 t2395
5918 S s2395 t688 h h2191 h2202 h1108 h2372 h2395
5919 G s2395 t2373
5920 B b2396 s2395
5921 T t2396 o1060 b2396 b2189
5922 B b2397 t2396
5923 T t2397 o1059 b2397 b4 b2393
5924 B b2398 t2397
5925 T t2398 o b2398 b4
5926 B b2399 t2398
5927 T t2399 o b2394 b2399
5928 B b2400 t2399
5929 T t2400 o1058 b2382 b2400
5930 B b2401 t2400
5931 NSummary!ext_goal ext_goal ext_goal Summary
5932 O o2401 ext_goal
5933 T t2401 o2401 b2394
5934 B b2402 t2401
5935 T t2402 o2401 b2398
5936 B b2403 t2402
5937 T t2403 o b2403 b4
5938 B b2404 t2403
5939 T t2404 o b2402 b2404
5940 B b2405 t2404
5941 T t2405 o2372 b1057 b2401 b2405 b4
5942 B b2406 t2405
5943 T t2406 o b2406 b4
5944 B b2407 t2406
5945 T t2407 o2184 b1057 b2208 b2372 b2407
5946 B b2408 t2407
5947 T t2408 o1055 b2408
5948 B b2409 t2408
5949 T t2409 o2176 b680 b2184 b2409 b4
5950 B b2410 t2409
5951 T t2410 o2175 b2410
5952 B b2411 t2410
5953 O o2411 location p p
5954 P p2411 String unique_inv1
5955 O o2412 rule p2411
5956 T t2412 o598 b582 b744 b832
5957 B b2412 t2412
5958 T t2413 o727 b588 b593 b2412 b606
5959 S s2413 t688 h
5960 G s2413 t2413
5961 B b2413 s2413
5962 T t2414 o681 b2413
5963 B b2414 t2414
5964 T t2415 o727 b588 b593 b744 b1085
5965 S s2415 t688 h
5966 G s2415 t2415
5967 B b2415 s2415
5968 T t2416 o681 b2415
5969 B b2416 t2416
5970 T t2417 o680 b2414 b2416
5971 B b2417 t2417
5972 T t2418 o680 b764 b2417
5973 B b2418 t2418
5974 T t2419 o680 b952 b2418
5975 B b2419 t2419
5976 T t2420 o680 b727 b2419
5977 B b2420 t2420
5978 T t2421 o680 b686 b2420
5979 B b2421 t2421
5980 T t2422 o680 b746 b2421
5981 B b2422 t2422
5982 T t2423 o680 b834 b2422
5983 B b2423 t2423
5984 P p2423 String "assumT 7 thenT equivSubstT << equiv{car{'g}; eqG{'g}; id{'g}; op{'g; inv{'g; 's}; 's}}>> 2 ttca"
5985 O o2423 ext_rule p2423
5986 T t2424 o b2413 b4
5987 B b2424 t2424
5988 T t2425 o b763 b2424
5989 B b2425 t2425
5990 T t2426 o b951 b2425
5991 B b2426 t2426
5992 T t2427 o b726 b2426
5993 B b2427 t2427
5994 T t2428 o b685 b2427
5995 B b2428 t2428
5996 T t2429 o b745 b2428
5997 B b2429 t2429
5998 T t2430 o b833 b2429
5999 B b2430 t2430
6000 T t2431 o1060 b2415 b2430
6001 B b2431 t2431
6002 T t2432 o1059 b2431 b4 b1065
6003 B b2432 t2432
6004 H h2432 v t2413
6005 S s2432 t688 h h2432
6006 G s2432 t1086
6007 B b2433 s2432
6008 T t2433 o1060 b2433 b2430
6009 B b2434 t2433
6010 S s2434 t688 h h2432
6011 G s2434 t2415
6012 B b2435 s2434
6013 T t2435 o1060 b2435 b2430
6014 B b2436 t2435
6015 T t2436 o2 b2432
6016 B b2437 t2436
6017 T t2437 o1059 b2436 b4 b2437
6018 B b2438 t2437
6019 T t2438 o2 b2438
6020 B b2439 t2438
6021 T t2439 o1059 b2434 b4 b2439
6022 B b2440 t2439
6023 T t2440 o727 b588 b593 b2412 b1086
6024 H h2440 z t2440
6025 S s2440 t688 h h2432 h2440
6026 G s2440 t2415
6027 B b2441 s2440
6028 T t2441 o1060 b2441 b2430
6029 B b2442 t2441
6030 T t2442 o1059 b2442 b4 b2439
6031 B b2443 t2442
6032 T t2443 o b2443 b4
6033 B b2444 t2443
6034 T t2444 o b2440 b2444
6035 B b2445 t2444
6036 T t2445 o1058 b2432 b2445
6037 B b2446 t2445
6038 P p2446 String "assertT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's}; 's}; id{'g}} >> ttca thenT equivSymT ttca"
6039 O o2446 ext_rule p2446
6040 T t2446 o1058 b2440 b4
6041 B b2447 t2446
6042 T t2447 o2446 b1057 b2447 b4 b4
6043 B b2448 t2447
6044 P p2448 String "groupCancelRightT 3 ttca"
6045 O o2448 ext_rule p2448
6046 T t2448 o1058 b2443 b4
6047 B b2449 t2448
6048 T t2449 o2448 b1057 b2449 b4 b4
6049 B b2450 t2449
6050 T t2450 o b2450 b4
6051 B b2451 t2450
6052 T t2451 o b2448 b2451
6053 B b2452 t2451
6054 T t2452 o2423 b1057 b2446 b2452 b4
6055 B b2453 t2452
6056 T t2453 o1055 b2453
6057 B b2454 t2453
6058 P p2454 Number 13853
6059 P p2455 Number 13861
6060 O o2455 resource_defs p2454 p2455 p204
6061 P p2456 Number 13859
6062 O o2456 uid p2456 p2455
6063 T t2456 o2456 b695
6064 B b2456 t2456
6065 T t2457 o b2456 b4
6066 B b2457 t2457
6067 T t2458 o2455 b2457
6068 B b2458 t2458
6069 T t2459 o b2458 b4
6070 B b2459 t2459
6071 T t2460 o2412 b680 b2423 b2454 b2459
6072 B b2460 t2460
6073 T t2461 o2411 b2460
6074 B b2461 t2461
6075 P p2461 String unique_inv2
60