/[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 3405 - (show annotations) (download)
Sun Sep 23 07:33:50 2001 UTC (19 years, 10 months ago) by xiny
File size: 122083 byte(s)
recommit .prla files

1 #PRL version 1.0.0 ASCII term
2 NPerv Perv Perv NIL
3 NPerv!cons cons cons Perv
4 O o cons
5 NSummary Summary Summary NIL
6 NSummary!location location location Summary
7 P p Number 0
8 P p1 Number 19
9 O o1 location p p1
10 NSummary!parent parent parent Summary
11 O o2 parent
12 P p2 String Czf_itt_set
13 O o3 parent p2
14 T t o3
15 B b t
16 NPerv!nil nil3 nil Perv
17 O o4 nil3
18 T t4 o4
19 B b4 t4
20 T t5 o b b4
21 B b5 t5
22 P p5 String Czf_itt_comment
23 O o5 parent p5
24 T t6 o5
25 B b6 t6
26 T t7 o b6 b4
27 B b7 t7
28 P p7 String Itt_theory
29 O o7 parent p7
30 T t8 o7
31 B b8 t8
32 T t9 o b8 b4
33 B b9 t9
34 P p9 String Itt_fset
35 O o9 parent p9
36 T t10 o9
37 B b10 t10
38 T t11 o b10 b4
39 B b11 t11
40 P p11 String Itt_prop_decide
41 O o11 parent p11
42 T t12 o11
43 B b12 t12
44 T t13 o b12 b4
45 B b13 t13
46 P p13 String Itt_derive
47 O o13 parent p13
48 T t14 o13
49 B b14 t14
50 T t15 o b14 b4
51 B b15 t15
52 P p15 String Itt_list2
53 O o15 parent p15
54 T t16 o15
55 B b16 t16
56 T t17 o b16 b4
57 B b17 t17
58 P p17 String Itt_list
59 O o17 parent p17
60 T t18 o17
61 B b18 t18
62 T t19 o b18 b4
63 B b19 t19
64 P p19 String Itt_quotient
65 O o19 parent p19
66 T t20 o19
67 B b20 t20
68 T t21 o b20 b4
69 B b21 t21
70 P p21 String Itt_esquash
71 O o21 parent p21
72 T t22 o21
73 B b22 t22
74 T t23 o b22 b4
75 B b23 t23
76 P p23 String Itt_srec
77 O o23 parent p23
78 T t24 o23
79 B b24 t24
80 T t25 o b24 b4
81 B b25 t25
82 P p25 String Itt_prec
83 O o25 parent p25
84 T t26 o25
85 B b26 t26
86 T t27 o b26 b4
87 B b27 t27
88 P p27 String Itt_w
89 O o27 parent p27
90 T t28 o27
91 B b28 t28
92 T t29 o b28 b4
93 B b29 t29
94 P p29 String Itt_bunion
95 O o29 parent p29
96 T t30 o29
97 B b30 t30
98 T t31 o b30 b4
99 B b31 t31
100 P p31 String Itt_bisect
101 O o31 parent p31
102 T t32 o31
103 B b32 t32
104 T t33 o b32 b4
105 B b33 t33
106 P p33 String Itt_tunion
107 O o33 parent p33
108 T t34 o33
109 B b34 t34
110 T t35 o b34 b4
111 B b35 t35
112 P p35 String Itt_isect
113 O o35 parent p35
114 T t36 o35
115 B b36 t36
116 T t37 o b36 b4
117 B b37 t37
118 P p37 String Itt_struct2
119 O o37 parent p37
120 T t38 o37
121 B b38 t38
122 T t39 o b38 b4
123 B b39 t39
124 P p39 String Itt_well_founded
125 O o39 parent p39
126 T t40 o39
127 B b40 t40
128 T t41 o b40 b4
129 B b41 t41
130 P p41 String Itt_int_arith
131 O o41 parent p41
132 T t42 o41
133 B b42 t42
134 T t43 o b42 b4
135 B b43 t43
136 P p43 String Itt_int_ext
137 O o43 parent p43
138 T t44 o43
139 B b44 t44
140 T t45 o b44 b4
141 B b45 t45
142 P p45 String Itt_int_base
143 O o45 parent p45
144 T t46 o45
145 B b46 t46
146 T t47 o b46 b4
147 B b47 t47
148 P p47 String Itt_atom_bool
149 O o47 parent p47
150 T t48 o47
151 B b48 t48
152 T t49 o b48 b4
153 B b49 t49
154 P p49 String Itt_atom
155 O o49 parent p49
156 T t50 o49
157 B b50 t50
158 T t51 o b50 b4
159 B b51 t51
160 P p51 String Itt_bool
161 O o51 parent p51
162 T t52 o51
163 B b52 t52
164 T t53 o b52 b4
165 B b53 t53
166 P p53 String Itt_decidable
167 O o53 parent p53
168 T t54 o53
169 B b54 t54
170 T t55 o b54 b4
171 B b55 t55
172 P p55 String Itt_logic
173 O o55 parent p55
174 T t56 o55
175 B b56 t56
176 T t57 o b56 b4
177 B b57 t57
178 P p57 String Itt_prod
179 O o57 parent p57
180 T t58 o57
181 B b58 t58
182 T t59 o b58 b4
183 B b59 t59
184 P p59 String Itt_dprod
185 O o59 parent p59
186 T t60 o59
187 B b60 t60
188 T t61 o b60 b4
189 B b61 t61
190 P p61 String Itt_fun
191 O o61 parent p61
192 T t62 o61
193 B b62 t62
194 T t63 o b62 b4
195 B b63 t63
196 P p63 String Itt_dfun
197 O o63 parent p63
198 T t64 o63
199 B b64 t64
200 T t65 o b64 b4
201 B b65 t65
202 P p65 String Itt_rfun
203 O o65 parent p65
204 T t66 o65
205 B b66 t66
206 T t67 o b66 b4
207 B b67 t67
208 P p67 String Itt_set
209 O o67 parent p67
210 T t68 o67
211 B b68 t68
212 T t69 o b68 b4
213 B b69 t69
214 P p69 String Itt_unit
215 O o69 parent p69
216 T t70 o69
217 B b70 t70
218 T t71 o b70 b4
219 B b71 t71
220 P p71 String Itt_squiggle
221 O o71 parent p71
222 T t72 o71
223 B b72 t72
224 T t73 o b72 b4
225 B b73 t73
226 P p73 String Itt_squash
227 O o73 parent p73
228 T t74 o73
229 B b74 t74
230 T t75 o b74 b4
231 B b75 t75
232 P p75 String Itt_union
233 O o75 parent p75
234 T t76 o75
235 B b76 t76
236 T t77 o b76 b4
237 B b77 t77
238 P p77 String Itt_void
239 O o77 parent p77
240 T t78 o77
241 B b78 t78
242 T t79 o b78 b4
243 B b79 t79
244 P p79 String Itt_subtype
245 O o79 parent p79
246 T t80 o79
247 B b80 t80
248 T t81 o b80 b4
249 B b81 t81
250 P p81 String Itt_struct
251 O o81 parent p81
252 T t82 o81
253 B b82 t82
254 T t83 o b82 b4
255 B b83 t83
256 P p83 String Itt_equal
257 O o83 parent p83
258 T t84 o83
259 B b84 t84
260 T t85 o b84 b4
261 B b85 t85
262 P p85 String Itt_comment
263 O o85 parent p85
264 T t86 o85
265 B b86 t86
266 T t87 o b86 b4
267 B b87 t87
268 P p87 String Base_theory
269 O o87 parent p87
270 T t88 o87
271 B b88 t88
272 T t89 o b88 b4
273 B b89 t89
274 P p89 String Base_meta
275 O o89 parent p89
276 T t90 o89
277 B b90 t90
278 T t91 o b90 b4
279 B b91 t91
280 P p91 String Base_cache
281 O o91 parent p91
282 T t92 o91
283 B b92 t92
284 T t93 o b92 b4
285 B b93 t93
286 P p93 String Tactic_cache
287 O o93 parent p93
288 T t94 o93
289 B b94 t94
290 T t95 o b94 b4
291 B b95 t95
292 P p95 String Typeinf
293 O o95 parent p95
294 T t96 o95
295 B b96 t96
296 T t97 o b96 b4
297 B b97 t97
298 P p97 String Ocaml_df
299 O o97 parent p97
300 T t98 o97
301 B b98 t98
302 T t99 o b98 b4
303 B b99 t99
304 P p99 String Ocaml_str_df
305 O o99 parent p99
306 T t100 o99
307 B b100 t100
308 T t101 o b100 b4
309 B b101 t101
310 P p101 String Ocaml_sig_df
311 O o101 parent p101
312 T t102 o101
313 B b102 t102
314 T t103 o b102 b4
315 B b103 t103
316 P p103 String Ocaml_me_df
317 O o103 parent p103
318 T t104 o103
319 B b104 t104
320 T t105 o b104 b4
321 B b105 t105
322 P p105 String Ocaml_mt_df
323 O o105 parent p105
324 T t106 o105
325 B b106 t106
326 T t107 o b106 b4
327 B b107 t107
328 P p107 String Ocaml_type_df
329 O o107 parent p107
330 T t108 o107
331 B b108 t108
332 T t109 o b108 b4
333 B b109 t109
334 P p109 String Ocaml_patt_df
335 O o109 parent p109
336 T t110 o109
337 B b110 t110
338 T t111 o b110 b4
339 B b111 t111
340 P p111 String Ocaml_expr_df
341 O o111 parent p111
342 T t112 o111
343 B b112 t112
344 T t113 o b112 b4
345 B b113 t113
346 P p113 String Ocaml_base_df
347 O o113 parent p113
348 T t114 o113
349 B b114 t114
350 T t115 o b114 b4
351 B b115 t115
352 P p115 String Ocaml
353 O o115 parent p115
354 T t116 o115
355 B b116 t116
356 T t117 o b116 b4
357 B b117 t117
358 P p117 String Base_rewrite
359 O o117 parent p117
360 T t118 o117
361 B b118 t118
362 T t119 o b118 b4
363 B b119 t119
364 P p119 String Base_dtactic
365 O o119 parent p119
366 T t120 o119
367 B b120 t120
368 T t121 o b120 b4
369 B b121 t121
370 P p121 String Base_auto_tactic
371 O o121 parent p121
372 T t122 o121
373 B b122 t122
374 T t123 o b122 b4
375 B b123 t123
376 P p123 String Base_trivial
377 O o123 parent p123
378 T t124 o123
379 B b124 t124
380 T t125 o b124 b4
381 B b125 t125
382 P p125 String Top_conversionals
383 O o125 parent p125
384 T t126 o125
385 B b126 t126
386 T t127 o b126 b4
387 B b127 t127
388 P p127 String Top_tacticals
389 O o127 parent p127
390 T t128 o127
391 B b128 t128
392 T t129 o b128 b4
393 B b129 t129
394 P p129 String Var
395 O o129 parent p129
396 T t130 o129
397 B b130 t130
398 T t131 o b130 b4
399 B b131 t131
400 P p131 String Mptop
401 O o131 parent p131
402 T t132 o131
403 B b132 t132
404 T t133 o b132 b4
405 B b133 t133
406 P p133 String Summary
407 O o133 parent p133
408 T t134 o133
409 B b134 t134
410 T t135 o b134 b4
411 B b135 t135
412 P p135 String Comment
413 O o135 parent p135
414 T t136 o135
415 B b136 t136
416 T t137 o b136 b4
417 B b137 t137
418 P p137 String Base_dform
419 O o137 parent p137
420 T t138 o137
421 B b138 t138
422 T t139 o b138 b4
423 B b139 t139
424 P p139 String Nuprl_font
425 O o139 parent p139
426 T t140 o139
427 B b140 t140
428 T t141 o b140 b4
429 B b141 t141
430 P p141 String Perv
431 O o141 parent p141
432 T t142 o141
433 B b142 t142
434 T t143 o b142 b4
435 B b143 t143
436 T t144 o b143 b4
437 B b144 t144
438 T t145 o b141 b144
439 B b145 t145
440 T t146 o b139 b145
441 B b146 t146
442 T t147 o b137 b146
443 B b147 t147
444 T t148 o b135 b147
445 B b148 t148
446 T t149 o b133 b148
447 B b149 t149
448 T t150 o b131 b149
449 B b150 t150
450 T t151 o b129 b150
451 B b151 t151
452 T t152 o b127 b151
453 B b152 t152
454 T t153 o b125 b152
455 B b153 t153
456 T t154 o b123 b153
457 B b154 t154
458 T t155 o b121 b154
459 B b155 t155
460 T t156 o b119 b155
461 B b156 t156
462 T t157 o b117 b156
463 B b157 t157
464 T t158 o b115 b157
465 B b158 t158
466 T t159 o b113 b158
467 B b159 t159
468 T t160 o b111 b159
469 B b160 t160
470 T t161 o b109 b160
471 B b161 t161
472 T t162 o b107 b161
473 B b162 t162
474 T t163 o b105 b162
475 B b163 t163
476 T t164 o b103 b163
477 B b164 t164
478 T t165 o b101 b164
479 B b165 t165
480 T t166 o b99 b165
481 B b166 t166
482 T t167 o b97 b166
483 B b167 t167
484 T t168 o b95 b167
485 B b168 t168
486 T t169 o b93 b168
487 B b169 t169
488 T t170 o b91 b169
489 B b170 t170
490 T t171 o b89 b170
491 B b171 t171
492 T t172 o b87 b171
493 B b172 t172
494 T t173 o b85 b172
495 B b173 t173
496 T t174 o b83 b173
497 B b174 t174
498 T t175 o b81 b174
499 B b175 t175
500 T t176 o b79 b175
501 B b176 t176
502 T t177 o b77 b176
503 B b177 t177
504 T t178 o b75 b177
505 B b178 t178
506 T t179 o b73 b178
507 B b179 t179
508 T t180 o b71 b179
509 B b180 t180
510 T t181 o b69 b180
511 B b181 t181
512 T t182 o b67 b181
513 B b182 t182
514 T t183 o b65 b182
515 B b183 t183
516 T t184 o b63 b183
517 B b184 t184
518 T t185 o b61 b184
519 B b185 t185
520 T t186 o b59 b185
521 B b186 t186
522 T t187 o b57 b186
523 B b187 t187
524 T t188 o b55 b187
525 B b188 t188
526 T t189 o b53 b188
527 B b189 t189
528 T t190 o b51 b189
529 B b190 t190
530 T t191 o b49 b190
531 B b191 t191
532 T t192 o b47 b191
533 B b192 t192
534 T t193 o b45 b192
535 B b193 t193
536 T t194 o b43 b193
537 B b194 t194
538 T t195 o b41 b194
539 B b195 t195
540 T t196 o b39 b195
541 B b196 t196
542 T t197 o b37 b196
543 B b197 t197
544 T t198 o b35 b197
545 B b198 t198
546 T t199 o b33 b198
547 B b199 t199
548 T t200 o b31 b199
549 B b200 t200
550 T t201 o b29 b200
551 B b201 t201
552 T t202 o b27 b201
553 B b202 t202
554 T t203 o b25 b202
555 B b203 t203
556 T t204 o b23 b203
557 B b204 t204
558 T t205 o b21 b204
559 B b205 t205
560 T t206 o b19 b205
561 B b206 t206
562 T t207 o b17 b206
563 B b207 t207
564 T t208 o b15 b207
565 B b208 t208
566 T t209 o b13 b208
567 B b209 t209
568 T t210 o b11 b209
569 B b210 t210
570 T t211 o b9 b210
571 B b211 t211
572 T t212 o b7 b211
573 B b212 t212
574 T t213 o b5 b212
575 B b213 t213
576 NSummary!resource resource resource Summary
577 P p213 String auto
578 O o213 resource p213
579 NOcaml Ocaml Ocaml NIL
580 NOcaml!type_lid type_lid type_lid Ocaml
581 P p214 Number 2332
582 P p215 Number 2341
583 O o215 type_lid p214 p215
584 P p216 String auto_info
585 O o216 type_lid p216
586 T t216 o216
587 B b216 t216
588 T t217 o215 b216
589 B b217 t217
590 NOcaml!type_prod type_prod type_prod Ocaml
591 P p217 Number 2343
592 P p218 Number 2367
593 O o218 type_prod p217 p218
594 P p219 Number 2349
595 O o219 type_lid p217 p219
596 P p220 String tactic
597 O o220 type_lid p220
598 T t220 o220
599 B b220 t220
600 T t221 o219 b220
601 B b221 t221
602 P p221 Number 2352
603 P p222 Number 2358
604 O o222 type_lid p221 p222
605 T t222 o222 b220
606 B b222 t222
607 P p223 Number 2361
608 O o223 type_lid p223 p218
609 T t223 o223 b220
610 B b223 t223
611 T t224 o b223 b4
612 B b224 t224
613 T t225 o b222 b224
614 B b225 t225
615 T t226 o b221 b225
616 B b226 t226
617 T t227 o218 b226
618 B b227 t227
619 T t228 o213 b217 b227
620 B b228 t228
621 P p228 String cache
622 O o228 resource p228
623 P p229 Number 1424
624 P p230 Number 1434
625 O o230 type_lid p229 p230
626 P p231 String cache_rule
627 O o231 type_lid p231
628 T t231 o231
629 B b231 t231
630 T t232 o230 b231
631 B b232 t232
632 P p232 Number 1436
633 P p233 Number 1441
634 O o233 type_lid p232 p233
635 O o234 type_lid p228
636 T t234 o234
637 B b234 t234
638 T t235 o233 b234
639 B b235 t235
640 T t236 o228 b232 b235
641 B b236 t236
642 P p236 String elim
643 O o236 resource p236
644 P p237 Number 1761
645 P p238 Number 1783
646 O o238 type_prod p237 p238
647 P p239 Number 1765
648 O o239 type_lid p237 p239
649 P p240 String term
650 O o240 type_lid p240
651 T t240 o240
652 B b240 t240
653 T t241 o239 b240
654 B b241 t241
655 NOcaml!type_fun type_fun type_fun Ocaml
656 P p241 Number 1769
657 P p242 Number 1782
658 O o242 type_fun p241 p242
659 P p243 Number 1772
660 O o243 type_lid p241 p243
661 P p244 String int
662 O o244 type_lid p244
663 T t244 o244
664 B b244 t244
665 T t245 o243 b244
666 B b245 t245
667 P p245 Number 1776
668 O o245 type_lid p245 p242
669 T t246 o245 b220
670 B b246 t246
671 T t247 o242 b245 b246
672 B b247 t247
673 T t248 o b247 b4
674 B b248 t248
675 T t249 o b241 b248
676 B b249 t249
677 T t250 o238 b249
678 B b250 t250
679 P p250 Number 1785
680 P p251 Number 1798
681 O o251 type_fun p250 p251
682 P p252 Number 1788
683 O o252 type_lid p250 p252
684 T t252 o252 b244
685 B b252 t252
686 P p253 Number 1792
687 O o253 type_lid p253 p251
688 T t253 o253 b220
689 B b253 t253
690 T t254 o251 b252 b253
691 B b254 t254
692 T t255 o236 b250 b254
693 B b255 t255
694 P p255 String eqcd
695 O o255 resource p255
696 P p256 Number 6168
697 P p257 Number 6181
698 O o257 type_prod p256 p257
699 P p258 Number 6172
700 O o258 type_lid p256 p258
701 T t258 o258 b240
702 B b258 t258
703 P p259 Number 6175
704 O o259 type_lid p259 p257
705 T t259 o259 b220
706 B b259 t259
707 T t260 o b259 b4
708 B b260 t260
709 T t261 o b258 b260
710 B b261 t261
711 T t262 o257 b261
712 B b262 t262
713 P p262 Number 6183
714 P p263 Number 6189
715 O o263 type_lid p262 p263
716 T t263 o263 b220
717 B b263 t263
718 T t264 o255 b262 b263
719 B b264 t264
720 P p264 String intro
721 O o264 resource p264
722 P p265 Number 1815
723 P p266 Number 1852
724 O o266 type_prod p265 p266
725 P p267 Number 1819
726 O o267 type_lid p265 p267
727 T t267 o267 b240
728 B b267 t267
729 P p268 Number 1823
730 P p269 Number 1851
731 O o269 type_prod p268 p269
732 P p270 Number 1829
733 O o270 type_lid p268 p270
734 P p271 String string
735 O o271 type_lid p271
736 T t271 o271
737 B b271 t271
738 T t272 o270 b271
739 B b272 t272
740 NOcaml!type_apply type_apply type_apply Ocaml
741 P p272 Number 1832
742 P p273 Number 1842
743 O o273 type_apply p272 p273
744 P p274 Number 1836
745 O o274 type_lid p274 p273
746 P p275 String option
747 O o275 type_lid p275
748 T t275 o275
749 B b275 t275
750 T t276 o274 b275
751 B b276 t276
752 P p276 Number 1835
753 O o276 type_lid p272 p276
754 T t277 o276 b244
755 B b277 t277
756 T t278 o273 b276 b277
757 B b278 t278
758 P p278 Number 1845
759 O o278 type_lid p278 p269
760 T t279 o278 b220
761 B b279 t279
762 T t280 o b279 b4
763 B b280 t280
764 T t281 o b278 b280
765 B b281 t281
766 T t282 o b272 b281
767 B b282 t282
768 T t283 o269 b282
769 B b283 t283
770 T t284 o b283 b4
771 B b284 t284
772 T t285 o b267 b284
773 B b285 t285
774 T t286 o266 b285
775 B b286 t286
776 P p286 Number 1854
777 P p287 Number 1860
778 O o287 type_lid p286 p287
779 T t287 o287 b220
780 B b287 t287
781 T t288 o264 b286 b287
782 B b288 t288
783 P p288 String reduce
784 O o288 resource p288
785 P p289 Number 2920
786 P p290 Number 2931
787 O o290 type_prod p289 p290
788 P p291 Number 2924
789 O o291 type_lid p289 p291
790 T t291 o291 b240
791 B b291 t291
792 P p292 Number 2927
793 O o292 type_lid p292 p290
794 P p293 String conv
795 O o293 type_lid p293
796 T t293 o293
797 B b293 t293
798 T t294 o292 b293
799 B b294 t294
800 T t295 o b294 b4
801 B b295 t295
802 T t296 o b291 b295
803 B b296 t296
804 T t297 o290 b296
805 B b297 t297
806 P p297 Number 2933
807 P p298 Number 2937
808 O o298 type_lid p297 p298
809 T t298 o298 b293
810 B b298 t298
811 T t299 o288 b297 b298
812 B b299 t299
813 P p299 String squash
814 O o299 resource p299
815 P p300 Number 4017
816 P p301 Number 4028
817 O o301 type_lid p300 p301
818 P p302 String squash_info
819 O o302 type_lid p302
820 T t302 o302
821 B b302 t302
822 T t303 o301 b302
823 B b303 t303
824 P p303 Number 4030
825 P p304 Number 4043
826 O o304 type_fun p303 p304
827 P p305 Number 4033
828 O o305 type_lid p303 p305
829 T t305 o305 b244
830 B b305 t305
831 P p306 Number 4037
832 O o306 type_lid p306 p304
833 T t306 o306 b220
834 B b306 t306
835 T t307 o304 b305 b306
836 B b307 t307
837 T t308 o299 b303 b307
838 B b308 t308
839 P p308 String sub
840 O o308 resource p308
841 P p309 Number 4882
842 P p310 Number 4899
843 O o310 type_lid p309 p310
844 P p311 String sub_resource_info
845 O o311 type_lid p311
846 T t311 o311
847 B b311 t311
848 T t312 o310 b311
849 B b312 t312
850 P p312 Number 4901
851 P p313 Number 4907
852 O o313 type_lid p312 p313
853 T t313 o313 b220
854 B b313 t313
855 T t314 o308 b312 b313
856 B b314 t314
857 P p314 String toploop
858 O o314 resource p314
859 P p315 Number 2445
860 P p316 Number 2467
861 O o316 type_prod p315 p316
862 P p317 Number 2451
863 O o317 type_lid p315 p317
864 T t317 o317 b271
865 B b317 t317
866 P p318 Number 2454
867 P p319 Number 2460
868 O o319 type_lid p318 p319
869 T t319 o319 b271
870 B b319 t319
871 P p320 Number 2463
872 O o320 type_lid p320 p316
873 P p321 String expr
874 O o321 type_lid p321
875 T t321 o321
876 B b321 t321
877 T t322 o320 b321
878 B b322 t322
879 T t323 o b322 b4
880 B b323 t323
881 T t324 o b319 b323
882 B b324 t324
883 T t325 o b317 b324
884 B b325 t325
885 T t326 o316 b325
886 B b326 t326
887 P p326 Number 2469
888 P p327 Number 2478
889 O o327 type_lid p326 p327
890 P p328 String top_table
891 O o328 type_lid p328
892 T t328 o328
893 B b328 t328
894 T t329 o327 b328
895 B b329 t329
896 T t330 o314 b326 b329
897 B b330 t330
898 P p330 String typeinf
899 O o330 resource p330
900 P p331 Number 2151
901 P p332 Number 2172
902 O o332 type_lid p331 p332
903 P p333 String typeinf_resource_info
904 O o333 type_lid p333
905 T t333 o333
906 B b333 t333
907 T t334 o332 b333
908 B b334 t334
909 P p334 Number 2174
910 P p335 Number 2186
911 O o335 type_lid p334 p335
912 P p336 String typeinf_func
913 O o336 type_lid p336
914 T t336 o336
915 B b336 t336
916 T t337 o335 b336
917 B b337 t337
918 T t338 o330 b334 b337
919 B b338 t338
920 P p338 String typeinf_subst
921 O o338 resource p338
922 P p339 Number 1825
923 P p340 Number 1843
924 O o340 type_lid p339 p340
925 P p341 String typeinf_subst_info
926 O o341 type_lid p341
927 T t341 o341
928 B b341 t341
929 T t342 o340 b341
930 B b342 t342
931 P p342 Number 1862
932 O o342 type_lid p278 p342
933 P p343 String typeinf_subst_fun
934 O o343 type_lid p343
935 T t343 o343
936 B b343 t343
937 T t344 o342 b343
938 B b344 t344
939 T t345 o338 b342 b344
940 B b345 t345
941 T t346 o b345 b4
942 B b346 t346
943 T t347 o b338 b346
944 B b347 t347
945 T t348 o b330 b347
946 B b348 t348
947 T t349 o b314 b348
948 B b349 t349
949 T t350 o b308 b349
950 B b350 t350
951 T t351 o b299 b350
952 B b351 t351
953 T t352 o b288 b351
954 B b352 t352
955 T t353 o b264 b352
956 B b353 t353
957 T t354 o b255 b353
958 B b354 t354
959 T t355 o b236 b354
960 B b355 t355
961 T t356 o b228 b355
962 B b356 t356
963 T t357 o2 b5 b213 b356
964 B b357 t357
965 T t358 o1 b357
966 B b358 t358
967 P p358 Number 20
968 P p359 Number 42
969 O o359 location p358 p359
970 P p360 String Czf_itt_member
971 O o360 parent p360
972 T t360 o360
973 B b360 t360
974 T t361 o b360 b4
975 B b361 t361
976 P p361 String Czf_itt_eq
977 O o361 parent p361
978 T t362 o361
979 B b362 t362
980 T t363 o b362 b4
981 B b363 t363
982 T t364 o b363 b4
983 B b364 t364
984 T t365 o b361 b364
985 B b365 t365
986 T t366 o2 b361 b365 b356
987 B b366 t366
988 T t367 o359 b366
989 B b367 t367
990 P p367 Number 43
991 P p368 Number 61
992 O o368 location p367 p368
993 T t368 o2 b363 b4 b356
994 B b368 t368
995 T t369 o368 b368
996 B b369 t369
997 P p369 Number 62
998 P p370 Number 82
999 O o370 location p369 p370
1000 P p371 String Czf_itt_dall
1001 O o371 parent p371
1002 T t371 o371
1003 B b371 t371
1004 T t372 o b371 b4
1005 B b372 t372
1006 P p372 String Czf_itt_set_ind
1007 O o372 parent p372
1008 T t373 o372
1009 B b373 t373
1010 T t374 o b373 b4
1011 B b374 t374
1012 P p374 String Czf_itt_all
1013 O o374 parent p374
1014 T t375 o374
1015 B b375 t375
1016 T t376 o b375 b4
1017 B b376 t376
1018 P p376 String Czf_itt_sep
1019 O o376 parent p376
1020 T t377 o376
1021 B b377 t377
1022 T t378 o b377 b4
1023 B b378 t378
1024 T t379 o b378 b4
1025 B b379 t379
1026 T t380 o b376 b379
1027 B b380 t380
1028 T t381 o b374 b380
1029 B b381 t381
1030 T t382 o b372 b381
1031 B b382 t382
1032 T t383 o2 b372 b382 b356
1033 B b383 t383
1034 T t384 o370 b383
1035 B b384 t384
1036 P p384 Number 83
1037 P p385 Number 102
1038 O o385 location p384 p385
1039 P p386 String Czf_itt_and
1040 O o386 parent p386
1041 T t386 o386
1042 B b386 t386
1043 T t387 o b386 b4
1044 B b387 t387
1045 T t388 o b387 b4
1046 B b388 t388
1047 T t389 o2 b387 b388 b356
1048 B b389 t389
1049 T t390 o385 b389
1050 B b390 t390
1051 P p390 Number 104
1052 P p391 Number 115
1053 O o391 location p390 p391
1054 NSummary!summary_item summary_item summary_item Summary
1055 O o392 summary_item
1056 NOcaml!str_open str_open str_open Ocaml
1057 O o393 str_open p390 p391
1058 NOcaml!string string string Ocaml
1059 P p393 String Printf
1060 O o394 string p393
1061 T t394 o394
1062 B b394 t394
1063 T t395 o b394 b4
1064 B b395 t395
1065 T t396 o393 b395
1066 B b396 t396
1067 T t397 o392 b396
1068 B b397 t397
1069 T t398 o391 b397
1070 B b398 t398
1071 P p398 Number 116
1072 P p399 Number 129
1073 O o399 location p398 p399
1074 O o400 str_open p398 p399
1075 P p400 String Mp_debug
1076 O o401 string p400
1077 T t401 o401
1078 B b401 t401
1079 T t402 o b401 b4
1080 B b402 t402
1081 T t403 o400 b402
1082 B b403 t403
1083 T t404 o392 b403
1084 B b404 t404
1085 T t405 o399 b404
1086 B b405 t405
1087 P p405 Number 130
1088 P p406 Number 159
1089 O o406 location p405 p406
1090 O o407 str_open p405 p406
1091 P p407 String Refiner
1092 O o408 string p407
1093 T t408 o408
1094 B b408 t408
1095 P p408 String TermType
1096 O o409 string p408
1097 T t409 o409
1098 B b409 t409
1099 T t410 o b409 b4
1100 B b410 t410
1101 T t411 o b408 b410
1102 B b411 t411
1103 T t412 o b408 b411
1104 B b412 t412
1105 T t413 o407 b412
1106 B b413 t413
1107 T t414 o392 b413
1108 B b414 t414
1109 T t415 o406 b414
1110 B b415 t415
1111 P p415 Number 160
1112 P p416 Number 185
1113 O o416 location p415 p416
1114 O o417 str_open p415 p416
1115 P p417 String Term
1116 O o418 string p417
1117 T t418 o418
1118 B b418 t418
1119 T t419 o b418 b4
1120 B b419 t419
1121 T t420 o b408 b419
1122 B b420 t420
1123 T t421 o b408 b420
1124 B b421 t421
1125 T t422 o417 b421
1126 B b422 t422
1127 T t423 o392 b422
1128 B b423 t423
1129 T t424 o416 b423
1130 B b424 t424
1131 P p424 Number 186
1132 P p425 Number 213
1133 O o425 location p424 p425
1134 O o426 str_open p424 p425
1135 P p426 String TermOp
1136 O o427 string p426
1137 T t427 o427
1138 B b427 t427
1139 T t428 o b427 b4
1140 B b428 t428
1141 T t429 o b408 b428
1142 B b429 t429
1143 T t430 o b408 b429
1144 B b430 t430
1145 T t431 o426 b430
1146 B b431 t431
1147 T t432 o392 b431
1148 B b432 t432
1149 T t433 o425 b432
1150 B b433 t433
1151 P p433 Number 214
1152 P p434 Number 243
1153 O o434 location p433 p434
1154 O o435 str_open p433 p434
1155 P p435 String TermAddr
1156 O o436 string p435
1157 T t436 o436
1158 B b436 t436
1159 T t437 o b436 b4
1160 B b437 t437
1161 T t438 o b408 b437
1162 B b438 t438
1163 T t439 o b408 b438
1164 B b439 t439
1165 T t440 o435 b439
1166 B b440 t440
1167 T t441 o392 b440
1168 B b441 t441
1169 T t442 o434 b441
1170 B b442 t442
1171 P p442 Number 244
1172 P p443 Number 272
1173 O o443 location p442 p443
1174 O o444 str_open p442 p443
1175 P p444 String TermMan
1176 O o445 string p444
1177 T t445 o445
1178 B b445 t445
1179 T t446 o b445 b4
1180 B b446 t446
1181 T t447 o b408 b446
1182 B b447 t447
1183 T t448 o b408 b447
1184 B b448 t448
1185 T t449 o444 b448
1186 B b449 t449
1187 T t450 o392 b449
1188 B b450 t450
1189 T t451 o443 b450
1190 B b451 t451
1191 P p451 Number 273
1192 P p452 Number 303
1193 O o452 location p451 p452
1194 O o453 str_open p451 p452
1195 P p453 String TermSubst
1196 O o454 string p453
1197 T t454 o454
1198 B b454 t454
1199 T t455 o b454 b4
1200 B b455 t455
1201 T t456 o b408 b455
1202 B b456 t456
1203 T t457 o b408 b456
1204 B b457 t457
1205 T t458 o453 b457
1206 B b458 t458
1207 T t459 o392 b458
1208 B b459 t459
1209 T t460 o452 b459
1210 B b460 t460
1211 P p460 Number 304
1212 P p461 Number 331
1213 O o461 location p460 p461
1214 O o462 str_open p460 p461
1215 P p462 String Refine
1216 O o463 string p462
1217 T t463 o463
1218 B b463 t463
1219 T t464 o b463 b4
1220 B b464 t464
1221 T t465 o b408 b464
1222 B b465 t465
1223 T t466 o b408 b465
1224 B b466 t466
1225 T t467 o462 b466
1226 B b467 t467
1227 T t468 o392 b467
1228 B b468 t468
1229 T t469 o461 b468
1230 B b469 t469
1231 P p469 Number 332
1232 P p470 Number 364
1233 O o470 location p469 p470
1234 O o471 str_open p469 p470
1235 P p471 String RefineError
1236 O o472 string p471
1237 T t472 o472
1238 B b472 t472
1239 T t473 o b472 b4
1240 B b473 t473
1241 T t474 o b408 b473
1242 B b474 t474
1243 T t475 o b408 b474
1244 B b475 t475
1245 T t476 o471 b475
1246 B b476 t476
1247 T t477 o392 b476
1248 B b477 t477
1249 T t478 o470 b477
1250 B b478 t478
1251 P p478 Number 365
1252 P p479 Number 381
1253 O o479 location p478 p479
1254 O o480 str_open p478 p479
1255 P p480 String Mp_resource
1256 O o481 string p480
1257 T t481 o481
1258 B b481 t481
1259 T t482 o b481 b4
1260 B b482 t482
1261 T t483 o480 b482
1262 B b483 t483
1263 T t484 o392 b483
1264 B b484 t484
1265 T t485 o479 b484
1266 B b485 t485
1267 P p485 Number 382
1268 P p486 Number 399
1269 O o486 location p485 p486
1270 O o487 str_open p485 p486
1271 P p487 String Simple_print
1272 O o488 string p487
1273 T t488 o488
1274 B b488 t488
1275 T t489 o b488 b4
1276 B b489 t489
1277 T t490 o487 b489
1278 B b490 t490
1279 T t491 o392 b490
1280 B b491 t491
1281 T t492 o486 b491
1282 B b492 t492
1283 P p492 Number 401
1284 P p493 Number 417
1285 O o493 location p492 p493
1286 O o494 str_open p492 p493
1287 P p494 String Tactic_type
1288 O o495 string p494
1289 T t495 o495
1290 B b495 t495
1291 T t496 o b495 b4
1292 B b496 t496
1293 T t497 o494 b496
1294 B b497 t497
1295 T t498 o392 b497
1296 B b498 t498
1297 T t499 o493 b498
1298 B b499 t499
1299 P p499 Number 418
1300 P p500 Number 444
1301 O o500 location p499 p500
1302 O o501 str_open p499 p500
1303 P p501 String Tacticals
1304 O o502 string p501
1305 T t502 o502
1306 B b502 t502
1307 T t503 o b502 b4
1308 B b503 t503
1309 T t504 o b495 b503
1310 B b504 t504
1311 T t505 o501 b504
1312 B b505 t505
1313 T t506 o392 b505
1314 B b506 t506
1315 T t507 o500 b506
1316 B b507 t507
1317 P p507 Number 445
1318 P p508 Number 469
1319 O o508 location p507 p508
1320 O o509 str_open p507 p508
1321 P p509 String Sequent
1322 O o510 string p509
1323 T t510 o510
1324 B b510 t510
1325 T t511 o b510 b4
1326 B b511 t511
1327 T t512 o b495 b511
1328 B b512 t512
1329 T t513 o509 b512
1330 B b513 t513
1331 T t514 o392 b513
1332 B b514 t514
1333 T t515 o508 b514
1334 B b515 t515
1335 P p515 Number 470
1336 P p516 Number 500
1337 O o516 location p515 p516
1338 O o517 str_open p515 p516
1339 P p517 String Conversionals
1340 O o518 string p517
1341 T t518 o518
1342 B b518 t518
1343 T t519 o b518 b4
1344 B b519 t519
1345 T t520 o b495 b519
1346 B b520 t520
1347 T t521 o517 b520
1348 B b521 t521
1349 T t522 o392 b521
1350 B b522 t522
1351 T t523 o516 b522
1352 B b523 t523
1353 P p523 Number 501
1354 P p524 Number 511
1355 O o524 location p523 p524
1356 O o525 str_open p523 p524
1357 O o526 string p131
1358 T t526 o526
1359 B b526 t526
1360 T t527 o b526 b4
1361 B b527 t527
1362 T t528 o525 b527
1363 B b528 t528
1364 T t529 o392 b528
1365 B b529 t529
1366 T t530 o524 b529
1367 B b530 t530
1368 P p530 Number 512
1369 P p531 Number 520
1370 O o531 location p530 p531
1371 O o532 str_open p530 p531
1372 O o533 string p129
1373 T t533 o533
1374 B b533 t533
1375 T t534 o b533 b4
1376 B b534 t534
1377 T t535 o532 b534
1378 B b535 t535
1379 T t536 o392 b535
1380 B b536 t536
1381 T t537 o531 b536
1382 B b537 t537
1383 P p537 Number 522
1384 P p538 Number 539
1385 O o538 location p537 p538
1386 O o539 str_open p537 p538
1387 O o540 string p119
1388 T t540 o540
1389 B b540 t540
1390 T t541 o b540 b4
1391 B b541 t541
1392 T t542 o539 b541
1393 B b542 t542
1394 T t543 o392 b542
1395 B b543 t543
1396 T t544 o538 b543
1397 B b544 t544
1398 P p544 Number 540
1399 P p545 Number 561
1400 O o545 location p544 p545
1401 O o546 str_open p544 p545
1402 O o547 string p121
1403 T t547 o547
1404 B b547 t547
1405 T t548 o b547 b4
1406 B b548 t548
1407 T t549 o546 b548
1408 B b549 t549
1409 T t550 o392 b549
1410 B b550 t550
1411 T t551 o545 b550
1412 B b551 t551
1413 P p551 Number 563
1414 P p552 Number 574
1415 O o552 location p551 p552
1416 NSummary!opname opname opname Summary
1417 P p553 String car
1418 O o553 opname p553
1419 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1420 NCzf_itt_group!car car car Czf_itt_group
1421 O o554 car
1422 T t554 o554
1423 B b554 t554
1424 T t555 o553 b554
1425 B b555 t555
1426 T t556 o552 b555
1427 B b556 t556
1428 P p556 Number 615
1429 P p557 Number 635
1430 O o557 location p556 p557
1431 P p558 String op
1432 O o558 opname p558
1433 NCzf_itt_group!op op op Czf_itt_group
1434 O o559 op
1435 Nvar var var NIL
1436 P p559 Var s1
1437 O o560 var p559
1438 T t560 o560
1439 B b560 t560
1440 P p560 Var s2
1441 O o561 var p560
1442 T t561 o561
1443 B b561 t561
1444 T t562 o559 b560 b561
1445 B b562 t562
1446 T t563 o558 b562
1447 B b563 t563
1448 T t564 o557 b563
1449 B b564 t564
1450 P p564 Number 636
1451 P p565 Number 646
1452 O o565 location p564 p565
1453 P p566 String id
1454 O o566 opname p566
1455 NCzf_itt_group!id id id Czf_itt_group
1456 O o567 id
1457 T t567 o567
1458 B b567 t567
1459 T t568 o566 b567
1460 B b568 t568
1461 T t569 o565 b568
1462 B b569 t569
1463 P p569 Number 647
1464 P p570 Number 662
1465 O o570 location p569 p570
1466 P p571 String inv
1467 O o571 opname p571
1468 NCzf_itt_group!inv inv inv Czf_itt_group
1469 O o572 inv
1470 P p572 Var s
1471 O o573 var p572
1472 T t573 o573
1473 B b573 t573
1474 T t574 o572 b573
1475 B b574 t574
1476 T t575 o571 b574
1477 B b575 t575
1478 T t576 o570 b575
1479 B b576 t576
1480 P p576 Number 664
1481 P p577 Number 712
1482 O o577 location p576 p577
1483 NSummary!dform dform dform Summary
1484 P p578 String car_df
1485 O o578 dform p578
1486 NSummary!except_mode_df except_mode_df except_mode_df Summary
1487 P p579 String src
1488 O o579 except_mode_df p579
1489 T t579 o579
1490 B b579 t579
1491 T t580 o b579 b4
1492 B b580 t580
1493 NSummary!df_term df_term df_term Summary
1494 O o580 df_term
1495 NPerv!string string580 string Perv
1496 P p580 String G
1497 O o581 string580 p580
1498 T t581 o581
1499 B b581 t581
1500 T t582 o b581 b4
1501 B b582 t582
1502 T t583 o580 b582
1503 B b583 t583
1504 T t584 o578 b580 b554 b583
1505 B b584 t584
1506 T t585 o577 b584
1507 B b585 t585
1508 P p585 Number 714
1509 P p586 Number 760
1510 O o586 location p585 p586
1511 P p587 String id_df
1512 O o587 dform p587
1513 P p588 String e
1514 O o588 string580 p588
1515 T t588 o588
1516 B b588 t588
1517 T t589 o b588 b4
1518 B b589 t589
1519 T t590 o580 b589
1520 B b590 t590
1521 T t591 o587 b580 b567 b590
1522 B b591 t591
1523 T t592 o586 b591
1524 B b592 t592
1525 P p592 Number 762
1526 P p593 Number 862
1527 O o593 location p592 p593
1528 P p594 String op_df
1529 O o594 dform p594
1530 NSummary!parens_df parens_df parens_df Summary
1531 O o595 parens_df
1532 T t595 o595
1533 B b595 t595
1534 T t596 o b595 b4
1535 B b596 t596
1536 T t597 o b579 b596
1537 B b597 t597
1538 Nslot slot slot NIL
1539 P p597 String le
1540 O o597 slot p597
1541 T t598 o597 b560
1542 B b598 t598
1543 P p598 String " * "
1544 O o598 string580 p598
1545 T t599 o598
1546 B b599 t599
1547 T t600 o597 b561
1548 B b600 t600
1549 T t601 o b600 b4
1550 B b601 t601
1551 T t602 o b599 b601
1552 B b602 t602
1553 T t603 o b598 b602
1554 B b603 t603
1555 T t604 o580 b603
1556 B b604 t604
1557 T t605 o594 b597 b562 b604
1558 B b605 t605
1559 T t606 o593 b605
1560 B b606 t606
1561 P p606 Number 864
1562 P p607 Number 941
1563 O o607 location p606 p607
1564 P p608 String inv_df
1565 O o608 dform p608
1566 T t608 o597 b573
1567 B b608 t608
1568 P p609 String '
1569 O o609 string580 p609
1570 T t609 o609
1571 B b609 t609
1572 T t610 o b609 b4
1573 B b610 t610
1574 T t611 o b608 b610
1575 B b611 t611
1576 T t612 o580 b611
1577 B b612 t612
1578 T t613 o608 b597 b574 b612
1579 B b613 t613
1580 T t614 o607 b613
1581 B b614 t614
1582 P p614 Number 956
1583 P p615 Number 1032
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 978
1618 P p624 Number 985
1619 O o624 resource_defs p623 p624 p264
1620 NOcaml!uid uid uid Ocaml
1621 P p625 Number 983
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 1034
1640 P p633 Number 1209
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 1056
1675 P p646 Number 1063
1676 O o646 resource_defs p645 p646 p264
1677 P p647 Number 1061
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 1211
1692 P p653 Number 1481
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 1233
1726 P p665 Number 1240
1727 O o665 resource_defs p664 p665 p264
1728 P p666 Number 1238
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 1483
1743 P p672 Number 1760
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 1505
1785 P p687 Number 1512
1786 O o687 resource_defs p686 p687 p264
1787 P p688 Number 1510
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 1762
1802 P p694 Number 2039
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 1784
1825 P p703 Number 1791
1826 O o703 resource_defs p702 p703 p264
1827 P p704 Number 1789
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 2041
1842 O o709 location p709 p334
1843 P p710 String op_fun1
1844 O o710 rule p710
1845 T t710 o620 b573
1846 S s710 t637 h
1847 G s710 t710
1848 B b710 s710
1849 T t711 o618 b710
1850 B b711 t711
1851 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1852 O o711 fun_set
1853 P p711 Var z
1854 O o712 var p711
1855 T t712 o712
1856 B b712 t712
1857 T t713 o559 b712 b573
1858 B b713 t713 z
1859 T t714 o711 b713
1860 S s714 t620 h
1861 G s714 t714
1862 B b714 s714
1863 T t715 o618 b714
1864 B b715 t715
1865 T t716 o635 b711 b715
1866 B b716 t716
1867 P p716 Number 2064
1868 P p717 Number 2071
1869 O o717 resource_defs p716 p717 p264
1870 P p718 Number 2069
1871 O o718 uid p718 p717
1872 T t718 o718 b626
1873 B b718 t718
1874 T t719 o b718 b4
1875 B b719 t719
1876 T t720 o717 b719
1877 B b720 t720
1878 T t721 o b720 b4
1879 B b721 t721
1880 T t722 o710 b618 b716 b623 b721
1881 B b722 t722
1882 T t723 o709 b722
1883 B b723 t723
1884 P p723 Number 2176
1885 P p724 Number 2309
1886 O o724 location p723 p724
1887 P p725 String op_fun2
1888 O o725 rule p725
1889 T t725 o559 b573 b712
1890 B b725 t725 z
1891 T t726 o711 b725
1892 S s726 t620 h
1893 G s726 t726
1894 B b726 s726
1895 T t727 o618 b726
1896 B b727 t727
1897 T t728 o635 b711 b727
1898 B b728 t728
1899 P p728 Number 2199
1900 P p729 Number 2206
1901 O o729 resource_defs p728 p729 p264
1902 P p730 Number 2204
1903 O o730 uid p730 p729
1904 T t730 o730 b626
1905 B b730 t730
1906 T t731 o b730 b4
1907 B b731 t731
1908 T t732 o729 b731
1909 B b732 t732
1910 T t733 o b732 b4
1911 B b733 t733
1912 T t734 o725 b618 b728 b623 b733
1913 B b734 t734
1914 T t735 o724 b734
1915 B b735 t735
1916 P p735 Number 2499
1917 P p736 Number 2892
1918 O o736 location p735 p736
1919 P p737 String op_assoc1
1920 O o737 rule p737
1921 T t737 o655 b674 b554
1922 S s737 t620 h
1923 G s737 t737
1924 B b737 s737
1925 T t738 o618 b737
1926 B b738 t738
1927 NCzf_itt_eq!equal equal equal Czf_itt_eq
1928 O o738 equal
1929 T t739 o559 b562 b674
1930 B b739 t739
1931 T t740 o559 b560 b696
1932 B b740 t740
1933 T t741 o738 b739 b740
1934 S s741 t620 h
1935 G s741 t741
1936 B b741 s741
1937 T t742 o618 b741
1938 B b742 t742
1939 T t743 o635 b738 b742
1940 B b743 t743
1941 T t744 o635 b658 b743
1942 B b744 t744
1943 T t745 o635 b656 b744
1944 B b745 t745
1945 T t746 o635 b676 b745
1946 B b746 t746
1947 T t747 o635 b641 b746
1948 B b747 t747
1949 T t748 o635 b639 b747
1950 B b748 t748
1951 P p748 Number 2524
1952 P p749 Number 2531
1953 O o749 resource_defs p748 p749 p264
1954 P p750 Number 2529
1955 O o750 uid p750 p749
1956 T t750 o750 b626
1957 B b750 t750
1958 T t751 o b750 b4
1959 B b751 t751
1960 T t752 o749 b751
1961 B b752 t752
1962 T t753 o b752 b4
1963 B b753 t753
1964 T t754 o737 b618 b748 b623 b753
1965 B b754 t754
1966 T t755 o736 b754
1967 B b755 t755
1968 P p755 Number 2965
1969 P p756 Number 3358
1970 O o756 location p755 p756
1971 P p757 String op_assoc2
1972 O o757 rule p757
1973 T t757 o738 b740 b739
1974 S s757 t620 h
1975 G s757 t757
1976 B b757 s757
1977 T t758 o618 b757
1978 B b758 t758
1979 T t759 o635 b738 b758
1980 B b759 t759
1981 T t760 o635 b658 b759
1982 B b760 t760
1983 T t761 o635 b656 b760
1984 B b761 t761
1985 T t762 o635 b676 b761
1986 B b762 t762
1987 T t763 o635 b641 b762
1988 B b763 t763
1989 T t764 o635 b639 b763
1990 B b764 t764
1991 P p764 Number 2990
1992 P p765 Number 2997
1993 O o765 resource_defs p764 p765 p264
1994 P p766 Number 2995
1995 O o766 uid p766 p765
1996 T t766 o766 b626
1997 B b766 t766
1998 T t767 o b766 b4
1999 B b767 t767
2000 T t768 o765 b767
2001 B b768 t768
2002 T t769 o b768 b4
2003 B b769 t769
2004 T t770 o757 b618 b764 b623 b769
2005 B b770 t770
2006 T t771 o756 b770
2007 B b771 t771
2008 P p771 Number 3431
2009 P p772 Number 3507
2010 O o772 location p771 p772
2011 P p773 String id_wf1
2012 O o773 rule p773
2013 T t773 o620 b567
2014 S s773 t620 h
2015 G s773 t773
2016 B b773 s773
2017 T t774 o618 b773
2018 B b774 t774
2019 P p774 Number 3453
2020 P p775 Number 3461
2021 O o775 resource_defs p774 p775 p264
2022 P p776 Number 3459
2023 O o776 uid p776 p775
2024 T t776 o776 b626
2025 B b776 t776
2026 T t777 o b776 b4
2027 B b777 t777
2028 T t778 o775 b777
2029 B b778 t778
2030 T t779 o b778 b4
2031 B b779 t779
2032 T t780 o773 b618 b774 b623 b779
2033 B b780 t780
2034 T t781 o772 b780
2035 B b781 t781
2036 P p781 Number 3509
2037 P p782 Number 3587
2038 O o782 location p781 p782
2039 P p783 String id_wf2
2040 O o783 rule p783
2041 T t783 o655 b567 b554
2042 S s783 t620 h
2043 G s783 t783
2044 B b783 s783
2045 T t784 o618 b783
2046 B b784 t784
2047 P p784 Number 3531
2048 P p785 Number 3538
2049 O o785 resource_defs p784 p785 p264
2050 P p786 Number 3536
2051 O o786 uid p786 p785
2052 T t786 o786 b626
2053 B b786 t786
2054 T t787 o b786 b4
2055 B b787 t787
2056 T t788 o785 b787
2057 B b788 t788
2058 T t789 o b788 b4
2059 B b789 t789
2060 T t790 o783 b618 b784 b623 b789
2061 B b790 t790
2062 T t791 o782 b790
2063 B b791 t791
2064 P p791 Number 3675
2065 P p792 Number 3851
2066 O o792 location p791 p792
2067 P p793 String id_eq1
2068 O o793 rule p793
2069 T t793 o655 b573 b554
2070 S s793 t620 h
2071 G s793 t793
2072 B b793 s793
2073 T t794 o618 b793
2074 B b794 t794
2075 T t795 o559 b567 b573
2076 B b795 t795
2077 T t796 o738 b795 b573
2078 S s796 t620 h
2079 G s796 t796
2080 B b796 s796
2081 T t797 o618 b796
2082 B b797 t797
2083 T t798 o635 b794 b797
2084 B b798 t798
2085 T t799 o635 b711 b798
2086 B b799 t799
2087 P p799 Number 3697
2088 P p800 Number 3704
2089 O o800 resource_defs p799 p800 p264
2090 P p801 Number 3702
2091 O o801 uid p801 p800
2092 T t801 o801 b626
2093 B b801 t801
2094 T t802 o b801 b4
2095 B b802 t802
2096 T t803 o800 b802
2097 B b803 t803
2098 T t804 o b803 b4
2099 B b804 t804
2100 T t805 o793 b618 b799 b623 b804
2101 B b805 t805
2102 T t806 o792 b805
2103 B b806 t806
2104 P p806 Number 3853
2105 P p807 Number 4029
2106 O o807 location p806 p807
2107 P p808 String id_eq2
2108 O o808 rule p808
2109 T t808 o559 b573 b567
2110 B b808 t808
2111 T t809 o738 b808 b573
2112 S s809 t620 h
2113 G s809 t809
2114 B b809 s809
2115 T t810 o618 b809
2116 B b810 t810
2117 T t811 o635 b794 b810
2118 B b811 t811
2119 T t812 o635 b711 b811
2120 B b812 t812
2121 P p812 Number 3875
2122 P p813 Number 3882
2123 O o813 resource_defs p812 p813 p264
2124 P p814 Number 3880
2125 O o814 uid p814 p813
2126 T t814 o814 b626
2127 B b814 t814
2128 T t815 o b814 b4
2129 B b815 t815
2130 T t816 o813 b815
2131 B b816 t816
2132 T t817 o b816 b4
2133 B b817 t817
2134 T t818 o808 b618 b812 b623 b817
2135 B b818 t818
2136 T t819 o807 b818
2137 B b819 t819
2138 P p819 Number 4031
2139 P p820 Number 4088
2140 O o820 location p819 p820
2141 NOcaml!str_let str_let str_let Ocaml
2142 O o821 str_let p819 p820
2143 NOcaml!patt_var patt_var patt_var Ocaml
2144 P p821 Number 4035
2145 O o822 patt_var p821 p820
2146 NOcaml!patt_done patt_done patt_done Ocaml
2147 O o823 patt_done p819 p820
2148 T t823 o823
2149 B b823 t823 id_elim2T
2150 T t824 o822 b823
2151 B b824 t824
2152 NOcaml!fun fun fun Ocaml
2153 O o824 fun p821 p820
2154 NOcaml!patt_if patt_if patt_if Ocaml
2155 O o825 patt_if p821 p820
2156 P p825 Number 4045
2157 P p826 Number 4046
2158 O o826 patt_var p825 p826
2159 NOcaml!patt_body patt_body patt_body Ocaml
2160 O o827 patt_body p821 p820
2161 NOcaml!apply apply apply Ocaml
2162 P p827 Number 4052
2163 O o828 apply p827 p820
2164 P p828 Number 4086
2165 O o829 apply p827 p828
2166 NOcaml!lid lid lid Ocaml
2167 P p829 Number 4058
2168 O o830 lid p827 p829
2169 O o831 lid p793
2170 T t831 o831
2171 B b831 t831
2172 T t832 o830 b831
2173 B b832 t832
2174 P p832 Number 4060
2175 P p833 Number 4085
2176 O o833 apply p832 p833
2177 NOcaml!proj proj proj Ocaml
2178 P p834 Number 4083
2179 O o834 proj p832 p834
2180 O o835 uid p832 p834
2181 O o836 uid p509
2182 T t836 o836
2183 B b836 t836
2184 T t837 o835 b836
2185 B b837 t837
2186 P p837 Number 4069
2187 O o837 lid p837 p834
2188 P p838 String hyp_count_addr
2189 O o838 lid p838
2190 T t838 o838
2191 B b838 t838
2192 T t839 o837 b838
2193 B b839 t839
2194 T t840 o834 b837 b839
2195 B b840 t840
2196 P p840 Number 4084
2197 O o840 lid p840 p833
2198 P p841 Var p
2199 O o841 var p841
2200 T t841 o841
2201 B b841 t841
2202 T t842 o840 b841
2203 B b842 t842
2204 T t843 o833 b840 b842
2205 B b843 t843
2206 T t844 o829 b832 b843
2207 B b844 t844
2208 P p844 Number 4087
2209 O o844 lid p844 p820
2210 T t845 o844 b841
2211 B b845 t845
2212 T t846 o828 b844 b845
2213 B b846 t846
2214 T t847 o827 b846
2215 B b847 t847 p
2216 T t848 o826 b847
2217 B b848 t848
2218 T t849 o825 b848
2219 B b849 t849
2220 T t850 o824 b849
2221 B b850 t850
2222 T t851 o821 b824 b850
2223 B b851 t851
2224 T t852 o b851 b4
2225 B b852 t852
2226 T t853 o821 b852
2227 B b853 t853
2228 T t854 o392 b853
2229 B b854 t854
2230 T t855 o820 b854
2231 B b855 t855
2232 P p855 Number 4090
2233 P p856 Number 4263
2234 O o856 location p855 p856
2235 P p857 String inv_wf1
2236 O o857 rule p857
2237 T t857 o572 b560
2238 B b857 t857
2239 T t858 o620 b857
2240 S s858 t620 h
2241 G s858 t858
2242 B b858 s858
2243 T t859 o618 b858
2244 B b859 t859
2245 T t860 o635 b656 b859
2246 B b860 t860
2247 T t861 o635 b639 b860
2248 B b861 t861
2249 P p861 Number 4113
2250 P p862 Number 4120
2251 O o862 resource_defs p861 p862 p264
2252 P p863 Number 4118
2253 O o863 uid p863 p862
2254 T t863 o863 b626
2255 B b863 t863
2256 T t864 o b863 b4
2257 B b864 t864
2258 T t865 o862 b864
2259 B b865 t865
2260 T t866 o b865 b4
2261 B b866 t866
2262 T t867 o857 b618 b861 b623 b866
2263 B b867 t867
2264 T t868 o856 b867
2265 B b868 t868
2266 P p868 Number 4265
2267 P p869 Number 4441
2268 O o869 location p868 p869
2269 P p870 String inv_wf2
2270 O o870 rule p870
2271 T t870 o655 b857 b554
2272 S s870 t620 h
2273 G s870 t870
2274 B b870 s870
2275 T t871 o618 b870
2276 B b871 t871
2277 T t872 o635 b656 b871
2278 B b872 t872
2279 T t873 o635 b639 b872
2280 B b873 t873
2281 P p873 Number 4288
2282 P p874 Number 4295
2283 O o874 resource_defs p873 p874 p264
2284 P p875 Number 4293
2285 O o875 uid p875 p874
2286 T t875 o875 b626
2287 B b875 t875
2288 T t876 o b875 b4
2289 B b876 t876
2290 T t877 o874 b876
2291 B b877 t877
2292 T t878 o b877 b4
2293 B b878 t878
2294 T t879 o870 b618 b873 b623 b878
2295 B b879 t879
2296 T t880 o869 b879
2297 B b880 t880
2298 P p880 Number 4443
2299 P p881 Number 4530
2300 O o881 location p880 p881
2301 P p882 String inv_fun1
2302 O o882 rule p882
2303 T t882 o572 b712
2304 B b882 t882 z
2305 T t883 o711 b882
2306 S s883 t620 h
2307 G s883 t883
2308 B b883 s883
2309 T t884 o618 b883
2310 B b884 t884
2311 P p884 Number 4467
2312 P p885 Number 4474
2313 O o885 resource_defs p884 p885 p264
2314 P p886 Number 4472
2315 O o886 uid p886 p885
2316 T t886 o886 b626
2317 B b886 t886
2318 T t887 o b886 b4
2319 B b887 t887
2320 T t888 o885 b887
2321 B b888 t888
2322 T t889 o b888 b4
2323 B b889 t889
2324 T t890 o882 b618 b884 b623 b889
2325 B b890 t890
2326 T t891 o881 b890
2327 B b891 t891
2328 P p891 Number 4532
2329 P p892 Number 4718
2330 O o892 location p891 p892
2331 P p893 String inv_id1
2332 O o893 rule p893
2333 T t893 o559 b857 b560
2334 B b893 t893
2335 T t894 o738 b893 b567
2336 S s894 t620 h
2337 G s894 t894
2338 B b894 s894
2339 T t895 o618 b894
2340 B b895 t895
2341 T t896 o635 b656 b895
2342 B b896 t896
2343 T t897 o635 b639 b896
2344 B b897 t897
2345 P p897 Number 4555
2346 P p898 Number 4562
2347 O o898 resource_defs p897 p898 p264
2348 P p899 Number 4560
2349 O o899 uid p899 p898
2350 T t899 o899 b626
2351 B b899 t899
2352 T t900 o b899 b4
2353 B b900 t900
2354 T t901 o898 b900
2355 B b901 t901
2356 T t902 o b901 b4
2357 B b902 t902
2358 T t903 o893 b618 b897 b623 b902
2359 B b903 t903
2360 T t904 o892 b903
2361 B b904 t904
2362 P p904 Number 4720
2363 P p905 Number 4906
2364 O o905 location p904 p905
2365 P p906 String inv_id2
2366 O o906 rule p906
2367 T t906 o559 b560 b857
2368 B b906 t906
2369 T t907 o738 b906 b567
2370 S s907 t620 h
2371 G s907 t907
2372 B b907 s907
2373 T t908 o618 b907
2374 B b908 t908
2375 T t909 o635 b656 b908
2376 B b909 t909
2377 T t910 o635 b639 b909
2378 B b910 t910
2379 P p910 Number 4743
2380 P p911 Number 4750
2381 O o911 resource_defs p910 p911 p264
2382 P p912 Number 4748
2383 O o912 uid p912 p911
2384 T t912 o912 b626
2385 B b912 t912
2386 T t913 o b912 b4
2387 B b913 t913
2388 T t914 o911 b913
2389 B b914 t914
2390 T t915 o b914 b4
2391 B b915 t915
2392 T t916 o906 b618 b910 b623 b915
2393 B b916 t916
2394 T t917 o905 b916
2395 B b917 t917
2396 P p917 Number 5367
2397 P p918 Number 5793
2398 O o918 location p917 p918
2399 P p919 String cancel1
2400 O o919 rule p919
2401 NSummary!term_param term_param term_param Summary
2402 O o920 term_param
2403 T t920 o920 b560
2404 B b920 t920
2405 T t921 o b920 b4
2406 B b921 t921
2407 T t922 o b617 b921
2408 B b922 t922
2409 T t923 o738 b562 b695
2410 S s923 t620 h
2411 G s923 t923
2412 B b923 s923
2413 T t924 o618 b923
2414 B b924 t924
2415 T t925 o738 b561 b674
2416 S s925 t620 h
2417 G s925 t925
2418 B b925 s925
2419 T t926 o618 b925
2420 B b926 t926
2421 T t927 o635 b924 b926
2422 B b927 t927
2423 T t928 o635 b738 b927
2424 B b928 t928
2425 T t929 o635 b658 b928
2426 B b929 t929
2427 T t930 o635 b656 b929
2428 B b930 t930
2429 T t931 o635 b676 b930
2430 B b931 t931
2431 T t932 o635 b641 b931
2432 B b932 t932
2433 T t933 o635 b639 b932
2434 B b933 t933
2435 NSummary!interactive interactive interactive Summary
2436 O o933 interactive
2437 NSummary!ext_rule ext_rule ext_rule Summary
2438 P p933 String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2439 O o934 ext_rule p933
2440 NSummary!status_incomplete status_incomplete status_incomplete Summary
2441 O o935 status_incomplete
2442 T t935 o935
2443 B b935 t935
2444 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2445 O o936 ext_unjustified
2446 NSummary!tactic_arg tactic_arg tactic_arg Summary
2447 P p936 String main
2448 O o937 tactic_arg p936
2449 NSummary!msequent msequent msequent Summary
2450 O o938 msequent
2451 T t938 o b923 b4
2452 B b938 t938
2453 T t939 o b737 b938
2454 B b939 t939
2455 T t940 o b657 b939
2456 B b940 t940
2457 T t941 o b655 b940
2458 B b941 t941
2459 T t942 o b675 b941
2460 B b942 t942
2461 T t943 o b640 b942
2462 B b943 t943
2463 T t944 o b638 b943
2464 B b944 t944
2465 T t945 o938 b925 b944
2466 B b945 t945
2467 NSummary!parent_none parent_none parent_none Summary
2468 O o945 parent_none
2469 T t946 o945
2470 B b946 t946
2471 T t947 o937 b945 b4 b946
2472 B b947 t947
2473 P p947 String assertion
2474 O o947 tactic_arg p947
2475 H h947 v t923
2476 T t948 o559 b857 b562
2477 B b948 t948
2478 T t949 o559 b857 b695
2479 B b949 t949
2480 T t950 o738 b948 b949
2481 S s950 t620 h h947
2482 G s950 t950
2483 B b950 s950
2484 T t951 o938 b950 b944
2485 B b951 t951
2486 S s951 t620 h h947
2487 G s951 t925
2488 B b952 s951
2489 T t952 o938 b952 b944
2490 B b953 t952
2491 T t953 o2 b947
2492 B b954 t953
2493 T t954 o937 b953 b4 b954
2494 B b955 t954
2495 T t955 o2 b955
2496 B b956 t955
2497 T t956 o947 b951 b4 b956
2498 B b957 t956
2499 H h957 v_1 t950
2500 S s957 t620 h h947 h957
2501 G s957 t925
2502 B b958 s957
2503 T t958 o938 b958 b944
2504 B b959 t958
2505 T t959 o937 b959 b4 b956
2506 B b960 t959
2507 T t960 o b960 b4
2508 B b961 t960
2509 T t961 o b957 b961
2510 B b962 t961
2511 T t962 o936 b947 b962
2512 B b963 t962
2513 P p963 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2514 O o963 ext_rule p963
2515 T t963 o936 b957 b4
2516 B b964 t963
2517 T t964 o963 b935 b964 b4 b4
2518 B b965 t964
2519 P p965 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2520 O o965 ext_rule p965
2521 P p966 String eq
2522 O o966 tactic_arg p966
2523 T t966 o559 b893 b561
2524 B b966 t966
2525 T t967 o738 b948 b966
2526 S s967 t620 h h947 h957
2527 G s967 t967
2528 B b967 s967
2529 T t968 o938 b967 b944
2530 B b968 t968
2531 T t969 o2 b960
2532 B b969 t969
2533 T t970 o966 b968 b4 b969
2534 B b970 t970
2535 T t971 o738 b966 b949
2536 H h971 v_2 t971
2537 S s971 t620 h h947 h957 h971
2538 G s971 t925
2539 B b971 s971
2540 T t972 o938 b971 b944
2541 B b972 t972
2542 T t973 o937 b972 b4 b969
2543 B b973 t973
2544 P p973 String wf
2545 O o973 tactic_arg p973
2546 B b974 t949 v_2
2547 T t974 o711 b974
2548 S s974 t620 h h947 h957
2549 G s974 t974
2550 B b975 s974
2551 T t975 o938 b975 b944
2552 B b976 t975
2553 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2554 O o976 fun_prop
2555 P p976 Var v_2
2556 O o977 var p976
2557 T t977 o977
2558 B b977 t977
2559 T t978 o738 b977 b949
2560 B b978 t978 v_2
2561 T t979 o976 b978
2562 S s979 t620 h h947 h957
2563 G s979 t979
2564 B b979 s979
2565 T t980 o938 b979 b944
2566 B b980 t980
2567 NSummary!arg_named arg_named arg_named Summary
2568 P p980 String d_auto
2569 O o980 arg_named p980
2570 NSummary!arg_bool arg_bool arg_bool Summary
2571 P p981 String true
2572 O o981 arg_bool p981
2573 T t981 o981
2574 B b981 t981
2575 T t982 o980 b981
2576 B b982 t982
2577 T t983 o b982 b4
2578 B b983 t983
2579 T t984 o973 b980 b983 b969
2580 B b984 t984
2581 T t985 o2 b984
2582 B b985 t985
2583 T t986 o973 b976 b4 b985
2584 B b986 t986
2585 T t987 o b986 b4
2586 B b987 t987
2587 T t988 o b973 b987
2588 B b988 t988
2589 T t989 o b970 b988
2590 B b989 t989
2591 T t990 o936 b960 b989
2592 B b990 t990
2593 P p990 String autoT
2594 O o990 ext_rule p990
2595 T t991 o936 b970 b4
2596 B b991 t991
2597 T t992 o990 b935 b991 b4 b4
2598 B b992 t992
2599 P p992 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2600 O o992 ext_rule p992
2601 T t993 o559 b893 b674
2602 B b993 t993
2603 T t994 o738 b949 b993
2604 S s994 t620 h h947 h957 h971
2605 G s994 t994
2606 B b994 s994
2607 T t995 o938 b994 b944
2608 B b995 t995
2609 T t996 o2 b973
2610 B b996 t996
2611 T t997 o966 b995 b4 b996
2612 B b997 t997
2613 T t998 o738 b966 b993
2614 H h998 v_3 t998
2615 S s998 t620 h h947 h957 h971 h998
2616 G s998 t925
2617 B b998 s998
2618 T t999 o938 b998 b944
2619 B b999 t999
2620 T t1000 o937 b999 b4 b996
2621 B b1000 t1000
2622 B b1001 t966 v_3
2623 T t1001 o711 b1001
2624 S s1001 t620 h h947 h957 h971
2625 G s1001 t1001
2626 B b1002 s1001
2627 T t1002 o938 b1002 b944
2628 B b1003 t1002
2629 P p1003 Var v_3
2630 O o1003 var p1003
2631 T t1003 o1003
2632 B b1004 t1003
2633 T t1004 o738 b966 b1004
2634 B b1005 t1004 v_3
2635 T t1005 o976 b1005
2636 S s1005 t620 h h947 h957 h971
2637 G s1005 t1005
2638 B b1006 s1005
2639 T t1006 o938 b1006 b944
2640 B b1007 t1006
2641 T t1007 o973 b1007 b983 b996
2642 B b1008 t1007
2643 T t1008 o2 b1008
2644 B b1009 t1008
2645 T t1009 o973 b1003 b4 b1009
2646 B b1010 t1009
2647 T t1010 o b1010 b4
2648 B b1011 t1010
2649 T t1011 o b1000 b1011
2650 B b1012 t1011
2651 T t1012 o b997 b1012
2652 B b1013 t1012
2653 T t1013 o936 b973 b1013
2654 B b1014 t1013
2655 T t1014 o936 b997 b4
2656 B b1015 t1014
2657 T t1015 o990 b935 b1015 b4 b4
2658 B b1016 t1015
2659 P p1016 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2660 O o1016 ext_rule p1016
2661 T t1016 o559 b567 b561
2662 B b1017 t1016
2663 T t1017 o559 b567 b674
2664 B b1018 t1017
2665 T t1018 o738 b1017 b1018
2666 H h1018 v_4 t1018
2667 S s1018 t620 h h947 h957 h971 h998 h1018
2668 G s1018 t925
2669 B b1019 s1018
2670 T t1019 o938 b1019 b944
2671 B b1020 t1019
2672 T t1020 o2 b1000
2673 B b1021 t1020
2674 T t1021 o937 b1020 b4 b1021
2675 B b1022 t1021
2676 T t1022 o b1022 b4
2677 B b1023 t1022
2678 T t1023 o936 b1000 b1023
2679 B b1024 t1023
2680 P p1024 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2681 O o1024 ext_rule p1024
2682 T t1024 o738 b561 b1018
2683 H h1024 v_5 t1024
2684 S s1024 t620 h h947 h957 h971 h998 h1018 h1024
2685 G s1024 t925
2686 B b1025 s1024
2687 T t1025 o938 b1025 b944
2688 B b1026 t1025
2689 T t1026 o2 b1022
2690 B b1027 t1026
2691 T t1027 o937 b1026 b4 b1027
2692 B b1028 t1027
2693 B b1029 t1017 v_5
2694 T t1029 o711 b1029
2695 S s1029 t620 h h947 h957 h971 h998 h1018
2696 G s1029 t1029
2697 B b1030 s1029
2698 T t1030 o938 b1030 b944
2699 B b1031 t1030
2700 P p1031 Var v_5
2701 O o1031 var p1031
2702 T t1031 o1031
2703 B b1032 t1031
2704 T t1032 o738 b1032 b1018
2705 B b1033 t1032 v_5
2706 T t1033 o976 b1033
2707 S s1033 t620 h h947 h957 h971 h998 h1018
2708 G s1033 t1033
2709 B b1034 s1033
2710 T t1034 o938 b1034 b944
2711 B b1035 t1034
2712 T t1035 o973 b1035 b983 b1027
2713 B b1036 t1035
2714 T t1036 o2 b1036
2715 B b1037 t1036
2716 T t1037 o973 b1031 b4 b1037
2717 B b1038 t1037
2718 T t1038 o b1038 b4
2719 B b1039 t1038
2720 T t1039 o b1028 b1039
2721 B b1040 t1039
2722 T t1040 o936 b1022 b1040
2723 B b1041 t1040
2724 P p1041 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2725 O o1041 ext_rule p1041
2726 H h1041 v_6 t925
2727 S s1041 t620 h h947 h957 h971 h998 h1018 h1024 h1041
2728 G s1041 t925
2729 B b1042 s1041
2730 T t1042 o938 b1042 b944
2731 B b1043 t1042
2732 T t1043 o2 b1028
2733 B b1044 t1043
2734 T t1044 o937 b1043 b4 b1044
2735 B b1045 t1044
2736 T t1045 o b1045 b4
2737 B b1046 t1045
2738 T t1046 o936 b1028 b1046
2739 B b1047 t1046
2740 P p1047 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2741 O o1047 ext_rule p1047
2742 T t1047 o936 b1045 b4
2743 B b1048 t1047
2744 T t1048 o1047 b935 b1048 b4 b4
2745 B b1049 t1048
2746 T t1049 o b1049 b4
2747 B b1050 t1049
2748 P p1050 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2749 O o1050 ext_rule p1050
2750 B b1051 t1016 v_6
2751 T t1051 o711 b1051
2752 S s1051 t620 h h947 h957 h971 h998 h1018 h1024
2753 G s1051 t1051
2754 B b1052 s1051
2755 T t1052 o938 b1052 b944
2756 B b1053 t1052
2757 P p1053 Var v_6
2758 O o1053 var p1053
2759 T t1053 o1053
2760 B b1054 t1053
2761 T t1054 o738 b1017 b1054
2762 B b1055 t1054 v_6
2763 T t1055 o976 b1055
2764 S s1055 t620 h h947 h957 h971 h998 h1018 h1024
2765 G s1055 t1055
2766 B b1056 s1055
2767 T t1056 o938 b1056 b944
2768 B b1057 t1056
2769 T t1057 o973 b1057 b983 b1044
2770 B b1058 t1057
2771 T t1058 o2 b1058
2772 B b1059 t1058
2773 T t1059 o973 b1053 b4 b1059
2774 B b1060 t1059
2775 T t1060 o936 b1060 b4
2776 B b1061 t1060
2777 T t1061 o1050 b935 b1061 b4 b4
2778 B b1062 t1061
2779 T t1062 o b1062 b4
2780 B b1063 t1062
2781 T t1063 o1041 b935 b1047 b1050 b1063
2782 B b1064 t1063
2783 T t1064 o936 b1038 b4
2784 B b1065 t1064
2785 T t1065 o1050 b935 b1065 b4 b4
2786 B b1066 t1065
2787 T t1066 o b1066 b4
2788 B b1067 t1066
2789 T t1067 o b1064 b1067
2790 B b1068 t1067
2791 T t1068 o1024 b935 b1041 b1068 b4
2792 B b1069 t1068
2793 T t1069 o b1069 b4
2794 B b1070 t1069
2795 T t1070 o1016 b935 b1024 b1070 b4
2796 B b1071 t1070
2797 P p1071 String "rwh unfold_fun_set 0 thenT autoT"
2798 O o1071 ext_rule p1071
2799 T t1071 o936 b1010 b4
2800 B b1072 t1071
2801 T t1072 o1071 b935 b1072 b4 b4
2802 B b1073 t1072
2803 T t1073 o b1073 b4
2804 B b1074 t1073
2805 T t1074 o b1071 b1074
2806 B b1075 t1074
2807 T t1075 o b1016 b1075
2808 B b1076 t1075
2809 T t1076 o992 b935 b1014 b1076 b4
2810 B b1077 t1076
2811 T t1077 o936 b986 b4
2812 B b1078 t1077
2813 T t1078 o1071 b935 b1078 b4 b4
2814 B b1079 t1078
2815 T t1079 o b1079 b4
2816 B b1080 t1079
2817 T t1080 o b1077 b1080
2818 B b1081 t1080
2819 T t1081 o b992 b1081
2820 B b1082 t1081
2821 T t1082 o965 b935 b990 b1082 b4
2822 B b1083 t1082
2823 T t1083 o b1083 b4
2824 B b1084 t1083
2825 T t1084 o b965 b1084
2826 B b1085 t1084
2827 NSummary!ext_goal ext_goal ext_goal Summary
2828 O o1085 ext_goal
2829 S s1085 t620 h
2830 G s1085 t950
2831 B b1086 s1085
2832 T t1086 o938 b1086 b944
2833 B b1087 t1086
2834 T t1087 o947 b1087 b4 b954
2835 B b1088 t1087
2836 T t1088 o1085 b1088
2837 B b1089 t1088
2838 T t1089 o b1089 b4
2839 B b1090 t1089
2840 T t1090 o963 b935 b1089 b1090 b4
2841 B b1091 t1090
2842 P p1091 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2843 O o1091 ext_rule p1091
2844 H h1091 v t950
2845 S s1091 t620 h h1091
2846 G s1091 t925
2847 B b1092 s1091
2848 T t1092 o938 b1092 b944
2849 B b1093 t1092
2850 T t1093 o937 b1093 b4 b954
2851 B b1094 t1093
2852 T t1094 o1085 b1094
2853 B b1095 t1094
2854 P p1095 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2855 O o1095 ext_rule p1095
2856 P p1096 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2857 O o1096 ext_rule p1096
2858 T t1096 o b1095 b4
2859 B b1096 t1096
2860 H h1096 x t923
2861 H h1097 v_1 t971
2862 H h1098 v_2 t998
2863 H h1099 v_3 t1018
2864 H h1100 v_4 t1024
2865 B b1100 t1016 v_5
2866 T t1100 o711 b1100
2867 S s1100 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2868 G s1100 t1100
2869 B b1101 s1100
2870 T t1101 o b737 b4
2871 B b1102 t1101
2872 T t1102 o b657 b1102
2873 B b1103 t1102
2874 T t1103 o b655 b1103
2875 B b1104 t1103
2876 T t1104 o b675 b1104
2877 B b1105 t1104
2878 T t1105 o b640 b1105
2879 B b1106 t1105
2880 T t1106 o b638 b1106
2881 B b1107 t1106
2882 T t1107 o938 b1101 b1107
2883 B b1108 t1107
2884 T t1108 o738 b1017 b1032
2885 B b1109 t1108 v_5
2886 T t1109 o976 b1109
2887 S s1109 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2888 G s1109 t1109
2889 B b1110 s1109
2890 T t1110 o938 b1110 b1107
2891 B b1111 t1110
2892 S s1111 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2893 G s1111 t925
2894 B b1112 s1111
2895 T t1112 o938 b1112 b1107
2896 B b1113 t1112
2897 S s1113 t620 h h1096 h1091 h1097 h1098 h1099
2898 G s1113 t925
2899 B b1114 s1113
2900 T t1114 o938 b1114 b1107
2901 B b1115 t1114
2902 S s1115 t620 h h1096 h1091 h1097 h1098
2903 G s1115 t925
2904 B b1116 s1115
2905 T t1116 o938 b1116 b1107
2906 B b1117 t1116
2907 S s1117 t620 h h1096 h1091 h1097
2908 G s1117 t925
2909 B b1118 s1117
2910 T t1118 o938 b1118 b1107
2911 B b1119 t1118
2912 S s1119 t620 h h1096 h1091
2913 G s1119 t925
2914 B b1120 s1119
2915 T t1120 o938 b1120 b1107
2916 B b1121 t1120
2917 S s1121 t620 h h1096
2918 G s1121 t925
2919 B b1122 s1121
2920 T t1122 o938 b1122 b1107
2921 B b1123 t1122
2922 T t1123 o937 b1123 b4 b946
2923 B b1124 t1123
2924 T t1124 o2 b1124
2925 B b1125 t1124
2926 T t1125 o937 b1121 b4 b1125
2927 B b1126 t1125
2928 T t1126 o2 b1126
2929 B b1127 t1126
2930 T t1127 o937 b1119 b4 b1127
2931 B b1128 t1127
2932 T t1128 o2 b1128
2933 B b1129 t1128
2934 T t1129 o937 b1117 b4 b1129
2935 B b1130 t1129
2936 T t1130 o2 b1130
2937 B b1131 t1130
2938 T t1131 o937 b1115 b4 b1131
2939 B b1132 t1131
2940 T t1132 o2 b1132
2941 B b1133 t1132
2942 T t1133 o937 b1113 b4 b1133
2943 B b1134 t1133
2944 T t1134 o2 b1134
2945 B b1135 t1134
2946 T t1135 o973 b1111 b983 b1135
2947 B b1136 t1135
2948 T t1136 o2 b1136
2949 B b1137 t1136
2950 T t1137 o973 b1108 b4 b1137
2951 B b1138 t1137
2952 T t1138 o936 b1138 b4
2953 B b1139 t1138
2954 T t1139 o1050 b935 b1139 b4 b4
2955 B b1140 t1139
2956 T t1140 o b1140 b4
2957 B b1141 t1140
2958 T t1141 o1096 b935 b1095 b1096 b1141
2959 B b1142 t1141
2960 T t1142 o b1142 b4
2961 B b1143 t1142
2962 B b1144 t1017 v_4
2963 T t1144 o711 b1144
2964 S s1144 t620 h h1096 h1091 h1097 h1098 h1099
2965 G s1144 t1144
2966 B b1145 s1144
2967 T t1145 o938 b1145 b1107
2968 B b1146 t1145
2969 P p1146 Var v_4
2970 O o1146 var p1146
2971 T t1146 o1146
2972 B b1147 t1146
2973 T t1147 o738 b1147 b1018
2974 B b1148 t1147 v_4
2975 T t1148 o976 b1148
2976 S s1148 t620 h h1096 h1091 h1097 h1098 h1099
2977 G s1148 t1148
2978 B b1149 s1148
2979 T t1149 o938 b1149 b1107
2980 B b1150 t1149
2981 T t1150 o973 b1150 b983 b1133
2982 B b1151 t1150
2983 T t1151 o2 b1151
2984 B b1152 t1151
2985 T t1152 o973 b1146 b4 b1152
2986 B b1153 t1152
2987 T t1153 o936 b1153 b4
2988 B b1154 t1153
2989 T t1154 o1050 b935 b1154 b4 b4
2990 B b1155 t1154
2991 T t1155 o b1155 b4
2992 B b1156 t1155
2993 T t1156 o1024 b935 b1095 b1143 b1156
2994 B b1157 t1156
2995 T t1157 o b1157 b4
2996 B b1158 t1157
2997 T t1158 o1016 b935 b1095 b1158 b4
2998 B b1159 t1158
2999 T t1159 o b1159 b4
3000 B b1160 t1159
3001 S s1160 t620 h h1096 h1091 h1097
3002 G s1160 t994
3003 B b1161 s1160
3004 T t1161 o938 b1161 b1107
3005 B b1162 t1161
3006 T t1162 o966 b1162 b4 b1129
3007 B b1163 t1162
3008 T t1163 o936 b1163 b4
3009 B b1164 t1163
3010 T t1164 o990 b935 b1164 b4 b4
3011 B b1165 t1164
3012 P p1165 String "rwh unfold_fun_prop 0 thenT autoT"
3013 O o1165 ext_rule p1165
3014 T t1165 o738 b966 b977
3015 B b1166 t1165 v_2
3016 T t1166 o976 b1166
3017 S s1166 t620 h h1096 h1091 h1097
3018 G s1166 t1166
3019 B b1167 s1166
3020 T t1167 o938 b1167 b1107
3021 B b1168 t1167
3022 T t1168 o973 b1168 b4 b1129
3023 B b1169 t1168
3024 NCzf_itt_set!set set set Czf_itt_set
3025 O o1169 set
3026 T t1169 o1169
3027 H h1169 s1_1 t1169
3028 H h1170 s2_1 t1169
3029 P p1170 Var s1_1
3030 O o1170 var p1170
3031 T t1170 o1170
3032 B b1170 t1170
3033 P p1171 Var s2_1
3034 O o1171 var p1171
3035 T t1171 o1171
3036 B b1171 t1171
3037 T t1172 o738 b1170 b1171
3038 H h1172 x_1 t1172
3039 T t1173 o738 b966 b1170
3040 H h1173 x_2 t1173
3041 T t1174 o676 b966 b1171
3042 S s1174 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3043 G s1174 t1174
3044 B b1174 s1174
3045 T t1175 o938 b1174 b1107
3046 B b1175 t1175
3047 T t1176 o738 b966 b1171
3048 S s1176 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3049 G s1176 t1176
3050 B b1176 s1176
3051 T t1177 o938 b1176 b1107
3052 B b1177 t1177
3053 NItt_logic Itt_logic Itt_logic NIL
3054 NItt_logic!implies implies implies Itt_logic
3055 O o1177 implies
3056 B b1178 t1173
3057 B b1179 t1176
3058 T t1179 o1177 b1178 b1179
3059 S s1179 t620 h h1096 h1091 h1097 h1169 h1170 h1172
3060 G s1179 t1179
3061 B b1180 s1179
3062 T t1180 o938 b1180 b1107
3063 B b1181 t1180
3064 B b1182 t1172
3065 B b1183 t1179
3066 T t1183 o1177 b1182 b1183
3067 S s1183 t620 h h1096 h1091 h1097 h1169 h1170
3068 G s1183 t1183
3069 B b1184 s1183
3070 T t1184 o938 b1184 b1107
3071 B b1185 t1184
3072 NItt_logic!all all all Itt_logic
3073 O o1185 all
3074 B b1186 t1169
3075 B b1187 t1183 s2_1
3076 T t1187 o1185 b1186 b1187
3077 S s1187 t620 h h1096 h1091 h1097 h1169
3078 G s1187 t1187
3079 B b1188 s1187
3080 T t1188 o938 b1188 b1107
3081 B b1189 t1188
3082 B b1190 t1187 s1_1
3083 T t1190 o1185 b1186 b1190
3084 S s1190 t620 h h1096 h1091 h1097
3085 G s1190 t1190
3086 B b1191 s1190
3087 T t1191 o938 b1191 b1107
3088 B b1192 t1191
3089 T t1192 o2 b1169
3090 B b1193 t1192
3091 T t1193 o973 b1192 b983 b1193
3092 B b1194 t1193
3093 T t1194 o2 b1194
3094 B b1195 t1194
3095 T t1195 o937 b1189 b983 b1195
3096 B b1196 t1195
3097 T t1196 o2 b1196
3098 B b1197 t1196
3099 T t1197 o937 b1185 b983 b1197
3100 B b1198 t1197
3101 T t1198 o2 b1198
3102 B b1199 t1198
3103 T t1199 o937 b1181 b983 b1199
3104 B b1200 t1199
3105 T t1200 o2 b1200
3106 B b1201 t1200
3107 T t1201 o937 b1177 b983 b1201
3108 B b1202 t1201
3109 T t1202 o2 b1202
3110 B b1203 t1202
3111 T t1203 o937 b1175 b4 b1203
3112 B b1204 t1203
3113 T t1204 o b1204 b4
3114 B b1205 t1204
3115 T t1205 o936 b1169 b1205
3116 B b1206 t1205
3117 P p1206 String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3118 O o1206 ext_rule p1206
3119 T t1206 o936 b1204 b4
3120 B b1207 t1206
3121 T t1207 o1206 b935 b1207 b4 b4
3122 B b1208 t1207
3123 T t1208 o b1208 b4
3124 B b1209 t1208
3125 T t1209 o1165 b935 b1206 b1209 b4
3126 B b1210 t1209
3127 T t1210 o b1210 b4
3128 B b1211 t1210
3129 T t1211 o b1165 b1211
3130 B b1212 t1211
3131 T t1212 o1095 b935 b1095 b1160 b1212
3132 B b1213 t1212
3133 T t1213 o b1213 b4
3134 B b1214 t1213
3135 S s1214 t620 h h1096 h1091
3136 G s1214 t967
3137 B b1215 s1214
3138 T t1215 o938 b1215 b1107
3139 B b1216 t1215
3140 T t1216 o966 b1216 b4 b1127
3141 B b1217 t1216
3142 T t1217 o936 b1217 b4
3143 B b1218 t1217
3144 T t1218 o990 b935 b1218 b4 b4
3145 B b1219 t1218
3146 P p1219 Var v_1
3147 O o1219 var p1219
3148 T t1219 o1219
3149 B b1220 t1219
3150 T t1220 o738 b1220 b949
3151 B b1221 t1220 v_1
3152 T t1221 o976 b1221
3153 S s1221 t620 h h1096 h1091
3154 G s1221 t1221
3155 B b1222 s1221
3156 T t1222 o938 b1222 b1107
3157 B b1223 t1222
3158 T t1223 o973 b1223 b4 b1127
3159 B b1224 t1223
3160 H h1224 s2 t1169
3161 T t1224 o738 b1170 b561
3162 H h1225 x_1 t1224
3163 T t1225 o738 b1170 b949
3164 H h1226 x_2 t1225
3165 T t1226 o676 b561 b949
3166 S s1226 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3167 G s1226 t1226
3168 B b1226 s1226
3169 T t1227 o938 b1226 b1107
3170 B b1227 t1227
3171 T t1228 o738 b561 b949
3172 S s1228 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3173 G s1228 t1228
3174 B b1228 s1228
3175 T t1229 o938 b1228 b1107
3176 B b1229 t1229
3177 B b1230 t1225
3178 B b1231 t1228
3179 T t1231 o1177 b1230 b1231
3180 S s1231 t620 h h1096 h1091 h1169 h1224 h1225
3181 G s1231 t1231
3182 B b1232 s1231
3183 T t1232 o938 b1232 b1107
3184 B b1233 t1232
3185 B b1234 t1224
3186 B b1235 t1231
3187 T t1235 o1177 b1234 b1235
3188 S s1235 t620 h h1096 h1091 h1169 h1224
3189 G s1235 t1235
3190 B b1236 s1235
3191 T t1236 o938 b1236 b1107
3192 B b1237 t1236
3193 B b1238 t1235 s2
3194 T t1238 o1185 b1186 b1238
3195 S s1238 t620 h h1096 h1091 h1169
3196 G s1238 t1238
3197 B b1239 s1238
3198 T t1239 o938 b1239 b1107
3199 B b1240 t1239
3200 B b1241 t1238 s1_1
3201 T t1241 o1185 b1186 b1241
3202 S s1241 t620 h h1096 h1091
3203 G s1241 t1241
3204 B b1242 s1241
3205 T t1242 o938 b1242 b1107
3206 B b1243 t1242
3207 T t1243 o2 b1224
3208 B b1244 t1243
3209 T t1244 o973 b1243 b983 b1244
3210 B b1245 t1244
3211 T t1245 o2 b1245
3212 B b1246 t1245
3213 T t1246 o937 b1240 b983 b1246
3214 B b1247 t1246
3215 T t1247 o2 b1247
3216 B b1248 t1247
3217 T t1248 o937 b1237 b983 b1248
3218 B b1249 t1248
3219 T t1249 o2 b1249
3220 B b1250 t1249
3221 T t1250 o937 b1233 b983 b1250
3222 B b1251 t1250
3223 T t1251 o2 b1251
3224 B b1252 t1251
3225 T t1252 o937 b1229 b983 b1252
3226 B b1253 t1252
3227 T t1253 o2 b1253
3228 B b1254 t1253
3229 T t1254 o937 b1227 b4 b1254
3230 B b1255 t1254
3231 T t1255 o b1255 b4
3232 B b1256 t1255
3233 T t1256 o936 b1224 b1256
3234 B b1257 t1256
3235 P p1257 String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3236 O o1257 ext_rule p1257
3237 T t1257 o936 b1255 b4
3238 B b1258 t1257
3239 T t1258 o1257 b935 b1258 b4 b4
3240 B b1259 t1258
3241 T t1259 o b1259 b4
3242 B b1260 t1259
3243 T t1260 o1165 b935 b1257 b1260 b4
3244 B b1261 t1260
3245 T t1261 o b1261 b4
3246 B b1262 t1261
3247 T t1262 o b1219 b1262
3248 B b1263 t1262
3249 T t1263 o1091 b935 b1095 b1214 b1263
3250 B b1264 t1263
3251 P p1264 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3252 O o1264 ext_rule p1264
3253 H h1264 y_1 t642
3254 T t1264 o620 b695
3255 H h1265 z_1 t1264
3256 T t1265 o676 b562 b695
3257 H h1266 z t1265
3258 T t1266 o676 b948 b949
3259 H h1267 v t1266
3260 T t1267 o676 b561 b674
3261 S s1267 t620 h h1264 h1265 h1266 h1267
3262 G s1267 t1267
3263 B b1267 s1267
3264 T t1268 o938 b1267 b1107
3265 B b1268 t1268
3266 S s1268 t620 h h1264 h1265 h1266 h1267
3267 G s1268 t925
3268 B b1269 s1268
3269 T t1269 o938 b1269 b1107
3270 B b1270 t1269
3271 NItt_logic!and and and Itt_logic
3272 O o1270 and
3273 B b1271 t642
3274 B b1272 t1264
3275 T t1272 o1270 b1271 b1272
3276 H h1272 y t1272
3277 S s1272 t620 h h1272 h1266 h1267
3278 G s1272 t925
3279 B b1273 s1272
3280 T t1273 o938 b1273 b1107
3281 B b1274 t1273
3282 B b1275 t1272
3283 B b1276 t1265
3284 T t1276 o1270 b1275 b1276
3285 H h1276 x t1276
3286 S s1276 t620 h h1276 h1267
3287 G s1276 t925
3288 B b1277 s1276
3289 T t1277 o938 b1277 b1107
3290 B b1278 t1277
3291 S s1278 t620 h h1276
3292 G s1278 t925
3293 B b1279 s1278
3294 T t1279 o938 b1279 b1107
3295 B b1280 t1279
3296 T t1280 o937 b1280 b4 b1125
3297 B b1281 t1280
3298 T t1281 o2 b1281
3299 B b1282 t1281
3300 T t1282 o937 b1278 b4 b1282
3301 B b1283 t1282
3302 T t1283 o2 b1283
3303 B b1284 t1283
3304 T t1284 o937 b1274 b4 b1284
3305 B b1285 t1284
3306 T t1285 o2 b1285
3307 B b1286 t1285
3308 T t1286 o937 b1270 b983 b1286
3309 B b1287 t1286
3310 T t1287 o2 b1287
3311 B b1288 t1287
3312 T t1288 o937 b1268 b4 b1288
3313 B b1289 t1288
3314 T t1289 o676 b966 b949
3315 H h1289 v_1 t1289
3316 S s1289 t620 h h1264 h1265 h1266 h1267 h1289
3317 G s1289 t1267
3318 B b1290 s1289
3319 T t1290 o938 b1290 b1107
3320 B b1291 t1290
3321 T t1291 o2 b1289
3322 B b1292 t1291
3323 T t1292 o937 b1291 b4 b1292
3324 B b1293 t1292
3325 B b1294 t949 v_1
3326 T t1294 o711 b1294
3327 S s1294 t620 h h1264 h1265 h1266 h1267
3328 G s1294 t1294
3329 B b1295 s1294
3330 T t1295 o938 b1295 b1107
3331 B b1296 t1295
3332 T t1296 o676 b1220 b949
3333 B b1297 t1296 v_1
3334 T t1297 o976 b1297
3335 S s1297 t620 h h1264 h1265 h1266 h1267
3336 G s1297 t1297
3337 B b1298 s1297
3338 T t1298 o938 b1298 b1107
3339 B b1299 t1298
3340 T t1299 o973 b1299 b983 b1292
3341 B b1300 t1299
3342 T t1300 o2 b1300
3343 B b1301 t1300
3344 T t1301 o973 b1296 b4 b1301
3345 B b1302 t1301
3346 T t1302 o b1302 b4
3347 B b1303 t1302
3348 T t1303 o b1293 b1303
3349 B b1304 t1303
3350 T t1304 o936 b1289 b1304
3351 B b1305 t1304
3352 P p1305 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3353 O o1305 ext_rule p1305
3354 T t1305 o676 b966 b993
3355 H h1305 v_2 t1305
3356 S s1305 t620 h h1264 h1265 h1266 h1267 h1289 h1305
3357 G s1305 t1267
3358 B b1306 s1305
3359 T t1306 o938 b1306 b1107
3360 B b1307 t1306
3361 T t1307 o2 b1293
3362 B b1308 t1307
3363 T t1308 o937 b1307 b4 b1308
3364 B b1309 t1308
3365 B b1310 t966 v_2
3366 T t1310 o711 b1310
3367 S s1310 t620 h h1264 h1265 h1266 h1267 h1289
3368 G s1310 t1310
3369 B b1311 s1310
3370 T t1311 o938 b1311 b1107
3371 B b1312 t1311
3372 T t1312 o676 b966 b977
3373 B b1313 t1312 v_2
3374 T t1313 o976 b1313
3375 S s1313 t620 h h1264 h1265 h1266 h1267 h1289
3376 G s1313 t1313
3377 B b1314 s1313
3378 T t1314 o938 b1314 b1107
3379 B b1315 t1314
3380 T t1315 o973 b1315 b983 b1308
3381 B b1316 t1315
3382 T t1316 o2 b1316
3383 B b1317 t1316
3384 T t1317 o973 b1312 b4 b1317
3385 B b1318 t1317
3386 T t1318 o b1318 b4
3387 B b1319 t1318
3388 T t1319 o b1309 b1319
3389 B b1320 t1319
3390 T t1320 o936 b1293 b1320
3391 B b1321 t1320
3392 P p1321 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3393 O o1321 ext_rule p1321
3394 T t1321 o676 b1017 b1018
3395 H h1321 v_3 t1321
3396 S s1321 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3397 G s1321 t1267
3398 B b1322 s1321
3399 T t1322 o938 b1322 b1107
3400 B b1323 t1322
3401 T t1323 o2 b1309
3402 B b1324 t1323
3403 T t1324 o937 b1323 b4 b1324
3404 B b1325 t1324
3405 T t1325 o b1325 b4
3406 B b1326 t1325
3407 T t1326 o936 b1309 b1326
3408 B b1327 t1326
3409 P p1327 String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"
3410 O o1327 ext_rule p1327
3411 T t1327 o676 b561 b1018
3412 H h1327 v_4 t1327
3413 S s1327 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1327
3414 G s1327 t1267
3415 B b1328 s1327
3416 T t1328 o938 b1328 b1107
3417 B b1329 t1328
3418 T t1329 o2 b1325
3419 B b1330 t1329
3420 T t1330 o937 b1329 b4 b1330
3421 B b1331 t1330
3422 S s1331 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3423 G s1331 t1144
3424 B b1332 s1331
3425 T t1332 o938 b1332 b1107
3426 B b1333 t1332
3427 T t1333 o676 b1147 b1018
3428 B b1334 t1333 v_4
3429 T t1334 o976 b1334
3430 S s1334 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3431 G s1334 t1334
3432 B b1335 s1334
3433 T t1335 o938 b1335 b1107
3434 B b1336 t1335
3435 T t1336 o973 b1336 b983 b1330
3436 B b1337 t1336
3437 T t1337 o2 b1337
3438 B b1338 t1337
3439 T t1338 o973 b1333 b4 b1338
3440 B b1339 t1338
3441 T t1339 o b1339 b4
3442 B b1340 t1339
3443 T t1340 o b1331 b1340
3444 B b1341 t1340
3445 T t1341 o936 b1325 b1341
3446 B b1342 t1341
3447 P p1342 String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3448 O o1342 ext_rule p1342
3449 T t1342 o936 b1331 b4
3450 B b1343 t1342
3451 T t1343 o1342 b935 b1343 b4 b4
3452 B b1344 t1343
3453 H h1344 s1 t1169
3454 T t1344 o738 b560 b561
3455 H h1345 x t1344
3456 T t1345 o738 b1018 b1018
3457 S s1345 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344 h1224 h1345
3458 G s1345 t1345
3459 B b1345 s1345
3460 T t1346 o938 b1345 b1107
3461 B b1346 t1346
3462 B b1347 t1344
3463 B b1348 t1345
3464 T t1348 o1177 b1347 b1348
3465 S s1348 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344 h1224
3466 G s1348 t1348
3467 B b1349 s1348
3468 T t1349 o938 b1349 b1107
3469 B b1350 t1349
3470 B b1351 t1348 s2
3471 T t1351 o1185 b1186 b1351
3472 S s1351 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344
3473 G s1351 t1351
3474 B b1352 s1351
3475 T t1352 o938 b1352 b1107
3476 B b1353 t1352
3477 B b1354 t1351 s1
3478 T t1354 o1185 b1186 b1354
3479 S s1354 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3480 G s1354 t1354
3481 B b1355 s1354
3482 T t1355 o938 b1355 b1107
3483 B b1356 t1355
3484 T t1356 o2 b1339
3485 B b1357 t1356
3486 T t1357 o973 b1356 b983 b1357
3487 B b1358 t1357
3488 T t1358 o2 b1358
3489 B b1359 t1358
3490 T t1359 o937 b1353 b983 b1359
3491 B b1360 t1359
3492 T t1360 o2 b1360
3493 B b1361 t1360
3494 T t1361 o937 b1350 b983 b1361
3495 B b1362 t1361
3496 T t1362 o2 b1362
3497 B b1363 t1362
3498 T t1363 o937 b1346 b4 b1363
3499 B b1364 t1363
3500 T t1364 o b1364 b4
3501 B b1365 t1364
3502 T t1365 o936 b1339 b1365
3503 B b1366 t1365
3504 T t1366 o1085 b1364
3505 B b1367 t1366
3506 T t1367 o b1367 b4
3507 B b1368 t1367
3508 T t1368 o1071 b935 b1366 b1368 b4
3509 B b1369 t1368
3510 T t1369 o b1369 b4
3511 B b1370 t1369
3512 T t1370 o b1344 b1370
3513 B b1371 t1370
3514 T t1371 o1327 b935 b1342 b1371 b4
3515 B b1372 t1371
3516 T t1372 o b1372 b4
3517 B b1373 t1372
3518 T t1373 o1321 b935 b1327 b1373 b4
3519 B b1374 t1373
3520 T t1374 o936 b1318 b4
3521 B b1375 t1374
3522 T t1375 o1071 b935 b1375 b4 b4
3523 B b1376 t1375
3524 T t1376 o b1376 b4
3525 B b1377 t1376
3526 T t1377 o b1374 b1377
3527 B b1378 t1377
3528 P p1378 String "eqSetSymT thenT autoT"
3529 O o1378 ext_rule p1378
3530 T t1378 o676 b949 b993
3531 S s1378 t620 h h1264 h1265 h1266 h1267 h1289
3532 G s1378 t1378
3533 B b1379 s1378
3534 T t1379 o938 b1379 b1107
3535 B b1380 t1379
3536 S s1380 t620 h h1264 h1265 h1266 h1267 h1289
3537 G s1380 t994
3538 B b1381 s1380
3539 T t1381 o938 b1381 b1107
3540 B b1382 t1381
3541 T t1382 o966 b1382 b983 b1308
3542 B b1383 t1382
3543 T t1383 o2 b1383
3544 B b1384 t1383
3545 T t1384 o966 b1380 b4 b1384
3546 B b1385 t1384
3547 T t1385 o676 b993 b949
3548 S s1385 t620 h h1264 h1265 h1266 h1267 h1289
3549 G s1385 t1385
3550 B b1386 s1385
3551 T t1386 o938 b1386 b1107
3552 B b1387 t1386
3553 T t1387 o2 b1385
3554 B b1388 t1387
3555 T t1388 o966 b1387 b4 b1388
3556 B b1389 t1388
3557 T t1389 o b1389 b4
3558 B b1390 t1389
3559 T t1390 o936 b1385 b1390
3560 B b1391 t1390
3561 T t1391 o1085 b1389
3562 B b1392 t1391
3563 T t1392 o b1392 b4
3564 B b1393 t1392
3565 T t1393 o1378 b935 b1391 b1393 b4
3566 B b1394 t1393
3567 T t1394 o b1394 b4
3568 B b1395 t1394
3569 T t1395 o1305 b935 b1321 b1378 b1395
3570 B b1396 t1395
3571 T t1396 o936 b1302 b4
3572 B b1397 t1396
3573 T t1397 o1071 b935 b1397 b4 b4
3574 B b1398 t1397
3575 T t1398 o b1398 b4
3576 B b1399 t1398
3577 T t1399 o b1396 b1399
3578 B b1400 t1399
3579 T t1400 o676 b948 b966
3580 S s1400 t620 h h1264 h1265 h1266 h1267
3581 G s1400 t1400
3582 B b1401 s1400
3583 T t1401 o938 b1401 b1107
3584 B b1402 t1401
3585 S s1402 t620 h h1264 h1265 h1266 h1267
3586 G s1402 t967
3587 B b1403 s1402
3588 T t1403 o938 b1403 b1107
3589 B b1404 t1403
3590 T t1404 o966 b1404 b983 b1292
3591 B b1405 t1404
3592 T t1405 o2 b1405
3593 B b1406 t1405
3594 T t1406 o966 b1402 b4 b1406
3595 B b1407 t1406
3596 T t1407 o676 b966 b948
3597 S s1407 t620 h h1264 h1265 h1266 h1267
3598 G s1407 t1407
3599 B b1408 s1407
3600 T t1408 o938 b1408 b1107
3601 B b1409 t1408
3602 T t1409 o2 b1407
3603 B b1410 t1409
3604 T t1410 o966 b1409 b4 b1410
3605 B b1411 t1410
3606 T t1411 o b1411 b4
3607 B b1412 t1411
3608 T t1412 o936 b1407 b1412
3609 B b1413 t1412
3610 T t1413 o1085 b1411
3611 B b1414 t1413
3612 T t1414 o b1414 b4
3613 B b1415 t1414
3614 T t1415 o1378 b935 b1413 b1415 b4
3615 B b1416 t1415
3616 T t1416 o b1416 b4
3617 B b1417 t1416
3618 T t1417 o1264 b935 b1305 b1400 b1417
3619 B b1418 t1417
3620 T t1418 o b1418 b4
3621 B b1419 t1418
3622 T t1419 o b1264 b1419
3623 B b1420 t1419
3624 T t1420 o b1091 b1420
3625 B b1421 t1420
3626 T t1421 o934 b935 b963 b1085 b1421
3627 B b1422 t1421
3628 T t1422 o933 b1422
3629 B b1423 t1422
3630 P p1423 Number 5390
3631 P p1424 Number 5398
3632 O o1424 resource_defs p1423 p1424 p264
3633 P p1425 Number 5396
3634 O o1425 uid p1425 p1424
3635 T t1425 o1425 b626
3636 B b1425 t1425
3637 T t1426 o b1425 b4
3638 B b1426 t1426
3639 T t1427 o1424 b1426
3640 B b1427 t1427
3641 T t1428 o b1427 b4
3642 B b1428 t1428
3643 T t1429 o919 b922 b933 b1423 b1428
3644 B b1429 t1429
3645 T t1430 o918 b1429
3646 B b1430 t1430
3647 P p1430 Number 5838
3648 P p1431 Number 6264
3649 O o1431 location p1430 p1431
3650 P p1432 String cancel2
3651 O o1432 rule p1432
3652 T t1432 o920 b674
3653 B b1432 t1432
3654 T t1433 o b1432 b4
3655 B b1433 t1433
3656 T t1434 o b617 b1433
3657 B b1434 t1434
3658 T t1435 o738 b695 b696
3659 S s1435 t620 h
3660 G s1435 t1435
3661 B b1435 s1435
3662 T t1436 o618 b1435
3663 B b1436 t1436
3664 S s1436 t620 h
3665 G s1436 t1344
3666 B b1437 s1436
3667 T t1437 o618 b1437
3668 B b1438 t1437
3669 T t1438 o635 b1436 b1438
3670 B b1439 t1438
3671 T t1439 o635 b738 b1439
3672 B b1440 t1439
3673 T t1440 o635 b658 b1440
3674 B b1441 t1440
3675 T t1441 o635 b656 b1441
3676 B b1442 t1441
3677 T t1442 o635 b676 b1442
3678 B b1443 t1442
3679 T t1443 o635 b641 b1443
3680 B b1444 t1443
3681 T t1444 o635 b639 b1444
3682 B b1445 t1444
3683 P p1445 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"
3684 O o1445 ext_rule p1445
3685 T t1445 o b1435 b4
3686 B b1446 t1445
3687 T t1446 o b737 b1446
3688 B b1447 t1446
3689 T t1447 o b657 b1447
3690 B b1448 t1447
3691 T t1448 o b655 b1448
3692 B b1449 t1448
3693 T t1449 o b675 b1449
3694 B b1450 t1449
3695 T t1450 o b640 b1450
3696 B b1451 t1450
3697 T t1451 o b638 b1451
3698 B b1452 t1451
3699 T t1452 o938 b1437 b1452
3700 B b1453 t1452
3701 T t1453 o937 b1453 b4 b946
3702 B b1454 t1453
3703 H h1454 v t1435
3704 T t1454 o572 b674
3705 B b1455 t1454
3706 T t1455 o559 b695 b1455
3707 B b1456 t1455
3708 T t1456 o559 b696 b1455
3709 B b1457 t1456
3710 T t1457 o738 b1456 b1457
3711 S s1457 t620 h h1454
3712 G s1457 t1457
3713 B b1458 s1457
3714 T t1458 o938 b1458 b1452
3715 B b1459 t1458
3716 S s1459 t620 h h1454
3717 G s1459 t1344
3718 B b1460 s1459
3719 T t1460 o938 b1460 b1452
3720 B b1461 t1460
3721 T t1461 o2 b1454
3722 B b1462 t1461
3723 T t1462 o937 b1461 b4 b1462
3724 B b1463 t1462
3725 T t1463 o2 b1463
3726 B b1464 t1463
3727 T t1464 o947 b1459 b4 b1464
3728 B b1465 t1464
3729 H h1465 v_1 t1457
3730 S s1465 t620 h h1454 h1465
3731 G s1465 t1344
3732 B b1466 s1465
3733 T t1466 o938 b1466 b1452
3734 B b1467 t1466
3735 T t1467 o937 b1467 b4 b1464
3736 B b1468 t1467
3737 T t1468 o b1468 b4
3738 B b1469 t1468
3739 T t1469 o b1465 b1469
3740 B b1470 t1469
3741 T t1470 o936 b1454 b1470
3742 B b1471 t1470
3743 T t1471 o936 b1465 b4
3744 B b1472 t1471
3745 T t1472 o963 b935 b1472 b4 b4
3746 B b1473 t1472
3747 P p1473 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
3748 O o1473 ext_rule p1473
3749 T t1473 o559 b674 b1455
3750 B b1474 t1473
3751 T t1474 o559 b560 b1474
3752 B b1475 t1474
3753 T t1475 o738 b1475 b1457
3754 H h1475 v_2 t1475
3755 S s1475 t620 h h1454 h1465 h1475
3756 G s1475 t1344
3757 B b1476 s1475
3758 T t1476 o938 b1476 b1452
3759 B b1477 t1476
3760 T t1477 o2 b1468
3761 B b1478 t1477
3762 T t1478 o937 b1477 b4 b1478
3763 B b1479 t1478
3764 B b1480 t1456 v_2
3765 T t1480 o711 b1480
3766 S s1480 t620 h h1454 h1465
3767 G s1480 t1480
3768 B b1481 s1480
3769 T t1481 o938 b1481 b1452
3770 B b1482 t1481
3771 T t1482 o738 b977 b1457
3772 B b1483 t1482 v_2
3773 T t1483 o976 b1483
3774 S s1483 t620 h h1454 h1465
3775 G s1483 t1483
3776 B b1484 s1483
3777 T t1484 o938 b1484 b1452
3778 B b1485 t1484
3779 T t1485 o973 b1485 b983 b1478
3780 B b1486 t1485
3781 T t1486 o2 b1486
3782 B b1487 t1486
3783 T t1487 o973 b1482 b4 b1487
3784 B b1488 t1487
3785 T t1488 o b1488 b4
3786 B b1489 t1488
3787 T t1489 o b1479 b1489
3788 B b1490 t1489
3789 T t1490 o936 b1468 b1490
3790 B b1491 t1490
3791 P p1491 String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
3792 O o1491 ext_rule p1491
3793 T t1491 o559 b561 b1474
3794 B b1492 t1491
3795 T t1492 o738 b1475 b1492
3796 H h1492 v_3 t1492
3797 S s1492 t620 h h1454 h1465 h1475 h1492
3798 G s1492 t1344
3799 B b1493 s1492
3800 T t1493 o938 b1493 b1452
3801 B b1494 t1493
3802 T t1494 o2 b1479
3803 B b1495 t1494
3804 T t1495 o937 b1494 b4 b1495
3805 B b1496 t1495
3806 B b1497 t1474 v_3
3807 T t1497 o711 b1497
3808 S s1497 t620 h h1454 h1465 h1475
3809 G s1497 t1497
3810 B b1498 s1497
3811 T t1498 o938 b1498 b1452
3812 B b1499 t1498
3813 T t1499 o738 b1475 b1004
3814 B b1500 t1499 v_3
3815 T t1500 o976 b1500
3816 S s1500 t620 h h1454 h1465 h1475
3817 G s1500 t1500
3818 B b1501 s1500
3819 T t1501 o938 b1501 b1452
3820 B b1502 t1501
3821 T t1502 o973 b1502 b983 b1495
3822 B b1503 t1502
3823 T t1503 o2 b1503
3824 B b1504 t1503
3825 T t1504 o973 b1499 b4 b1504
3826 B b1505 t1504
3827 T t1505 o b1505 b4
3828 B b1506 t1505
3829 T t1506 o b1496 b1506
3830 B b1507 t1506
3831 T t1507 o936 b1479 b1507
3832 B b1508 t1507
3833 P p1508 String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
3834 O o1508 ext_rule p1508
3835 T t1508 o559 b560 b567
3836 B b1509 t1508
3837 T t1509 o559 b561 b567
3838 B b1510 t1509
3839 T t1510 o738 b1509 b1510
3840 H h1510 v_4 t1510
3841 S s1510 t620 h h1454 h1465 h1475 h1492 h1510
3842 G s1510 t1344
3843 B b1511 s1510
3844 T t1511 o938 b1511 b1452
3845 B b1512 t1511
3846 T t1512 o2 b1496
3847 B b1513 t1512
3848 T t1513 o937 b1512 b4 b1513
3849 B b1514 t1513
3850 T t1514 o b1514 b4
3851 B b1515 t1514
3852 T t1515 o936 b1496 b1515
3853 B b1516 t1515
3854 P p1516 String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
3855 O o1516 ext_rule p1516
3856 T t1516 o738 b560 b1510
3857 H h1516 v_5 t1516
3858 S s1516 t620 h h1454 h1465 h1475 h1492 h1510 h1516
3859 G s1516 t1344
3860 B b1517 s1516
3861 T t1517 o938 b1517 b1452
3862 B b1518 t1517
3863 T t1518 o2 b1514
3864 B b1519 t1518
3865 T t1519 o937 b1518 b4 b1519
3866 B b1520 t1519
3867 B b1521 t1509 v_5
3868 T t1521 o711 b1521
3869 S s1521 t620 h h1454 h1465 h1475 h1492 h1510
3870 G s1521 t1521
3871 B b1522 s1521
3872 T t1522 o938 b1522 b1452
3873 B b1523 t1522
3874 T t1523 o738 b1032 b1510
3875 B b1524 t1523 v_5
3876 T t1524 o976 b1524
3877 S s1524 t620 h h1454 h1465 h1475 h1492 h1510
3878 G s1524 t1524
3879 B b1525 s1524
3880 T t1525 o938 b1525 b1452
3881 B b1526 t1525
3882 T t1526 o973 b1526 b983 b1519
3883 B b1527 t1526
3884 T t1527 o2 b1527
3885 B b1528 t1527
3886 T t1528 o973 b1523 b4 b1528
3887 B b1529 t1528
3888 T t1529 o b1529 b4
3889 B b1530 t1529
3890 T t1530 o b1520 b1530
3891 B b1531 t1530
3892 T t1531 o936 b1514 b1531
3893 B b1532 t1531
3894 P p1532 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3895 O o1532 ext_rule p1532
3896 T t1532 o936 b1520 b4
3897 B b1533 t1532
3898 T t1533 o1532 b935 b1533 b4 b4
3899 B b1534 t1533
3900 T t1534 o936 b1529 b4
3901 B b1535 t1534
3902 T t1535 o1050 b935 b1535 b4 b4
3903 B b1536 t1535
3904 T t1536 o b1536 b4
3905 B b1537 t1536
3906 T t1537 o b1534 b1537
3907 B b1538 t1537
3908 T t1538 o1516 b935 b1532 b1538 b4
3909 B b1539 t1538
3910 T t1539 o b1539 b4
3911 B b1540 t1539
3912 T t1540 o1508 b935 b1516 b1540 b4
3913 B b1541 t1540
3914 T t1541 o936 b1505 b4
3915 B b1542 t1541
3916 T t1542 o1050 b935 b1542 b4 b4
3917 B b1543 t1542
3918 T t1543 o b1543 b4
3919 B b1544 t1543
3920 T t1544 o b1541 b1544
3921 B b1545 t1544
3922 T t1545 o1491 b935 b1508 b1545 b4
3923 B b1546 t1545
3924 T t1546 o936 b1488 b4
3925 B b1547 t1546
3926 T t1547 o1050 b935 b1547 b4 b4
3927 B b1548 t1547
3928 T t1548 o b1548 b4
3929 B b1549 t1548
3930 T t1549 o b1546 b1549
3931 B b1550 t1549
3932 T t1550 o1473 b935 b1491 b1550 b4
3933 B b1551 t1550
3934 T t1551 o b1551 b4
3935 B b1552 t1551
3936 T t1552 o b1473 b1552
3937 B b1553 t1552
3938 S s1553 t620 h
3939 G s1553 t1457
3940 B b1554 s1553
3941 T t1554 o938 b1554 b1452
3942 B b1555 t1554
3943 T t1555 o947 b1555 b4 b1462
3944 B b1556 t1555
3945 T t1556 o1085 b1556
3946 B b1557 t1556
3947 T t1557 o b1557 b4
3948 B b1558 t1557
3949 T t1558 o963 b935 b1557 b1558 b4
3950 B b1559 t1558
3951 H h1559 v t1457
3952 S s1559 t620 h h1559
3953 G s1559 t1344
3954 B b1560 s1559
3955 T t1560 o938 b1560 b1452
3956 B b1561 t1560
3957 T t1561 o937 b1561 b4 b1462
3958 B b1562 t1561
3959 T t1562 o1085 b1562
3960 B b1563 t1562
3961 T t1563 o b1563 b4
3962 B b1564 t1563
3963 T t1564 o1532 b935 b1563 b1564 b4
3964 B b1565 t1564
3965 T t1565 o b1565 b4
3966 B b1566 t1565
3967 H h1566 x t1435
3968 H h1567 v_1 t1475
3969 H h1568 v_2 t1492
3970 H h1569 v_3 t1510
3971 B b1569 t1509 v_4
3972 T t1569 o711 b1569
3973 S s1569 t620 h h1566 h1559 h1567 h1568 h1569
3974 G s1569 t1569
3975 B b1570 s1569
3976 T t1570 o938 b1570 b1107
3977 B b1571 t1570
3978 T t1571 o738 b1147 b1510
3979 B b1572 t1571 v_4
3980 T t1572 o976 b1572
3981 S s1572 t620 h h1566 h1559 h1567 h1568 h1569
3982 G s1572 t1572
3983 B b1573 s1572
3984 T t1573 o938 b1573 b1107
3985 B b1574 t1573
3986 S s1574 t620 h h1566 h1559 h1567 h1568 h1569
3987 G s1574 t1344
3988 B b1575 s1574
3989 T t1575 o938 b1575 b1107
3990 B b1576 t1575
3991 S s1576 t620 h h1566 h1559 h1567 h1568
3992 G s1576 t1344
3993 B b1577 s1576
3994 T t1577 o938 b1577 b1107
3995 B b1578 t1577
3996 S s1578 t620 h h1566 h1559 h1567
3997 G s1578 t1344
3998 B b1579 s1578
3999 T t1579 o938 b1579 b1107
4000 B b1580 t1579
4001 S s1580 t620 h h1566 h1559
4002 G s1580 t1344
4003 B b1581 s1580
4004 T t1581 o938 b1581 b1107
4005 B b1582 t1581
4006 S s1582 t620 h h1566
4007 G s1582 t1344
4008 B b1583 s1582
4009 T t1583 o938 b1583 b1107
4010 B b1584 t1583
4011 T t1584 o937 b1584 b4 b946
4012 B b1585 t1584
4013 T t1585 o2 b1585
4014 B b1586 t1585
4015 T t1586 o937 b1582 b4 b1586
4016 B b1587 t1586
4017 T t1587 o2 b1587
4018 B b1588 t1587
4019 T t1588 o937 b1580 b4 b1588
4020 B b1589 t1588
4021 T t1589 o2 b1589
4022 B b1590 t1589
4023 T t1590 o937 b1578 b4 b1590
4024 B b1591 t1590
4025 T t1591 o2 b1591
4026 B b1592 t1591
4027 T t1592 o937 b1576 b4 b1592
4028 B b1593 t1592
4029 T t1593 o2 b1593
4030 B b1594 t1593
4031 T t1594 o973 b1574 b983 b1594
4032 B b1595 t1594
4033 T t1595 o2 b1595
4034 B b1596 t1595
4035 T t1596 o973 b1571 b4 b1596
4036 B b1597 t1596
4037 T t1597 o936 b1597 b4
4038 B b1598 t1597
4039 T t1598 o1050 b935 b1598 b4 b4
4040 B b1599 t1598
4041 T t1599 o b1599 b4
4042 B b1600 t1599
4043 T t1600 o1516 b935 b1563 b1566 b1600
4044 B b1601 t1600
4045 T t1601 o b1601 b4
4046 B b1602 t1601
4047 T t1602 o1508 b935 b1563 b1602 b4
4048 B b1603 t1602
4049 T t1603 o b1603 b4
4050 B b1604 t1603
4051 P p1604 String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
4052 O o1604 ext_rule p1604
4053 B b1605 t1474 v_2
4054 T t1605 o711 b1605
4055 S s1605 t620 h h1566 h1559 h1567
4056 G s1605 t1605
4057 B b1606 s1605
4058 T t1606 o938 b1606 b1107
4059 B b1607 t1606
4060 T t1607 o738 b1475 b977
4061 B b1608 t1607 v_2
4062 T t1608 o976 b1608
4063 S s1608 t620 h h1566 h1559 h1567
4064 G s1608 t1608
4065 B b1609 s1608
4066 T t1609 o938 b1609 b1107
4067 B b1610 t1609
4068 T t1610 o973 b1610 b983 b1590
4069 B b1611 t1610
4070 T t1611 o2 b1611
4071 B b1612 t1611
4072 T t1612 o973 b1607 b4 b1612
4073 B b1613 t1612
4074 T t1613 o936 b1613 b4
4075 B b1614 t1613
4076 T t1614 o1604 b935 b1614 b4 b4
4077 B b1615 t1614
4078 T t1615 o b1615 b4
4079 B b1616 t1615
4080 T t1616 o1491 b935 b1563 b1604 b1616
4081 B b1617 t1616
4082 T t1617 o b1617 b4
4083 B b1618 t1617
4084 B b1619 t1456 v_1
4085 T t1619 o711 b1619
4086 S s1619 t620 h h1566 h1559
4087 G s1619 t1619
4088 B b1620 s1619
4089 T t1620 o938 b1620 b1107
4090 B b1621 t1620
4091 T t1621 o738 b1220 b1457
4092 B b1622 t1621 v_1
4093 T t1622 o976 b1622
4094 S s1622 t620 h h1566 h1559
4095 G s1622 t1622
4096 B b1623 s1622
4097 T t1623 o938 b1623 b1107
4098 B b1624 t1623
4099 T t1624 o973 b1624 b983 b1588
4100 B b1625 t1624
4101 T t1625 o2 b1625
4102 B b1626 t1625
4103 T t1626 o973 b1621 b4 b1626
4104 B b1627 t1626
4105 T t1627 o936 b1627 b4
4106 B b1628 t1627
4107 T t1628 o1604 b935 b1628 b4 b4
4108 B b1629 t1628
4109 T t1629 o b1629 b4
4110 B b1630 t1629
4111 T t1630 o1473 b935 b1563 b1618 b1630
4112 B b1631 t1630
4113 T t1631 o b1631 b4
4114 B b1632 t1631
4115 T t1632 o b1559 b1632
4116 B b1633 t1632
4117 T t1633 o1445 b935 b1471 b1553 b1633
4118 B b1634 t1633
4119 T t1634 o933 b1634
4120 B b1635 t1634
4121 P p1635 Number 5861
4122 P p1636 Number 5869
4123 O o1636 resource_defs p1635 p1636 p264
4124 P p1637 Number 5867
4125 O o1637 uid p1637 p1636
4126 T t1637 o1637 b626
4127 B b1637 t1637
4128 T t1638 o b1637 b4
4129 B b1638 t1638
4130 T t1639 o1636 b1638
4131 B b1639 t1639
4132 T t1640 o b1639 b4
4133 B b1640 t1640
4134 T t1641 o1432 b1434 b1445 b1635 b1640
4135 B b1641 t1641
4136 T t1642 o1431 b1641
4137 B b1642 t1642
4138 P p1642 Number 6266
4139 P p1643 Number 6335
4140 O o1643 location p1642 p1643
4141 O o1644 str_let p1642 p1643
4142 P p1644 Number 6270
4143 O o1645 patt_var p1644 p1643
4144 O o1646 patt_done p1642 p1643
4145 T t1646 o1646
4146 B b1646 t1646 groupCancelLeftT
4147 T t1647 o1645 b1646
4148 B b1647 t1647
4149 O o1647 fun p1644 p1643
4150 O o1648 patt_if p1644 p1643
4151 P p1648 Number 6287
4152 P p1649 Number 6288
4153 O o1649 patt_var p1648 p1649
4154 O o1650 patt_body p1644 p1643
4155 P p1650 Number 6289
4156 P p1651 Number 6290
4157 O o1651 patt_var p1650 p1651
4158 P p1652 Number 6296
4159 O o1652 apply p1652 p1643
4160 P p1653 Number 6333
4161 O o1653 apply p1652 p1653
4162 P p1654 Number 6331
4163 O o1654 apply p1652 p1654
4164 P p1655 Number 6303
4165 O o1655 lid p1652 p1655
4166 O o1656 lid p919
4167 T t1656 o1656
4168 B b1656 t1656
4169 T t1657 o1655 b1656
4170 B b1657 t1657
4171 P p1657 Number 6305
4172 P p1658 Number 6330
4173 O o1658 apply p1657 p1658
4174 P p1659 Number 6328
4175 O o1659 proj p1657 p1659
4176 O o1660 uid p1657 p1659
4177 T t1660 o1660 b836
4178 B b1660 t1660
4179 P p1660 Number 6314
4180 O o1661 lid p1660 p1659
4181 T t1661 o1661 b838
4182 B b1661 t1661
4183 T t1662 o1659 b1660 b1661
4184 B b1662 t1662
4185 P p1662 Number 6329
4186 O o1662 lid p1662 p1658
4187 T t1663 o1662 b841
4188 B b1663 t1663
4189 T t1664 o1658 b1662 b1663
4190 B b1664 t1664
4191 T t1665 o1654 b1657 b1664
4192 B b1665 t1665
4193 P p1665 Number 6332
4194 O o1665 lid p1665 p1653
4195 P p1666 Var t
4196 O o1666 var p1666
4197 T t1666 o1666
4198 B b1666 t1666
4199 T t1667 o1665 b1666
4200 B b1667 t1667
4201 T t1668 o1653 b1665 b1667
4202 B b1668 t1668
4203 P p1668 Number 6334
4204 O o1668 lid p1668 p1643
4205 T t1669 o1668 b841
4206 B b1669 t1669
4207 T t1670 o1652 b1668 b1669
4208 B b1670 t1670
4209 T t1671 o1650 b1670
4210 B b1671 t1671 p
4211 T t1672 o1651 b1671
4212 B b1672 t1672
4213 T t1673 o1648 b1672
4214 B b1673 t1673
4215 T t1674 o1647 b1673
4216 B b1674 t1674
4217 T t1675 o1650 b1674
4218 B b1675 t1675 t
4219 T t1676 o1649 b1675
4220 B b1676 t1676
4221 T t1677 o1648 b1676
4222 B b1677 t1677
4223 T t1678 o1647 b1677
4224 B b1678 t1678
4225 T t1679 o1644 b1647 b1678
4226 B b1679 t1679
4227 T t1680 o b1679 b4
4228 B b1680 t1680
4229 T t1681 o1644 b1680
4230 B b1681 t1681
4231 T t1682 o392 b1681
4232 B b1682 t1682
4233 T t1683 o1643 b1682
4234 B b1683 t1683
4235 P p1683 Number 6337
4236 P p1684 Number 6407
4237 O o1684 location p1683 p1684
4238 O o1685 str_let p1683 p1684
4239 P p1685 Number 6341
4240 O o1686 patt_var p1685 p1684
4241 O o1687 patt_done p1683 p1684
4242 T t1687 o1687
4243 B b1687 t1687 groupCancelRightT
4244 T t1688 o1686 b1687
4245 B b1688 t1688
4246 O o1688 fun p1685 p1684
4247 O o1689 patt_if p1685 p1684
4248 P p1689 Number 6359
4249 P p1690 Number 6360
4250 O o1690 patt_var p1689 p1690
4251 O o1691 patt_body p1685 p1684
4252 P p1691 Number 6361
4253 P p1692 Number 6362
4254 O o1692 patt_var p1691 p1692
4255 P p1693 Number 6368
4256 O o1693 apply p1693 p1684
4257 P p1694 Number 6405
4258 O o1694 apply p1693 p1694
4259 P p1695 Number 6403
4260 O o1695 apply p1693 p1695
4261 P p1696 Number 6375
4262 O o1696 lid p1693 p1696
4263 O o1697 lid p1432
4264 T t1697 o1697
4265 B b1697 t1697
4266 T t1698 o1696 b1697
4267 B b1698 t1698
4268 P p1698 Number 6377
4269 P p1699 Number 6402
4270 O o1699 apply p1698 p1699
4271 P p1700 Number 6400
4272 O o1700 proj p1698 p1700
4273 O o1701 uid p1698 p1700
4274 T t1701 o1701 b836
4275 B b1701 t1701
4276 P p1701 Number 6386
4277 O o1702 lid p1701 p1700
4278 T t1702 o1702 b838
4279 B b1702 t1702
4280 T t1703 o1700 b1701 b1702
4281 B b1703 t1703
4282 P p1703 Number 6401
4283 O o1703 lid p1703 p1699
4284 T t1704 o1703 b841
4285 B b1704 t1704
4286 T t1705 o1699 b1703 b1704
4287 B b1705 t1705
4288 T t1706 o1695 b1698 b1705
4289 B b1706 t1706
4290 P p1706 Number 6404
4291 O o1706 lid p1706 p1694
4292 T t1707 o1706 b1666
4293 B b1707 t1707
4294 T t1708 o1694 b1706 b1707
4295 B b1708 t1708
4296 P p1708 Number 6406
4297 O o1708 lid p1708 p1684
4298 T t1709 o1708 b841
4299 B b1709 t1709
4300 T t1710 o1693 b1708 b1709
4301 B b1710 t1710
4302 T t1711 o1691 b1710
4303 B b1711 t1711 p
4304 T t1712 o1692 b1711
4305 B b1712 t1712
4306 T t1713 o1689 b1712
4307 B b1713 t1713
4308 T t1714 o1688 b1713
4309 B b1714 t1714
4310 T t1715 o1691 b1714
4311 B b1715 t1715 t
4312 T t1716 o1690 b1715
4313 B b1716 t1716
4314 T t1717 o1689 b1716
4315 B b1717 t1717
4316 T t1718 o1688 b1717
4317 B b1718 t1718
4318 T t1719 o1685 b1688 b1718
4319 B b1719 t1719
4320 T t1720 o b1719 b4
4321 B b1720 t1720
4322 T t1721 o1685 b1720
4323 B b1721 t1721
4324 T t1722 o392 b1721
4325 B b1722 t1722
4326 T t1723 o1684 b1722
4327 B b1723 t1723
4328 P p1723 Number 6425
4329 P p1724 Number 6666
4330 O o1724 location p1723 p1724
4331 P p1725 String unique_id1
4332 O o1725 rule p1725
4333 P p1726 Var e2
4334 O o1726 var p1726
4335 T t1726 o1726
4336 B b1726 t1726
4337 T t1727 o620 b1726
4338 S s1727 t637 h
4339 G s1727 t1727
4340 B b1727 s1727
4341 T t1728 o618 b1727
4342 B b1728 t1728
4343 T t1729 o655 b1726 b554
4344 S s1729 t620 h
4345 G s1729 t1729
4346 B b1729 s1729
4347 T t1730 o618 b1729
4348 B b1730 t1730
4349 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4350 NCzf_itt_dall!dall dall dall Czf_itt_dall
4351 O o1730 dall
4352 T t1731 o559 b1726 b573
4353 B b1731 t1731
4354 T t1732 o676 b1731 b573
4355 B b1732 t1732
4356 T t1733 o559 b573 b1726
4357 B b1733 t1733
4358 T t1734 o676 b1733 b573
4359 B b1734 t1734
4360 T t1735 o1270 b1732 b1734
4361 B b1735 t1735 s
4362 T t1736 o1730 b554 b1735
4363 H h1736 x t1736
4364 T t1737 o676 b1726 b567
4365 S s1737 t620 h h1736
4366 G s1737 t1737
4367 B b1737 s1737
4368 T t1738 o618 b1737
4369 B b1738 t1738
4370 T t1739 o635 b1730 b1738
4371 B b1739 t1739
4372 T t1740 o635 b1728 b1739
4373 B b1740 t1740
4374 P p1740 String "withT << id >> (dT 2) thenT autoT"
4375 O o1740 ext_rule p1740
4376 T t1741 o b1729 b4
4377 B b1741 t1741
4378 T t1742 o b1727 b1741
4379 B b1742 t1742
4380 T t1743 o938 b1737 b1742
4381 B b1743 t1743
4382 T t1744 o937 b1743 b4 b946
4383 B b1744 t1744
4384 T t1745 o559 b1726 b567
4385 B b1745 t1745
4386 T t1746 o676 b1745 b567
4387 H h1746 y t1746
4388 T t1747 o559 b567 b1726
4389 B b1747 t1747
4390 T t1748 o676 b1747 b567
4391 H h1748 z t1748
4392 S s1748 t620 h h1736 h1746 h1748
4393 G s1748 t1737
4394 B b1748 s1748
4395 T t1749 o938 b1748 b1742
4396 B b1749 t1749
4397 B b1750 t1746
4398 B b1751 t1748
4399 T t1751 o1270 b1750 b1751
4400 H h1751 w t1751
4401 S s1751 t620 h h1736 h1751
4402 G s1751 t1737
4403 B b1752 s1751
4404 T t1752 o938 b1752 b1742
4405 B b1753 t1752
4406 P p1753 String with
4407 O o1753 arg_named p1753
4408 NSummary!arg_term_list arg_term_list arg_term_list Summary
4409 O o1754 arg_term_list
4410 T t1754 o b567 b4
4411 B b1754 t1754
4412 T t1755 o1754 b1754
4413 B b1755 t1755
4414 T t1756 o1753 b1755
4415 B b1756 t1756
4416 T t1757 o b1756 b4
4417 B b1757 t1757
4418 T t1758 o937 b1743 b1757 b946
4419 B b1758 t1758
4420 T t1759 o2 b1758
4421 B b1759 t1759
4422 T t1760 o937 b1753 b4 b1759
4423 B b1760 t1760
4424 T t1761 o2 b1760
4425 B b1761 t1761
4426 T t1762 o937 b1749 b4 b1761
4427 B b1762 t1762
4428 T t1763 o b1762 b4
4429 B b1763 t1763
4430 T t1764 o936 b1744 b1763
4431 B b1764 t1764
4432 P p1764 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
4433 O o1764 ext_rule p1764
4434 T t1765 o936 b1762 b4
4435 B b1765 t1765
4436 T t1766 o1764 b935 b1765 b4 b4
4437 B b1766 t1766
4438 T t1767 o b1766 b4
4439 B b1767 t1767
4440 S s1767 t620 h
4441 G s1767 t1727
4442 B b1768 s1767
4443 T t1768 o b1768 b1741
4444 B b1769 t1768
4445 T t1769 o938 b1748 b1769
4446 B b1770 t1769
4447 T t1770 o938 b1752 b1769
4448 B b1771 t1770
4449 T t1771 o938 b1737 b1769
4450 B b1772 t1771
4451 T t1772 o937 b1772 b1757 b946
4452 B b1773 t1772
4453 T t1773 o2 b1773
4454 B b1774 t1773
4455 T t1774 o937 b1771 b4 b1774
4456 B b1775 t1774
4457 T t1775 o2 b1775
4458 B b1776 t1775
4459 T t1776 o937 b1770 b4 b1776
4460 B b1777 t1776
4461 T t1777 o936 b1777 b4
4462 B b1778 t1777
4463 T t1778 o1764 b935 b1778 b4 b4
4464 B b1779 t1778
4465 P p1779 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
4466 O o1779 ext_rule p1779
4467 H h1779 v t1737
4468 S s1779 t620 h h1736 h1746 h1748 h1779
4469 G s1779 t1737
4470 B b1780 s1779
4471 T t1780 o938 b1780 b1769
4472 B b1781 t1780
4473 T t1781 o2 b1777
4474 B b1782 t1781
4475 T t1782 o937 b1781 b4 b1782
4476 B b1783 t1782
4477 T t1783 o b1783 b4
4478 B b1784 t1783
4479 T t1784 o936 b1777 b1784
4480 B b1785 t1784
4481 T t1785 o1085 b1783
4482 B b1786 t1785
4483 T t1786 o b1786 b4
4484 B b1787 t1786
4485 T t1787 o1779 b935 b1785 b1787 b4
4486 B b1788 t1787
4487 P p1788 String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
4488 O o1788 ext_rule p1788
4489 P p1789 Var e
4490 O o1789 var p1789
4491 T t1789 o1789
4492 B b1789 t1789
4493 T t1790 o620 b1789
4494 S s1790 t637 h h1736 h1746 h1748
4495 G s1790 t1790
4496 B b1790 s1790
4497 T t1791 o938 b1790 b1769
4498 B b1791 t1791
4499 T t1792 o559 b1726 b1789
4500 B b1792 t1792
4501 T t1793 o620 b1792
4502 S s1793 t637 h h1736 h1746 h1748
4503 G s1793 t1793
4504 B b1793 s1793
4505 T t1794 o938 b1793 b1769
4506 B b1794 t1794
4507 T t1795 o738 b1792 b1726
4508 S s1795 t620 h h1736 h1746 h1748
4509 G s1795 t1795
4510 B b1795 s1795
4511 T t1796 o938 b1795 b1769
4512 B b1796 t1796
4513 T t1797 o966 b1796 b983 b1782
4514 B b1797 t1797
4515 T t1798 o2 b1797
4516 B b1798 t1798
4517 T t1799 o973 b1794 b983 b1798
4518 B b1799 t1799
4519 T t1800 o2 b1799
4520 B b1800 t1800
4521 T t1801 o973 b1791 b4 b1800
4522 B b1801 t1801
4523 T t1802 o676 b1792 b1726
4524 S s1802 t620 h h1736 h1746 h1748
4525 G s1802 t1802
4526 B b1802 s1802
4527 T t1803 o938 b1802 b1769
4528 B b1803 t1803
4529 T t1804 o966 b1803 b4 b1798
4530 B b1804 t1804
4531 H h1804 v t1746
4532 S s1804 t620 h h1736 h1746 h1748 h1804
4533 G s1804 t1737
4534 B b1805 s1804
4535 T t1805 o938 b1805 b1769
4536 B b1806 t1805
4537 T t1806 o937 b1806 b4 b1782
4538 B b1807 t1806
4539 B b1808 t1745 v
4540 T t1808 o711 b1808
4541 S s1808 t620 h h1736 h1746 h1748
4542 G s1808 t1808
4543 B b1809 s1808
4544 T t1809 o938 b1809 b1769
4545 B b1810 t1809
4546 B b1811 t1746 v
4547 T t1811 o976 b1811
4548 S s1811 t620 h h1736 h1746 h1748
4549 G s1811 t1811
4550 B b1812 s1811
4551 T t1812 o938 b1812 b1769
4552 B b1813 t1812
4553 T t1813 o973 b1813 b983 b1782
4554 B b1814 t1813
4555 T t1814 o2 b1814
4556 B b1815 t1814
4557 T t1815 o973 b1810 b4 b1815
4558 B b1816 t1815
4559 T t1816 o b1816 b4
4560 B b1817 t1816
4561 T t1817 o b1807 b1817
4562 B b1818 t1817
4563 T t1818 o b1804 b1818
4564 B b1819 t1818
4565 T t1819 o b1801 b1819
4566 B b1820 t1819
4567 T t1820 o936 b1777 b1820
4568 B b1821 t1820
4569 T t1821 o1085 b1801
4570 B b1822 t1821
4571 T t1822 o1085 b1804
4572 B b1823 t1822
4573 T t1823 o1085 b1807
4574 B b1824 t1823
4575 T t1824 o1085 b1816
4576 B b1825 t1824
4577 T t1825 o b1825 b4
4578 B b1826 t1825
4579 T t1826 o b1824 b1826
4580 B b1827 t1826
4581 T t1827 o b1823 b1827
4582 B b1828 t1827
4583 T t1828 o b1822 b1828
4584 B b1829 t1828
4585 T t1829 o1788 b935 b1821 b1829 b4
4586 B b1830 t1829
4587 T t1830 o b1830 b4
4588 B b1831 t1830
4589 T t1831 o b1830 b1831
4590 B b1832 t1831
4591 T t1832 o b1788 b1832
4592 B b1833 t1832
4593 T t1833 o b1779 b1833
4594 B b1834 t1833
4595 T t1834 o1740 b935 b1764 b1767 b1834
4596 B b1835 t1834
4597 T t1835 o933 b1835
4598 B b1836 t1835
4599 P p1836 Number 6451
4600 P p1837 Number 6459
4601 O o1837 resource_defs p1836 p1837 p264
4602 P p1838 Number 6457
4603 O o1838 uid p1838 p1837
4604 T t1838 o1838 b626
4605 B b1838 t1838
4606 T t1839 o b1838 b4
4607 B b1839 t1839
4608 T t1840 o1837 b1839
4609 B b1840 t1840
4610 T t1841 o b1840 b4
4611 B b1841 t1841
4612 T t1842 o1725 b618 b1740 b1836 b1841
4613 B b1842 t1842
4614 T t1843 o1724 b1842
4615 B b1843 t1843
4616 P p1843 Number 6981
4617 P p1844 Number 7305
4618 O o1844 location p1843 p1844
4619 P p1845 String unique_inv
4620 O o1845 rule p1845
4621 T t1845 o559 b561 b573
4622 B b1845 t1845
4623 T t1846 o738 b1845 b567
4624 H h1846 x t1846
4625 T t1847 o559 b573 b561
4626 B b1847 t1847
4627 T t1848 o738 b1847 b567
4628 H h1848 y t1848
4629 T t1849 o738 b561 b574
4630 S s1849 t620 h h1846 h1848
4631 G s1849 t1849
4632 B b1849 s1849
4633 T t1850 o618 b1849
4634 B b1850 t1850
4635 T t1851 o635 b658 b1850
4636 B b1851 t1851
4637 T t1852 o635 b794 b1851
4638 B b1852 t1852
4639 T t1853 o635 b641 b1852
4640 B b1853 t1853
4641 T t1854 o635 b711 b1853
4642 B b1854 t1854
4643 P p1854 String "assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
4644 O o1854 ext_rule p1854
4645 T t1855 o b657 b4
4646 B b1855 t1855
4647 T t1856 o b793 b1855
4648 B b1856 t1856
4649 T t1857 o b640 b1856
4650 B b1857 t1857
4651 T t1858 o b710 b1857
4652 B b1858 t1858
4653 T t1859 o938 b1849 b1858
4654 B b1859 t1859
4655 T t1860 o937 b1859 b4 b946
4656 B b1860 t1860
4657 T t1861 o559 b574 b573
4658 B b1861 t1861
4659 T t1862 o738 b1861 b567
4660 H h1862 v t1862
4661 S s1862 t620 h h1846 h1848 h1862
4662 G s1862 t1849
4663 B b1862 s1862
4664 T t1863 o938 b1862 b1858
4665 B b1863 t1863
4666 T t1864 o2 b1860
4667 B b1864 t1864
4668 T t1865 o937 b1863 b4 b1864
4669 B b1865 t1865
4670 T t1866 o b1865 b4
4671 B b1866 t1866
4672 T t1867 o936 b1860 b1866
4673 B b1867 t1867
4674 P p1867 String "setSubstT << equal{id; op{inv{'s}; 's}} >> 2 thenAT autoT"
4675 O o1867 ext_rule p1867
4676 T t1868 o676 b567 b1861
4677 S s1868 t620 h h1846 h1848 h1862
4678 G s1868 t1868
4679 B b1868 s1868
4680 T t1869 o938 b1868 b1858
4681 B b1869 t1869
4682 T t1870 o738 b567 b1861
4683 S s1870 t620 h h1846 h1848 h1862
4684 G s1870 t1870
4685 B b1870 s1870
4686 T t1871 o938 b1870 b1858
4687 B b1871 t1871
4688 T t1872 o2 b1865
4689 B b1872 t1872
4690 T t1873 o966 b1871 b983 b1872
4691 B b1873 t1873
4692 T t1874 o2 b1873
4693 B b1874 t1874
4694 T t1875 o966 b1869 b4 b1874
4695 B b1875 t1875
4696 T t1876 o738 b1845 b1861
4697 H h1876 v_1 t1876
4698 S s1876 t620 h h1846 h1848 h1862 h1876
4699 G s1876 t1849
4700 B b1876 s1876
4701 T t1877 o938 b1876 b1858
4702 B b1877 t1877
4703 T t1878 o937 b1877 b4 b1872
4704 B b1878 t1878
4705 B b1879 t1845 v_1
4706 T t1879 o711 b1879
4707 S s1879 t620 h h1846 h1848 h1862
4708 G s1879 t1879
4709 B b1880 s1879
4710 T t1880 o938 b1880 b1858
4711 B b1881 t1880
4712 T t1881 o738 b1845 b1220
4713 B b1882 t1881 v_1
4714 T t1882 o976 b1882
4715 S s1882 t620 h h1846 h1848 h1862
4716 G s1882 t1882
4717 B b1883 s1882
4718 T t1883 o938 b1883 b1858
4719 B b1884 t1883
4720 T t1884 o973 b1884 b983 b1872
4721 B b1885 t1884
4722 T t1885 o2 b1885
4723 B b1886 t1885
4724 T t1886 o973 b1881 b4 b1886
4725 B b1887 t1886
4726 T t1887 o b1887 b4
4727 B b1888 t1887
4728 T t1888 o b1878 b1888
4729 B b1889 t1888
4730 T t1889 o b1875 b1889
4731 B b1890 t1889
4732 T t1890 o936 b1865 b1890
4733 B b1891 t1890
4734 P p1891 String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
4735 O o1891 ext_rule p1891
4736 T t1891 o936 b1875 b4
4737 B b1892 t1891
4738 T t1892 o1891 b935 b1892 b4 b4
4739 B b1893 t1892
4740 P p1893 String "groupCancelRightT << 's >> thenT autoT"
4741 O o1893 ext_rule p1893
4742 T t1893 o936 b1878 b4
4743 B b1894 t1893
4744 T t1894 o1893 b935 b1894 b4 b4
4745 B b1895 t1894
4746 T t1895 o936 b1887 b4
4747 B b1896 t1895
4748 T t1896 o1071 b935 b1896 b4 b4
4749 B b1897 t1896
4750 T t1897 o b1897 b4
4751 B b1898 t1897
4752 T t1898 o b1895 b1898
4753 B b1899 t1898
4754 T t1899 o b1893 b1899
4755 B b1900 t1899
4756 T t1900 o1867 b935 b1891 b1900 b4
4757 B b1901 t1900
4758 T t1901 o b1901 b4
4759 B b1902 t1901
4760 T t1902 o1854 b935 b1867 b1902 b4
4761 B b1903 t1902
4762 T t1903 o933 b1903
4763 B b1904 t1903
4764 P p1904 Number 7007
4765 P p1905 Number 7015
4766 O o1905 resource_defs p1904 p1905 p264
4767 P p1906 Number 7013
4768 O o1906 uid p1906 p1905
4769 T t1906 o1906 b626
4770 B b1906 t1906
4771 T t1907 o b1906 b4
4772 B b1907 t1907
4773 T t1908 o1905 b1907
4774 B b1908 t1908
4775 T t1909 o b1908 b4
4776 B b1909 t1909
4777 T t1910 o1845 b618 b1854 b1904 b1909
4778 B b1910 t1910
4779 T t1911 o1844 b1910
4780 B b1911 t1911
4781 P p1911 Number 7356
4782 P p1912 Number 7775
4783 O o1912 location p1911 p1912
4784 P p1913 String unique_sol1
4785 O o1913 rule p1913
4786 P p1914 Var a
4787 O o1914 var p1914
4788 T t1914 o1914
4789 B b1914 t1914
4790 T t1915 o620 b1914
4791 S s1915 t637 h
4792 G s1915 t1915
4793 B b1915 s1915
4794 T t1916 o618 b1915
4795 B b1916 t1916
4796 P p1916 Var b
4797 O o1916 var p1916
4798 T t1917 o1916
4799 B b1917 t1917
4800 T t1918 o620 b1917
4801 S s1918 t637 h
4802 G s1918 t1918
4803 B b1918 s1918
4804 T t1919 o618 b1918
4805 B b1919 t1919
4806 P p1919 Var x
4807 O o1919 var p1919
4808 T t1920 o1919
4809 B b1920 t1920
4810 T t1921 o620 b1920
4811 S s1921 t637 h
4812 G s1921 t1921
4813 B b1921 s1921
4814 T t1922 o618 b1921
4815 B b1922 t1922
4816 T t1923 o655 b1914 b554
4817 S s1923 t620 h
4818 G s1923 t1923
4819 B b1923 s1923
4820 T t1924 o618 b1923
4821 B b1924 t1924
4822 T t1925 o655 b1917 b554
4823 S s1925 t620 h
4824 G s1925 t1925
4825 B b1925 s1925
4826 T t1926 o618 b1925
4827 B b1926 t1926
4828 T t1927 o655 b1920 b554
4829 S s1927 t620 h
4830 G s1927 t1927
4831 B b1927 s1927
4832 T t1928 o618 b1927
4833 B b1928 t1928
4834 T t1929 o559 b1914 b1920
4835 B b1929 t1929
4836 T t1930 o738 b1929 b1917
4837 S s1930 t620 h
4838 G s1930 t1930
4839 B b1930 s1930
4840 T t1931 o618 b1930
4841 B b1931 t1931
4842 T t1932 o572 b1914
4843 B b1932 t1932
4844 T t1933 o559 b1932 b1917
4845 B b1933 t1933
4846 T t1934 o738 b1920 b1933
4847 S s1934 t620 h
4848 G s1934 t1934
4849 B b1934 s1934
4850 T t1935 o618 b1934
4851 B b1935 t1935
4852 T t1936 o635 b1931 b1935
4853 B b1936 t1936
4854 T t1937 o635 b1928 b1936
4855 B b1937 t1937
4856 T t1938 o635 b1926 b1937
4857 B b1938 t1938
4858 T t1939 o635 b1924 b1938
4859 B b1939 t1939
4860 T t1940 o635 b1922 b1939
4861 B b1940 t1940
4862 T t1941 o635 b1919 b1940
4863 B b1941 t1941
4864 T t1942 o635 b1916 b1941
4865 B b1942 t1942
4866 P p1942 String "assumT 7 thenT rwh unfold_equal 2 thenT autoT thenT assertT << equal{op{inv{'a}; op{'a; 'x}}; op{inv{'a}; 'b}} >> thenWT autoT"
4867 O o1942 ext_rule p1942
4868 T t1943 o b1930 b4
4869 B b1943 t1943
4870 T t1944 o b1927 b1943
4871 B b1944 t1944
4872 T t1945 o b1925 b1944
4873 B b1945 t1945
4874 T t1946 o b1923 b1945
4875 B b1946 t1946
4876 T t1947 o b1921 b1946
4877 B b1947 t1947
4878 T t1948 o b1918 b1947
4879 B b1948 t1948
4880 T t1949 o b1915 b1948
4881 B b1949 t1949
4882 T t1950 o938 b1934 b1949
4883 B b1950 t1950
4884 T t1951 o937 b1950 b4 b946
4885 B b1951 t1951
4886 T t1952 o620 b1929
4887 H h1952 y_1 t1952
4888 H h1953 z_1 t1918
4889 T t1953 o676 b1929 b1917
4890 H h1954 z t1953
4891 T t1954 o559 b1932 b1929
4892 B b1954 t1954
4893 T t1955 o738 b1954 b1933
4894 S s1955 t620 h h1952 h1953 h1954
4895 G s1955 t1955
4896 B b1955 s1955
4897 T t1956 o938 b1955 b1949
4898 B b1956 t1956
4899 T t1957 o676 b1920 b1933
4900 S s1957 t620 h h1952 h1953 h1954
4901 G s1957 t1957
4902 B b1957 s1957
4903 T t1958 o938 b1957 b1949
4904 B b1958 t1958
4905 S s1958 t620 h h1952 h1953 h1954
4906 G s1958 t1934
4907 B b1959 s1958
4908 T t1959 o938 b1959 b1949
4909 B b1960 t1959
4910 B b1961 t1952
4911 B b1962 t1918
4912 T t1962 o1270 b1961 b1962
4913 H h1962 y t1962
4914 S s1962 t620 h h1962 h1954
4915 G s1962 t1934
4916 B b1963 s1962
4917 T t1963 o938 b1963 b1949
4918 B b1964 t1963
4919 B b1965 t1962
4920 B b1966 t1953
4921 T t1966 o1270 b1965 b1966
4922 H h1966 v t1966
4923 S s1966 t620 h h1966
4924 G s1966 t1934
4925 B b1967 s1966
4926 T t1967 o938 b1967 b1949
4927 B b1968 t1967
4928 H h1968 v t1930
4929 S s1968 t620 h h1968
4930 G s1968 t1934
4931 B b1969 s1968
4932 T t1969 o938 b1969 b1949
4933 B b1970 t1969
4934 T t1970 o2 b1951
4935 B b1971 t1970
4936 T t1971 o937 b1970 b4 b1971
4937 B b1972 t1971
4938 T t1972 o2 b1972
4939 B b1973 t1972
4940 T t1973 o937 b1968 b4 b1973
4941 B b1974 t1973
4942 T t1974 o2 b1974
4943 B b1975 t1974
4944 T t1975 o937 b1964 b4 b1975
4945 B b1976 t1975
4946 T t1976 o2 b1976
4947 B b1977 t1976
4948 T t1977 o937 b1960 b983 b1977
4949 B b1978 t1977
4950 T t1978 o2 b1978
4951 B b1979 t1978
4952 T t1979 o937 b1958 b4 b1979
4953 B b1980 t1979
4954 T t1980 o2 b1980
4955 B b1981 t1980
4956 T t1981 o947 b1956 b4 b1981
4957 B b1982 t1981
4958 H h1982 v t1955
4959 S s1982 t620 h h1952 h1953 h1954 h1982
4960 G s1982 t1957
4961 B b1983 s1982
4962 T t1983 o938 b1983 b1949
4963 B b1984 t1983
4964 T t1984 o937 b1984 b4 b1981
4965 B b1985 t1984
4966 T t1985 o b1985 b4
4967 B b1986 t1985
4968 T t1986 o b1982 b1986
4969 B b1987 t1986
4970 T t1987 o936 b1951 b1987
4971 B b1988 t1987
4972 T t1988 o936 b1982 b4
4973 B b1989 t1988
4974 T t1989 o990 b935 b1989 b4 b4
4975 B b1990 t1989
4976 P p1990 String "setSubstT << equal{op{inv{'a}; op{'a; 'x}}; op{op{inv{'a}; 'a}; 'x}} >> 5 thenT autoT"
4977 O o1990 ext_rule p1990
4978 T t1990 o559 b1932 b1914
4979 B b1991 t1990
4980 T t1991 o559 b1991 b1920
4981 B b1992 t1991
4982 T t1992 o738 b1992 b1933
4983 H h1992 v_1 t1992
4984 S s1992 t620 h h1952 h1953 h1954 h1982 h1992
4985 G s1992 t1957
4986 B b1993 s1992
4987 T t1993 o938 b1993 b1949
4988 B b1994 t1993
4989 T t1994 o2 b1985
4990 B b1995 t1994
4991 T t1995 o937 b1994 b4 b1995
4992 B b1996 t1995
4993 B b1997 t1933 v_1
4994 T t1997 o711 b1997
4995 S s1997 t620 h h1952 h1953 h1954 h1982
4996 G s1997 t1997
4997 B b1998 s1997
4998 T t1998 o938 b1998 b1949
4999 B b1999 t1998
5000 T t1999 o738 b1220 b1933
5001 B b2000 t1999 v_1
5002 T t2000 o976 b2000
5003 S s2000 t620 h h1952 h1953 h1954 h1982
5004 G s2000 t2000
5005 B b2001 s2000
5006 T t2001 o938 b2001 b1949
5007 B b2002 t2001
5008 T t2002 o973 b2002 b983 b1995
5009 B b2003 t2002
5010 T t2003 o2 b2003
5011 B b2004 t2003
5012 T t2004 o973 b1999 b4 b2004
5013 B b2005 t2004
5014 T t2005 o b2005 b4
5015 B b2006 t2005
5016 T t2006 o b1996 b2006
5017 B b2007 t2006
5018 T t2007 o936 b1985 b2007
5019 B b2008 t2007
5020 P p2008 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"
5021 O o2008 ext_rule p2008
5022 T t2008 o559 b567 b1920
5023 B b2009 t2008
5024 T t2009 o738 b2009 b1933
5025 H h2009 v_2 t2009
5026 S s2009 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5027 G s2009 t1957
5028 B b2010 s2009
5029 T t2010 o938 b2010 b1949
5030 B b2011 t2010
5031 T t2011 o2 b1996
5032 B b2012 t2011
5033 T t2012 o937 b2011 b4 b2012
5034 B b2013 t2012
5035 B b2014 t1933 v_2
5036 T t2014 o711 b2014
5037 S s2014 t620 h h1952 h1953 h1954 h1982 h1992
5038 G s2014 t2014
5039 B b2015 s2014
5040 T t2015 o938 b2015 b1949
5041 B b2016 t2015
5042 T t2016 o559 b977 b1920
5043 B b2017 t2016
5044 T t2017 o738 b2017 b1933
5045 B b2018 t2017 v_2
5046 T t2018 o976 b2018
5047 S s2018 t620 h h1952 h1953 h1954 h1982 h1992
5048 G s2018 t2018
5049 B b2019 s2018
5050 T t2019 o938 b2019 b1949
5051 B b2020 t2019
5052 T t2020 o973 b2020 b983 b2012
5053 B b2021 t2020
5054 T t2021 o2 b2021
5055 B b2022 t2021
5056 T t2022 o973 b2016 b4 b2022
5057 B b2023 t2022
5058 T t2023 o b2023 b4
5059 B b2024 t2023
5060 T t2024 o b2013 b2024
5061 B b2025 t2024
5062 T t2025 o936 b1996 b2025
5063 B b2026 t2025
5064 P p2026 String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"
5065 O o2026 ext_rule p2026
5066 H h2026 v_3 t1934
5067 S s2026 t620 h h1952 h1953 h1954 h1982 h1992 h2009 h2026
5068 G s2026 t1957
5069 B b2027 s2026
5070 T t2027 o938 b2027 b1949
5071 B b2028 t2027
5072 T t2028 o2 b2013
5073 B b2029 t2028
5074 T t2029 o937 b2028 b4 b2029
5075 B b2030 t2029
5076 B b2031 t1933 v_3
5077 T t2031 o711 b2031
5078 S s2031 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5079 G s2031 t2031
5080 B b2032 s2031
5081 T t2032 o938 b2032 b1949
5082 B b2033 t2032
5083 T t2033 o738 b1004 b1933
5084 B b2034 t2033 v_3
5085 T t2034 o976 b2034
5086 S s2034 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5087 G s2034 t2034
5088 B b2035 s2034
5089 T t2035 o938 b2035 b1949
5090 B b2036 t2035
5091 T t2036 o973 b2036 b983 b2029
5092 B b2037 t2036
5093 T t2037 o2 b2037
5094 B b2038 t2037
5095 T t2038 o973 b2033 b4 b2038
5096 B b2039 t2038
5097 T t2039 o b2039 b4
5098 B b2040 t2039
5099 T t2040 o b2030 b2040
5100 B b2041 t2040
5101 T t2041 o936 b2013 b2041
5102 B b2042 t2041
5103 P p2042 String "rwh unfold_equal 8 thenT autoT"
5104 O o2042 ext_rule p2042
5105 T t2042 o936 b2030 b4
5106 B b2043 t2042
5107 T t2043 o2042 b935 b2043 b4 b4
5108 B b2044 t2043
5109 T t2044 o936 b2039 b4
5110 B b2045 t2044
5111 T t2045 o1071 b935 b2045 b4 b4
5112 B b2046 t2045
5113 T t2046 o b2046 b4
5114 B b2047 t2046
5115 T t2047 o b2044 b2047
5116 B b2048 t2047
5117 T t2048 o2026 b935 b2042 b2048 b4
5118 B b2049 t2048
5119 T t2049 o936 b2023 b4
5120 B b2050 t2049
5121 T t2050 o1071 b935 b2050 b4 b4
5122 B b2051 t2050
5123 T t2051 o b2051 b4
5124 B b2052 t2051
5125 T t2052 o b2049 b2052
5126 B b2053 t2052
5127 T t2053 o2008 b935 b2026 b2053 b4
5128 B b2054 t2053
5129 T t2054 o936 b2005 b4
5130 B b2055 t2054
5131 T t2055 o1071 b935 b2055 b4 b4
5132 B b2056 t2055
5133 T t2056 o b2056 b4
5134 B b2057 t2056
5135 T t2057 o b2054 b2057
5136 B b2058 t2057
5137 T t2058 o738 b1954 b1992
5138 S s2058 t620 h h1952 h1953 h1954 h1982
5139 G s2058 t2058
5140 B b2059 s2058
5141 T t2059 o938 b2059 b1949
5142 B b2060 t2059
5143 T t2060 o966 b2060 b4 b1995
5144 B b2061 t2060
5145 T t2061 o936 b2061 b4
5146 B b2062 t2061
5147 T t2062 o990 b935 b2062 b4 b4
5148 B b2063 t2062
5149 P p2063 String "rwh unfold_fun_prop 0 thenT autoT thenT rwh unfold_equal 9 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 11 thenT autoT"
5150 O o2063 ext_rule p2063
5151 T t2063 o973 b2002 b4 b1995
5152 B b2064 t2063
5153 H h2064 x_1 t1344
5154 H h2065 y_2 t638
5155 T t2065 o620 b1933
5156 H h2066 z_3 t2065
5157 T t2066 o676 b560 b1933
5158 H h2067 z_2 t2066
5159 S s2067 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5160 G s2067 t1997
5161 B b2067 s2067
5162 T t2067 o938 b2067 b1949
5163 B b2068 t2067
5164 T t2068 o676 b1220 b1933
5165 B b2069 t2068 v_1
5166 T t2069 o976 b2069
5167 S s2069 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5168 G s2069 t2069
5169 B b2070 s2069
5170 T t2070 o938 b2070 b1949
5171 B b2071 t2070
5172 T t2071 o676 b561 b1933
5173 S s2071 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5174 G s2071 t2071
5175 B b2072 s2071
5176 T t2072 o938 b2072 b1949
5177 B b2073 t2072
5178 B b2074 t638
5179 B b2075 t2065
5180 T t2075 o1270 b2074 b2075
5181 H h2075 y t2075
5182 S s2075 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2075 h2067
5183 G s2075 t2071
5184 B b2076 s2075
5185 T t2076 o938 b2076 b1949
5186 B b2077 t2076
5187 B b2078 t2075
5188 B b2079 t2066
5189 T t2079 o1270 b2078 b2079
5190 H h2079 x_2 t2079
5191 S s2079 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2079
5192 G s2079 t2071
5193 B b2080 s2079
5194 T t2080 o938 b2080 b1949
5195 B b2081 t2080
5196 T t2081 o738 b560 b1933
5197 H h2081 x_2 t2081
5198 S s2081 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5199 G s2081 t2071
5200 B b2082 s2081
5201 T t2082 o938 b2082 b1949
5202 B b2083 t2082
5203 T t2083 o738 b561 b1933
5204 S s2083 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5205 G s2083 t2083
5206 B b2084 s2083
5207 T t2084 o938 b2084 b1949
5208 B b2085 t2084
5209 B b2086 t2081
5210 B b2087 t2083
5211 T t2087 o1177 b2086 b2087
5212 S s2087 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064
5213 G s2087 t2087
5214 B b2088 s2087
5215 T t2088 o938 b2088 b1949
5216 B b2089 t2088
5217 B b2090 t2087
5218 T t2090 o1177 b1347 b2090
5219 S s2090 t620 h h1952 h1953 h1954 h1982 h1344 h1224
5220 G s2090 t2090
5221 B b2091 s2090
5222 T t2091 o938 b2091 b1949
5223 B b2092 t2091
5224 B b2093 t2090 s2
5225 T t2093 o1185 b1186 b2093
5226 S s2093 t620 h h1952 h1953 h1954 h1982 h1344
5227 G s2093 t2093
5228 B b2094 s2093
5229 T t2094 o938 b2094 b1949
5230 B b2095 t2094
5231 B b2096 t2093 s1
5232 T t2096 o1185 b1186 b2096
5233 S s2096 t620 h h1952 h1953 h1954 h1982
5234 G s2096 t2096
5235 B b2097 s2096
5236 T t2097 o938 b2097 b1949
5237 B b2098 t2097
5238 T t2098 o2 b2064
5239 B b2099 t2098
5240 T t2099 o973 b2098 b983 b2099
5241 B b2100 t2099
5242 T t2100 o2 b2100
5243 B b2101 t2100
5244 T t2101 o937 b2095 b983 b2101
5245 B b2102 t2101
5246 T t2102 o2 b2102
5247 B b2103 t2102
5248 T t2103 o937 b2092 b983 b2103
5249 B b2104 t2103
5250 T t2104 o2 b2104
5251 B b2105 t2104
5252 T t2105 o937 b2089 b983 b2105
5253 B b2106 t2105
5254 T t2106 o2 b2106
5255 B b2107 t2106
5256 T t2107 o937 b2085 b983 b2107
5257 B b2108 t2107
5258 T t2108 o2 b2108
5259 B b2109 t2108
5260 T t2109 o937 b2083 b4 b2109
5261 B b2110 t2109
5262 T t2110 o2 b2110
5263 B b2111 t2110
5264 T t2111 o937 b2081 b4 b2111
5265 B b2112 t2111
5266 T t2112 o2 b2112
5267 B b2113 t2112
5268 T t2113 o937 b2077 b4 b2113
5269 B b2114 t2113
5270 T t2114 o2 b2114
5271 B b2115 t2114
5272 T t2115 o937 b2073 b4 b2115
5273 B b2116 t2115
5274 T t2116 o2 b2116
5275 B b2117 t2116
5276 T t2117 o973 b2071 b983 b2117
5277 B b2118 t2117
5278 T t2118 o2 b2118
5279 B b2119 t2118
5280 T t2119 o973 b2068 b4 b2119
5281 B b2120 t2119
5282 T t2120 o b2120 b4
5283 B b2121 t2120
5284 T t2121 o936 b2064 b2121
5285 B b2122 t2121
5286 T t2122 o936 b2120 b4
5287 B b2123 t2122
5288 T t2123 o1071 b935 b2123 b4 b4
5289 B b2124 t2123
5290 T t2124 o b2124 b4
5291 B b2125 t2124
5292 T t2125 o2063 b935 b2122 b2125 b4
5293 B b2126 t2125
5294 T t2126 o b2126 b4
5295 B b2127 t2126
5296 T t2127 o b2063 b2127
5297 B b2128 t2127
5298 T t2128 o1990 b935 b2008 b2058 b2128
5299 B b2129 t2128
5300 T t2129 o b2129 b4
5301 B b2130 t2129
5302 T t2130 o b1990 b2130
5303 B b2131 t2130
5304 T t2131 o1942 b935 b1988 b2131 b4
5305 B b2132 t2131
5306 T t2132 o933 b2132
5307 B b2133 t2132
5308 P p2133 Number 7383
5309 P p2134 Number 7391
5310 O o2134 resource_defs p2133 p2134 p264
5311 P p2135 Number 7389
5312 O o2135 uid p2135 p2134
5313 T t2135 o2135 b626
5314 B b2135 t2135
5315 T t2136 o b2135 b4
5316 B b2136 t2136
5317 T t2137 o2134 b2136
5318 B b2137 t2137
5319 T t2138 o b2137 b4
5320 B b2138 t2138
5321 T t2139 o1913 b618 b1942 b2133 b2138
5322 B b2139 t2139
5323 T t2140 o1912 b2139
5324 B b2140 t2140
5325 P p2140 Number 7826
5326 P p2141 Number 8245
5327 O o2141 location p2140 p2141
5328 P p2142 String unique_sol2
5329 O o2142 rule p2142
5330 P p2143 Var y
5331 O o2143 var p2143
5332 T t2143 o2143
5333 B b2143 t2143
5334 T t2144 o620 b2143
5335 S s2144 t637 h
5336 G s2144 t2144
5337 B b2144 s2144
5338 T t2145 o618 b2144
5339 B b2145 t2145
5340 T t2146 o655 b2143 b554
5341 S s2146 t620 h
5342 G s2146 t2146
5343 B b2146 s2146
5344 T t2147 o618 b2146
5345 B b2147 t2147
5346 T t2148 o559 b2143 b1914
5347 B b2148 t2148
5348 T t2149 o738 b2148 b1917
5349 S s2149 t620 h
5350 G s2149 t2149
5351 B b2149 s2149
5352 T t2150 o618 b2149
5353 B b2150 t2150
5354 T t2151 o559 b1917 b1932
5355 B b2151 t2151
5356 T t2152 o738 b2143 b2151
5357 S s2152 t620 h
5358 G s2152 t2152
5359 B b2152 s2152
5360 T t2153 o618 b2152
5361 B b2153 t2153
5362 T t2154 o635 b2150 b2153
5363 B b2154 t2154
5364 T t2155 o635 b2147 b2154
5365 B b2155 t2155
5366 T t2156 o635 b1926 b2155
5367 B b2156 t2156
5368 T t2157 o635 b1924 b2156
5369 B b2157 t2157
5370 T t2158 o635 b2145 b2157
5371 B b2158 t2158
5372 T t2159 o635 b1919 b2158
5373 B b2159 t2159
5374 T t2160 o635 b1916 b2159
5375 B b2160 t2160
5376 P p2160 String "assumT 7 thenT assertT << equal{op{op{'y; 'a}; inv{'a}}; op{'b; inv{'a}}} >> thenT autoT"
5377 O o2160 ext_rule p2160
5378 T t2161 o b2149 b4
5379 B b2161 t2161
5380 T t2162 o b2146 b2161
5381 B b2162 t2162
5382 T t2163 o b1925 b2162
5383 B b2163 t2163
5384 T t2164 o b1923 b2163
5385 B b2164 t2164
5386 T t2165 o b2144 b2164
5387 B b2165 t2165
5388 T t2166 o b1918 b2165
5389 B b2166 t2166
5390 T t2167 o b1915 b2166
5391 B b2167 t2167
5392 T t2168 o938 b2152 b2167
5393 B b2168 t2168
5394 T t2169 o937 b2168 b4 b946
5395 B b2169 t2169
5396 H h2169 v t2149
5397 T t2170 o676 b2148 b1917
5398 S s2170 t620 h h2169
5399 G s2170 t2170
5400 B b2170 s2170
5401 T t2171 o938 b2170 b2167
5402 B b2171 t2171
5403 T t2172 o559 b2148 b1932
5404 B b2172 t2172
5405 T t2173 o676 b2172 b2151
5406 S s2173 t620 h h2169
5407 G s2173 t2173
5408 B b2173 s2173
5409 T t2174 o938 b2173 b2167
5410 B b2174 t2174
5411 T t2175 o738 b2172 b2151
5412 S s2175 t620 h h2169
5413 G s2175 t2175
5414 B b2175 s2175
5415 T t2176 o938 b2175 b2167
5416 B b2176 t2176
5417 S s2176 t620 h h2169
5418 G s2176 t2152
5419 B b2177 s2176
5420 T t2177 o938 b2177 b2167
5421 B b2178 t2177
5422 T t2178 o2 b2169
5423 B b2179 t2178
5424 T t2179 o937 b2178 b4 b2179
5425 B b2180 t2179
5426 T t2180 o2 b2180
5427 B b2181 t2180
5428 T t2181 o947 b2176 b983 b2181
5429 B b2182 t2181
5430 T t2182 o2 b2182
5431 B b2183 t2182
5432 T t2183 o947 b2174 b983 b2183
5433 B b2184 t2183
5434 T t2184 o2 b2184
5435 B b2185 t2184
5436 T t2185 o947 b2171 b4 b2185
5437 B b2186 t2185
5438 H h2186 v_1 t2175
5439 T t2186 o676 b2143 b2151
5440 S s2186 t620 h h2169 h2186
5441 G s2186 t2186
5442 B b2187 s2186
5443 T t2187 o938 b2187 b2167
5444 B b2188 t2187
5445 S s2188 t620 h h2169 h2186
5446 G s2188 t2152
5447 B b2189 s2188
5448 T t2189 o938 b2189 b2167
5449 B b2190 t2189
5450 T t2190 o937 b2190 b983 b2181
5451 B b2191 t2190
5452 T t2191 o2 b2191
5453 B b2192 t2191
5454 T t2192 o937 b2188 b4 b2192
5455 B b2193 t2192
5456 T t2193 o b2193 b4
5457 B b2194 t2193
5458 T t2194 o b2186 b2194
5459 B b2195 t2194
5460 T t2195 o936 b2169 b2195
5461 B b2196 t2195
5462 P p2196 String "rwh unfold_equal 2 thenT autoT"
5463 O o2196 ext_rule p2196
5464 T t2196 o936 b2186 b4
5465 B b2197 t2196
5466 T t2197 o2196 b935 b2197 b4 b4
5467 B b2198 t2197
5468 P p2198 String "setSubstT << equal{op{op{'y; 'a}; inv{'a}}; op{'y; op{'a; inv{'a}}}} >> 3 thenT autoT"
5469 O o2198 ext_rule p2198
5470 T t2198 o559 b1914 b1932
5471 B b2199 t2198
5472 T t2199 o559 b2143 b2199
5473 B b2200 t2199
5474 T t2200 o738 b2200 b2151
5475 H h2200 v_2 t2200
5476 S s2200 t620 h h2169 h2186 h2200
5477 G s2200 t2186
5478 B b2201 s2200
5479 T t2201 o938 b2201 b2167
5480 B b2202 t2201
5481 T t2202 o2 b2193
5482 B b2203 t2202
5483 T t2203 o937 b2202 b4 b2203
5484 B b2204 t2203
5485 B b2205 t2151 v_2
5486 T t2205 o711 b2205
5487 S s2205 t620 h h2169 h2186
5488 G s2205 t2205
5489 B b2206 s2205
5490 T t2206 o938 b2206 b2167
5491 B b2207 t2206
5492 T t2207 o738 b977 b2151
5493 B b2208 t2207 v_2
5494 T t2208 o976 b2208
5495 S s2208 t620 h h2169 h2186
5496 G s2208 t2208
5497 B b2209 s2208
5498 T t2209 o938 b2209 b2167
5499 B b2210 t2209
5500 T t2210 o973 b2210 b983 b2203
5501 B b2211 t2210
5502 T t2211 o2 b2211
5503 B b2212 t2211
5504 T t2212 o973 b2207 b4 b2212
5505 B b2213 t2212
5506 T t2213 o b2213 b4
5507 B b2214 t2213
5508 T t2214 o b2204 b2214
5509 B b2215 t2214
5510 T t2215 o936 b2193 b2215
5511 B b2216 t2215
5512 P p2216 String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"
5513 O o2216 ext_rule p2216
5514 T t2216 o559 b2143 b567
5515 B b2217 t2216
5516 T t2217 o738 b2217 b2151
5517 H h2217 v_3 t2217
5518 S s2217 t620 h h2169 h2186 h2200 h2217
5519 G s2217 t2186
5520 B b2218 s2217
5521 T t2218 o938 b2218 b2167
5522 B b2219 t2218
5523 T t2219 o2 b2204
5524 B b2220 t2219
5525 T t2220 o937 b2219 b4 b2220
5526 B b2221 t2220
5527 B b2222 t2151 v_3
5528 T t2222 o711 b2222
5529 S s2222 t620 h h2169 h2186 h2200
5530 G s2222 t2222
5531 B b2223 s2222
5532 T t2223 o938 b2223 b2167
5533 B b2224 t2223
5534 T t2224 o559 b2143 b1004
5535 B b2225 t2224
5536 T t2225 o738 b2225 b2151
5537 B b2226 t2225 v_3
5538 T t2226 o976 b2226
5539 S s2226 t620 h h2169 h2186 h2200
5540 G s2226 t2226
5541 B b2227 s2226
5542 T t2227 o938 b2227 b2167
5543 B b2228 t2227
5544 T t2228 o973 b2228 b983 b2220
5545 B b2229 t2228
5546 T t2229 o2 b2229
5547 B b2230 t2229
5548 T t2230 o973 b2224 b4 b2230
5549 B b2231 t2230
5550 T t2231 o b2231 b4
5551 B b2232 t2231
5552 T t2232 o b2221 b2232
5553 B b2233 t2232
5554 T t2233 o936 b2204 b2233
5555 B b2234 t2233
5556 P p2234 String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"
5557 O o2234 ext_rule p2234
5558 T t2234 o620 b2217
5559 H h2234 y_2 t2234
5560 T t2235 o620 b2151
5561 H h2235 z_1 t2235
5562 T t2236 o676 b2217 b2151
5563 H h2236 z t2236
5564 S s2236 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5565 G s2236 t2222
5566 B b2236 s2236
5567 T t2237 o938 b2236 b2167
5568 B b2237 t2237
5569 T t2238 o676 b1004 b2151
5570 B b2238 t2238 v_3
5571 T t2239 o976 b2238
5572 S s2239 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5573 G s2239 t2239
5574 B b2239 s2239
5575 T t2240 o938 b2239 b2167
5576 B b2240 t2240
5577 S s2240 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5578 G s2240 t2186
5579 B b2241 s2240
5580 T t2241 o938 b2241 b2167
5581 B b2242 t2241
5582 B b2243 t2234
5583 B b2244 t2235
5584 T t2244 o1270 b2243 b2244
5585 H h2244 y_1 t2244
5586 S s2244 t620 h h2169 h2186 h2200 h2244 h2236
5587 G s2244 t2186
5588 B b2245 s2244
5589 T t2245 o938 b2245 b2167
5590 B b2246 t2245
5591 B b2247 t2244
5592 B b2248 t2236
5593 T t2248 o1270 b2247 b2248
5594 H h2248 v_3 t2248
5595 S s2248 t620 h h2169 h2186 h2200 h2248
5596 G s2248 t2186
5597 B b2249 s2248
5598 T t2249 o938 b2249 b2167
5599 B b2250 t2249
5600 T t2250 o2 b2221
5601 B b2251 t2250
5602 T t2251 o937 b2250 b4 b2251
5603 B b2252 t2251
5604 T t2252 o2 b2252
5605 B b2253 t2252
5606 T t2253 o937 b2246 b4 b2253
5607 B b2254 t2253
5608 T t2254 o2 b2254
5609 B b2255 t2254
5610 T t2255 o937 b2242 b4 b2255
5611 B b2256 t2255
5612 T t2256 o2 b2256
5613 B b2257 t2256
5614 T t2257 o973 b2240 b983 b2257
5615 B b2258 t2257
5616 T t2258 o2 b2258
5617 B b2259 t2258
5618 T t2259 o973 b2237 b4 b2259
5619 B b2260 t2259
5620 T t2260 o b2260 b4
5621 B b2261 t2260
5622 T t2261 o936 b2221 b2261
5623 B b2262 t2261
5624 T t2262 o936 b2260 b4
5625 B b2263 t2262
5626 T t2263 o1071 b935 b2263 b4 b4
5627 B b2264 t2263
5628 T t2264 o b2264 b4
5629 B b2265 t2264
5630 T t2265 o2234 b935 b2262 b2265 b4
5631 B b2266 t2265
5632 T t2266 o936 b2231 b4
5633 B b2267 t2266
5634 T t2267 o1071 b935 b2267 b4 b4
5635 B b2268 t2267
5636 T t2268 o b2268 b4
5637 B b2269 t2268
5638 T t2269 o b2266 b2269
5639 B b2270 t2269
5640 T t2270 o2216 b935 b2234 b2270 b4
5641 B b2271 t2270
5642 T t2271 o936 b2213 b4
5643 B b2272 t2271
5644 T t2272 o1071 b935 b2272 b4 b4
5645 B b2273 t2272
5646 T t2273 o b2273 b4
5647 B b2274 t2273
5648 T t2274 o b2271 b2274
5649 B b2275 t2274
5650 T t2275 o2198 b935 b2216 b2275 b4
5651 B b2276 t2275
5652 T t2276 o b2276 b4
5653 B b2277 t2276
5654 T t2277 o b2198 b2277
5655 B b2278 t2277
5656 T t2278 o2160 b935 b2196 b2278 b4
5657 B b2279 t2278
5658 T t2279 o933 b2279
5659 B b2280 t2279
5660 P p2280 Number 7853
5661 P p2281 Number 7861
5662 O o2281 resource_defs p2280 p2281 p264
5663 P p2282 Number 7859
5664 O o2282 uid p2282 p2281
5665 T t2282 o2282 b626
5666 B b2282 t2282
5667 T t2283 o b2282 b4
5668 B b2283 t2283
5669 T t2284 o2281 b2283
5670 B b2284 t2284
5671 T t2285 o b2284 b4
5672 B b2285 t2285
5673 T t2286 o2142 b618 b2160 b2280 b2285
5674 B b2286 t2286
5675 T t2287 o2141 b2286
5676 B b2287 t2287
5677 P p2287 Number 8273
5678 P p2288 Number 8568
5679 O o2288 location p2287 p2288
5680 P p2289 String inv_simplify
5681 O o2289 rule p2289
5682 T t2289 o559 b1914 b1917
5683 B b2289 t2289
5684 T t2290 o572 b2289
5685 B b2290 t2290
5686 T t2291 o572 b1917
5687 B b2291 t2291
5688 T t2292 o559 b2291 b1932
5689 B b2292 t2292
5690 T t2293 o738 b2290 b2292
5691 S s2293 t620 h
5692 G s2293 t2293
5693 B b2293 s2293
5694 T t2294 o618 b2293
5695 B b2294 t2294
5696 T t2295 o635 b1926 b2294
5697 B b2295 t2295
5698 T t2296 o635 b1924 b2295
5699 B b2296 t2296
5700 T t2297 o635 b1919 b2296
5701 B b2297 t2297
5702 T t2298 o635 b1916 b2297
5703 B b2298 t2298
5704 P p2298 String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >> thenAT autoT"
5705 O o2298 ext_rule p2298
5706 T t2299 o b1925 b4
5707 B b2299 t2299
5708 T t2300 o b1923 b2299
5709 B b2300 t2300
5710 T t2301 o b1918 b2300
5711 B b2301 t2301
5712 T t2302 o b1915 b2301
5713 B b2302 t2302
5714 T t2303 o938 b2293 b2302
5715 B b2303 t2303
5716 T t2304 o937 b2303 b4 b946
5717 B b2304 t2304
5718 T t2305 o559 b2290 b2289
5719 B b2305 t2305
5720 T t2306 o559 b2292 b2289
5721 B b2306 t2306
5722 T t2307 o738 b2305 b2306
5723 S s2307 t620 h
5724 G s2307 t2307
5725 B b2307 s2307
5726 T t2308 o938 b2307 b2302
5727 B b2308 t2308
5728 T t2309 o2 b2304
5729 B b2309 t2309
5730 T t2310 o947 b2308 b4 b2309
5731 B b2310 t2310
5732 H h2310 v t2307
5733 S s2310 t620 h h2310
5734 G s2310 t2293
5735 B b2311 s2310
5736 T t2311 o938 b2311 b2302
5737 B b2312 t2311
5738 T t2312 o937 b2312 b4 b2309
5739 B b2313 t2312
5740 T t2313 o b2313 b4
5741 B b2314 t2313
5742 T t2314 o b2310 b2314
5743 B b2315 t2314
5744 T t2315 o936 b2304 b2315
5745 B b2316 t2315
5746 P p2316 String "setSubstT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; id} >> 0 thenWT autoT"
5747 O o2316 ext_rule p2316
5748 T t2316 o738 b2305 b567
5749 S s2316 t620 h
5750 G s2316 t2316
5751 B b2317 s2316
5752 T t2317 o938 b2317 b2302
5753 B b2318 t2317
5754 T t2318 o2 b2310
5755 B b2319 t2318
5756 T t2319 o966 b2318 b4 b2319
5757 B b2320 t2319
5758 T t2320 o738 b567 b2306
5759 S s2320 t620 h
5760 G s2320 t2320
5761 B b2321 s2320
5762 T t2321 o938 b2321 b2302
5763 B b2322 t2321
5764 T t2322 o937 b2322 b4 b2319
5765 B b2323 t2322
5766 B b2324 t2306 v
5767 T t2324 o711 b2324
5768 S s2324 t620 h
5769 G s2324 t2324
5770 B b2325 s2324
5771 T t2325 o938 b2325 b2302
5772 B b2326 t2325
5773 P p2326 Var v
5774 O o2326 var p2326
5775 T t2326 o2326
5776 B b2327 t2326
5777 T t2327 o738 b2327 b2306
5778 B b2328 t2327 v
5779 T t2328 o976 b2328
5780 S s2328 t620 h
5781 G s2328 t2328
5782 B b2329 s2328
5783 T t2329 o938 b2329 b2302
5784 B b2330 t2329
5785 T t2330 o973 b2330 b983 b2319
5786 B b2331 t2330
5787 T t2331 o2 b2331
5788 B b2332 t2331
5789 T t2332 o973 b2326 b4 b2332
5790 B b2333 t2332
5791 T t2333 o b2333 b4
5792 B b2334 t2333
5793 T t2334 o b2323 b2334
5794 B b2335 t2334
5795 T t2335 o b2320 b2335
5796 B b2336 t2335
5797 T t2336 o936 b2310 b2336
5798 B b2337 t2336
5799 T t2337 o936 b2320 b4
5800 B b2338 t2337
5801 T t2338 o990 b935 b2338 b4 b4
5802 B b2339 t2338
5803 P p2339 String "setSubstT << equal{id; op{inv{'b}; op{inv{'a}; op{'a; 'b}}}} >> 0 thenWT autoT"
5804 O o2339 ext_rule p2339
5805 T t2339 o559 b1932 b2289
5806 B b2340 t2339
5807 T t2340 o559 b2291 b2340
5808 B b2341 t2340
5809 T t2341 o738 b567 b2341
5810 S s2341 t620 h
5811 G s2341 t2341
5812 B b2342 s2341
5813 T t2342 o938 b2342 b2302
5814 B b2343 t2342
5815 T t2343 o2 b2323
5816 B b2344 t2343
5817 T t2344 o966 b2343 b4 b2344
5818 B b2345 t2344
5819 T t2345 o738 b2341 b2306
5820 S s2345 t620 h
5821 G s2345 t2345
5822 B b2346 s2345
5823 T t2346 o938 b2346 b2302
5824 B b2347 t2346
5825 T t2347 o937 b2347 b4 b2344
5826 B b2348 t2347
5827 T t2348 o973 b2330 b983 b2344
5828 B b2349 t2348
5829 T t2349 o2 b2349
5830 B b2350 t2349
5831 T t2350 o973 b2326 b4 b2350
5832 B b2351 t2350
5833 T t2351 o b2351 b4
5834 B b2352 t2351
5835 T t2352 o b2348 b2352
5836 B b2353 t2352
5837 T t2353 o b2345 b2353
5838 B b2354 t2353
5839 T t2354 o936 b2323 b2354
5840 B b2355 t2354
5841 P p2355 String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"
5842 O o2355 ext_rule p2355
5843 T t2355 o559 b1991 b1917
5844 B b2356 t2355
5845 T t2356 o738 b2340 b2356
5846 S s2356 t620 h
5847 G s2356 t2356
5848 B b2357 s2356
5849 T t2357 o938 b2357 b2302
5850 B b2358 t2357
5851 T t2358 o2 b2345
5852 B b2359 t2358
5853 T t2359 o966 b2358 b4 b2359
5854 B b2360 t2359
5855 T t2360 o559 b2291 b2356
5856 B b2361 t2360
5857 T t2361 o738 b567 b2361
5858 S s2361 t620 h
5859 G s2361 t2361
5860 B b2362 s2361
5861 T t2362 o938 b2362 b2302
5862 B b2363 t2362
5863 T t2363 o937 b2363 b4 b2359
5864 B b2364 t2363
5865 T t2364 o b2364 b4
5866 B b2365 t2364
5867 T t2365 o b2360 b2365
5868 B b2366 t2365
5869 T t2366 o936 b2345 b2366
5870 B b2367 t2366
5871 T t2367 o936 b2360 b4
5872 B b2368 t2367
5873 T t2368 o990 b935 b2368 b4 b4
5874 B b2369 t2368
5875 P p2369 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 0 thenWT autoT"
5876 O o2369 ext_rule p2369
5877 T t2369 o738 b1991 b567
5878 S s2369 t620 h
5879 G s2369 t2369
5880 B b2370 s2369
5881 T t2370 o938 b2370 b2302
5882 B b2371 t2370
5883 T t2371 o2 b2364
5884 B b2372 t2371
5885 T t2372 o966 b2371 b4 b2372
5886 B b2373 t2372
5887 T t2373 o559 b567 b1917
5888 B b2374 t2373
5889 T t2374 o559 b2291 b2374
5890 B b2375 t2374
5891 T t2375 o738 b567 b2375
5892 S s2375 t620 h
5893 G s2375 t2375
5894 B b2376 s2375
5895 T t2376 o938 b2376 b2302
5896 B b2377 t2376
5897 T t2377 o937 b2377 b4 b2372
5898 B b2378 t2377
5899 T t2378 o559 b2327 b1917
5900 B b2379 t2378
5901 T t2379 o559 b2291 b2379
5902 B b2380 t2379 v
5903 T t2380 o711 b2380
5904 S s2380 t620 h
5905 G s2380 t2380
5906 B b2381 s2380
5907 T t2381 o938 b2381 b2302
5908 B b2382 t2381
5909 B b2383 t2379
5910 T t2383 o738 b567 b2383
5911 B b2384 t2383 v
5912 T t2384 o976 b2384
5913 S s2384 t620 h
5914 G s2384 t2384
5915 B b2385 s2384
5916 T t2385 o938 b2385 b2302
5917 B b2386 t2385
5918 T t2386 o973 b2386 b983 b2372
5919 B b2387 t2386
5920 T t2387 o2 b2387
5921 B b2388 t2387
5922 T t2388 o973 b2382 b4 b2388
5923 B b2389 t2388
5924 T t2389 o b2389 b4
5925 B b2390 t2389
5926 T t2390 o b2378 b2390
5927 B b2391 t2390
5928 T t2391 o b2373 b2391
5929 B b2392 t2391
5930 T t2392 o936 b2364 b2392
5931 B b2393 t2392
5932 T t2393 o936 b2373 b4
5933 B b2394 t2393
5934 T t2394 o990 b935 b2394 b4 b4
5935 B b2395 t2394
5936 P p2395 String "setSubstT << equal{op{id; 'b}; 'b} >> 0 thenWT autoT"
5937 O o2395 ext_rule p2395
5938 T t2395 o738 b2374 b1917
5939 S s2395 t620 h
5940 G s2395 t2395
5941 B b2396 s2395
5942 T t2396 o938 b2396 b2302
5943 B b2397 t2396
5944 T t2397 o2 b2378
5945 B b2398 t2397
5946 T t2398 o966 b2397 b4 b2398
5947 B b2399 t2398
5948 T t2399 o559 b2291 b1917
5949 B b2400 t2399
5950 T t2400 o738 b567 b2400
5951 S s2400 t620 h
5952 G s2400 t2400
5953 B b2401 s2400
5954 T t2401 o938 b2401 b2302
5955 B b2402 t2401
5956 T t2402 o937 b2402 b4 b2398
5957 B b2403 t2402
5958 T t2403 o b2403 b4
5959 B b2404 t2403
5960 T t2404 o b2399 b2404
5961 B b2405 t2404
5962 T t2405 o936 b2378 b2405
5963 B b2406 t2405
5964 T t2406 o936 b2399 b4
5965 B b2407 t2406
5966 T t2407 o990 b935 b2407 b4 b4
5967 B b2408 t2407
5968 P p2408 String "setSubstT << equal{op{inv{'b}; 'b}; id} >> 0 thenT autoT"
5969 O o2408 ext_rule p2408
5970 T t2408 o936 b2403 b4
5971 B b2409 t2408
5972 T t2409 o2408 b935 b2409 b4 b4
5973 B b2410 t2409
5974 T t2410 o b2410 b4
5975 B b2411 t2410
5976 T t2411 o b2408 b2411
5977 B b2412 t2411
5978 T t2412 o2395 b935 b2406 b2412 b4
5979 B b2413 t2412
5980 P p2413 String "rwh unfold_fun_set 0 thenT dT 0"
5981 O o2413 ext_rule p2413
5982 NItt_equal Itt_equal Itt_equal NIL
5983 NItt_equal!type type type Itt_equal
5984 O o2414 type
5985 T t2414 o2414 b1186
5986 S s2414 t637 h
5987 G s2414 t2414
5988 B b2414 s2414
5989 T t2415 o938 b2414 b2302
5990 B b2415 t2415
5991 T t2416 o559 b560 b1917
5992 B b2416 t2416
5993 T t2417 o559 b2291 b2416
5994 B b2417 t2417
5995 T t2418 o559 b561 b1917
5996 B b2418 t2418
5997 T t2419 o559 b2291 b2418
5998 B b2419 t2419
5999 T t2420 o738 b2417 b2419
6000 B b2420 t2420
6001 T t2421 o1177 b1347 b2420
6002 B b2421 t2421 s2
6003 T t2422 o1185 b1186 b2421
6004 B b2422 t2422 s1
6005 T t2423 o1185 b1186 b2422
6006 S s2423 t620 h
6007 G s2423 t2423
6008 B b2423 s2423
6009 T t2424 o938 b2423 b2302
6010 B b2424 t2424
6011 T t2425 o2 b2389
6012 B b2425 t2425
6013 T t2426 o973 b2424 b4 b2425
6014 B b2426 t2426
6015 T t2427 o2 b2426
6016 B b2427 t2427
6017 T t2428 o973 b2415 b4 b2427
6018 B b2428 t2428
6019 S s2428 t620 h h1344
6020 G s2428 t2422
6021 B b2429 s2428
6022 T t2429 o938 b2429 b2302
6023 B b2430 t2429
6024 T t2430 o937 b2430 b4 b2427
6025 B b2431 t2430
6026 T t2431 o b2431 b4
6027 B b2432 t2431
6028 T t2432 o b2428 b2432
6029 B b2433 t2432
6030 T t2433 o936 b2389 b2433
6031 B b2434 t2433
6032 T t2434 o936 b2428 b4
6033 B b2435 t2434
6034 T t2435 o990 b935 b2435 b4 b4
6035 B b2436 t2435
6036 P p2436 String "dT 0"
6037 O o2436 ext_rule p2436
6038 S s2436 t637 h h1344
6039 G s2436 t2414
6040 B b2437 s2436
6041 T t2437 o938 b2437 b2302
6042 B b2438 t2437
6043 T t2438 o2 b2431
6044 B b2439 t2438
6045 T t2439 o973 b2438 b4 b2439
6046 B b2440 t2439
6047 S s2440 t620 h h1344 h1224
6048 G s2440 t2421
6049 B b2441 s2440
6050 T t2441 o938 b2441 b2302
6051 B b2442 t2441
6052 T t2442 o937 b2442 b4 b2439
6053 B b2443 t2442
6054 T t2443 o b2443 b4
6055 B b2444 t2443
6056 T t2444 o b2440 b2444
6057 B b2445 t2444
6058 T t2445 o936 b2431 b2445
6059 B b2446 t2445
6060 T t2446 o936 b2440 b4
6061 B b2447 t2446
6062 T t2447 o990 b935 b2447 b4 b4
6063 B b2448 t2447
6064 T t2448 o2414 b1347
6065 S s2448 t637 h h1344 h1224
6066 G s2448 t2448
6067 B b2449 s2448
6068 T t2449 o938 b2449 b2302
6069 B b2450 t2449
6070 T t2450 o2 b2443
6071 B b2451 t2450
6072 T t2451 o973 b2450 b4 b2451
6073 B b2452 t2451
6074 S s2452 t620 h h1344 h1224 h1345
6075 G s2452 t2420
6076 B b2453 s2452
6077 T t2453 o938 b2453 b2302
6078 B b2454 t2453
6079 T t2454 o937 b2454 b4 b2451
6080 B b2455 t2454
6081 T t2455 o b2455 b4
6082 B b2456 t2455
6083 T t2456 o b2452 b2456
6084 B b2457 t2456
6085 T t2457 o936 b2443 b2457
6086 B b2458 t2457
6087 T t2458 o936 b2452 b4
6088 B b2459 t2458
6089 T t2459 o990 b935 b2459 b4 b4
6090 B b2460 t2459
6091 P p2460 String "rwh unfold_equal 0 thenT rwh unfold_equal 4 thenT autoT"
6092 O o2460 ext_rule p2460
6093 T t2460 o936 b2455 b4
6094 B b2461 t2460
6095 T t2461 o2460 b935 b2461 b4 b4
6096 B b2462 t2461
6097 T t2462 o b2462 b4
6098 B b2463 t2462
6099 T t2463 o b2460 b2463
6100 B b2464 t2463
6101 T t2464 o2436 b935 b2458 b2464 b4
6102 B b2465 t2464
6103 T t2465 o b2465 b4
6104