/[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 3484 - (show annotations) (download)
Wed Jan 30 00:36:09 2002 UTC (19 years, 5 months ago) by xiny
File size: 124393 byte(s)
Now a workable version for groups and cyclic subgroups. Rules proved, examples  added.
Problems left:
   The proofs for rules "power_property1", "power_property2", and "power_simplify" are not yet finished because of some itt problems.

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 p3 Number 1570
1743 P p4 Number 1847
1744 O o6 location p3 p4
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 p6 Number 1592
1785 P p8 Number 1599
1786 O o8 resource_defs p6 p8 p264
1787 P p10 Number 1597
1788 O o10 uid p10 p8
1789 T t965 o10 b626
1790 B b987 t965
1791 T t987 o b987 b4
1792 B b988 t987
1793 T t988 o8 b988
1794 B b989 t988
1795 T t989 o b989 b4
1796 B b990 t989
1797 T t990 o673 b618 b686 b623 b990
1798 B b1011 t990
1799 T t1011 o6 b1011
1800 B b1012 t1011
1801 P p1012 Number 1849
1802 P p1013 Number 2126
1803 O o1013 location p1012 p1013
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 p1014 Number 1871
1825 P p1015 Number 1878
1826 O o1015 resource_defs p1014 p1015 p264
1827 P p1017 Number 1876
1828 O o1017 uid p1017 p1015
1829 T t1028 o1017 b626
1830 B b1039 t1028
1831 T t1039 o b1039 b4
1832 B b1040 t1039
1833 T t1040 o1015 b1040
1834 B b1041 t1040
1835 T t1041 o b1041 b4
1836 B b1068 t1041
1837 T t1068 o695 b618 b702 b623 b1068
1838 B b1069 t1068
1839 T t1069 o1013 b1069
1840 B b1070 t1069
1841 P p1070 Number 2128
1842 P p1072 Number 2261
1843 O o1072 location p1070 p1072
1844 P p710 String op_fun1
1845 O o710 rule p710
1846 T t710 o620 b573
1847 S s710 t637 h
1848 G s710 t710
1849 B b710 s710
1850 T t711 o618 b710
1851 B b711 t711
1852 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1853 O o711 fun_set
1854 P p711 Var z
1855 O o712 var p711
1856 T t712 o712
1857 B b712 t712
1858 T t713 o559 b712 b573
1859 B b713 t713 z
1860 T t714 o711 b713
1861 S s714 t620 h
1862 G s714 t714
1863 B b714 s714
1864 T t715 o618 b714
1865 B b715 t715
1866 T t716 o635 b711 b715
1867 B b716 t716
1868 P p1073 Number 2158
1869 O o1073 resource_defs p331 p1073 p264
1870 P p1074 Number 2156
1871 O o1074 uid p1074 p1073
1872 T t1074 o1074 b626
1873 B b1075 t1074
1874 T t1075 o b1075 b4
1875 B b1076 t1075
1876 T t1076 o1073 b1076
1877 B b1077 t1076
1878 T t1080 o b1077 b4
1879 B b1081 t1080
1880 T t1081 o710 b618 b716 b623 b1081
1881 B b1082 t1081
1882 T t1082 o1072 b1082
1883 B b1083 t1082
1884 P p1083 Number 2263
1885 P p1084 Number 2396
1886 O o1084 location p1083 p1084
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 p1085 Number 2286
1900 P p1086 Number 2293
1901 O o1086 resource_defs p1085 p1086 p264
1902 P p1087 Number 2291
1903 O o1087 uid p1087 p1086
1904 T t1091 o1087 b626
1905 B b1173 t1091
1906 T t1181 o b1173 b4
1907 B b1266 t1181
1908 T t1271 o1086 b1266
1909 B b1303 t1271
1910 T t1303 o b1303 b4
1911 B b1304 t1303
1912 T t1304 o725 b618 b728 b623 b1304
1913 B b1305 t1304
1914 T t1309 o1084 b1305
1915 B b1319 t1309
1916 P p1319 Number 2398
1917 P p1320 Number 2791
1918 O o1320 location p1319 p1320
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 p1322 Number 2423
1952 P p1323 Number 2430
1953 O o1323 resource_defs p1322 p1323 p264
1954 P p1324 Number 2428
1955 O o1324 uid p1324 p1323
1956 T t1331 o1324 b626
1957 B b1340 t1331
1958 T t1340 o b1340 b4
1959 B b1341 t1340
1960 T t1341 o1323 b1341
1961 B b1342 t1341
1962 T t1345 o b1342 b4
1963 B b1345 t1345
1964 T t1346 o737 b618 b748 b623 b1345
1965 B b1346 t1346
1966 T t1347 o1320 b1346
1967 B b1348 t1347
1968 P p1348 Number 2864
1969 P p1349 Number 3257
1970 O o1349 location p1348 p1349
1971 P p756 Number 3358
1972 P p757 String op_assoc2
1973 O o757 rule p757
1974 T t757 o738 b740 b739
1975 S s757 t620 h
1976 G s757 t757
1977 B b757 s757
1978 T t758 o618 b757
1979 B b758 t758
1980 T t759 o635 b738 b758
1981 B b759 t759
1982 T t760 o635 b658 b759
1983 B b760 t760
1984 T t761 o635 b656 b760
1985 B b761 t761
1986 T t762 o635 b676 b761
1987 B b762 t762
1988 T t763 o635 b641 b762
1989 B b763 t763
1990 T t764 o635 b639 b763
1991 B b764 t764
1992 P p1350 Number 2889
1993 P p1351 Number 2896
1994 O o1351 resource_defs p1350 p1351 p264
1995 P p1352 Number 2894
1996 O o1352 uid p1352 p1351
1997 T t1352 o1352 b626
1998 B b1352 t1352
1999 T t1353 o b1352 b4
2000 B b1353 t1353
2001 T t1354 o1351 b1353
2002 B b1354 t1354
2003 T t1355 o b1354 b4
2004 B b1355 t1355
2005 T t1356 o757 b618 b764 b623 b1355
2006 B b1356 t1356
2007 T t1357 o1349 b1356
2008 B b1357 t1357
2009 P p1357 Number 3330
2010 P p1358 Number 3406
2011 O o1358 location p1357 p1358
2012 P p773 String id_wf1
2013 O o773 rule p773
2014 T t773 o620 b567
2015 S s773 t620 h
2016 G s773 t773
2017 B b773 s773
2018 T t774 o618 b773
2019 B b774 t774
2020 P p1359 Number 3352
2021 P p1360 Number 3360
2022 O o1360 resource_defs p1359 p1360 p264
2023 O o1361 uid p756 p1360
2024 T t1361 o1361 b626
2025 B b1361 t1361
2026 T t1362 o b1361 b4
2027 B b1362 t1362
2028 T t1363 o1360 b1362
2029 B b1363 t1363
2030 T t1364 o b1363 b4
2031 B b1364 t1364
2032 T t1365 o773 b618 b774 b623 b1364
2033 B b1365 t1365
2034 T t1366 o1358 b1365
2035 B b1366 t1366
2036 P p1366 Number 3408
2037 P p1367 Number 3486
2038 O o1367 location p1366 p1367
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 p1368 Number 3430
2048 P p1369 Number 3437
2049 O o1369 resource_defs p1368 p1369 p264
2050 P p1370 Number 3435
2051 O o1370 uid p1370 p1369
2052 T t1370 o1370 b626
2053 B b1370 t1370
2054 T t1371 o b1370 b4
2055 B b1371 t1371
2056 T t1372 o1369 b1371
2057 B b1372 t1372
2058 T t1373 o b1372 b4
2059 B b1373 t1373
2060 T t1376 o783 b618 b784 b623 b1373
2061 B b1377 t1376
2062 T t1377 o1367 b1377
2063 B b1378 t1377
2064 P p1379 Number 3574
2065 P p1380 Number 3750
2066 O o1380 location p1379 p1380
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 p1381 Number 3596
2088 P p1382 Number 3603
2089 O o1382 resource_defs p1381 p1382 p264
2090 P p1383 Number 3601
2091 O o1383 uid p1383 p1382
2092 T t1395 o1383 b626
2093 B b1396 t1395
2094 T t1398 o b1396 b4
2095 B b1399 t1398
2096 T t1399 o1382 b1399
2097 B b1400 t1399
2098 T t1402 o b1400 b4
2099 B b1418 t1402
2100 T t1418 o793 b618 b799 b623 b1418
2101 B b1419 t1418
2102 T t1419 o1380 b1419
2103 B b1420 t1419
2104 P p1420 Number 3752
2105 P p1421 Number 3928
2106 O o1421 location p1420 p1421
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 p1422 Number 3774
2122 P p1426 Number 3781
2123 O o1426 resource_defs p1422 p1426 p264
2124 P p1427 Number 3779
2125 O o1427 uid p1427 p1426
2126 T t1429 o1427 b626
2127 B b1429 t1429
2128 T t1430 o b1429 b4
2129 B b1430 t1430
2130 T t1459 o1426 b1430
2131 B b1489 t1459
2132 T t1489 o b1489 b4
2133 B b1490 t1489
2134 T t1490 o808 b618 b812 b623 b1490
2135 B b1491 t1490
2136 T t1496 o1421 b1491
2137 B b1506 t1496
2138 P p1506 Number 3930
2139 P p1507 Number 3987
2140 O o1507 location p1506 p1507
2141 NOcaml!str_let str_let str_let Ocaml
2142 O o1509 str_let p1506 p1507
2143 NOcaml!patt_var patt_var patt_var Ocaml
2144 P p1509 Number 3934
2145 O o1510 patt_var p1509 p1507
2146 NOcaml!patt_done patt_done patt_done Ocaml
2147 O o1511 patt_done p1506 p1507
2148 T t1520 o1511
2149 B b1530 t1520 id_elim2T
2150 T t1530 o1510 b1530
2151 B b1531 t1530
2152 NOcaml!fun fun fun Ocaml
2153 O o1531 fun p1509 p1507
2154 NOcaml!patt_if patt_if patt_if Ocaml
2155 O o1533 patt_if p1509 p1507
2156 P p1533 Number 3944
2157 P p1534 Number 3945
2158 O o1534 patt_var p1533 p1534
2159 NOcaml!patt_body patt_body patt_body Ocaml
2160 O o1535 patt_body p1509 p1507
2161 NOcaml!apply apply apply Ocaml
2162 P p1535 Number 3951
2163 O o1536 apply p1535 p1507
2164 P p1536 Number 3985
2165 O o1537 apply p1535 p1536
2166 NOcaml!lid lid lid Ocaml
2167 P p1537 Number 3957
2168 O o1538 lid p1535 p1537
2169 O o831 lid p793
2170 T t831 o831
2171 B b831 t831
2172 T t1538 o1538 b831
2173 B b1538 t1538
2174 P p1538 Number 3959
2175 P p1539 Number 3984
2176 O o1539 apply p1538 p1539
2177 NOcaml!proj proj proj Ocaml
2178 P p1540 Number 3982
2179 O o1540 proj p1538 p1540
2180 O o1541 uid p1538 p1540
2181 O o836 uid p509
2182 T t836 o836
2183 B b836 t836
2184 T t1544 o1541 b836
2185 B b1545 t1544
2186 P p1545 Number 3968
2187 O o1545 lid p1545 p1540
2188 P p838 String hyp_count_addr
2189 O o838 lid p838
2190 T t838 o838
2191 B b838 t838
2192 T t1545 o1545 b838
2193 B b1546 t1545
2194 T t1549 o1540 b1545 b1546
2195 B b1550 t1549
2196 P p1550 Number 3983
2197 O o1550 lid p1550 p1539
2198 P p841 Var p
2199 O o841 var p841
2200 T t841 o841
2201 B b841 t841
2202 T t1550 o1550 b841
2203 B b1551 t1550
2204 T t1551 o1539 b1550 b1551
2205 B b1552 t1551
2206 T t1552 o1537 b1538 b1552
2207 B b1553 t1552
2208 P p1553 Number 3986
2209 O o1553 lid p1553 p1507
2210 T t1553 o1553 b841
2211 B b1634 t1553
2212 T t1634 o1536 b1553 b1634
2213 B b1635 t1634
2214 T t1635 o1535 b1635
2215 B b1641 t1635 p
2216 T t1641 o1534 b1641
2217 B b1642 t1641
2218 T t1642 o1533 b1642
2219 B b1746 t1642
2220 T t1753 o1531 b1746
2221 B b1808 t1753
2222 T t1808 o1509 b1531 b1808
2223 B b1809 t1808
2224 T t1809 o b1809 b4
2225 B b1810 t1809
2226 T t1810 o1509 b1810
2227 B b1811 t1810
2228 T t1811 o392 b1811
2229 B b1812 t1811
2230 T t1812 o1507 b1812
2231 B b1813 t1812
2232 P p1813 Number 3989
2233 P p1814 Number 4162
2234 O o1814 location p1813 p1814
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 p1815 Number 4012
2250 P p1816 Number 4019
2251 O o1816 resource_defs p1815 p1816 p264
2252 O o1817 uid p300 p1816
2253 T t1817 o1817 b626
2254 B b1817 t1817
2255 T t1818 o b1817 b4
2256 B b1818 t1818
2257 T t1819 o1816 b1818
2258 B b1819 t1819
2259 T t1820 o b1819 b4
2260 B b1820 t1820
2261 T t1824 o857 b618 b861 b623 b1820
2262 B b1825 t1824
2263 T t1825 o1814 b1825
2264 B b1826 t1825
2265 P p1826 Number 4164
2266 P p1827 Number 4340
2267 O o1827 location p1826 p1827
2268 P p870 String inv_wf2
2269 O o870 rule p870
2270 T t870 o655 b857 b554
2271 S s870 t620 h
2272 G s870 t870
2273 B b870 s870
2274 T t871 o618 b870
2275 B b871 t871
2276 T t872 o635 b656 b871
2277 B b872 t872
2278 T t873 o635 b639 b872
2279 B b873 t873
2280 P p1828 Number 4187
2281 P p1829 Number 4194
2282 O o1829 resource_defs p1828 p1829 p264
2283 P p1830 Number 4192
2284 O o1830 uid p1830 p1829
2285 T t1830 o1830 b626
2286 B b1830 t1830
2287 T t1831 o b1830 b4
2288 B b1831 t1831
2289 T t1832 o1829 b1831
2290 B b1832 t1832
2291 T t1833 o b1832 b4
2292 B b1833 t1833
2293 T t1834 o870 b618 b873 b623 b1833
2294 B b1834 t1834
2295 T t1835 o1827 b1834
2296 B b1835 t1835
2297 P p1835 Number 4342
2298 P p1839 Number 4429
2299 O o1839 location p1835 p1839
2300 P p882 String inv_fun1
2301 O o882 rule p882
2302 T t882 o572 b712
2303 B b882 t882 z
2304 T t883 o711 b882
2305 S s883 t620 h
2306 G s883 t883
2307 B b883 s883
2308 T t884 o618 b883
2309 B b884 t884
2310 P p1840 Number 4366
2311 P p1841 Number 4373
2312 O o1841 resource_defs p1840 p1841 p264
2313 P p1842 Number 4371
2314 O o1842 uid p1842 p1841
2315 T t1842 o1842 b626
2316 B b1842 t1842
2317 T t1843 o b1842 b4
2318 B b1843 t1843
2319 T t1887 o1841 b1843
2320 B b1888 t1887
2321 T t1888 o b1888 b4
2322 B b1889 t1888
2323 T t1889 o882 b618 b884 b623 b1889
2324 B b1890 t1889
2325 T t1890 o1839 b1890
2326 B b1891 t1890
2327 P p1892 Number 4431
2328 P p1894 Number 4617
2329 O o1894 location p1892 p1894
2330 P p893 String inv_id1
2331 O o893 rule p893
2332 T t893 o559 b857 b560
2333 B b893 t893
2334 T t894 o738 b893 b567
2335 S s894 t620 h
2336 G s894 t894
2337 B b894 s894
2338 T t895 o618 b894
2339 B b895 t895
2340 T t896 o635 b656 b895
2341 B b896 t896
2342 T t897 o635 b639 b896
2343 B b897 t897
2344 P p1895 Number 4454
2345 P p1896 Number 4461
2346 O o1896 resource_defs p1895 p1896 p264
2347 P p1897 Number 4459
2348 O o1897 uid p1897 p1896
2349 T t1898 o1897 b626
2350 B b1899 t1898
2351 T t1899 o b1899 b4
2352 B b1900 t1899
2353 T t1900 o1896 b1900
2354 B b1901 t1900
2355 T t1901 o b1901 b4
2356 B b1902 t1901
2357 T t1902 o893 b618 b897 b623 b1902
2358 B b1903 t1902
2359 T t1903 o1894 b1903
2360 B b1904 t1903
2361 P p1907 Number 4619
2362 P p1908 Number 4805
2363 O o1908 location p1907 p1908
2364 P p906 String inv_id2
2365 O o906 rule p906
2366 T t906 o559 b560 b857
2367 B b906 t906
2368 T t907 o738 b906 b567
2369 S s907 t620 h
2370 G s907 t907
2371 B b907 s907
2372 T t908 o618 b907
2373 B b908 t908
2374 T t909 o635 b656 b908
2375 B b909 t909
2376 T t910 o635 b639 b909
2377 B b910 t910
2378 P p1909 Number 4642
2379 P p1910 Number 4649
2380 O o1910 resource_defs p1909 p1910 p264
2381 P p1915 Number 4647
2382 O o1915 uid p1915 p1910
2383 T t1961 o1915 b626
2384 B b2006 t1961
2385 T t2006 o b2006 b4
2386 B b2007 t2006
2387 T t2007 o1910 b2007
2388 B b2008 t2007
2389 T t2013 o b2008 b4
2390 B b2024 t2013
2391 T t2024 o906 b618 b910 b623 b2024
2392 B b2025 t2024
2393 T t2025 o1908 b2025
2394 B b2026 t2025
2395 P p2027 Number 4866
2396 P p2028 Number 5292
2397 O o2028 location p2027 p2028
2398 P p919 String cancel1
2399 O o919 rule p919
2400 NSummary!term_param term_param term_param Summary
2401 O o920 term_param
2402 T t920 o920 b560
2403 B b920 t920
2404 T t921 o b920 b4
2405 B b921 t921
2406 T t922 o b617 b921
2407 B b922 t922
2408 T t923 o738 b562 b695
2409 S s923 t620 h
2410 G s923 t923
2411 B b923 s923
2412 T t924 o618 b923
2413 B b924 t924
2414 T t925 o738 b561 b674
2415 S s925 t620 h
2416 G s925 t925
2417 B b925 s925
2418 T t926 o618 b925
2419 B b926 t926
2420 T t927 o635 b924 b926
2421 B b927 t927
2422 T t928 o635 b738 b927
2423 B b928 t928
2424 T t929 o635 b658 b928
2425 B b929 t929
2426 T t930 o635 b656 b929
2427 B b930 t930
2428 T t931 o635 b676 b930
2429 B b931 t931
2430 T t932 o635 b641 b931
2431 B b932 t932
2432 T t933 o635 b639 b932
2433 B b933 t933
2434 NSummary!interactive interactive interactive Summary
2435 O o933 interactive
2436 NSummary!ext_rule ext_rule ext_rule Summary
2437 P p933 String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2438 O o934 ext_rule p933
2439 NSummary!status_incomplete status_incomplete status_incomplete Summary
2440 O o935 status_incomplete
2441 T t935 o935
2442 B b935 t935
2443 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2444 O o936 ext_unjustified
2445 NSummary!tactic_arg tactic_arg tactic_arg Summary
2446 P p936 String main
2447 O o937 tactic_arg p936
2448 NSummary!msequent msequent msequent Summary
2449 O o938 msequent
2450 T t938 o b923 b4
2451 B b938 t938
2452 T t939 o b737 b938
2453 B b939 t939
2454 T t940 o b657 b939
2455 B b940 t940
2456 T t941 o b655 b940
2457 B b941 t941
2458 T t942 o b675 b941
2459 B b942 t942
2460 T t943 o b640 b942
2461 B b943 t943
2462 T t944 o b638 b943
2463 B b944 t944
2464 T t945 o938 b925 b944
2465 B b945 t945
2466 NSummary!parent_none parent_none parent_none Summary
2467 O o945 parent_none
2468 T t946 o945
2469 B b946 t946
2470 T t947 o937 b945 b4 b946
2471 B b947 t947
2472 P p947 String assertion
2473 O o947 tactic_arg p947
2474 H h947 v t923
2475 T t948 o559 b857 b562
2476 B b948 t948
2477 T t949 o559 b857 b695
2478 B b949 t949
2479 T t950 o738 b948 b949
2480 S s950 t620 h h947
2481 G s950 t950
2482 B b950 s950
2483 T t951 o938 b950 b944
2484 B b951 t951
2485 S s951 t620 h h947
2486 G s951 t925
2487 B b952 s951
2488 T t952 o938 b952 b944
2489 B b953 t952
2490 T t953 o2 b947
2491 B b954 t953
2492 T t954 o937 b953 b4 b954
2493 B b955 t954
2494 T t955 o2 b955
2495 B b956 t955
2496 T t956 o947 b951 b4 b956
2497 B b957 t956
2498 H h957 v_1 t950
2499 S s957 t620 h h947 h957
2500 G s957 t925
2501 B b958 s957
2502 T t958 o938 b958 b944
2503 B b959 t958
2504 T t959 o937 b959 b4 b956
2505 B b960 t959
2506 T t960 o b960 b4
2507 B b961 t960
2508 T t961 o b957 b961
2509 B b962 t961
2510 T t962 o936 b947 b962
2511 B b963 t962
2512 P p963 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2513 O o963 ext_rule p963
2514 T t963 o936 b957 b4
2515 B b964 t963
2516 T t964 o963 b935 b964 b4 b4
2517 B b965 t964
2518 P p965 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2519 O o965 ext_rule p965
2520 P p966 String eq
2521 O o966 tactic_arg p966
2522 T t966 o559 b893 b561
2523 B b966 t966
2524 T t967 o738 b948 b966
2525 S s967 t620 h h947 h957
2526 G s967 t967
2527 B b967 s967
2528 T t968 o938 b967 b944
2529 B b968 t968
2530 T t969 o2 b960
2531 B b969 t969
2532 T t970 o966 b968 b4 b969
2533 B b970 t970
2534 T t971 o738 b966 b949
2535 H h971 v_2 t971
2536 S s971 t620 h h947 h957 h971
2537 G s971 t925
2538 B b971 s971
2539 T t972 o938 b971 b944
2540 B b972 t972
2541 T t973 o937 b972 b4 b969
2542 B b973 t973
2543 T t1 o b973 b4
2544 B b1 t1
2545 T t2 o b970 b1
2546 B b2 t2
2547 T t3 o936 b960 b2
2548 B b3 t3
2549 P p973 String wf
2550 O o973 tactic_arg p973
2551 B b974 t949 v_2
2552 T t974 o711 b974
2553 S s974 t620 h h947 h957
2554 G s974 t974
2555 B b975 s974
2556 T t975 o938 b975 b944
2557 B b976 t975
2558 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2559 O o976 fun_prop
2560 P p976 Var v_2
2561 O o977 var p976
2562 T t977 o977
2563 B b977 t977
2564 T t978 o738 b977 b949
2565 B b978 t978 v_2
2566 T t979 o976 b978
2567 S s979 t620 h h947 h957
2568 G s979 t979
2569 B b979 s979
2570 T t980 o938 b979 b944
2571 B b980 t980
2572 NSummary!arg_named arg_named arg_named Summary
2573 P p980 String d_auto
2574 O o980 arg_named p980
2575 NSummary!arg_bool arg_bool arg_bool Summary
2576 P p981 String true
2577 O o981 arg_bool p981
2578 T t981 o981
2579 B b981 t981
2580 T t982 o980 b981
2581 B b982 t982
2582 T t983 o b982 b4
2583 B b983 t983
2584 T t984 o973 b980 b983 b969
2585 B b984 t984
2586 T t985 o2 b984
2587 B b985 t985
2588 T t986 o973 b976 b4 b985
2589 B b986 t986
2590 P p990 String autoT
2591 O o990 ext_rule p990
2592 T t991 o936 b970 b4
2593 B b991 t991
2594 T t992 o990 b935 b991 b4 b4
2595 B b992 t992
2596 P p992 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2597 O o992 ext_rule p992
2598 T t993 o559 b893 b674
2599 B b993 t993
2600 T t994 o738 b949 b993
2601 S s994 t620 h h947 h957 h971
2602 G s994 t994
2603 B b994 s994
2604 T t995 o938 b994 b944
2605 B b995 t995
2606 T t996 o2 b973
2607 B b996 t996
2608 T t997 o966 b995 b4 b996
2609 B b997 t997
2610 T t998 o738 b966 b993
2611 H h998 v_3 t998
2612 S s998 t620 h h947 h957 h971 h998
2613 G s998 t925
2614 B b998 s998
2615 T t999 o938 b998 b944
2616 B b999 t999
2617 T t1000 o937 b999 b4 b996
2618 B b1000 t1000
2619 T t214 o b1000 b4
2620 B b214 t214
2621 T t215 o b997 b214
2622 B b215 t215
2623 T t218 o936 b973 b215
2624 B b218 t218
2625 B b1001 t966 v_3
2626 T t1001 o711 b1001
2627 S s1001 t620 h h947 h957 h971
2628 G s1001 t1001
2629 B b1002 s1001
2630 T t1002 o938 b1002 b944
2631 B b1003 t1002
2632 P p1003 Var v_3
2633 O o1003 var p1003
2634 T t1003 o1003
2635 B b1004 t1003
2636 T t1004 o738 b966 b1004
2637 B b1005 t1004 v_3
2638 T t1005 o976 b1005
2639 S s1005 t620 h h947 h957 h971
2640 G s1005 t1005
2641 B b1006 s1005
2642 T t1006 o938 b1006 b944
2643 B b1007 t1006
2644 T t1007 o973 b1007 b983 b996
2645 B b1008 t1007
2646 T t1008 o2 b1008
2647 B b1009 t1008
2648 T t1009 o973 b1003 b4 b1009
2649 B b1010 t1009
2650 T t1014 o936 b997 b4
2651 B b1015 t1014
2652 T t1015 o990 b935 b1015 b4 b4
2653 B b1016 t1015
2654 P p1016 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2655 O o1016 ext_rule p1016
2656 T t1016 o559 b567 b561
2657 B b1017 t1016
2658 T t1017 o559 b567 b674
2659 B b1018 t1017
2660 T t1018 o738 b1017 b1018
2661 H h1018 v_4 t1018
2662 S s1018 t620 h h947 h957 h971 h998 h1018
2663 G s1018 t925
2664 B b1019 s1018
2665 T t1019 o938 b1019 b944
2666 B b1020 t1019
2667 T t1020 o2 b1000
2668 B b1021 t1020
2669 T t1021 o937 b1020 b4 b1021
2670 B b1022 t1021
2671 T t1022 o b1022 b4
2672 B b1023 t1022
2673 T t1023 o936 b1000 b1023
2674 B b1024 t1023
2675 P p1024 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2676 O o1024 ext_rule p1024
2677 T t1024 o738 b561 b1018
2678 H h1024 v_5 t1024
2679 S s1024 t620 h h947 h957 h971 h998 h1018 h1024
2680 G s1024 t925
2681 B b1025 s1024
2682 T t1025 o938 b1025 b944
2683 B b1026 t1025
2684 T t1026 o2 b1022
2685 B b1027 t1026
2686 T t1027 o937 b1026 b4 b1027
2687 B b1028 t1027
2688 T t219 o b1028 b4
2689 B b219 t219
2690 T t229 o936 b1022 b219
2691 B b229 t229
2692 B b1029 t1017 v_5
2693 T t1029 o711 b1029
2694 S s1029 t620 h h947 h957 h971 h998 h1018
2695 G s1029 t1029
2696 B b1030 s1029
2697 T t1030 o938 b1030 b944
2698 B b1031 t1030
2699 P p1031 Var v_5
2700 O o1031 var p1031
2701 T t1031 o1031
2702 B b1032 t1031
2703 T t1032 o738 b1032 b1018
2704 B b1033 t1032 v_5
2705 T t1033 o976 b1033
2706 S s1033 t620 h h947 h957 h971 h998 h1018
2707 G s1033 t1033
2708 B b1034 s1033
2709 T t1034 o938 b1034 b944
2710 B b1035 t1034
2711 T t1035 o973 b1035 b983 b1027
2712 B b1036 t1035
2713 T t1036 o2 b1036
2714 B b1037 t1036
2715 T t1037 o973 b1031 b4 b1037
2716 B b1038 t1037
2717 P p1041 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2718 O o1041 ext_rule p1041
2719 H h1041 v_6 t925
2720 S s1041 t620 h h947 h957 h971 h998 h1018 h1024 h1041
2721 G s1041 t925
2722 B b1042 s1041
2723 T t1042 o938 b1042 b944
2724 B b1043 t1042
2725 T t1043 o2 b1028
2726 B b1044 t1043
2727 T t1044 o937 b1043 b4 b1044
2728 B b1045 t1044
2729 T t1045 o b1045 b4
2730 B b1046 t1045
2731 T t1046 o936 b1028 b1046
2732 B b1047 t1046
2733 P p1047 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2734 O o1047 ext_rule p1047
2735 T t1047 o936 b1045 b4
2736 B b1048 t1047
2737 T t1048 o1047 b935 b1048 b4 b4
2738 B b1049 t1048
2739 T t1049 o b1049 b4
2740 B b1050 t1049
2741 P p1050 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2742 O o1050 ext_rule p1050
2743 B b1051 t1016 v_6
2744 T t1051 o711 b1051
2745 S s1051 t620 h h947 h957 h971 h998 h1018 h1024
2746 G s1051 t1051
2747 B b1052 s1051
2748 T t1052 o938 b1052 b944
2749 B b1053 t1052
2750 P p1053 Var v_6
2751 O o1053 var p1053
2752 T t1053 o1053
2753 B b1054 t1053
2754 T t1054 o738 b1017 b1054
2755 B b1055 t1054 v_6
2756 T t1055 o976 b1055
2757 S s1055 t620 h h947 h957 h971 h998 h1018 h1024
2758 G s1055 t1055
2759 B b1056 s1055
2760 T t1056 o938 b1056 b944
2761 B b1057 t1056
2762 T t1057 o973 b1057 b983 b1044
2763 B b1058 t1057
2764 T t1058 o2 b1058
2765 B b1059 t1058
2766 T t1059 o973 b1053 b4 b1059
2767 B b1060 t1059
2768 T t1060 o936 b1060 b4
2769 B b1061 t1060
2770 T t1061 o1050 b935 b1061 b4 b4
2771 B b1062 t1061
2772 T t1062 o b1062 b4
2773 B b1063 t1062
2774 T t1063 o1041 b935 b1047 b1050 b1063
2775 B b1064 t1063
2776 T t230 o b1064 b4
2777 B b230 t230
2778 T t1064 o936 b1038 b4
2779 B b1065 t1064
2780 T t1065 o1050 b935 b1065 b4 b4
2781 B b1066 t1065
2782 T t1066 o b1066 b4
2783 B b1067 t1066
2784 T t233 o1024 b935 b229 b230 b1067
2785 B b233 t233
2786 T t237 o b233 b4
2787 B b237 t237
2788 T t238 o1016 b935 b1024 b237 b4
2789 B b238 t238
2790 T t239 o b238 b4
2791 B b239 t239
2792 T t242 o b1016 b239
2793 B b242 t242
2794 P p1071 String "rwh unfold_fun_set 0 thenT autoT"
2795 O o1071 ext_rule p1071
2796 T t1071 o936 b1010 b4
2797 B b1072 t1071
2798 T t1072 o1071 b935 b1072 b4 b4
2799 B b1073 t1072
2800 T t1073 o b1073 b4
2801 B b1074 t1073
2802 T t243 o992 b935 b218 b242 b1074
2803 B b243 t243
2804 T t251 o b243 b4
2805 B b251 t251
2806 T t256 o b992 b251
2807 B b256 t256
2808 T t1077 o936 b986 b4
2809 B b1078 t1077
2810 T t1078 o1071 b935 b1078 b4 b4
2811 B b1079 t1078
2812 T t1079 o b1079 b4
2813 B b1080 t1079
2814 T t257 o965 b935 b3 b256 b1080
2815 B b257 t257
2816 T t265 o b257 b4
2817 B b265 t265
2818 T t266 o b965 b265
2819 B b266 t266
2820 NSummary!ext_goal ext_goal ext_goal Summary
2821 O o1085 ext_goal
2822 S s1085 t620 h
2823 G s1085 t950
2824 B b1086 s1085
2825 T t1086 o938 b1086 b944
2826 B b1087 t1086
2827 T t1087 o947 b1087 b4 b954
2828 B b1088 t1087
2829 T t1088 o1085 b1088
2830 B b1089 t1088
2831 T t1089 o b1089 b4
2832 B b1090 t1089
2833 T t1090 o963 b935 b1089 b1090 b4
2834 B b1091 t1090
2835 P p1091 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2836 O o1091 ext_rule p1091
2837 H h1091 v t950
2838 S s1091 t620 h h1091
2839 G s1091 t925
2840 B b1092 s1091
2841 T t1092 o938 b1092 b944
2842 B b1093 t1092
2843 T t1093 o937 b1093 b4 b954
2844 B b1094 t1093
2845 T t1094 o1085 b1094
2846 B b1095 t1094
2847 P p1095 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2848 O o1095 ext_rule p1095
2849 P p1096 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2850 O o1096 ext_rule p1096
2851 T t1096 o b1095 b4
2852 B b1096 t1096
2853 H h1096 x t923
2854 H h1097 v_1 t971
2855 H h1098 v_2 t998
2856 H h1099 v_3 t1018
2857 H h1100 v_4 t1024
2858 B b1100 t1016 v_5
2859 T t1100 o711 b1100
2860 S s1100 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2861 G s1100 t1100
2862 B b1101 s1100
2863 T t1101 o b737 b4
2864 B b1102 t1101
2865 T t1102 o b657 b1102
2866 B b1103 t1102
2867 T t1103 o b655 b1103
2868 B b1104 t1103
2869 T t1104 o b675 b1104
2870 B b1105 t1104
2871 T t1105 o b640 b1105
2872 B b1106 t1105
2873 T t1106 o b638 b1106
2874 B b1107 t1106
2875 T t1107 o938 b1101 b1107
2876 B b1108 t1107
2877 T t1108 o738 b1017 b1032
2878 B b1109 t1108 v_5
2879 T t1109 o976 b1109
2880 S s1109 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2881 G s1109 t1109
2882 B b1110 s1109
2883 T t1110 o938 b1110 b1107
2884 B b1111 t1110
2885 S s1111 t620 h h1096 h1091 h1097 h1098 h1099 h1100
2886 G s1111 t925
2887 B b1112 s1111
2888 T t1112 o938 b1112 b1107
2889 B b1113 t1112
2890 S s1113 t620 h h1096 h1091 h1097 h1098 h1099
2891 G s1113 t925
2892 B b1114 s1113
2893 T t1114 o938 b1114 b1107
2894 B b1115 t1114
2895 S s1115 t620 h h1096 h1091 h1097 h1098
2896 G s1115 t925
2897 B b1116 s1115
2898 T t1116 o938 b1116 b1107
2899 B b1117 t1116
2900 S s1117 t620 h h1096 h1091 h1097
2901 G s1117 t925
2902 B b1118 s1117
2903 T t1118 o938 b1118 b1107
2904 B b1119 t1118
2905 S s1119 t620 h h1096 h1091
2906 G s1119 t925
2907 B b1120 s1119
2908 T t1120 o938 b1120 b1107
2909 B b1121 t1120
2910 S s1121 t620 h h1096
2911 G s1121 t925
2912 B b1122 s1121
2913 T t1122 o938 b1122 b1107
2914 B b1123 t1122
2915 T t1123 o937 b1123 b4 b946
2916 B b1124 t1123
2917 T t1124 o2 b1124
2918 B b1125 t1124
2919 T t1125 o937 b1121 b4 b1125
2920 B b1126 t1125
2921 T t1126 o2 b1126
2922 B b1127 t1126
2923 T t1127 o937 b1119 b4 b1127
2924 B b1128 t1127
2925 T t1128 o2 b1128
2926 B b1129 t1128
2927 T t1129 o937 b1117 b4 b1129
2928 B b1130 t1129
2929 T t1130 o2 b1130
2930 B b1131 t1130
2931 T t1131 o937 b1115 b4 b1131
2932 B b1132 t1131
2933 T t1132 o2 b1132
2934 B b1133 t1132
2935 T t1133 o937 b1113 b4 b1133
2936 B b1134 t1133
2937 T t1134 o2 b1134
2938 B b1135 t1134
2939 T t1135 o973 b1111 b983 b1135
2940 B b1136 t1135
2941 T t1136 o2 b1136
2942 B b1137 t1136
2943 T t1137 o973 b1108 b4 b1137
2944 B b1138 t1137
2945 T t1138 o936 b1138 b4
2946 B b1139 t1138
2947 T t1139 o1050 b935 b1139 b4 b4
2948 B b1140 t1139
2949 T t1140 o b1140 b4
2950 B b1141 t1140
2951 T t1141 o1096 b935 b1095 b1096 b1141
2952 B b1142 t1141
2953 T t1142 o b1142 b4
2954 B b1143 t1142
2955 B b1144 t1017 v_4
2956 T t1144 o711 b1144
2957 S s1144 t620 h h1096 h1091 h1097 h1098 h1099
2958 G s1144 t1144
2959 B b1145 s1144
2960 T t1145 o938 b1145 b1107
2961 B b1146 t1145
2962 P p1146 Var v_4
2963 O o1146 var p1146
2964 T t1146 o1146
2965 B b1147 t1146
2966 T t1147 o738 b1147 b1018
2967 B b1148 t1147 v_4
2968 T t1148 o976 b1148
2969 S s1148 t620 h h1096 h1091 h1097 h1098 h1099
2970 G s1148 t1148
2971 B b1149 s1148
2972 T t1149 o938 b1149 b1107
2973 B b1150 t1149
2974 T t1150 o973 b1150 b983 b1133
2975 B b1151 t1150
2976 T t1151 o2 b1151
2977 B b1152 t1151
2978 T t1152 o973 b1146 b4 b1152
2979 B b1153 t1152
2980 T t1153 o936 b1153 b4
2981 B b1154 t1153
2982 T t1154 o1050 b935 b1154 b4 b4
2983 B b1155 t1154
2984 T t1155 o b1155 b4
2985 B b1156 t1155
2986 T t1156 o1024 b935 b1095 b1143 b1156
2987 B b1157 t1156
2988 T t1157 o b1157 b4
2989 B b1158 t1157
2990 T t1158 o1016 b935 b1095 b1158 b4
2991 B b1159 t1158
2992 T t1159 o b1159 b4
2993 B b1160 t1159
2994 S s1160 t620 h h1096 h1091 h1097
2995 G s1160 t994
2996 B b1161 s1160
2997 T t1161 o938 b1161 b1107
2998 B b1162 t1161
2999 T t1162 o966 b1162 b4 b1129
3000 B b1163 t1162
3001 T t1163 o936 b1163 b4
3002 B b1164 t1163
3003 T t1164 o990 b935 b1164 b4 b4
3004 B b1165 t1164
3005 P p1165 String "rwh unfold_fun_prop 0 thenT autoT"
3006 O o1165 ext_rule p1165
3007 T t1165 o738 b966 b977
3008 B b1166 t1165 v_2
3009 T t1166 o976 b1166
3010 S s1166 t620 h h1096 h1091 h1097
3011 G s1166 t1166
3012 B b1167 s1166
3013 T t1167 o938 b1167 b1107
3014 B b1168 t1167
3015 T t1168 o973 b1168 b4 b1129
3016 B b1169 t1168
3017 NCzf_itt_set!set set set Czf_itt_set
3018 O o1169 set
3019 T t1169 o1169
3020 H h1169 s1_1 t1169
3021 H h1170 s2_1 t1169
3022 P p1170 Var s1_1
3023 O o1170 var p1170
3024 T t1170 o1170
3025 B b1170 t1170
3026 P p1171 Var s2_1
3027 O o1171 var p1171
3028 T t1171 o1171
3029 B b1171 t1171
3030 T t1172 o738 b1170 b1171
3031 H h1172 x_1 t1172
3032 T t1173 o738 b966 b1170
3033 H h1173 x_2 t1173
3034 T t1174 o676 b966 b1171
3035 S s1174 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3036 G s1174 t1174
3037 B b1174 s1174
3038 T t1175 o938 b1174 b1107
3039 B b1175 t1175
3040 T t1176 o738 b966 b1171
3041 S s1176 t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3042 G s1176 t1176
3043 B b1176 s1176
3044 T t1177 o938 b1176 b1107
3045 B b1177 t1177
3046 NItt_logic Itt_logic Itt_logic NIL
3047 NItt_logic!implies implies implies Itt_logic
3048 O o1177 implies
3049 B b1178 t1173
3050 B b1179 t1176
3051 T t1179 o1177 b1178 b1179
3052 S s1179 t620 h h1096 h1091 h1097 h1169 h1170 h1172
3053 G s1179 t1179
3054 B b1180 s1179
3055 T t1180 o938 b1180 b1107
3056 B b1181 t1180
3057 B b1182 t1172
3058 B b1183 t1179
3059 T t1183 o1177 b1182 b1183
3060 S s1183 t620 h h1096 h1091 h1097 h1169 h1170
3061 G s1183 t1183
3062 B b1184 s1183
3063 T t1184 o938 b1184 b1107
3064 B b1185 t1184
3065 NItt_logic!all all all Itt_logic
3066 O o1185 all
3067 B b1186 t1169
3068 B b1187 t1183 s2_1
3069 T t1187 o1185 b1186 b1187
3070 S s1187 t620 h h1096 h1091 h1097 h1169
3071 G s1187 t1187
3072 B b1188 s1187
3073 T t1188 o938 b1188 b1107
3074 B b1189 t1188
3075 B b1190 t1187 s1_1
3076 T t1190 o1185 b1186 b1190
3077 S s1190 t620 h h1096 h1091 h1097
3078 G s1190 t1190
3079 B b1191 s1190
3080 T t1191 o938 b1191 b1107
3081 B b1192 t1191
3082 T t1192 o2 b1169
3083 B b1193 t1192
3084 T t1193 o973 b1192 b983 b1193
3085 B b1194 t1193
3086 T t1194 o2 b1194
3087 B b1195 t1194
3088 T t1195 o937 b1189 b983 b1195
3089 B b1196 t1195
3090 T t1196 o2 b1196
3091 B b1197 t1196
3092 T t1197 o937 b1185 b983 b1197
3093 B b1198 t1197
3094 T t1198 o2 b1198
3095 B b1199 t1198
3096 T t1199 o937 b1181 b983 b1199
3097 B b1200 t1199
3098 T t1200 o2 b1200
3099 B b1201 t1200
3100 T t1201 o937 b1177 b983 b1201
3101 B b1202 t1201
3102 T t1202 o2 b1202
3103 B b1203 t1202
3104 T t1203 o937 b1175 b4 b1203
3105 B b1204 t1203
3106 T t1204 o b1204 b4
3107 B b1205 t1204
3108 T t1205 o936 b1169 b1205
3109 B b1206 t1205
3110 P p1206 String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3111 O o1206 ext_rule p1206
3112 T t1206 o936 b1204 b4
3113 B b1207 t1206
3114 T t1207 o1206 b935 b1207 b4 b4
3115 B b1208 t1207
3116 T t1208 o b1208 b4
3117 B b1209 t1208
3118 T t1209 o1165 b935 b1206 b1209 b4
3119 B b1210 t1209
3120 T t1210 o b1210 b4
3121 B b1211 t1210
3122 T t1211 o b1165 b1211
3123 B b1212 t1211
3124 T t1212 o1095 b935 b1095 b1160 b1212
3125 B b1213 t1212
3126 T t1213 o b1213 b4
3127 B b1214 t1213
3128 S s1214 t620 h h1096 h1091
3129 G s1214 t967
3130 B b1215 s1214
3131 T t1215 o938 b1215 b1107
3132 B b1216 t1215
3133 T t1216 o966 b1216 b4 b1127
3134 B b1217 t1216
3135 T t1217 o936 b1217 b4
3136 B b1218 t1217
3137 T t1218 o990 b935 b1218 b4 b4
3138 B b1219 t1218
3139 P p1219 Var v_1
3140 O o1219 var p1219
3141 T t1219 o1219
3142 B b1220 t1219
3143 T t1220 o738 b1220 b949
3144 B b1221 t1220 v_1
3145 T t1221 o976 b1221
3146 S s1221 t620 h h1096 h1091
3147 G s1221 t1221
3148 B b1222 s1221
3149 T t1222 o938 b1222 b1107
3150 B b1223 t1222
3151 T t1223 o973 b1223 b4 b1127
3152 B b1224 t1223
3153 H h1224 s2 t1169
3154 T t1224 o738 b1170 b561
3155 H h1225 x_1 t1224
3156 T t1225 o738 b1170 b949
3157 H h1226 x_2 t1225
3158 T t1226 o676 b561 b949
3159 S s1226 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3160 G s1226 t1226
3161 B b1226 s1226
3162 T t1227 o938 b1226 b1107
3163 B b1227 t1227
3164 T t1228 o738 b561 b949
3165 S s1228 t620 h h1096 h1091 h1169 h1224 h1225 h1226
3166 G s1228 t1228
3167 B b1228 s1228
3168 T t1229 o938 b1228 b1107
3169 B b1229 t1229
3170 B b1230 t1225
3171 B b1231 t1228
3172 T t1231 o1177 b1230 b1231
3173 S s1231 t620 h h1096 h1091 h1169 h1224 h1225
3174 G s1231 t1231
3175 B b1232 s1231
3176 T t1232 o938 b1232 b1107
3177 B b1233 t1232
3178 B b1234 t1224
3179 B b1235 t1231
3180 T t1235 o1177 b1234 b1235
3181 S s1235 t620 h h1096 h1091 h1169 h1224
3182 G s1235 t1235
3183 B b1236 s1235
3184 T t1236 o938 b1236 b1107
3185 B b1237 t1236
3186 B b1238 t1235 s2
3187 T t1238 o1185 b1186 b1238
3188 S s1238 t620 h h1096 h1091 h1169
3189 G s1238 t1238
3190 B b1239 s1238
3191 T t1239 o938 b1239 b1107
3192 B b1240 t1239
3193 B b1241 t1238 s1_1
3194 T t1241 o1185 b1186 b1241
3195 S s1241 t620 h h1096 h1091
3196 G s1241 t1241
3197 B b1242 s1241
3198 T t1242 o938 b1242 b1107
3199 B b1243 t1242
3200 T t1243 o2 b1224
3201 B b1244 t1243
3202 T t1244 o973 b1243 b983 b1244
3203 B b1245 t1244
3204 T t1245 o2 b1245
3205 B b1246 t1245
3206 T t1246 o937 b1240 b983 b1246
3207 B b1247 t1246
3208 T t1247 o2 b1247
3209 B b1248 t1247
3210 T t1248 o937 b1237 b983 b1248
3211 B b1249 t1248
3212 T t1249 o2 b1249
3213 B b1250 t1249
3214 T t1250 o937 b1233 b983 b1250
3215 B b1251 t1250
3216 T t1251 o2 b1251
3217 B b1252 t1251
3218 T t1252 o937 b1229 b983 b1252
3219 B b1253 t1252
3220 T t1253 o2 b1253
3221 B b1254 t1253
3222 T t1254 o937 b1227 b4 b1254
3223 B b1255 t1254
3224 T t1255 o b1255 b4
3225 B b1256 t1255
3226 T t1256 o936 b1224 b1256
3227 B b1257 t1256
3228 P p1257 String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3229 O o1257 ext_rule p1257
3230 T t1257 o936 b1255 b4
3231 B b1258 t1257
3232 T t1258 o1257 b935 b1258 b4 b4
3233 B b1259 t1258
3234 T t1259 o b1259 b4
3235 B b1260 t1259
3236 T t1260 o1165 b935 b1257 b1260 b4
3237 B b1261 t1260
3238 T t1261 o b1261 b4
3239 B b1262 t1261
3240 T t1262 o b1219 b1262
3241 B b1263 t1262
3242 T t1263 o1091 b935 b1095 b1214 b1263
3243 B b1264 t1263
3244 P p1264 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3245 O o1264 ext_rule p1264
3246 H h1264 y_1 t642
3247 T t1264 o620 b695
3248 H h1265 z_1 t1264
3249 T t1265 o676 b562 b695
3250 H h1266 z t1265
3251 T t1266 o676 b948 b949
3252 H h1267 v t1266
3253 T t1267 o676 b561 b674
3254 S s1267 t620 h h1264 h1265 h1266 h1267
3255 G s1267 t1267
3256 B b1267 s1267
3257 T t1268 o938 b1267 b1107
3258 B b1268 t1268
3259 S s1268 t620 h h1264 h1265 h1266 h1267
3260 G s1268 t925
3261 B b1269 s1268
3262 T t1269 o938 b1269 b1107
3263 B b1270 t1269
3264 NItt_logic!and and and Itt_logic
3265 O o1270 and
3266 B b1271 t642
3267 B b1272 t1264
3268 T t1272 o1270 b1271 b1272
3269 H h1272 y t1272
3270 S s1272 t620 h h1272 h1266 h1267
3271 G s1272 t925
3272 B b1273 s1272
3273 T t1273 o938 b1273 b1107
3274 B b1274 t1273
3275 B b1275 t1272
3276 B b1276 t1265
3277 T t1276 o1270 b1275 b1276
3278 H h1276 x t1276
3279 S s1276 t620 h h1276 h1267
3280 G s1276 t925
3281 B b1277 s1276
3282 T t1277 o938 b1277 b1107
3283 B b1278 t1277
3284 S s1278 t620 h h1276
3285 G s1278 t925
3286 B b1279 s1278
3287 T t1279 o938 b1279 b1107
3288 B b1280 t1279
3289 T t1280 o937 b1280 b4 b1125
3290 B b1281 t1280
3291 T t1281 o2 b1281
3292 B b1282 t1281
3293 T t1282 o937 b1278 b4 b1282
3294 B b1283 t1282
3295 T t1283 o2 b1283
3296 B b1284 t1283
3297 T t1284 o937 b1274 b4 b1284
3298 B b1285 t1284
3299 T t1285 o2 b1285
3300 B b1286 t1285
3301 T t1286 o937 b1270 b983 b1286
3302 B b1287 t1286
3303 T t1287 o2 b1287
3304 B b1288 t1287
3305 T t1288 o937 b1268 b4 b1288
3306 B b1289 t1288
3307 T t1289 o676 b966 b949
3308 H h1289 v_1 t1289
3309 S s1289 t620 h h1264 h1265 h1266 h1267 h1289
3310 G s1289 t1267
3311 B b1290 s1289
3312 T t1290 o938 b1290 b1107
3313 B b1291 t1290
3314 T t1291 o2 b1289
3315 B b1292 t1291
3316 T t1292 o937 b1291 b4 b1292
3317 B b1293 t1292
3318 T t268 o b1293 b4
3319 B b268 t268
3320 T t269 o936 b1289 b268
3321 B b269 t269
3322 B b1294 t949 v_1
3323 T t1294 o711 b1294
3324 S s1294 t620 h h1264 h1265 h1266 h1267
3325 G s1294 t1294
3326 B b1295 s1294
3327 T t1295 o938 b1295 b1107
3328 B b1296 t1295
3329 T t1296 o676 b1220 b949
3330 B b1297 t1296 v_1
3331 T t1297 o976 b1297
3332 S s1297 t620 h h1264 h1265 h1266 h1267
3333 G s1297 t1297
3334 B b1298 s1297
3335 T t1298 o938 b1298 b1107
3336 B b1299 t1298
3337 T t1299 o973 b1299 b983 b1292
3338 B b1300 t1299
3339 T t1300 o2 b1300
3340 B b1301 t1300
3341 T t1301 o973 b1296 b4 b1301
3342 B b1302 t1301
3343 P p1305 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3344 O o1305 ext_rule p1305
3345 T t1305 o676 b966 b993
3346 H h1305 v_2 t1305
3347 S s1305 t620 h h1264 h1265 h1266 h1267 h1289 h1305
3348 G s1305 t1267
3349 B b1306 s1305
3350 T t1306 o938 b1306 b1107
3351 B b1307 t1306
3352 T t1307 o2 b1293
3353 B b1308 t1307
3354 T t1308 o937 b1307 b4 b1308
3355 B b1309 t1308
3356 T t270 o b1309 b4
3357 B b270 t270
3358 T t273 o936 b1293 b270
3359 B b273 t273
3360 B b1310 t966 v_2
3361 T t1310 o711 b1310
3362 S s1310 t620 h h1264 h1265 h1266 h1267 h1289
3363 G s1310 t1310
3364 B b1311 s1310
3365 T t1311 o938 b1311 b1107
3366 B b1312 t1311
3367 T t1312 o676 b966 b977
3368 B b1313 t1312 v_2
3369 T t1313 o976 b1313
3370 S s1313 t620 h h1264 h1265 h1266 h1267 h1289
3371 G s1313 t1313
3372 B b1314 s1313
3373 T t1314 o938 b1314 b1107
3374 B b1315 t1314
3375 T t1315 o973 b1315 b983 b1308
3376 B b1316 t1315
3377 T t1316 o2 b1316
3378 B b1317 t1316
3379 T t1317 o973 b1312 b4 b1317
3380 B b1318 t1317
3381 P p1321 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3382 O o1321 ext_rule p1321
3383 T t1321 o676 b1017 b1018
3384 H h1321 v_3 t1321
3385 S s1321 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3386 G s1321 t1267
3387 B b1322 s1321
3388 T t1322 o938 b1322 b1107
3389 B b1323 t1322
3390 T t1323 o2 b1309
3391 B b1324 t1323
3392 T t1324 o937 b1323 b4 b1324
3393 B b1325 t1324
3394 T t1325 o b1325 b4
3395 B b1326 t1325
3396 T t1326 o936 b1309 b1326
3397 B b1327 t1326
3398 P p1327 String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"
3399 O o1327 ext_rule p1327
3400 T t1327 o676 b561 b1018
3401 H h1327 v_4 t1327
3402 S s1327 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1327
3403 G s1327 t1267
3404 B b1328 s1327
3405 T t1328 o938 b1328 b1107
3406 B b1329 t1328
3407 T t1329 o2 b1325
3408 B b1330 t1329
3409 T t1330 o937 b1329 b4 b1330
3410 B b1331 t1330
3411 T t274 o b1331 b4
3412 B b274 t274
3413 T t289 o936 b1325 b274
3414 B b289 t289
3415 S s1331 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3416 G s1331 t1144
3417 B b1332 s1331
3418 T t1332 o938 b1332 b1107
3419 B b1333 t1332
3420 T t1333 o676 b1147 b1018
3421 B b1334 t1333 v_4
3422 T t1334 o976 b1334
3423 S s1334 t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3424 G s1334 t1334
3425 B b1335 s1334
3426 T t1335 o938 b1335 b1107
3427 B b1336 t1335
3428 T t1336 o973 b1336 b983 b1330
3429 B b1337 t1336
3430 T t1337 o2 b1337
3431 B b1338 t1337
3432 T t1338 o973 b1333 b4 b1338
3433 B b1339 t1338
3434 P p1342 String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3435 O o1342 ext_rule p1342
3436 T t1342 o936 b1331 b4
3437 B b1343 t1342
3438 T t1343 o1342 b935 b1343 b4 b4
3439 B b1344 t1343
3440 T t290 o b1344 b4
3441 B b290 t290
3442 T t292 o936 b1339 b4
3443 B b292 t292
3444 T t300 o1071 b935 b292 b4 b4
3445 B b300 t300
3446 T t301 o b300 b4
3447 B b301 t301
3448 T t304 o1327 b935 b289 b290 b301
3449 B b304 t304
3450 T t309 o b304 b4
3451 B b309 t309
3452 T t310 o1321 b935 b1327 b309 b4
3453 B b310 t310
3454 T t315 o b310 b4
3455 B b315 t315
3456 H h1344 s1 t1169
3457 T t1344 o738 b560 b561
3458 H h1345 x t1344
3459 B b1347 t1344
3460 T t1374 o936 b1318 b4
3461 B b1375 t1374
3462 T t1375 o1071 b935 b1375 b4 b4
3463 B b1376 t1375
3464 P p1378 String "eqSetSymT thenT autoT"
3465 O o1378 ext_rule p1378
3466 T t1378 o676 b949 b993
3467 S s1378 t620 h h1264 h1265 h1266 h1267 h1289
3468 G s1378 t1378
3469 B b1379 s1378
3470 T t1379 o938 b1379 b1107
3471 B b1380 t1379
3472 S s1380 t620 h h1264 h1265 h1266 h1267 h1289
3473 G s1380 t994
3474 B b1381 s1380
3475 T t1381 o938 b1381 b1107
3476 B b1382 t1381
3477 T t1382 o966 b1382 b983 b1308
3478 B b1383 t1382
3479 T t1383 o2 b1383
3480 B b1384 t1383
3481 T t1384 o966 b1380 b4 b1384
3482 B b1385 t1384
3483 T t1385 o676 b993 b949
3484 S s1385 t620 h h1264 h1265 h1266 h1267 h1289
3485 G s1385 t1385
3486 B b1386 s1385
3487 T t1386 o938 b1386 b1107
3488 B b1387 t1386
3489 T t1387 o2 b1385
3490 B b1388 t1387
3491 T t1388 o966 b1387 b4 b1388
3492 B b1389 t1388
3493 T t1389 o b1389 b4
3494 B b1390 t1389
3495 T t1390 o936 b1385 b1390
3496 B b1391 t1390
3497 T t1391 o1085 b1389
3498 B b1392 t1391
3499 T t1392 o b1392 b4
3500 B b1393 t1392
3501 T t1393 o1378 b935 b1391 b1393 b4
3502 B b1394 t1393
3503 T t1394 o b1394 b4
3504 B b1395 t1394
3505 T t316 o b1376 b1395
3506 B b316 t316
3507 T t318 o1305 b935 b273 b315 b316
3508 B b318 t318
3509 T t320 o b318 b4
3510 B b320 t320
3511 T t1396 o936 b1302 b4
3512 B b1397 t1396
3513 T t1397 o1071 b935 b1397 b4 b4
3514 B b1398 t1397
3515 T t1400 o676 b948 b966
3516 S s1400 t620 h h1264 h1265 h1266 h1267
3517 G s1400 t1400
3518 B b1401 s1400
3519 T t1401 o938 b1401 b1107
3520 B b1402 t1401
3521 S s1402 t620 h h1264 h1265 h1266 h1267
3522 G s1402 t967
3523 B b1403 s1402
3524 T t1403 o938 b1403 b1107
3525 B b1404 t1403
3526 T t1404 o966 b1404 b983 b1292
3527 B b1405 t1404
3528 T t1405 o2 b1405
3529 B b1406 t1405
3530 T t1406 o966 b1402 b4 b1406
3531 B b1407 t1406
3532 T t1407 o676 b966 b948
3533 S s1407 t620 h h1264 h1265 h1266 h1267
3534 G s1407 t1407
3535 B b1408 s1407
3536 T t1408 o938 b1408 b1107
3537 B b1409 t1408
3538 T t1409 o2 b1407
3539 B b1410 t1409
3540 T t1410 o966 b1409 b4 b1410
3541 B b1411 t1410
3542 T t1411 o b1411 b4
3543 B b1412 t1411
3544 T t1412 o936 b1407 b1412
3545 B b1413 t1412
3546 T t1413 o1085 b1411
3547 B b1414 t1413
3548 T t1414 o b1414 b4
3549 B b1415 t1414
3550 T t1415 o1378 b935 b1413 b1415 b4
3551 B b1416 t1415
3552 T t1416 o b1416 b4
3553 B b1417 t1416
3554 T t327 o b1398 b1417
3555 B b327 t327
3556 T t331 o1264 b935 b269 b320 b327
3557 B b331 t331
3558 T t332 o b331 b4
3559 B b332 t332
3560 T t335 o b1264 b332
3561 B b335 t335
3562 T t339 o b1091 b335
3563 B b339 t339
3564 T t340 o934 b935 b963 b266 b339
3565 B b340 t340
3566 T t359 o933 b340
3567 B b359 t359
3568 P p2029 Number 4889
3569 P p2030 Number 4897
3570 O o2030 resource_defs p2029 p2030 p264
3571 P p2031 Number 4895
3572 O o2031 uid p2031 p2030
3573 T t2039 o2031 b626
3574 B b2040 t2039
3575 T t2040 o b2040 b4
3576 B b2041 t2040
3577 T t2041 o2030 b2041
3578 B b2042 t2041
3579 T t2047 o b2042 b4
3580 B b2048 t2047
3581 T t2048 o919 b922 b933 b359 b2048
3582 B b2049 t2048
3583 T t2052 o2028 b2049
3584 B b2053 t2052
3585 P p2053 Number 5337
3586 P p2054 Number 5763
3587 O o2054 location p2053 p2054
3588 P p1432 String cancel2
3589 O o1432 rule p1432
3590 T t1432 o920 b674
3591 B b1432 t1432
3592 T t1433 o b1432 b4
3593 B b1433 t1433
3594 T t1434 o b617 b1433
3595 B b1434 t1434
3596 T t1435 o738 b695 b696
3597 S s1435 t620 h
3598 G s1435 t1435
3599 B b1435 s1435
3600 T t1436 o618 b1435
3601 B b1436 t1436
3602 S s1436 t620 h
3603 G s1436 t1344
3604 B b1437 s1436
3605 T t1437 o618 b1437
3606 B b1438 t1437
3607 T t1438 o635 b1436 b1438
3608 B b1439 t1438
3609 T t1439 o635 b738 b1439
3610 B b1440 t1439
3611 T t1440 o635 b658 b1440
3612 B b1441 t1440
3613 T t1441 o635 b656 b1441
3614 B b1442 t1441
3615 T t1442 o635 b676 b1442
3616 B b1443 t1442
3617 T t1443 o635 b641 b1443
3618 B b1444 t1443
3619 T t1444 o635 b639 b1444
3620 B b1445 t1444
3621 P p1445 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"
3622 O o1445 ext_rule p1445
3623 T t1445 o b1435 b4
3624 B b1446 t1445
3625 T t1446 o b737 b1446
3626 B b1447 t1446
3627 T t1447 o b657 b1447
3628 B b1448 t1447
3629 T t1448 o b655 b1448
3630 B b1449 t1448
3631 T t1449 o b675 b1449
3632 B b1450 t1449
3633 T t1450 o b640 b1450
3634 B b1451 t1450
3635 T t1451 o b638 b1451
3636 B b1452 t1451
3637 T t1452 o938 b1437 b1452
3638 B b1453 t1452
3639 T t1453 o937 b1453 b4 b946
3640 B b1454 t1453
3641 H h1454 v t1435
3642 T t1454 o572 b674
3643 B b1455 t1454
3644 T t1455 o559 b695 b1455
3645 B b1456 t1455
3646 T t1456 o559 b696 b1455
3647 B b1457 t1456
3648 T t1457 o738 b1456 b1457
3649 S s1457 t620 h h1454
3650 G s1457 t1457
3651 B b1458 s1457
3652 T t1458 o938 b1458 b1452
3653 B b1459 t1458
3654 S s1459 t620 h h1454
3655 G s1459 t1344
3656 B b1460 s1459
3657 T t1460 o938 b1460 b1452
3658 B b1461 t1460
3659 T t1461 o2 b1454
3660 B b1462 t1461
3661 T t1462 o937 b1461 b4 b1462
3662 B b1463 t1462
3663 T t1463 o2 b1463
3664 B b1464 t1463
3665 T t1464 o947 b1459 b4 b1464
3666 B b1465 t1464
3667 H h1465 v_1 t1457
3668 S s1465 t620 h h1454 h1465
3669 G s1465 t1344
3670 B b1466 s1465
3671 T t1466 o938 b1466 b1452
3672 B b1467 t1466
3673 T t1467 o937 b1467 b4 b1464
3674 B b1468 t1467
3675 T t1468 o b1468 b4
3676 B b1469 t1468
3677 T t1469 o b1465 b1469
3678 B b1470 t1469
3679 T t1470 o936 b1454 b1470
3680 B b1471 t1470
3681 T t1471 o936 b1465 b4
3682 B b1472 t1471
3683 T t1472 o963 b935 b1472 b4 b4
3684 B b1473 t1472
3685 P p1473 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
3686 O o1473 ext_rule p1473
3687 T t1473 o559 b674 b1455
3688 B b1474 t1473
3689 T t1474 o559 b560 b1474
3690 B b1475 t1474
3691 T t1475 o738 b1475 b1457
3692 H h1475 v_2 t1475
3693 S s1475 t620 h h1454 h1465 h1475
3694 G s1475 t1344
3695 B b1476 s1475
3696 T t1476 o938 b1476 b1452
3697 B b1477 t1476
3698 T t1477 o2 b1468
3699 B b1478 t1477
3700 T t1478 o937 b1477 b4 b1478
3701 B b1479 t1478
3702 T t391 o b1479 b4
3703 B b391 t391
3704 T t392 o936 b1468 b391
3705 B b392 t392
3706 B b1480 t1456 v_2
3707 T t1480 o711 b1480
3708 S s1480 t620 h h1454 h1465
3709 G s1480 t1480
3710 B b1481 s1480
3711 T t1481 o938 b1481 b1452
3712 B b1482 t1481
3713 T t1482 o738 b977 b1457
3714 B b1483 t1482 v_2
3715 T t1483 o976 b1483
3716 S s1483 t620 h h1454 h1465
3717 G s1483 t1483
3718 B b1484 s1483
3719 T t1484 o938 b1484 b1452
3720 B b1485 t1484
3721 T t1485 o973 b1485 b983 b1478
3722 B b1486 t1485
3723 T t1486 o2 b1486
3724 B b1487 t1486
3725 T t1487 o973 b1482 b4 b1487
3726 B b1488 t1487
3727 P p1491 String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
3728 O o1491 ext_rule p1491
3729 T t1491 o559 b561 b1474
3730 B b1492 t1491
3731 T t1492 o738 b1475 b1492
3732 H h1492 v_3 t1492
3733 S s1492 t620 h h1454 h1465 h1475 h1492
3734 G s1492 t1344
3735 B b1493 s1492
3736 T t1493 o938 b1493 b1452
3737 B b1494 t1493
3738 T t1494 o2 b1479
3739 B b1495 t1494
3740 T t1495 o937 b1494 b4 b1495
3741 B b1496 t1495
3742 T t393 o b1496 b4
3743 B b393 t393
3744 T t399 o936 b1479 b393
3745 B b399 t399
3746 B b1497 t1474 v_3
3747 T t1497 o711 b1497
3748 S s1497 t620 h h1454 h1465 h1475
3749 G s1497 t1497
3750 B b1498 s1497
3751 T t1498 o938 b1498 b1452
3752 B b1499 t1498
3753 T t1499 o738 b1475 b1004
3754 B b1500 t1499 v_3
3755 T t1500 o976 b1500
3756 S s1500 t620 h h1454 h1465 h1475
3757 G s1500 t1500
3758 B b1501 s1500
3759 T t1501 o938 b1501 b1452
3760 B b1502 t1501
3761 T t1502 o973 b1502 b983 b1495
3762 B b1503 t1502
3763 T t1503 o2 b1503
3764 B b1504 t1503
3765 T t1504 o973 b1499 b4 b1504
3766 B b1505 t1504
3767 P p1508 String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
3768 O o1508 ext_rule p1508
3769 T t1508 o559 b560 b567
3770 B b1509 t1508
3771 T t1509 o559 b561 b567
3772 B b1510 t1509
3773 T t1510 o738 b1509 b1510
3774 H h1510 v_4 t1510
3775 S s1510 t620 h h1454 h1465 h1475 h1492 h1510
3776 G s1510 t1344
3777 B b1511 s1510
3778 T t1511 o938 b1511 b1452
3779 B b1512 t1511
3780 T t1512 o2 b1496
3781 B b1513 t1512
3782 T t1513 o937 b1512 b4 b1513
3783 B b1514 t1513
3784 T t1514 o b1514 b4
3785 B b1515 t1514
3786 T t1515 o936 b1496 b1515
3787 B b1516 t1515
3788 P p1516 String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
3789 O o1516 ext_rule p1516
3790 T t1516 o738 b560 b1510
3791 H h1516 v_5 t1516
3792 S s1516 t620 h h1454 h1465 h1475 h1492 h1510 h1516
3793 G s1516 t1344
3794 B b1517 s1516
3795 T t1517 o938 b1517 b1452
3796 B b1518 t1517
3797 T t1518 o2 b1514
3798 B b1519 t1518
3799 T t1519 o937 b1518 b4 b1519
3800 B b1520 t1519
3801 T t400 o b1520 b4
3802 B b400 t400
3803 T t406 o936 b1514 b400
3804 B b406 t406
3805 B b1521 t1509 v_5
3806 T t1521 o711 b1521
3807 S s1521 t620 h h1454 h1465 h1475 h1492 h1510
3808 G s1521 t1521
3809 B b1522 s1521
3810 T t1522 o938 b1522 b1452
3811 B b1523 t1522
3812 T t1523 o738 b1032 b1510
3813 B b1524 t1523 v_5
3814 T t1524 o976 b1524
3815 S s1524 t620 h h1454 h1465 h1475 h1492 h1510
3816 G s1524 t1524
3817 B b1525 s1524
3818 T t1525 o938 b1525 b1452
3819 B b1526 t1525
3820 T t1526 o973 b1526 b983 b1519
3821 B b1527 t1526
3822 T t1527 o2 b1527
3823 B b1528 t1527
3824 T t1528 o973 b1523 b4 b1528
3825 B b1529 t1528
3826 P p1532 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3827 O o1532 ext_rule p1532
3828 T t1532 o936 b1520 b4
3829 B b1533 t1532
3830 T t1533 o1532 b935 b1533 b4 b4
3831 B b1534 t1533
3832 T t407 o b1534 b4
3833 B b407 t407
3834 T t1534 o936 b1529 b4
3835 B b1535 t1534
3836 T t1535 o1050 b935 b1535 b4 b4
3837 B b1536 t1535
3838 T t1536 o b1536 b4
3839 B b1537 t1536
3840 T t416 o1516 b935 b406 b407 b1537
3841 B b416 t416
3842 T t417 o b416 b4
3843 B b417 t417
3844 T t425 o1508 b935 b1516 b417 b4
3845 B b425 t425
3846 T t426 o b425 b4
3847 B b426 t426
3848 T t1541 o936 b1505 b4
3849 B b1542 t1541
3850 T t1542 o1050 b935 b1542 b4 b4
3851 B b1543 t1542
3852 T t1543 o b1543 b4
3853 B b1544 t1543
3854 T t434 o1491 b935 b399 b426 b1544
3855 B b434 t434
3856 T t435 o b434 b4
3857 B b435 t435
3858 T t1546 o936 b1488 b4
3859 B b1547 t1546
3860 T t1547 o1050 b935 b1547 b4 b4
3861 B b1548 t1547
3862 T t1548 o b1548 b4
3863 B b1549 t1548
3864 T t443 o1473 b935 b392 b435 b1549
3865 B b443 t443
3866 T t444 o b443 b4
3867 B b444 t444
3868 T t452 o b1473 b444
3869 B b452 t452
3870 S s1553 t620 h
3871 G s1553 t1457
3872 B b1554 s1553
3873 T t1554 o938 b1554 b1452
3874 B b1555 t1554
3875 T t1555 o947 b1555 b4 b1462
3876 B b1556 t1555
3877 T t1556 o1085 b1556
3878 B b1557 t1556
3879 T t1557 o b1557 b4
3880 B b1558 t1557
3881 T t1558 o963 b935 b1557 b1558 b4
3882 B b1559 t1558
3883 H h1559 v t1457
3884 S s1559 t620 h h1559
3885 G s1559 t1344
3886 B b1560 s1559
3887 T t1560 o938 b1560 b1452
3888 B b1561 t1560
3889 T t1561 o937 b1561 b4 b1462
3890 B b1562 t1561
3891 T t1562 o1085 b1562
3892 B b1563 t1562
3893 T t1563 o b1563 b4
3894 B b1564 t1563
3895 T t1564 o1532 b935 b1563 b1564 b4
3896 B b1565 t1564
3897 T t1565 o b1565 b4
3898 B b1566 t1565
3899 H h1566 x t1435
3900 H h1567 v_1 t1475
3901 H h1568 v_2 t1492
3902 H h1569 v_3 t1510
3903 B b1569 t1509 v_4
3904 T t1569 o711 b1569
3905 S s1569 t620 h h1566 h1559 h1567 h1568 h1569
3906 G s1569 t1569
3907 B b1570 s1569
3908 T t1570 o938 b1570 b1107
3909 B b1571 t1570
3910 T t1571 o738 b1147 b1510
3911 B b1572 t1571 v_4
3912 T t1572 o976 b1572
3913 S s1572 t620 h h1566 h1559 h1567 h1568 h1569
3914 G s1572 t1572
3915 B b1573 s1572
3916 T t1573 o938 b1573 b1107
3917 B b1574 t1573
3918 S s1574 t620 h h1566 h1559 h1567 h1568 h1569
3919 G s1574 t1344
3920 B b1575 s1574
3921 T t1575 o938 b1575 b1107
3922 B b1576 t1575
3923 S s1576 t620 h h1566 h1559 h1567 h1568
3924 G s1576 t1344
3925 B b1577 s1576
3926 T t1577 o938 b1577 b1107
3927 B b1578 t1577
3928 S s1578 t620 h h1566 h1559 h1567
3929 G s1578 t1344
3930 B b1579 s1578
3931 T t1579 o938 b1579 b1107
3932 B b1580 t1579
3933 S s1580 t620 h h1566 h1559
3934 G s1580 t1344
3935 B b1581 s1580
3936 T t1581 o938 b1581 b1107
3937 B b1582 t1581
3938 S s1582 t620 h h1566
3939 G s1582 t1344
3940 B b1583 s1582
3941 T t1583 o938 b1583 b1107
3942 B b1584 t1583
3943 T t1584 o937 b1584 b4 b946
3944 B b1585 t1584
3945 T t1585 o2 b1585
3946 B b1586 t1585
3947 T t1586 o937 b1582 b4 b1586
3948 B b1587 t1586
3949 T t1587 o2 b1587
3950 B b1588 t1587
3951 T t1588 o937 b1580 b4 b1588
3952 B b1589 t1588
3953 T t1589 o2 b1589
3954 B b1590 t1589
3955 T t1590 o937 b1578 b4 b1590
3956 B b1591 t1590
3957 T t1591 o2 b1591
3958 B b1592 t1591
3959 T t1592 o937 b1576 b4 b1592
3960 B b1593 t1592
3961 T t1593 o2 b1593
3962 B b1594 t1593
3963 T t1594 o973 b1574 b983 b1594
3964 B b1595 t1594
3965 T t1595 o2 b1595
3966 B b1596 t1595
3967 T t1596 o973 b1571 b4 b1596
3968 B b1597 t1596
3969 T t1597 o936 b1597 b4
3970 B b1598 t1597
3971 T t1598 o1050 b935 b1598 b4 b4
3972 B b1599 t1598
3973 T t1599 o b1599 b4
3974 B b1600 t1599
3975 T t1600 o1516 b935 b1563 b1566 b1600
3976 B b1601 t1600
3977 T t1601 o b1601 b4
3978 B b1602 t1601
3979 T t1602 o1508 b935 b1563 b1602 b4
3980 B b1603 t1602
3981 T t1603 o b1603 b4
3982 B b1604 t1603
3983 P p1604 String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
3984 O o1604 ext_rule p1604
3985 B b1605 t1474 v_2
3986 T t1605 o711 b1605
3987 S s1605 t620 h h1566 h1559 h1567
3988 G s1605 t1605
3989 B b1606 s1605
3990 T t1606 o938 b1606 b1107
3991 B b1607 t1606
3992 T t1607 o738 b1475 b977
3993 B b1608 t1607 v_2
3994 T t1608 o976 b1608
3995 S s1608 t620 h h1566 h1559 h1567
3996 G s1608 t1608
3997 B b1609 s1608
3998 T t1609 o938 b1609 b1107
3999 B b1610 t1609
4000 T t1610 o973 b1610 b983 b1590
4001 B b1611 t1610
4002 T t1611 o2 b1611
4003 B b1612 t1611
4004 T t1612 o973 b1607 b4 b1612
4005 B b1613 t1612
4006 T t1613 o936 b1613 b4
4007 B b1614 t1613
4008 T t1614 o1604 b935 b1614 b4 b4
4009 B b1615 t1614
4010 T t1615 o b1615 b4
4011 B b1616 t1615
4012 T t1616 o1491 b935 b1563 b1604 b1616
4013 B b1617 t1616
4014 T t1617 o b1617 b4
4015 B b1618 t1617
4016 B b1619 t1456 v_1
4017 T t1619 o711 b1619
4018 S s1619 t620 h h1566 h1559
4019 G s1619 t1619
4020 B b1620 s1619
4021 T t1620 o938 b1620 b1107
4022 B b1621 t1620
4023 T t1621 o738 b1220 b1457
4024 B b1622 t1621 v_1
4025 T t1622 o976 b1622
4026 S s1622 t620 h h1566 h1559
4027 G s1622 t1622
4028 B b1623 s1622
4029 T t1623 o938 b1623 b1107
4030 B b1624 t1623
4031 T t1624 o973 b1624 b983 b1588
4032 B b1625 t1624
4033 T t1625 o2 b1625
4034 B b1626 t1625
4035 T t1626 o973 b1621 b4 b1626
4036 B b1627 t1626
4037 T t1627 o936 b1627 b4
4038 B b1628 t1627
4039 T t1628 o1604 b935 b1628 b4 b4
4040 B b1629 t1628
4041 T t1629 o b1629 b4
4042 B b1630 t1629
4043 T t1630 o1473 b935 b1563 b1618 b1630
4044 B b1631 t1630
4045 T t1631 o b1631 b4
4046 B b1632 t1631
4047 T t1632 o b1559 b1632
4048 B b1633 t1632
4049 T t453 o1445 b935 b1471 b452 b1633
4050 B b453 t453
4051 T t461 o933 b453
4052 B b461 t461
4053 P p2055 Number 5360
4054 P p2056 Number 5368
4055 O o2056 resource_defs p2055 p2056 p264
4056 P p2057 Number 5366
4057 O o2057 uid p2057 p2056
4058 T t2057 o2057 b626
4059 B b2057 t2057
4060 T t2064 o b2057 b4
4061 B b2065 t2064
4062 T t2073 o2056 b2065
4063 B b2121 t2073
4064 T t2121 o b2121 b4
4065 B b2122 t2121
4066 T t2125 o1432 b1434 b1445 b461 b2122
4067 B b2126 t2125
4068 T t2126 o2054 b2126
4069 B b2127 t2126
4070 P p2127 Number 5765
4071 P p2128 Number 5834
4072 O o2128 location p2127 p2128
4073 O o2129 str_let p2127 p2128
4074 P p2129 Number 5769
4075 O o2130 patt_var p2129 p2128
4076 O o2131 patt_done p2127 p2128
4077 T t2131 o2131
4078 B b2131 t2131 groupCancelLeftT
4079 T t2132 o2130 b2131
4080 B b2132 t2132
4081 O o2132 fun p2129 p2128
4082 O o2133 patt_if p2129 p2128
4083 P p2136 Number 5786
4084 P p2137 Number 5787
4085 O o2137 patt_var p2136 p2137
4086 O o2138 patt_body p2129 p2128
4087 P p2138 Number 5788
4088 P p2139 Number 5789
4089 O o2139 patt_var p2138 p2139
4090 P p2144 Number 5795
4091 O o2144 apply p2144 p2128
4092 P p2145 Number 5832
4093 O o2145 apply p2144 p2145
4094 P p2146 Number 5830
4095 O o2146 apply p2144 p2146
4096 P p2147 Number 5802
4097 O o2147 lid p2144 p2147
4098 P p1635 Number 5861
4099 P p1637 Number 5867
4100 O o1656 lid p919
4101 T t1656 o1656
4102 B b1656 t1656
4103 T t2188 o2147 b1656
4104 B b2214 t2188
4105 P p2214 Number 5804
4106 P p2215 Number 5829
4107 O o2215 apply p2214 p2215
4108 P p2217 Number 5827
4109 O o2217 proj p2214 p2217
4110 O o2218 uid p2214 p2217
4111 T t2221 o2218 b836
4112 B b2232 t2221
4113 P p2232 Number 5813
4114 O o2232 lid p2232 p2217
4115 T t2232 o2232 b838
4116 B b2233 t2232
4117 T t2233 o2217 b2232 b2233
4118 B b2234 t2233
4119 P p2235 Number 5828
4120 O o2235 lid p2235 p2215
4121 T t2242 o2235 b841
4122 B b2261 t2242
4123 T t2261 o2215 b2234 b2261
4124 B b2262 t2261
4125 T t2265 o2146 b2214 b2262
4126 B b2266 t2265
4127 P p2266 Number 5831
4128 O o2266 lid p2266 p2145
4129 P p1666 Var t
4130 O o1666 var p1666
4131 T t1666 o1666
4132 B b1666 t1666
4133 T t2269 o2266 b1666
4134 B b2270 t2269
4135 T t2270 o2145 b2266 b2270
4136 B b2271 t2270
4137 P p2271 Number 5833
4138 O o2271 lid p2271 p2128
4139 T t2274 o2271 b841
4140 B b2275 t2274
4141 T t2275 o2144 b2271 b2275
4142 B b2276 t2275
4143 T t2276 o2138 b2276
4144 B b2277 t2276 p
4145 T t2277 o2139 b2277
4146 B b2278 t2277
4147 T t2278 o2133 b2278
4148 B b2279 t2278
4149 T t2279 o2132 b2279
4150 B b2280 t2279
4151 T t2280 o2138 b2280
4152 B b2281 t2280 t
4153 T t2281 o2137 b2281
4154 B b2286 t2281
4155 T t2286 o2133 b2286
4156 B b2287 t2286
4157 T t2287 o2132 b2287
4158 B b2288 t2287
4159 T t2288 o2129 b2132 b2288
4160 B b2324 t2288
4161 T t2324 o b2324 b4
4162 B b2325 t2324
4163 T t2325 o2129 b2325
4164 B b2326 t2325
4165 T t2327 o392 b2326
4166 B b2328 t2327
4167 T t2328 o2128 b2328
4168 B b2329 t2328
4169 P p2329 Number 5836
4170 P p2330 Number 5906
4171 O o2330 location p2329 p2330
4172 O o2331 str_let p2329 p2330
4173 P p2331 Number 5840
4174 O o2332 patt_var p2331 p2330
4175 O o2333 patt_done p2329 p2330
4176 T t2333 o2333
4177 B b2333 t2333 groupCancelRightT
4178 T t2334 o2332 b2333
4179 B b2334 t2334
4180 O o2334 fun p2331 p2330
4181 O o2335 patt_if p2331 p2330
4182 P p2335 Number 5858
4183 P p2336 Number 5859
4184 O o2336 patt_var p2335 p2336
4185 O o2337 patt_body p2331 p2330
4186 P p2337 Number 5860
4187 O o2338 patt_var p2337 p1635
4188 O o2340 apply p1637 p2330
4189 P p2340 Number 5904
4190 O o2341 apply p1637 p2340
4191 P p2341 Number 5902
4192 O o2342 apply p1637 p2341
4193 P p2342 Number 5874
4194 O o2343 lid p1637 p2342
4195 O o1697 lid p1432
4196 T t1697 o1697
4197 B b1697 t1697
4198 T t2348 o2343 b1697
4199 B b2349 t2348
4200 P p2349 Number 5876
4201 P p2350 Number 5901
4202 O o2350 apply p2349 p2350
4203 P p2351 Number 5899
4204 O o2351 proj p2349 p2351
4205 O o2352 uid p2349 p2351
4206 T t2352 o2352 b836
4207 B b2352 t2352
4208 P p2352 Number 5885
4209 O o2353 lid p2352 p2351
4210 T t2353 o2353 b838
4211 B b2353 t2353
4212 T t2354 o2351 b2352 b2353
4213 B b2354 t2354
4214 P p2354 Number 5900
4215 O o2354 lid p2354 p2350
4216 T t2382 o2354 b841
4217 B b2481 t2382
4218 T t2481 o2350 b2354 b2481
4219 B b2482 t2481
4220 T t2482 o2342 b2349 b2482
4221 B b2483 t2482
4222 P p2483 Number 5903
4223 O o2483 lid p2483 p2340
4224 T t2483 o2483 b1666
4225 B b2484 t2483
4226 T t2484 o2341 b2483 b2484
4227 B b2485 t2484
4228 P p2485 Number 5905
4229 O o2485 lid p2485 p2330
4230 T t2485 o2485 b841
4231 B b2486 t2485
4232 T t2486 o2340 b2485 b2486
4233 B b2487 t2486
4234 T t2487 o2337 b2487
4235 B b2488 t2487 p
4236 T t2488 o2338 b2488
4237 B b2489 t2488
4238 T t2489 o2335 b2489
4239 B b2490 t2489
4240 T t2490 o2334 b2490
4241 B b2491 t2490
4242 T t2491 o2337 b2491
4243 B b2492 t2491 t
4244 T t2492 o2336 b2492
4245 B b2493 t2492
4246 T t2493 o2335 b2493
4247 B b2494 t2493
4248 T t2494 o2334 b2494
4249 B b2495 t2494
4250 T t2495 o2331 b2334 b2495
4251 B b2496 t2495
4252 T t2496 o b2496 b4
4253 B b2497 t2496
4254 T t2497 o2331 b2497
4255 B b2498 t2497
4256 T t2498 o392 b2498
4257 B b2499 t2498
4258 T t2499 o2330 b2499
4259 B b2500 t2499
4260 P p2500 Number 5924
4261 P p2501 Number 6165
4262 O o2501 location p2500 p2501
4263 P p1725 String unique_id1
4264 O o1725 rule p1725
4265 P p1726 Var e2
4266 O o1726 var p1726
4267 T t1726 o1726
4268 B b1726 t1726
4269 T t1727 o620 b1726
4270 S s1727 t637 h
4271 G s1727 t1727
4272 B b1727 s1727
4273 T t1728 o618 b1727
4274 B b1728 t1728
4275 T t1729 o655 b1726 b554
4276 S s1729 t620 h
4277 G s1729 t1729
4278 B b1729 s1729
4279 T t1730 o618 b1729
4280 B b1730 t1730
4281 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
4282 NCzf_itt_dall!dall dall dall Czf_itt_dall
4283 O o1730 dall
4284 T t1731 o559 b1726 b573
4285 B b1731 t1731
4286 T t1732 o676 b1731 b573
4287 B b1732 t1732
4288 T t1733 o559 b573 b1726
4289 B b1733 t1733
4290 T t1734 o676 b1733 b573
4291 B b1734 t1734
4292 T t1735 o1270 b1732 b1734
4293 B b1735 t1735 s
4294 T t1736 o1730 b554 b1735
4295 H h1736 x t1736
4296 T t1737 o676 b1726 b567
4297 S s1737 t620 h h1736
4298 G s1737 t1737
4299 B b1737 s1737
4300 T t1738 o618 b1737
4301 B b1738 t1738
4302 T t1739 o635 b1730 b1738
4303 B b1739 t1739
4304 T t1740 o635 b1728 b1739
4305 B b1740 t1740
4306 P p1740 String "withT << id >> (dT 2) thenT autoT"
4307 O o1740 ext_rule p1740
4308 T t1741 o b1729 b4
4309 B b1741 t1741
4310 T t1742 o b1727 b1741
4311 B b1742 t1742
4312 T t1743 o938 b1737 b1742
4313 B b1743 t1743
4314 T t1744 o937 b1743 b4 b946
4315 B b1744 t1744
4316 T t1745 o559 b1726 b567
4317 B b1745 t1745
4318 T t1746 o676 b1745 b567
4319 H h1746 y t1746
4320 T t1747 o559 b567 b1726
4321 B b1747 t1747
4322 T t1748 o676 b1747 b567
4323 H h1748 z t1748
4324 S s1748 t620 h h1736 h1746 h1748
4325 G s1748 t1737
4326 B b1748 s1748
4327 T t1749 o938 b1748 b1742
4328 B b1749 t1749
4329 B b1750 t1746
4330 B b1751 t1748
4331 T t1751 o1270 b1750 b1751
4332 H h1751 w t1751
4333 S s1751 t620 h h1736 h1751
4334 G s1751 t1737
4335 B b1752 s1751
4336 T t1752 o938 b1752 b1742
4337 B b1753 t1752
4338 P p1753 String with
4339 O o1753 arg_named p1753
4340 NSummary!arg_term_list arg_term_list arg_term_list Summary
4341 O o1754 arg_term_list
4342 T t1754 o b567 b4
4343 B b1754 t1754
4344 T t1755 o1754 b1754
4345 B b1755 t1755
4346 T t1756 o1753 b1755
4347 B b1756 t1756
4348 T t1757 o b1756 b4
4349 B b1757 t1757
4350 T t1758 o937 b1743 b1757 b946
4351 B b1758 t1758
4352 T t1759 o2 b1758
4353 B b1759 t1759
4354 T t1760 o937 b1753 b4 b1759
4355 B b1760 t1760
4356 T t1761 o2 b1760
4357 B b1761 t1761
4358 T t1762 o937 b1749 b4 b1761
4359 B b1762 t1762
4360 T t1763 o b1762 b4
4361 B b1763 t1763
4362 T t1764 o936 b1744 b1763
4363 B b1764 t1764
4364 P p1764 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
4365 O o1764 ext_rule p1764
4366 T t1765 o936 b1762 b4
4367 B b1765 t1765
4368 T t1766 o1764 b935 b1765 b4 b4
4369 B b1766 t1766
4370 T t1767 o b1766 b4
4371 B b1767 t1767
4372 S s1767 t620 h
4373 G s1767 t1727
4374 B b1768 s1767
4375 T t1768 o b1768 b1741
4376 B b1769 t1768
4377 T t1769 o938 b1748 b1769
4378 B b1770 t1769
4379 T t1770 o938 b1752 b1769
4380 B b1771 t1770
4381 T t1771 o938 b1737 b1769
4382 B b1772 t1771
4383 T t1772 o937 b1772 b1757 b946
4384 B b1773 t1772
4385 T t1773 o2 b1773
4386 B b1774 t1773
4387 T t1774 o937 b1771 b4 b1774
4388 B b1775 t1774
4389 T t1775 o2 b1775
4390 B b1776 t1775
4391 T t1776 o937 b1770 b4 b1776
4392 B b1777 t1776
4393 T t1777 o936 b1777 b4
4394 B b1778 t1777
4395 T t1778 o1764 b935 b1778 b4 b4
4396 B b1779 t1778
4397 P p1779 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
4398 O o1779 ext_rule p1779
4399 H h1779 v t1737
4400 S s1779 t620 h h1736 h1746 h1748 h1779
4401 G s1779 t1737
4402 B b1780 s1779
4403 T t1780 o938 b1780 b1769
4404 B b1781 t1780
4405 T t1781 o2 b1777
4406 B b1782 t1781
4407 T t1782 o937 b1781 b4 b1782
4408 B b1783 t1782
4409 T t1783 o b1783 b4
4410 B b1784 t1783
4411 T t1784 o936 b1777 b1784
4412 B b1785 t1784
4413 T t1785 o1085 b1783
4414 B b1786 t1785
4415 T t1786 o b1786 b4
4416 B b1787 t1786
4417 T t1787 o1779 b935 b1785 b1787 b4
4418 B b1788 t1787
4419 P p1788 String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
4420 O o1788 ext_rule p1788
4421 P p1789 Var e
4422 O o1789 var p1789
4423 T t1789 o1789
4424 B b1789 t1789
4425 T t1790 o620 b1789
4426 S s1790 t637 h h1736 h1746 h1748
4427 G s1790 t1790
4428 B b1790 s1790
4429 T t1791 o938 b1790 b1769
4430 B b1791 t1791
4431 T t1792 o559 b1726 b1789
4432 B b1792 t1792
4433 T t1793 o620 b1792
4434 S s1793 t637 h h1736 h1746 h1748
4435 G s1793 t1793
4436 B b1793 s1793
4437 T t1794 o938 b1793 b1769
4438 B b1794 t1794
4439 T t1795 o738 b1792 b1726
4440 S s1795 t620 h h1736 h1746 h1748
4441 G s1795 t1795
4442 B b1795 s1795
4443 T t1796 o938 b1795 b1769
4444 B b1796 t1796
4445 T t1797 o966 b1796 b983 b1782
4446 B b1797 t1797
4447 T t1798 o2 b1797
4448 B b1798 t1798
4449 T t1799 o973 b1794 b983 b1798
4450 B b1799 t1799
4451 T t1800 o2 b1799
4452 B b1800 t1800
4453 T t1801 o973 b1791 b4 b1800
4454 B b1801 t1801
4455 T t1802 o676 b1792 b1726
4456 S s1802 t620 h h1736 h1746 h1748
4457 G s1802 t1802
4458 B b1802 s1802
4459 T t1803 o938 b1802 b1769
4460 B b1803 t1803
4461 T t1804 o966 b1803 b4 b1798
4462 B b1804 t1804
4463 H h1804 v t1746
4464 S s1804 t620 h h1736 h1746 h1748 h1804
4465 G s1804 t1737
4466 B b1805 s1804
4467 T t1805 o938 b1805 b1769
4468 B b1806 t1805
4469 T t1806 o937 b1806 b4 b1782
4470 B b1807 t1806
4471 T t471 o b1807 b4
4472 B b471 t471
4473 T t479 o b1804 b471
4474 B b479 t479
4475 T t480 o b1801 b479
4476 B b480 t480
4477 T t486 o936 b1777 b480
4478 B b486 t486
4479 T t1821 o1085 b1801
4480 B b1822 t1821
4481 T t1822 o1085 b1804
4482 B b1823 t1822
4483 T t1823 o1085 b1807
4484 B b1824 t1823
4485 T t487 o b1824 b4
4486 B b487 t487
4487 T t493 o b1823 b487
4488 B b493 t493
4489 T t494 o b1822 b493
4490 B b494 t494
4491 T t500 o1788 b935 b486 b494 b4
4492 B b500 t500
4493 T t501 o b500 b4
4494 B b501 t501
4495 T t508 o b500 b501
4496 B b508 t508
4497 T t509 o b1788 b508
4498 B b509 t509
4499 T t516 o b1779 b509
4500 B b516 t516
4501 T t517 o1740 b935 b1764 b1767 b516
4502 B b517 t517
4503 T t524 o933 b517
4504 B b524 t524
4505 P p2502 Number 5950
4506 P p2503 Number 5958
4507 O o2503 resource_defs p2502 p2503 p264
4508 P p2504 Number 5956
4509 O o2504 uid p2504 p2503
4510 T t2504 o2504 b626
4511 B b2504 t2504
4512 T t2505 o b2504 b4
4513 B b2505 t2505
4514 T t2506 o2503 b2505
4515 B b2506 t2506
4516 T t2507 o b2506 b4
4517 B b2507 t2507
4518 T t2508 o1725 b618 b1740 b524 b2507
4519 B b2508 t2508
4520 T t2509 o2501 b2508
4521 B b2509 t2509
4522 P p2509 Number 6812
4523 P p2510 Number 7193
4524 O o2510 location p2509 p2510
4525 P p2511 String unique_inv1
4526 O o2511 rule p2511
4527 T t1845 o559 b561 b573
4528 B b1845 t1845
4529 T t1846 o738 b1845 b567
4530 S s2511 t620 h
4531 G s2511 t1846
4532 B b2511 s2511
4533 T t2511 o618 b2511
4534 B b2512 t2511
4535 T t1847 o559 b573 b561
4536 B b1847 t1847
4537 T t1848 o738 b1847 b567
4538 S s2512 t620 h
4539 G s2512 t1848
4540 B b2513 s2512
4541 T t2513 o618 b2513
4542 B b2514 t2513
4543 T t1849 o738 b561 b574
4544 S s2514 t620 h
4545 G s2514 t1849
4546 B b2515 s2514
4547 T t2518 o618 b2515
4548 B b2519 t2518
4549 T t2519 o635 b2514 b2519
4550 B b2520 t2519
4551 T t2520 o635 b2512 b2520
4552 B b2521 t2520
4553 T t2521 o635 b658 b2521
4554 B b2522 t2521
4555 T t2522 o635 b794 b2522
4556 B b2527 t2522
4557 T t2527 o635 b641 b2527
4558 B b2528 t2527
4559 T t2528 o635 b711 b2528
4560 B b2532 t2528
4561 P p2532 String "assumT 5 thenT assumT 6"
4562 O o2532 ext_rule p2532
4563 T t2532 o b2513 b4
4564 B b2533 t2532
4565 T t2533 o b2511 b2533
4566 B b2534 t2533
4567 T t2534 o b657 b2534
4568 B b2535 t2534
4569 T t2535 o b793 b2535
4570 B b2536 t2535
4571 T t2536 o b640 b2536
4572 B b2537 t2536
4573 T t2537 o b710 b2537
4574 B b2538 t2537
4575 T t2538 o938 b2515 b2538
4576 B b2539 t2538
4577 T t2539 o937 b2539 b4 b946
4578 B b2540 t2539
4579 H h2540 v t1846
4580 H h2541 v_1 t1848
4581 S s2541 t620 h h2540 h2541
4582 G s2541 t1849
4583 B b2541 s2541
4584 T t2541 o938 b2541 b2538
4585 B b2542 t2541
4586 S s2542 t620 h h2540
4587 G s2542 t1849
4588 B b2543 s2542
4589 T t2543 o938 b2543 b2538
4590 B b2544 t2543
4591 T t2544 o2 b2540
4592 B b2545 t2544
4593 T t2545 o937 b2544 b4 b2545
4594 B b2546 t2545
4595 T t2546 o2 b2546
4596 B b2547 t2546
4597 T t2547 o937 b2542 b4 b2547
4598 B b2548 t2547
4599 T t2548 o b2548 b4
4600 B b2549 t2548
4601 T t2549 o936 b2540 b2549
4602 B b2550 t2549
4603 P p1854 String "assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
4604 O o1854 ext_rule p1854
4605 T t1861 o559 b574 b573
4606 B b1861 t1861
4607 T t1862 o738 b1861 b567
4608 H h2550 v_2 t1862
4609 S s2550 t620 h h2540 h2541 h2550
4610 G s2550 t1849
4611 B b2551 s2550
4612 T t2551 o938 b2551 b2538
4613 B b2552 t2551
4614 T t2552 o2 b2548
4615 B b2553 t2552
4616 T t2553 o937 b2552 b4 b2553
4617 B b2554 t2553
4618 T t2554 o b2554 b4
4619 B b2555 t2554
4620 T t2555 o936 b2548 b2555
4621 B b2556 t2555
4622 P p1867 String "setSubstT << equal{id; op{inv{'s}; 's}} >> 2 thenAT autoT"
4623 O o1867 ext_rule p1867
4624 T t1868 o676 b567 b1861
4625 S s2556 t620 h h2540 h2541 h2550
4626 G s2556 t1868
4627 B b2557 s2556
4628 T t2557 o938 b2557 b2538
4629 B b2558 t2557
4630 T t1870 o738 b567 b1861
4631 S s2558 t620 h h2540 h2541 h2550
4632 G s2558 t1870
4633 B b2559 s2558
4634 T t2559 o938 b2559 b2538
4635 B b2560 t2559
4636 T t2560 o2 b2554
4637 B b2561 t2560
4638 T t2561 o966 b2560 b983 b2561
4639 B b2562 t2561
4640 T t2562 o2 b2562
4641 B b2563 t2562
4642 T t2563 o966 b2558 b4 b2563
4643 B b2564 t2563
4644 T t1876 o738 b1845 b1861
4645 H h2564 v_3 t1876
4646 S s2564 t620 h h2540 h2541 h2550 h2564
4647 G s2564 t1849
4648 B b2565 s2564
4649 T t2565 o938 b2565 b2538
4650 B b2566 t2565
4651 T t2566 o937 b2566 b4 b2561
4652 B b2567 t2566
4653 T t2567 o b2567 b4
4654 B b2568 t2567
4655 T t2568 o b2564 b2568
4656 B b2569 t2568
4657 T t2569 o936 b2554 b2569
4658 B b2570 t2569
4659 P p1891 String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
4660 O o1891 ext_rule p1891
4661 T t2570 o936 b2564 b4
4662 B b2571 t2570
4663 T t2571 o1891 b935 b2571 b4 b4
4664 B b2572 t2571
4665 P p1893 String "groupCancelRightT << 's >> thenT autoT"
4666 O o1893 ext_rule p1893
4667 T t2572 o936 b2567 b4
4668 B b2573 t2572
4669 T t2573 o1893 b935 b2573 b4 b4
4670 B b2574 t2573
4671 T t2574 o b2574 b4
4672 B b2575 t2574
4673 T t2575 o b2572 b2575
4674 B b2576 t2575
4675 T t2576 o1867 b935 b2570 b2576 b4
4676 B b2577 t2576
4677 T t2577 o b2577 b4
4678 B b2578 t2577
4679 T t2578 o1854 b935 b2556 b2578 b4
4680 B b2579 t2578
4681 T t2579 o b2579 b4
4682 B b2580 t2579
4683 T t2580 o2532 b935 b2550 b2580 b4
4684 B b2581 t2580
4685 T t2581 o933 b2581
4686 B b2582 t2581
4687 P p2582 Number 6839
4688 P p2583 Number 6847
4689 O o2583 resource_defs p2582 p2583 p264
4690 P p2584 Number 6845
4691 O o2584 uid p2584 p2583
4692 T t2584 o2584 b626
4693 B b2584 t2584
4694 T t2585 o b2584 b4
4695 B b2585 t2585
4696 T t2586 o2583 b2585
4697 B b2586 t2586
4698 T t2587 o b2586 b4
4699 B b2587 t2587
4700 T t2588 o2511 b618 b2532 b2582 b2587
4701 B b2588 t2588
4702 T t2589 o2510 b2588
4703 B b2589 t2589
4704 P p2589 Number 7195
4705 P p2590 Number 7576
4706 O o2590 location p2589 p2590
4707 P p2591 String unique_inv2
4708 O o2591 rule p2591
4709 T t2591 o738 b574 b561
4710 S s2591 t620 h
4711 G s2591 t2591
4712 B b2591 s2591
4713 T t2592 o618 b2591
4714 B b2592 t2592
4715 T t2593 o635 b2514 b2592
4716 B b2593 t2593
4717 T t2594 o635 b2512 b2593
4718 B b2594 t2594
4719 T t2595 o635 b658 b2594
4720 B b2595 t2595
4721 T t2596 o635 b794 b2595
4722 B b2596 t2596
4723 T t2597 o635 b641 b2596
4724 B b2597 t2597
4725 T t2598 o635 b711 b2597
4726 B b2598 t2598
4727 P p2598 String "assumT 5 thenT assumT 6 thenT assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
4728 O o2598 ext_rule p2598
4729 T t2599 o938 b2591 b2538
4730 B b2599 t2599
4731 T t2600 o937 b2599 b4 b946
4732 B b2600 t2600
4733 S s2600 t620 h h2540 h2541 h2550
4734 G s2600 t2591
4735 B b2601 s2600
4736 T t2601 o938 b2601 b2538
4737 B b2602 t2601
4738 S s2602 t620 h h2540 h2541
4739 G s2602 t2591
4740 B b2603 s2602
4741 T t2603 o938 b2603 b2538
4742 B b2604 t2603
4743 S s2604 t620 h h2540
4744 G s2604 t2591
4745 B b2605 s2604
4746 T t2605 o938 b2605 b2538
4747 B b2606 t2605
4748 T t2606 o2 b2600
4749 B b2607 t2606
4750 T t2607 o937 b2606 b4 b2607
4751 B b2608 t2607
4752 T t2608 o2 b2608
4753 B b2609 t2608
4754 T t2609 o937 b2604 b4 b2609
4755 B b2610 t2609
4756 T t2610 o2 b2610
4757 B b2611 t2610
4758 T t2611 o937 b2602 b4 b2611
4759 B b2612 t2611
4760 T t2612 o b2612 b4
4761 B b2613 t2612
4762 T t2613 o936 b2600 b2613
4763 B b2614 t2613
4764 T t2614 o2 b2612
4765 B b2615 t2614
4766 T t2615 o966 b2560 b983 b2615
4767 B b2616 t2615
4768 T t2616 o2 b2616
4769 B b2617 t2616
4770 T t2617 o966 b2558 b4 b2617
4771 B b2618 t2617
4772 S s2618 t620 h h2540 h2541 h2550 h2564
4773 G s2618 t2591
4774 B b2619 s2618
4775 T t2619 o938 b2619 b2538
4776 B b2620 t2619
4777 T t2620 o937 b2620 b4 b2615
4778 B b2621 t2620
4779 T t2621 o b2621 b4
4780 B b2622 t2621
4781 T t2622 o b2618 b2622
4782 B b2623 t2622
4783 T t2623 o936 b2612 b2623
4784 B b2624 t2623
4785 T t2624 o936 b2618 b4
4786 B b2625 t2624
4787 T t2625 o1891 b935 b2625 b4 b4
4788 B b2626 t2625
4789 P p2626 String "assertT << equal{'s2; inv{'s}} >> thenT autoT"
4790 O o2626 ext_rule p2626
4791 H h2626 v_4 t1849
4792 T t2626 o676 b574 b561
4793 S s2626 t620 h h2540 h2541 h2550 h2564 h2626
4794 G s2626 t2626
4795 B b2627 s2626
4796 T t2627 o938 b2627 b2538
4797 B b2628 t2627
4798 S s2628 t620 h h2540 h2541 h2550 h2564 h2626
4799 G s2628 t2591
4800 B b2629 s2628
4801 T t2629 o938 b2629 b2538
4802 B b2630 t2629
4803 T t2630 o2 b2621
4804 B b2631 t2630
4805 T t2631 o937 b2630 b983 b2631
4806 B b2632 t2631
4807 T t2632 o2 b2632
4808 B b2633 t2632
4809 T t2633 o937 b2628 b4 b2633
4810 B b2634 t2633
4811 T t2634 o b2634 b4
4812 B b2635 t2634
4813 T t2635 o936 b2621 b2635
4814 B b2636 t2635
4815 P p2636 String "rwh unfold_equal 6 thenT autoT thenT eqSetSymT thenT autoT"
4816 O o2636 ext_rule p2636
4817 T t2636 o936 b2634 b4
4818 B b2637 t2636
4819 T t2637 o2636 b935 b2637 b4 b4
4820 B b2638 t2637
4821 T t2638 o b2638 b4
4822 B b2639 t2638
4823 T t2639 o2626 b935 b2636 b2639 b4
4824 B b2640 t2639
4825 T t2640 o b2640 b4
4826 B b2641 t2640
4827 T t2641 o b2626 b2641
4828 B b2642 t2641
4829 T t2642 o1867 b935 b2624 b2642 b4
4830 B b2643 t2642
4831 T t2643 o b2643 b4
4832 B b2644 t2643
4833 T t2644 o2598 b935 b2614 b2644 b4
4834 B b2645 t2644
4835 T t2645 o933 b2645
4836 B b2646 t2645
4837 P p2646 Number 7222
4838 P p2647 Number 7230
4839 O o2647 resource_defs p2646 p2647 p264
4840 P p2648 Number 7228
4841 O o2648 uid p2648 p2647
4842 T t2648 o2648 b626
4843 B b2648 t2648
4844 T t2649 o b2648 b4
4845 B b2649 t2649
4846 T t2650 o2647 b2649
4847 B b2650 t2650
4848 T t2651 o b2650 b4
4849 B b2651 t2651
4850 T t2652 o2591 b618 b2598 b2646 b2651
4851 B b2652 t2652
4852 T t2653 o2590 b2652
4853 B b2653 t2653
4854 P p2653 Number 7627
4855 P p2654 Number 8046
4856 O o2654 location p2653 p2654
4857 P p1913 String unique_sol1
4858 O o1913 rule p1913
4859 P p1914 Var a
4860 O o1914 var p1914
4861 T t1914 o1914
4862 B b1914 t1914
4863 T t1915 o620 b1914
4864 S s1915 t637 h
4865 G s1915 t1915
4866 B b1915 s1915
4867 T t1916 o618 b1915
4868 B b1916 t1916
4869 P p1916 Var b
4870 O o1916 var p1916
4871 T t1917 o1916
4872 B b1917 t1917
4873 T t1918 o620 b1917
4874 S s1918 t637 h
4875 G s1918 t1918
4876 B b1918 s1918
4877 T t1919 o618 b1918
4878 B b1919 t1919
4879 P p1919 Var x
4880 O o1919 var p1919
4881 T t1920 o1919
4882 B b1920 t1920
4883 T t1921 o620 b1920
4884 S s1921 t637 h
4885 G s1921 t1921
4886 B b1921 s1921
4887 T t1922 o618 b1921
4888 B b1922 t1922
4889 T t1923 o655 b1914 b554
4890 S s1923 t620 h
4891 G s1923 t1923
4892 B b1923 s1923
4893 T t1924 o618 b1923
4894 B b1924 t1924
4895 T t1925 o655 b1917 b554
4896 S s1925 t620 h
4897 G s1925 t1925
4898 B b1925 s1925
4899 T t1926 o618 b1925
4900 B b1926 t1926
4901 T t1927 o655 b1920 b554
4902 S s1927 t620 h
4903 G s1927 t1927
4904 B b1927 s1927
4905 T t1928 o618 b1927
4906 B b1928 t1928
4907 T t1929 o559 b1914 b1920
4908 B b1929 t1929
4909 T t1930 o738 b1929 b1917
4910 S s1930 t620 h
4911 G s1930 t1930
4912 B b1930 s1930
4913 T t1931 o618 b1930
4914 B b1931 t1931
4915 T t1932 o572 b1914
4916 B b1932 t1932
4917 T t1933 o559 b1932 b1917
4918 B b1933 t1933
4919 T t1934 o738 b1920 b1933
4920 S s1934 t620 h
4921 G s1934 t1934
4922 B b1934 s1934
4923 T t1935 o618 b1934
4924 B b1935 t1935
4925 T t1936 o635 b1931 b1935
4926 B b1936 t1936
4927 T t1937 o635 b1928 b1936
4928 B b1937 t1937
4929 T t1938 o635 b1926 b1937
4930 B b1938 t1938
4931 T t1939 o635 b1924 b1938
4932 B b1939 t1939
4933 T t1940 o635 b1922 b1939
4934 B b1940 t1940
4935 T t1941 o635 b1919 b1940
4936 B b1941 t1941
4937 T t1942 o635 b1916 b1941
4938 B b1942 t1942
4939 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"
4940 O o1942 ext_rule p1942
4941 T t1943 o b1930 b4
4942 B b1943 t1943
4943 T t1944 o b1927 b1943
4944 B b1944 t1944
4945 T t1945 o b1925 b1944
4946 B b1945 t1945
4947 T t1946 o b1923 b1945
4948 B b1946 t1946
4949 T t1947 o b1921 b1946
4950 B b1947 t1947
4951 T t1948 o b1918 b1947
4952 B b1948 t1948
4953 T t1949 o b1915 b1948
4954 B b1949 t1949
4955 T t1950 o938 b1934 b1949
4956 B b1950 t1950
4957 T t1951 o937 b1950 b4 b946
4958 B b1951 t1951
4959 T t1952 o620 b1929
4960 H h1952 y_1 t1952
4961 H h1953 z_1 t1918
4962 T t1953 o676 b1929 b1917
4963 H h1954 z t1953
4964 T t1954 o559 b1932 b1929
4965 B b1954 t1954
4966 T t1955 o738 b1954 b1933
4967 S s1955 t620 h h1952 h1953 h1954
4968 G s1955 t1955
4969 B b1955 s1955
4970 T t1956 o938 b1955 b1949
4971 B b1956 t1956
4972 T t1957 o676 b1920 b1933
4973 S s1957 t620 h h1952 h1953 h1954
4974 G s1957 t1957
4975 B b1957 s1957
4976 T t1958 o938 b1957 b1949
4977 B b1958 t1958
4978 S s1958 t620 h h1952 h1953 h1954
4979 G s1958 t1934
4980 B b1959 s1958
4981 T t1959 o938 b1959 b1949
4982 B b1960 t1959
4983 B b1961 t1952
4984 B b1962 t1918
4985 T t1962 o1270 b1961 b1962
4986 H h1962 y t1962
4987 S s1962 t620 h h1962 h1954
4988 G s1962 t1934
4989 B b1963 s1962
4990 T t1963 o938 b1963 b1949
4991 B b1964 t1963
4992 B b1965 t1962
4993 B b1966 t1953
4994 T t1966 o1270 b1965 b1966
4995 H h1966 v t1966
4996 S s1966 t620 h h1966
4997 G s1966 t1934
4998 B b1967 s1966
4999 T t1967 o938 b1967 b1949
5000 B b1968 t1967
5001 H h1968 v t1930
5002 S s1968 t620 h h1968
5003 G s1968 t1934
5004 B b1969 s1968
5005 T t1969 o938 b1969 b1949
5006 B b1970 t1969
5007 T t1970 o2 b1951
5008 B b1971 t1970
5009 T t1971 o937 b1970 b4 b1971
5010 B b1972 t1971
5011 T t1972 o2 b1972
5012 B b1973 t1972
5013 T t1973 o937 b1968 b4 b1973
5014 B b1974 t1973
5015 T t1974 o2 b1974
5016 B b1975 t1974
5017 T t1975 o937 b1964 b4 b1975
5018 B b1976 t1975
5019 T t1976 o2 b1976
5020 B b1977 t1976
5021 T t1977 o937 b1960 b983 b1977
5022 B b1978 t1977
5023 T t1978 o2 b1978
5024 B b1979 t1978
5025 T t1979 o937 b1958 b4 b1979
5026 B b1980 t1979
5027 T t1980 o2 b1980
5028 B b1981 t1980
5029 T t1981 o947 b1956 b4 b1981
5030 B b1982 t1981
5031 H h1982 v t1955
5032 S s1982 t620 h h1952 h1953 h1954 h1982
5033 G s1982 t1957
5034 B b1983 s1982
5035 T t1983 o938 b1983 b1949
5036 B b1984 t1983
5037 T t1984 o937 b1984 b4 b1981
5038 B b1985 t1984
5039 T t1985 o b1985 b4
5040 B b1986 t1985
5041 T t1986 o b1982 b1986
5042 B b1987 t1986
5043 T t1987 o936 b1951 b1987
5044 B b1988 t1987
5045 T t1988 o936 b1982 b4
5046 B b1989 t1988
5047 T t1989 o990 b935 b1989 b4 b4
5048 B b1990 t1989
5049 P p1990 String "setSubstT << equal{op{inv{'a}; op{'a; 'x}}; op{op{inv{'a}; 'a}; 'x}} >> 5 thenT autoT"
5050 O o1990 ext_rule p1990
5051 T t1990 o559 b1932 b1914
5052 B b1991 t1990
5053 T t1991 o559 b1991 b1920
5054 B b1992 t1991
5055 T t1992 o738 b1992 b1933
5056 H h1992 v_1 t1992
5057 S s1992 t620 h h1952 h1953 h1954 h1982 h1992
5058 G s1992 t1957
5059 B b1993 s1992
5060 T t1993 o938 b1993 b1949
5061 B b1994 t1993
5062 T t1994 o2 b1985
5063 B b1995 t1994
5064 T t1995 o937 b1994 b4 b1995
5065 B b1996 t1995
5066 T t566 o b1996 b4
5067 B b566 t566
5068 T t570 o936 b1985 b566
5069 B b570 t570
5070 B b1997 t1933 v_1
5071 T t1997 o711 b1997
5072 S s1997 t620 h h1952 h1953 h1954 h1982
5073 G s1997 t1997
5074 B b1998 s1997
5075 T t1998 o938 b1998 b1949
5076 B b1999 t1998
5077 T t1999 o738 b1220 b1933
5078 B b2000 t1999 v_1
5079 T t2000 o976 b2000
5080 S s2000 t620 h h1952 h1953 h1954 h1982
5081 G s2000 t2000
5082 B b2001 s2000
5083 T t2001 o938 b2001 b1949
5084 B b2002 t2001
5085 T t2002 o973 b2002 b983 b1995
5086 B b2003 t2002
5087 T t2003 o2 b2003
5088 B b2004 t2003
5089 T t2004 o973 b1999 b4 b2004
5090 B b2005 t2004
5091 P p2008 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"
5092 O o2008 ext_rule p2008
5093 T t2008 o559 b567 b1920
5094 B b2009 t2008
5095 T t2009 o738 b2009 b1933
5096 H h2009 v_2 t2009
5097 S s2009 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5098 G s2009 t1957
5099 B b2010 s2009
5100 T t2010 o938 b2010 b1949
5101 B b2011 t2010
5102 T t2011 o2 b1996
5103 B b2012 t2011
5104 T t2012 o937 b2011 b4 b2012
5105 B b2013 t2012
5106 T t571 o b2013 b4
5107 B b571 t571
5108 T t572 o936 b1996 b571
5109 B b572 t572
5110 B b2014 t1933 v_2
5111 T t2014 o711 b2014
5112 S s2014 t620 h h1952 h1953 h1954 h1982 h1992
5113 G s2014 t2014
5114 B b2015 s2014
5115 T t2015 o938 b2015 b1949
5116 B b2016 t2015
5117 T t2016 o559 b977 b1920
5118 B b2017 t2016
5119 T t2017 o738 b2017 b1933
5120 B b2018 t2017 v_2
5121 T t2018 o976 b2018
5122 S s2018 t620 h h1952 h1953 h1954 h1982 h1992
5123 G s2018 t2018
5124 B b2019 s2018
5125 T t2019 o938 b2019 b1949
5126 B b2020 t2019
5127 T t2020 o973 b2020 b983 b2012
5128 B b2021 t2020
5129 T t2021 o2 b2021
5130 B b2022 t2021
5131 T t2022 o973 b2016 b4 b2022
5132 B b2023 t2022
5133 P p2026 String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"
5134 O o2026 ext_rule p2026
5135 H h2026 v_3 t1934
5136 S s2026 t620 h h1952 h1953 h1954 h1982 h1992 h2009 h2026
5137 G s2026 t1957
5138 B b2027 s2026
5139 T t2027 o938 b2027 b1949
5140 B b2028 t2027
5141 T t2028 o2 b2013
5142 B b2029 t2028
5143 T t2029 o937 b2028 b4 b2029
5144 B b2030 t2029
5145 T t577 o b2030 b4
5146 B b577 t577
5147 T t578 o936 b2013 b577
5148 B b578 t578
5149 B b2031 t1933 v_3
5150 T t2031 o711 b2031
5151 S s2031 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5152 G s2031 t2031
5153 B b2032 s2031
5154 T t2032 o938 b2032 b1949
5155 B b2033 t2032
5156 T t2033 o738 b1004 b1933
5157 B b2034 t2033 v_3
5158 T t2034 o976 b2034
5159 S s2034 t620 h h1952 h1953 h1954 h1982 h1992 h2009
5160 G s2034 t2034
5161 B b2035 s2034
5162 T t2035 o938 b2035 b1949
5163 B b2036 t2035
5164 T t2036 o973 b2036 b983 b2029
5165 B b2037 t2036
5166 T t2037 o2 b2037
5167 B b2038 t2037
5168 T t2038 o973 b2033 b4 b2038
5169 B b2039 t2038
5170 P p2042 String "rwh unfold_equal 8 thenT autoT"
5171 O o2042 ext_rule p2042
5172 T t2042 o936 b2030 b4
5173 B b2043 t2042
5174 T t2043 o2042 b935 b2043 b4 b4
5175 B b2044 t2043
5176 T t586 o b2044 b4
5177 B b586 t586
5178 T t2044 o936 b2039 b4
5179 B b2045 t2044
5180 T t2045 o1071 b935 b2045 b4 b4
5181 B b2046 t2045
5182 T t2046 o b2046 b4
5183 B b2047 t2046
5184 T t587 o2026 b935 b578 b586 b2047
5185 B b587 t587
5186 T t593 o b587 b4
5187 B b593 t593
5188 T t2049 o936 b2023 b4
5189 B b2050 t2049
5190 T t2050 o1071 b935 b2050 b4 b4
5191 B b2051 t2050
5192 T t2051 o b2051 b4
5193 B b2052 t2051
5194 T t594 o2008 b935 b572 b593 b2052
5195 B b594 t594
5196 T t607 o b594 b4
5197 B b607 t607
5198 T t2054 o936 b2005 b4
5199 B b2055 t2054
5200 T t2055 o1071 b935 b2055 b4 b4
5201 B b2056 t2055
5202 T t2058 o738 b1954 b1992
5203 S s2058 t620 h h1952 h1953 h1954 h1982
5204 G s2058 t2058
5205 B b2059 s2058
5206 T t2059 o938 b2059 b1949
5207 B b2060 t2059
5208 T t2060 o966 b2060 b4 b1995
5209 B b2061 t2060
5210 T t2061 o936 b2061 b4
5211 B b2062 t2061
5212 T t2062 o990 b935 b2062 b4 b4
5213 B b2063 t2062
5214 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"
5215 O o2063 ext_rule p2063
5216 T t2063 o973 b2002 b4 b1995
5217 B b2064 t2063
5218 T t615 o936 b2064 b4
5219 B b615 t615
5220 H h2064 x_1 t1344
5221 H h2065 y_2 t638
5222 T t2065 o620 b1933
5223 H h2066 z_3 t2065
5224 T t2066 o676 b560 b1933
5225 H h2067 z_2 t2066
5226 S s2067 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5227 G s2067 t1997
5228 B b2067 s2067
5229 T t2067 o938 b2067 b1949
5230 B b2068 t2067
5231 T t2068 o676 b1220 b1933
5232 B b2069 t2068 v_1
5233 T t2069 o976 b2069
5234 S s2069 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5235 G s2069 t2069
5236 B b2070 s2069
5237 T t2070 o938 b2070 b1949
5238 B b2071 t2070
5239 T t2071 o676 b561 b1933
5240 S s2071 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2065 h2066 h2067
5241 G s2071 t2071
5242 B b2072 s2071
5243 T t2072 o938 b2072 b1949
5244 B b2073 t2072
5245 B b2074 t638
5246 B b2075 t2065
5247 T t2075 o1270 b2074 b2075
5248 H h2075 y t2075
5249 S s2075 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2075 h2067
5250 G s2075 t2071
5251 B b2076 s2075
5252 T t2076 o938 b2076 b1949
5253 B b2077 t2076
5254 B b2078 t2075
5255 B b2079 t2066
5256 T t2079 o1270 b2078 b2079
5257 H h2079 x_2 t2079
5258 S s2079 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2079
5259 G s2079 t2071
5260 B b2080 s2079
5261 T t2080 o938 b2080 b1949
5262 B b2081 t2080
5263 T t2081 o738 b560 b1933
5264 H h2081 x_2 t2081
5265 S s2081 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5266 G s2081 t2071
5267 B b2082 s2081
5268 T t2082 o938 b2082 b1949
5269 B b2083 t2082
5270 T t2083 o738 b561 b1933
5271 S s2083 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064 h2081
5272 G s2083 t2083
5273 B b2084 s2083
5274 T t2084 o938 b2084 b1949
5275 B b2085 t2084
5276 B b2086 t2081
5277 B b2087 t2083
5278 T t2087 o1177 b2086 b2087
5279 S s2087 t620 h h1952 h1953 h1954 h1982 h1344 h1224 h2064
5280 G s2087 t2087
5281 B b2088 s2087
5282 T t2088 o938 b2088 b1949
5283 B b2089 t2088
5284 B b2090 t2087
5285 T t2090 o1177 b1347 b2090
5286 S s2090 t620 h h1952 h1953 h1954 h1982 h1344 h1224
5287 G s2090 t2090
5288 B b2091 s2090
5289 T t2091 o938 b2091 b1949
5290 B b2092 t2091
5291 B b2093 t2090 s2
5292 T t2093 o1185 b1186 b2093
5293 S s2093 t620 h h1952 h1953 h1954 h1982 h1344
5294 G s2093 t2093
5295 B b2094 s2093
5296 T t2094 o938 b2094 b1949
5297 B b2095 t2094
5298 B b2096 t2093 s1
5299 T t2096 o1185 b1186 b2096
5300 S s2096 t620 h h1952 h1953 h1954 h1982
5301 G s2096 t2096
5302 B b2097 s2096
5303 T t2097 o938 b2097 b1949
5304 B b2098 t2097
5305 T t2098 o2 b2064
5306 B b2099 t2098
5307 T t2099 o973 b2098 b983 b2099
5308 B b2100 t2099
5309 T t2100 o2 b2100
5310 B b2101 t2100
5311 T t2101 o937 b2095 b983 b2101
5312 B b2102 t2101
5313 T t2102 o2 b2102
5314 B b2103 t2102
5315 T t2103 o937 b2092 b983 b2103
5316 B b2104 t2103
5317 T t2104 o2 b2104
5318 B b2105 t2104
5319 T t2105 o937 b2089 b983 b2105
5320 B b2106 t2105
5321 T t2106 o2 b2106
5322 B b2107 t2106
5323 T t2107 o937 b2085 b983 b2107
5324 B b2108 t2107
5325 T t2108 o2 b2108
5326 B b2109 t2108
5327 T t2109 o937 b2083 b4 b2109
5328 B b2110 t2109
5329 T t2110 o2 b2110
5330 B b2111 t2110
5331 T t2111 o937 b2081 b4 b2111
5332 B b2112 t2111
5333 T t2112 o2 b2112
5334 B b2113 t2112
5335 T t2113 o937 b2077 b4 b2113
5336 B b2114 t2113
5337 T t2114 o2 b2114
5338 B b2115 t2114
5339 T t2115 o937 b2073 b4 b2115
5340 B b2116 t2115
5341 T t2116 o2 b2116
5342 B b2117 t2116
5343 T t2117 o973 b2071 b983 b2117
5344 B b2118 t2117
5345 T t2118 o2 b2118
5346 B b2119 t2118
5347 T t2119 o973 b2068 b4 b2119
5348 B b2120 t2119
5349 T t2122 o936 b2120 b4
5350 B b2123 t2122
5351 T t2123 o1071 b935 b2123 b4 b4
5352 B b2124 t2123
5353 T t2124 o b2124 b4
5354 B b2125 t2124
5355 T t616 o2063 b935 b615 b4 b2125
5356 B b616 t616
5357 T t624 o b616 b4
5358 B b624 t624
5359 T t625 o b2063 b624
5360 B b625 t625
5361 T t633 o b2056 b625
5362 B b633 t633
5363 T t634 o1990 b935 b570 b607 b633
5364 B b634 t634
5365 T t635 o b634 b4
5366 B b635 t635
5367 T t646 o b1990 b635
5368 B b646 t646
5369 T t653 o1942 b935 b1988 b646 b4
5370 B b653 t653
5371 T t654 o933 b653
5372 B b654 t654
5373 P p2655 Number 7654
5374 P p2656 Number 7662
5375 O o2656 resource_defs p2655 p2656 p264
5376 P p2657 Number 7660
5377 O o2657 uid p2657 p2656
5378 T t2657 o2657 b626
5379 B b2657 t2657
5380 T t2658 o b2657 b4
5381 B b2658 t2658
5382 T t2659 o2656 b2658
5383 B b2659 t2659
5384 T t2660 o b2659 b4
5385 B b2660 t2660
5386 T t2661 o1913 b618 b1942 b654 b2660
5387 B b2661 t2661
5388 T t2662 o2654 b2661
5389 B b2662 t2662
5390 P p2662 Number 8097
5391 P p2663 Number 8516
5392 O o2663 location p2662 p2663
5393 P p2142 String unique_sol2
5394 O o2142 rule p2142
5395 P p2143 Var y
5396 O o2143 var p2143
5397 T t2143 o2143
5398 B b2143 t2143
5399 T t2144 o620 b2143
5400 S s2144 t637 h
5401 G s2144 t2144
5402 B b2144 s2144
5403 T t2145 o618 b2144
5404 B b2145 t2145
5405 T t2146 o655 b2143 b554
5406 S s2146 t620 h
5407 G s2146 t2146
5408 B b2146 s2146
5409 T t2147 o618 b2146
5410 B b2147 t2147
5411 T t2148 o559 b2143 b1914
5412 B b2148 t2148
5413 T t2149 o738 b2148 b1917
5414 S s2149 t620 h
5415 G s2149 t2149
5416 B b2149 s2149
5417 T t2150 o618 b2149
5418 B b2150 t2150
5419 T t2151 o559 b1917 b1932
5420 B b2151 t2151
5421 T t2152 o738 b2143 b2151
5422 S s2152 t620 h
5423 G s2152 t2152
5424 B b2152 s2152
5425 T t2153 o618 b2152
5426 B b2153 t2153
5427 T t2154 o635 b2150 b2153
5428 B b2154 t2154
5429 T t2155 o635 b2147 b2154
5430 B b2155 t2155
5431 T t2156 o635 b1926 b2155
5432 B b2156 t2156
5433 T t2157 o635 b1924 b2156
5434 B b2157 t2157
5435 T t2158 o635 b2145 b2157
5436 B b2158 t2158
5437 T t2159 o635 b1919 b2158
5438 B b2159 t2159
5439 T t2160 o635 b1916 b2159
5440 B b2160 t2160
5441 P p2160 String "assumT 7 thenT assertT << equal{op{op{'y; 'a}; inv{'a}}; op{'b; inv{'a}}} >> thenT autoT"
5442 O o2160 ext_rule p2160
5443 T t2161 o b2149 b4
5444 B b2161 t2161
5445 T t2162 o b2146 b2161
5446 B b2162 t2162
5447 T t2163 o b1925 b2162
5448 B b2163 t2163
5449 T t2164 o b1923 b2163
5450 B b2164 t2164
5451 T t2165 o b2144 b2164
5452 B b2165 t2165
5453 T t2166 o b1918 b2165
5454 B b2166 t2166
5455 T t2167 o b1915 b2166
5456 B b2167 t2167
5457 T t2168 o938 b2152 b2167
5458 B b2168 t2168
5459 T t2169 o937 b2168 b4 b946
5460 B b2169 t2169
5461 H h2169 v t2149
5462 T t2170 o676 b2148 b1917
5463 S s2170 t620 h h2169
5464 G s2170 t2170
5465 B b2170 s2170
5466 T t2171 o938 b2170 b2167
5467 B b2171 t2171
5468 T t2172 o559 b2148 b1932
5469 B b2172 t2172
5470 T t2173 o676 b2172 b2151
5471 S s2173 t620 h h2169
5472 G s2173 t2173
5473 B b2173 s2173
5474 T t2174 o938 b2173 b2167
5475 B b2174 t2174
5476 T t2175 o738 b2172 b2151
5477 S s2175 t620 h h2169
5478 G s2175 t2175
5479 B b2175 s2175
5480 T t2176 o938 b2175 b2167
5481 B b2176 t2176
5482 S s2176 t620 h h2169
5483 G s2176 t2152
5484 B b2177 s2176
5485 T t2177 o938 b2177 b2167
5486 B b2178 t2177
5487 T t2178 o2 b2169
5488 B b2179 t2178
5489 T t2179 o937 b2178 b4 b2179
5490 B b2180 t2179
5491 T t2180 o2 b2180
5492 B b2181 t2180
5493 T t2181 o947 b2176 b983 b2181
5494 B b2182 t2181
5495 T t2182 o2 b2182
5496 B b2183 t2182
5497 T t2183 o947 b2174 b983 b2183
5498 B b2184 t2183
5499 T t2184 o2 b2184
5500 B b2185 t2184
5501 T t2185 o947 b2171 b4 b2185
5502 B b2186 t2185
5503 H h2186 v_1 t2175
5504 T t2186 o676 b2143 b2151
5505 S s2186 t620 h h2169 h2186
5506 G s2186 t2186
5507 B b2187 s2186
5508 T t2187 o938 b2187 b2167
5509 B b2188 t2187
5510 S s2188 t620 h h2169 h2186
5511 G s2188 t2152
5512 B b2189 s2188
5513 T t2189 o938 b2189 b2167
5514 B b2190 t2189
5515 T t2190 o937 b2190 b983 b2181
5516 B b2191 t2190
5517 T t2191 o2 b2191
5518 B b2192 t2191
5519 T t2192 o937 b2188 b4 b2192
5520 B b2193 t2192
5521 T t2193 o b2193 b4
5522 B b2194 t2193
5523 T t2194 o b2186 b2194
5524 B b2195 t2194
5525 T t2195 o936 b2169 b2195
5526 B b2196 t2195
5527 P p2196 String "rwh unfold_equal 2 thenT autoT"
5528 O o2196 ext_rule p2196
5529 T t2196 o936 b2186 b4
5530 B b2197 t2196
5531 T t2197 o2196 b935 b2197 b4 b4
5532 B b2198 t2197
5533 P p2198 String "setSubstT << equal{op{op{'y; 'a}; inv{'a}}; op{'y; op{'a; inv{'a}}}} >> 3 thenT autoT"
5534 O o2198 ext_rule p2198
5535 T t2198 o559 b1914 b1932
5536 B b2199 t2198
5537 T t2199 o559 b2143 b2199
5538 B b2200 t2199
5539 T t2200 o738 b2200 b2151
5540 H h2200 v_2 t2200
5541 S s2200 t620 h h2169 h2186 h2200
5542 G s2200 t2186
5543 B b2201 s2200
5544 T t2201 o938 b2201 b2167
5545 B b2202 t2201
5546 T t2202 o2 b2193
5547 B b2203 t2202
5548 T t2203 o937 b2202 b4 b2203
5549 B b2204 t2203
5550 T t673 o b2204 b4
5551 B b673 t673
5552 T t687 o936 b2193 b673
5553 B b687 t687
5554 B b2205 t2151 v_2
5555 T t2205 o711 b2205
5556 S s2205 t620 h h2169 h2186
5557 G s2205 t2205
5558 B b2206 s2205
5559 T t2206 o938 b2206 b2167
5560 B b2207 t2206
5561 T t2207 o738 b977 b2151
5562 B b2208 t2207 v_2
5563 T t2208 o976 b2208
5564 S s2208 t620 h h2169 h2186
5565 G s2208 t2208
5566 B b2209 s2208
5567 T t2209 o938 b2209 b2167
5568 B b2210 t2209
5569 T t2210 o973 b2210 b983 b2203
5570 B b2211 t2210
5571 T t2211 o2 b2211
5572 B b2212 t2211
5573 T t2212 o973 b2207 b4 b2212
5574 B b2213 t2212
5575 P p2216 String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"
5576 O o2216 ext_rule p2216
5577 T t2216 o559 b2143 b567
5578 B b2217 t2216
5579 T t2217 o738 b2217 b2151
5580 H h2217 v_3 t2217
5581 S s2217 t620 h h2169 h2186 h2200 h2217
5582 G s2217 t2186
5583 B b2218 s2217
5584 T t2218 o938 b2218 b2167
5585 B b2219 t2218
5586 T t2219 o2 b2204
5587 B b2220 t2219
5588 T t2220 o937 b2219 b4 b2220
5589 B b2221 t2220
5590 T t694 o b2221 b4
5591 B b694 t694
5592 T t703 o936 b2204 b694
5593 B b703 t703
5594 B b2222 t2151 v_3
5595 T t2222 o711 b2222
5596 S s2222 t620 h h2169 h2186 h2200
5597 G s2222 t2222
5598 B b2223 s2222
5599 T t2223 o938 b2223 b2167
5600 B b2224 t2223
5601 T t2224 o559 b2143 b1004
5602 B b2225 t2224
5603 T t2225 o738 b2225 b2151
5604 B b2226 t2225 v_3
5605 T t2226 o976 b2226
5606 S s2226 t620 h h2169 h2186 h2200
5607 G s2226 t2226
5608 B b2227 s2226
5609 T t2227 o938 b2227 b2167
5610 B b2228 t2227
5611 T t2228 o973 b2228 b983 b2220
5612 B b2229 t2228
5613 T t2229 o2 b2229
5614 B b2230 t2229
5615 T t2230 o973 b2224 b4 b2230
5616 B b2231 t2230
5617 P p2234 String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"
5618 O o2234 ext_rule p2234
5619 T t717 o936 b2221 b4
5620 B b717 t717
5621 T t2234 o620 b2217
5622 H h2234 y_2 t2234
5623 T t2235 o620 b2151
5624 H h2235 z_1 t2235
5625 T t2236 o676 b2217 b2151
5626 H h2236 z t2236
5627 S s2236 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5628 G s2236 t2222
5629 B b2236 s2236
5630 T t2237 o938 b2236 b2167
5631 B b2237 t2237
5632 T t2238 o676 b1004 b2151
5633 B b2238 t2238 v_3
5634 T t2239 o976 b2238
5635 S s2239 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5636 G s2239 t2239
5637 B b2239 s2239
5638 T t2240 o938 b2239 b2167
5639 B b2240 t2240
5640 S s2240 t620 h h2169 h2186 h2200 h2234 h2235 h2236
5641 G s2240 t2186
5642 B b2241 s2240
5643 T t2241 o938 b2241 b2167
5644 B b2242 t2241
5645 B b2243 t2234
5646 B b2244 t2235
5647 T t2244 o1270 b2243 b2244
5648 H h2244 y_1 t2244
5649 S s2244 t620 h h2169 h2186 h2200 h2244 h2236
5650 G s2244 t2186
5651 B b2245 s2244
5652 T t2245 o938 b2245 b2167
5653 B b2246 t2245
5654 B b2247 t2244
5655 B b2248 t2236
5656 T t2248 o1270 b2247 b2248
5657 H h2248 v_3 t2248
5658 S s2248 t620 h h2169 h2186 h2200 h2248
5659 G s2248 t2186
5660 B b2249 s2248
5661 T t2249 o938 b2249 b2167
5662 B b2250 t2249
5663 T t2250 o2 b2221
5664 B b2251 t2250
5665 T t2251 o937 b2250 b4 b2251
5666 B b2252 t2251
5667 T t2252 o2 b2252
5668 B b2253 t2252
5669 T t2253 o937 b2246 b4 b2253
5670 B b2254 t2253
5671 T t2254 o2 b2254
5672 B b2255 t2254
5673 T t2255 o937 b2242 b4 b2255
5674 B b2256 t2255
5675 T t2256 o2 b2256
5676 B b2257 t2256
5677 T t2257 o973 b2240 b983 b2257
5678 B b2258 t2257
5679 T t2258 o2 b2258
5680 B b2259 t2258
5681 T t2259 o973 b2237 b4 b2259
5682 B b2260 t2259
5683 T t2262 o936 b2260 b4
5684 B b2263 t2262
5685 T t2263 o1071 b935 b2263 b4 b4
5686 B b2264 t2263
5687 T t2264 o b2264 b4
5688 B b2265 t2264
5689 T t724 o2234 b935 b717 b4 b2265
5690 B b724 t724
5691 T t729 o b724 b4
5692 B b729 t729
5693 T t2266 o936 b2231 b4
5694 B b2267 t2266
5695 T t2267 o1071 b935 b2267 b4 b4
5696 B b2268 t2267
5697 T t2268 o b2268 b4
5698 B b2269 t2268
5699 T t736 o2216 b935 b703 b729 b2269
5700 B b736 t736
5701 T t749 o b736 b4
5702 B b749 t749
5703 T t2271 o936 b2213 b4
5704 B b2272 t2271
5705 T t2272 o1071 b935 b2272 b4 b4
5706 B b2273 t2272
5707 T t2273 o b2273 b4
5708 B b2274 t2273
5709 T t756 o2198 b935 b687 b749 b2274
5710 B b756 t756
5711 T t765 o b756 b4
5712 B b765 t765
5713 T t772 o b2198 b765
5714 B b772 t772
5715 T t775 o2160 b935 b2196 b772 b4
5716 B b775 t775
5717 T t782 o933 b775
5718 B b782 t782
5719 P p2664 Number 8124
5720 P p2665 Number 8132
5721 O o2665 resource_defs p2664 p2665 p264
5722 P p2666 Number 8130
5723 O o2666 uid p2666 p2665
5724 T t2666 o2666 b626
5725 B b2666 t2666
5726 T t2667 o b2666 b4
5727 B b2667 t2667
5728 T t2668 o2665 b2667
5729 B b2668 t2668
5730 T t2669 o b2668 b4
5731 B b2669 t2669
5732 T t2670 o2142 b618 b2160 b782 b2669
5733 B b2670 t2670
5734 T t2671 o2663 b2670
5735 B b2671 t2671
5736 P p2671 Number 8544
5737 P p2672 Number 8839
5738 O o2672 location p2671 p2672
5739 P p2289 String inv_simplify
5740 O o2289 rule p2289
5741 T t2289 o559 b1914 b1917
5742 B b2289 t2289
5743 T t2290 o572 b2289
5744 B b2290 t2290
5745 T t2291 o572 b1917
5746 B b2291 t2291
5747 T t2292 o559 b2291 b1932
5748 B b2292 t2292
5749 T t2293 o738 b2290 b2292
5750 S s2293 t620 h
5751 G s2293 t2293
5752 B b2293 s2293
5753 T t2294 o618 b2293
5754 B b2294 t2294
5755 T t2295 o635 b1926 b2294
5756 B b2295 t2295
5757 T t2296 o635 b1924 b2295
5758 B b2296 t2296
5759 T t2297 o635 b1919 b2296
5760 B b2297 t2297
5761 T t2298 o635 b1916 b2297
5762 B b2298 t2298
5763 P p794 String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >>"
5764 O o794 ext_rule p794
5765 T t2299 o b1925 b4
5766 B b2299 t2299
5767 T t2300 o b1923 b2299
5768 B b2300 t2300
5769 T t2301 o b1918 b2300
5770 B b2301 t2301
5771 T t2302 o b1915 b2301
5772 B b2302 t2302
5773 T t2303 o938 b2293 b2302
5774 B b2303 t2303
5775 T t2304 o937 b2303 b4 b946
5776 B b2304 t2304
5777 T t2305 o559 b2290 b2289
5778 B b2305 t2305
5779 T t2306 o559 b2292 b2289
5780 B b2306 t2306
5781 T t2307 o738 b2305 b2306
5782 S s2307 t620 h
5783 G s2307 t2307
5784 B b2307 s2307
5785 T t2308 o938 b2307 b2302
5786 B b2308 t2308
5787 T t2309 o2 b2304
5788 B b2309 t2309
5789 T t2310 o947 b2308 b4 b2309
5790 B b2310 t2310
5791 H h2310 v t2307
5792 S s2310 t620 h h2310
5793 G s2310 t2293
5794 B b2311 s2310
5795 T t2311 o938 b2311 b2302
5796 B b2312 t2311
5797 T t2312 o937 b2312 b4 b2309
5798 B b2313 t2312
5799 T t2313 o b2313 b4
5800 B b2314 t2313
5801 T t2314 o b2310 b2314
5802 B b2315 t2314
5803 T t2315 o936 b2304 b2315
5804 B b2316 t2315
5805 P p2316 String "setSubstT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; id} >> 0 thenWT autoT"
5806 O o2316 ext_rule p2316
5807 T t2316 o738 b2305 b567
5808 S s2316 t620 h
5809 G s2316 t2316
5810 B b2317 s2316
5811 T t2317 o938 b2317 b2302
5812 B b2318 t2317
5813 T t2318 o2 b2310
5814 B b2319 t2318
5815 T t2319 o966 b2318 b4 b2319
5816 B b2320 t2319
5817 T t2320 o738 b567 b2306
5818 S s2320 t620 h
5819 G s2320 t2320
5820 B b2321 s2320
5821 T t2321 o938 b2321 b2302
5822 B b2322 t2321
5823 T t2322 o937 b2322 b4 b2319
5824 B b2323 t2322
5825 T t800 o b2323 b4
5826 B b800 t800
5827 T t807 o b2320 b800
5828 B b807 t807
5829 T t813 o936 b2310 b807
5830 B b813 t813
5831 P p2326 Var v
5832 O o2326 var p2326
5833 T t2326 o2326
5834 B b2327 t2326
5835 T t2337 o936 b2320 b4
5836 B b2338 t2337
5837 T t2338 o990 b935 b2338 b4 b4
5838 B b2339 t2338
5839 P p2339 String "setSubstT << equal{id; op{inv{'b}; op{inv{'a}; op{'a; 'b}}}} >> 0 thenWT autoT"
5840 O o2339 ext_rule p2339
5841 T t2339 o559 b1932 b2289
5842 B b2340 t2339
5843 T t2340 o559 b2291 b2340
5844 B b2341 t2340
5845 T t2341 o738 b567 b2341
5846 S s2341 t620 h
5847 G s2341 t2341
5848 B b2342 s2341
5849 T t2342 o938 b2342 b2302
5850 B b2343 t2342
5851 T t2343 o2 b2323
5852 B b2344 t2343
5853 T t2344 o966 b2343 b4 b2344
5854 B b2345 t2344
5855 T t2345 o738 b2341 b2306
5856 S s2345 t620 h
5857 G s2345 t2345
5858 B b2346 s2345
5859 T t2346 o938 b2346 b2302
5860 B b2347 t2346
5861 T t2347 o937 b2347 b4 b2344
5862 B b2348 t2347
5863 T t820 o b2348 b4
5864 B b820 t820
5865 T t821 o b2345 b820
5866 B b821 t821
5867 T t822 o936 b2323 b821
5868 B b822 t822
5869 P p2355 String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"
5870 O o2355 ext_rule p2355
5871 T t2355 o559 b1991 b1917
5872 B b2356 t2355
5873 T t2356 o738 b2340 b2356
5874 S s2356 t620 h
5875 G s2356 t2356
5876 B b2357 s2356
5877 T t2357 o938 b2357 b2302
5878 B b2358 t2357
5879 T t2358 o2 b2345
5880 B b2359 t2358
5881 T t2359 o966 b2358 b4 b2359
5882 B b2360 t2359
5883 T t2360 o559 b2291 b2356
5884 B b2361 t2360
5885 T t2361 o738 b567 b2361
5886 S s2361 t620 h
5887 G s2361 t2361
5888 B b2362 s2361
5889 T t2362 o938 b2362 b2302
5890 B b2363 t2362
5891 T t2363 o937 b2363 b4 b2359
5892 B b2364 t2363
5893 T t2364 o b2364 b4
5894 B b2365 t2364
5895 T t2365 o b2360 b2365
5896 B b2366 t2365
5897 T t2366 o936 b2345 b2366
5898 B b2367 t2366
5899 T t2367 o936 b2360 b4
5900 B b2368 t2367
5901 T t2368 o990 b935 b2368 b4 b4
5902 B b2369 t2368
5903 P p2369 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 0 thenWT autoT"
5904 O o2369 ext_rule p2369
5905 T t2369 o738 b1991 b567
5906 S s2369 t620 h
5907 G s2369 t2369
5908 B b2370 s2369
5909 T t2370 o938 b2370 b2302
5910 B b2371 t2370
5911 T t2371 o2 b2364
5912 B b2372 t2371
5913 T t2372 o966 b2371 b4 b2372
5914 B b2373 t2372
5915 T t2373 o559 b567 b1917
5916 B b2374 t2373
5917 T t2374 o559 b2291 b2374
5918 B b2375 t2374
5919 T t2375 o738 b567 b2375
5920 S s2375 t620 h
5921 G s2375 t2375
5922 B b2376 s2375
5923 T t2376 o938 b2376 b2302
5924 B b2377 t2376
5925 T t2377 o937 b2377 b4 b2372
5926 B b2378 t2377
5927 T t2378 o559 b2327 b1917
5928 B b2379 t2378
5929 T t2379 o559 b2291 b2379
5930 B b2380 t2379 v
5931 T t2380 o711 b2380
5932 S s2380 t620 h
5933 G s2380 t2380
5934 B b2381 s2380
5935 T t2381 o938 b2381 b2302
5936 B b2382 t2381
5937 B b2383 t2379
5938 T t2383 o738 b567 b2383
5939 B b2384 t2383 v
5940 T t2384 o976 b2384
5941 S s2384 t620 h
5942 G s2384 t2384
5943 B b2385 s2384
5944 T t2385 o938 b2385 b2302
5945 B b2386 t2385
5946 T t2386 o973 b2386 b983 b2372
5947 B b2387 t2386
5948 T t2387 o2 b2387
5949 B b2388 t2387
5950 T t2388 o973 b2382 b4 b2388
5951 B b2389 t2388
5952 T t2389 o b2389 b4
5953 B b2390 t2389
5954 T t2390 o b2378 b2390
5955 B b2391 t2390
5956 T t2391 o b2373 b2391
5957 B b2392 t2391
5958 T t2392 o936 b2364 b2392
5959 B b2393 t2392
5960 T t2393 o936 b2373 b4
5961 B b2394 t2393
5962 T t2394 o990 b935 b2394 b4 b4
5963 B b2395 t2394
5964 P p2395 String "setSubstT << equal{op{id; 'b}; 'b} >> 0 thenWT autoT"
5965 O o2395 ext_rule p2395
5966 T t2395 o738 b2374 b1917
5967 S s2395 t620 h
5968 G s2395 t2395
5969 B b2396 s2395
5970 T t2396 o938 b2396 b2302
5971 B b2397 t2396
5972 T t2397 o2 b2378
5973 B b2398 t2397
5974 T t2398 o966 b2397 b4 b2398
5975 B b2399 t2398
5976 T t2399 o559 b2291 b1917
5977 B b2400 t2399
5978 T t2400 o738 b567 b2400
5979 S s2400 t620 h
5980 G s2400 t2400
5981 B b2401 s2400
5982 T t2401 o938 b2401 b2302
5983 B b2402 t2401
5984 T t2402 o937 b2402 b4 b2398
5985 B b2403 t2402
5986 T t2403 o b2403 b4
5987 B b2404 t2403
5988 T t2404 o b2399 b2404
5989 B b2405 t2404
5990 T t2405 o936 b2378 b2405
5991 B b2406 t2405
5992 T t2406 o936 b2399 b4
5993 B b2407 t2406
5994 T t2407 o990 b935 b2407 b4 b4
5995 B b2408 t2407
5996 P p2408 String "setSubstT << equal{op{inv{'b}; 'b}; id} >> 0 thenT autoT"
5997 O o2408 ext_rule p2408
5998 T t2408 o936 b2403 b4
5999 B b2409 t2408
6000 T t2409 o2408 b935 b2409 b4 b4
6001 B b2410 t2409
6002 T t2410 o b2410 b4
6003 B b2411 t2410
6004 T t2411 o b2408 b2411
6005 B b2412 t2411
6006 T t2412 o2395 b935 b2406 b2412 b4
6007 B b2413 t2412
6008 P p2413 String "rwh unfold_fun_set 0 thenT dT 0"
6009 O o2413 ext_rule p2413
6010 NItt_equal Itt_equal Itt_equal NIL
6011 NItt_equal!type type type Itt_equal
6012 O o2414 type
6013 T t2414 o2414 b1186
6014 S s2414 t637 h
6015 G s2414 t2414
6016 B b2414 s2414
6017 T t2415 o938 b2414 b2302
6018 B b2415 t2415
6019 T t2416 o559 b560 b1917
6020 B b2416 t2416
6021 T t2417 o559 b2291 b2416
6022 B b2417 t2417
6023 T t2418 o559 b561 b1917
6024 B b2418 t2418
6025 T t2419 o559 b2291 b2418
6026 B b2419 t2419
6027 T t2420 o738 b2417 b2419
6028 B b2420 t2420
6029 T t2421 o1177 b1347 b2420
6030 B b2421 t2421 s2
6031 T t2422 o1185 b1186 b2421
6032 B b2422 t2422 s1
6033 T t2423 o1185 b1186 b2422
6034 S s2423 t620 h
6035 G s2423 t2423
6036 B b2423 s2423
6037 T t2424 o938 b2423 b2302
6038 B b2424 t2424
6039 T t2425 o2 b2389
6040 B b2425 t2425
6041 T t2426 o973 b2424 b4 b2425
6042 B b2426 t2426
6043 T t2427 o2 b2426
6044 B b2427 t2427
6045 T t2428 o973 b2415 b4 b2427
6046 B b2428 t2428
6047 S s2428 t620 h h1344
6048 G s2428 t2422
6049 B b2429 s2428
6050 T t2429 o938 b2429 b2302
6051 B b2430 t2429
6052 T t2430 o937 b2430 b4 b2427
6053 B b2431 t2430
6054 T t2431 o b2431 b4
6055 B b2432 t2431
6056 T t2432 o b2428 b2432
6057 B b2433 t2432
6058 T t2433 o936 b2389 b2433
6059 B b2434 t2433
6060 T t2434 o936 b2428 b4
6061 B b2435 t2434
6062 T t2435 o990 b935 b2435 b4 b4
6063 B b2436 t2435
6064 P p2436 String "dT 0"
6065 O o2436 ext_rule p2436
6066 S s2436 t637 h h1344
6067 G s2436 t2414
6068 B b2437 s2436
6069 T t2437 o938 b2437 b2302
6070 B b2438 t2437
6071 T t2438 o2 b2431
6072 B b2439 t2438
6073 T t2439 o973 b2438 b4 b2439
6074 B b2440 t2439
6075 S s2440 t620 h h1344 h1224
6076 G s2440 t2421
6077 B b2441 s2440
6078 T t2441 o938 b2441 b2302
6079 B b2442 t2441
6080 T t2442 o937 b2442 b4 b2439
6081 B b2443 t2442
6082 T t2443 o b2443 b4
6083 B b2444 t2443
6084 T t2444 o b2440 b2444
6085 B b2445 t2444
6086 T t2445 o936 b2431 b2445
6087 B b2446 t2445
6088 T t2446 o936 b2440 b4
6089 B b2447 t2446
6090 T t2447 o990 b935 b2447 b4 b4
6091 B b2448 t2447
6092 T t2448 o2414 b1347
6093 S s2448 t637 h h1344 h1224
6094 G s2448 t2448
6095 B b2449 s2448
6096 T t2449 o938 b2449 b2302
6097 B b2450 t2449
6098 T t2450 o2 b2443
6099 B b2451 t2450
6100 T t2451 o973 b2450 b4 b2451
6101 B b2452 t2451