/[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 3494 - (show annotations) (download)
Thu Feb 7 23:19:33 2002 UTC (19 years, 5 months ago) by xiny
File size: 122272 byte(s)
Removed tactics "op_assoc1T", "op_assoc2T" (previously as comments),
and "id_elim2T".

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 19
9 O o1 location p p1
10 NSummary!parent parent parent Summary
11 O o2 parent
12 P p2 String Czf_itt_set
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 Czf_itt_comment
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_theory
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_fset
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_prop_decide
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_derive
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_list2
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_list
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_quotient
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_esquash
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_srec
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_prec
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_w
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_bunion
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_bisect
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_tunion
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_isect
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_struct2
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_well_founded
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_int_arith
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_int_ext
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_int_base
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 Itt_atom_bool
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 Itt_atom
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 Itt_bool
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 Itt_decidable
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 Itt_logic
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 Itt_prod
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 Itt_dprod
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 Itt_fun
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 Itt_dfun
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 Itt_rfun
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 Itt_set
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 Itt_unit
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 Itt_squiggle
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 Itt_squash
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 Itt_union
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 Itt_void
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 Itt_subtype
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 Itt_struct
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 Itt_equal
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 Itt_comment
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 Base_theory
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 Base_meta
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 Base_cache
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 Tactic_cache
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 Typeinf
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 Ocaml_df
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 Ocaml_str_df
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 Ocaml_sig_df
311 O o101 parent p101
312 T t102 o101
313 B b102 t102
314 T t103 o b102 b4
315 B b103 t103
316 P p103 String Ocaml_me_df
317 O o103 parent p103
318 T t104 o103
319 B b104 t104
320 T t105 o b104 b4
321 B b105 t105
322 P p105 String Ocaml_mt_df
323 O o105 parent p105
324 T t106 o105
325 B b106 t106
326 T t107 o b106 b4
327 B b107 t107
328 P p107 String Ocaml_type_df
329 O o107 parent p107
330 T t108 o107
331 B b108 t108
332 T t109 o b108 b4
333 B b109 t109
334 P p109 String Ocaml_patt_df
335 O o109 parent p109
336 T t110 o109
337 B b110 t110
338 T t111 o b110 b4
339 B b111 t111
340 P p111 String Ocaml_expr_df
341 O o111 parent p111
342 T t112 o111
343 B b112 t112
344 T t113 o b112 b4
345 B b113 t113
346 P p113 String Ocaml_base_df
347 O o113 parent p113
348 T t114 o113
349 B b114 t114
350 T t115 o b114 b4
351 B b115 t115
352 P p115 String Ocaml
353 O o115 parent p115
354 T t116 o115
355 B b116 t116
356 T t117 o b116 b4
357 B b117 t117
358 P p117 String Base_rewrite
359 O o117 parent p117
360 T t118 o117
361 B b118 t118
362 T t119 o b118 b4
363 B b119 t119
364 P p119 String Base_dtactic
365 O o119 parent p119
366 T t120 o119
367 B b120 t120
368 T t121 o b120 b4
369 B b121 t121
370 P p121 String Base_auto_tactic
371 O o121 parent p121
372 T t122 o121
373 B b122 t122
374 T t123 o b122 b4
375 B b123 t123
376 P p123 String Base_trivial
377 O o123 parent p123
378 T t124 o123
379 B b124 t124
380 T t125 o b124 b4
381 B b125 t125
382 P p125 String Top_conversionals
383 O o125 parent p125
384 T t126 o125
385 B b126 t126
386 T t127 o b126 b4
387 B b127 t127
388 P p127 String Top_tacticals
389 O o127 parent p127
390 T t128 o127
391 B b128 t128
392 T t129 o b128 b4
393 B b129 t129
394 P p129 String Var
395 O o129 parent p129
396 T t130 o129
397 B b130 t130
398 T t131 o b130 b4
399 B b131 t131
400 P p131 String Mptop
401 O o131 parent p131
402 T t132 o131
403 B b132 t132
404 T t133 o b132 b4
405 B b133 t133
406 P p133 String Summary
407 O o133 parent p133
408 T t134 o133
409 B b134 t134
410 T t135 o b134 b4
411 B b135 t135
412 P p135 String Comment
413 O o135 parent p135
414 T t136 o135
415 B b136 t136
416 T t137 o b136 b4
417 B b137 t137
418 P p137 String Base_dform
419 O o137 parent p137
420 T t138 o137
421 B b138 t138
422 T t139 o b138 b4
423 B b139 t139
424 P p139 String Nuprl_font
425 O o139 parent p139
426 T t140 o139
427 B b140 t140
428 T t141 o b140 b4
429 B b141 t141
430 P p141 String Perv
431 O o141 parent p141
432 T t142 o141
433 B b142 t142
434 T t143 o b142 b4
435 B b143 t143
436 T t144 o b143 b4
437 B b144 t144
438 T t145 o b141 b144
439 B b145 t145
440 T t146 o b139 b145
441 B b146 t146
442 T t147 o b137 b146
443 B b147 t147
444 T t148 o b135 b147
445 B b148 t148
446 T t149 o b133 b148
447 B b149 t149
448 T t150 o b131 b149
449 B b150 t150
450 T t151 o b129 b150
451 B b151 t151
452 T t152 o b127 b151
453 B b152 t152
454 T t153 o b125 b152
455 B b153 t153
456 T t154 o b123 b153
457 B b154 t154
458 T t155 o b121 b154
459 B b155 t155
460 T t156 o b119 b155
461 B b156 t156
462 T t157 o b117 b156
463 B b157 t157
464 T t158 o b115 b157
465 B b158 t158
466 T t159 o b113 b158
467 B b159 t159
468 T t160 o b111 b159
469 B b160 t160
470 T t161 o b109 b160
471 B b161 t161
472 T t162 o b107 b161
473 B b162 t162
474 T t163 o b105 b162
475 B b163 t163
476 T t164 o b103 b163
477 B b164 t164
478 T t165 o b101 b164
479 B b165 t165
480 T t166 o b99 b165
481 B b166 t166
482 T t167 o b97 b166
483 B b167 t167
484 T t168 o b95 b167
485 B b168 t168
486 T t169 o b93 b168
487 B b169 t169
488 T t170 o b91 b169
489 B b170 t170
490 T t171 o b89 b170
491 B b171 t171
492 T t172 o b87 b171
493 B b172 t172
494 T t173 o b85 b172
495 B b173 t173
496 T t174 o b83 b173
497 B b174 t174
498 T t175 o b81 b174
499 B b175 t175
500 T t176 o b79 b175
501 B b176 t176
502 T t177 o b77 b176
503 B b177 t177
504 T t178 o b75 b177
505 B b178 t178
506 T t179 o b73 b178
507 B b179 t179
508 T t180 o b71 b179
509 B b180 t180
510 T t181 o b69 b180
511 B b181 t181
512 T t182 o b67 b181
513 B b182 t182
514 T t183 o b65 b182
515 B b183 t183
516 T t184 o b63 b183
517 B b184 t184
518 T t185 o b61 b184
519 B b185 t185
520 T t186 o b59 b185
521 B b186 t186
522 T t187 o b57 b186
523 B b187 t187
524 T t188 o b55 b187
525 B b188 t188
526 T t189 o b53 b188
527 B b189 t189
528 T t190 o b51 b189
529 B b190 t190
530 T t191 o b49 b190
531 B b191 t191
532 T t192 o b47 b191
533 B b192 t192
534 T t193 o b45 b192
535 B b193 t193
536 T t194 o b43 b193
537 B b194 t194
538 T t195 o b41 b194
539 B b195 t195
540 T t196 o b39 b195
541 B b196 t196
542 T t197 o b37 b196
543 B b197 t197
544 T t198 o b35 b197
545 B b198 t198
546 T t199 o b33 b198
547 B b199 t199
548 T t200 o b31 b199
549 B b200 t200
550 T t201 o b29 b200
551 B b201 t201
552 T t202 o b27 b201
553 B b202 t202
554 T t203 o b25 b202
555 B b203 t203
556 T t204 o b23 b203
557 B b204 t204
558 T t205 o b21 b204
559 B b205 t205
560 T t206 o b19 b205
561 B b206 t206
562 T t207 o b17 b206
563 B b207 t207
564 T t208 o b15 b207
565 B b208 t208
566 T t209 o b13 b208
567 B b209 t209
568 T t210 o b11 b209
569 B b210 t210
570 T t211 o b9 b210
571 B b211 t211
572 T t212 o b7 b211
573 B b212 t212
574 T t213 o b5 b212
575 B b213 t213
576 NSummary!resource resource resource Summary
577 P p213 String auto
578 O o213 resource p213
579 NOcaml Ocaml Ocaml NIL
580 NOcaml!type_lid type_lid type_lid Ocaml
581 P p214 Number 2332
582 P p215 Number 2341
583 O o215 type_lid p214 p215
584 P p216 String auto_info
585 O o216 type_lid p216
586 T t216 o216
587 B b216 t216
588 T t217 o215 b216
589 B b217 t217
590 NOcaml!type_prod type_prod type_prod Ocaml
591 P p217 Number 2343
592 P p218 Number 2367
593 O o218 type_prod p217 p218
594 P p219 Number 2349
595 O o219 type_lid p217 p219
596 P p220 String tactic
597 O o220 type_lid p220
598 T t220 o220
599 B b220 t220
600 T t221 o219 b220
601 B b221 t221
602 P p221 Number 2352
603 P p222 Number 2358
604 O o222 type_lid p221 p222
605 T t222 o222 b220
606 B b222 t222
607 P p223 Number 2361
608 O o223 type_lid p223 p218
609 T t223 o223 b220
610 B b223 t223
611 T t224 o b223 b4
612 B b224 t224
613 T t225 o b222 b224
614 B b225 t225
615 T t226 o b221 b225
616 B b226 t226
617 T t227 o218 b226
618 B b227 t227
619 T t228 o213 b217 b227
620 B b228 t228
621 P p228 String cache
622 O o228 resource p228
623 P p229 Number 1424
624 P p230 Number 1434
625 O o230 type_lid p229 p230
626 P p231 String cache_rule
627 O o231 type_lid p231
628 T t231 o231
629 B b231 t231
630 T t232 o230 b231
631 B b232 t232
632 P p232 Number 1436
633 P p233 Number 1441
634 O o233 type_lid p232 p233
635 O o234 type_lid p228
636 T t234 o234
637 B b234 t234
638 T t235 o233 b234
639 B b235 t235
640 T t236 o228 b232 b235
641 B b236 t236
642 P p236 String elim
643 O o236 resource p236
644 P p237 Number 1761
645 P p238 Number 1783
646 O o238 type_prod p237 p238
647 P p239 Number 1765
648 O o239 type_lid p237 p239
649 P p240 String term
650 O o240 type_lid p240
651 T t240 o240
652 B b240 t240
653 T t241 o239 b240
654 B b241 t241
655 NOcaml!type_fun type_fun type_fun Ocaml
656 P p241 Number 1769
657 P p242 Number 1782
658 O o242 type_fun p241 p242
659 P p243 Number 1772
660 O o243 type_lid p241 p243
661 P p244 String int
662 O o244 type_lid p244
663 T t244 o244
664 B b244 t244
665 T t245 o243 b244
666 B b245 t245
667 P p245 Number 1776
668 O o245 type_lid p245 p242
669 T t246 o245 b220
670 B b246 t246
671 T t247 o242 b245 b246
672 B b247 t247
673 T t248 o b247 b4
674 B b248 t248
675 T t249 o b241 b248
676 B b249 t249
677 T t250 o238 b249
678 B b250 t250
679 P p250 Number 1785
680 P p251 Number 1798
681 O o251 type_fun p250 p251
682 P p252 Number 1788
683 O o252 type_lid p250 p252
684 T t252 o252 b244
685 B b252 t252
686 P p253 Number 1792
687 O o253 type_lid p253 p251
688 T t253 o253 b220
689 B b253 t253
690 T t254 o251 b252 b253
691 B b254 t254
692 T t255 o236 b250 b254
693 B b255 t255
694 P p255 String eqcd
695 O o255 resource p255
696 P p256 Number 6168
697 P p257 Number 6181
698 O o257 type_prod p256 p257
699 P p258 Number 6172
700 O o258 type_lid p256 p258
701 T t258 o258 b240
702 B b258 t258
703 P p259 Number 6175
704 O o259 type_lid p259 p257
705 T t259 o259 b220
706 B b259 t259
707 T t260 o b259 b4
708 B b260 t260
709 T t261 o b258 b260
710 B b261 t261
711 T t262 o257 b261
712 B b262 t262
713 P p262 Number 6183
714 P p263 Number 6189
715 O o263 type_lid p262 p263
716 T t263 o263 b220
717 B b263 t263
718 T t264 o255 b262 b263
719 B b264 t264
720 P p264 String intro
721 O o264 resource p264
722 P p265 Number 1815
723 P p266 Number 1852
724 O o266 type_prod p265 p266
725 P p267 Number 1819
726 O o267 type_lid p265 p267
727 T t267 o267 b240
728 B b267 t267
729 P p268 Number 1823
730 P p269 Number 1851
731 O o269 type_prod p268 p269
732 P p270 Number 1829
733 O o270 type_lid p268 p270
734 P p271 String string
735 O o271 type_lid p271
736 T t271 o271
737 B b271 t271
738 T t272 o270 b271
739 B b272 t272
740 NOcaml!type_apply type_apply type_apply Ocaml
741 P p272 Number 1832
742 P p273 Number 1842
743 O o273 type_apply p272 p273
744 P p274 Number 1836
745 O o274 type_lid p274 p273
746 P p275 String option
747 O o275 type_lid p275
748 T t275 o275
749 B b275 t275
750 T t276 o274 b275
751 B b276 t276
752 P p276 Number 1835
753 O o276 type_lid p272 p276
754 T t277 o276 b244
755 B b277 t277
756 T t278 o273 b276 b277
757 B b278 t278
758 P p278 Number 1845
759 O o278 type_lid p278 p269
760 T t279 o278 b220
761 B b279 t279
762 T t280 o b279 b4
763 B b280 t280
764 T t281 o b278 b280
765 B b281 t281
766 T t282 o b272 b281
767 B b282 t282
768 T t283 o269 b282
769 B b283 t283
770 T t284 o b283 b4
771 B b284 t284
772 T t285 o b267 b284
773 B b285 t285
774 T t286 o266 b285
775 B b286 t286
776 P p286 Number 1854
777 P p287 Number 1860
778 O o287 type_lid p286 p287
779 T t287 o287 b220
780 B b287 t287
781 T t288 o264 b286 b287
782 B b288 t288
783 P p288 String reduce
784 O o288 resource p288
785 P p289 Number 2920
786 P p290 Number 2931
787 O o290 type_prod p289 p290
788 P p291 Number 2924
789 O o291 type_lid p289 p291
790 T t291 o291 b240
791 B b291 t291
792 P p292 Number 2927
793 O o292 type_lid p292 p290
794 P p293 String conv
795 O o293 type_lid p293
796 T t293 o293
797 B b293 t293
798 T t294 o292 b293
799 B b294 t294
800 T t295 o b294 b4
801 B b295 t295
802 T t296 o b291 b295
803 B b296 t296
804 T t297 o290 b296
805 B b297 t297
806 P p297 Number 2933
807 P p298 Number 2937
808 O o298 type_lid p297 p298
809 T t298 o298 b293
810 B b298 t298
811 T t299 o288 b297 b298
812 B b299 t299
813 P p299 String squash
814 O o299 resource p299
815 P p300 Number 4017
816 P p301 Number 4028
817 O o301 type_lid p300 p301
818 P p302 String squash_info
819 O o302 type_lid p302
820 T t302 o302
821 B b302 t302
822 T t303 o301 b302
823 B b303 t303
824 P p303 Number 4030
825 P p304 Number 4043
826 O o304 type_fun p303 p304
827 P p305 Number 4033
828 O o305 type_lid p303 p305
829 T t305 o305 b244
830 B b305 t305
831 P p306 Number 4037
832 O o306 type_lid p306 p304
833 T t306 o306 b220
834 B b306 t306
835 T t307 o304 b305 b306
836 B b307 t307
837 T t308 o299 b303 b307
838 B b308 t308
839 P p308 String sub
840 O o308 resource p308
841 P p309 Number 4882
842 P p310 Number 4899
843 O o310 type_lid p309 p310
844 P p311 String sub_resource_info
845 O o311 type_lid p311
846 T t311 o311
847 B b311 t311
848 T t312 o310 b311
849 B b312 t312
850 P p312 Number 4901
851 P p313 Number 4907
852 O o313 type_lid p312 p313
853 T t313 o313 b220
854 B b313 t313
855 T t314 o308 b312 b313
856 B b314 t314
857 P p314 String toploop
858 O o314 resource p314
859 P p315 Number 2445
860 P p316 Number 2467
861 O o316 type_prod p315 p316
862 P p317 Number 2451
863 O o317 type_lid p315 p317
864 T t317 o317 b271
865 B b317 t317
866 P p318 Number 2454
867 P p319 Number 2460
868 O o319 type_lid p318 p319
869 T t319 o319 b271
870 B b319 t319
871 P p320 Number 2463
872 O o320 type_lid p320 p316
873 P p321 String expr
874 O o321 type_lid p321
875 T t321 o321
876 B b321 t321
877 T t322 o320 b321
878 B b322 t322
879 T t323 o b322 b4
880 B b323 t323
881 T t324 o b319 b323
882 B b324 t324
883 T t325 o b317 b324
884 B b325 t325
885 T t326 o316 b325
886 B b326 t326
887 P p326 Number 2469
888 P p327 Number 2478
889 O o327 type_lid p326 p327
890 P p328 String top_table
891 O o328 type_lid p328
892 T t328 o328
893 B b328 t328
894 T t329 o327 b328
895 B b329 t329
896 T t330 o314 b326 b329
897 B b330 t330
898 P p330 String typeinf
899 O o330 resource p330
900 P p331 Number 2151
901 P p332 Number 2172
902 O o332 type_lid p331 p332
903 P p333 String typeinf_resource_info
904 O o333 type_lid p333
905 T t333 o333
906 B b333 t333
907 T t334 o332 b333
908 B b334 t334
909 P p334 Number 2174
910 P p335 Number 2186
911 O o335 type_lid p334 p335
912 P p336 String typeinf_func
913 O o336 type_lid p336
914 T t336 o336
915 B b336 t336
916 T t337 o335 b336
917 B b337 t337
918 T t338 o330 b334 b337
919 B b338 t338
920 P p338 String typeinf_subst
921 O o338 resource p338
922 P p339 Number 1825
923 P p340 Number 1843
924 O o340 type_lid p339 p340
925 P p341 String typeinf_subst_info
926 O o341 type_lid p341
927 T t341 o341
928 B b341 t341
929 T t342 o340 b341
930 B b342 t342
931 P p342 Number 1862
932 O o342 type_lid p278 p342
933 P p343 String typeinf_subst_fun
934 O o343 type_lid p343
935 T t343 o343
936 B b343 t343
937 T t344 o342 b343
938 B b344 t344
939 T t345 o338 b342 b344
940 B b345 t345
941 T t346 o b345 b4
942 B b346 t346
943 T t347 o b338 b346
944 B b347 t347
945 T t348 o b330 b347
946 B b348 t348
947 T t349 o b314 b348
948 B b349 t349
949 T t350 o b308 b349
950 B b350 t350
951 T t351 o b299 b350
952 B b351 t351
953 T t352 o b288 b351
954 B b352 t352
955 T t353 o b264 b352
956 B b353 t353
957 T t354 o b255 b353
958 B b354 t354
959 T t355 o b236 b354
960 B b355 t355
961 T t356 o b228 b355
962 B b356 t356
963 T t357 o2 b5 b213 b356
964 B b357 t357
965 T t358 o1 b357
966 B b358 t358
967 P p358 Number 20
968 P p359 Number 42
969 O o359 location p358 p359
970 P p360 String Czf_itt_member
971 O o360 parent p360
972 T t360 o360
973 B b360 t360
974 T t361 o b360 b4
975 B b361 t361
976 P p361 String Czf_itt_eq
977 O o361 parent p361
978 T t362 o361
979 B b362 t362
980 T t363 o b362 b4
981 B b363 t363
982 T t364 o b363 b4
983 B b364 t364
984 T t365 o b361 b364
985 B b365 t365
986 T t366 o2 b361 b365 b356
987 B b366 t366
988 T t367 o359 b366
989 B b367 t367
990 P p367 Number 43
991 P p368 Number 61
992 O o368 location p367 p368
993 T t368 o2 b363 b4 b356
994 B b368 t368
995 T t369 o368 b368
996 B b369 t369
997 P p369 Number 62
998 P p370 Number 82
999 O o370 location p369 p370
1000 P p371 String Czf_itt_dall
1001 O o371 parent p371
1002 T t371 o371
1003 B b371 t371
1004 T t372 o b371 b4
1005 B b372 t372
1006 P p372 String Czf_itt_set_ind
1007 O o372 parent p372
1008 T t373 o372
1009 B b373 t373
1010 T t374 o b373 b4
1011 B b374 t374
1012 P p374 String Czf_itt_all
1013 O o374 parent p374
1014 T t375 o374
1015 B b375 t375
1016 T t376 o b375 b4
1017 B b376 t376
1018 P p376 String Czf_itt_sep
1019 O o376 parent p376
1020 T t377 o376
1021 B b377 t377
1022 T t378 o b377 b4
1023 B b378 t378
1024 T t379 o b378 b4
1025 B b379 t379
1026 T t380 o b376 b379
1027 B b380 t380
1028 T t381 o b374 b380
1029 B b381 t381
1030 T t382 o b372 b381
1031 B b382 t382
1032 T t383 o2 b372 b382 b356
1033 B b383 t383
1034 T t384 o370 b383
1035 B b384 t384
1036 P p384 Number 83
1037 P p385 Number 102
1038 O o385 location p384 p385
1039 P p386 String Czf_itt_and
1040 O o386 parent p386
1041 T t386 o386
1042 B b386 t386
1043 T t387 o b386 b4
1044 B b387 t387
1045 T t388 o b387 b4
1046 B b388 t388
1047 T t389 o2 b387 b388 b356
1048 B b389 t389
1049 T t390 o385 b389
1050 B b390 t390
1051 P p390 Number 104
1052 P p391 Number 115
1053 O o391 location p390 p391
1054 NSummary!summary_item summary_item summary_item Summary
1055 O o392 summary_item
1056 NOcaml!str_open str_open str_open Ocaml
1057 O o393 str_open p390 p391
1058 NOcaml!string string string Ocaml
1059 P p393 String Printf
1060 O o394 string p393
1061 T t394 o394
1062 B b394 t394
1063 T t395 o b394 b4
1064 B b395 t395
1065 T t396 o393 b395
1066 B b396 t396
1067 T t397 o392 b396
1068 B b397 t397
1069 T t398 o391 b397
1070 B b398 t398
1071 P p398 Number 116
1072 P p399 Number 129
1073 O o399 location p398 p399
1074 O o400 str_open p398 p399
1075 P p400 String Mp_debug
1076 O o401 string p400
1077 T t401 o401
1078 B b401 t401
1079 T t402 o b401 b4
1080 B b402 t402
1081 T t403 o400 b402
1082 B b403 t403
1083 T t404 o392 b403
1084 B b404 t404
1085 T t405 o399 b404
1086 B b405 t405
1087 P p405 Number 130
1088 P p406 Number 159
1089 O o406 location p405 p406
1090 O o407 str_open p405 p406
1091 P p407 String Refiner
1092 O o408 string p407
1093 T t408 o408
1094 B b408 t408
1095 P p408 String TermType
1096 O o409 string p408
1097 T t409 o409
1098 B b409 t409
1099 T t410 o b409 b4
1100 B b410 t410
1101 T t411 o b408 b410
1102 B b411 t411
1103 T t412 o b408 b411
1104 B b412 t412
1105 T t413 o407 b412
1106 B b413 t413
1107 T t414 o392 b413
1108 B b414 t414
1109 T t415 o406 b414
1110 B b415 t415
1111 P p415 Number 160
1112 P p416 Number 185
1113 O o416 location p415 p416
1114 O o417 str_open p415 p416
1115 P p417 String Term
1116 O o418 string p417
1117 T t418 o418
1118 B b418 t418
1119 T t419 o b418 b4
1120 B b419 t419
1121 T t420 o b408 b419
1122 B b420 t420
1123 T t421 o b408 b420
1124 B b421 t421
1125 T t422 o417 b421
1126 B b422 t422
1127 T t423 o392 b422
1128 B b423 t423
1129 T t424 o416 b423
1130 B b424 t424
1131 P p424 Number 186
1132 P p425 Number 213
1133 O o425 location p424 p425
1134 O o426 str_open p424 p425
1135 P p426 String TermOp
1136 O o427 string p426
1137 T t427 o427
1138 B b427 t427
1139 T t428 o b427 b4
1140 B b428 t428
1141 T t429 o b408 b428
1142 B b429 t429
1143 T t430 o b408 b429
1144 B b430 t430
1145 T t431 o426 b430
1146 B b431 t431
1147 T t432 o392 b431
1148 B b432 t432
1149 T t433 o425 b432
1150 B b433 t433
1151 P p433 Number 214
1152 P p434 Number 243
1153 O o434 location p433 p434
1154 O o435 str_open p433 p434
1155 P p435 String TermAddr
1156 O o436 string p435
1157 T t436 o436
1158 B b436 t436
1159 T t437 o b436 b4
1160 B b437 t437
1161 T t438 o b408 b437
1162 B b438 t438
1163 T t439 o b408 b438
1164 B b439 t439
1165 T t440 o435 b439
1166 B b440 t440
1167 T t441 o392 b440
1168 B b441 t441
1169 T t442 o434 b441
1170 B b442 t442
1171 P p442 Number 244
1172 P p443 Number 272
1173 O o443 location p442 p443
1174 O o444 str_open p442 p443
1175 P p444 String TermMan
1176 O o445 string p444
1177 T t445 o445
1178 B b445 t445
1179 T t446 o b445 b4
1180 B b446 t446
1181 T t447 o b408 b446
1182 B b447 t447
1183 T t448 o b408 b447
1184 B b448 t448
1185 T t449 o444 b448
1186 B b449 t449
1187 T t450 o392 b449
1188 B b450 t450
1189 T t451 o443 b450
1190 B b451 t451
1191 P p451 Number 273
1192 P p452 Number 303
1193 O o452 location p451 p452
1194 O o453 str_open p451 p452
1195 P p453 String TermSubst
1196 O o454 string p453
1197 T t454 o454
1198 B b454 t454
1199 T t455 o b454 b4
1200 B b455 t455
1201 T t456 o b408 b455
1202 B b456 t456
1203 T t457 o b408 b456
1204 B b457 t457
1205 T t458 o453 b457
1206 B b458 t458
1207 T t459 o392 b458
1208 B b459 t459
1209 T t460 o452 b459
1210 B b460 t460
1211 P p460 Number 304
1212 P p461 Number 331
1213 O o461 location p460 p461
1214 O o462 str_open p460 p461
1215 P p462 String Refine
1216 O o463 string p462
1217 T t463 o463
1218 B b463 t463
1219 T t464 o b463 b4
1220 B b464 t464
1221 T t465 o b408 b464
1222 B b465 t465
1223 T t466 o b408 b465
1224 B b466 t466
1225 T t467 o462 b466
1226 B b467 t467
1227 T t468 o392 b467
1228 B b468 t468
1229 T t469 o461 b468
1230 B b469 t469
1231 P p469 Number 332
1232 P p470 Number 364
1233 O o470 location p469 p470
1234 O o471 str_open p469 p470
1235 P p471 String RefineError
1236 O o472 string p471
1237 T t472 o472
1238 B b472 t472
1239 T t473 o b472 b4
1240 B b473 t473
1241 T t474 o b408 b473
1242 B b474 t474
1243 T t475 o b408 b474
1244 B b475 t475
1245 T t476 o471 b475
1246 B b476 t476
1247 T t477 o392 b476
1248 B b477 t477
1249 T t478 o470 b477
1250 B b478 t478
1251 P p478 Number 365
1252 P p479 Number 381
1253 O o479 location p478 p479
1254 O o480 str_open p478 p479
1255 P p480 String Mp_resource
1256 O o481 string p480
1257 T t481 o481
1258 B b481 t481
1259 T t482 o b481 b4
1260 B b482 t482
1261 T t483 o480 b482
1262 B b483 t483
1263 T t484 o392 b483
1264 B b484 t484
1265 T t485 o479 b484
1266 B b485 t485
1267 P p485 Number 382
1268 P p486 Number 399
1269 O o486 location p485 p486
1270 O o487 str_open p485 p486
1271 P p487 String Simple_print
1272 O o488 string p487
1273 T t488 o488
1274 B b488 t488
1275 T t489 o b488 b4
1276 B b489 t489
1277 T t490 o487 b489
1278 B b490 t490
1279 T t491 o392 b490
1280 B b491 t491
1281 T t492 o486 b491
1282 B b492 t492
1283 P p492 Number 401
1284 P p493 Number 417
1285 O o493 location p492 p493
1286 O o494 str_open p492 p493
1287 P p494 String Tactic_type
1288 O o495 string p494
1289 T t495 o495
1290 B b495 t495
1291 T t496 o b495 b4
1292 B b496 t496
1293 T t497 o494 b496
1294 B b497 t497
1295 T t498 o392 b497
1296 B b498 t498
1297 T t499 o493 b498
1298 B b499 t499
1299 P p499 Number 418
1300 P p500 Number 444
1301 O o500 location p499 p500
1302 O o501 str_open p499 p500
1303 P p501 String Tacticals
1304 O o502 string p501
1305 T t502 o502
1306 B b502 t502
1307 T t503 o b502 b4
1308 B b503 t503
1309 T t504 o b495 b503
1310 B b504 t504
1311 T t505 o501 b504
1312 B b505 t505
1313 T t506 o392 b505
1314 B b506 t506
1315 T t507 o500 b506
1316 B b507 t507
1317 P p507 Number 445
1318 P p508 Number 469
1319 O o508 location p507 p508
1320 O o509 str_open p507 p508
1321 P p509 String Sequent
1322 O o510 string p509
1323 T t510 o510
1324 B b510 t510
1325 T t511 o b510 b4
1326 B b511 t511
1327 T t512 o b495 b511
1328 B b512 t512
1329 T t513 o509 b512
1330 B b513 t513
1331 T t514 o392 b513
1332 B b514 t514
1333 T t515 o508 b514
1334 B b515 t515
1335 P p515 Number 470
1336 P p516 Number 500
1337 O o516 location p515 p516
1338 O o517 str_open p515 p516
1339 P p517 String Conversionals
1340 O o518 string p517
1341 T t518 o518
1342 B b518 t518
1343 T t519 o b518 b4
1344 B b519 t519
1345 T t520 o b495 b519
1346 B b520 t520
1347 T t521 o517 b520
1348 B b521 t521
1349 T t522 o392 b521
1350 B b522 t522
1351 T t523 o516 b522
1352 B b523 t523
1353 P p523 Number 501
1354 P p524 Number 511
1355 O o524 location p523 p524
1356 O o525 str_open p523 p524
1357 O o526 string p131
1358 T t526 o526
1359 B b526 t526
1360 T t527 o b526 b4
1361 B b527 t527
1362 T t528 o525 b527
1363 B b528 t528
1364 T t529 o392 b528
1365 B b529 t529
1366 T t530 o524 b529
1367 B b530 t530
1368 P p530 Number 512
1369 P p531 Number 520
1370 O o531 location p530 p531
1371 O o532 str_open p530 p531
1372 O o533 string p129
1373 T t533 o533
1374 B b533 t533
1375 T t534 o b533 b4
1376 B b534 t534
1377 T t535 o532 b534
1378 B b535 t535
1379 T t536 o392 b535
1380 B b536 t536
1381 T t537 o531 b536
1382 B b537 t537
1383 P p537 Number 522
1384 P p538 Number 539
1385 O o538 location p537 p538
1386 O o539 str_open p537 p538
1387 O o540 string p119
1388 T t540 o540
1389 B b540 t540
1390 T t541 o b540 b4
1391 B b541 t541
1392 T t542 o539 b541
1393 B b542 t542
1394 T t543 o392 b542
1395 B b543 t543
1396 T t544 o538 b543
1397 B b544 t544
1398 P p544 Number 540
1399 P p545 Number 561
1400 O o545 location p544 p545
1401 O o546 str_open p544 p545
1402 O o547 string p121
1403 T t547 o547
1404 B b547 t547
1405 T t548 o b547 b4
1406 B b548 t548
1407 T t549 o546 b548
1408 B b549 t549
1409 T t550 o392 b549
1410 B b550 t550
1411 T t551 o545 b550
1412 B b551 t551
1413 P p551 Number 563
1414 P p552 Number 574
1415 O o552 location p551 p552
1416 NSummary!opname opname opname Summary
1417 P p553 String car
1418 O o553 opname p553
1419 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1420 NCzf_itt_group!car car car Czf_itt_group
1421 O o554 car
1422 T t554 o554
1423 B b554 t554
1424 T t555 o553 b554
1425 B b555 t555
1426 T t556 o552 b555
1427 B b556 t556
1428 P p556 Number 615
1429 P p557 Number 635
1430 O o557 location p556 p557
1431 P p558 String op
1432 O o558 opname p558
1433 NCzf_itt_group!op op op Czf_itt_group
1434 O o559 op
1435 Nvar var var NIL
1436 P p559 Var s1
1437 O o560 var p559
1438 T t560 o560
1439 B b560 t560
1440 P p560 Var s2
1441 O o561 var p560
1442 T t561 o561
1443 B b561 t561
1444 T t562 o559 b560 b561
1445 B b562 t562
1446 T t563 o558 b562
1447 B b563 t563
1448 T t564 o557 b563
1449 B b564 t564
1450 P p564 Number 636
1451 P p565 Number 646
1452 O o565 location p564 p565
1453 P p566 String id
1454 O o566 opname p566
1455 NCzf_itt_group!id id id Czf_itt_group
1456 O o567 id
1457 T t567 o567
1458 B b567 t567
1459 T t568 o566 b567
1460 B b568 t568
1461 T t569 o565 b568
1462 B b569 t569
1463 P p569 Number 647
1464 P p570 Number 662
1465 O o570 location p569 p570
1466 P p571 String inv
1467 O o571 opname p571
1468 NCzf_itt_group!inv inv inv Czf_itt_group
1469 O o572 inv
1470 P p572 Var s
1471 O o573 var p572
1472 T t573 o573
1473 B b573 t573
1474 T t574 o572 b573
1475 B b574 t574
1476 T t575 o571 b574
1477 B b575 t575
1478 T t576 o570 b575
1479 B b576 t576
1480 P p576 Number 664
1481 P p577 Number 712
1482 O o577 location p576 p577
1483 NSummary!dform dform dform Summary
1484 P p578 String car_df
1485 O o578 dform p578
1486 NSummary!except_mode_df except_mode_df except_mode_df Summary
1487 P p579 String src
1488 O o579 except_mode_df p579
1489 T t579 o579
1490 B b579 t579
1491 T t580 o b579 b4
1492 B b580 t580
1493 NSummary!df_term df_term df_term Summary
1494 O o580 df_term
1495 NPerv!string string580 string Perv
1496 P p580 String G
1497 O o581 string580 p580
1498 T t581 o581
1499 B b581 t581
1500 T t582 o b581 b4
1501 B b582 t582
1502 T t583 o580 b582
1503 B b583 t583
1504 T t584 o578 b580 b554 b583
1505 B b584 t584
1506 T t585 o577 b584
1507 B b585 t585
1508 P p585 Number 714
1509 P p586 Number 760
1510 O o586 location p585 p586
1511 P p587 String id_df
1512 O o587 dform p587
1513 P p588 String e
1514 O o588 string580 p588
1515 T t588 o588
1516 B b588 t588
1517 T t589 o b588 b4
1518 B b589 t589
1519 T t590 o580 b589
1520 B b590 t590
1521 T t591 o587 b580 b567 b590
1522 B b591 t591
1523 T t592 o586 b591
1524 B b592 t592
1525 P p592 Number 762
1526 P p593 Number 862
1527 O o593 location p592 p593
1528 P p594 String op_df
1529 O o594 dform p594
1530 NSummary!parens_df parens_df parens_df Summary
1531 O o595 parens_df
1532 T t595 o595
1533 B b595 t595
1534 T t596 o b595 b4
1535 B b596 t596
1536 T t597 o b579 b596
1537 B b597 t597
1538 Nslot slot slot NIL
1539 P p597 String le
1540 O o597 slot p597
1541 T t598 o597 b560
1542 B b598 t598
1543 P p598 String " * "
1544 O o598 string580 p598
1545 T t599 o598
1546 B b599 t599
1547 T t600 o597 b561
1548 B b600 t600
1549 T t601 o b600 b4
1550 B b601 t601
1551 T t602 o b599 b601
1552 B b602 t602
1553 T t603 o b598 b602
1554 B b603 t603
1555 T t604 o580 b603
1556 B b604 t604
1557 T t605 o594 b597 b562 b604
1558 B b605 t605
1559 T t606 o593 b605
1560 B b606 t606
1561 P p606 Number 864
1562 P p607 Number 941
1563 O o607 location p606 p607
1564 P p608 String inv_df
1565 O o608 dform p608
1566 T t608 o597 b573
1567 B b608 t608
1568 P p609 String '
1569 O o609 string580 p609
1570 T t609 o609
1571 B b609 t609
1572 T t610 o b609 b4
1573 B b610 t610
1574 T t611 o b608 b610
1575 B b611 t611
1576 T t612 o580 b611
1577 B b612 t612
1578 T t613 o608 b597 b574 b612
1579 B b613 t613
1580 T t614 o607 b613
1581 B b614 t614
1582 P p12 Number 960
1583 P p14 Number 1036
1584 O o14 location p12 p14
1585 NSummary!rule rule rule Summary
1586 P p616 String car_wf
1587 O o616 rule p616
1588 NSummary!context_param context_param context_param Summary
1589 P p617 String H
1590 O o617 context_param p617
1591 T t617 o617
1592 B b617 t617
1593 T t618 o b617 b4
1594 B b618 t618
1595 NSummary!meta_theorem meta_theorem meta_theorem Summary
1596 O o618 meta_theorem
1597 P p618 Var ext
1598 O o619 var p618
1599 T t619 o619
1600 B b619 t619
1601 T t620 o b619 b4
1602 C h H
1603 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1604 NCzf_itt_set!isset isset isset Czf_itt_set
1605 O o620 isset
1606 T t621 o620 b554
1607 S s t620 h
1608 G s t621
1609 B b621 s
1610 T t622 o618 b621
1611 B b622 t622
1612 NSummary!incomplete incomplete incomplete Summary
1613 O o622 incomplete
1614 T t623 o622
1615 B b623 t623
1616 NSummary!resource_defs resource_defs resource_defs Summary
1617 P p16 Number 982
1618 P p18 Number 989
1619 O o18 resource_defs p16 p18 p264
1620 NOcaml!uid uid uid Ocaml
1621 P p20 Number 987
1622 O o20 uid p20 p18
1623 P p626 String []
1624 O o626 uid p626
1625 T t626 o626
1626 B b626 t626
1627 T t370 o20 b626
1628 B b370 t370
1629 T t385 o b370 b4
1630 B b385 t385
1631 T t462 o18 b385
1632 B b462 t462
1633 T t470 o b462 b4
1634 B b470 t470
1635 T t525 o616 b618 b622 b623 b470
1636 B b525 t525
1637 T t531 o14 b525
1638 B b531 t531
1639 P p532 Number 1038
1640 P p533 Number 1213
1641 O o534 location p532 p533
1642 P p634 String op_wf1
1643 O o634 rule p634
1644 NSummary!meta_implies meta_implies meta_implies Summary
1645 O o635 meta_implies
1646 NBase_trivial Base_trivial Base_trivial NIL
1647 NBase_trivial!squash squash squash Base_trivial
1648 O o636 squash
1649 T t636 o636
1650 B b636 t636
1651 T t637 o b636 b4
1652 T t638 o620 b560
1653 S s638 t637 h
1654 G s638 t638
1655 B b638 s638
1656 T t639 o618 b638
1657 B b639 t639
1658 T t640 o620 b561
1659 S s640 t637 h
1660 G s640 t640
1661 B b640 s640
1662 T t641 o618 b640
1663 B b641 t641
1664 T t642 o620 b562
1665 S s642 t620 h
1666 G s642 t642
1667 B b642 s642
1668 T t643 o618 b642
1669 B b643 t643
1670 T t644 o635 b641 b643
1671 B b644 t644
1672 T t645 o635 b639 b644
1673 B b645 t645
1674 P p534 Number 1060
1675 P p535 Number 1067
1676 O o535 resource_defs p534 p535 p264
1677 P p536 Number 1065
1678 O o536 uid p536 p535
1679 T t538 o536 b626
1680 B b538 t538
1681 T t539 o b538 b4
1682 B b539 t539
1683 T t545 o535 b539
1684 B b545 t545
1685 T t546 o b545 b4
1686 B b546 t546
1687 T t552 o634 b618 b645 b623 b546
1688 B b552 t552
1689 T t553 o534 b552
1690 B b553 t553
1691 P p554 Number 1215
1692 P p555 Number 1485
1693 O o555 location p554 p555
1694 P p654 String op_wf2
1695 O o654 rule p654
1696 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1697 NCzf_itt_member!mem mem mem Czf_itt_member
1698 O o655 mem
1699 T t655 o655 b560 b554
1700 S s655 t620 h
1701 G s655 t655
1702 B b655 s655
1703 T t656 o618 b655
1704 B b656 t656
1705 T t657 o655 b561 b554
1706 S s657 t620 h
1707 G s657 t657
1708 B b657 s657
1709 T t658 o618 b657
1710 B b658 t658
1711 T t659 o655 b562 b554
1712 S s659 t620 h
1713 G s659 t659
1714 B b659 s659
1715 T t660 o618 b659
1716 B b660 t660
1717 T t661 o635 b658 b660
1718 B b661 t661
1719 T t662 o635 b656 b661
1720 B b662 t662
1721 T t663 o635 b641 b662
1722 B b663 t663
1723 T t664 o635 b639 b663
1724 B b664 t664
1725 P p561 Number 1237
1726 P p562 Number 1244
1727 O o562 resource_defs p561 p562 p264
1728 P p563 Number 1242
1729 O o563 uid p563 p562
1730 T t565 o563 b626
1731 B b565 t565
1732 T t665 o b565 b4
1733 B b665 t665
1734 T t672 o562 b665
1735 B b672 t672
1736 T t688 o b672 b4
1737 B b688 t688
1738 T t689 o654 b618 b664 b623 b688
1739 B b689 t689
1740 T t690 o555 b689
1741 B b690 t690
1742 P p690 Number 1574
1743 O o690 location p690 p269
1744 P p673 String op_eq1
1745 O o673 rule p673
1746 P p674 Var s3
1747 O o674 var p674
1748 T t674 o674
1749 B b674 t674
1750 T t675 o620 b674
1751 S s675 t637 h
1752 G s675 t675
1753 B b675 s675
1754 T t676 o618 b675
1755 B b676 t676
1756 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1757 NCzf_itt_eq!eq eq eq Czf_itt_eq
1758 O o676 eq
1759 T t677 o676 b560 b561
1760 S s677 t620 h
1761 G s677 t677
1762 B b677 s677
1763 T t678 o618 b677
1764 B b678 t678
1765 T t679 o559 b674 b560
1766 B b679 t679
1767 T t680 o559 b674 b561
1768 B b680 t680
1769 T t681 o676 b679 b680
1770 S s681 t620 h
1771 G s681 t681
1772 B b681 s681
1773 T t682 o618 b681
1774 B b682 t682
1775 T t683 o635 b678 b682
1776 B b683 t683
1777 T t684 o635 b676 b683
1778 B b684 t684
1779 T t685 o635 b641 b684
1780 B b685 t685
1781 T t686 o635 b639 b685
1782 B b686 t686
1783 P p691 Number 1596
1784 P p692 Number 1603
1785 O o692 resource_defs p691 p692 p264
1786 P p693 Number 1601
1787 O o693 uid p693 p692
1788 T t693 o693 b626
1789 B b693 t693
1790 T t704 o b693 b4
1791 B b704 t704
1792 T t705 o692 b704
1793 B b705 t705
1794 T t706 o b705 b4
1795 B b706 t706
1796 T t707 o673 b618 b686 b623 b706
1797 B b707 t707
1798 T t708 o690 b707
1799 B b708 t708
1800 P p708 Number 1853
1801 P p709 Number 2130
1802 O o709 location p708 p709
1803 P p695 String op_eq2
1804 O o695 rule p695
1805 T t695 o559 b560 b674
1806 B b695 t695
1807 T t696 o559 b561 b674
1808 B b696 t696
1809 T t697 o676 b695 b696
1810 S s697 t620 h
1811 G s697 t697
1812 B b697 s697
1813 T t698 o618 b697
1814 B b698 t698
1815 T t699 o635 b678 b698
1816 B b699 t699
1817 T t700 o635 b676 b699
1818 B b700 t700
1819 T t701 o635 b641 b700
1820 B b701 t701
1821 T t702 o635 b639 b701
1822 B b702 t702
1823 P p712 Number 1875
1824 P p713 Number 1882
1825 O o713 resource_defs p712 p713 p264
1826 P p714 Number 1880
1827 O o714 uid p714 p713
1828 T t718 o714 b626
1829 B b718 t718
1830 T t719 o b718 b4
1831 B b719 t719
1832 T t720 o713 b719
1833 B b720 t720
1834 T t721 o b720 b4
1835 B b721 t721
1836 T t722 o695 b618 b702 b623 b721
1837 B b722 t722
1838 T t723 o709 b722
1839 B b723 t723
1840 P p723 Number 2132
1841 P p724 Number 2265
1842 O o724 location p723 p724
1843 P p710 String op_fun1
1844 O o710 rule p710
1845 T t710 o620 b573
1846 S s710 t637 h
1847 G s710 t710
1848 B b710 s710
1849 T t711 o618 b710
1850 B b711 t711
1851 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1852 O o711 fun_set
1853 P p711 Var z
1854 O o712 var p711
1855 T t712 o712
1856 B b712 t712
1857 T t713 o559 b712 b573
1858 B b713 t713 z
1859 T t714 o711 b713
1860 S s714 t620 h
1861 G s714 t714
1862 B b714 s714
1863 T t715 o618 b714
1864 B b715 t715
1865 T t716 o635 b711 b715
1866 B b716 t716
1867 P p726 Number 2155
1868 P p727 Number 2162
1869 O o727 resource_defs p726 p727 p264
1870 P p728 Number 2160
1871 O o728 uid p728 p727
1872 T t730 o728 b626
1873 B b730 t730
1874 T t731 o b730 b4
1875 B b731 t731
1876 T t732 o727 b731
1877 B b732 t732
1878 T t733 o b732 b4
1879 B b733 t733
1880 T t734 o710 b618 b716 b623 b733
1881 B b734 t734
1882 T t735 o724 b734
1883 B b735 t735
1884 P p735 Number 2267
1885 P p736 Number 2400
1886 O o736 location p735 p736
1887 P p725 String op_fun2
1888 O o725 rule p725
1889 T t725 o559 b573 b712
1890 B b725 t725 z
1891 T t726 o711 b725
1892 S s726 t620 h
1893 G s726 t726
1894 B b726 s726
1895 T t727 o618 b726
1896 B b727 t727
1897 T t728 o635 b711 b727
1898 B b728 t728
1899 P p738 Number 2290
1900 P p739 Number 2297
1901 O o739 resource_defs p738 p739 p264
1902 P p740 Number 2295
1903 O o740 uid p740 p739
1904 T t750 o740 b626
1905 B b750 t750
1906 T t751 o b750 b4
1907 B b751 t751
1908 T t752 o739 b751
1909 B b752 t752
1910 T t753 o b752 b4
1911 B b753 t753
1912 T t754 o725 b618 b728 b623 b753
1913 B b754 t754
1914 T t755 o736 b754
1915 B b755 t755
1916 P p755 Number 2402
1917 P p758 Number 2795
1918 O o758 location p755 p758
1919 P p737 String op_assoc1
1920 O o737 rule p737
1921 T t737 o655 b674 b554
1922 S s737 t620 h
1923 G s737 t737
1924 B b737 s737
1925 T t738 o618 b737
1926 B b738 t738
1927 NCzf_itt_eq!equal equal equal Czf_itt_eq
1928 O o738 equal
1929 T t739 o559 b562 b674
1930 B b739 t739
1931 T t740 o559 b560 b696
1932 B b740 t740
1933 T t741 o738 b739 b740
1934 S s741 t620 h
1935 G s741 t741
1936 B b741 s741
1937 T t742 o618 b741
1938 B b742 t742
1939 T t743 o635 b738 b742
1940 B b743 t743
1941 T t744 o635 b658 b743
1942 B b744 t744
1943 T t745 o635 b656 b744
1944 B b745 t745
1945 T t746 o635 b676 b745
1946 B b746 t746
1947 T t747 o635 b641 b746
1948 B b747 t747
1949 T t748 o635 b639 b747
1950 B b748 t748
1951 P p759 Number 2427
1952 P p760 Number 2434
1953 O o760 resource_defs p759 p760 p264
1954 P p761 Number 2432
1955 O o761 uid p761 p760
1956 T t766 o761 b626
1957 B b766 t766
1958 T t767 o b766 b4
1959 B b767 t767
1960 T t768 o760 b767
1961 B b768 t768
1962 T t769 o b768 b4
1963 B b769 t769
1964 T t770 o737 b618 b748 b623 b769
1965 B b770 t770
1966 T t771 o758 b770
1967 B b771 t771
1968 P p771 Number 2797
1969 P p772 Number 3190
1970 O o772 location p771 p772
1971 P p757 String op_assoc2
1972 O o757 rule p757
1973 T t757 o738 b740 b739
1974 S s757 t620 h
1975 G s757 t757
1976 B b757 s757
1977 T t758 o618 b757
1978 B b758 t758
1979 T t759 o635 b738 b758
1980 B b759 t759
1981 T t760 o635 b658 b759
1982 B b760 t760
1983 T t761 o635 b656 b760
1984 B b761 t761
1985 T t762 o635 b676 b761
1986 B b762 t762
1987 T t763 o635 b641 b762
1988 B b763 t763
1989 T t764 o635 b639 b763
1990 B b764 t764
1991 P p774 Number 2822
1992 P p775 Number 2829
1993 O o775 resource_defs p774 p775 p264
1994 P p776 Number 2827
1995 O o776 uid p776 p775
1996 T t776 o776 b626
1997 B b776 t776
1998 T t777 o b776 b4
1999 B b777 t777
2000 T t778 o775 b777
2001 B b778 t778
2002 T t779 o b778 b4
2003 B b779 t779
2004 T t780 o757 b618 b764 b623 b779
2005 B b780 t780
2006 T t781 o772 b780
2007 B b781 t781
2008 P p781 Number 3192
2009 P p782 Number 3268
2010 O o782 location p781 p782
2011 P p773 String id_wf1
2012 O o773 rule p773
2013 T t773 o620 b567
2014 S s773 t620 h
2015 G s773 t773
2016 B b773 s773
2017 T t774 o618 b773
2018 B b774 t774
2019 P p784 Number 3214
2020 P p785 Number 3222
2021 O o785 resource_defs p784 p785 p264
2022 P p786 Number 3220
2023 O o786 uid p786 p785
2024 T t786 o786 b626
2025 B b786 t786
2026 T t787 o b786 b4
2027 B b787 t787
2028 T t788 o785 b787
2029 B b788 t788
2030 T t789 o b788 b4
2031 B b789 t789
2032 T t790 o773 b618 b774 b623 b789
2033 B b790 t790
2034 T t791 o782 b790
2035 B b791 t791
2036 P p791 Number 3270
2037 P p792 Number 3348
2038 O o792 location p791 p792
2039 P p783 String id_wf2
2040 O o783 rule p783
2041 T t783 o655 b567 b554
2042 S s783 t620 h
2043 G s783 t783
2044 B b783 s783
2045 T t784 o618 b783
2046 B b784 t784
2047 P p795 Number 3292
2048 P p796 Number 3299
2049 O o796 resource_defs p795 p796 p264
2050 P p797 Number 3297
2051 O o797 uid p797 p796
2052 T t801 o797 b626
2053 B b801 t801
2054 T t802 o b801 b4
2055 B b802 t802
2056 T t803 o796 b802
2057 B b803 t803
2058 T t804 o b803 b4
2059 B b804 t804
2060 T t805 o783 b618 b784 b623 b804
2061 B b805 t805
2062 T t806 o792 b805
2063 B b806 t806
2064 P p806 Number 3350
2065 P p807 Number 3526
2066 O o807 location p806 p807
2067 P p793 String id_eq1
2068 O o793 rule p793
2069 T t793 o655 b573 b554
2070 S s793 t620 h
2071 G s793 t793
2072 B b793 s793
2073 T t794 o618 b793
2074 B b794 t794
2075 T t795 o559 b567 b573
2076 B b795 t795
2077 T t796 o738 b795 b573
2078 S s796 t620 h
2079 G s796 t796
2080 B b796 s796
2081 T t797 o618 b796
2082 B b797 t797
2083 T t798 o635 b794 b797
2084 B b798 t798
2085 T t799 o635 b711 b798
2086 B b799 t799
2087 P p809 Number 3372
2088 P p810 Number 3379
2089 O o810 resource_defs p809 p810 p264
2090 P p811 Number 3377
2091 O o811 uid p811 p810
2092 T t814 o811 b626
2093 B b814 t814
2094 T t815 o b814 b4
2095 B b815 t815
2096 T t816 o810 b815
2097 B b816 t816
2098 T t817 o b816 b4
2099 B b817 t817
2100 T t818 o793 b618 b799 b623 b817
2101 B b818 t818
2102 T t819 o807 b818
2103 B b819 t819
2104 P p819 Number 3528
2105 P p820 Number 3704
2106 O o820 location p819 p820
2107 P p808 String id_eq2
2108 O o808 rule p808
2109 T t808 o559 b573 b567
2110 B b808 t808
2111 T t809 o738 b808 b573
2112 S s809 t620 h
2113 G s809 t809
2114 B b809 s809
2115 T t810 o618 b809
2116 B b810 t810
2117 T t811 o635 b794 b810
2118 B b811 t811
2119 T t812 o635 b711 b811
2120 B b812 t812
2121 P p821 Number 3550
2122 P p822 Number 3557
2123 O o822 resource_defs p821 p822 p264
2124 P p823 Number 3555
2125 O o823 uid p823 p822
2126 T t823 o823 b626
2127 B b823 t823
2128 T t824 o b823 b4
2129 B b824 t824
2130 T t832 o822 b824
2131 B b832 t832
2132 T t837 o b832 b4
2133 B b837 t837
2134 T t839 o808 b618 b812 b623 b837
2135 B b839 t839
2136 T t840 o820 b839
2137 B b840 t840
2138 P p840 Number 3706
2139 P p842 Number 3879
2140 O o842 location p840 p842
2141 NOcaml!str_let str_let str_let Ocaml
2142 NOcaml!patt_var patt_var patt_var Ocaml
2143 NOcaml!patt_done patt_done patt_done Ocaml
2144 NOcaml!fun fun fun Ocaml
2145 NOcaml!patt_if patt_if patt_if Ocaml
2146 NOcaml!patt_body patt_body patt_body Ocaml
2147 NOcaml!apply apply apply Ocaml
2148 NOcaml!lid lid lid Ocaml
2149 NOcaml!proj proj proj Ocaml
2150 O o836 uid p509
2151 T t836 o836
2152 B b836 t836
2153 P p838 String hyp_count_addr
2154 O o838 lid p838
2155 T t838 o838
2156 B b838 t838
2157 P p841 Var p
2158 O o841 var p841
2159 T t841 o841
2160 B b841 t841
2161 P p857 String inv_wf1
2162 O o857 rule p857
2163 T t857 o572 b560
2164 B b857 t857
2165 T t858 o620 b857
2166 S s858 t620 h
2167 G s858 t858
2168 B b858 s858
2169 T t859 o618 b858
2170 B b859 t859
2171 T t860 o635 b656 b859
2172 B b860 t860
2173 T t861 o635 b639 b860
2174 B b861 t861
2175 P p843 Number 3729
2176 P p844 Number 3736
2177 O o844 resource_defs p843 p844 p264
2178 P p845 Number 3734
2179 O o845 uid p845 p844
2180 T t845 o845 b626
2181 B b845 t845
2182 T t846 o b845 b4
2183 B b846 t846
2184 T t847 o844 b846
2185 B b847 t847
2186 T t848 o b847 b4
2187 B b848 t848
2188 T t849 o857 b618 b861 b623 b848
2189 B b849 t849
2190 T t850 o842 b849
2191 B b850 t850
2192 P p850 Number 3881
2193 P p851 Number 4057
2194 O o851 location p850 p851
2195 P p870 String inv_wf2
2196 O o870 rule p870
2197 T t870 o655 b857 b554
2198 S s870 t620 h
2199 G s870 t870
2200 B b870 s870
2201 T t871 o618 b870
2202 B b871 t871
2203 T t872 o635 b656 b871
2204 B b872 t872
2205 T t873 o635 b639 b872
2206 B b873 t873
2207 P p852 Number 3904
2208 P p853 Number 3911
2209 O o853 resource_defs p852 p853 p264
2210 P p854 Number 3909
2211 O o854 uid p854 p853
2212 T t854 o854 b626
2213 B b854 t854
2214 T t855 o b854 b4
2215 B b855 t855
2216 T t856 o853 b855
2217 B b856 t856
2218 T t862 o b856 b4
2219 B b862 t862
2220 T t863 o870 b618 b873 b623 b862
2221 B b863 t863
2222 T t864 o851 b863
2223 B b864 t864
2224 P p864 Number 4059
2225 P p865 Number 4146
2226 O o865 location p864 p865
2227 P p882 String inv_fun1
2228 O o882 rule p882
2229 T t882 o572 b712
2230 B b882 t882 z
2231 T t883 o711 b882
2232 S s883 t620 h
2233 G s883 t883
2234 B b883 s883
2235 T t884 o618 b883
2236 B b884 t884
2237 P p866 Number 4083
2238 P p867 Number 4090
2239 O o867 resource_defs p866 p867 p264
2240 P p868 Number 4088
2241 O o868 uid p868 p867
2242 T t868 o868 b626
2243 B b868 t868
2244 T t869 o b868 b4
2245 B b869 t869
2246 T t874 o867 b869
2247 B b874 t874
2248 T t875 o b874 b4
2249 B b875 t875
2250 T t876 o882 b618 b884 b623 b875
2251 B b876 t876
2252 T t877 o865 b876
2253 B b877 t877
2254 P p877 Number 4148
2255 P p878 Number 4334
2256 O o878 location p877 p878
2257 P p1840 Number 4366
2258 P p1894 Number 4617
2259 P p893 String inv_id1
2260 O o893 rule p893
2261 T t893 o559 b857 b560
2262 B b893 t893
2263 T t894 o738 b893 b567
2264 S s894 t620 h
2265 G s894 t894
2266 B b894 s894
2267 T t895 o618 b894
2268 B b895 t895
2269 T t896 o635 b656 b895
2270 B b896 t896
2271 T t897 o635 b639 b896
2272 B b897 t897
2273 P p879 Number 4171
2274 P p880 Number 4178
2275 O o880 resource_defs p879 p880 p264
2276 P p881 Number 4176
2277 O o881 uid p881 p880
2278 T t881 o881 b626
2279 B b881 t881
2280 T t885 o b881 b4
2281 B b885 t885
2282 T t886 o880 b885
2283 B b886 t886
2284 T t887 o b886 b4
2285 B b887 t887
2286 T t888 o893 b618 b897 b623 b887
2287 B b888 t888
2288 T t889 o878 b888
2289 B b889 t889
2290 P p889 Number 4336
2291 P p890 Number 4522
2292 O o890 location p889 p890
2293 P p1907 Number 4619
2294 P p906 String inv_id2
2295 O o906 rule p906
2296 T t906 o559 b560 b857
2297 B b906 t906
2298 T t907 o738 b906 b567
2299 S s907 t620 h
2300 G s907 t907
2301 B b907 s907
2302 T t908 o618 b907
2303 B b908 t908
2304 T t909 o635 b656 b908
2305 B b909 t909
2306 T t910 o635 b639 b909
2307 B b910 t910
2308 P p891 Number 4359
2309 O o891 resource_defs p891 p1840 p264
2310 P p892 Number 4364
2311 O o892 uid p892 p1840
2312 T t892 o892 b626
2313 B b892 t892
2314 T t898 o b892 b4
2315 B b898 t898
2316 T t899 o891 b898
2317 B b899 t899
2318 T t900 o b899 b4
2319 B b900 t900
2320 T t901 o906 b618 b910 b623 b900
2321 B b901 t901
2322 T t902 o890 b901
2323 B b902 t902
2324 P p902 Number 4588
2325 P p903 Number 5014
2326 O o903 location p902 p903
2327 P p919 String cancel1
2328 O o919 rule p919
2329 NSummary!term_param term_param term_param Summary
2330 O o920 term_param
2331 T t920 o920 b560
2332 B b920 t920
2333 T t921 o b920 b4
2334 B b921 t921
2335 T t922 o b617 b921
2336 B b922 t922
2337 T t923 o738 b562 b695
2338 S s923 t620 h
2339 G s923 t923
2340 B b923 s923
2341 T t924 o618 b923
2342 B b924 t924
2343 T t925 o738 b561 b674
2344 S s925 t620 h
2345 G s925 t925
2346 B b925 s925
2347 T t926 o618 b925
2348 B b926 t926
2349 T t927 o635 b924 b926
2350 B b927 t927
2351 T t928 o635 b738 b927
2352 B b928 t928
2353 T t929 o635 b658 b928
2354 B b929 t929
2355 T t930 o635 b656 b929
2356 B b930 t930
2357 T t931 o635 b676 b930
2358 B b931 t931
2359 T t932 o635 b641 b931
2360 B b932 t932
2361 T t933 o635 b639 b932
2362 B b933 t933
2363 NSummary!interactive interactive interactive Summary
2364 O o933 interactive
2365 NSummary!ext_rule ext_rule ext_rule Summary
2366 P p933 String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2367 O o934 ext_rule p933
2368 NSummary!status_incomplete status_incomplete status_incomplete Summary
2369 O o935 status_incomplete
2370 T t935 o935
2371 B b935 t935
2372 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2373 O o936 ext_unjustified
2374 NSummary!tactic_arg tactic_arg tactic_arg Summary
2375 P p936 String main
2376 O o937 tactic_arg p936
2377 NSummary!msequent msequent msequent Summary
2378 O o938 msequent
2379 T t938 o b923 b4
2380 B b938 t938
2381 T t939 o b737 b938
2382 B b939 t939
2383 T t940 o b657 b939
2384 B b940 t940
2385 T t941 o b655 b940
2386 B b941 t941
2387 T t942 o b675 b941
2388 B b942 t942
2389 T t943 o b640 b942
2390 B b943 t943
2391 T t944 o b638 b943
2392 B b944 t944
2393 T t945 o938 b925 b944
2394 B b945 t945
2395 NSummary!parent_none parent_none parent_none Summary
2396 O o945 parent_none
2397 T t946 o945
2398 B b946 t946
2399 T t947 o937 b945 b4 b946
2400 B b947 t947
2401 P p947 String assertion
2402 O o947 tactic_arg p947
2403 H h947 v t923
2404 T t948 o559 b857 b562
2405 B b948 t948
2406 T t949 o559 b857 b695
2407 B b949 t949
2408 T t950 o738 b948 b949
2409 S s950 t620 h h947
2410 G s950 t950
2411 B b950 s950
2412 T t951 o938 b950 b944
2413 B b951 t951
2414 S s951 t620 h h947
2415 G s951 t925
2416 B b952 s951
2417 T t952 o938 b952 b944
2418 B b953 t952
2419 T t953 o2 b947
2420 B b954 t953
2421 T t954 o937 b953 b4 b954
2422 B b955 t954
2423 T t955 o2 b955
2424 B b956 t955
2425 T t956 o947 b951 b4 b956
2426 B b957 t956
2427 H h957 v_1 t950
2428 S s957 t620 h h947 h957
2429 G s957 t925
2430 B b958 s957
2431 T t958 o938 b958 b944
2432 B b959 t958
2433 T t959 o937 b959 b4 b956
2434 B b960 t959
2435 T t960 o b960 b4
2436 B b961 t960
2437 T t961 o b957 b961
2438 B b962 t961
2439 T t962 o936 b947 b962
2440 B b963 t962
2441 P p963 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2442 O o963 ext_rule p963
2443 T t963 o936 b957 b4
2444 B b964 t963
2445 T t964 o963 b935 b964 b4 b4
2446 B b965 t964
2447 P p965 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2448 O o965 ext_rule p965
2449 P p966 String eq
2450 O o966 tactic_arg p966
2451 T t966 o559 b893 b561
2452 B b966 t966
2453 T t967 o738 b948 b966
2454 S s967 t620 h h947 h957
2455 G s967 t967
2456 B b967 s967
2457 T t968 o938 b967 b944
2458 B b968 t968
2459 T t969 o2 b960
2460 B b969 t969
2461 T t970 o966 b968 b4 b969
2462 B b970 t970
2463 T t971 o738 b966 b949
2464 H h971 v_2 t971
2465 S s971 t620 h h947 h957 h971
2466 G s971 t925
2467 B b971 s971
2468 T t972 o938 b971 b944
2469 B b972 t972
2470 T t973 o937 b972 b4 b969
2471 B b973 t973
2472 T t1 o b973 b4
2473 B b1 t1
2474 T t2 o b970 b1
2475 B b2 t2
2476 T t3 o936 b960 b2
2477 B b3 t3
2478 P p973 String wf
2479 O o973 tactic_arg p973
2480 B b974 t949 v_2
2481 T t974 o711 b974
2482 S s974 t620 h h947 h957
2483 G s974 t974
2484 B b975 s974
2485 T t975 o938 b975 b944
2486 B b976 t975
2487 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2488 O o976 fun_prop
2489 P p976 Var v_2
2490 O o977 var p976
2491 T t977 o977
2492 B b977 t977
2493 T t978 o738 b977 b949
2494 B b978 t978 v_2
2495 T t979 o976 b978
2496 S s979 t620 h h947 h957
2497 G s979 t979
2498 B b979 s979
2499 T t980 o938 b979 b944
2500 B b980 t980
2501 NSummary!arg_named arg_named arg_named Summary
2502 P p980 String d_auto
2503 O o980 arg_named p980
2504 NSummary!arg_bool arg_bool arg_bool Summary
2505 P p981 String true
2506 O o981 arg_bool p981
2507 T t981 o981
2508 B b981 t981
2509 T t982 o980 b981
2510 B b982 t982
2511 T t983 o b982 b4
2512 B b983 t983
2513 T t984 o973 b980 b983 b969
2514 B b984 t984
2515 T t985 o2 b984
2516 B b985 t985
2517 T t986 o973 b976 b4 b985
2518 B b986 t986
2519 P p990 String autoT
2520 O o990 ext_rule p990
2521 T t991 o936 b970 b4
2522 B b991 t991
2523 T t992 o990 b935 b991 b4 b4
2524 B b992 t992
2525 P p992 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2526 O o992 ext_rule p992
2527 T t993 o559 b893 b674
2528 B b993 t993
2529 T t994 o738 b949 b993
2530 S s994 t620 h h947 h957 h971
2531 G s994 t994
2532 B b994 s994
2533 T t995 o938 b994 b944
2534 B b995 t995
2535 T t996 o2 b973
2536 B b996 t996
2537 T t997 o966 b995 b4 b996
2538 B b997 t997
2539 T t998 o738 b966 b993
2540 H h998 v_3 t998
2541 S s998 t620 h h947 h957 h971 h998
2542 G s998 t925
2543 B b998 s998
2544 T t999 o938 b998 b944
2545 B b999 t999
2546 T t1000 o937 b999 b4 b996
2547 B b1000 t1000
2548 T t214 o b1000 b4
2549 B b214 t214
2550 T t215 o b997 b214
2551 B b215 t215
2552 T t218 o936 b973 b215
2553 B b218 t218
2554 B b1001 t966 v_3
2555 T t1001 o711 b1001
2556 S s1001 t620 h h947 h957 h971
2557 G s1001 t1001
2558 B b1002 s1001
2559 T t1002 o938 b1002 b944
2560 B b1003 t1002
2561 P p1003 Var v_3
2562 O o1003 var p1003
2563 T t1003 o1003
2564 B b1004 t1003
2565 T t1004 o738 b966 b1004
2566 B b1005 t1004 v_3
2567 T t1005 o976 b1005
2568 S s1005 t620 h h947 h957 h971
2569 G s1005 t1005
2570 B b1006 s1005
2571 T t1006 o938 b1006 b944
2572 B b1007 t1006
2573 T t1007 o973 b1007 b983 b996
2574 B b1008 t1007
2575 T t1008 o2 b1008
2576 B b1009 t1008
2577 T t1009 o973 b1003 b4 b1009
2578 B b1010 t1009
2579 T t1014 o936 b997 b4
2580 B b1015 t1014
2581 T t1015 o990 b935 b1015 b4 b4
2582 B b1016 t1015
2583 P p1016 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2584 O o1016 ext_rule p1016
2585 T t1016 o559 b567 b561
2586 B b1017 t1016
2587 T t1017 o559 b567 b674
2588 B b1018 t1017
2589 T t1018 o738 b1017 b1018
2590 H h1018 v_4 t1018
2591 S s1018 t620 h h947 h957 h971 h998 h1018
2592 G s1018 t925
2593 B b1019 s1018
2594 T t1019 o938 b1019 b944
2595 B b1020 t1019
2596 T t1020 o2 b1000
2597 B b1021 t1020
2598 T t1021 o937 b1020 b4 b1021
2599 B b1022 t1021
2600 T t1022 o b1022 b4
2601 B b1023 t1022
2602 T t1023 o936 b1000 b1023
2603 B b1024 t1023
2604 P p1024 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2605 O o1024 ext_rule p1024
2606 T t1024 o738 b561 b1018
2607 H h1024 v_5 t1024
2608 S s1024 t620 h h947 h957 h971 h998 h1018 h1024
2609 G s1024 t925
2610 B b1025 s1024
2611 T t1025 o938 b1025 b944
2612 B b1026 t1025
2613 T t1026 o2 b1022
2614 B b1027 t1026
2615 T t1027 o937 b1026 b4 b1027
2616 B b1028 t1027
2617 T t219 o b1028 b4
2618 B b219 t219
2619 T t229 o936 b1022 b219
2620 B b229 t229
2621 B b1029 t1017 v_5
2622 T t1029 o711 b1029
2623 S s1029 t620 h h947 h957 h971 h998 h1018
2624 G s1029 t1029
2625 B b1030 s1029
2626 T t1030 o938 b1030 b944
2627 B b1031 t1030
2628 P p1031 Var v_5
2629 O o1031 var p1031
2630 T t1031 o1031
2631 B b1032 t1031
2632 T t1032 o738 b1032 b1018
2633 B b1033 t1032 v_5
2634 T t1033 o976 b1033
2635 S s1033 t620 h h947 h957 h971 h998 h1018
2636 G s1033 t1033
2637 B b1034 s1033
2638 T t1034 o938 b1034 b944
2639 B b1035 t1034
2640 T t1035 o973 b1035 b983 b1027
2641 B b1036 t1035
2642 T t1036 o2 b1036
2643 B b1037 t1036
2644 T t1037 o973 b1031 b4 b1037
2645 B b1038 t1037
2646 P p1041 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2647 O o1041 ext_rule p1041
2648 H h1041 v_6 t925
2649 S s1041 t620 h h947 h957 h971 h998 h1018 h1024 h1041
2650 G s1041 t925
2651 B b1042 s1041
2652 T t1042 o938 b1042 b944
2653 B b1043 t1042
2654 T t1043 o2 b1028
2655 B b1044 t1043
2656 T t1044 o937 b1043 b4 b1044
2657 B b1045 t1044
2658 T t1045 o b1045 b4
2659 B b1046 t1045
2660 T t1046 o936 b1028 b1046
2661 B b1047 t1046
2662 P p1047 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2663 O o1047 ext_rule p1047
2664 T t1047 o936 b1045 b4
2665 B b1048 t1047
2666 T t1048 o1047 b935 b1048 b4 b4
2667 B b1049 t1048
2668 T t1049 o b1049 b4
2669 B b1050 t1049
2670 P p1050 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2671 O o1050 ext_rule p1050
2672 B b1051 t1016 v_6
2673 T t1051 o711 b1051
2674 S s1051 t620 h h947 h957 h971 h998 h1018 h1024
2675 G s1051 t1051
2676 B b1052 s1051
2677 T t1052 o938 b1052 b944
2678 B b1053 t1052
2679 P p1053 Var v_6
2680 O o1053 var p1053
2681 T t1053 o1053
2682 B b1054 t1053
2683 T t1054 o738 b1017 b1054
2684 B b1055 t1054 v_6
2685 T t1055 o976 b1055
2686 S s1055 t620 h h947 h957 h971 h998 h1018 h1024
2687 G s1055 t1055
2688 B b1056 s1055
2689 T t1056 o938 b1056 b944
2690 B b1057 t1056
2691 T t1057 o973 b1057 b983 b1044
2692 B b1058 t1057
2693 T t1058 o2 b1058
2694 B b1059 t1058
2695 T t1059 o973 b1053 b4 b1059
2696 B b1060 t1059
2697 T t1060 o936 b1060 b4
2698 B b1061 t1060
2699 T t1061 o1050 b935 b1061 b4 b4
2700 B b1062 t1061
2701 T t1062 o b1062 b4
2702 B b1063 t1062
2703 T t1063 o1041 b935 b1047 b1050 b1063
2704 B b1064 t1063
2705 T t230 o b1064 b4
2706 B b230 t230
2707 T t1064 o936 b1038 b4
2708 B b1065 t1064
2709 T t1065 o1050 b935 b1065 b4 b4
2710 B b1066 t1065
2711 T t1066 o b1066 b4
2712 B b1067 t1066
2713 T t233 o1024 b935 b229 b230 b1067
2714 B b233 t233
2715 T t237 o b233 b4
2716 B b237 t237
2717 T t238 o1016 b935 b1024 b237 b4
2718 B b238 t238
2719 T t239 o b238 b4
2720 B b239 t239
2721 T t242 o b1016 b239
2722 B b242 t242
2723 P p1071 String "rwh unfold_fun_set 0 thenT autoT"
2724 O o1071 ext_rule p1071
2725 T t1071 o936 b1010 b4
2726 B b1072 t1071
2727 T t1072 o1071 b935 b1072 b4 b4
2728 B b1073 t1072
2729 T t1073 o b1073 b4
2730 B b1074 t1073
2731 T t243 o992 b935 b218 b242 b1074
2732 B b243 t243
2733 T t251 o b243 b4
2734 B b251 t251
2735 T t256 o b992 b251
2736 B b256 t256
2737 T t1077 o936 b986 b4
2738 B b1078 t1077
2739 T t1078 o1071 b935 b1078 b4 b4
2740 B b1079 t1078
2741 T t1079 o b1079 b4
2742 B b1080 t1079
2743 T t257 o965 b935 b3 b256 b1080
2744 B b257 t257
2745 T t265 o b257 b4
2746 B b265 t265
2747 T t266 o b965 b265
2748 B b266 t266
2749 NSummary!ext_goal ext_goal ext_goal Summary
2750 O o1085 ext_goal
2751 S s1085 t620 h
2752 G s1085 t950
2753 B b1086 s1085
2754 T t1086 o938 b1086 b944
2755 B b1087 t1086
2756 T t1087 o947 b1087 b4 b954
2757 B b1088 t1087
2758 T t1088 o1085 b1088
2759 B b1089 t1088
2760 T t1089 o b1089 b4
2761 B b1090 t1089
2762 T t1090 o963 b935 b1089 b1090 b4
2763 B b1091 t1090
2764 P p1091 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2765 O o1091 ext_rule p1091
2766 H h1091 v t950
2767 S s1091 t620 h h1091
2768 G s1091 t925
2769 B b1092 s1091
2770 T t1092 o938 b1092 b944
2771 B b1093 t1092
2772 T t1093 o937 b1093 b4 b954
2773 B b1094 t1093
2774 T t1094 o1085 b1094
2775 B b1095 t1094
2776 P p1095 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2777 O o1095 ext_rule p1095
2778 P p1096 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2779 O o1096 ext_rule p1096
2780 T t1096 o b1095 b4
2781 B b1096 t1096
2782 H h1096 x t923
2783 H h1097 v_1 t971
2784 H h1098 v_2 t998
2785 H h1099 v_3 t1018
2786 H h1100 v_4 t1024
2787 B b1100 t1016 v_5
2788 T t1100 o711 b1100
2789 S s1100 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2790 G s1100 t1100
2791 B b1101 s1100
2792 T t1101 o b737 b4
2793 B b1102 t1101
2794 T t1102 o b657 b1102
2795 B b1103 t1102
2796 T t1103 o b655 b1103
2797 B b1104 t1103
2798 T t1104 o b675 b1104
2799 B b1105 t1104
2800 T t1105 o b640 b1105
2801 B b1106 t1105
2802 T t1106 o b638 b1106
2803 B b1107 t1106
2804 T t1107 o938 b1101 b1107
2805 B b1108 t1107
2806 T t1108 o738 b1017 b1032
2807 B b1109 t1108 v_5
2808 T t1109 o976 b1109
2809 S s1109 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2810 G s1109 t1109
2811 B b1110 s1109
2812 T t1110 o938 b1110 b1107
2813 B b1111 t1110
2814 S s1111 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2815 G s1111 t925
2816 B b1112 s1111
2817 T t1112 o938 b1112 b1107
2818 B b1113 t1112
2819 S s1113 t620 h h1096 h1091 h1097 h1098 h1099
2820 G s1113 t925
2821 B b1114 s1113
2822 T t1114 o938 b1114 b1107
2823 B b1115 t1114
2824 S s1115 t620 h h1096 h1091 h1097 h1098
2825 G s1115 t925
2826 B b1116 s1115
2827 T t1116 o938 b1116 b1107
2828 B b1117 t1116
2829 S s1117 t620 h h1096 h1091 h1097
2830 G s1117 t925
2831 B b1118 s1117
2832 T t1118 o938 b1118 b1107
2833 B b1119 t1118
2834 S s1119 t620 h h1096 h1091
2835 G s1119 t925
2836 B b1120 s1119
2837 T t1120 o938 b1120 b1107
2838 B b1121 t1120
2839 S s1121 t620 h h1096
2840 G s1121 t925
2841 B b1122 s1121
2842 T t1122 o938 b1122 b1107
2843 B b1123 t1122
2844 T t1123 o937 b1123 b4 b946
2845 B b1124 t1123
2846 T t1124 o2 b1124
2847 B b1125 t1124
2848 T t1125 o937 b1121 b4 b1125
2849 B b1126 t1125
2850 T t1126 o2 b1126
2851 B b1127 t1126
2852 T t1127 o937 b1119 b4 b1127
2853 B b1128 t1127
2854 T t1128 o2 b1128
2855 B b1129 t1128
2856 T t1129 o937 b1117 b4 b1129
2857 B b1130 t1129
2858 T t1130 o2 b1130
2859 B b1131 t1130
2860 T t1131 o937 b1115 b4 b1131
2861 B b1132 t1131
2862 T t1132 o2 b1132
2863 B b1133 t1132
2864 T t1133 o937 b1113 b4 b1133
2865 B b1134 t1133
2866 T t1134 o2 b1134
2867 B b1135 t1134
2868 T t1135 o973 b1111 b983 b1135
2869 B b1136 t1135
2870 T t1136 o2 b1136
2871 B b1137 t1136
2872 T t1137 o973 b1108 b4 b1137
2873 B b1138 t1137
2874 T t1138 o936 b1138 b4
2875 B b1139 t1138
2876 T t1139 o1050 b935 b1139 b4 b4
2877 B b1140 t1139
2878 T t1140 o b1140 b4
2879 B b1141 t1140
2880 T t1141 o1096 b935 b1095 b1096 b1141
2881 B b1142 t1141
2882 T t1142 o b1142 b4
2883 B b1143 t1142
2884 B b1144 t1017 v_4
2885 T t1144 o711 b1144
2886 S s1144 t620 h h1096 h1091 h1097 h1098 h1099
2887 G s1144 t1144
2888 B b1145 s1144
2889 T t1145 o938 b1145 b1107
2890 B b1146 t1145
2891 P p1146 Var v_4
2892 O o1146 var p1146
2893 T t1146 o1146
2894 B b1147 t1146
2895 T t1147 o738 b1147 b1018
2896 B b1148 t1147 v_4
2897 T t1148 o976 b1148
2898 S s1148 t620 h h1096 h1091 h1097 h1098 h1099
2899 G s1148 t1148
2900 B b1149 s1148
2901 T t1149 o938 b1149 b1107
2902 B b1150 t1149
2903 T t1150 o973 b1150 b983 b1133
2904 B b1151 t1150
2905 T t1151 o2 b1151
2906 B b1152 t1151
2907 T t1152 o973 b1146 b4 b1152
2908 B b1153 t1152
2909 T t1153 o936 b1153 b4
2910 B b1154 t1153
2911 T t1154 o1050 b935 b1154 b4 b4
2912 B b1155 t1154
2913 T t1155 o b1155 b4
2914 B b1156 t1155
2915 T t1156 o1024 b935 b1095 b1143 b1156
2916 B b1157 t1156
2917 T t1157 o b1157 b4
2918 B b1158 t1157
2919 T t1158 o1016 b935 b1095 b1158 b4
2920 B b1159 t1158
2921 T t1159 o b1159 b4
2922 B b1160 t1159
2923 S s1160 t620 h h1096 h1091 h1097
2924 G s1160 t994
2925 B b1161 s1160
2926 T t1161 o938 b1161 b1107
2927 B b1162 t1161
2928 T t1162 o966 b1162 b4 b1129
2929 B b1163 t1162
2930 T t1163 o936 b1163 b4
2931 B b1164 t1163
2932 T t1164 o990 b935 b1164 b4 b4
2933 B b1165 t1164
2934 P p1165 String "rwh unfold_fun_prop 0 thenT autoT"
2935 O o1165 ext_rule p1165
2936 T t1165 o738 b966 b977
2937 B b1166 t1165 v_2
2938 T t1166 o976 b1166
2939 S s1166 t620 h h1096 h1091 h1097
2940 G s1166 t1166
2941 B b1167 s1166
2942 T t1167 o938 b1167 b1107
2943 B b1168 t1167
2944 T t1168 o973 b1168 b4 b1129
2945 B b1169 t1168
2946 NCzf_itt_set!set set set Czf_itt_set
2947 O o1169 set
2948 T t1169 o1169
2949 H h1169 s1_1 t1169
2950 H h1170 s2_1 t1169
2951 P p1170 Var s1_1
2952 O o1170 var p1170
2953 T t1170 o1170
2954 B b1170 t1170
2955 P p1171 Var s2_1
2956 O o1171 var p1171
2957 T t1171 o1171
2958 B b1171 t1171
2959 T t1172 o738 b1170 b1171
2960 H h1172 x_1 t1172
2961 T t1173 o738 b966 b1170
2962 H h1173 x_2 t1173
2963 T t1174 o676 b966 b1171
2964 S s1174 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
2965 G s1174 t1174
2966 B b1174 s1174
2967 T t1175 o938 b1174 b1107
2968 B b1175 t1175
2969 T t1176 o738 b966 b1171
2970 S s1176 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
2971 G s1176 t1176
2972 B b1176 s1176
2973 T t1177 o938 b1176 b1107
2974 B b1177 t1177
2975 NItt_logic Itt_logic Itt_logic NIL
2976 NItt_logic!implies implies implies Itt_logic
2977 O o1177 implies
2978 B b1178 t1173
2979 B b1179 t1176
2980 T t1179 o1177 b1178 b1179
2981 S s1179 t620 h h1096 h1091 h1097 h1169 h1170 h1172
2982 G s1179 t1179
2983 B b1180 s1179
2984 T t1180 o938 b1180 b1107
2985 B b1181 t1180
2986 B b1182 t1172
2987 B b1183 t1179
2988 T t1183 o1177 b1182 b1183
2989 S s1183 t620 h h1096 h1091 h1097 h1169 h1170
2990 G s1183 t1183
2991 B b1184 s1183
2992 T t1184 o938 b1184 b1107
2993 B b1185 t1184
2994 NItt_logic!all all all Itt_logic
2995 O o1185 all
2996 B b1186 t1169
2997 B b1187 t1183 s2_1
2998 T t1187 o1185 b1186 b1187
2999 S s1187 t620 h h1096 h1091 h1097 h1169
3000 G s1187 t1187
3001 B b1188 s1187
3002 T t1188 o938 b1188 b1107
3003 B b1189 t1188
3004 B b1190 t1187 s1_1
3005 T t1190 o1185 b1186 b1190
3006 S s1190 t620 h h1096 h1091 h1097
3007 G s1190 t1190
3008 B b1191 s1190
3009 T t1191 o938 b1191 b1107
3010 B b1192 t1191
3011 T t1192 o2 b1169
3012 B b1193 t1192
3013 T t1193 o973 b1192 b983 b1193
3014 B b1194 t1193
3015 T t1194 o2 b1194
3016 B b1195 t1194
3017 T t1195 o937 b1189 b983 b1195
3018 B b1196 t1195
3019 T t1196 o2 b1196
3020 B b1197 t1196
3021 T t1197 o937 b1185 b983 b1197
3022 B b1198 t1197
3023 T t1198 o2 b1198
3024 B b1199 t1198
3025 T t1199 o937 b1181 b983 b1199
3026 B b1200 t1199
3027 T t1200 o2 b1200
3028 B b1201 t1200
3029 T t1201 o937 b1177 b983 b1201
3030 B b1202 t1201
3031 T t1202 o2 b1202
3032 B b1203 t1202
3033 T t1203 o937 b1175 b4 b1203
3034 B b1204 t1203
3035 T t1204 o b1204 b4
3036 B b1205 t1204
3037 T t1205 o936 b1169 b1205
3038 B b1206 t1205
3039 P p1206 String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3040 O o1206 ext_rule p1206
3041 T t1206 o936 b1204 b4
3042 B b1207 t1206
3043 T t1207 o1206 b935 b1207 b4 b4
3044 B b1208 t1207
3045 T t1208 o b1208 b4
3046 B b1209 t1208
3047 T t1209 o1165 b935 b1206 b1209 b4
3048 B b1210 t1209
3049 T t1210 o b1210 b4
3050 B b1211 t1210
3051 T t1211 o b1165 b1211
3052 B b1212 t1211
3053 T t1212 o1095 b935 b1095 b1160 b1212
3054 B b1213 t1212
3055 T t1213 o b1213 b4
3056 B b1214 t1213
3057 S s1214 t620 h h1096 h1091
3058 G s1214 t967
3059 B b1215 s1214
3060 T t1215 o938 b1215 b1107
3061 B b1216 t1215
3062 T t1216 o966 b1216 b4 b1127
3063 B b1217 t1216
3064 T t1217 o936 b1217 b4
3065 B b1218 t1217
3066 T t1218 o990 b935 b1218 b4 b4
3067 B b1219 t1218
3068 P p1219 Var v_1
3069 O o1219 var p1219
3070 T t1219 o1219
3071 B b1220 t1219
3072 T t1220 o738 b1220 b949
3073 B b1221 t1220 v_1
3074 T t1221 o976 b1221
3075 S s1221 t620 h h1096 h1091
3076 G s1221 t1221
3077 B b1222 s1221
3078 T t1222 o938 b1222 b1107
3079 B b1223 t1222
3080 T t1223 o973 b1223 b4 b1127
3081 B b1224 t1223
3082 H h1224 s2 t1169
3083 T t1224 o738 b1170 b561
3084 H h1225 x_1 t1224
3085 T t1225 o738 b1170 b949
3086 H h1226 x_2 t1225
3087 T t1226 o676 b561 b949
3088 S s1226 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3089 G s1226 t1226
3090 B b1226 s1226
3091 T t1227 o938 b1226 b1107
3092 B b1227 t1227
3093 T t1228 o738 b561 b949
3094 S s1228 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3095 G s1228 t1228
3096 B b1228 s1228
3097 T t1229 o938 b1228 b1107
3098 B b1229 t1229
3099 B b1230 t1225
3100 B b1231 t1228
3101 T t1231 o1177 b1230 b1231
3102 S s1231 t620 h h1096 h1091 h1169 h1224 h1225
3103 G s1231 t1231
3104 B b1232 s1231
3105 T t1232 o938 b1232 b1107
3106 B b1233 t1232
3107 B b1234 t1224
3108 B b1235 t1231
3109 T t1235 o1177 b1234 b1235
3110 S s1235 t620 h h1096 h1091 h1169 h1224
3111 G s1235 t1235
3112 B b1236 s1235
3113 T t1236 o938 b1236 b1107
3114 B b1237 t1236
3115 B b1238 t1235 s2
3116 T t1238 o1185 b1186 b1238
3117 S s1238 t620 h h1096 h1091 h1169
3118 G s1238 t1238
3119 B b1239 s1238
3120 T t1239 o938 b1239 b1107
3121 B b1240 t1239
3122 B b1241 t1238 s1_1
3123 T t1241 o1185 b1186 b1241
3124 S s1241 t620 h h1096 h1091
3125 G s1241 t1241
3126 B b1242 s1241
3127 T t1242 o938 b1242 b1107
3128 B b1243 t1242
3129 T t1243 o2 b1224
3130 B b1244 t1243
3131 T t1244 o973 b1243 b983 b1244
3132 B b1245 t1244
3133 T t1245 o2 b1245
3134 B b1246 t1245
3135 T t1246 o937 b1240 b983 b1246
3136 B b1247 t1246
3137 T t1247 o2 b1247
3138 B b1248 t1247
3139 T t1248 o937 b1237 b983 b1248
3140 B b1249 t1248
3141 T t1249 o2 b1249
3142 B b1250 t1249
3143 T t1250 o937 b1233 b983 b1250
3144 B b1251 t1250
3145 T t1251 o2 b1251
3146 B b1252 t1251
3147 T t1252 o937 b1229 b983 b1252
3148 B b1253 t1252
3149 T t1253 o2 b1253
3150 B b1254 t1253
3151 T t1254 o937 b1227 b4 b1254
3152 B b1255 t1254
3153 T t1255 o b1255 b4
3154 B b1256 t1255
3155 T t1256 o936 b1224 b1256
3156 B b1257 t1256
3157 P p1257 String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3158 O o1257 ext_rule p1257
3159 T t1257 o936 b1255 b4
3160 B b1258 t1257
3161 T t1258 o1257 b935 b1258 b4 b4
3162 B b1259 t1258
3163 T t1259 o b1259 b4
3164 B b1260 t1259
3165 T t1260 o1165 b935 b1257 b1260 b4
3166 B b1261 t1260
3167 T t1261 o b1261 b4
3168 B b1262 t1261
3169 T t1262 o b1219 b1262
3170 B b1263 t1262
3171 T t1263 o1091 b935 b1095 b1214 b1263
3172 B b1264 t1263
3173 P p1264 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3174 O o1264 ext_rule p1264
3175 H h1264 y_1 t642
3176 T t1264 o620 b695
3177 H h1265 z_1 t1264
3178 T t1265 o676 b562 b695
3179 H h1266 z t1265
3180 T t1266 o676 b948 b949
3181 H h1267 v t1266
3182 T t1267 o676 b561 b674
3183 S s1267 t620 h h1264 h1265 h1266 h1267
3184 G s1267 t1267
3185 B b1267 s1267
3186 T t1268 o938 b1267 b1107
3187 B b1268 t1268
3188 S s1268 t620 h h1264 h1265 h1266 h1267
3189 G s1268 t925
3190 B b1269 s1268
3191 T t1269 o938 b1269 b1107
3192 B b1270 t1269
3193 NItt_logic!and and and Itt_logic
3194 O o1270 and
3195 B b1271 t642
3196 B b1272 t1264
3197 T t1272 o1270 b1271 b1272
3198 H h1272 y t1272
3199 S s1272 t620 h h1272 h1266 h1267
3200 G s1272 t925
3201 B b1273 s1272
3202 T t1273 o938 b1273 b1107
3203 B b1274 t1273
3204 B b1275 t1272
3205 B b1276 t1265
3206 T t1276 o1270 b1275 b1276
3207 H h1276 x t1276
3208 S s1276 t620 h h1276 h1267
3209 G s1276 t925
3210 B b1277 s1276
3211 T t1277 o938 b1277 b1107
3212 B b1278 t1277
3213 S s1278 t620 h h1276
3214 G s1278 t925
3215 B b1279 s1278
3216 T t1279 o938 b1279 b1107
3217 B b1280 t1279
3218 T t1280 o937 b1280 b4 b1125
3219 B b1281 t1280
3220 T t1281 o2 b1281
3221 B b1282 t1281
3222 T t1282 o937 b1278 b4 b1282
3223 B b1283 t1282
3224 T t1283 o2 b1283
3225 B b1284 t1283
3226 T t1284 o937 b1274 b4 b1284
3227 B b1285 t1284
3228 T t1285 o2 b1285
3229 B b1286 t1285
3230 T t1286 o937 b1270 b983 b1286
3231 B b1287 t1286
3232 T t1287 o2 b1287
3233 B b1288 t1287
3234 T t1288 o937 b1268 b4 b1288
3235 B b1289 t1288
3236 T t1289 o676 b966 b949
3237 H h1289 v_1 t1289
3238 S s1289 t620 h h1264 h1265 h1266 h1267 h1289
3239 G s1289 t1267
3240 B b1290 s1289
3241 T t1290 o938 b1290 b1107
3242 B b1291 t1290
3243 T t1291 o2 b1289
3244 B b1292 t1291
3245 T t1292 o937 b1291 b4 b1292
3246 B b1293 t1292
3247 T t268 o b1293 b4
3248 B b268 t268
3249 T t269 o936 b1289 b268
3250 B b269 t269
3251 B b1294 t949 v_1
3252 T t1294 o711 b1294
3253 S s1294 t620 h h1264 h1265 h1266 h1267
3254 G s1294 t1294
3255 B b1295 s1294
3256 T t1295 o938 b1295 b1107
3257 B b1296 t1295
3258 T t1296 o676 b1220 b949
3259 B b1297 t1296 v_1
3260 T t1297 o976 b1297
3261 S s1297 t620 h h1264 h1265 h1266 h1267
3262 G s1297 t1297
3263 B b1298 s1297
3264 T t1298 o938 b1298 b1107
3265 B b1299 t1298
3266 T t1299 o973 b1299 b983 b1292
3267 B b1300 t1299
3268 T t1300 o2 b1300
3269 B b1301 t1300
3270 T t1301 o973 b1296 b4 b1301
3271 B b1302 t1301
3272 P p1305 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3273 O o1305 ext_rule p1305
3274 T t1305 o676 b966 b993
3275 H h1305 v_2 t1305
3276 S s1305 t620 h h1264 h1265 h1266 h1267 h1289 h1305
3277 G s1305 t1267
3278 B b1306 s1305
3279 T t1306 o938 b1306 b1107
3280 B b1307 t1306
3281 T t1307 o2 b1293
3282 B b1308 t1307
3283 T t1308 o937 b1307 b4 b1308
3284 B b1309 t1308
3285 T t270 o b1309 b4
3286 B b270 t270
3287 T t273 o936 b1293 b270
3288 B b273 t273
3289 B b1310 t966 v_2
3290 T t1310 o711 b1310
3291 S s1310 t620 h h1264 h1265 h1266 h1267 h1289
3292 G s1310 t1310
3293 B b1311 s1310
3294 T t1311 o938 b1311 b1107
3295 B b1312 t1311
3296 T t1312 o676 b966 b977
3297 B b1313 t1312 v_2
3298 T t1313 o976 b1313
3299 S s1313 t620 h h1264 h1265 h1266 h1267 h1289
3300 G s1313 t1313
3301 B b1314 s1313
3302 T t1314 o938 b1314 b1107
3303 B b1315 t1314
3304 T t1315 o973 b1315 b983 b1308
3305 B b1316 t1315
3306 T t1316 o2 b1316
3307 B b1317 t1316
3308 T t1317 o973 b1312 b4 b1317
3309 B b1318 t1317
3310 P p1321 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3311 O o1321 ext_rule p1321
3312 T t1321 o676 b1017 b1018
3313 H h1321 v_3 t1321
3314 S s1321 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3315 G s1321 t1267
3316 B b1322 s1321
3317 T t1322 o938 b1322 b1107
3318 B b1323 t1322
3319 T t1323 o2 b1309
3320 B b1324 t1323
3321 T t1324 o937 b1323 b4 b1324
3322 B b1325 t1324
3323 T t1325 o b1325 b4
3324 B b1326 t1325
3325 T t1326 o936 b1309 b1326
3326 B b1327 t1326
3327 P p1327 String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"
3328 O o1327 ext_rule p1327
3329 T t1327 o676 b561 b1018
3330 H h1327 v_4 t1327
3331 S s1327 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1327
3332 G s1327 t1267
3333 B b1328 s1327
3334 T t1328 o938 b1328 b1107
3335 B b1329 t1328
3336 T t1329 o2 b1325
3337 B b1330 t1329
3338 T t1330 o937 b1329 b4 b1330
3339 B b1331 t1330
3340 T t274 o b1331 b4
3341 B b274 t274
3342 T t289 o936 b1325 b274
3343 B b289 t289
3344 S s1331 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3345 G s1331 t1144
3346 B b1332 s1331
3347 T t1332 o938 b1332 b1107
3348 B b1333 t1332
3349 T t1333 o676 b1147 b1018
3350 B b1334 t1333 v_4
3351 T t1334 o976 b1334
3352 S s1334 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3353 G s1334 t1334
3354 B b1335 s1334
3355 T t1335 o938 b1335 b1107
3356 B b1336 t1335
3357 T t1336 o973 b1336 b983 b1330
3358 B b1337 t1336
3359 T t1337 o2 b1337
3360 B b1338 t1337
3361 T t1338 o973 b1333 b4 b1338
3362 B b1339 t1338
3363 P p1342 String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3364 O o1342 ext_rule p1342
3365 T t1342 o936 b1331 b4
3366 B b1343 t1342
3367 T t1343 o1342 b935 b1343 b4 b4
3368 B b1344 t1343
3369 T t290 o b1344 b4
3370 B b290 t290
3371 T t292 o936 b1339 b4
3372 B b292 t292
3373 T t300 o1071 b935 b292 b4 b4
3374 B b300 t300
3375 T t301 o b300 b4
3376 B b301 t301
3377 T t304 o1327 b935 b289 b290 b301
3378 B b304 t304
3379 T t309 o b304 b4
3380 B b309 t309
3381 T t310 o1321 b935 b1327 b309 b4
3382 B b310 t310
3383 T t315 o b310 b4
3384 B b315 t315
3385 H h1344 s1 t1169
3386 T t1344 o738 b560 b561
3387 H h1345 x t1344
3388 B b1347 t1344
3389 T t1374 o936 b1318 b4
3390 B b1375 t1374
3391 T t1375 o1071 b935 b1375 b4 b4
3392 B b1376 t1375
3393 P p1378 String "eqSetSymT thenT autoT"
3394 O o1378 ext_rule p1378
3395 T t1378 o676 b949 b993
3396 S s1378 t620 h h1264 h1265 h1266 h1267 h1289
3397 G s1378 t1378
3398 B b1379 s1378
3399 T t1379 o938 b1379 b1107
3400 B b1380 t1379
3401 S s1380 t620 h h1264 h1265 h1266 h1267 h1289
3402 G s1380 t994
3403 B b1381 s1380
3404 T t1381 o938 b1381 b1107
3405 B b1382 t1381
3406 T t1382 o966 b1382 b983 b1308
3407 B b1383 t1382
3408 T t1383 o2 b1383
3409 B b1384 t1383
3410 T t1384 o966 b1380 b4 b1384
3411 B b1385 t1384
3412 T t1385 o676 b993 b949
3413 S s1385 t620 h h1264 h1265 h1266 h1267 h1289
3414 G s1385 t1385
3415 B b1386 s1385
3416 T t1386 o938 b1386 b1107
3417 B b1387 t1386
3418 T t1387 o2 b1385
3419 B b1388 t1387
3420 T t1388 o966 b1387 b4 b1388
3421 B b1389 t1388
3422 T t1389 o b1389 b4
3423 B b1390 t1389
3424 T t1390 o936 b1385 b1390
3425 B b1391 t1390
3426 T t1391 o1085 b1389
3427 B b1392 t1391
3428 T t1392 o b1392 b4
3429 B b1393 t1392
3430 T t1393 o1378 b935 b1391 b1393 b4
3431 B b1394 t1393
3432 T t1394 o b1394 b4
3433 B b1395 t1394
3434 T t316 o b1376 b1395
3435 B b316 t316
3436 T t318 o1305 b935 b273 b315 b316
3437 B b318 t318
3438 T t320 o b318 b4
3439 B b320 t320
3440 T t1396 o936 b1302 b4
3441 B b1397 t1396
3442 T t1397 o1071 b935 b1397 b4 b4
3443 B b1398 t1397
3444 T t1400 o676 b948 b966
3445 S s1400 t620 h h1264 h1265 h1266 h1267
3446 G s1400 t1400
3447 B b1401 s1400
3448 T t1401 o938 b1401 b1107
3449 B b1402 t1401
3450 S s1402 t620 h h1264 h1265 h1266 h1267
3451 G s1402 t967
3452 B b1403 s1402
3453 T t1403 o938 b1403 b1107
3454 B b1404 t1403
3455 T t1404 o966 b1404 b983 b1292
3456 B b1405 t1404
3457 T t1405 o2 b1405
3458 B b1406 t1405
3459 T t1406 o966 b1402 b4 b1406
3460 B b1407 t1406
3461 T t1407 o676 b966 b948
3462 S s1407 t620 h h1264 h1265 h1266 h1267
3463 G s1407 t1407
3464 B b1408 s1407
3465 T t1408 o938 b1408 b1107
3466 B b1409 t1408
3467 T t1409 o2 b1407
3468 B b1410 t1409
3469 T t1410 o966 b1409 b4 b1410
3470 B b1411 t1410
3471 T t1411 o b1411 b4
3472 B b1412 t1411
3473 T t1412 o936 b1407 b1412
3474 B b1413 t1412
3475 T t1413 o1085 b1411
3476 B b1414 t1413
3477 T t1414 o b1414 b4
3478 B b1415 t1414
3479 T t1415 o1378 b935 b1413 b1415 b4
3480 B b1416 t1415
3481 T t1416 o b1416 b4
3482 B b1417 t1416
3483 T t327 o b1398 b1417
3484 B b327 t327
3485 T t331 o1264 b935 b269 b320 b327
3486 B b331 t331
3487 T t332 o b331 b4
3488 B b332 t332
3489 T t335 o b1264 b332
3490 B b335 t335
3491 T t339 o b1091 b335
3492 B b339 t339
3493 T t340 o934 b935 b963 b266 b339
3494 B b340 t340
3495 T t359 o933 b340
3496 B b359 t359
3497 P p904 Number 4611
3498 O o904 resource_defs p904 p1907 p264
3499 O o905 uid p1894 p1907
3500 T t905 o905 b626
3501 B b905 t905
3502 T t911 o b905 b4
3503 B b911 t911
3504 T t912 o904 b911
3505 B b912 t912
3506 T t913 o b912 b4
3507 B b913 t913
3508 T t914 o919 b922 b933 b359 b913
3509 B b914 t914
3510 T t915 o903 b914
3511 B b915 t915
3512 P p915 Number 5059
3513 P p916 Number 5485
3514 O o916 location p915 p916
3515 P p1432 String cancel2
3516 O o1432 rule p1432
3517 T t1432 o920 b674
3518 B b1432 t1432
3519 T t1433 o b1432 b4
3520 B b1433 t1433
3521 T t1434 o b617 b1433
3522 B b1434 t1434
3523 T t1435 o738 b695 b696
3524 S s1435 t620 h
3525 G s1435 t1435
3526 B b1435 s1435
3527 T t1436 o618 b1435
3528 B b1436 t1436
3529 S s1436 t620 h
3530 G s1436 t1344
3531 B b1437 s1436
3532 T t1437 o618 b1437
3533 B b1438 t1437
3534 T t1438 o635 b1436 b1438
3535 B b1439 t1438
3536 T t1439 o635 b738 b1439
3537 B b1440 t1439
3538 T t1440 o635 b658 b1440
3539 B b1441 t1440
3540 T t1441 o635 b656 b1441
3541 B b1442 t1441
3542 T t1442 o635 b676 b1442
3543 B b1443 t1442
3544 T t1443 o635 b641 b1443
3545 B b1444 t1443
3546 T t1444 o635 b639 b1444
3547 B b1445 t1444
3548 P p1445 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"
3549 O o1445 ext_rule p1445
3550 T t1445 o b1435 b4
3551 B b1446 t1445
3552 T t1446 o b737 b1446
3553 B b1447 t1446
3554 T t1447 o b657 b1447
3555 B b1448 t1447
3556 T t1448 o b655 b1448
3557 B b1449 t1448
3558 T t1449 o b675 b1449
3559 B b1450 t1449
3560 T t1450 o b640 b1450
3561 B b1451 t1450
3562 T t1451 o b638 b1451
3563 B b1452 t1451
3564 T t1452 o938 b1437 b1452
3565 B b1453 t1452
3566 T t1453 o937 b1453 b4 b946
3567 B b1454 t1453
3568 H h1454 v t1435
3569 T t1454 o572 b674
3570 B b1455 t1454
3571 T t1455 o559 b695 b1455
3572 B b1456 t1455
3573 T t1456 o559 b696 b1455
3574 B b1457 t1456
3575 T t1457 o738 b1456 b1457
3576 S s1457 t620 h h1454
3577 G s1457 t1457
3578 B b1458 s1457
3579 T t1458 o938 b1458 b1452
3580 B b1459 t1458
3581 S s1459 t620 h h1454
3582 G s1459 t1344
3583 B b1460 s1459
3584 T t1460 o938 b1460 b1452
3585 B b1461 t1460
3586 T t1461 o2 b1454
3587 B b1462 t1461
3588 T t1462 o937 b1461 b4 b1462
3589 B b1463 t1462
3590 T t1463 o2 b1463
3591 B b1464 t1463
3592 T t1464 o947 b1459 b4 b1464
3593 B b1465 t1464
3594 H h1465 v_1 t1457
3595 S s1465 t620 h h1454 h1465
3596 G s1465 t1344
3597 B b1466 s1465
3598 T t1466 o938 b1466 b1452
3599 B b1467 t1466
3600 T t1467 o937 b1467 b4 b1464
3601 B b1468 t1467
3602 T t1468 o b1468 b4
3603 B b1469 t1468
3604 T t1469 o b1465 b1469
3605 B b1470 t1469
3606 T t1470 o936 b1454 b1470
3607 B b1471 t1470
3608 T t1471 o936 b1465 b4
3609 B b1472 t1471
3610 T t1472 o963 b935 b1472 b4 b4
3611 B b1473 t1472
3612 P p1473 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
3613 O o1473 ext_rule p1473
3614 T t1473 o559 b674 b1455
3615 B b1474 t1473
3616 T t1474 o559 b560 b1474
3617 B b1475 t1474
3618 T t1475 o738 b1475 b1457
3619 H h1475 v_2 t1475
3620 S s1475 t620 h h1454 h1465 h1475
3621 G s1475 t1344
3622 B b1476 s1475
3623 T t1476 o938 b1476 b1452
3624 B b1477 t1476
3625 T t1477 o2 b1468
3626 B b1478 t1477
3627 T t1478 o937 b1477 b4 b1478
3628 B b1479 t1478
3629 T t391 o b1479 b4
3630 B b391 t391
3631 T t392 o936 b1468 b391
3632 B b392 t392
3633 B b1480 t1456 v_2
3634 T t1480 o711 b1480
3635 S s1480 t620 h h1454 h1465
3636 G s1480 t1480
3637 B b1481 s1480
3638 T t1481 o938 b1481 b1452
3639 B b1482 t1481
3640 T t1482 o738 b977 b1457
3641 B b1483 t1482 v_2
3642 T t1483 o976 b1483
3643 S s1483 t620 h h1454 h1465
3644 G s1483 t1483
3645 B b1484 s1483
3646 T t1484 o938 b1484 b1452
3647 B b1485 t1484
3648 T t1485 o973 b1485 b983 b1478
3649 B b1486 t1485
3650 T t1486 o2 b1486
3651 B b1487 t1486
3652 T t1487 o973 b1482 b4 b1487
3653 B b1488 t1487
3654 P p1491 String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
3655 O o1491 ext_rule p1491
3656 T t1491 o559 b561 b1474
3657 B b1492 t1491
3658 T t1492 o738 b1475 b1492
3659 H h1492 v_3 t1492
3660 S s1492 t620 h h1454 h1465 h1475 h1492
3661 G s1492 t1344
3662 B b1493 s1492
3663 T t1493 o938 b1493 b1452
3664 B b1494 t1493
3665 T t1494 o2 b1479
3666 B b1495 t1494
3667 T t1495 o937 b1494 b4 b1495
3668 B b1496 t1495
3669 T t393 o b1496 b4
3670 B b393 t393
3671 T t399 o936 b1479 b393
3672 B b399 t399
3673 B b1497 t1474 v_3
3674 T t1497 o711 b1497
3675 S s1497 t620 h h1454 h1465 h1475
3676 G s1497 t1497
3677 B b1498 s1497
3678 T t1498 o938 b1498 b1452
3679 B b1499 t1498
3680 T t1499 o738 b1475 b1004
3681 B b1500 t1499 v_3
3682 T t1500 o976 b1500
3683 S s1500 t620 h h1454 h1465 h1475
3684 G s1500 t1500
3685 B b1501 s1500
3686 T t1501 o938 b1501 b1452
3687 B b1502 t1501
3688 T t1502 o973 b1502 b983 b1495
3689 B b1503 t1502
3690 T t1503 o2 b1503
3691 B b1504 t1503
3692 T t1504 o973 b1499 b4 b1504
3693 B b1505 t1504
3694 P p1508 String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
3695 O o1508 ext_rule p1508
3696 T t1508 o559 b560 b567
3697 B b1509 t1508
3698 T t1509 o559 b561 b567
3699 B b1510 t1509
3700 T t1510 o738 b1509 b1510
3701 H h1510 v_4 t1510
3702 S s1510 t620 h h1454 h1465 h1475 h1492 h1510
3703 G s1510 t1344
3704 B b1511 s1510
3705 T t1511 o938 b1511 b1452
3706 B b1512 t1511
3707 T t1512 o2 b1496
3708 B b1513 t1512
3709 T t1513 o937 b1512 b4 b1513
3710 B b1514 t1513
3711 T t1514 o b1514 b4
3712 B b1515 t1514
3713 T t1515 o936 b1496 b1515
3714 B b1516 t1515
3715 P p1516 String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
3716 O o1516 ext_rule p1516
3717 T t1516 o738 b560 b1510
3718 H h1516 v_5 t1516
3719 S s1516 t620 h h1454 h1465 h1475 h1492 h1510 h1516
3720 G s1516 t1344
3721 B b1517 s1516
3722 T t1517 o938 b1517 b1452
3723 B b1518 t1517
3724 T t1518 o2 b1514
3725 B b1519 t1518
3726 T t1519 o937 b1518 b4 b1519
3727 B b1520 t1519
3728 T t400 o b1520 b4
3729 B b400 t400
3730 T t406 o936 b1514 b400
3731 B b406 t406
3732 B b1521 t1509 v_5
3733 T t1521 o711 b1521
3734 S s1521 t620 h h1454 h1465 h1475 h1492 h1510
3735 G s1521 t1521
3736 B b1522 s1521
3737 T t1522 o938 b1522 b1452
3738 B b1523 t1522
3739 T t1523 o738 b1032 b1510
3740 B b1524 t1523 v_5
3741 T t1524 o976 b1524
3742 S s1524 t620 h h1454 h1465 h1475 h1492 h1510
3743 G s1524 t1524
3744 B b1525 s1524
3745 T t1525 o938 b1525 b1452
3746 B b1526 t1525
3747 T t1526 o973 b1526 b983 b1519
3748 B b1527 t1526
3749 T t1527 o2 b1527
3750 B b1528 t1527
3751 T t1528 o973 b1523 b4 b1528
3752 B b1529 t1528
3753 P p1532 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3754 O o1532 ext_rule p1532
3755 T t1532 o936 b1520 b4
3756 B b1533 t1532
3757 T t1533 o1532 b935 b1533 b4 b4
3758 B b1534 t1533
3759 T t407 o b1534 b4
3760 B b407 t407
3761 T t1534 o936 b1529 b4
3762 B b1535 t1534
3763 T t1535 o1050 b935 b1535 b4 b4
3764 B b1536 t1535
3765 T t1536 o b1536 b4
3766 B b1537 t1536
3767 T t416 o1516 b935 b406 b407 b1537
3768 B b416 t416
3769 T t417 o b416 b4
3770 B b417 t417
3771 T t425 o1508 b935 b1516 b417 b4
3772 B b425 t425
3773 T t426 o b425 b4
3774 B b426 t426
3775 T t1541 o936 b1505 b4
3776 B b1542 t1541
3777 T t1542 o1050 b935 b1542 b4 b4
3778 B b1543 t1542
3779 T t1543 o b1543 b4
3780 B b1544 t1543
3781 T t434 o1491 b935 b399 b426 b1544
3782 B b434 t434
3783 T t435 o b434 b4
3784 B b435 t435
3785 T t1546 o936 b1488 b4
3786 B b1547 t1546
3787 T t1547 o1050 b935 b1547 b4 b4
3788 B b1548 t1547
3789 T t1548 o b1548 b4
3790 B b1549 t1548
3791 T t443 o1473 b935 b392 b435 b1549
3792 B b443 t443
3793 T t444 o b443 b4
3794 B b444 t444
3795 T t452 o b1473 b444
3796 B b452 t452
3797 S s1553 t620 h
3798 G s1553 t1457
3799 B b1554 s1553
3800 T t1554 o938 b1554 b1452
3801 B b1555 t1554
3802 T t1555 o947 b1555 b4 b1462
3803 B b1556 t1555
3804 T t1556 o1085 b1556
3805 B b1557 t1556
3806 T t1557 o b1557 b4
3807 B b1558 t1557
3808 T t1558 o963 b935 b1557 b1558 b4
3809 B b1559 t1558
3810 H h1559 v t1457
3811 S s1559 t620 h h1559
3812 G s1559 t1344
3813 B b1560 s1559
3814 T t1560 o938 b1560 b1452
3815 B b1561 t1560
3816 T t1561 o937 b1561 b4 b1462
3817 B b1562 t1561
3818 T t1562 o1085 b1562
3819 B b1563 t1562
3820 T t1563 o b1563 b4
3821 B b1564 t1563
3822 T t1564 o1532 b935 b1563 b1564 b4
3823 B b1565 t1564
3824 T t1565 o b1565 b4
3825 B b1566 t1565
3826 H h1566 x t1435
3827 H h1567 v_1 t1475
3828 H h1568 v_2 t1492
3829 H h1569 v_3 t1510
3830 B b1569 t1509 v_4
3831 T t1569 o711 b1569
3832 S s1569 t620 h h1566 h1559 h1567 h1568 h1569
3833 G s1569 t1569
3834 B b1570 s1569
3835 T t1570 o938 b1570 b1107
3836 B b1571 t1570
3837 T t1571 o738 b1147 b1510
3838 B b1572 t1571 v_4
3839 T t1572 o976 b1572
3840 S s1572 t620 h h1566 h1559 h1567 h1568 h1569
3841 G s1572 t1572
3842 B b1573 s1572
3843 T t1573 o938 b1573 b1107
3844 B b1574 t1573
3845 S s1574 t620 h h1566 h1559 h1567 h1568 h1569
3846 G s1574 t1344
3847 B b1575 s1574
3848 T t1575 o938 b1575 b1107
3849 B b1576 t1575
3850 S s1576 t620 h h1566 h1559 h1567 h1568
3851 G s1576 t1344
3852 B b1577 s1576
3853 T t1577 o938 b1577 b1107
3854 B b1578 t1577
3855 S s1578 t620 h h1566 h1559 h1567
3856 G s1578 t1344
3857 B b1579 s1578
3858 T t1579 o938 b1579 b1107
3859 B b1580 t1579
3860 S s1580 t620 h h1566 h1559
3861 G s1580 t1344
3862 B b1581 s1580
3863 T t1581 o938 b1581 b1107
3864 B b1582 t1581
3865 S s1582 t620 h h1566
3866 G s1582 t1344
3867 B b1583 s1582
3868 T t1583 o938 b1583 b1107
3869 B b1584 t1583
3870 T t1584 o937 b1584 b4 b946
3871 B b1585 t1584
3872 T t1585 o2 b1585
3873 B b1586 t1585
3874 T t1586 o937 b1582 b4 b1586
3875 B b1587 t1586
3876 T t1587 o2 b1587
3877 B b1588 t1587
3878 T t1588 o937 b1580 b4 b1588
3879 B b1589 t1588
3880 T t1589 o2 b1589
3881 B b1590 t1589
3882 T t1590 o937 b1578 b4 b1590
3883 B b1591 t1590
3884 T t1591 o2 b1591
3885 B b1592 t1591
3886 T t1592 o937 b1576 b4 b1592
3887 B b1593 t1592
3888 T t1593 o2 b1593
3889 B b1594 t1593
3890 T t1594 o973 b1574 b983 b1594
3891 B b1595 t1594
3892 T t1595 o2 b1595
3893 B b1596 t1595
3894 T t1596 o973 b1571 b4 b1596
3895 B b1597 t1596
3896 T t1597 o936 b1597 b4
3897 B b1598 t1597
3898 T t1598 o1050 b935 b1598 b4 b4
3899 B b1599 t1598
3900 T t1599 o b1599 b4
3901 B b1600 t1599
3902 T t1600 o1516 b935 b1563 b1566 b1600
3903 B b1601 t1600
3904 T t1601 o b1601 b4
3905 B b1602 t1601
3906 T t1602 o1508 b935 b1563 b1602 b4
3907 B b1603 t1602
3908 T t1603 o b1603 b4
3909 B b1604 t1603
3910 P p1604 String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
3911 O o1604 ext_rule p1604
3912 B b1605 t1474 v_2
3913 T t1605 o711 b1605
3914 S s1605 t620 h h1566 h1559 h1567
3915 G s1605 t1605
3916 B b1606 s1605
3917 T t1606 o938 b1606 b1107
3918 B b1607 t1606
3919 T t1607 o738 b1475 b977
3920 B b1608 t1607 v_2
3921 T t1608 o976 b1608
3922 S s1608 t620 h h1566 h1559 h1567
3923 G s1608 t1608
3924 B b1609 s1608
3925 T t1609 o938 b1609 b1107
3926 B b1610 t1609
3927 T t1610 o973 b1610 b983 b1590
3928 B b1611 t1610
3929 T t1611 o2 b1611
3930 B b1612 t1611
3931 T t1612 o973 b1607 b4 b1612
3932 B b1613 t1612
3933 T t1613 o936 b1613 b4
3934 B b1614 t1613
3935 T t1614 o1604 b935 b1614 b4 b4
3936 B b1615 t1614
3937 T t1615 o b1615 b4
3938 B b1616 t1615
3939 T t1616 o1491 b935 b1563 b1604 b1616
3940 B b1617 t1616
3941 T t1617 o b1617 b4
3942 B b1618 t1617
3943 B b1619 t1456 v_1
3944 T t1619 o711 b1619
3945 S s1619 t620 h h1566 h1559
3946 G s1619 t1619
3947 B b1620 s1619
3948 T t1620 o938 b1620 b1107
3949 B b1621 t1620
3950 T t1621 o738 b1220 b1457
3951 B b1622 t1621 v_1
3952 T t1622 o976 b1622
3953 S s1622 t620 h h1566 h1559
3954 G s1622 t1622
3955 B b1623 s1622
3956 T t1623 o938 b1623 b1107
3957 B b1624 t1623
3958 T t1624 o973 b1624 b983 b1588
3959 B b1625 t1624
3960 T t1625 o2 b1625
3961 B b1626 t1625
3962 T t1626 o973 b1621 b4 b1626
3963 B b1627 t1626
3964 T t1627 o936 b1627 b4
3965 B b1628 t1627
3966 T t1628 o1604 b935 b1628 b4 b4
3967 B b1629 t1628
3968 T t1629 o b1629 b4
3969 B b1630 t1629
3970 T t1630 o1473 b935 b1563 b1618 b1630
3971 B b1631 t1630
3972 T t1631 o b1631 b4
3973 B b1632 t1631
3974 T t1632 o b1559 b1632
3975 B b1633 t1632
3976 T t453 o1445 b935 b1471 b452 b1633
3977 B b453 t453
3978 T t461 o933 b453
3979 B b461 t461
3980 P p917 Number 5082
3981 P p918 Number 5090
3982 O o918 resource_defs p917 p918 p264
3983 P p920 Number 5088
3984 O o921 uid p920 p918
3985 T t934 o921 b626
3986 B b934 t934
3987 T t936 o b934 b4
3988 B b936 t936
3989 T t937 o918 b936
3990 B b937 t937
3991 T t957 o b937 b4
3992 B b1013 t957
3993 T t1013 o1432 b1434 b1445 b461 b1013
3994 B b1014 t1013
3995 T t1038 o916 b1014
3996 B b1071 t1038
3997 P p1075 Number 5487
3998 P p1076 Number 5556
3999 O o1076 location p1075 p1076
4000 O o1077 str_let p1075 p1076
4001 P p1077 Number 5491
4002 O o1078 patt_var p1077 p1076
4003 O o1079 patt_done p1075 p1076
4004 T t1083 o1079
4005 B b1084 t1083 groupCancelLeftT
4006 T t1084 o1078 b1084
4007 B b1085 t1084
4008 O o1088 fun p1077 p1076
4009 O o1089 patt_if p1077 p1076
4010 P p1089 Number 5508
4011 P p1090 Number 5509
4012 O o1090 patt_var p1089 p1090
4013 O o1092 patt_body p1077 p1076
4014 P p1092 Number 5510
4015 P p1093 Number 5511
4016 O o1093 patt_var p1092 p1093
4017 P p1094 Number 5517
4018 O o1094 apply p1094 p1076
4019 P p1097 Number 5554
4020 O o1097 apply p1094 p1097
4021 P p1098 Number 5552
4022 O o1098 apply p1094 p1098
4023 P p1099 Number 5524
4024 O o1099 lid p1094 p1099
4025 O o1656 lid p919
4026 T t1656 o1656
4027 B b1656 t1656
4028 T t1099 o1099 b1656
4029 B b1099 t1099
4030 P p1100 Number 5526
4031 P p1101 Number 5551
4032 O o1101 apply p1100 p1101
4033 P p1102 Number 5549
4034 O o1102 proj p1100 p1102
4035 O o1103 uid p1100 p1102
4036 T t1111 o1103 b836
4037 B b1172 t1111
4038 P p1172 Number 5535
4039 O o1172 lid p1172 p1102
4040 T t1178 o1172 b838
4041 B b1225 t1178
4042 T t1230 o1102 b1172 b1225
4043 B b1265 t1230
4044 P p1265 Number 5550
4045 O o1265 lid p1265 p1101
4046 T t1270 o1265 b841
4047 B b1320 t1270
4048 T t1320 o1101 b1265 b1320
4049 B b1321 t1320
4050 T t1339 o1098 b1099 b1321
4051 B b1349 t1339
4052 P p1353 Number 5553
4053 O o1353 lid p1353 p1097
4054 P p1666 Var t
4055 O o1666 var p1666
4056 T t1666 o1666
4057 B b1666 t1666
4058 T t1358 o1353 b1666
4059 B b1358 t1358
4060 T t1359 o1097 b1349 b1358
4061 B b1359 t1359
4062 P p1361 Number 5555
4063 O o1362 lid p1361 p1076
4064 T t1367 o1362 b841
4065 B b1367 t1367
4066 T t1368 o1094 b1359 b1367
4067 B b1368 t1368
4068 T t1369 o1092 b1368
4069 B b1369 t1369 p
4070 T t1380 o1093 b1369
4071 B b1421 t1380
4072 T t1421 o1089 b1421
4073 B b1422 t1421
4074 T t1422 o1088 b1422
4075 B b1423 t1422
4076 T t1423 o1092 b1423
4077 B b1424 t1423 t
4078 T t1424 o1090 b1424
4079 B b1425 t1424
4080 T t1425 o1089 b1425
4081 B b1426 t1425
4082 T t1426 o1088 b1426
4083 B b1427 t1426
4084 T t1427 o1077 b1085 b1427
4085 B b1428 t1427
4086 T t1428 o b1428 b4
4087 B b1431 t1428
4088 T t1431 o1077 b1431
4089 B b1507 t1431
4090 T t1507 o392 b1507
4091 B b1508 t1507
4092 T t1529 o1076 b1508
4093 B b1532 t1529
4094 P p1541 Number 5558
4095 P p1542 Number 5628
4096 O o1542 location p1541 p1542
4097 O o1543 str_let p1541 p1542
4098 P p1543 Number 5562
4099 O o1544 patt_var p1543 p1542
4100 O o1546 patt_done p1541 p1542
4101 T t1559 o1546
4102 B b1567 t1559 groupCancelRightT
4103 T t1567 o1544 b1567
4104 B b1568 t1567
4105 O o1568 fun p1543 p1542
4106 O o1569 patt_if p1543 p1542
4107 P p1569 Number 5580
4108 P p1570 Number 5581
4109 O o1570 patt_var p1569 p1570
4110 O o1571 patt_body p1543 p1542
4111 P p1571 Number 5582
4112 P p1572 Number 5583
4113 O o1572 patt_var p1571 p1572
4114 P p1573 Number 5589
4115 O o1573 apply p1573 p1542
4116 P p1574 Number 5626
4117 O o1574 apply p1573 p1574
4118 P p1575 Number 5624
4119 O o1575 apply p1573 p1575
4120 P p1576 Number 5596
4121 O o1576 lid p1573 p1576
4122 O o1697 lid p1432
4123 T t1697 o1697
4124 B b1697 t1697
4125 T t1576 o1576 b1697
4126 B b1636 t1576
4127 P p1636 Number 5598
4128 P p1638 Number 5623
4129 O o1638 apply p1636 p1638
4130 P p1639 Number 5621
4131 O o1639 proj p1636 p1639
4132 O o1640 uid p1636 p1639
4133 T t1640 o1640 b836
4134 B b1640 t1640
4135 P p1640 Number 5607
4136 O o1641 lid p1640 p1639
4137 T t1643 o1641 b838
4138 B b1643 t1643
4139 T t1644 o1639 b1640 b1643
4140 B b1644 t1644
4141 P p1644 Number 5622
4142 O o1644 lid p1644 p1638
4143 T t1645 o1644 b841
4144 B b1645 t1645
4145 T t1646 o1638 b1644 b1645
4146 B b1646 t1646
4147 T t1647 o1575 b1636 b1646
4148 B b1647 t1647
4149 P p1647 Number 5625
4150 O o1647 lid p1647 p1574
4151 T t1648 o1647 b1666
4152 B b1648 t1648
4153 T t1649 o1574 b1647 b1648
4154 B b1649 t1649
4155 P p1649 Number 5627
4156 O o1649 lid p1649 p1542
4157 T t1650 o1649 b841
4158 B b1650 t1650
4159 T t1651 o1573 b1649 b1650
4160 B b1651 t1651
4161 T t1652 o1571 b1651
4162 B b1652 t1652 p
4163 T t1653 o1572 b1652
4164 B b1653 t1653
4165 T t1654 o1569 b1653
4166 B b1654 t1654
4167 T t1655 o1568 b1654
4168 B b1655 t1655
4169 T t1657 o1571 b1655
4170 B b1657 t1657 t
4171 T t1658 o1570 b1657
4172 B b1658 t1658
4173 T t1659 o1569 b1658
4174 B b1659 t1659
4175 T t1660 o1568 b1659
4176 B b1660 t1660
4177 T t1661 o1543 b1568 b1660
4178 B b1661 t1661
4179 T t1662 o b1661 b4
4180 B b1662 t1662
4181 T t1663 o1543 b1662
4182 B b1663 t1663
4183 T t1664 o392 b1663
4184 B b1664 t1664
4185 T t1665 o1542 b1664
4186 B b1665 t1665
4187 P p1665 Number 5646
4188 P p1667 Number 5887
4189 O o1667 location p1665 p1667
4190 P p1725 String unique_id1
4191 O o1725 rule p1725
4192 P p1726 Var e2
4193 O o1726 var p1726
4194 T t1726 o1726
4195 B b1726 t1726
4196 T t1727 o620 b1726
4197 S s1727 t637 h
4198 G s1727 t1727
4199 B b1727 s1727
4200 T t1728 o618 b1727
4201 B b1728 t1728
4202 T t1729 o655 b1726 b554
4203 S s1729 t620 h
4204 G s1729 t1729
4205 B b1729 s1729
4206 T t1730 o618 b1729
4207 B b1730 t1730
4208 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4209 NCzf_itt_dall!dall dall dall Czf_itt_dall
4210 O o1730 dall
4211 T t1731 o559 b1726 b573
4212 B b1731 t1731
4213 T t1732 o676 b1731 b573
4214 B b1732 t1732
4215 T t1733 o559 b573 b1726
4216 B b1733 t1733
4217 T t1734 o676 b1733 b573
4218 B b1734 t1734
4219 T t1735 o1270 b1732 b1734
4220 B b1735 t1735 s
4221 T t1736 o1730 b554 b1735
4222 H h1736 x t1736
4223 T t1737 o676 b1726 b567
4224 S s1737 t620 h h1736
4225 G s1737 t1737
4226 B b1737 s1737
4227 T t1738 o618 b1737
4228 B b1738 t1738
4229 T t1739 o635 b1730 b1738
4230 B b1739 t1739
4231 T t1740 o635 b1728 b1739
4232 B b1740 t1740
4233 P p1740 String "withT << id >> (dT 2) thenT autoT"
4234 O o1740 ext_rule p1740
4235 T t1741 o b1729 b4
4236 B b1741 t1741
4237 T t1742 o b1727 b1741
4238 B b1742 t1742
4239 T t1743 o938 b1737 b1742
4240 B b1743 t1743
4241 T t1744 o937 b1743 b4 b946
4242 B b1744 t1744
4243 T t1745 o559 b1726 b567
4244 B b1745 t1745
4245 T t1746 o676 b1745 b567
4246 H h1746 y t1746
4247 T t1747 o559 b567 b1726
4248 B b1747 t1747
4249 T t1748 o676 b1747 b567
4250 H h1748 z t1748
4251 S s1748 t620 h h1736 h1746 h1748
4252 G s1748 t1737
4253 B b1748 s1748
4254 T t1749 o938 b1748 b1742
4255 B b1749 t1749
4256 B b1750 t1746
4257 B b1751 t1748
4258 T t1751 o1270 b1750 b1751
4259 H h1751 w t1751
4260 S s1751 t620 h h1736 h1751
4261 G s1751 t1737
4262 B b1752 s1751
4263 T t1752 o938 b1752 b1742
4264 B b1753 t1752
4265 P p1753 String with
4266 O o1753 arg_named p1753
4267 NSummary!arg_term_list arg_term_list arg_term_list Summary
4268 O o1754 arg_term_list
4269 T t1754 o b567 b4
4270 B b1754 t1754
4271 T t1755 o1754 b1754
4272 B b1755 t1755
4273 T t1756 o1753 b1755
4274 B b1756 t1756
4275 T t1757 o b1756 b4
4276 B b1757 t1757
4277 T t1758 o937 b1743 b1757 b946
4278 B b1758 t1758
4279 T t1759 o2 b1758
4280 B b1759 t1759
4281 T t1760 o937 b1753 b4 b1759
4282 B b1760 t1760
4283 T t1761 o2 b1760
4284 B b1761 t1761
4285 T t1762 o937 b1749 b4 b1761
4286 B b1762 t1762
4287 T t1763 o b1762 b4
4288 B b1763 t1763
4289 T t1764 o936 b1744 b1763
4290 B b1764 t1764
4291 P p1764 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
4292 O o1764 ext_rule p1764
4293 T t1765 o936 b1762 b4
4294 B b1765 t1765
4295 T t1766 o1764 b935 b1765 b4 b4
4296 B b1766 t1766
4297 T t1767 o b1766 b4
4298 B b1767 t1767
4299 S s1767 t620 h
4300 G s1767 t1727
4301 B b1768 s1767
4302 T t1768 o b1768 b1741
4303 B b1769 t1768
4304 T t1769 o938 b1748 b1769
4305 B b1770 t1769
4306 T t1770 o938 b1752 b1769
4307 B b1771 t1770
4308 T t1771 o938 b1737 b1769
4309 B b1772 t1771
4310 T t1772 o937 b1772 b1757 b946
4311 B b1773 t1772
4312 T t1773 o2 b1773
4313 B b1774 t1773
4314 T t1774 o937 b1771 b4 b1774
4315 B b1775 t1774
4316 T t1775 o2 b1775
4317 B b1776 t1775
4318 T t1776 o937 b1770 b4 b1776
4319 B b1777 t1776
4320 T t1777 o936 b1777 b4
4321 B b1778 t1777
4322 T t1778 o1764 b935 b1778 b4 b4
4323 B b1779 t1778
4324 P p1779 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
4325 O o1779 ext_rule p1779
4326 H h1779 v t1737
4327 S s1779 t620 h h1736 h1746 h1748 h1779
4328 G s1779 t1737
4329 B b1780 s1779
4330 T t1780 o938 b1780 b1769
4331 B b1781 t1780
4332 T t1781 o2 b1777
4333 B b1782 t1781
4334 T t1782 o937 b1781 b4 b1782
4335 B b1783 t1782
4336 T t1783 o b1783 b4
4337 B b1784 t1783
4338 T t1784 o936 b1777 b1784
4339 B b1785 t1784
4340 T t1785 o1085 b1783
4341 B b1786 t1785
4342 T t1786 o b1786 b4
4343 B b1787 t1786
4344 T t1787 o1779 b935 b1785 b1787 b4
4345 B b1788 t1787
4346 P p1788 String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
4347 O o1788 ext_rule p1788
4348 P p1789 Var e
4349 O o1789 var p1789
4350 T t1789 o1789
4351 B b1789 t1789
4352 T t1790 o620 b1789
4353 S s1790 t637 h h1736 h1746 h1748
4354 G s1790 t1790
4355 B b1790 s1790
4356 T t1791 o938 b1790 b1769
4357 B b1791 t1791
4358 T t1792 o559 b1726 b1789
4359 B b1792 t1792
4360 T t1793 o620 b1792
4361 S s1793 t637 h h1736 h1746 h1748
4362 G s1793 t1793
4363 B b1793 s1793
4364 T t1794 o938 b1793 b1769
4365 B b1794 t1794
4366 T t1795 o738 b1792 b1726
4367 S s1795 t620 h h1736 h1746 h1748
4368 G s1795 t1795
4369 B b1795 s1795
4370 T t1796 o938 b1795 b1769
4371 B b1796 t1796
4372 T t1797 o966 b1796 b983 b1782
4373 B b1797 t1797
4374 T t1798 o2 b1797
4375 B b1798 t1798
4376 T t1799 o973 b1794 b983 b1798
4377 B b1799 t1799
4378 T t1800 o2 b1799
4379 B b1800 t1800
4380 T t1801 o973 b1791 b4 b1800
4381 B b1801 t1801
4382 T t1802 o676 b1792 b1726
4383 S s1802 t620 h h1736 h1746 h1748
4384 G s1802 t1802
4385 B b1802 s1802
4386 T t1803 o938 b1802 b1769
4387 B b1803 t1803
4388 T t1804 o966 b1803 b4 b1798
4389 B b1804 t1804
4390 H h1804 v t1746
4391 S s1804 t620 h h1736 h1746 h1748 h1804
4392 G s1804 t1737
4393 B b1805 s1804
4394 T t1805 o938 b1805 b1769
4395 B b1806 t1805
4396 T t1806 o937 b1806 b4 b1782
4397 B b1807 t1806
4398 T t471 o b1807 b4
4399 B b471 t471
4400 T t479 o b1804 b471
4401 B b479 t479
4402 T t480 o b1801 b479
4403 B b480 t480
4404 T t486 o936 b1777 b480
4405 B b486 t486
4406 T t1821 o1085 b1801
4407 B b1822 t1821
4408 T t1822 o1085 b1804
4409 B b1823 t1822
4410 T t1823 o1085 b1807
4411 B b1824 t1823
4412 T t487 o b1824 b4
4413 B b487 t487
4414 T t493 o b1823 b487
4415 B b493 t493
4416 T t494 o b1822 b493
4417 B b494 t494
4418 T t500 o1788 b935 b486 b494 b4
4419 B b500 t500
4420 T t501 o b500 b4
4421 B b501 t501
4422 T t508 o b500 b501
4423 B b508 t508
4424 T t509 o b1788 b508
4425 B b509 t509
4426 T t516 o b1779 b509
4427 B b516 t516
4428 T t517 o1740 b935 b1764 b1767 b516
4429 B b517 t517
4430 T t524 o933 b517
4431 B b524 t524
4432 P p1668 Number 5672
4433 P p1669 Number 5680
4434 O o1669 resource_defs p1668 p1669 p264
4435 P p1670 Number 5678
4436 O o1670 uid p1670 p1669
4437 T t1670 o1670 b626
4438 B b1670 t1670
4439 T t1671 o b1670 b4
4440 B b1671 t1671
4441 T t1672 o1669 b1671
4442 B b1672 t1672
4443 T t1673 o b1672 b4
4444 B b1673 t1673
4445 T t1674 o1725 b618 b1740 b524 b1673
4446 B b1674 t1674
4447 T t1675 o1667 b1674
4448 B b1675 t1675
4449 P p1675 Number 6203
4450 P p1676 Number 6584
4451 O o1676 location p1675 p1676
4452 P p2511 String unique_inv1
4453 O o2511 rule p2511
4454 T t1845 o559 b561 b573
4455 B b1845 t1845
4456 T t1846 o738 b1845 b567
4457 S s2511 t620 h
4458 G s2511 t1846
4459 B b2511 s2511
4460 T t2511 o618 b2511
4461 B b2512 t2511
4462 T t1847 o559 b573 b561
4463 B b1847 t1847
4464 T t1848 o738 b1847 b567
4465 S s2512 t620 h
4466 G s2512 t1848
4467 B b2513 s2512
4468 T t2513 o618 b2513
4469 B b2514 t2513
4470 T t1849 o738 b561 b574
4471 S s2514 t620 h
4472 G s2514 t1849
4473 B b2515 s2514
4474 T t2518 o618 b2515
4475 B b2519 t2518
4476 T t2519 o635 b2514 b2519
4477 B b2520 t2519
4478 T t2520 o635 b2512 b2520
4479 B b2521 t2520
4480 T t2521 o635 b658 b2521
4481 B b2522 t2521
4482 T t2522 o635 b794 b2522
4483 B b2527 t2522
4484 T t2527 o635 b641 b2527
4485 B b2528 t2527
4486 T t2528 o635 b711 b2528
4487 B b2532 t2528
4488 P p2532 String "assumT 5 thenT assumT 6"
4489 O o2532 ext_rule p2532
4490 T t2532 o b2513 b4
4491 B b2533 t2532
4492 T t2533 o b2511 b2533
4493 B b2534 t2533
4494 T t2534 o b657 b2534
4495 B b2535 t2534
4496 T t2535 o b793 b2535
4497 B b2536 t2535
4498 T t2536 o b640 b2536
4499 B b2537 t2536
4500 T t2537 o b710 b2537
4501 B b2538 t2537
4502 T t2538 o938 b2515 b2538
4503 B b2539 t2538
4504 T t2539 o937 b2539 b4 b946
4505 B b2540 t2539
4506 H h2540 v t1846
4507 H h2541 v_1 t1848
4508 S s2541 t620 h h2540 h2541
4509 G s2541 t1849
4510 B b2541 s2541
4511 T t2541 o938 b2541 b2538
4512 B b2542 t2541
4513 S s2542 t620 h h2540
4514 G s2542 t1849
4515 B b2543 s2542
4516 T t2543 o938 b2543 b2538
4517 B b2544 t2543
4518 T t2544 o2 b2540
4519 B b2545 t2544
4520 T t2545 o937 b2544 b4 b2545
4521 B b2546 t2545
4522 T t2546 o2 b2546
4523 B b2547 t2546
4524 T t2547 o937 b2542 b4 b2547
4525 B b2548 t2547
4526 T t2548 o b2548 b4
4527 B b2549 t2548
4528 T t2549 o936 b2540 b2549
4529 B b2550 t2549
4530 P p1854 String "assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
4531 O o1854 ext_rule p1854
4532 T t1861 o559 b574 b573
4533 B b1861 t1861
4534 T t1862 o738 b1861 b567
4535 H h2550 v_2 t1862
4536 S s2550 t620 h h2540 h2541 h2550
4537 G s2550 t1849
4538 B b2551 s2550
4539 T t2551 o938 b2551 b2538
4540 B b2552 t2551
4541 T t2552 o2 b2548
4542 B b2553 t2552
4543 T t2553 o937 b2552 b4 b2553
4544 B b2554 t2553
4545 T t2554 o b2554 b4
4546 B b2555 t2554
4547 T t2555 o936 b2548 b2555
4548 B b2556 t2555
4549 P p1867 String "setSubstT << equal{id; op{inv{'s}; 's}} >> 2 thenAT autoT"
4550 O o1867 ext_rule p1867
4551 T t1868 o676 b567 b1861
4552 S s2556 t620 h h2540 h2541 h2550
4553 G s2556 t1868
4554 B b2557 s2556
4555 T t2557 o938 b2557 b2538
4556 B b2558 t2557
4557 T t1870 o738 b567 b1861
4558 S s2558 t620 h h2540 h2541 h2550
4559 G s2558 t1870
4560 B b2559 s2558
4561 T t2559 o938 b2559 b2538
4562 B b2560 t2559
4563 T t2560 o2 b2554
4564 B b2561 t2560
4565 T t2561 o966 b2560 b983 b2561
4566 B b2562 t2561
4567 T t2562 o2 b2562
4568 B b2563 t2562
4569 T t2563 o966 b2558 b4 b2563
4570 B b2564 t2563
4571 T t1876 o738 b1845 b1861
4572 H h2564 v_3 t1876
4573 S s2564 t620 h h2540 h2541 h2550 h2564
4574 G s2564 t1849
4575 B b2565 s2564
4576 T t2565 o938 b2565 b2538
4577 B b2566 t2565
4578 T t2566 o937 b2566 b4 b2561
4579 B b2567 t2566
4580 T t2567 o b2567 b4
4581 B b2568 t2567
4582 T t2568 o b2564 b2568
4583 B b2569 t2568
4584 T t2569 o936 b2554 b2569
4585 B b2570 t2569
4586 P p1891 String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
4587 O o1891 ext_rule p1891
4588 T t2570 o936 b2564 b4
4589 B b2571 t2570
4590 T t2571 o1891 b935 b2571 b4 b4
4591 B b2572 t2571
4592 P p1893 String "groupCancelRightT << 's >> thenT autoT"
4593 O o1893 ext_rule p1893
4594 T t2572 o936 b2567 b4
4595 B b2573 t2572
4596 T t2573 o1893 b935 b2573 b4 b4
4597 B b2574 t2573
4598 T t2574 o b2574 b4
4599 B b2575 t2574
4600 T t2575 o b2572 b2575
4601 B b2576 t2575
4602 T t2576 o1867 b935 b2570 b2576 b4
4603 B b2577 t2576
4604 T t2577 o b2577 b4
4605 B b2578 t2577
4606 T t2578 o1854 b935 b2556 b2578 b4
4607 B b2579 t2578
4608 T t2579 o b2579 b4
4609 B b2580 t2579
4610 T t2580 o2532 b935 b2550 b2580 b4
4611 B b2581 t2580
4612 T t2581 o933 b2581
4613 B b2582 t2581
4614 P p1677 Number 6230
4615 P p1678 Number 6238
4616 O o1678 resource_defs p1677 p1678 p264
4617 P p1679 Number 6236
4618 O o1679 uid p1679 p1678
4619 T t1679 o1679 b626
4620 B b1679 t1679
4621 T t1680 o b1679 b4
4622 B b1680 t1680
4623 T t1681 o1678 b1680
4624 B b1681 t1681
4625 T t1682 o b1681 b4
4626 B b1682 t1682
4627 T t1683 o2511 b618 b2532 b2582 b1682
4628 B b1683 t1683
4629 T t1684 o1676 b1683
4630 B b1684 t1684
4631 P p1684 Number 6586
4632 P p1685 Number 6967
4633 O o1685 location p1684 p1685
4634 P p2591 String unique_inv2
4635 O o2591 rule p2591
4636 T t2591 o738 b574 b561
4637 S s2591 t620 h
4638 G s2591 t2591
4639 B b2591 s2591
4640 T t2592 o618 b2591
4641 B b2592 t2592
4642 T t2593 o635 b2514 b2592
4643 B b2593 t2593
4644 T t2594 o635 b2512 b2593
4645 B b2594 t2594
4646 T t2595 o635 b658 b2594
4647 B b2595 t2595
4648 T t2596 o635 b794 b2595
4649 B b2596 t2596
4650 T t2597 o635 b641 b2596
4651 B b2597 t2597
4652 T t2598 o635 b711 b2597
4653 B b2598 t2598
4654 P p2598 String "assumT 5 thenT assumT 6 thenT assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
4655 O o2598 ext_rule p2598
4656 T t2599 o938 b2591 b2538
4657 B b2599 t2599
4658 T t2600 o937 b2599 b4 b946
4659 B b2600 t2600
4660 S s2600 t620 h h2540 h2541 h2550
4661 G s2600 t2591
4662 B b2601 s2600
4663 T t2601 o938 b2601 b2538
4664 B b2602 t2601
4665 S s2602 t620 h h2540 h2541
4666 G s2602 t2591
4667 B b2603 s2602
4668 T t2603 o938 b2603 b2538
4669 B b2604 t2603
4670 S s2604 t620 h h2540
4671 G s2604 t2591
4672 B b2605 s2604
4673 T t2605 o938 b2605 b2538
4674 B b2606 t2605
4675 T t2606 o2 b2600
4676 B b2607 t2606
4677 T t2607 o937 b2606 b4 b2607
4678 B b2608 t2607
4679 T t2608 o2 b2608
4680 B b2609 t2608
4681 T t2609 o937 b2604 b4 b2609
4682 B b2610 t2609
4683 T t2610 o2 b2610
4684 B b2611 t2610
4685 T t2611 o937 b2602 b4 b2611
4686 B b2612 t2611
4687 T t2612 o b2612 b4
4688 B b2613 t2612
4689 T t2613 o936 b2600 b2613
4690 B b2614 t2613
4691 T t2614 o2 b2612
4692 B b2615 t2614
4693 T t2615 o966 b2560 b983 b2615
4694 B b2616 t2615
4695 T t2616 o2 b2616
4696 B b2617 t2616
4697 T t2617 o966 b2558 b4 b2617
4698 B b2618 t2617
4699 S s2618 t620 h h2540 h2541 h2550 h2564
4700 G s2618 t2591
4701 B b2619 s2618
4702 T t2619 o938 b2619 b2538
4703 B b2620 t2619
4704 T t2620 o937 b2620 b4 b2615
4705 B b2621 t2620
4706 T t2621 o b2621 b4
4707 B b2622 t2621
4708 T t2622 o b2618 b2622
4709 B b2623 t2622
4710 T t2623 o936 b2612 b2623
4711 B b2624 t2623
4712 T t2624 o936 b2618 b4
4713 B b2625 t2624
4714 T t2625 o1891 b935 b2625 b4 b4
4715 B b2626 t2625
4716 P p2626 String "assertT << equal{'s2; inv{'s}} >> thenT autoT"
4717 O o2626 ext_rule p2626
4718 H h2626 v_4 t1849
4719 T t2626 o676 b574 b561
4720 S s2626 t620 h h2540 h2541 h2550 h2564 h2626
4721 G s2626 t2626
4722 B b2627 s2626
4723 T t2627 o938 b2627 b2538
4724 B b2628 t2627
4725 S s2628 t620 h h2540 h2541 h2550 h2564 h2626
4726 G s2628 t2591
4727 B b2629 s2628
4728 T t2629 o938 b2629 b2538
4729 B b2630 t2629
4730 T t2630 o2 b2621
4731 B b2631 t2630
4732 T t2631 o937 b2630 b983 b2631
4733 B b2632 t2631
4734 T t2632 o2 b2632
4735 B b2633 t2632
4736 T t2633 o937 b2628 b4 b2633
4737 B b2634 t2633
4738 T t2634 o b2634 b4
4739 B b2635 t2634
4740 T t2635 o936 b2621 b2635
4741 B b2636 t2635
4742 P p2636 String "rwh unfold_equal 6 thenT autoT thenT eqSetSymT thenT autoT"
4743 O o2636 ext_rule p2636
4744 T t2636 o936 b2634 b4
4745 B b2637 t2636
4746 T t2637 o2636 b935 b2637 b4 b4
4747 B b2638 t2637
4748 T t2638 o b2638 b4
4749 B b2639 t2638
4750 T t2639 o2626 b935 b2636 b2639 b4
4751 B b2640 t2639
4752 T t2640 o b2640 b4
4753 B b2641 t2640
4754 T t2641 o b2626 b2641
4755 B b2642 t2641
4756 T t2642 o1867 b935 b2624 b2642 b4
4757 B b2643 t2642
4758 T t2643 o b2643 b4
4759 B b2644 t2643
4760 T t2644 o2598 b935 b2614 b2644 b4
4761 B b2645 t2644
4762 T t2645 o933 b2645
4763 B b2646 t2645
4764 P p1686 Number 6613
4765 P p1687 Number 6621
4766 O o1687 resource_defs p1686 p1687 p264
4767 P p1688 Number 6619
4768 O o1688 uid p1688 p1687
4769 T t1688 o1688 b626
4770 B b1688 t1688
4771 T t1689 o b1688 b4
4772 B b1689 t1689
4773 T t1690 o1687 b1689
4774 B b1690 t1690
4775 T t1691 o b1690 b4
4776 B b1691 t1691
4777 T t1692 o2591 b618 b2598 b2646 b1691
4778 B b1692 t1692
4779 T t1693 o1685 b1692
4780 B b1693 t1693
4781 P p1693 Number 7018
4782 P p1694 Number 7437
4783 O o1694 location p1693 p1694
4784 P p1913 String unique_sol1
4785 O o1913 rule p1913
4786 P p1914 Var a
4787 O o1914 var p1914
4788 T t1914 o1914
4789 B b1914 t1914
4790 T t1915 o620 b1914
4791 S s1915 t637 h
4792 G s1915 t1915
4793 B b1915 s1915
4794 T t1916 o618 b1915
4795 B b1916 t1916
4796 P p1916 Var b
4797 O o1916 var p1916
4798 T t1917 o1916
4799 B b1917 t1917
4800 T t1918 o620 b1917
4801 S s1918 t637 h
4802 G s1918 t1918
4803 B b1918 s1918
4804 T t1919 o618 b1918
4805 B b1919 t1919
4806 P p1919 Var x
4807 O o1919 var p1919
4808 T t1920 o1919
4809 B b1920 t1920
4810 T t1921 o620 b1920
4811 S s1921 t637 h
4812 G s1921 t1921
4813 B b1921 s1921
4814 T t1922 o618 b1921
4815 B b1922 t1922
4816 T t1923 o655 b1914 b554
4817 S s1923 t620 h
4818 G s1923 t1923
4819 B b1923 s1923
4820 T t1924 o618 b1923
4821 B b1924 t1924
4822 T t1925 o655 b1917 b554
4823 S s1925 t620 h
4824 G s1925 t1925
4825 B b1925 s1925
4826 T t1926 o618 b1925
4827 B b1926 t1926
4828 T t1927 o655 b1920 b554
4829 S s1927 t620 h
4830 G s1927 t1927
4831 B b1927 s1927
4832 T t1928 o618 b1927
4833 B b1928 t1928
4834 T t1929 o559 b1914 b1920
4835 B b1929 t1929
4836 T t1930 o738 b1929 b1917
4837 S s1930 t620 h
4838 G s1930 t1930
4839 B b1930 s1930
4840 T t1931 o618 b1930
4841 B b1931 t1931
4842 T t1932 o572 b1914
4843 B b1932 t1932
4844 T t1933 o559 b1932 b1917
4845 B b1933 t1933
4846 T t1934 o738 b1920 b1933
4847 S s1934 t620 h
4848 G s1934 t1934
4849 B b1934 s1934
4850 T t1935 o618 b1934
4851 B b1935 t1935
4852 T t1936 o635 b1931 b1935
4853 B b1936 t1936
4854 T t1937 o635 b1928 b1936
4855 B b1937 t1937
4856 T t1938 o635 b1926 b1937
4857 B b1938 t1938
4858 T t1939 o635 b1924 b1938
4859 B b1939 t1939
4860 T t1940 o635 b1922 b1939
4861 B b1940 t1940
4862 T t1941 o635 b1919 b1940
4863 B b1941 t1941
4864 T t1942 o635 b1916 b1941
4865 B b1942 t1942
4866 P p1942 String "assumT 7 thenT rwh unfold_equal 2 thenT autoT thenT assertT << equal{op{inv{'a}; op{'a; 'x}}; op{inv{'a}; 'b}} >> thenWT autoT"
4867 O o1942 ext_rule p1942
4868 T t1943 o b1930 b4
4869 B b1943 t1943
4870 T t1944 o b1927 b1943
4871 B b1944 t1944
4872 T t1945 o b1925 b1944
4873 B b1945 t1945
4874 T t1946 o b1923 b1945
4875 B b1946 t1946
4876 T t1947 o b1921 b1946
4877 B b1947 t1947
4878 T t1948 o b1918 b1947
4879 B b1948 t1948
4880 T t1949 o b1915 b1948
4881 B b1949 t1949
4882 T t1950 o938 b1934 b1949
4883 B b1950 t1950
4884 T t1951 o937 b1950 b4 b946
4885 B b1951 t1951
4886 T t1952 o620 b1929
4887 H h1952 y_1 t1952
4888 H h1953 z_1 t1918
4889 T t1953 o676 b1929 b1917
4890 H h1954 z t1953
4891 T t1954 o559 b1932 b1929
4892 B b1954 t1954
4893 T t1955 o738 b1954 b1933
4894 S s1955 t620 h h1952 h1953 h1954
4895 G s1955 t1955
4896 B b1955 s1955
4897 T t1956 o938 b1955 b1949
4898 B b1956 t1956
4899 T t1957 o676 b1920 b1933
4900 S s1957 t620 h h1952 h1953 h1954
4901 G s1957 t1957
4902 B b1957 s1957
4903 T t1958 o938 b1957 b1949
4904 B b1958 t1958
4905 S s1958 t620 h h1952 h1953 h1954
4906 G s1958 t1934
4907 B b1959 s1958
4908 T t1959 o938 b1959 b1949
4909 B b1960 t1959
4910 B b1961 t1952
4911 B b1962 t1918
4912 T t1962 o1270 b1961 b1962
4913 H h1962 y t1962
4914 S s1962 t620 h h1962 h1954
4915 G s1962 t1934
4916 B b1963 s1962
4917 T t1963 o938 b1963 b1949
4918 B b1964 t1963
4919 B b1965 t1962
4920 B b1966 t1953
4921 T t1966 o1270 b1965 b1966
4922 H h1966 v t1966
4923 S s1966 t620 h h1966
4924 G s1966 t1934
4925 B b1967 s1966
4926 T t1967 o938 b1967 b1949
4927 B b1968 t1967
4928 H h1968 v t1930
4929 S s1968 t620 h h1968
4930 G s1968 t1934
4931 B b1969 s1968
4932 T t1969 o938 b1969 b1949
4933 B b1970 t1969
4934 T t1970 o2 b1951
4935 B b1971 t1970
4936 T t1971 o937 b1970 b4 b1971
4937 B b1972 t1971
4938 T t1972 o2 b1972
4939 B b1973 t1972
4940 T t1973 o937 b1968 b4 b1973
4941 B b1974 t1973
4942 T t1974 o2 b1974
4943 B b1975 t1974
4944 T t1975 o937 b1964 b4 b1975
4945 B b1976 t1975
4946 T t1976 o2 b1976
4947 B b1977 t1976
4948 T t1977 o937 b1960 b983 b1977
4949 B b1978 t1977
4950 T t1978 o2 b1978
4951 B b1979 t1978
4952 T t1979 o937 b1958 b4 b1979
4953 B b1980 t1979
4954 T t1980 o2 b1980
4955 B b1981 t1980
4956 T t1981 o947 b1956 b4 b1981
4957 B b1982 t1981
4958 H h1982 v t1955
4959 S s1982 t620 h h1952 h1953 h1954 h1982
4960 G s1982 t1957
4961 B b1983 s1982
4962 T t1983 o938 b1983 b1949
4963 B b1984 t1983
4964 T t1984 o937 b1984 b4 b1981
4965 B b1985 t1984
4966 T t1985 o b1985 b4
4967 B b1986 t1985
4968 T t1986 o b1982 b1986
4969 B b1987 t1986
4970 T t1987 o936 b1951 b1987
4971 B b1988 t1987
4972 T t1988 o936 b1982 b4
4973 B b1989 t1988
4974 T t1989 o990 b935 b1989 b4 b4
4975 B b1990 t1989
4976 P p1990 String "setSubstT << equal{op{inv{'a}; op{'a; 'x}}; op{op{inv{'a}; 'a}; 'x}} >> 5 thenT autoT"
4977 O o1990 ext_rule p1990
4978 T t1990 o559 b1932 b1914
4979 B b1991 t1990
4980 T t1991 o559 b1991 b1920
4981 B b1992 t1991
4982 T t1992 o738 b1992 b1933
4983 H h1992 v_1 t1992
4984 S s1992 t620 h h1952 h1953 h1954 h1982 h1992
4985 G s1992 t1957
4986 B b1993 s1992
4987 T t1993 o938 b1993 b1949
4988 B b1994 t1993
4989 T t1994 o2 b1985
4990 B b1995 t1994
4991 T t1995 o937 b1994 b4 b1995
4992 B b1996 t1995
4993 T t566 o b1996 b4
4994 B b566 t566
4995 T t570 o936 b1985 b566
4996 B b570 t570
4997 B b1997 t1933 v_1
4998 T t1997 o711 b1997
4999 S s1997 t620 h h1952 h1953 h1954 h1982
5000 G s1997 t1997
5001 B b1998 s1997
5002 T t1998 o938 b1998 b1949
5003 B b1999 t1998
5004 T t1999 o738 b1220 b1933
5005 B b2000 t1999 v_1
5006 T t2000 o976 b2000
5007 S s2000 t620 h h1952 h1953 h1954 h1982
5008 G s2000 t2000
5009 B b2001 s2000
5010 T t2001 o938 b2001 b1949
5011 B b2002 t2001
5012 T t2002 o973 b2002 b983 b1995
5013 B b2003 t2002
5014 T t2003 o2 b2003
5015 B b2004 t2003
5016 T t2004 o973 b1999 b4 b2004
5017 B b2005 t2004
5018 P p2008 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"
5019 O o2008 ext_rule p2008
5020 T t2008 o559 b567 b1920
5021 B b2009 t2008
5022 T t2009 o738 b2009 b1933
5023 H h2009 v_2 t2009
5024 S s2009 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5025 G s2009 t1957
5026 B b2010 s2009
5027 T t2010 o938 b2010 b1949
5028 B b2011 t2010
5029 T t2011 o2 b1996
5030 B b2012 t2011
5031 T t2012 o937 b2011 b4 b2012
5032 B b2013 t2012
5033 T t571 o b2013 b4
5034 B b571 t571
5035 T t572 o936 b1996 b571
5036 B b572 t572
5037 B b2014 t1933 v_2
5038 T t2014 o711 b2014
5039 S s2014 t620 h h1952 h1953 h1954 h1982 h1992
5040 G s2014 t2014
5041 B b2015 s2014
5042 T t2015 o938 b2015 b1949
5043 B b2016 t2015
5044 T t2016 o559 b977 b1920
5045 B b2017 t2016
5046 T t2017 o738 b2017 b1933
5047 B b2018 t2017 v_2
5048 T t2018 o976 b2018
5049 S s2018 t620 h h1952 h1953 h1954 h1982 h1992
5050 G s2018 t2018
5051 B b2019 s2018
5052 T t2019 o938 b2019 b1949
5053 B b2020 t2019
5054 T t2020 o973 b2020 b983 b2012
5055 B b2021 t2020
5056 T t2021 o2 b2021
5057 B b2022 t2021
5058 T t2022 o973 b2016 b4 b2022
5059 B b2023 t2022
5060 P p2026 String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"
5061 O o2026 ext_rule p2026
5062 H h2026 v_3 t1934
5063 S s2026 t620 h h1952 h1953 h1954 h1982 h1992 h2009 h2026
5064 G s2026 t1957
5065 B b2027 s2026
5066 T t2027 o938 b2027 b1949
5067 B b2028 t2027
5068 T t2028 o2 b2013
5069 B b2029 t2028
5070 T t2029 o937 b2028 b4 b2029
5071 B b2030 t2029
5072 T t577 o b2030 b4
5073 B b577 t577
5074 T t578 o936 b2013 b577
5075 B b578 t578
5076 B b2031 t1933 v_3
5077 T t2031 o711 b2031
5078 S s2031 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5079 G s2031 t2031
5080 B b2032 s2031
5081 T t2032 o938 b2032 b1949
5082 B b2033 t2032
5083 T t2033 o738 b1004 b1933
5084 B b2034 t2033 v_3
5085 T t2034 o976 b2034
5086 S s2034 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5087 G s2034 t2034
5088 B b2035 s2034
5089 T t2035 o938 b2035 b1949
5090 B b2036 t2035
5091 T t2036 o973 b2036 b983 b2029
5092 B b2037 t2036
5093 T t2037 o2 b2037
5094 B b2038 t2037
5095 T t2038 o973 b2033 b4 b2038
5096 B b2039 t2038
5097 P p2042 String "rwh unfold_equal 8 thenT autoT"
5098 O o2042 ext_rule p2042
5099 T t2042 o936 b2030 b4
5100 B b2043 t2042
5101 T t2043 o2042 b935 b2043 b4 b4
5102 B b2044 t2043
5103 T t586 o b2044 b4
5104 B b586 t586
5105 T t2044 o936 b2039 b4
5106 B b2045 t2044
5107 T t2045 o1071 b935 b2045 b4 b4
5108 B b2046 t2045
5109 T t2046 o b2046 b4
5110 B b2047 t2046
5111 T t587 o2026 b935 b578 b586 b2047
5112 B b587 t587
5113 T t593 o b587 b4
5114 B b593 t593
5115 T t2049 o936 b2023 b4
5116 B b2050 t2049
5117 T t2050 o1071 b935 b2050 b4 b4
5118 B b2051 t2050
5119 T t2051 o b2051 b4
5120 B b2052 t2051
5121 T t594 o2008 b935 b572 b593 b2052
5122 B b594 t594
5123 T t607 o b594 b4
5124 B b607 t607
5125 T t2054 o936 b2005 b4
5126 B b2055 t2054
5127 T t2055 o1071 b935 b2055 b4 b4
5128 B b2056 t2055
5129 T t2058 o738 b1954 b1992
5130 S s2058 t620 h h1952 h1953 h1954 h1982
5131 G s2058 t2058
5132 B b2059 s2058
5133 T t2059 o938 b2059 b1949
5134 B b2060 t2059
5135 T t2060 o966 b2060 b4 b1995
5136 B b2061 t2060
5137 T t2061 o936 b2061 b4
5138 B b2062 t2061
5139 T t2062 o990 b935 b2062 b4 b4
5140 B b2063 t2062
5141 P p2063 String "rwh unfold_fun_prop 0 thenT autoT thenT rwh unfold_equal 9 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 11 thenT autoT"
5142 O o2063 ext_rule p2063
5143 T t2063 o973 b2002 b4 b1995
5144 B b2064 t2063
5145 T t615 o936 b2064 b4
5146 B b615 t615
5147 H h2064 x_1 t1344
5148 H h2065 y_2 t638
5149 T t2065 o620 b1933
5150 H h2066 z_3 t2065
5151 T t2066 o676 b560 b1933
5152 H h2067 z_2 t2066
5153 S s2067 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5154 G s2067 t1997
5155 B b2067 s2067
5156 T t2067 o938 b2067 b1949
5157 B b2068 t2067
5158 T t2068 o676 b1220 b1933
5159 B b2069 t2068 v_1
5160 T t2069 o976 b2069
5161 S s2069 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5162 G s2069 t2069
5163 B b2070 s2069
5164 T t2070 o938 b2070 b1949
5165 B b2071 t2070
5166 T t2071 o676 b561 b1933
5167 S s2071 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5168 G s2071 t2071
5169 B b2072 s2071
5170 T t2072 o938 b2072 b1949
5171 B b2073 t2072
5172 B b2074 t638
5173 B b2075 t2065
5174 T t2075 o1270 b2074 b2075
5175 H h2075 y t2075
5176 S s2075 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2075 h2067
5177 G s2075 t2071
5178 B b2076 s2075
5179 T t2076 o938 b2076 b1949
5180 B b2077 t2076
5181 B b2078 t2075
5182 B b2079 t2066
5183 T t2079 o1270 b2078 b2079
5184 H h2079 x_2 t2079
5185 S s2079 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2079
5186 G s2079 t2071
5187 B b2080 s2079
5188 T t2080 o938 b2080 b1949
5189 B b2081 t2080
5190 T t2081 o738 b560 b1933
5191 H h2081 x_2 t2081
5192 S s2081 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5193 G s2081 t2071
5194 B b2082 s2081
5195 T t2082 o938 b2082 b1949
5196 B b2083 t2082
5197 T t2083 o738 b561 b1933
5198 S s2083 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5199 G s2083 t2083
5200 B b2084 s2083
5201 T t2084 o938 b2084 b1949
5202 B b2085 t2084
5203 B b2086 t2081
5204 B b2087 t2083
5205 T t2087 o1177 b2086 b2087
5206 S s2087 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064
5207 G s2087 t2087
5208 B b2088 s2087
5209 T t2088 o938 b2088 b1949
5210 B b2089 t2088
5211 B b2090 t2087
5212 T t2090 o1177 b1347 b2090
5213 S s2090 t620 h h1952 h1953 h1954 h1982 h1344 h1224
5214 G s2090 t2090
5215 B b2091 s2090
5216 T t2091 o938 b2091 b1949
5217 B b2092 t2091
5218 B b2093 t2090 s2
5219 T t2093 o1185 b1186 b2093
5220 S s2093 t620 h h1952 h1953 h1954 h1982 h1344
5221 G s2093 t2093
5222 B b2094 s2093
5223 T t2094 o938 b2094 b1949
5224 B b2095 t2094
5225 B b2096 t2093 s1
5226 T t2096 o1185 b1186 b2096
5227 S s2096 t620 h h1952 h1953 h1954 h1982
5228 G s2096 t2096
5229 B b2097 s2096
5230 T t2097 o938 b2097 b1949
5231 B b2098 t2097
5232 T t2098 o2 b2064
5233 B b2099 t2098
5234 T t2099 o973 b2098 b983 b2099
5235 B b2100 t2099
5236 T t2100 o2 b2100
5237 B b2101 t2100
5238 T t2101 o937 b2095 b983 b2101
5239 B b2102 t2101
5240 T t2102 o2 b2102
5241 B b2103 t2102
5242 T t2103 o937 b2092 b983 b2103
5243 B b2104 t2103
5244 T t2104 o2 b2104
5245 B b2105 t2104
5246 T t2105 o937 b2089 b983 b2105
5247 B b2106 t2105
5248 T t2106 o2 b2106
5249 B b2107 t2106
5250 T t2107 o937 b2085 b983 b2107
5251 B b2108 t2107
5252 T t2108 o2 b2108
5253 B b2109 t2108
5254 T t2109 o937 b2083 b4 b2109
5255 B b2110 t2109
5256 T t2110 o2 b2110
5257 B b2111 t2110
5258 T t2111 o937 b2081 b4 b2111
5259 B b2112 t2111
5260 T t2112 o2 b2112
5261 B b2113 t2112
5262 T t2113 o937 b2077 b4 b2113
5263 B b2114 t2113
5264 T t2114 o2 b2114
5265 B b2115 t2114
5266 T t2115 o937 b2073 b4 b2115
5267 B b2116 t2115
5268 T t2116 o2 b2116
5269 B b2117 t2116
5270 T t2117 o973 b2071 b983 b2117
5271 B b2118 t2117
5272 T t2118 o2 b2118
5273 B b2119 t2118
5274 T t2119 o973 b2068 b4 b2119
5275 B b2120 t2119
5276 T t2122 o936 b2120 b4
5277 B b2123 t2122
5278 T t2123 o1071 b935 b2123 b4 b4
5279 B b2124 t2123
5280 T t2124 o b2124 b4
5281 B b2125 t2124
5282 T t616 o2063 b935 b615 b4 b2125
5283 B b616 t616
5284 T t624 o b616 b4
5285 B b624 t624
5286 T t625 o b2063 b624
5287 B b625 t625
5288 T t633 o b2056 b625
5289 B b633 t633
5290 T t634 o1990 b935 b570 b607 b633
5291 B b634 t634
5292 T t635 o b634 b4
5293 B b635 t635
5294 T t646 o b1990 b635
5295 B b646 t646
5296 T t653 o1942 b935 b1988 b646 b4
5297 B b653 t653
5298 T t654 o933 b653
5299 B b654 t654
5300 P p1695 Number 7045
5301 P p1696 Number 7053
5302 O o1696 resource_defs p1695 p1696 p264
5303 P p1697 Number 7051
5304 O o1698 uid p1697 p1696
5305 T t1698 o1698 b626
5306 B b1698 t1698
5307 T t1699 o b1698 b4
5308 B b1699 t1699
5309 T t1700 o1696 b1699
5310 B b1700 t1700
5311 T t1701 o b1700 b4
5312 B b1701 t1701
5313 T t1702 o1913 b618 b1942 b654 b1701
5314 B b1702 t1702
5315 T t1703 o1694 b1702
5316 B b1703 t1703
5317 P p1703 Number 7488
5318 P p1704 Number 7907
5319 O o1704 location p1703 p1704
5320 P p2142 String unique_sol2
5321 O o2142 rule p2142
5322 P p2143 Var y
5323 O o2143 var p2143
5324 T t2143 o2143
5325 B b2143 t2143
5326 T t2144 o620 b2143
5327 S s2144 t637 h
5328 G s2144 t2144
5329 B b2144 s2144
5330 T t2145 o618 b2144
5331 B b2145 t2145
5332 T t2146 o655 b2143 b554
5333 S s2146 t620 h
5334 G s2146 t2146
5335 B b2146 s2146
5336 T t2147 o618 b2146
5337 B b2147 t2147
5338 T t2148 o559 b2143 b1914
5339 B b2148 t2148
5340 T t2149 o738 b2148 b1917
5341 S s2149 t620 h
5342 G s2149 t2149
5343 B b2149 s2149
5344 T t2150 o618 b2149
5345 B b2150 t2150
5346 T t2151 o559 b1917 b1932
5347 B b2151 t2151
5348 T t2152 o738 b2143 b2151
5349 S s2152 t620 h
5350 G s2152 t2152
5351 B b2152 s2152
5352 T t2153 o618 b2152
5353 B b2153 t2153
5354 T t2154 o635 b2150 b2153
5355 B b2154 t2154
5356 T t2155 o635 b2147 b2154
5357 B b2155 t2155
5358 T t2156 o635 b1926 b2155
5359 B b2156 t2156
5360 T t2157 o635 b1924 b2156
5361 B b2157 t2157
5362 T t2158 o635 b2145 b2157
5363 B b2158 t2158
5364 T t2159 o635 b1919 b2158
5365 B b2159 t2159
5366 T t2160 o635 b1916 b2159
5367 B b2160 t2160
5368 P p2160 String "assumT 7 thenT assertT << equal{op{op{'y; 'a}; inv{'a}}; op{'b; inv{'a}}} >> thenT autoT"
5369 O o2160 ext_rule p2160
5370 T t2161 o b2149 b4
5371 B b2161 t2161
5372 T t2162 o b2146 b2161
5373 B b2162 t2162
5374 T t2163 o b1925 b2162
5375 B b2163 t2163
5376 T t2164 o b1923 b2163
5377 B b2164 t2164
5378 T t2165 o b2144 b2164
5379 B b2165 t2165
5380 T t2166 o b1918 b2165
5381 B b2166 t2166
5382 T t2167 o b1915 b2166
5383 B b2167 t2167
5384 T t2168 o938 b2152 b2167
5385 B b2168 t2168
5386 T t2169 o937 b2168 b4 b946
5387 B b2169 t2169
5388 H h2169 v t2149
5389 T t2170 o676 b2148 b1917
5390 S s2170 t620 h h2169
5391 G s2170 t2170
5392 B b2170 s2170
5393 T t2171 o938 b2170 b2167
5394 B b2171 t2171
5395 T t2172 o559 b2148 b1932
5396 B b2172 t2172
5397 T t2173 o676 b2172 b2151
5398 S s2173 t620 h h2169
5399 G s2173 t2173
5400 B b2173 s2173
5401 T t2174 o938 b2173 b2167
5402 B b2174 t2174
5403 T t2175 o738 b2172 b2151
5404 S s2175 t620 h h2169
5405 G s2175 t2175
5406 B b2175 s2175
5407 T t2176 o938 b2175 b2167
5408 B b2176 t2176
5409 S s2176 t620 h h2169
5410 G s2176 t2152
5411 B b2177 s2176
5412 T t2177 o938 b2177 b2167
5413 B b2178 t2177
5414 T t2178 o2 b2169
5415 B b2179 t2178
5416 T t2179 o937 b2178 b4 b2179
5417 B b2180 t2179
5418 T t2180 o2 b2180
5419 B b2181 t2180
5420 T t2181 o947 b2176 b983 b2181
5421 B b2182 t2181
5422 T t2182 o2 b2182
5423 B b2183 t2182
5424 T t2183 o947 b2174 b983 b2183
5425 B b2184 t2183
5426 T t2184 o2 b2184
5427 B b2185 t2184
5428 T t2185 o947 b2171 b4 b2185
5429 B b2186 t2185
5430 H h2186 v_1 t2175
5431 T t2186 o676 b2143 b2151
5432 S s2186 t620 h h2169 h2186
5433 G s2186 t2186
5434 B b2187 s2186
5435 T t2187 o938 b2187 b2167
5436 B b2188 t2187
5437 S s2188 t620 h h2169 h2186
5438 G s2188 t2152
5439 B b2189 s2188
5440 T t2189 o938 b2189 b2167
5441 B b2190 t2189
5442 T t2190 o937 b2190 b983 b2181
5443 B b2191 t2190
5444 T t2191 o2 b2191
5445 B b2192 t2191
5446 T t2192 o937 b2188 b4 b2192
5447 B b2193 t2192
5448 T t2193 o b2193 b4
5449 B b2194 t2193
5450 T t2194 o b2186 b2194
5451 B b2195 t2194
5452 T t2195 o936 b2169 b2195
5453 B b2196 t2195
5454 P p2196 String "rwh unfold_equal 2 thenT autoT"
5455 O o2196 ext_rule p2196
5456 T t2196 o936 b2186 b4
5457 B b2197 t2196
5458 T t2197 o2196 b935 b2197 b4 b4
5459 B b2198 t2197
5460 P p2198 String "setSubstT << equal{op{op{'y; 'a}; inv{'a}}; op{'y; op{'a; inv{'a}}}} >> 3 thenT autoT"
5461 O o2198 ext_rule p2198
5462 T t2198 o559 b1914 b1932
5463 B b2199 t2198
5464 T t2199 o559 b2143 b2199
5465 B b2200 t2199
5466 T t2200 o738 b2200 b2151
5467 H h2200 v_2 t2200
5468 S s2200 t620 h h2169 h2186 h2200
5469 G s2200 t2186
5470 B b2201 s2200
5471 T t2201 o938 b2201 b2167
5472 B b2202 t2201
5473 T t2202 o2 b2193
5474 B b2203 t2202
5475 T t2203 o937 b2202 b4 b2203
5476 B b2204 t2203
5477 T t673 o b2204 b4
5478 B b673 t673
5479 T t687 o936 b2193 b673
5480 B b687 t687
5481 B b2205 t2151 v_2
5482 T t2205 o711 b2205
5483 S s2205 t620 h h2169 h2186
5484 G s2205 t2205
5485 B b2206 s2205
5486 T t2206 o938 b2206 b2167
5487 B b2207 t2206
5488 T t2207 o738 b977 b2151
5489 B b2208 t2207 v_2
5490 T t2208 o976 b2208
5491 S s2208 t620 h h2169 h2186
5492 G s2208 t2208
5493 B b2209 s2208
5494 T t2209 o938 b2209 b2167
5495 B b2210 t2209
5496 T t2210 o973 b2210 b983 b2203
5497 B b2211 t2210
5498 T t2211 o2 b2211
5499 B b2212 t2211
5500 T t2212 o973 b2207 b4 b2212
5501 B b2213 t2212
5502 P p2216 String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"
5503 O o2216 ext_rule p2216
5504 T t2216 o559 b2143 b567
5505 B b2217 t2216
5506 T t2217 o738 b2217 b2151
5507 H h2217 v_3 t2217
5508 S s2217 t620 h h2169 h2186 h2200 h2217
5509 G s2217 t2186
5510 B b2218 s2217
5511 T t2218 o938 b2218 b2167
5512 B b2219 t2218
5513 T t2219 o2 b2204
5514 B b2220 t2219
5515 T t2220 o937 b2219 b4 b2220
5516 B b2221 t2220
5517 T t694 o b2221 b4
5518 B b694 t694
5519 T t703 o936 b2204 b694
5520 B b703 t703
5521 B b2222 t2151 v_3
5522 T t2222 o711 b2222
5523 S s2222 t620 h h2169 h2186 h2200
5524 G s2222 t2222
5525 B b2223 s2222
5526 T t2223 o938 b2223 b2167
5527 B b2224 t2223
5528 T t2224 o559 b2143 b1004
5529 B b2225 t2224
5530 T t2225 o738 b2225 b2151
5531 B b2226 t2225 v_3
5532 T t2226 o976 b2226
5533 S s2226 t620 h h2169 h2186 h2200
5534 G s2226 t2226
5535 B b2227 s2226
5536 T t2227 o938 b2227 b2167
5537 B b2228 t2227
5538 T t2228 o973 b2228 b983 b2220
5539 B b2229 t2228
5540 T t2229 o2 b2229
5541 B b2230 t2229
5542 T t2230 o973 b2224 b4 b2230
5543 B b2231 t2230
5544 P p2234 String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"
5545 O o2234 ext_rule p2234
5546 T t717 o936 b2221 b4
5547 B b717 t717
5548 T t2234 o620 b2217
5549 H h2234 y_2 t2234
5550 T t2235 o620 b2151
5551 H h2235 z_1 t2235
5552 T t2236 o676 b2217 b2151
5553 H h2236 z t2236
5554 S s2236 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5555 G s2236 t2222
5556 B b2236 s2236
5557 T t2237 o938 b2236 b2167
5558 B b2237 t2237
5559 T t2238 o676 b1004 b2151
5560 B b2238 t2238 v_3
5561 T t2239 o976 b2238
5562 S s2239 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5563 G s2239 t2239
5564 B b2239 s2239
5565 T t2240 o938 b2239 b2167
5566 B b2240 t2240
5567 S s2240 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5568 G s2240 t2186
5569 B b2241 s2240
5570 T t2241 o938 b2241 b2167
5571 B b2242 t2241
5572 B b2243 t2234
5573 B b2244 t2235
5574 T t2244 o1270 b2243 b2244
5575 H h2244 y_1 t2244
5576 S s2244 t620 h h2169 h2186 h2200 h2244 h2236
5577 G s2244 t2186
5578 B b2245 s2244
5579 T t2245 o938 b2245 b2167
5580 B b2246 t2245
5581 B b2247 t2244
5582 B b2248 t2236
5583 T t2248 o1270 b2247 b2248
5584 H h2248 v_3 t2248
5585 S s2248 t620 h h2169 h2186 h2200 h2248
5586 G s2248 t2186
5587 B b2249 s2248
5588 T t2249 o938 b2249 b2167
5589 B b2250 t2249
5590 T t2250 o2 b2221
5591 B b2251 t2250
5592 T t2251 o937 b2250 b4 b2251
5593 B b2252 t2251
5594 T t2252 o2 b2252
5595 B b2253 t2252
5596 T t2253 o937 b2246 b4 b2253
5597 B b2254 t2253
5598 T t2254 o2 b2254
5599 B b2255 t2254
5600 T t2255 o937 b2242 b4 b2255
5601 B b2256 t2255
5602 T t2256 o2 b2256
5603 B b2257 t2256
5604 T t2257 o973 b2240 b983 b2257
5605 B b2258 t2257
5606 T t2258 o2 b2258
5607 B b2259 t2258
5608 T t2259 o973 b2237 b4 b2259
5609 B b2260 t2259
5610 T t2262 o936 b2260 b4
5611 B b2263 t2262
5612 T t2263 o1071 b935 b2263 b4 b4
5613 B b2264 t2263
5614 T t2264 o b2264 b4
5615 B b2265 t2264
5616 T t724 o2234 b935 b717 b4 b2265
5617 B b724 t724
5618 T t729 o b724 b4
5619 B b729 t729
5620 T t2266 o936 b2231 b4
5621 B b2267 t2266
5622 T t2267 o1071 b935 b2267 b4 b4
5623 B b2268 t2267
5624 T t2268 o b2268 b4
5625 B b2269 t2268
5626 T t736 o2216 b935 b703 b729 b2269
5627 B b736 t736
5628 T t749 o b736 b4
5629 B b749 t749
5630 T t2271 o936 b2213 b4
5631 B b2272 t2271
5632 T t2272 o1071 b935 b2272 b4 b4
5633 B b2273 t2272
5634 T t2273 o b2273 b4
5635 B b2274 t2273
5636 T t756 o2198 b935 b687 b749 b2274
5637 B b756 t756
5638 T t765 o b756 b4
5639 B b765 t765
5640 T t772 o b2198 b765
5641 B b772 t772
5642 T t775 o2160 b935 b2196 b772 b4
5643 B b775 t775
5644 T t782 o933 b775
5645 B b782 t782
5646 P p1705 Number 7515
5647 P p1706 Number 7523
5648 O o1706 resource_defs p1705 p1706 p264
5649 P p1707 Number 7521
5650 O o1707 uid p1707 p1706
5651 T t1707 o1707 b626
5652 B b1707 t1707
5653 T t1708 o b1707 b4
5654 B b1708 t1708
5655 T t1709 o1706 b1708
5656 B b1709 t1709
5657 T t1710 o b1709 b4
5658 B b1710 t1710
5659 T t1711 o2142 b618 b2160 b782 b1710
5660 B b1711 t1711
5661 T t1712 o1704 b1711
5662 B b1712 t1712
5663 P p1712 Number 7935
5664 P p1713 Number 8230
5665 O o1713 location p1712 p1713
5666 P p2289 String inv_simplify
5667 O o2289 rule p2289
5668 T t2289 o559 b1914 b1917
5669 B b2289 t2289
5670 T t2290 o572 b2289
5671 B b2290 t2290
5672 T t2291 o572 b1917
5673 B b2291 t2291
5674 T t2292 o559 b2291 b1932
5675 B b2292 t2292
5676 T t2293 o738 b2290 b2292
5677 S s2293 t620 h
5678 G s2293 t2293
5679 B b2293 s2293
5680 T t2294 o618 b2293
5681 B b2294 t2294
5682 T t2295 o635 b1926 b2294
5683 B b2295 t2295
5684 T t2296 o635 b1924 b2295
5685 B b2296 t2296
5686 T t2297 o635 b1919 b2296
5687 B b2297 t2297
5688 T t2298 o635 b1916 b2297
5689 B b2298 t2298
5690 P p794 String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >>"
5691 O o794 ext_rule p794
5692 T t2299 o b1925 b4
5693 B b2299 t2299
5694 T t2300 o b1923 b2299
5695 B b2300 t2300
5696 T t2301 o b1918 b2300
5697 B b2301 t2301
5698 T t2302 o b1915 b2301
5699 B b2302 t2302
5700 T t2303 o938 b2293 b2302
5701 B b2303 t2303
5702 T t2304 o937 b2303 b4 b946
5703 B b2304 t2304
5704 T t2305 o559 b2290 b2289
5705 B b2305 t2305
5706 T t2306 o559 b2292 b2289
5707 B b2306 t2306
5708 T t2307 o738 b2305 b2306
5709 S s2307 t620 h
5710 G s2307 t2307
5711 B b2307 s2307
5712 T t2308 o938 b2307 b2302
5713 B b2308 t2308
5714 T t2309 o2 b2304
5715 B b2309 t2309
5716 T t2310 o947 b2308 b4 b2309
5717 B b2310 t2310
5718 H h2310 v t2307
5719 S s2310 t620 h h2310
5720 G s2310 t2293
5721 B b2311 s2310
5722 T t2311 o938 b2311 b2302
5723 B b2312 t2311
5724 T t2312 o937 b2312 b4 b2309
5725 B b2313 t2312
5726 T t2313 o b2313 b4
5727 B b2314 t2313
5728 T t2314 o b2310 b2314
5729 B b2315 t2314
5730 T t2315 o936 b2304 b2315
5731 B b2316 t2315
5732 P p2316 String "setSubstT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; id} >> 0 thenWT autoT"
5733 O o2316 ext_rule p2316
5734 T t2316 o738 b2305 b567
5735 S s2316 t620 h
5736 G s2316 t2316
5737 B b2317 s2316
5738 T t2317 o938 b2317 b2302
5739 B b2318 t2317
5740 T t2318 o2 b2310
5741 B b2319 t2318
5742 T t2319 o966 b2318 b4 b2319
5743 B b2320 t2319
5744 T t2320 o738 b567 b2306
5745 S s2320 t620 h
5746 G s2320 t2320
5747 B b2321 s2320
5748 T t2321 o938 b2321 b2302
5749 B b2322 t2321
5750 T t2322 o937 b2322 b4 b2319
5751 B b2323 t2322
5752 T t800 o b2323 b4
5753 B b800 t800
5754 T t807 o b2320 b800
5755 B b807 t807
5756 T t813 o936 b2310 b807
5757 B b813 t813
5758 P p2326 Var v
5759 O o2326 var p2326
5760 T t2326 o2326
5761 B b2327 t2326
5762 T t2337 o936 b2320 b4
5763 B b2338 t2337
5764 T t2338 o990 b935 b2338 b4 b4
5765 B b2339 t2338
5766 P p2339 String "setSubstT << equal{id; op{inv{'b}; op{inv{'a}; op{'a; 'b}}}} >> 0 thenWT autoT"
5767 O o2339 ext_rule p2339
5768 T t2339 o559 b1932 b2289
5769 B b2340 t2339
5770 T t2340 o559 b2291 b2340
5771 B b2341 t2340
5772 T t2341 o738 b567 b2341
5773 S s2341 t620 h
5774 G s2341 t2341
5775 B b2342 s2341
5776 T t2342 o938 b2342 b2302
5777 B b2343 t2342
5778 T t2343 o2 b2323
5779 B b2344 t2343
5780 T t2344 o966 b2343 b4 b2344
5781 B b2345 t2344
5782 T t2345 o738 b2341 b2306
5783 S s2345 t620 h
5784 G s2345 t2345
5785 B b2346 s2345
5786 T t2346 o938 b2346 b2302
5787 B b2347 t2346
5788 T t2347 o937 b2347 b4 b2344
5789 B b2348 t2347
5790 T t820 o b2348 b4
5791 B b820 t820
5792 T t821 o b2345 b820
5793 B b821 t821
5794 T t822 o936 b2323 b821
5795 B b822 t822
5796 P p2355 String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"
5797 O o2355 ext_rule p2355
5798 T t2355 o559 b1991 b1917
5799 B b2356 t2355
5800 T t2356 o738 b2340 b2356
5801 S s2356 t620 h
5802 G s2356 t2356
5803 B b2357 s2356
5804 T t2357 o938 b2357 b2302
5805 B b2358 t2357
5806 T t2358 o2 b2345
5807 B b2359 t2358
5808 T t2359 o966 b2358 b4 b2359
5809 B b2360 t2359
5810 T t2360 o559 b2291 b2356
5811 B b2361 t2360
5812 T t2361 o738 b567 b2361
5813 S s2361 t620 h
5814 G s2361 t2361
5815 B b2362 s2361
5816 T t2362 o938 b2362 b2302
5817 B b2363 t2362
5818 T t2363 o937 b2363 b4 b2359
5819 B b2364 t2363
5820 T t2364 o b2364 b4
5821 B b2365 t2364
5822 T t2365 o b2360 b2365
5823 B b2366 t2365
5824 T t2366 o936 b2345 b2366
5825 B b2367 t2366
5826 T t2367 o936 b2360 b4
5827 B b2368 t2367
5828 T t2368 o990 b935 b2368 b4 b4
5829 B b2369 t2368
5830 P p2369 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 0 thenWT autoT"
5831 O o2369 ext_rule p2369
5832 T t2369 o738 b1991 b567
5833 S s2369 t620 h
5834 G s2369 t2369
5835 B b2370 s2369
5836 T t2370 o938 b2370 b2302
5837 B b2371 t2370
5838 T t2371 o2 b2364
5839 B b2372 t2371
5840 T t2372 o966 b2371 b4 b2372
5841 B b2373 t2372
5842 T t2373 o559 b567 b1917
5843 B b2374 t2373
5844 T t2374 o559 b2291 b2374
5845 B b2375 t2374
5846 T t2375 o738 b567 b2375
5847 S s2375 t620 h
5848 G s2375 t2375
5849 B b2376 s2375
5850 T t2376 o938 b2376 b2302
5851 B b2377 t2376
5852 T t2377 o937 b2377 b4 b2372
5853 B b2378 t2377
5854 T t2378 o559 b2327 b1917
5855 B b2379 t2378
5856 T t2379 o559 b2291 b2379
5857 B b2380 t2379 v
5858 T t2380 o711 b2380
5859 S s2380 t620 h
5860 G s2380 t2380
5861 B b2381 s2380
5862 T t2381 o938 b2381 b2302
5863 B b2382 t2381
5864 B b2383 t2379
5865 T t2383 o738 b567 b2383
5866 B b2384 t2383 v
5867 T t2384 o976 b2384
5868 S s2384 t620 h
5869 G s2384 t2384
5870 B b2385 s2384
5871 T t2385 o938 b2385 b2302
5872 B b2386 t2385
5873 T t2386 o973 b2386 b983 b2372
5874 B b2387 t2386
5875 T t2387 o2 b2387
5876 B b2388 t2387
5877 T t2388 o973 b2382 b4 b2388
5878 B b2389 t2388
5879 T t2389 o b2389 b4
5880 B b2390 t2389
5881 T t2390 o b2378 b2390
5882 B b2391 t2390
5883 T t2391 o b2373 b2391
5884 B b2392 t2391
5885 T t2392 o936 b2364 b2392
5886 B b2393 t2392
5887 T t2393 o936 b2373 b4
5888 B b2394 t2393
5889 T t2394 o990 b935 b2394 b4 b4
5890 B b2395 t2394
5891 P p2395 String "setSubstT << equal{op{id; 'b}; 'b} >> 0 thenWT autoT"
5892 O o2395 ext_rule p2395
5893 T t2395 o738 b2374 b1917
5894 S s2395 t620 h
5895 G s2395 t2395
5896 B b2396 s2395
5897 T t2396 o938 b2396 b2302
5898 B b2397 t2396
5899 T t2397 o2 b2378
5900 B b2398 t2397
5901 T t2398 o966 b2397 b4 b2398
5902 B b2399 t2398
5903 T t2399 o559 b2291 b1917
5904 B b2400 t2399
5905 T t2400 o738 b567 b2400
5906 S s2400 t620 h
5907 G s2400 t2400
5908 B b2401 s2400
5909 T t2401 o938 b2401 b2302
5910 B b2402 t2401
5911 T t2402 o937 b2402 b4 b2398
5912 B b2403 t2402
5913 T t2403 o b2403 b4
5914 B b2404 t2403
5915 T t2404 o b2399 b2404
5916 B b2405 t2404
5917 T t2405 o936 b2378 b2405
5918 B b2406 t2405
5919 T t2406 o936 b2399 b4
5920 B b2407 t2406
5921 T t2407 o990 b935 b2407 b4 b4
5922 B b2408 t2407
5923 P p2408 String "setSubstT << equal{op{inv{'b}; 'b}; id} >> 0 thenT autoT"
5924 O o2408 ext_rule p2408
5925 T t2408 o936 b2403 b4
5926 B b2409 t2408
5927 T t2409 o2408 b935 b2409 b4 b4
5928 B b2410 t2409
5929 T t2410 o b2410 b4
5930 B b2411 t2410
5931 T t2411 o b2408 b2411
5932 B b2412 t2411
5933 T t2412 o2395 b935 b2406 b2412 b4
5934 B b2413 t2412
5935 P p2413 String "rwh unfold_fun_set 0 thenT dT 0"
5936 O o2413 ext_rule p2413
5937 NItt_equal Itt_equal Itt_equal NIL
5938 NItt_equal!type type type Itt_equal
5939 O o2414 type
5940 T t2414 o2414 b1186
5941 S s2414 t637 h
5942 G s2414 t2414
5943 B b2414 s2414
5944 T t2415 o938 b2414 b2302
5945 B b2415 t2415
5946 T t2416 o559 b560 b1917
5947 B b2416 t2416
5948 T t2417 o559 b2291 b2416
5949 B b2417 t2417
5950 T t2418 o559 b561 b1917
5951 B b2418 t2418
5952 T t2419 o559 b2291 b2418
5953 B b2419 t2419
5954 T t2420 o738 b2417 b2419
5955 B b2420 t2420
5956 T t2421 o1177 b1347 b2420
5957 B b2421 t2421 s2
5958 T t2422 o1185 b1186 b2421
5959 B b2422 t2422 s1
5960 T t2423 o1185 b1186 b2422
5961 S s2423 t620 h
5962 G s2423 t2423
5963 B b2423 s2423
5964 T t2424 o938 b2423 b2302
5965 B b2424 t2424
5966 T t2425 o2 b2389
5967 B b2425 t2425
5968 T t2426 o973 b2424 b4 b2425
5969 B b2426 t2426
5970 T t2427 o2 b2426
5971 B b2427 t2427
5972 T t2428 o973 b2415 b4 b2427
5973 B b2428 t2428
5974 S s2428 t620 h h1344
5975 G s2428 t2422
5976 B b2429 s2428
5977 T t2429 o938 b2429 b2302
5978 B b2430 t2429
5979 T t2430 o937 b2430 b4 b2427
5980 B b2431 t2430
5981 T t2431 o b2431 b4
5982 B b2432 t2431
5983 T t2432 o b2428 b2432
5984 B b2433 t2432
5985 T t2433 o936 b2389 b2433
5986 B b2434 t2433
5987 T t2434 o936 b2428 b4
5988 B b2435 t2434
5989 T t2435 o990 b935 b2435 b4 b4
5990 B b2436 t2435
5991 P p2436 String "dT 0"
5992 O o2436 ext_rule p2436
5993 S s2436 t637 h h1344
5994 G s2436 t2414
5995 B b2437 s2436
5996 T t2437 o938 b2437 b2302
5997 B b2438 t2437
5998 T t2438 o2 b2431
5999 B b2439 t2438
6000 T t2439 o973 b2438 b4 b2439
6001 B b2440 t2439
6002 S s2440 t620 h h1344 h1224
6003 G s2440 t2421
6004 B b2441 s2440
6005 T t2441 o938 b2441 b2302
6006 B b2442 t2441
6007 T t2442 o937 b2442 b4 b2439
6008 B b2443 t2442
6009 T t2443 o b2443 b4
6010 B b2444 t2443
6011 T t2444 o b2440 b2444
6012 B b2445 t2444
6013 T t2445 o936 b2431 b2445
6014 B b2446 t2445
6015 T t2446 o936 b2440 b4
6016 B b2447 t2446
6017 T t2447 o990 b935 b2447 b4 b4
6018 B b2448 t2447
6019 T t2448 o2414 b1347
6020 S s2448 t637 h h1344 h1224
6021 G s2448 t2448
6022 B b2449 s2448
6023 T t2449 o938 b2449 b2302
6024 B b2450 t2449
6025 T t2450 o2 b2443
6026 B b2451 t2450
6027 T t2451 o973 b2450 b4 b2451
6028 B b2452 t2451
6029 S s2452 t620 h h1344 h1224 h1345
6030 G s2452 t2420
6031 B b2453 s2452
6032 T t2453 o938 b2453 b2302
6033 B b2454 t2453
6034 T t2454 o937 b2454 b4 b2451
6035 B b2455 t2454
6036 T t2455 o b2455 b4
6037 B b2456 t2455
6038 T t2456 o b2452 b2456
6039 B b2457 t2456
6040 T t2457 o936 b2443 b2457
6041 B b2458 t2457
6042 T t2458 o936 b2452 b4
6043 B b2459 t2458
6044 T t2459 o990 b935 b2459 b4 b4
6045 B b2460 t2459
6046 P p2460 String "rwh unfold_equal 0 thenT rwh unfold_equal 4 thenT autoT"
6047 O o2460 ext_rule p2460
6048 T t2460 o936 b2455 b4
6049 B b2461 t2460
6050 T t2461 o2460 b935 b2461 b4 b4
6051 B b2462 t2461
6052 T t2462 o b2462 b4
6053 B b2463 t2462
6054 T t2463 o b2460 b2463
6055 B b2464 t2463
6056 T t2464 o2436 b935 b2458 b2464 b4
6057 B b2465 t2464
6058 T t2465 o b2465 b4
6059 B b2466 t2465
6060 T t2466 o b2448 b2466
6061 B b2467 t2466
6062 T t2467 o2436 b935 b2446 b2467 b4
6063 B b2468 t2467
6064 T t2468 o b2468 b4
6065 B b2469 t2468
6066 T t2469 o b2436 b2469
6067 B b2470 t2469
6068 T t2470 o2413 b935 b2434 b2470 b4
6069 B b2471 t2470
6070 T t2471 o b2471 b4
6071 B b2472 t2471
6072 T t2472 o b2413 b2472
6073 B b2473 t2472
6074 T t2473 o b2395 b2473
6075 B b2474 t2473
6076 T t2474 o2369 b935 b2393 b2474 b4
6077 B b2475 t2474
6078 T t2475 o b2475 b4
6079 B b2476 t2475
6080 T t2476 o b2369 b2476
6081 B b2477 t2476
6082 T t2477 o2355 b935 b2367 b2477 b4
6083 B b2478 t2477
6084 T t2478 o936 b2348 b4
6085 B b2479 t2478
6086 T t2479 o990 b935 b2479 b4 b4
6087 B b2480 t2479
6088 T t825 o b2480 b4
6089 B b825 t825
6090 T t826 o b2478 b825
6091 B b826 t826
6092 T t827 o2339 b935 b822 b826 b4
6093 B b827 t827
6094 T t828 o b827 b4
6095 B b828 t828
6096 T t829 o b2339 b828
6097 B b829 t829
6098 T t830 o2316 b935 b813 b829 b4
6099 B b830 t830
6100 P p2515 String "groupCancelRightT << op{'a; 'b} >> thenT autoT"
6101 O o2515 ext_rule p2515
6102 T t2515 o936 b2313 b4
6103 B b2516 t2515