/[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 3530 - (show annotations) (download)
Thu Mar 7 23:13:10 2002 UTC (19 years, 4 months ago) by xiny
File size: 136215 byte(s)
1. Added properties that "e * a = a * e" and "a * e = e * a".
2. Changed the definition of groups to one-sided (left) definition,
   i.e., groups are defined by the left axioms, and proved the right
   axioms.
3. Removed the introduction forms of group cancellation laws which
   were put in comments in the last version.

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 p1053 String inv_id2
2700 O o1053 rule p1053
2701 P p1070 String equiv_op_fun1
2702 O o1070 rule p1070
2703 T t1070 o700 b597
2704 S s1070 t679 h
2705 G s1070 t1070
2706 B b1070 s1070
2707 T t1071 o677 b1070
2708 B b1071 t1071
2709 T t1072 o700 b598
2710 S s1072 t679 h
2711 G s1072 t1072
2712 B b1072 s1072
2713 T t1073 o677 b1072
2714 B b1073 t1073
2715 T t1074 o736 b597 b591
2716 S s1074 t684 h
2717 G s1074 t1074
2718 B b1074 s1074
2719 T t1075 o677 b1074
2720 B b1075 t1075
2721 T t1076 o736 b598 b591
2722 S s1076 t684 h
2723 G s1076 t1076
2724 B b1076 s1076
2725 T t1077 o677 b1076
2726 B b1077 t1077
2727 NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
2728 O o1077 equiv_fun_prop
2729 T t1078 o596 b585 b818 b597
2730 B b1078 t1078
2731 T t1079 o596 b585 b818 b598
2732 B b1079 t1079
2733 T t1080 o761 b591 b759 b1078 b1079
2734 B b1080 t1080 z
2735 T t1081 o1077 b591 b759 b1080
2736 S s1081 t684 h
2737 G s1081 t1081
2738 B b1081 s1081
2739 T t1082 o677 b1081
2740 B b1082 t1082
2741 T t1083 o676 b1077 b1082
2742 B b1083 t1083
2743 T t1084 o676 b1075 b1083
2744 B b1084 t1084
2745 T t1085 o676 b763 b1084
2746 B b1085 t1085
2747 T t1086 o676 b700 b1085
2748 B b1086 t1086
2749 T t1087 o676 b682 b1086
2750 B b1087 t1087
2751 T t1088 o676 b761 b1087
2752 B b1088 t1088
2753 T t1089 o676 b1073 b1088
2754 B b1089 t1089
2755 T t1090 o676 b1071 b1089
2756 B b1090 t1090
2757 NSummary!interactive interactive interactive Summary
2758 O o1090 interactive
2759 NSummary!ext_rule ext_rule ext_rule Summary
2760 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"
2761 O o1091 ext_rule p1090
2762 NSummary!status_incomplete status_incomplete status_incomplete Summary
2763 O o1092 status_incomplete
2764 T t1092 o1092
2765 B b1092 t1092
2766 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2767 O o1093 ext_unjustified
2768 NSummary!tactic_arg tactic_arg tactic_arg Summary
2769 P p1093 String main
2770 O o1094 tactic_arg p1093
2771 NSummary!msequent msequent msequent Summary
2772 O o1095 msequent
2773 T t1095 o b1076 b4
2774 B b1095 t1095
2775 T t1096 o b1074 b1095
2776 B b1096 t1096
2777 T t1097 o b762 b1096
2778 B b1097 t1097
2779 T t1098 o b699 b1097
2780 B b1098 t1098
2781 T t1099 o b681 b1098
2782 B b1099 t1099
2783 T t1100 o b760 b1099
2784 B b1100 t1100
2785 T t1101 o b1072 b1100
2786 B b1101 t1101
2787 T t1102 o b1070 b1101
2788 B b1102 t1102
2789 T t1103 o1095 b1081 b1102
2790 B b1103 t1103
2791 NSummary!parent_none parent_none parent_none Summary
2792 O o1103 parent_none
2793 T t1104 o1103
2794 B b1104 t1104
2795 T t1105 o1094 b1103 b4 b1104
2796 B b1105 t1105
2797 NCzf_itt_set!set set set Czf_itt_set
2798 O o1105 set
2799 T t1106 o1105
2800 H h1106 a_1 t1106
2801 H h1107 b_1 t1106
2802 H h1108 x t762
2803 P p1108 Var a_1
2804 O o1108 var p1108
2805 T t1108 o1108
2806 B b1108 t1108
2807 P p1109 Var b_1
2808 O o1109 var p1109
2809 T t1109 o1109
2810 B b1109 t1109
2811 T t1110 o761 b591 b759 b1108 b1109
2812 H h1110 x_1 t1110
2813 T t1111 o596 b585 b1108 b597
2814 B b1111 t1111
2815 T t1112 o596 b585 b1108 b598
2816 B b1112 t1112
2817 T t1113 o761 b591 b759 b1111 b1112
2818 H h1113 x_2 t1113
2819 T t1114 o596 b585 b1109 b597
2820 B b1114 t1114
2821 T t1115 o596 b585 b1109 b598
2822 B b1115 t1115
2823 T t1116 o761 b591 b759 b1114 b1115
2824 S s1116 t684 h h1106 h1107 h1108 h1110 h1113
2825 G s1116 t1116
2826 B b1116 s1116
2827 T t1117 o1095 b1116 b1102
2828 B b1117 t1117
2829 NItt_logic Itt_logic Itt_logic NIL
2830 NItt_logic!implies implies implies Itt_logic
2831 O o1117 implies
2832 B b1118 t1113
2833 B b1119 t1116
2834 T t1119 o1117 b1118 b1119
2835 S s1119 t684 h h1106 h1107 h1108 h1110
2836 G s1119 t1119
2837 B b1120 s1119
2838 T t1120 o1095 b1120 b1102
2839 B b1121 t1120
2840 B b1122 t1110
2841 B b1123 t1119
2842 T t1123 o1117 b1122 b1123
2843 S s1123 t684 h h1106 h1107 h1108
2844 G s1123 t1123
2845 B b1124 s1123
2846 T t1124 o1095 b1124 b1102
2847 B b1125 t1124
2848 B b1126 t762
2849 B b1127 t1123
2850 T t1127 o1117 b1126 b1127
2851 S s1127 t684 h h1106 h1107
2852 G s1127 t1127
2853 B b1128 s1127
2854 T t1128 o1095 b1128 b1102
2855 B b1129 t1128
2856 NItt_logic!all all all Itt_logic
2857 O o1129 all
2858 B b1130 t1106
2859 B b1131 t1127 b_1
2860 T t1131 o1129 b1130 b1131
2861 S s1131 t684 h h1106
2862 G s1131 t1131
2863 B b1132 s1131
2864 T t1132 o1095 b1132 b1102
2865 B b1133 t1132
2866 B b1134 t1131 a_1
2867 T t1134 o1129 b1130 b1134
2868 S s1134 t684 h
2869 G s1134 t1134
2870 B b1135 s1134
2871 T t1135 o1095 b1135 b1102
2872 B b1136 t1135
2873 T t1136 o2 b1105
2874 B b1137 t1136
2875 T t1137 o1094 b1136 b4 b1137
2876 B b1138 t1137
2877 T t1138 o2 b1138
2878 B b1139 t1138
2879 T t1139 o1094 b1133 b4 b1139
2880 B b1140 t1139
2881 T t1140 o2 b1140
2882 B b1141 t1140
2883 T t1141 o1094 b1129 b4 b1141
2884 B b1142 t1141
2885 T t1142 o2 b1142
2886 B b1143 t1142
2887 T t1143 o1094 b1125 b4 b1143
2888 B b1144 t1143
2889 T t1144 o2 b1144
2890 B b1145 t1144
2891 T t1145 o1094 b1121 b4 b1145
2892 B b1146 t1145
2893 T t1146 o2 b1146
2894 B b1147 t1146
2895 T t1147 o1094 b1117 b4 b1147
2896 B b1148 t1147
2897 T t1148 o b1148 b4
2898 B b1149 t1148
2899 T t1149 o1093 b1105 b1149
2900 B b1150 t1149
2901 P p1150 String "equivTransT << op{'g; 'b_1; 'a} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
2902 O o1150 ext_rule p1150
2903 NItt_logic!and and and Itt_logic
2904 O o1151 and
2905 B b1151 t700
2906 B b1152 t760
2907 T t1152 o700 b1111
2908 B b1153 t1152
2909 T t1153 o700 b1112
2910 B b1154 t1153
2911 T t1154 o1151 b1153 b1154
2912 B b1155 t1154
2913 T t1155 o1151 b1152 b1155
2914 B b1156 t1155
2915 T t1156 o1151 b1151 b1156
2916 B b1157 t1156
2917 T t1157 o736 b1111 b591
2918 B b1158 t1157
2919 T t1158 o736 b1112 b591
2920 B b1159 t1158
2921 T t1159 o1151 b1158 b1159
2922 B b1160 t1159
2923 T t1160 o1151 b1157 b1160
2924 B b1161 t1160
2925 NCzf_itt_pair Czf_itt_pair Czf_itt_pair NIL
2926 NCzf_itt_pair!pair pair pair Czf_itt_pair
2927 O o1161 pair
2928 T t1161 o1161 b1111 b1112
2929 B b1162 t1161
2930 T t1162 o736 b1162 b759
2931 B b1163 t1162
2932 T t1163 o1151 b1161 b1163
2933 H h1163 x_2 t1163
2934 T t1164 o736 b1114 b591
2935 S s1164 t684 h h1106 h1107 h1108 h1110 h1163
2936 G s1164 t1164
2937 B b1164 s1164
2938 T t1165 o1095 b1164 b1102
2939 B b1165 t1165
2940 S s1165 t684 h h1106 h1107 h1108 h1110 h1113
2941 G s1165 t1164
2942 B b1166 s1165
2943 T t1166 o1095 b1166 b1102
2944 B b1167 t1166
2945 T t1167 o2 b1148
2946 B b1168 t1167
2947 T t1168 o1094 b1167 b4 b1168
2948 B b1169 t1168
2949 T t1169 o2 b1169
2950 B b1170 t1169
2951 T t1170 o1094 b1165 b4 b1170
2952 B b1171 t1170
2953 T t1171 o761 b591 b759 b1111 b1114
2954 H h1171 u t1171
2955 T t1172 o761 b591 b759 b1114 b1112
2956 H h1172 v t1172
2957 S s1172 t684 h h1106 h1107 h1108 h1110 h1163 h1171 h1172
2958 G s1172 t1116
2959 B b1172 s1172
2960 T t1173 o1095 b1172 b1102
2961 B b1173 t1173
2962 S s1173 t684 h h1106 h1107 h1108 h1110 h1113 h1171 h1172
2963 G s1173 t1116
2964 B b1174 s1173
2965 T t1174 o1095 b1174 b1102
2966 B b1175 t1174
2967 T t1175 o1094 b1175 b4 b1168
2968 B b1176 t1175
2969 T t1176 o2 b1176
2970 B b1177 t1176
2971 T t1177 o1094 b1173 b4 b1177
2972 B b1178 t1177
2973 T t1178 o b1178 b4
2974 B b1179 t1178
2975 T t1179 o b1171 b1179
2976 B b1180 t1179
2977 T t1180 o1093 b1148 b1180
2978 B b1181 t1180
2979 P p1181 String "autoT thenT rwh unfold_equiv 5 ttca"
2980 O o1181 ext_rule p1181
2981 T t1181 o1093 b1171 b4
2982 B b1182 t1181
2983 T t1182 o1181 b1092 b1182 b4 b4
2984 B b1183 t1182
2985 P p1183 String "equivTransT << op{'g; 'b_1; 'b} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
2986 O o1183 ext_rule p1183
2987 T t1183 o1093 b1178 b4
2988 B b1184 t1183
2989 T t1184 o1183 b1092 b1184 b4 b4
2990 B b1185 t1184
2991 T t1185 o b1185 b4
2992 B b1186 t1185
2993 T t1186 o b1183 b1186
2994 B b1187 t1186
2995 T t1187 o1150 b1092 b1181 b1187 b4
2996 B b1188 t1187
2997 T t1188 o b1188 b4
2998 B b1189 t1188
2999 T t1189 o1091 b1092 b1150 b1189 b4
3000 B b1190 t1189
3001 T t1190 o1090 b1190
3002 B b1191 t1190
3003 P p1200 String equiv_op_fun2
3004 O o1200 rule p1200
3005 T t1200 o596 b585 b597 b818
3006 B b1200 t1200
3007 T t1201 o596 b585 b598 b818
3008 B b1201 t1201
3009 T t1202 o761 b591 b759 b1200 b1201
3010 B b1202 t1202 z
3011 T t1203 o1077 b591 b759 b1202
3012 S s1203 t684 h
3013 G s1203 t1203
3014 B b1203 s1203
3015 T t1204 o677 b1203
3016 B b1204 t1204
3017 T t1205 o676 b1077 b1204
3018 B b1205 t1205
3019 T t1206 o676 b1075 b1205
3020 B b1206 t1206
3021 T t1207 o676 b763 b1206
3022 B b1207 t1207
3023 T t1208 o676 b700 b1207
3024 B b1208 t1208
3025 T t1209 o676 b682 b1208
3026 B b1209 t1209
3027 T t1210 o676 b761 b1209
3028 B b1210 t1210
3029 T t1211 o676 b1073 b1210
3030 B b1211 t1211
3031 T t1212 o676 b1071 b1211
3032 B b1212 t1212
3033 T t1213 o1095 b1203 b1102
3034 B b1213 t1213
3035 T t1214 o1094 b1213 b4 b1104
3036 B b1214 t1214
3037 T t1215 o596 b585 b597 b1108
3038 B b1215 t1215
3039 T t1216 o596 b585 b598 b1108
3040 B b1216 t1216
3041 T t1217 o761 b591 b759 b1215 b1216
3042 H h1217 x_2 t1217
3043 T t1218 o596 b585 b597 b1109
3044 B b1218 t1218
3045 T t1219 o596 b585 b598 b1109
3046 B b1219 t1219
3047 T t1220 o761 b591 b759 b1218 b1219
3048 S s1220 t684 h h1106 h1107 h1108 h1110 h1217
3049 G s1220 t1220
3050 B b1220 s1220
3051 T t1221 o1095 b1220 b1102
3052 B b1221 t1221
3053 B b1222 t1217
3054 B b1223 t1220
3055 T t1223 o1117 b1222 b1223
3056 S s1223 t684 h h1106 h1107 h1108 h1110
3057 G s1223 t1223
3058 B b1224 s1223
3059 T t1224 o1095 b1224 b1102
3060 B b1225 t1224
3061 B b1226 t1223
3062 T t1226 o1117 b1122 b1226
3063 S s1226 t684 h h1106 h1107 h1108
3064 G s1226 t1226
3065 B b1227 s1226
3066 T t1227 o1095 b1227 b1102
3067 B b1228 t1227
3068 B b1229 t1226
3069 T t1229 o1117 b1126 b1229
3070 S s1229 t684 h h1106 h1107
3071 G s1229 t1229
3072 B b1230 s1229
3073 T t1230 o1095 b1230 b1102
3074 B b1231 t1230
3075 B b1232 t1229 b_1
3076 T t1232 o1129 b1130 b1232
3077 S s1232 t684 h h1106
3078 G s1232 t1232
3079 B b1233 s1232
3080 T t1233 o1095 b1233 b1102
3081 B b1234 t1233
3082 B b1235 t1232 a_1
3083 T t1235 o1129 b1130 b1235
3084 S s1235 t684 h
3085 G s1235 t1235
3086 B b1236 s1235
3087 T t1236 o1095 b1236 b1102
3088 B b1237 t1236
3089 T t1237 o2 b1214
3090 B b1238 t1237
3091 T t1238 o1094 b1237 b4 b1238
3092 B b1239 t1238
3093 T t1239 o2 b1239
3094 B b1240 t1239
3095 T t1240 o1094 b1234 b4 b1240
3096 B b1241 t1240
3097 T t1241 o2 b1241
3098 B b1242 t1241
3099 T t1242 o1094 b1231 b4 b1242
3100 B b1243 t1242
3101 T t1243 o2 b1243
3102 B b1244 t1243
3103 T t1244 o1094 b1228 b4 b1244
3104 B b1245 t1244
3105 T t1245 o2 b1245
3106 B b1246 t1245
3107 T t1246 o1094 b1225 b4 b1246
3108 B b1247 t1246
3109 T t1247 o2 b1247
3110 B b1248 t1247
3111 T t1248 o1094 b1221 b4 b1248
3112 B b1249 t1248
3113 T t1249 o b1249 b4
3114 B b1250 t1249
3115 T t1250 o1093 b1214 b1250
3116 B b1251 t1250
3117 P p1251 String "equivTransT << op{'g; 'a; 'b_1} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
3118 O o1251 ext_rule p1251
3119 T t1251 o700 b1215
3120 B b1252 t1251
3121 T t1252 o700 b1216
3122 B b1253 t1252
3123 T t1253 o1151 b1252 b1253
3124 B b1254 t1253
3125 T t1254 o1151 b1152 b1254
3126 B b1255 t1254
3127 T t1255 o1151 b1151 b1255
3128 B b1256 t1255
3129 T t1256 o736 b1215 b591
3130 B b1257 t1256
3131 T t1257 o736 b1216 b591
3132 B b1258 t1257
3133 T t1258 o1151 b1257 b1258
3134 B b1259 t1258
3135 T t1259 o1151 b1256 b1259
3136 B b1260 t1259
3137 T t1260 o1161 b1215 b1216
3138 B b1261 t1260
3139 T t1261 o736 b1261 b759
3140 B b1262 t1261
3141 T t1262 o1151 b1260 b1262
3142 H h1262 x_2 t1262
3143 T t1263 o736 b1218 b591
3144 S s1263 t684 h h1106 h1107 h1108 h1110 h1262
3145 G s1263 t1263
3146 B b1263 s1263
3147 T t1264 o1095 b1263 b1102
3148 B b1264 t1264
3149 S s1264 t684 h h1106 h1107 h1108 h1110 h1217
3150 G s1264 t1263
3151 B b1265 s1264
3152 T t1265 o1095 b1265 b1102
3153 B b1266 t1265
3154 T t1266 o2 b1249
3155 B b1267 t1266
3156 T t1267 o1094 b1266 b4 b1267
3157 B b1268 t1267
3158 T t1268 o2 b1268
3159 B b1269 t1268
3160 T t1269 o1094 b1264 b4 b1269
3161 B b1270 t1269
3162 T t1270 o761 b591 b759 b1215 b1218
3163 H h1270 u t1270
3164 T t1271 o761 b591 b759 b1218 b1216
3165 H h1271 v t1271
3166 S s1271 t684 h h1106 h1107 h1108 h1110 h1262 h1270 h1271
3167 G s1271 t1220
3168 B b1271 s1271
3169 T t1272 o1095 b1271 b1102
3170 B b1272 t1272
3171 S s1272 t684 h h1106 h1107 h1108 h1110 h1217 h1270 h1271
3172 G s1272 t1220
3173 B b1273 s1272
3174 T t1273 o1095 b1273 b1102
3175 B b1274 t1273
3176 T t1274 o1094 b1274 b4 b1267
3177 B b1275 t1274
3178 T t1275 o2 b1275
3179 B b1276 t1275
3180 T t1276 o1094 b1272 b4 b1276
3181 B b1277 t1276
3182 T t1277 o b1277 b4
3183 B b1278 t1277
3184 T t1278 o b1270 b1278
3185 B b1279 t1278
3186 T t1279 o1093 b1249 b1279
3187 B b1280 t1279
3188 T t1280 o1093 b1270 b4
3189 B b1281 t1280
3190 T t1281 o1181 b1092 b1281 b4 b4
3191 B b1282 t1281
3192 P p1282 String "equivTransT << op{'g; 'b; 'b_1} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3193 O o1282 ext_rule p1282
3194 T t1282 o1093 b1277 b4
3195 B b1283 t1282
3196 T t1283 o1282 b1092 b1283 b4 b4
3197 B b1284 t1283
3198 T t1284 o b1284 b4
3199 B b1285 t1284
3200 T t1285 o b1282 b1285
3201 B b1286 t1285
3202 T t1286 o1251 b1092 b1280 b1286 b4
3203 B b1287 t1286
3204 T t1287 o b1287 b4
3205 B b1288 t1287
3206 T t1288 o1091 b1092 b1251 b1288 b4
3207 B b1289 t1288
3208 T t1289 o1090 b1289
3209 B b1290 t1289
3210 P p1299 String cancel1
3211 O o1299 rule p1299
3212 P p1300 String J
3213 O o1300 context_param p1300
3214 T t1300 o1300
3215 B b1300 t1300
3216 T t1301 o b1300 b4
3217 B b1301 t1301
3218 T t1302 o b675 b1301
3219 B b1302 t1302
3220 T t1303 o761 b591 b759 b720 b791
3221 H h1303 x t1303
3222 P p1303 Var x
3223 O o1303 var p1303
3224 T t1304 o1303
3225 C h1304 J t1304
3226 S s1304 t679 h h1303 h1304
3227 G s1304 t715
3228 B b1304 s1304
3229 T t1305 o677 b1304
3230 B b1305 t1305
3231 S s1305 t679 h h1303 h1304
3232 G s1305 t718
3233 B b1306 s1305
3234 T t1306 o677 b1306
3235 B b1307 t1306
3236 S s1307 t679 h h1303 h1304
3237 G s1307 t757
3238 B b1308 s1307
3239 T t1308 o677 b1308
3240 B b1309 t1308
3241 S s1309 t679 h h1303 h1304
3242 G s1309 t760
3243 B b1310 s1309
3244 T t1310 o677 b1310
3245 B b1311 t1310
3246 S s1311 t679 h h1303 h1304
3247 G s1311 t681
3248 B b1312 s1311
3249 T t1312 o677 b1312
3250 B b1313 t1312
3251 S s1313 t684 h h1303 h1304
3252 G s1313 t586
3253 B b1314 s1313
3254 T t1314 o677 b1314
3255 B b1315 t1314
3256 S s1315 t684 h h1303 h1304
3257 G s1315 t762
3258 B b1316 s1315
3259 T t1316 o677 b1316
3260 B b1317 t1316
3261 S s1317 t684 h h1303 h1304
3262 G s1317 t736
3263 B b1318 s1317
3264 T t1318 o677 b1318
3265 B b1319 t1318
3266 S s1319 t684 h h1303 h1304
3267 G s1319 t738
3268 B b1320 s1319
3269 T t1320 o677 b1320
3270 B b1321 t1320
3271 S s1321 t684 h h1303 h1304
3272 G s1321 t764
3273 B b1322 s1321
3274 T t1322 o677 b1322
3275 B b1323 t1322
3276 T t1323 o761 b591 b759 b717 b756
3277 S s1323 t684 h h1303 h1304
3278 G s1323 t1323
3279 B b1324 s1323
3280 T t1324 o677 b1324
3281 B b1325 t1324
3282 T t1325 o676 b1323 b1325
3283 B b1326 t1325
3284 T t1326 o676 b1321 b1326
3285 B b1327 t1326
3286 T t1327 o676 b1319 b1327
3287 B b1328 t1327
3288 T t1328 o676 b1317 b1328
3289 B b1329 t1328
3290 T t1329 o676 b1315 b1329
3291 B b1330 t1329
3292 T t1330 o676 b1313 b1330
3293 B b1331 t1330
3294 T t1331 o676 b1311 b1331
3295 B b1332 t1331
3296 T t1332 o676 b1309 b1332
3297 B b1333 t1332
3298 T t1333 o676 b1307 b1333
3299 B b1334 t1333
3300 T t1334 o676 b1305 b1334
3301 B b1335 t1334
3302 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"
3303 O o1335 ext_rule p1335
3304 T t1335 o b1322 b4
3305 B b1336 t1335
3306 T t1336 o b1320 b1336
3307 B b1337 t1336
3308 T t1337 o b1318 b1337
3309 B b1338 t1337
3310 T t1338 o b1316 b1338
3311 B b1339 t1338
3312 T t1339 o b1314 b1339
3313 B b1340 t1339
3314 T t1340 o b1312 b1340
3315 B b1341 t1340
3316 T t1341 o b1310 b1341
3317 B b1342 t1341
3318 T t1342 o b1308 b1342
3319 B b1343 t1342
3320 T t1343 o b1306 b1343
3321 B b1344 t1343
3322 T t1344 o b1304 b1344
3323 B b1345 t1344
3324 T t1345 o1095 b1324 b1345
3325 B b1346 t1345
3326 T t1346 o1094 b1346 b4 b1104
3327 B b1347 t1346
3328 T t1347 o596 b585 b980 b720
3329 B b1348 t1347
3330 T t1348 o596 b585 b980 b791
3331 B b1349 t1348
3332 T t1349 o761 b591 b759 b1348 b1349
3333 H h1349 v t1349
3334 S s1349 t684 h h1303 h1304 h1349
3335 G s1349 t1323
3336 B b1350 s1349
3337 T t1350 o1095 b1350 b1345
3338 B b1351 t1350
3339 T t1351 o2 b1347
3340 B b1352 t1351
3341 T t1352 o1094 b1351 b4 b1352
3342 B b1353 t1352
3343 T t1353 o b1353 b4
3344 B b1354 t1353
3345 T t1354 o1093 b1347 b1354
3346 B b1355 t1354
3347 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"
3348 O o1355 ext_rule p1355
3349 T t1355 o596 b585 b1036 b717
3350 B b1356 t1355
3351 T t1356 o761 b591 b759 b1356 b1349
3352 H h1356 z t1356
3353 S s1356 t684 h h1303 h1304 h1349 h1356
3354 G s1356 t1323
3355 B b1357 s1356
3356 T t1357 o1095 b1357 b1345
3357 B b1358 t1357
3358 T t1358 o2 b1353
3359 B b1359 t1358
3360 T t1359 o1094 b1358 b4 b1359
3361 B b1360 t1359
3362 T t1360 o b1360 b4
3363 B b1361 t1360
3364 T t1361 o1093 b1353 b1361
3365 B b1362 t1361
3366 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"
3367 O o1362 ext_rule p1362
3368 T t1362 o596 b585 b1036 b756
3369 B b1363 t1362
3370 T t1363 o761 b591 b759 b1356 b1363
3371 H h1363 z_1 t1363
3372 S s1363 t684 h h1303 h1304 h1349 h1356 h1363
3373 G s1363 t1323
3374 B b1364 s1363
3375 T t1364 o1095 b1364 b1345
3376 B b1365 t1364
3377 T t1365 o2 b1360
3378 B b1366 t1365
3379 T t1366 o1094 b1365 b4 b1366
3380 B b1367 t1366
3381 T t1367 o b1367 b4
3382 B b1368 t1367
3383 T t1368 o1093 b1360 b1368
3384 B b1369 t1368
3385 P p1369 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"
3386 O o1369 ext_rule p1369
3387 T t1369 o596 b585 b604 b717
3388 B b1370 t1369
3389 T t1370 o596 b585 b604 b756
3390 B b1371 t1370
3391 T t1371 o761 b591 b759 b1370 b1371
3392 H h1371 z_2 t1371
3393 S s1371 t684 h h1303 h1304 h1349 h1356 h1363 h1371
3394 G s1371 t1323
3395 B b1372 s1371
3396 T t1372 o1095 b1372 b1345
3397 B b1373 t1372
3398 T t1373 o2 b1367
3399 B b1374 t1373
3400 T t1374 o1094 b1373 b4 b1374
3401 B b1375 t1374
3402 T t1375 o b1375 b4
3403 B b1376 t1375
3404 T t1376 o1093 b1367 b1376
3405 B b1377 t1376
3406 P p1377 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"
3407 O o1377 ext_rule p1377
3408 T t1377 o761 b591 b759 b717 b1371
3409 H h1377 z_3 t1377
3410 S s1377 t684 h h1303 h1304 h1349 h1356 h1363 h1371 h1377
3411 G s1377 t1323
3412 B b1378 s1377
3413 T t1378 o1095 b1378 b1345
3414 B b1379 t1378
3415 T t1379 o2 b1375
3416 B b1380 t1379
3417 T t1380 o1094 b1379 b4 b1380
3418 B b1381 t1380
3419 T t1381 o b1381 b4
3420 B b1382 t1381
3421 T t1382 o1093 b1375 b1382
3422 B b1383 t1382
3423 P p1383 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"
3424 O o1383 ext_rule p1383
3425 T t1383 o1093 b1381 b4
3426 B b1384 t1383
3427 T t1384 o1383 b1092 b1384 b4 b4
3428 B b1385 t1384
3429 T t1385 o b1385 b4
3430 B b1386 t1385
3431 T t1386 o1377 b1092 b1383 b1386 b4
3432 B b1387 t1386
3433 T t1387 o b1387 b4
3434 B b1388 t1387
3435 T t1388 o1369 b1092 b1377 b1388 b4
3436 B b1389 t1388
3437 T t1389 o b1389 b4
3438 B b1390 t1389
3439 T t1390 o1362 b1092 b1369 b1390 b4
3440 B b1391 t1390
3441 T t1391 o b1391 b4
3442 B b1392 t1391
3443 T t1392 o1355 b1092 b1362 b1392 b4
3444 B b1393 t1392
3445 T t1393 o b1393 b4
3446 B b1394 t1393
3447 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"
3448 O o1394 ext_rule p1394
3449 H h1394 v t1303
3450 H h1395 v_1 t1349
3451 S s1395 t684 h h1394 h1395
3452 G s1395 t1323
3453 B b1395 s1395
3454 S s1396 t684 h
3455 G s1396 t1303
3456 B b1396 s1396
3457 T t1396 o b1396 b4
3458 B b1397 t1396
3459 T t1397 o b764 b1397
3460 B b1398 t1397
3461 T t1398 o b738 b1398
3462 B b1399 t1398
3463 T t1399 o b736 b1399
3464 B b1400 t1399
3465 T t1400 o b762 b1400
3466 B b1401 t1400
3467 T t1401 o b699 b1401
3468 B b1402 t1401
3469 T t1402 o b681 b1402
3470 B b1403 t1402
3471 T t1403 o b760 b1403
3472 B b1404 t1403
3473 T t1404 o b757 b1404
3474 B b1405 t1404
3475 T t1405 o b718 b1405
3476 B b1406 t1405
3477 T t1406 o b715 b1406
3478 B b1407 t1406
3479 T t1407 o1095 b1395 b1407
3480 B b1408 t1407
3481 S s1408 t684 h h1394
3482 G s1408 t1323
3483 B b1409 s1408
3484 T t1409 o1095 b1409 b1407
3485 B b1410 t1409
3486 S s1410 t684 h
3487 G s1410 t1323
3488 B b1411 s1410
3489 T t1411 o1095 b1411 b1407
3490 B b1412 t1411
3491 T t1412 o1094 b1412 b4 b1104
3492 B b1413 t1412
3493 T t1413 o2 b1413
3494 B b1414 t1413
3495 T t1414 o1094 b1410 b4 b1414
3496 B b1415 t1414
3497 T t1415 o2 b1415
3498 B b1416 t1415
3499 T t1416 o1094 b1408 b4 b1416
3500 B b1417 t1416
3501 S s1417 t684 h h1394 h1395 h1356
3502 G s1417 t1323
3503 B b1418 s1417
3504 T t1418 o1095 b1418 b1407
3505 B b1419 t1418
3506 T t1419 o2 b1417
3507 B b1420 t1419
3508 T t1420 o1094 b1419 b4 b1420
3509 B b1421 t1420
3510 T t1421 o b1421 b4
3511 B b1422 t1421
3512 T t1422 o1093 b1417 b1422
3513 B b1423 t1422
3514 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"
3515 O o1423 ext_rule p1423
3516 S s1423 t684 h h1394 h1395 h1356 h1363
3517 G s1423 t1323
3518 B b1424 s1423
3519 T t1424 o1095 b1424 b1407
3520 B b1425 t1424
3521 T t1425 o2 b1421
3522 B b1426 t1425
3523 T t1426 o1094 b1425 b4 b1426
3524 B b1427 t1426
3525 T t1427 o b1427 b4
3526 B b1428 t1427
3527 T t1428 o1093 b1421 b1428
3528 B b1429 t1428
3529 P p1429 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 ttca"
3530 O o1429 ext_rule p1429
3531 S s1429 t684 h h1394 h1395 h1356 h1363 h1371
3532 G s1429 t1323
3533 B b1430 s1429
3534 T t1430 o1095 b1430 b1407
3535 B b1431 t1430
3536 T t1431 o2 b1427
3537 B b1432 t1431
3538 T t1432 o1094 b1431 b4 b1432
3539 B b1433 t1432
3540 T t1433 o b1433 b4
3541 B b1434 t1433
3542 T t1434 o1093 b1427 b1434
3543 B b1435 t1434
3544 P p1435 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 6 ttca"
3545 O o1435 ext_rule p1435
3546 S s1435 t684 h h1394 h1395 h1356 h1363 h1371 h1377
3547 G s1435 t1323
3548 B b1436 s1435
3549 T t1436 o1095 b1436 b1407
3550 B b1437 t1436
3551 T t1437 o2 b1433
3552 B b1438 t1437
3553 T t1438 o1094 b1437 b4 b1438
3554 B b1439 t1438
3555 T t1439 o b1439 b4
3556 B b1440 t1439
3557 T t1440 o1093 b1433 b1440
3558 B b1441 t1440
3559 P p1441 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 7 ttca"
3560 O o1441 ext_rule p1441
3561 T t1441 o1093 b1439 b4
3562 B b1442 t1441
3563 T t1442 o1441 b1092 b1442 b4 b4
3564 B b1443 t1442
3565 T t1443 o b1443 b4
3566 B b1444 t1443
3567 T t1444 o1435 b1092 b1441 b1444 b4
3568 B b1445 t1444
3569 T t1445 o b1445 b4
3570 B b1446 t1445
3571 T t1446 o1429 b1092 b1435 b1446 b4
3572 B b1447 t1446
3573 T t1447 o b1447 b4
3574 B b1448 t1447
3575 T t1448 o1423 b1092 b1429 b1448 b4
3576 B b1449 t1448
3577 T t1449 o b1449 b4
3578 B b1450 t1449
3579 T t1450 o1394 b1092 b1423 b1450 b4
3580 B b1451 t1450
3581 T t1451 o b1451 b4
3582 B b1452 t1451
3583 T t1452 o1335 b1092 b1355 b1394 b1452
3584 B b1453 t1452
3585 T t1453 o1090 b1453
3586 B b1454 t1453
3587 T t1454 o1299 b1302 b1335 b1454 b4
3588 B b1455 t1454
3589 P p1458 String cancel2
3590 O o1458 rule p1458
3591 H h1458 x t793
3592 S s1458 t679 h h1458 h1304
3593 G s1458 t715
3594 B b1458 s1458
3595 T t1458 o677 b1458
3596 B b1459 t1458
3597 S s1459 t679 h h1458 h1304
3598 G s1459 t718
3599 B b1460 s1459
3600 T t1460 o677 b1460
3601 B b1461 t1460
3602 S s1461 t679 h h1458 h1304
3603 G s1461 t757
3604 B b1462 s1461
3605 T t1462 o677 b1462
3606 B b1463 t1462
3607 S s1463 t679 h h1458 h1304
3608 G s1463 t760
3609 B b1464 s1463
3610 T t1464 o677 b1464
3611 B b1465 t1464
3612 S s1465 t679 h h1458 h1304
3613 G s1465 t681
3614 B b1466 s1465
3615 T t1466 o677 b1466
3616 B b1467 t1466
3617 S s1467 t684 h h1458 h1304
3618 G s1467 t586
3619 B b1468 s1467
3620 T t1468 o677 b1468
3621 B b1469 t1468
3622 S s1469 t684 h h1458 h1304
3623 G s1469 t762
3624 B b1470 s1469
3625 T t1470 o677 b1470
3626 B b1471 t1470
3627 S s1471 t684 h h1458 h1304
3628 G s1471 t736
3629 B b1472 s1471
3630 T t1472 o677 b1472
3631 B b1473 t1472
3632 S s1473 t684 h h1458 h1304
3633 G s1473 t738
3634 B b1474 s1473
3635 T t1474 o677 b1474
3636 B b1475 t1474
3637 S s1475 t684 h h1458 h1304
3638 G s1475 t764
3639 B b1476 s1475
3640 T t1476 o677 b1476
3641 B b1477 t1476
3642 S s1477 t684 h h1458 h1304
3643 G s1477 t766
3644 B b1478 s1477
3645 T t1478 o677 b1478
3646 B b1479 t1478
3647 T t1479 o676 b1477 b1479
3648 B b1480 t1479
3649 T t1480 o676 b1475 b1480
3650 B b1481 t1480
3651 T t1481 o676 b1473 b1481
3652 B b1482 t1481
3653 T t1482 o676 b1471 b1482
3654 B b1483 t1482
3655 T t1483 o676 b1469 b1483
3656 B b1484 t1483
3657 T t1484 o676 b1467 b1484
3658 B b1485 t1484
3659 T t1485 o676 b1465 b1485
3660 B b1486 t1485
3661 T t1486 o676 b1463 b1486
3662 B b1487 t1486
3663 T t1487 o676 b1461 b1487
3664 B b1488 t1487
3665 T t1488 o676 b1459 b1488
3666 B b1489 t1488
3667 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"
3668 O o1489 ext_rule p1489
3669 T t1489 o b1476 b4
3670 B b1490 t1489
3671 T t1490 o b1474 b1490
3672 B b1491 t1490
3673 T t1491 o b1472 b1491
3674 B b1492 t1491
3675 T t1492 o b1470 b1492
3676 B b1493 t1492
3677 T t1493 o b1468 b1493
3678 B b1494 t1493
3679 T t1494 o b1466 b1494
3680 B b1495 t1494
3681 T t1495 o b1464 b1495
3682 B b1496 t1495
3683 T t1496 o b1462 b1496
3684 B b1497 t1496
3685 T t1497 o b1460 b1497
3686 B b1498 t1497
3687 T t1498 o b1458 b1498
3688 B b1499 t1498
3689 T t1499 o1095 b1478 b1499
3690 B b1500 t1499
3691 T t1500 o1094 b1500 b4 b1104
3692 B b1501 t1500
3693 T t1501 o609 b585 b756
3694 B b1502 t1501
3695 T t1502 o596 b585 b791 b1502
3696 B b1503 t1502
3697 T t1503 o596 b585 b792 b1502
3698 B b1504 t1503
3699 T t1504 o761 b591 b759 b1503 b1504
3700 H h1504 v t1504
3701 S s1504 t684 h h1458 h1304 h1504
3702 G s1504 t766
3703 B b1505 s1504
3704 T t1505 o1095 b1505 b1499
3705 B b1506 t1505
3706 T t1506 o2 b1501
3707 B b1507 t1506
3708 T t1507 o1094 b1506 b4 b1507
3709 B b1508 t1507
3710 T t1508 o b1508 b4
3711 B b1509 t1508
3712 T t1509 o1093 b1501 b1509
3713 B b1510 t1509
3714 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"
3715 O o1510 ext_rule p1510
3716 T t1510 o596 b585 b756 b1502
3717 B b1511 t1510
3718 T t1511 o596 b585 b714 b1511
3719 B b1512 t1511
3720 T t1512 o761 b591 b759 b1512 b1504
3721 H h1512 z t1512
3722 S s1512 t684 h h1458 h1304 h1504 h1512
3723 G s1512 t766
3724 B b1513 s1512
3725 T t1513 o1095 b1513 b1499
3726 B b1514 t1513
3727 T t1514 o2 b1508
3728 B b1515 t1514
3729 T t1515 o1094 b1514 b4 b1515
3730 B b1516 t1515
3731 T t1516 o b1516 b4
3732 B b1517 t1516
3733 T t1517 o1093 b1508 b1517
3734 B b1518 t1517
3735 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"
3736 O o1518 ext_rule p1518
3737 T t1518 o596 b585 b717 b1511
3738 B b1519 t1518
3739 T t1519 o761 b591 b759 b1512 b1519
3740 H h1519 z_1 t1519
3741 S s1519 t684 h h1458 h1304 h1504 h1512 h1519
3742 G s1519 t766
3743 B b1520 s1519
3744 T t1520 o1095 b1520 b1499
3745 B b1521 t1520
3746 T t1521 o2 b1516
3747 B b1522 t1521
3748 T t1522 o1094 b1521 b4 b1522
3749 B b1523 t1522
3750 T t1523 o b1523 b4
3751 B b1524 t1523
3752 T t1524 o1093 b1516 b1524
3753 B b1525 t1524
3754 P p1525 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 6 ttca"
3755 O o1525 ext_rule p1525
3756 T t1525 o596 b585 b714 b604
3757 B b1526 t1525
3758 T t1526 o596 b585 b717 b604
3759 B b1527 t1526
3760 T t1527 o761 b591 b759 b1526 b1527
3761 H h1527 z_2 t1527
3762 S s1527 t684 h h1458 h1304 h1504 h1512 h1519 h1527
3763 G s1527 t766
3764 B b1528 s1527
3765 T t1528 o1095 b1528 b1499
3766 B b1529 t1528
3767 T t1529 o2 b1523
3768 B b1530 t1529
3769 T t1530 o1094 b1529 b4 b1530
3770 B b1531 t1530
3771 T t1531 o b1531 b4
3772 B b1532 t1531
3773 T t1532 o1093 b1523 b1532
3774 B b1533 t1532
3775 P p1533 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's1; id{'g}}; 's1} >> 7 ttca"
3776 O o1533 ext_rule p1533
3777 T t1533 o761 b591 b759 b714 b1527
3778 H h1533 z_3 t1533
3779 S s1533 t684 h h1458 h1304 h1504 h1512 h1519 h1527 h1533
3780 G s1533 t766
3781 B b1534 s1533
3782 T t1534 o1095 b1534 b1499
3783 B b1535 t1534
3784 T t1535 o2 b1531
3785 B b1536 t1535
3786 T t1536 o1094 b1535 b4 b1536
3787 B b1537 t1536
3788 T t1537 o b1537 b4
3789 B b1538 t1537
3790 T t1538 o1093 b1531 b1538
3791 B b1539 t1538
3792 P p1539 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's2; id{'g}}; 's2} >> 8 ttca"
3793 O o1539 ext_rule p1539
3794 T t1539 o1093 b1537 b4
3795 B b1540 t1539
3796 T t1540 o1539 b1092 b1540 b4 b4
3797 B b1541 t1540
3798 T t1541 o b1541 b4
3799 B b1542 t1541
3800 T t1542 o1533 b1092 b1539 b1542 b4
3801 B b1543 t1542
3802 T t1543 o b1543 b4
3803 B b1544 t1543
3804 T t1544 o1525 b1092 b1533 b1544 b4
3805 B b1545 t1544
3806 T t1545 o b1545 b4
3807 B b1546 t1545
3808 T t1546 o1518 b1092 b1525 b1546 b4
3809 B b1547 t1546
3810 T t1547 o b1547 b4
3811 B b1548 t1547
3812 T t1548 o1510 b1092 b1518 b1548 b4
3813 B b1549 t1548
3814 T t1549 o b1549 b4
3815 B b1550 t1549
3816 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"
3817 O o1550 ext_rule p1550
3818 H h1550 v t793
3819 H h1551 v_1 t1504
3820 S s1551 t684 h h1550 h1551
3821 G s1551 t766
3822 B b1551 s1551
3823 T t1551 o b793 b4
3824 B b1552 t1551
3825 T t1552 o b764 b1552
3826 B b1553 t1552
3827 T t1553 o b738 b1553
3828 B b1554 t1553
3829 T t1554 o b736 b1554
3830 B b1555 t1554
3831 T t1555 o b762 b1555
3832 B b1556 t1555
3833 T t1556 o b699 b1556
3834 B b1557 t1556
3835 T t1557 o b681 b1557
3836 B b1558 t1557
3837 T t1558 o b760 b1558
3838 B b1559 t1558
3839 T t1559 o b757 b1559
3840 B b1560 t1559
3841 T t1560 o b718 b1560
3842 B b1561 t1560
3843 T t1561 o b715 b1561
3844 B b1562 t1561
3845 T t1562 o1095 b1551 b1562
3846 B b1563 t1562
3847 S s1563 t684 h h1550
3848 G s1563 t766
3849 B b1564 s1563
3850 T t1564 o1095 b1564 b1562
3851 B b1565 t1564
3852 T t1565 o1095 b766 b1562
3853 B b1566 t1565
3854 T t1566 o1094 b1566 b4 b1104
3855 B b1567 t1566
3856 T t1567 o2 b1567
3857 B b1568 t1567
3858 T t1568 o1094 b1565 b4 b1568
3859 B b1569 t1568
3860 T t1569 o2 b1569
3861 B b1570 t1569
3862 T t1570 o1094 b1563 b4 b1570
3863 B b1571 t1570
3864 S s1571 t684 h h1550 h1551 h1512
3865 G s1571 t766
3866 B b1572 s1571
3867 T t1572 o1095 b1572 b1562
3868 B b1573 t1572
3869 T t1573 o2 b1571
3870 B b1574 t1573
3871 T t1574 o1094 b1573 b4 b1574
3872 B b1575 t1574
3873 T t1575 o b1575 b4
3874 B b1576 t1575
3875 T t1576 o1093 b1571 b1576
3876 B b1577 t1576
3877 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"
3878 O o1577 ext_rule p1577
3879 S s1577 t684 h h1550 h1551 h1512 h1519
3880 G s1577 t766
3881 B b1578 s1577
3882 T t1578 o1095 b1578 b1562
3883 B b1579 t1578
3884 T t1579 o2 b1575
3885 B b1580 t1579
3886 T t1580 o1094 b1579 b4 b1580
3887 B b1581 t1580
3888 T t1581 o b1581 b4
3889 B b1582 t1581
3890 T t1582 o1093 b1575 b1582
3891 B b1583 t1582
3892 P p1583 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 5 ttca"
3893 O o1583 ext_rule p1583
3894 S s1583 t684 h h1550 h1551 h1512 h1519 h1527
3895 G s1583 t766
3896 B b1584 s1583
3897 T t1584 o1095 b1584 b1562
3898 B b1585 t1584
3899 T t1585 o2 b1581
3900 B b1586 t1585
3901 T t1586 o1094 b1585 b4 b1586
3902 B b1587 t1586
3903 T t1587 o b1587 b4
3904 B b1588 t1587
3905 T t1588 o1093 b1581 b1588
3906 B b1589 t1588
3907 P p1589 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's1; id{'g}}; 's1} >> 6 ttca"
3908 O o1589 ext_rule p1589
3909 S s1589 t684 h h1550 h1551 h1512 h1519 h1527 h1533
3910 G s1589 t766
3911 B b1590 s1589
3912 T t1590 o1095 b1590 b1562
3913 B b1591 t1590
3914 T t1591 o2 b1587
3915 B b1592 t1591
3916 T t1592 o1094 b1591 b4 b1592
3917 B b1593 t1592
3918 T t1593 o b1593 b4
3919 B b1594 t1593
3920 T t1594 o1093 b1587 b1594
3921 B b1595 t1594
3922 P p1595 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's2; id{'g}}; 's2} >> 7 ttca"
3923 O o1595 ext_rule p1595
3924 T t1595 o1093 b1593 b4
3925 B b1596 t1595
3926 T t1596 o1595 b1092 b1596 b4 b4
3927 B b1597 t1596
3928 T t1597 o b1597 b4
3929 B b1598 t1597
3930 T t1598 o1589 b1092 b1595 b1598 b4
3931 B b1599 t1598
3932 T t1599 o b1599 b4
3933 B b1600 t1599
3934 T t1600 o1583 b1092 b1589 b1600 b4
3935 B b1601 t1600
3936 T t1601 o b1601 b4
3937 B b1602 t1601
3938 T t1602 o1577 b1092 b1583 b1602 b4
3939 B b1603 t1602
3940 T t1603 o b1603 b4
3941 B b1604 t1603
3942 T t1604 o1550 b1092 b1577 b1604 b4
3943 B b1605 t1604
3944 T t1605 o b1605 b4
3945 B b1606 t1605
3946 T t1606 o1489 b1092 b1510 b1550 b1606
3947 B b1607 t1606
3948 T t1607 o1090 b1607
3949 B b1608 t1607
3950 T t1608 o1458 b1302 b1489 b1608 b4
3951 B b1609 t1608
3952 NOcaml!str_let str_let str_let Ocaml
3953 NOcaml!patt_var patt_var patt_var Ocaml
3954 NOcaml!patt_done patt_done patt_done Ocaml
3955 NOcaml!fun fun fun Ocaml
3956 NOcaml!patt_if patt_if patt_if Ocaml
3957 NOcaml!patt_body patt_body patt_body Ocaml
3958 NOcaml!let let let Ocaml
3959 NOcaml!patt_tuple patt_tuple patt_tuple Ocaml
3960 NOcaml!patt_tuple_arg patt_tuple_arg patt_tuple_arg Ocaml
3961 NOcaml!patt_tuple_end patt_tuple_end patt_tuple_end Ocaml
3962 NOcaml!patt_in patt_in patt_in Ocaml
3963 NOcaml!apply apply apply Ocaml
3964 NOcaml!lid lid lid Ocaml
3965 O o1632 lid p1299
3966 T t1632 o1632
3967 B b1632 t1632
3968 P p1634 Var j
3969 O o1634 var p1634
3970 T t1634 o1634
3971 B b1634 t1634
3972 P p1637 Var k
3973 O o1637 var p1637
3974 T t1637 o1637
3975 B b1637 t1637
3976 P p1640 Var p
3977 O o1640 var p1640
3978 T t1640 o1640
3979 B b1640 t1640
3980 NOcaml!proj proj proj Ocaml
3981 O o1653 uid p539
3982 T t1653 o1653
3983 B b1653 t1653
3984 P p1655 String hyp_indices
3985 O o1655 lid p1655
3986 T t1655 o1655
3987 B b1655 t1655
3988 P p1660 Var i
3989 O o1660 var p1660
3990 T t1660 o1660
3991 B b1660 t1660
3992 O o1699 lid p1458
3993 T t1699 o1699
3994 B b1699 t1699
3995 P p1739 String unique_id1
3996 O o1739 rule p1739
3997 P p1740 Var e2
3998 O o1740 var p1740
3999 T t1740 o1740
4000 B b1740 t1740
4001 T t1741 o700 b1740
4002 S s1741 t679 h
4003 G s1741 t1741
4004 B b1741 s1741
4005 T t1742 o677 b1741
4006 B b1742 t1742
4007 T t1743 o736 b1740 b591
4008 S s1743 t684 h
4009 G s1743 t1743
4010 B b1743 s1743
4011 T t1744 o677 b1743
4012 B b1744 t1744
4013 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4014 NCzf_itt_dall!dall dall dall Czf_itt_dall
4015 O o1744 dall
4016 T t1745 o596 b585 b1740 b815
4017 B b1745 t1745
4018 T t1746 o761 b591 b759 b1745 b815
4019 B b1746 t1746 s
4020 T t1747 o1744 b591 b1746
4021 S s1747 t684 h
4022 G s1747 t1747
4023 B b1747 s1747
4024 T t1748 o677 b1747
4025 B b1748 t1748
4026 T t1749 o761 b591 b759 b1740 b604
4027 S s1749 t684 h
4028 G s1749 t1749
4029 B b1749 s1749
4030 T t1750 o677 b1749
4031 B b1750 t1750
4032 T t1751 o676 b1748 b1750
4033 B b1751 t1751
4034 T t1752 o676 b1744 b1751
4035 B b1752 t1752
4036 T t1753 o676 b763 b1752
4037 B b1753 t1753
4038 T t1754 o676 b700 b1753
4039 B b1754 t1754
4040 T t1755 o676 b682 b1754
4041 B b1755 t1755
4042 T t1756 o676 b761 b1755
4043 B b1756 t1756
4044 T t1757 o676 b1742 b1756
4045 B b1757 t1757
4046 P p1757 String "assumT 7 thenT withT << id{'g} >> (dT 2) ttca"
4047 O o1757 ext_rule p1757
4048 T t1758 o b1747 b4
4049 B b1758 t1758
4050 T t1759 o b1743 b1758
4051 B b1759 t1759
4052 T t1760 o b762 b1759
4053 B b1760 t1760
4054 T t1761 o b699 b1760
4055 B b1761 t1761
4056 T t1762 o b681 b1761
4057 B b1762 t1762
4058 T t1763 o b760 b1762
4059 B b1763 t1763
4060 T t1764 o b1741 b1763
4061 B b1764 t1764
4062 T t1765 o1095 b1749 b1764
4063 B b1765 t1765
4064 T t1766 o1094 b1765 b4 b1104
4065 B b1766 t1766
4066 P p1766 String wf
4067 O o1766 tactic_arg p1766
4068 H h1766 v t1747
4069 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
4070 O o1767 fun_prop
4071 P p1767 Var w
4072 O o1768 var p1767
4073 T t1768 o1768
4074 B b1768 t1768
4075 T t1769 o596 b585 b1740 b1768
4076 B b1769 t1769
4077 T t1770 o761 b591 b759 b1769 b1768
4078 B b1770 t1770 w
4079 T t1771 o1767 b1770
4080 S s1771 t684 h h1766
4081 G s1771 t1771
4082 B b1771 s1771
4083 T t1772 o1095 b1771 b1764
4084 B b1772 t1772
4085 S s1772 t684 h h1766
4086 G s1772 t1749
4087 B b1773 s1772
4088 T t1773 o1095 b1773 b1764
4089 B b1774 t1773
4090 NSummary!arg_named arg_named arg_named Summary
4091 P p1774 String with
4092 O o1774 arg_named p1774
4093 NSummary!arg_term_list arg_term_list arg_term_list Summary
4094 O o1775 arg_term_list
4095 T t1775 o b604 b4
4096 B b1775 t1775
4097 T t1776 o1775 b1775
4098 B b1776 t1776
4099 T t1777 o1774 b1776
4100 B b1777 t1777
4101 T t1778 o b1777 b4
4102 B b1778 t1778
4103 T t1779 o2 b1766
4104 B b1779 t1779
4105 T t1780 o1094 b1774 b1778 b1779
4106 B b1780 t1780
4107 T t1781 o2 b1780
4108 B b1781 t1781
4109 T t1782 o1766 b1772 b4 b1781
4110 B b1782 t1782
4111 T t1783 o596 b585 b1740 b604
4112 B b1783 t1783
4113 T t1784 o761 b591 b759 b1783 b604
4114 H h1784 w t1784
4115 S s1784 t684 h h1766 h1784
4116 G s1784 t1749
4117 B b1784 s1784
4118 T t1785 o1095 b1784 b1764
4119 B b1785 t1785
4120 T t1786 o1094 b1785 b4 b1781
4121 B b1786 t1786
4122 T t1787 o b1786 b4
4123 B b1787 t1787
4124 T t1788 o b1782 b1787
4125 B b1788 t1788
4126 T t1789 o1093 b1766 b1788
4127 B b1789 t1789
4128 P p1789 String "rwh unfold_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
4129 O o1789 ext_rule p1789
4130 H h1789 s1 t1106
4131 H h1790 s2 t1106
4132 NCzf_itt_eq!equal equal1790 equal Czf_itt_eq
4133 O o1790 equal1790
4134 T t1790 o1790 b714 b717
4135 H h1791 x t1790
4136 T t1791 o596 b585 b1740 b714
4137 B b1791 t1791
4138 T t1792 o761 b591 b759 b1791 b714
4139 H h1792 x_1 t1792
4140 T t1793 o596 b585 b1740 b717
4141 B b1793 t1793
4142 T t1794 o761 b591 b759 b1793 b717
4143 S s1794 t684 h h1766 h1789 h1790 h1791 h1792
4144 G s1794 t1794
4145 B b1794 s1794
4146 T t1795 o1095 b1794 b1764
4147 B b1795 t1795
4148 B b1796 t1792
4149 B b1797 t1794
4150 T t1797 o1117 b1796 b1797
4151 S s1797 t684 h h1766 h1789 h1790 h1791
4152 G s1797 t1797
4153 B b1798 s1797
4154 T t1798 o1095 b1798 b1764
4155 B b1799 t1798
4156 B b1800 t1790
4157 B b1801 t1797
4158 T t1801 o1117 b1800 b1801
4159 S s1801 t684 h h1766 h1789 h1790
4160 G s1801 t1801
4161 B b1802 s1801
4162 T t1802 o1095 b1802 b1764
4163 B b1803 t1802
4164 B b1804 t1801 s2
4165 T t1804 o1129 b1130 b1804
4166 S s1804 t684 h h1766 h1789
4167 G s1804 t1804
4168 B b1805 s1804
4169 T t1805 o1095 b1805 b1764
4170 B b1806 t1805
4171 B b1807 t1804 s1
4172 T t1807 o1129 b1130 b1807
4173 S s1807 t684 h h1766
4174 G s1807 t1807
4175 B b1808 s1807
4176 T t1808 o1095 b1808 b1764
4177 B b1809 t1808
4178 T t1809 o2 b1782
4179 B b1810 t1809
4180 T t1810 o1766 b1809 b4 b1810
4181 B b1811 t1810
4182 T t1811 o2 b1811
4183 B b1812 t1811
4184 T t1812 o1094 b1806 b4 b1812
4185 B b1813 t1812
4186 T t1813 o2 b1813
4187 B b1814 t1813
4188 T t1814 o1094 b1803 b4 b1814
4189 B b1815 t1814
4190 T t1815 o2 b1815
4191 B b1816 t1815
4192 T t1816 o1094 b1799 b4 b1816
4193 B b1817 t1816
4194 T t1817 o2 b1817
4195 B b1818 t1817
4196 T t1818 o1094 b1795 b4 b1818
4197 B b1819 t1818
4198 T t1819 o b1819 b4
4199 B b1820 t1819
4200 T t1820 o1093 b1782 b1820
4201 B b1821 t1820
4202 P p1821 String "equivTransT << op{'g; 'e2; 's2} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
4203 O o1821 ext_rule p1821
4204 T t1821 o700 b1791
4205 B b1822 t1821
4206 B b1823 t715
4207 T t1823 o1151 b1822 b1823
4208 B b1824 t1823
4209 T t1824 o1151 b1152 b1824
4210 B b1825 t1824
4211 T t1825 o1151 b1151 b1825
4212 B b1826 t1825
4213 T t1826 o736 b1791 b591
4214 B b1827 t1826
4215 B b1828 t736
4216 T t1828 o1151 b1827 b1828
4217 B b1829 t1828
4218 T t1829 o1151 b1826 b1829
4219 B b1830 t1829
4220 T t1830 o1161 b1791 b714
4221 B b1831 t1830
4222 T t1831 o736 b1831 b759
4223 B b1832 t1831
4224 T t1832 o1151 b1830 b1832
4225 H h1832 x_1 t1832
4226 T t1833 o736 b1793 b591
4227 S s1833 t684 h h1766 h1789 h1790 h1791 h1832
4228 G s1833 t1833
4229 B b1833 s1833
4230 T t1834 o1095 b1833 b1764
4231 B b1834 t1834
4232 S s1834 t684 h h1766 h1789 h1790 h1791 h1792
4233 G s1834 t1833
4234 B b1835 s1834
4235 T t1835 o1095 b1835 b1764
4236 B b1836 t1835
4237 T t1836 o2 b1819
4238 B b1837 t1836
4239 T t1837 o1094 b1836 b4 b1837
4240 B b1838 t1837
4241 T t1838 o2 b1838
4242 B b1839 t1838
4243 T t1839 o1094 b1834 b4 b1839
4244 B b1840 t1839
4245 T t1840 o761 b591 b759 b1791 b1793
4246 H h1840 u t1840
4247 T t1841 o761 b591 b759 b1793 b714
4248 H h1841 v_1 t1841
4249 S s1841 t684 h h1766 h1789 h1790 h1791 h1832 h1840 h1841
4250 G s1841 t1794
4251 B b1841 s1841
4252 T t1842 o1095 b1841 b1764
4253 B b1842 t1842
4254 S s1842 t684 h h1766 h1789 h1790 h1791 h1792 h1840 h1841
4255 G s1842 t1794
4256 B b1843 s1842
4257 T t1843 o1095 b1843 b1764
4258 B b1844 t1843
4259 T t1844 o1094 b1844 b4 b1837
4260 B b1845 t1844
4261 T t1845 o2 b1845
4262 B b1846 t1845
4263 T t1846 o1094 b1842 b4 b1846
4264 B b1847 t1846
4265 T t1847 o b1847 b4
4266 B b1848 t1847
4267 T t1848 o b1840 b1848
4268 B b1849 t1848
4269 T t1849 o1093 b1819 b1849
4270 B b1850 t1849
4271 P p1850 String "autoT thenT setSubstT << equal{'s1; 's2} >> 11 ttca"
4272 O o1850 ext_rule p1850
4273 T t1850 o1093 b1840 b4
4274 B b1851 t1850
4275 T t1851 o1850 b1092 b1851 b4 b4
4276 B b1852 t1851
4277 P p1852 String "equivTransT << 's2 >> 8 thenT autoT"
4278 O o1852 ext_rule p1852
4279 H h1852 y_2 t700
4280 H h1853 y_1 t760
4281 H h1854 y_3 t1821
4282 H h1855 z_1 t715
4283 H h1856 y t1826
4284 H h1857 z_2 t736
4285 H h1858 z t1831
4286 S s1858 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1854 h1855 h1856 h1857 h1858 h1840 h1841
4287 G s1858 t738
4288 B b1858 s1858
4289 T t1858 o1095 b1858 b1764
4290 B b1859 t1858
4291 S s1859 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1854 h1855 h1856 h1857 h1858 h1840 h1841
4292 G s1859 t1833
4293 B b1860 s1859
4294 T t1860 o1095 b1860 b1764
4295 B b1861 t1860
4296 P p1861 String d_auto
4297 O o1861 arg_named p1861
4298 NSummary!arg_bool arg_bool arg_bool Summary
4299 P p1862 String true
4300 O o1862 arg_bool p1862
4301 T t1862 o1862
4302 B b1862 t1862
4303 T t1863 o1861 b1862
4304 B b1863 t1863
4305 T t1864 o b1863 b4
4306 B b1864 t1864
4307 H h1864 z_3 t1823
4308 S s1864 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1864 h1856 h1857 h1858 h1840 h1841
4309 G s1864 t1833
4310 B b1865 s1864
4311 T t1865 o1095 b1865 b1764
4312 B b1866 t1865
4313 H h1866 z_1 t1824
4314 S s1866 t684 h h1766 h1789 h1790 h1791 h1852 h1866 h1856 h1857 h1858 h1840 h1841
4315 G s1866 t1833
4316 B b1867 s1866
4317 T t1867 o1095 b1867 b1764
4318 B b1868 t1867
4319 H h1868 y_1 t1825
4320 S s1868 t684 h h1766 h1789 h1790 h1791 h1868 h1856 h1857 h1858 h1840 h1841
4321 G s1868 t1833
4322 B b1869 s1868
4323 T t1869 o1095 b1869 b1764
4324 B b1870 t1869
4325 H h1870 z_1 t1828
4326 S s1870 t684 h h1766 h1789 h1790 h1791 h1868 h1870 h1858 h1840 h1841
4327 G s1870 t1833
4328 B b1871 s1870
4329 T t1871 o1095 b1871 b1764
4330 B b1872 t1871
4331 H h1872 y t1829
4332 S s1872 t684 h h1766 h1789 h1790 h1791 h1872 h1858 h1840 h1841
4333 G s1872 t1833
4334 B b1873 s1872
4335 T t1873 o1095 b1873 b1764
4336 B b1874 t1873
4337 S s1874 t684 h h1766 h1789 h1790 h1791 h1832 h1840 h1841
4338 G s1874 t1833
4339 B b1875 s1874
4340 T t1875 o1095 b1875 b1764
4341 B b1876 t1875
4342 T t1876 o2 b1847
4343 B b1877 t1876
4344 T t1877 o1094 b1876 b4 b1877
4345 B b1878 t1877
4346 T t1878 o2 b1878
4347 B b1879 t1878
4348 T t1879 o1094 b1874 b4 b1879
4349 B b1880 t1879
4350 T t1880 o2 b1880
4351 B b1881 t1880
4352 T t1881 o1094 b1872 b4 b1881
4353 B b1882 t1881
4354 T t1882 o2 b1882
4355 B b1883 t1882
4356 T t1883 o1094 b1870 b4 b1883
4357 B b1884 t1883
4358 T t1884 o2 b1884
4359 B b1885 t1884
4360 T t1885 o1094 b1868 b4 b1885
4361 B b1886 t1885
4362 T t1886 o2 b1886
4363 B b1887 t1886
4364 T t1887 o1094 b1866 b4 b1887
4365 B b1888 t1887
4366 T t1888 o2 b1888
4367 B b1889 t1888
4368 T t1889 o1094 b1861 b1864 b1889
4369 B b1890 t1889
4370 T t1890 o2 b1890
4371 B b1891 t1890
4372 T t1891 o1094 b1859 b4 b1891
4373 B b1892 t1891
4374 T t1892 o b1892 b4
4375 B b1893 t1892
4376 T t1893 o1093 b1847 b1893
4377 B b1894 t1893
4378 P p1894 String "setSubstT << equal{'s1; 's2} >> 11 ttca"
4379 O o1894 ext_rule p1894
4380 T t1894 o1093 b1892 b4
4381 B b1895 t1894
4382 T t1895 o1894 b1092 b1895 b4 b4
4383 B b1896 t1895
4384 T t1896 o b1896 b4
4385 B b1897 t1896
4386 T t1897 o1852 b1092 b1894 b1897 b4
4387 B b1898 t1897
4388 T t1898 o b1898 b4
4389 B b1899 t1898
4390 T t1899 o b1852 b1899
4391 B b1900 t1899
4392 T t1900 o1821 b1092 b1850 b1900 b4
4393 B b1901 t1900
4394 T t1901 o b1901 b4
4395 B b1902 t1901
4396 T t1902 o1789 b1092 b1821 b1902 b4
4397 B b1903 t1902
4398 P p1903 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'e2; id{'g}}; 'e2} >> 3 ttca"
4399 O o1903 ext_rule p1903
4400 T t1903 o1093 b1786 b4
4401 B b1904 t1903
4402 T t1904 o1903 b1092 b1904 b4 b4
4403 B b1905 t1904
4404 T t1905 o b1905 b4
4405 B b1906 t1905
4406 T t1906 o b1903 b1906
4407 B b1907 t1906
4408 T t1907 o1757 b1092 b1789 b1907 b4
4409 B b1908 t1907
4410 T t1908 o1090 b1908
4411 B b1909 t1908
4412 P p1918 String unique_id2
4413 O o1918 rule p1918
4414 T t1918 o596 b585 b815 b1740
4415 B b1918 t1918
4416 T t1919 o761 b591 b759 b1918 b815
4417 B b1919 t1919 s
4418 T t1920 o1744 b591 b1919
4419 S s1920 t684 h
4420 G s1920 t1920
4421 B b1920 s1920
4422 T t1921 o677 b1920
4423 B b1921 t1921
4424 T t1922 o676 b1921 b1750
4425 B b1922 t1922
4426 T t1923 o676 b1744 b1922
4427 B b1923 t1923
4428 T t1924 o676 b763 b1923
4429 B b1924 t1924
4430 T t1925 o676 b700 b1924
4431 B b1925 t1925
4432 T t1926 o676 b682 b1925
4433 B b1926 t1926
4434 T t1927 o676 b761 b1926
4435 B b1927 t1927
4436 T t1928 o676 b1742 b1927
4437 B b1928 t1928
4438 T t1929 o b1920 b4
4439 B b1929 t1929
4440 T t1930 o b1743 b1929
4441 B b1930 t1930
4442 T t1931 o b762 b1930
4443 B b1931 t1931
4444 T t1932 o b699 b1931
4445 B b1932 t1932
4446 T t1933 o b681 b1932
4447 B b1933 t1933
4448 T t1934 o b760 b1933
4449 B b1934 t1934
4450 T t1935 o b1741 b1934
4451 B b1935 t1935
4452 T t1936 o1095 b1749 b1935
4453 B b1936 t1936
4454 T t1937 o1094 b1936 b4 b1104
4455 B b1937 t1937
4456 H h1937 v t1920
4457 T t1938 o596 b585 b1768 b1740
4458 B b1938 t1938
4459 T t1939 o761 b591 b759 b1938 b1768
4460 B b1939 t1939 w
4461 T t1940 o1767 b1939
4462 S s1940 t684 h h1937
4463 G s1940 t1940
4464 B b1940 s1940
4465 T t1941 o1095 b1940 b1935
4466 B b1941 t1941
4467 S s1941 t684 h h1937
4468 G s1941 t1749
4469 B b1942 s1941
4470 T t1942 o1095 b1942 b1935
4471 B b1943 t1942
4472 T t1943 o2 b1937
4473 B b1944 t1943
4474 T t1944 o1094 b1943 b1778 b1944
4475 B b1945 t1944
4476 T t1945 o2 b1945
4477 B b1946 t1945
4478 T t1946 o1766 b1941 b4 b1946
4479 B b1947 t1946
4480 T t1947 o596 b585 b604 b1740
4481 B b1948 t1947
4482 T t1948 o761 b591 b759 b1948 b604
4483 H h1948 w t1948
4484 S s1948 t684 h h1937 h1948
4485 G s1948 t1749
4486 B b1949 s1948
4487 T t1949 o1095 b1949 b1935
4488 B b1950 t1949
4489 T t1950 o1094 b1950 b4 b1946
4490 B b1951 t1950
4491 T t1951 o b1951 b4
4492 B b1952 t1951
4493 T t1952 o b1947 b1952
4494 B b1953 t1952
4495 T t1953 o1093 b1937 b1953
4496 B b1954 t1953
4497 P p1954 String "rwh unfold_fun_prop 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
4498 O o1954 ext_rule p1954
4499 T t1954 o596 b585 b714 b1740
4500 B b1955 t1954
4501 T t1955 o761 b591 b759 b1955 b714
4502 H h1955 x_1 t1955
4503 T t1956 o596 b585 b717 b1740
4504 B b1956 t1956
4505 T t1957 o761 b591 b759 b1956 b717
4506 S s1957 t684 h h1937 h1789 h1790 h1791 h1955
4507 G s1957 t1957
4508 B b1957 s1957
4509 T t1958 o1095 b1957 b1935
4510 B b1958 t1958
4511 B b1959 t1955
4512 B b1960 t1957
4513 T t1960 o1117 b1959 b1960
4514 S s1960 t684 h h1937 h1789 h1790 h1791
4515 G s1960 t1960
4516 B b1961 s1960
4517 T t1961 o1095 b1961 b1935
4518 B b1962 t1961
4519 B b1963 t1960
4520 T t1963 o1117 b1800 b1963
4521 S s1963 t684 h h1937 h1789 h1790
4522 G s1963 t1963
4523 B b1964 s1963
4524 T t1964 o1095 b1964 b1935
4525 B b1965 t1964
4526 B b1966 t1963 s2
4527 T t1966 o1129 b1130 b1966
4528 S s1966 t684 h h1937 h1789
4529 G s1966 t1966
4530 B b1967 s1966
4531 T t1967 o1095 b1967 b1935
4532 B b1968 t1967
4533 B b1969 t1966 s1
4534 T t1969 o1129 b1130 b1969
4535 S s1969 t684 h h1937
4536 G s1969 t1969
4537 B b1970 s1969
4538 T t1970 o1095 b1970 b1935
4539 B b1971 t1970
4540 T t1971 o2 b1947
4541 B b1972 t1971
4542 T t1972 o1766 b1971 b4 b1972
4543 B b1973 t1972
4544 T t1973 o2 b1973
4545 B b1974 t1973
4546 T t1974 o1094 b1968 b4 b1974
4547 B b1975 t1974
4548 T t1975 o2 b1975
4549 B b1976 t1975
4550 T t1976 o1094 b1965 b4 b1976
4551 B b1977 t1976
4552 T t1977 o2 b1977
4553 B b1978 t1977
4554 T t1978 o1094 b1962 b4 b1978
4555 B b1979 t1978
4556 T t1979 o2 b1979
4557 B b1980 t1979
4558 T t1980 o1094 b1958 b4 b1980
4559 B b1981 t1980
4560 T t1981 o b1981 b4
4561 B b1982 t1981
4562 T t1982 o1093 b1947 b1982
4563 B b1983 t1982
4564 P p1983 String "equivTransT << op{'g; 's2; 'e2} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
4565 O o1983 ext_rule p1983
4566 T t1983 o700 b1955
4567 B b1984 t1983
4568 T t1984 o1151 b1984 b1823
4569 B b1985 t1984
4570 T t1985 o1151 b1152 b1985
4571 B b1986 t1985
4572 T t1986 o1151 b1151 b1986
4573 B b1987 t1986
4574 T t1987 o736 b1955 b591
4575 B b1988 t1987
4576 T t1988 o1151 b1988 b1828
4577 B b1989 t1988
4578 T t1989 o1151 b1987 b1989
4579 B b1990 t1989
4580 T t1990 o1161 b1955 b714
4581 B b1991 t1990
4582 T t1991 o736 b1991 b759
4583 B b1992 t1991
4584 T t1992 o1151 b1990 b1992
4585 H h1992 x_1 t1992
4586 T t1993 o736 b1956 b591
4587 S s1993 t684 h h1937 h1789 h1790 h1791 h1992
4588 G s1993 t1993
4589 B b1993 s1993
4590 T t1994 o1095 b1993 b1935
4591 B b1994 t1994
4592 S s1994 t684 h h1937 h1789 h1790 h1791 h1955
4593 G s1994 t1993
4594 B b1995 s1994
4595 T t1995 o1095 b1995 b1935
4596 B b1996 t1995
4597 T t1996 o2 b1981
4598 B b1997 t1996
4599 T t1997 o1094 b1996 b4 b1997
4600 B b1998 t1997
4601 T t1998 o2 b1998
4602 B b1999 t1998
4603 T t1999 o1094 b1994 b4 b1999
4604 B b2000 t1999
4605 T t2000 o761 b591 b759 b1955 b1956
4606 H h2000 u t2000
4607 T t2001 o761 b591 b759 b1956 b714
4608 H h2001 v_1 t2001
4609 S s2001 t684 h h1937 h1789 h1790 h1791 h1992 h2000 h2001
4610 G s2001 t1957
4611 B b2001 s2001
4612 T t2002 o1095 b2001 b1935
4613 B b2002 t2002
4614 S s2002 t684 h h1937 h1789 h1790 h1791 h1955 h2000 h2001
4615 G s2002 t1957
4616 B b2003 s2002
4617 T t2003 o1095 b2003 b1935
4618 B b2004 t2003
4619 T t2004 o1094 b2004 b4 b1997
4620 B b2005 t2004
4621 T t2005 o2 b2005
4622 B b2006 t2005
4623 T t2006 o1094 b2002 b4 b2006
4624 B b2007 t2006
4625 T t2007 o b2007 b4
4626 B b2008 t2007
4627 T t2008 o b2000 b2008
4628 B b2009 t2008
4629 T t2009 o1093 b1981 b2009
4630 B b2010 t2009
4631 T t2010 o1093 b2000 b4
4632 B b2011 t2010
4633 T t2011 o1850 b1092 b2011 b4 b4
4634 B b2012 t2011
4635 H h2012 y_3 t1983
4636 H h2013 y t1987
4637 H h2014 z t1991
4638 S s2014 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2012 h1855 h2013 h1857 h2014 h2000 h2001
4639 G s2014 t738
4640 B b2014 s2014
4641 T t2014 o1095 b2014 b1935
4642 B b2015 t2014
4643 S s2015 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2012 h1855 h2013 h1857 h2014 h2000 h2001
4644 G s2015 t1993
4645 B b2016 s2015
4646 T t2016 o1095 b2016 b1935
4647 B b2017 t2016
4648 H h2017 z_3 t1984
4649 S s2017 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2017 h2013 h1857 h2014 h2000 h2001
4650 G s2017 t1993
4651 B b2018 s2017
4652 T t2018 o1095 b2018 b1935
4653 B b2019 t2018
4654 H h2019 z_1 t1985
4655 S s2019 t684 h h1937 h1789 h1790 h1791 h1852 h2019 h2013 h1857 h2014 h2000 h2001
4656 G s2019 t1993
4657 B b2020 s2019
4658 T t2020 o1095 b2020 b1935
4659 B b2021 t2020
4660 H h2021 y_1 t1986
4661 S s2021 t684 h h1937 h1789 h1790 h1791 h2021 h2013 h1857 h2014 h2000 h2001
4662 G s2021 t1993
4663 B b2022 s2021
4664 T t2022 o1095 b2022 b1935
4665 B b2023 t2022
4666 H h2023 z_1 t1988
4667 S s2023 t684 h h1937 h1789 h1790 h1791 h2021 h2023 h2014 h2000 h2001
4668 G s2023 t1993
4669 B b2024 s2023
4670 T t2024 o1095 b2024 b1935
4671 B b2025 t2024
4672 H h2025 y t1989
4673 S s2025 t684 h h1937 h1789 h1790 h1791 h2025 h2014 h2000 h2001
4674 G s2025 t1993
4675 B b2026 s2025
4676 T t2026 o1095 b2026 b1935
4677 B b2027 t2026
4678 S s2027 t684 h h1937 h1789 h1790 h1791 h1992 h2000 h2001
4679 G s2027 t1993
4680 B b2028 s2027
4681 T t2028 o1095 b2028 b1935
4682 B b2029 t2028
4683 T t2029 o2 b2007
4684 B b2030 t2029
4685 T t2030 o1094 b2029 b4 b2030
4686 B b2031 t2030
4687 T t2031 o2 b2031
4688 B b2032 t2031
4689 T t2032 o1094 b2027 b4 b2032
4690 B b2033 t2032
4691 T t2033 o2 b2033
4692 B b2034 t2033
4693 T t2034 o1094 b2025 b4 b2034
4694 B b2035 t2034
4695 T t2035 o2 b2035
4696 B b2036 t2035
4697 T t2036 o1094 b2023 b4 b2036
4698 B b2037 t2036
4699 T t2037 o2 b2037
4700 B b2038 t2037
4701 T t2038 o1094 b2021 b4 b2038
4702 B b2039 t2038
4703 T t2039 o2 b2039
4704 B b2040 t2039
4705 T t2040 o1094 b2019 b4 b2040
4706 B b2041 t2040
4707 T t2041 o2 b2041
4708 B b2042 t2041
4709 T t2042 o1094 b2017 b1864 b2042
4710 B b2043 t2042
4711 T t2043 o2 b2043
4712 B b2044 t2043
4713 T t2044 o1094 b2015 b4 b2044
4714 B b2045 t2044
4715 T t2045 o b2045 b4
4716 B b2046 t2045
4717 T t2046 o1093 b2007 b2046
4718 B b2047 t2046
4719 T t2047 o1093 b2045 b4
4720 B b2048 t2047
4721 T t2048 o1894 b1092 b2048 b4 b4
4722 B b2049 t2048
4723 T t2049 o b2049 b4
4724 B b2050 t2049
4725 T t2050 o1852 b1092 b2047 b2050 b4
4726 B b2051 t2050
4727 T t2051 o b2051 b4
4728 B b2052 t2051
4729 T t2052 o b2012 b2052
4730 B b2053 t2052
4731 T t2053 o1983 b1092 b2010 b2053 b4
4732 B b2054 t2053
4733 T t2054 o b2054 b4
4734 B b2055 t2054
4735 T t2055 o1954 b1092 b1983 b2055 b4
4736 B b2056 t2055
4737 P p2056 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 'e2}; 'e2} >> 3 ttca"
4738 O o2056 ext_rule p2056
4739 T t2056 o1093 b1951 b4
4740 B b2057 t2056
4741 T t2057 o2056 b1092 b2057 b4 b4
4742 B b2058 t2057
4743 T t2058 o b2058 b4
4744 B b2059 t2058
4745 T t2059 o b2056 b2059
4746 B b2060 t2059
4747 T t2060 o1757 b1092 b1954 b2060 b4
4748 B b2061 t2060
4749 T t2061 o1090 b2061
4750 B b2062 t2061
4751 P p2071 String unique_inv1
4752 O o2071 rule p2071
4753 T t2071 o596 b585 b717 b815
4754 B b2071 t2071
4755 T t2072 o761 b591 b759 b2071 b604
4756 S s2072 t684 h
4757 G s2072 t2072
4758 B b2072 s2072
4759 T t2073 o677 b2072
4760 B b2073 t2073
4761 T t2074 o609 b585 b815
4762 B b2074 t2074
4763 T t2075 o761 b591 b759 b717 b2074
4764 S s2075 t684 h
4765 G s2075 t2075
4766 B b2075 s2075
4767 T t2076 o677 b2075
4768 B b2076 t2076
4769 T t2077 o676 b2073 b2076
4770 B b2077 t2077
4771 T t2078 o676 b739 b2077
4772 B b2078 t2078
4773 T t2079 o676 b945 b2078
4774 B b2079 t2079
4775 T t2080 o676 b763 b2079
4776 B b2080 t2080
4777 T t2081 o676 b700 b2080
4778 B b2081 t2081
4779 T t2082 o676 b682 b2081
4780 B b2082 t2082
4781 T t2083 o676 b761 b2082
4782 B b2083 t2083
4783 T t2084 o676 b719 b2083
4784 B b2084 t2084
4785 T t2085 o676 b817 b2084
4786 B b2085 t2085
4787 P p2085 String "assumT 9 thenT equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; inv{'g; 's}; 's}}>> 2 ttca"
4788 O o2085 ext_rule p2085
4789 T t2086 o b2072 b4
4790 B b2086 t2086
4791 T t2087 o b738 b2086
4792 B b2087 t2087
4793 T t2088 o b944 b2087
4794 B b2088 t2088
4795 T t2089 o b762 b2088
4796 B b2089 t2089
4797 T t2090 o b699 b2089
4798 B b2090 t2090
4799 T t2091 o b681 b2090
4800 B b2091 t2091
4801 T t2092 o b760 b2091
4802 B b2092 t2092
4803 T t2093 o b718 b2092
4804 B b2093 t2093
4805 T t2094 o b816 b2093
4806 B b2094 t2094
4807 T t2095 o1095 b2075 b2094
4808 B b2095 t2095
4809 T t2096 o1094 b2095 b4 b1104
4810 B b2096 t2096
4811 H h2096 v t2072
4812 T t2097 o596 b585 b2074 b815
4813 B b2097 t2097
4814 T t2098 o761 b591 b759 b604 b2097
4815 S s2098 t684 h h2096
4816 G s2098 t2098
4817 B b2098 s2098
4818 T t2099 o1095 b2098 b2094
4819 B b2099 t2099
4820 S s2099 t684 h h2096
4821 G s2099 t2075
4822 B b2100 s2099
4823 T t2100 o1095 b2100 b2094
4824 B b2101 t2100
4825 T t2101 o2 b2096
4826 B b2102 t2101
4827 T t2102 o1094 b2101 b4 b2102
4828 B b2103 t2102
4829 T t2103 o2 b2103
4830 B b2104 t2103
4831 T t2104 o1094 b2099 b4 b2104
4832 B b2105 t2104
4833 T t2105 o761 b591 b759 b2071 b2097
4834 H h2105 z t2105
4835 S s2105 t684 h h2096 h2105
4836 G s2105 t2075
4837 B b2106 s2105
4838 T t2106 o1095 b2106 b2094
4839 B b2107 t2106
4840 T t2107 o1094 b2107 b4 b2104
4841 B b2108 t2107
4842 T t2108 o b2108 b4
4843 B b2109 t2108
4844 T t2109 o b2105 b2109
4845 B b2110 t2109
4846 T t2110 o1093 b2096 b2110
4847 B b2111 t2110
4848 P p2111 String "assertT << equiv{car{'g}; 'R; op{'g; inv{'g; 's}; 's}; id{'g}} >> ttca thenT equivSymT 3 ttca"
4849 O o2111 ext_rule p2111
4850 T t2111 o1093 b2105 b4
4851 B b2112 t2111
4852 T t2112 o2111 b1092 b2112 b4 b4
4853 B b2113 t2112
4854 P p3 String "groupCancelRightT 3 ttca"
4855 O o6 ext_rule p3
4856 T t2113 o1093 b2108 b4
4857 B b2114 t2113
4858 T t154 o6 b1092 b2114 b4 b4
4859 B b154 t154
4860 T t155 o b154 b4
4861 B b155 t155
4862 T t158 o b2113 b155
4863 B b158 t158
4864 T t159 o2085 b1092 b2111 b158 b4
4865 B b159 t159
4866 T t169 o1090 b159
4867 B b169 t169
4868 P p2128 String unique_inv2
4869 O o2128 rule p2128
4870 T t2128 o596 b585 b815 b717
4871 B b2128 t2128
4872 T t2129 o761 b591 b759 b2128 b604
4873 S s2129 t684 h
4874 G s2129 t2129
4875 B b2129 s2129
4876 T t2130 o677 b2129
4877 B b2130 t2130
4878 T t2131 o676 b2130 b2076
4879 B b2131 t2131
4880 T t2132 o676 b739 b2131
4881 B b2132 t2132
4882 T t2133 o676 b945 b2132
4883 B b2133 t2133
4884 T t2134 o676 b763 b2133
4885 B b2134 t2134
4886 T t2135 o676 b700 b2134
4887 B b2135 t2135
4888 T t2136 o676 b761 b2135
4889 B b2136 t2136
4890 T t2137 o676 b682 b2136
4891 B b2137 t2137
4892 T t2138 o676 b719 b2137
4893 B b2138 t2138
4894 T t2139 o676 b817 b2138
4895 B b2139 t2139
4896 P p2139 String "assumT 9 thenT equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; 's; inv{'g; 's}}}>> 2 ttca"
4897 O o2139 ext_rule p2139
4898 T t2140 o b2129 b4
4899 B b2140 t2140
4900 T t2141 o b738 b2140
4901 B b2141 t2141
4902 T t2142 o b944 b2141
4903 B b2142 t2142
4904 T t2143 o b762 b2142
4905 B b2143 t2143
4906 T t2144 o b699 b2143
4907 B b2144 t2144
4908 T t2145 o b760 b2144
4909 B b2145 t2145
4910 T t2146 o b681 b2145
4911 B b2146 t2146
4912 T t2147 o b718 b2146
4913 B b2147 t2147
4914 T t2148 o b816 b2147
4915 B b2148 t2148
4916 T t2149 o1095 b2075 b2148
4917 B b2149 t2149
4918 T t2150 o1094 b2149 b4 b1104
4919 B b2150 t2150
4920 H h2150 v t2129
4921 T t2151 o596 b585 b815 b2074
4922 B b2151 t2151
4923 T t2152 o761 b591 b759 b604 b2151
4924 S s2152 t684 h h2150
4925 G s2152 t2152
4926 B b2152 s2152
4927 T t2153 o1095 b2152 b2148
4928 B b2153 t2153
4929 S s2153 t684 h h2150
4930 G s2153 t2075
4931 B b2154 s2153
4932 T t2154 o1095 b2154 b2148
4933 B b2155 t2154
4934 T t2155 o2 b2150
4935 B b2156 t2155
4936 T t2156 o1094 b2155 b4 b2156
4937 B b2157 t2156
4938 T t2157 o2 b2157
4939 B b2158 t2157
4940 T t2158 o1094 b2153 b4 b2158
4941 B b2159 t2158
4942 T t2159 o761 b591 b759 b2128 b2151
4943 H h2159 z t2159
4944 S s2159 t684 h h2150 h2159
4945 G s2159 t2075
4946 B b2160 s2159
4947 T t2160 o1095 b2160 b2148
4948 B b2161 t2160
4949 T t2161 o1094 b2161 b4 b2158
4950 B b2162 t2161
4951 T t2162 o b2162 b4
4952 B b2163 t2162
4953 T t2163 o b2159 b2163
4954 B b2164 t2163
4955 T t2164 o1093 b2150 b2164
4956 B b2165 t2164
4957 P p2165 String "assertT << equiv{car{'g}; 'R; op{'g; 's; inv{'g; 's}}; id{'g}} >> ttca thenT equivSymT 3 ttca"
4958 O o2165 ext_rule p2165
4959 T t2165 o1093 b2159 b4
4960 B b2166 t2165
4961 T t2166 o2165 b1092 b2166 b4 b4
4962 B b2167 t2166
4963 P p2167 String "groupCancelLeftT 3 ttca"
4964 O o2167 ext_rule p2167
4965 T t2167 o1093 b2162 b4
4966 B b2168 t2167
4967 T t2168 o2167 b1092 b2168 b4 b4
4968 B b2169 t2168
4969 T t2169 o b2169 b4
4970 B b2170 t2169
4971 T t2170 o b2167 b2170
4972 B b2171 t2170
4973 T t2171 o2139 b1092 b2165 b2171 b4
4974 B b2172 t2171
4975 T t2172 o1090 b2172
4976 B b2173 t2172
4977 P p2182 String unique_sol1
4978 O o2182 rule p2182
4979 B b2182 t1304
4980 T t2182 o700 b2182
4981 S s2182 t679 h
4982 G s2182 t2182
4983 B b2183 s2182
4984 T t2183 o677 b2183
4985 B b2184 t2183
4986 T t2184 o736 b2182 b591
4987 S s2184 t684 h
4988 G s2184 t2184
4989 B b2185 s2184
4990 T t2185 o677 b2185
4991 B b2186 t2185
4992 T t2186 o596 b585 b597 b2182
4993 B b2187 t2186
4994 T t2187 o761 b591 b759 b2187 b598
4995 S s2187 t684 h
4996 G s2187 t2187
4997 B b2188 s2187
4998 T t2188 o677 b2188
4999 B b2189 t2188
5000 T t2189 o596 b585 b609 b598
5001 B b2190 t2189
5002 T t2190 o761 b591 b759 b2182 b2190
5003 S s2190 t684 h
5004 G s2190 t2190
5005 B b2191 s2190
5006 T t2191 o677 b2191
5007 B b2192 t2191
5008 T t2192 o676 b2189 b2192
5009 B b2193 t2192
5010 T t2193 o676 b2186 b2193
5011 B b2194 t2193
5012 T t2194 o676 b1077 b2194
5013 B b2195 t2194
5014 T t2195 o676 b1075 b2195
5015 B b2196 t2195
5016 T t2196 o676 b763 b2196
5017 B b2197 t2196
5018 T t2197 o676 b700 b2197
5019 B b2198 t2197
5020 T t2198 o676 b682 b2198
5021 B b2199 t2198
5022 T t2199 o676 b761 b2199
5023 B b2200 t2199
5024 T t2200 o676 b2184 b2200
5025 B b2201 t2200
5026 T t2201 o676 b1073 b2201
5027 B b2202 t2201
5028 T t2202 o676 b1071 b2202
5029 B b2203 t2202
5030 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"
5031 O o2203 ext_rule p2203
5032 T t2203 o b2188 b4
5033 B b2204 t2203
5034 T t2204 o b2185 b2204
5035 B b2205 t2204
5036 T t2205 o b1076 b2205
5037 B b2206 t2205
5038 T t2206 o b1074 b2206
5039 B b2207 t2206
5040 T t2207 o b762 b2207
5041 B b2208 t2207
5042 T t2208 o b699 b2208
5043 B b2209 t2208
5044 T t2209 o b681 b2209
5045 B b2210 t2209
5046 T t2210 o b760 b2210
5047 B b2211 t2210
5048 T t2211 o b2183 b2211
5049 B b2212 t2211
5050 T t2212 o b1072 b2212
5051 B b2213 t2212
5052 T t2213 o b1070 b2213
5053 B b2214 t2213
5054 T t2214 o1095 b2191 b2214
5055 B b2215 t2214
5056 T t2215 o1094 b2215 b4 b1104
5057 B b2216 t2215
5058 H h2216 v t2187
5059 T t2216 o596 b585 b609 b2187
5060 B b2217 t2216
5061 T t2217 o761 b591 b759 b2217 b2190
5062 H h2217 v_1 t2217
5063 S s2217 t684 h h2216 h2217
5064 G s2217 t2190
5065 B b2218 s2217
5066 T t2218 o1095 b2218 b2214
5067 B b2219 t2218
5068 S s2219 t684 h h2216
5069 G s2219 t2190
5070 B b2220 s2219
5071 T t2220 o1095 b2220 b2214
5072 B b2221 t2220
5073 T t2221 o2 b2216
5074 B b2222 t2221
5075 T t2222 o1094 b2221 b4 b2222
5076 B b2223 t2222
5077 T t2223 o2 b2223
5078 B b2224 t2223
5079 T t2224 o1094 b2219 b4 b2224
5080 B b2225 t2224
5081 T t2225 o b2225 b4
5082 B b2226 t2225
5083 T t2226 o1093 b2216 b2226
5084 B b2227 t2226
5085 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"
5086 O o2227 ext_rule p2227
5087 T t2227 o596 b585 b609 b597
5088 B b2228 t2227
5089 T t2228 o596 b585 b2228 b2182
5090 B b2229 t2228
5091 T t2229 o761 b591 b759 b2229 b2190
5092 H h2229 z t2229
5093 S s2229 t684 h h2216 h2217 h2229
5094 G s2229 t2190
5095 B b2230 s2229
5096 T t2230 o1095 b2230 b2214
5097 B b2231 t2230
5098 T t2231 o2 b2225
5099 B b2232 t2231
5100 T t2232 o1094 b2231 b4 b2232
5101 B b2233 t2232
5102 T t2233 o b2233 b4
5103 B b2234 t2233
5104 T t2234 o1093 b2225 b2234
5105 B b2235 t2234
5106 P p2235 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 'a}; 'a}; id{'g}} >> 4 ttca"
5107 O o2235 ext_rule p2235
5108 T t2235 o596 b585 b604 b2182
5109 B b2236 t2235
5110 T t2236 o761 b591 b759 b2236 b2190
5111 H h2236 z_1 t2236
5112 S s2236 t684 h h2216 h2217 h2229 h2236
5113 G s2236 t2190
5114 B b2237 s2236
5115 T t2237 o1095 b2237 b2214
5116 B b2238 t2237
5117 T t2238 o2 b2233
5118 B b2239 t2238
5119 T t2239 o1094 b2238 b4 b2239
5120 B b2240 t2239
5121 T t2240 o b2240 b4
5122 B b2241 t2240
5123 T t2241 o1093 b2233 b2241
5124 B b2242 t2241
5125 P p2242 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 'x}; 'x} >> 5 ttca"
5126 O o2242 ext_rule p2242
5127 T t2242 o1093 b2240 b4
5128 B b2243 t2242
5129 T t2243 o2242 b1092 b2243 b4 b4
5130 B b2244 t2243
5131 T t2244 o b2244 b4
5132 B b2245 t2244
5133 T t2245 o2235 b1092 b2242 b2245 b4
5134 B b2246 t2245
5135 T t2246 o b2246 b4
5136 B b2247 t2246
5137 T t2247 o2227 b1092 b2235 b2247 b4
5138 B b2248 t2247
5139 T t2248 o b2248 b4
5140 B b2249 t2248
5141 T t2249 o2203 b1092 b2227 b2249 b4
5142 B b2250 t2249
5143 T t2250 o1090 b2250
5144 B b2251 t2250
5145 P p2260 String unique_sol2
5146 O o2260 rule p2260
5147 P p2261 Var y
5148 O o2261 var p2261
5149 T t2261 o2261
5150 B b2261 t2261
5151 T t2262 o700 b2261
5152 S s2262 t679 h
5153 G s2262 t2262
5154 B b2262 s2262
5155 T t2263 o677 b2262
5156 B b2263 t2263
5157 T t2264 o736 b2261 b591
5158 S s2264 t684 h
5159 G s2264 t2264
5160 B b2264 s2264
5161 T t2265 o677 b2264
5162 B b2265 t2265
5163 T t2266 o596 b585 b2261 b597
5164 B b2266 t2266
5165 T t2267 o761 b591 b759 b2266 b598
5166 S s2267 t684 h
5167 G s2267 t2267
5168 B b2267 s2267
5169 T t2268 o677 b2267
5170 B b2268 t2268
5171 T t2269 o596 b585 b598 b609
5172 B b2269 t2269
5173 T t2270 o761 b591 b759 b2261 b2269
5174 S s2270 t684 h
5175 G s2270 t2270
5176 B b2270 s2270
5177 T t2271 o677 b2270
5178 B b2271 t2271
5179 T t2272 o676 b2268 b2271
5180 B b2272 t2272
5181 T t2273 o676 b2265 b2272
5182 B b2273 t2273
5183 T t2274 o676 b1077 b2273
5184 B b2274 t2274
5185 T t2275 o676 b1075 b2274
5186 B b2275 t2275
5187 T t2276 o676 b763 b2275
5188 B b2276 t2276
5189 T t2277 o676 b700 b2276
5190 B b2277 t2277
5191 T t2278 o676 b682 b2277
5192 B b2278 t2278
5193 T t2279 o676 b761 b2278
5194 B b2279 t2279
5195 T t2280 o676 b2263 b2279
5196 B b2280 t2280
5197 T t2281 o676 b1073 b2280
5198 B b2281 t2281
5199 T t2282 o676 b1071 b2281
5200 B b2282 t2282
5201 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"
5202 O o175 ext_rule p174
5203 T t2283 o b2267 b4
5204 B b2283 t2283
5205 T t2284 o b2264 b2283
5206 B b2284 t2284
5207 T t2285 o b1076 b2284
5208 B b2285 t2285
5209 T t2286 o b1074 b2285
5210 B b2286 t2286
5211 T t2287 o b762 b2286
5212 B b2287 t2287
5213 T t2288 o b699 b2287
5214 B b2288 t2288
5215 T t2289 o b681 b2288
5216 B b2289 t2289
5217 T t2290 o b760 b2289
5218 B b2290 t2290
5219 T t2291 o b2262 b2290
5220 B b2291 t2291
5221 T t2292 o b1072 b2291
5222 B b2292 t2292
5223 T t2293 o b1070 b2292
5224 B b2293 t2293
5225 T t2294 o1095 b2270 b2293
5226 B b2294 t2294
5227 T t2295 o1094 b2294 b4 b1104
5228 B b2295 t2295
5229 H h2295 v t2267
5230 T t2296 o596 b585 b2266 b609
5231 B b2296 t2296
5232 T t2297 o761 b591 b759 b2296 b2269
5233 H h2297 v_1 t2297
5234 S s2300 t684 h h2295 h2297
5235 G s2300 t2270
5236 B b2301 s2300
5237 T t2301 o1095 b2301 b2293
5238 B b2302 t2301
5239 S s2302 t684 h h2295
5240 G s2302 t2270
5241 B b2303 s2302
5242 T t2303 o1095 b2303 b2293
5243 B b2304 t2303
5244 T t2304 o2 b2295
5245 B b2305 t2304
5246 T t2305 o1094 b2304 b4 b2305
5247 B b2306 t2305
5248 T t2306 o2 b2306
5249 B b2307 t2306
5250 T t2314 o1094 b2302 b4 b2307
5251 B b2315 t2314
5252 T t177 o b2315 b4
5253 B b177 t177
5254 T t178 o1093 b2295 b177
5255 B b178 t178
5256 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"
5257 O o186 ext_rule p186
5258 T t2315 o596 b585 b597 b609
5259 B b2316 t2315
5260 T t2316 o596 b585 b2261 b2316
5261 B b2317 t2316
5262 T t2317 o761 b591 b759 b2317 b2269
5263 H h2317 z t2317
5264 S s2319 t684 h h2295 h2297 h2317
5265 G s2319 t2270
5266 B b2320 s2319
5267 T t2320 o1095 b2320 b2293
5268 B b2321 t2320
5269 T t2321 o2 b2315
5270 B b2322 t2321
5271 P p2329 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'a; inv{'g; 'a}}; id{'g}} >> 4 ttca"
5272 O o2329 ext_rule p2329
5273 T t2329 o1094 b2321 b4 b2322
5274 B b2330 t2329
5275 T t191 o b2330 b4
5276 B b191 t191
5277 T t196 o1093 b2315 b191
5278 B b196 t196
5279 T t2330 o596 b585 b2261 b604
5280 B b2331 t2330
5281 T t2331 o761 b591 b759 b2331 b2269
5282 H h2331 z_1 t2331
5283 S s2331 t684 h h2295 h2297 h2317 h2331
5284 G s2331 t2270
5285 B b2332 s2331
5286 T t2332 o1095 b2332 b2293
5287 B b2333 t2332
5288 T t2333 o2 b2330
5289 B b2334 t2333
5290 T t2334 o1094 b2333 b4 b2334
5291 B b2335 t2334
5292 T t2335 o b2335 b4
5293 B b2336 t2335
5294 T t2336 o1093 b2330 b2336
5295 B b2337 t2336
5296 P p2337 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'y; id{'g}}; 'y} >> 5 ttca"
5297 O o2337 ext_rule p2337
5298 T t2337 o1093 b2335 b4
5299 B b2338 t2337
5300 T t2338 o2337 b1092 b2338 b4 b4
5301 B b2339 t2338
5302 T t2339 o b2339 b4
5303 B b2340 t2339
5304 T t2340 o2329 b1092 b2337 b2340 b4
5305 B b2341 t2340
5306 T t2341 o b2341 b4
5307 B b2342 t2341
5308 T t197 o186 b1092 b196 b2342 b4
5309 B b197 t197
5310 T t205 o b197 b4
5311 B b205 t205
5312 T t206 o175 b1092 b178 b205 b4
5313 B b206 t206
5314 T t208 o1090 b206
5315 B b208 t208
5316 P p2355 String inv_simplify
5317 O o2355 rule p2355
5318 T t2355 o609 b585 b599
5319 B b2355 t2355
5320 T t2356 o609 b585 b598
5321 B b2356 t2356
5322 T t2357 o596 b585 b2356 b609
5323 B b2357 t2357
5324 T t2358 o761 b591 b759 b2355 b2357
5325 S s2358 t684 h
5326 G s2358 t2358
5327 B b2358 s2358
5328 T t2359 o677 b2358
5329 B b2359 t2359
5330 T t2360 o676 b1077 b2359
5331 B b2360 t2360
5332 T t2361 o676 b1075 b2360
5333 B b2361 t2361
5334 T t2362 o676 b763 b2361
5335 B b2362 t2362
5336 T t2363 o676 b700 b2362
5337 B b2363 t2363
5338 T t2364 o676 b682 b2363
5339 B b2364 t2364
5340 T t2365 o676 b761 b2364
5341 B b2365 t2365
5342 T t2366 o676 b1073 b2365
5343 B b2366 t2366
5344 T t2367 o676 b1071 b2366
5345 B b2367 t2367
5346 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}}} >>"
5347 O o2367 ext_rule p2367
5348 T t2368 o1095 b2358 b1102
5349 B b2368 t2368
5350 T t2369 o1094 b2368 b4 b1104
5351 B b2369 t2369
5352 P p2369 String assertion
5353 O o2369 tactic_arg p2369
5354 T t2370 o596 b585 b2355 b599
5355 B b2370 t2370
5356 T t2371 o596 b585 b2357 b599
5357 B b2371 t2371
5358 T t2372 o761 b591 b759 b2370 b2371
5359 S s2372 t684 h
5360 G s2372 t2372
5361 B b2372 s2372
5362 T t2373 o1095 b2372 b1102
5363 B b2373 t2373
5364 T t2374 o2 b2369
5365 B b2374 t2374
5366 T t2375 o2369 b2373 b4 b2374
5367 B b2375 t2375
5368 H h2375 v t2372
5369 S s2375 t684 h h2375
5370 G s2375 t2358
5371 B b2376 s2375
5372 T t2376 o1095 b2376 b1102
5373 B b2377 t2376
5374 T t2377 o1094 b2377 b4 b2374
5375 B b2378 t2377
5376 T t2378 o b2378 b4
5377 B b2379 t2378
5378 T t2379 o b2375 b2379
5379 B b2380 t2379
5380 T t2380 o1093 b2369 b2380
5381 B b2381 t2380
5382 P p2381 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; op{'g; 'a; 'b}}; op{'g; 'a; 'b}}; id{'g}} >> 0 ttca"
5383 O o2381 ext_rule p2381
5384 T t2381 o761 b591 b759 b604 b2371
5385 S s2381 t684 h
5386 G s2381 t2381
5387 B b2382 s2381
5388 T t2382 o1095 b2382 b1102
5389 B b2383 t2382
5390 T t2383 o2 b2375
5391 B b2384 t2383
5392 T t2384 o2369 b2383 b4 b2384
5393 B b2385 t2384
5394 T t2385 o b2385 b4
5395 B b2386 t2385
5396 T t2386 o1093 b2375 b2386
5397 B b2387 t2386
5398 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"
5399 O o2387 ext_rule p2387
5400 T t2387 o1093 b2385 b4
5401 B b2388 t2387
5402 T t2388 o2387 b1092 b2388 b4 b4
5403 B b2389 t2388
5404 T t2389 o b2389 b4
5405 B b2390 t2389
5406 T t2390 o2381 b1092 b2387 b2390 b4
5407 B b2391 t2390
5408 P p217 String "groupCancelRightT 2 ttca"
5409 O o217 ext_rule p217
5410 T t2391 o1093 b2378 b4
5411 B b2392 t2391
5412 T t229 o217 b1092 b2392 b4 b4
5413 B b229 t229
5414 T t230 o b229 b4
5415 B b230 t230
5416 T t232 o b2391 b230
5417 B b232 t232
5418 T t240 o2367 b1092 b2381 b232 b4
5419 B b240 t240
5420 T t241 o1090 b240
5421 B b241 t241
5422 P p2406 String inv_of_id
5423 O o2406 rule p2406
5424 T t2406 o609 b585 b604
5425 B b2406 t2406
5426 T t2407 o761 b591 b759 b2406 b604
5427 S s2407 t684 h
5428 G s2407 t2407
5429 B b2407 s2407
5430 T t2408 o677 b2407
5431 B b2408 t2408
5432 T t2409 o676 b763 b2408
5433 B b2409 t2409
5434 T t2410 o676 b700 b2409
5435 B b2410 t2410
5436 T t2411 o676 b682 b2410
5437 B b2411 t2411
5438 T t2412 o676 b761 b2411
5439 B b2412 t2412
5440 P p2412 String "assertT << equiv{car{'g}; 'R; id{'g}; inv{'g; id{'g}}} >> thenAT autoT"
5441 O o2412 ext_rule p2412
5442 T t2413 o b762 b4
5443 B b2413 t2413
5444 T t2414 o b699 b2413
5445 B b2414 t2414
5446 T t2415 o b681 b2414
5447 B b2415 t2415
5448 T t2416 o b760 b2415
5449 B b2416 t2416
5450 T t2417 o1095 b2407 b2416
5451 B b2417 t2417
5452 T t2418 o1094 b2417 b4 b1104
5453 B b2418 t2418
5454 T t2419 o761 b591 b759 b604 b2406
5455 H h2419 v t2419
5456 S s2419 t684 h h2419
5457 G s2419 t2407
5458 B b2419 s2419
5459 T t2420 o1095 b2419 b2416
5460 B b2420 t2420
5461 T t2421 o2 b2418
5462 B b2421 t2421
5463 T t2422 o1094 b2420 b4 b2421
5464 B b2422 t2422
5465 T t2423 o b2422 b4
5466 B b2423 t2423
5467 T t2424 o1093 b2418 b2423
5468 B b2424 t2424
5469 P p2424 String "equivSymT 2 ttca"
5470 O o2424 ext_rule p2424
5471 T t2425 o1093 b2422 b4
5472 B b2425 t2425
5473 T t2426 o2424 b1092 b2425 b4 b4
5474 B b2426 t2426
5475 T t2427 o b2426 b4
5476 B b2427 t2427
5477 T t2428 o2412 b1092 b2424 b2427 b4
5478 B b2428 t2428
5479 T t2429 o1090 b2428
5480 B b2429 t2429
5481 O o2436 location p p
5482 P p502 String id_judge_elim
5483 O o503 rule p502
5484 T t509 o596 b585 b815 b815
5485 B b509 t509
5486 T t510 o761 b591 b759 b509 b815
5487 H h510 x t510
5488 S s510 t679 h h510 h1304
5489 G s510 t816
5490 B b510 s510
5491 T t516 o677 b510
5492 B b516 t516
5493 S s516 t679 h h510 h1304
5494 G s516 t760
5495 B b517 s516
5496 T t517 o677 b517
5497 B b523 t517
5498 S s523 t679 h h510 h1304
5499 G s523 t681
5500 B b524 s523
5501 T t524 o677 b524
5502 B b530 t524
5503 S s530 t684 h h510 h1304
5504 G s530 t586
5505 B b531 s530
5506 T t531 o677 b531
5507 B b538 t531
5508 S s538 t684 h h510 h1304
5509 G s538 t762
5510 B b539 s538
5511 T t539 o677 b539
5512 B b546 t539
5513 T t546 o761 b591 b759 b815 b604
5514 H h546 y t546
5515 P p548 Var C
5516 O o549 var p548
5517 T t554 o549 b2182
5518 S s554 t684 h h510 h1304 h546
5519 G s554 t554
5520 B b554 s554
5521 T t555 o677 b554
5522 B b555 t555
5523 S s555 t684 h h510 h1304
5524 G s555 t554
5525 B b561 s555
5526 T t561 o677 b561
5527 B b562 t561
5528 T t562 o676 b555 b562
5529 B b568 t562
5530 T t568 o676 b546 b568
5531 B b569 t568
5532 T t569 o676 b538 b569
5533 B b575 t569
5534 T t575 o676 b530 b575
5535 B b576 t575
5536 T t576 o676 b523 b576
5537 B b582 t576
5538 T t582 o676 b516 b582
5539 B b583 t582
5540 P p585 String "assertT << equiv{car{'g}; 'R; 's; id{'g}} >> ttca"
5541 O o586 ext_rule p585
5542 T t589 o b554 b4
5543 B b589 t589
5544 T t590 o b539 b589
5545 B b590 t590
5546 T t594 o b531 b590
5547 B b594 t594
5548 T t595 o b524 b594
5549 B b595 t595
5550 T t596 o b517 b595
5551 B b596 t596
5552 T t602 o b510 b596
5553 B b602 t602
5554 T t603 o1095 b561 b602
5555 B b603 t603
5556 T t607 o1094 b603 b4 b1104
5557 B b607 t607
5558 S s607 t684 h h510 h1304
5559 G s607 t546
5560 B b608 s607
5561 T t608 o1095 b608 b602
5562 B b612 t608
5563 T t612 o2 b607
5564 B b615 t612
5565 T t615 o2369 b612 b4 b615
5566 B b616 t615
5567 T t616 o b616 b4
5568 B b626 t616
5569 T t626 o1093 b607 b626
5570 B b679 t626
5571 P p679 String "equivSubstT << equiv{car{'g}; 'R; 's; op{'g; id{'g}; 's}} >> 0 ttca"
5572 O o681 ext_rule p679
5573 T t713 o761 b591 b759 b815 b946
5574 S s713 t684 h h510 h1304
5575 G s713 t713
5576 B b1106 s713
5577 T t1121 o1095 b1106 b602
5578 B b1738 t1121
5579 T t1738 o2 b616
5580 B b1739 t1738
5581 T t1739 o2369 b1738 b4 b1739
5582 B b1767 t1739
5583 T t1767 o761 b591 b759 b946 b604
5584 S s1767 t684 h h510 h1304
5585 G s1767 t1767
5586 B b1790 s1767
5587 T t1796 o1095 b1790 b602
5588 B b1853 t1796
5589 T t1853 o2369 b1853 b4 b1739
5590 B b1854 t1853
5591 T t1854 o b1854 b4
5592 B b1855 t1854
5593 T t1855 o b1767 b1855
5594 B b1856 t1855
5595 T t1856 o1093 b616 b1856
5596 B b1857 t1856
5597 P p1857 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's}; 's} >> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
5598 O o1857 ext_rule p1857
5599 T t1857 o1093 b1767 b4
5600 B b1910 t1857
5601 T t1910 o1857 b1092 b1910 b4 b4
5602 B b1917 t1910
5603 P p1919 String "equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; inv{'g; 's}; 's}} >> 0 ttca"
5604 O o1919 ext_rule p1919
5605 S s1919 t684 h h510 h1304
5606 G s1919 t2098
5607 B b2013 s1919
5608 T t2013 o1095 b2013 b602
5609 B b2063 t2013
5610 T t2063 o2 b1854
5611 B b2070 t2063
5612 T t2070 o2369 b2063 b4 b2070
5613 B b2115 t2070
5614 T t2115 o596 b585 b2097 b815
5615 B b2116 t2115
5616 T t2116 o761 b591 b759 b2116 b2097
5617 S s2116 t684 h h510 h1304
5618 G s2116 t2116
5619 B b2117 s2116
5620 T t2117 o1095 b2117 b602
5621 B b2118 t2117
5622 T t2118 o2369 b2118 b4 b2070
5623 B b2119 t2118
5624 B b2120 t819
5625 T t2120 o761 b591 b759 b2120 b818
5626 B b2125 t2120 z
5627 T t2125 o1077 b591 b759 b2125
5628 S s2125 t684 h h510 h1304
5629 G s2125 t2125
5630 B b2126 s2125
5631 T t2126 o1095 b2126 b602
5632 B b2127 t2126
5633 T t2127 o2369 b2127 b4 b2070
5634 B b2174 t2127
5635 T t2174 o b2174 b4
5636 B b2181 t2174
5637 T t2181 o b2119 b2181
5638 B b2252 t2181
5639 T t2252 o b2115 b2252
5640 B b2259 t2252
5641 T t2259 o1093 b1854 b2259
5642 B b2260 t2259
5643 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"
5644 O o2262 ext_rule p2262
5645 T t2298 o1093 b2115 b4
5646 B b2298 t2298
5647 T t2299 o2262 b1092 b2298 b4 b4
5648 B b2299 t2299
5649 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"
5650 O o2299 ext_rule p2299
5651 T t2300 o1093 b2119 b4
5652 B b2300 t2300
5653 T t2302 o2299 b1092 b2300 b4 b4
5654 B b2308 t2302
5655 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"
5656 O o2308 ext_rule p2308
5657 H h2308 a t1106
5658 H h2309 b t1106
5659 H h2310 x_1 t762
5660 T t2310 o761 b591 b759 b597 b598
5661 H h2311 x_2 t2310
5662 T t2311 o596 b585 b597 b815
5663 B b2311 t2311
5664 T t2312 o761 b591 b759 b2311 b597
5665 H h2312 x_3 t2312
5666 T t2313 o596 b585 b598 b815
5667 B b2313 t2313
5668 T t2318 o761 b591 b759 b2313 b598
5669 S s2318 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2312
5670 G s2318 t2318
5671 B b2318 s2318
5672 T t2319 o1095 b2318 b602
5673 B b2319 t2319
5674 B b2323 t2312
5675 B b2324 t2318
5676 T t2324 o1117 b2323 b2324
5677 S s2324 t684 h h510 h1304 h2308 h2309 h2310 h2311
5678 G s2324 t2324
5679 B b2325 s2324
5680 T t2325 o1095 b2325 b602
5681 B b2326 t2325
5682 B b2327 t2310
5683 B b2328 t2324
5684 T t2328 o1117 b2327 b2328
5685 S s2328 t684 h h510 h1304 h2308 h2309 h2310
5686 G s2328 t2328
5687 B b2329 s2328
5688 T t2342 o1095 b2329 b602
5689 B b2343 t2342
5690 B b2344 t2328
5691 T t2344 o1117 b1126 b2344
5692 S s2344 t684 h h510 h1304 h2308 h2309
5693 G s2344 t2344
5694 B b2345 s2344
5695 T t2345 o1095 b2345 b602
5696 B b2346 t2345
5697 B b2347 t2344 b
5698 T t2347 o1129 b1130 b2347
5699 S s2347 t684 h h510 h1304 h2308
5700 G s2347 t2347
5701 B b2352 s2347
5702 T t2352 o1095 b2352 b602
5703 B b2353 t2352
5704 B b2354 t2347 a
5705 T t2354 o1129 b1130 b2354
5706 S s2354 t684 h h510 h1304
5707 G s2354 t2354
5708 B b2393 s2354
5709 T t2393 o1095 b2393 b602
5710 B b2394 t2393
5711 T t2394 o2 b2174
5712 B b2395 t2394
5713 T t2395 o2369 b2394 b4 b2395
5714 B b2396 t2395
5715 T t2396 o2 b2396
5716 B b2397 t2396
5717 T t2397 o1094 b2353 b4 b2397
5718 B b2398 t2397
5719 T t2398 o2 b2398
5720 B b2403 t2398
5721 T t2403 o1094 b2346 b4 b2403
5722 B b2404 t2403
5723 T t2404 o2 b2404
5724 B b2405 t2404
5725 T t2405 o1094 b2343 b4 b2405
5726 B b2430 t2405
5727 T t2430 o2 b2430
5728 B b2440 t2430
5729 T t2440 o1094 b2326 b4 b2440
5730 B b2441 t2440
5731 T t2441 o2 b2441
5732 B b2442 t2441
5733 T t2442 o1094 b2319 b4 b2442
5734 B b2443 t2442
5735 T t2443 o b2443 b4
5736 B b2444 t2443
5737 T t2444 o1093 b2174 b2444
5738 B b2445 t2444
5739 P p2445 String "equivTransT << op{'g; 'b; 's} >> 8 ttca thenT rwh unfold_equiv 8 ttca"
5740 O o2445 ext_rule p2445
5741 T t2445 o700 b2311
5742 B b2446 t2445
5743 B b2447 t1070
5744 T t2447 o1151 b2446 b2447
5745 B b2448 t2447
5746 T t2448 o1151 b1152 b2448
5747 B b2449 t2448
5748 T t2449 o1151 b1151 b2449
5749 B b2450 t2449
5750 T t2450 o736 b2311 b591
5751 B b2451 t2450
5752 B b2452 t1074
5753 T t2452 o1151 b2451 b2452
5754 B b2453 t2452
5755 T t2453 o1151 b2450 b2453
5756 B b2454 t2453
5757 T t2454 o1161 b2311 b597
5758 B b2455 t2454
5759 T t2455 o736 b2455 b759
5760 B b2456 t2455
5761 T t2456 o1151 b2454 b2456
5762 H h2456 x_3 t2456
5763 T t2457 o736 b2313 b591
5764 S s2457 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2456
5765 G s2457 t2457
5766 B b2457 s2457
5767 T t2458 o1095 b2457 b602
5768 B b2458 t2458
5769 S s2458 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2312
5770 G s2458 t2457
5771 B b2459 s2458
5772 T t2459 o1095 b2459 b602
5773 B b2460 t2459
5774 T t2460 o2 b2443
5775 B b2461 t2460
5776 T t2461 o1094 b2460 b4 b2461
5777 B b2462 t2461
5778 T t2462 o2 b2462
5779 B b2463 t2462
5780 T t2463 o1094 b2458 b4 b2463
5781 B b2464 t2463
5782 T t2464 o761 b591 b759 b2311 b2313
5783 H h2464 u t2464
5784 T t2465 o761 b591 b759 b2313 b597
5785 H h2465 v t2465
5786 S s2465 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2456 h2464 h2465
5787 G s2465 t2318
5788 B b2465 s2465
5789 T t2466 o1095 b2465 b602
5790 B b2466 t2466
5791 S s2466 t684 h h510 h1304 h2308 h2309 h2310 h2311 h2312 h2464 h2465
5792 G s2466 t2318
5793 B b2467 s2466
5794 T t2467 o1095 b2467 b602
5795 B b2468 t2467
5796 T t2468 o1094 b2468 b4 b2461
5797 B b2469 t2468
5798 T t2469 o2 b2469
5799 B b2470 t2469
5800 T t2470 o1094 b2466 b4 b2470
5801 B b2471 t2470
5802 T t2471 o b2471 b4
5803 B b2472 t2471
5804 T t2472 o b2464 b2472
5805 B b2473 t2472
5806 T t2473 o1093 b2443 b2473
5807 B b2474 t2473
5808 P p2474 String "autoT thenT rwh unfold_equiv 7 ttca thenT rwh unfold_equiv 2 ttca"
5809 O o2474 ext_rule p2474
5810 T t2474 o1093 b2464 b4
5811 B b2475 t2474
5812 T t2475 o2474 b1092 b2475 b4 b4
5813 B b2476 t2475
5814 P p2476 String "equivTransT << 'b >> 10 thenT autoT thenT rwh unfold_equiv 7 ttca thenT rwh unfold_equiv 2 ttca"
5815 O o2476 ext_rule p2476
5816 T t2476 o1093 b2471 b4
5817 B b2477 t2476
5818 T t2477 o2476 b1092 b2477 b4 b4
5819 B b2478 t2477
5820 T t2478 o b2478 b4
5821 B b2479 t2478
5822 T t2479 o b2476 b2479
5823 B b2480 t2479
5824 T t2480 o2445 b1092 b2474 b2480 b4
5825 B b2481 t2480
5826 T t2481 o b2481 b4
5827 B b2482 t2481
5828 T t2482 o2308 b1092 b2445 b2482 b4
5829 B b2483 t2482
5830 T t2483 o b2483 b4
5831 B b2484 t2483
5832 T t2484 o b2308 b2484
5833 B b2485 t2484
5834 T t2485 o b2299 b2485
5835 B b2486 t2485
5836 T t2486 o1919 b1092 b2260 b2486 b4
5837 B b2487 t2486
5838 T t2487 o b2487 b4
5839 B b2488 t2487
5840 T t2488 o b1917 b2488
5841 B b2489 t2488
5842 T t2489 o681 b1092 b1857 b2489 b4
5843 B b2490 t2489
5844 T t2490 o b2490 b4
5845 B b2491 t2490
5846 T t2491 o586 b1092 b679 b2491 b4
5847 B b2492 t2491
5848 T t2492 o1090 b2492
5849 B b2493 t2492
5850 P p2493 Number 8536
5851 P p2494 Number 8543
5852 O o2494 resource_defs p2493 p2494 p176
5853 P p2495 Number 8541
5854 O o2495 uid p2495 p2494
5855 T t2495 o2495 b691
5856 B b2495 t2495
5857 T t2496 o b2495 b4
5858 B b2496 t2496
5859 T t2497 o2494 b2496
5860 B b2497 t2497
5861 T t2498 o b2497 b4
5862 B b2498 t2498
5863 T t2499 o503 b1302 b583 b2493 b2498
5864 B b2499 t2499
5865 T t2500 o2436 b2499
5866 B b2500 t2500
5867 T t2501 o761 b591 b759 b2151 b604
5868 S s2501 t684 h
5869 G s2501 t2501
5870 B b2501 s2501
5871 T t2502 o677 b2501
5872 B b2502 t2502
5873 T t2503 o676 b945 b2502
5874 B b2503 t2503
5875 T t2504 o676 b763 b2503
5876 B b2504 t2504
5877 T t2505 o676 b700 b2504
5878 B b2505 t2505
5879 T t2506 o676 b682 b2505
5880 B b2506 t2506
5881 T t2507 o676 b761 b2506
5882 B b2507 t2507
5883 T t2508 o676 b817 b2507
5884 B b2508 t2508
5885 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"
5886 O o2508 ext_rule p2508
5887 T t2509 o b944 b4
5888 B b2509 t2509
5889 T t2510 o b762 b2509
5890 B b2510 t2510
5891 T t2511 o b699 b2510
5892 B b2511 t2511
5893 T t2512 o b681 b2511
5894 B b2512 t2512
5895 T t2513 o b760 b2512
5896 B b2513 t2513
5897 T t2514 o b816 b2513
5898 B b2514 t2514
5899 T t2515 o1095 b2501 b2514
5900 B b2515 t2515
5901 T t2516 o1094 b2515 b4 b1104
5902 B b2516 t2516
5903 T t2517 o596 b585 b2151 b2151
5904 B b2517 t2517
5905 T t2518 o761 b591 b759 b2517 b2151
5906 S s2518 t684 h
5907 G s2518 t2518
5908 B b2518 s2518
5909 T t2519 o1095 b2518 b2514
5910 B b2519 t2519
5911 T t2520 o2 b2516
5912 B b2520 t2520
5913 T t2521 o2369 b2519 b4 b2520
5914 B b2521 t2521
5915 H h2521 v t2518
5916 S s2521 t684 h h2521
5917 G s2521 t2501
5918 B b2522 s2521
5919 T t2522 o1095 b2522 b2514
5920 B b2523 t2522
5921 T t2523 o1094 b2523 b4 b2520
5922 B b2524 t2523
5923 T t2524 o b2524 b4
5924 B b2525 t2524
5925 T t2525 o b2521 b2525
5926 B b2526 t2525
5927 T t2526 o1093 b2516 b2526
5928 B b2527 t2526
5929 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"
5930 O o2527 ext_rule p2527
5931 T t2527 o596 b585 b2074 b2151
5932 B b2528 t2527
5933 T t2528 o596 b585 b815 b2528
5934 B b2529 t2528
5935 T t2529 o761 b591 b759 b2529 b2151
5936 S s2529 t684 h
5937 G s2529 t2529
5938 B b2530 s2529
5939 T t2530 o1095 b2530 b2514
5940 B b2531 t2530
5941 T t2531 o2 b2521
5942 B b2532 t2531
5943 T t2532 o2369 b2531 b4 b2532
5944 B b2533 t2532
5945 T t2533 o b2533 b4
5946 B b2534 t2533
5947 T t2534 o1093 b2521 b2534
5948 B b2535 t2534
5949 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"
5950 O o2535 ext_rule p2535
5951 T t2535 o596 b585 b2097 b2074
5952 B b2536 t2535
5953 T t2536 o596 b585 b815 b2536
5954 B b2537 t2536
5955 T t2537 o761 b591 b759 b2537 b2151
5956 S s2537 t684 h
5957 G s2537 t2537
5958 B b2538 s2537
5959 T t2538 o1095 b2538 b2514
5960 B b2539 t2538
5961 T t2539 o2 b2533
5962 B b2540 t2539
5963 T t2540 o2369 b2539 b4 b2540
5964 B b2541 t2540
5965 T t2541 o b2541 b4
5966 B b2542 t2541
5967 T t2542 o1093 b2533 b2542
5968 B b2543 t2542
5969 P p2543 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT"
5970 O o2543 ext_rule p2543
5971 T t2543 o596 b585 b818 b2074
5972 B b2544 t2543
5973 T t2544 o596 b585 b815 b2544
5974 B b2545 t2544 z
5975 T t2545 o817 b591 b759 b2545
5976 S s2545 t684 h
5977 G s2545 t2545
5978 B b2546 s2545
5979 T t2546 o1095 b2546 b2514
5980 B b2547 t2546
5981 B b2548 t2544
5982 T t2548 o761 b591 b759 b2548 b2151
5983 B b2549 t2548 z
5984 T t2549 o1077 b591 b759 b2549
5985 S s2549 t684 h
5986 G s2549 t2549
5987 B b2550 s2549
5988 T t2550 o1095 b2550 b2514
5989 B b2551 t2550
5990 T t2551 o2 b2541
5991 B b2552 t2551
5992 T t2552 o2369 b2551 b1864 b2552
5993 B b2553 t2552
5994 T t2553 o2 b2553
5995 B b2554 t2553
5996 T t2554 o2369 b2547 b4 b2554
5997 B b2555 t2554
5998 T t2555 o b2555 b4
5999 B b2556 t2555
6000 T t2556 o1093 b2541 b2556
6001 B b2557 t2556
6002 P p2557 String "rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 5 ttca"
6003 O o2557 ext_rule p2557
6004 T t2557 o1093 b2555 b4
6005 B b2558 t2557
6006 T t2558 o2557 b1092 b2558 b4 b4
6007 B b2559 t2558
6008 T t2559 o b2559 b4
6009 B b2560 t2559
6010 T t2560 o2543 b1092 b2557 b2560 b4
6011 B b2561 t2560
6012 T t2561 o b2561 b4
6013 B b2562 t2561
6014 T t2562 o2535 b1092 b2543 b2562 b4
6015 B b2563 t2562
6016 T t2563 o b2563 b4
6017 B b2564 t2563
6018 T t2564 o2527 b1092 b2535 b2564 b4
6019 B b2565 t2564
6020 P p2565 String "dT 2 ttca"
6021 O o2565 ext_rule p2565
6022 T t2565 o1093 b2524 b4
6023 B b2566 t2565
6024 T t2566 o2565 b1092 b2566 b4 b4
6025 B b2567 t2566
6026 T t2567 o b2567 b4
6027 B b2568 t2567
6028 T t2568 o b2565 b2568
6029 B b2569 t2568
6030 T t2569 o2508 b1092 b2527 b2569 b4
6031 B b2570 t2569
6032 T t2570 o1090 b2570
6033 B b2571 t2570
6034 P p2571 Number 9272
6035 P p2572 Number 9279
6036 O o2572 resource_defs p2571 p2572 p204
6037 P p2573 Number 9277
6038 O o2573 uid p2573 p2572
6039 T t2573 o2573 b691
6040 B b2573 t2573
6041 T t2574 o b2573 b4
6042 B b2574 t2574
6043 T t2575 o2572 b2574
6044 B b2575 t2575
6045 T t2576 o b2575 b4
6046 B b2576 t2576
6047 T t2577 o1053 b676 b2508 b2571 b2576
6048 B b2577 t2577
6049 T t2578 o2436 b2577
6050 B b2578 t2578
6051 T t2579 o1095 b964 b2514
6052 B b2579 t2579
6053 T t2580 o1094 b2579 b4 b1104
6054 B b2580 t2580
6055 S s2580 t684 h
6056 G s2580 t2098
6057 B b2581 s2580
6058 T t2581 o1095 b2581 b2514
6059 B b2582 t2581
6060 T t2582 o2 b2580
6061 B b2583 t2582
6062 T t2583 o1094 b2582 b4 b2583
6063 B b2584 t2583
6064 T t2584 o596 b585 b815 b2097
6065 B b2585 t2584
6066 T t2585 o761 b591 b759 b2585 b815
6067 S s2585 t684 h
6068 G s2585 t2585
6069 B b2586 s2585
6070 T t2586 o1095 b2586 b2514
6071