/[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 3463 - (show annotations) (download)
Sat Dec 8 03:17:49 2001 UTC (19 years, 7 months ago) by nogin
File size: 117380 byte(s)
Fixed bug #10 - now the term_match_table fall-back mechanism is more complete.
This broke couple of proofs, I fixed them.

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 T t1 o b973 b4
2545 B b1 t1
2546 T t2 o b970 b1
2547 B b2 t2
2548 T t3 o936 b960 b2
2549 B b3 t3
2550 P p973 String wf
2551 O o973 tactic_arg p973
2552 B b974 t949 v_2
2553 T t974 o711 b974
2554 S s974 t620 h h947 h957
2555 G s974 t974
2556 B b975 s974
2557 T t975 o938 b975 b944
2558 B b976 t975
2559 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2560 O o976 fun_prop
2561 P p976 Var v_2
2562 O o977 var p976
2563 T t977 o977
2564 B b977 t977
2565 T t978 o738 b977 b949
2566 B b978 t978 v_2
2567 T t979 o976 b978
2568 S s979 t620 h h947 h957
2569 G s979 t979
2570 B b979 s979
2571 T t980 o938 b979 b944
2572 B b980 t980
2573 NSummary!arg_named arg_named arg_named Summary
2574 P p980 String d_auto
2575 O o980 arg_named p980
2576 NSummary!arg_bool arg_bool arg_bool Summary
2577 P p981 String true
2578 O o981 arg_bool p981
2579 T t981 o981
2580 B b981 t981
2581 T t982 o980 b981
2582 B b982 t982
2583 T t983 o b982 b4
2584 B b983 t983
2585 T t984 o973 b980 b983 b969
2586 B b984 t984
2587 T t985 o2 b984
2588 B b985 t985
2589 T t986 o973 b976 b4 b985
2590 B b986 t986
2591 P p990 String autoT
2592 O o990 ext_rule p990
2593 T t991 o936 b970 b4
2594 B b991 t991
2595 T t992 o990 b935 b991 b4 b4
2596 B b992 t992
2597 P p992 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2598 O o992 ext_rule p992
2599 T t993 o559 b893 b674
2600 B b993 t993
2601 T t994 o738 b949 b993
2602 S s994 t620 h h947 h957 h971
2603 G s994 t994
2604 B b994 s994
2605 T t995 o938 b994 b944
2606 B b995 t995
2607 T t996 o2 b973
2608 B b996 t996
2609 T t997 o966 b995 b4 b996
2610 B b997 t997
2611 T t998 o738 b966 b993
2612 H h998 v_3 t998
2613 S s998 t620 h h947 h957 h971 h998
2614 G s998 t925
2615 B b998 s998
2616 T t999 o938 b998 b944
2617 B b999 t999
2618 T t1000 o937 b999 b4 b996
2619 B b1000 t1000
2620 T t214 o b1000 b4
2621 B b214 t214
2622 T t215 o b997 b214
2623 B b215 t215
2624 T t218 o936 b973 b215
2625 B b218 t218
2626 B b1001 t966 v_3
2627 T t1001 o711 b1001
2628 S s1001 t620 h h947 h957 h971
2629 G s1001 t1001
2630 B b1002 s1001
2631 T t1002 o938 b1002 b944
2632 B b1003 t1002
2633 P p1003 Var v_3
2634 O o1003 var p1003
2635 T t1003 o1003
2636 B b1004 t1003
2637 T t1004 o738 b966 b1004
2638 B b1005 t1004 v_3
2639 T t1005 o976 b1005
2640 S s1005 t620 h h947 h957 h971
2641 G s1005 t1005
2642 B b1006 s1005
2643 T t1006 o938 b1006 b944
2644 B b1007 t1006
2645 T t1007 o973 b1007 b983 b996
2646 B b1008 t1007
2647 T t1008 o2 b1008
2648 B b1009 t1008
2649 T t1009 o973 b1003 b4 b1009
2650 B b1010 t1009
2651 T t1014 o936 b997 b4
2652 B b1015 t1014
2653 T t1015 o990 b935 b1015 b4 b4
2654 B b1016 t1015
2655 P p1016 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2656 O o1016 ext_rule p1016
2657 T t1016 o559 b567 b561
2658 B b1017 t1016
2659 T t1017 o559 b567 b674
2660 B b1018 t1017
2661 T t1018 o738 b1017 b1018
2662 H h1018 v_4 t1018
2663 S s1018 t620 h h947 h957 h971 h998 h1018
2664 G s1018 t925
2665 B b1019 s1018
2666 T t1019 o938 b1019 b944
2667 B b1020 t1019
2668 T t1020 o2 b1000
2669 B b1021 t1020
2670 T t1021 o937 b1020 b4 b1021
2671 B b1022 t1021
2672 T t1022 o b1022 b4
2673 B b1023 t1022
2674 T t1023 o936 b1000 b1023
2675 B b1024 t1023
2676 P p1024 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2677 O o1024 ext_rule p1024
2678 T t1024 o738 b561 b1018
2679 H h1024 v_5 t1024
2680 S s1024 t620 h h947 h957 h971 h998 h1018 h1024
2681 G s1024 t925
2682 B b1025 s1024
2683 T t1025 o938 b1025 b944
2684 B b1026 t1025
2685 T t1026 o2 b1022
2686 B b1027 t1026
2687 T t1027 o937 b1026 b4 b1027
2688 B b1028 t1027
2689 T t219 o b1028 b4
2690 B b219 t219
2691 T t229 o936 b1022 b219
2692 B b229 t229
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 P p1041 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2719 O o1041 ext_rule p1041
2720 H h1041 v_6 t925
2721 S s1041 t620 h h947 h957 h971 h998 h1018 h1024 h1041
2722 G s1041 t925
2723 B b1042 s1041
2724 T t1042 o938 b1042 b944
2725 B b1043 t1042
2726 T t1043 o2 b1028
2727 B b1044 t1043
2728 T t1044 o937 b1043 b4 b1044
2729 B b1045 t1044
2730 T t1045 o b1045 b4
2731 B b1046 t1045
2732 T t1046 o936 b1028 b1046
2733 B b1047 t1046
2734 P p1047 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2735 O o1047 ext_rule p1047
2736 T t1047 o936 b1045 b4
2737 B b1048 t1047
2738 T t1048 o1047 b935 b1048 b4 b4
2739 B b1049 t1048
2740 T t1049 o b1049 b4
2741 B b1050 t1049
2742 P p1050 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2743 O o1050 ext_rule p1050
2744 B b1051 t1016 v_6
2745 T t1051 o711 b1051
2746 S s1051 t620 h h947 h957 h971 h998 h1018 h1024
2747 G s1051 t1051
2748 B b1052 s1051
2749 T t1052 o938 b1052 b944
2750 B b1053 t1052
2751 P p1053 Var v_6
2752 O o1053 var p1053
2753 T t1053 o1053
2754 B b1054 t1053
2755 T t1054 o738 b1017 b1054
2756 B b1055 t1054 v_6
2757 T t1055 o976 b1055
2758 S s1055 t620 h h947 h957 h971 h998 h1018 h1024
2759 G s1055 t1055
2760 B b1056 s1055
2761 T t1056 o938 b1056 b944
2762 B b1057 t1056
2763 T t1057 o973 b1057 b983 b1044
2764 B b1058 t1057
2765 T t1058 o2 b1058
2766 B b1059 t1058
2767 T t1059 o973 b1053 b4 b1059
2768 B b1060 t1059
2769 T t1060 o936 b1060 b4
2770 B b1061 t1060
2771 T t1061 o1050 b935 b1061 b4 b4
2772 B b1062 t1061
2773 T t1062 o b1062 b4
2774 B b1063 t1062
2775 T t1063 o1041 b935 b1047 b1050 b1063
2776 B b1064 t1063
2777 T t230 o b1064 b4
2778 B b230 t230
2779 T t1064 o936 b1038 b4
2780 B b1065 t1064
2781 T t1065 o1050 b935 b1065 b4 b4
2782 B b1066 t1065
2783 T t1066 o b1066 b4
2784 B b1067 t1066
2785 T t233 o1024 b935 b229 b230 b1067
2786 B b233 t233
2787 T t237 o b233 b4
2788 B b237 t237
2789 T t238 o1016 b935 b1024 b237 b4
2790 B b238 t238
2791 T t239 o b238 b4
2792 B b239 t239
2793 T t242 o b1016 b239
2794 B b242 t242
2795 P p1071 String "rwh unfold_fun_set 0 thenT autoT"
2796 O o1071 ext_rule p1071
2797 T t1071 o936 b1010 b4
2798 B b1072 t1071
2799 T t1072 o1071 b935 b1072 b4 b4
2800 B b1073 t1072
2801 T t1073 o b1073 b4
2802 B b1074 t1073
2803 T t243 o992 b935 b218 b242 b1074
2804 B b243 t243
2805 T t251 o b243 b4
2806 B b251 t251
2807 T t256 o b992 b251
2808 B b256 t256
2809 T t1077 o936 b986 b4
2810 B b1078 t1077
2811 T t1078 o1071 b935 b1078 b4 b4
2812 B b1079 t1078
2813 T t1079 o b1079 b4
2814 B b1080 t1079
2815 T t257 o965 b935 b3 b256 b1080
2816 B b257 t257
2817 T t265 o b257 b4
2818 B b265 t265
2819 T t266 o b965 b265
2820 B b266 t266
2821 NSummary!ext_goal ext_goal ext_goal Summary
2822 O o1085 ext_goal
2823 S s1085 t620 h
2824 G s1085 t950
2825 B b1086 s1085
2826 T t1086 o938 b1086 b944
2827 B b1087 t1086
2828 T t1087 o947 b1087 b4 b954
2829 B b1088 t1087
2830 T t1088 o1085 b1088
2831 B b1089 t1088
2832 T t1089 o b1089 b4
2833 B b1090 t1089
2834 T t1090 o963 b935 b1089 b1090 b4
2835 B b1091 t1090
2836 P p1091 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2837 O o1091 ext_rule p1091
2838 H h1091 v t950
2839 S s1091 t620 h h1091
2840 G s1091 t925
2841 B b1092 s1091
2842 T t1092 o938 b1092 b944
2843 B b1093 t1092
2844 T t1093 o937 b1093 b4 b954
2845 B b1094 t1093
2846 T t1094 o1085 b1094
2847 B b1095 t1094
2848 P p1095 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2849 O o1095 ext_rule p1095
2850 P p1096 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2851 O o1096 ext_rule p1096
2852 T t1096 o b1095 b4
2853 B b1096 t1096
2854 H h1096 x t923
2855 H h1097 v_1 t971
2856 H h1098 v_2 t998
2857 H h1099 v_3 t1018
2858 H h1100 v_4 t1024
2859 B b1100 t1016 v_5
2860 T t1100 o711 b1100
2861 S s1100 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2862 G s1100 t1100
2863 B b1101 s1100
2864 T t1101 o b737 b4
2865 B b1102 t1101
2866 T t1102 o b657 b1102
2867 B b1103 t1102
2868 T t1103 o b655 b1103
2869 B b1104 t1103
2870 T t1104 o b675 b1104
2871 B b1105 t1104
2872 T t1105 o b640 b1105
2873 B b1106 t1105
2874 T t1106 o b638 b1106
2875 B b1107 t1106
2876 T t1107 o938 b1101 b1107
2877 B b1108 t1107
2878 T t1108 o738 b1017 b1032
2879 B b1109 t1108 v_5
2880 T t1109 o976 b1109
2881 S s1109 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2882 G s1109 t1109
2883 B b1110 s1109
2884 T t1110 o938 b1110 b1107
2885 B b1111 t1110
2886 S s1111 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2887 G s1111 t925
2888 B b1112 s1111
2889 T t1112 o938 b1112 b1107
2890 B b1113 t1112
2891 S s1113 t620 h h1096 h1091 h1097 h1098 h1099
2892 G s1113 t925
2893 B b1114 s1113
2894 T t1114 o938 b1114 b1107
2895 B b1115 t1114
2896 S s1115 t620 h h1096 h1091 h1097 h1098
2897 G s1115 t925
2898 B b1116 s1115
2899 T t1116 o938 b1116 b1107
2900 B b1117 t1116
2901 S s1117 t620 h h1096 h1091 h1097
2902 G s1117 t925
2903 B b1118 s1117
2904 T t1118 o938 b1118 b1107
2905 B b1119 t1118
2906 S s1119 t620 h h1096 h1091
2907 G s1119 t925
2908 B b1120 s1119
2909 T t1120 o938 b1120 b1107
2910 B b1121 t1120
2911 S s1121 t620 h h1096
2912 G s1121 t925
2913 B b1122 s1121
2914 T t1122 o938 b1122 b1107
2915 B b1123 t1122
2916 T t1123 o937 b1123 b4 b946
2917 B b1124 t1123
2918 T t1124 o2 b1124
2919 B b1125 t1124
2920 T t1125 o937 b1121 b4 b1125
2921 B b1126 t1125
2922 T t1126 o2 b1126
2923 B b1127 t1126
2924 T t1127 o937 b1119 b4 b1127
2925 B b1128 t1127
2926 T t1128 o2 b1128
2927 B b1129 t1128
2928 T t1129 o937 b1117 b4 b1129
2929 B b1130 t1129
2930 T t1130 o2 b1130
2931 B b1131 t1130
2932 T t1131 o937 b1115 b4 b1131
2933 B b1132 t1131
2934 T t1132 o2 b1132
2935 B b1133 t1132
2936 T t1133 o937 b1113 b4 b1133
2937 B b1134 t1133
2938 T t1134 o2 b1134
2939 B b1135 t1134
2940 T t1135 o973 b1111 b983 b1135
2941 B b1136 t1135
2942 T t1136 o2 b1136
2943 B b1137 t1136
2944 T t1137 o973 b1108 b4 b1137
2945 B b1138 t1137
2946 T t1138 o936 b1138 b4
2947 B b1139 t1138
2948 T t1139 o1050 b935 b1139 b4 b4
2949 B b1140 t1139
2950 T t1140 o b1140 b4
2951 B b1141 t1140
2952 T t1141 o1096 b935 b1095 b1096 b1141
2953 B b1142 t1141
2954 T t1142 o b1142 b4
2955 B b1143 t1142
2956 B b1144 t1017 v_4
2957 T t1144 o711 b1144
2958 S s1144 t620 h h1096 h1091 h1097 h1098 h1099
2959 G s1144 t1144
2960 B b1145 s1144
2961 T t1145 o938 b1145 b1107
2962 B b1146 t1145
2963 P p1146 Var v_4
2964 O o1146 var p1146
2965 T t1146 o1146
2966 B b1147 t1146
2967 T t1147 o738 b1147 b1018
2968 B b1148 t1147 v_4
2969 T t1148 o976 b1148
2970 S s1148 t620 h h1096 h1091 h1097 h1098 h1099
2971 G s1148 t1148
2972 B b1149 s1148
2973 T t1149 o938 b1149 b1107
2974 B b1150 t1149
2975 T t1150 o973 b1150 b983 b1133
2976 B b1151 t1150
2977 T t1151 o2 b1151
2978 B b1152 t1151
2979 T t1152 o973 b1146 b4 b1152
2980 B b1153 t1152
2981 T t1153 o936 b1153 b4
2982 B b1154 t1153
2983 T t1154 o1050 b935 b1154 b4 b4
2984 B b1155 t1154
2985 T t1155 o b1155 b4
2986 B b1156 t1155
2987 T t1156 o1024 b935 b1095 b1143 b1156
2988 B b1157 t1156
2989 T t1157 o b1157 b4
2990 B b1158 t1157
2991 T t1158 o1016 b935 b1095 b1158 b4
2992 B b1159 t1158
2993 T t1159 o b1159 b4
2994 B b1160 t1159
2995 S s1160 t620 h h1096 h1091 h1097
2996 G s1160 t994
2997 B b1161 s1160
2998 T t1161 o938 b1161 b1107
2999 B b1162 t1161
3000 T t1162 o966 b1162 b4 b1129
3001 B b1163 t1162
3002 T t1163 o936 b1163 b4
3003 B b1164 t1163
3004 T t1164 o990 b935 b1164 b4 b4
3005 B b1165 t1164
3006 P p1165 String "rwh unfold_fun_prop 0 thenT autoT"
3007 O o1165 ext_rule p1165
3008 T t1165 o738 b966 b977
3009 B b1166 t1165 v_2
3010 T t1166 o976 b1166
3011 S s1166 t620 h h1096 h1091 h1097
3012 G s1166 t1166
3013 B b1167 s1166
3014 T t1167 o938 b1167 b1107
3015 B b1168 t1167
3016 T t1168 o973 b1168 b4 b1129
3017 B b1169 t1168
3018 NCzf_itt_set!set set set Czf_itt_set
3019 O o1169 set
3020 T t1169 o1169
3021 H h1169 s1_1 t1169
3022 H h1170 s2_1 t1169
3023 P p1170 Var s1_1
3024 O o1170 var p1170
3025 T t1170 o1170
3026 B b1170 t1170
3027 P p1171 Var s2_1
3028 O o1171 var p1171
3029 T t1171 o1171
3030 B b1171 t1171
3031 T t1172 o738 b1170 b1171
3032 H h1172 x_1 t1172
3033 T t1173 o738 b966 b1170
3034 H h1173 x_2 t1173
3035 T t1174 o676 b966 b1171
3036 S s1174 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3037 G s1174 t1174
3038 B b1174 s1174
3039 T t1175 o938 b1174 b1107
3040 B b1175 t1175
3041 T t1176 o738 b966 b1171
3042 S s1176 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3043 G s1176 t1176
3044 B b1176 s1176
3045 T t1177 o938 b1176 b1107
3046 B b1177 t1177
3047 NItt_logic Itt_logic Itt_logic NIL
3048 NItt_logic!implies implies implies Itt_logic
3049 O o1177 implies
3050 B b1178 t1173
3051 B b1179 t1176
3052 T t1179 o1177 b1178 b1179
3053 S s1179 t620 h h1096 h1091 h1097 h1169 h1170 h1172
3054 G s1179 t1179
3055 B b1180 s1179
3056 T t1180 o938 b1180 b1107
3057 B b1181 t1180
3058 B b1182 t1172
3059 B b1183 t1179
3060 T t1183 o1177 b1182 b1183
3061 S s1183 t620 h h1096 h1091 h1097 h1169 h1170
3062 G s1183 t1183
3063 B b1184 s1183
3064 T t1184 o938 b1184 b1107
3065 B b1185 t1184
3066 NItt_logic!all all all Itt_logic
3067 O o1185 all
3068 B b1186 t1169
3069 B b1187 t1183 s2_1
3070 T t1187 o1185 b1186 b1187
3071 S s1187 t620 h h1096 h1091 h1097 h1169
3072 G s1187 t1187
3073 B b1188 s1187
3074 T t1188 o938 b1188 b1107
3075 B b1189 t1188
3076 B b1190 t1187 s1_1
3077 T t1190 o1185 b1186 b1190
3078 S s1190 t620 h h1096 h1091 h1097
3079 G s1190 t1190
3080 B b1191 s1190
3081 T t1191 o938 b1191 b1107
3082 B b1192 t1191
3083 T t1192 o2 b1169
3084 B b1193 t1192
3085 T t1193 o973 b1192 b983 b1193
3086 B b1194 t1193
3087 T t1194 o2 b1194
3088 B b1195 t1194
3089 T t1195 o937 b1189 b983 b1195
3090 B b1196 t1195
3091 T t1196 o2 b1196
3092 B b1197 t1196
3093 T t1197 o937 b1185 b983 b1197
3094 B b1198 t1197
3095 T t1198 o2 b1198
3096 B b1199 t1198
3097 T t1199 o937 b1181 b983 b1199
3098 B b1200 t1199
3099 T t1200 o2 b1200
3100 B b1201 t1200
3101 T t1201 o937 b1177 b983 b1201
3102 B b1202 t1201
3103 T t1202 o2 b1202
3104 B b1203 t1202
3105 T t1203 o937 b1175 b4 b1203
3106 B b1204 t1203
3107 T t1204 o b1204 b4
3108 B b1205 t1204
3109 T t1205 o936 b1169 b1205
3110 B b1206 t1205
3111 P p1206 String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3112 O o1206 ext_rule p1206
3113 T t1206 o936 b1204 b4
3114 B b1207 t1206
3115 T t1207 o1206 b935 b1207 b4 b4
3116 B b1208 t1207
3117 T t1208 o b1208 b4
3118 B b1209 t1208
3119 T t1209 o1165 b935 b1206 b1209 b4
3120 B b1210 t1209
3121 T t1210 o b1210 b4
3122 B b1211 t1210
3123 T t1211 o b1165 b1211
3124 B b1212 t1211
3125 T t1212 o1095 b935 b1095 b1160 b1212
3126 B b1213 t1212
3127 T t1213 o b1213 b4
3128 B b1214 t1213
3129 S s1214 t620 h h1096 h1091
3130 G s1214 t967
3131 B b1215 s1214
3132 T t1215 o938 b1215 b1107
3133 B b1216 t1215
3134 T t1216 o966 b1216 b4 b1127
3135 B b1217 t1216
3136 T t1217 o936 b1217 b4
3137 B b1218 t1217
3138 T t1218 o990 b935 b1218 b4 b4
3139 B b1219 t1218
3140 P p1219 Var v_1
3141 O o1219 var p1219
3142 T t1219 o1219
3143 B b1220 t1219
3144 T t1220 o738 b1220 b949
3145 B b1221 t1220 v_1
3146 T t1221 o976 b1221
3147 S s1221 t620 h h1096 h1091
3148 G s1221 t1221
3149 B b1222 s1221
3150 T t1222 o938 b1222 b1107
3151 B b1223 t1222
3152 T t1223 o973 b1223 b4 b1127
3153 B b1224 t1223
3154 H h1224 s2 t1169
3155 T t1224 o738 b1170 b561
3156 H h1225 x_1 t1224
3157 T t1225 o738 b1170 b949
3158 H h1226 x_2 t1225
3159 T t1226 o676 b561 b949
3160 S s1226 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3161 G s1226 t1226
3162 B b1226 s1226
3163 T t1227 o938 b1226 b1107
3164 B b1227 t1227
3165 T t1228 o738 b561 b949
3166 S s1228 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3167 G s1228 t1228
3168 B b1228 s1228
3169 T t1229 o938 b1228 b1107
3170 B b1229 t1229
3171 B b1230 t1225
3172 B b1231 t1228
3173 T t1231 o1177 b1230 b1231
3174 S s1231 t620 h h1096 h1091 h1169 h1224 h1225
3175 G s1231 t1231
3176 B b1232 s1231
3177 T t1232 o938 b1232 b1107
3178 B b1233 t1232
3179 B b1234 t1224
3180 B b1235 t1231
3181 T t1235 o1177 b1234 b1235
3182 S s1235 t620 h h1096 h1091 h1169 h1224
3183 G s1235 t1235
3184 B b1236 s1235
3185 T t1236 o938 b1236 b1107
3186 B b1237 t1236
3187 B b1238 t1235 s2
3188 T t1238 o1185 b1186 b1238
3189 S s1238 t620 h h1096 h1091 h1169
3190 G s1238 t1238
3191 B b1239 s1238
3192 T t1239 o938 b1239 b1107
3193 B b1240 t1239
3194 B b1241 t1238 s1_1
3195 T t1241 o1185 b1186 b1241
3196 S s1241 t620 h h1096 h1091
3197 G s1241 t1241
3198 B b1242 s1241
3199 T t1242 o938 b1242 b1107
3200 B b1243 t1242
3201 T t1243 o2 b1224
3202 B b1244 t1243
3203 T t1244 o973 b1243 b983 b1244
3204 B b1245 t1244
3205 T t1245 o2 b1245
3206 B b1246 t1245
3207 T t1246 o937 b1240 b983 b1246
3208 B b1247 t1246
3209 T t1247 o2 b1247
3210 B b1248 t1247
3211 T t1248 o937 b1237 b983 b1248
3212 B b1249 t1248
3213 T t1249 o2 b1249
3214 B b1250 t1249
3215 T t1250 o937 b1233 b983 b1250
3216 B b1251 t1250
3217 T t1251 o2 b1251
3218 B b1252 t1251
3219 T t1252 o937 b1229 b983 b1252
3220 B b1253 t1252
3221 T t1253 o2 b1253
3222 B b1254 t1253
3223 T t1254 o937 b1227 b4 b1254
3224 B b1255 t1254
3225 T t1255 o b1255 b4
3226 B b1256 t1255
3227 T t1256 o936 b1224 b1256
3228 B b1257 t1256
3229 P p1257 String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3230 O o1257 ext_rule p1257
3231 T t1257 o936 b1255 b4
3232 B b1258 t1257
3233 T t1258 o1257 b935 b1258 b4 b4
3234 B b1259 t1258
3235 T t1259 o b1259 b4
3236 B b1260 t1259
3237 T t1260 o1165 b935 b1257 b1260 b4
3238 B b1261 t1260
3239 T t1261 o b1261 b4
3240 B b1262 t1261
3241 T t1262 o b1219 b1262
3242 B b1263 t1262
3243 T t1263 o1091 b935 b1095 b1214 b1263
3244 B b1264 t1263
3245 P p1264 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3246 O o1264 ext_rule p1264
3247 H h1264 y_1 t642
3248 T t1264 o620 b695
3249 H h1265 z_1 t1264
3250 T t1265 o676 b562 b695
3251 H h1266 z t1265
3252 T t1266 o676 b948 b949
3253 H h1267 v t1266
3254 T t1267 o676 b561 b674
3255 S s1267 t620 h h1264 h1265 h1266 h1267
3256 G s1267 t1267
3257 B b1267 s1267
3258 T t1268 o938 b1267 b1107
3259 B b1268 t1268
3260 S s1268 t620 h h1264 h1265 h1266 h1267
3261 G s1268 t925
3262 B b1269 s1268
3263 T t1269 o938 b1269 b1107
3264 B b1270 t1269
3265 NItt_logic!and and and Itt_logic
3266 O o1270 and
3267 B b1271 t642
3268 B b1272 t1264
3269 T t1272 o1270 b1271 b1272
3270 H h1272 y t1272
3271 S s1272 t620 h h1272 h1266 h1267
3272 G s1272 t925
3273 B b1273 s1272
3274 T t1273 o938 b1273 b1107
3275 B b1274 t1273
3276 B b1275 t1272
3277 B b1276 t1265
3278 T t1276 o1270 b1275 b1276
3279 H h1276 x t1276
3280 S s1276 t620 h h1276 h1267
3281 G s1276 t925
3282 B b1277 s1276
3283 T t1277 o938 b1277 b1107
3284 B b1278 t1277
3285 S s1278 t620 h h1276
3286 G s1278 t925
3287 B b1279 s1278
3288 T t1279 o938 b1279 b1107
3289 B b1280 t1279
3290 T t1280 o937 b1280 b4 b1125
3291 B b1281 t1280
3292 T t1281 o2 b1281
3293 B b1282 t1281
3294 T t1282 o937 b1278 b4 b1282
3295 B b1283 t1282
3296 T t1283 o2 b1283
3297 B b1284 t1283
3298 T t1284 o937 b1274 b4 b1284
3299 B b1285 t1284
3300 T t1285 o2 b1285
3301 B b1286 t1285
3302 T t1286 o937 b1270 b983 b1286
3303 B b1287 t1286
3304 T t1287 o2 b1287
3305 B b1288 t1287
3306 T t1288 o937 b1268 b4 b1288
3307 B b1289 t1288
3308 T t1289 o676 b966 b949
3309 H h1289 v_1 t1289
3310 S s1289 t620 h h1264 h1265 h1266 h1267 h1289
3311 G s1289 t1267
3312 B b1290 s1289
3313 T t1290 o938 b1290 b1107
3314 B b1291 t1290
3315 T t1291 o2 b1289
3316 B b1292 t1291
3317 T t1292 o937 b1291 b4 b1292
3318 B b1293 t1292
3319 T t268 o b1293 b4
3320 B b268 t268
3321 T t269 o936 b1289 b268
3322 B b269 t269
3323 B b1294 t949 v_1
3324 T t1294 o711 b1294
3325 S s1294 t620 h h1264 h1265 h1266 h1267
3326 G s1294 t1294
3327 B b1295 s1294
3328 T t1295 o938 b1295 b1107
3329 B b1296 t1295
3330 T t1296 o676 b1220 b949
3331 B b1297 t1296 v_1
3332 T t1297 o976 b1297
3333 S s1297 t620 h h1264 h1265 h1266 h1267
3334 G s1297 t1297
3335 B b1298 s1297
3336 T t1298 o938 b1298 b1107
3337 B b1299 t1298
3338 T t1299 o973 b1299 b983 b1292
3339 B b1300 t1299
3340 T t1300 o2 b1300
3341 B b1301 t1300
3342 T t1301 o973 b1296 b4 b1301
3343 B b1302 t1301
3344 P p1305 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3345 O o1305 ext_rule p1305
3346 T t1305 o676 b966 b993
3347 H h1305 v_2 t1305
3348 S s1305 t620 h h1264 h1265 h1266 h1267 h1289 h1305
3349 G s1305 t1267
3350 B b1306 s1305
3351 T t1306 o938 b1306 b1107
3352 B b1307 t1306
3353 T t1307 o2 b1293
3354 B b1308 t1307
3355 T t1308 o937 b1307 b4 b1308
3356 B b1309 t1308
3357 T t270 o b1309 b4
3358 B b270 t270
3359 T t273 o936 b1293 b270
3360 B b273 t273
3361 B b1310 t966 v_2
3362 T t1310 o711 b1310
3363 S s1310 t620 h h1264 h1265 h1266 h1267 h1289
3364 G s1310 t1310
3365 B b1311 s1310
3366 T t1311 o938 b1311 b1107
3367 B b1312 t1311
3368 T t1312 o676 b966 b977
3369 B b1313 t1312 v_2
3370 T t1313 o976 b1313
3371 S s1313 t620 h h1264 h1265 h1266 h1267 h1289
3372 G s1313 t1313
3373 B b1314 s1313
3374 T t1314 o938 b1314 b1107
3375 B b1315 t1314
3376 T t1315 o973 b1315 b983 b1308
3377 B b1316 t1315
3378 T t1316 o2 b1316
3379 B b1317 t1316
3380 T t1317 o973 b1312 b4 b1317
3381 B b1318 t1317
3382 P p1321 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3383 O o1321 ext_rule p1321
3384 T t1321 o676 b1017 b1018
3385 H h1321 v_3 t1321
3386 S s1321 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3387 G s1321 t1267
3388 B b1322 s1321
3389 T t1322 o938 b1322 b1107
3390 B b1323 t1322
3391 T t1323 o2 b1309
3392 B b1324 t1323
3393 T t1324 o937 b1323 b4 b1324
3394 B b1325 t1324
3395 T t1325 o b1325 b4
3396 B b1326 t1325
3397 T t1326 o936 b1309 b1326
3398 B b1327 t1326
3399 P p1327 String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"
3400 O o1327 ext_rule p1327
3401 T t1327 o676 b561 b1018
3402 H h1327 v_4 t1327
3403 S s1327 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1327
3404 G s1327 t1267
3405 B b1328 s1327
3406 T t1328 o938 b1328 b1107
3407 B b1329 t1328
3408 T t1329 o2 b1325
3409 B b1330 t1329
3410 T t1330 o937 b1329 b4 b1330
3411 B b1331 t1330
3412 T t274 o b1331 b4
3413 B b274 t274
3414 T t289 o936 b1325 b274
3415 B b289 t289
3416 S s1331 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3417 G s1331 t1144
3418 B b1332 s1331
3419 T t1332 o938 b1332 b1107
3420 B b1333 t1332
3421 T t1333 o676 b1147 b1018
3422 B b1334 t1333 v_4
3423 T t1334 o976 b1334
3424 S s1334 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3425 G s1334 t1334
3426 B b1335 s1334
3427 T t1335 o938 b1335 b1107
3428 B b1336 t1335
3429 T t1336 o973 b1336 b983 b1330
3430 B b1337 t1336
3431 T t1337 o2 b1337
3432 B b1338 t1337
3433 T t1338 o973 b1333 b4 b1338
3434 B b1339 t1338
3435 P p1342 String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3436 O o1342 ext_rule p1342
3437 T t1342 o936 b1331 b4
3438 B b1343 t1342
3439 T t1343 o1342 b935 b1343 b4 b4
3440 B b1344 t1343
3441 T t290 o b1344 b4
3442 B b290 t290
3443 T t292 o936 b1339 b4
3444 B b292 t292
3445 T t300 o1071 b935 b292 b4 b4
3446 B b300 t300
3447 T t301 o b300 b4
3448 B b301 t301
3449 T t304 o1327 b935 b289 b290 b301
3450 B b304 t304
3451 T t309 o b304 b4
3452 B b309 t309
3453 T t310 o1321 b935 b1327 b309 b4
3454 B b310 t310
3455 T t315 o b310 b4
3456 B b315 t315
3457 H h1344 s1 t1169
3458 T t1344 o738 b560 b561
3459 H h1345 x t1344
3460 B b1347 t1344
3461 T t1374 o936 b1318 b4
3462 B b1375 t1374
3463 T t1375 o1071 b935 b1375 b4 b4
3464 B b1376 t1375
3465 P p1378 String "eqSetSymT thenT autoT"
3466 O o1378 ext_rule p1378
3467 T t1378 o676 b949 b993
3468 S s1378 t620 h h1264 h1265 h1266 h1267 h1289
3469 G s1378 t1378
3470 B b1379 s1378
3471 T t1379 o938 b1379 b1107
3472 B b1380 t1379
3473 S s1380 t620 h h1264 h1265 h1266 h1267 h1289
3474 G s1380 t994
3475 B b1381 s1380
3476 T t1381 o938 b1381 b1107
3477 B b1382 t1381
3478 T t1382 o966 b1382 b983 b1308
3479 B b1383 t1382
3480 T t1383 o2 b1383
3481 B b1384 t1383
3482 T t1384 o966 b1380 b4 b1384
3483 B b1385 t1384
3484 T t1385 o676 b993 b949
3485 S s1385 t620 h h1264 h1265 h1266 h1267 h1289
3486 G s1385 t1385
3487 B b1386 s1385
3488 T t1386 o938 b1386 b1107
3489 B b1387 t1386
3490 T t1387 o2 b1385
3491 B b1388 t1387
3492 T t1388 o966 b1387 b4 b1388
3493 B b1389 t1388
3494 T t1389 o b1389 b4
3495 B b1390 t1389
3496 T t1390 o936 b1385 b1390
3497 B b1391 t1390
3498 T t1391 o1085 b1389
3499 B b1392 t1391
3500 T t1392 o b1392 b4
3501 B b1393 t1392
3502 T t1393 o1378 b935 b1391 b1393 b4
3503 B b1394 t1393
3504 T t1394 o b1394 b4
3505 B b1395 t1394
3506 T t316 o b1376 b1395
3507 B b316 t316
3508 T t318 o1305 b935 b273 b315 b316
3509 B b318 t318
3510 T t320 o b318 b4
3511 B b320 t320
3512 T t1396 o936 b1302 b4
3513 B b1397 t1396
3514 T t1397 o1071 b935 b1397 b4 b4
3515 B b1398 t1397
3516 T t1400 o676 b948 b966
3517 S s1400 t620 h h1264 h1265 h1266 h1267
3518 G s1400 t1400
3519 B b1401 s1400
3520 T t1401 o938 b1401 b1107
3521 B b1402 t1401
3522 S s1402 t620 h h1264 h1265 h1266 h1267
3523 G s1402 t967
3524 B b1403 s1402
3525 T t1403 o938 b1403 b1107
3526 B b1404 t1403
3527 T t1404 o966 b1404 b983 b1292
3528 B b1405 t1404
3529 T t1405 o2 b1405
3530 B b1406 t1405
3531 T t1406 o966 b1402 b4 b1406
3532 B b1407 t1406
3533 T t1407 o676 b966 b948
3534 S s1407 t620 h h1264 h1265 h1266 h1267
3535 G s1407 t1407
3536 B b1408 s1407
3537 T t1408 o938 b1408 b1107
3538 B b1409 t1408
3539 T t1409 o2 b1407
3540 B b1410 t1409
3541 T t1410 o966 b1409 b4 b1410
3542 B b1411 t1410
3543 T t1411 o b1411 b4
3544 B b1412 t1411
3545 T t1412 o936 b1407 b1412
3546 B b1413 t1412
3547 T t1413 o1085 b1411
3548 B b1414 t1413
3549 T t1414 o b1414 b4
3550 B b1415 t1414
3551 T t1415 o1378 b935 b1413 b1415 b4
3552 B b1416 t1415
3553 T t1416 o b1416 b4
3554 B b1417 t1416
3555 T t327 o b1398 b1417
3556 B b327 t327
3557 T t331 o1264 b935 b269 b320 b327
3558 B b331 t331
3559 T t332 o b331 b4
3560 B b332 t332
3561 T t335 o b1264 b332
3562 B b335 t335
3563 T t339 o b1091 b335
3564 B b339 t339
3565 T t340 o934 b935 b963 b266 b339
3566 B b340 t340
3567 T t359 o933 b340
3568 B b359 t359
3569 P p1423 Number 5390
3570 P p1424 Number 5398
3571 O o1424 resource_defs p1423 p1424 p264
3572 P p1425 Number 5396
3573 O o1425 uid p1425 p1424
3574 T t1425 o1425 b626
3575 B b1425 t1425
3576 T t1426 o b1425 b4
3577 B b1426 t1426
3578 T t1427 o1424 b1426
3579 B b1427 t1427
3580 T t1428 o b1427 b4
3581 B b1428 t1428
3582 T t370 o919 b922 b933 b359 b1428
3583 B b370 t370
3584 T t385 o918 b370
3585 B b385 t385
3586 P p1430 Number 5838
3587 P p1431 Number 6264
3588 O o1431 location p1430 p1431
3589 P p1432 String cancel2
3590 O o1432 rule p1432
3591 T t1432 o920 b674
3592 B b1432 t1432
3593 T t1433 o b1432 b4
3594 B b1433 t1433
3595 T t1434 o b617 b1433
3596 B b1434 t1434
3597 T t1435 o738 b695 b696
3598 S s1435 t620 h
3599 G s1435 t1435
3600 B b1435 s1435
3601 T t1436 o618 b1435
3602 B b1436 t1436
3603 S s1436 t620 h
3604 G s1436 t1344
3605 B b1437 s1436
3606 T t1437 o618 b1437
3607 B b1438 t1437
3608 T t1438 o635 b1436 b1438
3609 B b1439 t1438
3610 T t1439 o635 b738 b1439
3611 B b1440 t1439
3612 T t1440 o635 b658 b1440
3613 B b1441 t1440
3614 T t1441 o635 b656 b1441
3615 B b1442 t1441
3616 T t1442 o635 b676 b1442
3617 B b1443 t1442
3618 T t1443 o635 b641 b1443
3619 B b1444 t1443
3620 T t1444 o635 b639 b1444
3621 B b1445 t1444
3622 P p1445 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"
3623 O o1445 ext_rule p1445
3624 T t1445 o b1435 b4
3625 B b1446 t1445
3626 T t1446 o b737 b1446
3627 B b1447 t1446
3628 T t1447 o b657 b1447
3629 B b1448 t1447
3630 T t1448 o b655 b1448
3631 B b1449 t1448
3632 T t1449 o b675 b1449
3633 B b1450 t1449
3634 T t1450 o b640 b1450
3635 B b1451 t1450
3636 T t1451 o b638 b1451
3637 B b1452 t1451
3638 T t1452 o938 b1437 b1452
3639 B b1453 t1452
3640 T t1453 o937 b1453 b4 b946
3641 B b1454 t1453
3642 H h1454 v t1435
3643 T t1454 o572 b674
3644 B b1455 t1454
3645 T t1455 o559 b695 b1455
3646 B b1456 t1455
3647 T t1456 o559 b696 b1455
3648 B b1457 t1456
3649 T t1457 o738 b1456 b1457
3650 S s1457 t620 h h1454
3651 G s1457 t1457
3652 B b1458 s1457
3653 T t1458 o938 b1458 b1452
3654 B b1459 t1458
3655 S s1459 t620 h h1454
3656 G s1459 t1344
3657 B b1460 s1459
3658 T t1460 o938 b1460 b1452
3659 B b1461 t1460
3660 T t1461 o2 b1454
3661 B b1462 t1461
3662 T t1462 o937 b1461 b4 b1462
3663 B b1463 t1462
3664 T t1463 o2 b1463
3665 B b1464 t1463
3666 T t1464 o947 b1459 b4 b1464
3667 B b1465 t1464
3668 H h1465 v_1 t1457
3669 S s1465 t620 h h1454 h1465
3670 G s1465 t1344
3671 B b1466 s1465
3672 T t1466 o938 b1466 b1452
3673 B b1467 t1466
3674 T t1467 o937 b1467 b4 b1464
3675 B b1468 t1467
3676 T t1468 o b1468 b4
3677 B b1469 t1468
3678 T t1469 o b1465 b1469
3679 B b1470 t1469
3680 T t1470 o936 b1454 b1470
3681 B b1471 t1470
3682 T t1471 o936 b1465 b4
3683 B b1472 t1471
3684 T t1472 o963 b935 b1472 b4 b4
3685 B b1473 t1472
3686 P p1473 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
3687 O o1473 ext_rule p1473
3688 T t1473 o559 b674 b1455
3689 B b1474 t1473
3690 T t1474 o559 b560 b1474
3691 B b1475 t1474
3692 T t1475 o738 b1475 b1457
3693 H h1475 v_2 t1475
3694 S s1475 t620 h h1454 h1465 h1475
3695 G s1475 t1344
3696 B b1476 s1475
3697 T t1476 o938 b1476 b1452
3698 B b1477 t1476
3699 T t1477 o2 b1468
3700 B b1478 t1477
3701 T t1478 o937 b1477 b4 b1478
3702 B b1479 t1478
3703 T t391 o b1479 b4
3704 B b391 t391
3705 T t392 o936 b1468 b391
3706 B b392 t392
3707 B b1480 t1456 v_2
3708 T t1480 o711 b1480
3709 S s1480 t620 h h1454 h1465
3710 G s1480 t1480
3711 B b1481 s1480
3712 T t1481 o938 b1481 b1452
3713 B b1482 t1481
3714 T t1482 o738 b977 b1457
3715 B b1483 t1482 v_2
3716 T t1483 o976 b1483
3717 S s1483 t620 h h1454 h1465
3718 G s1483 t1483
3719 B b1484 s1483
3720 T t1484 o938 b1484 b1452
3721 B b1485 t1484
3722 T t1485 o973 b1485 b983 b1478
3723 B b1486 t1485
3724 T t1486 o2 b1486
3725 B b1487 t1486
3726 T t1487 o973 b1482 b4 b1487
3727 B b1488 t1487
3728 P p1491 String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
3729 O o1491 ext_rule p1491
3730 T t1491 o559 b561 b1474
3731 B b1492 t1491
3732 T t1492 o738 b1475 b1492
3733 H h1492 v_3 t1492
3734 S s1492 t620 h h1454 h1465 h1475 h1492
3735 G s1492 t1344
3736 B b1493 s1492
3737 T t1493 o938 b1493 b1452
3738 B b1494 t1493
3739 T t1494 o2 b1479
3740 B b1495 t1494
3741 T t1495 o937 b1494 b4 b1495
3742 B b1496 t1495
3743 T t393 o b1496 b4
3744 B b393 t393
3745 T t399 o936 b1479 b393
3746 B b399 t399
3747 B b1497 t1474 v_3
3748 T t1497 o711 b1497
3749 S s1497 t620 h h1454 h1465 h1475
3750 G s1497 t1497
3751 B b1498 s1497
3752 T t1498 o938 b1498 b1452
3753 B b1499 t1498
3754 T t1499 o738 b1475 b1004
3755 B b1500 t1499 v_3
3756 T t1500 o976 b1500
3757 S s1500 t620 h h1454 h1465 h1475
3758 G s1500 t1500
3759 B b1501 s1500
3760 T t1501 o938 b1501 b1452
3761 B b1502 t1501
3762 T t1502 o973 b1502 b983 b1495
3763 B b1503 t1502
3764 T t1503 o2 b1503
3765 B b1504 t1503
3766 T t1504 o973 b1499 b4 b1504
3767 B b1505 t1504
3768 P p1508 String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
3769 O o1508 ext_rule p1508
3770 T t1508 o559 b560 b567
3771 B b1509 t1508
3772 T t1509 o559 b561 b567
3773 B b1510 t1509
3774 T t1510 o738 b1509 b1510
3775 H h1510 v_4 t1510
3776 S s1510 t620 h h1454 h1465 h1475 h1492 h1510
3777 G s1510 t1344
3778 B b1511 s1510
3779 T t1511 o938 b1511 b1452
3780 B b1512 t1511
3781 T t1512 o2 b1496
3782 B b1513 t1512
3783 T t1513 o937 b1512 b4 b1513
3784 B b1514 t1513
3785 T t1514 o b1514 b4
3786 B b1515 t1514
3787 T t1515 o936 b1496 b1515
3788 B b1516 t1515
3789 P p1516 String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
3790 O o1516 ext_rule p1516
3791 T t1516 o738 b560 b1510
3792 H h1516 v_5 t1516
3793 S s1516 t620 h h1454 h1465 h1475 h1492 h1510 h1516
3794 G s1516 t1344
3795 B b1517 s1516
3796 T t1517 o938 b1517 b1452
3797 B b1518 t1517
3798 T t1518 o2 b1514
3799 B b1519 t1518
3800 T t1519 o937 b1518 b4 b1519
3801 B b1520 t1519
3802 T t400 o b1520 b4
3803 B b400 t400
3804 T t406 o936 b1514 b400
3805 B b406 t406
3806 B b1521 t1509 v_5
3807 T t1521 o711 b1521
3808 S s1521 t620 h h1454 h1465 h1475 h1492 h1510
3809 G s1521 t1521
3810 B b1522 s1521
3811 T t1522 o938 b1522 b1452
3812 B b1523 t1522
3813 T t1523 o738 b1032 b1510
3814 B b1524 t1523 v_5
3815 T t1524 o976 b1524
3816 S s1524 t620 h h1454 h1465 h1475 h1492 h1510
3817 G s1524 t1524
3818 B b1525 s1524
3819 T t1525 o938 b1525 b1452
3820 B b1526 t1525
3821 T t1526 o973 b1526 b983 b1519
3822 B b1527 t1526
3823 T t1527 o2 b1527
3824 B b1528 t1527
3825 T t1528 o973 b1523 b4 b1528
3826 B b1529 t1528
3827 P p1532 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3828 O o1532 ext_rule p1532
3829 T t1532 o936 b1520 b4
3830 B b1533 t1532
3831 T t1533 o1532 b935 b1533 b4 b4
3832 B b1534 t1533
3833 T t407 o b1534 b4
3834 B b407 t407
3835 T t1534 o936 b1529 b4
3836 B b1535 t1534
3837 T t1535 o1050 b935 b1535 b4 b4
3838 B b1536 t1535
3839 T t1536 o b1536 b4
3840 B b1537 t1536
3841 T t416 o1516 b935 b406 b407 b1537
3842 B b416 t416
3843 T t417 o b416 b4
3844 B b417 t417
3845 T t425 o1508 b935 b1516 b417 b4
3846 B b425 t425
3847 T t426 o b425 b4
3848 B b426 t426
3849 T t1541 o936 b1505 b4
3850 B b1542 t1541
3851 T t1542 o1050 b935 b1542 b4 b4
3852 B b1543 t1542
3853 T t1543 o b1543 b4
3854 B b1544 t1543
3855 T t434 o1491 b935 b399 b426 b1544
3856 B b434 t434
3857 T t435 o b434 b4
3858 B b435 t435
3859 T t1546 o936 b1488 b4
3860 B b1547 t1546
3861 T t1547 o1050 b935 b1547 b4 b4
3862 B b1548 t1547
3863 T t1548 o b1548 b4
3864 B b1549 t1548
3865 T t443 o1473 b935 b392 b435 b1549
3866 B b443 t443
3867 T t444 o b443 b4
3868 B b444 t444
3869 T t452 o b1473 b444
3870 B b452 t452
3871 S s1553 t620 h
3872 G s1553 t1457
3873 B b1554 s1553
3874 T t1554 o938 b1554 b1452
3875 B b1555 t1554
3876 T t1555 o947 b1555 b4 b1462
3877 B b1556 t1555
3878 T t1556 o1085 b1556
3879 B b1557 t1556
3880 T t1557 o b1557 b4
3881 B b1558 t1557
3882 T t1558 o963 b935 b1557 b1558 b4
3883 B b1559 t1558
3884 H h1559 v t1457
3885 S s1559 t620 h h1559
3886 G s1559 t1344
3887 B b1560 s1559
3888 T t1560 o938 b1560 b1452
3889 B b1561 t1560
3890 T t1561 o937 b1561 b4 b1462
3891 B b1562 t1561
3892 T t1562 o1085 b1562
3893 B b1563 t1562
3894 T t1563 o b1563 b4
3895 B b1564 t1563
3896 T t1564 o1532 b935 b1563 b1564 b4
3897 B b1565 t1564
3898 T t1565 o b1565 b4
3899 B b1566 t1565
3900 H h1566 x t1435
3901 H h1567 v_1 t1475
3902 H h1568 v_2 t1492
3903 H h1569 v_3 t1510
3904 B b1569 t1509 v_4
3905 T t1569 o711 b1569
3906 S s1569 t620 h h1566 h1559 h1567 h1568 h1569
3907 G s1569 t1569
3908 B b1570 s1569
3909 T t1570 o938 b1570 b1107
3910 B b1571 t1570
3911 T t1571 o738 b1147 b1510
3912 B b1572 t1571 v_4
3913 T t1572 o976 b1572
3914 S s1572 t620 h h1566 h1559 h1567 h1568 h1569
3915 G s1572 t1572
3916 B b1573 s1572
3917 T t1573 o938 b1573 b1107
3918 B b1574 t1573
3919 S s1574 t620 h h1566 h1559 h1567 h1568 h1569
3920 G s1574 t1344
3921 B b1575 s1574
3922 T t1575 o938 b1575 b1107
3923 B b1576 t1575
3924 S s1576 t620 h h1566 h1559 h1567 h1568
3925 G s1576 t1344
3926 B b1577 s1576
3927 T t1577 o938 b1577 b1107
3928 B b1578 t1577
3929 S s1578 t620 h h1566 h1559 h1567
3930 G s1578 t1344
3931 B b1579 s1578
3932 T t1579 o938 b1579 b1107
3933 B b1580 t1579
3934 S s1580 t620 h h1566 h1559
3935 G s1580 t1344
3936 B b1581 s1580
3937 T t1581 o938 b1581 b1107
3938 B b1582 t1581
3939 S s1582 t620 h h1566
3940 G s1582 t1344
3941 B b1583 s1582
3942 T t1583 o938 b1583 b1107
3943 B b1584 t1583
3944 T t1584 o937 b1584 b4 b946
3945 B b1585 t1584
3946 T t1585 o2 b1585
3947 B b1586 t1585
3948 T t1586 o937 b1582 b4 b1586
3949 B b1587 t1586
3950 T t1587 o2 b1587
3951 B b1588 t1587
3952 T t1588 o937 b1580 b4 b1588
3953 B b1589 t1588
3954 T t1589 o2 b1589
3955 B b1590 t1589
3956 T t1590 o937 b1578 b4 b1590
3957 B b1591 t1590
3958 T t1591 o2 b1591
3959 B b1592 t1591
3960 T t1592 o937 b1576 b4 b1592
3961 B b1593 t1592
3962 T t1593 o2 b1593
3963 B b1594 t1593
3964 T t1594 o973 b1574 b983 b1594
3965 B b1595 t1594
3966 T t1595 o2 b1595
3967 B b1596 t1595
3968 T t1596 o973 b1571 b4 b1596
3969 B b1597 t1596
3970 T t1597 o936 b1597 b4
3971 B b1598 t1597
3972 T t1598 o1050 b935 b1598 b4 b4
3973 B b1599 t1598
3974 T t1599 o b1599 b4
3975 B b1600 t1599
3976 T t1600 o1516 b935 b1563 b1566 b1600
3977 B b1601 t1600
3978 T t1601 o b1601 b4
3979 B b1602 t1601
3980 T t1602 o1508 b935 b1563 b1602 b4
3981 B b1603 t1602
3982 T t1603 o b1603 b4
3983 B b1604 t1603
3984 P p1604 String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
3985 O o1604 ext_rule p1604
3986 B b1605 t1474 v_2
3987 T t1605 o711 b1605
3988 S s1605 t620 h h1566 h1559 h1567
3989 G s1605 t1605
3990 B b1606 s1605
3991 T t1606 o938 b1606 b1107
3992 B b1607 t1606
3993 T t1607 o738 b1475 b977
3994 B b1608 t1607 v_2
3995 T t1608 o976 b1608
3996 S s1608 t620 h h1566 h1559 h1567
3997 G s1608 t1608
3998 B b1609 s1608
3999 T t1609 o938 b1609 b1107
4000 B b1610 t1609
4001 T t1610 o973 b1610 b983 b1590
4002 B b1611 t1610
4003 T t1611 o2 b1611
4004 B b1612 t1611
4005 T t1612 o973 b1607 b4 b1612
4006 B b1613 t1612
4007 T t1613 o936 b1613 b4
4008 B b1614 t1613
4009 T t1614 o1604 b935 b1614 b4 b4
4010 B b1615 t1614
4011 T t1615 o b1615 b4
4012 B b1616 t1615
4013 T t1616 o1491 b935 b1563 b1604 b1616
4014 B b1617 t1616
4015 T t1617 o b1617 b4
4016 B b1618 t1617
4017 B b1619 t1456 v_1
4018 T t1619 o711 b1619
4019 S s1619 t620 h h1566 h1559
4020 G s1619 t1619
4021 B b1620 s1619
4022 T t1620 o938 b1620 b1107
4023 B b1621 t1620
4024 T t1621 o738 b1220 b1457
4025 B b1622 t1621 v_1
4026 T t1622 o976 b1622
4027 S s1622 t620 h h1566 h1559
4028 G s1622 t1622
4029 B b1623 s1622
4030 T t1623 o938 b1623 b1107
4031 B b1624 t1623
4032 T t1624 o973 b1624 b983 b1588
4033 B b1625 t1624
4034 T t1625 o2 b1625
4035 B b1626 t1625
4036 T t1626 o973 b1621 b4 b1626
4037 B b1627 t1626
4038 T t1627 o936 b1627 b4
4039 B b1628 t1627
4040 T t1628 o1604 b935 b1628 b4 b4
4041 B b1629 t1628
4042 T t1629 o b1629 b4
4043 B b1630 t1629
4044 T t1630 o1473 b935 b1563 b1618 b1630
4045 B b1631 t1630
4046 T t1631 o b1631 b4
4047 B b1632 t1631
4048 T t1632 o b1559 b1632
4049 B b1633 t1632
4050 T t453 o1445 b935 b1471 b452 b1633
4051 B b453 t453
4052 T t461 o933 b453
4053 B b461 t461
4054 P p1635 Number 5861
4055 P p1636 Number 5869
4056 O o1636 resource_defs p1635 p1636 p264
4057 P p1637 Number 5867
4058 O o1637 uid p1637 p1636
4059 T t1637 o1637 b626
4060 B b1637 t1637
4061 T t1638 o b1637 b4
4062 B b1638 t1638
4063 T t1639 o1636 b1638
4064 B b1639 t1639
4065 T t1640 o b1639 b4
4066 B b1640 t1640
4067 T t462 o1432 b1434 b1445 b461 b1640
4068 B b462 t462
4069 T t470 o1431 b462
4070 B b470 t470
4071 P p1642 Number 6266
4072 P p1643 Number 6335
4073 O o1643 location p1642 p1643
4074 O o1644 str_let p1642 p1643
4075 P p1644 Number 6270
4076 O o1645 patt_var p1644 p1643
4077 O o1646 patt_done p1642 p1643
4078 T t1646 o1646
4079 B b1646 t1646 groupCancelLeftT
4080 T t1647 o1645 b1646
4081 B b1647 t1647
4082 O o1647 fun p1644 p1643
4083 O o1648 patt_if p1644 p1643
4084 P p1648 Number 6287
4085 P p1649 Number 6288
4086 O o1649 patt_var p1648 p1649
4087 O o1650 patt_body p1644 p1643
4088 P p1650 Number 6289
4089 P p1651 Number 6290
4090 O o1651 patt_var p1650 p1651
4091 P p1652 Number 6296
4092 O o1652 apply p1652 p1643
4093 P p1653 Number 6333
4094 O o1653 apply p1652 p1653
4095 P p1654 Number 6331
4096 O o1654 apply p1652 p1654
4097 P p1655 Number 6303
4098 O o1655 lid p1652 p1655
4099 O o1656 lid p919
4100 T t1656 o1656
4101 B b1656 t1656
4102 T t1657 o1655 b1656
4103 B b1657 t1657
4104 P p1657 Number 6305
4105 P p1658 Number 6330
4106 O o1658 apply p1657 p1658
4107 P p1659 Number 6328
4108 O o1659 proj p1657 p1659
4109 O o1660 uid p1657 p1659
4110 T t1660 o1660 b836
4111 B b1660 t1660
4112 P p1660 Number 6314
4113 O o1661 lid p1660 p1659
4114 T t1661 o1661 b838
4115 B b1661 t1661
4116 T t1662 o1659 b1660 b1661
4117 B b1662 t1662
4118 P p1662 Number 6329
4119 O o1662 lid p1662 p1658
4120 T t1663 o1662 b841
4121 B b1663 t1663
4122 T t1664 o1658 b1662 b1663
4123 B b1664 t1664
4124 T t1665 o1654 b1657 b1664
4125 B b1665 t1665
4126 P p1665 Number 6332
4127 O o1665 lid p1665 p1653
4128 P p1666 Var t
4129 O o1666 var p1666
4130 T t1666 o1666
4131 B b1666 t1666
4132 T t1667 o1665 b1666
4133 B b1667 t1667
4134 T t1668 o1653 b1665 b1667
4135 B b1668 t1668
4136 P p1668 Number 6334
4137 O o1668 lid p1668 p1643
4138 T t1669 o1668 b841
4139 B b1669 t1669
4140 T t1670 o1652 b1668 b1669
4141 B b1670 t1670
4142 T t1671 o1650 b1670
4143 B b1671 t1671 p
4144 T t1672 o1651 b1671
4145 B b1672 t1672
4146 T t1673 o1648 b1672
4147 B b1673 t1673
4148 T t1674 o1647 b1673
4149 B b1674 t1674
4150 T t1675 o1650 b1674
4151 B b1675 t1675 t
4152 T t1676 o1649 b1675
4153 B b1676 t1676
4154 T t1677 o1648 b1676
4155 B b1677 t1677
4156 T t1678 o1647 b1677
4157 B b1678 t1678
4158 T t1679 o1644 b1647 b1678
4159 B b1679 t1679
4160 T t1680 o b1679 b4
4161 B b1680 t1680
4162 T t1681 o1644 b1680
4163 B b1681 t1681
4164 T t1682 o392 b1681
4165 B b1682 t1682
4166 T t1683 o1643 b1682
4167 B b1683 t1683
4168 P p1683 Number 6337
4169 P p1684 Number 6407
4170 O o1684 location p1683 p1684
4171 O o1685 str_let p1683 p1684
4172 P p1685 Number 6341
4173 O o1686 patt_var p1685 p1684
4174 O o1687 patt_done p1683 p1684
4175 T t1687 o1687
4176 B b1687 t1687 groupCancelRightT
4177 T t1688 o1686 b1687
4178 B b1688 t1688
4179 O o1688 fun p1685 p1684
4180 O o1689 patt_if p1685 p1684
4181 P p1689 Number 6359
4182 P p1690 Number 6360
4183 O o1690 patt_var p1689 p1690
4184 O o1691 patt_body p1685 p1684
4185 P p1691 Number 6361
4186 P p1692 Number 6362
4187 O o1692 patt_var p1691 p1692
4188 P p1693 Number 6368
4189 O o1693 apply p1693 p1684
4190 P p1694 Number 6405
4191 O o1694 apply p1693 p1694
4192 P p1695 Number 6403
4193 O o1695 apply p1693 p1695
4194 P p1696 Number 6375
4195 O o1696 lid p1693 p1696
4196 O o1697 lid p1432
4197 T t1697 o1697
4198 B b1697 t1697
4199 T t1698 o1696 b1697
4200 B b1698 t1698
4201 P p1698 Number 6377
4202 P p1699 Number 6402
4203 O o1699 apply p1698 p1699
4204 P p1700 Number 6400
4205 O o1700 proj p1698 p1700
4206 O o1701 uid p1698 p1700
4207 T t1701 o1701 b836
4208 B b1701 t1701
4209 P p1701 Number 6386
4210 O o1702 lid p1701 p1700
4211 T t1702 o1702 b838
4212 B b1702 t1702
4213 T t1703 o1700 b1701 b1702
4214 B b1703 t1703
4215 P p1703 Number 6401
4216 O o1703 lid p1703 p1699
4217 T t1704 o1703 b841
4218 B b1704 t1704
4219 T t1705 o1699 b1703 b1704
4220 B b1705 t1705
4221 T t1706 o1695 b1698 b1705
4222 B b1706 t1706
4223 P p1706 Number 6404
4224 O o1706 lid p1706 p1694
4225 T t1707 o1706 b1666
4226 B b1707 t1707
4227 T t1708 o1694 b1706 b1707
4228 B b1708 t1708
4229 P p1708 Number 6406
4230 O o1708 lid p1708 p1684
4231 T t1709 o1708 b841
4232 B b1709 t1709
4233 T t1710 o1693 b1708 b1709
4234 B b1710 t1710
4235 T t1711 o1691 b1710
4236 B b1711 t1711 p
4237 T t1712 o1692 b1711
4238 B b1712 t1712
4239 T t1713 o1689 b1712
4240 B b1713 t1713
4241 T t1714 o1688 b1713
4242 B b1714 t1714
4243 T t1715 o1691 b1714
4244 B b1715 t1715 t
4245 T t1716 o1690 b1715
4246 B b1716 t1716
4247 T t1717 o1689 b1716
4248 B b1717 t1717
4249 T t1718 o1688 b1717
4250 B b1718 t1718
4251 T t1719 o1685 b1688 b1718
4252 B b1719 t1719
4253 T t1720 o b1719 b4
4254 B b1720 t1720
4255 T t1721 o1685 b1720
4256 B b1721 t1721
4257 T t1722 o392 b1721
4258 B b1722 t1722
4259 T t1723 o1684 b1722
4260 B b1723 t1723
4261 P p1723 Number 6425
4262 P p1724 Number 6666
4263 O o1724 location p1723 p1724
4264 P p1725 String unique_id1
4265 O o1725 rule p1725
4266 P p1726 Var e2
4267 O o1726 var p1726
4268 T t1726 o1726
4269 B b1726 t1726
4270 T t1727 o620 b1726
4271 S s1727 t637 h
4272 G s1727 t1727
4273 B b1727 s1727
4274 T t1728 o618 b1727
4275 B b1728 t1728
4276 T t1729 o655 b1726 b554
4277 S s1729 t620 h
4278 G s1729 t1729
4279 B b1729 s1729
4280 T t1730 o618 b1729
4281 B b1730 t1730
4282 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4283 NCzf_itt_dall!dall dall dall Czf_itt_dall
4284 O o1730 dall
4285 T t1731 o559 b1726 b573
4286 B b1731 t1731
4287 T t1732 o676 b1731 b573
4288 B b1732 t1732
4289 T t1733 o559 b573 b1726
4290 B b1733 t1733
4291 T t1734 o676 b1733 b573
4292 B b1734 t1734
4293 T t1735 o1270 b1732 b1734
4294 B b1735 t1735 s
4295 T t1736 o1730 b554 b1735
4296 H h1736 x t1736
4297 T t1737 o676 b1726 b567
4298 S s1737 t620 h h1736
4299 G s1737 t1737
4300 B b1737 s1737
4301 T t1738 o618 b1737
4302 B b1738 t1738
4303 T t1739 o635 b1730 b1738
4304 B b1739 t1739
4305 T t1740 o635 b1728 b1739
4306 B b1740 t1740
4307 P p1740 String "withT << id >> (dT 2) thenT autoT"
4308 O o1740 ext_rule p1740
4309 T t1741 o b1729 b4
4310 B b1741 t1741
4311 T t1742 o b1727 b1741
4312 B b1742 t1742
4313 T t1743 o938 b1737 b1742
4314 B b1743 t1743
4315 T t1744 o937 b1743 b4 b946
4316 B b1744 t1744
4317 T t1745 o559 b1726 b567
4318 B b1745 t1745
4319 T t1746 o676 b1745 b567
4320 H h1746 y t1746
4321 T t1747 o559 b567 b1726
4322 B b1747 t1747
4323 T t1748 o676 b1747 b567
4324 H h1748 z t1748
4325 S s1748 t620 h h1736 h1746 h1748
4326 G s1748 t1737
4327 B b1748 s1748
4328 T t1749 o938 b1748 b1742
4329 B b1749 t1749
4330 B b1750 t1746
4331 B b1751 t1748
4332 T t1751 o1270 b1750 b1751
4333 H h1751 w t1751
4334 S s1751 t620 h h1736 h1751
4335 G s1751 t1737
4336 B b1752 s1751
4337 T t1752 o938 b1752 b1742
4338 B b1753 t1752
4339 P p1753 String with
4340 O o1753 arg_named p1753
4341 NSummary!arg_term_list arg_term_list arg_term_list Summary
4342 O o1754 arg_term_list
4343 T t1754 o b567 b4
4344 B b1754 t1754
4345 T t1755 o1754 b1754
4346 B b1755 t1755
4347 T t1756 o1753 b1755
4348 B b1756 t1756
4349 T t1757 o b1756 b4
4350 B b1757 t1757
4351 T t1758 o937 b1743 b1757 b946
4352 B b1758 t1758
4353 T t1759 o2 b1758
4354 B b1759 t1759
4355 T t1760 o937 b1753 b4 b1759
4356 B b1760 t1760
4357 T t1761 o2 b1760
4358 B b1761 t1761
4359 T t1762 o937 b1749 b4 b1761
4360 B b1762 t1762
4361 T t1763 o b1762 b4
4362 B b1763 t1763
4363 T t1764 o936 b1744 b1763
4364 B b1764 t1764
4365 P p1764 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
4366 O o1764 ext_rule p1764
4367 T t1765 o936 b1762 b4
4368 B b1765 t1765
4369 T t1766 o1764 b935 b1765 b4 b4
4370 B b1766 t1766
4371 T t1767 o b1766 b4
4372 B b1767 t1767
4373 S s1767 t620 h
4374 G s1767 t1727
4375 B b1768 s1767
4376 T t1768 o b1768 b1741
4377 B b1769 t1768
4378 T t1769 o938 b1748 b1769
4379 B b1770 t1769
4380 T t1770 o938 b1752 b1769
4381 B b1771 t1770
4382 T t1771 o938 b1737 b1769
4383 B b1772 t1771
4384 T t1772 o937 b1772 b1757 b946
4385 B b1773 t1772
4386 T t1773 o2 b1773
4387 B b1774 t1773
4388 T t1774 o937 b1771 b4 b1774
4389 B b1775 t1774
4390 T t1775 o2 b1775
4391 B b1776 t1775
4392 T t1776 o937 b1770 b4 b1776
4393 B b1777 t1776
4394 T t1777 o936 b1777 b4
4395 B b1778 t1777
4396 T t1778 o1764 b935 b1778 b4 b4
4397 B b1779 t1778
4398 P p1779 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
4399 O o1779 ext_rule p1779
4400 H h1779 v t1737
4401 S s1779 t620 h h1736 h1746 h1748 h1779
4402 G s1779 t1737
4403 B b1780 s1779
4404 T t1780 o938 b1780 b1769
4405 B b1781 t1780
4406 T t1781 o2 b1777
4407 B b1782 t1781
4408 T t1782 o937 b1781 b4 b1782
4409 B b1783 t1782
4410 T t1783 o b1783 b4
4411 B b1784 t1783
4412 T t1784 o936 b1777 b1784
4413 B b1785 t1784
4414 T t1785 o1085 b1783
4415 B b1786 t1785
4416 T t1786 o b1786 b4
4417 B b1787 t1786
4418 T t1787 o1779 b935 b1785 b1787 b4
4419 B b1788 t1787
4420 P p1788 String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
4421 O o1788 ext_rule p1788
4422 P p1789 Var e
4423 O o1789 var p1789
4424 T t1789 o1789
4425 B b1789 t1789
4426 T t1790 o620 b1789
4427 S s1790 t637 h h1736 h1746 h1748
4428 G s1790 t1790
4429 B b1790 s1790
4430 T t1791 o938 b1790 b1769
4431 B b1791 t1791
4432 T t1792 o559 b1726 b1789
4433 B b1792 t1792
4434 T t1793 o620 b1792
4435 S s1793 t637 h h1736 h1746 h1748
4436 G s1793 t1793
4437 B b1793 s1793
4438 T t1794 o938 b1793 b1769
4439 B b1794 t1794
4440 T t1795 o738 b1792 b1726
4441 S s1795 t620 h h1736 h1746 h1748
4442 G s1795 t1795
4443 B b1795 s1795
4444 T t1796 o938 b1795 b1769
4445 B b1796 t1796
4446 T t1797 o966 b1796 b983 b1782
4447 B b1797 t1797
4448 T t1798 o2 b1797
4449 B b1798 t1798
4450 T t1799 o973 b1794 b983 b1798
4451 B b1799 t1799
4452 T t1800 o2 b1799
4453 B b1800 t1800
4454 T t1801 o973 b1791 b4 b1800
4455 B b1801 t1801
4456 T t1802 o676 b1792 b1726
4457 S s1802 t620 h h1736 h1746 h1748
4458 G s1802 t1802
4459 B b1802 s1802
4460 T t1803 o938 b1802 b1769
4461 B b1803 t1803
4462 T t1804 o966 b1803 b4 b1798
4463 B b1804 t1804
4464 H h1804 v t1746
4465 S s1804 t620 h h1736 h1746 h1748 h1804
4466 G s1804 t1737
4467 B b1805 s1804
4468 T t1805 o938 b1805 b1769
4469 B b1806 t1805
4470 T t1806 o937 b1806 b4 b1782
4471 B b1807 t1806
4472 T t471 o b1807 b4
4473 B b471 t471
4474 T t479 o b1804 b471
4475 B b479 t479
4476 T t480 o b1801 b479
4477 B b480 t480
4478 T t486 o936 b1777 b480
4479 B b486 t486
4480 T t1821 o1085 b1801
4481 B b1822 t1821
4482 T t1822 o1085 b1804
4483 B b1823 t1822
4484 T t1823 o1085 b1807
4485 B b1824 t1823
4486 T t487 o b1824 b4
4487 B b487 t487
4488 T t493 o b1823 b487
4489 B b493 t493
4490 T t494 o b1822 b493
4491 B b494 t494
4492 T t500 o1788 b935 b486 b494 b4
4493 B b500 t500
4494 T t501 o b500 b4
4495 B b501 t501
4496 T t508 o b500 b501
4497 B b508 t508
4498 T t509 o b1788 b508
4499 B b509 t509
4500 T t516 o b1779 b509
4501 B b516 t516
4502 T t517 o1740 b935 b1764 b1767 b516
4503 B b517 t517
4504 T t524 o933 b517
4505 B b524 t524
4506 P p1836 Number 6451
4507 P p1837 Number 6459
4508 O o1837 resource_defs p1836 p1837 p264
4509 P p1838 Number 6457
4510 O o1838 uid p1838 p1837
4511 T t1838 o1838 b626
4512 B b1838 t1838
4513 T t1839 o b1838 b4
4514 B b1839 t1839
4515 T t1840 o1837 b1839
4516 B b1840 t1840
4517 T t1841 o b1840 b4
4518 B b1841 t1841
4519 T t525 o1725 b618 b1740 b524 b1841
4520 B b525 t525
4521 T t531 o1724 b525
4522 B b531 t531
4523 P p1843 Number 6981
4524 P p1844 Number 7305
4525 O o1844 location p1843 p1844
4526 P p1845 String unique_inv
4527 O o1845 rule p1845
4528 T t1845 o559 b561 b573
4529 B b1845 t1845
4530 T t1846 o738 b1845 b567
4531 H h1846 x t1846
4532 T t1847 o559 b573 b561
4533 B b1847 t1847
4534 T t1848 o738 b1847 b567
4535 H h1848 y t1848
4536 T t1849 o738 b561 b574
4537 S s1849 t620 h h1846 h1848
4538 G s1849 t1849
4539 B b1849 s1849
4540 T t1850 o618 b1849
4541 B b1850 t1850
4542 T t1851 o635 b658 b1850
4543 B b1851 t1851
4544 T t1852 o635 b794 b1851
4545 B b1852 t1852
4546 T t1853 o635 b641 b1852
4547 B b1853 t1853
4548 T t1854 o635 b711 b1853
4549 B b1854 t1854
4550 P p1854 String "assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
4551 O o1854 ext_rule p1854
4552 T t1855 o b657 b4
4553 B b1855 t1855
4554 T t1856 o b793 b1855
4555 B b1856 t1856
4556 T t1857 o b640 b1856
4557 B b1857 t1857
4558 T t1858 o b710 b1857
4559 B b1858 t1858
4560 T t1859 o938 b1849 b1858
4561 B b1859 t1859
4562 T t1860 o937 b1859 b4 b946
4563 B b1860 t1860
4564 T t1861 o559 b574 b573
4565 B b1861 t1861
4566 T t1862 o738 b1861 b567
4567 H h1862 v t1862
4568 S s1862 t620 h h1846 h1848 h1862
4569 G s1862 t1849
4570 B b1862 s1862
4571 T t1863 o938 b1862 b1858
4572 B b1863 t1863
4573 T t1864 o2 b1860
4574 B b1864 t1864
4575 T t1865 o937 b1863 b4 b1864
4576 B b1865 t1865
4577 T t1866 o b1865 b4
4578 B b1866 t1866
4579 T t1867 o936 b1860 b1866
4580 B b1867 t1867
4581 P p1867 String "setSubstT << equal{id; op{inv{'s}; 's}} >> 2 thenAT autoT"
4582 O o1867 ext_rule p1867
4583 T t1868 o676 b567 b1861
4584 S s1868 t620 h h1846 h1848 h1862
4585 G s1868 t1868
4586 B b1868 s1868
4587 T t1869 o938 b1868 b1858
4588 B b1869 t1869
4589 T t1870 o738 b567 b1861
4590 S s1870 t620 h h1846 h1848 h1862
4591 G s1870 t1870
4592 B b1870 s1870
4593 T t1871 o938 b1870 b1858
4594 B b1871 t1871
4595 T t1872 o2 b1865
4596 B b1872 t1872
4597 T t1873 o966 b1871 b983 b1872
4598 B b1873 t1873
4599 T t1874 o2 b1873
4600 B b1874 t1874
4601 T t1875 o966 b1869 b4 b1874
4602 B b1875 t1875
4603 T t1876 o738 b1845 b1861
4604 H h1876 v_1 t1876
4605 S s1876 t620 h h1846 h1848 h1862 h1876
4606 G s1876 t1849
4607 B b1876 s1876
4608 T t1877 o938 b1876 b1858
4609 B b1877 t1877
4610 T t1878 o937 b1877 b4 b1872
4611 B b1878 t1878
4612 T t532 o b1878 b4
4613 B b532 t532
4614 T t538 o b1875 b532
4615 B b538 t538
4616 T t539 o936 b1865 b538
4617 B b539 t539
4618 B b1879 t1845 v_1
4619 T t1879 o711 b1879
4620 S s1879 t620 h h1846 h1848 h1862
4621 G s1879 t1879
4622 B b1880 s1879
4623 T t1880 o938 b1880 b1858
4624 B b1881 t1880
4625 T t1881 o738 b1845 b1220
4626 B b1882 t1881 v_1
4627 T t1882 o976 b1882
4628 S s1882 t620 h h1846 h1848 h1862
4629 G s1882 t1882
4630 B b1883 s1882
4631 T t1883 o938 b1883 b1858
4632 B b1884 t1883
4633 T t1884 o973 b1884 b983 b1872
4634 B b1885 t1884
4635 T t1885 o2 b1885
4636 B b1886 t1885
4637 T t1886 o973 b1881 b4 b1886
4638 B b1887 t1886
4639 P p1891 String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
4640 O o1891 ext_rule p1891
4641 T t1891 o936 b1875 b4
4642 B b1892 t1891
4643 T t1892 o1891 b935 b1892 b4 b4
4644 B b1893 t1892
4645 P p1893 String "groupCancelRightT << 's >> thenT autoT"
4646 O o1893 ext_rule p1893
4647 T t1893 o936 b1878 b4
4648 B b1894 t1893
4649 T t1894 o1893 b935 b1894 b4 b4
4650 B b1895 t1894
4651 T t545 o b1895 b4
4652 B b545 t545
4653 T t546 o b1893 b545
4654 B b546 t546
4655 T t1895 o936 b1887 b4
4656 B b1896 t1895
4657 T t1896 o1071 b935 b1896 b4 b4
4658 B b1897 t1896
4659 T t1897 o b1897 b4
4660 B b1898 t1897
4661 T t552 o1867 b935 b539 b546 b1898
4662 B b552 t552
4663 T t553 o b552 b4
4664 B b553 t553
4665 T t557 o1854 b935 b1867 b553 b4
4666 B b557 t557
4667 T t558 o933 b557
4668 B b558 t558
4669 P p1904 Number 7007
4670 P p1905 Number 7015
4671 O o1905 resource_defs p1904 p1905 p264
4672 P p1906 Number 7013
4673 O o1906 uid p1906 p1905
4674 T t1906 o1906 b626
4675 B b1906 t1906
4676 T t1907 o b1906 b4
4677 B b1907 t1907
4678 T t1908 o1905 b1907
4679 B b1908 t1908
4680 T t1909 o b1908 b4
4681 B b1909 t1909
4682 T t559 o1845 b618 b1854 b558 b1909
4683 B b559 t559
4684 T t565 o1844 b559
4685 B b565 t565
4686 P p1911 Number 7356
4687 P p1912 Number 7775
4688 O o1912 location p1911 p1912
4689 P p1913 String unique_sol1
4690 O o1913 rule p1913
4691 P p1914 Var a
4692 O o1914 var p1914
4693 T t1914 o1914
4694 B b1914 t1914
4695 T t1915 o620 b1914
4696 S s1915 t637 h
4697 G s1915 t1915
4698 B b1915 s1915
4699 T t1916 o618 b1915
4700 B b1916 t1916
4701 P p1916 Var b
4702 O o1916 var p1916
4703 T t1917 o1916
4704 B b1917 t1917
4705 T t1918 o620 b1917
4706 S s1918 t637 h
4707 G s1918 t1918
4708 B b1918 s1918
4709 T t1919 o618 b1918
4710 B b1919 t1919
4711 P p1919 Var x
4712 O o1919 var p1919
4713 T t1920 o1919
4714 B b1920 t1920
4715 T t1921 o620 b1920
4716 S s1921 t637 h
4717 G s1921 t1921
4718 B b1921 s1921
4719 T t1922 o618 b1921
4720 B b1922 t1922
4721 T t1923 o655 b1914 b554
4722 S s1923 t620 h
4723 G s1923 t1923
4724 B b1923 s1923
4725 T t1924 o618 b1923
4726 B b1924 t1924
4727 T t1925 o655 b1917 b554
4728 S s1925 t620 h
4729 G s1925 t1925
4730 B b1925 s1925
4731 T t1926 o618 b1925
4732 B b1926 t1926
4733 T t1927 o655 b1920 b554
4734 S s1927 t620 h
4735 G s1927 t1927
4736 B b1927 s1927
4737 T t1928 o618 b1927
4738 B b1928 t1928
4739 T t1929 o559 b1914 b1920
4740 B b1929 t1929
4741 T t1930 o738 b1929 b1917
4742 S s1930 t620 h
4743 G s1930 t1930
4744 B b1930 s1930
4745 T t1931 o618 b1930
4746 B b1931 t1931
4747 T t1932 o572 b1914
4748 B b1932 t1932
4749 T t1933 o559 b1932 b1917
4750 B b1933 t1933
4751 T t1934 o738 b1920 b1933
4752 S s1934 t620 h
4753 G s1934 t1934
4754 B b1934 s1934
4755 T t1935 o618 b1934
4756 B b1935 t1935
4757 T t1936 o635 b1931 b1935
4758 B b1936 t1936
4759 T t1937 o635 b1928 b1936
4760 B b1937 t1937
4761 T t1938 o635 b1926 b1937
4762 B b1938 t1938
4763 T t1939 o635 b1924 b1938
4764 B b1939 t1939
4765 T t1940 o635 b1922 b1939
4766 B b1940 t1940
4767 T t1941 o635 b1919 b1940
4768 B b1941 t1941
4769 T t1942 o635 b1916 b1941
4770 B b1942 t1942
4771 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"
4772 O o1942 ext_rule p1942
4773 T t1943 o b1930 b4
4774 B b1943 t1943
4775 T t1944 o b1927 b1943
4776 B b1944 t1944
4777 T t1945 o b1925 b1944
4778 B b1945 t1945
4779 T t1946 o b1923 b1945
4780 B b1946 t1946
4781 T t1947 o b1921 b1946
4782 B b1947 t1947
4783 T t1948 o b1918 b1947
4784 B b1948 t1948
4785 T t1949 o b1915 b1948
4786 B b1949 t1949
4787 T t1950 o938 b1934 b1949
4788 B b1950 t1950
4789 T t1951 o937 b1950 b4 b946
4790 B b1951 t1951
4791 T t1952 o620 b1929
4792 H h1952 y_1 t1952
4793 H h1953 z_1 t1918
4794 T t1953 o676 b1929 b1917
4795 H h1954 z t1953
4796 T t1954 o559 b1932 b1929
4797 B b1954 t1954
4798 T t1955 o738 b1954 b1933
4799 S s1955 t620 h h1952 h1953 h1954
4800 G s1955 t1955
4801 B b1955 s1955
4802 T t1956 o938 b1955 b1949
4803 B b1956 t1956
4804 T t1957 o676 b1920 b1933
4805 S s1957 t620 h h1952 h1953 h1954
4806 G s1957 t1957
4807 B b1957 s1957
4808 T t1958 o938 b1957 b1949
4809 B b1958 t1958
4810 S s1958 t620 h h1952 h1953 h1954
4811 G s1958 t1934
4812 B b1959 s1958
4813 T t1959 o938 b1959 b1949
4814 B b1960 t1959
4815 B b1961 t1952
4816 B b1962 t1918
4817 T t1962 o1270 b1961 b1962
4818 H h1962 y t1962
4819 S s1962 t620 h h1962 h1954
4820 G s1962 t1934
4821 B b1963 s1962
4822 T t1963 o938 b1963 b1949
4823 B b1964 t1963
4824 B b1965 t1962
4825 B b1966 t1953
4826 T t1966 o1270 b1965 b1966
4827 H h1966 v t1966
4828 S s1966 t620 h h1966
4829 G s1966 t1934
4830 B b1967 s1966
4831 T t1967 o938 b1967 b1949
4832 B b1968 t1967
4833 H h1968 v t1930
4834 S s1968 t620 h h1968
4835 G s1968 t1934
4836 B b1969 s1968
4837 T t1969 o938 b1969 b1949
4838 B b1970 t1969
4839 T t1970 o2 b1951
4840 B b1971 t1970
4841 T t1971 o937 b1970 b4 b1971
4842 B b1972 t1971
4843 T t1972 o2 b1972
4844 B b1973 t1972
4845 T t1973 o937 b1968 b4 b1973
4846 B b1974 t1973
4847 T t1974 o2 b1974
4848 B b1975 t1974
4849 T t1975 o937 b1964 b4 b1975
4850 B b1976 t1975
4851 T t1976 o2 b1976
4852 B b1977 t1976
4853 T t1977 o937 b1960 b983 b1977
4854 B b1978 t1977
4855 T t1978 o2 b1978
4856 B b1979 t1978
4857 T t1979 o937 b1958 b4 b1979
4858 B b1980 t1979
4859 T t1980 o2 b1980
4860 B b1981 t1980
4861 T t1981 o947 b1956 b4 b1981
4862 B b1982 t1981
4863 H h1982 v t1955
4864 S s1982 t620 h h1952 h1953 h1954 h1982
4865 G s1982 t1957
4866 B b1983 s1982
4867 T t1983 o938 b1983 b1949
4868 B b1984 t1983
4869 T t1984 o937 b1984 b4 b1981
4870 B b1985 t1984
4871 T t1985 o b1985 b4
4872 B b1986 t1985
4873 T t1986 o b1982 b1986
4874 B b1987 t1986
4875 T t1987 o936 b1951 b1987
4876 B b1988 t1987
4877 T t1988 o936 b1982 b4
4878 B b1989 t1988
4879 T t1989 o990 b935 b1989 b4 b4
4880 B b1990 t1989
4881 P p1990 String "setSubstT << equal{op{inv{'a}; op{'a; 'x}}; op{op{inv{'a}; 'a}; 'x}} >> 5 thenT autoT"
4882 O o1990 ext_rule p1990
4883 T t1990 o559 b1932 b1914
4884 B b1991 t1990
4885 T t1991 o559 b1991 b1920
4886 B b1992 t1991
4887 T t1992 o738 b1992 b1933
4888 H h1992 v_1 t1992
4889 S s1992 t620 h h1952 h1953 h1954 h1982 h1992
4890 G s1992 t1957
4891 B b1993 s1992
4892 T t1993 o938 b1993 b1949
4893 B b1994 t1993
4894 T t1994 o2 b1985
4895 B b1995 t1994
4896 T t1995 o937 b1994 b4 b1995
4897 B b1996 t1995
4898 T t566 o b1996 b4
4899 B b566 t566
4900 T t570 o936 b1985 b566
4901 B b570 t570
4902 B b1997 t1933 v_1
4903 T t1997 o711 b1997
4904 S s1997 t620 h h1952 h1953 h1954 h1982
4905 G s1997 t1997
4906 B b1998 s1997
4907 T t1998 o938 b1998 b1949
4908 B b1999 t1998
4909 T t1999 o738 b1220 b1933
4910 B b2000 t1999 v_1
4911 T t2000 o976 b2000
4912 S s2000 t620 h h1952 h1953 h1954 h1982
4913 G s2000 t2000
4914 B b2001 s2000
4915 T t2001 o938 b2001 b1949
4916 B b2002 t2001
4917 T t2002 o973 b2002 b983 b1995
4918 B b2003 t2002
4919 T t2003 o2 b2003
4920 B b2004 t2003
4921 T t2004 o973 b1999 b4 b2004
4922 B b2005 t2004
4923 P p2008 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"
4924 O o2008 ext_rule p2008
4925 T t2008 o559 b567 b1920
4926 B b2009 t2008
4927 T t2009 o738 b2009 b1933
4928 H h2009 v_2 t2009
4929 S s2009 t620 h h1952 h1953 h1954 h1982 h1992 h2009
4930 G s2009 t1957
4931 B b2010 s2009
4932 T t2010 o938 b2010 b1949
4933 B b2011 t2010
4934 T t2011 o2 b1996
4935 B b2012 t2011
4936 T t2012 o937 b2011 b4 b2012
4937 B b2013 t2012
4938 T t571 o b2013 b4
4939 B b571 t571
4940 T t572 o936 b1996 b571
4941 B b572 t572
4942 B b2014 t1933 v_2
4943 T t2014 o711 b2014
4944 S s2014 t620 h h1952 h1953 h1954 h1982 h1992
4945 G s2014 t2014
4946 B b2015 s2014
4947 T t2015 o938 b2015 b1949
4948 B b2016 t2015
4949 T t2016 o559 b977 b1920
4950 B b2017 t2016
4951 T t2017 o738 b2017 b1933
4952 B b2018 t2017 v_2
4953 T t2018 o976 b2018
4954 S s2018 t620 h h1952 h1953 h1954 h1982 h1992
4955 G s2018 t2018
4956 B b2019 s2018
4957 T t2019 o938 b2019 b1949
4958 B b2020 t2019
4959 T t2020 o973 b2020 b983 b2012
4960 B b2021 t2020
4961 T t2021 o2 b2021
4962 B b2022 t2021
4963 T t2022 o973 b2016 b4 b2022
4964 B b2023 t2022
4965 P p2026 String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"
4966 O o2026 ext_rule p2026
4967 H h2026 v_3 t1934
4968 S s2026 t620 h h1952 h1953 h1954 h1982 h1992 h2009 h2026
4969 G s2026 t1957
4970 B b2027 s2026
4971 T t2027 o938 b2027 b1949
4972 B b2028 t2027
4973 T t2028 o2 b2013
4974 B b2029 t2028
4975 T t2029 o937 b2028 b4 b2029
4976 B b2030 t2029
4977 T t577 o b2030 b4
4978 B b577 t577
4979 T t578 o936 b2013 b577
4980 B b578 t578
4981 B b2031 t1933 v_3
4982 T t2031 o711 b2031
4983 S s2031 t620 h h1952 h1953 h1954 h1982 h1992 h2009
4984 G s2031 t2031
4985 B b2032 s2031
4986 T t2032 o938 b2032 b1949
4987 B b2033 t2032
4988 T t2033 o738 b1004 b1933
4989 B b2034 t2033 v_3
4990 T t2034 o976 b2034
4991 S s2034 t620 h h1952 h1953 h1954 h1982 h1992 h2009
4992 G s2034 t2034
4993 B b2035 s2034
4994 T t2035 o938 b2035 b1949
4995 B b2036 t2035
4996 T t2036 o973 b2036 b983 b2029
4997 B b2037 t2036
4998 T t2037 o2 b2037
4999 B b2038 t2037
5000 T t2038 o973 b2033 b4 b2038
5001 B b2039 t2038
5002 P p2042 String "rwh unfold_equal 8 thenT autoT"
5003 O o2042 ext_rule p2042
5004 T t2042 o936 b2030 b4
5005 B b2043 t2042
5006 T t2043 o2042 b935 b2043 b4 b4
5007 B b2044 t2043
5008 T t586 o b2044 b4
5009 B b586 t586
5010 T t2044 o936 b2039 b4
5011 B b2045 t2044
5012 T t2045 o1071 b935 b2045 b4 b4
5013 B b2046 t2045
5014 T t2046 o b2046 b4
5015 B b2047 t2046
5016 T t587 o2026 b935 b578 b586 b2047
5017 B b587 t587
5018 T t593 o b587 b4
5019 B b593 t593
5020 T t2049 o936 b2023 b4
5021 B b2050 t2049
5022 T t2050 o1071 b935 b2050 b4 b4
5023 B b2051 t2050
5024 T t2051 o b2051 b4
5025 B b2052 t2051
5026 T t594 o2008 b935 b572 b593 b2052
5027 B b594 t594
5028 T t607 o b594 b4
5029 B b607 t607
5030 T t2054 o936 b2005 b4
5031 B b2055 t2054
5032 T t2055 o1071 b935 b2055 b4 b4
5033 B b2056 t2055
5034 T t2058 o738 b1954 b1992
5035 S s2058 t620 h h1952 h1953 h1954 h1982
5036 G s2058 t2058
5037 B b2059 s2058
5038 T t2059 o938 b2059 b1949
5039 B b2060 t2059
5040 T t2060 o966 b2060 b4 b1995
5041 B b2061 t2060
5042 T t2061 o936 b2061 b4
5043 B b2062 t2061
5044 T t2062 o990 b935 b2062 b4 b4
5045 B b2063 t2062
5046 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"
5047 O o2063 ext_rule p2063
5048 T t2063 o973 b2002 b4 b1995
5049 B b2064 t2063
5050 T t615 o936 b2064 b4
5051 B b615 t615
5052 H h2064 x_1 t1344
5053 H h2065 y_2 t638
5054 T t2065 o620 b1933
5055 H h2066 z_3 t2065
5056 T t2066 o676 b560 b1933
5057 H h2067 z_2 t2066
5058 S s2067 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5059 G s2067 t1997
5060 B b2067 s2067
5061 T t2067 o938 b2067 b1949
5062 B b2068 t2067
5063 T t2068 o676 b1220 b1933
5064 B b2069 t2068 v_1
5065 T t2069 o976 b2069
5066 S s2069 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5067 G s2069 t2069
5068 B b2070 s2069
5069 T t2070 o938 b2070 b1949
5070 B b2071 t2070
5071 T t2071 o676 b561 b1933
5072 S s2071 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5073 G s2071 t2071
5074 B b2072 s2071
5075 T t2072 o938 b2072 b1949
5076 B b2073 t2072
5077 B b2074 t638
5078 B b2075 t2065
5079 T t2075 o1270 b2074 b2075
5080 H h2075 y t2075
5081 S s2075 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2075 h2067
5082 G s2075 t2071
5083 B b2076 s2075
5084 T t2076 o938 b2076 b1949
5085 B b2077 t2076
5086 B b2078 t2075
5087 B b2079 t2066
5088 T t2079 o1270 b2078 b2079
5089 H h2079 x_2 t2079
5090 S s2079 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2079
5091 G s2079 t2071
5092 B b2080 s2079
5093 T t2080 o938 b2080 b1949
5094 B b2081 t2080
5095 T t2081 o738 b560 b1933
5096 H h2081 x_2 t2081
5097 S s2081 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5098 G s2081 t2071
5099 B b2082 s2081
5100 T t2082 o938 b2082 b1949
5101 B b2083 t2082
5102 T t2083 o738 b561 b1933
5103 S s2083 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5104 G s2083 t2083
5105 B b2084 s2083
5106 T t2084 o938 b2084 b1949
5107 B b2085 t2084
5108 B b2086 t2081
5109 B b2087 t2083
5110 T t2087 o1177 b2086 b2087
5111 S s2087 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064
5112 G s2087 t2087
5113 B b2088 s2087
5114 T t2088 o938 b2088 b1949
5115 B b2089 t2088
5116 B b2090 t2087
5117 T t2090 o1177 b1347 b2090
5118 S s2090 t620 h h1952 h1953 h1954 h1982 h1344 h1224
5119 G s2090 t2090
5120 B b2091 s2090
5121 T t2091 o938 b2091 b1949
5122 B b2092 t2091
5123 B b2093 t2090 s2
5124 T t2093 o1185 b1186 b2093
5125 S s2093 t620 h h1952 h1953 h1954 h1982 h1344
5126 G s2093 t2093
5127 B b2094 s2093
5128 T t2094 o938 b2094 b1949
5129 B b2095 t2094
5130 B b2096 t2093 s1
5131 T t2096 o1185 b1186 b2096
5132 S s2096 t620 h h1952 h1953 h1954 h1982
5133 G s2096 t2096
5134 B b2097 s2096
5135 T t2097 o938 b2097 b1949
5136 B b2098 t2097
5137 T t2098 o2 b2064
5138 B b2099 t2098
5139 T t2099 o973 b2098 b983 b2099
5140 B b2100 t2099
5141 T t2100 o2 b2100
5142 B b2101 t2100
5143 T t2101 o937 b2095 b983 b2101
5144 B b2102 t2101
5145 T t2102 o2 b2102
5146 B b2103 t2102
5147 T t2103 o937 b2092 b983 b2103
5148 B b2104 t2103
5149 T t2104 o2 b2104
5150 B b2105 t2104
5151 T t2105 o937 b2089 b983 b2105
5152 B b2106 t2105
5153 T t2106 o2 b2106
5154 B b2107 t2106
5155 T t2107 o937 b2085 b983 b2107
5156 B b2108 t2107
5157 T t2108 o2 b2108
5158 B b2109 t2108
5159 T t2109 o937 b2083 b4 b2109
5160 B b2110 t2109
5161 T t2110 o2 b2110
5162 B b2111 t2110
5163 T t2111 o937 b2081 b4 b2111
5164 B b2112 t2111
5165 T t2112 o2 b2112
5166 B b2113 t2112
5167 T t2113 o937 b2077 b4 b2113
5168 B b2114 t2113
5169 T t2114 o2 b2114
5170 B b2115 t2114
5171 T t2115 o937 b2073 b4 b2115
5172 B b2116 t2115
5173 T t2116 o2 b2116
5174 B b2117 t2116
5175 T t2117 o973 b2071 b983 b2117
5176 B b2118 t2117
5177 T t2118 o2 b2118
5178 B b2119 t2118
5179 T t2119 o973 b2068 b4 b2119
5180 B b2120 t2119
5181 T t2122 o936 b2120 b4
5182 B b2123 t2122
5183 T t2123 o1071 b935 b2123 b4 b4
5184 B b2124 t2123
5185 T t2124 o b2124 b4
5186 B b2125 t2124
5187 T t616 o2063 b935 b615 b4 b2125
5188 B b616 t616
5189 T t624 o b616 b4
5190 B b624 t624
5191 T t625 o b2063 b624
5192 B b625 t625
5193 T t633 o b2056 b625
5194 B b633 t633
5195 T t634 o1990 b935 b570 b607 b633
5196 B b634 t634
5197 T t635 o b634 b4
5198 B b635 t635
5199 T t646 o b1990 b635
5200 B b646 t646
5201 T t653 o1942 b935 b1988 b646 b4
5202 B b653 t653
5203 T t654 o933 b653
5204 B b654 t654
5205 P p2133 Number 7383
5206 P p2134 Number 7391
5207 O o2134 resource_defs p2133 p2134 p264
5208 P p2135 Number 7389
5209 O o2135 uid p2135 p2134
5210 T t2135 o2135 b626
5211 B b2135 t2135
5212 T t2136 o b2135 b4
5213 B b2136 t2136
5214 T t2137 o2134 b2136
5215 B b2137 t2137
5216 T t2138 o b2137 b4
5217 B b2138 t2138
5218 T t665 o1913 b618 b1942 b654 b2138
5219 B b665 t665
5220 T t672 o1912 b665
5221 B b672 t672
5222 P p2140 Number 7826
5223 P p2141 Number 8245
5224 O o2141 location p2140 p2141
5225 P p2142 String unique_sol2
5226 O o2142 rule p2142
5227 P p2143 Var y
5228 O o2143 var p2143
5229 T t2143 o2143
5230 B b2143 t2143
5231 T t2144 o620 b2143
5232 S s2144 t637 h
5233 G s2144 t2144
5234 B b2144 s2144
5235 T t2145 o618 b2144
5236 B b2145 t2145
5237 T t2146 o655 b2143 b554
5238 S s2146 t620 h
5239 G s2146 t2146
5240 B b2146 s2146
5241 T t2147 o618 b2146
5242 B b2147 t2147
5243 T t2148 o559 b2143 b1914
5244 B b2148 t2148
5245 T t2149 o738 b2148 b1917
5246 S s2149 t620 h
5247 G s2149 t2149
5248 B b2149 s2149
5249 T t2150 o618 b2149
5250 B b2150 t2150
5251 T t2151 o559 b1917 b1932
5252 B b2151 t2151
5253 T t2152 o738 b2143 b2151
5254 S s2152 t620 h
5255 G s2152 t2152
5256 B b2152 s2152
5257 T t2153 o618 b2152
5258 B b2153 t2153
5259 T t2154 o635 b2150 b2153
5260 B b2154 t2154
5261 T t2155 o635 b2147 b2154
5262 B b2155 t2155
5263 T t2156 o635 b1926 b2155
5264 B b2156 t2156
5265 T t2157 o635 b1924 b2156
5266 B b2157 t2157
5267 T t2158 o635 b2145 b2157
5268 B b2158 t2158
5269 T t2159 o635 b1919 b2158
5270 B b2159 t2159
5271 T t2160 o635 b1916 b2159
5272 B b2160 t2160
5273 P p2160 String "assumT 7 thenT assertT << equal{op{op{'y; 'a}; inv{'a}}; op{'b; inv{'a}}} >> thenT autoT"
5274 O o2160 ext_rule p2160
5275 T t2161 o b2149 b4
5276 B b2161 t2161
5277 T t2162 o b2146 b2161
5278 B b2162 t2162
5279 T t2163 o b1925 b2162
5280 B b2163 t2163
5281 T t2164 o b1923 b2163
5282 B b2164 t2164
5283 T t2165 o b2144 b2164
5284 B b2165 t2165
5285 T t2166 o b1918 b2165
5286 B b2166 t2166
5287 T t2167 o b1915 b2166
5288 B b2167 t2167
5289 T t2168 o938 b2152 b2167
5290 B b2168 t2168
5291 T t2169 o937 b2168 b4 b946
5292 B b2169 t2169
5293 H h2169 v t2149
5294 T t2170 o676 b2148 b1917
5295 S s2170 t620 h h2169
5296 G s2170 t2170
5297 B b2170 s2170
5298 T t2171 o938 b2170 b2167
5299 B b2171 t2171
5300 T t2172 o559 b2148 b1932
5301 B b2172 t2172
5302 T t2173 o676 b2172 b2151
5303 S s2173 t620 h h2169
5304 G s2173 t2173
5305 B b2173 s2173
5306 T t2174 o938 b2173 b2167
5307 B b2174 t2174
5308 T t2175 o738 b2172 b2151
5309 S s2175 t620 h h2169
5310 G s2175 t2175
5311 B b2175 s2175
5312 T t2176 o938 b2175 b2167
5313 B b2176 t2176
5314 S s2176 t620 h h2169
5315 G s2176 t2152
5316 B b2177 s2176
5317 T t2177 o938 b2177 b2167
5318 B b2178 t2177
5319 T t2178 o2 b2169
5320 B b2179 t2178
5321 T t2179 o937 b2178 b4 b2179
5322 B b2180 t2179
5323 T t2180 o2 b2180
5324 B b2181 t2180
5325 T t2181 o947 b2176 b983 b2181
5326 B b2182 t2181
5327 T t2182 o2 b2182
5328 B b2183 t2182
5329 T t2183 o947 b2174 b983 b2183
5330 B b2184 t2183
5331 T t2184 o2 b2184
5332 B b2185 t2184
5333 T t2185 o947 b2171 b4 b2185
5334 B b2186 t2185
5335 H h2186 v_1 t2175
5336 T t2186 o676 b2143 b2151
5337 S s2186 t620 h h2169 h2186
5338 G s2186 t2186
5339 B b2187 s2186
5340 T t2187 o938 b2187 b2167
5341 B b2188 t2187
5342 S s2188 t620 h h2169 h2186
5343 G s2188 t2152
5344 B b2189 s2188
5345 T t2189 o938 b2189 b2167
5346 B b2190 t2189
5347 T t2190 o937 b2190 b983 b2181
5348 B b2191 t2190
5349 T t2191 o2 b2191
5350 B b2192 t2191
5351 T t2192 o937 b2188 b4 b2192
5352 B b2193 t2192
5353 T t2193 o b2193 b4
5354 B b2194 t2193
5355 T t2194 o b2186 b2194
5356 B b2195 t2194
5357 T t2195 o936 b2169 b2195
5358 B b2196 t2195
5359 P p2196 String "rwh unfold_equal 2 thenT autoT"
5360 O o2196 ext_rule p2196
5361 T t2196 o936 b2186 b4
5362 B b2197 t2196
5363 T t2197 o2196 b935 b2197 b4 b4
5364 B b2198 t2197
5365 P p2198 String "setSubstT << equal{op{op{'y; 'a}; inv{'a}}; op{'y; op{'a; inv{'a}}}} >> 3 thenT autoT"
5366 O o2198 ext_rule p2198
5367 T t2198 o559 b1914 b1932
5368 B b2199 t2198
5369 T t2199 o559 b2143 b2199
5370 B b2200 t2199
5371 T t2200 o738 b2200 b2151
5372 H h2200 v_2 t2200
5373 S s2200 t620 h h2169 h2186 h2200
5374 G s2200 t2186
5375 B b2201 s2200
5376 T t2201 o938 b2201 b2167
5377 B b2202 t2201
5378 T t2202 o2 b2193
5379 B b2203 t2202
5380 T t2203 o937 b2202 b4 b2203
5381 B b2204 t2203
5382 T t673 o b2204 b4
5383 B b673 t673
5384 T t687 o936 b2193 b673
5385 B b687 t687
5386 B b2205 t2151 v_2
5387 T t2205 o711 b2205
5388 S s2205 t620 h h2169 h2186
5389 G s2205 t2205
5390 B b2206 s2205
5391 T t2206 o938 b2206 b2167
5392 B b2207 t2206
5393 T t2207 o738 b977 b2151
5394 B b2208 t2207 v_2
5395 T t2208 o976 b2208
5396 S s2208 t620 h h2169 h2186
5397 G s2208 t2208
5398 B b2209 s2208
5399 T t2209 o938 b2209 b2167
5400 B b2210 t2209
5401 T t2210 o973 b2210 b983 b2203
5402 B b2211 t2210
5403 T t2211 o2 b2211
5404 B b2212 t2211
5405 T t2212 o973 b2207 b4 b2212
5406 B b2213 t2212
5407 P p2216 String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"
5408 O o2216 ext_rule p2216
5409 T t2216 o559 b2143 b567
5410 B b2217 t2216
5411 T t2217 o738 b2217 b2151
5412 H h2217 v_3 t2217
5413 S s2217 t620 h h2169 h2186 h2200 h2217
5414 G s2217 t2186
5415 B b2218 s2217
5416 T t2218 o938 b2218 b2167
5417 B b2219 t2218
5418 T t2219 o2 b2204
5419 B b2220 t2219
5420 T t2220 o937 b2219 b4 b2220
5421 B b2221 t2220
5422 T t694 o b2221 b4
5423 B b694 t694
5424 T t703 o936 b2204 b694
5425 B b703 t703
5426 B b2222 t2151 v_3
5427 T t2222 o711 b2222
5428 S s2222 t620 h h2169 h2186 h2200
5429 G s2222 t2222
5430 B b2223 s2222
5431 T t2223 o938 b2223 b2167
5432 B b2224 t2223
5433 T t2224 o559 b2143 b1004
5434 B b2225 t2224
5435 T t2225 o738 b2225 b2151
5436 B b2226 t2225 v_3
5437 T t2226 o976 b2226
5438 S s2226 t620 h h2169 h2186 h2200
5439 G s2226 t2226
5440 B b2227 s2226
5441 T t2227 o938 b2227 b2167
5442 B b2228 t2227
5443 T t2228 o973 b2228 b983 b2220
5444 B b2229 t2228
5445 T t2229 o2 b2229
5446 B b2230 t2229
5447 T t2230 o973 b2224 b4 b2230
5448 B b2231 t2230
5449 P p2234 String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"
5450 O o2234 ext_rule p2234
5451 T t717 o936 b2221 b4
5452 B b717 t717
5453 T t2234 o620 b2217
5454 H h2234 y_2 t2234
5455 T t2235 o620 b2151
5456 H h2235 z_1 t2235
5457 T t2236 o676 b2217 b2151
5458 H h2236 z t2236
5459 S s2236 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5460 G s2236 t2222
5461 B b2236 s2236
5462 T t2237 o938 b2236 b2167
5463 B b2237 t2237
5464 T t2238 o676 b1004 b2151
5465 B b2238 t2238 v_3
5466 T t2239 o976 b2238
5467 S s2239 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5468 G s2239 t2239
5469 B b2239 s2239
5470 T t2240 o938 b2239 b2167
5471 B b2240 t2240
5472 S s2240 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5473 G s2240 t2186
5474 B b2241 s2240
5475 T t2241 o938 b2241 b2167
5476 B b2242 t2241
5477 B b2243 t2234
5478 B b2244 t2235
5479 T t2244 o1270 b2243 b2244
5480 H h2244 y_1 t2244
5481 S s2244 t620 h h2169 h2186 h2200 h2244 h2236
5482 G s2244 t2186
5483 B b2245 s2244
5484 T t2245 o938 b2245 b2167
5485 B b2246 t2245
5486 B b2247 t2244
5487 B b2248 t2236
5488 T t2248 o1270 b2247 b2248
5489 H h2248 v_3 t2248
5490 S s2248 t620 h h2169 h2186 h2200 h2248
5491 G s2248 t2186
5492 B b2249 s2248
5493 T t2249 o938 b2249 b2167
5494 B b2250 t2249
5495 T t2250 o2 b2221
5496 B b2251 t2250
5497 T t2251 o937 b2250 b4 b2251
5498 B b2252 t2251
5499 T t2252 o2 b2252
5500 B b2253 t2252
5501 T t2253 o937 b2246 b4 b2253
5502 B b2254 t2253
5503 T t2254 o2 b2254
5504 B b2255 t2254
5505 T t2255 o937 b2242 b4 b2255
5506 B b2256 t2255
5507 T t2256 o2 b2256
5508 B b2257 t2256
5509 T t2257 o973 b2240 b983 b2257
5510 B b2258 t2257
5511 T t2258 o2 b2258
5512 B b2259 t2258
5513 T t2259 o973 b2237 b4 b2259
5514 B b2260 t2259
5515 T t2262 o936 b2260 b4
5516 B b2263 t2262
5517 T t2263 o1071 b935 b2263 b4 b4
5518 B b2264 t2263
5519 T t2264 o b2264 b4
5520 B b2265 t2264
5521 T t724 o2234 b935 b717 b4 b2265
5522 B b724 t724
5523 T t729 o b724 b4
5524 B b729 t729
5525 T t2266 o936 b2231 b4
5526 B b2267 t2266
5527 T t2267 o1071 b935 b2267 b4 b4
5528 B b2268 t2267
5529 T t2268 o b2268 b4
5530 B b2269 t2268
5531 T t736 o2216 b935 b703 b729 b2269
5532 B b736 t736
5533 T t749 o b736 b4
5534 B b749 t749
5535 T t2271 o936 b2213 b4
5536 B b2272 t2271
5537 T t2272 o1071 b935 b2272 b4 b4
5538 B b2273 t2272
5539 T t2273 o b2273 b4
5540 B b2274 t2273
5541 T t756 o2198 b935 b687 b749 b2274
5542 B b756 t756
5543 T t765 o b756 b4
5544 B b765 t765
5545 T t772 o b2198 b765
5546 B b772 t772
5547 T t775 o2160 b935 b2196 b772 b4
5548 B b775 t775
5549 T t782 o933 b775
5550 B b782 t782
5551 P p2280 Number 7853
5552 P p2281 Number 7861
5553 O o2281 resource_defs p2280 p2281 p264
5554 P p2282 Number 7859
5555 O o2282 uid p2282 p2281
5556 T t2282 o2282 b626
5557 B b2282 t2282
5558 T t2283 o b2282 b4
5559 B b2283 t2283
5560 T t2284 o2281 b2283
5561 B b2284 t2284
5562 T t2285 o b2284 b4
5563 B b2285 t2285
5564 T t785 o2142 b618 b2160 b782 b2285
5565 B b785 t785
5566 T t792 o2141 b785
5567 B b792 t792
5568 P p2287 Number 8273
5569 P p2288 Number 8568
5570 O o2288 location p2287 p2288
5571 P p2289 String inv_simplify
5572 O o2289 rule p2289
5573 T t2289 o559 b1914 b1917
5574 B b2289 t2289
5575 T t2290 o572 b2289
5576 B b2290 t2290
5577 T t2291 o572 b1917
5578 B b2291 t2291
5579 T t2292 o559 b2291 b1932
5580 B b2292 t2292
5581 T t2293 o738 b2290 b2292
5582 S s2293 t620 h
5583 G s2293 t2293
5584 B b2293 s2293
5585 T t2294 o618 b2293
5586 B b2294 t2294
5587 T t2295 o635 b1926 b2294
5588 B b2295 t2295
5589 T t2296 o635 b1924 b2295
5590 B b2296 t2296
5591 T t2297 o635 b1919 b2296
5592 B b2297 t2297
5593 T t2298 o635 b1916 b2297
5594 B b2298 t2298
5595 P p794 String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >>"
5596 O o794 ext_rule p794
5597 T t2299 o b1925 b4
5598 B b2299 t2299
5599 T t2300 o b1923 b2299
5600 B b2300 t2300
5601 T t2301 o b1918 b2300
5602 B b2301 t2301
5603 T t2302 o b1915 b2301
5604 B b2302 t2302
5605 T t2303 o938 b2293 b2302
5606 B b2303 t2303
5607 T t2304 o937 b2303 b4 b946
5608 B b2304 t2304
5609 T t2305 o559 b2290 b2289
5610 B b2305 t2305
5611 T t2306 o559 b2292 b2289
5612 B b2306 t2306
5613 T t2307 o738 b2305 b2306
5614 S s2307 t620 h
5615 G s2307 t2307
5616 B b2307 s2307
5617 T t2308 o938 b2307 b2302
5618 B b2308 t2308
5619 T t2309 o2 b2304
5620 B b2309 t2309
5621 T t2310 o947 b2308 b4 b2309
5622 B b2310 t2310
5623 H h2310 v t2307
5624 S s2310 t620 h h2310
5625 G s2310 t2293
5626 B b2311 s2310
5627 T t2311 o938 b2311 b2302
5628 B b2312 t2311
5629 T t2312 o937 b2312 b4 b2309
5630 B b2313 t2312
5631 T t2313 o b2313 b4
5632 B b2314 t2313
5633 T t2314 o b2310 b2314
5634 B b2315 t2314
5635 T t2315 o936 b2304 b2315
5636 B b2316 t2315
5637 P p2316 String "setSubstT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; id} >> 0 thenWT autoT"
5638 O o2316 ext_rule p2316
5639 T t2316 o738 b2305 b567
5640 S s2316 t620 h
5641 G s2316 t2316
5642 B b2317 s2316
5643 T t2317 o938 b2317 b2302
5644 B b2318 t2317
5645 T t2318 o2 b2310
5646 B b2319 t2318
5647 T t2319 o966 b2318 b4 b2319
5648 B b2320 t2319
5649 T t2320 o738 b567 b2306
5650 S s2320 t620 h
5651 G s2320 t2320
5652 B b2321 s2320
5653 T t2321 o938 b2321 b2302
5654 B b2322 t2321
5655 T t2322 o937 b2322 b4 b2319
5656 B b2323 t2322
5657 T t800 o b2323 b4
5658 B b800 t800
5659 T t807 o b2320 b800
5660 B b807 t807
5661 T t813 o936 b2310 b807
5662 B b813 t813
5663 P p2326 Var v
5664 O o2326 var p2326
5665 T t2326 o2326
5666 B b2327 t2326
5667 T t2337 o936 b2320 b4
5668 B b2338 t2337
5669 T t2338 o990 b935 b2338 b4 b4
5670 B b2339 t2338
5671 P p2339 String "setSubstT << equal{id; op{inv{'b}; op{inv{'a}; op{'a; 'b}}}} >> 0 thenWT autoT"
5672 O o2339 ext_rule p2339
5673 T t2339 o559 b1932 b2289
5674 B b2340 t2339
5675 T t2340 o559 b2291 b2340
5676 B b2341 t2340
5677 T t2341 o738 b567 b2341
5678 S s2341 t620 h
5679 G s2341 t2341
5680 B b2342 s2341
5681 T t2342 o938 b2342 b2302
5682 B b2343 t2342
5683 T t2343 o2 b2323
5684 B b2344 t2343
5685 T t2344 o966 b2343 b4 b2344
5686 B b2345 t2344
5687 T t2345 o738 b2341 b2306
5688 S s2345 t620 h
5689 G s2345 t2345
5690 B b2346 s2345
5691 T t2346 o938 b2346 b2302
5692 B b2347 t2346
5693 T t2347 o937 b2347 b4 b2344
5694 B b2348 t2347
5695 T t820 o b2348 b4
5696 B b820 t820
5697 T t821 o b2345 b820
5698 B b821 t821
5699 T t822 o936 b2323 b821
5700 B b822 t822
5701 P p2355 String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"
5702 O o2355 ext_rule p2355
5703 T t2355 o559 b1991 b1917
5704 B b2356 t2355
5705 T t2356 o738 b2340 b2356
5706 S s2356 t620 h
5707 G s2356 t2356
5708 B b2357 s2356
5709 T t2357 o938 b2357 b2302
5710 B b2358 t2357
5711 T t2358 o2 b2345
5712 B b2359 t2358
5713 T t2359 o966 b2358 b4 b2359
5714 B b2360 t2359
5715 T t2360 o559 b2291 b2356
5716 B b2361 t2360
5717 T t2361 o738 b567 b2361
5718 S s2361 t620 h
5719 G s2361 t2361
5720 B b2362 s2361
5721 T t2362 o938 b2362 b2302
5722 B b2363 t2362
5723 T t2363 o937 b2363 b4 b2359
5724 B b2364 t2363
5725 T t2364 o b2364 b4
5726 B b2365 t2364
5727 T t2365 o b2360 b2365
5728 B b2366 t2365
5729 T t2366 o936 b2345 b2366
5730 B b2367 t2366
5731 T t2367 o936 b2360 b4
5732 B b2368 t2367
5733 T t2368 o990 b935 b2368 b4 b4
5734 B b2369 t2368
5735 P p2369 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 0 thenWT autoT"
5736 O o2369 ext_rule p2369
5737 T t2369 o738 b1991 b567
5738 S s2369 t620 h
5739 G s2369 t2369
5740 B b2370 s2369
5741 T t2370 o938 b2370 b2302
5742 B b2371 t2370
5743 T t2371 o2 b2364
5744 B b2372 t2371
5745 T t2372 o966 b2371 b4 b2372
5746 B b2373 t2372
5747 T t2373 o559 b567 b1917
5748 B b2374 t2373
5749 T t2374 o559 b2291 b2374
5750 B b2375 t2374
5751 T t2375 o738 b567 b2375
5752 S s2375 t620 h
5753 G s2375 t2375
5754 B b2376 s2375
5755 T t2376 o938 b2376 b2302
5756 B b2377 t2376
5757 T t2377 o937 b2377 b4 b2372
5758 B b2378 t2377
5759 T t2378 o559 b2327 b1917
5760 B b2379 t2378
5761 T t2379 o559 b2291 b2379
5762 B b2380 t2379 v
5763 T t2380 o711 b2380
5764 S s2380 t620 h
5765 G s2380 t2380
5766 B b2381 s2380
5767 T t2381 o938 b2381 b2302
5768 B b2382 t2381
5769 B b2383 t2379
5770 T t2383 o738 b567 b2383
5771 B b2384 t2383 v
5772 T t2384 o976 b2384
5773 S s2384 t620 h
5774 G s2384 t2384
5775 B b2385 s2384
5776 T t2385 o938 b2385 b2302
5777 B b2386 t2385
5778 T t2386 o973 b2386 b983 b2372
5779 B b2387 t2386
5780 T t2387 o2 b2387
5781 B b2388 t2387
5782 T t2388 o973 b2382 b4 b2388
5783 B b2389 t2388
5784 T t2389 o b2389 b4
5785 B b2390 t2389
5786 T t2390 o b2378 b2390
5787 B b2391 t2390
5788 T t2391 o b2373 b2391
5789 B b2392 t2391
5790 T t2392 o936 b2364 b2392
5791 B b2393 t2392
5792 T t2393 o936 b2373 b4
5793 B b2394 t2393
5794 T t2394 o990 b935 b2394 b4 b4
5795 B b2395 t2394
5796 P p2395 String "setSubstT << equal{op{id; 'b}; 'b} >> 0 thenWT autoT"
5797 O o2395 ext_rule p2395
5798 T t2395 o738 b2374 b1917
5799 S s2395 t620 h
5800 G s2395 t2395
5801 B b2396 s2395
5802 T t2396 o938 b2396 b2302
5803 B b2397 t2396
5804 T t2397 o2 b2378
5805 B b2398 t2397
5806 T t2398 o966 b2397 b4 b2398
5807 B b2399 t2398
5808 T t2399 o559 b2291 b1917
5809 B b2400 t2399
5810 T t2400 o738 b567 b2400
5811 S s2400 t620 h
5812 G s2400 t2400
5813 B b2401 s2400
5814 T t2401 o938 b2401 b2302
5815 B b2402 t2401
5816 T t2402 o937 b2402 b4 b2398
5817 B b2403 t2402
5818 T t2403 o b2403 b4
5819 B b2404 t2403
5820 T t2404 o b2399 b2404
5821 B b2405 t2404
5822 T t2405 o936 b2378 b2405
5823 B b2406 t2405
5824 T t2406 o936 b2399 b4
5825 B b2407 t2406
5826 T t2407 o990 b935 b2407 b4 b4
5827 B b2408 t2407
5828 P p2408 String "setSubstT << equal{op{inv{'b}; 'b}; id} >> 0 thenT autoT"
5829 O o2408 ext_rule p2408
5830 T t2408 o936 b2403 b4
5831 B b2409 t2408
5832 T t2409 o2408 b935 b2409 b4 b4
5833 B b2410 t2409
5834 T t2410 o b2410 b4
5835 B b2411 t2410
5836 T t2411 o b2408 b2411
5837 B b2412 t2411
5838 T t2412 o2395 b935 b2406 b2412 b4
5839 B b2413 t2412
5840 P p2413 String "rwh unfold_fun_set 0 thenT dT 0"
5841 O o2413 ext_rule p2413
5842 NItt_equal Itt_equal Itt_equal NIL
5843 NItt_equal!type type type Itt_equal
5844 O o2414 type
5845 T t2414 o2414 b1186
5846 S s2414 t637 h
5847 G s2414 t2414
5848 B b2414 s2414
5849 T t2415 o938 b2414 b2302
5850 B b2415 t2415
5851 T t2416 o559 b560 b1917
5852 B b2416 t2416
5853 T t2417 o559 b2291 b2416
5854 B b2417 t2417
5855 T t2418 o559 b561 b1917
5856 B b2418 t2418
5857 T t2419 o559 b2291 b2418
5858 B b2419 t2419
5859 T t2420 o738 b2417 b2419
5860 B b2420 t2420
5861 T t2421 o1177 b1347 b2420
5862 B b2421 t2421 s2
5863 T t2422 o1185 b1186 b2421
5864 B b2422 t2422 s1
5865 T t2423 o1185 b1186 b2422
5866 S s2423 t620 h
5867 G s2423 t2423
5868 B b2423 s2423
5869 T t2424 o938 b2423 b2302
5870 B b2424 t2424
5871 T t2425 o2 b2389
5872 B b2425 t2425
5873 T t2426 o973 b2424 b4 b2425
5874 B b2426 t2426
5875 T t2427 o2 b2426
5876 B b2427 t2427
5877 T t2428 o973 b2415 b4 b2427
5878 B b2428 t2428
5879 S s2428 t620 h h1344
5880 G s2428 t2422
5881 B b2429 s2428
5882 T t2429 o938 b2429 b2302
5883 B b2430 t2429
5884 T t2430 o937 b2430 b4 b2427
5885 B b2431 t2430
5886 T t2431 o b2431 b4
5887 B b2432 t2431
5888 T t2432 o b2428 b2432
5889 B b2433 t2432
5890 T t2433 o936 b2389 b2433
5891 B b2434 t2433
5892 T t2434 o936 b2428 b4
5893 B b2435 t2434
5894 T t2435 o990 b935 b2435 b4 b4
5895 B b2436 t2435
5896 P p2436 String "dT 0"
5897 O o2436 ext_rule p2436
5898 S s2436 t637 h h1344
5899 G s2436 t2414
5900 B b2437 s2436
5901 T t2437 o938 b2437 b2302
5902 B b2438 t2437
5903 T t2438 o2 b2431
5904 B b2439 t2438
5905 T t2439 o973 b2438 b4 b2439
5906 B b2440 t2439
5907 S s2440 t620 h h1344 h1224
5908 G s2440 t2421
5909 B b2441 s2440
5910 T t2441 o938 b2441 b2302
5911 B b2442 t2441
5912 T t2442 o937 b2442 b4 b2439
5913 B b2443 t2442
5914 T t2443 o b2443 b4
5915 B b2444 t2443
5916 T t2444 o b2440 b2444
5917 B b2445 t2444
5918 T t2445 o936 b2431 b2445
5919 B b2446 t2445
5920 T t2446 o936 b2440 b4
5921 B b2447 t2446
5922 T t2447 o990 b935 b2447 b4 b4
5923 B b2448 t2447
5924 T t2448 o2414 b1347
5925 S s2448 t637 h h1344 h1224
5926 G s2448 t2448
5927 B b2449 s2448
5928 T t2449 o938 b2449 b2302
5929 B b2450 t2449
5930 T t2450 o2 b2443
5931 B b2451 t2450
5932 T t2451 o973 b2450 b4 b2451
5933 B b2452 t2451
5934 S s2452 t620 h h1344 h1224 h1345
5935 G s2452 t2420
5936 B b2453 s2452
5937 T t2453 o938 b2453 b2302
5938 B b2454 t2453
5939 T t2454 o937 b2454 b4 b2451
5940 B b2455 t2454
5941 T t2455 o b2455 b4
5942 B b2456 t2455
5943 T t2456 o b2452 b2456
5944 B b2457 t2456
5945 T t2457 o936 b2443 b2457
5946 B b2458 t2457
5947 T t2458 o936 b2452 b4
5948 B b2459 t2458
5949 T t2459 o990 b935 b2459 b4 b4
5950 B b2460 t2459
5951 P p2460 String "rwh unfold_equal 0 thenT rwh unfold_equal 4 thenT autoT"
5952 O o2460 ext_rule p2460
5953 T t2460 o936 b2455 b4
5954 B b2461 t2460
5955 T t2461 o2460 b935 b2461 b4 b4
5956 B b2462 t2461
5957 T t2462 o b2462 b4
5958 B b2463 t2462
5959 T t2463 o b2460 b2463
5960 B b2464 t2463
5961 T t2464 o2436 b935 b2458 b2464 b4
5962 B b2465 t2464
5963 T t2465 o b2465 b4
5964 B b2466 t2465
5965 T t2466 o b2448 b2466
5966 B b2467 t2466
5967 T t2467 o2436 b935 b2446 b2467 b4
5968 B b2468 t2467
5969 T t2468 o b2468 b4
5970 B b2469 t2468
5971 T t2469 o b2436 b2469
5972 B b2470 t2469
5973 T t2470 o2413 b935 b2434 b2470 b4
5974 B b2471 t2470
5975 T t2471 o b2471 b4
5976 B b2472 t2471
5977 T t2472 o b2413 b2472
5978 B b2473 t2472
5979 T t2473 o b2395 b2473
5980 B b2474 t2473
5981 T t2474 o2369 b935 b2393 b2474 b4
5982 B b2475 t2474
5983 T t2475 o b2475 b4
5984 B b2476 t2475
5985 T t2476 o b2369 b2476
5986 B b2477 t2476
5987 T t2477 o2355 b935 b2367 b2477 b4
5988 B b2478 t2477
5989 T t2478 o936 b2348 b4
5990 B b2479 t2478
5991 T t2479 o990 b935 b2479 b4 b4
5992 B b2480 t2479
5993 T t825 o b2480 b4
5994 B b825 t825
5995 T t826 o b2478 b825
5996 B b826 t826
5997 T t827 o2339 b935 b822 b826 b4
5998 B b827 t827
5999 T t828 o b827 b4
6000 B b828 t828
6001 T t829 o b2339 b828
6002 B b829 t829
6003 T t830 o2316 b935 b813 b829 b4
6004 B b830 t830
6005 P p2515 String "groupCancelRightT << op{'a; 'b} >> thenT autoT"
6006 O o2515 ext_rule p2515
6007 T t2515 o936 b2313 b4
6008 B b2516 t2515
6009 T t2516 o2515 b935 b2516 b4 b4
6010 B b2517 t2516
6011 T t2517 o b2517 b4
6012 B b2518 t2517
6013 T t833 o b830 b2518
6014 B b833 t833
6015 T t834 o794 b935 b2316 b833 b4
6016 B b834 t834
6017 T t835 o933 b834
6018 B b835 t835
6019 P p2521 Number 8301
6020 P p2522 Number 8309
6021 O o2522 resource_defs p2521 p2522 p264
6022 P p2523 Number 8307
6023 O o2523 uid p2523 p2522
6024 T t2523 o2523 b626
6025 B b2523 t2523
6026 T t2524 o b2523 b4
6027 B b2524 t2524
6028 T t2525 o2522 b2524
6029 B b2525 t2525
6030 T t2526 o b2525 b4
6031 B b2526 t2526
6032 T t856 o2289 b618 b2298 b835 b2526
6033 B b856 t856
6034 T t862 o2288 b856
6035 B b862 t862
6036 O o2528 location p p
6037 NSummary!id id2528 id Summary
6038 P p2528 Number 646427455
6039 O o2529 id2528 p2528
6040 T t2529 o2529
6041 B b2529 t2529
6042 T t2530 o2528 b2529
6043 B b2530 t2530
6044 T t2531 o b2530 b4
6045 B b2531 t2531
6046 T t869 o b862 b2531
6047 B b869 t869
6048 T t874 o b792 b869
6049 B b874 t874
6050 T t881 o b672 b874
6051 B b881 t881
6052 T t885 o b565 b881
6053 B b885 t885
6054 T t892 o b531 b885
6055 B b892 t892
6056 T t898 o b1723 b892
6057 B b898 t898
6058 T t905 o b1683 b898
6059 B b905 t905
6060 T t911 o b470 b905
6061 B b911 t911
6062 T t918 o b385 b911
6063 B b918 t918
6064 T t919 o b917 b918
6065 B b919 t919
6066 T t934 o b904 b919
6067 B b934 t934
6068 T t936 o b891 b934
6069 B b936 t936
6070 T t937 o b880 b936
6071 B b937 t937
6072 T t957 o b868 b937
6073 B b1097 t957
6074 T t1097 o b855 b1097
6075 B b1098 t1097
6076 T t1098 o b819 b1098
6077 B b1099 t1098
6078 T t1099 o b806 b1099
6079 B b1172 t1099
6080 T t1178 o b791 b1172
6081 B b1225 t1178
6082 T t1230 o b781 b1225
6083 B b1265 t1230
6084 T t1270 o b771 b1265
6085 B b1424 t1270
6086 T t1424 o b755 b1424
6087 B b1431 t1424
6088 T t1431 o b735 b1431
6089 B b1567 t1431
6090 T t1567 o b723 b1567
6091 B b1568 t1567
6092 T t1568 o b709 b1568
6093 B b1636 t1568
6094 T t1636 o b693 b1636
6095 B b1643 t1636
6096 T t1643 o b671 b1643
6097 B b1644 t1643
6098 T t1644 o b652 b1644
6099 B b1645 t1644
6100 T t1645 o b632 b1645
6101 B b1648 t1645
6102 T t1648 o b614 b1648
6103 B b1649 t1648
6104 T t1649 o b606 b1649
6105 B b1650 t1649
61