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

1 #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 45
809 O o299 location p298 p299
810 P p300 String Czf_itt_set
811 O o300 parent p300
812 T t300 o300
813 B b300 t300
814 T t301 o b300 b4
815 B b301 t301
816 P p301 String Czf_itt_comment
817 O o301 parent p301
818 T t302 o301
819 B b302 t302
820 T t303 o b302 b4
821 B b303 t303
822 P p303 String Itt_theory
823 O o303 parent p303
824 T t304 o303
825 B b304 t304
826 T t305 o b304 b4
827 B b305 t305
828 P p305 String Itt_fset
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_prop_decide
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_derive
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_list2
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_list
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_quotient
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_esquash
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_srec
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_prec
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_w
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_bunion
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_bisect
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_tunion
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_isect
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_struct2
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_well_founded
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_int_arith
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_atom_bool
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_atom
937 O o341 parent p341
938 T t342 o341
939 B b342 t342
940 T t343 o b342 b4
941 B b343 t343
942 T t344 o b343 b4
943 B b344 t344
944 T t345 o b341 b344
945 B b345 t345
946 T t346 o b339 b345
947 B b346 t346
948 T t347 o b337 b346
949 B b347 t347
950 T t348 o b335 b347
951 B b348 t348
952 T t349 o b333 b348
953 B b349 t349
954 T t350 o b331 b349
955 B b350 t350
956 T t351 o b329 b350
957 B b351 t351
958 T t352 o b327 b351
959 B b352 t352
960 T t353 o b325 b352
961 B b353 t353
962 T t354 o b323 b353
963 B b354 t354
964 T t355 o b321 b354
965 B b355 t355
966 T t356 o b319 b355
967 B b356 t356
968 T t357 o b317 b356
969 B b357 t357
970 T t358 o b315 b357
971 B b358 t358
972 T t359 o b313 b358
973 B b359 t359
974 T t360 o b311 b359
975 B b360 t360
976 T t361 o b309 b360
977 B b361 t361
978 T t362 o b307 b361
979 B b362 t362
980 T t363 o b305 b362
981 B b363 t363
982 T t364 o b303 b363
983 B b364 t364
984 T t365 o b301 b364
985 B b365 t365
986 T t366 o2 b301 b365 b296
987 B b366 t366
988 T t367 o299 b366
989 B b367 t367
990 P p367 Number 46
991 P p368 Number 68
992 O o368 location p367 p368
993 P p369 String Czf_itt_member
994 O o369 parent p369
995 T t369 o369
996 B b369 t369
997 T t370 o b369 b4
998 B b370 t370
999 P p370 String Czf_itt_eq
1000 O o370 parent p370
1001 T t371 o370
1002 B b371 t371
1003 T t372 o b371 b4
1004 B b372 t372
1005 T t373 o b372 b4
1006 B b373 t373
1007 T t374 o b370 b373
1008 B b374 t374
1009 T t375 o2 b370 b374 b296
1010 B b375 t375
1011 T t376 o368 b375
1012 B b376 t376
1013 P p376 Number 69
1014 P p377 Number 87
1015 O o377 location p376 p377
1016 T t377 o2 b372 b4 b296
1017 B b377 t377
1018 T t378 o377 b377
1019 B b378 t378
1020 P p378 Number 88
1021 P p379 Number 108
1022 O o379 location p378 p379
1023 P p380 String Czf_itt_dall
1024 O o380 parent p380
1025 T t380 o380
1026 B b380 t380
1027 T t381 o b380 b4
1028 B b381 t381
1029 P p381 String Czf_itt_set_ind
1030 O o381 parent p381
1031 T t382 o381
1032 B b382 t382
1033 T t383 o b382 b4
1034 B b383 t383
1035 P p383 String Czf_itt_all
1036 O o383 parent p383
1037 T t384 o383
1038 B b384 t384
1039 T t385 o b384 b4
1040 B b385 t385
1041 P p385 String Czf_itt_sep
1042 O o385 parent p385
1043 T t386 o385
1044 B b386 t386
1045 T t387 o b386 b4
1046 B b387 t387
1047 T t388 o b387 b4
1048 B b388 t388
1049 T t389 o b385 b388
1050 B b389 t389
1051 T t390 o b383 b389
1052 B b390 t390
1053 T t391 o b381 b390
1054 B b391 t391
1055 T t392 o2 b381 b391 b296
1056 B b392 t392
1057 T t393 o379 b392
1058 B b393 t393
1059 P p393 Number 109
1060 P p394 Number 128
1061 O o394 location p393 p394
1062 P p395 String Czf_itt_and
1063 O o395 parent p395
1064 T t395 o395
1065 B b395 t395
1066 T t396 o b395 b4
1067 B b396 t396
1068 T t397 o b396 b4
1069 B b397 t397
1070 T t398 o2 b396 b397 b296
1071 B b398 t398
1072 T t399 o394 b398
1073 B b399 t399
1074 P p399 Number 129
1075 P p400 Number 150
1076 O o400 location p399 p400
1077 P p401 String Czf_itt_equiv
1078 O o401 parent p401
1079 T t401 o401
1080 B b401 t401
1081 T t402 o b401 b4
1082 B b402 t402
1083 P p402 String Czf_itt_pair
1084 O o402 parent p402
1085 T t403 o402
1086 B b403 t403
1087 T t404 o b403 b4
1088 B b404 t404
1089 P p404 String Czf_itt_singleton
1090 O o404 parent p404
1091 T t405 o404
1092 B b405 t405
1093 T t406 o b405 b4
1094 B b406 t406
1095 P p406 String Czf_itt_union
1096 O o406 parent p406
1097 T t407 o406
1098 B b407 t407
1099 T t408 o b407 b4
1100 B b408 t408
1101 P p408 String Czf_itt_subset
1102 O o408 parent p408
1103 T t409 o408
1104 B b409 t409
1105 T t410 o b409 b4
1106 B b410 t410
1107 P p410 String Czf_itt_dexists
1108 O o410 parent p410
1109 T t411 o410
1110 B b411 t411
1111 T t412 o b411 b4
1112 B b412 t412
1113 T t413 o b412 b4
1114 B b413 t413
1115 T t414 o b410 b413
1116 B b414 t414
1117 T t415 o b408 b414
1118 B b415 t415
1119 T t416 o b406 b415
1120 B b416 t416
1121 T t417 o b404 b416
1122 B b417 t417
1123 T t418 o b402 b417
1124 B b418 t418
1125 T t419 o2 b402 b418 b296
1126 B b419 t419
1127 T t420 o400 b419
1128 B b420 t420
1129 P p420 Number 152
1130 P p421 Number 163
1131 O o421 location p420 p421
1132 NSummary!summary_item summary_item summary_item Summary
1133 O o422 summary_item
1134 NOcaml!str_open str_open str_open Ocaml
1135 O o423 str_open p420 p421
1136 NOcaml!string string string Ocaml
1137 P p423 String Printf
1138 O o424 string p423
1139 T t424 o424
1140 B b424 t424
1141 T t425 o b424 b4
1142 B b425 t425
1143 T t426 o423 b425
1144 B b426 t426
1145 T t427 o422 b426
1146 B b427 t427
1147 T t428 o421 b427
1148 B b428 t428
1149 P p428 Number 164
1150 P p429 Number 177
1151 O o429 location p428 p429
1152 O o430 str_open p428 p429
1153 P p430 String Mp_debug
1154 O o431 string p430
1155 T t431 o431
1156 B b431 t431
1157 T t432 o b431 b4
1158 B b432 t432
1159 T t433 o430 b432
1160 B b433 t433
1161 T t434 o422 b433
1162 B b434 t434
1163 T t435 o429 b434
1164 B b435 t435
1165 P p435 Number 178
1166 P p436 Number 207
1167 O o436 location p435 p436
1168 O o437 str_open p435 p436
1169 P p437 String Refiner
1170 O o438 string p437
1171 T t438 o438
1172 B b438 t438
1173 P p438 String TermType
1174 O o439 string p438
1175 T t439 o439
1176 B b439 t439
1177 T t440 o b439 b4
1178 B b440 t440
1179 T t441 o b438 b440
1180 B b441 t441
1181 T t442 o b438 b441
1182 B b442 t442
1183 T t443 o437 b442
1184 B b443 t443
1185 T t444 o422 b443
1186 B b444 t444
1187 T t445 o436 b444
1188 B b445 t445
1189 P p445 Number 208
1190 P p446 Number 233
1191 O o446 location p445 p446
1192 O o447 str_open p445 p446
1193 P p447 String Term
1194 O o448 string p447
1195 T t448 o448
1196 B b448 t448
1197 T t449 o b448 b4
1198 B b449 t449
1199 T t450 o b438 b449
1200 B b450 t450
1201 T t451 o b438 b450
1202 B b451 t451
1203 T t452 o447 b451
1204 B b452 t452
1205 T t453 o422 b452
1206 B b453 t453
1207 T t454 o446 b453
1208 B b454 t454
1209 P p454 Number 234
1210 P p455 Number 261
1211 O o455 location p454 p455
1212 O o456 str_open p454 p455
1213 P p456 String TermOp
1214 O o457 string p456
1215 T t457 o457
1216 B b457 t457
1217 T t458 o b457 b4
1218 B b458 t458
1219 T t459 o b438 b458
1220 B b459 t459
1221 T t460 o b438 b459
1222 B b460 t460
1223 T t461 o456 b460
1224 B b461 t461
1225 T t462 o422 b461
1226 B b462 t462
1227 T t463 o455 b462
1228 B b463 t463
1229 P p463 Number 262
1230 P p464 Number 291
1231 O o464 location p463 p464
1232 O o465 str_open p463 p464
1233 P p465 String TermAddr
1234 O o466 string p465
1235 T t466 o466
1236 B b466 t466
1237 T t467 o b466 b4
1238 B b467 t467
1239 T t468 o b438 b467
1240 B b468 t468
1241 T t469 o b438 b468
1242 B b469 t469
1243 T t470 o465 b469
1244 B b470 t470
1245 T t471 o422 b470
1246 B b471 t471
1247 T t472 o464 b471
1248 B b472 t472
1249 P p472 Number 292
1250 P p473 Number 320
1251 O o473 location p472 p473
1252 O o474 str_open p472 p473
1253 P p474 String TermMan
1254 O o475 string p474
1255 T t475 o475
1256 B b475 t475
1257 T t476 o b475 b4
1258 B b476 t476
1259 T t477 o b438 b476
1260 B b477 t477
1261 T t478 o b438 b477
1262 B b478 t478
1263 T t479 o474 b478
1264 B b479 t479
1265 T t480 o422 b479
1266 B b480 t480
1267 T t481 o473 b480
1268 B b481 t481
1269 P p481 Number 321
1270 P p482 Number 351
1271 O o482 location p481 p482
1272 O o483 str_open p481 p482
1273 P p483 String TermSubst
1274 O o484 string p483
1275 T t484 o484
1276 B b484 t484
1277 T t485 o b484 b4
1278 B b485 t485
1279 T t486 o b438 b485
1280 B b486 t486
1281 T t487 o b438 b486
1282 B b487 t487
1283 T t488 o483 b487
1284 B b488 t488
1285 T t489 o422 b488
1286 B b489 t489
1287 T t490 o482 b489
1288 B b490 t490
1289 P p490 Number 352
1290 P p491 Number 379
1291 O o491 location p490 p491
1292 O o492 str_open p490 p491
1293 P p492 String Refine
1294 O o493 string p492
1295 T t493 o493
1296 B b493 t493
1297 T t494 o b493 b4
1298 B b494 t494
1299 T t495 o b438 b494
1300 B b495 t495
1301 T t496 o b438 b495
1302 B b496 t496
1303 T t497 o492 b496
1304 B b497 t497
1305 T t498 o422 b497
1306 B b498 t498
1307 T t499 o491 b498
1308 B b499 t499
1309 P p499 Number 380
1310 P p500 Number 412
1311 O o500 location p499 p500
1312 O o501 str_open p499 p500
1313 P p501 String RefineError
1314 O o502 string p501
1315 T t502 o502
1316 B b502 t502
1317 T t503 o b502 b4
1318 B b503 t503
1319 T t504 o b438 b503
1320 B b504 t504
1321 T t505 o b438 b504
1322 B b505 t505
1323 T t506 o501 b505
1324 B b506 t506
1325 T t507 o422 b506
1326 B b507 t507
1327 T t508 o500 b507
1328 B b508 t508
1329 P p508 Number 413
1330 P p509 Number 429
1331 O o509 location p508 p509
1332 O o510 str_open p508 p509
1333 P p510 String Mp_resource
1334 O o511 string p510
1335 T t511 o511
1336 B b511 t511
1337 T t512 o b511 b4
1338 B b512 t512
1339 T t513 o510 b512
1340 B b513 t513
1341 T t514 o422 b513
1342 B b514 t514
1343 T t515 o509 b514
1344 B b515 t515
1345 P p515 Number 430
1346 P p516 Number 447
1347 O o516 location p515 p516
1348 O o517 str_open p515 p516
1349 P p517 String Simple_print
1350 O o518 string p517
1351 T t518 o518
1352 B b518 t518
1353 T t519 o b518 b4
1354 B b519 t519
1355 T t520 o517 b519
1356 B b520 t520
1357 T t521 o422 b520
1358 B b521 t521
1359 T t522 o516 b521
1360 B b522 t522
1361 P p522 Number 449
1362 P p523 Number 465
1363 O o523 location p522 p523
1364 O o524 str_open p522 p523
1365 P p524 String Tactic_type
1366 O o525 string p524
1367 T t525 o525
1368 B b525 t525
1369 T t526 o b525 b4
1370 B b526 t526
1371 T t527 o524 b526
1372 B b527 t527
1373 T t528 o422 b527
1374 B b528 t528
1375 T t529 o523 b528
1376 B b529 t529
1377 P p529 Number 466
1378 P p530 Number 492
1379 O o530 location p529 p530
1380 O o531 str_open p529 p530
1381 P p531 String Tacticals
1382 O o532 string p531
1383 T t532 o532
1384 B b532 t532
1385 T t533 o b532 b4
1386 B b533 t533
1387 T t534 o b525 b533
1388 B b534 t534
1389 T t535 o531 b534
1390 B b535 t535
1391 T t536 o422 b535
1392 B b536 t536
1393 T t537 o530 b536
1394 B b537 t537
1395 P p537 Number 493
1396 P p538 Number 517
1397 O o538 location p537 p538
1398 O o539 str_open p537 p538
1399 P p539 String Sequent
1400 O o540 string p539
1401 T t540 o540
1402 B b540 t540
1403 T t541 o b540 b4
1404 B b541 t541
1405 T t542 o b525 b541
1406 B b542 t542
1407 T t543 o539 b542
1408 B b543 t543
1409 T t544 o422 b543
1410 B b544 t544
1411 T t545 o538 b544
1412 B b545 t545
1413 P p545 Number 518
1414 P p546 Number 548
1415 O o546 location p545 p546
1416 O o547 str_open p545 p546
1417 P p547 String Conversionals
1418 O o548 string p547
1419 T t548 o548
1420 B b548 t548
1421 T t549 o b548 b4
1422 B b549 t549
1423 T t550 o b525 b549
1424 B b550 t550
1425 T t551 o547 b550
1426 B b551 t551
1427 T t552 o422 b551
1428 B b552 t552
1429 T t553 o546 b552
1430 B b553 t553
1431 P p553 Number 549
1432 P p554 Number 559
1433 O o554 location p553 p554
1434 O o555 str_open p553 p554
1435 O o556 string p91
1436 T t556 o556
1437 B b556 t556
1438 T t557 o b556 b4
1439 B b557 t557
1440 T t558 o555 b557
1441 B b558 t558
1442 T t559 o422 b558
1443 B b559 t559
1444 T t560 o554 b559
1445 B b560 t560
1446 P p560 Number 560
1447 P p561 Number 568
1448 O o561 location p560 p561
1449 O o562 str_open p560 p561
1450 O o563 string p89
1451 T t563 o563
1452 B b563 t563
1453 T t564 o b563 b4
1454 B b564 t564
1455 T t565 o562 b564
1456 B b565 t565
1457 T t566 o422 b565
1458 B b566 t566
1459 T t567 o561 b566
1460 B b567 t567
1461 P p567 Number 570
1462 P p568 Number 587
1463 O o568 location p567 p568
1464 O o569 str_open p567 p568
1465 O o570 string p79
1466 T t570 o570
1467 B b570 t570
1468 T t571 o b570 b4
1469 B b571 t571
1470 T t572 o569 b571
1471 B b572 t572
1472 T t573 o422 b572
1473 B b573 t573
1474 T t574 o568 b573
1475 B b574 t574
1476 P p574 Number 588
1477 P p575 Number 609
1478 O o575 location p574 p575
1479 O o576 str_open p574 p575
1480 O o577 string p81
1481 T t577 o577
1482 B b577 t577
1483 T t578 o b577 b4
1484 B b578 t578
1485 T t579 o576 b578
1486 B b579 t579
1487 T t580 o422 b579
1488 B b580 t580
1489 T t581 o575 b580
1490 B b581 t581
1491 P p581 Number 611
1492 P p582 Number 628
1493 O o582 location p581 p582
1494 NSummary!opname opname opname Summary
1495 P p583 String group
1496 O o583 opname p583
1497 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1498 NCzf_itt_group!group group group Czf_itt_group
1499 O o584 group
1500 Nvar var var NIL
1501 P p584 Var g
1502 O o585 var p584
1503 T t585 o585
1504 B b585 t585
1505 T t586 o584 b585
1506 B b586 t586
1507 T t587 o583 b586
1508 B b587 t587
1509 T t588 o582 b587
1510 B b588 t588
1511 P p588 Number 629
1512 P p589 Number 644
1513 O o589 location p588 p589
1514 P p590 String car
1515 O o590 opname p590
1516 NCzf_itt_group!car car car Czf_itt_group
1517 O o591 car
1518 T t591 o591 b585
1519 B b591 t591
1520 T t592 o590 b591
1521 B b592 t592
1522 T t593 o589 b592
1523 B b593 t593
1524 P p593 Number 685
1525 P p594 Number 707
1526 O o594 location p593 p594
1527 P p595 String op
1528 O o595 opname p595
1529 NCzf_itt_group!op op op Czf_itt_group
1530 O o596 op
1531 P p596 Var a
1532 O o597 var p596
1533 T t597 o597
1534 B b597 t597
1535 P p597 Var b
1536 O o598 var p597
1537 T t598 o598
1538 B b598 t598
1539 T t599 o596 b585 b597 b598
1540 B b599 t599
1541 T t600 o595 b599
1542 B b600 t600
1543 T t601 o594 b600
1544 B b601 t601
1545 P p601 Number 708
1546 P p602 Number 722
1547 O o602 location p601 p602
1548 P p603 String id
1549 O o603 opname p603
1550 NCzf_itt_group!id id id Czf_itt_group
1551 O o604 id
1552 T t604 o604 b585
1553 B b604 t604
1554 T t605 o603 b604
1555 B b605 t605
1556 T t606 o602 b605
1557 B b606 t606
1558 P p606 Number 723
1559 P p607 Number 742
1560 O o607 location p606 p607
1561 P p608 String inv
1562 O o608 opname p608
1563 NCzf_itt_group!inv inv inv Czf_itt_group
1564 O o609 inv
1565 T t609 o609 b585 b597
1566 B b609 t609
1567 T t610 o608 b609
1568 B b610 t610
1569 T t611 o607 b610
1570 B b611 t611
1571 P p611 Number 744
1572 P p612 Number 756
1573 O o612 location p611 p612
1574 NSummary!prec prec prec Summary
1575 P p613 String prec_op
1576 O o613 prec p613
1577 T t613 o613
1578 B b613 t613
1579 T t614 o612 b613
1580 B b614 t614
1581 P p614 Number 758
1582 P p615 Number 828
1583 O o615 location p614 p615
1584 NSummary!dform dform dform Summary
1585 P p616 String group_df
1586 O o616 dform p616
1587 NSummary!except_mode_df except_mode_df except_mode_df Summary
1588 P p617 String src
1589 O o617 except_mode_df p617
1590 T t617 o617
1591 B b617 t617
1592 T t618 o b617 b4
1593 B b618 t618
1594 NSummary!df_term df_term df_term Summary
1595 O o618 df_term
1596 Nslot slot slot NIL
1597 O o619 slot
1598 T t619 o619 b585
1599 B b619 t619
1600 NPerv!string string619 string Perv
1601 P p619 String " group"
1602 O o620 string619 p619
1603 T t620 o620
1604 B b620 t620
1605 T t621 o b620 b4
1606 B b621 t621
1607 T t622 o b619 b621
1608 B b622 t622
1609 T t623 o618 b622
1610 B b623 t623
1611 T t624 o616 b618 b586 b623
1612 B b624 t624
1613 T t625 o615 b624
1614 B b625 t625
1615 P p625 Number 830
1616 P p626 Number 899
1617 O o626 location p625 p626
1618 P p627 String car_df
1619 O o627 dform p627
1620 P p628 String car(
1621 O o628 string619 p628
1622 T t628 o628
1623 B b628 t628
1624 P p629 String )
1625 O o629 string619 p629
1626 T t629 o629
1627 B b629 t629
1628 T t630 o b629 b4
1629 B b630 t630
1630 T t631 o b619 b630
1631 B b631 t631
1632 T t632 o b628 b631
1633 B b632 t632
1634 T t633 o618 b632
1635 B b633 t633
1636 T t634 o627 b618 b591 b633
1637 B b634 t634
1638 T t635 o626 b634
1639 B b635 t635
1640 P p635 Number 901
1641 P p636 Number 967
1642 O o636 location p635 p636
1643 P p637 String id_df
1644 O o637 dform p637
1645 P p638 String id(
1646 O o638 string619 p638
1647 T t638 o638
1648 B b638 t638
1649 T t639 o b638 b631
1650 B b639 t639
1651 T t640 o618 b639
1652 B b640 t640
1653 T t641 o637 b618 b604 b640
1654 B b641 t641
1655 T t642 o636 b641
1656 B b642 t642
1657 P p642 Number 969
1658 P p643 Number 1103
1659 O o643 location p642 p643
1660 P p644 String op_df
1661 O o644 dform p644
1662 NSummary!prec_df prec_df prec_df Summary
1663 O o645 prec_df p613
1664 T t645 o645
1665 B b645 t645
1666 NSummary!parens_df parens_df parens_df Summary
1667 O o646 parens_df
1668 T t646 o646
1669 B b646 t646
1670 T t647 o b646 b4
1671 B b647 t647
1672 T t648 o b645 b647
1673 B b648 t648
1674 T t649 o b617 b648
1675 B b649 t649
1676 P p649 String op(
1677 O o649 string619 p649
1678 T t650 o649
1679 B b650 t650
1680 P p650 String "; "
1681 O o650 string619 p650
1682 T t651 o650
1683 B b651 t651
1684 T t652 o619 b597
1685 B b652 t652
1686 T t653 o619 b598
1687 B b653 t653
1688 T t654 o b653 b630
1689 B b654 t654
1690 T t655 o b651 b654
1691 B b655 t655
1692 T t656 o b652 b655
1693 B b656 t656
1694 T t657 o b651 b656
1695 B b657 t657
1696 T t658 o b619 b657
1697 B b658 t658
1698 T t659 o b650 b658
1699 B b659 t659
1700 T t660 o618 b659
1701 B b660 t660
1702 T t661 o644 b649 b599 b660
1703 B b661 t661
1704 T t662 o643 b661
1705 B b662 t662
1706 P p662 Number 1105
1707 P p663 Number 1203
1708 O o663 location p662 p663
1709 P p664 String inv_df
1710 O o664 dform p664
1711 T t664 o b617 b647
1712 B b664 t664
1713 P p665 String inv(
1714 O o665 string619 p665
1715 T t665 o665
1716 B b665 t665
1717 T t666 o b652 b630
1718 B b666 t666
1719 T t667 o b651 b666
1720 B b667 t667
1721 T t668 o b619 b667
1722 B b668 t668
1723 T t669 o b665 b668
1724 B b669 t669
1725 T t670 o618 b669
1726 B b670 t670
1727 T t671 o664 b664 b609 b670
1728 B b671 t671
1729 T t672 o663 b671
1730 B b672 t672
1731 P p672 Number 1222
1732 P p673 Number 1356
1733 O o673 location p672 p673
1734 NSummary!rule rule rule Summary
1735 P p674 String group_type
1736 O o674 rule p674
1737 NSummary!context_param context_param context_param Summary
1738 P p675 String H
1739 O o675 context_param p675
1740 T t675 o675
1741 B b675 t675
1742 T t676 o b675 b4
1743 B b676 t676
1744 NSummary!meta_implies meta_implies meta_implies Summary
1745 O o676 meta_implies
1746 NSummary!meta_theorem meta_theorem meta_theorem Summary
1747 O o677 meta_theorem
1748 NBase_trivial Base_trivial Base_trivial NIL
1749 NBase_trivial!squash squash squash Base_trivial
1750 O o678 squash
1751 T t678 o678
1752 B b678 t678
1753 T t679 o b678 b4
1754 C h H
1755 NItt_equal Itt_equal Itt_equal NIL
1756 NItt_equal!equal equal equal Itt_equal
1757 O o679 equal
1758 NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1759 NItt_record_label0!label label label Itt_record_label0
1760 O o680 label
1761 T t680 o680
1762 B b680 t680
1763 T t681 o679 b680 b585 b585
1764 S s t679 h
1765 G s t681
1766 B b681 s
1767 T t682 o677 b681
1768 B b682 t682
1769 P p682 Var ext
1770 O o682 var p682
1771 T t683 o682
1772 B b683 t683
1773 T t684 o b683 b4
1774 NItt_equal!type type type Itt_equal
1775 O o684 type
1776 T t685 o684 b586
1777 S s685 t684 h
1778 G s685 t685
1779 B b685 s685
1780 T t686 o677 b685
1781 B b686 t686
1782 T t687 o676 b682 b686
1783 B b687 t687
1784 NSummary!incomplete incomplete incomplete Summary
1785 O o687 incomplete
1786 T t688 o687
1787 B b688 t688
1788 NSummary!resource_defs resource_defs resource_defs Summary
1789 P p688 Number 1248
1790 P p689 Number 1256
1791 O o689 resource_defs p688 p689 p204
1792 NOcaml!uid uid uid Ocaml
1793 P p690 Number 1254
1794 O o690 uid p690 p689
1795 P p691 String []
1796 O o691 uid p691
1797 T t691 o691
1798 B b691 t691
1799 T t692 o690 b691
1800 B b692 t692
1801 T t693 o b692 b4
1802 B b693 t693
1803 T t694 o689 b693
1804 B b694 t694
1805 T t695 o b694 b4
1806 B b695 t695
1807 T t696 o674 b676 b687 b688 b695
1808 B b696 t696
1809 T t697 o673 b696
1810 B b697 t697
1811 P p697 Number 1358
1812 P p698 Number 1526
1813 O o698 location p697 p698
1814 P p699 String car_wf
1815 O o699 rule p699
1816 S s699 t684 h
1817 G s699 t586
1818 B b699 s699
1819 T t699 o677 b699
1820 B b700 t699
1821 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1822 NCzf_itt_set!isset isset isset Czf_itt_set
1823 O o700 isset
1824 T t700 o700 b591
1825 S s700 t684 h
1826 G s700 t700
1827 B b701 s700
1828 T t701 o677 b701
1829 B b702 t701
1830 T t702 o676 b700 b702
1831 B b703 t702
1832 T t703 o676 b682 b703
1833 B b704 t703
1834 P p704 Number 1380
1835 P p705 Number 1387
1836 O o705 resource_defs p704 p705 p204
1837 P p706 Number 1385
1838 O o706 uid p706 p705
1839 T t706 o706 b691
1840 B b706 t706
1841 T t707 o b706 b4
1842 B b707 t707
1843 T t708 o705 b707
1844 B b708 t708
1845 T t709 o b708 b4
1846 B b709 t709
1847 T t710 o699 b676 b704 b688 b709
1848 B b710 t710
1849 T t711 o698 b710
1850 B b711 t711
1851 P p711 Number 1528
1852 P p712 Number 1795
1853 O o712 location p711 p712
1854 P p713 String op_wf1
1855 O o713 rule p713
1856 P p714 Var s1
1857 O o714 var p714
1858 T t714 o714
1859 B b714 t714
1860 T t715 o700 b714
1861 S s715 t679 h
1862 G s715 t715
1863 B b715 s715
1864 T t716 o677 b715
1865 B b716 t716
1866 P p716 Var s2
1867 O o716 var p716
1868 T t717 o716
1869 B b717 t717
1870 T t718 o700 b717
1871 S s718 t679 h
1872 G s718 t718
1873 B b718 s718
1874 T t719 o677 b718
1875 B b719 t719
1876 T t720 o596 b585 b714 b717
1877 B b720 t720
1878 T t721 o700 b720
1879 S s721 t684 h
1880 G s721 t721
1881 B b721 s721
1882 T t722 o677 b721
1883 B b722 t722
1884 T t723 o676 b719 b722
1885 B b723 t723
1886 T t724 o676 b716 b723
1887 B b724 t724
1888 T t725 o676 b700 b724
1889 B b725 t725
1890 T t726 o676 b682 b725
1891 B b726 t726
1892 P p726 Number 1550
1893 P p727 Number 1557
1894 O o727 resource_defs p726 p727 p204
1895 P p728 Number 1555
1896 O o728 uid p728 p727
1897 T t728 o728 b691
1898 B b728 t728
1899 T t729 o b728 b4
1900 B b729 t729
1901 T t730 o727 b729
1902 B b730 t730
1903 T t731 o b730 b4
1904 B b731 t731
1905 T t732 o713 b676 b726 b688 b731
1906 B b732 t732
1907 T t733 o712 b732
1908 B b733 t733
1909 P p733 Number 1797
1910 P p734 Number 2171
1911 O o734 location p733 p734
1912 P p735 String op_wf2
1913 O o735 rule p735
1914 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1915 NCzf_itt_member!mem mem mem Czf_itt_member
1916 O o736 mem
1917 T t736 o736 b714 b591
1918 S s736 t684 h
1919 G s736 t736
1920 B b736 s736
1921 T t737 o677 b736
1922 B b737 t737
1923 T t738 o736 b717 b591
1924 S s738 t684 h
1925 G s738 t738
1926 B b738 s738
1927 T t739 o677 b738
1928 B b739 t739
1929 T t740 o736 b720 b591
1930 S s740 t684 h
1931 G s740 t740
1932 B b740 s740
1933 T t741 o677 b740
1934 B b741 t741
1935 T t742 o676 b739 b741
1936 B b742 t742
1937 T t743 o676 b737 b742
1938 B b743 t743
1939 T t744 o676 b700 b743
1940 B b744 t744
1941 T t745 o676 b682 b744
1942 B b745 t745
1943 T t746 o676 b719 b745
1944 B b746 t746
1945 T t747 o676 b716 b746
1946 B b747 t747
1947 P p747 Number 1826
1948 O o747 resource_defs p207 p747 p204
1949 P p748 Number 1824
1950 O o748 uid p748 p747
1951 T t748 o748 b691
1952 B b748 t748
1953 T t749 o b748 b4
1954 B b749 t749
1955 T t750 o747 b749
1956 B b750 t750
1957 T t751 o b750 b4
1958 B b751 t751
1959 T t752 o735 b676 b747 b688 b751
1960 B b752 t752
1961 T t753 o734 b752
1962 B b753 t753
1963 P p753 Number 2173
1964 P p754 Number 2825
1965 O o754 location p753 p754
1966 P p755 String op_equiv1
1967 O o755 rule p755
1968 P p756 Var s3
1969 O o756 var p756
1970 T t756 o756
1971 B b756 t756
1972 T t757 o700 b756
1973 S s757 t679 h
1974 G s757 t757
1975 B b757 s757
1976 T t758 o677 b757
1977 B b758 t758
1978 P p758 Var R
1979 O o758 var p758
1980 T t759 o758
1981 B b759 t759
1982 T t760 o700 b759
1983 S s760 t679 h
1984 G s760 t760
1985 B b760 s760
1986 T t761 o677 b760
1987 B b761 t761
1988 NCzf_itt_equiv Czf_itt_equiv Czf_itt_equiv NIL
1989 NCzf_itt_equiv!equiv equiv equiv Czf_itt_equiv
1990 O o761 equiv
1991 T t762 o761 b591 b759
1992 S s762 t684 h
1993 G s762 t762
1994 B b762 s762
1995 T t763 o677 b762
1996 B b763 t763
1997 T t764 o736 b756 b591
1998 S s764 t684 h
1999 G s764 t764
2000 B b764 s764
2001 T t765 o677 b764
2002 B b765 t765
2003 T t766 o761 b591 b759 b714 b717
2004 S s766 t684 h
2005 G s766 t766
2006 B b766 s766
2007 T t767 o677 b766
2008 B b767 t767
2009 T t768 o596 b585 b756 b714
2010 B b768 t768
2011 T t769 o596 b585 b756 b717
2012 B b769 t769
2013 T t770 o761 b591 b759 b768 b769
2014 S s770 t684 h
2015 G s770 t770
2016 B b770 s770
2017 T t771 o677 b770
2018 B b771 t771
2019 T t772 o676 b767 b771
2020 B b772 t772
2021 T t773 o676 b765 b772
2022 B b773 t773
2023 T t774 o676 b739 b773
2024 B b774 t774
2025 T t775 o676 b737 b774
2026 B b775 t775
2027 T t776 o676 b763 b775
2028 B b776 t776
2029 T t777 o676 b700 b776
2030 B b777 t777
2031 T t778 o676 b682 b777
2032 B b778 t778
2033 T t779 o676 b761 b778
2034 B b779 t779
2035 T t780 o676 b758 b779
2036 B b780 t780
2037 T t781 o676 b719 b780
2038 B b781 t781
2039 T t782 o676 b716 b781
2040 B b782 t782
2041 P p782 Number 2198
2042 P p783 Number 2205
2043 O o783 resource_defs p782 p783 p204
2044 P p784 Number 2203
2045 O o784 uid p784 p783
2046 T t784 o784 b691
2047 B b784 t784
2048 T t785 o b784 b4
2049 B b785 t785
2050 T t786 o783 b785
2051 B b786 t786
2052 T t787 o b786 b4
2053 B b787 t787
2054 T t788 o755 b676 b782 b688 b787
2055 B b788 t788
2056 T t789 o754 b788
2057 B b789 t789
2058 P p789 Number 2827
2059 P p790 Number 3479
2060 O o790 location p789 p790
2061 P p791 String op_equiv2
2062 O o791 rule p791
2063 T t791 o596 b585 b714 b756
2064 B b791 t791
2065 T t792 o596 b585 b717 b756
2066 B b792 t792
2067 T t793 o761 b591 b759 b791 b792
2068 S s793 t684 h
2069 G s793 t793
2070 B b793 s793
2071 T t794 o677 b793
2072 B b794 t794
2073 T t795 o676 b767 b794
2074 B b795 t795
2075 T t796 o676 b765 b795
2076 B b796 t796
2077 T t797 o676 b739 b796
2078 B b797 t797
2079 T t798 o676 b737 b797
2080 B b798 t798
2081 T t799 o676 b763 b798
2082 B b799 t799
2083 T t800 o676 b700 b799
2084 B b800 t800
2085 T t801 o676 b682 b800
2086 B b801 t801
2087 T t802 o676 b761 b801
2088 B b802 t802
2089 T t803 o676 b758 b802
2090 B b803 t803
2091 T t804 o676 b719 b803
2092 B b804 t804
2093 T t805 o676 b716 b804
2094 B b805 t805
2095 P p805 Number 2852
2096 P p806 Number 2859
2097 O o806 resource_defs p805 p806 p204
2098 P p807 Number 2857
2099 O o807 uid p807 p806
2100 T t807 o807 b691
2101 B b807 t807
2102 T t808 o b807 b4
2103 B b808 t808
2104 T t809 o806 b808
2105 B b809 t809
2106 T t810 o b809 b4
2107 B b810 t810
2108 T t811 o791 b676 b805 b688 b810
2109 B b811 t811
2110 T t812 o790 b811
2111 B b812 t812
2112 P p812 Number 3481
2113 P p813 Number 3826
2114 O o813 location p812 p813
2115 P p814 String op_equiv_fun1
2116 O o814 rule p814
2117 P p815 Var s
2118 O o815 var p815
2119 T t815 o815
2120 B b815 t815
2121 T t816 o700 b815
2122 S s816 t679 h
2123 G s816 t816
2124 B b816 s816
2125 T t817 o677 b816
2126 B b817 t817
2127 NCzf_itt_equiv!equiv_fun_set equiv_fun_set equiv_fun_set Czf_itt_equiv
2128 O o817 equiv_fun_set
2129 P p817 Var z
2130 O o818 var p817
2131 T t818 o818
2132 B b818 t818
2133 T t819 o596 b585 b818 b815
2134 B b819 t819 z
2135 T t820 o817 b591 b759 b819
2136 S s820 t684 h
2137 G s820 t820
2138 B b820 s820
2139 T t821 o677 b820
2140 B b821 t821
2141 T t822 o676 b763 b821
2142 B b822 t822
2143 T t823 o676 b700 b822
2144 B b823 t823
2145 T t824 o676 b682 b823
2146 B b824 t824
2147 T t825 o676 b761 b824
2148 B b825 t825
2149 T t826 o676 b817 b825
2150 B b826 t826
2151 P p826 Number 3510
2152 P p827 Number 3517
2153 O o827 resource_defs p826 p827 p204
2154 P p828 Number 3515
2155 O o828 uid p828 p827
2156 T t828 o828 b691
2157 B b828 t828
2158 T t829 o b828 b4
2159 B b829 t829
2160 T t830 o827 b829
2161 B b830 t830
2162 T t831 o b830 b4
2163 B b831 t831
2164 T t832 o814 b676 b826 b688 b831
2165 B b832 t832
2166 T t833 o813 b832
2167 B b833 t833
2168 P p833 Number 3828
2169 P p834 Number 4173
2170 O o834 location p833 p834
2171 P p835 String op_equiv_fun2
2172 O o835 rule p835
2173 T t835 o596 b585 b815 b818
2174 B b835 t835 z
2175 T t836 o817 b591 b759 b835
2176 S s836 t684 h
2177 G s836 t836
2178 B b836 s836
2179 T t837 o677 b836
2180 B b837 t837
2181 T t838 o676 b763 b837
2182 B b838 t838
2183 T t839 o676 b700 b838
2184 B b839 t839
2185 T t840 o676 b682 b839
2186 B b840 t840
2187 T t841 o676 b761 b840
2188 B b841 t841
2189 T t842 o676 b817 b841
2190 B b842 t842
2191 P p842 Number 3857
2192 P p843 Number 3864
2193 O o843 resource_defs p842 p843 p204
2194 P p844 Number 3862
2195 O o844 uid p844 p843
2196 T t844 o844 b691
2197 B b844 t844
2198 T t845 o b844 b4
2199 B b845 t845
2200 T t846 o843 b845
2201 B b846 t846
2202 T t847 o b846 b4
2203 B b847 t847
2204 T t848 o835 b676 b842 b688 b847
2205 B b848 t848
2206 T t849 o834 b848
2207 B b849 t849
2208 P p849 Number 4175
2209 P p850 Number 4403
2210 O o850 location p849 p850
2211 P p851 String op_eq_fun1
2212 O o851 rule p851
2213 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
2214 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
2215 O o852 fun_set
2216 T t852 o852 b819
2217 S s852 t684 h
2218 G s852 t852
2219 B b852 s852
2220 T t853 o677 b852
2221 B b853 t853
2222 T t854 o676 b700 b853
2223 B b854 t854
2224 T t855 o676 b682 b854
2225 B b855 t855
2226 T t856 o676 b817 b855
2227 B b856 t856
2228 P p856 Number 4201
2229 P p857 Number 4208
2230 O o857 resource_defs p856 p857 p204
2231 P p858 Number 4206
2232 O o858 uid p858 p857
2233 T t858 o858 b691
2234 B b858 t858
2235 T t859 o b858 b4
2236 B b859 t859
2237 T t860 o857 b859
2238 B b860 t860
2239 T t861 o b860 b4
2240 B b861 t861
2241 T t862 o851 b676 b856 b688 b861
2242 B b862 t862
2243 T t863 o850 b862
2244 B b863 t863
2245 P p863 Number 4405
2246 P p864 Number 4633
2247 O o864 location p863 p864
2248 P p865 String op_eq_fun2
2249 O o865 rule p865
2250 T t865 o852 b835
2251 S s865 t684 h
2252 G s865 t865
2253 B b865 s865
2254 T t866 o677 b865
2255 B b866 t866
2256 T t867 o676 b700 b866
2257 B b867 t867
2258 T t868 o676 b682 b867
2259 B b868 t868
2260 T t869 o676 b817 b868
2261 B b869 t869
2262 P p869 Number 4431
2263 P p870 Number 4438
2264 O o870 resource_defs p869 p870 p204
2265 P p871 Number 4436
2266 O o871 uid p871 p870
2267 T t871 o871 b691
2268 B b871 t871
2269 T t872 o b871 b4
2270 B b872 t872
2271 T t873 o870 b872
2272 B b873 t873
2273 T t874 o b873 b4
2274 B b874 t874
2275 T t875 o865 b676 b869 b688 b874
2276 B b875 t875
2277 T t876 o864 b875
2278 B b876 t876
2279 P p876 Number 4635
2280 P p877 Number 5252
2281 O o877 location p876 p877
2282 P p878 String op_assoc1
2283 O o878 rule p878
2284 T t878 o596 b585 b720 b756
2285 B b878 t878
2286 T t879 o596 b585 b714 b792
2287 B b879 t879
2288 T t880 o761 b591 b759 b878 b879
2289 S s880 t684 h
2290 G s880 t880
2291 B b880 s880
2292 T t881 o677 b880
2293 B b881 t881
2294 T t882 o676 b765 b881
2295 B b882 t882
2296 T t883 o676 b739 b882
2297 B b883 t883
2298 T t884 o676 b737 b883
2299 B b884 t884
2300 T t885 o676 b763 b884
2301 B b885 t885
2302 T t886 o676 b700 b885
2303 B b886 t886
2304 T t887 o676 b682 b886
2305 B b887 t887
2306 T t888 o676 b761 b887
2307 B b888 t888
2308 T t889 o676 b758 b888
2309 B b889 t889
2310 T t890 o676 b719 b889
2311 B b890 t890
2312 T t891 o676 b716 b890
2313 B b891 t891
2314 P p891 Number 4660
2315 P p892 Number 4667
2316 O o892 resource_defs p891 p892 p204
2317 P p893 Number 4665
2318 O o893 uid p893 p892
2319 T t893 o893 b691
2320 B b893 t893
2321 T t894 o b893 b4
2322 B b894 t894
2323 T t895 o892 b894
2324 B b895 t895
2325 T t896 o b895 b4
2326 B b896 t896
2327 T t897 o878 b676 b891 b688 b896
2328 B b897 t897
2329 T t898 o877 b897
2330 B b898 t898
2331 P p898 Number 5254
2332 P p899 Number 5871
2333 O o899 location p898 p899
2334 P p900 String op_assoc2
2335 O o900 rule p900
2336 T t900 o761 b591 b759 b879 b878
2337 S s900 t684 h
2338 G s900 t900
2339 B b900 s900
2340 T t901 o677 b900
2341 B b901 t901
2342 T t902 o676 b765 b901
2343 B b902 t902
2344 T t903 o676 b739 b902
2345 B b903 t903
2346 T t904 o676 b737 b903
2347 B b904 t904
2348 T t905 o676 b763 b904
2349 B b905 t905
2350 T t906 o676 b700 b905
2351 B b906 t906
2352 T t907 o676 b682 b906
2353 B b907 t907
2354 T t908 o676 b761 b907
2355 B b908 t908
2356 T t909 o676 b758 b908
2357 B b909 t909
2358 T t910 o676 b719 b909
2359 B b910 t910
2360 T t911 o676 b716 b910
2361 B b911 t911
2362 P p911 Number 5279
2363 P p912 Number 5286
2364 O o912 resource_defs p911 p912 p204
2365 P p913 Number 5284
2366 O o913 uid p913 p912
2367 T t913 o913 b691
2368 B b913 t913
2369 T t914 o b913 b4
2370 B b914 t914
2371 T t915 o912 b914
2372 B b915 t915
2373 T t916 o b915 b4
2374 B b916 t916
2375 T t917 o900 b676 b911 b688 b916
2376 B b917 t917
2377 T t918 o899 b917
2378 B b918 t918
2379 P p918 Number 5873
2380 P p919 Number 6041
2381 O o919 location p918 p919
2382 P p920 String id_wf1
2383 O o920 rule p920
2384 T t920 o700 b604
2385 S s920 t684 h
2386 G s920 t920
2387 B b920 s920
2388 T t921 o677 b920
2389 B b921 t921
2390 T t922 o676 b700 b921
2391 B b922 t922
2392 T t923 o676 b682 b922
2393 B b923 t923
2394 P p923 Number 5895
2395 P p924 Number 5903
2396 O o924 resource_defs p923 p924 p204
2397 P p925 Number 5901
2398 O o925 uid p925 p924
2399 T t925 o925 b691
2400 B b925 t925
2401 T t926 o b925 b4
2402 B b926 t926
2403 T t927 o924 b926
2404 B b927 t927
2405 T t928 o b927 b4
2406 B b928 t928
2407 T t929 o920 b676 b923 b688 b928
2408 B b929 t929
2409 T t930 o919 b929
2410 B b930 t930
2411 P p930 Number 6043
2412 P p931 Number 6217
2413 O o931 location p930 p931
2414 P p932 String id_wf2
2415 O o932 rule p932
2416 T t932 o736 b604 b591
2417 S s932 t684 h
2418 G s932 t932
2419 B b932 s932
2420 T t933 o677 b932
2421 B b933 t933
2422 T t934 o676 b700 b933
2423 B b934 t934
2424 T t935 o676 b682 b934
2425 B b935 t935
2426 P p935 Number 6065
2427 P p936 Number 6072
2428 O o936 resource_defs p935 p936 p204
2429 P p937 Number 6070
2430 O o937 uid p937 p936
2431 T t937 o937 b691
2432 B b937 t937
2433 T t938 o b937 b4
2434 B b938 t938
2435 T t939 o936 b938
2436 B b939 t939
2437 T t940 o b939 b4
2438 B b940 t940
2439 T t941 o932 b676 b935 b688 b940
2440 B b941 t941
2441 T t942 o931 b941
2442 B b942 t942
2443 P p942 Number 6219
2444 P p943 Number 6603
2445 O o943 location p942 p943
2446 P p944 String id_eq1
2447 O o944 rule p944
2448 T t944 o736 b815 b591
2449 S s944 t684 h
2450 G s944 t944
2451 B b944 s944
2452 T t945 o677 b944
2453 B b945 t945
2454 T t946 o596 b585 b604 b815
2455 B b946 t946
2456 T t947 o761 b591 b759 b946 b815
2457 S s947 t684 h
2458 G s947 t947
2459 B b947 s947
2460 T t948 o677 b947
2461 B b948 t948
2462 T t949 o676 b945 b948
2463 B b949 t949
2464 T t950 o676 b763 b949
2465 B b950 t950
2466 T t951 o676 b700 b950
2467 B b951 t951
2468 T t952 o676 b682 b951
2469 B b952 t952
2470 T t953 o676 b761 b952
2471 B b953 t953
2472 T t954 o676 b817 b953
2473 B b954 t954
2474 P p954 Number 6241
2475 P p955 Number 6248
2476 O o955 resource_defs p954 p955 p204
2477 P p956 Number 6246
2478 O o956 uid p956 p955
2479 T t956 o956 b691
2480 B b956 t956
2481 T t957 o b956 b4
2482 B b957 t957
2483 T t958 o955 b957
2484 B b958 t958
2485 T t959 o b958 b4
2486 B b959 t959
2487 T t960 o944 b676 b954 b688 b959
2488 B b960 t960
2489 T t961 o943 b960
2490 B b961 t961
2491 P p961 Number 6605
2492 P p6 Number 6874
2493 O o10 location p961 p6
2494 P p963 String id_eq2
2495 O o963 rule p963
2496 T t963 o596 b585 b815 b604
2497 B b963 t963
2498 T t964 o761 b591 b759 b963 b815
2499 S s964 t684 h
2500 G s964 t964
2501 B b964 s964
2502 T t965 o677 b964
2503 B b965 t965
2504 T t966 o676 b945 b965
2505 B b966 t966
2506 T t967 o676 b763 b966
2507 B b967 t967
2508 T t968 o676 b700 b967
2509 B b968 t968
2510 T t969 o676 b682 b968
2511 B b969 t969
2512 T t970 o676 b761 b969
2513 B b970 t970
2514 T t971 o676 b817 b970
2515 B b971 t971
2516 P p980 String inv_wf1
2517 O o980 rule p980
2518 T t980 o609 b585 b714
2519 B b980 t980
2520 T t981 o700 b980
2521 S s981 t684 h
2522 G s981 t981
2523 B b981 s981
2524 T t982 o677 b981
2525 B b982 t982
2526 T t983 o676 b737 b982
2527 B b983 t983
2528 T t984 o676 b700 b983
2529 B b984 t984
2530 T t985 o676 b682 b984
2531 B b985 t985
2532 T t986 o676 b716 b985
2533 B b986 t986
2534 P p10 Number 6628
2535 P p12 Number 6635
2536 O o12 resource_defs p10 p12 p204
2537 P p14 Number 6633
2538 O o14 uid p14 p12
2539 T t250 o14 b691
2540 B b250 t250
2541 T t255 o b250 b4
2542 B b255 t255
2543 T t256 o12 b255
2544 B b256 t256
2545 T t258 o b256 b4
2546 B b258 t258
2547 T t260 o980 b676 b986 b688 b258
2548 B b260 t260
2549 T t267 o10 b260
2550 B b267 t267
2551 P p269 Number 6876
2552 P p277 Number 7152
2553 O o277 location p269 p277
2554 P p995 String inv_wf2
2555 O o995 rule p995
2556 T t995 o736 b980 b591
2557 S s995 t684 h
2558 G s995 t995
2559 B b995 s995
2560 T t996 o677 b995
2561 B b996 t996
2562 T t997 o676 b737 b996
2563 B b997 t997
2564 T t998 o676 b700 b997
2565 B b998 t998
2566 T t999 o676 b682 b998
2567 B b999 t999
2568 T t1000 o676 b716 b999
2569 B b1000 t1000
2570 P p284 Number 6899
2571 P p285 Number 6906
2572 O o285 resource_defs p284 p285 p204
2573 P p286 Number 6904
2574 O o286 uid p286 p285
2575 T t299 o286 b691
2576 B b299 t299
2577 T t368 o b299 b4
2578 B b368 t368
2579 T t379 o285 b368
2580 B b379 t379
2581 T t394 o b379 b4
2582 B b394 t394
2583 T t400 o995 b676 b1000 b688 b394
2584 B b400 t400
2585 T t421 o277 b400
2586 B b421 t421
2587 P p422 Number 7154
2588 P p424 Number 7453
2589 O o425 location p422 p424
2590 P p1009 String inv_equiv_fun1
2591 O o1009 rule p1009
2592 T t1009 o609 b585 b818
2593 B b1009 t1009 z
2594 T t1010 o817 b591 b759 b1009
2595 S s1010 t684 h
2596 G s1010 t1010
2597 B b1010 s1010
2598 T t1011 o677 b1010
2599 B b1011 t1011
2600 T t1012 o676 b763 b1011
2601 B b1012 t1012
2602 T t1013 o676 b700 b1012
2603 B b1013 t1013
2604 T t1014 o676 b682 b1013
2605 B b1014 t1014
2606 T t1015 o676 b761 b1014
2607 B b1015 t1015
2608 P p425 Number 7184
2609 P p426 Number 7191
2610 O o426 resource_defs p425 p426 p204
2611 P p427 Number 7189
2612 O o427 uid p427 p426
2613 T t429 o427 b691
2614 B b429 t429
2615 T t430 o b429 b4
2616 B b430 t430
2617 T t436 o426 b430
2618 B b436 t436
2619 T t437 o b436 b4
2620 B b437 t437
2621 T t446 o1009 b676 b1015 b688 b437
2622 B b446 t446
2623 T t447 o425 b446
2624 B b447 t447
2625 P p448 Number 7455
2626 P p449 Number 7637
2627 O o449 location p448 p449
2628 P p1024 String inv_eq_fun1
2629 O o1024 rule p1024
2630 T t1024 o852 b1009
2631 S s1024 t684 h
2632 G s1024 t1024
2633 B b1024 s1024
2634 T t1025 o677 b1024
2635 B b1025 t1025
2636 T t1026 o676 b700 b1025
2637 B b1026 t1026
2638 T t1027 o676 b682 b1026
2639 B b1027 t1027
2640 P p450 Number 7482
2641 P p451 Number 7489
2642 O o451 resource_defs p450 p451 p204
2643 P p452 Number 7487
2644 O o452 uid p452 p451
2645 T t455 o452 b691
2646 B b455 t455
2647 T t456 o b455 b4
2648 B b456 t456
2649 T t464 o451 b456
2650 B b464 t464
2651 T t465 o b464 b4
2652 B b465 t465
2653 T t473 o1024 b676 b1027 b688 b465
2654 B b473 t473
2655 T t474 o449 b473
2656 B b474 t474
2657 P p475 Number 7639
2658 P p476 Number 8037
2659 O o476 location p475 p476
2660 P p1036 String inv_id1
2661 O o1036 rule p1036
2662 T t1036 o596 b585 b980 b714
2663 B b1036 t1036
2664 T t1037 o761 b591 b759 b1036 b604
2665 S s1037 t684 h
2666 G s1037 t1037
2667 B b1037 s1037
2668 T t1038 o677 b1037
2669 B b1038 t1038
2670 T t1039 o676 b737 b1038
2671 B b1039 t1039
2672 T t1040 o676 b763 b1039
2673 B b1040 t1040
2674 T t1041 o676 b700 b1040
2675 B b1041 t1041
2676 T t1042 o676 b682 b1041
2677 B b1042 t1042
2678 T t1043 o676 b761 b1042
2679 B b1043 t1043
2680 T t1044 o676 b716 b1043
2681 B b1044 t1044
2682 P p477 Number 7662
2683 P p478 Number 7669
2684 O o478 resource_defs p477 p478 p204
2685 P p479 Number 7667
2686 O o479 uid p479 p478
2687 T t482 o479 b691
2688 B b482 t482
2689 T t483 o b482 b4
2690 B b483 t483
2691 T t491 o478 b483
2692 B b491 t491
2693 T t492 o b491 b4
2694 B b492 t492
2695 T t500 o1036 b676 b1044 b688 b492
2696 B b500 t500
2697 T t501 o476 b500
2698 B b501 t501
2699 P p8 Number 8056
2700 P p16 Number 8796
2701 O o16 location p8 p16
2702 P p1053 String inv_id2
2703 O o1053 rule p1053
2704 P p1070 String equiv_op_fun1
2705 O o1070 rule p1070
2706 T t1070 o700 b597
2707 S s1070 t679 h
2708 G s1070 t1070
2709 B b1070 s1070
2710 T t1071 o677 b1070
2711 B b1071 t1071
2712 T t1072 o700 b598
2713 S s1072 t679 h
2714 G s1072 t1072
2715 B b1072 s1072
2716 T t1073 o677 b1072
2717 B b1073 t1073
2718 T t1074 o736 b597 b591
2719 S s1074 t684 h
2720 G s1074 t1074
2721 B b1074 s1074
2722 T t1075 o677 b1074
2723 B b1075 t1075
2724 T t1076 o736 b598 b591
2725 S s1076 t684 h
2726 G s1076 t1076
2727 B b1076 s1076
2728 T t1077 o677 b1076
2729 B b1077 t1077
2730 NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
2731 O o1077 equiv_fun_prop
2732 T t1078 o596 b585 b818 b597
2733 B b1078 t1078
2734 T t1079 o596 b585 b818 b598
2735 B b1079 t1079
2736 T t1080 o761 b591 b759 b1078 b1079
2737 B b1080 t1080 z
2738 T t1081 o1077 b591 b759 b1080
2739 S s1081 t684 h
2740 G s1081 t1081
2741 B b1081 s1081
2742 T t1082 o677 b1081
2743 B b1082 t1082
2744 T t1083 o676 b1077 b1082
2745 B b1083 t1083
2746 T t1084 o676 b1075 b1083
2747 B b1084 t1084
2748 T t1085 o676 b763 b1084
2749 B b1085 t1085
2750 T t1086 o676 b700 b1085
2751 B b1086 t1086
2752 T t1087 o676 b682 b1086
2753 B b1087 t1087
2754 T t1088 o676 b761 b1087
2755 B b1088 t1088
2756 T t1089 o676 b1073 b1088
2757 B b1089 t1089
2758 T t1090 o676 b1071 b1089
2759 B b1090 t1090
2760 NSummary!interactive interactive interactive Summary
2761 O o1090 interactive
2762 NSummary!ext_rule ext_rule ext_rule Summary
2763 P p1090 String "rwh unfold_equiv_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
2764 O o1091 ext_rule p1090
2765 NSummary!status_incomplete status_incomplete status_incomplete Summary
2766 O o1092 status_incomplete
2767 T t1092 o1092
2768 B b1092 t1092
2769 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2770 O o1093 ext_unjustified
2771 NSummary!tactic_arg tactic_arg tactic_arg Summary
2772 P p1093 String main
2773 O o1094 tactic_arg p1093
2774 NSummary!msequent msequent msequent Summary
2775 O o1095 msequent
2776 T t1095 o b1076 b4
2777 B b1095 t1095
2778 T t1096 o b1074 b1095
2779 B b1096 t1096
2780 T t1097 o b762 b1096
2781 B b1097 t1097
2782 T t1098 o b699 b1097
2783 B b1098 t1098
2784 T t1099 o b681 b1098
2785 B b1099 t1099
2786 T t1100 o b760 b1099
2787 B b1100 t1100
2788 T t1101 o b1072 b1100
2789 B b1101 t1101
2790 T t1102 o b1070 b1101
2791 B b1102 t1102
2792 T t1103 o1095 b1081 b1102
2793 B b1103 t1103
2794 NSummary!parent_none parent_none parent_none Summary
2795 O o1103 parent_none
2796 T t1104 o1103
2797 B b1104 t1104
2798 T t1105 o1094 b1103 b4 b1104
2799 B b1105 t1105
2800 NCzf_itt_set!set set set Czf_itt_set
2801 O o1105 set
2802 T t1106 o1105
2803 H h1106 a_1 t1106
2804 H h1107 b_1 t1106
2805 H h1108 x t762
2806 P p1108 Var a_1
2807 O o1108 var p1108
2808 T t1108 o1108
2809 B b1108 t1108
2810 P p1109 Var b_1
2811 O o1109 var p1109
2812 T t1109 o1109
2813 B b1109 t1109
2814 T t1110 o761 b591 b759 b1108 b1109
2815 H h1110 x_1 t1110
2816 T t1111 o596 b585 b1108 b597
2817 B b1111 t1111
2818 T t1112 o596 b585 b1108 b598
2819 B b1112 t1112
2820 T t1113 o761 b591 b759 b1111 b1112
2821 H h1113 x_2 t1113
2822 T t1114 o596 b585 b1109 b597
2823 B b1114 t1114
2824 T t1115 o596 b585 b1109 b598
2825 B b1115 t1115
2826 T t1116 o761 b591 b759 b1114 b1115
2827 S s1116 t684 h h1106 h1107 h1108 h1110 h1113
2828 G s1116 t1116
2829 B b1116 s1116
2830 T t1117 o1095 b1116 b1102
2831 B b1117 t1117
2832 NItt_logic Itt_logic Itt_logic NIL
2833 NItt_logic!implies implies implies Itt_logic
2834 O o1117 implies
2835 B b1118 t1113
2836 B b1119 t1116
2837 T t1119 o1117 b1118 b1119
2838 S s1119 t684 h h1106 h1107 h1108 h1110
2839 G s1119 t1119
2840 B b1120 s1119
2841 T t1120 o1095 b1120 b1102
2842 B b1121 t1120
2843 B b1122 t1110
2844 B b1123 t1119
2845 T t1123 o1117 b1122 b1123
2846 S s1123 t684 h h1106 h1107 h1108
2847 G s1123 t1123
2848 B b1124 s1123
2849 T t1124 o1095 b1124 b1102
2850 B b1125 t1124
2851 B b1126 t762
2852 B b1127 t1123
2853 T t1127 o1117 b1126 b1127
2854 S s1127 t684 h h1106 h1107
2855 G s1127 t1127
2856 B b1128 s1127
2857 T t1128 o1095 b1128 b1102
2858 B b1129 t1128
2859 NItt_logic!all all all Itt_logic
2860 O o1129 all
2861 B b1130 t1106
2862 B b1131 t1127 b_1
2863 T t1131 o1129 b1130 b1131
2864 S s1131 t684 h h1106
2865 G s1131 t1131
2866 B b1132 s1131
2867 T t1132 o1095 b1132 b1102
2868 B b1133 t1132
2869 B b1134 t1131 a_1
2870 T t1134 o1129 b1130 b1134
2871 S s1134 t684 h
2872 G s1134 t1134
2873 B b1135 s1134
2874 T t1135 o1095 b1135 b1102
2875 B b1136 t1135
2876 T t1136 o2 b1105
2877 B b1137 t1136
2878 T t1137 o1094 b1136 b4 b1137
2879 B b1138 t1137
2880 T t1138 o2 b1138
2881 B b1139 t1138
2882 T t1139 o1094 b1133 b4 b1139
2883 B b1140 t1139
2884 T t1140 o2 b1140
2885 B b1141 t1140
2886 T t1141 o1094 b1129 b4 b1141
2887 B b1142 t1141
2888 T t1142 o2 b1142
2889 B b1143 t1142
2890 T t1143 o1094 b1125 b4 b1143
2891 B b1144 t1143
2892 T t1144 o2 b1144
2893 B b1145 t1144
2894 T t1145 o1094 b1121 b4 b1145
2895 B b1146 t1145
2896 T t1146 o2 b1146
2897 B b1147 t1146
2898 T t1147 o1094 b1117 b4 b1147
2899 B b1148 t1147
2900 T t1148 o b1148 b4
2901 B b1149 t1148
2902 T t1149 o1093 b1105 b1149
2903 B b1150 t1149
2904 P p1150 String "equivTransT << op{'g; 'b_1; 'a} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
2905 O o1150 ext_rule p1150
2906 NItt_logic!and and and Itt_logic
2907 O o1151 and
2908 B b1151 t700
2909 B b1152 t760
2910 T t1152 o700 b1111
2911 B b1153 t1152
2912 T t1153 o700 b1112
2913 B b1154 t1153
2914 T t1154 o1151 b1153 b1154
2915 B b1155 t1154
2916 T t1155 o1151 b1152 b1155
2917 B b1156 t1155
2918 T t1156 o1151 b1151 b1156
2919 B b1157 t1156
2920 T t1157 o736 b1111 b591
2921 B b1158 t1157
2922 T t1158 o736 b1112 b591
2923 B b1159 t1158
2924 T t1159 o1151 b1158 b1159
2925 B b1160 t1159
2926 T t1160 o1151 b1157 b1160
2927 B b1161 t1160
2928 NCzf_itt_pair Czf_itt_pair Czf_itt_pair NIL
2929 NCzf_itt_pair!pair pair pair Czf_itt_pair
2930 O o1161 pair
2931 T t1161 o1161 b1111 b1112
2932 B b1162 t1161
2933 T t1162 o736 b1162 b759
2934 B b1163 t1162
2935 T t1163 o1151 b1161 b1163
2936 H h1163 x_2 t1163
2937 T t1164 o736 b1114 b591
2938 S s1164 t684 h h1106 h1107 h1108 h1110 h1163
2939 G s1164 t1164
2940 B b1164 s1164
2941 T t1165 o1095 b1164 b1102
2942 B b1165 t1165
2943 S s1165 t684 h h1106 h1107 h1108 h1110 h1113
2944 G s1165 t1164
2945 B b1166 s1165
2946 T t1166 o1095 b1166 b1102
2947 B b1167 t1166
2948 T t1167 o2 b1148
2949 B b1168 t1167
2950 T t1168 o1094 b1167 b4 b1168
2951 B b1169 t1168
2952 T t1169 o2 b1169
2953 B b1170 t1169
2954 T t1170 o1094 b1165 b4 b1170
2955 B b1171 t1170
2956 T t1171 o761 b591 b759 b1111 b1114
2957 H h1171 u t1171
2958 T t1172 o761 b591 b759 b1114 b1112
2959 H h1172 v t1172
2960 S s1172 t684 h h1106 h1107 h1108 h1110 h1163 h1171 h1172
2961 G s1172 t1116
2962 B b1172 s1172
2963 T t1173 o1095 b1172 b1102
2964 B b1173 t1173
2965 S s1173 t684 h h1106 h1107 h1108 h1110 h1113 h1171 h1172
2966 G s1173 t1116
2967 B b1174 s1173
2968 T t1174 o1095 b1174 b1102
2969 B b1175 t1174
2970 T t1175 o1094 b1175 b4 b1168
2971 B b1176 t1175
2972 T t1176 o2 b1176
2973 B b1177 t1176
2974 T t1177 o1094 b1173 b4 b1177
2975 B b1178 t1177
2976 T t1178 o b1178 b4
2977 B b1179 t1178
2978 T t1179 o b1171 b1179
2979 B b1180 t1179
2980 T t1180 o1093 b1148 b1180
2981 B b1181 t1180
2982 P p1181 String "autoT thenT rwh unfold_equiv 5 ttca"
2983 O o1181 ext_rule p1181
2984 T t1181 o1093 b1171 b4
2985 B b1182 t1181
2986 T t1182 o1181 b1092 b1182 b4 b4
2987 B b1183 t1182
2988 P p1183 String "equivTransT << op{'g; 'b_1; 'b} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
2989 O o1183 ext_rule p1183
2990 T t1183 o1093 b1178 b4
2991 B b1184 t1183
2992 T t1184 o1183 b1092 b1184 b4 b4
2993 B b1185 t1184
2994 T t1185 o b1185 b4
2995 B b1186 t1185
2996 T t1186 o b1183 b1186
2997 B b1187 t1186
2998 T t1187 o1150 b1092 b1181 b1187 b4
2999 B b1188 t1187
3000 T t1188 o b1188 b4
3001 B b1189 t1188
3002 T t1189 o1091 b1092 b1150 b1189 b4
3003 B b1190 t1189
3004 T t1190 o1090 b1190
3005 B b1191 t1190
3006 P p1200 String equiv_op_fun2
3007 O o1200 rule p1200
3008 T t1200 o596 b585 b597 b818
3009 B b1200 t1200
3010 T t1201 o596 b585 b598 b818
3011 B b1201 t1201
3012 T t1202 o761 b591 b759 b1200 b1201
3013 B b1202 t1202 z
3014 T t1203 o1077 b591 b759 b1202
3015 S s1203 t684 h
3016 G s1203 t1203
3017 B b1203 s1203
3018 T t1204 o677 b1203
3019 B b1204 t1204
3020 T t1205 o676 b1077 b1204
3021 B b1205 t1205
3022 T t1206 o676 b1075 b1205
3023 B b1206 t1206
3024 T t1207 o676 b763 b1206
3025 B b1207 t1207
3026 T t1208 o676 b700 b1207
3027 B b1208 t1208
3028 T t1209 o676 b682 b1208
3029 B b1209 t1209
3030 T t1210 o676 b761 b1209
3031 B b1210 t1210
3032 T t1211 o676 b1073 b1210
3033 B b1211 t1211
3034 T t1212 o676 b1071 b1211
3035 B b1212 t1212
3036 T t1213 o1095 b1203 b1102
3037 B b1213 t1213
3038 T t1214 o1094 b1213 b4 b1104
3039 B b1214 t1214
3040 T t1215 o596 b585 b597 b1108
3041 B b1215 t1215
3042 T t1216 o596 b585 b598 b1108
3043 B b1216 t1216
3044 T t1217 o761 b591 b759 b1215 b1216
3045 H h1217 x_2 t1217
3046 T t1218 o596 b585 b597 b1109
3047 B b1218 t1218
3048 T t1219 o596 b585 b598 b1109
3049 B b1219 t1219
3050 T t1220 o761 b591 b759 b1218 b1219
3051 S s1220 t684 h h1106 h1107 h1108 h1110 h1217
3052 G s1220 t1220
3053 B b1220 s1220
3054 T t1221 o1095 b1220 b1102
3055 B b1221 t1221
3056 B b1222 t1217
3057 B b1223 t1220
3058 T t1223 o1117 b1222 b1223
3059 S s1223 t684 h h1106 h1107 h1108 h1110
3060 G s1223 t1223
3061 B b1224 s1223
3062 T t1224 o1095 b1224 b1102
3063 B b1225 t1224
3064 B b1226 t1223
3065 T t1226 o1117 b1122 b1226
3066 S s1226 t684 h h1106 h1107 h1108
3067 G s1226 t1226
3068 B b1227 s1226
3069 T t1227 o1095 b1227 b1102
3070 B b1228 t1227
3071 B b1229 t1226
3072 T t1229 o1117 b1126 b1229
3073 S s1229 t684 h h1106 h1107
3074 G s1229 t1229
3075 B b1230 s1229
3076 T t1230 o1095 b1230 b1102
3077 B b1231 t1230
3078 B b1232 t1229 b_1
3079 T t1232 o1129 b1130 b1232
3080 S s1232 t684 h h1106
3081 G s1232 t1232
3082 B b1233 s1232
3083 T t1233 o1095 b1233 b1102
3084 B b1234 t1233
3085 B b1235 t1232 a_1
3086 T t1235 o1129 b1130 b1235
3087 S s1235 t684 h
3088 G s1235 t1235
3089 B b1236 s1235
3090 T t1236 o1095 b1236 b1102
3091 B b1237 t1236
3092 T t1237 o2 b1214
3093 B b1238 t1237
3094 T t1238 o1094 b1237 b4 b1238
3095 B b1239 t1238
3096 T t1239 o2 b1239
3097 B b1240 t1239
3098 T t1240 o1094 b1234 b4 b1240
3099 B b1241 t1240
3100 T t1241 o2 b1241
3101 B b1242 t1241
3102 T t1242 o1094 b1231 b4 b1242
3103 B b1243 t1242
3104 T t1243 o2 b1243
3105 B b1244 t1243
3106 T t1244 o1094 b1228 b4 b1244
3107 B b1245 t1244
3108 T t1245 o2 b1245
3109 B b1246 t1245
3110 T t1246 o1094 b1225 b4 b1246
3111 B b1247 t1246
3112 T t1247 o2 b1247
3113 B b1248 t1247
3114 T t1248 o1094 b1221 b4 b1248
3115 B b1249 t1248
3116 T t1249 o b1249 b4
3117 B b1250 t1249
3118 T t1250 o1093 b1214 b1250
3119 B b1251 t1250
3120 P p1251 String "equivTransT << op{'g; 'a; 'b_1} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
3121 O o1251 ext_rule p1251
3122 T t1251 o700 b1215
3123 B b1252 t1251
3124 T t1252 o700 b1216
3125 B b1253 t1252
3126 T t1253 o1151 b1252 b1253
3127 B b1254 t1253
3128 T t1254 o1151 b1152 b1254
3129 B b1255 t1254
3130 T t1255 o1151 b1151 b1255
3131 B b1256 t1255
3132 T t1256 o736 b1215 b591
3133 B b1257 t1256
3134 T t1257 o736 b1216 b591
3135 B b1258 t1257
3136 T t1258 o1151 b1257 b1258
3137 B b1259 t1258
3138 T t1259 o1151 b1256 b1259
3139 B b1260 t1259
3140 T t1260 o1161 b1215 b1216
3141 B b1261 t1260
3142 T t1261 o736 b1261 b759
3143 B b1262 t1261
3144 T t1262 o1151 b1260 b1262
3145 H h1262 x_2 t1262
3146 T t1263 o736 b1218 b591
3147 S s1263 t684 h h1106 h1107 h1108 h1110 h1262
3148 G s1263 t1263
3149 B b1263 s1263
3150 T t1264 o1095 b1263 b1102
3151 B b1264 t1264
3152 S s1264 t684 h h1106 h1107 h1108 h1110 h1217
3153 G s1264 t1263
3154 B b1265 s1264
3155 T t1265 o1095 b1265 b1102
3156 B b1266 t1265
3157 T t1266 o2 b1249
3158 B b1267 t1266
3159 T t1267 o1094 b1266 b4 b1267
3160 B b1268 t1267
3161 T t1268 o2 b1268
3162 B b1269 t1268
3163 T t1269 o1094 b1264 b4 b1269
3164 B b1270 t1269
3165 T t1270 o761 b591 b759 b1215 b1218
3166 H h1270 u t1270
3167 T t1271 o761 b591 b759 b1218 b1216
3168 H h1271 v t1271
3169 S s1271 t684 h h1106 h1107 h1108 h1110 h1262 h1270 h1271
3170 G s1271 t1220
3171 B b1271 s1271
3172 T t1272 o1095 b1271 b1102
3173 B b1272 t1272
3174 S s1272 t684 h h1106 h1107 h1108 h1110 h1217 h1270 h1271
3175 G s1272 t1220
3176 B b1273 s1272
3177 T t1273 o1095 b1273 b1102
3178 B b1274 t1273
3179 T t1274 o1094 b1274 b4 b1267
3180 B b1275 t1274
3181 T t1275 o2 b1275
3182 B b1276 t1275
3183 T t1276 o1094 b1272 b4 b1276
3184 B b1277 t1276
3185 T t1277 o b1277 b4
3186 B b1278 t1277
3187 T t1278 o b1270 b1278
3188 B b1279 t1278
3189 T t1279 o1093 b1249 b1279
3190 B b1280 t1279
3191 T t1280 o1093 b1270 b4
3192 B b1281 t1280
3193 T t1281 o1181 b1092 b1281 b4 b4
3194 B b1282 t1281
3195 P p1282 String "equivTransT << op{'g; 'b; 'b_1} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3196 O o1282 ext_rule p1282
3197 T t1282 o1093 b1277 b4
3198 B b1283 t1282
3199 T t1283 o1282 b1092 b1283 b4 b4
3200 B b1284 t1283
3201 T t1284 o b1284 b4
3202 B b1285 t1284
3203 T t1285 o b1282 b1285
3204 B b1286 t1285
3205 T t1286 o1251 b1092 b1280 b1286 b4
3206 B b1287 t1286
3207 T t1287 o b1287 b4
3208 B b1288 t1287
3209 T t1288 o1091 b1092 b1251 b1288 b4
3210 B b1289 t1288
3211 T t1289 o1090 b1289
3212 B b1290 t1289
3213 P p1299 String cancel1
3214 O o1299 rule p1299
3215 P p1300 String J
3216 O o1300 context_param p1300
3217 T t1300 o1300
3218 B b1300 t1300
3219 T t1301 o b1300 b4
3220 B b1301 t1301
3221 T t1302 o b675 b1301
3222 B b1302 t1302
3223 T t1303 o761 b591 b759 b720 b791
3224 H h1303 x t1303
3225 P p1303 Var x
3226 O o1303 var p1303
3227 T t1304 o1303
3228 C h1304 J t1304
3229 S s1304 t679 h h1303 h1304
3230 G s1304 t715
3231 B b1304 s1304
3232 T t1305 o677 b1304
3233 B b1305 t1305
3234 S s1305 t679 h h1303 h1304
3235 G s1305 t718
3236 B b1306 s1305
3237 T t1306 o677 b1306
3238 B b1307 t1306
3239 S s1307 t679 h h1303 h1304
3240 G s1307 t757
3241 B b1308 s1307
3242 T t1308 o677 b1308
3243 B b1309 t1308
3244 S s1309 t679 h h1303 h1304
3245 G s1309 t760
3246 B b1310 s1309
3247 T t1310 o677 b1310
3248 B b1311 t1310
3249 S s1311 t679 h h1303 h1304
3250 G s1311 t681
3251 B b1312 s1311
3252 T t1312 o677 b1312
3253 B b1313 t1312
3254 S s1313 t684 h h1303 h1304
3255 G s1313 t586
3256 B b1314 s1313
3257 T t1314 o677 b1314
3258 B b1315 t1314
3259 S s1315 t684 h h1303 h1304
3260 G s1315 t762
3261 B b1316 s1315
3262 T t1316 o677 b1316
3263 B b1317 t1316
3264 S s1317 t684 h h1303 h1304
3265 G s1317 t736
3266 B b1318 s1317
3267 T t1318 o677 b1318
3268 B b1319 t1318
3269 S s1319 t684 h h1303 h1304
3270 G s1319 t738
3271 B b1320 s1319
3272 T t1320 o677 b1320
3273 B b1321 t1320
3274 S s1321 t684 h h1303 h1304
3275 G s1321 t764
3276 B b1322 s1321
3277 T t1322 o677 b1322
3278 B b1323 t1322
3279 T t1323 o761 b591 b759 b717 b756
3280 S s1323 t684 h h1303 h1304
3281 G s1323 t1323
3282 B b1324 s1323
3283 T t1324 o677 b1324
3284 B b1325 t1324
3285 T t1325 o676 b1323 b1325
3286 B b1326 t1325
3287 T t1326 o676 b1321 b1326
3288 B b1327 t1326
3289 T t1327 o676 b1319 b1327
3290 B b1328 t1327
3291 T t1328 o676 b1317 b1328
3292 B b1329 t1328
3293 T t1329 o676 b1315 b1329
3294 B b1330 t1329
3295 T t1330 o676 b1313 b1330
3296 B b1331 t1330
3297 T t1331 o676 b1311 b1331
3298 B b1332 t1331
3299 T t1332 o676 b1309 b1332
3300 B b1333 t1332
3301 T t1333 o676 b1307 b1333
3302 B b1334 t1333
3303 T t1334 o676 b1305 b1334
3304 B b1335 t1334
3305 P p1335 String "assertT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenAT autoT"
3306 O o1335 ext_rule p1335
3307 T t1335 o b1322 b4
3308 B b1336 t1335
3309 T t1336 o b1320 b1336
3310 B b1337 t1336
3311 T t1337 o b1318 b1337
3312 B b1338 t1337
3313 T t1338 o b1316 b1338
3314 B b1339 t1338
3315 T t1339 o b1314 b1339
3316 B b1340 t1339
3317 T t1340 o b1312 b1340
3318 B b1341 t1340
3319 T t1341 o b1310 b1341
3320 B b1342 t1341
3321 T t1342 o b1308 b1342
3322 B b1343 t1342
3323 T t1343 o b1306 b1343
3324 B b1344 t1343
3325 T t1344 o b1304 b1344
3326 B b1345 t1344
3327 T t1345 o1095 b1324 b1345
3328 B b1346 t1345
3329 T t1346 o1094 b1346 b4 b1104
3330 B b1347 t1346
3331 T t1347 o596 b585 b980 b720
3332 B b1348 t1347
3333 T t1348 o596 b585 b980 b791
3334 B b1349 t1348
3335 T t1349 o761 b591 b759 b1348 b1349
3336 H h1349 v t1349
3337 S s1349 t684 h h1303 h1304 h1349
3338 G s1349 t1323
3339 B b1350 s1349
3340 T t1350 o1095 b1350 b1345
3341 B b1351 t1350
3342 T t1351 o2 b1347
3343 B b1352 t1351
3344 T t1352 o1094 b1351 b4 b1352
3345 B b1353 t1352
3346 T t1353 o b1353 b4
3347 B b1354 t1353
3348 T t1354 o1093 b1347 b1354
3349 B b1355 t1354
3350 P p1355 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 4 ttca"
3351 O o1355 ext_rule p1355
3352 T t1355 o596 b585 b1036 b717
3353 B b1356 t1355
3354 T t1356 o761 b591 b759 b1356 b1349
3355 H h1356 z t1356
3356 S s1356 t684 h h1303 h1304 h1349 h1356
3357 G s1356 t1323
3358 B b1357 s1356
3359 T t1357 o1095 b1357 b1345
3360 B b1358 t1357
3361 T t1358 o2 b1353
3362 B b1359 t1358
3363 T t1359 o1094 b1358 b4 b1359
3364 B b1360 t1359
3365 T t1360 o b1360 b4
3366 B b1361 t1360
3367 T t1361 o1093 b1353 b1361
3368 B b1362 t1361
3369 P p1362 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 5 ttca"
3370 O o1362 ext_rule p1362
3371 T t1362 o596 b585 b1036 b756
3372 B b1363 t1362
3373 T t1363 o761 b591 b759 b1356 b1363
3374 H h1363 z_1 t1363
3375 S s1363 t684 h h1303 h1304 h1349 h1356 h1363
3376 G s1363 t1323
3377 B b1364 s1363
3378 T t1364 o1095 b1364 b1345
3379 B b1365 t1364
3380 T t1365 o2 b1360
3381 B b1366 t1365
3382 T t1366 o1094 b1365 b4 b1366
3383 B b1367 t1366
3384 T t1367 o b1367 b4
3385 B b1368 t1367
3386 T t1368 o1093 b1360 b1368
3387 B b1369 t1368
3388 P p1369 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"
3389 O o1369 ext_rule p1369
3390 T t1369 o596 b585 b604 b717
3391 B b1370 t1369
3392 T t1370 o596 b585 b604 b756
3393 B b1371 t1370
3394 T t1371 o761 b591 b759 b1370 b1371
3395 H h1371 z_2 t1371
3396 S s1371 t684 h h1303 h1304 h1349 h1356 h1363 h1371
3397 G s1371 t1323
3398 B b1372 s1371
3399 T t1372 o1095 b1372 b1345
3400 B b1373 t1372
3401 T t1373 o2 b1367
3402 B b1374 t1373
3403 T t1374 o1094 b1373 b4 b1374
3404 B b1375 t1374
3405 T t1375 o b1375 b4
3406 B b1376 t1375
3407 T t1376 o1093 b1367 b1376
3408 B b1377 t1376
3409 P p1377 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"
3410 O o1377 ext_rule p1377
3411 T t1377 o761 b591 b759 b717 b1371
3412 H h1377 z_3 t1377
3413 S s1377 t684 h h1303 h1304 h1349 h1356 h1363 h1371 h1377
3414 G s1377 t1323
3415 B b1378 s1377
3416 T t1378 o1095 b1378 b1345
3417 B b1379 t1378
3418 T t1379 o2 b1375
3419 B b1380 t1379
3420 T t1380 o1094 b1379 b4 b1380
3421 B b1381 t1380
3422 T t1381 o b1381 b4
3423 B b1382 t1381
3424 T t1382 o1093 b1375 b1382
3425 B b1383 t1382
3426 P p1383 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"
3427 O o1383 ext_rule p1383
3428 T t1383 o1093 b1381 b4
3429 B b1384 t1383
3430 T t1384 o1383 b1092 b1384 b4 b4
3431 B b1385 t1384
3432 T t1385 o b1385 b4
3433 B b1386 t1385
3434 T t1386 o1377 b1092 b1383 b1386 b4
3435 B b1387 t1386
3436 T t1387 o b1387 b4
3437 B b1388 t1387
3438 T t1388 o1369 b1092 b1377 b1388 b4
3439 B b1389 t1388
3440 T t1389 o b1389 b4
3441 B b1390 t1389
3442 T t1390 o1362 b1092 b1369 b1390 b4
3443 B b1391 t1390
3444 T t1391 o b1391 b4
3445 B b1392 t1391
3446 T t1392 o1355 b1092 b1362 b1392 b4
3447 B b1393 t1392
3448 T t1393 o b1393 b4
3449 B b1394 t1393
3450 P p1394 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 3 ttca"
3451 O o1394 ext_rule p1394
3452 H h1394 v t1303
3453 H h1395 v_1 t1349
3454 S s1395 t684 h h1394 h1395
3455 G s1395 t1323
3456 B b1395 s1395
3457 S s1396 t684 h
3458 G s1396 t1303
3459 B b1396 s1396
3460 T t1396 o b1396 b4
3461 B b1397 t1396
3462 T t1397 o b764 b1397
3463 B b1398 t1397
3464 T t1398 o b738 b1398
3465 B b1399 t1398
3466 T t1399 o b736 b1399
3467 B b1400 t1399
3468 T t1400 o b762 b1400
3469 B b1401 t1400
3470 T t1401 o b699 b1401
3471 B b1402 t1401
3472 T t1402 o b681 b1402
3473 B b1403 t1402
3474 T t1403 o b760 b1403
3475 B b1404 t1403
3476 T t1404 o b757 b1404
3477 B b1405 t1404
3478 T t1405 o b718 b1405
3479 B b1406 t1405
3480 T t1406 o b715 b1406
3481 B b1407 t1406
3482 T t1407 o1095 b1395 b1407
3483 B b1408 t1407
3484 S s1408 t684 h h1394
3485 G s1408 t1323
3486 B b1409 s1408
3487 T t1409 o1095 b1409 b1407
3488 B b1410 t1409
3489 S s1410 t684 h
3490 G s1410 t1323
3491 B b1411 s1410
3492 T t1411 o1095 b1411 b1407
3493 B b1412 t1411
3494 T t1412 o1094 b1412 b4 b1104
3495 B b1413 t1412
3496 T t1413 o2 b1413
3497 B b1414 t1413
3498 T t1414 o1094 b1410 b4 b1414
3499 B b1415 t1414
3500 T t1415 o2 b1415
3501 B b1416 t1415
3502 T t1416 o1094 b1408 b4 b1416
3503 B b1417 t1416
3504 S s1417 t684 h h1394 h1395 h1356
3505 G s1417 t1323
3506 B b1418 s1417
3507 T t1418 o1095 b1418 b1407
3508 B b1419 t1418
3509 T t1419 o2 b1417
3510 B b1420 t1419
3511 T t1420 o1094 b1419 b4 b1420
3512 B b1421 t1420
3513 T t1421 o b1421 b4
3514 B b1422 t1421
3515 T t1422 o1093 b1417 b1422
3516 B b1423 t1422
3517 P p1423 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 4 ttca"
3518 O o1423 ext_rule p1423
3519 S s1423 t684 h h1394 h1395 h1356 h1363
3520 G s1423 t1323
3521 B b1424 s1423
3522 T t1424 o1095 b1424 b1407
3523 B b1425 t1424
3524 T t1425 o2 b1421
3525 B b1426 t1425
3526 T t1426 o1094 b1425 b4 b1426
3527 B b1427 t1426
3528 T t1427 o b1427 b4
3529 B b1428 t1427
3530 T t1428 o1093 b1421 b1428
3531 B b1429 t1428
3532 P p1429 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 ttca"
3533 O o1429 ext_rule p1429
3534 S s1429 t684 h h1394 h1395 h1356 h1363 h1371
3535 G s1429 t1323
3536 B b1430 s1429
3537 T t1430 o1095 b1430 b1407
3538 B b1431 t1430
3539 T t1431 o2 b1427
3540 B b1432 t1431
3541 T t1432 o1094 b1431 b4 b1432
3542 B b1433 t1432
3543 T t1433 o b1433 b4
3544 B b1434 t1433
3545 T t1434 o1093 b1427 b1434
3546 B b1435 t1434
3547 P p1435 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 6 ttca"
3548 O o1435 ext_rule p1435
3549 S s1435 t684 h h1394 h1395 h1356 h1363 h1371 h1377
3550 G s1435 t1323
3551 B b1436 s1435
3552 T t1436 o1095 b1436 b1407
3553 B b1437 t1436
3554 T t1437 o2 b1433
3555 B b1438 t1437
3556 T t1438 o1094 b1437 b4 b1438
3557 B b1439 t1438
3558 T t1439 o b1439 b4
3559 B b1440 t1439
3560 T t1440 o1093 b1433 b1440
3561 B b1441 t1440
3562 P p1441 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 7 ttca"
3563 O o1441 ext_rule p1441
3564 T t1441 o1093 b1439 b4
3565 B b1442 t1441
3566 T t1442 o1441 b1092 b1442 b4 b4
3567 B b1443 t1442
3568 T t1443 o b1443 b4
3569 B b1444 t1443
3570 T t1444 o1435 b1092 b1441 b1444 b4
3571 B b1445 t1444
3572 T t1445 o b1445 b4
3573 B b1446 t1445
3574 T t1446 o1429 b1092 b1435 b1446 b4
3575 B b1447 t1446
3576 T t1447 o b1447 b4
3577 B b1448 t1447
3578 T t1448 o1423 b1092 b1429 b1448 b4
3579 B b1449 t1448
3580 T t1449 o b1449 b4
3581 B b1450 t1449
3582 T t1450 o1394 b1092 b1423 b1450 b4
3583 B b1451 t1450
3584 T t1451 o b1451 b4
3585 B b1452 t1451
3586 T t1452 o1335 b1092 b1355 b1394 b1452
3587 B b1453 t1452
3588 T t1453 o1090 b1453
3589 B b1454 t1453
3590 T t1454 o1299 b1302 b1335 b1454 b4
3591 B b1455 t1454
3592 P p1458 String cancel2
3593 O o1458 rule p1458
3594 H h1458 x t793
3595 S s1458 t679 h h1458 h1304
3596 G s1458 t715
3597 B b1458 s1458
3598 T t1458 o677 b1458
3599 B b1459 t1458
3600 S s1459 t679 h h1458 h1304
3601 G s1459 t718
3602 B b1460 s1459
3603 T t1460 o677 b1460
3604 B b1461 t1460
3605 S s1461 t679 h h1458 h1304
3606 G s1461 t757
3607 B b1462 s1461
3608 T t1462 o677 b1462
3609 B b1463 t1462
3610 S s1463 t679 h h1458 h1304
3611 G s1463 t760
3612 B b1464 s1463
3613 T t1464 o677 b1464
3614 B b1465 t1464
3615 S s1465 t679 h h1458 h1304
3616 G s1465 t681
3617 B b1466 s1465
3618 T t1466 o677 b1466
3619 B b1467 t1466
3620 S s1467 t684 h h1458 h1304
3621 G s1467 t586
3622 B b1468 s1467
3623 T t1468 o677 b1468
3624 B b1469 t1468
3625 S s1469 t684 h h1458 h1304
3626 G s1469 t762
3627 B b1470 s1469
3628 T t1470 o677 b1470
3629 B b1471 t1470
3630 S s1471 t684 h h1458 h1304
3631 G s1471 t736
3632 B b1472 s1471
3633 T t1472 o677 b1472
3634 B b1473 t1472
3635 S s1473 t684 h h1458 h1304
3636 G s1473 t738
3637 B b1474 s1473
3638 T t1474 o677 b1474
3639 B b1475 t1474
3640 S s1475 t684 h h1458 h1304
3641 G s1475 t764
3642 B b1476 s1475
3643 T t1476 o677 b1476
3644 B b1477 t1476
3645 S s1477 t684 h h1458 h1304
3646 G s1477 t766
3647 B b1478 s1477
3648 T t1478 o677 b1478
3649 B b1479 t1478
3650 T t1479 o676 b1477 b1479
3651 B b1480 t1479
3652 T t1480 o676 b1475 b1480
3653 B b1481 t1480
3654 T t1481 o676 b1473 b1481
3655 B b1482 t1481
3656 T t1482 o676 b1471 b1482
3657 B b1483 t1482
3658 T t1483 o676 b1469 b1483
3659 B b1484 t1483
3660 T t1484 o676 b1467 b1484
3661 B b1485 t1484
3662 T t1485 o676 b1465 b1485
3663 B b1486 t1485
3664 T t1486 o676 b1463 b1486
3665 B b1487 t1486
3666 T t1487 o676 b1461 b1487
3667 B b1488 t1487
3668 T t1488 o676 b1459 b1488
3669 B b1489 t1488
3670 P p1489 String "assertT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}} >> thenAT autoT"
3671 O o1489 ext_rule p1489
3672 T t1489 o b1476 b4
3673 B b1490 t1489
3674 T t1490 o b1474 b1490
3675 B b1491 t1490
3676 T t1491 o b1472 b1491
3677 B b1492 t1491
3678 T t1492 o b1470 b1492
3679 B b1493 t1492
3680 T t1493 o b1468 b1493
3681 B b1494 t1493
3682 T t1494 o b1466 b1494
3683 B b1495 t1494
3684 T t1495 o b1464 b1495
3685 B b1496 t1495
3686 T t1496 o b1462 b1496
3687 B b1497 t1496
3688 T t1497 o b1460 b1497
3689 B b1498 t1497
3690 T t1498 o b1458 b1498
3691 B b1499 t1498
3692 T t1499 o1095 b1478 b1499
3693 B b1500 t1499
3694 T t1500 o1094 b1500 b4 b1104
3695 B b1501 t1500
3696 T t1501 o609 b585 b756
3697 B b1502 t1501
3698 T t1502 o596 b585 b791 b1502
3699 B b1503 t1502
3700 T t1503 o596 b585 b792 b1502
3701 B b1504 t1503
3702 T t1504 o761 b591 b759 b1503 b1504
3703 H h1504 v t1504
3704 S s1504 t684 h h1458 h1304 h1504
3705 G s1504 t766
3706 B b1505 s1504
3707 T t1505 o1095 b1505 b1499
3708 B b1506 t1505
3709 T t1506 o2 b1501
3710 B b1507 t1506
3711 T t1507 o1094 b1506 b4 b1507
3712 B b1508 t1507
3713 T t1508 o b1508 b4
3714 B b1509 t1508
3715 T t1509 o1093 b1501 b1509
3716 B b1510 t1509
3717 P p1510 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 4 ttca"
3718 O o1510 ext_rule p1510
3719 T t1510 o596 b585 b756 b1502
3720 B b1511 t1510
3721 T t1511 o596 b585 b714 b1511
3722 B b1512 t1511
3723 T t1512 o761 b591 b759 b1512 b1504
3724 H h1512 z t1512
3725 S s1512 t684 h h1458 h1304 h1504 h1512
3726 G s1512 t766
3727 B b1513 s1512
3728 T t1513 o1095 b1513 b1499
3729 B b1514 t1513
3730 T t1514 o2 b1508
3731 B b1515 t1514
3732 T t1515 o1094 b1514 b4 b1515
3733 B b1516 t1515
3734 T t1516 o b1516 b4
3735 B b1517 t1516
3736 T t1517 o1093 b1508 b1517
3737 B b1518 t1517
3738 P p1518 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 5 ttca"
3739 O o1518 ext_rule p1518
3740 T t1518 o596 b585 b717 b1511
3741 B b1519 t1518
3742 T t1519 o761 b591 b759 b1512 b1519
3743 H h1519 z_1 t1519
3744 S s1519 t684 h h1458 h1304 h1504 h1512 h1519
3745 G s1519 t766
3746 B b1520 s1519
3747 T t1520 o1095 b1520 b1499
3748 B b1521 t1520
3749 T t1521 o2 b1516
3750 B b1522 t1521
3751 T t1522 o1094 b1521 b4 b1522
3752 B b1523 t1522
3753 T t1523 o b1523 b4
3754 B b1524 t1523
3755 T t1524 o1093 b1516 b1524
3756 B b1525 t1524
3757 P p1525 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 6 ttca"
3758 O o1525 ext_rule p1525
3759 T t1525 o596 b585 b714 b604
3760 B b1526 t1525
3761 T t1526 o596 b585 b717 b604
3762 B b1527 t1526
3763 T t1527 o761 b591 b759 b1526 b1527
3764 H h1527 z_2 t1527
3765 S s1527 t684 h h1458 h1304 h1504 h1512 h1519 h1527
3766 G s1527 t766
3767 B b1528 s1527
3768 T t1528 o1095 b1528 b1499
3769 B b1529 t1528
3770 T t1529 o2 b1523
3771 B b1530 t1529
3772 T t1530 o1094 b1529 b4 b1530
3773 B b1531 t1530
3774 T t1531 o b1531 b4
3775 B b1532 t1531
3776 T t1532 o1093 b1523 b1532
3777 B b1533 t1532
3778 P p1533 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's1; id{'g}}; 's1} >> 7 ttca"
3779 O o1533 ext_rule p1533
3780 T t1533 o761 b591 b759 b714 b1527
3781 H h1533 z_3 t1533
3782 S s1533 t684 h h1458 h1304 h1504 h1512 h1519 h1527 h1533
3783 G s1533 t766
3784 B b1534 s1533
3785 T t1534 o1095 b1534 b1499
3786 B b1535 t1534
3787 T t1535 o2 b1531
3788 B b1536 t1535
3789 T t1536 o1094 b1535 b4 b1536
3790 B b1537 t1536
3791 T t1537 o b1537 b4
3792 B b1538 t1537
3793 T t1538 o1093 b1531 b1538
3794 B b1539 t1538
3795 P p1539 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's2; id{'g}}; 's2} >> 8 ttca"
3796 O o1539 ext_rule p1539
3797 T t1539 o1093 b1537 b4
3798 B b1540 t1539
3799 T t1540 o1539 b1092 b1540 b4 b4
3800 B b1541 t1540
3801 T t1541 o b1541 b4
3802 B b1542 t1541
3803 T t1542 o1533 b1092 b1539 b1542 b4
3804 B b1543 t1542
3805 T t1543 o b1543 b4
3806 B b1544 t1543
3807 T t1544 o1525 b1092 b1533 b1544 b4
3808 B b1545 t1544
3809 T t1545 o b1545 b4
3810 B b1546 t1545
3811 T t1546 o1518 b1092 b1525 b1546 b4
3812 B b1547 t1546
3813 T t1547 o b1547 b4
3814 B b1548 t1547
3815 T t1548 o1510 b1092 b1518 b1548 b4
3816 B b1549 t1548
3817 T t1549 o b1549 b4
3818 B b1550 t1549
3819 P p1550 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 3 ttca"
3820 O o1550 ext_rule p1550
3821 H h1550 v t793
3822 H h1551 v_1 t1504
3823 S s1551 t684 h h1550 h1551
3824 G s1551 t766
3825 B b1551 s1551
3826 T t1551 o b793 b4
3827 B b1552 t1551
3828 T t1552 o b764 b1552
3829 B b1553 t1552
3830 T t1553 o b738 b1553
3831 B b1554 t1553
3832 T t1554 o b736 b1554
3833 B b1555 t1554
3834 T t1555 o b762 b1555
3835 B b1556 t1555
3836 T t1556 o b699 b1556
3837 B b1557 t1556
3838 T t1557 o b681 b1557
3839 B b1558 t1557
3840 T t1558 o b760 b1558
3841 B b1559 t1558
3842 T t1559 o b757 b1559
3843 B b1560 t1559
3844 T t1560 o b718 b1560
3845 B b1561 t1560
3846 T t1561 o b715 b1561
3847 B b1562 t1561
3848 T t1562 o1095 b1551 b1562
3849 B b1563 t1562
3850 S s1563 t684 h h1550
3851 G s1563 t766
3852 B b1564 s1563
3853 T t1564 o1095 b1564 b1562
3854 B b1565 t1564
3855 T t1565 o1095 b766 b1562
3856 B b1566 t1565
3857 T t1566 o1094 b1566 b4 b1104
3858 B b1567 t1566
3859 T t1567 o2 b1567
3860 B b1568 t1567
3861 T t1568 o1094 b1565 b4 b1568
3862 B b1569 t1568
3863 T t1569 o2 b1569
3864 B b1570 t1569
3865 T t1570 o1094 b1563 b4 b1570
3866 B b1571 t1570
3867 S s1571 t684 h h1550 h1551 h1512
3868 G s1571 t766
3869 B b1572 s1571
3870 T t1572 o1095 b1572 b1562
3871 B b1573 t1572
3872 T t1573 o2 b1571
3873 B b1574 t1573
3874 T t1574 o1094 b1573 b4 b1574
3875 B b1575 t1574
3876 T t1575 o b1575 b4
3877 B b1576 t1575
3878 T t1576 o1093 b1571 b1576
3879 B b1577 t1576
3880 P p1577 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 4 ttca"
3881 O o1577 ext_rule p1577
3882 S s1577 t684 h h1550 h1551 h1512 h1519
3883 G s1577 t766
3884 B b1578 s1577
3885 T t1578 o1095 b1578 b1562
3886 B b1579 t1578
3887 T t1579 o2 b1575
3888 B b1580 t1579
3889 T t1580 o1094 b1579 b4 b1580
3890 B b1581 t1580
3891 T t1581 o b1581 b4
3892 B b1582 t1581
3893 T t1582 o1093 b1575 b1582
3894 B b1583 t1582
3895 P p1583 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 5 ttca"
3896 O o1583 ext_rule p1583
3897 S s1583 t684 h h1550 h1551 h1512 h1519 h1527
3898 G s1583 t766
3899 B b1584 s1583
3900 T t1584 o1095 b1584 b1562
3901 B b1585 t1584
3902 T t1585 o2 b1581
3903 B b1586 t1585
3904 T t1586 o1094 b1585 b4 b1586
3905 B b1587 t1586
3906 T t1587 o b1587 b4
3907 B b1588 t1587
3908 T t1588 o1093 b1581 b1588
3909 B b1589 t1588
3910 P p1589 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's1; id{'g}}; 's1} >> 6 ttca"
3911 O o1589 ext_rule p1589
3912 S s1589 t684 h h1550 h1551 h1512 h1519 h1527 h1533
3913 G s1589 t766
3914 B b1590 s1589
3915 T t1590 o1095 b1590 b1562
3916 B b1591 t1590
3917 T t1591 o2 b1587
3918 B b1592 t1591
3919 T t1592 o1094 b1591 b4 b1592
3920 B b1593 t1592
3921 T t1593 o b1593 b4
3922 B b1594 t1593
3923 T t1594 o1093 b1587 b1594
3924 B b1595 t1594
3925 P p1595 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's2; id{'g}}; 's2} >> 7 ttca"
3926 O o1595 ext_rule p1595
3927 T t1595 o1093 b1593 b4
3928 B b1596 t1595
3929 T t1596 o1595 b1092 b1596 b4 b4
3930 B b1597 t1596
3931 T t1597 o b1597 b4
3932 B b1598 t1597
3933 T t1598 o1589 b1092 b1595 b1598 b4
3934 B b1599 t1598
3935 T t1599 o b1599 b4
3936 B b1600 t1599
3937 T t1600 o1583 b1092 b1589 b1600 b4
3938 B b1601 t1600
3939 T t1601 o b1601 b4
3940 B b1602 t1601
3941 T t1602 o1577 b1092 b1583 b1602 b4
3942 B b1603 t1602
3943 T t1603 o b1603 b4
3944 B b1604 t1603
3945 T t1604 o1550 b1092 b1577 b1604 b4
3946 B b1605 t1604
3947 T t1605 o b1605 b4
3948 B b1606 t1605
3949 T t1606 o1489 b1092 b1510 b1550 b1606
3950 B b1607 t1606
3951 T t1607 o1090 b1607
3952 B b1608 t1607
3953 T t1608 o1458 b1302 b1489 b1608 b4
3954 B b1609 t1608
3955 NOcaml!str_let str_let str_let Ocaml
3956 NOcaml!patt_var patt_var patt_var Ocaml
3957 NOcaml!patt_done patt_done patt_done Ocaml
3958 NOcaml!fun fun fun Ocaml
3959 NOcaml!patt_if patt_if patt_if Ocaml
3960 NOcaml!patt_body patt_body patt_body Ocaml
3961 NOcaml!let let let Ocaml
3962 NOcaml!patt_tuple patt_tuple patt_tuple Ocaml
3963 NOcaml!patt_tuple_arg patt_tuple_arg patt_tuple_arg Ocaml
3964 NOcaml!patt_tuple_end patt_tuple_end patt_tuple_end Ocaml
3965 NOcaml!patt_in patt_in patt_in Ocaml
3966 NOcaml!apply apply apply Ocaml
3967 NOcaml!lid lid lid Ocaml
3968 O o1632 lid p1299
3969 T t1632 o1632
3970 B b1632 t1632
3971 P p1634 Var j
3972 O o1634 var p1634
3973 T t1634 o1634
3974 B b1634 t1634
3975 P p1637 Var k
3976 O o1637 var p1637
3977 T t1637 o1637
3978 B b1637 t1637
3979 P p1640 Var p
3980 O o1640 var p1640
3981 T t1640 o1640
3982 B b1640 t1640
3983 NOcaml!proj proj proj Ocaml
3984 O o1653 uid p539
3985 T t1653 o1653
3986 B b1653 t1653
3987 P p1655 String hyp_indices
3988 O o1655 lid p1655
3989 T t1655 o1655
3990 B b1655 t1655
3991 P p1660 Var i
3992 O o1660 var p1660
3993 T t1660 o1660
3994 B b1660 t1660
3995 O o1699 lid p1458
3996 T t1699 o1699
3997 B b1699 t1699
3998 P p1739 String unique_id1
3999 O o1739 rule p1739
4000 P p1740 Var e2
4001 O o1740 var p1740
4002 T t1740 o1740
4003 B b1740 t1740
4004 T t1741 o700 b1740
4005 S s1741 t679 h
4006 G s1741 t1741
4007 B b1741 s1741
4008 T t1742 o677 b1741
4009 B b1742 t1742
4010 T t1743 o736 b1740 b591
4011 S s1743 t684 h
4012 G s1743 t1743
4013 B b1743 s1743
4014 T t1744 o677 b1743
4015 B b1744 t1744
4016 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4017 NCzf_itt_dall!dall dall dall Czf_itt_dall
4018 O o1744 dall
4019 T t1745 o596 b585 b1740 b815
4020 B b1745 t1745
4021 T t1746 o761 b591 b759 b1745 b815
4022 B b1746 t1746 s
4023 T t1747 o1744 b591 b1746
4024 S s1747 t684 h
4025 G s1747 t1747
4026 B b1747 s1747
4027 T t1748 o677 b1747
4028 B b1748 t1748
4029 T t1749 o761 b591 b759 b1740 b604
4030 S s1749 t684 h
4031 G s1749 t1749
4032 B b1749 s1749
4033 T t1750 o677 b1749
4034 B b1750 t1750
4035 T t1751 o676 b1748 b1750
4036 B b1751 t1751
4037 T t1752 o676 b1744 b1751
4038 B b1752 t1752
4039 T t1753 o676 b763 b1752
4040 B b1753 t1753
4041 T t1754 o676 b700 b1753
4042 B b1754 t1754
4043 T t1755 o676 b682 b1754
4044 B b1755 t1755
4045 T t1756 o676 b761 b1755
4046 B b1756 t1756
4047 T t1757 o676 b1742 b1756
4048 B b1757 t1757
4049 P p1757 String "assumT 7 thenT withT << id{'g} >> (dT 2) ttca"
4050 O o1757 ext_rule p1757
4051 T t1758 o b1747 b4
4052 B b1758 t1758
4053 T t1759 o b1743 b1758
4054 B b1759 t1759
4055 T t1760 o b762 b1759
4056 B b1760 t1760
4057 T t1761 o b699 b1760
4058 B b1761 t1761
4059 T t1762 o b681 b1761
4060 B b1762 t1762
4061 T t1763 o b760 b1762
4062 B b1763 t1763
4063 T t1764 o b1741 b1763
4064 B b1764 t1764
4065 T t1765 o1095 b1749 b1764
4066 B b1765 t1765
4067 T t1766 o1094 b1765 b4 b1104
4068 B b1766 t1766
4069 P p1766 String wf
4070 O o1766 tactic_arg p1766
4071 H h1766 v t1747
4072 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
4073 O o1767 fun_prop
4074 P p1767 Var w
4075 O o1768 var p1767
4076 T t1768 o1768
4077 B b1768 t1768
4078 T t1769 o596 b585 b1740 b1768
4079 B b1769 t1769
4080 T t1770 o761 b591 b759 b1769 b1768
4081 B b1770 t1770 w
4082 T t1771 o1767 b1770
4083 S s1771 t684 h h1766
4084 G s1771 t1771
4085 B b1771 s1771
4086 T t1772 o1095 b1771 b1764
4087 B b1772 t1772
4088 S s1772 t684 h h1766
4089 G s1772 t1749
4090 B b1773 s1772
4091 T t1773 o1095 b1773 b1764
4092 B b1774 t1773
4093 NSummary!arg_named arg_named arg_named Summary
4094 P p1774 String with
4095 O o1774 arg_named p1774
4096 NSummary!arg_term_list arg_term_list arg_term_list Summary
4097 O o1775 arg_term_list
4098 T t1775 o b604 b4
4099 B b1775 t1775
4100 T t1776 o1775 b1775
4101 B b1776 t1776
4102 T t1777 o1774 b1776
4103 B b1777 t1777
4104 T t1778 o b1777 b4
4105 B b1778 t1778
4106 T t1779 o2 b1766
4107 B b1779 t1779
4108 T t1780 o1094 b1774 b1778 b1779
4109 B b1780 t1780
4110 T t1781 o2 b1780
4111 B b1781 t1781
4112 T t1782 o1766 b1772 b4 b1781
4113 B b1782 t1782
4114 T t1783 o596 b585 b1740 b604
4115 B b1783 t1783
4116 T t1784 o761 b591 b759 b1783 b604
4117 H h1784 w t1784
4118 S s1784 t684 h h1766 h1784
4119 G s1784 t1749
4120 B b1784 s1784
4121 T t1785 o1095 b1784 b1764
4122 B b1785 t1785
4123 T t1786 o1094 b1785 b4 b1781
4124 B b1786 t1786
4125 T t1787 o b1786 b4
4126 B b1787 t1787
4127 T t1788 o b1782 b1787
4128 B b1788 t1788
4129 T t1789 o1093 b1766 b1788
4130 B b1789 t1789
4131 P p1789 String "rwh unfold_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
4132 O o1789 ext_rule p1789
4133 H h1789 s1 t1106
4134 H h1790 s2 t1106
4135 NCzf_itt_eq!equal equal1790 equal Czf_itt_eq
4136 O o1790 equal1790
4137 T t1790 o1790 b714 b717
4138 H h1791 x t1790
4139 T t1791 o596 b585 b1740 b714
4140 B b1791 t1791
4141 T t1792 o761 b591 b759 b1791 b714
4142 H h1792 x_1 t1792
4143 T t1793 o596 b585 b1740 b717
4144 B b1793 t1793
4145 T t1794 o761 b591 b759 b1793 b717
4146 S s1794 t684 h h1766 h1789 h1790 h1791 h1792
4147 G s1794 t1794
4148 B b1794 s1794
4149 T t1795 o1095 b1794 b1764
4150 B b1795 t1795
4151 B b1796 t1792
4152 B b1797 t1794
4153 T t1797 o1117 b1796 b1797
4154 S s1797 t684 h h1766 h1789 h1790 h1791
4155 G s1797 t1797
4156 B b1798 s1797
4157 T t1798 o1095 b1798 b1764
4158 B b1799 t1798
4159 B b1800 t1790
4160 B b1801 t1797
4161 T t1801 o1117 b1800 b1801
4162 S s1801 t684 h h1766 h1789 h1790
4163 G s1801 t1801
4164 B b1802 s1801
4165 T t1802 o1095 b1802 b1764
4166 B b1803 t1802
4167 B b1804 t1801 s2
4168 T t1804 o1129 b1130 b1804
4169 S s1804 t684 h h1766 h1789
4170 G s1804 t1804
4171 B b1805 s1804
4172 T t1805 o1095 b1805 b1764
4173 B b1806 t1805
4174 B b1807 t1804 s1
4175 T t1807 o1129 b1130 b1807
4176 S s1807 t684 h h1766
4177 G s1807 t1807
4178 B b1808 s1807
4179 T t1808 o1095 b1808 b1764
4180 B b1809 t1808
4181 T t1809 o2 b1782
4182 B b1810 t1809
4183 T t1810 o1766 b1809 b4 b1810
4184 B b1811 t1810
4185 T t1811 o2 b1811
4186 B b1812 t1811
4187 T t1812 o1094 b1806 b4 b1812
4188 B b1813 t1812
4189 T t1813 o2 b1813
4190 B b1814 t1813
4191 T t1814 o1094 b1803 b4 b1814
4192 B b1815 t1814
4193 T t1815 o2 b1815
4194 B b1816 t1815
4195 T t1816 o1094 b1799 b4 b1816
4196 B b1817 t1816
4197 T t1817 o2 b1817
4198 B b1818 t1817
4199 T t1818 o1094 b1795 b4 b1818
4200 B b1819 t1818
4201 T t1819 o b1819 b4
4202 B b1820 t1819
4203 T t1820 o1093 b1782 b1820
4204 B b1821 t1820
4205 P p1821 String "equivTransT << op{'g; 'e2; 's2} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
4206 O o1821 ext_rule p1821
4207 T t1821 o700 b1791
4208 B b1822 t1821
4209 B b1823 t715
4210 T t1823 o1151 b1822 b1823
4211 B b1824 t1823
4212 T t1824 o1151 b1152 b1824
4213 B b1825 t1824
4214 T t1825 o1151 b1151 b1825
4215 B b1826 t1825
4216 T t1826 o736 b1791 b591
4217 B b1827 t1826
4218 B b1828 t736
4219 T t1828 o1151 b1827 b1828
4220 B b1829 t1828
4221 T t1829 o1151 b1826 b1829
4222 B b1830 t1829
4223 T t1830 o1161 b1791 b714
4224 B b1831 t1830
4225 T t1831 o736 b1831 b759
4226 B b1832 t1831
4227 T t1832 o1151 b1830 b1832
4228 H h1832 x_1 t1832
4229 T t1833 o736 b1793 b591
4230 S s1833 t684 h h1766 h1789 h1790 h1791 h1832
4231 G s1833 t1833
4232 B b1833 s1833
4233 T t1834 o1095 b1833 b1764
4234 B b1834 t1834
4235 S s1834 t684 h h1766 h1789 h1790 h1791 h1792
4236 G s1834 t1833
4237 B b1835 s1834
4238 T t1835 o1095 b1835 b1764
4239 B b1836 t1835
4240 T t1836 o2 b1819
4241 B b1837 t1836
4242 T t1837 o1094 b1836 b4 b1837
4243 B b1838 t1837
4244 T t1838 o2 b1838
4245 B b1839 t1838
4246 T t1839 o1094 b1834 b4 b1839
4247 B b1840 t1839
4248 T t1840 o761 b591 b759 b1791 b1793
4249 H h1840 u t1840
4250 T t1841 o761 b591 b759 b1793 b714
4251 H h1841 v_1 t1841
4252 S s1841 t684 h h1766 h1789 h1790 h1791 h1832 h1840 h1841
4253 G s1841 t1794
4254 B b1841 s1841
4255 T t1842 o1095 b1841 b1764
4256 B b1842 t1842
4257 S s1842 t684 h h1766 h1789 h1790 h1791 h1792 h1840 h1841
4258 G s1842 t1794
4259 B b1843 s1842
4260 T t1843 o1095 b1843 b1764
4261 B b1844 t1843
4262 T t1844 o1094 b1844 b4 b1837
4263 B b1845 t1844
4264 T t1845 o2 b1845
4265 B b1846 t1845
4266 T t1846 o1094 b1842 b4 b1846
4267 B b1847 t1846
4268 T t1847 o b1847 b4
4269 B b1848 t1847
4270 T t1848 o b1840 b1848
4271 B b1849 t1848
4272 T t1849 o1093 b1819 b1849
4273 B b1850 t1849
4274 P p1850 String "autoT thenT setSubstT << equal{'s1; 's2} >> 11 ttca"
4275 O o1850 ext_rule p1850
4276 T t1850 o1093 b1840 b4
4277 B b1851 t1850
4278 T t1851 o1850 b1092 b1851 b4 b4
4279 B b1852 t1851
4280 P p1852 String "equivTransT << 's2 >> 8 thenT autoT"
4281 O o1852 ext_rule p1852
4282 H h1852 y_2 t700
4283 H h1853 y_1 t760
4284 H h1854 y_3 t1821
4285 H h1855 z_1 t715
4286 H h1856 y t1826
4287 H h1857 z_2 t736
4288 H h1858 z t1831
4289 S s1858 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1854 h1855 h1856 h1857 h1858 h1840 h1841
4290 G s1858 t738
4291 B b1858 s1858
4292 T t1858 o1095 b1858 b1764
4293 B b1859 t1858
4294 S s1859 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1854 h1855 h1856 h1857 h1858 h1840 h1841
4295 G s1859 t1833
4296 B b1860 s1859
4297 T t1860 o1095 b1860 b1764
4298 B b1861 t1860
4299 P p1861 String d_auto
4300 O o1861 arg_named p1861
4301 NSummary!arg_bool arg_bool arg_bool Summary
4302 P p1862 String true
4303 O o1862 arg_bool p1862
4304 T t1862 o1862
4305 B b1862 t1862
4306 T t1863 o1861 b1862
4307 B b1863 t1863
4308 T t1864 o b1863 b4
4309 B b1864 t1864
4310 H h1864 z_3 t1823
4311 S s1864 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1864 h1856 h1857 h1858 h1840 h1841
4312 G s1864 t1833
4313 B b1865 s1864
4314 T t1865 o1095 b1865 b1764
4315 B b1866 t1865
4316 H h1866 z_1 t1824
4317 S s1866 t684 h h1766 h1789 h1790 h1791 h1852 h1866 h1856 h1857 h1858 h1840 h1841
4318 G s1866 t1833
4319 B b1867 s1866
4320 T t1867 o1095 b1867 b1764
4321 B b1868 t1867
4322 H h1868 y_1 t1825
4323 S s1868 t684 h h1766 h1789 h1790 h1791 h1868 h1856 h1857 h1858 h1840 h1841
4324 G s1868 t1833
4325 B b1869 s1868
4326 T t1869 o1095 b1869 b1764
4327 B b1870 t1869
4328 H h1870 z_1 t1828
4329 S s1870 t684 h h1766 h1789 h1790 h1791 h1868 h1870 h1858 h1840 h1841
4330 G s1870 t1833
4331 B b1871 s1870
4332 T t1871 o1095 b1871 b1764
4333 B b1872 t1871
4334 H h1872 y t1829
4335 S s1872 t684 h h1766 h1789 h1790 h1791 h1872 h1858 h1840 h1841
4336 G s1872 t1833
4337 B b1873 s1872
4338 T t1873 o1095 b1873 b1764
4339 B b1874 t1873
4340 S s1874 t684 h h1766 h1789 h1790 h1791 h1832 h1840 h1841
4341 G s1874 t1833
4342 B b1875 s1874
4343 T t1875 o1095 b1875 b1764
4344 B b1876 t1875
4345 T t1876 o2 b1847
4346 B b1877 t1876
4347 T t1877 o1094 b1876 b4 b1877
4348 B b1878 t1877
4349 T t1878 o2 b1878
4350 B b1879 t1878
4351 T t1879 o1094 b1874 b4 b1879
4352 B b1880 t1879
4353 T t1880 o2 b1880
4354 B b1881 t1880
4355 T t1881 o1094 b1872 b4 b1881
4356 B b1882 t1881
4357 T t1882 o2 b1882
4358 B b1883 t1882
4359 T t1883 o1094 b1870 b4 b1883
4360 B b1884 t1883
4361 T t1884 o2 b1884
4362 B b1885 t1884
4363 T t1885 o1094 b1868 b4 b1885
4364 B b1886 t1885
4365 T t1886 o2 b1886
4366 B b1887 t1886
4367 T t1887 o1094 b1866 b4 b1887
4368 B b1888 t1887
4369 T t1888 o2 b1888
4370 B b1889 t1888
4371 T t1889 o1094 b1861 b1864 b1889
4372 B b1890 t1889
4373 T t1890 o2 b1890
4374 B b1891 t1890
4375 T t1891 o1094 b1859 b4 b1891
4376 B b1892 t1891
4377 T t1892 o b1892 b4
4378 B b1893 t1892
4379 T t1893 o1093 b1847 b1893
4380 B b1894 t1893
4381 P p1894 String "setSubstT << equal{'s1; 's2} >> 11 ttca"
4382 O o1894 ext_rule p1894
4383 T t1894 o1093 b1892 b4
4384 B b1895 t1894
4385 T t1895 o1894 b1092 b1895 b4 b4
4386 B b1896 t1895
4387 T t1896 o b1896 b4
4388 B b1897 t1896
4389 T t1897 o1852 b1092 b1894 b1897 b4
4390 B b1898 t1897
4391 T t1898 o b1898 b4
4392 B b1899 t1898
4393 T t1899 o b1852 b1899
4394 B b1900 t1899
4395 T t1900 o1821 b1092 b1850 b1900 b4
4396 B b1901 t1900
4397 T t1901 o b1901 b4
4398 B b1902 t1901
4399 T t1902 o1789 b1092 b1821 b1902 b4
4400 B b1903 t1902
4401 P p1903 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'e2; id{'g}}; 'e2} >> 3 ttca"
4402 O o1903 ext_rule p1903
4403 T t1903 o1093 b1786 b4
4404 B b1904 t1903
4405 T t1904 o1903 b1092 b1904 b4 b4
4406 B b1905 t1904
4407 T t1905 o b1905 b4
4408 B b1906 t1905
4409 T t1906 o b1903 b1906
4410 B b1907 t1906
4411 T t1907 o1757 b1092 b1789 b1907 b4
4412 B b1908 t1907
4413 T t1908 o1090 b1908
4414 B b1909 t1908
4415 P p1918 String unique_id2
4416 O o1918 rule p1918
4417 T t1918 o596 b585 b815 b1740
4418 B b1918 t1918
4419 T t1919 o761 b591 b759 b1918 b815
4420 B b1919 t1919 s
4421 T t1920 o1744 b591 b1919
4422 S s1920 t684 h
4423 G s1920 t1920
4424 B b1920 s1920
4425 T t1921 o677 b1920
4426 B b1921 t1921
4427 T t1922 o676 b1921 b1750
4428 B b1922 t1922
4429 T t1923 o676 b1744 b1922
4430 B b1923 t1923
4431 T t1924 o676 b763 b1923
4432 B b1924 t1924
4433 T t1925 o676 b700 b1924
4434 B b1925 t1925
4435 T t1926 o676 b682 b1925
4436 B b1926 t1926
4437 T t1927 o676 b761 b1926
4438 B b1927 t1927
4439 T t1928 o676 b1742 b1927
4440 B b1928 t1928
4441 T t1929 o b1920 b4
4442 B b1929 t1929
4443 T t1930 o b1743 b1929
4444 B b1930 t1930
4445 T t1931 o b762 b1930
4446 B b1931 t1931
4447 T t1932 o b699 b1931
4448 B b1932 t1932
4449 T t1933 o b681 b1932
4450 B b1933 t1933
4451 T t1934 o b760 b1933
4452 B b1934 t1934
4453 T t1935 o b1741 b1934
4454 B b1935 t1935
4455 T t1936 o1095 b1749 b1935
4456 B b1936 t1936
4457 T t1937 o1094 b1936 b4 b1104
4458 B b1937 t1937
4459 H h1937 v t1920
4460 T t1938 o596 b585 b1768 b1740
4461 B b1938 t1938
4462 T t1939 o761 b591 b759 b1938 b1768
4463 B b1939 t1939 w
4464 T t1940 o1767 b1939
4465 S s1940 t684 h h1937
4466 G s1940 t1940
4467 B b1940 s1940
4468 T t1941 o1095 b1940 b1935
4469 B b1941 t1941
4470 S s1941 t684 h h1937
4471 G s1941 t1749
4472 B b1942 s1941
4473 T t1942 o1095 b1942 b1935
4474 B b1943 t1942
4475 T t1943 o2 b1937
4476 B b1944 t1943
4477 T t1944 o1094 b1943 b1778 b1944
4478 B b1945 t1944
4479 T t1945 o2 b1945
4480 B b1946 t1945
4481 T t1946 o1766 b1941 b4 b1946
4482 B b1947 t1946
4483 T t1947 o596 b585 b604 b1740
4484 B b1948 t1947
4485 T t1948 o761 b591 b759 b1948 b604
4486 H h1948 w t1948
4487 S s1948 t684 h h1937 h1948
4488 G s1948 t1749
4489 B b1949 s1948
4490 T t1949 o1095 b1949 b1935
4491 B b1950 t1949
4492 T t1950 o1094 b1950 b4 b1946
4493 B b1951 t1950
4494 T t1951 o b1951 b4
4495 B b1952 t1951
4496 T t1952 o b1947 b1952
4497 B b1953 t1952
4498 T t1953 o1093 b1937 b1953
4499 B b1954 t1953
4500 P p1954 String "rwh unfold_fun_prop 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
4501 O o1954 ext_rule p1954
4502 T t1954 o596 b585 b714 b1740
4503 B b1955 t1954
4504 T t1955 o761 b591 b759 b1955 b714
4505 H h1955 x_1 t1955
4506 T t1956 o596 b585 b717 b1740
4507 B b1956 t1956
4508 T t1957 o761 b591 b759 b1956 b717
4509 S s1957 t684 h h1937 h1789 h1790 h1791 h1955
4510 G s1957 t1957
4511 B b1957 s1957
4512 T t1958 o1095 b1957 b1935
4513 B b1958 t1958
4514 B b1959 t1955
4515 B b1960 t1957
4516 T t1960 o1117 b1959 b1960
4517 S s1960 t684 h h1937 h1789 h1790 h1791
4518 G s1960 t1960
4519 B b1961 s1960
4520 T t1961 o1095 b1961 b1935
4521 B b1962 t1961
4522 B b1963 t1960
4523 T t1963 o1117 b1800 b1963
4524 S s1963 t684 h h1937 h1789 h1790
4525 G s1963 t1963
4526 B b1964 s1963
4527 T t1964 o1095 b1964 b1935
4528 B b1965 t1964
4529 B b1966 t1963 s2
4530 T t1966 o1129 b1130 b1966
4531 S s1966 t684 h h1937 h1789
4532 G s1966 t1966
4533 B b1967 s1966
4534 T t1967 o1095 b1967 b1935
4535 B b1968 t1967
4536 B b1969 t1966 s1
4537 T t1969 o1129 b1130 b1969
4538 S s1969 t684 h h1937
4539 G s1969 t1969
4540 B b1970 s1969
4541 T t1970 o1095 b1970 b1935
4542 B b1971 t1970
4543 T t1971 o2 b1947
4544 B b1972 t1971
4545 T t1972 o1766 b1971 b4 b1972
4546 B b1973 t1972
4547 T t1973 o2 b1973
4548 B b1974 t1973
4549 T t1974 o1094 b1968 b4 b1974
4550 B b1975 t1974
4551 T t1975 o2 b1975
4552 B b1976 t1975
4553 T t1976 o1094 b1965 b4 b1976
4554 B b1977 t1976
4555 T t1977 o2 b1977
4556 B b1978 t1977
4557 T t1978 o1094 b1962 b4 b1978
4558 B b1979 t1978
4559 T t1979 o2 b1979
4560 B b1980 t1979
4561 T t1980 o1094 b1958 b4 b1980
4562 B b1981 t1980
4563 T t1981 o b1981 b4
4564 B b1982 t1981
4565 T t1982 o1093 b1947 b1982
4566 B b1983 t1982
4567 P p1983 String "equivTransT << op{'g; 's2; 'e2} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
4568 O o1983 ext_rule p1983
4569 T t1983 o700 b1955
4570 B b1984 t1983
4571 T t1984 o1151 b1984 b1823
4572 B b1985 t1984
4573 T t1985 o1151 b1152 b1985
4574 B b1986 t1985
4575 T t1986 o1151 b1151 b1986
4576 B b1987 t1986
4577 T t1987 o736 b1955 b591
4578 B b1988 t1987
4579 T t1988 o1151 b1988 b1828
4580 B b1989 t1988
4581 T t1989 o1151 b1987 b1989
4582 B b1990 t1989
4583 T t1990 o1161 b1955 b714
4584 B b1991 t1990
4585 T t1991 o736 b1991 b759
4586 B b1992 t1991
4587 T t1992 o1151 b1990 b1992
4588 H h1992 x_1 t1992
4589 T t1993 o736 b1956 b591
4590 S s1993 t684 h h1937 h1789 h1790 h1791 h1992
4591 G s1993 t1993
4592 B b1993 s1993
4593 T t1994 o1095 b1993 b1935
4594 B b1994 t1994
4595 S s1994 t684 h h1937 h1789 h1790 h1791 h1955
4596 G s1994 t1993
4597 B b1995 s1994
4598 T t1995 o1095 b1995 b1935
4599 B b1996 t1995
4600 T t1996 o2 b1981
4601 B b1997 t1996
4602 T t1997 o1094 b1996 b4 b1997
4603 B b1998 t1997
4604 T t1998 o2 b1998
4605 B b1999 t1998
4606 T t1999 o1094 b1994 b4 b1999
4607 B b2000 t1999
4608 T t2000 o761 b591 b759 b1955 b1956
4609 H h2000 u t2000
4610 T t2001 o761 b591 b759 b1956 b714
4611 H h2001 v_1 t2001
4612 S s2001 t684 h h1937 h1789 h1790 h1791 h1992 h2000 h2001
4613 G s2001 t1957
4614 B b2001 s2001
4615 T t2002 o1095 b2001 b1935
4616 B b2002 t2002
4617 S s2002 t684 h h1937 h1789 h1790 h1791 h1955 h2000 h2001
4618 G s2002 t1957
4619 B b2003 s2002
4620 T t2003 o1095 b2003 b1935
4621 B b2004 t2003
4622 T t2004 o1094 b2004 b4 b1997
4623 B b2005 t2004
4624 T t2005 o2 b2005
4625 B b2006 t2005
4626 T t2006 o1094 b2002 b4 b2006
4627 B b2007 t2006
4628 T t2007 o b2007 b4
4629 B b2008 t2007
4630 T t2008 o b2000 b2008
4631 B b2009 t2008
4632 T t2009 o1093 b1981 b2009
4633 B b2010 t2009
4634 T t2010 o1093 b2000 b4
4635 B b2011 t2010
4636 T t2011 o1850 b1092 b2011 b4 b4
4637 B b2012 t2011
4638 H h2012 y_3 t1983
4639 H h2013 y t1987
4640 H h2014 z t1991
4641 S s2014 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2012 h1855 h2013 h1857 h2014 h2000 h2001
4642 G s2014 t738
4643 B b2014 s2014
4644 T t2014 o1095 b2014 b1935
4645 B b2015 t2014
4646 S s2015 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2012 h1855 h2013 h1857 h2014 h2000 h2001
4647 G s2015 t1993
4648 B b2016 s2015
4649 T t2016 o1095 b2016 b1935
4650 B b2017 t2016
4651 H h2017 z_3 t1984
4652 S s2017 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2017 h2013 h1857 h2014 h2000 h2001
4653 G s2017 t1993
4654 B b2018 s2017
4655 T t2018 o1095 b2018 b1935
4656 B b2019 t2018
4657 H h2019 z_1 t1985
4658 S s2019 t684 h h1937 h1789 h1790 h1791 h1852 h2019 h2013 h1857 h2014 h2000 h2001
4659 G s2019 t1993
4660 B b2020 s2019
4661 T t2020 o1095 b2020 b1935
4662 B b2021 t2020
4663 H h2021 y_1 t1986
4664 S s2021 t684 h h1937 h1789 h1790 h1791 h2021 h2013 h1857 h2014 h2000 h2001
4665 G s2021 t1993
4666 B b2022 s2021
4667 T t2022 o1095 b2022 b1935
4668 B b2023 t2022
4669 H h2023 z_1 t1988
4670 S s2023 t684 h h1937 h1789 h1790 h1791 h2021 h2023 h2014 h2000 h2001
4671 G s2023 t1993
4672 B b2024 s2023
4673 T t2024 o1095 b2024 b1935
4674 B b2025 t2024
4675 H h2025 y t1989
4676 S s2025 t684 h h1937 h1789 h1790 h1791 h2025 h2014 h2000 h2001
4677 G s2025 t1993
4678 B b2026 s2025
4679 T t2026 o1095 b2026 b1935
4680 B b2027 t2026
4681 S s2027 t684 h h1937 h1789 h1790 h1791 h1992 h2000 h2001
4682 G s2027 t1993
4683 B b2028 s2027
4684 T t2028 o1095 b2028 b1935
4685 B b2029 t2028
4686 T t2029 o2 b2007
4687 B b2030 t2029
4688 T t2030 o1094 b2029 b4 b2030
4689 B b2031 t2030
4690 T t2031 o2 b2031
4691 B b2032 t2031
4692 T t2032 o1094 b2027 b4 b2032
4693 B b2033 t2032
4694 T t2033 o2 b2033
4695 B b2034 t2033
4696 T t2034 o1094 b2025 b4 b2034
4697 B b2035 t2034
4698 T t2035 o2 b2035
4699 B b2036 t2035
4700 T t2036 o1094 b2023 b4 b2036
4701 B b2037 t2036
4702 T t2037 o2 b2037
4703 B b2038 t2037
4704 T t2038 o1094 b2021 b4 b2038
4705 B b2039 t2038
4706 T t2039 o2 b2039
4707 B b2040 t2039
4708 T t2040 o1094 b2019 b4 b2040
4709 B b2041 t2040
4710 T t2041 o2 b2041
4711 B b2042 t2041
4712 T t2042 o1094 b2017 b1864 b2042
4713 B b2043 t2042
4714 T t2043 o2 b2043
4715 B b2044 t2043
4716 T t2044 o1094 b2015 b4 b2044
4717 B b2045 t2044
4718 T t2045 o b2045 b4
4719 B b2046 t2045
4720 T t2046 o1093 b2007 b2046
4721 B b2047 t2046
4722 T t2047 o1093 b2045 b4
4723 B b2048 t2047
4724 T t2048 o1894 b1092 b2048 b4 b4
4725 B b2049 t2048
4726 T t2049 o b2049 b4
4727 B b2050 t2049
4728 T t2050 o1852 b1092 b2047 b2050 b4
4729 B b2051 t2050
4730 T t2051 o b2051 b4
4731 B b2052 t2051
4732 T t2052 o b2012 b2052
4733 B b2053 t2052
4734 T t2053 o1983 b1092 b2010 b2053 b4
4735 B b2054 t2053
4736 T t2054 o b2054 b4
4737 B b2055 t2054
4738 T t2055 o1954 b1092 b1983 b2055 b4
4739 B b2056 t2055
4740 P p2056 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 'e2}; 'e2} >> 3 ttca"
4741 O o2056 ext_rule p2056
4742 T t2056 o1093 b1951 b4
4743 B b2057 t2056
4744 T t2057 o2056 b1092 b2057 b4 b4
4745 B b2058 t2057
4746 T t2058 o b2058 b4
4747 B b2059 t2058
4748 T t2059 o b2056 b2059
4749 B b2060 t2059
4750 T t2060 o1757 b1092 b1954 b2060 b4
4751 B b2061 t2060
4752 T t2061 o1090 b2061
4753 B b2062 t2061
4754 P p2071 String unique_inv1
4755 O o2071 rule p2071
4756 T t2071 o596 b585 b717 b815
4757 B b2071 t2071
4758 T t2072 o761 b591 b759 b2071 b604
4759 S s2072 t684 h
4760 G s2072 t2072
4761 B b2072 s2072
4762 T t2073 o677 b2072
4763 B b2073 t2073
4764 T t2074 o609 b585 b815
4765 B b2074 t2074
4766 T t2075 o761 b591 b759 b717 b2074
4767 S s2075 t684 h
4768 G s2075 t2075
4769 B b2075 s2075
4770 T t2076 o677 b2075
4771 B b2076 t2076
4772 T t2077 o676 b2073 b2076
4773 B b2077 t2077
4774 T t2078 o676 b739 b2077
4775 B b2078 t2078
4776 T t2079 o676 b945 b2078
4777 B b2079 t2079
4778 T t2080 o676 b763 b2079
4779 B b2080 t2080
4780 T t2081 o676 b700 b2080
4781 B b2081 t2081
4782 T t2082 o676 b682 b2081
4783 B b2082 t2082
4784 T t2083 o676 b761 b2082
4785 B b2083 t2083
4786 T t2084 o676 b719 b2083
4787 B b2084 t2084
4788 T t2085 o676 b817 b2084
4789 B b2085 t2085
4790 P p2085 String "assumT 9 thenT equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; inv{'g; 's}; 's}}>> 2 ttca"
4791 O o2085 ext_rule p2085
4792 T t2086 o b2072 b4
4793 B b2086 t2086
4794 T t2087 o b738 b2086
4795 B b2087 t2087
4796 T t2088 o b944 b2087
4797 B b2088 t2088
4798 T t2089 o b762 b2088
4799 B b2089 t2089
4800 T t2090 o b699 b2089
4801 B b2090 t2090
4802 T t2091 o b681 b2090
4803 B b2091 t2091
4804 T t2092 o b760 b2091
4805 B b2092 t2092
4806 T t2093 o b718 b2092
4807 B b2093 t2093
4808 T t2094 o b816 b2093
4809 B b2094 t2094
4810 T t2095 o1095 b2075 b2094
4811 B b2095 t2095
4812 T t2096 o1094 b2095 b4 b1104
4813 B b2096 t2096
4814 H h2096 v t2072
4815 T t2097 o596 b585 b2074 b815
4816 B b2097 t2097
4817 T t2098 o761 b591 b759 b604 b2097
4818 S s2098 t684 h h2096
4819 G s2098 t2098
4820 B b2098 s2098
4821 T t2099 o1095 b2098 b2094
4822 B b2099 t2099
4823 S s2099 t684 h h2096
4824 G s2099 t2075
4825 B b2100 s2099
4826 T t2100 o1095 b2100 b2094
4827 B b2101 t2100
4828 T t2101 o2 b2096
4829 B b2102 t2101
4830 T t2102 o1094 b2101 b4 b2102
4831 B b2103 t2102
4832 T t2103 o2 b2103
4833 B b2104 t2103
4834 T t2104 o1094 b2099 b4 b2104
4835 B b2105 t2104
4836 T t2105 o761 b591 b759 b2071 b2097
4837 H h2105 z t2105
4838 S s2105 t684 h h2096 h2105
4839 G s2105 t2075
4840 B b2106 s2105
4841 T t2106 o1095 b2106 b2094
4842 B b2107 t2106
4843 T t2107 o1094 b2107 b4 b2104
4844 B b2108 t2107
4845 T t2108 o b2108 b4
4846 B b2109 t2108
4847 T t2109 o b2105 b2109
4848 B b2110 t2109
4849 T t2110 o1093 b2096 b2110
4850 B b2111 t2110
4851 P p2111 String "assertT << equiv{car{'g}; 'R; op{'g; inv{'g; 's}; 's}; id{'g}} >> ttca thenT equivSymT 3 ttca"
4852 O o2111 ext_rule p2111
4853 T t2111 o1093 b2105 b4
4854 B b2112 t2111
4855 T t2112 o2111 b1092 b2112 b4 b4
4856 B b2113 t2112
4857 P p3 String "groupCancelRightT 3 ttca"
4858 O o6 ext_rule p3
4859 T t2113 o1093 b2108 b4
4860 B b2114 t2113
4861 T t154 o6 b1092 b2114 b4 b4
4862 B b154 t154
4863 T t155 o b154 b4
4864 B b155 t155
4865 T t158 o b2113 b155
4866 B b158 t158
4867 T t159 o2085 b1092 b2111 b158 b4
4868 B b159 t159
4869 T t169 o1090 b159
4870 B b169 t169
4871 P p2128 String unique_inv2
4872 O o2128 rule p2128
4873 T t2128 o596 b585 b815 b717
4874 B b2128 t2128
4875 T t2129 o761 b591 b759 b2128 b604
4876 S s2129 t684 h
4877 G s2129 t2129
4878 B b2129 s2129
4879 T t2130 o677 b2129
4880 B b2130 t2130
4881 T t2131 o676 b2130 b2076
4882 B b2131 t2131
4883 T t2132 o676 b739 b2131
4884 B b2132 t2132
4885 T t2133 o676 b945 b2132
4886 B b2133 t2133
4887 T t2134 o676 b763 b2133
4888 B b2134 t2134
4889 T t2135 o676 b700 b2134
4890 B b2135 t2135
4891 T t2136 o676 b761 b2135
4892 B b2136 t2136
4893 T t2137 o676 b682 b2136
4894 B b2137 t2137
4895 T t2138 o676 b719 b2137
4896 B b2138 t2138
4897 T t2139 o676 b817 b2138
4898 B b2139 t2139
4899 P p2139 String "assumT 9 thenT equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; 's; inv{'g; 's}}}>> 2 ttca"
4900 O o2139 ext_rule p2139
4901 T t2140 o b2129 b4
4902 B b2140 t2140
4903 T t2141 o b738 b2140
4904 B b2141 t2141
4905 T t2142 o b944 b2141
4906 B b2142 t2142
4907 T t2143 o b762 b2142
4908 B b2143 t2143
4909 T t2144 o b699 b2143
4910 B b2144 t2144
4911 T t2145 o b760 b2144
4912 B b2145 t2145
4913 T t2146 o b681 b2145
4914 B b2146 t2146
4915 T t2147 o b718 b2146
4916 B b2147 t2147
4917 T t2148 o b816 b2147
4918 B b2148 t2148
4919 T t2149 o1095 b2075 b2148
4920 B b2149 t2149
4921 T t2150 o1094 b2149 b4 b1104
4922 B b2150 t2150
4923 H h2150 v t2129
4924 T t2151 o596 b585 b815 b2074
4925 B b2151 t2151
4926 T t2152 o761 b591 b759 b604 b2151
4927 S s2152 t684 h h2150
4928 G s2152 t2152
4929 B b2152 s2152
4930 T t2153 o1095 b2152 b2148
4931 B b2153 t2153
4932 S s2153 t684 h h2150
4933 G s2153 t2075
4934 B b2154 s2153
4935 T t2154 o1095 b2154 b2148
4936 B b2155 t2154
4937 T t2155 o2 b2150
4938 B b2156 t2155
4939 T t2156 o1094 b2155 b4 b2156
4940 B b2157 t2156
4941 T t2157 o2 b2157
4942 B b2158 t2157
4943 T t2158 o1094 b2153 b4 b2158
4944 B b2159 t2158
4945 T t2159 o761 b591 b759 b2128 b2151
4946 H h2159 z t2159
4947 S s2159 t684 h h2150 h2159
4948 G s2159 t2075
4949 B b2160 s2159
4950 T t2160 o1095 b2160 b2148
4951 B b2161 t2160
4952 T t2161 o1094 b2161 b4 b2158
4953 B b2162 t2161
4954 T t2162 o b2162 b4
4955 B b2163 t2162
4956 T t2163 o b2159 b2163
4957 B b2164 t2163
4958 T t2164 o1093 b2150 b2164
4959 B b2165 t2164
4960 P p2165 String "assertT << equiv{car{'g}; 'R; op{'g; 's; inv{'g; 's}}; id{'g}} >> ttca thenT equivSymT 3 ttca"
4961 O o2165 ext_rule p2165
4962 T t2165 o1093 b2159 b4
4963 B b2166 t2165
4964 T t2166 o2165 b1092 b2166 b4 b4
4965 B b2167 t2166
4966 P p2167 String "groupCancelLeftT 3 ttca"
4967 O o2167 ext_rule p2167
4968 T t2167 o1093 b2162 b4
4969 B b2168 t2167
4970 T t2168 o2167 b1092 b2168 b4 b4
4971 B b2169 t2168
4972 T t2169 o b2169 b4
4973 B b2170 t2169
4974 T t2170 o b2167 b2170
4975 B b2171 t2170
4976 T t2171 o2139 b1092 b2165 b2171 b4
4977 B b2172 t2171
4978 T t2172 o1090 b2172
4979 B b2173 t2172
4980 P p2182 String unique_sol1
4981 O o2182 rule p2182
4982 B b2182 t1304
4983 T t2182 o700 b2182
4984 S s2182 t679 h
4985 G s2182 t2182
4986 B b2183 s2182
4987 T t2183 o677 b2183
4988 B b2184 t2183
4989 T t2184 o736 b2182 b591
4990 S s2184 t684 h
4991 G s2184 t2184
4992 B b2185 s2184
4993 T t2185 o677 b2185
4994 B b2186 t2185
4995 T t2186 o596 b585 b597 b2182
4996 B b2187 t2186
4997 T t2187 o761 b591 b759 b2187 b598
4998 S s2187 t684 h
4999 G s2187 t2187
5000 B b2188 s2187
5001 T t2188 o677 b2188
5002 B b2189 t2188
5003 T t2189 o596 b585 b609 b598
5004 B b2190 t2189
5005 T t2190 o761 b591 b759 b2182 b2190
5006 S s2190 t684 h
5007 G s2190 t2190
5008 B b2191 s2190
5009 T t2191 o677 b2191
5010 B b2192 t2191
5011 T t2192 o676 b2189 b2192
5012 B b2193 t2192
5013 T t2193 o676 b2186 b2193
5014 B b2194 t2193
5015 T t2194 o676 b1077 b2194
5016 B b2195 t2194
5017 T t2195 o676 b1075 b2195
5018 B b2196 t2195
5019 T t2196 o676 b763 b2196
5020 B b2197 t2196
5021 T t2197 o676 b700 b2197
5022 B b2198 t2197
5023 T t2198 o676 b682 b2198
5024 B b2199 t2198
5025 T t2199 o676 b761 b2199
5026 B b2200 t2199
5027 T t2200 o676 b2184 b2200
5028 B b2201 t2200
5029 T t2201 o676 b1073 b2201
5030 B b2202 t2201
5031 T t2202 o676 b1071 b2202
5032 B b2203 t2202
5033 P p2203 String "assumT 11 thenT assertT << equiv{car{'g}; 'R; op{'g; inv{'g; 'a}; op{'g; 'a; 'x}}; op{'g; inv{'g; 'a}; 'b}} >> ttca"
5034 O o2203 ext_rule p2203
5035 T t2203 o b2188 b4
5036 B b2204 t2203
5037 T t2204 o b2185 b2204
5038 B b2205 t2204
5039 T t2205 o b1076 b2205
5040 B b2206 t2205
5041 T t2206 o b1074 b2206
5042 B b2207 t2206
5043 T t2207 o b762 b2207
5044 B b2208 t2207
5045 T t2208 o b699 b2208
5046 B b2209 t2208
5047 T t2209 o b681 b2209
5048 B b2210 t2209
5049 T t2210 o b760 b2210
5050 B b2211 t2210
5051 T t2211 o b2183 b2211
5052 B b2212 t2211
5053 T t2212 o b1072 b2212
5054 B b2213 t2212
5055 T t2213 o b1070 b2213
5056 B b2214 t2213
5057 T t2214 o1095 b2191 b2214
5058 B b2215 t2214
5059 T t2215 o1094 b2215 b4 b1104
5060 B b2216 t2215
5061 H h2216 v t2187
5062 T t2216 o596 b585 b609 b2187
5063 B b2217 t2216
5064 T t2217 o761 b591 b759 b2217 b2190
5065 H h2217 v_1 t2217
5066 S s2217 t684 h h2216 h2217
5067 G s2217 t2190
5068 B b2218 s2217
5069 T t2218 o1095 b2218 b2214
5070 B b2219 t2218
5071 S s2219 t684 h h2216
5072 G s2219 t2190
5073 B b2220 s2219
5074 T t2220 o1095 b2220 b2214
5075 B b2221 t2220
5076 T t2221 o2 b2216
5077 B b2222 t2221
5078 T t2222 o1094 b2221 b4 b2222
5079 B b2223 t2222
5080 T t2223 o2 b2223
5081 B b2224 t2223
5082 T t2224 o1094 b2219 b4 b2224
5083 B b2225 t2224
5084 T t2225 o b2225 b4
5085 B b2226 t2225
5086 T t2226 o1093 b2216 b2226
5087 B b2227 t2226
5088 P p2227 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 'a}; op{'g; 'a; 'x}}; op{'g; op{'g; inv{'g; 'a}; 'a}; 'x}} >> 3 ttca"
5089 O o2227 ext_rule p2227
5090 T t2227 o596 b585 b609 b597
5091 B b2228 t2227
5092 T t2228 o596 b585 b2228 b2182
5093 B b2229 t2228
5094 T t2229 o761 b591 b759 b2229 b2190
5095 H h2229 z t2229
5096 S s2229 t684 h h2216 h2217 h2229
5097 G s2229 t2190
5098 B b2230 s2229
5099 T t2230 o1095 b2230 b2214
5100 B b2231 t2230
5101 T t2231 o2 b2225
5102 B b2232 t2231
5103 T t2232 o1094 b2231 b4 b2232
5104 B b2233 t2232
5105 T t2233 o b2233 b4
5106 B b2234 t2233
5107 T t2234 o1093 b2225 b2234
5108 B b2235 t2234
5109 P p2235 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 'a}; 'a}; id{'g}} >> 4 ttca"
5110 O o2235 ext_rule p2235
5111 T t2235 o596 b585 b604 b2182
5112 B b2236 t2235
5113 T t2236 o761 b591 b759 b2236 b2190
5114 H h2236 z_1 t2236
5115 S s2236 t684 h h2216 h2217 h2229 h2236
5116 G s2236 t2190
5117 B b2237 s2236
5118 T t2237 o1095 b2237 b2214
5119 B b2238 t2237
5120 T t2238 o2 b2233
5121 B b2239 t2238
5122 T t2239 o1094 b2238 b4 b2239
5123 B b2240 t2239
5124 T t2240 o b2240 b4
5125 B b2241 t2240
5126 T t2241 o1093 b2233 b2241
5127 B b2242 t2241
5128 P p2242 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 'x}; 'x} >> 5 ttca"
5129 O o2242 ext_rule p2242
5130 T t2242 o1093 b2240 b4
5131 B b2243 t2242
5132 T t2243 o2242 b1092 b2243 b4 b4
5133 B b2244 t2243
5134 T t2244 o b2244 b4
5135 B b2245 t2244
5136 T t2245 o2235 b1092 b2242 b2245 b4
5137 B b2246 t2245
5138 T t2246 o b2246 b4
5139 B b2247 t2246
5140 T t2247 o2227 b1092 b2235 b2247 b4
5141 B b2248 t2247
5142 T t2248 o b2248 b4
5143 B b2249 t2248
5144 T t2249 o2203 b1092 b2227 b2249 b4
5145 B b2250 t2249
5146 T t2250 o1090 b2250
5147 B b2251 t2250
5148 P p2260 String unique_sol2
5149 O o2260 rule p2260
5150 P p2261 Var y
5151 O o2261 var p2261
5152 T t2261 o2261
5153 B b2261 t2261
5154 T t2262 o700 b2261
5155 S s2262 t679 h
5156 G s2262 t2262
5157 B b2262 s2262
5158 T t2263 o677 b2262
5159 B b2263 t2263
5160 T t2264 o736 b2261 b591
5161 S s2264 t684 h
5162 G s2264 t2264
5163 B b2264 s2264
5164 T t2265 o677 b2264
5165 B b2265 t2265
5166 T t2266 o596 b585 b2261 b597
5167 B b2266 t2266
5168 T t2267 o761 b591 b759 b2266 b598
5169 S s2267 t684 h
5170 G s2267 t2267
5171 B b2267 s2267
5172 T t2268 o677 b2267
5173 B b2268 t2268
5174 T t2269 o596 b585 b598 b609
5175 B b2269 t2269
5176 T t2270 o761 b591 b759 b2261 b2269
5177 S s2270 t684 h
5178 G s2270 t2270
5179 B b2270 s2270
5180 T t2271 o677 b2270
5181 B b2271 t2271
5182 T t2272 o676 b2268 b2271
5183 B b2272 t2272
5184 T t2273 o676 b2265 b2272
5185 B b2273 t2273
5186 T t2274 o676 b1077 b2273
5187 B b2274 t2274
5188 T t2275 o676 b1075 b2274
5189 B b2275 t2275
5190 T t2276 o676 b763 b2275
5191 B b2276 t2276
5192 T t2277 o676 b700 b2276
5193 B b2277 t2277
5194 T t2278 o676 b682 b2277
5195 B b2278 t2278
5196 T t2279 o676 b761 b2278
5197 B b2279 t2279
5198 T t2280 o676 b2263 b2279
5199 B b2280 t2280
5200 T t2281 o676 b1073 b2280
5201 B b2281 t2281
5202 T t2282 o676 b1071 b2281
5203 B b2282 t2282
5204 P p174 String "assumT 11 thenT assertT << equiv{car{'g}; 'R; op{'g; op{'g; 'y; 'a}; inv{'g; 'a}}; op{'g; 'b; inv{'g; 'a}}} >> ttca"
5205 O o175 ext_rule p174
5206 T t2283 o b2267 b4
5207 B b2283 t2283
5208 T t2284 o b2264 b2283
5209 B b2284 t2284
5210 T t2285 o b1076 b2284
5211 B b2285 t2285
5212 T t2286 o b1074 b2285
5213 B b2286 t2286
5214 T t2287 o b762 b2286
5215 B b2287 t2287
5216 T t2288 o b699 b2287
5217 B b2288 t2288
5218 T t2289 o b681 b2288
5219 B b2289 t2289
5220 T t2290 o b760 b2289
5221 B b2290 t2290
5222 T t2291 o b2262 b2290
5223 B b2291 t2291
5224 T t2292 o b1072 b2291
5225 B b2292 t2292
5226 T t2293 o b1070 b2292
5227 B b2293 t2293
5228 T t2294 o1095 b2270 b2293
5229 B b2294 t2294
5230 T t2295 o1094 b2294 b4 b1104
5231 B b2295 t2295
5232 H h2295 v t2267
5233 T t2296 o596 b585 b2266 b609
5234 B b2296 t2296
5235 T t2297 o761 b591 b759 b2296 b2269
5236 H h2297 v_1 t2297
5237 S s2300 t684 h h2295 h2297
5238 G s2300 t2270
5239 B b2301 s2300
5240 T t2301 o1095 b2301 b2293
5241 B b2302 t2301
5242 S s2302 t684 h h2295
5243 G s2302 t2270
5244 B b2303 s2302
5245 T t2303 o1095 b2303 b2293
5246 B b2304 t2303
5247 T t2304 o2 b2295
5248 B b2305 t2304
5249 T t2305 o1094 b2304 b4 b2305
5250 B b2306 t2305
5251 T t2306 o2 b2306
5252 B b2307 t2306
5253 T t2314 o1094 b2302 b4 b2307
5254 B b2315 t2314
5255 T t177 o b2315 b4
5256 B b177 t177
5257 T t178 o1093 b2295 b177
5258 B b178 t178
5259 P p186 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'y; 'a}; inv{'g; 'a}}; op{'g; 'y; op{'g; 'a; inv{'g; 'a}}}} >> 3 ttca"
5260 O o186 ext_rule p186
5261 T t2315 o596 b585 b597 b609
5262 B b2316 t2315
5263 T t2316 o596 b585 b2261 b2316
5264 B b2317 t2316
5265 T t2317 o761 b591 b759 b2317 b2269
5266 H h2317 z t2317
5267 S s2319 t684 h h2295 h2297 h2317
5268 G s2319 t2270
5269 B b2320 s2319
5270 T t2320 o1095 b2320 b2293
5271 B b2321 t2320
5272 T t2321 o2 b2315
5273 B b2322 t2321
5274 P p2329 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'a; inv{'g; 'a}}; id{'g}} >> 4 ttca"
5275 O o2329 ext_rule p2329
5276 T t2329 o1094 b2321 b4 b2322
5277 B b2330 t2329
5278 T t191 o b2330 b4
5279 B b191 t191
5280 T t196 o1093 b2315 b191
5281 B b196 t196
5282 T t2330 o596 b585 b2261 b604
5283 B b2331 t2330
5284 T t2331 o761 b591 b759 b2331 b2269
5285 H h2331 z_1 t2331
5286 S s2331 t684 h h2295 h2297 h2317 h2331
5287 G s2331 t2270
5288 B b2332 s2331
5289 T t2332 o1095 b2332 b2293
5290 B b2333 t2332
5291 T t2333 o2 b2330
5292 B b2334 t2333
5293 T t2334 o1094 b2333 b4 b2334
5294 B b2335 t2334
5295 T t2335 o b2335 b4
5296 B b2336 t2335
5297 T t2336 o1093 b2330 b2336
5298 B b2337 t2336
5299 P p2337 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'y; id{'g}}; 'y} >> 5 ttca"
5300 O o2337 ext_rule p2337
5301 T t2337 o1093 b2335 b4
5302 B b2338 t2337
5303 T t2338 o2337 b1092 b2338 b4 b4
5304 B b2339 t2338
5305 T t2339 o b2339 b4
5306 B b2340 t2339
5307 T t2340 o2329 b1092 b2337 b2340 b4
5308 B b2341 t2340
5309 T t2341 o b2341 b4
5310 B b2342 t2341
5311 T t197 o186 b1092 b196 b2342 b4
5312 B b197 t197
5313 T t205 o b197 b4
5314 B b205 t205
5315 T t206 o175 b1092 b178 b205 b4
5316 B b206 t206
5317 T t208 o1090 b206
5318 B b208 t208
5319 P p2355 String inv_simplify
5320 O o2355 rule p2355
5321 T t2355 o609 b585 b599
5322 B b2355 t2355
5323 T t2356 o609 b585 b598
5324 B b2356 t2356
5325 T t2357 o596 b585 b2356 b609
5326 B b2357 t2357
5327 T t2358 o761 b591 b759 b2355 b2357
5328 S s2358 t684 h
5329 G s2358 t2358
5330 B b2358 s2358
5331 T t2359 o677 b2358
5332 B b2359 t2359
5333 T t2360 o676 b1077 b2359
5334 B b2360 t2360
5335 T t2361 o676 b1075 b2360
5336 B b2361 t2361
5337 T t2362 o676 b763 b2361
5338 B b2362 t2362
5339 T t2363 o676 b700 b2362
5340 B b2363 t2363
5341 T t2364 o676 b682 b2363
5342 B b2364 t2364
5343 T t2365 o676 b761 b2364
5344 B b2365 t2365
5345 T t2366 o676 b1073 b2365
5346 B b2366 t2366
5347 T t2367 o676 b1071 b2366
5348 B b2367 t2367
5349 P p2367 String "assertT << equiv{car{'g}; 'R; op{'g; inv{'g; op{'g; 'a; 'b}}; op{'g; 'a; 'b}}; op{'g; op{'g; inv{'g; 'b}; inv{'g; 'a}}; op{'g; 'a; 'b}}} >>"
5350 O o2367 ext_rule p2367
5351 T t2368 o1095 b2358 b1102
5352 B b2368 t2368
5353 T t2369 o1094 b2368 b4 b1104
5354 B b2369 t2369
5355 P p2369 String assertion
5356 O o2369 tactic_arg p2369
5357 T t2370 o596 b585 b2355 b599
5358 B b2370 t2370
5359 T t2371 o596 b585 b2357 b599
5360 B b2371 t2371
5361 T t2372 o761 b591 b759 b2370 b2371
5362 S s2372 t684 h
5363 G s2372 t2372
5364 B b2372 s2372
5365 T t2373 o1095 b2372 b1102
5366 B b2373 t2373
5367 T t2374 o2 b2369
5368 B b2374 t2374
5369 T t2375 o2369 b2373 b4 b2374
5370 B b2375 t2375
5371 H h2375 v t2372
5372 S s2375 t684 h h2375
5373 G s2375 t2358
5374 B b2376 s2375
5375 T t2376 o1095 b2376 b1102
5376 B b2377 t2376
5377 T t2377 o1094 b2377 b4 b2374
5378 B b2378 t2377
5379 T t2378 o b2378 b4
5380 B b2379 t2378
5381 T t2379 o b2375 b2379
5382 B b2380 t2379
5383 T t2380 o1093 b2369 b2380
5384 B b2381 t2380
5385 P p2381 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; op{'g; 'a; 'b}}; op{'g; 'a; 'b}}; id{'g}} >> 0 ttca"
5386 O o2381 ext_rule p2381
5387 T t2381 o761 b591 b759 b604 b2371
5388 S s2381 t684 h
5389 G s2381 t2381
5390 B b2382 s2381
5391 T t2382 o1095 b2382 b1102
5392 B b2383 t2382
5393 T t2383 o2 b2375
5394 B b2384 t2383
5395 T t2384 o2369 b2383 b4 b2384
5396 B b2385 t2384
5397 T t2385 o b2385 b4
5398 B b2386 t2385
5399 T t2386 o1093 b2375 b2386
5400 B b2387 t2386
5401 P p2387 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; inv{'g; 'b}; inv{'g; 'a}}; op{'g; 'a; 'b}}; op{'g; inv{'g; 'b}; op{'g; inv{'g; 'a}; op{'g; 'a; 'b}}}} >> 0 ttca"
5402 O o2387 ext_rule p2387
5403 T t2387 o1093 b2385 b4
5404 B b2388 t2387
5405 T t2388 o2387 b1092 b2388 b4 b4
5406 B b2389 t2388
5407 T t2389 o b2389 b4
5408 B b2390 t2389
5409 T t2390 o2381 b1092 b2387 b2390 b4
5410 B b2391 t2390
5411 P p217 String "groupCancelRightT 2 ttca"
5412 O o217 ext_rule p217
5413 T t2391 o1093 b2378 b4
5414 B b2392 t2391
5415 T t229 o217 b1092 b2392 b4 b4
5416 B b229 t229
5417 T t230 o b229 b4
5418 B b230 t230
5419 T t232 o b2391 b230
5420 B b232 t232
5421 T t240 o2367 b1092 b2381 b232 b4
5422 B b240 t240
5423 T t241 o1090 b240
5424 B b241 t241
5425 P p2406 String inv_of_id
5426 O o2406 rule p2406
5427 T t2406 o609 b585 b604
5428 B b2406 t2406
5429 T t2407 o761 b591 b759 b2406 b604
5430 S s2407 t684 h
5431 G s2407 t2407
5432 B b2407 s2407
5433 T t2408 o677 b2407
5434 B b2408 t2408
5435 T t2409 o676 b763 b2408
5436 B b2409 t2409
5437 T t2410 o676 b700 b2409
5438 B b2410 t2410
5439 T t2411 o676 b682 b2410
5440 B b2411 t2411
5441 T t2412 o676 b761 b2411
5442 B b2412 t2412
5443 P p2412 String "assertT << equiv{car{'g}; 'R; id{'g}; inv{'g; id{'g}}} >> thenAT autoT"
5444 O o2412 ext_rule p2412
5445 T t2413 o b762 b4
5446 B b2413 t2413
5447 T t2414 o b699 b2413
5448 B b2414 t2414
5449 T t2415 o b681 b2414
5450 B b2415 t2415
5451 T t2416 o b760 b2415
5452 B b2416 t2416
5453 T t2417 o1095 b2407 b2416
5454 B b2417 t2417
5455 T t2418 o1094 b2417 b4 b1104
5456 B b2418 t2418
5457 T t2419 o761 b591 b759 b604 b2406
5458 H h2419 v t2419
5459 S s2419 t684 h h2419
5460 G s2419 t2407
5461 B b2419 s2419
5462 T t2420 o1095 b2419 b2416
5463 B b2420 t2420
5464 T t2421 o2 b2418
5465 B b2421 t2421
5466 T t2422 o1094 b2420 b4 b2421
5467 B b2422 t2422
5468 T t2423 o b2422 b4
5469 B b2423 t2423
5470 T t2424 o1093 b2418 b2423
5471 B b2424 t2424
5472 P p2424 String "equivSymT 2 ttca"
5473 O o2424 ext_rule p2424
5474 T t2425 o1093 b2422 b4
5475 B b2425 t2425
5476 T t2426 o2424 b1092 b2425 b4 b4
5477 B b2426 t2426
5478 T t2427 o b2426 b4
5479 B b2427 t2427
5480 T t2428 o2412 b1092 b2424 b2427 b4
5481 B b2428 t2428
5482 T t2429 o1090 b2428
5483 B b2429 t2429
5484 O o2436 location p p
5485 P p502 String id_judge_elim
5486 O o503 rule p502
5487 T t509 o596 b585 b815 b815
5488 B b509 t509
5489 T t510 o761 b591 b759 b509 b815
5490 H h510 x t510
5491 S s510 t679 h h510 h1304
5492 G s510 t816
5493 B b510 s510
5494 T t516 o677 b510
5495 B b516 t516
5496 S s516 t679 h h510 h1304
5497 G s516 t760
5498 B b517 s516
5499 T t517 o677 b517
5500 B b523 t517
5501 S s523 t679 h h510 h1304
5502 G s523 t681
5503 B b524 s523
5504 T t524 o677 b524
5505 B b530 t524
5506 S s530 t684 h h510 h1304
5507 G s530 t586
5508 B b531 s530
5509 T t531 o677 b531
5510 B b538 t531
5511 S s538 t684 h h510 h1304
5512 G s538 t762
5513 B b539 s538
5514 T t539 o677 b539
5515 B b546 t539
5516 T t546 o761 b591 b759 b815 b604
5517 H h546 y t546
5518 P p548 Var C
5519 O o549 var p548
5520 T t554 o549 b2182
5521 S s554 t684 h h510 h1304 h546
5522 G s554 t554
5523 B b554 s554
5524 T t555 o677 b554
5525 B b555 t555
5526 S s555 t684 h h510 h1304
5527 G s555 t554
5528 B b561 s555
5529 T t561 o677 b561
5530 B b562 t561
5531 T t562 o676 b555 b562
5532 B b568 t562
5533 T t568 o676 b546 b568
5534 B b569 t568
5535 T t569 o676 b538 b569
5536 B b575 t569
5537 T t575 o676 b530 b575
5538 B b576 t575
5539 T t576 o676 b523 b576
5540 B b582 t576
5541 T t582 o676 b516 b582
5542 B b583 t582
5543 P p585 String "assertT << equiv{car{'g}; 'R; 's; id{'g}} >> ttca"
5544 O o586 ext_rule p585
5545 T t589 o b554 b4
5546 B b589 t589
5547 T t590 o b539 b589
5548 B b590 t590
5549 T t594 o b531 b590
5550 B b594 t594
5551 T t595 o b524 b594
5552 B b595 t595
5553 T t596 o b517 b595
5554 B b596 t596
5555 T t602 o b510 b596
5556 B b602 t602
5557 T t603 o1095 b561 b602
5558 B b603 t603
5559 T t607 o1094 b603 b4 b1104
5560 B b607 t607
5561 S s607 t684 h h510 h1304
5562 G s607 t546
5563 B b608 s607
5564 T t608 o1095 b608 b602
5565 B b612 t608
5566 T t612 o2 b607
5567 B b615 t612
5568 T t615 o2369 b612 b4 b615
5569 B b616 t615
5570 T t616 o b616 b4
5571 B b626 t616
5572 T t626 o1093 b607 b626
5573 B b679 t626
5574 P p679 String "equivSubstT << equiv{car{'g}; 'R; 's; op{'g; id{'g}; 's}} >> 0 ttca"
5575 O o681 ext_rule p679
5576 T t713 o761 b591 b759 b815 b946
5577 S s713 t684 h h510 h1304
5578 G s713 t713
5579 B b1106 s713
5580 T t1121 o1095 b1106 b602
5581 B b1738 t1121
5582 T t1738 o2 b616
5583 B b1739 t1738
5584 T t1739 o2369 b1738 b4 b1739
5585 B b1767 t1739
5586 T t1767 o761 b591 b759 b946 b604
5587 S s1767 t684 h h510 h1304
5588 G s1767 t1767
5589 B b1790 s1767
5590 T t1796 o1095 b1790 b602
5591 B b1853 t1796
5592 T t1853 o2369 b1853 b4 b1739
5593 B b1854 t1853
5594 T t1854 o b1854 b4
5595 B b1855 t1854
5596 T t1855 o b1767 b1855
5597 B b1856 t1855
5598 T t1856 o1093 b616 b1856
5599 B b1857 t1856
5600 P p1857 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's}; 's} >> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
5601 O o1857 ext_rule p1857
5602 T t1857 o1093 b1767 b4
5603 B b1910 t1857
5604 T t1910 o1857 b1092 b1910 b4 b4
5605 B b1917 t1910
5606 P p1919 String "equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; inv{'g; 's}; 's}} >> 0 ttca"
5607 O o1919 ext_rule p1919
5608 S s1919 t684 h h510 h1304
5609 G s1919 t2098
5610 B b2013 s1919
5611 T t2013 o1095 b2013 b602
5612 B b2063 t2013
5613 T t2063 o2 b1854
5614 B b2070 t2063
5615 T t2070 o2369 b2063 b4 b2070
5616 B b2115 t2070
5617 T t2115 o596 b585 b2097 b815
5618 B b2116 t2115
5619 T t2116 o761 b591 b759 b2116 b2097
5620 S s2116 t684 h h510 h1304
5621 G s2116 t2116
5622 B b2117 s2116
5623 T t2117 o1095 b2117 b602
5624 B b2118 t2117
5625 T t2118 o2369 b2118 b4 b2070
5626 B b2119 t2118
5627 B b2120 t819
5628 T t2120 o761 b591 b759 b2120 b818
5629 B b2125 t2120 z
5630 T t2125 o1077 b591 b759 b2125
5631 S s2125 t684 h h510 h1304
5632 G s2125 t2125
5633 B b2126 s2125
5634 T t2126 o1095 b2126 b602
5635 B b2127 t2126
5636 T t2127 o2369 b2127 b4 b2070
5637 B b2174 t2127
5638 T t2174 o b2174 b4
5639 B b2181 t2174
5640 T t2181 o b2119 b2181
5641 B b2252 t2181
5642 T t2252 o b2115 b2252
5643 B b2259 t2252
5644 T t2259 o1093 b1854 b2259
5645 B b2260 t2259
5646 P p2262 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT thenT rwh unfold_equiv 2 ttca"
5647 O o2262 ext_rule p2262
5648 T t2298 o1093 b2115 b4
5649 B b2298 t2298
5650 T t2299 o2262 b1092 b2298 b4 b4
5651 B b2299 t2299
5652 P p2299 String "equivSubstT << equiv{car{'g}; 'R; 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"
5653 O o2299 ext_rule p2299
5654 T t2300 o1093 b2119 b4
5655 B b2300 t2300
5656 T t2302 o2299 b1092 b2300 b4 b4
5657 B b2308 t2302
5658 P p2308 String "rwh unfold_equiv_fun_prop 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca thenT dT 0 ttca"
5659 O o2308 ext_rule p2308
5660 H h2308 a t1106
5661 H h2309 b t1106
5662 H h2310 x_1 t762
5663 T t2310 o761 b591 b759 b597 b598
5664 H h2311 x_2 t2310
5665 T t2311 o596 b585 b597 b815
5666 B b2311 t2311
5667 T t2312 o761 b591 b759 b2311 b597
5668 H h2312 x_3 t2312
5669 T t2313 o596 b585 b598 b815
5670 B b2313 t2313
5671 T t2318 o761 b591 b759 b2313 b598
5672 S s2318 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2312
5673 G s2318 t2318
5674 B b2318 s2318
5675 T t2319 o1095 b2318 b602
5676 B b2319 t2319
5677 B b2323 t2312
5678 B b2324 t2318
5679 T t2324 o1117 b2323 b2324
5680 S s2324 t684 h h510 h1304 h2308 h2309 h2310 h2311
5681 G s2324 t2324
5682 B b2325 s2324
5683 T t2325 o1095 b2325 b602
5684 B b2326 t2325
5685 B b2327 t2310
5686 B b2328 t2324
5687 T t2328 o1117 b2327 b2328
5688 S s2328 t684 h h510 h1304 h2308 h2309 h2310
5689 G s2328 t2328
5690 B b2329 s2328
5691 T t2342 o1095 b2329 b602
5692 B b2343 t2342
5693 B b2344 t2328
5694 T t2344 o1117 b1126 b2344
5695 S s2344 t684 h h510 h1304 h2308 h2309
5696 G s2344 t2344
5697 B b2345 s2344
5698 T t2345 o1095 b2345 b602
5699 B b2346 t2345
5700 B b2347 t2344 b
5701 T t2347 o1129 b1130 b2347
5702 S s2347 t684 h h510 h1304 h2308
5703 G s2347 t2347
5704 B b2352 s2347
5705 T t2352 o1095 b2352 b602
5706 B b2353 t2352
5707 B b2354 t2347 a
5708 T t2354 o1129 b1130 b2354
5709 S s2354 t684 h h510 h1304
5710 G s2354 t2354
5711 B b2393 s2354
5712 T t2393 o1095 b2393 b602
5713 B b2394 t2393
5714 T t2394 o2 b2174
5715 B b2395 t2394
5716 T t2395 o2369 b2394 b4 b2395
5717 B b2396 t2395
5718 T t2396 o2 b2396
5719 B b2397 t2396
5720 T t2397 o1094 b2353 b4 b2397
5721 B b2398 t2397
5722 T t2398 o2 b2398
5723 B b2403 t2398
5724 T t2403 o1094 b2346 b4 b2403
5725 B b2404 t2403
5726 T t2404 o2 b2404
5727 B b2405 t2404
5728 T t2405 o1094 b2343 b4 b2405
5729 B b2430 t2405
5730 T t2430 o2 b2430
5731 B b2440 t2430
5732 T t2440 o1094 b2326 b4 b2440
5733 B b2441 t2440
5734 T t2441 o2 b2441
5735 B b2442 t2441
5736 T t2442 o1094 b2319 b4 b2442
5737 B b2443 t2442
5738 T t2443 o b2443 b4
5739 B b2444 t2443
5740 T t2444 o1093 b2174 b2444
5741 B b2445 t2444
5742 P p2445 String "equivTransT << op{'g; 'b; 's} >> 8 ttca thenT rwh unfold_equiv 8 ttca"
5743 O o2445 ext_rule p2445
5744 T t2445 o700 b2311
5745 B b2446 t2445
5746 B b2447 t1070
5747 T t2447 o1151 b2446 b2447
5748 B b2448 t2447
5749 T t2448 o1151 b1152 b2448
5750 B b2449 t2448
5751 T t2449 o1151 b1151 b2449
5752 B b2450 t2449
5753 T t2450 o736 b2311 b591
5754 B b2451 t2450
5755 B b2452 t1074
5756 T t2452 o1151 b2451 b2452
5757 B b2453 t2452
5758 T t2453 o1151 b2450 b2453
5759 B b2454 t2453
5760 T t2454 o1161 b2311 b597
5761 B b2455 t2454
5762 T t2455 o736 b2455 b759
5763 B b2456 t2455
5764 T t2456 o1151 b2454 b2456
5765 H h2456 x_3 t2456
5766 T t2457 o736 b2313 b591
5767 S s2457 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2456
5768 G s2457 t2457
5769 B b2457 s2457
5770 T t2458 o1095 b2457 b602
5771 B b2458 t2458
5772 S s2458 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2312
5773 G s2458 t2457
5774 B b2459 s2458
5775 T t2459 o1095 b2459 b602
5776 B b2460 t2459
5777 T t2460 o2 b2443
5778 B b2461 t2460
5779 T t2461 o1094 b2460 b4 b2461
5780 B b2462 t2461
5781 T t2462 o2 b2462
5782 B b2463 t2462
5783 T t2463 o1094 b2458 b4 b2463
5784 B b2464 t2463
5785 T t2464 o761 b591 b759 b2311 b2313
5786 H h2464 u t2464
5787 T t2465 o761 b591 b759 b2313 b597
5788 H h2465 v t2465
5789 S s2465 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2456 h2464 h2465
5790 G s2465 t2318
5791 B b2465 s2465
5792 T t2466 o1095 b2465 b602
5793 B b2466 t2466
5794 S s2466 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2312 h2464 h2465
5795 G s2466 t2318
5796 B b2467 s2466
5797 T t2467 o1095 b2467 b602
5798 B b2468 t2467
5799 T t2468 o1094 b2468 b4 b2461
5800 B b2469 t2468
5801 T t2469 o2 b2469
5802 B b2470 t2469
5803 T t2470 o1094 b2466 b4 b2470
5804 B b2471 t2470
5805 T t2471 o b2471 b4
5806 B b2472 t2471
5807 T t2472 o b2464 b2472
5808 B b2473 t2472
5809 T t2473 o1093 b2443 b2473
5810 B b2474 t2473
5811 P p2474 String "autoT thenT rwh unfold_equiv 7 ttca thenT rwh unfold_equiv 2 ttca"
5812 O o2474 ext_rule p2474
5813 T t2474 o1093 b2464 b4
5814 B b2475 t2474
5815 T t2475 o2474 b1092 b2475 b4 b4
5816 B b2476 t2475
5817 P p2476 String "equivTransT << 'b >> 10 thenT autoT thenT rwh unfold_equiv 7 ttca thenT rwh unfold_equiv 2 ttca"
5818 O o2476 ext_rule p2476
5819 T t2476 o1093 b2471 b4
5820 B b2477 t2476
5821 T t2477 o2476 b1092 b2477 b4 b4
5822 B b2478 t2477
5823 T t2478 o b2478 b4
5824 B b2479 t2478
5825 T t2479 o b2476 b2479
5826 B b2480 t2479
5827 T t2480 o2445 b1092 b2474 b2480 b4
5828 B b2481 t2480
5829 T t2481 o b2481 b4
5830 B b2482 t2481
5831 T t2482 o2308 b1092 b2445 b2482 b4
5832 B b2483 t2482
5833 T t2483 o b2483 b4
5834 B b2484 t2483
5835 T t2484 o b2308 b2484
5836 B b2485 t2484
5837 T t2485 o b2299 b2485
5838 B b2486 t2485
5839 T t2486 o1919 b1092 b2260 b2486 b4
5840 B b2487 t2486
5841 T t2487 o b2487 b4
5842 B b2488 t2487
5843 T t2488 o b1917 b2488
5844 B b2489 t2488
5845 T t2489 o681 b1092 b1857 b2489 b4
5846 B b2490 t2489
5847 T t2490 o b2490 b4
5848 B b2491 t2490
5849 T t2491 o586 b1092 b679 b2491 b4
5850 B b2492 t2491
5851 T t2492 o1090 b2492
5852 B b2493 t2492
5853 P p18 Number 8085
5854 P p20 Number 8092
5855 O o20 resource_defs p18 p20 p176
5856 P p22 Number 8090
5857 O o22 uid p22 p20
5858 T t170 o22 b691
5859 B b170 t170
5860 T t173 o b170 b4
5861 B b173 t173
5862 T t209 o20 b173
5863 B b209 t209
5864 T t210 o b209 b4
5865 B b210 t210
5866 T t244 o503 b1302 b583 b2493 b210
5867 B b244 t244
5868 T t249 o16 b244
5869 B b249 t249
5870 P p262 Number 8798
5871 P p263 Number 9192
5872 O o263 location p262 p263
5873 T t2501 o761 b591 b759 b2151 b604
5874 S s2501 t684 h
5875 G s2501 t2501
5876 B b2501 s2501
5877 T t2502 o677 b2501
5878 B b2502 t2502
5879 T t2503 o676 b945 b2502
5880 B b2503 t2503
5881 T t2504 o676 b763 b2503
5882 B b2504 t2504
5883 T t2505 o676 b700 b2504
5884 B b2505 t2505
5885 T t2506 o676 b682 b2505
5886 B b2506 t2506
5887 T t2507 o676 b761 b2506
5888 B b2507 t2507
5889 T t2508 o676 b817 b2507
5890 B b2508 t2508
5891 P p2508 String "assertT << equiv{car{'g}; 'R; op{'g; op{'g; 's; inv{'g; 's}}; op{'g; 's; inv{'g; 's}}}; op{'g; 's; inv{'g; 's}}} >> ttca"
5892 O o2508 ext_rule p2508
5893 T t2509 o b944 b4
5894 B b2509 t2509
5895 T t2510 o b762 b2509
5896 B b2510 t2510
5897 T t2511 o b699 b2510
5898 B b2511 t2511
5899 T t2512 o b681 b2511
5900 B b2512 t2512
5901 T t2513 o b760 b2512
5902 B b2513 t2513
5903 T t2514 o b816 b2513
5904 B b2514 t2514
5905 T t2515 o1095 b2501 b2514
5906 B b2515 t2515
5907 T t2516 o1094 b2515 b4 b1104
5908 B b2516 t2516
5909 T t2517 o596 b585 b2151 b2151
5910 B b2517 t2517
5911 T t2518 o761 b591 b759 b2517 b2151
5912 S s2518 t684 h
5913 G s2518 t2518
5914 B b2518 s2518
5915 T t2519 o1095 b2518 b2514
5916 B b2519 t2519
5917 T t2520 o2 b2516
5918 B b2520 t2520
5919 T t2521 o2369 b2519 b4 b2520
5920 B b2521 t2521
5921 H h2521 v t2518
5922 S s2521 t684 h h2521
5923 G s2521 t2501
5924 B b2522 s2521
5925 T t2522 o1095 b2522 b2514
5926 B b2523 t2522
5927 T t2523 o1094 b2523 b4 b2520
5928 B b2524 t2523
5929 T t2524 o b2524 b4
5930 B b2525 t2524
5931 T t2525 o b2521 b2525
5932 B b2526 t2525
5933 T t2526 o1093 b2516 b2526
5934 B b2527 t2526
5935 P p2527 String "equivSubstT << equiv{car{'g}; 'R; 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"
5936 O o2527 ext_rule p2527
5937 T t2527 o596 b585 b2074 b2151
5938 B b2528 t2527
5939 T t2528 o596 b585 b815 b2528
5940 B b2529 t2528
5941 T t2529 o761 b591 b759 b2529 b2151
5942 S s2529 t684 h
5943 G s2529 t2529
5944 B b2530 s2529
5945 T t2530 o1095 b2530 b2514
5946 B b2531 t2530
5947 T t2531 o2 b2521
5948 B b2532 t2531
5949 T t2532 o2369 b2531 b4 b2532
5950 B b2533 t2532
5951 T t2533 o b2533 b4
5952 B b2534 t2533
5953 T t2534 o1093 b2521 b2534
5954 B b2535 t2534
5955 P p2535 String "equivSubstT << equiv{car{'g}; 'R; 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"
5956 O o2535 ext_rule p2535
5957 T t2535 o596 b585 b2097 b2074
5958 B b2536 t2535
5959 T t2536 o596 b585 b815 b2536
5960 B b2537 t2536
5961 T t2537 o761 b591 b759 b2537 b2151
5962 S s2537 t684 h
5963 G s2537 t2537
5964 B b2538 s2537
5965 T t2538 o1095 b2538 b2514
5966 B b2539 t2538
5967 T t2539 o2 b2533
5968 B b2540 t2539
5969 T t2540 o2369 b2539 b4 b2540
5970 B b2541 t2540
5971 T t2541 o b2541 b4
5972 B b2542 t2541
5973 T t2542 o1093 b2533 b2542
5974 B b2543 t2542
5975 P p2543 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT"
5976 O o2543 ext_rule p2543
5977 T t2543 o596 b585 b818 b2074
5978 B b2544 t2543
5979 T t2544 o596 b585 b815 b2544
5980 B b2545 t2544 z
5981 T t2545 o817 b591 b759 b2545
5982 S s2545 t684 h
5983 G s2545 t2545
5984 B b2546 s2545
5985 T t2546 o1095 b2546 b2514
5986 B b2547 t2546
5987 B b2548 t2544
5988 T t2548 o761 b591 b759 b2548 b2151
5989 B b2549 t2548 z
5990 T t2549 o1077 b591 b759 b2549
5991 S s2549 t684 h
5992 G s2549 t2549
5993 B b2550 s2549
5994 T t2550 o1095 b2550 b2514
5995 B b2551 t2550
5996 T t2551 o2 b2541
5997 B b2552 t2551
5998 T t2552 o2369 b2551 b1864 b2552
5999 B b2553 t2552
6000 T t2553 o2 b2553
6001 B b2554 t2553
6002 T t2554 o2369 b2547 b4 b2554
6003 B b2555 t2554
6004 T t2555 o b2555 b4
6005 B b2556 t2555
6006 T t2556 o1093 b2541 b2556
6007 B b2557 t2556
6008 P p2557 String "rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 5 ttca"
6009 O o2557 ext_rule p2557
6010 T t2557 o1093 b2555 b4
6011 B b2558 t2557
6012 T t2558 o2557 b1092 b2558 b4 b4
6013 B b2559 t2558
6014 T t2559 o b2559 b4
6015 B b2560 t2559
6016 T t2560 o2543 b1092 b2557 b2560 b4
6017 B b2561 t2560
6018 T t2561 o b2561 b4
6019 B b2562 t2561
6020 T t2562 o2535 b1092 b2543 b2562 b4
6021 B b2563 t2562
6022 T t2563 o b2563 b4
6023 B b2564 t2563
6024 T t2564 o2527 b1092 b2535 b2564 b4
6025 B b2565 t2564
6026 P p2565 String "dT 2 ttca"
6027 O o2565 ext_rule p2565
6028 T t2565 o1093 b2524 b4
6029 B b2566 t2565
6030 T t2566 o2565 b1092 b2566 b4 b4
6031 B b2567 t2566
6032 T t2567 o b2567 b4
6033 B b2568 t2567
6034 T t2568 o b2565 b2568
6035 B b2569 t2568
6036 T t2569 o2508 b1092 b2527 b2569 b4
6037 B b2570 t2569
6038 T t2570 o1090 b2570
6039 B b2571 t2570
6040 P p264 Number 8821
6041 P p265 Number 8828
6042 O o265 resource_defs p264 p265 p204
6043 P p287 Number 8826
6044 O o287 uid p287 p265
6045 T t422 o287 b691
6046 B b422 t422
6047 T t423 o b422 b4
6048 B b423 t423
6049 T t523 o265 b423
6050 B b547 t523
6051 T t547 o b547 b4
6052 B b584 t547
6053 T t584 o1053 b676 b2508 b2571 b584
6054 B b684 t584
6055 T t727 o263 b684
6056 B b727 t727
6057 P p729 Number 9194
6058 P p730 Number 9578
6059 O o730 location p729 p730
6060 T t2579 o1095 b964 b2514
6061 B b2579 t2579
6062 T t2580 o1094 b2579 b4 b1104
6063 B b2580 t2580
6064 S s2580 t684 h
6065 G s2580 t2098
6066 B b2581 s2580
6067 T t2581 o1095 b2581 b2514
6068 B b2582 t2581
6069 T t2582 o2 b2580
6070 B b2583 t2582
6071 T t2583 o1094 b2582 b4 b2583
6072 B b2584 t2583
6073<