/[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 3379 - (show annotations) (download)
Fri Sep 14 07:00:13 2001 UTC (19 years, 10 months ago) by xiny
File size: 103995 byte(s)
Definition of algebraic group.

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 2358
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 O o221 type_lid p221 p218
604 T t222 o221 b220
605 B b222 t222
606 T t223 o b222 b4
607 B b223 t223
608 T t224 o b221 b223
609 B b224 t224
610 T t225 o218 b224
611 B b225 t225
612 T t226 o213 b217 b225
613 B b226 t226
614 P p226 String cache
615 O o226 resource p226
616 P p227 Number 1424
617 P p228 Number 1434
618 O o228 type_lid p227 p228
619 P p229 String cache_rule
620 O o229 type_lid p229
621 T t229 o229
622 B b229 t229
623 T t230 o228 b229
624 B b230 t230
625 P p230 Number 1436
626 P p231 Number 1441
627 O o231 type_lid p230 p231
628 O o232 type_lid p226
629 T t232 o232
630 B b232 t232
631 T t233 o231 b232
632 B b233 t233
633 T t234 o226 b230 b233
634 B b234 t234
635 P p234 String elim
636 O o234 resource p234
637 P p235 Number 1761
638 P p236 Number 1783
639 O o236 type_prod p235 p236
640 P p237 Number 1765
641 O o237 type_lid p235 p237
642 P p238 String term
643 O o238 type_lid p238
644 T t238 o238
645 B b238 t238
646 T t239 o237 b238
647 B b239 t239
648 NOcaml!type_fun type_fun type_fun Ocaml
649 P p239 Number 1769
650 P p240 Number 1782
651 O o240 type_fun p239 p240
652 P p241 Number 1772
653 O o241 type_lid p239 p241
654 P p242 String int
655 O o242 type_lid p242
656 T t242 o242
657 B b242 t242
658 T t243 o241 b242
659 B b243 t243
660 P p243 Number 1776
661 O o243 type_lid p243 p240
662 T t244 o243 b220
663 B b244 t244
664 T t245 o240 b243 b244
665 B b245 t245
666 T t246 o b245 b4
667 B b246 t246
668 T t247 o b239 b246
669 B b247 t247
670 T t248 o236 b247
671 B b248 t248
672 P p248 Number 1785
673 P p249 Number 1798
674 O o249 type_fun p248 p249
675 P p250 Number 1788
676 O o250 type_lid p248 p250
677 T t250 o250 b242
678 B b250 t250
679 P p251 Number 1792
680 O o251 type_lid p251 p249
681 T t251 o251 b220
682 B b251 t251
683 T t252 o249 b250 b251
684 B b252 t252
685 T t253 o234 b248 b252
686 B b253 t253
687 P p253 String eqcd
688 O o253 resource p253
689 P p254 Number 6168
690 P p255 Number 6181
691 O o255 type_prod p254 p255
692 P p256 Number 6172
693 O o256 type_lid p254 p256
694 T t256 o256 b238
695 B b256 t256
696 P p257 Number 6175
697 O o257 type_lid p257 p255
698 T t257 o257 b220
699 B b257 t257
700 T t258 o b257 b4
701 B b258 t258
702 T t259 o b256 b258
703 B b259 t259
704 T t260 o255 b259
705 B b260 t260
706 P p260 Number 6183
707 P p261 Number 6189
708 O o261 type_lid p260 p261
709 T t261 o261 b220
710 B b261 t261
711 T t262 o253 b260 b261
712 B b262 t262
713 P p262 String intro
714 O o262 resource p262
715 P p263 Number 1815
716 P p264 Number 1852
717 O o264 type_prod p263 p264
718 P p265 Number 1819
719 O o265 type_lid p263 p265
720 T t265 o265 b238
721 B b265 t265
722 P p266 Number 1823
723 P p267 Number 1851
724 O o267 type_prod p266 p267
725 P p268 Number 1829
726 O o268 type_lid p266 p268
727 P p269 String string
728 O o269 type_lid p269
729 T t269 o269
730 B b269 t269
731 T t270 o268 b269
732 B b270 t270
733 NOcaml!type_apply type_apply type_apply Ocaml
734 P p270 Number 1832
735 P p271 Number 1842
736 O o271 type_apply p270 p271
737 P p272 Number 1836
738 O o272 type_lid p272 p271
739 P p273 String option
740 O o273 type_lid p273
741 T t273 o273
742 B b273 t273
743 T t274 o272 b273
744 B b274 t274
745 P p274 Number 1835
746 O o274 type_lid p270 p274
747 T t275 o274 b242
748 B b275 t275
749 T t276 o271 b274 b275
750 B b276 t276
751 P p276 Number 1845
752 O o276 type_lid p276 p267
753 T t277 o276 b220
754 B b277 t277
755 T t278 o b277 b4
756 B b278 t278
757 T t279 o b276 b278
758 B b279 t279
759 T t280 o b270 b279
760 B b280 t280
761 T t281 o267 b280
762 B b281 t281
763 T t282 o b281 b4
764 B b282 t282
765 T t283 o b265 b282
766 B b283 t283
767 T t284 o264 b283
768 B b284 t284
769 P p284 Number 1854
770 P p285 Number 1860
771 O o285 type_lid p284 p285
772 T t285 o285 b220
773 B b285 t285
774 T t286 o262 b284 b285
775 B b286 t286
776 P p286 String reduce
777 O o286 resource p286
778 P p287 Number 2920
779 P p288 Number 2931
780 O o288 type_prod p287 p288
781 P p289 Number 2924
782 O o289 type_lid p287 p289
783 T t289 o289 b238
784 B b289 t289
785 P p290 Number 2927
786 O o290 type_lid p290 p288
787 P p291 String conv
788 O o291 type_lid p291
789 T t291 o291
790 B b291 t291
791 T t292 o290 b291
792 B b292 t292
793 T t293 o b292 b4
794 B b293 t293
795 T t294 o b289 b293
796 B b294 t294
797 T t295 o288 b294
798 B b295 t295
799 P p295 Number 2933
800 P p296 Number 2937
801 O o296 type_lid p295 p296
802 T t296 o296 b291
803 B b296 t296
804 T t297 o286 b295 b296
805 B b297 t297
806 P p297 String squash
807 O o297 resource p297
808 P p298 Number 4017
809 P p299 Number 4028
810 O o299 type_lid p298 p299
811 P p300 String squash_info
812 O o300 type_lid p300
813 T t300 o300
814 B b300 t300
815 T t301 o299 b300
816 B b301 t301
817 P p301 Number 4030
818 P p302 Number 4043
819 O o302 type_fun p301 p302
820 P p303 Number 4033
821 O o303 type_lid p301 p303
822 T t303 o303 b242
823 B b303 t303
824 P p304 Number 4037
825 O o304 type_lid p304 p302
826 T t304 o304 b220
827 B b304 t304
828 T t305 o302 b303 b304
829 B b305 t305
830 T t306 o297 b301 b305
831 B b306 t306
832 P p306 String sub
833 O o306 resource p306
834 P p307 Number 4871
835 P p308 Number 4888
836 O o308 type_lid p307 p308
837 P p309 String sub_resource_info
838 O o309 type_lid p309
839 T t309 o309
840 B b309 t309
841 T t310 o308 b309
842 B b310 t310
843 P p310 Number 4890
844 P p311 Number 4896
845 O o311 type_lid p310 p311
846 T t311 o311 b220
847 B b311 t311
848 T t312 o306 b310 b311
849 B b312 t312
850 P p312 String toploop
851 O o312 resource p312
852 P p313 Number 2445
853 P p314 Number 2467
854 O o314 type_prod p313 p314
855 P p315 Number 2451
856 O o315 type_lid p313 p315
857 T t315 o315 b269
858 B b315 t315
859 P p316 Number 2454
860 P p317 Number 2460
861 O o317 type_lid p316 p317
862 T t317 o317 b269
863 B b317 t317
864 P p318 Number 2463
865 O o318 type_lid p318 p314
866 P p319 String expr
867 O o319 type_lid p319
868 T t319 o319
869 B b319 t319
870 T t320 o318 b319
871 B b320 t320
872 T t321 o b320 b4
873 B b321 t321
874 T t322 o b317 b321
875 B b322 t322
876 T t323 o b315 b322
877 B b323 t323
878 T t324 o314 b323
879 B b324 t324
880 P p324 Number 2469
881 P p325 Number 2478
882 O o325 type_lid p324 p325
883 P p326 String top_table
884 O o326 type_lid p326
885 T t326 o326
886 B b326 t326
887 T t327 o325 b326
888 B b327 t327
889 T t328 o312 b324 b327
890 B b328 t328
891 P p328 String typeinf
892 O o328 resource p328
893 P p329 Number 2151
894 P p330 Number 2172
895 O o330 type_lid p329 p330
896 P p331 String typeinf_resource_info
897 O o331 type_lid p331
898 T t331 o331
899 B b331 t331
900 T t332 o330 b331
901 B b332 t332
902 P p332 Number 2174
903 P p333 Number 2186
904 O o333 type_lid p332 p333
905 P p334 String typeinf_func
906 O o334 type_lid p334
907 T t334 o334
908 B b334 t334
909 T t335 o333 b334
910 B b335 t335
911 T t336 o328 b332 b335
912 B b336 t336
913 P p336 String typeinf_subst
914 O o336 resource p336
915 P p337 Number 1825
916 P p338 Number 1843
917 O o338 type_lid p337 p338
918 P p339 String typeinf_subst_info
919 O o339 type_lid p339
920 T t339 o339
921 B b339 t339
922 T t340 o338 b339
923 B b340 t340
924 P p340 Number 1862
925 O o340 type_lid p276 p340
926 P p341 String typeinf_subst_fun
927 O o341 type_lid p341
928 T t341 o341
929 B b341 t341
930 T t342 o340 b341
931 B b342 t342
932 T t343 o336 b340 b342
933 B b343 t343
934 T t344 o b343 b4
935 B b344 t344
936 T t345 o b336 b344
937 B b345 t345
938 T t346 o b328 b345
939 B b346 t346
940 T t347 o b312 b346
941 B b347 t347
942 T t348 o b306 b347
943 B b348 t348
944 T t349 o b297 b348
945 B b349 t349
946 T t350 o b286 b349
947 B b350 t350
948 T t351 o b262 b350
949 B b351 t351
950 T t352 o b253 b351
951 B b352 t352
952 T t353 o b234 b352
953 B b353 t353
954 T t354 o b226 b353
955 B b354 t354
956 T t355 o2 b5 b213 b354
957 B b355 t355
958 T t356 o1 b355
959 B b356 t356
960 P p356 Number 20
961 P p357 Number 42
962 O o357 location p356 p357
963 P p358 String Czf_itt_member
964 O o358 parent p358
965 T t358 o358
966 B b358 t358
967 T t359 o b358 b4
968 B b359 t359
969 P p359 String Czf_itt_eq
970 O o359 parent p359
971 T t360 o359
972 B b360 t360
973 T t361 o b360 b4
974 B b361 t361
975 T t362 o b361 b4
976 B b362 t362
977 T t363 o b359 b362
978 B b363 t363
979 T t364 o2 b359 b363 b354
980 B b364 t364
981 T t365 o357 b364
982 B b365 t365
983 P p365 Number 43
984 P p366 Number 61
985 O o366 location p365 p366
986 T t366 o2 b361 b4 b354
987 B b366 t366
988 T t367 o366 b366
989 B b367 t367
990 P p367 Number 62
991 P p368 Number 82
992 O o368 location p367 p368
993 P p369 String Czf_itt_dall
994 O o369 parent p369
995 T t369 o369
996 B b369 t369
997 T t370 o b369 b4
998 B b370 t370
999 P p370 String Czf_itt_set_ind
1000 O o370 parent p370
1001 T t371 o370
1002 B b371 t371
1003 T t372 o b371 b4
1004 B b372 t372
1005 P p372 String Czf_itt_all
1006 O o372 parent p372
1007 T t373 o372
1008 B b373 t373
1009 T t374 o b373 b4
1010 B b374 t374
1011 P p374 String Czf_itt_sep
1012 O o374 parent p374
1013 T t375 o374
1014 B b375 t375
1015 T t376 o b375 b4
1016 B b376 t376
1017 T t377 o b376 b4
1018 B b377 t377
1019 T t378 o b374 b377
1020 B b378 t378
1021 T t379 o b372 b378
1022 B b379 t379
1023 T t380 o b370 b379
1024 B b380 t380
1025 T t381 o2 b370 b380 b354
1026 B b381 t381
1027 T t382 o368 b381
1028 B b382 t382
1029 P p382 Number 83
1030 P p383 Number 102
1031 O o383 location p382 p383
1032 P p384 String Czf_itt_and
1033 O o384 parent p384
1034 T t384 o384
1035 B b384 t384
1036 T t385 o b384 b4
1037 B b385 t385
1038 T t386 o b385 b4
1039 B b386 t386
1040 T t387 o2 b385 b386 b354
1041 B b387 t387
1042 T t388 o383 b387
1043 B b388 t388
1044 P p388 Number 104
1045 P p389 Number 115
1046 O o389 location p388 p389
1047 NSummary!summary_item summary_item summary_item Summary
1048 O o390 summary_item
1049 NOcaml!str_open str_open str_open Ocaml
1050 O o391 str_open p388 p389
1051 NOcaml!string string string Ocaml
1052 P p391 String Printf
1053 O o392 string p391
1054 T t392 o392
1055 B b392 t392
1056 T t393 o b392 b4
1057 B b393 t393
1058 T t394 o391 b393
1059 B b394 t394
1060 T t395 o390 b394
1061 B b395 t395
1062 T t396 o389 b395
1063 B b396 t396
1064 P p396 Number 116
1065 P p397 Number 129
1066 O o397 location p396 p397
1067 O o398 str_open p396 p397
1068 P p398 String Mp_debug
1069 O o399 string p398
1070 T t399 o399
1071 B b399 t399
1072 T t400 o b399 b4
1073 B b400 t400
1074 T t401 o398 b400
1075 B b401 t401
1076 T t402 o390 b401
1077 B b402 t402
1078 T t403 o397 b402
1079 B b403 t403
1080 P p403 Number 130
1081 P p404 Number 159
1082 O o404 location p403 p404
1083 O o405 str_open p403 p404
1084 P p405 String Refiner
1085 O o406 string p405
1086 T t406 o406
1087 B b406 t406
1088 P p406 String TermType
1089 O o407 string p406
1090 T t407 o407
1091 B b407 t407
1092 T t408 o b407 b4
1093 B b408 t408
1094 T t409 o b406 b408
1095 B b409 t409
1096 T t410 o b406 b409
1097 B b410 t410
1098 T t411 o405 b410
1099 B b411 t411
1100 T t412 o390 b411
1101 B b412 t412
1102 T t413 o404 b412
1103 B b413 t413
1104 P p413 Number 160
1105 P p414 Number 185
1106 O o414 location p413 p414
1107 O o415 str_open p413 p414
1108 P p415 String Term
1109 O o416 string p415
1110 T t416 o416
1111 B b416 t416
1112 T t417 o b416 b4
1113 B b417 t417
1114 T t418 o b406 b417
1115 B b418 t418
1116 T t419 o b406 b418
1117 B b419 t419
1118 T t420 o415 b419
1119 B b420 t420
1120 T t421 o390 b420
1121 B b421 t421
1122 T t422 o414 b421
1123 B b422 t422
1124 P p422 Number 186
1125 P p423 Number 213
1126 O o423 location p422 p423
1127 O o424 str_open p422 p423
1128 P p424 String TermOp
1129 O o425 string p424
1130 T t425 o425
1131 B b425 t425
1132 T t426 o b425 b4
1133 B b426 t426
1134 T t427 o b406 b426
1135 B b427 t427
1136 T t428 o b406 b427
1137 B b428 t428
1138 T t429 o424 b428
1139 B b429 t429
1140 T t430 o390 b429
1141 B b430 t430
1142 T t431 o423 b430
1143 B b431 t431
1144 P p431 Number 214
1145 P p432 Number 243
1146 O o432 location p431 p432
1147 O o433 str_open p431 p432
1148 P p433 String TermAddr
1149 O o434 string p433
1150 T t434 o434
1151 B b434 t434
1152 T t435 o b434 b4
1153 B b435 t435
1154 T t436 o b406 b435
1155 B b436 t436
1156 T t437 o b406 b436
1157 B b437 t437
1158 T t438 o433 b437
1159 B b438 t438
1160 T t439 o390 b438
1161 B b439 t439
1162 T t440 o432 b439
1163 B b440 t440
1164 P p440 Number 244
1165 P p441 Number 272
1166 O o441 location p440 p441
1167 O o442 str_open p440 p441
1168 P p442 String TermMan
1169 O o443 string p442
1170 T t443 o443
1171 B b443 t443
1172 T t444 o b443 b4
1173 B b444 t444
1174 T t445 o b406 b444
1175 B b445 t445
1176 T t446 o b406 b445
1177 B b446 t446
1178 T t447 o442 b446
1179 B b447 t447
1180 T t448 o390 b447
1181 B b448 t448
1182 T t449 o441 b448
1183 B b449 t449
1184 P p449 Number 273
1185 P p450 Number 303
1186 O o450 location p449 p450
1187 O o451 str_open p449 p450
1188 P p451 String TermSubst
1189 O o452 string p451
1190 T t452 o452
1191 B b452 t452
1192 T t453 o b452 b4
1193 B b453 t453
1194 T t454 o b406 b453
1195 B b454 t454
1196 T t455 o b406 b454
1197 B b455 t455
1198 T t456 o451 b455
1199 B b456 t456
1200 T t457 o390 b456
1201 B b457 t457
1202 T t458 o450 b457
1203 B b458 t458
1204 P p458 Number 304
1205 P p459 Number 331
1206 O o459 location p458 p459
1207 O o460 str_open p458 p459
1208 P p460 String Refine
1209 O o461 string p460
1210 T t461 o461
1211 B b461 t461
1212 T t462 o b461 b4
1213 B b462 t462
1214 T t463 o b406 b462
1215 B b463 t463
1216 T t464 o b406 b463
1217 B b464 t464
1218 T t465 o460 b464
1219 B b465 t465
1220 T t466 o390 b465
1221 B b466 t466
1222 T t467 o459 b466
1223 B b467 t467
1224 P p467 Number 332
1225 P p468 Number 364
1226 O o468 location p467 p468
1227 O o469 str_open p467 p468
1228 P p469 String RefineError
1229 O o470 string p469
1230 T t470 o470
1231 B b470 t470
1232 T t471 o b470 b4
1233 B b471 t471
1234 T t472 o b406 b471
1235 B b472 t472
1236 T t473 o b406 b472
1237 B b473 t473
1238 T t474 o469 b473
1239 B b474 t474
1240 T t475 o390 b474
1241 B b475 t475
1242 T t476 o468 b475
1243 B b476 t476
1244 P p476 Number 365
1245 P p477 Number 381
1246 O o477 location p476 p477
1247 O o478 str_open p476 p477
1248 P p478 String Mp_resource
1249 O o479 string p478
1250 T t479 o479
1251 B b479 t479
1252 T t480 o b479 b4
1253 B b480 t480
1254 T t481 o478 b480
1255 B b481 t481
1256 T t482 o390 b481
1257 B b482 t482
1258 T t483 o477 b482
1259 B b483 t483
1260 P p483 Number 382
1261 P p484 Number 399
1262 O o484 location p483 p484
1263 O o485 str_open p483 p484
1264 P p485 String Simple_print
1265 O o486 string p485
1266 T t486 o486
1267 B b486 t486
1268 T t487 o b486 b4
1269 B b487 t487
1270 T t488 o485 b487
1271 B b488 t488
1272 T t489 o390 b488
1273 B b489 t489
1274 T t490 o484 b489
1275 B b490 t490
1276 P p490 Number 401
1277 P p491 Number 417
1278 O o491 location p490 p491
1279 O o492 str_open p490 p491
1280 P p492 String Tactic_type
1281 O o493 string p492
1282 T t493 o493
1283 B b493 t493
1284 T t494 o b493 b4
1285 B b494 t494
1286 T t495 o492 b494
1287 B b495 t495
1288 T t496 o390 b495
1289 B b496 t496
1290 T t497 o491 b496
1291 B b497 t497
1292 P p497 Number 418
1293 P p498 Number 444
1294 O o498 location p497 p498
1295 O o499 str_open p497 p498
1296 P p499 String Tacticals
1297 O o500 string p499
1298 T t500 o500
1299 B b500 t500
1300 T t501 o b500 b4
1301 B b501 t501
1302 T t502 o b493 b501
1303 B b502 t502
1304 T t503 o499 b502
1305 B b503 t503
1306 T t504 o390 b503
1307 B b504 t504
1308 T t505 o498 b504
1309 B b505 t505
1310 P p505 Number 445
1311 P p506 Number 469
1312 O o506 location p505 p506
1313 O o507 str_open p505 p506
1314 P p507 String Sequent
1315 O o508 string p507
1316 T t508 o508
1317 B b508 t508
1318 T t509 o b508 b4
1319 B b509 t509
1320 T t510 o b493 b509
1321 B b510 t510
1322 T t511 o507 b510
1323 B b511 t511
1324 T t512 o390 b511
1325 B b512 t512
1326 T t513 o506 b512
1327 B b513 t513
1328 P p513 Number 470
1329 P p514 Number 500
1330 O o514 location p513 p514
1331 O o515 str_open p513 p514
1332 P p515 String Conversionals
1333 O o516 string p515
1334 T t516 o516
1335 B b516 t516
1336 T t517 o b516 b4
1337 B b517 t517
1338 T t518 o b493 b517
1339 B b518 t518
1340 T t519 o515 b518
1341 B b519 t519
1342 T t520 o390 b519
1343 B b520 t520
1344 T t521 o514 b520
1345 B b521 t521
1346 P p521 Number 501
1347 P p522 Number 511
1348 O o522 location p521 p522
1349 O o523 str_open p521 p522
1350 O o524 string p131
1351 T t524 o524
1352 B b524 t524
1353 T t525 o b524 b4
1354 B b525 t525
1355 T t526 o523 b525
1356 B b526 t526
1357 T t527 o390 b526
1358 B b527 t527
1359 T t528 o522 b527
1360 B b528 t528
1361 P p528 Number 512
1362 P p529 Number 520
1363 O o529 location p528 p529
1364 O o530 str_open p528 p529
1365 O o531 string p129
1366 T t531 o531
1367 B b531 t531
1368 T t532 o b531 b4
1369 B b532 t532
1370 T t533 o530 b532
1371 B b533 t533
1372 T t534 o390 b533
1373 B b534 t534
1374 T t535 o529 b534
1375 B b535 t535
1376 P p535 Number 522
1377 P p536 Number 539
1378 O o536 location p535 p536
1379 O o537 str_open p535 p536
1380 O o538 string p119
1381 T t538 o538
1382 B b538 t538
1383 T t539 o b538 b4
1384 B b539 t539
1385 T t540 o537 b539
1386 B b540 t540
1387 T t541 o390 b540
1388 B b541 t541
1389 T t542 o536 b541
1390 B b542 t542
1391 P p542 Number 540
1392 P p543 Number 561
1393 O o543 location p542 p543
1394 O o544 str_open p542 p543
1395 O o545 string p121
1396 T t545 o545
1397 B b545 t545
1398 T t546 o b545 b4
1399 B b546 t546
1400 T t547 o544 b546
1401 B b547 t547
1402 T t548 o390 b547
1403 B b548 t548
1404 T t549 o543 b548
1405 B b549 t549
1406 P p549 Number 563
1407 P p550 Number 574
1408 O o550 location p549 p550
1409 NSummary!opname opname opname Summary
1410 P p551 String car
1411 O o551 opname p551
1412 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1413 NCzf_itt_group!car car car Czf_itt_group
1414 O o552 car
1415 T t552 o552
1416 B b552 t552
1417 T t553 o551 b552
1418 B b553 t553
1419 T t554 o550 b553
1420 B b554 t554
1421 P p554 Number 615
1422 P p555 Number 635
1423 O o555 location p554 p555
1424 P p556 String op
1425 O o556 opname p556
1426 NCzf_itt_group!op op op Czf_itt_group
1427 O o557 op
1428 Nvar var var NIL
1429 P p557 Var s1
1430 O o558 var p557
1431 T t558 o558
1432 B b558 t558
1433 P p558 Var s2
1434 O o559 var p558
1435 T t559 o559
1436 B b559 t559
1437 T t560 o557 b558 b559
1438 B b560 t560
1439 T t561 o556 b560
1440 B b561 t561
1441 T t562 o555 b561
1442 B b562 t562
1443 P p562 Number 636
1444 P p563 Number 646
1445 O o563 location p562 p563
1446 P p564 String id
1447 O o564 opname p564
1448 NCzf_itt_group!id id id Czf_itt_group
1449 O o565 id
1450 T t565 o565
1451 B b565 t565
1452 T t566 o564 b565
1453 B b566 t566
1454 T t567 o563 b566
1455 B b567 t567
1456 P p567 Number 647
1457 P p568 Number 662
1458 O o568 location p567 p568
1459 P p569 String inv
1460 O o569 opname p569
1461 NCzf_itt_group!inv inv inv Czf_itt_group
1462 O o570 inv
1463 P p570 Var s
1464 O o571 var p570
1465 T t571 o571
1466 B b571 t571
1467 T t572 o570 b571
1468 B b572 t572
1469 T t573 o569 b572
1470 B b573 t573
1471 T t574 o568 b573
1472 B b574 t574
1473 P p574 Number 664
1474 P p575 Number 713
1475 O o575 location p574 p575
1476 NSummary!dform dform dform Summary
1477 P p576 String car_df
1478 O o576 dform p576
1479 NSummary!except_mode_df except_mode_df except_mode_df Summary
1480 P p577 String src
1481 O o577 except_mode_df p577
1482 T t577 o577
1483 B b577 t577
1484 T t578 o b577 b4
1485 B b578 t578
1486 NSummary!df_term df_term df_term Summary
1487 O o578 df_term
1488 NPerv!string string578 string Perv
1489 P p578 String S
1490 O o579 string578 p578
1491 T t579 o579
1492 B b579 t579
1493 T t580 o b579 b4
1494 B b580 t580
1495 T t581 o578 b580
1496 B b581 t581
1497 T t582 o576 b578 b552 b581
1498 B b582 t582
1499 T t583 o575 b582
1500 B b583 t583
1501 P p583 Number 715
1502 P p584 Number 762
1503 O o584 location p583 p584
1504 P p585 String id_df
1505 O o585 dform p585
1506 P p586 String e
1507 O o586 string578 p586
1508 T t586 o586
1509 B b586 t586
1510 T t587 o b586 b4
1511 B b587 t587
1512 T t588 o578 b587
1513 B b588 t588
1514 T t589 o585 b578 b565 b588
1515 B b589 t589
1516 T t590 o584 b589
1517 B b590 t590
1518 P p590 Number 765
1519 P p591 Number 866
1520 O o591 location p590 p591
1521 P p592 String op_df
1522 O o592 dform p592
1523 NSummary!parens_df parens_df parens_df Summary
1524 O o593 parens_df
1525 T t593 o593
1526 B b593 t593
1527 T t594 o b593 b4
1528 B b594 t594
1529 T t595 o b577 b594
1530 B b595 t595
1531 Nslot slot slot NIL
1532 P p595 String le
1533 O o595 slot p595
1534 T t596 o595 b558
1535 B b596 t596
1536 P p596 String " * "
1537 O o596 string578 p596
1538 T t597 o596
1539 B b597 t597
1540 T t598 o595 b559
1541 B b598 t598
1542 T t599 o b598 b4
1543 B b599 t599
1544 T t600 o b597 b599
1545 B b600 t600
1546 T t601 o b596 b600
1547 B b601 t601
1548 T t602 o578 b601
1549 B b602 t602
1550 T t603 o592 b595 b560 b602
1551 B b603 t603
1552 T t604 o591 b603
1553 B b604 t604
1554 P p604 Number 868
1555 P p605 Number 946
1556 O o605 location p604 p605
1557 P p606 String inv_df
1558 O o606 dform p606
1559 T t606 o595 b571
1560 B b606 t606
1561 P p607 String '
1562 O o607 string578 p607
1563 T t607 o607
1564 B b607 t607
1565 T t608 o b607 b4
1566 B b608 t608
1567 T t609 o b606 b608
1568 B b609 t609
1569 T t610 o578 b609
1570 B b610 t610
1571 T t611 o606 b595 b572 b610
1572 B b611 t611
1573 T t612 o605 b611
1574 B b612 t612
1575 P p612 Number 961
1576 P p613 Number 1037
1577 O o613 location p612 p613
1578 NSummary!rule rule rule Summary
1579 P p614 String car_wf
1580 O o614 rule p614
1581 NSummary!context_param context_param context_param Summary
1582 P p615 String H
1583 O o615 context_param p615
1584 T t615 o615
1585 B b615 t615
1586 T t616 o b615 b4
1587 B b616 t616
1588 NSummary!meta_theorem meta_theorem meta_theorem Summary
1589 O o616 meta_theorem
1590 P p616 Var ext
1591 O o617 var p616
1592 T t617 o617
1593 B b617 t617
1594 T t618 o b617 b4
1595 C h H
1596 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1597 NCzf_itt_set!isset isset isset Czf_itt_set
1598 O o618 isset
1599 T t619 o618 b552
1600 S s t618 h
1601 G s t619
1602 B b619 s
1603 T t620 o616 b619
1604 B b620 t620
1605 NSummary!incomplete incomplete incomplete Summary
1606 O o620 incomplete
1607 T t621 o620
1608 B b621 t621
1609 NSummary!resource_defs resource_defs resource_defs Summary
1610 P p621 Number 983
1611 P p622 Number 990
1612 O o622 resource_defs p621 p622 p262
1613 NOcaml!uid uid uid Ocaml
1614 P p623 Number 988
1615 O o623 uid p623 p622
1616 P p624 String []
1617 O o624 uid p624
1618 T t624 o624
1619 B b624 t624
1620 T t625 o623 b624
1621 B b625 t625
1622 T t626 o b625 b4
1623 B b626 t626
1624 T t627 o622 b626
1625 B b627 t627
1626 T t628 o b627 b4
1627 B b628 t628
1628 T t629 o614 b616 b620 b621 b628
1629 B b629 t629
1630 T t630 o613 b629
1631 B b630 t630
1632 P p630 Number 1039
1633 P p631 Number 1214
1634 O o631 location p630 p631
1635 P p632 String op_wf1
1636 O o632 rule p632
1637 NSummary!meta_implies meta_implies meta_implies Summary
1638 O o633 meta_implies
1639 NBase_trivial Base_trivial Base_trivial NIL
1640 NBase_trivial!squash squash squash Base_trivial
1641 O o634 squash
1642 T t634 o634
1643 B b634 t634
1644 T t635 o b634 b4
1645 T t636 o618 b558
1646 S s636 t635 h
1647 G s636 t636
1648 B b636 s636
1649 T t637 o616 b636
1650 B b637 t637
1651 T t638 o618 b559
1652 S s638 t635 h
1653 G s638 t638
1654 B b638 s638
1655 T t639 o616 b638
1656 B b639 t639
1657 T t640 o618 b560
1658 S s640 t618 h
1659 G s640 t640
1660 B b640 s640
1661 T t641 o616 b640
1662 B b641 t641
1663 T t642 o633 b639 b641
1664 B b642 t642
1665 T t643 o633 b637 b642
1666 B b643 t643
1667 P p643 Number 1061
1668 P p644 Number 1068
1669 O o644 resource_defs p643 p644 p262
1670 P p645 Number 1066
1671 O o645 uid p645 p644
1672 T t645 o645 b624
1673 B b645 t645
1674 T t646 o b645 b4
1675 B b646 t646
1676 T t647 o644 b646
1677 B b647 t647
1678 T t648 o b647 b4
1679 B b648 t648
1680 T t649 o632 b616 b643 b621 b648
1681 B b649 t649
1682 T t650 o631 b649
1683 B b650 t650
1684 P p650 Number 1216
1685 P p651 Number 1486
1686 O o651 location p650 p651
1687 P p652 String op_wf2
1688 O o652 rule p652
1689 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1690 NCzf_itt_member!mem mem mem Czf_itt_member
1691 O o653 mem
1692 T t653 o653 b558 b552
1693 S s653 t618 h
1694 G s653 t653
1695 B b653 s653
1696 T t654 o616 b653
1697 B b654 t654
1698 T t655 o653 b559 b552
1699 S s655 t618 h
1700 G s655 t655
1701 B b655 s655
1702 T t656 o616 b655
1703 B b656 t656
1704 T t657 o653 b560 b552
1705 S s657 t618 h
1706 G s657 t657
1707 B b657 s657
1708 T t658 o616 b657
1709 B b658 t658
1710 T t659 o633 b656 b658
1711 B b659 t659
1712 T t660 o633 b654 b659
1713 B b660 t660
1714 T t661 o633 b639 b660
1715 B b661 t661
1716 T t662 o633 b637 b661
1717 B b662 t662
1718 P p662 Number 1238
1719 P p663 Number 1245
1720 O o663 resource_defs p662 p663 p262
1721 P p664 Number 1243
1722 O o664 uid p664 p663
1723 T t664 o664 b624
1724 B b664 t664
1725 T t665 o b664 b4
1726 B b665 t665
1727 T t666 o663 b665
1728 B b666 t666
1729 T t667 o b666 b4
1730 B b667 t667
1731 T t668 o652 b616 b662 b621 b667
1732 B b668 t668
1733 T t669 o651 b668
1734 B b669 t669
1735 P p669 Number 1488
1736 P p670 Number 1766
1737 O o670 location p669 p670
1738 P p671 String op_eq1
1739 O o671 rule p671
1740 P p672 Var s3
1741 O o672 var p672
1742 T t672 o672
1743 B b672 t672
1744 T t673 o618 b672
1745 S s673 t635 h
1746 G s673 t673
1747 B b673 s673
1748 T t674 o616 b673
1749 B b674 t674
1750 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1751 NCzf_itt_eq!eq eq eq Czf_itt_eq
1752 O o674 eq
1753 T t675 o674 b558 b559
1754 S s675 t618 h
1755 G s675 t675
1756 B b675 s675
1757 T t676 o616 b675
1758 B b676 t676
1759 T t677 o557 b672 b558
1760 B b677 t677
1761 T t678 o557 b672 b559
1762 B b678 t678
1763 T t679 o674 b677 b678
1764 S s679 t618 h
1765 G s679 t679
1766 B b679 s679
1767 T t680 o616 b679
1768 B b680 t680
1769 T t681 o633 b676 b680
1770 B b681 t681
1771 T t682 o633 b674 b681
1772 B b682 t682
1773 T t683 o633 b639 b682
1774 B b683 t683
1775 T t684 o633 b637 b683
1776 B b684 t684
1777 P p684 Number 1510
1778 P p685 Number 1517
1779 O o685 resource_defs p684 p685 p262
1780 P p686 Number 1515
1781 O o686 uid p686 p685
1782 T t686 o686 b624
1783 B b686 t686
1784 T t687 o b686 b4
1785 B b687 t687
1786 T t688 o685 b687
1787 B b688 t688
1788 T t689 o b688 b4
1789 B b689 t689
1790 T t690 o671 b616 b684 b621 b689
1791 B b690 t690
1792 T t691 o670 b690
1793 B b691 t691
1794 P p691 Number 1768
1795 P p692 Number 2046
1796 O o692 location p691 p692
1797 P p693 String op_eq2
1798 O o693 rule p693
1799 T t693 o557 b558 b672
1800 B b693 t693
1801 T t694 o557 b559 b672
1802 B b694 t694
1803 T t695 o674 b693 b694
1804 S s695 t618 h
1805 G s695 t695
1806 B b695 s695
1807 T t696 o616 b695
1808 B b696 t696
1809 T t697 o633 b676 b696
1810 B b697 t697
1811 T t698 o633 b674 b697
1812 B b698 t698
1813 T t699 o633 b639 b698
1814 B b699 t699
1815 T t700 o633 b637 b699
1816 B b700 t700
1817 P p700 Number 1790
1818 P p701 Number 1797
1819 O o701 resource_defs p700 p701 p262
1820 P p702 Number 1795
1821 O o702 uid p702 p701
1822 T t702 o702 b624
1823 B b702 t702
1824 T t703 o b702 b4
1825 B b703 t703
1826 T t704 o701 b703
1827 B b704 t704
1828 T t705 o b704 b4
1829 B b705 t705
1830 T t706 o693 b616 b700 b621 b705
1831 B b706 t706
1832 T t707 o692 b706
1833 B b707 t707
1834 P p707 Number 2048
1835 P p708 Number 2181
1836 O o708 location p707 p708
1837 P p709 String op_fun1
1838 O o709 rule p709
1839 T t709 o618 b571
1840 S s709 t635 h
1841 G s709 t709
1842 B b709 s709
1843 T t710 o616 b709
1844 B b710 t710
1845 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1846 O o710 fun_set
1847 P p710 Var z
1848 O o711 var p710
1849 T t711 o711
1850 B b711 t711
1851 T t712 o557 b711 b571
1852 B b712 t712 z
1853 T t713 o710 b712
1854 S s713 t618 h
1855 G s713 t713
1856 B b713 s713
1857 T t714 o616 b713
1858 B b714 t714
1859 T t715 o633 b710 b714
1860 B b715 t715
1861 P p715 Number 2071
1862 P p716 Number 2078
1863 O o716 resource_defs p715 p716 p262
1864 P p717 Number 2076
1865 O o717 uid p717 p716
1866 T t717 o717 b624
1867 B b717 t717
1868 T t718 o b717 b4
1869 B b718 t718
1870 T t719 o716 b718
1871 B b719 t719
1872 T t720 o b719 b4
1873 B b720 t720
1874 T t721 o709 b616 b715 b621 b720
1875 B b721 t721
1876 T t722 o708 b721
1877 B b722 t722
1878 P p722 Number 2183
1879 P p723 Number 2316
1880 O o723 location p722 p723
1881 P p724 String op_fun2
1882 O o724 rule p724
1883 T t724 o557 b571 b711
1884 B b724 t724 z
1885 T t725 o710 b724
1886 S s725 t618 h
1887 G s725 t725
1888 B b725 s725
1889 T t726 o616 b725
1890 B b726 t726
1891 T t727 o633 b710 b726
1892 B b727 t727
1893 P p727 Number 2206
1894 P p728 Number 2213
1895 O o728 resource_defs p727 p728 p262
1896 P p729 Number 2211
1897 O o729 uid p729 p728
1898 T t729 o729 b624
1899 B b729 t729
1900 T t730 o b729 b4
1901 B b730 t730
1902 T t731 o728 b730
1903 B b731 t731
1904 T t732 o b731 b4
1905 B b732 t732
1906 T t733 o724 b616 b727 b621 b732
1907 B b733 t733
1908 T t734 o723 b733
1909 B b734 t734
1910 P p734 Number 2506
1911 P p735 Number 2899
1912 O o735 location p734 p735
1913 P p736 String op_assoc1
1914 O o736 rule p736
1915 T t736 o653 b672 b552
1916 S s736 t618 h
1917 G s736 t736
1918 B b736 s736
1919 T t737 o616 b736
1920 B b737 t737
1921 NCzf_itt_eq!equal equal equal Czf_itt_eq
1922 O o737 equal
1923 T t738 o557 b560 b672
1924 B b738 t738
1925 T t739 o557 b558 b694
1926 B b739 t739
1927 T t740 o737 b738 b739
1928 S s740 t618 h
1929 G s740 t740
1930 B b740 s740
1931 T t741 o616 b740
1932 B b741 t741
1933 T t742 o633 b737 b741
1934 B b742 t742
1935 T t743 o633 b656 b742
1936 B b743 t743
1937 T t744 o633 b654 b743
1938 B b744 t744
1939 T t745 o633 b674 b744
1940 B b745 t745
1941 T t746 o633 b639 b745
1942 B b746 t746
1943 T t747 o633 b637 b746
1944 B b747 t747
1945 P p747 Number 2531
1946 P p748 Number 2538
1947 O o748 resource_defs p747 p748 p262
1948 P p749 Number 2536
1949 O o749 uid p749 p748
1950 T t749 o749 b624
1951 B b749 t749
1952 T t750 o b749 b4
1953 B b750 t750
1954 T t751 o748 b750
1955 B b751 t751
1956 T t752 o b751 b4
1957 B b752 t752
1958 T t753 o736 b616 b747 b621 b752
1959 B b753 t753
1960 T t754 o735 b753
1961 B b754 t754
1962 P p754 Number 2972
1963 P p755 Number 3365
1964 O o755 location p754 p755
1965 P p756 String op_assoc2
1966 O o756 rule p756
1967 T t756 o737 b739 b738
1968 S s756 t618 h
1969 G s756 t756
1970 B b756 s756
1971 T t757 o616 b756
1972 B b757 t757
1973 T t758 o633 b737 b757
1974 B b758 t758
1975 T t759 o633 b656 b758
1976 B b759 t759
1977 T t760 o633 b654 b759
1978 B b760 t760
1979 T t761 o633 b674 b760
1980 B b761 t761
1981 T t762 o633 b639 b761
1982 B b762 t762
1983 T t763 o633 b637 b762
1984 B b763 t763
1985 P p763 Number 2997
1986 P p764 Number 3004
1987 O o764 resource_defs p763 p764 p262
1988 P p765 Number 3002
1989 O o765 uid p765 p764
1990 T t765 o765 b624
1991 B b765 t765
1992 T t766 o b765 b4
1993 B b766 t766
1994 T t767 o764 b766
1995 B b767 t767
1996 T t768 o b767 b4
1997 B b768 t768
1998 T t769 o756 b616 b763 b621 b768
1999 B b769 t769
2000 T t770 o755 b769
2001 B b770 t770
2002 P p770 Number 3438
2003 P p771 Number 3514
2004 O o771 location p770 p771
2005 P p772 String id_wf1
2006 O o772 rule p772
2007 T t772 o618 b565
2008 S s772 t618 h
2009 G s772 t772
2010 B b772 s772
2011 T t773 o616 b772
2012 B b773 t773
2013 P p773 Number 3460
2014 P p774 Number 3468
2015 O o774 resource_defs p773 p774 p262
2016 P p775 Number 3466
2017 O o775 uid p775 p774
2018 T t775 o775 b624
2019 B b775 t775
2020 T t776 o b775 b4
2021 B b776 t776
2022 T t777 o774 b776
2023 B b777 t777
2024 T t778 o b777 b4
2025 B b778 t778
2026 T t779 o772 b616 b773 b621 b778
2027 B b779 t779
2028 T t780 o771 b779
2029 B b780 t780
2030 P p780 Number 3517
2031 P p781 Number 3595
2032 O o781 location p780 p781
2033 P p782 String id_wf2
2034 O o782 rule p782
2035 T t782 o653 b565 b552
2036 S s782 t618 h
2037 G s782 t782
2038 B b782 s782
2039 T t783 o616 b782
2040 B b783 t783
2041 P p783 Number 3539
2042 P p784 Number 3546
2043 O o784 resource_defs p783 p784 p262
2044 P p785 Number 3544
2045 O o785 uid p785 p784
2046 T t785 o785 b624
2047 B b785 t785
2048 T t786 o b785 b4
2049 B b786 t786
2050 T t787 o784 b786
2051 B b787 t787
2052 T t788 o b787 b4
2053 B b788 t788
2054 T t789 o782 b616 b783 b621 b788
2055 B b789 t789
2056 T t790 o781 b789
2057 B b790 t790
2058 P p790 Number 3683
2059 P p791 Number 3859
2060 O o791 location p790 p791
2061 P p792 String id_eq1
2062 O o792 rule p792
2063 T t792 o653 b571 b552
2064 S s792 t618 h
2065 G s792 t792
2066 B b792 s792
2067 T t793 o616 b792
2068 B b793 t793
2069 T t794 o557 b565 b571
2070 B b794 t794
2071 T t795 o737 b794 b571
2072 S s795 t618 h
2073 G s795 t795
2074 B b795 s795
2075 T t796 o616 b795
2076 B b796 t796
2077 T t797 o633 b793 b796
2078 B b797 t797
2079 T t798 o633 b710 b797
2080 B b798 t798
2081 P p798 Number 3705
2082 P p799 Number 3712
2083 O o799 resource_defs p798 p799 p262
2084 P p800 Number 3710
2085 O o800 uid p800 p799
2086 T t800 o800 b624
2087 B b800 t800
2088 T t801 o b800 b4
2089 B b801 t801
2090 T t802 o799 b801
2091 B b802 t802
2092 T t803 o b802 b4
2093 B b803 t803
2094 T t804 o792 b616 b798 b621 b803
2095 B b804 t804
2096 T t805 o791 b804
2097 B b805 t805
2098 P p805 Number 3861
2099 O o805 location p805 p304
2100 P p806 String id_eq2
2101 O o806 rule p806
2102 T t806 o557 b571 b565
2103 B b806 t806
2104 T t807 o737 b806 b571
2105 S s807 t618 h
2106 G s807 t807
2107 B b807 s807
2108 T t808 o616 b807
2109 B b808 t808
2110 T t809 o633 b793 b808
2111 B b809 t809
2112 T t810 o633 b710 b809
2113 B b810 t810
2114 P p810 Number 3883
2115 P p811 Number 3890
2116 O o811 resource_defs p810 p811 p262
2117 P p812 Number 3888
2118 O o812 uid p812 p811
2119 T t812 o812 b624
2120 B b812 t812
2121 T t813 o b812 b4
2122 B b813 t813
2123 T t814 o811 b813
2124 B b814 t814
2125 T t815 o b814 b4
2126 B b815 t815
2127 T t816 o806 b616 b810 b621 b815
2128 B b816 t816
2129 T t817 o805 b816
2130 B b817 t817
2131 P p817 Number 4039
2132 P p818 Number 4096
2133 O o818 location p817 p818
2134 NOcaml!str_let str_let str_let Ocaml
2135 O o819 str_let p817 p818
2136 NOcaml!patt_var patt_var patt_var Ocaml
2137 O o820 patt_var p302 p818
2138 NOcaml!patt_done patt_done patt_done Ocaml
2139 O o821 patt_done p817 p818
2140 T t821 o821
2141 B b821 t821 id_elim2T
2142 T t822 o820 b821
2143 B b822 t822
2144 NOcaml!fun fun fun Ocaml
2145 O o822 fun p302 p818
2146 NOcaml!patt_if patt_if patt_if Ocaml
2147 O o823 patt_if p302 p818
2148 P p823 Number 4053
2149 P p824 Number 4054
2150 O o824 patt_var p823 p824
2151 NOcaml!patt_body patt_body patt_body Ocaml
2152 O o825 patt_body p302 p818
2153 NOcaml!apply apply apply Ocaml
2154 P p825 Number 4060
2155 O o826 apply p825 p818
2156 P p826 Number 4094
2157 O o827 apply p825 p826
2158 NOcaml!lid lid lid Ocaml
2159 P p827 Number 4066
2160 O o828 lid p825 p827
2161 O o829 lid p792
2162 T t829 o829
2163 B b829 t829
2164 T t830 o828 b829
2165 B b830 t830
2166 P p830 Number 4068
2167 P p831 Number 4093
2168 O o831 apply p830 p831
2169 NOcaml!proj proj proj Ocaml
2170 P p832 Number 4091
2171 O o832 proj p830 p832
2172 O o833 uid p830 p832
2173 O o834 uid p507
2174 T t834 o834
2175 B b834 t834
2176 T t835 o833 b834
2177 B b835 t835
2178 P p835 Number 4077
2179 O o835 lid p835 p832
2180 P p836 String hyp_count_addr
2181 O o836 lid p836
2182 T t836 o836
2183 B b836 t836
2184 T t837 o835 b836
2185 B b837 t837
2186 T t838 o832 b835 b837
2187 B b838 t838
2188 P p838 Number 4092
2189 O o838 lid p838 p831
2190 P p839 Var p
2191 O o839 var p839
2192 T t839 o839
2193 B b839 t839
2194 T t840 o838 b839
2195 B b840 t840
2196 T t841 o831 b838 b840
2197 B b841 t841
2198 T t842 o827 b830 b841
2199 B b842 t842
2200 P p842 Number 4095
2201 O o842 lid p842 p818
2202 T t843 o842 b839
2203 B b843 t843
2204 T t844 o826 b842 b843
2205 B b844 t844
2206 T t845 o825 b844
2207 B b845 t845 p
2208 T t846 o824 b845
2209 B b846 t846
2210 T t847 o823 b846
2211 B b847 t847
2212 T t848 o822 b847
2213 B b848 t848
2214 T t849 o819 b822 b848
2215 B b849 t849
2216 T t850 o b849 b4
2217 B b850 t850
2218 T t851 o819 b850
2219 B b851 t851
2220 T t852 o390 b851
2221 B b852 t852
2222 T t853 o818 b852
2223 B b853 t853
2224 P p853 Number 4098
2225 P p854 Number 4271
2226 O o854 location p853 p854
2227 P p855 String inv_wf1
2228 O o855 rule p855
2229 T t855 o570 b558
2230 B b855 t855
2231 T t856 o618 b855
2232 S s856 t618 h
2233 G s856 t856
2234 B b856 s856
2235 T t857 o616 b856
2236 B b857 t857
2237 T t858 o633 b654 b857
2238 B b858 t858
2239 T t859 o633 b637 b858
2240 B b859 t859
2241 P p859 Number 4121
2242 P p860 Number 4128
2243 O o860 resource_defs p859 p860 p262
2244 P p861 Number 4126
2245 O o861 uid p861 p860
2246 T t861 o861 b624
2247 B b861 t861
2248 T t862 o b861 b4
2249 B b862 t862
2250 T t863 o860 b862
2251 B b863 t863
2252 T t864 o b863 b4
2253 B b864 t864
2254 T t865 o855 b616 b859 b621 b864
2255 B b865 t865
2256 T t866 o854 b865
2257 B b866 t866
2258 P p866 Number 4273
2259 P p867 Number 4449
2260 O o867 location p866 p867
2261 P p868 String inv_wf2
2262 O o868 rule p868
2263 T t868 o653 b855 b552
2264 S s868 t618 h
2265 G s868 t868
2266 B b868 s868
2267 T t869 o616 b868
2268 B b869 t869
2269 T t870 o633 b654 b869
2270 B b870 t870
2271 T t871 o633 b637 b870
2272 B b871 t871
2273 P p871 Number 4296
2274 P p872 Number 4303
2275 O o872 resource_defs p871 p872 p262
2276 P p873 Number 4301
2277 O o873 uid p873 p872
2278 T t873 o873 b624
2279 B b873 t873
2280 T t874 o b873 b4
2281 B b874 t874
2282 T t875 o872 b874
2283 B b875 t875
2284 T t876 o b875 b4
2285 B b876 t876
2286 T t877 o868 b616 b871 b621 b876
2287 B b877 t877
2288 T t878 o867 b877
2289 B b878 t878
2290 P p878 Number 4451
2291 P p879 Number 4637
2292 O o879 location p878 p879
2293 P p880 String inv_id1
2294 O o880 rule p880
2295 T t880 o557 b855 b558
2296 B b880 t880
2297 T t881 o737 b880 b565
2298 S s881 t618 h
2299 G s881 t881
2300 B b881 s881
2301 T t882 o616 b881
2302 B b882 t882
2303 T t883 o633 b654 b882
2304 B b883 t883
2305 T t884 o633 b637 b883
2306 B b884 t884
2307 P p884 Number 4474
2308 P p885 Number 4481
2309 O o885 resource_defs p884 p885 p262
2310 P p886 Number 4479
2311 O o886 uid p886 p885
2312 T t886 o886 b624
2313 B b886 t886
2314 T t887 o b886 b4
2315 B b887 t887
2316 T t888 o885 b887
2317 B b888 t888
2318 T t889 o b888 b4
2319 B b889 t889
2320 T t890 o880 b616 b884 b621 b889
2321 B b890 t890
2322 T t891 o879 b890
2323 B b891 t891
2324 P p891 Number 4639
2325 P p892 Number 4825
2326 O o892 location p891 p892
2327 P p893 String inv_id2
2328 O o893 rule p893
2329 T t893 o557 b558 b855
2330 B b893 t893
2331 T t894 o737 b893 b565
2332 S s894 t618 h
2333 G s894 t894
2334 B b894 s894
2335 T t895 o616 b894
2336 B b895 t895
2337 T t896 o633 b654 b895
2338 B b896 t896
2339 T t897 o633 b637 b896
2340 B b897 t897
2341 P p897 Number 4662
2342 P p898 Number 4669
2343 O o898 resource_defs p897 p898 p262
2344 P p899 Number 4667
2345 O o899 uid p899 p898
2346 T t899 o899 b624
2347 B b899 t899
2348 T t900 o b899 b4
2349 B b900 t900
2350 T t901 o898 b900
2351 B b901 t901
2352 T t902 o b901 b4
2353 B b902 t902
2354 T t903 o893 b616 b897 b621 b902
2355 B b903 t903
2356 T t904 o892 b903
2357 B b904 t904
2358 P p904 Number 4885
2359 P p905 Number 5314
2360 O o905 location p904 p905
2361 P p906 String cancelLeft
2362 O o906 rule p906
2363 NSummary!term_param term_param term_param Summary
2364 O o907 term_param
2365 T t907 o907 b558
2366 B b907 t907
2367 T t908 o b907 b4
2368 B b908 t908
2369 T t909 o b615 b908
2370 B b909 t909
2371 T t910 o737 b560 b693
2372 S s910 t618 h
2373 G s910 t910
2374 B b910 s910
2375 T t911 o616 b910
2376 B b911 t911
2377 T t912 o737 b559 b672
2378 S s912 t618 h
2379 G s912 t912
2380 B b912 s912
2381 T t913 o616 b912
2382 B b913 t913
2383 T t914 o633 b911 b913
2384 B b914 t914
2385 T t915 o633 b737 b914
2386 B b915 t915
2387 T t916 o633 b656 b915
2388 B b916 t916
2389 T t917 o633 b654 b916
2390 B b917 t917
2391 T t918 o633 b674 b917
2392 B b918 t918
2393 T t919 o633 b639 b918
2394 B b919 t919
2395 T t920 o633 b637 b919
2396 B b920 t920
2397 NSummary!interactive interactive interactive Summary
2398 O o920 interactive
2399 NSummary!ext_rule ext_rule ext_rule Summary
2400 P p920 String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2401 O o921 ext_rule p920
2402 NSummary!status_incomplete status_incomplete status_incomplete Summary
2403 O o922 status_incomplete
2404 T t922 o922
2405 B b922 t922
2406 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2407 O o923 ext_unjustified
2408 NSummary!tactic_arg tactic_arg tactic_arg Summary
2409 P p923 String main
2410 O o924 tactic_arg p923
2411 NSummary!msequent msequent msequent Summary
2412 O o925 msequent
2413 T t925 o b910 b4
2414 B b925 t925
2415 T t926 o b736 b925
2416 B b926 t926
2417 T t927 o b655 b926
2418 B b927 t927
2419 T t928 o b653 b927
2420 B b928 t928
2421 T t929 o b673 b928
2422 B b929 t929
2423 T t930 o b638 b929
2424 B b930 t930
2425 T t931 o b636 b930
2426 B b931 t931
2427 T t932 o925 b912 b931
2428 B b932 t932
2429 NSummary!parent_none parent_none parent_none Summary
2430 O o932 parent_none
2431 T t933 o932
2432 B b933 t933
2433 T t934 o924 b932 b4 b933
2434 B b934 t934
2435 P p934 String assertion
2436 O o934 tactic_arg p934
2437 H h934 v t910
2438 T t935 o557 b855 b560
2439 B b935 t935
2440 T t936 o557 b855 b693
2441 B b936 t936
2442 T t937 o737 b935 b936
2443 S s937 t618 h h934
2444 G s937 t937
2445 B b937 s937
2446 T t938 o925 b937 b931
2447 B b938 t938
2448 S s938 t618 h h934
2449 G s938 t912
2450 B b939 s938
2451 T t939 o925 b939 b931
2452 B b940 t939
2453 T t940 o2 b934
2454 B b941 t940
2455 T t941 o924 b940 b4 b941
2456 B b942 t941
2457 T t942 o2 b942
2458 B b943 t942
2459 T t943 o934 b938 b4 b943
2460 B b944 t943
2461 H h944 v_1 t937
2462 S s944 t618 h h934 h944
2463 G s944 t912
2464 B b945 s944
2465 T t945 o925 b945 b931
2466 B b946 t945
2467 T t946 o924 b946 b4 b943
2468 B b947 t946
2469 T t947 o b947 b4
2470 B b948 t947
2471 T t948 o b944 b948
2472 B b949 t948
2473 T t949 o923 b934 b949
2474 B b950 t949
2475 P p950 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2476 O o950 ext_rule p950
2477 T t950 o923 b944 b4
2478 B b951 t950
2479 T t951 o950 b922 b951 b4 b4
2480 B b952 t951
2481 P p952 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2482 O o952 ext_rule p952
2483 P p953 String eq
2484 O o953 tactic_arg p953
2485 T t953 o557 b880 b559
2486 B b953 t953
2487 T t954 o737 b935 b953
2488 S s954 t618 h h934 h944
2489 G s954 t954
2490 B b954 s954
2491 T t955 o925 b954 b931
2492 B b955 t955
2493 T t956 o2 b947
2494 B b956 t956
2495 T t957 o953 b955 b4 b956
2496 B b957 t957
2497 T t958 o737 b953 b936
2498 H h958 v_2 t958
2499 S s958 t618 h h934 h944 h958
2500 G s958 t912
2501 B b958 s958
2502 T t959 o925 b958 b931
2503 B b959 t959
2504 T t960 o924 b959 b4 b956
2505 B b960 t960
2506 P p960 String wf
2507 O o960 tactic_arg p960
2508 B b961 t936 v_2
2509 T t961 o710 b961
2510 S s961 t618 h h934 h944
2511 G s961 t961
2512 B b962 s961
2513 T t962 o925 b962 b931
2514 B b963 t962
2515 NCzf_itt_eq!fun_prop fun_prop fun_prop Czf_itt_eq
2516 O o963 fun_prop
2517 P p963 Var v_2
2518 O o964 var p963
2519 T t964 o964
2520 B b964 t964
2521 T t965 o737 b964 b936
2522 B b965 t965 v_2
2523 T t966 o963 b965
2524 S s966 t618 h h934 h944
2525 G s966 t966
2526 B b966 s966
2527 T t967 o925 b966 b931
2528 B b967 t967
2529 NSummary!arg_named arg_named arg_named Summary
2530 P p967 String d_auto
2531 O o967 arg_named p967
2532 NSummary!arg_bool arg_bool arg_bool Summary
2533 P p968 String true
2534 O o968 arg_bool p968
2535 T t968 o968
2536 B b968 t968
2537 T t969 o967 b968
2538 B b969 t969
2539 T t970 o b969 b4
2540 B b970 t970
2541 T t971 o960 b967 b970 b956
2542 B b971 t971
2543 T t972 o2 b971
2544 B b972 t972
2545 T t973 o960 b963 b4 b972
2546 B b973 t973
2547 T t974 o b973 b4
2548 B b974 t974
2549 T t975 o b960 b974
2550 B b975 t975
2551 T t976 o b957 b975
2552 B b976 t976
2553 T t977 o923 b947 b976
2554 B b977 t977
2555 P p977 String autoT
2556 O o977 ext_rule p977
2557 T t978 o923 b957 b4
2558 B b978 t978
2559 T t979 o977 b922 b978 b4 b4
2560 B b979 t979
2561 P p979 String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2562 O o979 ext_rule p979
2563 T t980 o557 b880 b672
2564 B b980 t980
2565 T t981 o737 b936 b980
2566 S s981 t618 h h934 h944 h958
2567 G s981 t981
2568 B b981 s981
2569 T t982 o925 b981 b931
2570 B b982 t982
2571 T t983 o2 b960
2572 B b983 t983
2573 T t984 o953 b982 b4 b983
2574 B b984 t984
2575 T t985 o737 b953 b980
2576 H h985 v_3 t985
2577 S s985 t618 h h934 h944 h958 h985
2578 G s985 t912
2579 B b985 s985
2580 T t986 o925 b985 b931
2581 B b986 t986
2582 T t987 o924 b986 b4 b983
2583 B b987 t987
2584 B b988 t953 v_3
2585 T t988 o710 b988
2586 S s988 t618 h h934 h944 h958
2587 G s988 t988
2588 B b989 s988
2589 T t989 o925 b989 b931
2590 B b990 t989
2591 P p990 Var v_3
2592 O o990 var p990
2593 T t990 o990
2594 B b991 t990
2595 T t991 o737 b953 b991
2596 B b992 t991 v_3
2597 T t992 o963 b992
2598 S s992 t618 h h934 h944 h958
2599 G s992 t992
2600 B b993 s992
2601 T t993 o925 b993 b931
2602 B b994 t993
2603 T t994 o960 b994 b970 b983
2604 B b995 t994
2605 T t995 o2 b995
2606 B b996 t995
2607 T t996 o960 b990 b4 b996
2608 B b997 t996
2609 T t997 o b997 b4
2610 B b998 t997
2611 T t998 o b987 b998
2612 B b999 t998
2613 T t999 o b984 b999
2614 B b1000 t999
2615 T t1000 o923 b960 b1000
2616 B b1001 t1000
2617 T t1001 o923 b984 b4
2618 B b1002 t1001
2619 T t1002 o977 b922 b1002 b4 b4
2620 B b1003 t1002
2621 P p1003 String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2622 O o1003 ext_rule p1003
2623 T t1003 o557 b565 b559
2624 B b1004 t1003
2625 T t1004 o557 b565 b672
2626 B b1005 t1004
2627 T t1005 o737 b1004 b1005
2628 H h1005 v_4 t1005
2629 S s1005 t618 h h934 h944 h958 h985 h1005
2630 G s1005 t912
2631 B b1006 s1005
2632 T t1006 o925 b1006 b931
2633 B b1007 t1006
2634 T t1007 o2 b987
2635 B b1008 t1007
2636 T t1008 o924 b1007 b4 b1008
2637 B b1009 t1008
2638 T t1009 o b1009 b4
2639 B b1010 t1009
2640 T t1010 o923 b987 b1010
2641 B b1011 t1010
2642 P p1011 String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2643 O o1011 ext_rule p1011
2644 T t1011 o737 b559 b1005
2645 H h1011 v_5 t1011
2646 S s1011 t618 h h934 h944 h958 h985 h1005 h1011
2647 G s1011 t912
2648 B b1012 s1011
2649 T t1012 o925 b1012 b931
2650 B b1013 t1012
2651 T t1013 o2 b1009
2652 B b1014 t1013
2653 T t1014 o924 b1013 b4 b1014
2654 B b1015 t1014
2655 B b1016 t1004 v_5
2656 T t1016 o710 b1016
2657 S s1016 t618 h h934 h944 h958 h985 h1005
2658 G s1016 t1016
2659 B b1017 s1016
2660 T t1017 o925 b1017 b931
2661 B b1018 t1017
2662 P p1018 Var v_5
2663 O o1018 var p1018
2664 T t1018 o1018
2665 B b1019 t1018
2666 T t1019 o737 b1019 b1005
2667 B b1020 t1019 v_5
2668 T t1020 o963 b1020
2669 S s1020 t618 h h934 h944 h958 h985 h1005
2670 G s1020 t1020
2671 B b1021 s1020
2672 T t1021 o925 b1021 b931
2673 B b1022 t1021
2674 T t1022 o960 b1022 b970 b1014
2675 B b1023 t1022
2676 T t1023 o2 b1023
2677 B b1024 t1023
2678 T t1024 o960 b1018 b4 b1024
2679 B b1025 t1024
2680 T t1025 o b1025 b4
2681 B b1026 t1025
2682 T t1026 o b1015 b1026
2683 B b1027 t1026
2684 T t1027 o923 b1009 b1027
2685 B b1028 t1027
2686 P p1028 String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2687 O o1028 ext_rule p1028
2688 H h1028 v_6 t912
2689 S s1028 t618 h h934 h944 h958 h985 h1005 h1011 h1028
2690 G s1028 t912
2691 B b1029 s1028
2692 T t1029 o925 b1029 b931
2693 B b1030 t1029
2694 T t1030 o2 b1015
2695 B b1031 t1030
2696 T t1031 o924 b1030 b4 b1031
2697 B b1032 t1031
2698 T t1032 o b1032 b4
2699 B b1033 t1032
2700 T t1033 o923 b1015 b1033
2701 B b1034 t1033
2702 P p1034 String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2703 O o1034 ext_rule p1034
2704 T t1034 o923 b1032 b4
2705 B b1035 t1034
2706 T t1035 o1034 b922 b1035 b4 b4
2707 B b1036 t1035
2708 T t1036 o b1036 b4
2709 B b1037 t1036
2710 T t1037 o1028 b922 b1034 b1037 b4
2711 B b1038 t1037
2712 P p1038 String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2713 O o1038 ext_rule p1038
2714 T t1038 o923 b1025 b4
2715 B b1039 t1038
2716 T t1039 o1038 b922 b1039 b4 b4
2717 B b1040 t1039
2718 T t1040 o b1040 b4
2719 B b1041 t1040
2720 T t1041 o b1038 b1041
2721 B b1042 t1041
2722 T t1042 o1011 b922 b1028 b1042 b4
2723 B b1043 t1042
2724 T t1043 o b1043 b4
2725 B b1044 t1043
2726 T t1044 o1003 b922 b1011 b1044 b4
2727 B b1045 t1044
2728 T t1045 o923 b997 b4
2729 B b1046 t1045
2730 T t1046 o1038 b922 b1046 b4 b4
2731 B b1047 t1046
2732 T t1047 o b1047 b4
2733 B b1048 t1047
2734 T t1048 o b1045 b1048
2735 B b1049 t1048
2736 T t1049 o b1003 b1049
2737 B b1050 t1049
2738 T t1050 o979 b922 b1001 b1050 b4
2739 B b1051 t1050
2740 T t1051 o923 b973 b4
2741 B b1052 t1051
2742 T t1052 o1038 b922 b1052 b4 b4
2743 B b1053 t1052
2744 T t1053 o b1053 b4
2745 B b1054 t1053
2746 T t1054 o b1051 b1054
2747 B b1055 t1054
2748 T t1055 o b979 b1055
2749 B b1056 t1055
2750 T t1056 o952 b922 b977 b1056 b4
2751 B b1057 t1056
2752 T t1057 o b1057 b4
2753 B b1058 t1057
2754 T t1058 o b952 b1058
2755 B b1059 t1058
2756 T t1059 o921 b922 b950 b1059 b4
2757 B b1060 t1059
2758 T t1060 o920 b1060
2759 B b1061 t1060
2760 P p1061 Number 4911
2761 P p1062 Number 4919
2762 O o1062 resource_defs p1061 p1062 p262
2763 P p1063 Number 4917
2764 O o1063 uid p1063 p1062
2765 T t1063 o1063 b624
2766 B b1063 t1063
2767 T t1064 o b1063 b4
2768 B b1064 t1064
2769 T t1065 o1062 b1064
2770 B b1065 t1065
2771 T t1066 o b1065 b4
2772 B b1066 t1066
2773 T t1067 o906 b909 b920 b1061 b1066
2774 B b1067 t1067
2775 T t1068 o905 b1067
2776 B b1068 t1068
2777 P p1068 Number 5359
2778 P p1069 Number 5789
2779 O o1069 location p1068 p1069
2780 P p1070 String cancelRight
2781 O o1070 rule p1070
2782 T t1070 o907 b672
2783 B b1070 t1070
2784 T t1071 o b1070 b4
2785 B b1071 t1071
2786 T t1072 o b615 b1071
2787 B b1072 t1072
2788 T t1073 o737 b693 b694
2789 S s1073 t618 h
2790 G s1073 t1073
2791 B b1073 s1073
2792 T t1074 o616 b1073
2793 B b1074 t1074
2794 T t1075 o737 b558 b559
2795 S s1075 t618 h
2796 G s1075 t1075
2797 B b1075 s1075
2798 T t1076 o616 b1075
2799 B b1076 t1076
2800 T t1077 o633 b1074 b1076
2801 B b1077 t1077
2802 T t1078 o633 b737 b1077
2803 B b1078 t1078
2804 T t1079 o633 b656 b1078
2805 B b1079 t1079
2806 T t1080 o633 b654 b1079
2807 B b1080 t1080
2808 T t1081 o633 b674 b1080
2809 B b1081 t1081
2810 T t1082 o633 b639 b1081
2811 B b1082 t1082
2812 T t1083 o633 b637 b1082
2813 B b1083 t1083
2814 P p1083 String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenWT autoT"
2815 O o1083 ext_rule p1083
2816 T t1084 o b1073 b4
2817 B b1084 t1084
2818 T t1085 o b736 b1084
2819 B b1085 t1085
2820 T t1086 o b655 b1085
2821 B b1086 t1086
2822 T t1087 o b653 b1086
2823 B b1087 t1087
2824 T t1088 o b673 b1087
2825 B b1088 t1088
2826 T t1089 o b638 b1088
2827 B b1089 t1089
2828 T t1090 o b636 b1089
2829 B b1090 t1090
2830 T t1091 o925 b1075 b1090
2831 B b1091 t1091
2832 T t1092 o924 b1091 b4 b933
2833 B b1092 t1092
2834 H h1092 v t1073
2835 T t1093 o570 b672
2836 B b1093 t1093
2837 T t1094 o557 b693 b1093
2838 B b1094 t1094
2839 T t1095 o557 b694 b1093
2840 B b1095 t1095
2841 T t1096 o737 b1094 b1095
2842 S s1096 t618 h h1092
2843 G s1096 t1096
2844 B b1096 s1096
2845 T t1097 o925 b1096 b1090
2846 B b1097 t1097
2847 S s1097 t618 h h1092
2848 G s1097 t1075
2849 B b1098 s1097
2850 T t1098 o925 b1098 b1090
2851 B b1099 t1098
2852 T t1099 o2 b1092
2853 B b1100 t1099
2854 T t1100 o924 b1099 b4 b1100
2855 B b1101 t1100
2856 T t1101 o2 b1101
2857 B b1102 t1101
2858 T t1102 o934 b1097 b4 b1102
2859 B b1103 t1102
2860 H h1103 v_1 t1096
2861 S s1103 t618 h h1092 h1103
2862 G s1103 t1075
2863 B b1104 s1103
2864 T t1104 o925 b1104 b1090
2865 B b1105 t1104
2866 T t1105 o924 b1105 b4 b1102
2867 B b1106 t1105
2868 T t1106 o b1106 b4
2869 B b1107 t1106
2870 T t1107 o b1103 b1107
2871 B b1108 t1107
2872 T t1108 o923 b1092 b1108
2873 B b1109 t1108
2874 T t1109 o923 b1103 b4
2875 B b1110 t1109
2876 T t1110 o950 b922 b1110 b4 b4
2877 B b1111 t1110
2878 P p1111 String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
2879 O o1111 ext_rule p1111
2880 T t1111 o557 b672 b1093
2881 B b1112 t1111
2882 T t1112 o557 b558 b1112
2883 B b1113 t1112
2884 T t1113 o737 b1113 b1095
2885 H h1113 v_2 t1113
2886 S s1113 t618 h h1092 h1103 h1113
2887 G s1113 t1075
2888 B b1114 s1113
2889 T t1114 o925 b1114 b1090
2890 B b1115 t1114
2891 T t1115 o2 b1106
2892 B b1116 t1115
2893 T t1116 o924 b1115 b4 b1116
2894 B b1117 t1116
2895 B b1118 t1095 v_2
2896 T t1118 o710 b1118
2897 S s1118 t618 h h1092 h1103
2898 G s1118 t1118
2899 B b1119 s1118
2900 T t1119 o925 b1119 b1090
2901 B b1120 t1119
2902 T t1120 o737 b964 b1095
2903 B b1121 t1120 v_2
2904 T t1121 o963 b1121
2905 S s1121 t618 h h1092 h1103
2906 G s1121 t1121
2907 B b1122 s1121
2908 T t1122 o925 b1122 b1090
2909 B b1123 t1122
2910 T t1123 o960 b1123 b970 b1116
2911 B b1124 t1123
2912 T t1124 o2 b1124
2913 B b1125 t1124
2914 T t1125 o960 b1120 b4 b1125
2915 B b1126 t1125
2916 T t1126 o b1126 b4
2917 B b1127 t1126
2918 T t1127 o b1117 b1127
2919 B b1128 t1127
2920 T t1128 o923 b1106 b1128
2921 B b1129 t1128
2922 P p1129 String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
2923 O o1129 ext_rule p1129
2924 T t1129 o557 b559 b1112
2925 B b1130 t1129
2926 T t1130 o737 b1113 b1130
2927 H h1130 v_3 t1130
2928 S s1130 t618 h h1092 h1103 h1113 h1130
2929 G s1130 t1075
2930 B b1131 s1130
2931 T t1131 o925 b1131 b1090
2932 B b1132 t1131
2933 T t1132 o2 b1117
2934 B b1133 t1132
2935 T t1133 o924 b1132 b4 b1133
2936 B b1134 t1133
2937 B b1135 t1112 v_3
2938 T t1135 o710 b1135
2939 S s1135 t618 h h1092 h1103 h1113
2940 G s1135 t1135
2941 B b1136 s1135
2942 T t1136 o925 b1136 b1090
2943 B b1137 t1136
2944 T t1137 o737 b1113 b991
2945 B b1138 t1137 v_3
2946 T t1138 o963 b1138
2947 S s1138 t618 h h1092 h1103 h1113
2948 G s1138 t1138
2949 B b1139 s1138
2950 T t1139 o925 b1139 b1090
2951 B b1140 t1139
2952 T t1140 o960 b1140 b970 b1133
2953 B b1141 t1140
2954 T t1141 o2 b1141
2955 B b1142 t1141
2956 T t1142 o960 b1137 b4 b1142
2957 B b1143 t1142
2958 T t1143 o b1143 b4
2959 B b1144 t1143
2960 T t1144 o b1134 b1144
2961 B b1145 t1144
2962 T t1145 o923 b1117 b1145
2963 B b1146 t1145
2964 P p1146 String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
2965 O o1146 ext_rule p1146
2966 T t1146 o557 b558 b565
2967 B b1147 t1146
2968 T t1147 o557 b559 b565
2969 B b1148 t1147
2970 T t1148 o737 b1147 b1148
2971 H h1148 v_4 t1148
2972 S s1148 t618 h h1092 h1103 h1113 h1130 h1148
2973 G s1148 t1075
2974 B b1149 s1148
2975 T t1149 o925 b1149 b1090
2976 B b1150 t1149
2977 T t1150 o2 b1134
2978 B b1151 t1150
2979 T t1151 o924 b1150 b4 b1151
2980 B b1152 t1151
2981 T t1152 o b1152 b4
2982 B b1153 t1152
2983 T t1153 o923 b1134 b1153
2984 B b1154 t1153
2985 P p1154 String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
2986 O o1154 ext_rule p1154
2987 T t1154 o737 b558 b1148
2988 H h1154 v_5 t1154
2989 S s1154 t618 h h1092 h1103 h1113 h1130 h1148 h1154
2990 G s1154 t1075
2991 B b1155 s1154
2992 T t1155 o925 b1155 b1090
2993 B b1156 t1155
2994 T t1156 o2 b1152
2995 B b1157 t1156
2996 T t1157 o924 b1156 b4 b1157
2997 B b1158 t1157
2998 B b1159 t1147 v_5
2999 T t1159 o710 b1159
3000 S s1159 t618 h h1092 h1103 h1113 h1130 h1148
3001 G s1159 t1159
3002 B b1160 s1159
3003 T t1160 o925 b1160 b1090
3004 B b1161 t1160
3005 T t1161 o737 b1019 b1148
3006 B b1162 t1161 v_5
3007 T t1162 o963 b1162
3008 S s1162 t618 h h1092 h1103 h1113 h1130 h1148
3009 G s1162 t1162
3010 B b1163 s1162
3011 T t1163 o925 b1163 b1090
3012 B b1164 t1163
3013 T t1164 o960 b1164 b970 b1157
3014 B b1165 t1164
3015 T t1165 o2 b1165
3016 B b1166 t1165
3017 T t1166 o960 b1161 b4 b1166
3018 B b1167 t1166
3019 T t1167 o b1167 b4
3020 B b1168 t1167
3021 T t1168 o b1158 b1168
3022 B b1169 t1168
3023 T t1169 o923 b1152 b1169
3024 B b1170 t1169
3025 P p1170 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3026 O o1170 ext_rule p1170
3027 T t1170 o923 b1158 b4
3028 B b1171 t1170
3029 T t1171 o1170 b922 b1171 b4 b4
3030 B b1172 t1171
3031 P p1172 String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
3032 O o1172 ext_rule p1172
3033 T t1172 o923 b1167 b4
3034 B b1173 t1172
3035 T t1173 o1172 b922 b1173 b4 b4
3036 B b1174 t1173
3037 T t1174 o b1174 b4
3038 B b1175 t1174
3039 T t1175 o b1172 b1175
3040 B b1176 t1175
3041 T t1176 o1154 b922 b1170 b1176 b4
3042 B b1177 t1176
3043 T t1177 o b1177 b4
3044 B b1178 t1177
3045 T t1178 o1146 b922 b1154 b1178 b4
3046 B b1179 t1178
3047 T t1179 o923 b1143 b4
3048 B b1180 t1179
3049 T t1180 o1172 b922 b1180 b4 b4
3050 B b1181 t1180
3051 T t1181 o b1181 b4
3052 B b1182 t1181
3053 T t1182 o b1179 b1182
3054 B b1183 t1182
3055 T t1183 o1129 b922 b1146 b1183 b4
3056 B b1184 t1183
3057 T t1184 o923 b1126 b4
3058 B b1185 t1184
3059 T t1185 o1172 b922 b1185 b4 b4
3060 B b1186 t1185
3061 T t1186 o b1186 b4
3062 B b1187 t1186
3063 T t1187 o b1184 b1187
3064 B b1188 t1187
3065 S s1188 t618 h h1092 h1103 h1113
3066 G s1188 t675
3067 B b1189 s1188
3068 T t1189 o925 b1189 b1090
3069 B b1190 t1189
3070 T t1190 o924 b1115 b970 b1116
3071 B b1191 t1190
3072 T t1191 o2 b1191
3073 B b1192 t1191
3074 T t1192 o924 b1190 b4 b1192
3075 B b1193 t1192
3076 S s1193 t618 h h1092 h1103 h1113 h1130
3077 G s1193 t675
3078 B b1194 s1193
3079 T t1194 o925 b1194 b1090
3080 B b1195 t1194
3081 T t1195 o2 b1193
3082 B b1196 t1195
3083 T t1196 o924 b1195 b4 b1196
3084 B b1197 t1196
3085 T t1197 o960 b1140 b970 b1196
3086 B b1198 t1197
3087 T t1198 o2 b1198
3088 B b1199 t1198
3089 T t1199 o960 b1137 b4 b1199
3090 B b1200 t1199
3091 T t1200 o b1200 b4
3092 B b1201 t1200
3093 T t1201 o b1197 b1201
3094 B b1202 t1201
3095 T t1202 o923 b1193 b1202
3096 B b1203 t1202
3097 S s1203 t618 h h1092 h1103 h1113 h1130 h1148
3098 G s1203 t675
3099 B b1204 s1203
3100 T t1204 o925 b1204 b1090
3101 B b1205 t1204
3102 T t1205 o2 b1197
3103 B b1206 t1205
3104 T t1206 o924 b1205 b4 b1206
3105 B b1207 t1206
3106 T t1207 o b1207 b4
3107 B b1208 t1207
3108 T t1208 o923 b1197 b1208
3109 B b1209 t1208
3110 S s1209 t618 h h1092 h1103 h1113 h1130 h1148 h1154
3111 G s1209 t675
3112 B b1210 s1209
3113 T t1210 o925 b1210 b1090
3114 B b1211 t1210
3115 T t1211 o2 b1207
3116 B b1212 t1211
3117 T t1212 o924 b1211 b4 b1212
3118 B b1213 t1212
3119 T t1213 o960 b1164 b970 b1212
3120 B b1214 t1213
3121 T t1214 o2 b1214
3122 B b1215 t1214
3123 T t1215 o960 b1161 b4 b1215
3124 B b1216 t1215
3125 T t1216 o b1216 b4
3126 B b1217 t1216
3127 T t1217 o b1213 b1217
3128 B b1218 t1217
3129 T t1218 o923 b1207 b1218
3130 B b1219 t1218
3131 P p1219 String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT thenT rwh unfold_equal 8 thenT autoT"
3132 O o1219 ext_rule p1219
3133 T t1219 o923 b1213 b4
3134 B b1220 t1219
3135 T t1220 o1219 b922 b1220 b4 b4
3136 B b1221 t1220
3137 T t1221 o923 b1216 b4
3138 B b1222 t1221
3139 T t1222 o1038 b922 b1222 b4 b4
3140 B b1223 t1222
3141 T t1223 o b1223 b4
3142 B b1224 t1223
3143 T t1224 o b1221 b1224
3144 B b1225 t1224
3145 T t1225 o1154 b922 b1219 b1225 b4
3146 B b1226 t1225
3147 T t1226 o b1226 b4
3148 B b1227 t1226
3149 T t1227 o1146 b922 b1209 b1227 b4
3150 B b1228 t1227
3151 P p1228 String "rwh unfold_fun_set 0 thenT autoT"
3152 O o1228 ext_rule p1228
3153 NCzf_itt_set!set set set Czf_itt_set
3154 O o1229 set
3155 T t1229 o1229
3156 H h1229 s1_1 t1229
3157 H h1230 s2 t1229
3158 P p1230 Var s1_1
3159 O o1230 var p1230
3160 T t1230 o1230
3161 B b1230 t1230
3162 T t1231 o737 b1230 b559
3163 H h1231 x t1231
3164 T t1232 o737 b1113 b1113
3165 S s1232 t618 h h1092 h1103 h1113 h1229 h1230 h1231
3166 G s1232 t1232
3167 B b1232 s1232
3168 T t1233 o925 b1232 b1090
3169 B b1233 t1233
3170 NItt_logic Itt_logic Itt_logic NIL
3171 NItt_logic!implies implies implies Itt_logic
3172 O o1233 implies
3173 B b1234 t1231
3174 B b1235 t1232
3175 T t1235 o1233 b1234 b1235
3176 S s1235 t618 h h1092 h1103 h1113 h1229 h1230
3177 G s1235 t1235
3178 B b1236 s1235
3179 T t1236 o925 b1236 b1090
3180 B b1237 t1236
3181 NItt_logic!all all all Itt_logic
3182 O o1237 all
3183 B b1238 t1229
3184 B b1239 t1235 s2
3185 T t1239 o1237 b1238 b1239
3186 S s1239 t618 h h1092 h1103 h1113 h1229
3187 G s1239 t1239
3188 B b1240 s1239
3189 T t1240 o925 b1240 b1090
3190 B b1241 t1240
3191 B b1242 t1239 s1_1
3192 T t1242 o1237 b1238 b1242
3193 S s1242 t618 h h1092 h1103 h1113
3194 G s1242 t1242
3195 B b1243 s1242
3196 T t1243 o925 b1243 b1090
3197 B b1244 t1243
3198 T t1244 o2 b1200
3199 B b1245 t1244
3200 T t1245 o960 b1244 b970 b1245
3201 B b1246 t1245
3202 T t1246 o2 b1246
3203 B b1247 t1246
3204 T t1247 o924 b1241 b970 b1247
3205 B b1248 t1247
3206 T t1248 o2 b1248
3207 B b1249 t1248
3208 T t1249 o924 b1237 b970 b1249
3209 B b1250 t1249
3210 T t1250 o2 b1250
3211 B b1251 t1250
3212 T t1251 o924 b1233 b4 b1251
3213 B b1252 t1251
3214 T t1252 o b1252 b4
3215 B b1253 t1252
3216 T t1253 o923 b1200 b1253
3217 B b1254 t1253
3218 NSummary!ext_goal ext_goal ext_goal Summary
3219 O o1254 ext_goal
3220 T t1254 o1254 b1252
3221 B b1255 t1254
3222 T t1255 o b1255 b4
3223 B b1256 t1255
3224 T t1256 o1228 b922 b1254 b1256 b4
3225 B b1257 t1256
3226 T t1257 o b1257 b4
3227 B b1258 t1257
3228 T t1258 o b1228 b1258
3229 B b1259 t1258
3230 T t1259 o1129 b922 b1203 b1259 b4
3231 B b1260 t1259
3232 T t1260 o b1260 b4
3233 B b1261 t1260
3234 T t1261 o1111 b922 b1129 b1188 b1261
3235 B b1262 t1261
3236 T t1262 o b1262 b4
3237 B b1263 t1262
3238 T t1263 o b1111 b1263
3239 B b1264 t1263
3240 T t1264 o1083 b922 b1109 b1264 b4
3241 B b1265 t1264
3242 T t1265 o920 b1265
3243 B b1266 t1265
3244 P p1266 Number 5386
3245 P p1267 Number 5394
3246 O o1267 resource_defs p1266 p1267 p262
3247 P p1268 Number 5392
3248 O o1268 uid p1268 p1267
3249 T t1268 o1268 b624
3250 B b1268 t1268
3251 T t1269 o b1268 b4
3252 B b1269 t1269
3253 T t1270 o1267 b1269
3254 B b1270 t1270
3255 T t1271 o b1270 b4
3256 B b1271 t1271
3257 T t1272 o1070 b1072 b1083 b1266 b1271
3258 B b1272 t1272
3259 T t1273 o1069 b1272
3260 B b1273 t1273
3261 P p1273 Number 5791
3262 P p1274 Number 5863
3263 O o1274 location p1273 p1274
3264 O o1275 str_let p1273 p1274
3265 P p1275 Number 5795
3266 O o1276 patt_var p1275 p1274
3267 O o1277 patt_done p1273 p1274
3268 T t1277 o1277
3269 B b1277 t1277 groupCancelLeftT
3270 T t1278 o1276 b1277
3271 B b1278 t1278
3272 O o1278 fun p1275 p1274
3273 O o1279 patt_if p1275 p1274
3274 P p1279 Number 5812
3275 P p1280 Number 5813
3276 O o1280 patt_var p1279 p1280
3277 O o1281 patt_body p1275 p1274
3278 P p1281 Number 5814
3279 P p1282 Number 5815
3280 O o1282 patt_var p1281 p1282
3281 P p1283 Number 5821
3282 O o1283 apply p1283 p1274
3283 P p1284 Number 5861
3284 O o1284 apply p1283 p1284
3285 P p1285 Number 5859
3286 O o1285 apply p1283 p1285
3287 P p1286 Number 5831
3288 O o1286 lid p1283 p1286
3289 O o1287 lid p906
3290 T t1287 o1287
3291 B b1287 t1287
3292 T t1288 o1286 b1287
3293 B b1288 t1288
3294 P p1288 Number 5833
3295 P p1289 Number 5858
3296 O o1289 apply p1288 p1289
3297 P p1290 Number 5856
3298 O o1290 proj p1288 p1290
3299 O o1291 uid p1288 p1290
3300 T t1291 o1291 b834
3301 B b1291 t1291
3302 P p1291 Number 5842
3303 O o1292 lid p1291 p1290
3304 T t1292 o1292 b836
3305 B b1292 t1292
3306 T t1293 o1290 b1291 b1292
3307 B b1293 t1293
3308 P p1293 Number 5857
3309 O o1293 lid p1293 p1289
3310 T t1294 o1293 b839
3311 B b1294 t1294
3312 T t1295 o1289 b1293 b1294
3313 B b1295 t1295
3314 T t1296 o1285 b1288 b1295
3315 B b1296 t1296
3316 P p1296 Number 5860
3317 O o1296 lid p1296 p1284
3318 P p1297 Var t
3319 O o1297 var p1297
3320 T t1297 o1297
3321 B b1297 t1297
3322 T t1298 o1296 b1297
3323 B b1298 t1298
3324 T t1299 o1284 b1296 b1298
3325 B b1299 t1299
3326 P p1299 Number 5862
3327 O o1299 lid p1299 p1274
3328 T t1300 o1299 b839
3329 B b1300 t1300
3330 T t1301 o1283 b1299 b1300
3331 B b1301 t1301
3332 T t1302 o1281 b1301
3333 B b1302 t1302 p
3334 T t1303 o1282 b1302
3335 B b1303 t1303
3336 T t1304 o1279 b1303
3337 B b1304 t1304
3338 T t1305 o1278 b1304
3339 B b1305 t1305
3340 T t1306 o1281 b1305
3341 B b1306 t1306 t
3342 T t1307 o1280 b1306
3343 B b1307 t1307
3344 T t1308 o1279 b1307
3345 B b1308 t1308
3346 T t1309 o1278 b1308
3347 B b1309 t1309
3348 T t1310 o1275 b1278 b1309
3349 B b1310 t1310
3350 T t1311 o b1310 b4
3351 B b1311 t1311
3352 T t1312 o1275 b1311
3353 B b1312 t1312
3354 T t1313 o390 b1312
3355 B b1313 t1313
3356 T t1314 o1274 b1313
3357 B b1314 t1314
3358 P p1314 Number 5865
3359 P p1315 Number 5939
3360 O o1315 location p1314 p1315
3361 O o1316 str_let p1314 p1315
3362 P p1316 Number 5869
3363 O o1317 patt_var p1316 p1315
3364 O o1318 patt_done p1314 p1315
3365 T t1318 o1318
3366 B b1318 t1318 groupCancelRightT
3367 T t1319 o1317 b1318
3368 B b1319 t1319
3369 O o1319 fun p1316 p1315
3370 O o1320 patt_if p1316 p1315
3371 P p1320 Number 5887
3372 P p1321 Number 5888
3373 O o1321 patt_var p1320 p1321
3374 O o1322 patt_body p1316 p1315
3375 P p1322 Number 5889
3376 P p1323 Number 5890
3377 O o1323 patt_var p1322 p1323
3378 P p1324 Number 5896
3379 O o1324 apply p1324 p1315
3380 P p1325 Number 5937
3381 O o1325 apply p1324 p1325
3382 P p1326 Number 5935
3383 O o1326 apply p1324 p1326
3384 P p1327 Number 5907
3385 O o1327 lid p1324 p1327
3386 O o1328 lid p1070
3387 T t1328 o1328
3388 B b1328 t1328
3389 T t1329 o1327 b1328
3390 B b1329 t1329
3391 P p1329 Number 5909
3392 P p1330 Number 5934
3393 O o1330 apply p1329 p1330
3394 P p1331 Number 5932
3395 O o1331 proj p1329 p1331
3396 O o1332 uid p1329 p1331
3397 T t1332 o1332 b834
3398 B b1332 t1332
3399 P p1332 Number 5918
3400 O o1333 lid p1332 p1331
3401 T t1333 o1333 b836
3402 B b1333 t1333
3403 T t1334 o1331 b1332 b1333
3404 B b1334 t1334
3405 P p1334 Number 5933
3406 O o1334 lid p1334 p1330
3407 T t1335 o1334 b839
3408 B b1335 t1335
3409 T t1336 o1330 b1334 b1335
3410 B b1336 t1336
3411 T t1337 o1326 b1329 b1336
3412 B b1337 t1337
3413 P p1337 Number 5936
3414 O o1337 lid p1337 p1325
3415 T t1338 o1337 b1297
3416 B b1338 t1338
3417 T t1339 o1325 b1337 b1338
3418 B b1339 t1339
3419 P p1339 Number 5938
3420 O o1339 lid p1339 p1315
3421 T t1340 o1339 b839
3422 B b1340 t1340
3423 T t1341 o1324 b1339 b1340
3424 B b1341 t1341
3425 T t1342 o1322 b1341
3426 B b1342 t1342 p
3427 T t1343 o1323 b1342
3428 B b1343 t1343
3429 T t1344 o1320 b1343
3430 B b1344 t1344
3431 T t1345 o1319 b1344
3432 B b1345 t1345
3433 T t1346 o1322 b1345
3434 B b1346 t1346 t
3435 T t1347 o1321 b1346
3436 B b1347 t1347
3437 T t1348 o1320 b1347
3438 B b1348 t1348
3439 T t1349 o1319 b1348
3440 B b1349 t1349
3441 T t1350 o1316 b1319 b1349
3442 B b1350 t1350
3443 T t1351 o b1350 b4
3444 B b1351 t1351
3445 T t1352 o1316 b1351
3446 B b1352 t1352
3447 T t1353 o390 b1352
3448 B b1353 t1353
3449 T t1354 o1315 b1353
3450 B b1354 t1354
3451 P p1354 Number 5957
3452 P p1355 Number 6198
3453 O o1355 location p1354 p1355
3454 P p1356 String unique_id1
3455 O o1356 rule p1356
3456 P p1357 Var e2
3457 O o1357 var p1357
3458 T t1357 o1357
3459 B b1357 t1357
3460 T t1358 o618 b1357
3461 S s1358 t635 h
3462 G s1358 t1358
3463 B b1358 s1358
3464 T t1359 o616 b1358
3465 B b1359 t1359
3466 T t1360 o653 b1357 b552
3467 S s1360 t618 h
3468 G s1360 t1360
3469 B b1360 s1360
3470 T t1361 o616 b1360
3471 B b1361 t1361
3472 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
3473 NCzf_itt_dall!dall dall dall Czf_itt_dall
3474 O o1361 dall
3475 NItt_logic!and and and Itt_logic
3476 O o1362 and
3477 T t1362 o557 b1357 b571
3478 B b1362 t1362
3479 T t1363 o674 b1362 b571
3480 B b1363 t1363
3481 T t1364 o557 b571 b1357
3482 B b1364 t1364
3483 T t1365 o674 b1364 b571
3484 B b1365 t1365
3485 T t1366 o1362 b1363 b1365
3486 B b1366 t1366 s
3487 T t1367 o1361 b552 b1366
3488 H h1367 x t1367
3489 T t1368 o674 b1357 b565
3490 S s1368 t618 h h1367
3491 G s1368 t1368
3492 B b1368 s1368
3493 T t1369 o616 b1368
3494 B b1369 t1369
3495 T t1370 o633 b1361 b1369
3496 B b1370 t1370
3497 T t1371 o633 b1359 b1370
3498 B b1371 t1371
3499 P p1371 String "withT << id >> (dT 2) thenT autoT"
3500 O o1371 ext_rule p1371
3501 T t1372 o b1360 b4
3502 B b1372 t1372
3503 T t1373 o b1358 b1372
3504 B b1373 t1373
3505 T t1374 o925 b1368 b1373
3506 B b1374 t1374
3507 T t1375 o924 b1374 b4 b933
3508 B b1375 t1375
3509 T t1376 o557 b1357 b565
3510 B b1376 t1376
3511 T t1377 o674 b1376 b565
3512 H h1377 y t1377
3513 T t1378 o557 b565 b1357
3514 B b1378 t1378
3515 T t1379 o674 b1378 b565
3516 H h1379 z t1379
3517 S s1379 t618 h h1367 h1377 h1379
3518 G s1379 t1368
3519 B b1379 s1379
3520 T t1380 o925 b1379 b1373
3521 B b1380 t1380
3522 B b1381 t1377
3523 B b1382 t1379
3524 T t1382 o1362 b1381 b1382
3525 H h1382 w t1382
3526 S s1382 t618 h h1367 h1382
3527 G s1382 t1368
3528 B b1383 s1382
3529 T t1383 o925 b1383 b1373
3530 B b1384 t1383
3531 P p1384 String with
3532 O o1384 arg_named p1384
3533 NSummary!arg_term_list arg_term_list arg_term_list Summary
3534 O o1385 arg_term_list
3535 T t1385 o b565 b4
3536 B b1385 t1385
3537 T t1386 o1385 b1385
3538 B b1386 t1386
3539 T t1387 o1384 b1386
3540 B b1387 t1387
3541 T t1388 o b1387 b4
3542 B b1388 t1388
3543 T t1389 o924 b1374 b1388 b933
3544 B b1389 t1389
3545 T t1390 o2 b1389
3546 B b1390 t1390
3547 T t1391 o924 b1384 b4 b1390
3548 B b1391 t1391
3549 T t1392 o2 b1391
3550 B b1392 t1392
3551 T t1393 o924 b1380 b4 b1392
3552 B b1393 t1393
3553 T t1394 o b1393 b4
3554 B b1394 t1394
3555 T t1395 o923 b1375 b1394
3556 B b1395 t1395
3557 P p1395 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
3558 O o1395 ext_rule p1395
3559 T t1396 o923 b1393 b4
3560 B b1396 t1396
3561 T t1397 o1395 b922 b1396 b4 b4
3562 B b1397 t1397
3563 T t1398 o b1397 b4
3564 B b1398 t1398
3565 S s1398 t618 h
3566 G s1398 t1358
3567 B b1399 s1398
3568 T t1399 o b1399 b1372
3569 B b1400 t1399
3570 T t1400 o925 b1379 b1400
3571 B b1401 t1400
3572 T t1401 o925 b1383 b1400
3573 B b1402 t1401
3574 T t1402 o925 b1368 b1400
3575 B b1403 t1402
3576 T t1403 o924 b1403 b1388 b933
3577 B b1404 t1403
3578 T t1404 o2 b1404
3579 B b1405 t1404
3580 T t1405 o924 b1402 b4 b1405
3581 B b1406 t1405
3582 T t1406 o2 b1406
3583 B b1407 t1406
3584 T t1407 o924 b1401 b4 b1407
3585 B b1408 t1407
3586 T t1408 o923 b1408 b4
3587 B b1409 t1408
3588 T t1409 o1395 b922 b1409 b4 b4
3589 B b1410 t1409
3590 P p1410 String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
3591 O o1410 ext_rule p1410
3592 H h1410 v t1368
3593 S s1410 t618 h h1367 h1377 h1379 h1410
3594 G s1410 t1368
3595 B b1411 s1410
3596 T t1411 o925 b1411 b1400
3597 B b1412 t1411
3598 T t1412 o2 b1408
3599 B b1413 t1412
3600 T t1413 o924 b1412 b4 b1413
3601 B b1414 t1413
3602 T t1414 o b1414 b4
3603 B b1415 t1414
3604 T t1415 o923 b1408 b1415
3605 B b1416 t1415
3606 T t1416 o1254 b1414
3607 B b1417 t1416
3608 T t1417 o b1417 b4
3609 B b1418 t1417
3610 T t1418 o1410 b922 b1416 b1418 b4
3611 B b1419 t1418
3612 P p1419 String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
3613 O o1419 ext_rule p1419
3614 P p1420 Var e
3615 O o1420 var p1420
3616 T t1420 o1420
3617 B b1420 t1420
3618 T t1421 o618 b1420
3619 S s1421 t635 h h1367 h1377 h1379
3620 G s1421 t1421
3621 B b1421 s1421
3622 T t1422 o925 b1421 b1400
3623 B b1422 t1422
3624 T t1423 o557 b1357 b1420
3625 B b1423 t1423
3626 T t1424 o618 b1423
3627 S s1424 t635 h h1367 h1377 h1379
3628 G s1424 t1424
3629 B b1424 s1424
3630 T t1425 o925 b1424 b1400
3631 B b1425 t1425
3632 T t1426 o737 b1423 b1357
3633 S s1426 t618 h h1367 h1377 h1379
3634 G s1426 t1426
3635 B b1426 s1426
3636 T t1427 o925 b1426 b1400
3637 B b1427 t1427
3638 T t1428 o953 b1427 b970 b1413
3639 B b1428 t1428
3640 T t1429 o2 b1428
3641 B b1429 t1429
3642 T t1430 o960 b1425 b970 b1429
3643 B b1430 t1430
3644 T t1431 o2 b1430
3645 B b1431 t1431
3646 T t1432 o960 b1422 b4 b1431
3647 B b1432 t1432
3648 T t1433 o674 b1423 b1357
3649 S s1433 t618 h h1367 h1377 h1379
3650 G s1433 t1433
3651 B b1433 s1433
3652 T t1434 o925 b1433 b1400
3653 B b1434 t1434
3654 T t1435 o953 b1434 b4 b1429
3655 B b1435 t1435
3656 H h1435 v t1377
3657 S s1435 t618 h h1367 h1377 h1379 h1435
3658 G s1435 t1368
3659 B b1436 s1435
3660 T t1436 o925 b1436 b1400
3661 B b1437 t1436
3662 T t1437 o924 b1437 b4 b1413
3663 B b1438 t1437
3664 B b1439 t1376 v
3665 T t1439 o710 b1439
3666 S s1439 t618 h h1367 h1377 h1379
3667 G s1439 t1439
3668 B b1440 s1439
3669 T t1440 o925 b1440 b1400
3670 B b1441 t1440
3671 B b1442 t1377 v
3672 T t1442 o963 b1442
3673 S s1442 t618 h h1367 h1377 h1379
3674 G s1442 t1442
3675 B b1443 s1442
3676 T t1443 o925 b1443 b1400
3677 B b1444 t1443
3678 T t1444 o960 b1444 b970 b1413
3679 B b1445 t1444
3680 T t1445 o2 b1445
3681 B b1446 t1445
3682 T t1446 o960 b1441 b4 b1446
3683 B b1447 t1446
3684 T t1447 o b1447 b4
3685 B b1448 t1447
3686 T t1448 o b1438 b1448
3687 B b1449 t1448
3688 T t1449 o b1435 b1449
3689 B b1450 t1449
3690 T t1450 o b1432 b1450
3691 B b1451 t1450
3692 T t1451 o923 b1408 b1451
3693 B b1452 t1451
3694 T t1452 o1254 b1432
3695 B b1453 t1452
3696 T t1453 o1254 b1435
3697 B b1454 t1453
3698 T t1454 o1254 b1438
3699 B b1455 t1454
3700 T t1455 o1254 b1447
3701 B b1456 t1455
3702 T t1456 o b1456 b4
3703 B b1457 t1456
3704 T t1457 o b1455 b1457
3705 B b1458 t1457
3706 T t1458 o b1454 b1458
3707 B b1459 t1458
3708 T t1459 o b1453 b1459
3709 B b1460 t1459
3710 T t1460 o1419 b922 b1452 b1460 b4
3711 B b1461 t1460
3712 T t1461 o b1461 b4
3713 B b1462 t1461
3714 T t1462 o b1461 b1462
3715 B b1463 t1462
3716 T t1463 o b1419 b1463
3717 B b1464 t1463
3718 T t1464 o b1410 b1464
3719 B b1465 t1464
3720 T t1465 o1371 b922 b1395 b1398 b1465
3721 B b1466 t1465
3722 T t1466 o920 b1466
3723 B b1467 t1466
3724 P p1467 Number 5983
3725 P p1468 Number 5991
3726 O o1468 resource_defs p1467 p1468 p262
3727 P p1469 Number 5989
3728 O o1469 uid p1469 p1468
3729 T t1469 o1469 b624
3730 B b1469 t1469
3731 T t1470 o b1469 b4
3732 B b1470 t1470
3733 T t1471 o1468 b1470
3734 B b1471 t1471
3735 T t1472 o b1471 b4
3736 B b1472 t1472
3737 T t1473 o1356 b616 b1371 b1467 b1472
3738 B b1473 t1473
3739 T t1474 o1355 b1473
3740 B b1474 t1474
3741 P p1474 Number 6221
3742 P p1475 Number 6548
3743 O o1475 location p1474 p1475
3744 P p1476 String unique_inv
3745 O o1476 rule p1476
3746 T t1476 o557 b559 b571
3747 B b1476 t1476
3748 T t1477 o737 b1476 b565
3749 H h1477 x t1477
3750 T t1478 o557 b571 b559
3751 B b1478 t1478
3752 T t1479 o737 b1478 b565
3753 H h1479 y t1479
3754 T t1480 o737 b559 b572
3755 S s1480 t618 h h1477 h1479
3756 G s1480 t1480
3757 B b1480 s1480
3758 T t1481 o616 b1480
3759 B b1481 t1481
3760 T t1482 o633 b656 b1481
3761 B b1482 t1482
3762 T t1483 o633 b793 b1482
3763 B b1483 t1483
3764 T t1484 o633 b639 b1483
3765 B b1484 t1484
3766 T t1485 o633 b710 b1484
3767 B b1485 t1485
3768 P p1485 String "assertT << equal{op{inv{'s}; 's}; id} >> thenAT autoT"
3769 O o1485 ext_rule p1485
3770 T t1486 o b655 b4
3771 B b1486 t1486
3772 T t1487 o b792 b1486
3773 B b1487 t1487
3774 T t1488 o b638 b1487
3775 B b1488 t1488
3776 T t1489 o b709 b1488
3777 B b1489 t1489
3778 T t1490 o925 b1480 b1489
3779 B b1490 t1490
3780 T t1491 o924 b1490 b4 b933
3781 B b1491 t1491
3782 T t1492 o557 b572 b571
3783 B b1492 t1492
3784 T t1493 o737 b1492 b565
3785 H h1493 v t1493
3786 S s1493 t618 h h1477 h1479 h1493
3787 G s1493 t1480
3788 B b1493 s1493
3789 T t1494 o925 b1493 b1489
3790 B b1494 t1494
3791 T t1495 o2 b1491
3792 B b1495 t1495
3793 T t1496 o924 b1494 b4 b1495
3794 B b1496 t1496
3795 T t1497 o b1496 b4
3796 B b1497 t1497
3797 T t1498 o923 b1491 b1497
3798 B b1498 t1498
3799 P p1498 String "setSubstT << equal{id; op{inv{'s}; 's}} >> 2 thenAT autoT"
3800 O o1498 ext_rule p1498
3801 T t1499 o674 b565 b1492
3802 S s1499 t618 h h1477 h1479 h1493
3803 G s1499 t1499
3804 B b1499 s1499
3805 T t1500 o925 b1499 b1489
3806 B b1500 t1500
3807 T t1501 o737 b565 b1492
3808 S s1501 t618 h h1477 h1479 h1493
3809 G s1501 t1501
3810 B b1501 s1501
3811 T t1502 o925 b1501 b1489
3812 B b1502 t1502
3813 T t1503 o2 b1496
3814 B b1503 t1503
3815 T t1504 o953 b1502 b970 b1503
3816 B b1504 t1504
3817 T t1505 o2 b1504
3818 B b1505 t1505
3819 T t1506 o953 b1500 b4 b1505
3820 B b1506 t1506
3821 T t1507 o737 b1476 b1492
3822 H h1507 v_1 t1507
3823 S s1507 t618 h h1477 h1479 h1493 h1507
3824 G s1507 t1480
3825 B b1507 s1507
3826 T t1508 o925 b1507 b1489
3827 B b1508 t1508
3828 T t1509 o924 b1508 b4 b1503
3829 B b1509 t1509
3830 B b1510 t1476 v_1
3831 T t1510 o710 b1510
3832 S s1510 t618 h h1477 h1479 h1493
3833 G s1510 t1510
3834 B b1511 s1510
3835 T t1511 o925 b1511 b1489
3836 B b1512 t1511
3837 P p1512 Var v_1
3838 O o1512 var p1512
3839 T t1512 o1512
3840 B b1513 t1512
3841 T t1513 o737 b1476 b1513
3842 B b1514 t1513 v_1
3843 T t1514 o963 b1514
3844 S s1514 t618 h h1477 h1479 h1493
3845 G s1514 t1514
3846 B b1515 s1514
3847 T t1515 o925 b1515 b1489
3848 B b1516 t1515
3849 T t1516 o960 b1516 b970 b1503
3850 B b1517 t1516
3851 T t1517 o2 b1517
3852 B b1518 t1517
3853 T t1518 o960 b1512 b4 b1518
3854 B b1519 t1518
3855 T t1519 o b1519 b4
3856 B b1520 t1519
3857 T t1520 o b1509 b1520
3858 B b1521 t1520
3859 T t1521 o b1506 b1521
3860 B b1522 t1521
3861 T t1522 o923 b1496 b1522
3862 B b1523 t1522
3863 P p1523 String "rwh unfold_equal 4 thenT autoT thenT eqSetSymT thenT autoT"
3864 O o1523 ext_rule p1523
3865 T t1523 o923 b1506 b4
3866 B b1524 t1523
3867 T t1524 o1523 b922 b1524 b4 b4
3868 B b1525 t1524
3869 P p1525 String "groupCancelRightT << 's >> thenT autoT"
3870 O o1525 ext_rule p1525
3871 T t1525 o923 b1509 b4
3872 B b1526 t1525
3873 T t1526 o1525 b922 b1526 b4 b4
3874 B b1527 t1526
3875 T t1527 o923 b1519 b4
3876 B b1528 t1527
3877 T t1528 o1228 b922 b1528 b4 b4
3878 B b1529 t1528
3879 T t1529 o b1529 b4
3880 B b1530 t1529
3881 T t1530 o b1527 b1530
3882 B b1531 t1530
3883 T t1531 o b1525 b1531
3884 B b1532 t1531
3885 T t1532 o1498 b922 b1523 b1532 b4
3886 B b1533 t1532
3887 T t1533 o b1533 b4
3888 B b1534 t1533
3889 T t1534 o1485 b922 b1498 b1534 b4
3890 B b1535 t1534
3891 T t1535 o920 b1535
3892 B b1536 t1535
3893 P p1536 Number 6247
3894 P p1537 Number 6255
3895 O o1537 resource_defs p1536 p1537 p262
3896 P p1538 Number 6253
3897 O o1538 uid p1538 p1537
3898 T t1538 o1538 b624
3899 B b1538 t1538
3900 T t1539 o b1538 b4
3901 B b1539 t1539
3902 T t1540 o1537 b1539
3903 B b1540 t1540
3904 T t1541 o b1540 b4
3905 B b1541 t1541
3906 T t1542 o1476 b616 b1485 b1536 b1541
3907 B b1542 t1542
3908 T t1543 o1475 b1542
3909 B b1543 t1543
3910 P p1543 Number 6599
3911 P p1544 Number 7021
3912 O o1544 location p1543 p1544
3913 P p1545 String unique_sol1
3914 O o1545 rule p1545
3915 P p1546 Var a
3916 O o1546 var p1546
3917 T t1546 o1546
3918 B b1546 t1546
3919 T t1547 o618 b1546
3920 S s1547 t635 h
3921 G s1547 t1547
3922 B b1547 s1547
3923 T t1548 o616 b1547
3924 B b1548 t1548
3925 P p1548 Var b
3926 O o1548 var p1548
3927 T t1549 o1548
3928 B b1549 t1549
3929 T t1550 o618 b1549
3930 S s1550 t635 h
3931 G s1550 t1550
3932 B b1550 s1550
3933 T t1551 o616 b1550
3934 B b1551 t1551
3935 P p1551 Var x
3936 O o1551 var p1551
3937 T t1552 o1551
3938 B b1552 t1552
3939 T t1553 o618 b1552
3940 S s1553 t635 h
3941 G s1553 t1553
3942 B b1553 s1553
3943 T t1554 o616 b1553
3944 B b1554 t1554
3945 T t1555 o653 b1546 b552
3946 S s1555 t618 h
3947 G s1555 t1555
3948 B b1555 s1555
3949 T t1556 o616 b1555
3950 B b1556 t1556
3951 T t1557 o653 b1549 b552
3952 S s1557 t618 h
3953 G s1557 t1557
3954 B b1557 s1557
3955 T t1558 o616 b1557
3956 B b1558 t1558
3957 T t1559 o653 b1552 b552
3958 S s1559 t618 h
3959 G s1559 t1559
3960 B b1559 s1559
3961 T t1560 o616 b1559
3962 B b1560 t1560
3963 T t1561 o557 b1546 b1552
3964 B b1561 t1561
3965 T t1562 o737 b1561 b1549
3966 S s1562 t618 h
3967 G s1562 t1562
3968 B b1562 s1562
3969 T t1563 o616 b1562
3970 B b1563 t1563
3971 T t1564 o570 b1546
3972 B b1564 t1564
3973 T t1565 o557 b1564 b1549
3974 B b1565 t1565
3975 T t1566 o737 b1552 b1565
3976 S s1566 t618 h
3977 G s1566 t1566
3978 B b1566 s1566
3979 T t1567 o616 b1566
3980 B b1567 t1567
3981 T t1568 o633 b1563 b1567
3982 B b1568 t1568
3983 T t1569 o633 b1560 b1568
3984 B b1569 t1569
3985 T t1570 o633 b1558 b1569
3986 B b1570 t1570
3987 T t1571 o633 b1556 b1570
3988 B b1571 t1571
3989 T t1572 o633 b1554 b1571
3990 B b1572 t1572
3991 T t1573 o633 b1551 b1572
3992 B b1573 t1573
3993 T t1574 o633 b1548 b1573
3994 B b1574 t1574
3995 P p1574 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"
3996 O o1574 ext_rule p1574
3997 T t1575 o b1562 b4
3998 B b1575 t1575
3999 T t1576 o b1559 b1575
4000 B b1576 t1576
4001 T t1577 o b1557 b1576
4002 B b1577 t1577
4003 T t1578 o b1555 b1577
4004 B b1578 t1578
4005 T t1579 o b1553 b1578
4006 B b1579 t1579
4007 T t1580 o b1550 b1579
4008 B b1580 t1580
4009 T t1581 o b1547 b1580
4010 B b1581 t1581
4011 T t1582 o925 b1566 b1581
4012 B b1582 t1582
4013 T t1583 o924 b1582 b4 b933
4014 B b1583 t1583
4015 T t1584 o618 b1561
4016 H h1584 y_1 t1584
4017 H h1585 z_1 t1550
4018 T t1585 o674 b1561 b1549
4019 H h1586 z t1585
4020 T t1586 o557 b1564 b1561
4021 B b1586 t1586
4022 T t1587 o737 b1586 b1565
4023 S s1587 t618 h h1584 h1585 h1586
4024 G s1587 t1587
4025 B b1587 s1587
4026 T t1588 o925 b1587 b1581
4027 B b1588 t1588
4028 T t1589 o674 b1552 b1565
4029 S s1589 t618 h h1584 h1585 h1586
4030 G s1589 t1589
4031 B b1589 s1589
4032 T t1590 o925 b1589 b1581
4033 B b1590 t1590
4034 S s1590 t618 h h1584 h1585 h1586
4035 G s1590 t1566
4036 B b1591 s1590
4037 T t1591 o925 b1591 b1581
4038 B b1592 t1591
4039 B b1593 t1584
4040 B b1594 t1550
4041 T t1594 o1362 b1593 b1594
4042 H h1594 y t1594
4043 S s1594 t618 h h1594 h1586
4044 G s1594 t1566
4045 B b1595 s1594
4046 T t1595 o925 b1595 b1581
4047 B b1596 t1595
4048 B b1597 t1594
4049 B b1598 t1585
4050 T t1598 o1362 b1597 b1598
4051 H h1598 v t1598
4052 S s1598 t618 h h1598
4053 G s1598 t1566
4054 B b1599 s1598
4055 T t1599 o925 b1599 b1581
4056 B b1600 t1599
4057 H h1600 v t1562
4058 S s1600 t618 h h1600
4059 G s1600 t1566
4060 B b1601 s1600
4061 T t1601 o925 b1601 b1581
4062 B b1602 t1601
4063 T t1602 o2 b1583
4064 B b1603 t1602
4065 T t1603 o924 b1602 b4 b1603
4066 B b1604 t1603
4067 T t1604 o2 b1604
4068 B b1605 t1604
4069 T t1605 o924 b1600 b4 b1605
4070 B b1606 t1605
4071 T t1606 o2 b1606
4072 B b1607 t1606
4073 T t1607 o924 b1596 b4 b1607
4074 B b1608 t1607
4075 T t1608 o2 b1608
4076 B b1609 t1608
4077 T t1609 o924 b1592 b970 b1609
4078 B b1610 t1609
4079 T t1610 o2 b1610
4080 B b1611 t1610
4081 T t1611 o924 b1590 b4 b1611
4082 B b1612 t1611
4083 T t1612 o2 b1612
4084 B b1613 t1612
4085 T t1613 o934 b1588 b4 b1613
4086 B b1614 t1613
4087 H h1614 v t1587
4088 S s1614 t618 h h1584 h1585 h1586 h1614
4089 G s1614 t1589
4090 B b1615 s1614
4091 T t1615 o925 b1615 b1581
4092 B b1616 t1615
4093 T t1616 o924 b1616 b4 b1613
4094 B b1617 t1616
4095 T t1617 o b1617 b4
4096 B b1618 t1617
4097 T t1618 o b1614 b1618
4098 B b1619 t1618
4099 T t1619 o923 b1583 b1619
4100 B b1620 t1619
4101 T t1620 o923 b1614 b4
4102 B b1621 t1620
4103 T t1621 o977 b922 b1621 b4 b4
4104 B b1622 t1621
4105 P p1622 String "setSubstT << equal{op{inv{'a}; op{'a; 'x}}; op{op{inv{'a}; 'a}; 'x}} >> 5 thenT autoT"
4106 O o1622 ext_rule p1622
4107 T t1622 o557 b1564 b1546
4108 B b1623 t1622
4109 T t1623 o557 b1623 b1552
4110 B b1624 t1623
4111 T t1624 o737 b1624 b1565
4112 H h1624 v_1 t1624
4113 S s1624 t618 h h1584 h1585 h1586 h1614 h1624
4114 G s1624 t1589
4115 B b1625 s1624
4116 T t1625 o925 b1625 b1581
4117 B b1626 t1625
4118 T t1626 o2 b1617
4119 B b1627 t1626
4120 T t1627 o924 b1626 b4 b1627
4121 B b1628 t1627
4122 B b1629 t1565 v_1
4123 T t1629 o710 b1629
4124 S s1629 t618 h h1584 h1585 h1586 h1614
4125 G s1629 t1629
4126 B b1630 s1629
4127 T t1630 o925 b1630 b1581
4128 B b1631 t1630
4129 T t1631 o737 b1513 b1565
4130 B b1632 t1631 v_1
4131 T t1632 o963 b1632
4132 S s1632 t618 h h1584 h1585 h1586 h1614
4133 G s1632 t1632
4134 B b1633 s1632
4135 T t1633 o925 b1633 b1581
4136 B b1634 t1633
4137 T t1634 o960 b1634 b970 b1627
4138 B b1635 t1634
4139 T t1635 o2 b1635
4140 B b1636 t1635
4141 T t1636 o960 b1631 b4 b1636
4142 B b1637 t1636
4143 T t1637 o b1637 b4
4144 B b1638 t1637
4145 T t1638 o b1628 b1638
4146 B b1639 t1638
4147 T t1639 o923 b1617 b1639
4148 B b1640 t1639
4149 P p1640 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 6 thenT autoT"
4150 O o1640 ext_rule p1640
4151 T t1640 o557 b565 b1552
4152 B b1641 t1640
4153 T t1641 o737 b1641 b1565
4154 H h1641 v_2 t1641
4155 S s1641 t618 h h1584 h1585 h1586 h1614 h1624 h1641
4156 G s1641 t1589
4157 B b1642 s1641
4158 T t1642 o925 b1642 b1581
4159 B b1643 t1642
4160 T t1643 o2 b1628
4161 B b1644 t1643
4162 T t1644 o924 b1643 b4 b1644
4163 B b1645 t1644
4164 B b1646 t1565 v_2
4165 T t1646 o710 b1646
4166 S s1646 t618 h h1584 h1585 h1586 h1614 h1624
4167 G s1646 t1646
4168 B b1647 s1646
4169 T t1647 o925 b1647 b1581
4170 B b1648 t1647
4171 T t1648 o557 b964 b1552
4172 B b1649 t1648
4173 T t1649 o737 b1649 b1565
4174 B b1650 t1649 v_2
4175 T t1650 o963 b1650
4176 S s1650 t618 h h1584 h1585 h1586 h1614 h1624
4177 G s1650 t1650
4178 B b1651 s1650
4179 T t1651 o925 b1651 b1581
4180 B b1652 t1651
4181 T t1652 o960 b1652 b970 b1644
4182 B b1653 t1652
4183 T t1653 o2 b1653
4184 B b1654 t1653
4185 T t1654 o960 b1648 b4 b1654
4186 B b1655 t1654
4187 T t1655 o b1655 b4
4188 B b1656 t1655
4189 T t1656 o b1645 b1656
4190 B b1657 t1656
4191 T t1657 o923 b1628 b1657
4192 B b1658 t1657
4193 P p1658 String "setSubstT << equal{op{id; 'x}; 'x} >> 7 thenT autoT"
4194 O o1658 ext_rule p1658
4195 H h1658 v_3 t1566
4196 S s1658 t618 h h1584 h1585 h1586 h1614 h1624 h1641 h1658
4197 G s1658 t1589
4198 B b1659 s1658
4199 T t1659 o925 b1659 b1581
4200 B b1660 t1659
4201 T t1660 o2 b1645
4202 B b1661 t1660
4203 T t1661 o924 b1660 b4 b1661
4204 B b1662 t1661
4205 B b1663 t1565 v_3
4206 T t1663 o710 b1663
4207 S s1663 t618 h h1584 h1585 h1586 h1614 h1624 h1641
4208 G s1663 t1663
4209 B b1664 s1663
4210 T t1664 o925 b1664 b1581
4211 B b1665 t1664
4212 T t1665 o737 b991 b1565
4213 B b1666 t1665 v_3
4214 T t1666 o963 b1666
4215 S s1666 t618 h h1584 h1585 h1586 h1614 h1624 h1641
4216 G s1666 t1666
4217 B b1667 s1666
4218 T t1667 o925 b1667 b1581
4219 B b1668 t1667
4220 T t1668 o960 b1668 b970 b1661
4221 B b1669 t1668
4222 T t1669 o2 b1669
4223 B b1670 t1669
4224 T t1670 o960 b1665 b4 b1670
4225 B b1671 t1670
4226 T t1671 o b1671 b4
4227 B b1672 t1671
4228 T t1672 o b1662 b1672
4229 B b1673 t1672
4230 T t1673 o923 b1645 b1673
4231 B b1674 t1673
4232 P p1674 String "rwh unfold_equal 8 thenT autoT"
4233 O o1674 ext_rule p1674
4234 T t1674 o923 b1662 b4
4235 B b1675 t1674
4236 T t1675 o1674 b922 b1675 b4 b4
4237 B b1676 t1675
4238 T t1676 o923 b1671 b4
4239 B b1677 t1676
4240 T t1677 o1228 b922 b1677 b4 b4
4241 B b1678 t1677
4242 T t1678 o b1678 b4
4243 B b1679 t1678
4244 T t1679 o b1676 b1679
4245 B b1680 t1679
4246 T t1680 o1658 b922 b1674 b1680 b4
4247 B b1681 t1680
4248 T t1681 o923 b1655 b4
4249 B b1682 t1681
4250 T t1682 o1228 b922 b1682 b4 b4
4251 B b1683 t1682
4252 T t1683 o b1683 b4
4253 B b1684 t1683
4254 T t1684 o b1681 b1684
4255 B b1685 t1684
4256 T t1685 o1640 b922 b1658 b1685 b4
4257 B b1686 t1685
4258 T t1686 o923 b1637 b4
4259 B b1687 t1686
4260 T t1687 o1228 b922 b1687 b4 b4
4261 B b1688 t1687
4262 T t1688 o b1688 b4
4263 B b1689 t1688
4264 T t1689 o b1686 b1689
4265 B b1690 t1689
4266 T t1690 o737 b1586 b1624
4267 S s1690 t618 h h1584 h1585 h1586 h1614
4268 G s1690 t1690
4269 B b1691 s1690
4270 T t1691 o925 b1691 b1581
4271 B b1692 t1691
4272 T t1692 o953 b1692 b4 b1627
4273 B b1693 t1692
4274 T t1693 o923 b1693 b4
4275 B b1694 t1693
4276 T t1694 o977 b922 b1694 b4 b4
4277 B b1695 t1694
4278 P p1695 String "rwh unfold_fun_prop 0 thenT autoT thenT rwh unfold_equal 9 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 11 thenT autoT"
4279 O o1695 ext_rule p1695
4280 T t1695 o960 b1634 b4 b1627
4281 B b1696 t1695
4282 H h1696 s1 t1229
4283 H h1697 x_1 t1075
4284 H h1698 y_2 t636
4285 T t1698 o618 b1565
4286 H h1699 z_3 t1698
4287 T t1699 o674 b558 b1565
4288 H h1700 z_2 t1699
4289 S s1700 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697 h1698 h1699 h1700
4290 G s1700 t1629
4291 B b1700 s1700
4292 T t1700 o925 b1700 b1581
4293 B b1701 t1700
4294 T t1701 o674 b1513 b1565
4295 B b1702 t1701 v_1
4296 T t1702 o963 b1702
4297 S s1702 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697 h1698 h1699 h1700
4298 G s1702 t1702
4299 B b1703 s1702
4300 T t1703 o925 b1703 b1581
4301 B b1704 t1703
4302 T t1704 o674 b559 b1565
4303 S s1704 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697 h1698 h1699 h1700
4304 G s1704 t1704
4305 B b1705 s1704
4306 T t1705 o925 b1705 b1581
4307 B b1706 t1705
4308 B b1707 t636
4309 B b1708 t1698
4310 T t1708 o1362 b1707 b1708
4311 H h1708 y t1708
4312 S s1708 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697 h1708 h1700
4313 G s1708 t1704
4314 B b1709 s1708
4315 T t1709 o925 b1709 b1581
4316 B b1710 t1709
4317 B b1711 t1708
4318 B b1712 t1699
4319 T t1712 o1362 b1711 b1712
4320 H h1712 x_2 t1712
4321 S s1712 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697 h1712
4322 G s1712 t1704
4323 B b1713 s1712
4324 T t1713 o925 b1713 b1581
4325 B b1714 t1713
4326 T t1714 o737 b558 b1565
4327 H h1714 x_2 t1714
4328 S s1714 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697 h1714
4329 G s1714 t1704
4330 B b1715 s1714
4331 T t1715 o925 b1715 b1581
4332 B b1716 t1715
4333 T t1716 o737 b559 b1565
4334 S s1716 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697 h1714
4335 G s1716 t1716
4336 B b1717 s1716
4337 T t1717 o925 b1717 b1581
4338 B b1718 t1717
4339 B b1719 t1714
4340 B b1720 t1716
4341 T t1720 o1233 b1719 b1720
4342 S s1720 t618 h h1584 h1585 h1586 h1614 h1696 h1230 h1697
4343 G s1720 t1720
4344 B b1721 s1720
4345 T t1721 o925 b1721 b1581
4346 B b1722 t1721
4347 B b1723 t1075
4348 B b1724 t1720
4349 T t1724 o1233 b1723 b1724
4350 S s1724 t618 h h1584 h1585 h1586 h1614 h1696 h1230
4351 G s1724 t1724
4352 B b1725 s1724
4353 T t1725 o925 b1725 b1581
4354 B b1726 t1725
4355 B b1727 t1724 s2
4356 T t1727 o1237 b1238 b1727
4357 S s1727 t618 h h1584 h1585 h1586 h1614 h1696
4358 G s1727 t1727
4359 B b1728 s1727
4360 T t1728 o925 b1728 b1581
4361 B b1729 t1728
4362 B b1730 t1727 s1
4363 T t1730 o1237 b1238 b1730
4364 S s1730 t618 h h1584 h1585 h1586 h1614
4365 G s1730 t1730
4366 B b1731 s1730
4367 T t1731 o925 b1731 b1581
4368 B b1732 t1731
4369 T t1732 o2 b1696
4370 B b1733 t1732
4371 T t1733 o960 b1732 b970 b1733
4372 B b1734 t1733
4373 T t1734 o2 b1734
4374 B b1735 t1734
4375 T t1735 o924 b1729 b970 b1735
4376 B b1736 t1735
4377 T t1736 o2 b1736
4378 B b1737 t1736
4379 T t1737 o924 b1726 b970 b1737
4380 B b1738 t1737
4381 T t1738 o2 b1738
4382 B b1739 t1738
4383 T t1739 o924 b1722 b970 b1739
4384 B b1740 t1739
4385 T t1740 o2 b1740
4386 B b1741 t1740
4387 T t1741 o924 b1718 b970 b1741
4388 B b1742 t1741
4389 T t1742 o2 b1742
4390 B b1743 t1742
4391 T t1743 o924 b1716 b4 b1743
4392 B b1744 t1743
4393 T t1744 o2 b1744
4394 B b1745 t1744
4395 T t1745 o924 b1714 b4 b1745
4396 B b1746 t1745
4397 T t1746 o2 b1746
4398 B b1747 t1746
4399 T t1747 o924 b1710 b4 b1747
4400 B b1748 t1747
4401 T t1748 o2 b1748
4402 B b1749 t1748
4403 T t1749 o924 b1706 b4 b1749
4404 B b1750 t1749
4405 T t1750 o2 b1750
4406 B b1751 t1750
4407 T t1751 o960 b1704 b970 b1751
4408 B b1752 t1751
4409 T t1752 o2 b1752
4410 B b1753 t1752
4411 T t1753 o960 b1701 b4 b1753
4412 B b1754 t1753
4413 T t1754 o b1754 b4
4414 B b1755 t1754
4415 T t1755 o923 b1696 b1755
4416 B b1756 t1755
4417 T t1756 o923 b1754 b4
4418 B b1757 t1756
4419 T t1757 o1228 b922 b1757 b4 b4
4420 B b1758 t1757
4421 T t1758 o b1758 b4
4422 B b1759 t1758
4423 T t1759 o1695 b922 b1756 b1759 b4
4424 B b1760 t1759
4425 T t1760 o b1760 b4
4426 B b1761 t1760
4427 T t1761 o b1695 b1761
4428 B b1762 t1761
4429 T t1762 o1622 b922 b1640 b1690 b1762
4430 B b1763 t1762
4431 T t1763 o b1763 b4
4432 B b1764 t1763
4433 T t1764 o b1622 b1764
4434 B b1765 t1764
4435 T t1765 o1574 b922 b1620 b1765 b4
4436 B b1766 t1765
4437 T t1766 o920 b1766
4438 B b1767 t1766
4439 P p1767 Number 6626
4440 P p1768 Number 6634
4441 O o1768 resource_defs p1767 p1768 p262
4442 P p1769 Number 6632
4443 O o1769 uid p1769 p1768
4444 T t1769 o1769 b624
4445 B b1769 t1769
4446 T t1770 o b1769 b4
4447 B b1770 t1770
4448 T t1771 o1768 b1770
4449 B b1771 t1771
4450 T t1772 o b1771 b4
4451 B b1772 t1772
4452 T t1773 o1545 b616 b1574 b1767 b1772
4453 B b1773 t1773
4454 T t1774 o1544 b1773
4455 B b1774 t1774
4456 P p1774 Number 7072
4457 P p1775 Number 7494
4458 O o1775 location p1774 p1775
4459 P p1776 String unique_sol2
4460 O o1776 rule p1776
4461 P p1777 Var y
4462 O o1777 var p1777
4463 T t1777 o1777
4464 B b1777 t1777
4465 T t1778 o618 b1777
4466 S s1778 t635 h
4467 G s1778 t1778
4468 B b1778 s1778
4469 T t1779 o616 b1778
4470 B b1779 t1779
4471 T t1780 o653 b1777 b552
4472 S s1780 t618 h
4473 G s1780 t1780
4474 B b1780 s1780
4475 T t1781 o616 b1780
4476 B b1781 t1781
4477 T t1782 o557 b1777 b1546
4478 B b1782 t1782
4479 T t1783 o737 b1782 b1549
4480 S s1783 t618 h
4481 G s1783 t1783
4482 B b1783 s1783
4483 T t1784 o616 b1783
4484 B b1784 t1784
4485 T t1785 o557 b1549 b1564
4486 B b1785 t1785
4487 T t1786 o737 b1777 b1785
4488 S s1786 t618 h
4489 G s1786 t1786
4490 B b1786 s1786
4491 T t1787 o616 b1786
4492 B b1787 t1787
4493 T t1788 o633 b1784 b1787
4494 B b1788 t1788
4495 T t1789 o633 b1781 b1788
4496 B b1789 t1789
4497 T t1790 o633 b1558 b1789
4498 B b1790 t1790
4499 T t1791 o633 b1556 b1790
4500 B b1791 t1791
4501 T t1792 o633 b1779 b1791
4502 B b1792 t1792
4503 T t1793 o633 b1551 b1792
4504 B b1793 t1793
4505 T t1794 o633 b1548 b1793
4506 B b1794 t1794
4507 P p1794 String "assumT 7 thenT assertT << equal{op{op{'y; 'a}; inv{'a}}; op{'b; inv{'a}}} >> thenT autoT"
4508 O o1794 ext_rule p1794
4509 T t1795 o b1783 b4
4510 B b1795 t1795
4511 T t1796 o b1780 b1795
4512 B b1796 t1796
4513 T t1797 o b1557 b1796
4514 B b1797 t1797
4515 T t1798 o b1555 b1797
4516 B b1798 t1798
4517 T t1799 o b1778 b1798
4518 B b1799 t1799
4519 T t1800 o b1550 b1799
4520 B b1800 t1800
4521 T t1801 o b1547 b1800
4522 B b1801 t1801
4523 T t1802 o925 b1786 b1801
4524 B b1802 t1802
4525 T t1803 o924 b1802 b4 b933
4526 B b1803 t1803
4527 H h1803 v t1783
4528 T t1804 o674 b1782 b1549
4529 S s1804 t618 h h1803
4530 G s1804 t1804
4531 B b1804 s1804
4532 T t1805 o925 b1804 b1801
4533 B b1805 t1805
4534 T t1806 o557 b1782 b1564
4535 B b1806 t1806
4536 T t1807 o674 b1806 b1785
4537 S s1807 t618 h h1803
4538 G s1807 t1807
4539 B b1807 s1807
4540 T t1808 o925 b1807 b1801
4541 B b1808 t1808
4542 T t1809 o737 b1806 b1785
4543 S s1809 t618 h h1803
4544 G s1809 t1809
4545 B b1809 s1809
4546 T t1810 o925 b1809 b1801
4547 B b1810 t1810
4548 S s1810 t618 h h1803
4549 G s1810 t1786
4550 B b1811 s1810
4551 T t1811 o925 b1811 b1801
4552 B b1812 t1811
4553 T t1812 o2 b1803
4554 B b1813 t1812
4555 T t1813 o924 b1812 b4 b1813
4556 B b1814 t1813
4557 T t1814 o2 b1814
4558 B b1815 t1814
4559 T t1815 o934 b1810 b970 b1815
4560 B b1816 t1815
4561 T t1816 o2 b1816
4562 B b1817 t1816
4563 T t1817 o934 b1808 b970 b1817
4564 B b1818 t1817
4565 T t1818 o2 b1818
4566 B b1819 t1818
4567 T t1819 o934 b1805 b4 b1819
4568 B b1820 t1819
4569 H h1820 v_1 t1809
4570 T t1820 o674 b1777 b1785
4571 S s1820 t618 h h1803 h1820
4572 G s1820 t1820
4573 B b1821 s1820
4574 T t1821 o925 b1821 b1801
4575 B b1822 t1821
4576 S s1822 t618 h h1803 h1820
4577 G s1822 t1786
4578 B b1823 s1822
4579 T t1823 o925 b1823 b1801
4580 B b1824 t1823
4581 T t1824 o924 b1824 b970 b1815
4582 B b1825 t1824
4583 T t1825 o2 b1825
4584 B b1826 t1825
4585 T t1826 o924 b1822 b4 b1826
4586 B b1827 t1826
4587 T t1827 o b1827 b4
4588 B b1828 t1827
4589 T t1828 o b1820 b1828
4590 B b1829 t1828
4591 T t1829 o923 b1803 b1829
4592 B b1830 t1829
4593 P p1830 String "rwh unfold_equal 2 thenT autoT"
4594 O o1830 ext_rule p1830
4595 T t1830 o923 b1820 b4
4596 B b1831 t1830
4597 T t1831 o1830 b922 b1831 b4 b4
4598 B b1832 t1831
4599 P p1832 String "setSubstT << equal{op{op{'y; 'a}; inv{'a}}; op{'y; op{'a; inv{'a}}}} >> 3 thenT autoT"
4600 O o1832 ext_rule p1832
4601 T t1832 o557 b1546 b1564
4602 B b1833 t1832
4603 T t1833 o557 b1777 b1833
4604 B b1834 t1833
4605 T t1834 o737 b1834 b1785
4606 H h1834 v_2 t1834
4607 S s1834 t618 h h1803 h1820 h1834
4608 G s1834 t1820
4609 B b1835 s1834
4610 T t1835 o925 b1835 b1801
4611 B b1836 t1835
4612 T t1836 o2 b1827
4613 B b1837 t1836
4614 T t1837 o924 b1836 b4 b1837
4615 B b1838 t1837
4616 B b1839 t1785 v_2
4617 T t1839 o710 b1839
4618 S s1839 t618 h h1803 h1820
4619 G s1839 t1839
4620 B b1840 s1839
4621 T t1840 o925 b1840 b1801
4622 B b1841 t1840
4623 T t1841 o737 b964 b1785
4624 B b1842 t1841 v_2
4625 T t1842 o963 b1842
4626 S s1842 t618 h h1803 h1820
4627 G s1842 t1842
4628 B b1843 s1842
4629 T t1843 o925 b1843 b1801
4630 B b1844 t1843
4631 T t1844 o960 b1844 b970 b1837
4632 B b1845 t1844
4633 T t1845 o2 b1845
4634 B b1846 t1845
4635 T t1846 o960 b1841 b4 b1846
4636 B b1847 t1846
4637 T t1847 o b1847 b4
4638 B b1848 t1847
4639 T t1848 o b1838 b1848
4640 B b1849 t1848
4641 T t1849 o923 b1827 b1849
4642 B b1850 t1849
4643 P p1850 String "setSubstT << equal{op{'a; inv{'a}}; id} >> 4 thenT autoT"
4644 O o1850 ext_rule p1850
4645 T t1850 o557 b1777 b565
4646 B b1851 t1850
4647 T t1851 o737 b1851 b1785
4648 H h1851 v_3 t1851
4649 S s1851 t618 h h1803 h1820 h1834 h1851
4650 G s1851 t1820
4651 B b1852 s1851
4652 T t1852 o925 b1852 b1801
4653 B b1853 t1852
4654 T t1853 o2 b1838
4655 B b1854 t1853
4656 T t1854 o924 b1853 b4 b1854
4657 B b1855 t1854
4658 B b1856 t1785 v_3
4659 T t1856 o710 b1856
4660 S s1856 t618 h h1803 h1820 h1834
4661 G s1856 t1856
4662 B b1857 s1856
4663 T t1857 o925 b1857 b1801
4664 B b1858 t1857
4665 T t1858 o557 b1777 b991
4666 B b1859 t1858
4667 T t1859 o737 b1859 b1785
4668 B b1860 t1859 v_3
4669 T t1860 o963 b1860
4670 S s1860 t618 h h1803 h1820 h1834
4671 G s1860 t1860
4672 B b1861 s1860
4673 T t1861 o925 b1861 b1801
4674 B b1862 t1861
4675 T t1862 o960 b1862 b970 b1854
4676 B b1863 t1862
4677 T t1863 o2 b1863
4678 B b1864 t1863
4679 T t1864 o960 b1858 b4 b1864
4680 B b1865 t1864
4681 T t1865 o b1865 b4
4682 B b1866 t1865
4683 T t1866 o b1855 b1866
4684 B b1867 t1866
4685 T t1867 o923 b1838 b1867
4686 B b1868 t1867
4687 P p1868 String "rwh unfold_equal 5 thenT autoT thenT setSubstT << equal{op{'y; id}; 'y}>> 7 thenT autoT"
4688 O o1868 ext_rule p1868
4689 T t1868 o618 b1851
4690 H h1868 y_2 t1868
4691 T t1869 o618 b1785
4692 H h1869 z_1 t1869
4693 T t1870 o674 b1851 b1785
4694 H h1870 z t1870
4695 S s1870 t618 h h1803 h1820 h1834 h1868 h1869 h1870
4696 G s1870 t1856
4697 B b1870 s1870
4698 T t1871 o925 b1870 b1801
4699 B b1871 t1871
4700 T t1872 o674 b991 b1785
4701 B b1872 t1872 v_3
4702 T t1873 o963 b1872
4703 S s1873 t618 h h1803 h1820 h1834 h1868 h1869 h1870
4704 G s1873 t1873
4705 B b1873 s1873
4706 T t1874 o925 b1873 b1801
4707 B b1874 t1874
4708 S s1874 t618 h h1803 h1820 h1834 h1868 h1869 h1870
4709 G s1874 t1820
4710 B b1875 s1874
4711 T t1875 o925 b1875 b1801
4712 B b1876 t1875
4713 B b1877 t1868
4714 B b1878 t1869
4715 T t1878 o1362 b1877 b1878
4716 H h1878 y_1 t1878
4717 S s1878 t618 h h1803 h1820 h1834 h1878 h1870
4718 G s1878 t1820
4719 B b1879 s1878
4720 T t1879 o925 b1879 b1801
4721 B b1880 t1879
4722 B b1881 t1878
4723 B b1882 t1870
4724 T t1882 o1362 b1881 b1882
4725 H h1882 v_3 t1882
4726 S s1882 t618 h h1803 h1820 h1834 h1882
4727 G s1882 t1820
4728 B b1883 s1882
4729 T t1883 o925 b1883 b1801
4730 B b1884 t1883
4731 T t1884 o2 b1855
4732 B b1885 t1884
4733 T t1885 o924 b1884 b4 b1885
4734 B b1886 t1885
4735 T t1886 o2 b1886
4736 B b1887 t1886
4737 T t1887 o924 b1880 b4 b1887
4738 B b1888 t1887
4739 T t1888 o2 b1888
4740 B b1889 t1888
4741 T t1889 o924 b1876 b4 b1889
4742 B b1890 t1889
4743 T t1890 o2 b1890
4744 B b1891 t1890
4745 T t1891 o960 b1874 b970 b1891
4746 B b1892 t1891
4747 T t1892 o2 b1892
4748 B b1893 t1892
4749 T t1893 o960 b1871 b4 b1893
4750 B b1894 t1893
4751 T t1894 o b1894 b4
4752 B b1895 t1894
4753 T t1895 o923 b1855 b1895
4754 B b1896 t1895
4755 T t1896 o923 b1894 b4
4756 B b1897 t1896
4757 T t1897 o1228 b922 b1897 b4 b4
4758 B b1898 t1897
4759 T t1898 o b1898 b4
4760 B b1899 t1898
4761 T t1899 o1868 b922 b1896 b1899 b4
4762 B b1900 t1899
4763 T t1900 o923 b1865 b4
4764 B b1901 t1900
4765 T t1901 o1228 b922 b1901 b4 b4
4766 B b1902 t1901
4767 T t1902 o b1902 b4
4768 B b1903 t1902
4769 T t1903 o b1900 b1903
4770 B b1904 t1903
4771 T t1904 o1850 b922 b1868 b1904 b4
4772 B b1905 t1904
4773 T t1905 o923 b1847 b4
4774 B b1906 t1905
4775 T t1906 o1228 b922 b1906 b4 b4
4776 B b1907 t1906
4777 T t1907 o b1907 b4
4778 B b1908 t1907
4779 T t1908 o b1905 b1908
4780 B b1909 t1908
4781 T t1909 o1832 b922 b1850 b1909 b4
4782 B b1910 t1909
4783 T t1910 o b1910 b4
4784 B b1911 t1910
4785 T t1911 o b1832 b1911
4786 B b1912 t1911
4787 T t1912 o1794 b922 b1830 b1912 b4
4788 B b1913 t1912
4789 T t1913 o920 b1913
4790 B b1914 t1913
4791 P p1914 Number 7099
4792 P p1915 Number 7107
4793 O o1915 resource_defs p1914 p1915 p262
4794 P p1916 Number 7105
4795 O o1916 uid p1916 p1915
4796 T t1916 o1916 b624
4797 B b1916 t1916
4798 T t1917 o b1916 b4
4799 B b1917 t1917
4800 T t1918 o1915 b1917
4801 B b1918 t1918
4802 T t1919 o b1918 b4
4803 B b1919 t1919
4804 T t1920 o1776 b616 b1794 b1914 b1919
4805 B b1920 t1920
4806 T t1921 o1775 b1920
4807 B b1921 t1921
4808 P p1921 Number 7522
4809 P p1922 Number 7820
4810 O o1922 location p1921 p1922
4811 P p1923 String inv_simplify
4812 O o1923 rule p1923
4813 T t1923 o557 b1546 b1549
4814 B b1923 t1923
4815 T t1924 o570 b1923
4816 B b1924 t1924
4817 T t1925 o570 b1549
4818 B b1925 t1925
4819 T t1926 o557 b1925 b1564
4820 B b1926 t1926
4821 T t1927 o737 b1924 b1926
4822 S s1927 t618 h
4823 G s1927 t1927
4824 B b1927 s1927
4825 T t1928 o616 b1927
4826 B b1928 t1928
4827 T t1929 o633 b1558 b1928
4828 B b1929 t1929
4829 T t1930 o633 b1556 b1929
4830 B b1930 t1930
4831 T t1931 o633 b1551 b1930
4832 B b1931 t1931
4833 T t1932 o633 b1548 b1931
4834 B b1932 t1932
4835 P p1932 String "assertT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; op{op{inv{'b}; inv{'a}}; op{'a; 'b}}} >> thenAT autoT"
4836 O o1932 ext_rule p1932
4837 T t1933 o b1557 b4
4838 B b1933 t1933
4839 T t1934 o b1555 b1933
4840 B b1934 t1934
4841 T t1935 o b1550 b1934
4842 B b1935 t1935
4843 T t1936 o b1547 b1935
4844 B b1936 t1936
4845 T t1937 o925 b1927 b1936
4846 B b1937 t1937
4847 T t1938 o924 b1937 b4 b933
4848 B b1938 t1938
4849 T t1939 o557 b1924 b1923
4850 B b1939 t1939
4851 T t1940 o557 b1926 b1923
4852 B b1940 t1940
4853 T t1941 o737 b1939 b1940
4854 S s1941 t618 h
4855 G s1941 t1941
4856 B b1941 s1941
4857 T t1942 o925 b1941 b1936
4858 B b1942 t1942
4859 T t1943 o2 b1938
4860 B b1943 t1943
4861 T t1944 o934 b1942 b4 b1943
4862 B b1944 t1944
4863 H h1944 v t1941
4864 S s1944 t618 h h1944
4865 G s1944 t1927
4866 B b1945 s1944
4867 T t1945 o925 b1945 b1936
4868 B b1946 t1945
4869 T t1946 o924 b1946 b4 b1943
4870 B b1947 t1946
4871 T t1947 o b1947 b4
4872 B b1948 t1947
4873 T t1948 o b1944 b1948
4874 B b1949 t1948
4875 T t1949 o923 b1938 b1949
4876 B b1950 t1949
4877 P p1950 String "setSubstT << equal{op{inv{op{'a; 'b}}; op{'a; 'b}}; id} >> 0 thenWT autoT"
4878 O o1950 ext_rule p1950
4879 T t1950 o737 b1939 b565
4880 S s1950 t618 h
4881 G s1950 t1950
4882 B b1951 s1950
4883 T t1951 o925 b1951 b1936
4884 B b1952 t1951
4885 T t1952 o2 b1944
4886 B b1953 t1952
4887 T t1953 o953 b1952 b4 b1953
4888 B b1954 t1953
4889 T t1954 o737 b565 b1940
4890 S s1954 t618 h
4891 G s1954 t1954
4892 B b1955 s1954
4893 T t1955 o925 b1955 b1936
4894 B b1956 t1955
4895 T t1956 o924 b1956 b4 b1953
4896 B b1957 t1956
4897 B b1958 t1940 v
4898 T t1958 o710 b1958
4899 S s1958 t618 h
4900 G s1958 t1958
4901 B b1959 s1958
4902 T t1959 o925 b1959 b1936
4903 B b1960 t1959
4904 P p1960 Var v
4905 O o1960 var p1960
4906 T t1960 o1960
4907 B b1961 t1960
4908 T t1961 o737 b1961 b1940
4909 B b1962 t1961 v
4910 T t1962 o963 b1962
4911 S s1962 t618 h
4912 G s1962 t1962
4913 B b1963 s1962
4914 T t1963 o925 b1963 b1936
4915 B b1964 t1963
4916 T t1964 o960 b1964 b970 b1953
4917 B b1965 t1964
4918 T t1965 o2 b1965
4919 B b1966 t1965
4920 T t1966 o960 b1960 b4 b1966
4921 B b1967 t1966
4922 T t1967 o b1967 b4
4923 B b1968 t1967
4924 T t1968 o b1957 b1968
4925 B b1969 t1968
4926 T t1969 o b1954 b1969
4927 B b1970 t1969
4928 T t1970 o923 b1944 b1970
4929 B b1971 t1970
4930 T t1971 o923 b1954 b4
4931 B b1972 t1971
4932 T t1972 o977 b922 b1972 b4 b4
4933 B b1973 t1972
4934 P p1973 String "setSubstT << equal{id; op{inv{'b}; op{inv{'a}; op{'a; 'b}}}} >> 0 thenWT autoT"
4935 O o1973 ext_rule p1973
4936 T t1973 o557 b1564 b1923
4937 B b1974 t1973
4938 T t1974 o557 b1925 b1974
4939 B b1975 t1974
4940 T t1975 o737 b565 b1975
4941 S s1975 t618 h
4942 G s1975 t1975
4943 B b1976 s1975
4944 T t1976 o925 b1976 b1936
4945 B b1977 t1976
4946 T t1977 o2 b1957
4947 B b1978 t1977
4948 T t1978 o953 b1977 b4 b1978
4949 B b1979 t1978
4950 T t1979 o737 b1975 b1940
4951 S s1979 t618 h
4952 G s1979 t1979
4953 B b1980 s1979
4954 T t1980 o925 b1980 b1936
4955 B b1981 t1980
4956 T t1981 o924 b1981 b4 b1978
4957 B b1982 t1981
4958 T t1982 o960 b1964 b970 b1978
4959 B b1983 t1982
4960 T t1983 o2 b1983
4961 B b1984 t1983
4962 T t1984 o960 b1960 b4 b1984
4963 B b1985 t1984
4964 T t1985 o b1985 b4
4965 B b1986 t1985
4966 T t1986 o b1982 b1986
4967 B b1987 t1986
4968 T t1987 o b1979 b1987
4969 B b1988 t1987
4970 T t1988 o923 b1957 b1988
4971 B b1989 t1988
4972 P p1989 String "setSubstT << equal{op{inv{'a}; op{'a; 'b}}; op{op{inv{'a}; 'a}; 'b}} >> 0 thenWT autoT"
4973 O o1989 ext_rule p1989
4974 T t1989 o557 b1623 b1549
4975 B b1990 t1989
4976 T t1990 o737 b1974 b1990
4977 S s1990 t618 h
4978 G s1990 t1990
4979 B b1991 s1990
4980 T t1991 o925 b1991 b1936
4981 B b1992 t1991
4982 T t1992 o2 b1979
4983 B b1993 t1992
4984 T t1993 o953 b1992 b4 b1993
4985 B b1994 t1993
4986 T t1994 o557 b1925 b1990
4987 B b1995 t1994
4988 T t1995 o737 b565 b1995
4989 S s1995 t618 h
4990 G s1995 t1995
4991 B b1996 s1995
4992 T t1996 o925 b1996 b1936
4993 B b1997 t1996
4994 T t1997 o924 b1997 b4 b1993
4995 B b1998 t1997
4996 T t1998 o b1998 b4
4997 B b1999 t1998
4998 T t1999 o b1994 b1999
4999 B b2000 t1999
5000 T t2000 o923 b1979 b2000
5001 B b2001 t2000
5002 T t2001 o923 b1994 b4
5003 B b2002 t2001
5004 T t2002 o977 b922 b2002 b4 b4
5005 B b2003 t2002
5006 P p2003 String "setSubstT << equal{op{inv{'a}; 'a}; id} >> 0 thenWT autoT"
5007 O o2003 ext_rule p2003
5008 T t2003 o737 b1623 b565
5009 S s2003 t618 h
5010 G s2003 t2003
5011 B b2004 s2003
5012 T t2004 o925 b2004 b1936
5013 B b2005 t2004
5014 T t2005 o2 b1998
5015 B b2006 t2005
5016 T t2006 o953 b2005 b4 b2006
5017 B b2007 t2006
5018 T t2007 o557 b565 b1549
5019 B b2008 t2007
5020 T t2008 o557 b1925 b2008
5021 B b2009 t2008
5022 T t2009 o737 b565 b2009
5023 S s2009 t618 h
5024 G s2009 t2009
5025 B b2010 s2009
5026 T t2010 o925 b2010 b1936
5027 B b2011 t2010
5028 T t2011 o924 b2011 b4 b2006
5029 B b2012 t2011
5030 T t2012 o557 b1961 b1549
5031 B b2013 t2012
5032 T t2013 o557 b1925 b2013
5033 B b2014 t2013 v
5034 T t2014 o710 b2014
5035 S s2014 t618 h
5036 G s2014 t2014
5037 B b2015 s2014
5038 T t2015 o925 b2015 b1936
5039 B b2016 t2015
5040 B b2017 t2013
5041 T t2017 o737 b565 b2017
5042 B b2018 t2017 v
5043 T t2018 o963 b2018
5044 S s2018 t618 h
5045 G s2018 t2018
5046 B b2019 s2018
5047 T t2019 o925 b2019 b1936
5048 B b2020 t2019
5049 T t2020 o960 b2020 b970 b2006
5050 B b2021 t2020
5051 T t2021 o2 b2021
5052 B b2022 t2021
5053 T t2022 o960 b2016 b4 b2022
5054 B b2023 t2022
5055 T t2023 o b2023 b4
5056 B b2024 t2023
5057 T t2024 o b2012 b2024
5058 B b2025 t2024
5059 T t2025 o b2007 b2025
5060 B b2026 t2025
5061 T t2026 o923 b1998 b2026
5062 B b2027 t2026
5063 T t2027 o923 b2007 b4
5064 B b2028 t2027
5065 T t2028 o977 b922 b2028 b4 b4
5066 B b2029 t2028
5067 P p2029 String "setSubstT << equal{op{id; 'b}; 'b} >> 0 thenWT autoT"
5068 O o2029 ext_rule p2029
5069 T t2029 o737 b2008 b1549
5070 S s2029 t618 h
5071 G s2029 t2029
5072 B b2030 s2029
5073 T t2030 o925 b2030 b1936
5074 B b2031 t2030
5075 T t2031 o2 b2012
5076 B b2032 t2031
5077 T t2032 o953 b2031 b4 b2032
5078 B b2033 t2032
5079 T t2033 o557 b1925 b1549
5080 B b2034 t2033
5081 T t2034 o737 b565 b2034
5082 S s2034 t618 h
5083 G s2034 t2034
5084 B b2035 s2034
5085 T t2035 o925 b2035 b1936
5086 B b2036 t2035
5087 T t2036 o924 b2036 b4 b2032
5088 B b2037 t2036
5089 T t2037 o b2037 b4
5090 B b2038 t2037
5091 T t2038 o b2033 b2038
5092 B b2039 t2038
5093 T t2039 o923 b2012 b2039
5094 B b2040 t2039
5095 T t2040 o923 b2033 b4
5096 B b2041 t2040
5097 T t2041 o977 b922 b2041 b4 b4
5098 B b2042 t2041
5099 P p2042 String "setSubstT << equal{op{inv{'b}; 'b}; id} >> 0 thenT autoT"
5100 O o2042 ext_rule p2042
5101 T t2042 o923 b2037 b4
5102 B b2043 t2042
5103 T t2043 o2042 b922 b2043 b4 b4
5104 B b2044 t2043
5105 T t2044 o b2044 b4
5106 B b2045 t2044
5107 T t2045 o b2042 b2045
5108 B b2046 t2045
5109 T t2046 o2029 b922 b2040 b2046 b4
5110 B b2047 t2046
5111 P p2047 String "rwh unfold_fun_set 0 thenT dT 0"
5112 O o2047 ext_rule p2047
5113 NItt_equal Itt_equal Itt_equal NIL
5114 NItt_equal!type type type Itt_equal
5115 O o2048 type
5116 T t2048 o2048 b1238
5117 S s2048 t635 h
5118 G s2048 t2048
5119 B b2048 s2048
5120 T t2049 o925 b2048 b1936
5121 B b2049 t2049
5122 T t2050 o557 b558 b1549
5123 B b2050 t2050
5124 T t2051 o557 b1925 b2050
5125 B b2051 t2051
5126 T t2052 o557 b559 b1549
5127 B b2052 t2052
5128 T t2053 o557 b1925 b2052
5129 B b2053 t2053
5130 T t2054 o737 b2051 b2053
5131 B b2054 t2054
5132 T t2055 o1233 b1723 b2054
5133 B b2055 t2055 s2
5134 T t2056 o1237 b1238 b2055
5135 B b2056 t2056 s1
5136 T t2057 o1237 b1238 b2056
5137 S s2057 t618 h
5138 G s2057 t2057
5139 B b2057 s2057
5140 T t2058 o925 b2057 b1936
5141 B b2058 t2058
5142 T t2059 o2 b2023
5143 B b2059 t2059
5144 T t2060 o960 b2058 b4 b2059
5145 B b2060 t2060
5146 T t2061 o2 b2060
5147 B b2061 t2061
5148 T t2062 o960 b2049 b4 b2061
5149 B b2062 t2062
5150 S s2062 t618 h h1696
5151 G s2062 t2056
5152 B b2063 s2062
5153 T t2063 o925 b2063 b1936
5154 B b2064 t2063
5155 T t2064 o924 b2064 b4 b2061
5156 B b2065 t2064
5157 T t2065 o b2065 b4
5158 B b2066 t2065
5159 T t2066 o b2062 b2066
5160 B b2067 t2066
5161 T t2067 o923 b2023 b2067
5162 B b2068 t2067
5163 T t2068 o923 b2062 b4
5164 B b2069 t2068
5165 T t2069 o977 b922 b2069 b4 b4
5166 B b2070 t2069
5167 P p2070 String "dT 0"
5168 O o2070 ext_rule p2070
5169 S s2070 t635 h h1696
5170 G s2070 t2048
5171 B b2071 s2070
5172 T t2071 o925 b2071 b1936
5173 B b2072 t2071
5174 T t2072 o2 b2065
5175 B b2073 t2072
5176 T t2073 o960 b2072 b4 b2073
5177 B b2074 t2073
5178 S s2074 t618 h h1696 h1230
5179 G s2074 t2055
5180 B b2075 s2074
5181 T t2075 o925 b2075 b1936
5182 B b2076 t2075
5183 T t2076 o924 b2076 b4 b2073
5184 B b2077 t2076
5185 T t2077 o b2077 b4
5186 B b2078 t2077
5187 T t2078 o b2074 b2078
5188 B b2079 t2078
5189 T t2079 o923 b2065 b2079
5190 B b2080 t2079
5191 T t2080 o923 b2074 b4
5192 B b2081 t2080
5193 T t2081 o977 b922 b2081 b4 b4
5194 B b2082 t2081
5195 T t2082 o2048 b1723
5196 S s2082 t635 h h1696 h1230
5197 G s2082 t2082
5198 B b2083 s2082
5199 T t2083 o925 b2083 b1936
5200 B b2084 t2083
5201 T t2084 o2 b2077
5202 B b2085 t2084
5203 T t2085 o960 b2084 b4 b2085
5204 B b2086 t2085
5205 H h2086 x t1075
5206 S s2086 t618 h h1696 h1230 h2086
5207 G s2086 t2054
5208 B b2087 s2086
5209 T t2087 o925 b2087 b1936
5210 B b2088 t2087
5211 T t2088 o924 b2088 b4 b2085
5212 B b2089 t2088
5213 T t2089 o b2089 b4
5214 B b2090 t2089
5215 T t2090 o b2086 b2090
5216 B b2091 t2090
5217 T t2091 o923 b2077 b2091
5218 B b2092 t2091
5219 T t2092 o923 b2086 b4
5220 B b2093 t2092
5221 T t2093 o977 b922 b2093 b4 b4
5222 B b2094 t2093
5223 P p2094 String "rwh unfold_equal 0 thenT rwh unfold_equal 4 thenT autoT"
5224 O o2094 ext_rule p2094
5225 T t2094 o923 b2089 b4
5226 B b2095 t2094
5227 T t2095 o2094 b922 b2095 b4 b4
5228 B b2096 t2095
5229 T t2096 o b2096 b4
5230 B b2097 t2096
5231 T t2097 o b2094 b2097
5232 B b2098 t2097
5233 T t2098 o2070 b922 b2092 b2098 b4
5234 B b2099 t2098
5235 T t2099 o b2099 b4
5236 B b2100 t2099
5237 T t2100 o b2082 b2100
5238 B b2101 t2100
5239 T t2101 o2070 b922 b2080 b2101 b4
5240 B b2102 t2101
5241 T t2102 o b2102 b4
5242 B b2103 t2102
5243 T t2103 o b2070 b2103
5244 B b2104 t2103
5245 T t2104 o2047 b922 b2068 b2104 b4
5246 B b2105 t2104
5247 T t2105 o b2105 b4
5248 B b2106 t2105
5249 T t2106 o b2047 b2106
5250 B b2107 t2106
5251 T t2107 o b2029 b2107
5252 B b2108 t2107
5253 T t2108 o2003 b922 b2027 b2108 b4
5254 B b2109 t2108
5255 T t2109 o b2109 b4
5256 B b2110 t2109
5257 T t2110 o b2003 b2110
5258 B b2111 t2110
5259 T t2111 o1989 b922 b2001 b2111 b4
5260 B b2112 t2111
5261 T t2112 o923 b1982 b4
5262 B b2113 t2112
5263 T t2113 o977 b922 b2113 b4 b4
5264 B b2114 t2113
5265 T t2114 o923 b1985 b4
5266 B b2115 t2114
5267 T t2115 o1038 b922 b2115 b4 b4
5268 B b2116 t2115
5269 T t2116 o b2116 b4
5270 B b2117 t2116
5271 T t2117 o b2114 b2117
5272 B b2118 t2117
5273 T t2118 o b2112 b2118
5274 B b2119 t2118
5275 T t2119 o1973 b922 b1989 b2119 b4
5276 B b2120 t2119
5277 T t2120 o737 b1940 b1940
5278 S s2120 t618 h h1696 h1230 h2086
5279 G s2120 t2120
5280 B b2121 s2120
5281 T t2121 o925 b2121 b1936
5282 B b2122 t2121
5283 B b2123 t2120
5284 T t2123 o1233 b1723 b2123
5285 S s2123 t618 h h1696 h1230
5286 G s2123 t2123
5287 B b2124 s2123
5288 T t2124 o925 b2124 b1936
5289 B b2125 t2124
5290 B b2126 t2123 s2
5291 T t2126 o1237 b1238 b2126
5292 S s2126 t618 h h1696
5293 G s2126 t2126
5294 B b2127 s2126
5295 T t2127 o925 b2127 b1936
5296 B b2128 t2127
5297 B b2129 t2126 s1
5298 T t2129 o1237 b1238 b2129
5299 S s2129 t618 h
5300 G s2129 t2129
5301 B b2130 s2129
5302 T t2130 o925 b2130 b1936
5303 B b2131 t2130
5304 T t2131 o2 b1967
5305 B b2132 t2131
5306 T t2132 o960 b2131 b970 b2132
5307 B b2133 t2132
5308 T t2133 o2 b2133
5309 B b2134 t2133
5310 T t2134 o924 b2128 b970 b2134
5311 B b2135 t2134
5312 T t2135 o2 b2135
5313 B b2136 t2135
5314 T t2136 o924 b2125 b970 b2136
5315 B b2137 t2136
5316 T t2137 o2 b2137
5317 B b2138 t2137
5318 T t2138 o924 b2122 b4 b2138
5319 B b2139 t2138
5320 T t2139 o b2139 b4
5321 B b2140 t2139
5322 T t2140 o923 b1967 b2140
5323 B b2141 t2140
5324 P p2141 String "rwh unfold_equal 0 thenT autoT"
5325 O o2141 ext_rule p2141
5326 T t2141 o923 b2139 b4
5327 B b2142 t2141
5328 T t2142 o2141 b922 b2142 b4 b4
5329 B b2143 t2142
5330 T t2143 o b2143 b4
5331 B b2144 t2143
5332 T t2144 o1228 b922 b2141 b2144 b4
5333 B b2145 t2144
5334 T t2145 o b2145 b4
5335 B b2146 t2145
5336 T t2146 o b2120 b2146
5337 B b2147 t2146
5338 T t2147 o b1973 b2147
5339 B b2148 t2147
5340 T t2148 o1950 b922 b1971 b2148 b4
5341 B b2149 t2148
5342 P p2149 String "groupCancelRightT << op{'a; 'b} >> thenT autoT"
5343 O o2149 ext_rule p2149
5344 T t2149 o923 b1947 b4
5345 B b2150 t2149
5346 T t2150 o2149 b922 b2150 b4 b4
5347 B b2151 t2150
5348 T t2151 o b2151 b4
5349 B b2152 t2151
5350 T t2152 o b2149 b2152
5351 B b2153 t2152
5352 T t2153 o1932 b922 b1950 b2153 b4
5353 B b2154 t2153
5354 T t2154 o920 b2154
5355 B b2155 t2154
5356 P p2155 Number 7550
5357 P p2156 Number 7558
5358 O o2156 resource_defs p2155 p2156 p262
5359 P p2157 Number 7556
5360 O o2157 uid p2157 p2156
5361 T t2157 o2157 b624
5362 B b2157 t2157
5363 T t2158 o b2157 b4
5364 B b2158 t2158
5365 T t2159 o2156 b2158
5366 B b2159 t2159
5367 T t2160 o b2159 b4
5368 B b2160 t2160
5369 T t2161 o1923 b616 b1932 b2155 b2160
5370 B b2161 t2161
5371 T t2162 o1922 b2161
5372 B b2162 t2162
5373 O o2162 location p p
5374 NSummary!id id2162 id Summary
5375 P p2162 Number 646427455
5376 O o2163 id2162 p2162
5377 T t2163 o2163
5378 B b2163 t2163
5379 T t2164 o2162 b2163
5380 B b2164 t2164
5381 T t2165 o b2164 b4
5382 B b2165 t2165
5383 T t2166 o b2162 b2165
5384 B b2166 t2166
5385 T t2167 o b1921 b2166
5386 B b2167 t2167
5387 T t2168 o b1774 b2167
5388 B b2168 t2168
5389 T t2169 o b1543 b2168
5390 B b2169 t2169
5391 T t2170 o b1474 b2169
5392 B b2170 t2170
5393 T t2171 o b1354 b2170
5394 B b2171 t2171
5395 T t2172 o b1314 b2171
5396 B b2172 t2172
5397 T t2173 o b1273 b2172
5398 B b2173 t2173
5399 T t2174 o b1068 b2173
5400 B b2174 t2174
5401 T t2175 o b904 b2174
5402 B b2175 t2175
5403 T t2176 o b891 b2175
5404 B b2176 t2176
5405 T t2177 o b878 b2176
5406 B b2177 t2177
5407 T t2178 o b866 b2177
5408 B b2178 t2178
5409 T t2179 o b853 b2178
5410 B b2179 t2179
5411 T t2180 o b817 b2179
5412 B b2180 t2180
5413 T t2181 o b805 b2180
5414 B b2181 t2181
5415 T t2182 o b790 b2181
5416 B b2182 t2182
5417 T t2183 o b780 b2182
5418 B b2183 t2183
5419 T t2184 o b770 b2183
5420 B b2184 t2184
5421 T t2185 o b754 b2184
5422 B b2185 t2185
5423 T t2186 o b734 b2185
5424 B b2186 t2186
5425 T t2187 o b722 b2186
5426 B b2187 t2187
5427 T t2188 o b707 b2187
5428 B b2188 t2188
5429 T t2189 o b691 b2188
5430 B b2189 t2189
5431 T t2190 o b669 b2189
5432 B b2190 t2190
5433 T t2191 o b650 b2190
5434 B b2191 t2191
5435 T t2192 o b630 b2191
5436 B b2192 t2192
5437 T t2193 o b612 b2192
5438 B b2193 t2193
5439 T t2194 o b604 b2193
5440 B b2194 t2194
5441 T t2195 o b590 b2194
5442 B b2195 t2195
5443 T t2196 o b583 b2195
5444 B b2196 t2196
5445 T t2197 o b574 b2196
5446 B b2197 t2197
5447 T t2198 o b567 b2197
5448 B b2198 t2198
5449 T t2199 o b562 b2198
5450 B b2199 t2199
5451 T t2200 o b554 b2199
5452 B b2200 t2200
5453 T t2201 o b549 b2200
5454 B b2201 t2201
5455 T t2202 o b542 b2201
5456 B b2202 t2202
5457 T t2203 o b535 b2202
5458 B b2203 t2203
5459 T t2204 o b528 b2203
5460 B b2204 t2204
5461 T t2205 o b521 b2204
5462 B b2205 t2205
5463 T t2206 o b513 b2205
5464 B b2206 t2206
5465 T t2207 o b505 b2206
5466 B b2207 t2207
5467 T t2208 o b497 b2207
5468 B b2208 t2208
5469 T t2209 o b490 b2208
5470 B b2209 t2209
5471 T t2210 o b483 b2209
5472 B b2210 t2210
5473 T t2211 o b476 b2210
5474 B b2211 t2211
5475 T t2212 o b467 b2211
5476 B b2212 t2212
5477 T t2213 o b458 b2212
5478 B b2213 t2213
5479 T t2214 o b449 b2213
5480 B b2214 t2214
5481 T t2215 o b440 b2214
5482 B b2215 t2215
5483 T t2216 o b431 b2215
5484 B b2216 t2216
5485 T t2217 o b422 b2216
5486 B b2217 t2217
5487 T t2218 o b413 b2217
5488 B b2218 t2218
5489 T t2219 o b403 b2218
5490 B b2219 t2219
5491 T t2220 o b396 b2219
5492 B b2220 t2220
5493 T t2221 o b388 b2220
5494 B b2221 t2221
5495 T t2222 o b382 b2221
5496 B b2222 t2222
5497 T t2223 o b367 b2222
5498 B b2223 t2223
5499 T t2224 o b365 b2223
5500 B b2224 t2224
5501 T t2225 o b356 b2224

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26