/[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 3527 - (show annotations) (download)
Mon Mar 4 02:20:01 2002 UTC (19 years, 4 months ago) by xiny
File size: 120257 byte(s)
1. Replaced equality relations with equivalence relations in
   the definition axioms for "op", "inv", and "id".
2. Defined the equivalence functionality for "op" and "inv".
3. Changed the tactics for "left and right cancellation laws"
   (i.e., groupCancelLeftT and groupCancelRightT) to make it
   easier to use.
4. Re-proved all properties.

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 p962 Number 6989
2493 O o962 location p961 p962
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 p971 Number 6627
2517 P p972 Number 6634
2518 O o972 resource_defs p971 p972 p204
2519 P p973 Number 6632
2520 O o973 uid p973 p972
2521 T t973 o973 b691
2522 B b973 t973
2523 T t974 o b973 b4
2524 B b974 t974
2525 T t975 o972 b974
2526 B b975 t975
2527 T t976 o b975 b4
2528 B b976 t976
2529 T t977 o963 b676 b971 b688 b976
2530 B b977 t977
2531 T t978 o962 b977
2532 B b978 t978
2533 P p978 Number 6991
2534 P p979 Number 7260
2535 O o979 location p978 p979
2536 P p980 String inv_wf1
2537 O o980 rule p980
2538 T t980 o609 b585 b714
2539 B b980 t980
2540 T t981 o700 b980
2541 S s981 t684 h
2542 G s981 t981
2543 B b981 s981
2544 T t982 o677 b981
2545 B b982 t982
2546 T t983 o676 b737 b982
2547 B b983 t983
2548 T t984 o676 b700 b983
2549 B b984 t984
2550 T t985 o676 b682 b984
2551 B b985 t985
2552 T t986 o676 b716 b985
2553 B b986 t986
2554 P p986 Number 7014
2555 P p987 Number 7021
2556 O o987 resource_defs p986 p987 p204
2557 P p988 Number 7019
2558 O o988 uid p988 p987
2559 T t988 o988 b691
2560 B b988 t988
2561 T t989 o b988 b4
2562 B b989 t989
2563 T t990 o987 b989
2564 B b990 t990
2565 T t991 o b990 b4
2566 B b991 t991
2567 T t992 o980 b676 b986 b688 b991
2568 B b992 t992
2569 T t993 o979 b992
2570 B b993 t993
2571 P p993 Number 7262
2572 P p994 Number 7538
2573 O o994 location p993 p994
2574 P p995 String inv_wf2
2575 O o995 rule p995
2576 T t995 o736 b980 b591
2577 S s995 t684 h
2578 G s995 t995
2579 B b995 s995
2580 T t996 o677 b995
2581 B b996 t996
2582 T t997 o676 b737 b996
2583 B b997 t997
2584 T t998 o676 b700 b997
2585 B b998 t998
2586 T t999 o676 b682 b998
2587 B b999 t999
2588 T t1000 o676 b716 b999
2589 B b1000 t1000
2590 P p1000 Number 7285
2591 P p1001 Number 7292
2592 O o1001 resource_defs p1000 p1001 p204
2593 P p1002 Number 7290
2594 O o1002 uid p1002 p1001
2595 T t1002 o1002 b691
2596 B b1002 t1002
2597 T t1003 o b1002 b4
2598 B b1003 t1003
2599 T t1004 o1001 b1003
2600 B b1004 t1004
2601 T t1005 o b1004 b4
2602 B b1005 t1005
2603 T t1006 o995 b676 b1000 b688 b1005
2604 B b1006 t1006
2605 T t1007 o994 b1006
2606 B b1007 t1007
2607 P p1007 Number 7540
2608 P p1008 Number 7839
2609 O o1008 location p1007 p1008
2610 P p1009 String inv_equiv_fun1
2611 O o1009 rule p1009
2612 T t1009 o609 b585 b818
2613 B b1009 t1009 z
2614 T t1010 o817 b591 b759 b1009
2615 S s1010 t684 h
2616 G s1010 t1010
2617 B b1010 s1010
2618 T t1011 o677 b1010
2619 B b1011 t1011
2620 T t1012 o676 b763 b1011
2621 B b1012 t1012
2622 T t1013 o676 b700 b1012
2623 B b1013 t1013
2624 T t1014 o676 b682 b1013
2625 B b1014 t1014
2626 T t1015 o676 b761 b1014
2627 B b1015 t1015
2628 P p1015 Number 7570
2629 P p1016 Number 7577
2630 O o1016 resource_defs p1015 p1016 p204
2631 P p1017 Number 7575
2632 O o1017 uid p1017 p1016
2633 T t1017 o1017 b691
2634 B b1017 t1017
2635 T t1018 o b1017 b4
2636 B b1018 t1018
2637 T t1019 o1016 b1018
2638 B b1019 t1019
2639 T t1020 o b1019 b4
2640 B b1020 t1020
2641 T t1021 o1009 b676 b1015 b688 b1020
2642 B b1021 t1021
2643 T t1022 o1008 b1021
2644 B b1022 t1022
2645 P p1022 Number 7841
2646 P p1023 Number 8023
2647 O o1023 location p1022 p1023
2648 P p1024 String inv_eq_fun1
2649 O o1024 rule p1024
2650 T t1024 o852 b1009
2651 S s1024 t684 h
2652 G s1024 t1024
2653 B b1024 s1024
2654 T t1025 o677 b1024
2655 B b1025 t1025
2656 T t1026 o676 b700 b1025
2657 B b1026 t1026
2658 T t1027 o676 b682 b1026
2659 B b1027 t1027
2660 P p1027 Number 7868
2661 P p1028 Number 7875
2662 O o1028 resource_defs p1027 p1028 p204
2663 P p1029 Number 7873
2664 O o1029 uid p1029 p1028
2665 T t1029 o1029 b691
2666 B b1029 t1029
2667 T t1030 o b1029 b4
2668 B b1030 t1030
2669 T t1031 o1028 b1030
2670 B b1031 t1031
2671 T t1032 o b1031 b4
2672 B b1032 t1032
2673 T t1033 o1024 b676 b1027 b688 b1032
2674 B b1033 t1033
2675 T t1034 o1023 b1033
2676 B b1034 t1034
2677 P p1034 Number 8025
2678 P p1035 Number 8423
2679 O o1035 location p1034 p1035
2680 P p1036 String inv_id1
2681 O o1036 rule p1036
2682 T t1036 o596 b585 b980 b714
2683 B b1036 t1036
2684 T t1037 o761 b591 b759 b1036 b604
2685 S s1037 t684 h
2686 G s1037 t1037
2687 B b1037 s1037
2688 T t1038 o677 b1037
2689 B b1038 t1038
2690 T t1039 o676 b737 b1038
2691 B b1039 t1039
2692 T t1040 o676 b763 b1039
2693 B b1040 t1040
2694 T t1041 o676 b700 b1040
2695 B b1041 t1041
2696 T t1042 o676 b682 b1041
2697 B b1042 t1042
2698 T t1043 o676 b761 b1042
2699 B b1043 t1043
2700 T t1044 o676 b716 b1043
2701 B b1044 t1044
2702 P p1044 Number 8048
2703 P p1045 Number 8055
2704 O o1045 resource_defs p1044 p1045 p204
2705 P p1046 Number 8053
2706 O o1046 uid p1046 p1045
2707 T t1046 o1046 b691
2708 B b1046 t1046
2709 T t1047 o b1046 b4
2710 B b1047 t1047
2711 T t1048 o1045 b1047
2712 B b1048 t1048
2713 T t1049 o b1048 b4
2714 B b1049 t1049
2715 T t1050 o1036 b676 b1044 b688 b1049
2716 B b1050 t1050
2717 T t1051 o1035 b1050
2718 B b1051 t1051
2719 P p1051 Number 8425
2720 P p1052 Number 8823
2721 O o1052 location p1051 p1052
2722 P p1053 String inv_id2
2723 O o1053 rule p1053
2724 T t1053 o596 b585 b714 b980
2725 B b1053 t1053
2726 T t1054 o761 b591 b759 b1053 b604
2727 S s1054 t684 h
2728 G s1054 t1054
2729 B b1054 s1054
2730 T t1055 o677 b1054
2731 B b1055 t1055
2732 T t1056 o676 b737 b1055
2733 B b1056 t1056
2734 T t1057 o676 b763 b1056
2735 B b1057 t1057
2736 T t1058 o676 b700 b1057
2737 B b1058 t1058
2738 T t1059 o676 b682 b1058
2739 B b1059 t1059
2740 T t1060 o676 b761 b1059
2741 B b1060 t1060
2742 T t1061 o676 b716 b1060
2743 B b1061 t1061
2744 P p1061 Number 8448
2745 P p1062 Number 8455
2746 O o1062 resource_defs p1061 p1062 p204
2747 P p1063 Number 8453
2748 O o1063 uid p1063 p1062
2749 T t1063 o1063 b691
2750 B b1063 t1063
2751 T t1064 o b1063 b4
2752 B b1064 t1064
2753 T t1065 o1062 b1064
2754 B b1065 t1065
2755 T t1066 o b1065 b4
2756 B b1066 t1066
2757 T t1067 o1053 b676 b1061 b688 b1066
2758 B b1067 t1067
2759 T t1068 o1052 b1067
2760 B b1068 t1068
2761 P p1068 Number 8845
2762 P p1069 Number 9369
2763 O o1069 location p1068 p1069
2764 P p1070 String equiv_op_fun1
2765 O o1070 rule p1070
2766 T t1070 o700 b597
2767 S s1070 t679 h
2768 G s1070 t1070
2769 B b1070 s1070
2770 T t1071 o677 b1070
2771 B b1071 t1071
2772 T t1072 o700 b598
2773 S s1072 t679 h
2774 G s1072 t1072
2775 B b1072 s1072
2776 T t1073 o677 b1072
2777 B b1073 t1073
2778 T t1074 o736 b597 b591
2779 S s1074 t684 h
2780 G s1074 t1074
2781 B b1074 s1074
2782 T t1075 o677 b1074
2783 B b1075 t1075
2784 T t1076 o736 b598 b591
2785 S s1076 t684 h
2786 G s1076 t1076
2787 B b1076 s1076
2788 T t1077 o677 b1076
2789 B b1077 t1077
2790 NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
2791 O o1077 equiv_fun_prop
2792 T t1078 o596 b585 b818 b597
2793 B b1078 t1078
2794 T t1079 o596 b585 b818 b598
2795 B b1079 t1079
2796 T t1080 o761 b591 b759 b1078 b1079
2797 B b1080 t1080 z
2798 T t1081 o1077 b591 b759 b1080
2799 S s1081 t684 h
2800 G s1081 t1081
2801 B b1081 s1081
2802 T t1082 o677 b1081
2803 B b1082 t1082
2804 T t1083 o676 b1077 b1082
2805 B b1083 t1083
2806 T t1084 o676 b1075 b1083
2807 B b1084 t1084
2808 T t1085 o676 b763 b1084
2809 B b1085 t1085
2810 T t1086 o676 b700 b1085
2811 B b1086 t1086
2812 T t1087 o676 b682 b1086
2813 B b1087 t1087
2814 T t1088 o676 b761 b1087
2815 B b1088 t1088
2816 T t1089 o676 b1073 b1088
2817 B b1089 t1089
2818 T t1090 o676 b1071 b1089
2819 B b1090 t1090
2820 NSummary!interactive interactive interactive Summary
2821 O o1090 interactive
2822 NSummary!ext_rule ext_rule ext_rule Summary
2823 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"
2824 O o1091 ext_rule p1090
2825 NSummary!status_incomplete status_incomplete status_incomplete Summary
2826 O o1092 status_incomplete
2827 T t1092 o1092
2828 B b1092 t1092
2829 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2830 O o1093 ext_unjustified
2831 NSummary!tactic_arg tactic_arg tactic_arg Summary
2832 P p1093 String main
2833 O o1094 tactic_arg p1093
2834 NSummary!msequent msequent msequent Summary
2835 O o1095 msequent
2836 T t1095 o b1076 b4
2837 B b1095 t1095
2838 T t1096 o b1074 b1095
2839 B b1096 t1096
2840 T t1097 o b762 b1096
2841 B b1097 t1097
2842 T t1098 o b699 b1097
2843 B b1098 t1098
2844 T t1099 o b681 b1098
2845 B b1099 t1099
2846 T t1100 o b760 b1099
2847 B b1100 t1100
2848 T t1101 o b1072 b1100
2849 B b1101 t1101
2850 T t1102 o b1070 b1101
2851 B b1102 t1102
2852 T t1103 o1095 b1081 b1102
2853 B b1103 t1103
2854 NSummary!parent_none parent_none parent_none Summary
2855 O o1103 parent_none
2856 T t1104 o1103
2857 B b1104 t1104
2858 T t1105 o1094 b1103 b4 b1104
2859 B b1105 t1105
2860 NCzf_itt_set!set set set Czf_itt_set
2861 O o1105 set
2862 T t1106 o1105
2863 H h1106 a_1 t1106
2864 H h1107 b_1 t1106
2865 H h1108 x t762
2866 P p1108 Var a_1
2867 O o1108 var p1108
2868 T t1108 o1108
2869 B b1108 t1108
2870 P p1109 Var b_1
2871 O o1109 var p1109
2872 T t1109 o1109
2873 B b1109 t1109
2874 T t1110 o761 b591 b759 b1108 b1109
2875 H h1110 x_1 t1110
2876 T t1111 o596 b585 b1108 b597
2877 B b1111 t1111
2878 T t1112 o596 b585 b1108 b598
2879 B b1112 t1112
2880 T t1113 o761 b591 b759 b1111 b1112
2881 H h1113 x_2 t1113
2882 T t1114 o596 b585 b1109 b597
2883 B b1114 t1114
2884 T t1115 o596 b585 b1109 b598
2885 B b1115 t1115
2886 T t1116 o761 b591 b759 b1114 b1115
2887 S s1116 t684 h h1106 h1107 h1108 h1110 h1113
2888 G s1116 t1116
2889 B b1116 s1116
2890 T t1117 o1095 b1116 b1102
2891 B b1117 t1117
2892 NItt_logic Itt_logic Itt_logic NIL
2893 NItt_logic!implies implies implies Itt_logic
2894 O o1117 implies
2895 B b1118 t1113
2896 B b1119 t1116
2897 T t1119 o1117 b1118 b1119
2898 S s1119 t684 h h1106 h1107 h1108 h1110
2899 G s1119 t1119
2900 B b1120 s1119
2901 T t1120 o1095 b1120 b1102
2902 B b1121 t1120
2903 B b1122 t1110
2904 B b1123 t1119
2905 T t1123 o1117 b1122 b1123
2906 S s1123 t684 h h1106 h1107 h1108
2907 G s1123 t1123
2908 B b1124 s1123
2909 T t1124 o1095 b1124 b1102
2910 B b1125 t1124
2911 B b1126 t762
2912 B b1127 t1123
2913 T t1127 o1117 b1126 b1127
2914 S s1127 t684 h h1106 h1107
2915 G s1127 t1127
2916 B b1128 s1127
2917 T t1128 o1095 b1128 b1102
2918 B b1129 t1128
2919 NItt_logic!all all all Itt_logic
2920 O o1129 all
2921 B b1130 t1106
2922 B b1131 t1127 b_1
2923 T t1131 o1129 b1130 b1131
2924 S s1131 t684 h h1106
2925 G s1131 t1131
2926 B b1132 s1131
2927 T t1132 o1095 b1132 b1102
2928 B b1133 t1132
2929 B b1134 t1131 a_1
2930 T t1134 o1129 b1130 b1134
2931 S s1134 t684 h
2932 G s1134 t1134
2933 B b1135 s1134
2934 T t1135 o1095 b1135 b1102
2935 B b1136 t1135
2936 T t1136 o2 b1105
2937 B b1137 t1136
2938 T t1137 o1094 b1136 b4 b1137
2939 B b1138 t1137
2940 T t1138 o2 b1138
2941 B b1139 t1138
2942 T t1139 o1094 b1133 b4 b1139
2943 B b1140 t1139
2944 T t1140 o2 b1140
2945 B b1141 t1140
2946 T t1141 o1094 b1129 b4 b1141
2947 B b1142 t1141
2948 T t1142 o2 b1142
2949 B b1143 t1142
2950 T t1143 o1094 b1125 b4 b1143
2951 B b1144 t1143
2952 T t1144 o2 b1144
2953 B b1145 t1144
2954 T t1145 o1094 b1121 b4 b1145
2955 B b1146 t1145
2956 T t1146 o2 b1146
2957 B b1147 t1146
2958 T t1147 o1094 b1117 b4 b1147
2959 B b1148 t1147
2960 T t1148 o b1148 b4
2961 B b1149 t1148
2962 T t1149 o1093 b1105 b1149
2963 B b1150 t1149
2964 P p1150 String "equivTransT << op{'g; 'b_1; 'a} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
2965 O o1150 ext_rule p1150
2966 NItt_logic!and and and Itt_logic
2967 O o1151 and
2968 B b1151 t700
2969 B b1152 t760
2970 T t1152 o700 b1111
2971 B b1153 t1152
2972 T t1153 o700 b1112
2973 B b1154 t1153
2974 T t1154 o1151 b1153 b1154
2975 B b1155 t1154
2976 T t1155 o1151 b1152 b1155
2977 B b1156 t1155
2978 T t1156 o1151 b1151 b1156
2979 B b1157 t1156
2980 T t1157 o736 b1111 b591
2981 B b1158 t1157
2982 T t1158 o736 b1112 b591
2983 B b1159 t1158
2984 T t1159 o1151 b1158 b1159
2985 B b1160 t1159
2986 T t1160 o1151 b1157 b1160
2987 B b1161 t1160
2988 NCzf_itt_pair Czf_itt_pair Czf_itt_pair NIL
2989 NCzf_itt_pair!pair pair pair Czf_itt_pair
2990 O o1161 pair
2991 T t1161 o1161 b1111 b1112
2992 B b1162 t1161
2993 T t1162 o736 b1162 b759
2994 B b1163 t1162
2995 T t1163 o1151 b1161 b1163
2996 H h1163 x_2 t1163
2997 T t1164 o736 b1114 b591
2998 S s1164 t684 h h1106 h1107 h1108 h1110 h1163
2999 G s1164 t1164
3000 B b1164 s1164
3001 T t1165 o1095 b1164 b1102
3002 B b1165 t1165
3003 S s1165 t684 h h1106 h1107 h1108 h1110 h1113
3004 G s1165 t1164
3005 B b1166 s1165
3006 T t1166 o1095 b1166 b1102
3007 B b1167 t1166
3008 T t1167 o2 b1148
3009 B b1168 t1167
3010 T t1168 o1094 b1167 b4 b1168
3011 B b1169 t1168
3012 T t1169 o2 b1169
3013 B b1170 t1169
3014 T t1170 o1094 b1165 b4 b1170
3015 B b1171 t1170
3016 T t1171 o761 b591 b759 b1111 b1114
3017 H h1171 u t1171
3018 T t1172 o761 b591 b759 b1114 b1112
3019 H h1172 v t1172
3020 S s1172 t684 h h1106 h1107 h1108 h1110 h1163 h1171 h1172
3021 G s1172 t1116
3022 B b1172 s1172
3023 T t1173 o1095 b1172 b1102
3024 B b1173 t1173
3025 S s1173 t684 h h1106 h1107 h1108 h1110 h1113 h1171 h1172
3026 G s1173 t1116
3027 B b1174 s1173
3028 T t1174 o1095 b1174 b1102
3029 B b1175 t1174
3030 T t1175 o1094 b1175 b4 b1168
3031 B b1176 t1175
3032 T t1176 o2 b1176
3033 B b1177 t1176
3034 T t1177 o1094 b1173 b4 b1177
3035 B b1178 t1177
3036 T t1178 o b1178 b4
3037 B b1179 t1178
3038 T t1179 o b1171 b1179
3039 B b1180 t1179
3040 T t1180 o1093 b1148 b1180
3041 B b1181 t1180
3042 P p1181 String "autoT thenT rwh unfold_equiv 5 ttca"
3043 O o1181 ext_rule p1181
3044 T t1181 o1093 b1171 b4
3045 B b1182 t1181
3046 T t1182 o1181 b1092 b1182 b4 b4
3047 B b1183 t1182
3048 P p1183 String "equivTransT << op{'g; 'b_1; 'b} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3049 O o1183 ext_rule p1183
3050 T t1183 o1093 b1178 b4
3051 B b1184 t1183
3052 T t1184 o1183 b1092 b1184 b4 b4
3053 B b1185 t1184
3054 T t1185 o b1185 b4
3055 B b1186 t1185
3056 T t1186 o b1183 b1186
3057 B b1187 t1186
3058 T t1187 o1150 b1092 b1181 b1187 b4
3059 B b1188 t1187
3060 T t1188 o b1188 b4
3061 B b1189 t1188
3062 T t1189 o1091 b1092 b1150 b1189 b4
3063 B b1190 t1189
3064 T t1190 o1090 b1190
3065 B b1191 t1190
3066 P p1191 Number 8874
3067 P p1192 Number 8881
3068 O o1192 resource_defs p1191 p1192 p204
3069 P p1193 Number 8879
3070 O o1193 uid p1193 p1192
3071 T t1193 o1193 b691
3072 B b1193 t1193
3073 T t1194 o b1193 b4
3074 B b1194 t1194
3075 T t1195 o1192 b1194
3076 B b1195 t1195
3077 T t1196 o b1195 b4
3078 B b1196 t1196
3079 T t1197 o1070 b676 b1090 b1191 b1196
3080 B b1197 t1197
3081 T t1198 o1069 b1197
3082 B b1198 t1198
3083 P p1198 Number 9371
3084 P p1199 Number 9895
3085 O o1199 location p1198 p1199
3086 P p1200 String equiv_op_fun2
3087 O o1200 rule p1200
3088 T t1200 o596 b585 b597 b818
3089 B b1200 t1200
3090 T t1201 o596 b585 b598 b818
3091 B b1201 t1201
3092 T t1202 o761 b591 b759 b1200 b1201
3093 B b1202 t1202 z
3094 T t1203 o1077 b591 b759 b1202
3095 S s1203 t684 h
3096 G s1203 t1203
3097 B b1203 s1203
3098 T t1204 o677 b1203
3099 B b1204 t1204
3100 T t1205 o676 b1077 b1204
3101 B b1205 t1205
3102 T t1206 o676 b1075 b1205
3103 B b1206 t1206
3104 T t1207 o676 b763 b1206
3105 B b1207 t1207
3106 T t1208 o676 b700 b1207
3107 B b1208 t1208
3108 T t1209 o676 b682 b1208
3109 B b1209 t1209
3110 T t1210 o676 b761 b1209
3111 B b1210 t1210
3112 T t1211 o676 b1073 b1210
3113 B b1211 t1211
3114 T t1212 o676 b1071 b1211
3115 B b1212 t1212
3116 T t1213 o1095 b1203 b1102
3117 B b1213 t1213
3118 T t1214 o1094 b1213 b4 b1104
3119 B b1214 t1214
3120 T t1215 o596 b585 b597 b1108
3121 B b1215 t1215
3122 T t1216 o596 b585 b598 b1108
3123 B b1216 t1216
3124 T t1217 o761 b591 b759 b1215 b1216
3125 H h1217 x_2 t1217
3126 T t1218 o596 b585 b597 b1109
3127 B b1218 t1218
3128 T t1219 o596 b585 b598 b1109
3129 B b1219 t1219
3130 T t1220 o761 b591 b759 b1218 b1219
3131 S s1220 t684 h h1106 h1107 h1108 h1110 h1217
3132 G s1220 t1220
3133 B b1220 s1220
3134 T t1221 o1095 b1220 b1102
3135 B b1221 t1221
3136 B b1222 t1217
3137 B b1223 t1220
3138 T t1223 o1117 b1222 b1223
3139 S s1223 t684 h h1106 h1107 h1108 h1110
3140 G s1223 t1223
3141 B b1224 s1223
3142 T t1224 o1095 b1224 b1102
3143 B b1225 t1224
3144 B b1226 t1223
3145 T t1226 o1117 b1122 b1226
3146 S s1226 t684 h h1106 h1107 h1108
3147 G s1226 t1226
3148 B b1227 s1226
3149 T t1227 o1095 b1227 b1102
3150 B b1228 t1227
3151 B b1229 t1226
3152 T t1229 o1117 b1126 b1229
3153 S s1229 t684 h h1106 h1107
3154 G s1229 t1229
3155 B b1230 s1229
3156 T t1230 o1095 b1230 b1102
3157 B b1231 t1230
3158 B b1232 t1229 b_1
3159 T t1232 o1129 b1130 b1232
3160 S s1232 t684 h h1106
3161 G s1232 t1232
3162 B b1233 s1232
3163 T t1233 o1095 b1233 b1102
3164 B b1234 t1233
3165 B b1235 t1232 a_1
3166 T t1235 o1129 b1130 b1235
3167 S s1235 t684 h
3168 G s1235 t1235
3169 B b1236 s1235
3170 T t1236 o1095 b1236 b1102
3171 B b1237 t1236
3172 T t1237 o2 b1214
3173 B b1238 t1237
3174 T t1238 o1094 b1237 b4 b1238
3175 B b1239 t1238
3176 T t1239 o2 b1239
3177 B b1240 t1239
3178 T t1240 o1094 b1234 b4 b1240
3179 B b1241 t1240
3180 T t1241 o2 b1241
3181 B b1242 t1241
3182 T t1242 o1094 b1231 b4 b1242
3183 B b1243 t1242
3184 T t1243 o2 b1243
3185 B b1244 t1243
3186 T t1244 o1094 b1228 b4 b1244
3187 B b1245 t1244
3188 T t1245 o2 b1245
3189 B b1246 t1245
3190 T t1246 o1094 b1225 b4 b1246
3191 B b1247 t1246
3192 T t1247 o2 b1247
3193 B b1248 t1247
3194 T t1248 o1094 b1221 b4 b1248
3195 B b1249 t1248
3196 T t1249 o b1249 b4
3197 B b1250 t1249
3198 T t1250 o1093 b1214 b1250
3199 B b1251 t1250
3200 P p1251 String "equivTransT << op{'g; 'a; 'b_1} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
3201 O o1251 ext_rule p1251
3202 T t1251 o700 b1215
3203 B b1252 t1251
3204 T t1252 o700 b1216
3205 B b1253 t1252
3206 T t1253 o1151 b1252 b1253
3207 B b1254 t1253
3208 T t1254 o1151 b1152 b1254
3209 B b1255 t1254
3210 T t1255 o1151 b1151 b1255
3211 B b1256 t1255
3212 T t1256 o736 b1215 b591
3213 B b1257 t1256
3214 T t1257 o736 b1216 b591
3215 B b1258 t1257
3216 T t1258 o1151 b1257 b1258
3217 B b1259 t1258
3218 T t1259 o1151 b1256 b1259
3219 B b1260 t1259
3220 T t1260 o1161 b1215 b1216
3221 B b1261 t1260
3222 T t1261 o736 b1261 b759
3223 B b1262 t1261
3224 T t1262 o1151 b1260 b1262
3225 H h1262 x_2 t1262
3226 T t1263 o736 b1218 b591
3227 S s1263 t684 h h1106 h1107 h1108 h1110 h1262
3228 G s1263 t1263
3229 B b1263 s1263
3230 T t1264 o1095 b1263 b1102
3231 B b1264 t1264
3232 S s1264 t684 h h1106 h1107 h1108 h1110 h1217
3233 G s1264 t1263
3234 B b1265 s1264
3235 T t1265 o1095 b1265 b1102
3236 B b1266 t1265
3237 T t1266 o2 b1249
3238 B b1267 t1266
3239 T t1267 o1094 b1266 b4 b1267
3240 B b1268 t1267
3241 T t1268 o2 b1268
3242 B b1269 t1268
3243 T t1269 o1094 b1264 b4 b1269
3244 B b1270 t1269
3245 T t1270 o761 b591 b759 b1215 b1218
3246 H h1270 u t1270
3247 T t1271 o761 b591 b759 b1218 b1216
3248 H h1271 v t1271
3249 S s1271 t684 h h1106 h1107 h1108 h1110 h1262 h1270 h1271
3250 G s1271 t1220
3251 B b1271 s1271
3252 T t1272 o1095 b1271 b1102
3253 B b1272 t1272
3254 S s1272 t684 h h1106 h1107 h1108 h1110 h1217 h1270 h1271
3255 G s1272 t1220
3256 B b1273 s1272
3257 T t1273 o1095 b1273 b1102
3258 B b1274 t1273
3259 T t1274 o1094 b1274 b4 b1267
3260 B b1275 t1274
3261 T t1275 o2 b1275
3262 B b1276 t1275
3263 T t1276 o1094 b1272 b4 b1276
3264 B b1277 t1276
3265 T t1277 o b1277 b4
3266 B b1278 t1277
3267 T t1278 o b1270 b1278
3268 B b1279 t1278
3269 T t1279 o1093 b1249 b1279
3270 B b1280 t1279
3271 T t1280 o1093 b1270 b4
3272 B b1281 t1280
3273 T t1281 o1181 b1092 b1281 b4 b4
3274 B b1282 t1281
3275 P p1282 String "equivTransT << op{'g; 'b; 'b_1} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3276 O o1282 ext_rule p1282
3277 T t1282 o1093 b1277 b4
3278 B b1283 t1282
3279 T t1283 o1282 b1092 b1283 b4 b4
3280 B b1284 t1283
3281 T t1284 o b1284 b4
3282 B b1285 t1284
3283 T t1285 o b1282 b1285
3284 B b1286 t1285
3285 T t1286 o1251 b1092 b1280 b1286 b4
3286 B b1287 t1286
3287 T t1287 o b1287 b4
3288 B b1288 t1287
3289 T t1288 o1091 b1092 b1251 b1288 b4
3290 B b1289 t1288
3291 T t1289 o1090 b1289
3292 B b1290 t1289
3293 P p1290 Number 9400
3294 P p1291 Number 9407
3295 O o1291 resource_defs p1290 p1291 p204
3296 P p1292 Number 9405
3297 O o1292 uid p1292 p1291
3298 T t1292 o1292 b691
3299 B b1292 t1292
3300 T t1293 o b1292 b4
3301 B b1293 t1293
3302 T t1294 o1291 b1293
3303 B b1294 t1294
3304 T t1295 o b1294 b4
3305 B b1295 t1295
3306 T t1296 o1200 b676 b1212 b1290 b1295
3307 B b1296 t1296
3308 T t1297 o1199 b1296
3309 B b1297 t1297
3310 P p1297 Number 11515
3311 P p1298 Number 12822
3312 O o1298 location p1297 p1298
3313 P p1299 String cancel1
3314 O o1299 rule p1299
3315 P p1300 String J
3316 O o1300 context_param p1300
3317 T t1300 o1300
3318 B b1300 t1300
3319 T t1301 o b1300 b4
3320 B b1301 t1301
3321 T t1302 o b675 b1301
3322 B b1302 t1302
3323 T t1303 o761 b591 b759 b720 b791
3324 H h1303 x t1303
3325 P p1303 Var x
3326 O o1303 var p1303
3327 T t1304 o1303
3328 C h1304 J t1304
3329 S s1304 t679 h h1303 h1304
3330 G s1304 t715
3331 B b1304 s1304
3332 T t1305 o677 b1304
3333 B b1305 t1305
3334 S s1305 t679 h h1303 h1304
3335 G s1305 t718
3336 B b1306 s1305
3337 T t1306 o677 b1306
3338 B b1307 t1306
3339 S s1307 t679 h h1303 h1304
3340 G s1307 t757
3341 B b1308 s1307
3342 T t1308 o677 b1308
3343 B b1309 t1308
3344 S s1309 t679 h h1303 h1304
3345 G s1309 t760
3346 B b1310 s1309
3347 T t1310 o677 b1310
3348 B b1311 t1310
3349 S s1311 t679 h h1303 h1304
3350 G s1311 t681
3351 B b1312 s1311
3352 T t1312 o677 b1312
3353 B b1313 t1312
3354 S s1313 t684 h h1303 h1304
3355 G s1313 t586
3356 B b1314 s1313
3357 T t1314 o677 b1314
3358 B b1315 t1314
3359 S s1315 t684 h h1303 h1304
3360 G s1315 t762
3361 B b1316 s1315
3362 T t1316 o677 b1316
3363 B b1317 t1316
3364 S s1317 t684 h h1303 h1304
3365 G s1317 t736
3366 B b1318 s1317
3367 T t1318 o677 b1318
3368 B b1319 t1318
3369 S s1319 t684 h h1303 h1304
3370 G s1319 t738
3371 B b1320 s1319
3372 T t1320 o677 b1320
3373 B b1321 t1320
3374 S s1321 t684 h h1303 h1304
3375 G s1321 t764
3376 B b1322 s1321
3377 T t1322 o677 b1322
3378 B b1323 t1322
3379 T t1323 o761 b591 b759 b717 b756
3380 S s1323 t684 h h1303 h1304
3381 G s1323 t1323
3382 B b1324 s1323
3383 T t1324 o677 b1324
3384 B b1325 t1324
3385 T t1325 o676 b1323 b1325
3386 B b1326 t1325
3387 T t1326 o676 b1321 b1326
3388 B b1327 t1326
3389 T t1327 o676 b1319 b1327
3390 B b1328 t1327
3391 T t1328 o676 b1317 b1328
3392 B b1329 t1328
3393 T t1329 o676 b1315 b1329
3394 B b1330 t1329
3395 T t1330 o676 b1313 b1330
3396 B b1331 t1330
3397 T t1331 o676 b1311 b1331
3398 B b1332 t1331
3399 T t1332 o676 b1309 b1332
3400 B b1333 t1332
3401 T t1333 o676 b1307 b1333
3402 B b1334 t1333
3403 T t1334 o676 b1305 b1334
3404 B b1335 t1334
3405 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"
3406 O o1335 ext_rule p1335
3407 T t1335 o b1322 b4
3408 B b1336 t1335
3409 T t1336 o b1320 b1336
3410 B b1337 t1336
3411 T t1337 o b1318 b1337
3412 B b1338 t1337
3413 T t1338 o b1316 b1338
3414 B b1339 t1338
3415 T t1339 o b1314 b1339
3416 B b1340 t1339
3417 T t1340 o b1312 b1340
3418 B b1341 t1340
3419 T t1341 o b1310 b1341
3420 B b1342 t1341
3421 T t1342 o b1308 b1342
3422 B b1343 t1342
3423 T t1343 o b1306 b1343
3424 B b1344 t1343
3425 T t1344 o b1304 b1344
3426 B b1345 t1344
3427 T t1345 o1095 b1324 b1345
3428 B b1346 t1345
3429 T t1346 o1094 b1346 b4 b1104
3430 B b1347 t1346
3431 T t1347 o596 b585 b980 b720
3432 B b1348 t1347
3433 T t1348 o596 b585 b980 b791
3434 B b1349 t1348
3435 T t1349 o761 b591 b759 b1348 b1349
3436 H h1349 v t1349
3437 S s1349 t684 h h1303 h1304 h1349
3438 G s1349 t1323
3439 B b1350 s1349
3440 T t1350 o1095 b1350 b1345
3441 B b1351 t1350
3442 T t1351 o2 b1347
3443 B b1352 t1351
3444 T t1352 o1094 b1351 b4 b1352
3445 B b1353 t1352
3446 T t1353 o b1353 b4
3447 B b1354 t1353
3448 T t1354 o1093 b1347 b1354
3449 B b1355 t1354
3450 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"
3451 O o1355 ext_rule p1355
3452 T t1355 o596 b585 b1036 b717
3453 B b1356 t1355
3454 T t1356 o761 b591 b759 b1356 b1349
3455 H h1356 z t1356
3456 S s1356 t684 h h1303 h1304 h1349 h1356
3457 G s1356 t1323
3458 B b1357 s1356
3459 T t1357 o1095 b1357 b1345
3460 B b1358 t1357
3461 T t1358 o2 b1353
3462 B b1359 t1358
3463 T t1359 o1094 b1358 b4 b1359
3464 B b1360 t1359
3465 T t1360 o b1360 b4
3466 B b1361 t1360
3467 T t1361 o1093 b1353 b1361
3468 B b1362 t1361
3469 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"
3470 O o1362 ext_rule p1362
3471 T t1362 o596 b585 b1036 b756
3472 B b1363 t1362
3473 T t1363 o761 b591 b759 b1356 b1363
3474 H h1363 z_1 t1363
3475 S s1363 t684 h h1303 h1304 h1349 h1356 h1363
3476 G s1363 t1323
3477 B b1364 s1363
3478 T t1364 o1095 b1364 b1345
3479 B b1365 t1364
3480 T t1365 o2 b1360
3481 B b1366 t1365
3482 T t1366 o1094 b1365 b4 b1366
3483 B b1367 t1366
3484 T t1367 o b1367 b4
3485 B b1368 t1367
3486 T t1368 o1093 b1360 b1368
3487 B b1369 t1368
3488 P p1369 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"
3489 O o1369 ext_rule p1369
3490 T t1369 o596 b585 b604 b717
3491 B b1370 t1369
3492 T t1370 o596 b585 b604 b756
3493 B b1371 t1370
3494 T t1371 o761 b591 b759 b1370 b1371
3495 H h1371 z_2 t1371
3496 S s1371 t684 h h1303 h1304 h1349 h1356 h1363 h1371
3497 G s1371 t1323
3498 B b1372 s1371
3499 T t1372 o1095 b1372 b1345
3500 B b1373 t1372
3501 T t1373 o2 b1367
3502 B b1374 t1373
3503 T t1374 o1094 b1373 b4 b1374
3504 B b1375 t1374
3505 T t1375 o b1375 b4
3506 B b1376 t1375
3507 T t1376 o1093 b1367 b1376
3508 B b1377 t1376
3509 P p1377 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"
3510 O o1377 ext_rule p1377
3511 T t1377 o761 b591 b759 b717 b1371
3512 H h1377 z_3 t1377
3513 S s1377 t684 h h1303 h1304 h1349 h1356 h1363 h1371 h1377
3514 G s1377 t1323
3515 B b1378 s1377
3516 T t1378 o1095 b1378 b1345
3517 B b1379 t1378
3518 T t1379 o2 b1375
3519 B b1380 t1379
3520 T t1380 o1094 b1379 b4 b1380
3521 B b1381 t1380
3522 T t1381 o b1381 b4
3523 B b1382 t1381
3524 T t1382 o1093 b1375 b1382
3525 B b1383 t1382
3526 P p1383 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"
3527 O o1383 ext_rule p1383
3528 T t1383 o1093 b1381 b4
3529 B b1384 t1383
3530 T t1384 o1383 b1092 b1384 b4 b4
3531 B b1385 t1384
3532 T t1385 o b1385 b4
3533 B b1386 t1385
3534 T t1386 o1377 b1092 b1383 b1386 b4
3535 B b1387 t1386
3536 T t1387 o b1387 b4
3537 B b1388 t1387
3538 T t1388 o1369 b1092 b1377 b1388 b4
3539 B b1389 t1388
3540 T t1389 o b1389 b4
3541 B b1390 t1389
3542 T t1390 o1362 b1092 b1369 b1390 b4
3543 B b1391 t1390
3544 T t1391 o b1391 b4
3545 B b1392 t1391
3546 T t1392 o1355 b1092 b1362 b1392 b4
3547 B b1393 t1392
3548 T t1393 o b1393 b4
3549 B b1394 t1393
3550 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"
3551 O o1394 ext_rule p1394
3552 H h1394 v t1303
3553 H h1395 v_1 t1349
3554 S s1395 t684 h h1394 h1395
3555 G s1395 t1323
3556 B b1395 s1395
3557 S s1396 t684 h
3558 G s1396 t1303
3559 B b1396 s1396
3560 T t1396 o b1396 b4
3561 B b1397 t1396
3562 T t1397 o b764 b1397
3563 B b1398 t1397
3564 T t1398 o b738 b1398
3565 B b1399 t1398
3566 T t1399 o b736 b1399
3567 B b1400 t1399
3568 T t1400 o b762 b1400
3569 B b1401 t1400
3570 T t1401 o b699 b1401
3571 B b1402 t1401
3572 T t1402 o b681 b1402
3573 B b1403 t1402
3574 T t1403 o b760 b1403
3575 B b1404 t1403
3576 T t1404 o b757 b1404
3577 B b1405 t1404
3578 T t1405 o b718 b1405
3579 B b1406 t1405
3580 T t1406 o b715 b1406
3581 B b1407 t1406
3582 T t1407 o1095 b1395 b1407
3583 B b1408 t1407
3584 S s1408 t684 h h1394
3585 G s1408 t1323
3586 B b1409 s1408
3587 T t1409 o1095 b1409 b1407
3588 B b1410 t1409
3589 S s1410 t684 h
3590 G s1410 t1323
3591 B b1411 s1410
3592 T t1411 o1095 b1411 b1407
3593 B b1412 t1411
3594 T t1412 o1094 b1412 b4 b1104
3595 B b1413 t1412
3596 T t1413 o2 b1413
3597 B b1414 t1413
3598 T t1414 o1094 b1410 b4 b1414
3599 B b1415 t1414
3600 T t1415 o2 b1415
3601 B b1416 t1415
3602 T t1416 o1094 b1408 b4 b1416
3603 B b1417 t1416
3604 S s1417 t684 h h1394 h1395 h1356
3605 G s1417 t1323
3606 B b1418 s1417
3607 T t1418 o1095 b1418 b1407
3608 B b1419 t1418
3609 T t1419 o2 b1417
3610 B b1420 t1419
3611 T t1420 o1094 b1419 b4 b1420
3612 B b1421 t1420
3613 T t1421 o b1421 b4
3614 B b1422 t1421
3615 T t1422 o1093 b1417 b1422
3616 B b1423 t1422
3617 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"
3618 O o1423 ext_rule p1423
3619 S s1423 t684 h h1394 h1395 h1356 h1363
3620 G s1423 t1323
3621 B b1424 s1423
3622 T t1424 o1095 b1424 b1407
3623 B b1425 t1424
3624 T t1425 o2 b1421
3625 B b1426 t1425
3626 T t1426 o1094 b1425 b4 b1426
3627 B b1427 t1426
3628 T t1427 o b1427 b4
3629 B b1428 t1427
3630 T t1428 o1093 b1421 b1428
3631 B b1429 t1428
3632 P p1429 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 ttca"
3633 O o1429 ext_rule p1429
3634 S s1429 t684 h h1394 h1395 h1356 h1363 h1371
3635 G s1429 t1323
3636 B b1430 s1429
3637 T t1430 o1095 b1430 b1407
3638 B b1431 t1430
3639 T t1431 o2 b1427
3640 B b1432 t1431
3641 T t1432 o1094 b1431 b4 b1432
3642 B b1433 t1432
3643 T t1433 o b1433 b4
3644 B b1434 t1433
3645 T t1434 o1093 b1427 b1434
3646 B b1435 t1434
3647 P p1435 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 6 ttca"
3648 O o1435 ext_rule p1435
3649 S s1435 t684 h h1394 h1395 h1356 h1363 h1371 h1377
3650 G s1435 t1323
3651 B b1436 s1435
3652 T t1436 o1095 b1436 b1407
3653 B b1437 t1436
3654 T t1437 o2 b1433
3655 B b1438 t1437
3656 T t1438 o1094 b1437 b4 b1438
3657 B b1439 t1438
3658 T t1439 o b1439 b4
3659 B b1440 t1439
3660 T t1440 o1093 b1433 b1440
3661 B b1441 t1440
3662 P p1441 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 7 ttca"
3663 O o1441 ext_rule p1441
3664 T t1441 o1093 b1439 b4
3665 B b1442 t1441
3666 T t1442 o1441 b1092 b1442 b4 b4
3667 B b1443 t1442
3668 T t1443 o b1443 b4
3669 B b1444 t1443
3670 T t1444 o1435 b1092 b1441 b1444 b4
3671 B b1445 t1444
3672 T t1445 o b1445 b4
3673 B b1446 t1445
3674 T t1446 o1429 b1092 b1435 b1446 b4
3675 B b1447 t1446
3676 T t1447 o b1447 b4
3677 B b1448 t1447
3678 T t1448 o1423 b1092 b1429 b1448 b4
3679 B b1449 t1448
3680 T t1449 o b1449 b4
3681 B b1450 t1449
3682 T t1450 o1394 b1092 b1423 b1450 b4
3683 B b1451 t1450
3684 T t1451 o b1451 b4
3685 B b1452 t1451
3686 T t1452 o1335 b1092 b1355 b1394 b1452
3687 B b1453 t1452
3688 T t1453 o1090 b1453
3689 B b1454 t1453
3690 T t1454 o1299 b1302 b1335 b1454 b4
3691 B b1455 t1454
3692 T t1455 o1298 b1455
3693 B b1456 t1455
3694 P p1456 Number 12867
3695 P p1457 Number 14174
3696 O o1457 location p1456 p1457
3697 P p1458 String cancel2
3698 O o1458 rule p1458
3699 H h1458 x t793
3700 S s1458 t679 h h1458 h1304
3701 G s1458 t715
3702 B b1458 s1458
3703 T t1458 o677 b1458
3704 B b1459 t1458
3705 S s1459 t679 h h1458 h1304
3706 G s1459 t718
3707 B b1460 s1459
3708 T t1460 o677 b1460
3709 B b1461 t1460
3710 S s1461 t679 h h1458 h1304
3711 G s1461 t757
3712 B b1462 s1461
3713 T t1462 o677 b1462
3714 B b1463 t1462
3715 S s1463 t679 h h1458 h1304
3716 G s1463 t760
3717 B b1464 s1463
3718 T t1464 o677 b1464
3719 B b1465 t1464
3720 S s1465 t679 h h1458 h1304
3721 G s1465 t681
3722 B b1466 s1465
3723 T t1466 o677 b1466
3724 B b1467 t1466
3725 S s1467 t684 h h1458 h1304
3726 G s1467 t586
3727 B b1468 s1467
3728 T t1468 o677 b1468
3729 B b1469 t1468
3730 S s1469 t684 h h1458 h1304
3731 G s1469 t762
3732 B b1470 s1469
3733 T t1470 o677 b1470
3734 B b1471 t1470
3735 S s1471 t684 h h1458 h1304
3736 G s1471 t736
3737 B b1472 s1471
3738 T t1472 o677 b1472
3739 B b1473 t1472
3740 S s1473 t684 h h1458 h1304
3741 G s1473 t738
3742 B b1474 s1473
3743 T t1474 o677 b1474
3744 B b1475 t1474
3745 S s1475 t684 h h1458 h1304
3746 G s1475 t764
3747 B b1476 s1475
3748 T t1476 o677 b1476
3749 B b1477 t1476
3750 S s1477 t684 h h1458 h1304
3751 G s1477 t766
3752 B b1478 s1477
3753 T t1478 o677 b1478
3754 B b1479 t1478
3755 T t1479 o676 b1477 b1479
3756 B b1480 t1479
3757 T t1480 o676 b1475 b1480
3758 B b1481 t1480
3759 T t1481 o676 b1473 b1481
3760 B b1482 t1481
3761 T t1482 o676 b1471 b1482
3762 B b1483 t1482
3763 T t1483 o676 b1469 b1483
3764 B b1484 t1483
3765 T t1484 o676 b1467 b1484
3766 B b1485 t1484
3767 T t1485 o676 b1465 b1485
3768 B b1486 t1485
3769 T t1486 o676 b1463 b1486
3770 B b1487 t1486
3771 T t1487 o676 b1461 b1487
3772 B b1488 t1487
3773 T t1488 o676 b1459 b1488
3774 B b1489 t1488
3775 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"
3776 O o1489 ext_rule p1489
3777 T t1489 o b1476 b4
3778 B b1490 t1489
3779 T t1490 o b1474 b1490
3780 B b1491 t1490
3781 T t1491 o b1472 b1491
3782 B b1492 t1491
3783 T t1492 o b1470 b1492
3784 B b1493 t1492
3785 T t1493 o b1468 b1493
3786 B b1494 t1493
3787 T t1494 o b1466 b1494
3788 B b1495 t1494
3789 T t1495 o b1464 b1495
3790 B b1496 t1495
3791 T t1496 o b1462 b1496
3792 B b1497 t1496
3793 T t1497 o b1460 b1497
3794 B b1498 t1497
3795 T t1498 o b1458 b1498
3796 B b1499 t1498
3797 T t1499 o1095 b1478 b1499
3798 B b1500 t1499
3799 T t1500 o1094 b1500 b4 b1104
3800 B b1501 t1500
3801 T t1501 o609 b585 b756
3802 B b1502 t1501
3803 T t1502 o596 b585 b791 b1502
3804 B b1503 t1502
3805 T t1503 o596 b585 b792 b1502
3806 B b1504 t1503
3807 T t1504 o761 b591 b759 b1503 b1504
3808 H h1504 v t1504
3809 S s1504 t684 h h1458 h1304 h1504
3810 G s1504 t766
3811 B b1505 s1504
3812 T t1505 o1095 b1505 b1499
3813 B b1506 t1505
3814 T t1506 o2 b1501
3815 B b1507 t1506
3816 T t1507 o1094 b1506 b4 b1507
3817 B b1508 t1507
3818 T t1508 o b1508 b4
3819 B b1509 t1508
3820 T t1509 o1093 b1501 b1509
3821 B b1510 t1509
3822 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"
3823 O o1510 ext_rule p1510
3824 T t1510 o596 b585 b756 b1502
3825 B b1511 t1510
3826 T t1511 o596 b585 b714 b1511
3827 B b1512 t1511
3828 T t1512 o761 b591 b759 b1512 b1504
3829 H h1512 z t1512
3830 S s1512 t684 h h1458 h1304 h1504 h1512
3831 G s1512 t766
3832 B b1513 s1512
3833 T t1513 o1095 b1513 b1499
3834 B b1514 t1513
3835 T t1514 o2 b1508
3836 B b1515 t1514
3837 T t1515 o1094 b1514 b4 b1515
3838 B b1516 t1515
3839 T t1516 o b1516 b4
3840 B b1517 t1516
3841 T t1517 o1093 b1508 b1517
3842 B b1518 t1517
3843 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"
3844 O o1518 ext_rule p1518
3845 T t1518 o596 b585 b717 b1511
3846 B b1519 t1518
3847 T t1519 o761 b591 b759 b1512 b1519
3848 H h1519 z_1 t1519
3849 S s1519 t684 h h1458 h1304 h1504 h1512 h1519
3850 G s1519 t766
3851 B b1520 s1519
3852 T t1520 o1095 b1520 b1499
3853 B b1521 t1520
3854 T t1521 o2 b1516
3855 B b1522 t1521
3856 T t1522 o1094 b1521 b4 b1522
3857 B b1523 t1522
3858 T t1523 o b1523 b4
3859 B b1524 t1523
3860 T t1524 o1093 b1516 b1524
3861 B b1525 t1524
3862 P p1525 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 6 ttca"
3863 O o1525 ext_rule p1525
3864 T t1525 o596 b585 b714 b604
3865 B b1526 t1525
3866 T t1526 o596 b585 b717 b604
3867 B b1527 t1526
3868 T t1527 o761 b591 b759 b1526 b1527
3869 H h1527 z_2 t1527
3870 S s1527 t684 h h1458 h1304 h1504 h1512 h1519 h1527
3871 G s1527 t766
3872 B b1528 s1527
3873 T t1528 o1095 b1528 b1499
3874 B b1529 t1528
3875 T t1529 o2 b1523
3876 B b1530 t1529
3877 T t1530 o1094 b1529 b4 b1530
3878 B b1531 t1530
3879 T t1531 o b1531 b4
3880 B b1532 t1531
3881 T t1532 o1093 b1523 b1532
3882 B b1533 t1532
3883 P p1533 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's1; id{'g}}; 's1} >> 7 ttca"
3884 O o1533 ext_rule p1533
3885 T t1533 o761 b591 b759 b714 b1527
3886 H h1533 z_3 t1533
3887 S s1533 t684 h h1458 h1304 h1504 h1512 h1519 h1527 h1533
3888 G s1533 t766
3889 B b1534 s1533
3890 T t1534 o1095 b1534 b1499
3891 B b1535 t1534
3892 T t1535 o2 b1531
3893 B b1536 t1535
3894 T t1536 o1094 b1535 b4 b1536
3895 B b1537 t1536
3896 T t1537 o b1537 b4
3897 B b1538 t1537
3898 T t1538 o1093 b1531 b1538
3899 B b1539 t1538
3900 P p1539 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's2; id{'g}}; 's2} >> 8 ttca"
3901 O o1539 ext_rule p1539
3902 T t1539 o1093 b1537 b4
3903 B b1540 t1539
3904 T t1540 o1539 b1092 b1540 b4 b4
3905 B b1541 t1540
3906 T t1541 o b1541 b4
3907 B b1542 t1541
3908 T t1542 o1533 b1092 b1539 b1542 b4
3909 B b1543 t1542
3910 T t1543 o b1543 b4
3911 B b1544 t1543
3912 T t1544 o1525 b1092 b1533 b1544 b4
3913 B b1545 t1544
3914 T t1545 o b1545 b4
3915 B b1546 t1545
3916 T t1546 o1518 b1092 b1525 b1546 b4
3917 B b1547 t1546
3918 T t1547 o b1547 b4
3919 B b1548 t1547
3920 T t1548 o1510 b1092 b1518 b1548 b4
3921 B b1549 t1548
3922 T t1549 o b1549 b4
3923 B b1550 t1549
3924 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"
3925 O o1550 ext_rule p1550
3926 H h1550 v t793
3927 H h1551 v_1 t1504
3928 S s1551 t684 h h1550 h1551
3929 G s1551 t766
3930 B b1551 s1551
3931 T t1551 o b793 b4
3932 B b1552 t1551
3933 T t1552 o b764 b1552
3934 B b1553 t1552
3935 T t1553 o b738 b1553
3936 B b1554 t1553
3937 T t1554 o b736 b1554
3938 B b1555 t1554
3939 T t1555 o b762 b1555
3940 B b1556 t1555
3941 T t1556 o b699 b1556
3942 B b1557 t1556
3943 T t1557 o b681 b1557
3944 B b1558 t1557
3945 T t1558 o b760 b1558
3946 B b1559 t1558
3947 T t1559 o b757 b1559
3948 B b1560 t1559
3949 T t1560 o b718 b1560
3950 B b1561 t1560
3951 T t1561 o b715 b1561
3952 B b1562 t1561
3953 T t1562 o1095 b1551 b1562
3954 B b1563 t1562
3955 S s1563 t684 h h1550
3956 G s1563 t766
3957 B b1564 s1563
3958 T t1564 o1095 b1564 b1562
3959 B b1565 t1564
3960 T t1565 o1095 b766 b1562
3961 B b1566 t1565
3962 T t1566 o1094 b1566 b4 b1104
3963 B b1567 t1566
3964 T t1567 o2 b1567
3965 B b1568 t1567
3966 T t1568 o1094 b1565 b4 b1568
3967 B b1569 t1568
3968 T t1569 o2 b1569
3969 B b1570 t1569
3970 T t1570 o1094 b1563 b4 b1570
3971 B b1571 t1570
3972 S s1571 t684 h h1550 h1551 h1512
3973 G s1571 t766
3974 B b1572 s1571
3975 T t1572 o1095 b1572 b1562
3976 B b1573 t1572
3977 T t1573 o2 b1571
3978 B b1574 t1573
3979 T t1574 o1094 b1573 b4 b1574
3980 B b1575 t1574
3981 T t1575 o b1575 b4
3982 B b1576 t1575
3983 T t1576 o1093 b1571 b1576
3984 B b1577 t1576
3985 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"
3986 O o1577 ext_rule p1577
3987 S s1577 t684 h h1550 h1551 h1512 h1519
3988 G s1577 t766
3989 B b1578 s1577
3990 T t1578 o1095 b1578 b1562
3991 B b1579 t1578
3992 T t1579 o2 b1575
3993 B b1580 t1579
3994 T t1580 o1094 b1579 b4 b1580
3995 B b1581 t1580
3996 T t1581 o b1581 b4
3997 B b1582 t1581
3998 T t1582 o1093 b1575 b1582
3999 B b1583 t1582
4000 P p1583 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 5 ttca"
4001 O o1583 ext_rule p1583
4002 S s1583 t684 h h1550 h1551 h1512 h1519 h1527
4003 G s1583 t766
4004 B b1584 s1583
4005 T t1584 o1095 b1584 b1562
4006 B b1585 t1584
4007 T t1585 o2 b1581
4008 B b1586 t1585
4009 T t1586 o1094 b1585 b4 b1586
4010 B b1587 t1586
4011 T t1587 o b1587 b4
4012 B b1588 t1587
4013 T t1588 o1093 b1581 b1588
4014 B b1589 t1588
4015 P p1589 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's1; id{'g}}; 's1} >> 6 ttca"
4016 O o1589 ext_rule p1589
4017 S s1589 t684 h h1550 h1551 h1512 h1519 h1527 h1533
4018 G s1589 t766
4019 B b1590 s1589
4020 T t1590 o1095 b1590 b1562
4021 B b1591 t1590
4022 T t1591 o2 b1587
4023 B b1592 t1591
4024 T t1592 o1094 b1591 b4 b1592
4025 B b1593 t1592
4026 T t1593 o b1593 b4
4027 B b1594 t1593
4028 T t1594 o1093 b1587 b1594
4029 B b1595 t1594
4030 P p1595 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's2; id{'g}}; 's2} >> 7 ttca"
4031 O o1595 ext_rule p1595
4032 T t1595 o1093 b1593 b4
4033 B b1596 t1595
4034 T t1596 o1595 b1092 b1596 b4 b4
4035 B b1597 t1596
4036 T t1597 o b1597 b4
4037 B b1598 t1597
4038 T t1598 o1589 b1092 b1595 b1598 b4
4039 B b1599 t1598
4040 T t1599 o b1599 b4
4041 B b1600 t1599
4042 T t1600 o1583 b1092 b1589 b1600 b4
4043 B b1601 t1600
4044 T t1601 o b1601 b4
4045 B b1602 t1601
4046 T t1602 o1577 b1092 b1583 b1602 b4
4047 B b1603 t1602
4048 T t1603 o b1603 b4
4049 B b1604 t1603
4050 T t1604 o1550 b1092 b1577 b1604 b4
4051 B b1605 t1604
4052 T t1605 o b1605 b4
4053 B b1606 t1605
4054 T t1606 o1489 b1092 b1510 b1550 b1606
4055 B b1607 t1606
4056 T t1607 o1090 b1607
4057 B b1608 t1607
4058 T t1608 o1458 b1302 b1489 b1608 b4
4059 B b1609 t1608
4060 T t1609 o1457 b1609
4061 B b1610 t1609
4062 P p1610 Number 14176
4063 P p1611 Number 14263
4064 O o1611 location p1610 p1611
4065 NOcaml!str_let str_let str_let Ocaml
4066 O o1612 str_let p1610 p1611
4067 NOcaml!patt_var patt_var patt_var Ocaml
4068 P p1612 Number 14180
4069 O o1613 patt_var p1612 p1611
4070 NOcaml!patt_done patt_done patt_done Ocaml
4071 O o1614 patt_done p1610 p1611
4072 T t1614 o1614
4073 B b1614 t1614 groupCancelLeftT
4074 T t1615 o1613 b1614
4075 B b1615 t1615
4076 NOcaml!fun fun fun Ocaml
4077 O o1615 fun p1612 p1611
4078 NOcaml!patt_if patt_if patt_if Ocaml
4079 O o1616 patt_if p1612 p1611
4080 P p1616 Number 14197
4081 P p1617 Number 14198
4082 O o1617 patt_var p1616 p1617
4083 NOcaml!patt_body patt_body patt_body Ocaml
4084 O o1618 patt_body p1612 p1611
4085 P p1618 Number 14199
4086 P p1619 Number 14200
4087 O o1619 patt_var p1618 p1619
4088 NOcaml!let let let Ocaml
4089 P p1620 Number 14206
4090 O o1620 let p1620 p1611
4091 NOcaml!patt_tuple patt_tuple patt_tuple Ocaml
4092 P p1621 Number 14210
4093 P p1622 Number 14214
4094 O o1622 patt_tuple p1621 p1622
4095 P p1623 Number 14211
4096 O o1623 patt_var p1621 p1623
4097 NOcaml!patt_tuple_arg patt_tuple_arg patt_tuple_arg Ocaml
4098 O o1624 patt_tuple_arg p1621 p1622
4099 P p1624 Number 14213
4100 O o1625 patt_var p1624 p1622
4101 NOcaml!patt_tuple_end patt_tuple_end patt_tuple_end Ocaml
4102 O o1626 patt_tuple_end p1621 p1622
4103 NOcaml!patt_in patt_in patt_in Ocaml
4104 O o1627 patt_in p1620 p1611
4105 NOcaml!apply apply apply Ocaml
4106 P p1627 Number 14250
4107 O o1628 apply p1627 p1611
4108 P p1628 Number 14261
4109 O o1629 apply p1627 p1628
4110 P p1629 Number 14259
4111 O o1630 apply p1627 p1629
4112 NOcaml!lid lid lid Ocaml
4113 P p1630 Number 14257
4114 O o1631 lid p1627 p1630
4115 O o1632 lid p1299
4116 T t1632 o1632
4117 B b1632 t1632
4118 T t1633 o1631 b1632
4119 B b1633 t1633
4120 P p1633 Number 14258
4121 O o1633 lid p1633 p1629
4122 P p1634 Var j
4123 O o1634 var p1634
4124 T t1634 o1634
4125 B b1634 t1634
4126 T t1635 o1633 b1634
4127 B b1635 t1635
4128 T t1636 o1630 b1633 b1635
4129 B b1636 t1636
4130 P p1636 Number 14260
4131 O o1636 lid p1636 p1628
4132 P p1637 Var k
4133 O o1637 var p1637
4134 T t1637 o1637
4135 B b1637 t1637
4136 T t1638 o1636 b1637
4137 B b1638 t1638
4138 T t1639 o1629 b1636 b1638
4139 B b1639 t1639
4140 P p1639 Number 14262
4141 O o1639 lid p1639 p1611
4142 P p1640 Var p
4143 O o1640 var p1640
4144 T t1640 o1640
4145 B b1640 t1640
4146 T t1641 o1639 b1640
4147 B b1641 t1641
4148 T t1642 o1628 b1639 b1641
4149 B b1642 t1642
4150 T t1643 o1627 b1642
4151 B b1643 t1643
4152 T t1644 o1626 b1643
4153 B b1644 t1644 k
4154 T t1645 o1625 b1644
4155 B b1645 t1645
4156 T t1646 o1624 b1645
4157 B b1646 t1646 j
4158 T t1647 o1623 b1646
4159 B b1647 t1647
4160 T t1648 o1622 b1647
4161 B b1648 t1648
4162 P p1648 Number 14217
4163 P p1649 Number 14240
4164 O o1649 apply p1648 p1649
4165 P p1650 Number 14238
4166 O o1650 apply p1648 p1650
4167 NOcaml!proj proj proj Ocaml
4168 P p1651 Number 14236
4169 O o1651 proj p1648 p1651
4170 O o1652 uid p1648 p1651
4171 O o1653 uid p539
4172 T t1653 o1653
4173 B b1653 t1653
4174 T t1654 o1652 b1653
4175 B b1654 t1654
4176 P p1654 Number 14225
4177 O o1654 lid p1654 p1651
4178 P p1655 String hyp_indices
4179 O o1655 lid p1655
4180 T t1655 o1655
4181 B b1655 t1655
4182 T t1656 o1654 b1655
4183 B b1656 t1656
4184 T t1657 o1651 b1654 b1656
4185 B b1657 t1657
4186 P p1657 Number 14237
4187 O o1657 lid p1657 p1650
4188 T t1658 o1657 b1640
4189 B b1658 t1658
4190 T t1659 o1650 b1657 b1658
4191 B b1659 t1659
4192 P p1659 Number 14239
4193 O o1659 lid p1659 p1649
4194 P p1660 Var i
4195 O o1660 var p1660
4196 T t1660 o1660
4197 B b1660 t1660
4198 T t1661 o1659 b1660
4199 B b1661 t1661
4200 T t1662 o1649 b1659 b1661
4201 B b1662 t1662
4202 T t1663 o b1662 b4
4203 B b1663 t1663
4204 T t1664 o1620 b1648 b1663
4205 B b1664 t1664
4206 T t1665 o1618 b1664
4207 B b1665 t1665 p
4208 T t1666 o1619 b1665
4209 B b1666 t1666
4210 T t1667 o1616 b1666
4211 B b1667 t1667
4212 T t1668 o1615 b1667
4213 B b1668 t1668
4214 T t1669 o1618 b1668
4215 B b1669 t1669 i
4216 T t1670 o1617 b1669
4217 B b1670 t1670
4218 T t1671 o1616 b1670
4219 B b1671 t1671
4220 T t1672 o1615 b1671
4221 B b1672 t1672
4222 T t1673 o1612 b1615 b1672
4223 B b1673 t1673
4224 T t1674 o b1673 b4
4225 B b1674 t1674
4226 T t1675 o1612 b1674
4227 B b1675 t1675
4228 T t1676 o422 b1675
4229 B b1676 t1676
4230 T t1677 o1611 b1676
4231 B b1677 t1677
4232 P p1677 Number 14265
4233 P p1678 Number 14353
4234 O o1678 location p1677 p1678
4235 O o1679 str_let p1677 p1678
4236 P p1679 Number 14269
4237 O o1680 patt_var p1679 p1678
4238 O o1681 patt_done p1677 p1678
4239 T t1681 o1681
4240 B b1681 t1681 groupCancelRightT
4241 T t1682 o1680 b1681
4242 B b1682 t1682
4243 O o1682 fun p1679 p1678
4244 O o1683 patt_if p1679 p1678
4245 P p1683 Number 14287
4246 P p1684 Number 14288
4247 O o1684 patt_var p1683 p1684
4248 O o1685 patt_body p1679 p1678
4249 P p1685 Number 14289
4250 P p1686 Number 14290
4251 O o1686 patt_var p1685 p1686
4252 P p1687 Number 14296
4253 O o1687 let p1687 p1678
4254 P p1688 Number 14300
4255 P p1689 Number 14304
4256 O o1689 patt_tuple p1688 p1689
4257 P p1690 Number 14301
4258 O o1690 patt_var p1688 p1690
4259 O o1691 patt_tuple_arg p1688 p1689
4260 P p1691 Number 14303
4261 O o1692 patt_var p1691 p1689
4262 O o1693 patt_tuple_end p1688 p1689
4263 O o1694 patt_in p1687 p1678
4264 P p1694 Number 14340
4265 O o1695 apply p1694 p1678
4266 P p1695 Number 14351
4267 O o1696 apply p1694 p1695
4268 P p1696 Number 14349
4269 O o1697 apply p1694 p1696
4270 P p1697 Number 14347
4271 O o1698 lid p1694 p1697
4272 O o1699 lid p1458
4273 T t1699 o1699
4274 B b1699 t1699
4275 T t1700 o1698 b1699
4276 B b1700 t1700
4277 P p1700 Number 14348
4278 O o1700 lid p1700 p1696
4279 T t1701 o1700 b1634
4280 B b1701 t1701
4281 T t1702 o1697 b1700 b1701
4282 B b1702 t1702
4283 P p1702 Number 14350
4284 O o1702 lid p1702 p1695
4285 T t1703 o1702 b1637
4286 B b1703 t1703
4287 T t1704 o1696 b1702 b1703
4288 B b1704 t1704
4289 P p1704 Number 14352
4290 O o1704 lid p1704 p1678
4291 T t1705 o1704 b1640
4292 B b1705 t1705
4293 T t1706 o1695 b1704 b1705
4294 B b1706 t1706
4295 T t1707 o1694 b1706
4296 B b1707 t1707
4297 T t1708 o1693 b1707
4298 B b1708 t1708 k
4299 T t1709 o1692 b1708
4300 B b1709 t1709
4301 T t1710 o1691 b1709
4302 B b1710 t1710 j
4303 T t1711 o1690 b1710
4304 B b1711 t1711
4305 T t1712 o1689 b1711
4306 B b1712 t1712
4307 P p1712 Number 14307
4308 P p1713 Number 14330
4309 O o1713 apply p1712 p1713
4310 P p1714 Number 14328
4311 O o1714 apply p1712 p1714
4312 P p1715 Number 14326
4313 O o1715 proj p1712 p1715
4314 O o1716 uid p1712 p1715
4315 T t1716 o1716 b1653
4316 B b1716 t1716
4317 P p1716 Number 14315
4318 O o1717 lid p1716 p1715
4319 T t1717 o1717 b1655
4320 B b1717 t1717
4321 T t1718 o1715 b1716 b1717
4322 B b1718 t1718
4323 P p1718 Number 14327
4324 O o1718 lid p1718 p1714
4325 T t1719 o1718 b1640
4326 B b1719 t1719
4327 T t1720 o1714 b1718 b1719
4328 B b1720 t1720
4329 P p1720 Number 14329
4330 O o1720 lid p1720 p1713
4331 T t1721 o1720 b1660
4332 B b1721 t1721
4333 T t1722 o1713 b1720 b1721
4334 B b1722 t1722
4335 T t1723 o b1722 b4
4336 B b1723 t1723
4337 T t1724 o1687 b1712 b1723
4338 B b1724 t1724
4339 T t1725 o1685 b1724
4340 B b1725 t1725 p
4341 T t1726 o1686 b1725
4342 B b1726 t1726
4343 T t1727 o1683 b1726
4344 B b1727 t1727
4345 T t1728 o1682 b1727
4346 B b1728 t1728
4347 T t1729 o1685 b1728
4348 B b1729 t1729 i
4349 T t1730 o1684 b1729
4350 B b1730 t1730
4351 T t1731 o1683 b1730
4352 B b1731 t1731
4353 T t1732 o1682 b1731
4354 B b1732 t1732
4355 T t1733 o1679 b1682 b1732
4356 B b1733 t1733
4357 T t1734 o b1733 b4
4358 B b1734 t1734
4359 T t1735 o1679 b1734
4360 B b1735 t1735
4361 T t1736 o422 b1735
4362 B b1736 t1736
4363 T t1737 o1678 b1736
4364 B b1737 t1737
4365 P p1737 Number 14371
4366 P p1738 Number 14843
4367 O o1738 location p1737 p1738
4368 P p1739 String unique_id1
4369 O o1739 rule p1739
4370 P p1740 Var e2
4371 O o1740 var p1740
4372 T t1740 o1740
4373 B b1740 t1740
4374 T t1741 o700 b1740
4375 S s1741 t679 h
4376 G s1741 t1741
4377 B b1741 s1741
4378 T t1742 o677 b1741
4379 B b1742 t1742
4380 T t1743 o736 b1740 b591
4381 S s1743 t684 h
4382 G s1743 t1743
4383 B b1743 s1743
4384 T t1744 o677 b1743
4385 B b1744 t1744
4386 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4387 NCzf_itt_dall!dall dall dall Czf_itt_dall
4388 O o1744 dall
4389 T t1745 o596 b585 b1740 b815
4390 B b1745 t1745
4391 T t1746 o761 b591 b759 b1745 b815
4392 B b1746 t1746 s
4393 T t1747 o1744 b591 b1746
4394 S s1747 t684 h
4395 G s1747 t1747
4396 B b1747 s1747
4397 T t1748 o677 b1747
4398 B b1748 t1748
4399 T t1749 o761 b591 b759 b1740 b604
4400 S s1749 t684 h
4401 G s1749 t1749
4402 B b1749 s1749
4403 T t1750 o677 b1749
4404 B b1750 t1750
4405 T t1751 o676 b1748 b1750
4406 B b1751 t1751
4407 T t1752 o676 b1744 b1751
4408 B b1752 t1752
4409 T t1753 o676 b763 b1752
4410 B b1753 t1753
4411 T t1754 o676 b700 b1753
4412 B b1754 t1754
4413 T t1755 o676 b682 b1754
4414 B b1755 t1755
4415 T t1756 o676 b761 b1755
4416 B b1756 t1756
4417 T t1757 o676 b1742 b1756
4418 B b1757 t1757
4419 P p1757 String "assumT 7 thenT withT << id{'g} >> (dT 2) ttca"
4420 O o1757 ext_rule p1757
4421 T t1758 o b1747 b4
4422 B b1758 t1758
4423 T t1759 o b1743 b1758
4424 B b1759 t1759
4425 T t1760 o b762 b1759
4426 B b1760 t1760
4427 T t1761 o b699 b1760
4428 B b1761 t1761
4429 T t1762 o b681 b1761
4430 B b1762 t1762
4431 T t1763 o b760 b1762
4432 B b1763 t1763
4433 T t1764 o b1741 b1763
4434 B b1764 t1764
4435 T t1765 o1095 b1749 b1764
4436 B b1765 t1765
4437 T t1766 o1094 b1765 b4 b1104
4438 B b1766 t1766
4439 P p1766 String wf
4440 O o1766 tactic_arg p1766
4441 H h1766 v t1747
4442 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
4443 O o1767 fun_prop
4444 P p1767 Var w
4445 O o1768 var p1767
4446 T t1768 o1768
4447 B b1768 t1768
4448 T t1769 o596 b585 b1740 b1768
4449 B b1769 t1769
4450 T t1770 o761 b591 b759 b1769 b1768
4451 B b1770 t1770 w
4452 T t1771 o1767 b1770
4453 S s1771 t684 h h1766
4454 G s1771 t1771
4455 B b1771 s1771
4456 T t1772 o1095 b1771 b1764
4457 B b1772 t1772
4458 S s1772 t684 h h1766
4459 G s1772 t1749
4460 B b1773 s1772
4461 T t1773 o1095 b1773 b1764
4462 B b1774 t1773
4463 NSummary!arg_named arg_named arg_named Summary
4464 P p1774 String with
4465 O o1774 arg_named p1774
4466 NSummary!arg_term_list arg_term_list arg_term_list Summary
4467 O o1775 arg_term_list
4468 T t1775 o b604 b4
4469 B b1775 t1775
4470 T t1776 o1775 b1775
4471 B b1776 t1776
4472 T t1777 o1774 b1776
4473 B b1777 t1777
4474 T t1778 o b1777 b4
4475 B b1778 t1778
4476 T t1779 o2 b1766
4477 B b1779 t1779
4478 T t1780 o1094 b1774 b1778 b1779
4479 B b1780 t1780
4480 T t1781 o2 b1780
4481 B b1781 t1781
4482 T t1782 o1766 b1772 b4 b1781
4483 B b1782 t1782
4484 T t1783 o596 b585 b1740 b604
4485 B b1783 t1783
4486 T t1784 o761 b591 b759 b1783 b604
4487 H h1784 w t1784
4488 S s1784 t684 h h1766 h1784
4489 G s1784 t1749
4490 B b1784 s1784
4491 T t1785 o1095 b1784 b1764
4492 B b1785 t1785
4493 T t1786 o1094 b1785 b4 b1781
4494 B b1786 t1786
4495 T t1787 o b1786 b4
4496 B b1787 t1787
4497 T t1788 o b1782 b1787
4498 B b1788 t1788
4499 T t1789 o1093 b1766 b1788
4500 B b1789 t1789
4501 P p1789 String "rwh unfold_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
4502 O o1789 ext_rule p1789
4503 H h1789 s1 t1106
4504 H h1790 s2 t1106
4505 NCzf_itt_eq!equal equal1790 equal Czf_itt_eq
4506 O o1790 equal1790
4507 T t1790 o1790 b714 b717
4508 H h1791 x t1790
4509 T t1791 o596 b585 b1740 b714
4510 B b1791 t1791
4511 T t1792 o761 b591 b759 b1791 b714
4512 H h1792 x_1 t1792
4513 T t1793 o596 b585 b1740 b717
4514 B b1793 t1793
4515 T t1794 o761 b591 b759 b1793 b717
4516 S s1794 t684 h h1766 h1789 h1790 h1791 h1792
4517 G s1794 t1794
4518 B b1794 s1794
4519 T t1795 o1095 b1794 b1764
4520 B b1795 t1795
4521 B b1796 t1792
4522 B b1797 t1794
4523 T t1797 o1117 b1796 b1797
4524 S s1797 t684 h h1766 h1789 h1790 h1791
4525 G s1797 t1797
4526 B b1798 s1797
4527 T t1798 o1095 b1798 b1764
4528 B b1799 t1798
4529 B b1800 t1790
4530 B b1801 t1797
4531 T t1801 o1117 b1800 b1801
4532 S s1801 t684 h h1766 h1789 h1790
4533 G s1801 t1801
4534 B b1802 s1801
4535 T t1802 o1095 b1802 b1764
4536 B b1803 t1802
4537 B b1804 t1801 s2
4538 T t1804 o1129 b1130 b1804
4539 S s1804 t684 h h1766 h1789
4540 G s1804 t1804
4541 B b1805 s1804
4542 T t1805 o1095 b1805 b1764
4543 B b1806 t1805
4544 B b1807 t1804 s1
4545 T t1807 o1129 b1130 b1807
4546 S s1807 t684 h h1766
4547 G s1807 t1807
4548 B b1808 s1807
4549 T t1808 o1095 b1808 b1764
4550 B b1809 t1808
4551 T t1809 o2 b1782
4552 B b1810 t1809
4553 T t1810 o1766 b1809 b4 b1810
4554 B b1811 t1810
4555 T t1811 o2 b1811
4556 B b1812 t1811
4557 T t1812 o1094 b1806 b4 b1812
4558 B b1813 t1812
4559 T t1813 o2 b1813
4560 B b1814 t1813
4561 T t1814 o1094 b1803 b4 b1814
4562 B b1815 t1814
4563 T t1815 o2 b1815
4564 B b1816 t1815
4565 T t1816 o1094 b1799 b4 b1816
4566 B b1817 t1816
4567 T t1817 o2 b1817
4568 B b1818 t1817
4569 T t1818 o1094 b1795 b4 b1818
4570 B b1819 t1818
4571 T t1819 o b1819 b4
4572 B b1820 t1819
4573 T t1820 o1093 b1782 b1820
4574 B b1821 t1820
4575 P p1821 String "equivTransT << op{'g; 'e2; 's2} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
4576 O o1821 ext_rule p1821
4577 T t1821 o700 b1791
4578 B b1822 t1821
4579 B b1823 t715
4580 T t1823 o1151 b1822 b1823
4581 B b1824 t1823
4582 T t1824 o1151 b1152 b1824
4583 B b1825 t1824
4584 T t1825 o1151 b1151 b1825
4585 B b1826 t1825
4586 T t1826 o736 b1791 b591
4587 B b1827 t1826
4588 B b1828 t736
4589 T t1828 o1151 b1827 b1828
4590 B b1829 t1828
4591 T t1829 o1151 b1826 b1829
4592 B b1830 t1829
4593 T t1830 o1161 b1791 b714
4594 B b1831 t1830
4595 T t1831 o736 b1831 b759
4596 B b1832 t1831
4597 T t1832 o1151 b1830 b1832
4598 H h1832 x_1 t1832
4599 T t1833 o736 b1793 b591
4600 S s1833 t684 h h1766 h1789 h1790 h1791 h1832
4601 G s1833 t1833
4602 B b1833 s1833
4603 T t1834 o1095 b1833 b1764
4604 B b1834 t1834
4605 S s1834 t684 h h1766 h1789 h1790 h1791 h1792
4606 G s1834 t1833
4607 B b1835 s1834
4608 T t1835 o1095 b1835 b1764
4609 B b1836 t1835
4610 T t1836 o2 b1819
4611 B b1837 t1836
4612 T t1837 o1094 b1836 b4 b1837
4613 B b1838 t1837
4614 T t1838 o2 b1838
4615 B b1839 t1838
4616 T t1839 o1094 b1834 b4 b1839
4617 B b1840 t1839
4618 T t1840 o761 b591 b759 b1791 b1793
4619 H h1840 u t1840
4620 T t1841 o761 b591 b759 b1793 b714
4621 H h1841 v_1 t1841
4622 S s1841 t684 h h1766 h1789 h1790 h1791 h1832 h1840 h1841
4623 G s1841 t1794
4624 B b1841 s1841
4625 T t1842 o1095 b1841 b1764
4626 B b1842 t1842
4627 S s1842 t684 h h1766 h1789 h1790 h1791 h1792 h1840 h1841
4628 G s1842 t1794
4629 B b1843 s1842
4630 T t1843 o1095 b1843 b1764
4631 B b1844 t1843
4632 T t1844 o1094 b1844 b4 b1837
4633 B b1845 t1844
4634 T t1845 o2 b1845
4635 B b1846 t1845
4636 T t1846 o1094 b1842 b4 b1846
4637 B b1847 t1846
4638 T t1847 o b1847 b4
4639 B b1848 t1847
4640 T t1848 o b1840 b1848
4641 B b1849 t1848
4642 T t1849 o1093 b1819 b1849
4643 B b1850 t1849
4644 P p1850 String "autoT thenT setSubstT << equal{'s1; 's2} >> 11 ttca"
4645 O o1850 ext_rule p1850
4646 T t1850 o1093 b1840 b4
4647 B b1851 t1850
4648 T t1851 o1850 b1092 b1851 b4 b4
4649 B b1852 t1851
4650 P p1852 String "equivTransT << 's2 >> 8 thenT autoT"
4651 O o1852 ext_rule p1852
4652 H h1852 y_2 t700
4653 H h1853 y_1 t760
4654 H h1854 y_3 t1821
4655 H h1855 z_1 t715
4656 H h1856 y t1826
4657 H h1857 z_2 t736
4658 H h1858 z t1831
4659 S s1858 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1854 h1855 h1856 h1857 h1858 h1840 h1841
4660 G s1858 t738
4661 B b1858 s1858
4662 T t1858 o1095 b1858 b1764
4663 B b1859 t1858
4664 S s1859 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1854 h1855 h1856 h1857 h1858 h1840 h1841
4665 G s1859 t1833
4666 B b1860 s1859
4667 T t1860 o1095 b1860 b1764
4668 B b1861 t1860
4669 P p1861 String d_auto
4670 O o1861 arg_named p1861
4671 NSummary!arg_bool arg_bool arg_bool Summary
4672 P p1862 String true
4673 O o1862 arg_bool p1862
4674 T t1862 o1862
4675 B b1862 t1862
4676 T t1863 o1861 b1862
4677 B b1863 t1863
4678 T t1864 o b1863 b4
4679 B b1864 t1864
4680 H h1864 z_3 t1823
4681 S s1864 t684 h h1766 h1789 h1790 h1791 h1852 h1853 h1864 h1856 h1857 h1858 h1840 h1841
4682 G s1864 t1833
4683 B b1865 s1864
4684 T t1865 o1095 b1865 b1764
4685 B b1866 t1865
4686 H h1866 z_1 t1824
4687 S s1866 t684 h h1766 h1789 h1790 h1791 h1852 h1866 h1856 h1857 h1858 h1840 h1841
4688 G s1866 t1833
4689 B b1867 s1866
4690 T t1867 o1095 b1867 b1764
4691 B b1868 t1867
4692 H h1868 y_1 t1825
4693 S s1868 t684 h h1766 h1789 h1790 h1791 h1868 h1856 h1857 h1858 h1840 h1841
4694 G s1868 t1833
4695 B b1869 s1868
4696 T t1869 o1095 b1869 b1764
4697 B b1870 t1869
4698 H h1870 z_1 t1828
4699 S s1870 t684 h h1766 h1789 h1790 h1791 h1868 h1870 h1858 h1840 h1841
4700 G s1870 t1833
4701 B b1871 s1870
4702 T t1871 o1095 b1871 b1764
4703 B b1872 t1871
4704 H h1872 y t1829
4705 S s1872 t684 h h1766 h1789 h1790 h1791 h1872 h1858 h1840 h1841
4706 G s1872 t1833
4707 B b1873 s1872
4708 T t1873 o1095 b1873 b1764
4709 B b1874 t1873
4710 S s1874 t684 h h1766 h1789 h1790 h1791 h1832 h1840 h1841
4711 G s1874 t1833
4712 B b1875 s1874
4713 T t1875 o1095 b1875 b1764
4714 B b1876 t1875
4715 T t1876 o2 b1847
4716 B b1877 t1876
4717 T t1877 o1094 b1876 b4 b1877
4718 B b1878 t1877
4719 T t1878 o2 b1878
4720 B b1879 t1878
4721 T t1879 o1094 b1874 b4 b1879
4722 B b1880 t1879
4723 T t1880 o2 b1880
4724 B b1881 t1880
4725 T t1881 o1094 b1872 b4 b1881
4726 B b1882 t1881
4727 T t1882 o2 b1882
4728 B b1883 t1882
4729 T t1883 o1094 b1870 b4 b1883
4730 B b1884 t1883
4731 T t1884 o2 b1884
4732 B b1885 t1884
4733 T t1885 o1094 b1868 b4 b1885
4734 B b1886 t1885
4735 T t1886 o2 b1886
4736 B b1887 t1886
4737 T t1887 o1094 b1866 b4 b1887
4738 B b1888 t1887
4739 T t1888 o2 b1888
4740 B b1889 t1888
4741 T t1889 o1094 b1861 b1864 b1889
4742 B b1890 t1889
4743 T t1890 o2 b1890
4744 B b1891 t1890
4745 T t1891 o1094 b1859 b4 b1891
4746 B b1892 t1891
4747 T t1892 o b1892 b4
4748 B b1893 t1892
4749 T t1893 o1093 b1847 b1893
4750 B b1894 t1893
4751 P p1894 String "setSubstT << equal{'s1; 's2} >> 11 ttca"
4752 O o1894 ext_rule p1894
4753 T t1894 o1093 b1892 b4
4754 B b1895 t1894
4755 T t1895 o1894 b1092 b1895 b4 b4
4756 B b1896 t1895
4757 T t1896 o b1896 b4
4758 B b1897 t1896
4759 T t1897 o1852 b1092 b1894 b1897 b4
4760 B b1898 t1897
4761 T t1898 o b1898 b4
4762 B b1899 t1898
4763 T t1899 o b1852 b1899
4764 B b1900 t1899
4765 T t1900 o1821 b1092 b1850 b1900 b4
4766 B b1901 t1900
4767 T t1901 o b1901 b4
4768 B b1902 t1901
4769 T t1902 o1789 b1092 b1821 b1902 b4
4770 B b1903 t1902
4771 P p1903 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'e2; id{'g}}; 'e2} >> 3 ttca"
4772 O o1903 ext_rule p1903
4773 T t1903 o1093 b1786 b4
4774 B b1904 t1903
4775 T t1904 o1903 b1092 b1904 b4 b4
4776 B b1905 t1904
4777 T t1905 o b1905 b4
4778 B b1906 t1905
4779 T t1906 o b1903 b1906
4780 B b1907 t1906
4781 T t1907 o1757 b1092 b1789 b1907 b4
4782 B b1908 t1907
4783 T t1908 o1090 b1908
4784 B b1909 t1908
4785 P p1909 Number 14397
4786 P p1910 Number 14405
4787 O o1910 resource_defs p1909 p1910 p204
4788 P p1911 Number 14403
4789 O o1911 uid p1911 p1910
4790 T t1911 o1911 b691
4791 B b1911 t1911
4792 T t1912 o b1911 b4
4793 B b1912 t1912
4794 T t1913 o1910 b1912
4795 B b1913 t1913
4796 T t1914 o b1913 b4
4797 B b1914 t1914
4798 T t1915 o1739 b676 b1757 b1909 b1914
4799 B b1915 t1915
4800 T t1916 o1738 b1915
4801 B b1916 t1916
4802 P p1916 Number 14845
4803 P p1917 Number 15317
4804 O o1917 location p1916 p1917
4805 P p1918 String unique_id2
4806 O o1918 rule p1918
4807 T t1918 o596 b585 b815 b1740
4808 B b1918 t1918
4809 T t1919 o761 b591 b759 b1918 b815
4810 B b1919 t1919 s
4811 T t1920 o1744 b591 b1919
4812 S s1920 t684 h
4813 G s1920 t1920
4814 B b1920 s1920
4815 T t1921 o677 b1920
4816 B b1921 t1921
4817 T t1922 o676 b1921 b1750
4818 B b1922 t1922
4819 T t1923 o676 b1744 b1922
4820 B b1923 t1923
4821 T t1924 o676 b763 b1923
4822 B b1924 t1924
4823 T t1925 o676 b700 b1924
4824 B b1925 t1925
4825 T t1926 o676 b682 b1925
4826 B b1926 t1926
4827 T t1927 o676 b761 b1926
4828 B b1927 t1927
4829 T t1928 o676 b1742 b1927
4830 B b1928 t1928
4831 T t1929 o b1920 b4
4832 B b1929 t1929
4833 T t1930 o b1743 b1929
4834 B b1930 t1930
4835 T t1931 o b762 b1930
4836 B b1931 t1931
4837 T t1932 o b699 b1931
4838 B b1932 t1932
4839 T t1933 o b681 b1932
4840 B b1933 t1933
4841 T t1934 o b760 b1933
4842 B b1934 t1934
4843 T t1935 o b1741 b1934
4844 B b1935 t1935
4845 T t1936 o1095 b1749 b1935
4846 B b1936 t1936
4847 T t1937 o1094 b1936 b4 b1104
4848 B b1937 t1937
4849 H h1937 v t1920
4850 T t1938 o596 b585 b1768 b1740
4851 B b1938 t1938
4852 T t1939 o761 b591 b759 b1938 b1768
4853 B b1939 t1939 w
4854 T t1940 o1767 b1939
4855 S s1940 t684 h h1937
4856 G s1940 t1940
4857 B b1940 s1940
4858 T t1941 o1095 b1940 b1935
4859 B b1941 t1941
4860 S s1941 t684 h h1937
4861 G s1941 t1749
4862 B b1942 s1941
4863 T t1942 o1095 b1942 b1935
4864 B b1943 t1942
4865 T t1943 o2 b1937
4866 B b1944 t1943
4867 T t1944 o1094 b1943 b1778 b1944
4868 B b1945 t1944
4869 T t1945 o2 b1945
4870 B b1946 t1945
4871 T t1946 o1766 b1941 b4 b1946
4872 B b1947 t1946
4873 T t1947 o596 b585 b604 b1740
4874 B b1948 t1947
4875 T t1948 o761 b591 b759 b1948 b604
4876 H h1948 w t1948
4877 S s1948 t684 h h1937 h1948
4878 G s1948 t1749
4879 B b1949 s1948
4880 T t1949 o1095 b1949 b1935
4881 B b1950 t1949
4882 T t1950 o1094 b1950 b4 b1946
4883 B b1951 t1950
4884 T t1951 o b1951 b4
4885 B b1952 t1951
4886 T t1952 o b1947 b1952
4887 B b1953 t1952
4888 T t1953 o1093 b1937 b1953
4889 B b1954 t1953
4890 P p1954 String "rwh unfold_fun_prop 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
4891 O o1954 ext_rule p1954
4892 T t1954 o596 b585 b714 b1740
4893 B b1955 t1954
4894 T t1955 o761 b591 b759 b1955 b714
4895 H h1955 x_1 t1955
4896 T t1956 o596 b585 b717 b1740
4897 B b1956 t1956
4898 T t1957 o761 b591 b759 b1956 b717
4899 S s1957 t684 h h1937 h1789 h1790 h1791 h1955
4900 G s1957 t1957
4901 B b1957 s1957
4902 T t1958 o1095 b1957 b1935
4903 B b1958 t1958
4904 B b1959 t1955
4905 B b1960 t1957
4906 T t1960 o1117 b1959 b1960
4907 S s1960 t684 h h1937 h1789 h1790 h1791
4908 G s1960 t1960
4909 B b1961 s1960
4910 T t1961 o1095 b1961 b1935
4911 B b1962 t1961
4912 B b1963 t1960
4913 T t1963 o1117 b1800 b1963
4914 S s1963 t684 h h1937 h1789 h1790
4915 G s1963 t1963
4916 B b1964 s1963
4917 T t1964 o1095 b1964 b1935
4918 B b1965 t1964
4919 B b1966 t1963 s2
4920 T t1966 o1129 b1130 b1966
4921 S s1966 t684 h h1937 h1789
4922 G s1966 t1966
4923 B b1967 s1966
4924 T t1967 o1095 b1967 b1935
4925 B b1968 t1967
4926 B b1969 t1966 s1
4927 T t1969 o1129 b1130 b1969
4928 S s1969 t684 h h1937
4929 G s1969 t1969
4930 B b1970 s1969
4931 T t1970 o1095 b1970 b1935
4932 B b1971 t1970
4933 T t1971 o2 b1947
4934 B b1972 t1971
4935 T t1972 o1766 b1971 b4 b1972
4936 B b1973 t1972
4937 T t1973 o2 b1973
4938 B b1974 t1973
4939 T t1974 o1094 b1968 b4 b1974
4940 B b1975 t1974
4941 T t1975 o2 b1975
4942 B b1976 t1975
4943 T t1976 o1094 b1965 b4 b1976
4944 B b1977 t1976
4945 T t1977 o2 b1977
4946 B b1978 t1977
4947 T t1978 o1094 b1962 b4 b1978
4948 B b1979 t1978
4949 T t1979 o2 b1979
4950 B b1980 t1979
4951 T t1980 o1094 b1958 b4 b1980
4952 B b1981 t1980
4953 T t1981 o b1981 b4
4954 B b1982 t1981
4955 T t1982 o1093 b1947 b1982
4956 B b1983 t1982
4957 P p1983 String "equivTransT << op{'g; 's2; 'e2} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
4958 O o1983 ext_rule p1983
4959 T t1983 o700 b1955
4960 B b1984 t1983
4961 T t1984 o1151 b1984 b1823
4962 B b1985 t1984
4963 T t1985 o1151 b1152 b1985
4964 B b1986 t1985
4965 T t1986 o1151 b1151 b1986
4966 B b1987 t1986
4967 T t1987 o736 b1955 b591
4968 B b1988 t1987
4969 T t1988 o1151 b1988 b1828
4970 B b1989 t1988
4971 T t1989 o1151 b1987 b1989
4972 B b1990 t1989
4973 T t1990 o1161 b1955 b714
4974 B b1991 t1990
4975 T t1991 o736 b1991 b759
4976 B b1992 t1991
4977 T t1992 o1151 b1990 b1992
4978 H h1992 x_1 t1992
4979 T t1993 o736 b1956 b591
4980 S s1993 t684 h h1937 h1789 h1790 h1791 h1992
4981 G s1993 t1993
4982 B b1993 s1993
4983 T t1994 o1095 b1993 b1935
4984 B b1994 t1994
4985 S s1994 t684 h h1937 h1789 h1790 h1791 h1955
4986 G s1994 t1993
4987 B b1995 s1994
4988 T t1995 o1095 b1995 b1935
4989 B b1996 t1995
4990 T t1996 o2 b1981
4991 B b1997 t1996
4992 T t1997 o1094 b1996 b4 b1997
4993 B b1998 t1997
4994 T t1998 o2 b1998
4995 B b1999 t1998
4996 T t1999 o1094 b1994 b4 b1999
4997 B b2000 t1999
4998 T t2000 o761 b591 b759 b1955 b1956
4999 H h2000 u t2000
5000 T t2001 o761 b591 b759 b1956 b714
5001 H h2001 v_1 t2001
5002 S s2001 t684 h h1937 h1789 h1790 h1791 h1992 h2000 h2001
5003 G s2001 t1957
5004 B b2001 s2001
5005 T t2002 o1095 b2001 b1935
5006 B b2002 t2002
5007 S s2002 t684 h h1937 h1789 h1790 h1791 h1955 h2000 h2001
5008 G s2002 t1957
5009 B b2003 s2002
5010 T t2003 o1095 b2003 b1935
5011 B b2004 t2003
5012 T t2004 o1094 b2004 b4 b1997
5013 B b2005 t2004
5014 T t2005 o2 b2005
5015 B b2006 t2005
5016 T t2006 o1094 b2002 b4 b2006
5017 B b2007 t2006
5018 T t2007 o b2007 b4
5019 B b2008 t2007
5020 T t2008 o b2000 b2008
5021 B b2009 t2008
5022 T t2009 o1093 b1981 b2009
5023 B b2010 t2009
5024 T t2010 o1093 b2000 b4
5025 B b2011 t2010
5026 T t2011 o1850 b1092 b2011 b4 b4
5027 B b2012 t2011
5028 H h2012 y_3 t1983
5029 H h2013 y t1987
5030 H h2014 z t1991
5031 S s2014 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2012 h1855 h2013 h1857 h2014 h2000 h2001
5032 G s2014 t738
5033 B b2014 s2014
5034 T t2014 o1095 b2014 b1935
5035 B b2015 t2014
5036 S s2015 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2012 h1855 h2013 h1857 h2014 h2000 h2001
5037 G s2015 t1993
5038 B b2016 s2015
5039 T t2016 o1095 b2016 b1935
5040 B b2017 t2016
5041 H h2017 z_3 t1984
5042 S s2017 t684 h h1937 h1789 h1790 h1791 h1852 h1853 h2017 h2013 h1857 h2014 h2000 h2001
5043 G s2017 t1993
5044 B b2018 s2017
5045 T t2018 o1095 b2018 b1935
5046 B b2019 t2018
5047 H h2019 z_1 t1985
5048 S s2019 t684 h h1937 h1789 h1790 h1791 h1852 h2019 h2013 h1857 h2014 h2000 h2001
5049 G s2019 t1993
5050 B b2020 s2019
5051 T t2020 o1095 b2020 b1935
5052 B b2021 t2020
5053 H h2021 y_1 t1986
5054 S s2021 t684 h h1937 h1789 h1790 h1791 h2021 h2013 h1857 h2014 h2000 h2001
5055 G s2021 t1993
5056 B b2022 s2021
5057 T t2022 o1095 b2022 b1935
5058 B b2023 t2022
5059 H h2023 z_1 t1988
5060 S s2023 t684 h h1937 h1789 h1790 h1791 h2021 h2023 h2014 h2000 h2001
5061 G s2023 t1993
5062 B b2024 s2023
5063 T t2024 o1095 b2024 b1935
5064 B b2025 t2024
5065 H h2025 y t1989
5066 S s2025 t684 h h1937 h1789 h1790 h1791 h2025 h2014 h2000 h2001
5067 G s2025 t1993
5068 B b2026 s2025
5069 T t2026 o1095 b2026 b1935
5070 B b2027 t2026
5071 S s2027 t684 h h1937 h1789 h1790 h1791 h1992 h2000 h2001
5072 G s2027 t1993
5073 B b2028 s2027
5074 T t2028 o1095 b2028 b1935
5075 B b2029 t2028
5076 T t2029 o2 b2007
5077 B b2030 t2029
5078 T t2030 o1094 b2029 b4 b2030
5079 B b2031 t2030
5080 T t2031 o2 b2031
5081 B b2032 t2031
5082 T t2032 o1094 b2027 b4 b2032
5083 B b2033 t2032
5084 T t2033 o2 b2033
5085 B b2034 t2033
5086 T t2034 o1094 b2025 b4 b2034
5087 B b2035 t2034
5088 T t2035 o2 b2035
5089 B b2036 t2035
5090 T t2036 o1094 b2023 b4 b2036
5091 B b2037 t2036
5092 T t2037 o2 b2037
5093 B b2038 t2037
5094 T t2038 o1094 b2021 b4 b2038
5095 B b2039 t2038
5096 T t2039 o2 b2039
5097 B b2040 t2039
5098 T t2040 o1094 b2019 b4 b2040
5099 B b2041 t2040
5100 T t2041 o2 b2041
5101 B b2042 t2041
5102 T t2042 o1094 b2017 b1864 b2042
5103 B b2043 t2042
5104 T t2043 o2 b2043
5105 B b2044 t2043
5106 T t2044 o1094 b2015 b4 b2044
5107 B b2045 t2044
5108 T t2045 o b2045 b4
5109 B b2046 t2045
5110 T t2046 o1093 b2007 b2046
5111 B b2047 t2046
5112 T t2047 o1093 b2045 b4
5113 B b2048 t2047
5114 T t2048 o1894 b1092 b2048 b4 b4
5115 B b2049 t2048
5116 T t2049 o b2049 b4
5117 B b2050 t2049
5118 T t2050 o1852 b1092 b2047 b2050 b4
5119 B b2051 t2050
5120 T t2051 o b2051 b4
5121 B b2052 t2051
5122 T t2052 o b2012 b2052
5123 B b2053 t2052
5124 T t2053 o1983 b1092 b2010 b2053 b4
5125 B b2054 t2053
5126 T t2054 o b2054 b4
5127 B b2055 t2054
5128 T t2055 o1954 b1092 b1983 b2055 b4
5129 B b2056 t2055
5130 P p2056 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 'e2}; 'e2} >> 3 ttca"
5131 O o2056 ext_rule p2056
5132 T t2056 o1093 b1951 b4
5133 B b2057 t2056
5134 T t2057 o2056 b1092 b2057 b4 b4
5135 B b2058 t2057
5136 T t2058 o b2058 b4
5137 B b2059 t2058
5138 T t2059 o b2056 b2059
5139 B b2060 t2059
5140 T t2060 o1757 b1092 b1954 b2060 b4
5141 B b2061 t2060
5142 T t2061 o1090 b2061
5143 B b2062 t2061
5144 P p2062 Number 14871
5145 P p2063 Number 14879
5146 O o2063 resource_defs p2062 p2063 p204
5147 P p2064 Number 14877
5148 O o2064 uid p2064 p2063
5149 T t2064 o2064 b691
5150 B b2064 t2064
5151 T t2065 o b2064 b4
5152 B b2065 t2065
5153 T t2066 o2063 b2065
5154 B b2066 t2066
5155 T t2067 o b2066 b4
5156 B b2067 t2067
5157 T t2068 o1918 b676 b1928 b2062 b2067
5158 B b2068 t2068
5159 T t2069 o1917 b2068
5160 B b2069 t2069
5161 P p2069 Number 15319
5162 P p2070 Number 15874
5163 O o2070 location p2069 p2070
5164 P p2071 String unique_inv1
5165 O o2071 rule p2071
5166 T t2071 o596 b585 b717 b815
5167 B b2071 t2071
5168 T t2072 o761 b591 b759 b2071 b604
5169 S s2072 t684 h
5170 G s2072 t2072
5171 B b2072 s2072
5172 T t2073 o677 b2072
5173 B b2073 t2073
5174 T t2074 o609 b585 b815
5175 B b2074 t2074
5176 T t2075 o761 b591 b759 b717 b2074
5177 S s2075 t684 h
5178 G s2075 t2075
5179 B b2075 s2075
5180 T t2076 o677 b2075
5181 B b2076 t2076
5182 T t2077 o676 b2073 b2076
5183 B b2077 t2077
5184 T t2078 o676 b739 b2077
5185 B b2078 t2078
5186 T t2079 o676 b945 b2078
5187 B b2079 t2079
5188 T t2080 o676 b763 b2079
5189 B b2080 t2080
5190 T t2081 o676 b700 b2080
5191 B b2081 t2081
5192 T t2082 o676 b682 b2081
5193 B b2082 t2082
5194 T t2083 o676 b761 b2082
5195 B b2083 t2083
5196 T t2084 o676 b719 b2083
5197 B b2084 t2084
5198 T t2085 o676 b817 b2084
5199 B b2085 t2085
5200 P p2085 String "assumT 9 thenT equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; inv{'g; 's}; 's}}>> 2 ttca"
5201 O o2085 ext_rule p2085
5202 T t2086 o b2072 b4
5203 B b2086 t2086
5204 T t2087 o b738 b2086
5205 B b2087 t2087
5206 T t2088 o b944 b2087
5207 B b2088 t2088
5208 T t2089 o b762 b2088
5209 B b2089 t2089
5210 T t2090 o b699 b2089
5211 B b2090 t2090
5212 T t2091 o b681 b2090
5213 B b2091 t2091
5214 T t2092 o b760 b2091
5215 B b2092 t2092
5216 T t2093 o b718 b2092
5217 B b2093 t2093
5218 T t2094 o b816 b2093
5219 B b2094 t2094
5220 T t2095 o1095 b2075 b2094
5221 B b2095 t2095
5222 T t2096 o1094 b2095 b4 b1104
5223 B b2096 t2096
5224 H h2096 v t2072
5225 T t2097 o596 b585 b2074 b815
5226 B b2097 t2097
5227 T t2098 o761 b591 b759 b604 b2097
5228 S s2098 t684 h h2096
5229 G s2098 t2098
5230 B b2098 s2098
5231 T t2099 o1095 b2098 b2094
5232 B b2099 t2099
5233 S s2099 t684 h h2096
5234 G s2099 t2075
5235 B b2100 s2099
5236 T t2100 o1095 b2100 b2094
5237 B b2101 t2100
5238 T t2101 o2 b2096
5239 B b2102 t2101
5240 T t2102 o1094 b2101 b4 b2102
5241 B b2103 t2102
5242 T t2103 o2 b2103
5243 B b2104 t2103
5244 T t2104 o1094 b2099 b4 b2104
5245 B b2105 t2104
5246 T t2105 o761 b591 b759 b2071 b2097
5247 H h2105 z t2105
5248 S s2105 t684 h h2096 h2105
5249 G s2105 t2075
5250 B b2106 s2105
5251 T t2106 o1095 b2106 b2094
5252 B b2107 t2106
5253 T t2107 o1094 b2107 b4 b2104
5254 B b2108 t2107
5255 T t2108 o b2108 b4
5256 B b2109 t2108
5257 T t2109 o b2105 b2109
5258 B b2110 t2109
5259 T t2110 o1093 b2096 b2110
5260 B b2111 t2110
5261 P p2111 String "assertT << equiv{car{'g}; 'R; op{'g; inv{'g; 's}; 's}; id{'g}} >> ttca thenT equivSymT 3 ttca"
5262 O o2111 ext_rule p2111
5263 T t2111 o1093 b2105 b4
5264 B b2112 t2111
5265 T t2112 o2111 b1092 b2112 b4 b4
5266 B b2113 t2112
5267 P p3 String "groupCancelRightT 3 ttca"
5268 O o6 ext_rule p3
5269 T t2113 o1093 b2108 b4
5270 B b2114 t2113
5271 T t154 o6 b1092 b2114 b4 b4
5272 B b154 t154
5273 T t155 o b154 b4
5274 B b155 t155
5275 T t158 o b2113 b155
5276 B b158 t158
5277 T t159 o2085 b1092 b2111 b158 b4
5278 B b159 t159
5279 T t169 o1090 b159
5280 B b169 t169
5281 P p2119 Number 15346
5282 P p2120 Number 15354
5283 O o2120 resource_defs p2119 p2120 p204
5284 P p2121 Number 15352
5285 O o2121 uid p2121 p2120
5286 T t2121 o2121 b691
5287 B b2121 t2121
5288 T t2122 o b2121 b4
5289 B b2122 t2122
5290 T t2123 o2120 b2122
5291 B b2123 t2123
5292 T t2124 o b2123 b4
5293 B b2124 t2124
5294 T t170 o2071 b676 b2085 b169 b2124
5295 B b170 t170
5296 T t173 o2070 b170
5297 B b173 t173
5298 P p2126 Number 15876
5299 P p2127 Number 16431
5300 O o2127 location p2126 p2127
5301 P p2128 String unique_inv2
5302 O o2128 rule p2128
5303 T t2128 o596 b585 b815 b717
5304 B b2128 t2128
5305 T t2129 o761 b591 b759 b2128 b604
5306 S s2129 t684 h
5307 G s2129 t2129
5308 B b2129 s2129
5309 T t2130 o677 b2129
5310 B b2130 t2130
5311 T t2131 o676 b2130 b2076
5312 B b2131 t2131
5313 T t2132 o676 b739 b2131
5314 B b2132 t2132
5315 T t2133 o676 b945 b2132
5316 B b2133 t2133
5317 T t2134 o676 b763 b2133
5318 B b2134 t2134
5319 T t2135 o676 b700 b2134
5320 B b2135 t2135
5321 T t2136 o676 b761 b2135
5322 B b2136 t2136
5323 T t2137 o676 b682 b2136
5324 B b2137 t2137
5325 T t2138 o676 b719 b2137
5326 B b2138 t2138
5327 T t2139 o676 b817 b2138
5328 B b2139 t2139
5329 P p2139 String "assumT 9 thenT equivSubstT << equiv{car{'g}; 'R; id{'g}; op{'g; 's; inv{'g; 's}}}>> 2 ttca"
5330 O o2139 ext_rule p2139
5331 T t2140 o b2129 b4
5332 B b2140 t2140
5333 T t2141 o b738 b2140
5334 B b2141 t2141
5335 T t2142 o b944 b2141
5336 B b2142 t2142
5337 T t2143 o b762 b2142
5338 B b2143 t2143
5339 T t2144 o b699 b2143
5340 B b2144 t2144
5341 T t2145 o b760 b2144
5342 B b2145 t2145
5343 T t2146 o b681 b2145
5344 B b2146 t2146
5345 T t2147 o b718 b2146
5346 B b2147 t2147
5347 T t2148 o b816 b2147
5348 B b2148 t2148
5349 T t2149 o1095 b2075 b2148
5350 B b2149 t2149
5351 T t2150 o1094 b2149 b4 b1104
5352 B b2150 t2150
5353 H h2150 v t2129
5354 T t2151 o596 b585 b815 b2074
5355 B b2151 t2151
5356 T t2152 o761 b591 b759 b604 b2151
5357 S s2152 t684 h h2150
5358 G s2152 t2152
5359 B b2152 s2152
5360 T t2153 o1095 b2152 b2148
5361 B b2153 t2153
5362 S s2153 t684 h h2150
5363 G s2153 t2075
5364 B b2154 s2153
5365 T t2154 o1095 b2154 b2148
5366 B b2155 t2154
5367 T t2155 o2 b2150
5368 B b2156 t2155
5369 T t2156 o1094 b2155 b4 b2156
5370 B b2157 t2156
5371 T t2157 o2 b2157
5372 B b2158 t2157
5373 T t2158 o1094 b2153 b4 b2158
5374 B b2159 t2158
5375 T t2159 o761 b591 b759 b2128 b2151
5376 H h2159 z t2159
5377 S s2159 t684 h h2150 h2159
5378 G s2159 t2075
5379 B b2160 s2159
5380 T t2160 o1095 b2160 b2148
5381 B b2161 t2160
5382 T t2161 o1094 b2161 b4 b2158
5383 B b2162 t2161
5384 T t2162 o b2162 b4
5385 B b2163 t2162
5386 T t2163 o b2159 b2163
5387 B b2164 t2163
5388 T t2164 o1093 b2150 b2164
5389 B b2165 t2164
5390 P p2165 String "assertT << equiv{car{'g}; 'R; op{'g; 's; inv{'g; 's}}; id{'g}} >> ttca thenT equivSymT 3 ttca"
5391 O o2165 ext_rule p2165
5392 T t2165 o1093 b2159 b4
5393 B b2166 t2165
5394 T t2166 o2165 b1092 b2166 b4 b4
5395 B b2167 t2166
5396 P p2167 String "groupCancelLeftT 3 ttca"
5397 O o2167 ext_rule p2167
5398 T t2167 o1093 b2162 b4
5399 B b2168 t2167
5400 T t2168 o2167 b1092 b2168 b4 b4
5401 B b2169 t2168
5402 T t2169 o b2169 b4
5403 B b2170 t2169
5404 T t2170 o b2167 b2170
5405 B b2171 t2170
5406 T t2171 o2139 b1092 b2165 b2171 b4
5407 B b2172 t2171
5408 T t2172 o1090 b2172
5409 B b2173 t2172
5410 P p2173 Number 15903
5411 P p2174 Number 15911
5412 O o2174 resource_defs p2173 p2174 p204
5413 P p2175 Number 15909
5414 O o2175 uid p2175 p2174
5415 T t2175 o2175 b691
5416 B b2175 t2175
5417 T t2176 o b2175 b4
5418 B b2176 t2176
5419 T t2177 o2174 b2176
5420 B b2177 t2177
5421 T t2178 o b2177 b4
5422 B b2178 t2178
5423 T t2179 o2128 b676 b2139 b2173 b2178
5424 B b2179 t2179
5425 T t2180 o2127 b2179
5426 B b2180 t2180
5427 P p2180 Number 16482
5428 P p2181 Number 17134
5429 O o2181 location p2180 p2181
5430 P p2182 String unique_sol1
5431 O o2182 rule p2182
5432 B b2182 t1304
5433 T t2182 o700 b2182
5434 S s2182 t679 h
5435 G s2182 t2182
5436 B b2183 s2182
5437 T t2183 o677 b2183
5438 B b2184 t2183
5439 T t2184 o736 b2182 b591
5440 S s2184 t684 h
5441 G s2184 t2184
5442 B b2185 s2184
5443 T t2185 o677 b2185
5444 B b2186 t2185
5445 T t2186 o596 b585 b597 b2182
5446 B b2187 t2186
5447 T t2187 o761 b591 b759 b2187 b598
5448 S s2187 t684 h
5449 G s2187 t2187
5450 B b2188 s2187
5451 T t2188 o677 b2188
5452 B b2189 t2188
5453 T t2189 o596 b585 b609 b598
5454 B b2190 t2189
5455 T t2190 o761 b591 b759 b2182 b2190
5456 S s2190 t684 h
5457 G s2190 t2190
5458 B b2191 s2190
5459 T t2191 o677 b2191
5460 B b2192 t2191
5461 T t2192 o676 b2189 b2192
5462 B b2193 t2192
5463 T t2193 o676 b2186 b2193
5464 B b2194 t2193
5465 T t2194 o676 b1077 b2194
5466 B b2195 t2194
5467 T t2195 o676 b1075 b2195
5468 B b2196 t2195
5469 T t2196 o676 b763 b2196
5470 B b2197 t2196
5471 T t2197 o676 b700 b2197
5472 B b2198 t2197
5473 T t2198 o676 b682 b2198
5474 B b2199 t2198
5475 T t2199 o676 b761 b2199
5476 B b2200 t2199
5477 T t2200 o676 b2184 b2200
5478 B b2201 t2200
5479 T t2201 o676 b1073 b2201
5480 B b2202 t2201
5481 T t2202 o676 b1071 b2202
5482 B b2203 t2202
5483 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"
5484 O o2203 ext_rule p2203
5485 T t2203 o b2188 b4
5486 B b2204 t2203
5487 T t2204 o b2185 b2204
5488 B b2205 t2204
5489 T t2205 o b1076 b2205
5490 B b2206 t2205
5491 T t2206 o b1074 b2206
5492 B b2207 t2206
5493 T t2207 o b762 b2207
5494 B b2208 t2207
5495 T t2208 o b699 b2208
5496 B b2209 t2208
5497 T t2209 o b681 b2209
5498 B b2210 t2209
5499 T t2210 o b760 b2210
5500 B b2211 t2210
5501 T t2211 o b2183 b2211
5502 B b2212 t2211
5503 T t2212 o b1072 b2212
5504 B b2213 t2212
5505 T t2213 o b1070 b2213
5506 B b2214 t2213
5507 T t2214 o1095 b2191 b2214
5508 B b2215 t2214
5509 T t2215 o1094 b2215 b4 b1104
5510 B b2216 t2215
5511 H h2216 v t2187
5512 T t2216 o596 b585 b609 b2187
5513 B b2217 t2216
5514 T t2217 o761 b591 b759 b2217 b2190
5515 H h2217 v_1 t2217
5516 S s2217 t684 h h2216 h2217
5517 G s2217 t2190
5518 B b2218 s2217
5519 T t2218 o1095 b2218 b2214
5520 B b2219 t2218
5521 S s2219 t684 h h2216
5522 G s2219 t2190
5523 B b2220 s2219
5524 T t2220 o1095 b2220 b2214
5525 B b2221 t2220
5526 T t2221 o2 b2216
5527 B b2222 t2221
5528 T t2222 o1094 b2221 b4 b2222
5529 B b2223 t2222
5530 T t2223 o2 b2223
5531 B b2224 t2223
5532 T t2224 o1094 b2219 b4 b2224
5533 B b2225 t2224
5534 T t2225 o b2225 b4
5535 B b2226 t2225
5536 T t2226 o1093 b2216 b2226
5537 B b2227 t2226
5538 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"
5539 O o2227 ext_rule p2227
5540 T t2227 o596 b585 b609 b597
5541 B b2228 t2227
5542 T t2228 o596 b585 b2228 b2182
5543 B b2229 t2228
5544 T t2229 o761 b591 b759 b2229 b2190
5545 H h2229 z t2229
5546 S s2229 t684 h h2216 h2217 h2229
5547 G s2229 t2190
5548 B b2230 s2229
5549 T t2230 o1095 b2230 b2214
5550 B b2231 t2230
5551 T t2231 o2 b2225
5552 B b2232 t2231
5553 T t2232 o1094 b2231 b4 b2232
5554 B b2233 t2232
5555 T t2233 o b2233 b4
5556 B b2234 t2233
5557 T t2234 o1093 b2225 b2234
5558 B b2235 t2234
5559 P p2235 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 'a}; 'a}; id{'g}} >> 4 ttca"
5560 O o2235 ext_rule p2235
5561 T t2235 o596 b585 b604 b2182
5562 B b2236 t2235
5563 T t2236 o761 b591 b759 b2236 b2190
5564 H h2236 z_1 t2236
5565 S s2236 t684 h h2216 h2217 h2229 h2236
5566 G s2236 t2190
5567 B b2237 s2236
5568 T t2237 o1095 b2237 b2214
5569 B b2238 t2237
5570 T t2238 o2 b2233
5571 B b2239 t2238
5572 T t2239 o1094 b2238 b4 b2239
5573 B b2240 t2239
5574 T t2240 o b2240 b4
5575 B b2241 t2240
5576 T t2241 o1093 b2233 b2241
5577 B b2242 t2241
5578 P p2242 String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 'x}; 'x} >> 5 ttca"
5579 O o2242 ext_rule p2242
5580 T t2242 o1093 b2240 b4
5581 B b2243 t2242
5582 T t2243 o2242 b1092 b2243 b4 b4
5583 B b2244 t2243
5584 T t2244 o b2244 b4
5585 B b2245 t2244
5586 T t2245 o2235 b1092 b2242 b2245 b4
5587 B b2246 t2245
5588 T t2246 o b2246 b4
5589 B b2247 t2246
5590 T t2247 o2227 b1092 b2235 b2247 b4
5591 B b2248 t2247
5592 T t2248 o b2248 b4
5593 B b2249 t2248
5594 T t2249 o2203 b1092 b2227 b2249 b4
5595 B b2250 t2249
5596 T t2250 o1090 b2250
5597 B b2251 t2250
5598 P p2251 Number 16509
5599 P p2252 Number 16517
5600 O o2252 resource_defs p2251 p2252 p204
5601 P p2253 Number 16515
5602 O o2253 uid p2253 p2252
5603 T t2253 o2253 b691
5604 B b2253 t2253
5605 T t2254 o b2253 b4
5606 B b2254 t2254
5607 T t2255 o2252 b2254
5608 B b2255 t2255
5609 T t2256 o b2255 b4
5610 B b2256 t2256
5611 T t2257 o2182 b676 b2203 b2251 b2256
5612 B b2257 t2257
5613 T t2258 o2181 b2257
5614 B b2258 t2258
5615 P p2258 Number 17185
5616 P p2259 Number 17837
5617 O o2259 location p2258 p2259
5618 P p2260 String unique_sol2
5619 O o2260 rule p2260
5620 P p2261 Var y
5621 O o2261 var p2261
5622 T t2261 o2261
5623 B b2261 t2261
5624 T t2262 o700 b2261
5625 S s2262 t679 h
5626 G s2262 t2262
5627 B b2262 s2262
5628 T t2263 o677 b2262
5629 B b2263 t2263
5630 T t2264 o736 b2261 b591
5631 S s2264 t684 h
5632 G s2264 t2264
5633 B b2264 s2264
5634 T t2265 o677 b2264
5635 B b2265 t2265
5636 T t2266 o596 b585 b2261 b597
5637 B b2266 t2266
5638 T t2267 o761 b591 b759 b2266 b598
5639 S s2267 t684 h
5640 G s2267 t2267
5641 B b2267 s2267
5642 T t2268 o677 b2267
5643 B b2268 t2268
5644 T t2269 o596 b585 b598 b609
5645 B b2269 t2269
5646 T t2270 o761 b591 b759 b2261 b2269
5647 S s2270 t684 h
5648 G s2270 t2270
5649 B b2270 s2270
5650 T t2271 o677 b2270
5651 B b2271 t2271
5652 T t2272 o676 b2268 b2271
5653 B b2272 t2272
5654 T t2273 o676 b2265 b2272
5655 B b2273 t2273
5656 T t2274 o676 b1077 b2273
5657 B b2274 t2274
5658 T t2275 o676 b1075 b2274
5659 B b2275 t2275
5660 T t2276 o676 b763 b2275
5661 B b2276 t2276
5662 T t2277 o676 b700 b2276
5663 B b2277 t2277
5664 T t2278 o676 b682 b2277
5665 B b2278 t2278
5666 T t2279 o676 b761 b2278
5667 B b2279 t2279
5668 T t2280 o676 b2263 b2279
5669 B b2280 t2280
5670 T t2281 o676 b1073 b2280
5671 B b2281 t2281
5672 T t2282 o676 b1071 b2281
5673 B b2282 t2282
5674 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"
5675 O o175 ext_rule p174
5676 T t2283 o b2267 b4
5677 B b2283 t2283
5678 T t2284 o b2264 b2283
5679 B b2284 t2284
5680 T t2285 o b1076 b2284
5681 B b2285 t2285
5682 T t2286 o b1074 b2285
5683 B b2286 t2286
5684 T t2287 o b762 b2286
5685 B b2287 t2287
5686 T t2288 o b699 b2287
5687 B b2288 t2288
5688 T t2289 o b681 b2288
5689 B b2289 t2289
5690 T t2290 o b760 b2289
5691 B b2290 t2290
5692 T t2291 o b2262 b2290
5693 B b2291 t2291
5694 T t2292 o b1072 b2291
5695 B b2292 t2292
5696 T t2293 o b1070 b2292
5697 B b2293 t2293
5698 T t2294 o1095 b2270 b2293
5699 B b2294 t2294
5700 T t2295 o1094 b2294 b4 b1104
5701 B b2295 t2295
5702 H h2295 v t2267
5703 T t2296 o596 b585 b2266 b609
5704 B b2296 t2296
5705 T t2297 o761 b591 b759 b2296 b2269
5706 H h2297 v_1 t2297
5707 S s2300 t684 h h2295 h2297
5708 G s2300 t2270
5709 B b2301 s2300
5710 T t2301 o1095 b2301 b2293
5711 B b2302 t2301
5712 S s2302 t684 h h2295
5713 G s2302 t2270
5714 B b2303 s2302
5715 T t2303 o1095 b2303 b2293
5716 B b2304 t2303
5717 T t2304 o2 b2295
5718 B b2305 t2304
5719 T t2305 o1094 b2304 b4 b2305
5720 B b2306 t2305
5721 T t2306 o2 b2306
5722 B b2307 t2306
5723 T t2314 o1094 b2302 b4 b2307
5724 B b2315 t2314
5725 T t177 o b2315 b4
5726 B b177 t177
5727 T t178 o1093 b2295 b177
5728 B b178 t178
5729 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"
5730 O o186 ext_rule p186
5731 T t2315 o596 b585 b597 b609
5732 B b2316 t2315
5733 T t2316 o596 b585 b2261 b2316
5734 B b2317 t2316
5735 T t2317 o761 b591 b759 b2317 b2269
5736 H h2317 z t2317
5737 S s2319 t684 h h2295 h2297 h2317
5738 G s2319 t2270
5739 B b2320 s2319
5740 T t2320 o1095 b2320 b2293
5741 B b2321 t2320
5742 T t2321 o2 b2315
5743 B b2322 t2321
5744 P p2329 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'a; inv{'g; 'a}}; id{'g}} >> 4 ttca"
5745 O o2329 ext_rule p2329
5746 T t2329 o1094 b2321 b4 b2322
5747 B b2330 t2329
5748 T t191 o b2330 b4
5749 B b191 t191
5750 T t196 o1093 b2315 b191
5751 B b196 t196
5752 T t2330 o596 b585 b2261 b604
5753 B b2331 t2330
5754 T t2331 o761 b591 b759 b2331 b2269
5755 H h2331 z_1 t2331
5756 S s2331 t684 h h2295 h2297 h2317 h2331
5757 G s2331 t2270
5758 B b2332 s2331
5759 T t2332 o1095 b2332 b2293
5760 B b2333 t2332
5761 T t2333 o2 b2330
5762 B b2334 t2333
5763 T t2334 o1094 b2333 b4 b2334
5764 B b2335 t2334
5765 T t2335 o b2335 b4
5766 B b2336 t2335
5767 T t2336 o1093 b2330 b2336
5768 B b2337 t2336
5769 P p2337 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'y; id{'g}}; 'y} >> 5 ttca"
5770 O o2337 ext_rule p2337
5771 T t2337 o1093 b2335 b4
5772 B b2338 t2337
5773 T t2338 o2337 b1092 b2338 b4 b4
5774 B b2339 t2338
5775 T t2339 o b2339 b4
5776 B b2340 t2339
5777 T t2340 o2329 b1092 b2337 b2340 b4
5778 B b2341 t2340
5779 T t2341 o b2341 b4
5780 B b2342 t2341
5781 T t197 o186 b1092 b196 b2342 b4
5782 B b197 t197
5783 T t205 o b197 b4
5784 B b205 t205
5785 T t206 o175 b1092 b178 b205 b4
5786 B b206 t206
5787 T t208 o1090 b206
5788 B b208 t208
5789 P p2346 Number 17212
5790 P p2347 Number 17220
5791 O o2347 resource_defs p2346 p2347 p204
5792 P p2348 Number 17218
5793 O o2348 uid p2348 p2347
5794 T t2348 o2348 b691
5795 B b2348 t2348
5796 T t2349 o b2348 b4
5797 B b2349 t2349
5798 T t2350 o2347 b2349
5799 B b2350 t2350
5800 T t2351 o b2350 b4
5801 B b2351 t2351
5802 T t209 o2260 b676 b2282 b208 b2351
5803 B b209 t209
5804 T t210 o2259 b209
5805 B b210 t210
5806 P p2353 Number 17865
5807 P p2354 Number 18384
5808 O o2354 location p2353 p2354
5809 P p2355 String inv_simplify
5810 O o2355 rule p2355
5811 T t2355 o609 b585 b599
5812 B b2355 t2355
5813 T t2356 o609 b585 b598
5814 B b2356 t2356
5815 T t2357 o596 b585 b2356 b609
5816 B b2357 t2357
5817 T t2358 o761 b591 b759 b2355 b2357
5818 S s2358 t684 h
5819 G s2358 t2358
5820 B b2358 s2358
5821 T t2359 o677 b2358
5822 B b2359 t2359
5823 T t2360 o676 b1077 b2359
5824 B b2360 t2360
5825 T t2361 o676 b1075 b2360
5826 B b2361 t2361
5827 T t2362 o676 b763 b2361
5828 B b2362 t2362
5829 T t2363 o676 b700 b2362
5830 B b2363 t2363
5831 T t2364 o676 b682 b2363
5832 B b2364 t2364
5833 T t2365 o676 b761 b2364
5834 B b2365 t2365
5835 T t2366 o676 b1073 b2365
5836 B b2366 t2366
5837 T t2367 o676 b1071 b2366
5838 B b2367 t2367
5839 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}}} >>"
5840 O o2367 ext_rule p2367
5841 T t2368 o1095 b2358 b1102
5842 B b2368 t2368
5843 T t2369 o1094 b2368 b4 b1104
5844 B b2369 t2369
5845 P p2369 String assertion
5846 O o2369 tactic_arg p2369
5847 T t2370 o596 b585 b2355 b599
5848 B b2370 t2370
5849 T t2371 o596 b585 b2357 b599
5850 B b2371 t2371
5851 T t2372 o761 b591 b759 b2370 b2371
5852 S s2372 t684 h
5853 G s2372 t2372
5854 B b2372 s2372
5855 T t2373 o1095 b2372 b1102
5856 B b2373 t2373
5857 T t2374 o2 b2369
5858 B b2374 t2374
5859 T t2375 o2369 b2373 b4 b2374
5860 B b2375 t2375
5861 H h2375 v t2372
5862 S s2375 t684 h h2375
5863 G s2375 t2358
5864 B b2376 s2375
5865 T t2376 o1095 b2376 b1102
5866 B b2377 t2376
5867 T t2377 o1094 b2377 b4 b2374
5868 B b2378 t2377
5869 T t2378 o b2378 b4
5870 B b2379 t2378
5871 T t2379 o b2375 b2379
5872 B b2380 t2379
5873 T t2380 o1093 b2369 b2380
5874 B b2381 t2380
5875 P p2381 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; op{'g; 'a; 'b}}; op{'g; 'a; 'b}}; id{'g}} >> 0 ttca"
5876 O o2381 ext_rule p2381
5877 T t2381 o761 b591 b759 b604 b2371
5878 S s2381 t684 h
5879 G s2381 t2381
5880 B b2382 s2381
5881 T t2382 o1095 b2382 b1102
5882 B b2383 t2382
5883 T t2383 o2 b2375
5884 B b2384 t2383
5885 T t2384 o2369 b2383 b4 b2384
5886 B b2385 t2384
5887 T t2385 o b2385 b4
5888 B b2386 t2385
5889 T t2386 o1093 b2375 b2386
5890 B b2387 t2386
5891 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"
5892 O o2387 ext_rule p2387
5893 T t2387 o1093 b2385 b4
5894 B b2388 t2387
5895 T t2388 o2387 b1092 b2388 b4 b4
5896 B b2389 t2388
5897 T t2389 o b2389 b4
5898 B b2390 t2389
5899 T t2390 o2381 b1092 b2387 b2390 b4
5900 B b2391 t2390
5901 P p217 String "groupCancelRightT 2 ttca"
5902 O o217 ext_rule p217
5903 T t2391 o1093 b2378 b4
5904 B b2392 t2391
5905 T t229 o217 b1092 b2392 b4 b4
5906 B b229 t229
5907 T t230 o b229 b4
5908 B b230 t230
5909 T t232 o b2391 b230
5910 B b232 t232
5911 T t240 o2367 b1092 b2381 b232 b4
5912 B b240 t240
5913 T t241 o1090 b240
5914 B b241 t241
5915 P p2397 Number 17893
5916 P p2398 Number 17901
5917 O o2398 resource_defs p2397 p2398 p204
5918 P p2399 Number 17899
5919 O o2399 uid p2399 p2398
5920 T t2399 o2399 b691
5921 B b2399 t2399
5922 T t2400 o b2399 b4
5923 B b2400 t2400
5924 T t2401 o2398 b2400
5925 B b2401 t2401
5926 T t2402 o b2401 b4
5927 B b2402 t2402
5928 T t244 o2355 b676 b2367 b241 b2402
5929 B b244 t244
5930 T t249 o2354 b244
5931 B b249 t249
5932 P p2404 Number 18406
5933 P p2405 Number 18702
5934 O o2405 location p2404 p2405
5935 P p2406 String inv_of_id
5936 O o2406 rule p2406
5937 T t2406 o609 b585 b604
5938 B b2406 t2406
5939 T t2407 o761 b591 b759 b2406 b604
5940 S s2407 t684 h
5941 G s2407 t2407
5942 B b2407 s2407
5943 T t2408 o677 b2407
5944 B b2408 t2408
5945 T t2409 o676 b763 b2408
5946 B b2409 t2409
5947 T t2410 o676 b700 b2409
5948 B b2410 t2410
5949 T t2411 o676 b682 b2410
5950 B b2411 t2411
5951 T t2412 o676 b761 b2411
5952 B b2412 t2412
5953 P p2412 String "assertT << equiv{car{'g}; 'R; id{'g}; inv{'g; id{'g}}} >> thenAT autoT"
5954 O o2412 ext_rule p2412
5955 T t2413 o b762 b4
5956 B b2413 t2413
5957 T t2414 o b699 b2413
5958 B b2414 t2414
5959 T t2415 o b681 b2414
5960 B b2415 t2415
5961 T t2416 o b760 b2415
5962 B b2416 t2416
5963 T t2417 o1095 b2407 b2416
5964 B b2417 t2417
5965 T t2418 o1094 b2417 b4 b1104
5966 B b2418 t2418
5967 T t2419 o761 b591 b759 b604 b2406
5968 H h2419 v t2419
5969 S s2419 t684 h h2419
5970 G s2419 t2407
5971 B b2419 s2419
5972 T t2420 o1095 b2419 b2416
5973 B b2420 t2420
5974 T t2421 o2 b2418
5975 B b2421 t2421
5976 T t2422 o1094 b2420 b4 b2421
5977 B b2422 t2422
5978 T t2423 o b2422 b4
5979 B b2423 t2423
5980 T t2424 o1093 b2418 b2423
5981 B b2424 t2424
5982 P p2424 String "equivSymT 2 ttca"
5983 O o2424 ext_rule p2424
5984 T t2425 o1093 b2422 b4
5985 B b2425 t2425
5986 T t2426 o2424 b1092 b2425 b4 b4
5987 B b2426 t2426
5988 T t2427 o b2426 b4
5989 B b2427 t2427
5990 T t2428 o2412 b1092 b2424 b2427 b4
5991 B b2428 t2428
5992 T t2429 o1090 b2428
5993 B b2429 t2429
5994 P p2429 Number 18431
5995 P p2430 Number 18439
5996 O o2430 resource_defs p2429 p2430 p204
5997 P p2431 Number 18437
5998 O o2431 uid p2431 p2430
5999 T t2431 o2431 b691
6000 B b2431 t2431
6001 T t2432 o b2431 b4
6002 B b2432 t2432
6003 T t2433 o2430 b2432
6004 B b2433 t2433
6005 T t2434 o b2433 b4
6006 B b2434 t2434
6007 T t2435 o2406 b676 b2412 b2429 b2434
6008 B b2435 t2435
6009 T t2436 o2405 b2435
6010 B b2436 t2436
6011 O o2436 location p p
6012 NSummary!id id2436 id Summary
6013 P p2436 Number 646427455
6014 O o2437 id2436 p2436
6015 T t2437 o2437
6016 B b2437 t2437
6017 T t2438 o2436 b2437
6018 B b2438 t2438
6019 T t2439 o b2438 b4
6020 B b2439 t2439
6021 T t2440 o b2436 b2439
6022 B b2440 t2440
6023 T t250 o b249 b2440
6024 B b250 t250
6025 T t255 o b210 b250
6026 B b255 t255
6027 T t256 o b2258 b255
6028 B b256 t256
6029 T t258 o b2180 b256
6030 B b258 t258
6031 T t260 o b173 b258
6032 B b260 t260
6033 T t267 o b2069 b260
6034 B b267 t267
6035 T t271 o b1916 b267
6036 B b271 t271
6037 T t272 o b1737 b271
6038 B b272 t272
6039 T t275 o b1677 b272
6040 B b275 t275
6041 T t279 o b1610 b275
6042 B b279 t279
6043 T t280 o b1456 b279
6044 B b280 t280
6045 T t299 o b1297 b280
6046 B b299 t299
6047 T t368 o b1198 b299
6048 B b368 t368
6049 T t379 o b1068 b368
6050 B b379 t379
6051 T t394 o b1051 b379
6052 B b394 t394
6053 T t400 o b1034 b394
6054 B b400 t400
6055 T t421 o b1022 b400
6056 B b421 t421
6057 T t422 o b1007 b421
6058 B b422 t422
6059 T t423 o b993 b422
6060 B b423 t423
6061 T t429 o b978 b423
6062 B b429 t429
6063 T t430 o b961 b429
6064 B b430 t430
6065 T t436 o b942 b430
6066 B b436 t436
6067 T t437 o b930 b436
6068 B b437 t437
6069 T t446 o b918 b437
6070 B b446 t446
6071 T t447 o b898 b446
6072 B b447 t447
6073 T t455 o b876 b447
6074 B b455 t455
6075 T t456 o b863 b455
6076 B b456 t456
6077 T t464 o b849 b456
6078 B b464 t464
6079 T t465 o b833 b464
6080 B b465 t465
6081 T t473 o b812 b465