/[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 3404 - (show annotations) (download)
Sun Sep 23 07:25:28 2001 UTC (19 years, 10 months ago) by xiny
File size: 123630 byte(s)
1. Minor changes in czf_itt_group;
2. Define subgroup and abelian group;
3. Define cyclic subgroup and cyclic group. However, there are
   problems with the proofs in czf_itt_cyclic_subgroup.

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 713
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 715
1509 P p586 Number 762
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 765
1526 P p593 Number 866
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 868
1562 P p607 Number 946
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 p614 Number 961
1583 P p615 Number 1037
1584 O o615 location p614 p615
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 p623 Number 983
1618 P p624 Number 990
1619 O o624 resource_defs p623 p624 p264
1620 NOcaml!uid uid uid Ocaml
1621 P p625 Number 988
1622 O o625 uid p625 p624
1623 P p626 String []
1624 O o626 uid p626
1625 T t626 o626
1626 B b626 t626
1627 T t627 o625 b626
1628 B b627 t627
1629 T t628 o b627 b4
1630 B b628 t628
1631 T t629 o624 b628
1632 B b629 t629
1633 T t630 o b629 b4
1634 B b630 t630
1635 T t631 o616 b618 b622 b623 b630
1636 B b631 t631
1637 T t632 o615 b631
1638 B b632 t632
1639 P p632 Number 1039
1640 P p633 Number 1214
1641 O o633 location p632 p633
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 p645 Number 1061
1675 P p646 Number 1068
1676 O o646 resource_defs p645 p646 p264
1677 P p647 Number 1066
1678 O o647 uid p647 p646
1679 T t647 o647 b626
1680 B b647 t647
1681 T t648 o b647 b4
1682 B b648 t648
1683 T t649 o646 b648
1684 B b649 t649
1685 T t650 o b649 b4
1686 B b650 t650
1687 T t651 o634 b618 b645 b623 b650
1688 B b651 t651
1689 T t652 o633 b651
1690 B b652 t652
1691 P p652 Number 1216
1692 P p653 Number 1486
1693 O o653 location p652 p653
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 p664 Number 1238
1726 P p665 Number 1245
1727 O o665 resource_defs p664 p665 p264
1728 P p666 Number 1243
1729 O o666 uid p666 p665
1730 T t666 o666 b626
1731 B b666 t666
1732 T t667 o b666 b4
1733 B b667 t667
1734 T t668 o665 b667
1735 B b668 t668
1736 T t669 o b668 b4
1737 B b669 t669
1738 T t670 o654 b618 b664 b623 b669
1739 B b670 t670
1740 T t671 o653 b670
1741 B b671 t671
1742 P p671 Number 1488
1743 P p672 Number 1766
1744 O o672 location p671 p672
1745 P p673 String op_eq1
1746 O o673 rule p673
1747 P p674 Var s3
1748 O o674 var p674
1749 T t674 o674
1750 B b674 t674
1751 T t675 o620 b674
1752 S s675 t637 h
1753 G s675 t675
1754 B b675 s675
1755 T t676 o618 b675
1756 B b676 t676
1757 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1758 NCzf_itt_eq!eq eq eq Czf_itt_eq
1759 O o676 eq
1760 T t677 o676 b560 b561
1761 S s677 t620 h
1762 G s677 t677
1763 B b677 s677
1764 T t678 o618 b677
1765 B b678 t678
1766 T t679 o559 b674 b560
1767 B b679 t679
1768 T t680 o559 b674 b561
1769 B b680 t680
1770 T t681 o676 b679 b680
1771 S s681 t620 h
1772 G s681 t681
1773 B b681 s681
1774 T t682 o618 b681
1775 B b682 t682
1776 T t683 o635 b678 b682
1777 B b683 t683
1778 T t684 o635 b676 b683
1779 B b684 t684
1780 T t685 o635 b641 b684
1781 B b685 t685
1782 T t686 o635 b639 b685
1783 B b686 t686
1784 P p686 Number 1510
1785 P p687 Number 1517
1786 O o687 resource_defs p686 p687 p264
1787 P p688 Number 1515
1788 O o688 uid p688 p687
1789 T t688 o688 b626
1790 B b688 t688
1791 T t689 o b688 b4
1792 B b689 t689
1793 T t690 o687 b689
1794 B b690 t690
1795 T t691 o b690 b4
1796 B b691 t691
1797 T t692 o673 b618 b686 b623 b691
1798 B b692 t692
1799 T t693 o672 b692
1800 B b693 t693
1801 P p693 Number 1768
1802 P p694 Number 2046
1803 O o694 location p693 p694
1804 P p695 String op_eq2
1805 O o695 rule p695
1806 T t695 o559 b560 b674
1807 B b695 t695
1808 T t696 o559 b561 b674
1809 B b696 t696
1810 T t697 o676 b695 b696
1811 S s697 t620 h
1812 G s697 t697
1813 B b697 s697
1814 T t698 o618 b697
1815 B b698 t698
1816 T t699 o635 b678 b698
1817 B b699 t699
1818 T t700 o635 b676 b699
1819 B b700 t700
1820 T t701 o635 b641 b700
1821 B b701 t701
1822 T t702 o635 b639 b701
1823 B b702 t702
1824 P p702 Number 1790
1825 P p703 Number 1797
1826 O o703 resource_defs p702 p703 p264
1827 P p704 Number 1795
1828 O o704 uid p704 p703
1829 T t704 o704 b626
1830 B b704 t704
1831 T t705 o b704 b4
1832 B b705 t705
1833 T t706 o703 b705
1834 B b706 t706
1835 T t707 o b706 b4
1836 B b707 t707
1837 T t708 o695 b618 b702 b623 b707
1838 B b708 t708
1839 T t709 o694 b708
1840 B b709 t709
1841 P p709 Number 2048
1842 P p710 Number 2181
1843 O o710 location p709 p710
1844 P p711 String op_fun1
1845 O o711 rule p711
1846 T t711 o620 b573
1847 S s711 t637 h
1848 G s711 t711
1849 B b711 s711
1850 T t712 o618 b711
1851 B b712 t712
1852 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1853 O o712 fun_set
1854 P p712 Var z
1855 O o713 var p712
1856 T t713 o713
1857 B b713 t713
1858 T t714 o559 b713 b573
1859 B b714 t714 z
1860 T t715 o712 b714
1861 S s715 t620 h
1862 G s715 t715
1863 B b715 s715
1864 T t716 o618 b715
1865 B b716 t716
1866 T t717 o635 b712 b716
1867 B b717 t717
1868 P p717 Number 2071
1869 P p718 Number 2078
1870 O o718 resource_defs p717 p718 p264
1871 P p719 Number 2076
1872 O o719 uid p719 p718
1873 T t719 o719 b626
1874 B b719 t719
1875 T t720 o b719 b4
1876 B b720 t720
1877 T t721 o718 b720
1878 B b721 t721
1879 T t722 o b721 b4
1880 B b722 t722
1881 T t723 o711 b618 b717 b623 b722
1882 B b723 t723
1883 T t724 o710 b723
1884 B b724 t724
1885 P p724 Number 2183
1886 P p725 Number 2316
1887 O o725 location p724 p725
1888 P p726 String op_fun2
1889 O o726 rule p726
1890 T t726 o559 b573 b713
1891 B b726 t726 z
1892 T t727 o712 b726
1893 S s727 t620 h
1894 G s727 t727
1895 B b727 s727
1896 T t728 o618 b727
1897 B b728 t728
1898 T t729 o635 b712 b728
1899 B b729 t729
1900 P p729 Number 2206
1901 P p730 Number 2213
1902 O o730 resource_defs p729 p730 p264
1903 P p731 Number 2211
1904 O o731 uid p731 p730
1905 T t731 o731 b626
1906 B b731 t731
1907 T t732 o b731 b4
1908 B b732 t732
1909 T t733 o730 b732
1910 B b733 t733
1911 T t734 o b733 b4
1912 B b734 t734
1913 T t735 o726 b618 b729 b623 b734
1914 B b735 t735
1915 T t736 o725 b735
1916 B b736 t736
1917 P p736 Number 2506
1918 P p737 Number 2899
1919 O o737 location p736 p737
1920 P p738 String op_assoc1
1921 O o738 rule p738
1922 T t738 o655 b674 b554
1923 S s738 t620 h
1924 G s738 t738
1925 B b738 s738
1926 T t739 o618 b738
1927 B b739 t739
1928 NCzf_itt_eq!equal equal equal Czf_itt_eq
1929 O o739 equal
1930 T t740 o559 b562 b674
1931 B b740 t740
1932 T t741 o559 b560 b696
1933 B b741 t741
1934 T t742 o739 b740 b741
1935 S s742 t620 h
1936 G s742 t742
1937 B b742 s742
1938 T t743 o618 b742
1939 B b743 t743
1940 T t744 o635 b739 b743
1941 B b744 t744
1942 T t745 o635 b658 b744
1943 B b745 t745
1944 T t746 o635 b656 b745
1945 B b746 t746
1946 T t747 o635 b676 b746
1947 B b747 t747
1948 T t748 o635 b641 b747
1949 B b748 t748
1950 T t749 o635 b639 b748
1951 B b749 t749
1952 P p749 Number 2531
1953 P p750 Number 2538
1954 O o750 resource_defs p749 p750 p264
1955 P p751 Number 2536
1956 O o751 uid p751 p750
1957 T t751 o751 b626
1958 B b751 t751
1959 T t752 o b751 b4
1960 B b752 t752
1961 T t753 o750 b752
1962 B b753 t753
1963 T t754 o b753 b4
1964 B b754 t754
1965 T t755 o738 b618 b749 b623 b754
1966 B b755 t755
1967 T t756 o737 b755
1968 B b756 t756
1969 P p756 Number 2972
1970 P p757 Number 3365
1971 O o757 location p756 p757
1972 P p758 String op_assoc2
1973 O o758 rule p758
1974 T t758 o739 b741 b740
1975 S s758 t620 h
1976 G s758 t758
1977 B b758 s758
1978 T t759 o618 b758
1979 B b759 t759
1980 T t760 o635 b739 b759
1981 B b760 t760
1982 T t761 o635 b658 b760
1983 B b761 t761
1984 T t762 o635 b656 b761
1985 B b762 t762
1986 T t763 o635 b676 b762
1987 B b763 t763
1988 T t764 o635 b641 b763
1989 B b764 t764
1990 T t765 o635 b639 b764
1991 B b765 t765
1992 P p765 Number 2997
1993 P p766 Number 3004
1994 O o766 resource_defs p765 p766 p264
1995 P p767 Number 3002
1996 O o767 uid p767 p766
1997 T t767 o767 b626
1998 B b767 t767
1999 T t768 o b767 b4
2000 B b768 t768
2001 T t769 o766 b768
2002 B b769 t769
2003 T t770 o b769 b4
2004 B b770 t770
2005 T t771 o758 b618 b765 b623 b770
2006 B b771 t771
2007 T t772 o757 b771
2008 B b772 t772
2009 P p772 Number 3438
2010 P p773 Number 3514
2011 O o773 location p772 p773
2012 P p774 String id_wf1
2013 O o774 rule p774
2014 T t774 o620 b567
2015 S s774 t620 h
2016 G s774 t774
2017 B b774 s774
2018 T t775 o618 b774
2019 B b775 t775
2020 P p775 Number 3460
2021 P p776 Number 3468
2022 O o776 resource_defs p775 p776 p264
2023 P p777 Number 3466
2024 O o777 uid p777 p776
2025 T t777 o777 b626
2026 B b777 t777
2027 T t778 o b777 b4
2028 B b778 t778
2029 T t779 o776 b778
2030 B b779 t779
2031 T t780 o b779 b4
2032 B b780 t780
2033 T t781 o774 b618 b775 b623 b780
2034 B b781 t781
2035 T t782 o773 b781
2036 B b782 t782
2037 P p782 Number 3517
2038 P p783 Number 3595
2039 O o783 location p782 p783
2040 P p784 String id_wf2
2041 O o784 rule p784
2042 T t784 o655 b567 b554
2043 S s784 t620 h
2044 G s784 t784
2045 B b784 s784
2046 T t785 o618 b784
2047 B b785 t785
2048 P p785 Number 3539
2049 P p786 Number 3546
2050 O o786 resource_defs p785 p786 p264
2051 P p787 Number 3544
2052 O o787 uid p787 p786
2053 T t787 o787 b626
2054 B b787 t787
2055 T t788 o b787 b4
2056 B b788 t788
2057 T t789 o786 b788
2058 B b789 t789
2059 T t790 o b789 b4
2060 B b790 t790
2061 T t791 o784 b618 b785 b623 b790
2062 B b791 t791
2063 T t792 o783 b791
2064 B b792 t792
2065 P p792 Number 3684
2066 P p793 Number 3860
2067 O o793 location p792 p793
2068 P p794 String id_eq1
2069 O o794 rule p794
2070 T t794 o655 b573 b554
2071 S s794 t620 h
2072 G s794 t794
2073 B b794 s794
2074 T t795 o618 b794
2075 B b795 t795
2076 T t796 o559 b567 b573
2077 B b796 t796
2078 T t797 o739 b796 b573
2079 S s797 t620 h
2080 G s797 t797
2081 B b797 s797
2082 T t798 o618 b797
2083 B b798 t798
2084 T t799 o635 b795 b798
2085 B b799 t799
2086 T t800 o635 b712 b799
2087 B b800 t800
2088 P p800 Number 3706
2089 P p801 Number 3713
2090 O o801 resource_defs p800 p801 p264
2091 P p802 Number 3711
2092 O o802 uid p802 p801
2093 T t802 o802 b626
2094 B b802 t802
2095 T t803 o b802 b4
2096 B b803 t803
2097 T t804 o801 b803
2098 B b804 t804
2099 T t805 o b804 b4
2100 B b805 t805
2101 T t806 o794 b618 b800 b623 b805
2102 B b806 t806
2103 T t807 o793 b806
2104 B b807 t807
2105 P p807 Number 3862
2106 P p808 Number 4038
2107 O o808 location p807 p808
2108 P p809 String id_eq2
2109 O o809 rule p809
2110 T t809 o559 b573 b567
2111 B b809 t809
2112 T t810 o739 b809 b573
2113 S s810 t620 h
2114 G s810 t810
2115 B b810 s810
2116 T t811 o618 b810
2117 B b811 t811
2118 T t812 o635 b795 b811
2119 B b812 t812
2120 T t813 o635 b712 b812
2121 B b813 t813
2122 P p813 Number 3884
2123 P p814 Number 3891
2124 O o814 resource_defs p813 p814 p264
2125 P p815 Number 3889
2126 O o815 uid p815 p814
2127 T t815 o815 b626
2128 B b815 t815
2129 T t816 o b815 b4
2130 B b816 t816
2131 T t817 o814 b816
2132 B b817 t817
2133 T t818 o b817 b4
2134 B b818 t818
2135 T t819 o809 b618 b813 b623 b818
2136 B b819 t819
2137 T t820 o808 b819
2138 B b820 t820
2139 P p820 Number 4040
2140 P p821 Number 4097
2141 O o821 location p820 p821
2142 NOcaml!str_let str_let str_let Ocaml
2143 O o822 str_let p820 p821
2144 NOcaml!patt_var patt_var patt_var Ocaml
2145 P p822 Number 4044
2146 O o823 patt_var p822 p821
2147 NOcaml!patt_done patt_done patt_done Ocaml
2148 O o824 patt_done p820 p821
2149 T t824 o824
2150 B b824 t824 id_elim2T
2151 T t825 o823 b824
2152 B b825 t825
2153 NOcaml!fun fun fun Ocaml
2154 O o825 fun p822 p821
2155 NOcaml!patt_if patt_if patt_if Ocaml
2156 O o826 patt_if p822 p821
2157 P p826 Number 4054
2158 P p827 Number 4055
2159 O o827 patt_var p826 p827
2160 NOcaml!patt_body patt_body patt_body Ocaml
2161 O o828 patt_body p822 p821
2162 NOcaml!apply apply apply Ocaml
2163 P p828 Number 4061
2164 O o829 apply p828 p821
2165 P p829 Number 4095
2166 O o830 apply p828 p829
2167 NOcaml!lid lid lid Ocaml
2168 P p830 Number 4067
2169 O o831 lid p828 p830
2170 O o832 lid p794
2171 T t832 o832
2172 B b832 t832
2173 T t833 o831 b832
2174 B b833 t833
2175 P p833 Number 4069
2176 P p834 Number 4094
2177 O o834 apply p833 p834
2178 NOcaml!proj proj proj Ocaml
2179 P p835 Number 4092
2180 O o835 proj p833 p835
2181 O o836 uid p833 p835
2182 O o837 uid p509
2183 T t837 o837
2184 B b837 t837
2185 T t838 o836 b837
2186 B b838 t838
2187 P p838 Number 4078
2188 O o838 lid p838 p835
2189 P p839 String hyp_count_addr
2190 O o839 lid p839
2191 T t839 o839
2192 B b839 t839
2193 T t840 o838 b839
2194 B b840 t840
2195 T t841 o835 b838 b840
2196 B b841 t841
2197 P p841 Number 4093
2198 O o841 lid p841 p834
2199 P p842 Var p
2200 O o842 var p842
2201 T t842 o842
2202 B b842 t842
2203 T t843 o841 b842
2204 B b843 t843
2205 T t844 o834 b841 b843
2206 B b844 t844
2207 T t845 o830 b833 b844
2208 B b845 t845
2209 P p845 Number 4096
2210 O o845 lid p845 p821
2211 T t846 o845 b842
2212 B b846 t846
2213 T t847 o829 b845 b846
2214 B b847 t847
2215 T t848 o828 b847
2216 B b848 t848 p
2217 T t849 o827 b848
2218 B b849 t849
2219 T t850 o826 b849
2220 B b850 t850
2221 T t851 o825 b850
2222 B b851 t851
2223 T t852 o822 b825 b851
2224 B b852 t852
2225 T t853 o b852 b4
2226 B b853 t853
2227 T t854 o822 b853
2228 B b854 t854
2229 T t855 o392 b854
2230 B b855 t855
2231 T t856 o821 b855
2232 B b856 t856
2233 P p856 Number 4099
2234 P p857 Number 4272
2235 O o857 location p856 p857
2236 P p858 String inv_wf1
2237 O o858 rule p858
2238 T t858 o572 b560
2239 B b858 t858
2240 T t859 o620 b858
2241 S s859 t620 h
2242 G s859 t859
2243 B b859 s859
2244 T t860 o618 b859
2245 B b860 t860
2246 T t861 o635 b656 b860
2247 B b861 t861
2248 T t862 o635 b639 b861
2249 B b862 t862
2250 P p862 Number 4122
2251 P p863 Number 4129
2252 O o863 resource_defs p862 p863 p264
2253 P p864 Number 4127
2254 O o864 uid p864 p863
2255 T t864 o864 b626
2256 B b864 t864
2257 T t865 o b864 b4
2258 B b865 t865
2259 T t866 o863 b865
2260 B b866 t866
2261 T t867 o b866 b4
2262 B b867 t867
2263 T t868 o858 b618 b862 b623 b867
2264 B b868 t868
2265 T t869 o857 b868
2266 B b869 t869
2267 P p869 Number 4274
2268 P p870 Number 4450
2269 O o870 location p869 p870
2270 P p871 String inv_wf2
2271 O o871 rule p871
2272 T t871 o655 b858 b554
2273 S s871 t620 h
2274 G s871 t871
2275 B b871 s871
2276 T t872 o618 b871
2277 B b872 t872
2278 T t873 o635 b656 b872
2279 B b873 t873
2280 T t874 o635 b639 b873
2281 B b874 t874
2282 P p874 Number 4297
2283 P p875 Number 4304
2284 O o875 resource_defs p874 p875 p264
2285 P p876 Number 4302
2286 O o876 uid p876 p875
2287 T t876 o876 b626
2288 B b876 t876
2289 T t877 o b876 b4
2290 B b877 t877
2291 T t878 o875 b877
2292 B b878 t878
2293 T t879 o b878 b4
2294 B b879 t879
2295 T t880 o871 b618 b874 b623 b879
2296 B b880 t880
2297 T t881 o870 b880
2298 B b881 t881
2299 P p881 Number 4452
2300 P p882 Number 4539
2301 O o882 location p881 p882
2302 P p883 String inv_fun1
2303 O o883 rule p883
2304 T t883 o572 b713
2305 B b883 t883 z
2306 T t884 o712 b883
2307 S s884 t620 h
2308 G s884 t884
2309 B b884 s884
2310 T t885 o618 b884
2311 B b885 t885
2312 P p885 Number 4476
2313 P p886 Number 4483
2314 O o886 resource_defs p885 p886 p264
2315 P p887 Number 4481
2316 O o887 uid p887 p886
2317 T t887 o887 b626
2318 B b887 t887
2319 T t888 o b887 b4
2320 B b888 t888
2321 T t889 o886 b888
2322 B b889 t889
2323 T t890 o b889 b4
2324 B b890 t890
2325 T t891 o883 b618 b885 b623 b890
2326 B b891 t891
2327 T t892 o882 b891
2328 B b892 t892
2329 P p892 Number 4541
2330 P p893 Number 4727
2331 O o893 location p892 p893
2332 P p894 String inv_id1
2333 O o894 rule p894
2334 T t894 o559 b858 b560
2335 B b894 t894
2336 T t895 o739 b894 b567
2337 S s895 t620 h
2338 G s895 t895
2339 B b895 s895
2340 T t896 o618 b895
2341 B b896 t896
2342 T t897 o635 b656 b896
2343 B b897 t897
2344 T t898 o635 b639 b897
2345 B b898 t898
2346 P p898 Number 4564
2347 P p899 Number 4571
2348 O o899 resource_defs p898 p899 p264
2349 P p900 Number 4569
2350 O o900 uid p900 p899
2351 T t900 o900 b626
2352 B b900 t900
2353 T t901 o b900 b4
2354 B b901 t901
2355 T t902 o899 b901
2356 B b902 t902
2357 T t903 o b902 b4
2358 B b903 t903
2359 T t904 o894 b618 b898 b623 b903
2360 B b904 t904
2361 T t905 o893 b904
2362 B b905 t905
2363 P p905 Number 4729
2364 P p906 Number 4915
2365 O o906 location p905 p906
2366 P p907 String inv_id2
2367 O o907 rule p907
2368 T t907 o559 b560 b858
2369 B b907 t907
2370 T t908 o739 b907 b567
2371 S s908 t620 h
2372 G s908 t908
2373 B b908 s908
2374 T t909 o618 b908
2375 B b909 t909
2376 T t910 o635 b656 b909
2377 B b910 t910
2378 T t911 o635 b639 b910
2379 B b911 t911
2380 P p911 Number 4752
2381 P p912 Number 4759
2382 O o912 resource_defs p911 p912 p264
2383 P p913 Number 4757
2384 O o913 uid p913 p912
2385 T t913 o913 b626
2386 B b913 t913
2387 T t914 o b913 b4
2388 B b914 t914
2389 T t915 o912 b914
2390 B b915 t915
2391 T t916 o b915 b4
2392 B b916 t916
2393 T t917 o907 b618 b911 b623 b916
2394 B b917 t917
2395 T t918 o906 b917
2396 B b918 t918
2397 P p918 Number 5376
2398 P p919 Number 5802
2399 O o919 location p918 p919
2400 P p920 String cancel1
2401 O o920 rule p920
2402 NSummary!term_param term_param term_param Summary
2403 O o921 term_param
2404 T t921 o921 b560
2405 B b921 t921
2406 T t922 o b921 b4
2407 B b922 t922
2408 T t923 o b617 b922
2409 B b923 t923
2410 T t924 o739 b562 b695
2411 S s924 t620 h
2412 G s924 t924
2413 B b924 s924
2414 T t925 o618 b924
2415 B b925 t925
2416 T t926 o739 b561 b674
2417 S s926 t620 h
2418 G s926 t926
2419 B b926 s926
2420 T t927 o618 b926
2421 B b927 t927
2422 T t928 o635 b925 b927
2423 B b928 t928
2424 T t929 o635 b739 b928
2425 B b929 t929
2426 T t930 o635 b658 b929
2427 B b930 t930
2428 T t931 o635 b656 b930
2429 B b931 t931
2430 T t932 o635 b676 b931
2431 B b932 t932
2432 T t933 o635 b641 b932
2433 B b933 t933
2434 T t934 o635 b639 b933
2435 B b934 t934
2436 NSummary!interactive interactive interactive Summary
2437 O o934 interactive
2438 NSummary!ext_rule ext_rule ext_rule Summary
2439 P p934 String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2440 O o935 ext_rule p934
2441 NSummary!status_incomplete status_incomplete status_incomplete Summary
2442 O o936 status_incomplete
2443 T t936 o936
2444 B b936 t936
2445 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2446 O o937 ext_unjustified
2447 NSummary!tactic_arg tactic_arg tactic_arg Summary
2448 P p937 String main
2449 O o938 tactic_arg p937
2450 NSummary!msequent msequent msequent Summary
2451 O o939 msequent
2452 T t939 o b924 b4
2453 B b939 t939
2454 T t940 o b738 b939
2455 B b940 t940
2456 T t941 o b657 b940
2457 B b941 t941
2458 T t942 o b655 b941
2459 B b942 t942
2460 T t943 o b675 b942
2461 B b943 t943
2462 T t944 o b640 b943
2463 B b944 t944
2464 T t945 o b638 b944
2465 B b945 t945
2466 T t946 o939 b926 b945
2467 B b946 t946
2468 NSummary!parent_none parent_none parent_none Summary
2469 O o946 parent_none
2470 T t947 o946
2471 B b947 t947
2472 T t948 o938 b946 b4 b947
2473 B b948 t948
2474 P p948 String assertion
2475 O o948 tactic_arg p948
2476 H h948 v t924
2477 T t949 o559 b858 b562
2478 B b949 t949
2479 T t950 o559 b858 b695
2480 B b950 t950
2481 T t951 o739 b949 b950
2482 S s951 t620 h h948
2483 G s951 t951
2484 B b951 s951
2485 T t952 o939 b951 b945
2486 B b952 t952
2487 S s952 t620 h h948
2488 G s952 t926
2489 B b953 s952
2490 T t953 o939 b953 b945
2491 B b954 t953
2492 T t954 o2 b948
2493 B b955 t954
2494 T t955 o938 b954 b4 b955
2495 B b956 t955
2496 T t956 o2 b956
2497 B b957 t956
2498 T t957 o948 b952 b4 b957
2499 B b958 t957
2500 H h958 v_1 t951
2501 S s958 t620 h h948 h958
2502 G s958 t926
2503 B b959 s958
2504 T t959 o939 b959 b945
2505 B b960 t959
2506 T t960 o938 b960 b4 b957
2507 B b961 t960
2508 T t961 o b961 b4
2509 B b962 t961
2510 T t962 o b958 b962
2511 B b963 t962
2512 T t963 o937 b948 b963
2513 B b964 t963
2514 P p964 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2515 O o964 ext_rule p964
2516 T t964 o937 b958 b4
2517 B b965 t964
2518 T t965 o964 b936 b965 b4 b4
2519 B b966 t965
2520 P p966 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2521 O o966 ext_rule p966
2522 P p967 String eq
2523 O o967 tactic_arg p967
2524 T t967 o559 b894 b561
2525 B b967 t967
2526 T t968 o739 b949 b967
2527 S s968 t620 h h948 h958
2528 G s968 t968
2529 B b968 s968
2530 T t969 o939 b968 b945
2531 B b969 t969
2532 T t970 o2 b961
2533 B b970 t970
2534 T t971 o967 b969 b4 b970
2535 B b971 t971
2536 T t972 o739 b967 b950
2537 H h972 v_2 t972
2538 S s972 t620 h h948 h958 h972
2539 G s972 t926
2540 B b972 s972
2541 T t973 o939 b972 b945
2542 B b973 t973
2543 T t974 o938 b973 b4 b970
2544 B b974 t974
2545 P p974 String wf
2546 O o974 tactic_arg p974
2547 B b975 t950 v_2
2548 T t975 o712 b975
2549 S s975 t620 h h948 h958
2550 G s975 t975
2551 B b976 s975
2552 T t976 o939 b976 b945
2553 B b977 t976
2554 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2555 O o977 fun_prop
2556 P p977 Var v_2
2557 O o978 var p977
2558 T t978 o978
2559 B b978 t978
2560 T t979 o739 b978 b950
2561 B b979 t979 v_2
2562 T t980 o977 b979
2563 S s980 t620 h h948 h958
2564 G s980 t980
2565 B b980 s980
2566 T t981 o939 b980 b945
2567 B b981 t981
2568 NSummary!arg_named arg_named arg_named Summary
2569 P p981 String d_auto
2570 O o981 arg_named p981
2571 NSummary!arg_bool arg_bool arg_bool Summary
2572 P p982 String true
2573 O o982 arg_bool p982
2574 T t982 o982
2575 B b982 t982
2576 T t983 o981 b982
2577 B b983 t983
2578 T t984 o b983 b4
2579 B b984 t984
2580 T t985 o974 b981 b984 b970
2581 B b985 t985
2582 T t986 o2 b985
2583 B b986 t986
2584 T t987 o974 b977 b4 b986
2585 B b987 t987
2586 T t988 o b987 b4
2587 B b988 t988
2588 T t989 o b974 b988
2589 B b989 t989
2590 T t990 o b971 b989
2591 B b990 t990
2592 T t991 o937 b961 b990
2593 B b991 t991
2594 P p991 String autoT
2595 O o991 ext_rule p991
2596 T t992 o937 b971 b4
2597 B b992 t992
2598 T t993 o991 b936 b992 b4 b4
2599 B b993 t993
2600 P p993 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2601 O o993 ext_rule p993
2602 T t994 o559 b894 b674
2603 B b994 t994
2604 T t995 o739 b950 b994
2605 S s995 t620 h h948 h958 h972
2606 G s995 t995
2607 B b995 s995
2608 T t996 o939 b995 b945
2609 B b996 t996
2610 T t997 o2 b974
2611 B b997 t997
2612 T t998 o967 b996 b4 b997
2613 B b998 t998
2614 T t999 o739 b967 b994
2615 H h999 v_3 t999
2616 S s999 t620 h h948 h958 h972 h999
2617 G s999 t926
2618 B b999 s999
2619 T t1000 o939 b999 b945
2620 B b1000 t1000
2621 T t1001 o938 b1000 b4 b997
2622 B b1001 t1001
2623 B b1002 t967 v_3
2624 T t1002 o712 b1002
2625 S s1002 t620 h h948 h958 h972
2626 G s1002 t1002
2627 B b1003 s1002
2628 T t1003 o939 b1003 b945
2629 B b1004 t1003
2630 P p1004 Var v_3
2631 O o1004 var p1004
2632 T t1004 o1004
2633 B b1005 t1004
2634 T t1005 o739 b967 b1005
2635 B b1006 t1005 v_3
2636 T t1006 o977 b1006
2637 S s1006 t620 h h948 h958 h972
2638 G s1006 t1006
2639 B b1007 s1006
2640 T t1007 o939 b1007 b945
2641 B b1008 t1007
2642 T t1008 o974 b1008 b984 b997
2643 B b1009 t1008
2644 T t1009 o2 b1009
2645 B b1010 t1009
2646 T t1010 o974 b1004 b4 b1010
2647 B b1011 t1010
2648 T t1011 o b1011 b4
2649 B b1012 t1011
2650 T t1012 o b1001 b1012
2651 B b1013 t1012
2652 T t1013 o b998 b1013
2653 B b1014 t1013
2654 T t1014 o937 b974 b1014
2655 B b1015 t1014
2656 T t1015 o937 b998 b4
2657 B b1016 t1015
2658 T t1016 o991 b936 b1016 b4 b4
2659 B b1017 t1016
2660 P p1017 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2661 O o1017 ext_rule p1017
2662 T t1017 o559 b567 b561
2663 B b1018 t1017
2664 T t1018 o559 b567 b674
2665 B b1019 t1018
2666 T t1019 o739 b1018 b1019
2667 H h1019 v_4 t1019
2668 S s1019 t620 h h948 h958 h972 h999 h1019
2669 G s1019 t926
2670 B b1020 s1019
2671 T t1020 o939 b1020 b945
2672 B b1021 t1020
2673 T t1021 o2 b1001
2674 B b1022 t1021
2675 T t1022 o938 b1021 b4 b1022
2676 B b1023 t1022
2677 T t1023 o b1023 b4
2678 B b1024 t1023
2679 T t1024 o937 b1001 b1024
2680 B b1025 t1024
2681 P p1025 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2682 O o1025 ext_rule p1025
2683 T t1025 o739 b561 b1019
2684 H h1025 v_5 t1025
2685 S s1025 t620 h h948 h958 h972 h999 h1019 h1025
2686 G s1025 t926
2687 B b1026 s1025
2688 T t1026 o939 b1026 b945
2689 B b1027 t1026
2690 T t1027 o2 b1023
2691 B b1028 t1027
2692 T t1028 o938 b1027 b4 b1028
2693 B b1029 t1028
2694 B b1030 t1018 v_5
2695 T t1030 o712 b1030
2696 S s1030 t620 h h948 h958 h972 h999 h1019
2697 G s1030 t1030
2698 B b1031 s1030
2699 T t1031 o939 b1031 b945
2700 B b1032 t1031
2701 P p1032 Var v_5
2702 O o1032 var p1032
2703 T t1032 o1032
2704 B b1033 t1032
2705 T t1033 o739 b1033 b1019
2706 B b1034 t1033 v_5
2707 T t1034 o977 b1034
2708 S s1034 t620 h h948 h958 h972 h999 h1019
2709 G s1034 t1034
2710 B b1035 s1034
2711 T t1035 o939 b1035 b945
2712 B b1036 t1035
2713 T t1036 o974 b1036 b984 b1028
2714 B b1037 t1036
2715 T t1037 o2 b1037
2716 B b1038 t1037
2717 T t1038 o974 b1032 b4 b1038
2718 B b1039 t1038
2719 T t1039 o b1039 b4
2720 B b1040 t1039
2721 T t1040 o b1029 b1040
2722 B b1041 t1040
2723 T t1041 o937 b1023 b1041
2724 B b1042 t1041
2725 P p1042 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2726 O o1042 ext_rule p1042
2727 H h1042 v_6 t926
2728 S s1042 t620 h h948 h958 h972 h999 h1019 h1025 h1042
2729 G s1042 t926
2730 B b1043 s1042
2731 T t1043 o939 b1043 b945
2732 B b1044 t1043
2733 T t1044 o2 b1029
2734 B b1045 t1044
2735 T t1045 o938 b1044 b4 b1045
2736 B b1046 t1045
2737 T t1046 o b1046 b4
2738 B b1047 t1046
2739 T t1047 o937 b1029 b1047
2740 B b1048 t1047
2741 P p1048 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2742 O o1048 ext_rule p1048
2743 T t1048 o937 b1046 b4
2744 B b1049 t1048
2745 T t1049 o1048 b936 b1049 b4 b4
2746 B b1050 t1049
2747 T t1050 o b1050 b4
2748 B b1051 t1050
2749 P p1051 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2750 O o1051 ext_rule p1051
2751 B b1052 t1017 v_6
2752 T t1052 o712 b1052
2753 S s1052 t620 h h948 h958 h972 h999 h1019 h1025
2754 G s1052 t1052
2755 B b1053 s1052
2756 T t1053 o939 b1053 b945
2757 B b1054 t1053
2758 P p1054 Var v_6
2759 O o1054 var p1054
2760 T t1054 o1054
2761 B b1055 t1054
2762 T t1055 o739 b1018 b1055
2763 B b1056 t1055 v_6
2764 T t1056 o977 b1056
2765 S s1056 t620 h h948 h958 h972 h999 h1019 h1025
2766 G s1056 t1056
2767 B b1057 s1056
2768 T t1057 o939 b1057 b945
2769 B b1058 t1057
2770 T t1058 o974 b1058 b984 b1045
2771 B b1059 t1058
2772 T t1059 o2 b1059
2773 B b1060 t1059
2774 T t1060 o974 b1054 b4 b1060
2775 B b1061 t1060
2776 T t1061 o937 b1061 b4
2777 B b1062 t1061
2778 T t1062 o1051 b936 b1062 b4 b4
2779 B b1063 t1062
2780 T t1063 o b1063 b4
2781 B b1064 t1063
2782 T t1064 o1042 b936 b1048 b1051 b1064
2783 B b1065 t1064
2784 T t1065 o937 b1039 b4
2785 B b1066 t1065
2786 T t1066 o1051 b936 b1066 b4 b4
2787 B b1067 t1066
2788 T t1067 o b1067 b4
2789 B b1068 t1067
2790 T t1068 o b1065 b1068
2791 B b1069 t1068
2792 T t1069 o1025 b936 b1042 b1069 b4
2793 B b1070 t1069
2794 T t1070 o b1070 b4
2795 B b1071 t1070
2796 T t1071 o1017 b936 b1025 b1071 b4
2797 B b1072 t1071
2798 P p1072 String "rwh unfold_fun_set 0 thenT autoT"
2799 O o1072 ext_rule p1072
2800 T t1072 o937 b1011 b4
2801 B b1073 t1072
2802 T t1073 o1072 b936 b1073 b4 b4
2803 B b1074 t1073
2804 T t1074 o b1074 b4
2805 B b1075 t1074
2806 T t1075 o b1072 b1075
2807 B b1076 t1075
2808 T t1076 o b1017 b1076
2809 B b1077 t1076
2810 T t1077 o993 b936 b1015 b1077 b4
2811 B b1078 t1077
2812 T t1078 o937 b987 b4
2813 B b1079 t1078
2814 T t1079 o1072 b936 b1079 b4 b4
2815 B b1080 t1079
2816 T t1080 o b1080 b4
2817 B b1081 t1080
2818 T t1081 o b1078 b1081
2819 B b1082 t1081
2820 T t1082 o b993 b1082
2821 B b1083 t1082
2822 T t1083 o966 b936 b991 b1083 b4
2823 B b1084 t1083
2824 T t1084 o b1084 b4
2825 B b1085 t1084
2826 T t1085 o b966 b1085
2827 B b1086 t1085
2828 NSummary!ext_goal ext_goal ext_goal Summary
2829 O o1086 ext_goal
2830 S s1086 t620 h
2831 G s1086 t951
2832 B b1087 s1086
2833 T t1087 o939 b1087 b945
2834 B b1088 t1087
2835 T t1088 o948 b1088 b4 b955
2836 B b1089 t1088
2837 T t1089 o1086 b1089
2838 B b1090 t1089
2839 T t1090 o b1090 b4
2840 B b1091 t1090
2841 T t1091 o964 b936 b1090 b1091 b4
2842 B b1092 t1091
2843 P p1092 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2844 O o1092 ext_rule p1092
2845 H h1092 v t951
2846 S s1092 t620 h h1092
2847 G s1092 t926
2848 B b1093 s1092
2849 T t1093 o939 b1093 b945
2850 B b1094 t1093
2851 T t1094 o938 b1094 b4 b955
2852 B b1095 t1094
2853 T t1095 o1086 b1095
2854 B b1096 t1095
2855 P p1096 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2856 O o1096 ext_rule p1096
2857 P p1097 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2858 O o1097 ext_rule p1097
2859 T t1097 o b1096 b4
2860 B b1097 t1097
2861 H h1097 x t924
2862 H h1098 v_1 t972
2863 H h1099 v_2 t999
2864 H h1100 v_3 t1019
2865 H h1101 v_4 t1025
2866 B b1101 t1017 v_5
2867 T t1101 o712 b1101
2868 S s1101 t620 h h1097 h1092 h1098 h1099 h1100 h1101
2869 G s1101 t1101
2870 B b1102 s1101
2871 T t1102 o b738 b4
2872 B b1103 t1102
2873 T t1103 o b657 b1103
2874 B b1104 t1103
2875 T t1104 o b655 b1104
2876 B b1105 t1104
2877 T t1105 o b675 b1105
2878 B b1106 t1105
2879 T t1106 o b640 b1106
2880 B b1107 t1106
2881 T t1107 o b638 b1107
2882 B b1108 t1107
2883 T t1108 o939 b1102 b1108
2884 B b1109 t1108
2885 T t1109 o739 b1018 b1033
2886 B b1110 t1109 v_5
2887 T t1110 o977 b1110
2888 S s1110 t620 h h1097 h1092 h1098 h1099 h1100 h1101
2889 G s1110 t1110
2890 B b1111 s1110
2891 T t1111 o939 b1111 b1108
2892 B b1112 t1111
2893 S s1112 t620 h h1097 h1092 h1098 h1099 h1100 h1101
2894 G s1112 t926
2895 B b1113 s1112
2896 T t1113 o939 b1113 b1108
2897 B b1114 t1113
2898 S s1114 t620 h h1097 h1092 h1098 h1099 h1100
2899 G s1114 t926
2900 B b1115 s1114
2901 T t1115 o939 b1115 b1108
2902 B b1116 t1115
2903 S s1116 t620 h h1097 h1092 h1098 h1099
2904 G s1116 t926
2905 B b1117 s1116
2906 T t1117 o939 b1117 b1108
2907 B b1118 t1117
2908 S s1118 t620 h h1097 h1092 h1098
2909 G s1118 t926
2910 B b1119 s1118
2911 T t1119 o939 b1119 b1108
2912 B b1120 t1119
2913 S s1120 t620 h h1097 h1092
2914 G s1120 t926
2915 B b1121 s1120
2916 T t1121 o939 b1121 b1108
2917 B b1122 t1121
2918 S s1122 t620 h h1097
2919 G s1122 t926
2920 B b1123 s1122
2921 T t1123 o939 b1123 b1108
2922 B b1124 t1123
2923 T t1124 o938 b1124 b4 b947
2924 B b1125 t1124
2925 T t1125 o2 b1125
2926 B b1126 t1125
2927 T t1126 o938 b1122 b4 b1126
2928 B b1127 t1126
2929 T t1127 o2 b1127
2930 B b1128 t1127
2931 T t1128 o938 b1120 b4 b1128
2932 B b1129 t1128
2933 T t1129 o2 b1129
2934 B b1130 t1129
2935 T t1130 o938 b1118 b4 b1130
2936 B b1131 t1130
2937 T t1131 o2 b1131
2938 B b1132 t1131
2939 T t1132 o938 b1116 b4 b1132
2940 B b1133 t1132
2941 T t1133 o2 b1133
2942 B b1134 t1133
2943 T t1134 o938 b1114 b4 b1134
2944 B b1135 t1134
2945 T t1135 o2 b1135
2946 B b1136 t1135
2947 T t1136 o974 b1112 b984 b1136
2948 B b1137 t1136
2949 T t1137 o2 b1137
2950 B b1138 t1137
2951 T t1138 o974 b1109 b4 b1138
2952 B b1139 t1138
2953 T t1139 o937 b1139 b4
2954 B b1140 t1139
2955 T t1140 o1051 b936 b1140 b4 b4
2956 B b1141 t1140
2957 T t1141 o b1141 b4
2958 B b1142 t1141
2959 T t1142 o1097 b936 b1096 b1097 b1142
2960 B b1143 t1142
2961 T t1143 o b1143 b4
2962 B b1144 t1143
2963 B b1145 t1018 v_4
2964 T t1145 o712 b1145
2965 S s1145 t620 h h1097 h1092 h1098 h1099 h1100
2966 G s1145 t1145
2967 B b1146 s1145
2968 T t1146 o939 b1146 b1108
2969 B b1147 t1146
2970 P p1147 Var v_4
2971 O o1147 var p1147
2972 T t1147 o1147
2973 B b1148 t1147
2974 T t1148 o739 b1148 b1019
2975 B b1149 t1148 v_4
2976 T t1149 o977 b1149
2977 S s1149 t620 h h1097 h1092 h1098 h1099 h1100
2978 G s1149 t1149
2979 B b1150 s1149
2980 T t1150 o939 b1150 b1108
2981 B b1151 t1150
2982 T t1151 o974 b1151 b984 b1134
2983 B b1152 t1151
2984 T t1152 o2 b1152
2985 B b1153 t1152
2986 T t1153 o974 b1147 b4 b1153
2987 B b1154 t1153
2988 T t1154 o937 b1154 b4
2989 B b1155 t1154
2990 T t1155 o1051 b936 b1155 b4 b4
2991 B b1156 t1155
2992 T t1156 o b1156 b4
2993 B b1157 t1156
2994 T t1157 o1025 b936 b1096 b1144 b1157
2995 B b1158 t1157
2996 T t1158 o b1158 b4
2997 B b1159 t1158
2998 T t1159 o1017 b936 b1096 b1159 b4
2999 B b1160 t1159
3000 T t1160 o b1160 b4
3001 B b1161 t1160
3002 S s1161 t620 h h1097 h1092 h1098
3003 G s1161 t995
3004 B b1162 s1161
3005 T t1162 o939 b1162 b1108
3006 B b1163 t1162
3007 T t1163 o967 b1163 b4 b1130
3008 B b1164 t1163
3009 T t1164 o937 b1164 b4
3010 B b1165 t1164
3011 T t1165 o991 b936 b1165 b4 b4
3012 B b1166 t1165
3013 P p1166 String "rwh unfold_fun_prop 0 thenT autoT"
3014 O o1166 ext_rule p1166
3015 T t1166 o739 b967 b978
3016 B b1167 t1166 v_2
3017 T t1167 o977 b1167
3018 S s1167 t620 h h1097 h1092 h1098
3019 G s1167 t1167
3020 B b1168 s1167
3021 T t1168 o939 b1168 b1108
3022 B b1169 t1168
3023 T t1169 o974 b1169 b4 b1130
3024 B b1170 t1169
3025 NCzf_itt_set!set set set Czf_itt_set
3026 O o1170 set
3027 T t1170 o1170
3028 H h1170 s1_1 t1170
3029 H h1171 s2_1 t1170
3030 P p1171 Var s1_1
3031 O o1171 var p1171
3032 T t1171 o1171
3033 B b1171 t1171
3034 P p1172 Var s2_1
3035 O o1172 var p1172
3036 T t1172 o1172
3037 B b1172 t1172
3038 T t1173 o739 b1171 b1172
3039 H h1173 x_1 t1173
3040 T t1174 o739 b967 b1171
3041 H h1174 x_2 t1174
3042 T t1175 o676 b967 b1172
3043 S s1175 t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174
3044 G s1175 t1175
3045 B b1175 s1175
3046 T t1176 o939 b1175 b1108
3047 B b1176 t1176
3048 T t1177 o739 b967 b1172
3049 S s1177 t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174
3050 G s1177 t1177
3051 B b1177 s1177
3052 T t1178 o939 b1177 b1108
3053 B b1178 t1178
3054 NItt_logic Itt_logic Itt_logic NIL
3055 NItt_logic!implies implies implies Itt_logic
3056 O o1178 implies
3057 B b1179 t1174
3058 B b1180 t1177
3059 T t1180 o1178 b1179 b1180
3060 S s1180 t620 h h1097 h1092 h1098 h1170 h1171 h1173
3061 G s1180 t1180
3062 B b1181 s1180
3063 T t1181 o939 b1181 b1108
3064 B b1182 t1181
3065 B b1183 t1173
3066 B b1184 t1180
3067 T t1184 o1178 b1183 b1184
3068 S s1184 t620 h h1097 h1092 h1098 h1170 h1171
3069 G s1184 t1184
3070 B b1185 s1184
3071 T t1185 o939 b1185 b1108
3072 B b1186 t1185
3073 NItt_logic!all all all Itt_logic
3074 O o1186 all
3075 B b1187 t1170
3076 B b1188 t1184 s2_1
3077 T t1188 o1186 b1187 b1188
3078 S s1188 t620 h h1097 h1092 h1098 h1170
3079 G s1188 t1188
3080 B b1189 s1188
3081 T t1189 o939 b1189 b1108
3082 B b1190 t1189
3083 B b1191 t1188 s1_1
3084 T t1191 o1186 b1187 b1191
3085 S s1191 t620 h h1097 h1092 h1098
3086 G s1191 t1191
3087 B b1192 s1191
3088 T t1192 o939 b1192 b1108
3089 B b1193 t1192
3090 T t1193 o2 b1170
3091 B b1194 t1193
3092 T t1194 o974 b1193 b984 b1194
3093 B b1195 t1194
3094 T t1195 o2 b1195
3095 B b1196 t1195
3096 T t1196 o938 b1190 b984 b1196
3097 B b1197 t1196
3098 T t1197 o2 b1197
3099 B b1198 t1197
3100 T t1198 o938 b1186 b984 b1198
3101 B b1199 t1198
3102 T t1199 o2 b1199
3103 B b1200 t1199
3104 T t1200 o938 b1182 b984 b1200
3105 B b1201 t1200
3106 T t1201 o2 b1201
3107 B b1202 t1201
3108 T t1202 o938 b1178 b984 b1202
3109 B b1203 t1202
3110 T t1203 o2 b1203
3111 B b1204 t1203
3112 T t1204 o938 b1176 b4 b1204
3113 B b1205 t1204
3114 T t1205 o b1205 b4
3115 B b1206 t1205
3116 T t1206 o937 b1170 b1206
3117 B b1207 t1206
3118 P p1207 String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3119 O o1207 ext_rule p1207
3120 T t1207 o937 b1205 b4
3121 B b1208 t1207
3122 T t1208 o1207 b936 b1208 b4 b4
3123 B b1209 t1208
3124 T t1209 o b1209 b4
3125 B b1210 t1209
3126 T t1210 o1166 b936 b1207 b1210 b4
3127 B b1211 t1210
3128 T t1211 o b1211 b4
3129 B b1212 t1211
3130 T t1212 o b1166 b1212
3131 B b1213 t1212
3132 T t1213 o1096 b936 b1096 b1161 b1213
3133 B b1214 t1213
3134 T t1214 o b1214 b4
3135 B b1215 t1214
3136 S s1215 t620 h h1097 h1092
3137 G s1215 t968
3138 B b1216 s1215
3139 T t1216 o939 b1216 b1108
3140 B b1217 t1216
3141 T t1217 o967 b1217 b4 b1128
3142 B b1218 t1217
3143 T t1218 o937 b1218 b4
3144 B b1219 t1218
3145 T t1219 o991 b936 b1219 b4 b4
3146 B b1220 t1219
3147 P p1220 Var v_1
3148 O o1220 var p1220
3149 T t1220 o1220
3150 B b1221 t1220
3151 T t1221 o739 b1221 b950
3152 B b1222 t1221 v_1
3153 T t1222 o977 b1222
3154 S s1222 t620 h h1097 h1092
3155 G s1222 t1222
3156 B b1223 s1222
3157 T t1223 o939 b1223 b1108
3158 B b1224 t1223
3159 T t1224 o974 b1224 b4 b1128
3160 B b1225 t1224
3161 H h1225 s2 t1170
3162 T t1225 o739 b1171 b561
3163 H h1226 x_1 t1225
3164 T t1226 o739 b1171 b950
3165 H h1227 x_2 t1226
3166 T t1227 o676 b561 b950
3167 S s1227 t620 h h1097 h1092 h1170 h1225 h1226 h1227
3168 G s1227 t1227
3169 B b1227 s1227
3170 T t1228 o939 b1227 b1108
3171 B b1228 t1228
3172 T t1229 o739 b561 b950
3173 S s1229 t620 h h1097 h1092 h1170 h1225 h1226 h1227
3174 G s1229 t1229
3175 B b1229 s1229
3176 T t1230 o939 b1229 b1108
3177 B b1230 t1230
3178 B b1231 t1226
3179 B b1232 t1229
3180 T t1232 o1178 b1231 b1232
3181 S s1232 t620 h h1097 h1092 h1170 h1225 h1226
3182 G s1232 t1232
3183 B b1233 s1232
3184 T t1233 o939 b1233 b1108
3185 B b1234 t1233
3186 B b1235 t1225
3187 B b1236 t1232
3188 T t1236 o1178 b1235 b1236
3189 S s1236 t620 h h1097 h1092 h1170 h1225
3190 G s1236 t1236
3191 B b1237 s1236
3192 T t1237 o939 b1237 b1108
3193 B b1238 t1237
3194 B b1239 t1236 s2
3195 T t1239 o1186 b1187 b1239
3196 S s1239 t620 h h1097 h1092 h1170
3197 G s1239 t1239
3198 B b1240 s1239
3199 T t1240 o939 b1240 b1108
3200 B b1241 t1240
3201 B b1242 t1239 s1_1
3202 T t1242 o1186 b1187 b1242
3203 S s1242 t620 h h1097 h1092
3204 G s1242 t1242
3205 B b1243 s1242
3206 T t1243 o939 b1243 b1108
3207 B b1244 t1243
3208 T t1244 o2 b1225
3209 B b1245 t1244
3210 T t1245 o974 b1244 b984 b1245
3211 B b1246 t1245
3212 T t1246 o2 b1246
3213 B b1247 t1246
3214 T t1247 o938 b1241 b984 b1247
3215 B b1248 t1247
3216 T t1248 o2 b1248
3217 B b1249 t1248
3218 T t1249 o938 b1238 b984 b1249
3219 B b1250 t1249
3220 T t1250 o2 b1250
3221 B b1251 t1250
3222 T t1251 o938 b1234 b984 b1251
3223 B b1252 t1251
3224 T t1252 o2 b1252
3225 B b1253 t1252
3226 T t1253 o938 b1230 b984 b1253
3227 B b1254 t1253
3228 T t1254 o2 b1254
3229 B b1255 t1254
3230 T t1255 o938 b1228 b4 b1255
3231 B b1256 t1255
3232 T t1256 o b1256 b4
3233 B b1257 t1256
3234 T t1257 o937 b1225 b1257
3235 B b1258 t1257
3236 P p1258 String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3237 O o1258 ext_rule p1258
3238 T t1258 o937 b1256 b4
3239 B b1259 t1258
3240 T t1259 o1258 b936 b1259 b4 b4
3241 B b1260 t1259
3242 T t1260 o b1260 b4
3243 B b1261 t1260
3244 T t1261 o1166 b936 b1258 b1261 b4
3245 B b1262 t1261
3246 T t1262 o b1262 b4
3247 B b1263 t1262
3248 T t1263 o b1220 b1263
3249 B b1264 t1263
3250 T t1264 o1092 b936 b1096 b1215 b1264
3251 B b1265 t1264
3252 P p1265 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3253 O o1265 ext_rule p1265
3254 H h1265 y_1 t642
3255 T t1265 o620 b695
3256 H h1266 z_1 t1265
3257 T t1266 o676 b562 b695
3258 H h1267 z t1266
3259 T t1267 o676 b949 b950
3260 H h1268 v t1267
3261 T t1268 o676 b561 b674
3262 S s1268 t620 h h1265 h1266 h1267 h1268
3263 G s1268 t1268
3264 B b1268 s1268
3265 T t1269 o939 b1268 b1108
3266 B b1269 t1269
3267 S s1269 t620 h h1265 h1266 h1267 h1268
3268 G s1269 t926
3269 B b1270 s1269
3270 T t1270 o939 b1270 b1108
3271 B b1271 t1270
3272 NItt_logic!and and and Itt_logic
3273 O o1271 and
3274 B b1272 t642
3275 B b1273 t1265
3276 T t1273 o1271 b1272 b1273
3277 H h1273 y t1273
3278 S s1273 t620 h h1273 h1267 h1268
3279 G s1273 t926
3280 B b1274 s1273
3281 T t1274 o939 b1274 b1108
3282 B b1275 t1274
3283 B b1276 t1273
3284 B b1277 t1266
3285 T t1277 o1271 b1276 b1277
3286 H h1277 x t1277
3287 S s1277 t620 h h1277 h1268
3288 G s1277 t926
3289 B b1278 s1277
3290 T t1278 o939 b1278 b1108
3291 B b1279 t1278
3292 S s1279 t620 h h1277
3293 G s1279 t926
3294 B b1280 s1279
3295 T t1280 o939 b1280 b1108
3296 B b1281 t1280
3297 T t1281 o938 b1281 b4 b1126
3298 B b1282 t1281
3299 T t1282 o2 b1282
3300 B b1283 t1282
3301 T t1283 o938 b1279 b4 b1283
3302 B b1284 t1283
3303 T t1284 o2 b1284
3304 B b1285 t1284
3305 T t1285 o938 b1275 b4 b1285
3306 B b1286 t1285
3307 T t1286 o2 b1286
3308 B b1287 t1286
3309 T t1287 o938 b1271 b984 b1287
3310 B b1288 t1287
3311 T t1288 o2 b1288
3312 B b1289 t1288
3313 T t1289 o938 b1269 b4 b1289
3314 B b1290 t1289
3315 T t1290 o676 b967 b950
3316 H h1290 v_1 t1290
3317 S s1290 t620 h h1265 h1266 h1267 h1268 h1290
3318 G s1290 t1268
3319 B b1291 s1290
3320 T t1291 o939 b1291 b1108
3321 B b1292 t1291
3322 T t1292 o2 b1290
3323 B b1293 t1292
3324 T t1293 o938 b1292 b4 b1293
3325 B b1294 t1293
3326 B b1295 t950 v_1
3327 T t1295 o712 b1295
3328 S s1295 t620 h h1265 h1266 h1267 h1268
3329 G s1295 t1295
3330 B b1296 s1295
3331 T t1296 o939 b1296 b1108
3332 B b1297 t1296
3333 T t1297 o676 b1221 b950
3334 B b1298 t1297 v_1
3335 T t1298 o977 b1298
3336 S s1298 t620 h h1265 h1266 h1267 h1268
3337 G s1298 t1298
3338 B b1299 s1298
3339 T t1299 o939 b1299 b1108
3340 B b1300 t1299
3341 T t1300 o974 b1300 b984 b1293
3342 B b1301 t1300
3343 T t1301 o2 b1301
3344 B b1302 t1301
3345 T t1302 o974 b1297 b4 b1302
3346 B b1303 t1302
3347 T t1303 o b1303 b4
3348 B b1304 t1303
3349 T t1304 o b1294 b1304
3350 B b1305 t1304
3351 T t1305 o937 b1290 b1305
3352 B b1306 t1305
3353 P p1306 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3354 O o1306 ext_rule p1306
3355 T t1306 o676 b967 b994
3356 H h1306 v_2 t1306
3357 S s1306 t620 h h1265 h1266 h1267 h1268 h1290 h1306
3358 G s1306 t1268
3359 B b1307 s1306
3360 T t1307 o939 b1307 b1108
3361 B b1308 t1307
3362 T t1308 o2 b1294
3363 B b1309 t1308
3364 T t1309 o938 b1308 b4 b1309
3365 B b1310 t1309
3366 B b1311 t967 v_2
3367 T t1311 o712 b1311
3368 S s1311 t620 h h1265 h1266 h1267 h1268 h1290
3369 G s1311 t1311
3370 B b1312 s1311
3371 T t1312 o939 b1312 b1108
3372 B b1313 t1312
3373 T t1313 o676 b967 b978
3374 B b1314 t1313 v_2
3375 T t1314 o977 b1314
3376 S s1314 t620 h h1265 h1266 h1267 h1268 h1290
3377 G s1314 t1314
3378 B b1315 s1314
3379 T t1315 o939 b1315 b1108
3380 B b1316 t1315
3381 T t1316 o974 b1316 b984 b1309
3382 B b1317 t1316
3383 T t1317 o2 b1317
3384 B b1318 t1317
3385 T t1318 o974 b1313 b4 b1318
3386 B b1319 t1318
3387 T t1319 o b1319 b4
3388 B b1320 t1319
3389 T t1320 o b1310 b1320
3390 B b1321 t1320
3391 T t1321 o937 b1294 b1321
3392 B b1322 t1321
3393 P p1322 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3394 O o1322 ext_rule p1322
3395 T t1322 o676 b1018 b1019
3396 H h1322 v_3 t1322
3397 S s1322 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3398 G s1322 t1268
3399 B b1323 s1322
3400 T t1323 o939 b1323 b1108
3401 B b1324 t1323
3402 T t1324 o2 b1310
3403 B b1325 t1324
3404 T t1325 o938 b1324 b4 b1325
3405 B b1326 t1325
3406 T t1326 o b1326 b4
3407 B b1327 t1326
3408 T t1327 o937 b1310 b1327
3409 B b1328 t1327
3410 P p1328 String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"
3411 O o1328 ext_rule p1328
3412 T t1328 o676 b561 b1019
3413 H h1328 v_4 t1328
3414 S s1328 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1328
3415 G s1328 t1268
3416 B b1329 s1328
3417 T t1329 o939 b1329 b1108
3418 B b1330 t1329
3419 T t1330 o2 b1326
3420 B b1331 t1330
3421 T t1331 o938 b1330 b4 b1331
3422 B b1332 t1331
3423 S s1332 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3424 G s1332 t1145
3425 B b1333 s1332
3426 T t1333 o939 b1333 b1108
3427 B b1334 t1333
3428 T t1334 o676 b1148 b1019
3429 B b1335 t1334 v_4
3430 T t1335 o977 b1335
3431 S s1335 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3432 G s1335 t1335
3433 B b1336 s1335
3434 T t1336 o939 b1336 b1108
3435 B b1337 t1336
3436 T t1337 o974 b1337 b984 b1331
3437 B b1338 t1337
3438 T t1338 o2 b1338
3439 B b1339 t1338
3440 T t1339 o974 b1334 b4 b1339
3441 B b1340 t1339
3442 T t1340 o b1340 b4
3443 B b1341 t1340
3444 T t1341 o b1332 b1341
3445 B b1342 t1341
3446 T t1342 o937 b1326 b1342
3447 B b1343 t1342
3448 P p1343 String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3449 O o1343 ext_rule p1343
3450 T t1343 o937 b1332 b4
3451 B b1344 t1343
3452 T t1344 o1343 b936 b1344 b4 b4
3453 B b1345 t1344
3454 H h1345 s1 t1170
3455 T t1345 o739 b560 b561
3456 H h1346 x t1345
3457 T t1346 o739 b1019 b1019
3458 S s1346 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345 h1225 h1346
3459 G s1346 t1346
3460 B b1346 s1346
3461 T t1347 o939 b1346 b1108
3462 B b1347 t1347
3463 B b1348 t1345
3464 B b1349 t1346
3465 T t1349 o1178 b1348 b1349
3466 S s1349 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345 h1225
3467 G s1349 t1349
3468 B b1350 s1349
3469 T t1350 o939 b1350 b1108
3470 B b1351 t1350
3471 B b1352 t1349 s2
3472 T t1352 o1186 b1187 b1352
3473 S s1352 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345
3474 G s1352 t1352
3475 B b1353 s1352
3476 T t1353 o939 b1353 b1108
3477 B b1354 t1353
3478 B b1355 t1352 s1
3479 T t1355 o1186 b1187 b1355
3480 S s1355 t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322
3481 G s1355 t1355
3482 B b1356 s1355
3483 T t1356 o939 b1356 b1108
3484 B b1357 t1356
3485 T t1357 o2 b1340
3486 B b1358 t1357
3487 T t1358 o974 b1357 b984 b1358
3488 B b1359 t1358
3489 T t1359 o2 b1359
3490 B b1360 t1359
3491 T t1360 o938 b1354 b984 b1360
3492 B b1361 t1360
3493 T t1361 o2 b1361
3494 B b1362 t1361
3495 T t1362 o938 b1351 b984 b1362
3496 B b1363 t1362
3497 T t1363 o2 b1363
3498 B b1364 t1363
3499 T t1364 o938 b1347 b4 b1364
3500 B b1365 t1364
3501 T t1365 o b1365 b4
3502 B b1366 t1365
3503 T t1366 o937 b1340 b1366
3504 B b1367 t1366
3505 T t1367 o1086 b1365
3506 B b1368 t1367
3507 T t1368 o b1368 b4
3508 B b1369 t1368
3509 T t1369 o1072 b936 b1367 b1369 b4
3510 B b1370 t1369
3511 T t1370 o b1370 b4
3512 B b1371 t1370
3513 T t1371 o b1345 b1371
3514 B b1372 t1371
3515 T t1372 o1328 b936 b1343 b1372 b4
3516 B b1373 t1372
3517 T t1373 o b1373 b4
3518 B b1374 t1373
3519 T t1374 o1322 b936 b1328 b1374 b4
3520 B b1375 t1374
3521 T t1375 o937 b1319 b4
3522 B b1376 t1375
3523 T t1376 o1072 b936 b1376 b4 b4
3524 B b1377 t1376
3525 T t1377 o b1377 b4
3526 B b1378 t1377
3527 T t1378 o b1375 b1378
3528 B b1379 t1378
3529 P p1379 String "eqSetSymT thenT autoT"
3530 O o1379 ext_rule p1379
3531 T t1379 o676 b950 b994
3532 S s1379 t620 h h1265 h1266 h1267 h1268 h1290
3533 G s1379 t1379
3534 B b1380 s1379
3535 T t1380 o939 b1380 b1108
3536 B b1381 t1380
3537 S s1381 t620 h h1265 h1266 h1267 h1268 h1290
3538 G s1381 t995
3539 B b1382 s1381
3540 T t1382 o939 b1382 b1108
3541 B b1383 t1382
3542 T t1383 o967 b1383 b984 b1309
3543 B b1384 t1383
3544 T t1384 o2 b1384
3545 B b1385 t1384
3546 T t1385 o967 b1381 b4 b1385
3547 B b1386 t1385
3548 T t1386 o676 b994 b950
3549 S s1386 t620 h h1265 h1266 h1267 h1268 h1290
3550 G s1386 t1386
3551 B b1387 s1386
3552 T t1387 o939 b1387 b1108
3553 B b1388 t1387
3554 T t1388 o2 b1386
3555 B b1389 t1388
3556 T t1389 o967 b1388 b4 b1389
3557 B b1390 t1389
3558 T t1390 o b1390 b4
3559 B b1391 t1390
3560 T t1391 o937 b1386 b1391
3561 B b1392 t1391
3562 T t1392 o1086 b1390
3563 B b1393 t1392
3564 T t1393 o b1393 b4
3565 B b1394 t1393
3566 T t1394 o1379 b936 b1392 b1394 b4
3567 B b1395 t1394
3568 T t1395 o b1395 b4
3569 B b1396 t1395
3570 T t1396 o1306 b936 b1322 b1379 b1396
3571 B b1397 t1396
3572 T t1397 o937 b1303 b4
3573 B b1398 t1397
3574 T t1398 o1072 b936 b1398 b4 b4
3575 B b1399 t1398
3576 T t1399 o b1399 b4
3577 B b1400 t1399
3578 T t1400 o b1397 b1400
3579 B b1401 t1400
3580 T t1401 o676 b949 b967
3581 S s1401 t620 h h1265 h1266 h1267 h1268
3582 G s1401 t1401
3583 B b1402 s1401
3584 T t1402 o939 b1402 b1108
3585 B b1403 t1402
3586 S s1403 t620 h h1265 h1266 h1267 h1268
3587 G s1403 t968
3588 B b1404 s1403
3589 T t1404 o939 b1404 b1108
3590 B b1405 t1404
3591 T t1405 o967 b1405 b984 b1293
3592 B b1406 t1405
3593 T t1406 o2 b1406
3594 B b1407 t1406
3595 T t1407 o967 b1403 b4 b1407
3596 B b1408 t1407
3597 T t1408 o676 b967 b949
3598 S s1408 t620 h h1265 h1266 h1267 h1268
3599 G s1408 t1408
3600 B b1409 s1408
3601 T t1409 o939 b1409 b1108
3602 B b1410 t1409
3603 T t1410 o2 b1408
3604 B b1411 t1410
3605 T t1411 o967 b1410 b4 b1411
3606 B b1412 t1411
3607 T t1412 o b1412 b4
3608 B b1413 t1412
3609 T t1413 o937 b1408 b1413
3610 B b1414 t1413
3611 T t1414 o1086 b1412
3612 B b1415 t1414
3613 T t1415 o b1415 b4
3614 B b1416 t1415
3615 T t1416 o1379 b936 b1414 b1416 b4
3616 B b1417 t1416
3617 T t1417 o b1417 b4
3618 B b1418 t1417
3619 T t1418 o1265 b936 b1306 b1401 b1418
3620 B b1419 t1418
3621 T t1419 o b1419 b4
3622 B b1420 t1419
3623 T t1420 o b1265 b1420
3624 B b1421 t1420
3625 T t1421 o b1092 b1421
3626 B b1422 t1421
3627 T t1422 o935 b936 b964 b1086 b1422
3628 B b1423 t1422
3629 T t1423 o934 b1423
3630 B b1424 t1423
3631 P p1424 Number 5399
3632 P p1425 Number 5407
3633 O o1425 resource_defs p1424 p1425 p264
3634 P p1426 Number 5405
3635 O o1426 uid p1426 p1425
3636 T t1426 o1426 b626
3637 B b1426 t1426
3638 T t1427 o b1426 b4
3639 B b1427 t1427
3640 T t1428 o1425 b1427
3641 B b1428 t1428
3642 T t1429 o b1428 b4
3643 B b1429 t1429
3644 T t1430 o920 b923 b934 b1424 b1429
3645 B b1430 t1430
3646 T t1431 o919 b1430
3647 B b1431 t1431
3648 P p1431 Number 5847
3649 P p1432 Number 6273
3650 O o1432 location p1431 p1432
3651 P p1433 String cancel2
3652 O o1433 rule p1433
3653 T t1433 o921 b674
3654 B b1433 t1433
3655 T t1434 o b1433 b4
3656 B b1434 t1434
3657 T t1435 o b617 b1434
3658 B b1435 t1435
3659 T t1436 o739 b695 b696
3660 S s1436 t620 h
3661 G s1436 t1436
3662 B b1436 s1436
3663 T t1437 o618 b1436
3664 B b1437 t1437
3665 S s1437 t620 h
3666 G s1437 t1345
3667 B b1438 s1437
3668 T t1438 o618 b1438
3669 B b1439 t1438
3670 T t1439 o635 b1437 b1439
3671 B b1440 t1439
3672 T t1440 o635 b739 b1440
3673 B b1441 t1440
3674 T t1441 o635 b658 b1441
3675 B b1442 t1441
3676 T t1442 o635 b656 b1442
3677 B b1443 t1442
3678 T t1443 o635 b676 b1443
3679 B b1444 t1443
3680 T t1444 o635 b641 b1444
3681 B b1445 t1444
3682 T t1445 o635 b639 b1445
3683 B b1446 t1445
3684 P p1446 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"
3685 O o1446 ext_rule p1446
3686 T t1446 o b1436 b4
3687 B b1447 t1446
3688 T t1447 o b738 b1447
3689 B b1448 t1447
3690 T t1448 o b657 b1448
3691 B b1449 t1448
3692 T t1449 o b655 b1449
3693 B b1450 t1449
3694 T t1450 o b675 b1450
3695 B b1451 t1450
3696 T t1451 o b640 b1451
3697 B b1452 t1451
3698 T t1452 o b638 b1452
3699 B b1453 t1452
3700 T t1453 o939 b1438 b1453
3701 B b1454 t1453
3702 T t1454 o938 b1454 b4 b947
3703 B b1455 t1454
3704 H h1455 v t1436
3705 T t1455 o572 b674
3706 B b1456 t1455
3707 T t1456 o559 b695 b1456
3708 B b1457 t1456
3709 T t1457 o559 b696 b1456
3710 B b1458 t1457
3711 T t1458 o739 b1457 b1458
3712 S s1458 t620 h h1455
3713 G s1458 t1458
3714 B b1459 s1458
3715 T t1459 o939 b1459 b1453
3716 B b1460 t1459
3717 S s1460 t620 h h1455
3718 G s1460 t1345
3719 B b1461 s1460
3720 T t1461 o939 b1461 b1453
3721 B b1462 t1461
3722 T t1462 o2 b1455
3723 B b1463 t1462
3724 T t1463 o938 b1462 b4 b1463
3725 B b1464 t1463
3726 T t1464 o2 b1464
3727 B b1465 t1464
3728 T t1465 o948 b1460 b4 b1465
3729 B b1466 t1465
3730 H h1466 v_1 t1458
3731 S s1466 t620 h h1455 h1466
3732 G s1466 t1345
3733 B b1467 s1466
3734 T t1467 o939 b1467 b1453
3735 B b1468 t1467
3736 T t1468 o938 b1468 b4 b1465
3737 B b1469 t1468
3738 T t1469 o b1469 b4
3739 B b1470 t1469
3740 T t1470 o b1466 b1470
3741 B b1471 t1470
3742 T t1471 o937 b1455 b1471
3743 B b1472 t1471
3744 T t1472 o937 b1466 b4
3745 B b1473 t1472
3746 T t1473 o964 b936 b1473 b4 b4
3747 B b1474 t1473
3748 P p1474 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
3749 O o1474 ext_rule p1474
3750 T t1474 o559 b674 b1456
3751 B b1475 t1474
3752 T t1475 o559 b560 b1475
3753 B b1476 t1475
3754 T t1476 o739 b1476 b1458
3755 H h1476 v_2 t1476
3756 S s1476 t620 h h1455 h1466 h1476
3757 G s1476 t1345
3758 B b1477 s1476
3759 T t1477 o939 b1477 b1453
3760 B b1478 t1477
3761 T t1478 o2 b1469
3762 B b1479 t1478
3763 T t1479 o938 b1478 b4 b1479
3764 B b1480 t1479
3765 B b1481 t1457 v_2
3766 T t1481 o712 b1481
3767 S s1481 t620 h h1455 h1466
3768 G s1481 t1481
3769 B b1482 s1481
3770 T t1482 o939 b1482 b1453
3771 B b1483 t1482
3772 T t1483 o739 b978 b1458
3773 B b1484 t1483 v_2
3774 T t1484 o977 b1484
3775 S s1484 t620 h h1455 h1466
3776 G s1484 t1484
3777 B b1485 s1484
3778 T t1485 o939 b1485 b1453
3779 B b1486 t1485
3780 T t1486 o974 b1486 b984 b1479
3781 B b1487 t1486
3782 T t1487 o2 b1487
3783 B b1488 t1487
3784 T t1488 o974 b1483 b4 b1488
3785 B b1489 t1488
3786 T t1489 o b1489 b4
3787 B b1490 t1489
3788 T t1490 o b1480 b1490
3789 B b1491 t1490
3790 T t1491 o937 b1469 b1491
3791 B b1492 t1491
3792 P p1492 String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
3793 O o1492 ext_rule p1492
3794 T t1492 o559 b561 b1475
3795 B b1493 t1492
3796 T t1493 o739 b1476 b1493
3797 H h1493 v_3 t1493
3798 S s1493 t620 h h1455 h1466 h1476 h1493
3799 G s1493 t1345
3800 B b1494 s1493
3801 T t1494 o939 b1494 b1453
3802 B b1495 t1494
3803 T t1495 o2 b1480
3804 B b1496 t1495
3805 T t1496 o938 b1495 b4 b1496
3806 B b1497 t1496
3807 B b1498 t1475 v_3
3808 T t1498 o712 b1498
3809 S s1498 t620 h h1455 h1466 h1476
3810 G s1498 t1498
3811 B b1499 s1498
3812 T t1499 o939 b1499 b1453
3813 B b1500 t1499
3814 T t1500 o739 b1476 b1005
3815 B b1501 t1500 v_3
3816 T t1501 o977 b1501
3817 S s1501 t620 h h1455 h1466 h1476
3818 G s1501 t1501
3819 B b1502 s1501
3820 T t1502 o939 b1502 b1453
3821 B b1503 t1502
3822 T t1503 o974 b1503 b984 b1496
3823 B b1504 t1503
3824 T t1504 o2 b1504
3825 B b1505 t1504
3826 T t1505 o974 b1500 b4 b1505
3827 B b1506 t1505
3828 T t1506 o b1506 b4
3829 B b1507 t1506
3830 T t1507 o b1497 b1507
3831 B b1508 t1507
3832 T t1508 o937 b1480 b1508
3833 B b1509 t1508
3834 P p1509 String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
3835 O o1509 ext_rule p1509
3836 T t1509 o559 b560 b567
3837 B b1510 t1509
3838 T t1510 o559 b561 b567
3839 B b1511 t1510
3840 T t1511 o739 b1510 b1511
3841 H h1511 v_4 t1511
3842 S s1511 t620 h h1455 h1466 h1476 h1493 h1511
3843 G s1511 t1345
3844 B b1512 s1511
3845 T t1512 o939 b1512 b1453
3846 B b1513 t1512
3847 T t1513 o2 b1497
3848 B b1514 t1513
3849 T t1514 o938 b1513 b4 b1514
3850 B b1515 t1514
3851 T t1515 o b1515 b4
3852 B b1516 t1515
3853 T t1516 o937 b1497 b1516
3854 B b1517 t1516
3855 P p1517 String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
3856 O o1517 ext_rule p1517
3857 T t1517 o739 b560 b1511
3858 H h1517 v_5 t1517
3859 S s1517 t620 h h1455 h1466 h1476 h1493 h1511 h1517
3860 G s1517 t1345
3861 B b1518 s1517
3862 T t1518 o939 b1518 b1453
3863 B b1519 t1518
3864 T t1519 o2 b1515
3865 B b1520 t1519
3866 T t1520 o938 b1519 b4 b1520
3867 B b1521 t1520
3868 B b1522 t1510 v_5
3869 T t1522 o712 b1522
3870 S s1522 t620 h h1455 h1466 h1476 h1493 h1511
3871 G s1522 t1522
3872 B b1523 s1522
3873 T t1523 o939 b1523 b1453
3874 B b1524 t1523
3875 T t1524 o739 b1033 b1511
3876 B b1525 t1524 v_5
3877 T t1525 o977 b1525
3878 S s1525 t620 h h1455 h1466 h1476 h1493 h1511
3879 G s1525 t1525
3880 B b1526 s1525
3881 T t1526 o939 b1526 b1453
3882 B b1527 t1526
3883 T t1527 o974 b1527 b984 b1520
3884 B b1528 t1527
3885 T t1528 o2 b1528
3886 B b1529 t1528
3887 T t1529 o974 b1524 b4 b1529
3888 B b1530 t1529
3889 T t1530 o b1530 b4
3890 B b1531 t1530
3891 T t1531 o b1521 b1531
3892 B b1532 t1531
3893 T t1532 o937 b1515 b1532
3894 B b1533 t1532
3895 P p1533 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3896 O o1533 ext_rule p1533
3897 T t1533 o937 b1521 b4
3898 B b1534 t1533
3899 T t1534 o1533 b936 b1534 b4 b4
3900 B b1535 t1534
3901 T t1535 o937 b1530 b4
3902 B b1536 t1535
3903 T t1536 o1051 b936 b1536 b4 b4
3904 B b1537 t1536
3905 T t1537 o b1537 b4
3906 B b1538 t1537
3907 T t1538 o b1535 b1538
3908 B b1539 t1538
3909 T t1539 o1517 b936 b1533 b1539 b4
3910 B b1540 t1539
3911 T t1540 o b1540 b4
3912 B b1541 t1540
3913 T t1541 o1509 b936 b1517 b1541 b4
3914 B b1542 t1541
3915 T t1542 o937 b1506 b4
3916 B b1543 t1542
3917 T t1543 o1051 b936 b1543 b4 b4
3918 B b1544 t1543
3919 T t1544 o b1544 b4
3920 B b1545 t1544
3921 T t1545 o b1542 b1545
3922 B b1546 t1545
3923 T t1546 o1492 b936 b1509 b1546 b4
3924 B b1547 t1546
3925 T t1547 o937 b1489 b4
3926 B b1548 t1547
3927 T t1548 o1051 b936 b1548 b4 b4
3928 B b1549 t1548
3929 T t1549 o b1549 b4
3930 B b1550 t1549
3931 T t1550 o b1547 b1550
3932 B b1551 t1550
3933 T t1551 o1474 b936 b1492 b1551 b4
3934 B b1552 t1551
3935 T t1552 o b1552 b4
3936 B b1553 t1552
3937 T t1553 o b1474 b1553
3938 B b1554 t1553
3939 S s1554 t620 h
3940 G s1554 t1458
3941 B b1555 s1554
3942 T t1555 o939 b1555 b1453
3943 B b1556 t1555
3944 T t1556 o948 b1556 b4 b1463
3945 B b1557 t1556
3946 T t1557 o1086 b1557
3947 B b1558 t1557
3948 T t1558 o b1558 b4
3949 B b1559 t1558
3950 T t1559 o964 b936 b1558 b1559 b4
3951 B b1560 t1559
3952 H h1560 v t1458
3953 S s1560 t620 h h1560
3954 G s1560 t1345
3955 B b1561 s1560
3956 T t1561 o939 b1561 b1453
3957 B b1562 t1561
3958 T t1562 o938 b1562 b4 b1463
3959 B b1563 t1562
3960 T t1563 o1086 b1563
3961 B b1564 t1563
3962 T t1564 o b1564 b4
3963 B b1565 t1564
3964 T t1565 o1533 b936 b1564 b1565 b4
3965 B b1566 t1565
3966 T t1566 o b1566 b4
3967 B b1567 t1566
3968 H h1567 x t1436
3969 H h1568 v_1 t1476
3970 H h1569 v_2 t1493
3971 H h1570 v_3 t1511
3972 B b1570 t1510 v_4
3973 T t1570 o712 b1570
3974 S s1570 t620 h h1567 h1560 h1568 h1569 h1570
3975 G s1570 t1570
3976 B b1571 s1570
3977 T t1571 o939 b1571 b1108
3978 B b1572 t1571
3979 T t1572 o739 b1148 b1511
3980 B b1573 t1572 v_4
3981 T t1573 o977 b1573
3982 S s1573 t620 h h1567 h1560 h1568 h1569 h1570
3983 G s1573 t1573
3984 B b1574 s1573
3985 T t1574 o939 b1574 b1108
3986 B b1575 t1574
3987 S s1575 t620 h h1567 h1560 h1568 h1569 h1570
3988 G s1575 t1345
3989 B b1576 s1575
3990 T t1576 o939 b1576 b1108
3991 B b1577 t1576
3992 S s1577 t620 h h1567 h1560 h1568 h1569
3993 G s1577 t1345
3994 B b1578 s1577
3995 T t1578 o939 b1578 b1108
3996 B b1579 t1578
3997 S s1579 t620 h h1567 h1560 h1568
3998 G s1579 t1345
3999 B b1580 s1579
4000 T t1580 o939 b1580 b1108
4001 B b1581 t1580
4002 S s1581 t620 h h1567 h1560
4003 G s1581 t1345
4004 B b1582 s1581
4005 T t1582 o939 b1582 b1108
4006 B b1583 t1582
4007 S s1583 t620 h h1567
4008 G s1583 t1345
4009 B b1584 s1583
4010 T t1584 o939 b1584 b1108
4011 B b1585 t1584
4012 T t1585 o938 b1585 b4 b947
4013 B b1586 t1585
4014 T t1586 o2 b1586
4015 B b1587 t1586
4016 T t1587 o938 b1583 b4 b1587
4017 B b1588 t1587
4018 T t1588 o2 b1588
4019 B b1589 t1588
4020 T t1589 o938 b1581 b4 b1589
4021 B b1590 t1589
4022 T t1590 o2 b1590
4023 B b1591 t1590
4024 T t1591 o938 b1579 b4 b1591
4025 B b1592 t1591
4026 T t1592 o2 b1592
4027 B b1593 t1592
4028 T t1593 o938 b1577 b4 b1593
4029 B b1594 t1593
4030 T t1594 o2 b1594
4031 B b1595 t1594
4032 T t1595 o974 b1575 b984 b1595
4033 B b1596 t1595
4034 T t1596 o2 b1596
4035 B b1597 t1596
4036 T t1597 o974 b1572 b4 b1597
4037 B b1598 t1597
4038 T t1598 o937 b1598 b4
4039 B b1599 t1598
4040 T t1599 o1051 b936 b1599 b4 b4
4041 B b1600 t1599
4042 T t1600 o b1600 b4
4043 B b1601 t1600
4044 T t1601 o1517 b936 b1564 b1567 b1601
4045 B b1602 t1601
4046 T t1602 o b1602 b4
4047 B b1603 t1602
4048 T t1603 o1509 b936 b1564 b1603 b4
4049 B b1604 t1603
4050 T t1604 o b1604 b4
4051 B b1605 t1604
4052 P p1605 String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
4053 O o1605 ext_rule p1605
4054 B b1606 t1475 v_2
4055 T t1606 o712 b1606
4056 S s1606 t620 h h1567 h1560 h1568
4057 G s1606 t1606
4058 B b1607 s1606
4059 T t1607 o939 b1607 b1108
4060 B b1608 t1607
4061 T t1608 o739 b1476 b978
4062 B b1609 t1608 v_2
4063 T t1609 o977 b1609
4064 S s1609 t620 h h1567 h1560 h1568
4065 G s1609 t1609
4066 B b1610 s1609
4067 T t1610 o939 b1610 b1108
4068 B b1611 t1610
4069 T t1611 o974 b1611 b984 b1591
4070 B b1612 t1611
4071 T t1612 o2 b1612
4072 B b1613 t1612
4073 T t1613 o974 b1608 b4 b1613
4074 B b1614 t1613
4075 T t1614 o937 b1614 b4
4076 B b1615 t1614
4077 T t1615 o1605 b936 b1615 b4 b4
4078 B b1616 t1615
4079 T t1616 o b1616 b4
4080 B b1617 t1616
4081 T t1617 o1492 b936 b1564 b1605 b1617
4082 B b1618 t1617
4083 T t1618 o b1618 b4
4084 B b1619 t1618
4085 B b1620 t1457 v_1
4086 T t1620 o712 b1620
4087 S s1620 t620 h h1567 h1560
4088 G s1620 t1620
4089 B b1621 s1620
4090 T t1621 o939 b1621 b1108
4091 B b1622 t1621
4092 T t1622 o739 b1221 b1458
4093 B b1623 t1622 v_1
4094 T t1623 o977 b1623
4095 S s1623 t620 h h1567 h1560
4096 G s1623 t1623
4097 B b1624 s1623
4098 T t1624 o939 b1624 b1108
4099 B b1625 t1624
4100 T t1625 o974 b1625 b984 b1589
4101 B b1626 t1625
4102 T t1626 o2 b1626
4103 B b1627 t1626
4104 T t1627 o974 b1622 b4 b1627
4105 B b1628 t1627
4106 T t1628 o937 b1628 b4
4107 B b1629 t1628
4108 T t1629 o1605 b936 b1629 b4 b4
4109 B b1630 t1629
4110 T t1630 o b1630 b4
4111 B b1631 t1630
4112 T t1631 o1474 b936 b1564 b1619 b1631
4113 B b1632 t1631
4114 T t1632 o b1632 b4
4115 B b1633 t1632
4116 T t1633 o b1560 b1633
4117 B b1634 t1633
4118 T t1634 o1446 b936 b1472 b1554 b1634
4119 B b1635 t1634
4120 T t1635 o934 b1635
4121 B b1636 t1635
4122 P p1636 Number 5870
4123 P p1637 Number 5878
4124 O o1637 resource_defs p1636 p1637 p264
4125 P p1638 Number 5876
4126 O o1638 uid p1638 p1637
4127 T t1638 o1638 b626
4128 B b1638 t1638
4129 T t1639 o b1638 b4
4130 B b1639 t1639
4131 T t1640 o1637 b1639
4132 B b1640 t1640
4133 T t1641 o b1640 b4
4134 B b1641 t1641
4135 T t1642 o1433 b1435 b1446 b1636 b1641
4136 B b1642 t1642
4137 T t1643 o1432 b1642
4138 B b1643 t1643
4139 P p1643 Number 6275
4140 P p1644 Number 6344
4141 O o1644 location p1643 p1644
4142 O o1645 str_let p1643 p1644
4143 P p1645 Number 6279
4144 O o1646 patt_var p1645 p1644
4145 O o1647 patt_done p1643 p1644
4146 T t1647 o1647
4147 B b1647 t1647 groupCancelLeftT
4148 T t1648 o1646 b1647
4149 B b1648 t1648
4150 O o1648 fun p1645 p1644
4151 O o1649 patt_if p1645 p1644
4152 P p1649 Number 6296
4153 P p1650 Number 6297
4154 O o1650 patt_var p1649 p1650
4155 O o1651 patt_body p1645 p1644
4156 P p1651 Number 6298
4157 P p1652 Number 6299
4158 O o1652 patt_var p1651 p1652
4159 P p1653 Number 6305
4160 O o1653 apply p1653 p1644
4161 P p1654 Number 6342
4162 O o1654 apply p1653 p1654
4163 P p1655 Number 6340
4164 O o1655 apply p1653 p1655
4165 P p1656 Number 6312
4166 O o1656 lid p1653 p1656
4167 O o1657 lid p920
4168 T t1657 o1657
4169 B b1657 t1657
4170 T t1658 o1656 b1657
4171 B b1658 t1658
4172 P p1658 Number 6314
4173 P p1659 Number 6339
4174 O o1659 apply p1658 p1659
4175 P p1660 Number 6337
4176 O o1660 proj p1658 p1660
4177 O o1661 uid p1658 p1660
4178 T t1661 o1661 b837
4179 B b1661 t1661
4180 P p1661 Number 6323
4181 O o1662 lid p1661 p1660
4182 T t1662 o1662 b839
4183 B b1662 t1662
4184 T t1663 o1660 b1661 b1662
4185 B b1663 t1663
4186 P p1663 Number 6338
4187 O o1663 lid p1663 p1659
4188 T t1664 o1663 b842
4189 B b1664 t1664
4190 T t1665 o1659 b1663 b1664
4191 B b1665 t1665
4192 T t1666 o1655 b1658 b1665
4193 B b1666 t1666
4194 P p1666 Number 6341
4195 O o1666 lid p1666 p1654
4196 P p1667 Var t
4197 O o1667 var p1667
4198 T t1667 o1667
4199 B b1667 t1667
4200 T t1668 o1666 b1667
4201 B b1668 t1668
4202 T t1669 o1654 b1666 b1668
4203 B b1669 t1669
4204 P p1669 Number 6343
4205 O o1669 lid p1669 p1644
4206 T t1670 o1669 b842
4207 B b1670 t1670
4208 T t1671 o1653 b1669 b1670
4209 B b1671 t1671
4210 T t1672 o1651 b1671
4211 B b1672 t1672 p
4212 T t1673 o1652 b1672
4213 B b1673 t1673
4214 T t1674 o1649 b1673
4215 B b1674 t1674
4216 T t1675 o1648 b1674
4217 B b1675 t1675
4218 T t1676 o1651 b1675
4219 B b1676 t1676 t
4220 T t1677 o1650 b1676
4221 B b1677 t1677
4222 T t1678 o1649 b1677
4223 B b1678 t1678
4224 T t1679 o1648 b1678
4225 B b1679 t1679
4226 T t1680 o1645 b1648 b1679
4227 B b1680 t1680
4228 T t1681 o b1680 b4
4229 B b1681 t1681
4230 T t1682 o1645 b1681
4231 B b1682 t1682
4232 T t1683 o392 b1682
4233 B b1683 t1683
4234 T t1684 o1644 b1683
4235 B b1684 t1684
4236 P p1684 Number 6346
4237 P p1685 Number 6416
4238 O o1685 location p1684 p1685
4239 O o1686 str_let p1684 p1685
4240 P p1686 Number 6350
4241 O o1687 patt_var p1686 p1685
4242 O o1688 patt_done p1684 p1685
4243 T t1688 o1688
4244 B b1688 t1688 groupCancelRightT
4245 T t1689 o1687 b1688
4246 B b1689 t1689
4247 O o1689 fun p1686 p1685
4248 O o1690 patt_if p1686 p1685
4249 P p1690 Number 6368
4250 P p1691 Number 6369
4251 O o1691 patt_var p1690 p1691
4252 O o1692 patt_body p1686 p1685
4253 P p1692 Number 6370
4254 P p1693 Number 6371
4255 O o1693 patt_var p1692 p1693
4256 P p1694 Number 6377
4257 O o1694 apply p1694 p1685
4258 P p1695 Number 6414
4259 O o1695 apply p1694 p1695
4260 P p1696 Number 6412
4261 O o1696 apply p1694 p1696
4262 P p1697 Number 6384
4263 O o1697 lid p1694 p1697
4264 O o1698 lid p1433
4265 T t1698 o1698
4266 B b1698 t1698
4267 T t1699 o1697 b1698
4268 B b1699 t1699
4269 P p1699 Number 6386
4270 P p1700 Number 6411
4271 O o1700 apply p1699 p1700
4272 P p1701 Number 6409
4273 O o1701 proj p1699 p1701
4274 O o1702 uid p1699 p1701
4275 T t1702 o1702 b837
4276 B b1702 t1702
4277 P p1702 Number 6395
4278 O o1703 lid p1702 p1701
4279 T t1703 o1703 b839
4280 B b1703 t1703
4281 T t1704 o1701 b1702 b1703
4282 B b1704 t1704
4283 P p1704 Number 6410
4284 O o1704 lid p1704 p1700
4285 T t1705 o1704 b842
4286 B b1705 t1705
4287 T t1706 o1700 b1704 b1705
4288 B b1706 t1706
4289 T t1707 o1696 b1699 b1706
4290 B b1707 t1707
4291 P p1707 Number 6413
4292 O o1707 lid p1707 p1695
4293 T t1708 o1707 b1667
4294 B b1708 t1708
4295 T t1709 o1695 b1707 b1708
4296 B b1709 t1709
4297 P p1709 Number 6415
4298 O o1709 lid p1709 p1685
4299 T t1710 o1709 b842
4300 B b1710 t1710
4301 T t1711 o1694 b1709 b1710
4302 B b1711 t1711
4303 T t1712 o1692 b1711
4304 B b1712 t1712 p
4305 T t1713 o1693 b1712
4306 B b1713 t1713
4307 T t1714 o1690 b1713
4308 B b1714 t1714
4309 T t1715 o1689 b1714
4310 B b1715 t1715
4311 T t1716 o1692 b1715
4312 B b1716 t1716 t
4313 T t1717 o1691 b1716
4314 B b1717 t1717
4315 T t1718 o1690 b1717
4316 B b1718 t1718
4317 T t1719 o1689 b1718
4318 B b1719 t1719
4319 T t1720 o1686 b1689 b1719
4320 B b1720 t1720
4321 T t1721 o b1720 b4
4322 B b1721 t1721
4323 T t1722 o1686 b1721
4324 B b1722 t1722
4325 T t1723 o392 b1722
4326 B b1723 t1723
4327 T t1724 o1685 b1723
4328 B b1724 t1724
4329 P p1724 Number 6434
4330 P p1725 Number 6675
4331 O o1725 location p1724 p1725
4332 P p1726 String unique_id1
4333 O o1726 rule p1726
4334 P p1727 Var e2
4335 O o1727 var p1727
4336 T t1727 o1727
4337 B b1727 t1727
4338 T t1728 o620 b1727
4339 S s1728 t637 h
4340 G s1728 t1728
4341 B b1728 s1728
4342 T t1729 o618 b1728
4343 B b1729 t1729
4344 T t1730 o655 b1727 b554
4345 S s1730 t620 h
4346 G s1730 t1730
4347 B b1730 s1730
4348 T t1731 o618 b1730
4349 B b1731 t1731
4350 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4351 NCzf_itt_dall!dall dall dall Czf_itt_dall
4352 O o1731 dall
4353 T t1732 o559 b1727 b573
4354 B b1732 t1732
4355 T t1733 o676 b1732 b573
4356 B b1733 t1733
4357 T t1734 o559 b573 b1727
4358 B b1734 t1734
4359 T t1735 o676 b1734 b573
4360 B b1735 t1735
4361 T t1736 o1271 b1733 b1735
4362 B b1736 t1736 s
4363 T t1737 o1731 b554 b1736
4364 H h1737 x t1737
4365 T t1738 o676 b1727 b567
4366 S s1738 t620 h h1737
4367 G s1738 t1738
4368 B b1738 s1738
4369 T t1739 o618 b1738
4370 B b1739 t1739
4371 T t1740 o635 b1731 b1739
4372 B b1740 t1740
4373 T t1741 o635 b1729 b1740
4374 B b1741 t1741
4375 P p1741 String "withT << id >> (dT 2) thenT autoT"
4376 O o1741 ext_rule p1741
4377 T t1742 o b1730 b4
4378 B b1742 t1742
4379 T t1743 o b1728 b1742
4380 B b1743 t1743
4381 T t1744 o939 b1738 b1743
4382 B b1744 t1744
4383 T t1745 o938 b1744 b4 b947
4384 B b1745 t1745
4385 T t1746 o559 b1727 b567
4386 B b1746 t1746
4387 T t1747 o676 b1746 b567
4388 H h1747 y t1747
4389 T t1748 o559 b567 b1727
4390 B b1748 t1748
4391 T t1749 o676 b1748 b567
4392 H h1749 z t1749
4393 S s1749 t620 h h1737 h1747 h1749
4394 G s1749 t1738
4395 B b1749 s1749
4396 T t1750 o939 b1749 b1743
4397 B b1750 t1750
4398 B b1751 t1747
4399 B b1752 t1749
4400 T t1752 o1271 b1751 b1752
4401 H h1752 w t1752
4402 S s1752 t620 h h1737 h1752
4403 G s1752 t1738
4404 B b1753 s1752
4405 T t1753 o939 b1753 b1743
4406 B b1754 t1753
4407 P p1754 String with
4408 O o1754 arg_named p1754
4409 NSummary!arg_term_list arg_term_list arg_term_list Summary
4410 O o1755 arg_term_list
4411 T t1755 o b567 b4
4412 B b1755 t1755
4413 T t1756 o1755 b1755
4414 B b1756 t1756
4415 T t1757 o1754 b1756
4416 B b1757 t1757
4417 T t1758 o b1757 b4
4418 B b1758 t1758
4419 T t1759 o938 b1744 b1758 b947
4420 B b1759 t1759
4421 T t1760 o2 b1759
4422 B b1760 t1760
4423 T t1761 o938 b1754 b4 b1760
4424 B b1761 t1761
4425 T t1762 o2 b1761
4426 B b1762 t1762
4427 T t1763 o938 b1750 b4 b1762
4428 B b1763 t1763
4429 T t1764 o b1763 b4
4430 B b1764 t1764
4431 T t1765 o937 b1745 b1764
4432 B b1765 t1765
4433 P p1765 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
4434 O o1765 ext_rule p1765
4435 T t1766 o937 b1763 b4
4436 B b1766 t1766
4437 T t1767 o1765 b936 b1766 b4 b4
4438 B b1767 t1767
4439 T t1768 o b1767 b4
4440 B b1768 t1768
4441 S s1768 t620 h
4442 G s1768 t1728
4443 B b1769 s1768
4444 T t1769 o b1769 b1742
4445 B b1770 t1769
4446 T t1770 o939 b1749 b1770
4447 B b1771 t1770
4448 T t1771 o939 b1753 b1770
4449 B b1772 t1771
4450 T t1772 o939 b1738 b1770
4451 B b1773 t1772
4452 T t1773 o938 b1773 b1758 b947
4453 B b1774 t1773
4454 T t1774 o2 b1774
4455 B b1775 t1774
4456 T t1775 o938 b1772 b4 b1775
4457 B b1776 t1775
4458 T t1776 o2 b1776
4459 B b1777 t1776
4460 T t1777 o938 b1771 b4 b1777
4461 B b1778 t1777
4462 T t1778 o937 b1778 b4
4463 B b1779 t1778
4464 T t1779 o1765 b936 b1779 b4 b4
4465 B b1780 t1779
4466 P p1780 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
4467 O o1780 ext_rule p1780
4468 H h1780 v t1738
4469 S s1780 t620 h h1737 h1747 h1749 h1780
4470 G s1780 t1738
4471 B b1781 s1780
4472 T t1781 o939 b1781 b1770
4473 B b1782 t1781
4474 T t1782 o2 b1778
4475 B b1783 t1782
4476 T t1783 o938 b1782 b4 b1783
4477 B b1784 t1783
4478 T t1784 o b1784 b4
4479 B b1785 t1784
4480 T t1785 o937 b1778 b1785
4481 B b1786 t1785
4482 T t1786 o1086 b1784
4483 B b1787 t1786
4484 T t1787 o b1787 b4
4485 B b1788 t1787
4486 T t1788 o1780 b936 b1786 b1788 b4
4487 B b1789 t1788
4488 P p1789 String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
4489 O o1789 ext_rule p1789
4490 P p1790 Var e
4491 O o1790 var p1790
4492 T t1790 o1790
4493 B b1790 t1790
4494 T t1791 o620 b1790
4495 S s1791 t637 h h1737 h1747 h1749
4496 G s1791 t1791
4497 B b1791 s1791
4498 T t1792 o939 b1791 b1770
4499 B b1792 t1792
4500 T t1793 o559 b1727 b1790
4501 B b1793 t1793
4502 T t1794 o620 b1793
4503 S s1794 t637 h h1737 h1747 h1749
4504 G s1794 t1794
4505 B b1794 s1794
4506 T t1795 o939 b1794 b1770
4507 B b1795 t1795
4508 T t1796 o739 b1793 b1727
4509 S s1796 t620 h h1737 h1747 h1749
4510 G s1796 t1796
4511 B b1796 s1796
4512 T t1797 o939 b1796 b1770
4513 B b1797 t1797
4514 T t1798 o967 b1797 b984 b1783
4515 B b1798 t1798
4516 T t1799 o2 b1798
4517 B b1799 t1799
4518 T t1800 o974 b1795 b984 b1799
4519 B b1800 t1800
4520 T t1801 o2 b1800
4521 B b1801 t1801
4522 T t1802 o974 b1792 b4 b1801
4523 B b1802 t1802
4524 T t1803 o676 b1793 b1727
4525 S s1803 t620 h h1737 h1747 h1749
4526 G s1803 t1803
4527 B b1803 s1803
4528 T t1804 o939 b1803 b1770
4529 B b1804 t1804
4530 T t1805 o967 b1804 b4 b1799
4531 B b1805 t1805
4532 H h1805 v t1747
4533 S s1805 t620 h h1737 h1747 h1749 h1805
4534 G s1805 t1738
4535 B b1806 s1805
4536 T t1806 o939 b1806 b1770
4537 B b1807 t1806
4538 T t1807 o938 b1807 b4 b1783
4539 B b1808 t1807
4540 B b1809 t1746 v
4541 T t1809 o712 b1809
4542 S s1809 t620 h h1737 h1747 h1749
4543 G s1809 t1809
4544 B b1810 s1809
4545 T t1810 o939 b1810 b1770
4546 B b1811 t1810
4547 B b1812 t1747 v
4548 T t1812 o977 b1812
4549 S s1812 t620 h h1737 h1747 h1749
4550 G s1812 t1812
4551 B b1813 s1812
4552 T t1813 o939 b1813 b1770
4553 B b1814 t1813
4554 T t1814 o974 b1814 b984 b1783
4555 B b1815 t1814
4556 T t1815 o2 b1815
4557 B b1816 t1815
4558 T t1816 o974 b1811 b4 b1816
4559 B b1817 t1816
4560 T t1817 o b1817 b4
4561 B b1818 t1817
4562 T t1818 o b1808 b1818
4563 B b1819 t1818
4564 T t1819 o b1805 b1819
4565 B b1820 t1819
4566 T t1820 o b1802 b1820
4567 B b1821 t1820
4568 T t1821 o937 b1778 b1821
4569 B b1822 t1821
4570 T t1822 o1086 b1802
4571 B b1823 t1822
4572 T t1823 o1086 b1805
4573 B b1824 t1823
4574 T t1824 o1086 b1808
4575 B b1825 t1824
4576 T t1825 o1086 b1817
4577 B b1826 t1825
4578 T t1826 o b1826 b4
4579 B b1827 t1826
4580 T t1827 o b1825 b1827
4581 B b1828 t1827
4582 T t1828 o b1824 b1828
4583 B b1829 t1828
4584 T t1829 o b1823 b1829
4585 B b1830 t1829
4586 T t1830 o1789 b936 b1822 b1830 b4
4587 B b1831 t1830
4588 T t1831 o b1831 b4
4589 B b1832 t1831
4590 T t1832 o b1831 b1832
4591 B b1833 t1832
4592 T t1833 o b1789 b1833
4593 B b1834 t1833
4594 T t1834 o b1780 b1834
4595 B b1835 t1834
4596 T t1835 o1741 b936 b1765 b1768 b1835
4597 B b1836 t1835
4598 T t1836 o934 b1836
4599 B b1837 t1836
4600 P p1837 Number 6460
4601 P p1838 Number 6468
4602 O o1838 resource_defs p1837 p1838 p264
4603 P p1839 Number 6466
4604 O o1839 uid p1839 p1838
4605 T t1839 o1839 b626
4606 B b1839 t1839
4607 T t1840 o b1839 b4
4608 B b1840 t1840
4609 T t1841 o1838 b1840
4610 B b1841 t1841
4611 T t1842 o b1841 b4
4612 B b1842 t1842
4613 T t1843 o1726 b618 b1741 b1837 b1842
4614 B b1843 t1843
4615 T t1844 o1725 b1843
4616 B b1844 t1844
4617 P p1844 Number 6993
4618 P p1845 Number 7320
4619 O o1845 location p1844 p1845
4620 P p1846 String unique_inv
4621 O o1846 rule p1846
4622 T t1846 o559 b561 b573
4623 B b1846 t1846
4624 T t1847 o739 b1846 b567
4625 H h1847 x t1847
4626 T t1848 o559 b573 b561
4627 B b1848 t1848
4628 T t1849 o739 b1848 b567
4629 H h1849 y t1849
4630 T t1850 o739 b561 b574
4631 S s1850 t620 h h1847 h1849
4632 G s1850 t1850
4633 B b1850 s1850
4634 T t1851 o618 b1850
4635 B b1851 t1851
4636 T t1852 o635 b658 b1851
4637 B b1852 t1852
4638 T t1853 o635 b795 b1852
4639 B b1853 t1853
4640 T t1854 o635 b641 b1853
4641 B b1854 t1854
4642 T t1855 o635 b712 b1854
4643 B b1855 t1855
4644 P p1855 String "assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
4645 O o1855 ext_rule p1855
4646 T t1856 o b657 b4
4647 B b1856 t1856
4648 T t1857 o b794 b1856
4649 B b1857 t1857
4650 T t1858 o b640 b1857
4651 B b1858 t1858
4652 T t1859 o b711 b1858
4653 B b1859 t1859
4654 T t1860 o939 b1850 b1859
4655 B b1860 t1860
4656 T t1861 o938 b1860 b4 b947
4657 B b1861 t1861
4658 T t1862 o559 b574 b573
4659 B b1862 t1862
4660 T t1863 o739 b1862 b567
4661 H h1863 v t1863
4662 S s1863 t620 h h1847 h1849 h1863
4663 G s1863 t1850
4664 B b1863 s1863
4665 T t1864 o939 b1863 b1859
4666 B b1864 t1864
4667 T t1865 o2 b1861
4668 B b1865 t1865
4669 T t1866 o938 b1864 b4 b1865
4670 B b1866 t1866
4671 T t1867 o b1866 b4
4672 B b1867 t1867
4673 T t1868 o937 b1861 b1867
4674 B b1868 t1868
4675 P p1868 String "setSubstT << equal{id; op{inv{'s}; 's}} >> 2 thenAT autoT"
4676 O o1868 ext_rule p1868
4677 T t1869 o676 b567 b1862
4678 S s1869 t620 h h1847 h1849 h1863
4679 G s1869 t1869
4680 B b1869 s1869
4681 T t1870 o939 b1869 b1859
4682 B b1870 t1870
4683 T t1871 o739 b567 b1862
4684 S s1871 t620 h h1847 h1849 h1863
4685 G s1871 t1871
4686 B b1871 s1871
4687 T t1872 o939 b1871 b1859
4688 B b1872 t1872
4689 T t1873 o2 b1866
4690 B b1873 t1873
4691 T t1874 o967 b1872 b984 b1873
4692 B b1874 t1874
4693 T t1875 o2 b1874
4694 B b1875 t1875
4695 T t1876 o967 b1870 b4 b1875
4696 B b1876 t1876
4697 T t1877 o739 b1846 b1862
4698 H h1877 v_1 t1877
4699 S s1877 t620 h h1847 h1849 h1863 h1877
4700 G s1877 t1850
4701 B b1877 s1877
4702 T t1878 o939 b1877 b1859
4703 B b1878 t1878
4704 T t1879 o938 b1878 b4 b1873
4705 B b1879 t1879
4706 B b1880 t1846 v_1
4707 T t1880 o712 b1880
4708 S s1880 t620 h h1847 h1849 h1863
4709 G s1880 t1880
4710 B b1881 s1880
4711 T t1881 o939 b1881 b1859
4712 B b1882 t1881
4713 T t1882 o739 b1846 b1221
4714 B b1883 t1882 v_1
4715 T t1883 o977 b1883
4716 S s1883 t620 h h1847 h1849 h1863
4717 G s1883 t1883
4718 B b1884 s1883
4719 T t1884 o939 b1884 b1859
4720 B b1885 t1884
4721 T t1885 o974 b1885 b984 b1873
4722 B b1886 t1885
4723 T t1886 o2 b1886
4724 B b1887 t1886
4725 T t1887 o974 b1882 b4 b1887
4726 B b1888 t1887
4727 T t1888 o b1888 b4
4728 B b1889 t1888
4729 T t1889 o b1879 b1889
4730 B b1890 t1889
4731 T t1890 o b1876 b1890
4732 B b1891 t1890
4733 T t1891 o937 b1866 b1891
4734 B b1892 t1891
4735 P p1892 String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
4736 O o1892 ext_rule p1892
4737 T t1892 o937 b1876 b4
4738 B b1893 t1892
4739 T t1893 o1892 b936 b1893 b4 b4
4740 B b1894 t1893
4741 P p1894 String "groupCancelRightT << 's >> thenT autoT"
4742 O o1894 ext_rule p1894
4743 T t1894 o937 b1879 b4
4744 B b1895 t1894
4745 T t1895 o1894 b936 b1895 b4 b4
4746 B b1896 t1895
4747 T t1896 o937 b1888 b4
4748 B b1897 t1896
4749 T t1897 o1072 b936 b1897 b4 b4
4750 B b1898 t1897
4751 T t1898 o b1898 b4
4752 B b1899 t1898
4753 T t1899 o b1896 b1899
4754 B b1900 t1899
4755 T t1900 o b1894 b1900
4756 B b1901 t1900
4757 T t1901 o1868 b936 b1892 b1901 b4
4758 B b1902 t1901
4759 T t1902 o b1902 b4
4760 B b1903 t1902
4761 T t1903 o1855 b936 b1868 b1903 b4
4762 B b1904 t1903
4763 T t1904 o934 b1904
4764 B b1905 t1904
4765 P p1905 Number 7019
4766 P p1906 Number 7027
4767 O o1906 resource_defs p1905 p1906 p264
4768 P p1907 Number 7025
4769 O o1907 uid p1907 p1906
4770 T t1907 o1907 b626
4771 B b1907 t1907
4772 T t1908 o b1907 b4
4773 B b1908 t1908
4774 T t1909 o1906 b1908
4775 B b1909 t1909
4776 T t1910 o b1909 b4
4777 B b1910 t1910
4778 T t1911 o1846 b618 b1855 b1905 b1910
4779 B b1911 t1911
4780 T t1912 o1845 b1911
4781 B b1912 t1912
4782 P p1912 Number 7322
4783 P p1913 Number 7387
4784 O o1913 location p1912 p1913
4785 O o1914 str_let p1912 p1913
4786 P p1914 Number 7326
4787 O o1915 patt_var p1914 p1913
4788 O o1916 patt_done p1912 p1913
4789 T t1916 o1916
4790 B b1916 t1916 unique_InvT
4791 T t1917 o1915 b1916
4792 B b1917 t1917
4793 O o1917 fun p1914 p1913
4794 O o1918 patt_if p1914 p1913
4795 P p1918 Number 7338
4796 P p1919 Number 7339
4797 O o1919 patt_var p1918 p1919
4798 O o1920 patt_body p1914 p1913
4799 P p1920 Number 7348
4800 O o1921 apply p1920 p1913
4801 P p1921 Number 7385
4802 O o1922 apply p1920 p1921
4803 P p1922 Number 7358
4804 O o1923 lid p1920 p1922
4805 O o1924 lid p1846
4806 T t1924 o1924
4807 B b1924 t1924
4808 T t1925 o1923 b1924
4809 B b1925 t1925
4810 P p1925 Number 7360
4811 P p1926 Number 7384
4812 O o1926 apply p1925 p1926
4813 P p1927 Number 7382
4814 O o1927 proj p1925 p1927
4815 O o1928 uid p1925 p1927
4816 T t1928 o1928 b837
4817 B b1928 t1928
4818 P p1928 Number 7368
4819 O o1929 lid p1928 p1927
4820 T t1929 o1929 b839
4821 B b1929 t1929
4822 T t1930 o1927 b1928 b1929
4823 B b1930 t1930
4824 P p1930 Number 7383
4825 O o1930 lid p1930 p1926
4826 T t1931 o1930 b842
4827 B b1931 t1931
4828 T t1932 o1926 b1930 b1931
4829 B b1932 t1932
4830 T t1933 o1922 b1925 b1932
4831 B b1933 t1933
4832 P p1933 Number 7386
4833 O o1933 lid p1933 p1913
4834 T t1934 o1933 b842
4835 B b1934 t1934
4836 T t1935 o1921 b1933 b1934
4837 B b1935 t1935
4838 T t1936 o1920 b1935
4839 B b1936 t1936 p
4840 T t1937 o1919 b1936
4841 B b1937 t1937
4842 T t1938 o1918 b1937
4843 B b1938 t1938
4844 T t1939 o1917 b1938
4845 B b1939 t1939
4846 T t1940 o1914 b1917 b1939
4847 B b1940 t1940
4848 T t1941 o b1940 b4
4849 B b1941 t1941
4850 T t1942 o1914 b1941
4851 B b1942 t1942
4852 T t1943 o392 b1942
4853 B b1943 t1943
4854 T t1944 o1913 b1943
4855 B b1944 t1944
4856 P p1944 Number 7439
4857 P p1945 Number 7861
4858 O o1945 location p1944 p1945
4859 P p1946 String unique_sol1
4860 O o1946 rule p1946
4861 P p1947 Var a
4862 O o1947 var p1947
4863 T t1947 o1947
4864 B b1947 t1947
4865 T t1948 o620 b1947
4866 S s1948 t637 h
4867 G s1948 t1948
4868 B b1948 s1948
4869 T t1949 o618 b1948
4870 B b1949 t1949
4871 P p1949 Var b
4872 O o1949 var p1949
4873 T t1950 o1949
4874 B b1950 t1950
4875 T t1951 o620 b1950
4876 S s1951 t637 h
4877 G s1951 t1951
4878 B b1951 s1951
4879 T t1952 o618 b1951
4880 B b1952 t1952
4881 P p1952 Var x
4882 O o1952 var p1952
4883 T t1953 o1952
4884 B b1953 t1953
4885 T t1954 o620 b1953
4886 S s1954 t637 h
4887 G s1954 t1954
4888 B b1954 s1954
4889 T t1955 o618 b1954
4890 B b1955 t1955
4891 T t1956 o655 b1947 b554
4892 S s1956 t620 h
4893 G s1956 t1956
4894 B b1956 s1956
4895 T t1957 o618 b1956
4896 B b1957 t1957
4897 T t1958 o655 b1950 b554
4898 S s1958 t620 h
4899 G s1958 t1958
4900 B b1958 s1958
4901 T t1959 o618 b1958
4902 B b1959 t1959
4903 T t1960 o655 b1953 b554
4904 S s1960 t620 h
4905 G s1960 t1960
4906 B b1960 s1960
4907 T t1961 o618 b1960
4908 B b1961 t1961
4909 T t1962 o559 b1947 b1953
4910 B b1962 t1962
4911 T t1963 o739 b1962 b1950
4912 S s1963 t620 h
4913 G s1963 t1963
4914 B b1963 s1963
4915 T t1964 o618 b1963
4916 B b1964 t1964
4917 T t1965 o572 b1947
4918 B b1965 t1965
4919 T t1966 o559 b1965 b1950
4920 B b1966 t1966
4921 T t1967 o739 b1953 b1966
4922 S s1967 t620 h
4923 G s1967 t1967
4924 B b1967 s1967
4925 T t1968 o618 b1967
4926 B b1968 t1968
4927 T t1969 o635 b1964 b1968
4928 B b1969 t1969
4929 T t1970 o635 b1961 b1969
4930 B b1970 t1970
4931 T t1971 o635 b1959 b1970
4932 B b1971 t1971
4933 T t1972 o635 b1957 b1971
4934 B b1972 t1972
4935 T t1973 o635 b1955 b1972
4936 B b1973 t1973
4937 T t1974 o635 b1952 b1973
4938 B b1974 t1974
4939 T t1975 o635 b1949 b1974
4940 B b1975 t1975
4941 P p1975 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"
4942 O o1975 ext_rule p1975
4943 T t1976 o b1963 b4
4944 B b1976 t1976
4945 T t1977 o b1960 b1976
4946 B b1977 t1977
4947 T t1978 o b1958 b1977
4948 B b1978 t1978
4949 T t1979 o b1956 b1978
4950 B b1979 t1979
4951 T t1980 o b1954 b1979
4952 B b1980 t1980
4953 T t1981 o b1951 b1980
4954 B b1981 t1981
4955 T t1982 o b1948 b1981
4956 B b1982 t1982
4957 T t1983 o939 b1967 b1982
4958 B b1983 t1983
4959 T t1984 o938 b1983 b4 b947
4960 B b1984 t1984
4961 T t1985 o620 b1962
4962 H h1985 y_1 t1985
4963 H h1986 z_1 t1951
4964 T t1986 o676 b1962 b1950
4965 H h1987 z t1986
4966 T t1987 o559 b1965 b1962
4967 B b1987 t1987
4968 T t1988 o739 b1987 b1966
4969 S s1988 t620 h h1985 h1986 h1987
4970 G s1988 t1988
4971 B b1988 s1988
4972 T t1989 o939 b1988 b1982
4973 B b1989 t1989
4974 T t1990 o676 b1953 b1966
4975 S s1990 t620 h h1985 h1986 h1987
4976 G s1990 t1990
4977 B b1990 s1990
4978 T t1991 o939 b1990 b1982
4979 B b1991 t1991
4980 S s1991 t620 h h1985 h1986 h1987
4981 G s1991 t1967
4982 B b1992 s1991
4983 T t1992 o939 b1992 b1982
4984 B b1993 t1992
4985 B b1994 t1985
4986 B b1995 t1951
4987 T t1995 o1271 b1994 b1995
4988 H h1995 y t1995
4989 S s1995 t620 h h1995 h1987
4990 G s1995 t1967
4991 B b1996 s1995
4992 T t1996 o939 b1996 b1982
4993 B b1997 t1996
4994 B b1998 t1995
4995 B b1999 t1986
4996 T t1999 o1271 b1998 b1999
4997 H h1999 v t1999
4998 S s1999 t620 h h1999
4999 G s1999 t1967
5000 B b2000 s1999
5001 T t2000 o939 b2000 b1982
5002 B b2001 t2000
5003 H h2001 v t1963
5004 S s2001 t620 h h2001
5005 G s2001 t1967
5006 B b2002 s2001
5007 T t2002 o939 b2002 b1982
5008 B b2003 t2002
5009 T t2003 o2 b1984
5010 B b2004 t2003
5011 T t2004 o938 b2003 b4 b2004
5012 B b2005 t2004
5013 T t2005 o2 b2005
5014 B b2006 t2005
5015 T t2006 o938 b2001 b4 b2006
5016 B b2007 t2006
5017 T t2007 o2 b2007
5018 B b2008 t2007
5019 T t2008 o938 b1997 b4 b2008
5020 B b2009 t2008
5021 T t2009 o2 b2009
5022 B b2010 t2009
5023 T t2010 o938 b1993 b984 b2010
5024 B b2011 t2010
5025 T t2011 o2 b2011
5026 B b2012 t2011
5027 T t2012 o938 b1991 b4 b2012
5028 B b2013 t2012
5029 T t2013 o2 b2013
5030 B b2014 t2013
5031 T t2014 o948 b1989 b4 b2014
5032 B b2015 t2014
5033 H h2015 v t1988
5034 S s2015 t620 h h1985 h1986 h1987 h2015
5035 G s2015 t1990
5036 B b2016 s2015
5037 T t2016 o939 b2016 b1982
5038 B b2017 t2016
5039 T t2017 o938 b2017 b4 b2014
5040 B b2018 t2017
5041 T t2018 o b2018 b4
5042 B b2019 t2018
5043 T t2019 o b2015 b2019
5044 B b2020 t2019
5045 T t2020 o937 b1984 b2020
5046 B b2021 t2020
5047 T t2021 o937 b2015 b4
5048 B b2022 t2021
5049 T t2022 o991 b936 b2022 b4 b4
5050 B b2023 t2022
5051 P p2023 String "setSubstT << equal{op{inv{'a}; op{'a; 'x}}; op{op{inv{'a}; 'a}; 'x}} >> 5 thenT autoT"
5052 O o2023 ext_rule p2023
5053 T t2023 o559 b1965 b1947
5054 B b2024 t2023
5055 T t2024 o559 b2024 b1953
5056 B b2025 t2024
5057 T t2025 o739 b2025 b1966
5058 H h2025 v_1 t2025
5059 S s2025 t620 h h1985 h1986 h1987 h2015 h2025
5060 G s2025 t1990
5061 B b2026 s2025
5062 T t2026 o939 b2026 b1982
5063 B b2027 t2026
5064 T t2027 o2 b2018
5065 B b2028 t2027
5066 T t2028 o938 b2027 b4 b2028
5067 B b2029 t2028
5068 B b2030 t1966 v_1
5069 T t2030 o712 b2030
5070 S s2030 t620 h h1985 h1986 h1987 h2015
5071 G s2030 t2030
5072 B b2031 s2030
5073 T t2031 o939 b2031 b1982
5074 B b2032 t2031
5075 T t2032 o739 b1221 b1966
5076 B b2033 t2032 v_1
5077 T t2033 o977 b2033
5078 S s2033 t620 h h1985 h1986 h1987 h2015
5079 G s2033 t2033
5080 B b2034 s2033
5081 T t2034 o939 b2034 b1982
5082 B b2035 t2034
5083 T t2035 o974 b2035 b984 b2028
5084 B b2036 t2035
5085 T t2036 o2 b2036
5086 B b2037 t2036
5087 T t2037 o974 b2032 b4 b2037
5088 B b2038 t2037
5089 T t2038 o b2038 b4
5090 B b2039 t2038
5091 T t2039 o b2029 b2039
5092 B b2040 t2039
5093 T t2040 o937 b2018 b2040
5094 B b2041 t2040
5095 P p2041 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"
5096 O o2041 ext_rule p2041
5097 T t2041 o559 b567 b1953
5098 B b2042 t2041
5099 T t2042 o739 b2042 b1966
5100 H h2042 v_2 t2042
5101 S s2042 t620 h h1985 h1986 h1987 h2015 h2025 h2042
5102 G s2042 t1990
5103 B b2043 s2042
5104 T t2043 o939 b2043 b1982
5105 B b2044 t2043
5106 T t2044 o2 b2029
5107 B b2045 t2044
5108 T t2045 o938 b2044 b4 b2045
5109 B b2046 t2045
5110 B b2047 t1966 v_2
5111 T t2047 o712 b2047
5112 S s2047 t620 h h1985 h1986 h1987 h2015 h2025
5113 G s2047 t2047
5114 B b2048 s2047
5115 T t2048 o939 b2048 b1982
5116 B b2049 t2048
5117 T t2049 o559 b978 b1953
5118 B b2050 t2049
5119 T t2050 o739 b2050 b1966
5120 B b2051 t2050 v_2
5121 T t2051 o977 b2051
5122 S s2051 t620 h h1985 h1986 h1987 h2015 h2025
5123 G s2051 t2051
5124 B b2052 s2051
5125 T t2052 o939 b2052 b1982
5126 B b2053 t2052
5127 T t2053 o974 b2053 b984 b2045
5128 B b2054 t2053
5129 T t2054 o2 b2054
5130 B b2055 t2054
5131 T t2055 o974 b2049 b4 b2055
5132 B b2056 t2055
5133 T t2056 o b2056 b4
5134 B b2057 t2056
5135 T t2057 o b2046 b2057
5136 B b2058 t2057
5137 T t2058 o937 b2029 b2058
5138 B b2059 t2058
5139 P p2059 String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"
5140 O o2059 ext_rule p2059
5141 H h2059 v_3 t1967
5142 S s2059 t620 h h1985 h1986 h1987 h2015 h2025 h2042 h2059
5143 G s2059 t1990
5144 B b2060 s2059
5145 T t2060 o939 b2060 b1982
5146 B b2061 t2060
5147 T t2061 o2 b2046
5148 B b2062 t2061
5149 T t2062 o938 b2061 b4 b2062
5150 B b2063 t2062
5151 B b2064 t1966 v_3
5152 T t2064 o712 b2064
5153 S s2064 t620 h h1985 h1986 h1987 h2015 h2025 h2042
5154 G s2064 t2064
5155 B b2065 s2064
5156 T t2065 o939 b2065 b1982
5157 B b2066 t2065
5158 T t2066 o739 b1005 b1966
5159 B b2067 t2066 v_3
5160 T t2067 o977 b2067
5161 S s2067 t620 h h1985 h1986 h1987 h2015 h2025 h2042
5162 G s2067 t2067
5163 B b2068 s2067
5164 T t2068 o939 b2068 b1982
5165 B b2069 t2068
5166 T t2069 o974 b2069 b984 b2062
5167 B b2070 t2069
5168 T t2070 o2 b2070
5169 B b2071 t2070
5170 T t2071 o974 b2066 b4 b2071
5171 B b2072 t2071
5172 T t2072 o b2072 b4
5173 B b2073 t2072
5174 T t2073 o b2063 b2073
5175 B b2074 t2073
5176 T t2074 o937 b2046 b2074
5177 B b2075 t2074
5178 P p2075 String "rwh unfold_equal 8 thenT autoT"
5179 O o2075 ext_rule p2075
5180 T t2075 o937 b2063 b4
5181 B b2076 t2075
5182 T t2076 o2075 b936 b2076 b4 b4
5183 B b2077 t2076
5184 T t2077 o937 b2072 b4
5185 B b2078 t2077
5186 T t2078 o1072 b936 b2078 b4 b4
5187 B b2079 t2078
5188 T t2079 o b2079 b4
5189 B b2080 t2079
5190 T t2080 o b2077 b2080
5191 B b2081 t2080
5192 T t2081 o2059 b936 b2075 b2081 b4
5193 B b2082 t2081
5194 T t2082 o937 b2056 b4
5195 B b2083 t2082
5196 T t2083 o1072 b936 b2083 b4 b4
5197 B b2084 t2083
5198 T t2084 o b2084 b4
5199 B b2085 t2084
5200 T t2085 o b2082 b2085
5201 B b2086 t2085
5202 T t2086 o2041 b936 b2059 b2086 b4
5203 B b2087 t2086
5204 T t2087 o937 b2038 b4
5205 B b2088 t2087
5206 T t2088 o1072 b936 b2088 b4 b4
5207 B b2089 t2088
5208 T t2089 o b2089 b4
5209 B b2090 t2089
5210 T t2090 o b2087 b2090
5211 B b2091 t2090
5212 T t2091 o739 b1987 b2025
5213 S s2091 t620 h h1985 h1986 h1987 h2015
5214 G s2091 t2091
5215 B b2092 s2091
5216 T t2092 o939 b2092 b1982
5217 B b2093 t2092
5218 T t2093 o967 b2093 b4 b2028
5219 B b2094 t2093
5220 T t2094 o937 b2094 b4
5221 B b2095 t2094
5222 T t2095 o991 b936 b2095 b4 b4
5223 B b2096 t2095
5224 P p2096 String "rwh unfold_fun_prop 0 thenT autoT thenT rwh unfold_equal 9 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 11 thenT autoT"
5225 O o2096 ext_rule p2096
5226 T t2096 o974 b2035 b4 b2028
5227 B b2097 t2096
5228 H h2097 x_1 t1345
5229 H h2098 y_2 t638
5230 T t2098 o620 b1966
5231 H h2099 z_3 t2098
5232 T t2099 o676 b560 b1966
5233 H h2100 z_2 t2099
5234 S s2100 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097 h2098 h2099 h2100
5235 G s2100 t2030
5236 B b2100 s2100
5237 T t2100 o939 b2100 b1982
5238 B b2101 t2100
5239 T t2101 o676 b1221 b1966
5240 B b2102 t2101 v_1
5241 T t2102 o977 b2102
5242 S s2102 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097 h2098 h2099 h2100
5243 G s2102 t2102
5244 B b2103 s2102
5245 T t2103 o939 b2103 b1982
5246 B b2104 t2103
5247 T t2104 o676 b561 b1966
5248 S s2104 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097 h2098 h2099 h2100
5249 G s2104 t2104
5250 B b2105 s2104
5251 T t2105 o939 b2105 b1982
5252 B b2106 t2105
5253 B b2107 t638
5254 B b2108 t2098
5255 T t2108 o1271 b2107 b2108
5256 H h2108 y t2108
5257 S s2108 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097 h2108 h2100
5258 G s2108 t2104
5259 B b2109 s2108
5260 T t2109 o939 b2109 b1982
5261 B b2110 t2109
5262 B b2111 t2108
5263 B b2112 t2099
5264 T t2112 o1271 b2111 b2112
5265 H h2112 x_2 t2112
5266 S s2112 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097 h2112
5267 G s2112 t2104
5268 B b2113 s2112
5269 T t2113 o939 b2113 b1982
5270 B b2114 t2113
5271 T t2114 o739 b560 b1966
5272 H h2114 x_2 t2114
5273 S s2114 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097 h2114
5274 G s2114 t2104
5275 B b2115 s2114
5276 T t2115 o939 b2115 b1982
5277 B b2116 t2115
5278 T t2116 o739 b561 b1966
5279 S s2116 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097 h2114
5280 G s2116 t2116
5281 B b2117 s2116
5282 T t2117 o939 b2117 b1982
5283 B b2118 t2117
5284 B b2119 t2114
5285 B b2120 t2116
5286 T t2120 o1178 b2119 b2120
5287 S s2120 t620 h h1985 h1986 h1987 h2015 h1345 h1225 h2097
5288 G s2120 t2120
5289 B b2121 s2120
5290 T t2121 o939 b2121 b1982
5291 B b2122 t2121
5292 B b2123 t2120
5293 T t2123 o1178 b1348 b2123
5294 S s2123 t620 h h1985 h1986 h1987 h2015 h1345 h1225
5295 G s2123 t2123
5296 B b2124 s2123
5297 T t2124 o939 b2124 b1982
5298 B b2125 t2124
5299 B b2126 t2123 s2
5300 T t2126 o1186 b1187 b2126
5301 S s2126 t620 h h1985 h1986 h1987 h2015 h1345
5302 G s2126 t2126
5303 B b2127 s2126
5304 T t2127 o939 b2127 b1982
5305 B b2128 t2127
5306 B b2129 t2126 s1
5307 T t2129 o1186 b1187 b2129
5308 S s2129 t620 h h1985 h1986 h1987 h2015
5309 G s2129 t2129
5310 B b2130 s2129
5311 T t2130 o939 b2130 b1982
5312 B b2131 t2130
5313 T t2131 o2 b2097
5314 B b2132 t2131
5315 T t2132 o974 b2131 b984 b2132
5316 B b2133 t2132
5317 T t2133 o2 b2133
5318 B b2134 t2133
5319 T t2134 o938 b2128 b984 b2134
5320 B b2135 t2134
5321 T t2135 o2 b2135
5322 B b2136 t2135
5323 T t2136 o938 b2125 b984 b2136
5324 B b2137 t2136
5325 T t2137 o2 b2137
5326 B b2138 t2137
5327 T t2138 o938 b2122 b984 b2138
5328 B b2139 t2138
5329 T t2139 o2 b2139
5330 B b2140 t2139
5331 T t2140 o938 b2118 b984 b2140
5332 B b2141 t2140
5333 T t2141 o2 b2141
5334 B b2142 t2141
5335 T t2142 o938 b2116 b4 b2142
5336 B b2143 t2142
5337 T t2143 o2 b2143
5338 B b2144 t2143
5339 T t2144 o938 b2114 b4 b2144
5340 B b2145 t2144
5341 T t2145 o2 b2145
5342 B b2146 t2145
5343 T t2146 o938 b2110 b4 b2146
5344 B b2147 t2146
5345 T t2147 o2 b2147
5346 B b2148 t2147
5347 T t2148 o938 b2106 b4 b2148
5348 B b2149 t2148
5349 T t2149 o2 b2149
5350 B b2150 t2149
5351 T t2150 o974 b2104 b984 b2150
5352 B b2151 t2150
5353 T t2151 o2 b2151
5354 B b2152 t2151
5355 T t2152 o974 b2101 b4 b2152
5356 B b2153 t2152
5357 T t2153 o b2153 b4
5358 B b2154 t2153
5359 T t2154 o937 b2097 b2154
5360 B b2155 t2154
5361 T t2155 o937 b2153 b4
5362 B b2156 t2155
5363 T t2156 o1072 b936 b2156 b4 b4
5364 B b2157 t2156
5365 T t2157 o b2157 b4
5366 B b2158 t2157
5367 T t2158 o2096 b936 b2155 b2158 b4
5368 B b2159 t2158
5369 T t2159 o b2159 b4
5370 B b2160 t2159
5371 T t2160 o b2096 b2160
5372 B b2161 t2160
5373 T t2161 o2023 b936 b2041 b2091 b2161
5374 B b2162 t2161
5375 T t2162 o b2162 b4
5376 B b2163 t2162
5377 T t2163 o b2023 b2163
5378 B b2164 t2163
5379 T t2164 o1975 b936 b2021 b2164 b4
5380 B b2165 t2164
5381 T t2165 o934 b2165
5382 B b2166 t2165
5383 P p2166 Number 7466
5384 P p2167 Number 7474
5385 O o2167 resource_defs p2166 p2167 p264
5386 P p2168 Number 7472
5387 O o2168 uid p2168 p2167
5388 T t2168 o2168 b626
5389 B b2168 t2168
5390 T t2169 o b2168 b4
5391 B b2169 t2169
5392 T t2170 o2167 b2169
5393 B b2170 t2170
5394 T t2171 o b2170 b4
5395 B b2171 t2171
5396 T t2172 o1946 b618 b1975 b2166 b2171
5397 B b2172 t2172
5398 T t2173 o1945 b2172
5399 B b2173 t2173
5400 P p2173 Number 7912
5401 P p2174 Number 8334
5402 O o2174 location p2173 p2174
5403 P p2175 String unique_sol2
5404 O o2175 rule p2175
5405 P p2176 Var y
5406 O o2176 var p2176
5407 T t2176 o2176
5408 B b2176 t2176
5409 T t2177 o620 b2176
5410 S s2177 t637 h
5411 G s2177 t2177
5412 B b2177 s2177
5413 T t2178 o618 b2177
5414 B b2178 t2178
5415 T t2179 o655 b2176 b554
5416 S s2179 t620 h
5417 G s2179 t2179
5418 B b2179 s2179
5419 T t2180 o618 b2179
5420 B b2180 t2180
5421 T t2181 o559 b2176 b1947
5422 B b2181 t2181
5423 T t2182 o739 b2181 b1950
5424 S s2182 t620 h
5425 G s2182 t2182
5426 B b2182 s2182
5427 T t2183 o618 b2182
5428 B b2183 t2183
5429 T t2184 o559 b1950 b1965
5430 B b2184 t2184
5431 T t2185 o739 b2176 b2184
5432 S s2185 t620 h
5433 G s2185 t2185
5434 B b2185 s2185
5435 T t2186 o618 b2185
5436 B b2186 t2186
5437 T t2187 o635 b2183 b2186
5438 B b2187 t2187
5439 T t2188 o635 b2180 b2187
5440 B b2188 t2188
5441 T t2189 o635 b1959 b2188
5442 B b2189 t2189
5443 T t2190 o635 b1957 b2189
5444 B b2190 t2190
5445 T t2191 o635 b2178 b2190
5446 B b2191 t2191
5447 T t2192 o635 b1952 b2191
5448 B b2192 t2192
5449 T t2193 o635 b1949 b2192
5450 B b2193 t2193
5451 P p2193 String "assumT 7 thenT assertT << equal{op{op{'y; 'a}; inv{'a}}; op{'b; inv{'a}}} >> thenT autoT"
5452 O o2193 ext_rule p2193
5453 T t2194 o b2182 b4
5454 B b2194 t2194
5455 T t2195 o b2179 b2194
5456 B b2195 t2195
5457 T t2196 o b1958 b2195
5458 B b2196 t2196
5459 T t2197 o b1956 b2196
5460 B b2197 t2197
5461 T t2198 o b2177 b2197
5462 B b2198 t2198
5463 T t2199 o b1951 b2198
5464 B b2199 t2199
5465 T t2200 o b1948 b2199
5466 B b2200 t2200
5467 T t2201 o939 b2185 b2200
5468 B b2201 t2201
5469 T t2202 o938 b2201 b4 b947
5470 B b2202 t2202
5471 H h2202 v t2182
5472 T t2203 o676 b2181 b1950
5473 S s2203 t620 h h2202
5474 G s2203 t2203
5475 B b2203 s2203
5476 T t2204 o939 b2203 b2200
5477 B b2204 t2204
5478 T t2205 o559 b2181 b1965
5479 B b2205 t2205
5480 T t2206 o676 b2205 b2184
5481 S s2206 t620 h h2202
5482 G s2206 t2206
5483 B b2206 s2206
5484 T t2207 o939 b2206 b2200
5485 B b2207 t2207
5486 T t2208 o739 b2205 b2184
5487 S s2208 t620 h h2202
5488 G s2208 t2208
5489 B b2208 s2208
5490 T t2209 o939 b2208 b2200
5491 B b2209 t2209
5492 S s2209 t620 h h2202
5493 G s2209 t2185
5494 B b2210 s2209
5495 T t2210 o939 b2210 b2200
5496 B b2211 t2210
5497 T t2211 o2 b2202
5498 B b2212 t2211
5499 T t2212 o938 b2211 b4 b2212
5500 B b2213 t2212
5501 T t2213 o2 b2213
5502 B b2214 t2213
5503 T t2214 o948 b2209 b984 b2214
5504 B b2215 t2214
5505 T t2215 o2 b2215
5506 B b2216 t2215
5507 T t2216 o948 b2207 b984 b2216
5508 B b2217 t2216
5509 T t2217 o2 b2217
5510 B b2218 t2217
5511 T t2218 o948 b2204 b4 b2218
5512 B b2219 t2218
5513 H h2219 v_1 t2208
5514 T t2219 o676 b2176 b2184
5515 S s2219 t620 h h2202 h2219
5516 G s2219 t2219
5517 B b2220 s2219
5518 T t2220 o939 b2220 b2200
5519 B b2221 t2220
5520 S s2221 t620 h h2202 h2219
5521 G s2221 t2185
5522 B b2222 s2221
5523 T t2222 o939 b2222 b2200
5524 B b2223 t2222
5525 T t2223 o938 b2223 b984 b2214
5526 B b2224 t2223
5527 T t2224 o2 b2224
5528 B b2225 t2224
5529 T t2225 o938 b2221 b4 b2225
5530 B b2226 t2225
5531 T t2226 o b2226 b4
5532 B b2227 t2226
5533 T t2227 o b2219 b2227
5534 B b2228 t2227
5535 T t2228 o937 b2202 b2228
5536 B b2229 t2228
5537 P p2229 String "rwh unfold_equal 2 thenT autoT"
5538 O o2229 ext_rule p2229
5539 T t2229 o937 b2219 b4
5540 B b2230 t2229
5541 T t2230 o2229 b936 b2230 b4 b4
5542 B b2231 t2230
5543 P p2231 String "setSubstT << equal{op{op{'y; 'a}; inv{'a}}; op{'y; op{'a; inv{'a}}}} >> 3 thenT autoT"
5544 O o2231 ext_rule p2231
5545 T t2231 o559 b1947 b1965
5546 B b2232 t2231
5547 T t2232 o559 b2176 b2232
5548 B b2233 t2232
5549 T t2233 o739 b2233 b2184
5550 H h2233 v_2 t2233
5551 S s2233 t620 h h2202 h2219 h2233
5552 G s2233 t2219
5553 B b2234 s2233
5554 T t2234 o939 b2234 b2200
5555 B b2235 t2234
5556 T t2235 o2 b2226
5557 B b2236 t2235
5558 T t2236 o938 b2235 b4 b2236
5559 B b2237 t2236
5560 B b2238 t2184 v_2
5561 T t2238 o712 b2238
5562 S s2238 t620 h h2202 h2219
5563 G s2238 t2238
5564 B b2239 s2238
5565 T t2239 o939 b2239 b2200
5566 B b2240 t2239
5567 T t2240 o739 b978 b2184
5568 B b2241 t2240 v_2
5569 T t2241 o977 b2241
5570 S s2241 t620 h h2202 h2219
5571 G s2241 t2241
5572 B b2242 s2241
5573 T t2242 o939 b2242 b2200
5574 B b2243 t2242
5575 T t2243 o974 b2243 b984 b2236
5576 B b2244 t2243
5577 T t2244 o2 b2244
5578 B b2245 t2244
5579 T t2245 o974 b2240 b4 b2245
5580 B b2246 t2245
5581 T t2246 o b2246 b4
5582 B b2247 t2246
5583 T t2247 o b2237 b2247
5584 B b2248 t2247
5585 T t2248 o937 b2226 b2248
5586 B b2249 t2248
5587 P p2249 String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"
5588 O o2249 ext_rule p2249
5589 T t2249 o559 b2176 b567
5590 B b2250 t2249
5591 T t2250 o739 b2250 b2184
5592 H h2250 v_3 t2250
5593 S s2250 t620 h h2202 h2219 h2233 h2250
5594 G s2250 t2219
5595 B b2251 s2250
5596 T t2251 o939 b2251 b2200
5597 B b2252 t2251
5598 T t2252 o2 b2237
5599 B b2253 t2252
5600 T t2253 o938 b2252 b4 b2253
5601 B b2254 t2253
5602 B b2255 t2184 v_3
5603 T t2255 o712 b2255
5604 S s2255 t620 h h2202 h2219 h2233
5605 G s2255 t2255
5606 B b2256 s2255
5607 T t2256 o939 b2256 b2200
5608 B b2257 t2256
5609 T t2257 o559 b2176 b1005
5610 B b2258 t2257
5611 T t2258 o739 b2258 b2184
5612 B b2259 t2258 v_3
5613 T t2259 o977 b2259
5614 S s2259 t620 h h2202 h2219 h2233
5615 G s2259 t2259
5616 B b2260 s2259
5617 T t2260 o939 b2260 b2200
5618 B b2261 t2260
5619 T t2261 o974 b2261 b984 b2253
5620 B b2262 t2261
5621 T t2262 o2 b2262
5622 B b2263 t2262
5623 T t2263 o974 b2257 b4 b2263
5624 B b2264 t2263
5625 T t2264 o b2264 b4
5626 B b2265 t2264
5627 T t2265 o b2254 b2265
5628 B b2266 t2265
5629 T t2266 o937 b2237 b2266
5630 B b2267 t2266
5631 P p2267 String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"
5632 O o2267 ext_rule p2267
5633 T t2267 o620 b2250
5634 H h2267 y_2 t2267
5635 T t2268 o620 b2184
5636 H h2268 z_1 t2268
5637 T t2269 o676 b2250 b2184
5638 H h2269 z t2269
5639 S s2269 t620 h h2202 h2219 h2233 h2267 h2268 h2269
5640 G s2269 t2255
5641 B b2269 s2269
5642 T t2270 o939 b2269 b2200
5643 B b2270 t2270
5644 T t2271 o676 b1005 b2184
5645 B b2271 t2271 v_3
5646 T t2272 o977 b2271
5647 S s2272 t620 h h2202 h2219 h2233 h2267 h2268 h2269
5648 G s2272 t2272
5649 B b2272 s2272
5650 T t2273 o939 b2272 b2200
5651 B b2273 t2273
5652 S s2273 t620 h h2202 h2219 h2233 h2267 h2268 h2269
5653 G s2273 t2219
5654 B b2274 s2273
5655 T t2274 o939 b2274 b2200
5656 B b2275 t2274
5657 B b2276 t2267
5658 B b2277 t2268
5659 T t2277 o1271 b2276 b2277
5660 H h2277 y_1 t2277
5661 S s2277 t620 h h2202 h2219 h2233 h2277 h2269
5662 G s2277 t2219
5663 B b2278 s2277
5664 T t2278 o939 b2278 b2200
5665 B b2279 t2278
5666 B b2280 t2277
5667 B b2281 t2269
5668 T t2281 o1271 b2280 b2281
5669 H h2281 v_3 t2281
5670 S s2281 t620 h h2202 h2219 h2233 h2281
5671 G s2281 t2219
5672 B b2282 s2281
5673 T t2282 o939 b2282 b2200
5674 B b2283 t2282
5675 T t2283 o2 b2254
5676 B b2284 t2283
5677 T t2284 o938 b2283 b4 b2284
5678 B b2285 t2284
5679 T t2285 o2 b2285
5680 B b2286 t2285
5681 T t2286 o938 b2279 b4 b2286
5682 B b2287 t2286
5683 T t2287 o2 b2287
5684 B b2288 t2287
5685 T t2288 o938 b2275 b4 b2288
5686 B b2289 t2288
5687 T t2289 o2 b2289
5688 B b2290 t2289
5689 T t2290 o974 b2273 b984 b2290
5690 B b2291 t2290
5691 T t2291 o2 b2291
5692 B b2292 t2291
5693 T t2292 o974 b2270 b4 b2292
5694 B b2293 t2292
5695 T t2293 o b2293 b4
5696 B b2294 t2293
5697 T t2294 o937 b2254 b2294
5698 B b2295 t2294
5699 T t2295 o937 b2293 b4
5700 B b2296 t2295
5701 T t2296 o1072 b936 b2296 b4 b4
5702 B b2297 t2296
5703 T t2297 o b2297 b4
5704 B b2298 t2297
5705 T t2298 o2267 b936 b2295 b2298 b4
5706 B b2299 t2298
5707 T t2299 o937 b2264 b4
5708 B b2300 t2299
5709 T t2300 o1072 b936 b2300 b4 b4
5710 B b2301 t2300
5711 T t2301 o b2301 b4
5712 B b2302 t2301
5713 T t2302 o b2299 b2302
5714 B b2303 t2302
5715 T t2303 o2249 b936 b2267 b2303 b4
5716 B b2304 t2303
5717 T t2304 o937 b2246 b4
5718 B b2305 t2304
5719 T t2305 o1072 b936 b2305 b4 b4
5720 B b2306 t2305
5721 T t2306 o b2306 b4
5722 B b2307 t2306
5723 T t2307 o b2304 b2307
5724 B b2308 t2307
5725 T t2308 o2231 b936 b2249 b2308 b4
5726 B b2309 t2308
5727 T t2309 o b2309 b4
5728 B b2310 t2309
5729 T t2310 o b2231 b2310
5730 B b2311 t2310
5731 T t2311 o2193 b936 b2229 b2311 b4
5732 B b2312 t2311
5733 T t2312 o934 b2312
5734 B b2313 t2312
5735 P p2313 Number 7939
5736 P p2314 Number 7947
5737 O o2314 resource_defs p2313 p2314 p264
5738 P p2315 Number 7945
5739 O o2315 uid p2315 p2314
5740 T t2315 o2315 b626
5741 B b2315 t2315
5742 T t2316 o b2315 b4
5743 B b2316 t2316
5744 T t2317 o2314 b2316
5745 B b2317 t2317
5746 T t2318 o b2317 b4
5747 B b2318 t2318
5748 T t2319 o2175 b618 b2193 b2313 b2318
5749 B b2319 t2319
5750 T t2320 o2174 b2319
5751 B b2320 t2320
5752 P p2320 Number 8336
5753 P p2321 Number 8634
5754 O o2321 location p2320 p2321
5755 P p2322 String inv_simplify
5756 O o2322 rule p2322
5757 T t2322 o559 b1947 b1950
5758 B b2322 t2322
5759 T t2323 o572 b2322
5760 B b2323 t2323
5761 T t2324 o572 b1950
5762 B b2324 t2324
5763 T t2325 o559 b2324 b1965
5764 B b2325 t2325
5765 T t2326 o739 b2323 b2325
5766 S s2326 t620 h
5767 G s2326 t2326
5768 B b2326 s2326
5769 T t2327 o618 b2326
5770 B b2327 t2327
5771 T t2328 o635 b1959 b2327
5772 B b2328 t2328
5773 T t2329 o635 b1957 b2328
5774 B b2329 t2329
5775 T t2330 o635 b1952 b2329
5776 B b2330 t2330
5777 T t2331 o635 b1949 b2330
5778 B b2331 t2331
5779 P p2331 String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >> thenAT autoT"
5780 O o2331 ext_rule p2331
5781 T t2332 o b1958 b4
5782 B b2332 t2332
5783 T t2333 o b1956 b2332
5784 B b2333 t2333
5785 T t2334 o b1951 b2333
5786 B b2334 t2334
5787 T t2335 o b1948 b2334
5788 B b2335 t2335
5789 T t2336 o939 b2326 b2335
5790 B b2336 t2336
5791 T t2337 o938 b2336 b4 b947
5792 B b2337 t2337
5793 T t2338 o559 b2323 b2322
5794 B b2338 t2338
5795 T t2339 o559 b2325 b2322
5796 B b2339 t2339
5797 T t2340 o739 b2338 b2339
5798 S s2340 t620 h
5799 G s2340 t2340
5800 B b2340 s2340
5801 T t2341 o939 b2340 b2335
5802 B b2341 t2341
5803 T t2342 o2 b2337
5804 B b2342 t2342
5805 T t2343 o948 b2341 b4 b2342
5806 B b2343 t2343
5807 H h2343 v t2340
5808 S s2343 t620 h h2343
5809 G s2343 t2326
5810 B b2344 s2343
5811 T t2344 o939 b2344 b2335
5812 B b2345 t2344
5813 T t2345 o938 b2345 b4 b2342
5814 B b2346 t2345
5815 T t2346 o b2346 b4
5816 B b2347 t2346
5817 T t2347 o b2343 b2347
5818 B b2348 t2347
5819 T t2348 o937 b2337 b2348
5820 B b2349 t2348
5821 P p2349 String "setSubstT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; id} >> 0 thenWT autoT"
5822 O o2349 ext_rule p2349
5823 T t2349 o739 b2338 b567
5824 S s2349 t620 h
5825 G s2349 t2349
5826 B b2350 s2349
5827 T t2350 o939 b2350 b2335
5828 B b2351 t2350
5829 T t2351 o2 b2343
5830 B b2352 t2351
5831 T t2352 o967 b2351 b4 b2352
5832 B b2353 t2352
5833 T t2353 o739 b567 b2339
5834 S s2353 t620 h
5835 G s2353 t2353
5836 B b2354 s2353
5837 T t2354 o939 b2354 b2335
5838 B b2355 t2354
5839 T t2355 o938 b2355 b4 b2352
5840 B b2356 t2355
5841 B b2357 t2339 v
5842 T t2357 o712 b2357
5843 S s2357 t620 h
5844 G s2357 t2357
5845 B b2358 s2357
5846 T t2358 o939 b2358 b2335
5847 B b2359 t2358
5848 P p2359 Var v
5849 O o2359 var p2359
5850 T t2359 o2359
5851 B b2360 t2359
5852 T t2360 o739 b2360 b2339
5853 B b2361 t2360 v
5854 T t2361 o977 b2361
5855 S s2361 t620 h
5856 G s2361 t2361
5857 B b2362 s2361
5858 T t2362 o939 b2362 b2335
5859 B b2363 t2362
5860 T t2363 o974 b2363 b984 b2352
5861 B b2364 t2363
5862 T t2364 o2 b2364
5863 B b2365 t2364
5864 T t2365 o974 b2359 b4 b2365
5865 B b2366 t2365
5866 T t2366 o b2366 b4
5867 B b2367 t2366
5868 T t2367 o b2356 b2367
5869 B b2368 t2367
5870 T t2368 o b2353 b2368
5871 B b2369 t2368
5872 T t2369 o937 b2343 b2369
5873 B b2370 t2369
5874 T t2370 o937 b2353 b4
5875 B b2371 t2370
5876 T t2371 o991 b936 b2371 b4 b4
5877 B b2372 t2371
5878 P p2372 String "setSubstT << equal{id; op{inv{'b}; op{inv{'a}; op{'a; 'b}}}} >> 0 thenWT autoT"
5879 O o2372 ext_rule p2372
5880 T t2372 o559 b1965 b2322
5881 B b2373 t2372
5882 T t2373 o559 b2324 b2373
5883 B b2374 t2373
5884 T t2374 o739 b567 b2374
5885 S s2374 t620 h
5886 G s2374 t2374
5887 B b2375 s2374
5888 T t2375 o939 b2375 b2335
5889 B b2376 t2375
5890 T t2376 o2 b2356
5891 B b2377 t2376
5892 T t2377 o967 b2376 b4 b2377
5893 B b2378 t2377
5894 T t2378 o739 b2374 b2339
5895 S s2378 t620 h
5896 G s2378 t2378
5897 B b2379 s2378
5898 T t2379 o939 b2379 b2335
5899 B b2380 t2379
5900 T t2380 o938 b2380 b4 b2377
5901 B b2381 t2380
5902 T t2381 o974 b2363 b984 b2377
5903 B b2382 t2381
5904 T t2382 o2 b2382
5905 B b2383 t2382
5906 T t2383 o974 b2359 b4 b2383
5907 B b2384 t2383
5908 T t2384 o b2384 b4
5909 B b2385 t2384
5910 T t2385 o b2381 b2385
5911 B b2386 t2385
5912 T t2386 o b2378 b2386
5913 B b2387 t2386
5914 T t2387 o937 b2356 b2387
5915 B b2388 t2387
5916 P p2388 String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"
5917 O o2388 ext_rule p2388
5918 T t2388 o559 b2024 b1950
5919 B b2389 t2388
5920 T t2389 o739 b2373 b2389
5921 S s2389 t620 h
5922 G s2389 t2389
5923 B b2390 s2389
5924 T t2390 o939 b2390 b2335
5925 B b2391 t2390
5926 T t2391 o2 b2378
5927 B b2392 t2391
5928 T t2392 o967 b2391 b4 b2392
5929 B b2393 t2392
5930 T t2393 o559 b2324 b2389
5931 B b2394 t2393
5932 T t2394 o739 b567 b2394
5933 S s2394 t620 h
5934 G s2394 t2394
5935 B b2395 s2394
5936 T t2395 o939 b2395 b2335
5937 B b2396 t2395
5938 T t2396 o938 b2396 b4 b2392
5939 B b2397 t2396
5940 T t2397 o b2397 b4
5941 B b2398 t2397
5942 T t2398 o b2393 b2398
5943 B b2399 t2398
5944 T t2399 o937 b2378 b2399
5945 B b2400 t2399
5946 T t2400 o937 b2393 b4
5947 B b2401 t2400
5948 T t2401 o991 b936 b2401 b4 b4
5949 B b2402 t2401
5950 P p2402 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 0 thenWT autoT"
5951 O o2402 ext_rule p2402
5952 T t2402 o739 b2024 b567
5953 S s2402 t620 h
5954 G s2402 t2402
5955 B b2403 s2402
5956 T t2403 o939 b2403 b2335
5957 B b2404 t2403
5958 T t2404 o2 b2397
5959 B b2405 t2404
5960 T t2405 o967 b2404 b4 b2405
5961 B b2406 t2405
5962 T t2406 o559 b567 b1950
5963 B b2407 t2406
5964 T t2407 o559 b2324 b2407
5965 B b2408 t2407
5966 T t2408 o739 b567 b2408
5967 S s2408 t620 h
5968 G s2408 t2408
5969 B b2409 s2408
5970 T t2409 o939 b2409 b2335
5971 B b2410 t2409
5972 T t2410 o938 b2410 b4 b2405
5973 B b2411 t2410
5974 T t2411 o559 b2360 b1950
5975 B b2412 t2411
5976 T t2412 o559 b2324 b2412
5977 B b2413 t2412 v
5978 T t2413 o712 b2413
5979 S s2413 t620 h
5980 G s2413 t2413
5981 B b2414 s2413
5982 T t2414 o939 b2414 b2335
5983 B b2415 t2414
5984 B b2416 t2412
5985 T t2416 o739 b567 b2416
5986 B b2417 t2416 v
5987 T t2417 o977 b2417
5988 S s2417 t620 h
5989 G s2417 t2417
5990 B b2418 s2417
5991 T t2418 o939 b2418 b2335
5992 B b2419 t2418
5993 T t2419 o974 b2419 b984 b2405
5994 B b2420 t2419
5995 T t2420 o2 b2420
5996 B b2421 t2420
5997 T t2421 o974 b2415 b4 b2421
5998 B b2422 t2421
5999 T t2422 o b2422 b4
6000 B b2423 t2422
6001 T t2423 o b2411 b2423
6002 B b2424 t2423
6003 T t2424 o b2406 b2424
6004 B b2425 t2424
6005 T t2425 o937 b2397 b2425
6006 B b2426 t2425
6007 T t2426 o937 b2406 b4
6008 B b2427 t2426
6009 T t2427 o991 b936 b2427 b4 b4
6010 B b2428 t2427
6011 P p2428 String "setSubstT << equal{op{id; 'b}; 'b} >> 0 thenWT autoT"
6012 O o2428 ext_rule p2428
6013 T t2428 o739 b2407 b1950
6014 S s2428 t620 h
6015 G s2428 t2428
6016 B b2429 s2428
6017 T t2429 o939 b2429 b2335
6018 B b2430 t2429
6019 T t2430 o2 b2411
6020 B b2431 t2430
6021 T t2431 o967 b2430 b4 b2431
6022 B b2432 t2431
6023 T t2432 o559 b2324 b1950
6024 B b2433 t2432
6025 T t2433 o739 b567 b2433
6026 S s2433 t620 h
6027 G s2433 t2433
6028 B b2434 s2433
6029 T t2434 o939 b2434 b2335
6030 B b2435 t2434
6031 T t2435 o938 b2435 b4 b2431
6032 B b2436 t2435
6033 T t2436 o b2436 b4
6034 B b2437 t2436
6035 T t2437 o b2432 b2437
6036 B b2438 t2437
6037 T t2438 o937 b2411 b2438
6038 B b2439 t2438
6039 T t2439 o937 b2432 b4
6040 B b2440 t2439
6041 T t2440 o991 b936 b2440 b4 b4
6042 B b2441 t2440
6043 P p2441 String "setSubstT << equal{op{inv{'b}; 'b}; id} >> 0 thenT autoT"
6044 O o2441 ext_rule p2441
6045 T t2441 o937 b2436 b4
6046 B b2442 t2441
6047 T t2442 o2441 b936 b2442 b4 b4
6048 B b2443 t2442
6049 T t2443 o b2443 b4
6050 B b2444 t2443
6051 T t2444 o b2441 b2444
6052 B b2445 t2444
6053 T t2445 o2428 b936 b2439 b2445 b4
6054 B b2446 t2445
6055 P p2446 String "rwh unfold_fun_set 0 thenT dT 0"
6056 O o2446 ext_rule p2446
6057 NItt_equal Itt_equal Itt_equal NIL
6058 NItt_equal!type type type Itt_equal
6059 O o2447 type
6060 T t2447 o2447 b1187
6061 S s2447 t637 h
6062 G s2447 t2447
6063 B b2447 s2447
6064 T t2448 o939 b2447 b2335
6065 B b2448 t2448
6066 T t2449 o559 b560 b1950
6067 B b2449 t2449
6068 T t2450 o559 b2324 b2449
6069 B b2450 t2450
6070 T t2451 o559 b561 b1950
6071 B b2451 t2451
6072 T t2452 o559 b2324 b2451
6073 B b2452 t2452
6074 T t2453 o739 b2450 b2452
6075 B b2453 t2453
6076 T t2454 o1178 b1348 b2453
6077 B b2454 t2454 s2
6078 T t2455 o1186 b1187 b2454
6079 B b2455 t2455 s1
6080 T t2456 o1186 b1187 b2455
6081 S s2456 t620 h
6082 G s2456 t2456
6083 B b2456 s2456
6084 T t2457 o939 b2456 b2335
6085 B b2457 t2457
6086 T t2458 o2 b2422
6087 B b2458 t2458
6088 T t2459 o974 b2457 b4 b2458
6089 B b2459 t2459
6090 T t2460 o2 b2459
6091 B b2460 t2460
6092 T t2461 o974 b2448 b4 b2460
6093 B b2461 t2461
6094 S s2461 t620 h h1345
6095 G s2461 t2455
6096 B b2462 s2461
6097 T t2462 o939 b2462 b2335
6098 B b2463 t2462
6099 T t2463 o938 b2463 b4 b2460
6100 B b2464 t2463
6101 T t2464 o b2464 b4
6102 B b2465 t2464
6103 T