/[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 3498 - (show annotations) (download)
Sun Feb 17 02:09:08 2002 UTC (19 years, 5 months ago) by xiny
File size: 94358 byte(s)
Changed the definition of groups completely.
The former version is awkward for defining specific groups like
<Z, +> and is lack of generality since only ONE general group is
defined.
The current version adopts a parameter which makes it capable of
handling complicated situations.

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 25
9 O o1 location p p1
10 NSummary!parent parent parent Summary
11 O o2 parent
12 P p2 String Itt_record_label0
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 Itt_nat
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_int_ext
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_int_base
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_bool
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_decidable
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_logic
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_union
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_prod
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_dprod
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_fun
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_dfun
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_rfun
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_void
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_set
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_unit
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_squiggle
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_subtype
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_squash
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_struct
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_equal
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_comment
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 Base_theory
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 Base_meta
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 Base_cache
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 Tactic_cache
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 Typeinf
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 Ocaml_df
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 Ocaml_str_df
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 Ocaml_sig_df
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 Ocaml_me_df
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 Ocaml_mt_df
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 Ocaml_type_df
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 Ocaml_patt_df
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 Ocaml_expr_df
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 Ocaml_base_df
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 Ocaml
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 Base_rewrite
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 Base_dtactic
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 Base_auto_tactic
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 Base_trivial
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 Top_conversionals
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 Top_tacticals
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 Var
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 Mptop
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 Summary
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 Comment
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 Base_dform
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 Nuprl_font
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 Perv
311 O o101 parent p101
312 T t102 o101
313 B b102 t102
314 T t103 o b102 b4
315 B b103 t103
316 T t104 o b103 b4
317 B b104 t104
318 T t105 o b101 b104
319 B b105 t105
320 T t106 o b99 b105
321 B b106 t106
322 T t107 o b97 b106
323 B b107 t107
324 T t108 o b95 b107
325 B b108 t108
326 T t109 o b93 b108
327 B b109 t109
328 T t110 o b91 b109
329 B b110 t110
330 T t111 o b89 b110
331 B b111 t111
332 T t112 o b87 b111
333 B b112 t112
334 T t113 o b85 b112
335 B b113 t113
336 T t114 o b83 b113
337 B b114 t114
338 T t115 o b81 b114
339 B b115 t115
340 T t116 o b79 b115
341 B b116 t116
342 T t117 o b77 b116
343 B b117 t117
344 T t118 o b75 b117
345 B b118 t118
346 T t119 o b73 b118
347 B b119 t119
348 T t120 o b71 b119
349 B b120 t120
350 T t121 o b69 b120
351 B b121 t121
352 T t122 o b67 b121
353 B b122 t122
354 T t123 o b65 b122
355 B b123 t123
356 T t124 o b63 b123
357 B b124 t124
358 T t125 o b61 b124
359 B b125 t125
360 T t126 o b59 b125
361 B b126 t126
362 T t127 o b57 b126
363 B b127 t127
364 T t128 o b55 b127
365 B b128 t128
366 T t129 o b53 b128
367 B b129 t129
368 T t130 o b51 b129
369 B b130 t130
370 T t131 o b49 b130
371 B b131 t131
372 T t132 o b47 b131
373 B b132 t132
374 T t133 o b45 b132
375 B b133 t133
376 T t134 o b43 b133
377 B b134 t134
378 T t135 o b41 b134
379 B b135 t135
380 T t136 o b39 b135
381 B b136 t136
382 T t137 o b37 b136
383 B b137 t137
384 T t138 o b35 b137
385 B b138 t138
386 T t139 o b33 b138
387 B b139 t139
388 T t140 o b31 b139
389 B b140 t140
390 T t141 o b29 b140
391 B b141 t141
392 T t142 o b27 b141
393 B b142 t142
394 T t143 o b25 b142
395 B b143 t143
396 T t144 o b23 b143
397 B b144 t144
398 T t145 o b21 b144
399 B b145 t145
400 T t146 o b19 b145
401 B b146 t146
402 T t147 o b17 b146
403 B b147 t147
404 T t148 o b15 b147
405 B b148 t148
406 T t149 o b13 b148
407 B b149 t149
408 T t150 o b11 b149
409 B b150 t150
410 T t151 o b9 b150
411 B b151 t151
412 T t152 o b7 b151
413 B b152 t152
414 T t153 o b5 b152
415 B b153 t153
416 NSummary!resource resource resource Summary
417 P p153 String auto
418 O o153 resource p153
419 NOcaml Ocaml Ocaml NIL
420 NOcaml!type_lid type_lid type_lid Ocaml
421 P p154 Number 2332
422 P p155 Number 2341
423 O o155 type_lid p154 p155
424 P p156 String auto_info
425 O o156 type_lid p156
426 T t156 o156
427 B b156 t156
428 T t157 o155 b156
429 B b157 t157
430 NOcaml!type_prod type_prod type_prod Ocaml
431 P p157 Number 2343
432 P p158 Number 2367
433 O o158 type_prod p157 p158
434 P p159 Number 2349
435 O o159 type_lid p157 p159
436 P p160 String tactic
437 O o160 type_lid p160
438 T t160 o160
439 B b160 t160
440 T t161 o159 b160
441 B b161 t161
442 P p161 Number 2352
443 P p162 Number 2358
444 O o162 type_lid p161 p162
445 T t162 o162 b160
446 B b162 t162
447 P p163 Number 2361
448 O o163 type_lid p163 p158
449 T t163 o163 b160
450 B b163 t163
451 T t164 o b163 b4
452 B b164 t164
453 T t165 o b162 b164
454 B b165 t165
455 T t166 o b161 b165
456 B b166 t166
457 T t167 o158 b166
458 B b167 t167
459 T t168 o153 b157 b167
460 B b168 t168
461 P p168 String cache
462 O o168 resource p168
463 P p169 Number 1424
464 P p170 Number 1434
465 O o170 type_lid p169 p170
466 P p171 String cache_rule
467 O o171 type_lid p171
468 T t171 o171
469 B b171 t171
470 T t172 o170 b171
471 B b172 t172
472 P p172 Number 1436
473 P p173 Number 1441
474 O o173 type_lid p172 p173
475 O o174 type_lid p168
476 T t174 o174
477 B b174 t174
478 T t175 o173 b174
479 B b175 t175
480 T t176 o168 b172 b175
481 B b176 t176
482 P p176 String elim
483 O o176 resource p176
484 P p177 Number 1761
485 P p178 Number 1783
486 O o178 type_prod p177 p178
487 P p179 Number 1765
488 O o179 type_lid p177 p179
489 P p180 String term
490 O o180 type_lid p180
491 T t180 o180
492 B b180 t180
493 T t181 o179 b180
494 B b181 t181
495 NOcaml!type_fun type_fun type_fun Ocaml
496 P p181 Number 1769
497 P p182 Number 1782
498 O o182 type_fun p181 p182
499 P p183 Number 1772
500 O o183 type_lid p181 p183
501 P p184 String int
502 O o184 type_lid p184
503 T t184 o184
504 B b184 t184
505 T t185 o183 b184
506 B b185 t185
507 P p185 Number 1776
508 O o185 type_lid p185 p182
509 T t186 o185 b160
510 B b186 t186
511 T t187 o182 b185 b186
512 B b187 t187
513 T t188 o b187 b4
514 B b188 t188
515 T t189 o b181 b188
516 B b189 t189
517 T t190 o178 b189
518 B b190 t190
519 P p190 Number 1785
520 P p191 Number 1798
521 O o191 type_fun p190 p191
522 P p192 Number 1788
523 O o192 type_lid p190 p192
524 T t192 o192 b184
525 B b192 t192
526 P p193 Number 1792
527 O o193 type_lid p193 p191
528 T t193 o193 b160
529 B b193 t193
530 T t194 o191 b192 b193
531 B b194 t194
532 T t195 o176 b190 b194
533 B b195 t195
534 P p195 String eqcd
535 O o195 resource p195
536 P p196 Number 6168
537 P p197 Number 6181
538 O o197 type_prod p196 p197
539 P p198 Number 6172
540 O o198 type_lid p196 p198
541 T t198 o198 b180
542 B b198 t198
543 P p199 Number 6175
544 O o199 type_lid p199 p197
545 T t199 o199 b160
546 B b199 t199
547 T t200 o b199 b4
548 B b200 t200
549 T t201 o b198 b200
550 B b201 t201
551 T t202 o197 b201
552 B b202 t202
553 P p202 Number 6183
554 P p203 Number 6189
555 O o203 type_lid p202 p203
556 T t203 o203 b160
557 B b203 t203
558 T t204 o195 b202 b203
559 B b204 t204
560 P p204 String intro
561 O o204 resource p204
562 P p205 Number 1815
563 P p206 Number 1852
564 O o206 type_prod p205 p206
565 P p207 Number 1819
566 O o207 type_lid p205 p207
567 T t207 o207 b180
568 B b207 t207
569 P p208 Number 1823
570 P p209 Number 1851
571 O o209 type_prod p208 p209
572 P p210 Number 1829
573 O o210 type_lid p208 p210
574 P p211 String string
575 O o211 type_lid p211
576 T t211 o211
577 B b211 t211
578 T t212 o210 b211
579 B b212 t212
580 NOcaml!type_apply type_apply type_apply Ocaml
581 P p212 Number 1832
582 P p213 Number 1842
583 O o213 type_apply p212 p213
584 P p214 Number 1836
585 O o214 type_lid p214 p213
586 P p215 String option
587 O o215 type_lid p215
588 T t215 o215
589 B b215 t215
590 T t216 o214 b215
591 B b216 t216
592 P p216 Number 1835
593 O o216 type_lid p212 p216
594 T t217 o216 b184
595 B b217 t217
596 T t218 o213 b216 b217
597 B b218 t218
598 P p218 Number 1845
599 O o218 type_lid p218 p209
600 T t219 o218 b160
601 B b219 t219
602 T t220 o b219 b4
603 B b220 t220
604 T t221 o b218 b220
605 B b221 t221
606 T t222 o b212 b221
607 B b222 t222
608 T t223 o209 b222
609 B b223 t223
610 T t224 o b223 b4
611 B b224 t224
612 T t225 o b207 b224
613 B b225 t225
614 T t226 o206 b225
615 B b226 t226
616 P p226 Number 1854
617 P p227 Number 1860
618 O o227 type_lid p226 p227
619 T t227 o227 b160
620 B b227 t227
621 T t228 o204 b226 b227
622 B b228 t228
623 P p228 String reduce
624 O o228 resource p228
625 P p229 Number 2920
626 P p230 Number 2931
627 O o230 type_prod p229 p230
628 P p231 Number 2924
629 O o231 type_lid p229 p231
630 T t231 o231 b180
631 B b231 t231
632 P p232 Number 2927
633 O o232 type_lid p232 p230
634 P p233 String conv
635 O o233 type_lid p233
636 T t233 o233
637 B b233 t233
638 T t234 o232 b233
639 B b234 t234
640 T t235 o b234 b4
641 B b235 t235
642 T t236 o b231 b235
643 B b236 t236
644 T t237 o230 b236
645 B b237 t237
646 P p237 Number 2933
647 P p238 Number 2937
648 O o238 type_lid p237 p238
649 T t238 o238 b233
650 B b238 t238
651 T t239 o228 b237 b238
652 B b239 t239
653 P p239 String squash
654 O o239 resource p239
655 P p240 Number 4017
656 P p241 Number 4028
657 O o241 type_lid p240 p241
658 P p242 String squash_info
659 O o242 type_lid p242
660 T t242 o242
661 B b242 t242
662 T t243 o241 b242
663 B b243 t243
664 P p243 Number 4030
665 P p244 Number 4043
666 O o244 type_fun p243 p244
667 P p245 Number 4033
668 O o245 type_lid p243 p245
669 T t245 o245 b184
670 B b245 t245
671 P p246 Number 4037
672 O o246 type_lid p246 p244
673 T t246 o246 b160
674 B b246 t246
675 T t247 o244 b245 b246
676 B b247 t247
677 T t248 o239 b243 b247
678 B b248 t248
679 P p248 String sub
680 O o248 resource p248
681 P p249 Number 4882
682 P p250 Number 4899
683 O o250 type_lid p249 p250
684 P p251 String sub_resource_info
685 O o251 type_lid p251
686 T t251 o251
687 B b251 t251
688 T t252 o250 b251
689 B b252 t252
690 P p252 Number 4901
691 P p253 Number 4907
692 O o253 type_lid p252 p253
693 T t253 o253 b160
694 B b253 t253
695 T t254 o248 b252 b253
696 B b254 t254
697 P p254 String toploop
698 O o254 resource p254
699 P p255 Number 2445
700 P p256 Number 2467
701 O o256 type_prod p255 p256
702 P p257 Number 2451
703 O o257 type_lid p255 p257
704 T t257 o257 b211
705 B b257 t257
706 P p258 Number 2454
707 P p259 Number 2460
708 O o259 type_lid p258 p259
709 T t259 o259 b211
710 B b259 t259
711 P p260 Number 2463
712 O o260 type_lid p260 p256
713 P p261 String expr
714 O o261 type_lid p261
715 T t261 o261
716 B b261 t261
717 T t262 o260 b261
718 B b262 t262
719 T t263 o b262 b4
720 B b263 t263
721 T t264 o b259 b263
722 B b264 t264
723 T t265 o b257 b264
724 B b265 t265
725 T t266 o256 b265
726 B b266 t266
727 P p266 Number 2469
728 P p267 Number 2478
729 O o267 type_lid p266 p267
730 P p268 String top_table
731 O o268 type_lid p268
732 T t268 o268
733 B b268 t268
734 T t269 o267 b268
735 B b269 t269
736 T t270 o254 b266 b269
737 B b270 t270
738 P p270 String typeinf
739 O o270 resource p270
740 P p271 Number 2151
741 P p272 Number 2172
742 O o272 type_lid p271 p272
743 P p273 String typeinf_resource_info
744 O o273 type_lid p273
745 T t273 o273
746 B b273 t273
747 T t274 o272 b273
748 B b274 t274
749 P p274 Number 2174
750 P p275 Number 2186
751 O o275 type_lid p274 p275
752 P p276 String typeinf_func
753 O o276 type_lid p276
754 T t276 o276
755 B b276 t276
756 T t277 o275 b276
757 B b277 t277
758 T t278 o270 b274 b277
759 B b278 t278
760 P p278 String typeinf_subst
761 O o278 resource p278
762 P p279 Number 1825
763 P p280 Number 1843
764 O o280 type_lid p279 p280
765 P p281 String typeinf_subst_info
766 O o281 type_lid p281
767 T t281 o281
768 B b281 t281
769 T t282 o280 b281
770 B b282 t282
771 P p282 Number 1862
772 O o282 type_lid p218 p282
773 P p283 String typeinf_subst_fun
774 O o283 type_lid p283
775 T t283 o283
776 B b283 t283
777 T t284 o282 b283
778 B b284 t284
779 T t285 o278 b282 b284
780 B b285 t285
781 T t286 o b285 b4
782 B b286 t286
783 T t287 o b278 b286
784 B b287 t287
785 T t288 o b270 b287
786 B b288 t288
787 T t289 o b254 b288
788 B b289 t289
789 T t290 o b248 b289
790 B b290 t290
791 T t291 o b239 b290
792 B b291 t291
793 T t292 o b228 b291
794 B b292 t292
795 T t293 o b204 b292
796 B b293 t293
797 T t294 o b195 b293
798 B b294 t294
799 T t295 o b176 b294
800 B b295 t295
801 T t296 o b168 b295
802 B b296 t296
803 T t297 o2 b5 b153 b296
804 B b297 t297
805 T t298 o1 b297
806 B b298 t298
807 P p298 Number 26
808 P p299 Number 45
809 O o299 location p298 p299
810 P p300 String Czf_itt_set
811 O o300 parent p300
812 T t300 o300
813 B b300 t300
814 T t301 o b300 b4
815 B b301 t301
816 P p301 String Czf_itt_comment
817 O o301 parent p301
818 T t302 o301
819 B b302 t302
820 T t303 o b302 b4
821 B b303 t303
822 P p303 String Itt_theory
823 O o303 parent p303
824 T t304 o303
825 B b304 t304
826 T t305 o b304 b4
827 B b305 t305
828 P p305 String Itt_fset
829 O o305 parent p305
830 T t306 o305
831 B b306 t306
832 T t307 o b306 b4
833 B b307 t307
834 P p307 String Itt_prop_decide
835 O o307 parent p307
836 T t308 o307
837 B b308 t308
838 T t309 o b308 b4
839 B b309 t309
840 P p309 String Itt_derive
841 O o309 parent p309
842 T t310 o309
843 B b310 t310
844 T t311 o b310 b4
845 B b311 t311
846 P p311 String Itt_list2
847 O o311 parent p311
848 T t312 o311
849 B b312 t312
850 T t313 o b312 b4
851 B b313 t313
852 P p313 String Itt_list
853 O o313 parent p313
854 T t314 o313
855 B b314 t314
856 T t315 o b314 b4
857 B b315 t315
858 P p315 String Itt_quotient
859 O o315 parent p315
860 T t316 o315
861 B b316 t316
862 T t317 o b316 b4
863 B b317 t317
864 P p317 String Itt_esquash
865 O o317 parent p317
866 T t318 o317
867 B b318 t318
868 T t319 o b318 b4
869 B b319 t319
870 P p319 String Itt_srec
871 O o319 parent p319
872 T t320 o319
873 B b320 t320
874 T t321 o b320 b4
875 B b321 t321
876 P p321 String Itt_prec
877 O o321 parent p321
878 T t322 o321
879 B b322 t322
880 T t323 o b322 b4
881 B b323 t323
882 P p323 String Itt_w
883 O o323 parent p323
884 T t324 o323
885 B b324 t324
886 T t325 o b324 b4
887 B b325 t325
888 P p325 String Itt_bunion
889 O o325 parent p325
890 T t326 o325
891 B b326 t326
892 T t327 o b326 b4
893 B b327 t327
894 P p327 String Itt_bisect
895 O o327 parent p327
896 T t328 o327
897 B b328 t328
898 T t329 o b328 b4
899 B b329 t329
900 P p329 String Itt_tunion
901 O o329 parent p329
902 T t330 o329
903 B b330 t330
904 T t331 o b330 b4
905 B b331 t331
906 P p331 String Itt_isect
907 O o331 parent p331
908 T t332 o331
909 B b332 t332
910 T t333 o b332 b4
911 B b333 t333
912 P p333 String Itt_struct2
913 O o333 parent p333
914 T t334 o333
915 B b334 t334
916 T t335 o b334 b4
917 B b335 t335
918 P p335 String Itt_well_founded
919 O o335 parent p335
920 T t336 o335
921 B b336 t336
922 T t337 o b336 b4
923 B b337 t337
924 P p337 String Itt_int_arith
925 O o337 parent p337
926 T t338 o337
927 B b338 t338
928 T t339 o b338 b4
929 B b339 t339
930 P p339 String Itt_atom_bool
931 O o339 parent p339
932 T t340 o339
933 B b340 t340
934 T t341 o b340 b4
935 B b341 t341
936 P p341 String Itt_atom
937 O o341 parent p341
938 T t342 o341
939 B b342 t342
940 T t343 o b342 b4
941 B b343 t343
942 T t344 o b343 b4
943 B b344 t344
944 T t345 o b341 b344
945 B b345 t345
946 T t346 o b339 b345
947 B b346 t346
948 T t347 o b337 b346
949 B b347 t347
950 T t348 o b335 b347
951 B b348 t348
952 T t349 o b333 b348
953 B b349 t349
954 T t350 o b331 b349
955 B b350 t350
956 T t351 o b329 b350
957 B b351 t351
958 T t352 o b327 b351
959 B b352 t352
960 T t353 o b325 b352
961 B b353 t353
962 T t354 o b323 b353
963 B b354 t354
964 T t355 o b321 b354
965 B b355 t355
966 T t356 o b319 b355
967 B b356 t356
968 T t357 o b317 b356
969 B b357 t357
970 T t358 o b315 b357
971 B b358 t358
972 T t359 o b313 b358
973 B b359 t359
974 T t360 o b311 b359
975 B b360 t360
976 T t361 o b309 b360
977 B b361 t361
978 T t362 o b307 b361
979 B b362 t362
980 T t363 o b305 b362
981 B b363 t363
982 T t364 o b303 b363
983 B b364 t364
984 T t365 o b301 b364
985 B b365 t365
986 T t366 o2 b301 b365 b296
987 B b366 t366
988 T t367 o299 b366
989 B b367 t367
990 P p367 Number 46
991 P p368 Number 68
992 O o368 location p367 p368
993 P p369 String Czf_itt_member
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_eq
1000 O o370 parent p370
1001 T t371 o370
1002 B b371 t371
1003 T t372 o b371 b4
1004 B b372 t372
1005 T t373 o b372 b4
1006 B b373 t373
1007 T t374 o b370 b373
1008 B b374 t374
1009 T t375 o2 b370 b374 b296
1010 B b375 t375
1011 T t376 o368 b375
1012 B b376 t376
1013 P p376 Number 69
1014 P p377 Number 87
1015 O o377 location p376 p377
1016 T t377 o2 b372 b4 b296
1017 B b377 t377
1018 T t378 o377 b377
1019 B b378 t378
1020 P p378 Number 88
1021 P p379 Number 108
1022 O o379 location p378 p379
1023 P p380 String Czf_itt_dall
1024 O o380 parent p380
1025 T t380 o380
1026 B b380 t380
1027 T t381 o b380 b4
1028 B b381 t381
1029 P p381 String Czf_itt_set_ind
1030 O o381 parent p381
1031 T t382 o381
1032 B b382 t382
1033 T t383 o b382 b4
1034 B b383 t383
1035 P p383 String Czf_itt_all
1036 O o383 parent p383
1037 T t384 o383
1038 B b384 t384
1039 T t385 o b384 b4
1040 B b385 t385
1041 P p385 String Czf_itt_sep
1042 O o385 parent p385
1043 T t386 o385
1044 B b386 t386
1045 T t387 o b386 b4
1046 B b387 t387
1047 T t388 o b387 b4
1048 B b388 t388
1049 T t389 o b385 b388
1050 B b389 t389
1051 T t390 o b383 b389
1052 B b390 t390
1053 T t391 o b381 b390
1054 B b391 t391
1055 T t392 o2 b381 b391 b296
1056 B b392 t392
1057 T t393 o379 b392
1058 B b393 t393
1059 P p393 Number 109
1060 P p394 Number 128
1061 O o394 location p393 p394
1062 P p395 String Czf_itt_and
1063 O o395 parent p395
1064 T t395 o395
1065 B b395 t395
1066 T t396 o b395 b4
1067 B b396 t396
1068 T t397 o b396 b4
1069 B b397 t397
1070 T t398 o2 b396 b397 b296
1071 B b398 t398
1072 T t399 o394 b398
1073 B b399 t399
1074 P p399 Number 130
1075 P p400 Number 141
1076 O o400 location p399 p400
1077 NSummary!summary_item summary_item summary_item Summary
1078 O o401 summary_item
1079 NOcaml!str_open str_open str_open Ocaml
1080 O o402 str_open p399 p400
1081 NOcaml!string string string Ocaml
1082 P p402 String Printf
1083 O o403 string p402
1084 T t403 o403
1085 B b403 t403
1086 T t404 o b403 b4
1087 B b404 t404
1088 T t405 o402 b404
1089 B b405 t405
1090 T t406 o401 b405
1091 B b406 t406
1092 T t407 o400 b406
1093 B b407 t407
1094 P p407 Number 142
1095 P p408 Number 155
1096 O o408 location p407 p408
1097 O o409 str_open p407 p408
1098 P p409 String Mp_debug
1099 O o410 string p409
1100 T t410 o410
1101 B b410 t410
1102 T t411 o b410 b4
1103 B b411 t411
1104 T t412 o409 b411
1105 B b412 t412
1106 T t413 o401 b412
1107 B b413 t413
1108 T t414 o408 b413
1109 B b414 t414
1110 P p414 Number 156
1111 P p415 Number 185
1112 O o415 location p414 p415
1113 O o416 str_open p414 p415
1114 P p416 String Refiner
1115 O o417 string p416
1116 T t417 o417
1117 B b417 t417
1118 P p417 String TermType
1119 O o418 string p417
1120 T t418 o418
1121 B b418 t418
1122 T t419 o b418 b4
1123 B b419 t419
1124 T t420 o b417 b419
1125 B b420 t420
1126 T t421 o b417 b420
1127 B b421 t421
1128 T t422 o416 b421
1129 B b422 t422
1130 T t423 o401 b422
1131 B b423 t423
1132 T t424 o415 b423
1133 B b424 t424
1134 P p424 Number 186
1135 P p425 Number 211
1136 O o425 location p424 p425
1137 O o426 str_open p424 p425
1138 P p426 String Term
1139 O o427 string p426
1140 T t427 o427
1141 B b427 t427
1142 T t428 o b427 b4
1143 B b428 t428
1144 T t429 o b417 b428
1145 B b429 t429
1146 T t430 o b417 b429
1147 B b430 t430
1148 T t431 o426 b430
1149 B b431 t431
1150 T t432 o401 b431
1151 B b432 t432
1152 T t433 o425 b432
1153 B b433 t433
1154 P p433 Number 212
1155 P p434 Number 239
1156 O o434 location p433 p434
1157 O o435 str_open p433 p434
1158 P p435 String TermOp
1159 O o436 string p435
1160 T t436 o436
1161 B b436 t436
1162 T t437 o b436 b4
1163 B b437 t437
1164 T t438 o b417 b437
1165 B b438 t438
1166 T t439 o b417 b438
1167 B b439 t439
1168 T t440 o435 b439
1169 B b440 t440
1170 T t441 o401 b440
1171 B b441 t441
1172 T t442 o434 b441
1173 B b442 t442
1174 P p442 Number 240
1175 P p443 Number 269
1176 O o443 location p442 p443
1177 O o444 str_open p442 p443
1178 P p444 String TermAddr
1179 O o445 string p444
1180 T t445 o445
1181 B b445 t445
1182 T t446 o b445 b4
1183 B b446 t446
1184 T t447 o b417 b446
1185 B b447 t447
1186 T t448 o b417 b447
1187 B b448 t448
1188 T t449 o444 b448
1189 B b449 t449
1190 T t450 o401 b449
1191 B b450 t450
1192 T t451 o443 b450
1193 B b451 t451
1194 P p451 Number 270
1195 P p452 Number 298
1196 O o452 location p451 p452
1197 O o453 str_open p451 p452
1198 P p453 String TermMan
1199 O o454 string p453
1200 T t454 o454
1201 B b454 t454
1202 T t455 o b454 b4
1203 B b455 t455
1204 T t456 o b417 b455
1205 B b456 t456
1206 T t457 o b417 b456
1207 B b457 t457
1208 T t458 o453 b457
1209 B b458 t458
1210 T t459 o401 b458
1211 B b459 t459
1212 T t460 o452 b459
1213 B b460 t460
1214 P p460 Number 299
1215 P p461 Number 329
1216 O o461 location p460 p461
1217 O o462 str_open p460 p461
1218 P p462 String TermSubst
1219 O o463 string p462
1220 T t463 o463
1221 B b463 t463
1222 T t464 o b463 b4
1223 B b464 t464
1224 T t465 o b417 b464
1225 B b465 t465
1226 T t466 o b417 b465
1227 B b466 t466
1228 T t467 o462 b466
1229 B b467 t467
1230 T t468 o401 b467
1231 B b468 t468
1232 T t469 o461 b468
1233 B b469 t469
1234 P p469 Number 330
1235 P p470 Number 357
1236 O o470 location p469 p470
1237 O o471 str_open p469 p470
1238 P p471 String Refine
1239 O o472 string p471
1240 T t472 o472
1241 B b472 t472
1242 T t473 o b472 b4
1243 B b473 t473
1244 T t474 o b417 b473
1245 B b474 t474
1246 T t475 o b417 b474
1247 B b475 t475
1248 T t476 o471 b475
1249 B b476 t476
1250 T t477 o401 b476
1251 B b477 t477
1252 T t478 o470 b477
1253 B b478 t478
1254 P p478 Number 358
1255 P p479 Number 390
1256 O o479 location p478 p479
1257 O o480 str_open p478 p479
1258 P p480 String RefineError
1259 O o481 string p480
1260 T t481 o481
1261 B b481 t481
1262 T t482 o b481 b4
1263 B b482 t482
1264 T t483 o b417 b482
1265 B b483 t483
1266 T t484 o b417 b483
1267 B b484 t484
1268 T t485 o480 b484
1269 B b485 t485
1270 T t486 o401 b485
1271 B b486 t486
1272 T t487 o479 b486
1273 B b487 t487
1274 P p487 Number 391
1275 P p488 Number 407
1276 O o488 location p487 p488
1277 O o489 str_open p487 p488
1278 P p489 String Mp_resource
1279 O o490 string p489
1280 T t490 o490
1281 B b490 t490
1282 T t491 o b490 b4
1283 B b491 t491
1284 T t492 o489 b491
1285 B b492 t492
1286 T t493 o401 b492
1287 B b493 t493
1288 T t494 o488 b493
1289 B b494 t494
1290 P p494 Number 408
1291 P p495 Number 425
1292 O o495 location p494 p495
1293 O o496 str_open p494 p495
1294 P p496 String Simple_print
1295 O o497 string p496
1296 T t497 o497
1297 B b497 t497
1298 T t498 o b497 b4
1299 B b498 t498
1300 T t499 o496 b498
1301 B b499 t499
1302 T t500 o401 b499
1303 B b500 t500
1304 T t501 o495 b500
1305 B b501 t501
1306 P p501 Number 427
1307 P p502 Number 443
1308 O o502 location p501 p502
1309 O o503 str_open p501 p502
1310 P p503 String Tactic_type
1311 O o504 string p503
1312 T t504 o504
1313 B b504 t504
1314 T t505 o b504 b4
1315 B b505 t505
1316 T t506 o503 b505
1317 B b506 t506
1318 T t507 o401 b506
1319 B b507 t507
1320 T t508 o502 b507
1321 B b508 t508
1322 P p508 Number 444
1323 P p509 Number 470
1324 O o509 location p508 p509
1325 O o510 str_open p508 p509
1326 P p510 String Tacticals
1327 O o511 string p510
1328 T t511 o511
1329 B b511 t511
1330 T t512 o b511 b4
1331 B b512 t512
1332 T t513 o b504 b512
1333 B b513 t513
1334 T t514 o510 b513
1335 B b514 t514
1336 T t515 o401 b514
1337 B b515 t515
1338 T t516 o509 b515
1339 B b516 t516
1340 P p516 Number 471
1341 P p517 Number 495
1342 O o517 location p516 p517
1343 O o518 str_open p516 p517
1344 P p518 String Sequent
1345 O o519 string p518
1346 T t519 o519
1347 B b519 t519
1348 T t520 o b519 b4
1349 B b520 t520
1350 T t521 o b504 b520
1351 B b521 t521
1352 T t522 o518 b521
1353 B b522 t522
1354 T t523 o401 b522
1355 B b523 t523
1356 T t524 o517 b523
1357 B b524 t524
1358 P p524 Number 496
1359 P p525 Number 526
1360 O o525 location p524 p525
1361 O o526 str_open p524 p525
1362 P p526 String Conversionals
1363 O o527 string p526
1364 T t527 o527
1365 B b527 t527
1366 T t528 o b527 b4
1367 B b528 t528
1368 T t529 o b504 b528
1369 B b529 t529
1370 T t530 o526 b529
1371 B b530 t530
1372 T t531 o401 b530
1373 B b531 t531
1374 T t532 o525 b531
1375 B b532 t532
1376 P p532 Number 527
1377 P p533 Number 537
1378 O o533 location p532 p533
1379 O o534 str_open p532 p533
1380 O o535 string p91
1381 T t535 o535
1382 B b535 t535
1383 T t536 o b535 b4
1384 B b536 t536
1385 T t537 o534 b536
1386 B b537 t537
1387 T t538 o401 b537
1388 B b538 t538
1389 T t539 o533 b538
1390 B b539 t539
1391 P p539 Number 538
1392 P p540 Number 546
1393 O o540 location p539 p540
1394 O o541 str_open p539 p540
1395 O o542 string p89
1396 T t542 o542
1397 B b542 t542
1398 T t543 o b542 b4
1399 B b543 t543
1400 T t544 o541 b543
1401 B b544 t544
1402 T t545 o401 b544
1403 B b545 t545
1404 T t546 o540 b545
1405 B b546 t546
1406 P p546 Number 548
1407 P p547 Number 565
1408 O o547 location p546 p547
1409 O o548 str_open p546 p547
1410 O o549 string p79
1411 T t549 o549
1412 B b549 t549
1413 T t550 o b549 b4
1414 B b550 t550
1415 T t551 o548 b550
1416 B b551 t551
1417 T t552 o401 b551
1418 B b552 t552
1419 T t553 o547 b552
1420 B b553 t553
1421 P p553 Number 566
1422 P p554 Number 587
1423 O o554 location p553 p554
1424 O o555 str_open p553 p554
1425 O o556 string p81
1426 T t556 o556
1427 B b556 t556
1428 T t557 o b556 b4
1429 B b557 t557
1430 T t558 o555 b557
1431 B b558 t558
1432 T t559 o401 b558
1433 B b559 t559
1434 T t560 o554 b559
1435 B b560 t560
1436 P p560 Number 589
1437 P p561 Number 606
1438 O o561 location p560 p561
1439 NSummary!opname opname opname Summary
1440 P p562 String group
1441 O o562 opname p562
1442 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1443 NCzf_itt_group!group group group Czf_itt_group
1444 O o563 group
1445 Nvar var var NIL
1446 P p563 Var g
1447 O o564 var p563
1448 T t564 o564
1449 B b564 t564
1450 T t565 o563 b564
1451 B b565 t565
1452 T t566 o562 b565
1453 B b566 t566
1454 T t567 o561 b566
1455 B b567 t567
1456 P p567 Number 607
1457 P p568 Number 622
1458 O o568 location p567 p568
1459 P p569 String car
1460 O o569 opname p569
1461 NCzf_itt_group!car car car Czf_itt_group
1462 O o570 car
1463 T t570 o570 b564
1464 B b570 t570
1465 T t571 o569 b570
1466 B b571 t571
1467 T t572 o568 b571
1468 B b572 t572
1469 P p572 Number 663
1470 P p573 Number 687
1471 O o573 location p572 p573
1472 P p574 String op
1473 O o574 opname p574
1474 NCzf_itt_group!op op op Czf_itt_group
1475 O o575 op
1476 P p575 Var s1
1477 O o576 var p575
1478 T t576 o576
1479 B b576 t576
1480 P p576 Var s2
1481 O o577 var p576
1482 T t577 o577
1483 B b577 t577
1484 T t578 o575 b564 b576 b577
1485 B b578 t578
1486 T t579 o574 b578
1487 B b579 t579
1488 T t580 o573 b579
1489 B b580 t580
1490 P p580 Number 688
1491 P p581 Number 702
1492 O o581 location p580 p581
1493 P p582 String id
1494 O o582 opname p582
1495 NCzf_itt_group!id id id Czf_itt_group
1496 O o583 id
1497 T t583 o583 b564
1498 B b583 t583
1499 T t584 o582 b583
1500 B b584 t584
1501 T t585 o581 b584
1502 B b585 t585
1503 P p585 Number 703
1504 P p586 Number 722
1505 O o586 location p585 p586
1506 P p587 String inv
1507 O o587 opname p587
1508 NCzf_itt_group!inv inv inv Czf_itt_group
1509 O o588 inv
1510 P p588 Var s
1511 O o589 var p588
1512 T t589 o589
1513 B b589 t589
1514 T t590 o588 b564 b589
1515 B b590 t590
1516 T t591 o587 b590
1517 B b591 t591
1518 T t592 o586 b591
1519 B b592 t592
1520 P p592 Number 723
1521 P p593 Number 751
1522 O o593 location p592 p593
1523 P p594 String eqElem
1524 O o594 opname p594
1525 NCzf_itt_group!eqElem eqElem eqElem Czf_itt_group
1526 O o595 eqElem
1527 T t595 o595 b564 b576 b577
1528 B b595 t595
1529 T t596 o594 b595
1530 B b596 t596
1531 T t597 o593 b596
1532 B b597 t597
1533 P p597 Number 753
1534 P p3 Number 765
1535 O o6 location p597 p3
1536 NSummary!prec prec prec Summary
1537 P p6 String prec_op
1538 O o8 prec p6
1539 T t154 o8
1540 B b154 t154
1541 T t155 o6 b154
1542 B b155 t155
1543 P p164 Number 767
1544 P p165 Number 837
1545 O o165 location p164 p165
1546 NSummary!dform dform dform Summary
1547 P p599 String group_df
1548 O o599 dform p599
1549 NSummary!except_mode_df except_mode_df except_mode_df Summary
1550 P p600 String src
1551 O o600 except_mode_df p600
1552 T t600 o600
1553 B b600 t600
1554 T t601 o b600 b4
1555 B b601 t601
1556 NSummary!df_term df_term df_term Summary
1557 O o601 df_term
1558 Nslot slot slot NIL
1559 O o602 slot
1560 T t602 o602 b564
1561 B b602 t602
1562 NPerv!string string602 string Perv
1563 P p602 String " group"
1564 O o603 string602 p602
1565 T t603 o603
1566 B b603 t603
1567 T t604 o b603 b4
1568 B b604 t604
1569 T t605 o b602 b604
1570 B b605 t605
1571 T t606 o601 b605
1572 B b606 t606
1573 T t607 o599 b601 b565 b606
1574 B b607 t607
1575 T t169 o165 b607
1576 B b169 t169
1577 P p174 Number 839
1578 P p175 Number 908
1579 O o175 location p174 p175
1580 P p610 String car_df
1581 O o610 dform p610
1582 P p611 String car(
1583 O o611 string602 p611
1584 T t611 o611
1585 B b611 t611
1586 P p612 String )
1587 O o612 string602 p612
1588 T t612 o612
1589 B b612 t612
1590 T t613 o b612 b4
1591 B b613 t613
1592 T t614 o b602 b613
1593 B b614 t614
1594 T t615 o b611 b614
1595 B b615 t615
1596 T t616 o601 b615
1597 B b616 t616
1598 T t617 o610 b601 b570 b616
1599 B b617 t617
1600 T t177 o175 b617
1601 B b177 t177
1602 P p186 Number 910
1603 P p187 Number 976
1604 O o187 location p186 p187
1605 P p620 String id_df
1606 O o620 dform p620
1607 P p621 String id(
1608 O o621 string602 p621
1609 T t621 o621
1610 B b621 t621
1611 T t622 o b621 b614
1612 B b622 t622
1613 T t623 o601 b622
1614 B b623 t623
1615 T t624 o620 b601 b583 b623
1616 B b624 t624
1617 T t191 o187 b624
1618 B b191 t191
1619 P p194 Number 978
1620 P p200 Number 1116
1621 O o200 location p194 p200
1622 P p627 String op_df
1623 O o627 dform p627
1624 NSummary!prec_df prec_df prec_df Summary
1625 O o201 prec_df p6
1626 T t205 o201
1627 B b205 t205
1628 NSummary!parens_df parens_df parens_df Summary
1629 O o628 parens_df
1630 T t628 o628
1631 B b628 t628
1632 T t629 o b628 b4
1633 B b629 t629
1634 T t206 o b205 b629
1635 B b206 t206
1636 T t208 o b600 b206
1637 B b208 t208
1638 T t630 o b600 b629
1639 B b630 t630
1640 P p630 String op(
1641 O o630 string602 p630
1642 T t631 o630
1643 B b631 t631
1644 P p631 String "; "
1645 O o631 string602 p631
1646 T t632 o631
1647 B b632 t632
1648 T t633 o602 b576
1649 B b633 t633
1650 T t634 o602 b577
1651 B b634 t634
1652 T t635 o b634 b613
1653 B b635 t635
1654 T t636 o b632 b635
1655 B b636 t636
1656 T t637 o b633 b636
1657 B b637 t637
1658 T t638 o b632 b637
1659 B b638 t638
1660 T t639 o b602 b638
1661 B b639 t639
1662 T t640 o b631 b639
1663 B b640 t640
1664 T t641 o601 b640
1665 B b641 t641
1666 T t209 o627 b208 b578 b641
1667 B b209 t209
1668 T t210 o200 b209
1669 B b210 t210
1670 P p217 Number 1118
1671 P p219 Number 1216
1672 O o219 location p217 p219
1673 P p645 String inv_df
1674 O o645 dform p645
1675 P p646 String inv(
1676 O o646 string602 p646
1677 T t646 o646
1678 B b646 t646
1679 T t647 o602 b589
1680 B b647 t647
1681 T t648 o b647 b613
1682 B b648 t648
1683 T t649 o b632 b648
1684 B b649 t649
1685 T t650 o b602 b649
1686 B b650 t650
1687 T t651 o b646 b650
1688 B b651 t651
1689 T t652 o601 b651
1690 B b652 t652
1691 T t653 o645 b630 b590 b652
1692 B b653 t653
1693 T t229 o219 b653
1694 B b229 t229
1695 P p234 Number 1218
1696 P p235 Number 1344
1697 O o235 location p234 p235
1698 P p656 String eqElem_df
1699 O o656 dform p656
1700 P p657 String eq(
1701 O o657 string602 p657
1702 T t657 o657
1703 B b657 t657
1704 T t658 o b657 b639
1705 B b658 t658
1706 T t659 o601 b658
1707 B b659 t659
1708 T t660 o656 b630 b595 b659
1709 B b660 t660
1710 T t240 o235 b660
1711 B b240 t240
1712 P p247 Number 1363
1713 P p262 Number 1497
1714 O o262 location p247 p262
1715 NSummary!rule rule rule Summary
1716 P p663 String group_type
1717 O o663 rule p663
1718 NSummary!context_param context_param context_param Summary
1719 P p664 String H
1720 O o664 context_param p664
1721 T t664 o664
1722 B b664 t664
1723 T t665 o b664 b4
1724 B b665 t665
1725 NSummary!meta_implies meta_implies meta_implies Summary
1726 O o665 meta_implies
1727 NSummary!meta_theorem meta_theorem meta_theorem Summary
1728 O o666 meta_theorem
1729 NBase_trivial Base_trivial Base_trivial NIL
1730 NBase_trivial!squash squash squash Base_trivial
1731 O o667 squash
1732 T t667 o667
1733 B b667 t667
1734 T t668 o b667 b4
1735 C h H
1736 NItt_equal Itt_equal Itt_equal NIL
1737 NItt_equal!equal equal equal Itt_equal
1738 O o668 equal
1739 NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1740 NItt_record_label0!label label label Itt_record_label0
1741 O o669 label
1742 T t669 o669
1743 B b669 t669
1744 T t670 o668 b669 b564 b564
1745 S s t668 h
1746 G s t670
1747 B b670 s
1748 T t671 o666 b670
1749 B b671 t671
1750 P p671 Var ext
1751 O o671 var p671
1752 T t672 o671
1753 B b672 t672
1754 T t673 o b672 b4
1755 NItt_equal!type type type Itt_equal
1756 O o673 type
1757 T t674 o673 b565
1758 S s674 t673 h
1759 G s674 t674
1760 B b674 s674
1761 T t675 o666 b674
1762 B b675 t675
1763 T t676 o665 b671 b675
1764 B b676 t676
1765 NSummary!incomplete incomplete incomplete Summary
1766 O o676 incomplete
1767 T t677 o676
1768 B b677 t677
1769 NSummary!resource_defs resource_defs resource_defs Summary
1770 P p263 Number 1389
1771 P p264 Number 1397
1772 O o264 resource_defs p263 p264 p204
1773 NOcaml!uid uid uid Ocaml
1774 P p265 Number 1395
1775 O o265 uid p265 p264
1776 P p680 String []
1777 O o680 uid p680
1778 T t680 o680
1779 B b680 t680
1780 T t267 o265 b680
1781 B b267 t267
1782 T t271 o b267 b4
1783 B b271 t271
1784 T t272 o264 b271
1785 B b272 t272
1786 T t275 o b272 b4
1787 B b275 t275
1788 T t279 o663 b665 b676 b677 b275
1789 B b279 t279
1790 T t280 o262 b279
1791 B b280 t280
1792 P p284 Number 1499
1793 P p285 Number 1667
1794 O o285 location p284 p285
1795 P p688 String car_wf
1796 O o688 rule p688
1797 S s688 t673 h
1798 G s688 t565
1799 B b688 s688
1800 T t688 o666 b688
1801 B b689 t688
1802 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1803 NCzf_itt_set!isset isset isset Czf_itt_set
1804 O o689 isset
1805 T t689 o689 b570
1806 S s689 t673 h
1807 G s689 t689
1808 B b690 s689
1809 T t690 o666 b690
1810 B b691 t690
1811 T t691 o665 b689 b691
1812 B b692 t691
1813 T t692 o665 b671 b692
1814 B b693 t692
1815 P p286 Number 1521
1816 P p287 Number 1528
1817 O o287 resource_defs p286 p287 p204
1818 P p288 Number 1526
1819 O o288 uid p288 p287
1820 T t299 o288 b680
1821 B b299 t299
1822 T t368 o b299 b4
1823 B b368 t368
1824 T t379 o287 b368
1825 B b379 t379
1826 T t394 o b379 b4
1827 B b394 t394
1828 T t400 o688 b665 b693 b677 b394
1829 B b400 t400
1830 T t401 o285 b400
1831 B b401 t401
1832 P p401 Number 1669
1833 P p403 Number 1936
1834 O o404 location p401 p403
1835 P p702 String op_wf1
1836 O o702 rule p702
1837 T t702 o689 b576
1838 S s702 t668 h
1839 G s702 t702
1840 B b702 s702
1841 T t703 o666 b702
1842 B b703 t703
1843 T t704 o689 b577
1844 S s704 t668 h
1845 G s704 t704
1846 B b704 s704
1847 T t705 o666 b704
1848 B b705 t705
1849 T t706 o689 b578
1850 S s706 t673 h
1851 G s706 t706
1852 B b706 s706
1853 T t707 o666 b706
1854 B b707 t707
1855 T t708 o665 b705 b707
1856 B b708 t708
1857 T t709 o665 b703 b708
1858 B b709 t709
1859 T t710 o665 b689 b709
1860 B b710 t710
1861 T t711 o665 b671 b710
1862 B b711 t711
1863 P p404 Number 1691
1864 P p405 Number 1698
1865 O o405 resource_defs p404 p405 p204
1866 P p406 Number 1696
1867 O o406 uid p406 p405
1868 T t408 o406 b680
1869 B b408 t408
1870 T t409 o b408 b4
1871 B b409 t409
1872 T t415 o405 b409
1873 B b415 t415
1874 T t416 o b415 b4
1875 B b416 t416
1876 T t425 o702 b665 b711 b677 b416
1877 B b425 t425
1878 T t426 o404 b425
1879 B b426 t426
1880 P p427 Number 1938
1881 P p428 Number 2312
1882 O o428 location p427 p428
1883 P p720 String op_wf2
1884 O o720 rule p720
1885 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1886 NCzf_itt_member!mem mem mem Czf_itt_member
1887 O o721 mem
1888 T t721 o721 b576 b570
1889 S s721 t673 h
1890 G s721 t721
1891 B b721 s721
1892 T t722 o666 b721
1893 B b722 t722
1894 T t723 o721 b577 b570
1895 S s723 t673 h
1896 G s723 t723
1897 B b723 s723
1898 T t724 o666 b723
1899 B b724 t724
1900 T t725 o721 b578 b570
1901 S s725 t673 h
1902 G s725 t725
1903 B b725 s725
1904 T t726 o666 b725
1905 B b726 t726
1906 T t727 o665 b724 b726
1907 B b727 t727
1908 T t728 o665 b722 b727
1909 B b728 t728
1910 T t729 o665 b689 b728
1911 B b729 t729
1912 T t730 o665 b671 b729
1913 B b730 t730
1914 T t731 o665 b705 b730
1915 B b731 t731
1916 T t732 o665 b703 b731
1917 B b732 t732
1918 P p429 Number 1960
1919 P p430 Number 1967
1920 O o430 resource_defs p429 p430 p204
1921 P p431 Number 1965
1922 O o431 uid p431 p430
1923 T t434 o431 b680
1924 B b434 t434
1925 T t435 o b434 b4
1926 B b435 t435
1927 T t443 o430 b435
1928 B b443 t443
1929 T t444 o b443 b4
1930 B b444 t444
1931 T t452 o720 b665 b732 b677 b444
1932 B b452 t452
1933 T t453 o428 b452
1934 B b453 t453
1935 P p454 Number 2401
1936 P p455 Number 2774
1937 O o455 location p454 p455
1938 P p741 String op_eq1
1939 O o741 rule p741
1940 P p742 Var s3
1941 O o742 var p742
1942 T t742 o742
1943 B b742 t742
1944 T t743 o689 b742
1945 S s743 t668 h
1946 G s743 t743
1947 B b743 s743
1948 T t744 o666 b743
1949 B b744 t744
1950 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1951 NCzf_itt_eq!eq eq eq Czf_itt_eq
1952 O o744 eq
1953 T t745 o744 b576 b577
1954 S s745 t673 h
1955 G s745 t745
1956 B b745 s745
1957 T t746 o666 b745
1958 B b746 t746
1959 T t747 o575 b564 b742 b576
1960 B b747 t747
1961 T t748 o575 b564 b742 b577
1962 B b748 t748
1963 T t749 o744 b747 b748
1964 S s749 t673 h
1965 G s749 t749
1966 B b749 s749
1967 T t750 o666 b749
1968 B b750 t750
1969 T t751 o665 b746 b750
1970 B b751 t751
1971 T t752 o665 b689 b751
1972 B b752 t752
1973 T t753 o665 b671 b752
1974 B b753 t753
1975 T t754 o665 b744 b753
1976 B b754 t754
1977 T t755 o665 b705 b754
1978 B b755 t755
1979 T t756 o665 b703 b755
1980 B b756 t756
1981 P p456 Number 2423
1982 P p457 Number 2430
1983 O o457 resource_defs p456 p457 p204
1984 P p458 Number 2428
1985 O o458 uid p458 p457
1986 T t461 o458 b680
1987 B b461 t461
1988 T t462 o b461 b4
1989 B b462 t462
1990 T t470 o457 b462
1991 B b470 t470
1992 T t471 o b470 b4
1993 B b471 t471
1994 T t479 o741 b665 b756 b677 b471
1995 B b479 t479
1996 T t480 o455 b479
1997 B b480 t480
1998 P p481 Number 2776
1999 P p482 Number 3149
2000 O o482 location p481 p482
2001 P p765 String op_eq2
2002 O o765 rule p765
2003 T t765 o575 b564 b576 b742
2004 B b765 t765
2005 T t766 o575 b564 b577 b742
2006 B b766 t766
2007 T t767 o744 b765 b766
2008 S s767 t673 h
2009 G s767 t767
2010 B b767 s767
2011 T t768 o666 b767
2012 B b768 t768
2013 T t769 o665 b746 b768
2014 B b769 t769
2015 T t770 o665 b689 b769
2016 B b770 t770
2017 T t771 o665 b671 b770
2018 B b771 t771
2019 T t772 o665 b744 b771
2020 B b772 t772
2021 T t773 o665 b705 b772
2022 B b773 t773
2023 T t774 o665 b703 b773
2024 B b774 t774
2025 P p483 Number 2798
2026 P p484 Number 2805
2027 O o484 resource_defs p483 p484 p204
2028 P p485 Number 2803
2029 O o485 uid p485 p484
2030 T t488 o485 b680
2031 B b488 t488
2032 T t489 o b488 b4
2033 B b489 t489
2034 T t495 o484 b489
2035 B b495 t495
2036 T t496 o b495 b4
2037 B b496 t496
2038 T t502 o765 b665 b774 b677 b496
2039 B b502 t502
2040 T t503 o482 b502
2041 B b503 t503
2042 P p504 Number 3151
2043 P p505 Number 3288
2044 O o505 location p504 p505
2045 P p783 String op_fun1
2046 O o783 rule p783
2047 T t783 o689 b589
2048 S s783 t668 h
2049 G s783 t783
2050 B b783 s783
2051 T t784 o666 b783
2052 B b784 t784
2053 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
2054 O o784 fun_set
2055 P p784 Var z
2056 O o785 var p784
2057 T t785 o785
2058 B b785 t785
2059 T t786 o575 b564 b785 b589
2060 B b786 t786 z
2061 T t787 o784 b786
2062 S s787 t673 h
2063 G s787 t787
2064 B b787 s787
2065 T t788 o666 b787
2066 B b788 t788
2067 T t789 o665 b784 b788
2068 B b789 t789
2069 P p506 Number 3174
2070 P p507 Number 3181
2071 O o507 resource_defs p506 p507 p204
2072 P p511 Number 3179
2073 O o512 uid p511 p507
2074 T t517 o512 b680
2075 B b517 t517
2076 T t518 o b517 b4
2077 B b518 t518
2078 T t525 o507 b518
2079 B b525 t525
2080 T t526 o b525 b4
2081 B b526 t526
2082 T t533 o783 b665 b789 b677 b526
2083 B b533 t533
2084 T t534 o505 b533
2085 B b534 t534
2086 P p534 Number 3290
2087 P p535 Number 3427
2088 O o536 location p534 p535
2089 P p798 String op_fun2
2090 O o798 rule p798
2091 T t798 o575 b564 b589 b785
2092 B b798 t798 z
2093 T t799 o784 b798
2094 S s799 t673 h
2095 G s799 t799
2096 B b799 s799
2097 T t800 o666 b799
2098 B b800 t800
2099 T t801 o665 b784 b800
2100 B b801 t801
2101 P p536 Number 3313
2102 P p537 Number 3320
2103 O o537 resource_defs p536 p537 p204
2104 P p538 Number 3318
2105 O o538 uid p538 p537
2106 T t540 o538 b680
2107 B b540 t540
2108 T t541 o b540 b4
2109 B b541 t541
2110 T t547 o537 b541
2111 B b547 t547
2112 T t548 o b547 b4
2113 B b548 t548
2114 T t554 o798 b665 b801 b677 b548
2115 B b554 t554
2116 T t555 o536 b554
2117 B b555 t555
2118 P p555 Number 3429
2119 P p556 Number 3938
2120 O o557 location p555 p556
2121 P p810 String op_assoc1
2122 O o810 rule p810
2123 T t810 o721 b742 b570
2124 S s810 t673 h
2125 G s810 t810
2126 B b810 s810
2127 T t811 o666 b810
2128 B b811 t811
2129 NCzf_itt_eq!equal equal811 equal Czf_itt_eq
2130 O o811 equal811
2131 T t812 o575 b564 b578 b742
2132 B b812 t812
2133 T t813 o575 b564 b576 b766
2134 B b813 t813
2135 T t814 o811 b812 b813
2136 S s814 t673 h
2137 G s814 t814
2138 B b814 s814
2139 T t815 o666 b814
2140 B b815 t815
2141 T t816 o665 b811 b815
2142 B b816 t816
2143 T t817 o665 b724 b816
2144 B b817 t817
2145 T t818 o665 b722 b817
2146 B b818 t818
2147 T t819 o665 b689 b818
2148 B b819 t819
2149 T t820 o665 b671 b819
2150 B b820 t820
2151 T t821 o665 b744 b820
2152 B b821 t821
2153 T t822 o665 b705 b821
2154 B b822 t822
2155 T t823 o665 b703 b822
2156 B b823 t823
2157 P p557 Number 3454
2158 P p558 Number 3461
2159 O o558 resource_defs p557 p558 p204
2160 P p559 Number 3459
2161 O o559 uid p559 p558
2162 T t561 o559 b680
2163 B b561 t561
2164 T t562 o b561 b4
2165 B b562 t562
2166 T t563 o558 b562
2167 B b563 t563
2168 T t568 o b563 b4
2169 B b568 t568
2170 T t569 o810 b665 b823 b677 b568
2171 B b569 t569
2172 T t573 o557 b569
2173 B b573 t573
2174 P p577 Number 3940
2175 P p578 Number 4449
2176 O o578 location p577 p578
2177 P p832 String op_assoc2
2178 O o832 rule p832
2179 T t832 o811 b813 b812
2180 S s832 t673 h
2181 G s832 t832
2182 B b832 s832
2183 T t833 o666 b832
2184 B b833 t833
2185 T t834 o665 b811 b833
2186 B b834 t834
2187 T t835 o665 b724 b834
2188 B b835 t835
2189 T t836 o665 b722 b835
2190 B b836 t836
2191 T t837 o665 b689 b836
2192 B b837 t837
2193 T t838 o665 b671 b837
2194 B b838 t838
2195 T t839 o665 b744 b838
2196 B b839 t839
2197 T t840 o665 b705 b839
2198 B b840 t840
2199 T t841 o665 b703 b840
2200 B b841 t841
2201 P p579 Number 3965
2202 P p583 Number 3972
2203 O o584 resource_defs p579 p583 p204
2204 P p584 Number 3970
2205 O o585 uid p584 p583
2206 T t586 o585 b680
2207 B b586 t586
2208 T t587 o b586 b4
2209 B b587 t587
2210 T t588 o584 b587
2211 B b588 t588
2212 T t593 o b588 b4
2213 B b593 t593
2214 T t594 o832 b665 b841 b677 b593
2215 B b594 t594
2216 T t598 o578 b594
2217 B b598 t598
2218 P p601 Number 4451
2219 P p603 Number 4619
2220 O o604 location p601 p603
2221 P p850 String id_wf1
2222 O o850 rule p850
2223 T t850 o689 b583
2224 S s850 t673 h
2225 G s850 t850
2226 B b850 s850
2227 T t851 o666 b850
2228 B b851 t851
2229 T t852 o665 b689 b851
2230 B b852 t852
2231 T t853 o665 b671 b852
2232 B b853 t853
2233 P p604 Number 4473
2234 P p605 Number 4481
2235 O o605 resource_defs p604 p605 p204
2236 P p606 Number 4479
2237 O o606 uid p606 p605
2238 T t609 o606 b680
2239 B b609 t609
2240 T t610 o b609 b4
2241 B b610 t610
2242 T t619 o605 b610
2243 B b619 t619
2244 T t620 o b619 b4
2245 B b620 t620
2246 T t626 o850 b665 b853 b677 b620
2247 B b626 t626
2248 T t627 o604 b626
2249 B b627 t627
2250 P p628 Number 4621
2251 P p629 Number 4795
2252 O o629 location p628 p629
2253 P p862 String id_wf2
2254 O o862 rule p862
2255 T t862 o721 b583 b570
2256 S s862 t673 h
2257 G s862 t862
2258 B b862 s862
2259 T t863 o666 b862
2260 B b863 t863
2261 T t864 o665 b689 b863
2262 B b864 t864
2263 T t865 o665 b671 b864
2264 B b865 t865
2265 P p632 Number 4643
2266 P p633 Number 4650
2267 O o633 resource_defs p632 p633 p204
2268 P p634 Number 4648
2269 O o634 uid p634 p633
2270 T t644 o634 b680
2271 B b644 t644
2272 T t645 o b644 b4
2273 B b645 t645
2274 T t655 o633 b645
2275 B b655 t655
2276 T t656 o b655 b4
2277 B b656 t656
2278 T t662 o862 b665 b865 b677 b656
2279 B b662 t662
2280 T t663 o629 b662
2281 B b663 t663
2282 P p665 Number 4797
2283 P p666 Number 5073
2284 O o670 location p665 p666
2285 P p874 String id_eq1
2286 O o874 rule p874
2287 T t874 o721 b589 b570
2288 S s874 t673 h
2289 G s874 t874
2290 B b874 s874
2291 T t875 o666 b874
2292 B b875 t875
2293 T t876 o575 b564 b583 b589
2294 B b876 t876
2295 T t877 o811 b876 b589
2296 S s877 t673 h
2297 G s877 t877
2298 B b877 s877
2299 T t878 o666 b877
2300 B b878 t878
2301 T t879 o665 b875 b878
2302 B b879 t879
2303 T t880 o665 b689 b879
2304 B b880 t880
2305 T t881 o665 b671 b880
2306 B b881 t881
2307 T t882 o665 b784 b881
2308 B b882 t882
2309 P p670 Number 4819
2310 P p672 Number 4826
2311 O o672 resource_defs p670 p672 p204
2312 P p673 Number 4824
2313 O o674 uid p673 p672
2314 T t678 o674 b680
2315 B b678 t678
2316 T t679 o b678 b4
2317 B b679 t679
2318 T t687 o672 b679
2319 B b687 t687
2320 T t693 o b687 b4
2321 B b694 t693
2322 T t694 o874 b665 b882 b677 b694
2323 B b701 t694
2324 T t701 o670 b701
2325 B b712 t701
2326 P p714 Number 5075
2327 P p715 Number 5351
2328 O o715 location p714 p715
2329 P p891 String id_eq2
2330 O o891 rule p891
2331 T t891 o575 b564 b589 b583
2332 B b891 t891
2333 T t892 o811 b891 b589
2334 S s892 t673 h
2335 G s892 t892
2336 B b892 s892
2337 T t893 o666 b892
2338 B b893 t893
2339 T t894 o665 b875 b893
2340 B b894 t894
2341 T t895 o665 b689 b894
2342 B b895 t895
2343 T t896 o665 b671 b895
2344 B b896 t896
2345 T t897 o665 b784 b896
2346 B b897 t897
2347 P p716 Number 5097
2348 P p717 Number 5104
2349 O o717 resource_defs p716 p717 p204
2350 P p721 Number 5102
2351 O o722 uid p721 p717
2352 T t733 o722 b680
2353 B b733 t733
2354 T t740 o b733 b4
2355 B b740 t740
2356 T t741 o717 b740
2357 B b741 t741
2358 T t757 o b741 b4
2359 B b757 t757
2360 T t764 o891 b665 b897 b677 b757
2361 B b764 t764
2362 T t775 o715 b764
2363 B b775 t775
2364 P p777 Number 5353
2365 P p778 Number 5622
2366 O o778 location p777 p778
2367 P p906 String inv_wf1
2368 O o906 rule p906
2369 T t906 o588 b564 b576
2370 B b906 t906
2371 T t907 o689 b906
2372 S s907 t673 h
2373 G s907 t907
2374 B b907 s907
2375 T t908 o666 b907
2376 B b908 t908
2377 T t909 o665 b722 b908
2378 B b909 t909
2379 T t910 o665 b689 b909
2380 B b910 t910
2381 T t911 o665 b671 b910
2382 B b911 t911
2383 T t912 o665 b703 b911
2384 B b912 t912
2385 P p779 Number 5376
2386 P p780 Number 5383
2387 O o780 resource_defs p779 p780 p204
2388 P p785 Number 5381
2389 O o786 uid p785 p780
2390 T t790 o786 b680
2391 B b790 t790
2392 T t797 o b790 b4
2393 B b797 t797
2394 T t802 o780 b797
2395 B b802 t802
2396 T t809 o b802 b4
2397 B b809 t809
2398 T t824 o906 b665 b912 b677 b809
2399 B b824 t824
2400 T t831 o778 b824
2401 B b831 t831
2402 P p833 Number 5624
2403 P p921 String inv_wf2
2404 O o921 rule p921
2405 T t921 o721 b906 b570
2406 S s921 t673 h
2407 G s921 t921
2408 B b921 s921
2409 T t922 o666 b921
2410 B b922 t922
2411 T t923 o665 b722 b922
2412 B b923 t923
2413 T t924 o665 b689 b923
2414 B b924 t924
2415 T t925 o665 b671 b924
2416 B b925 t925
2417 T t926 o665 b703 b925
2418 B b926 t926
2419 P p935 String inv_fun1
2420 O o935 rule p935
2421 T t935 o588 b564 b785
2422 B b935 t935 z
2423 T t936 o784 b935
2424 S s936 t673 h
2425 G s936 t936
2426 B b936 s936
2427 T t937 o666 b936
2428 B b937 t937
2429 T t938 o665 b689 b937
2430 B b938 t938
2431 T t939 o665 b671 b938
2432 B b939 t939
2433 P p940 Number 5900
2434 O o833 location p833 p940
2435 P p834 Number 5647
2436 P p835 Number 5654
2437 O o835 resource_defs p834 p835 p204
2438 P p836 Number 5652
2439 O o836 uid p836 p835
2440 T t842 o836 b680
2441 B b842 t842
2442 T t849 o b842 b4
2443 B b849 t849
2444 T t854 o835 b849
2445 B b854 t854
2446 T t861 o b854 b4
2447 B b861 t861
2448 T t866 o921 b665 b926 b677 b861
2449 B b866 t866
2450 T t873 o833 b866
2451 B b873 t873
2452 P p875 Number 5902
2453 P p876 Number 6081
2454 O o876 location p875 p876
2455 P p877 Number 5926
2456 P p878 Number 5933
2457 O o878 resource_defs p877 p878 p204
2458 P p879 Number 5931
2459 O o879 uid p879 p878
2460 T t883 o879 b680
2461 B b883 t883
2462 T t890 o b883 b4
2463 B b890 t890
2464 T t898 o878 b890
2465 B b898 t898
2466 T t905 o b898 b4
2467 B b905 t905
2468 T t913 o935 b665 b939 b677 b905
2469 B b913 t913
2470 T t920 o876 b913
2471 B b920 t920
2472 P p922 Number 6083
2473 P p923 Number 6373
2474 O o923 location p922 p923
2475 P p948 String inv_id1
2476 O o948 rule p948
2477 T t948 o575 b564 b906 b576
2478 B b948 t948
2479 T t949 o811 b948 b583
2480 S s949 t673 h
2481 G s949 t949
2482 B b949 s949
2483 T t950 o666 b949
2484 B b950 t950
2485 T t951 o665 b722 b950
2486 B b951 t951
2487 T t952 o665 b689 b951
2488 B b952 t952
2489 T t953 o665 b671 b952
2490 B b953 t953
2491 T t954 o665 b703 b953
2492 B b954 t954
2493 P p924 Number 6106
2494 P p925 Number 6113
2495 O o925 resource_defs p924 p925 p204
2496 P p929 Number 6111
2497 O o929 uid p929 p925
2498 T t934 o929 b680
2499 B b934 t934
2500 T t940 o b934 b4
2501 B b940 t940
2502 T t947 o925 b940
2503 B b947 t947
2504 T t955 o b947 b4
2505 B b955 t955
2506 T t962 o948 b665 b954 b677 b955
2507 B b962 t962
2508 T t970 o923 b962
2509 B b970 t970
2510 P p972 Number 6375
2511 P p973 Number 6665
2512 O o973 location p972 p973
2513 P p963 String inv_id2
2514 O o963 rule p963
2515 T t963 o575 b564 b576 b906
2516 B b963 t963
2517 T t964 o811 b963 b583
2518 S s964 t673 h
2519 G s964 t964
2520 B b964 s964
2521 T t965 o666 b964
2522 B b965 t965
2523 T t966 o665 b722 b965
2524 B b966 t966
2525 T t967 o665 b689 b966
2526 B b967 t967
2527 T t968 o665 b671 b967
2528 B b968 t968
2529 T t969 o665 b703 b968
2530 B b969 t969
2531 P p974 Number 6398
2532 P p975 Number 6405
2533 O o975 resource_defs p974 p975 p204
2534 P p979 Number 6403
2535 O o980 uid p979 p975
2536 T t997 o980 b680
2537 B b997 t997
2538 T t999 o b997 b4
2539 B b999 t999
2540 T t1000 o975 b999
2541 B b1000 t1000
2542 T t1022 o b1000 b4
2543 B b1073 t1022
2544 T t1073 o963 b665 b969 b677 b1073
2545 B b1080 t1073
2546 T t1080 o973 b1080
2547 B b1171 t1080
2548 P p1173 Number 6730
2549 P p1174 Number 7267
2550 O o1174 location p1173 p1174
2551 P p978 String cancel1
2552 O o978 rule p978
2553 NSummary!term_param term_param term_param Summary
2554 O o979 term_param
2555 T t979 o979 b564
2556 B b979 t979
2557 T t980 o979 b576
2558 B b980 t980
2559 T t981 o b980 b4
2560 B b981 t981
2561 T t982 o b979 b981
2562 B b982 t982
2563 T t983 o b664 b982
2564 B b983 t983
2565 T t984 o811 b578 b765
2566 S s984 t673 h
2567 G s984 t984
2568 B b984 s984
2569 T t985 o666 b984
2570 B b985 t985
2571 T t986 o811 b577 b742
2572 S s986 t673 h
2573 G s986 t986
2574 B b986 s986
2575 T t987 o666 b986
2576 B b987 t987
2577 T t988 o665 b985 b987
2578 B b988 t988
2579 T t989 o665 b811 b988
2580 B b989 t989
2581 T t990 o665 b724 b989
2582 B b990 t990
2583 T t991 o665 b722 b990
2584 B b991 t991
2585 T t992 o665 b689 b991
2586 B b992 t992
2587 T t993 o665 b671 b992
2588 B b993 t993
2589 T t994 o665 b744 b993
2590 B b994 t994
2591 T t995 o665 b705 b994
2592 B b995 t995
2593 T t996 o665 b703 b995
2594 B b996 t996
2595 NSummary!interactive interactive interactive Summary
2596 O o996 interactive
2597 NSummary!ext_rule ext_rule ext_rule Summary
2598 P p996 String "assumT 9 thenT assertT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenWT autoT"
2599 O o997 ext_rule p996
2600 NSummary!status_incomplete status_incomplete status_incomplete Summary
2601 O o998 status_incomplete
2602 T t998 o998
2603 B b998 t998
2604 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2605 O o999 ext_unjustified
2606 NSummary!tactic_arg tactic_arg tactic_arg Summary
2607 P p999 String main
2608 O o1000 tactic_arg p999
2609 NSummary!msequent msequent msequent Summary
2610 O o1001 msequent
2611 T t1001 o b984 b4
2612 B b1001 t1001
2613 T t1002 o b810 b1001
2614 B b1002 t1002
2615 T t1003 o b723 b1002
2616 B b1003 t1003
2617 T t1004 o b721 b1003
2618 B b1004 t1004
2619 T t1005 o b688 b1004
2620 B b1005 t1005
2621 T t1006 o b670 b1005
2622 B b1006 t1006
2623 T t1007 o b743 b1006
2624 B b1007 t1007
2625 T t1008 o b704 b1007
2626 B b1008 t1008
2627 T t1009 o b702 b1008
2628 B b1009 t1009
2629 T t1010 o1001 b986 b1009
2630 B b1010 t1010
2631 NSummary!parent_none parent_none parent_none Summary
2632 O o1010 parent_none
2633 T t1011 o1010
2634 B b1011 t1011
2635 T t1012 o1000 b1010 b4 b1011
2636 B b1012 t1012
2637 P p1012 String assertion
2638 O o1012 tactic_arg p1012
2639 H h1012 v t984
2640 T t1013 o575 b564 b906 b578
2641 B b1013 t1013
2642 T t1014 o575 b564 b906 b765
2643 B b1014 t1014
2644 T t1015 o811 b1013 b1014
2645 S s1015 t673 h h1012
2646 G s1015 t1015
2647 B b1015 s1015
2648 T t1016 o1001 b1015 b1009
2649 B b1016 t1016
2650 S s1016 t673 h h1012
2651 G s1016 t986
2652 B b1017 s1016
2653 T t1017 o1001 b1017 b1009
2654 B b1018 t1017
2655 T t1018 o2 b1012
2656 B b1019 t1018
2657 T t1019 o1000 b1018 b4 b1019
2658 B b1020 t1019
2659 T t1020 o2 b1020
2660 B b1021 t1020
2661 T t1021 o1012 b1016 b4 b1021
2662 B b1022 t1021
2663 H h1022 v_1 t1015
2664 S s1022 t673 h h1012 h1022
2665 G s1022 t986
2666 B b1023 s1022
2667 T t1023 o1001 b1023 b1009
2668 B b1024 t1023
2669 T t1024 o1000 b1024 b4 b1021
2670 B b1025 t1024
2671 T t1025 o b1025 b4
2672 B b1026 t1025
2673 T t1026 o b1022 b1026
2674 B b1027 t1026
2675 T t1027 o999 b1012 b1027
2676 B b1028 t1027
2677 P p1028 String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2678 O o1028 ext_rule p1028
2679 T t1028 o999 b1022 b4
2680 B b1029 t1028
2681 T t1029 o1028 b998 b1029 b4 b4
2682 B b1030 t1029
2683 P p1030 String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 3 thenAT autoT"
2684 O o1030 ext_rule p1030
2685 T t1030 o575 b564 b948 b577
2686 B b1031 t1030
2687 T t1031 o811 b1031 b1014
2688 H h1031 v_2 t1031
2689 S s1031 t673 h h1012 h1022 h1031
2690 G s1031 t986
2691 B b1032 s1031
2692 T t1032 o1001 b1032 b1009
2693 B b1033 t1032
2694 T t1033 o2 b1025
2695 B b1034 t1033
2696 T t1034 o1000 b1033 b4 b1034
2697 B b1035 t1034
2698 T t1035 o b1035 b4
2699 B b1036 t1035
2700 T t1036 o999 b1025 b1036
2701 B b1037 t1036
2702 P p1037 String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 4 thenAT autoT"
2703 O o1037 ext_rule p1037
2704 T t1037 o575 b564 b948 b742
2705 B b1038 t1037
2706 T t1038 o811 b1031 b1038
2707 H h1038 v_3 t1038
2708 S s1038 t673 h h1012 h1022 h1031 h1038
2709 G s1038 t986
2710 B b1039 s1038
2711 T t1039 o1001 b1039 b1009
2712 B b1040 t1039
2713 T t1040 o2 b1035
2714 B b1041 t1040
2715 T t1041 o1000 b1040 b4 b1041
2716 B b1042 t1041
2717 T t1042 o b1042 b4
2718 B b1043 t1042
2719 T t1043 o999 b1035 b1043
2720 B b1044 t1043
2721 P p1044 String "setSubstT << equal{op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 thenAT autoT"
2722 O o1044 ext_rule p1044
2723 T t1044 o575 b564 b583 b577
2724 B b1045 t1044
2725 T t1045 o575 b564 b583 b742
2726 B b1046 t1045
2727 T t1046 o811 b1045 b1046
2728 H h1046 v_4 t1046
2729 S s1046 t673 h h1012 h1022 h1031 h1038 h1046
2730 G s1046 t986
2731 B b1047 s1046
2732 T t1047 o1001 b1047 b1009
2733 B b1048 t1047
2734 T t1048 o2 b1042
2735 B b1049 t1048
2736 T t1049 o1000 b1048 b4 b1049
2737 B b1050 t1049
2738 T t1050 o b1050 b4
2739 B b1051 t1050
2740 T t1051 o999 b1042 b1051
2741 B b1052 t1051
2742 P p1052 String "setSubstT << equal{op{'g; id{'g}; 's2}; 's2} >> 6 thenAT autoT"
2743 O o1052 ext_rule p1052
2744 T t1052 o811 b577 b1046
2745 H h1052 v_5 t1052
2746 S s1052 t673 h h1012 h1022 h1031 h1038 h1046 h1052
2747 G s1052 t986
2748 B b1053 s1052
2749 T t1053 o1001 b1053 b1009
2750 B b1054 t1053
2751 T t1054 o2 b1050
2752 B b1055 t1054
2753 T t1055 o1000 b1054 b4 b1055
2754 B b1056 t1055
2755 T t1056 o b1056 b4
2756 B b1057 t1056
2757 T t1057 o999 b1050 b1057
2758 B b1058 t1057
2759 P p1058 String "setSubstT << equal{op{'g; id{'g}; 's3}; 's3} >> 7 thenT autoT"
2760 O o1058 ext_rule p1058
2761 T t1058 o999 b1056 b4
2762 B b1059 t1058
2763 T t1059 o1058 b998 b1059 b4 b4
2764 B b1060 t1059
2765 T t1060 o b1060 b4
2766 B b1061 t1060
2767 T t1061 o1052 b998 b1058 b1061 b4
2768 B b1062 t1061
2769 T t1062 o b1062 b4
2770 B b1063 t1062
2771 T t1063 o1044 b998 b1052 b1063 b4
2772 B b1064 t1063
2773 T t1064 o b1064 b4
2774 B b1065 t1064
2775 T t1065 o1037 b998 b1044 b1065 b4
2776 B b1066 t1065
2777 T t1066 o b1066 b4
2778 B b1067 t1066
2779 T t1067 o1030 b998 b1037 b1067 b4
2780 B b1068 t1067
2781 T t1068 o b1068 b4
2782 B b1069 t1068
2783 T t1069 o b1030 b1069
2784 B b1070 t1069
2785 T t1070 o997 b998 b1028 b1070 b4
2786 B b1071 t1070
2787 T t1071 o996 b1071
2788 B b1072 t1071
2789 P p1175 Number 6753
2790 P p1176 Number 6761
2791 O o1176 resource_defs p1175 p1176 p204
2792 P p1180 Number 6759
2793 O o1187 uid p1180 p1176
2794 T t1187 o1187 b680
2795 B b1187 t1187
2796 T t1188 o b1187 b4
2797 B b1188 t1188
2798 T t1189 o1176 b1188
2799 B b1189 t1189
2800 T t1190 o b1189 b4
2801 B b1190 t1190
2802 T t1191 o978 b983 b996 b1072 b1190
2803 B b1191 t1191
2804 T t1192 o1174 b1191
2805 B b1192 t1192
2806 P p1194 Number 7312
2807 P p1198 Number 7849
2808 O o1202 location p1194 p1198
2809 P p1081 String cancel2
2810 O o1081 rule p1081
2811 T t1081 o979 b742
2812 B b1081 t1081
2813 T t1082 o b1081 b4
2814 B b1082 t1082
2815 T t1083 o b979 b1082
2816 B b1083 t1083
2817 T t1084 o b664 b1083
2818 B b1084 t1084
2819 T t1085 o811 b765 b766
2820 S s1085 t673 h
2821 G s1085 t1085
2822 B b1085 s1085
2823 T t1086 o666 b1085
2824 B b1086 t1086
2825 T t1087 o811 b576 b577
2826 S s1087 t673 h
2827 G s1087 t1087
2828 B b1087 s1087
2829 T t1088 o666 b1087
2830 B b1088 t1088
2831 T t1089 o665 b1086 b1088
2832 B b1089 t1089
2833 T t1090 o665 b811 b1089
2834 B b1090 t1090
2835 T t1091 o665 b724 b1090
2836 B b1091 t1091
2837 T t1092 o665 b722 b1091
2838 B b1092 t1092
2839 T t1093 o665 b689 b1092
2840 B b1093 t1093
2841 T t1094 o665 b671 b1093
2842 B b1094 t1094
2843 T t1095 o665 b744 b1094
2844 B b1095 t1095
2845 T t1096 o665 b705 b1095
2846 B b1096 t1096
2847 T t1097 o665 b703 b1096
2848 B b1097 t1097
2849 P p1097 String "assumT 9 thenT assertT << equal{op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}} >> thenT autoT"
2850 O o1097 ext_rule p1097
2851 T t1098 o b1085 b4
2852 B b1098 t1098
2853 T t1099 o b810 b1098
2854 B b1099 t1099
2855 T t1100 o b723 b1099
2856 B b1100 t1100
2857 T t1101 o b721 b1100
2858 B b1101 t1101
2859 T t1102 o b688 b1101
2860 B b1102 t1102
2861 T t1103 o b670 b1102
2862 B b1103 t1103
2863 T t1104 o b743 b1103
2864 B b1104 t1104
2865 T t1105 o b704 b1104
2866 B b1105 t1105
2867 T t1106 o b702 b1105
2868 B b1106 t1106
2869 T t1107 o1001 b1087 b1106
2870 B b1107 t1107
2871 T t1108 o1000 b1107 b4 b1011
2872 B b1108 t1108
2873 H h1108 v t1085
2874 T t1109 o588 b564 b742
2875 B b1109 t1109
2876 T t1110 o575 b564 b765 b1109
2877 B b1110 t1110
2878 T t1111 o575 b564 b766 b1109
2879 B b1111 t1111
2880 T t1112 o811 b1110 b1111
2881 S s1112 t673 h h1108
2882 G s1112 t1112
2883 B b1112 s1112
2884 T t1113 o1001 b1112 b1106
2885 B b1113 t1113
2886 S s1113 t673 h h1108
2887 G s1113 t1087
2888 B b1114 s1113
2889 T t1114 o1001 b1114 b1106
2890 B b1115 t1114
2891 T t1115 o2 b1108
2892 B b1116 t1115
2893 T t1116 o1000 b1115 b4 b1116
2894 B b1117 t1116
2895 T t1117 o2 b1117
2896 B b1118 t1117
2897 T t1118 o1012 b1113 b4 b1118
2898 B b1119 t1118
2899 H h1119 v_1 t1112
2900 S s1119 t673 h h1108 h1119
2901 G s1119 t1087
2902 B b1120 s1119
2903 T t1120 o1001 b1120 b1106
2904 B b1121 t1120
2905 T t1121 o1000 b1121 b4 b1118
2906 B b1122 t1121
2907 T t1122 o b1122 b4
2908 B b1123 t1122
2909 T t1123 o b1119 b1123
2910 B b1124 t1123
2911 T t1124 o999 b1108 b1124
2912 B b1125 t1124
2913 T t1125 o999 b1119 b4
2914 B b1126 t1125
2915 T t1126 o1028 b998 b1126 b4 b4
2916 B b1127 t1126
2917 P p1127 String "setSubstT << equal{op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 3 thenT autoT"
2918 O o1127 ext_rule p1127
2919 T t1127 o575 b564 b742 b1109
2920 B b1128 t1127
2921 T t1128 o575 b564 b576 b1128
2922 B b1129 t1128
2923 T t1129 o811 b1129 b1111
2924 H h1129 v_2 t1129
2925 S s1129 t673 h h1108 h1119 h1129
2926 G s1129 t1087
2927 B b1130 s1129
2928 T t1130 o1001 b1130 b1106
2929 B b1131 t1130
2930 T t1131 o2 b1122
2931 B b1132 t1131
2932 T t1132 o1000 b1131 b4 b1132
2933 B b1133 t1132
2934 T t1133 o b1133 b4
2935 B b1134 t1133
2936 T t1134 o999 b1122 b1134
2937 B b1135 t1134
2938 P p1135 String "setSubstT << equal{op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 4 thenT autoT"
2939 O o1135 ext_rule p1135
2940 T t1135 o575 b564 b577 b1128
2941 B b1136 t1135
2942 T t1136 o811 b1129 b1136
2943 H h1136 v_3 t1136
2944 S s1136 t673 h h1108 h1119 h1129 h1136
2945 G s1136 t1087
2946 B b1137 s1136
2947 T t1137 o1001 b1137 b1106
2948 B b1138 t1137
2949 T t1138 o2 b1133
2950 B b1139 t1138
2951 T t1139 o1000 b1138 b4 b1139
2952 B b1140 t1139
2953 T t1140 o b1140 b4
2954 B b1141 t1140
2955 T t1141 o999 b1133 b1141
2956 B b1142 t1141
2957 P p1142 String "setSubstT << equal{op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 5 thenT autoT"
2958 O o1142 ext_rule p1142
2959 T t1142 o575 b564 b576 b583
2960 B b1143 t1142
2961 T t1143 o575 b564 b577 b583
2962 B b1144 t1143
2963 T t1144 o811 b1143 b1144
2964 H h1144 v_4 t1144
2965 S s1144 t673 h h1108 h1119 h1129 h1136 h1144
2966 G s1144 t1087
2967 B b1145 s1144
2968 T t1145 o1001 b1145 b1106
2969 B b1146 t1145
2970 T t1146 o2 b1140
2971 B b1147 t1146
2972 T t1147 o1000 b1146 b4 b1147
2973 B b1148 t1147
2974 T t1148 o b1148 b4
2975 B b1149 t1148
2976 T t1149 o999 b1140 b1149
2977 B b1150 t1149
2978 P p1150 String "setSubstT << equal{op{'g; 's1; id{'g}}; 's1} >> 6 thenT autoT"
2979 O o1150 ext_rule p1150
2980 T t1150 o811 b576 b1144
2981 H h1150 v_5 t1150
2982 S s1150 t673 h h1108 h1119 h1129 h1136 h1144 h1150
2983 G s1150 t1087
2984 B b1151 s1150
2985 T t1151 o1001 b1151 b1106
2986 B b1152 t1151
2987 T t1152 o2 b1148
2988 B b1153 t1152
2989 T t1153 o1000 b1152 b4 b1153
2990 B b1154 t1153
2991 T t1154 o b1154 b4
2992 B b1155 t1154
2993 T t1155 o999 b1148 b1155
2994 B b1156 t1155
2995 P p1156 String "setSubstT << equal{op{'g; 's2; id{'g}}; 's2} >> 7 thenT autoT"
2996 O o1156 ext_rule p1156
2997 T t1156 o999 b1154 b4
2998 B b1157 t1156
2999 T t1157 o1156 b998 b1157 b4 b4
3000 B b1158 t1157
3001 T t1158 o b1158 b4
3002 B b1159 t1158
3003 T t1159 o1150 b998 b1156 b1159 b4
3004 B b1160 t1159
3005 T t1160 o b1160 b4
3006 B b1161 t1160
3007 T t1161 o1142 b998 b1150 b1161 b4
3008 B b1162 t1161
3009 T t1162 o b1162 b4
3010 B b1163 t1162
3011 T t1163 o1135 b998 b1142 b1163 b4
3012 B b1164 t1163
3013 T t1164 o b1164 b4
3014 B b1165 t1164
3015 T t1165 o1127 b998 b1135 b1165 b4
3016 B b1166 t1165
3017 T t1166 o b1166 b4
3018 B b1167 t1166
3019 T t1167 o b1127 b1167
3020 B b1168 t1167
3021 T t1168 o1097 b998 b1125 b1168 b4
3022 B b1169 t1168
3023 T t1169 o996 b1169
3024 B b1170 t1169
3025 P p1202 Number 7335
3026 P p1205 Number 7343
3027 O o1205 resource_defs p1202 p1205 p204
3028 P p1206 Number 7341
3029 O o1206 uid p1206 p1205
3030 T t1233 o1206 b680
3031 B b1233 t1233
3032 T t1234 o b1233 b4
3033 B b1234 t1234
3034 T t1235 o1205 b1234
3035 B b1235 t1235
3036 T t1238 o b1235 b4
3037 B b1238 t1238
3038 T t1239 o1081 b1084 b1097 b1170 b1238
3039 B b1239 t1239
3040 T t1240 o1202 b1239
3041 B b1240 t1240
3042 P p1249 Number 7851
3043 P p1254 Number 7928
3044 O o1256 location p1249 p1254
3045 NOcaml!str_let str_let str_let Ocaml
3046 O o1257 str_let p1249 p1254
3047 NOcaml!patt_var patt_var patt_var Ocaml
3048 P p1257 Number 7855
3049 O o1259 patt_var p1257 p1254
3050 NOcaml!patt_done patt_done patt_done Ocaml
3051 O o1261 patt_done p1249 p1254
3052 T t1282 o1261
3053 B b1282 t1282 groupCancelLeftT
3054 T t1283 o1259 b1282
3055 B b1283 t1283
3056 NOcaml!fun fun fun Ocaml
3057 O o1285 fun p1257 p1254
3058 NOcaml!patt_if patt_if patt_if Ocaml
3059 O o1286 patt_if p1257 p1254
3060 P p1286 Number 7872
3061 P p1287 Number 7874
3062 O o1287 patt_var p1286 p1287
3063 NOcaml!patt_body patt_body patt_body Ocaml
3064 O o1290 patt_body p1257 p1254
3065 P p1290 Number 7875
3066 P p1291 Number 7877
3067 O o1291 patt_var p1290 p1291
3068 P p1292 Number 7878
3069 P p1293 Number 7879
3070 O o1293 patt_var p1292 p1293
3071 NOcaml!apply apply apply Ocaml
3072 NOcaml!lid lid lid Ocaml
3073 O o1194 lid p978
3074 T t1194 o1194
3075 B b1194 t1194
3076 NOcaml!proj proj proj Ocaml
3077 O o1199 uid p518
3078 T t1199 o1199
3079 B b1199 t1199
3080 P p1201 String hyp_count_addr
3081 O o1201 lid p1201
3082 T t1201 o1201
3083 B b1201 t1201
3084 P p1203 Number 7885
3085 O o1294 apply p1203 p1254
3086 P p1204 Var p
3087 O o1204 var p1204
3088 T t1204 o1204
3089 B b1204 t1204
3090 P p1208 Var t1
3091 O o1208 var p1208
3092 T t1208 o1208
3093 B b1208 t1208
3094 P p1211 Var t2
3095 O o1211 var p1211
3096 T t1211 o1211
3097 B b1211 t1211
3098 P p1213 Number 7894
3099 P p1238 Number 7919
3100 P p1239 Number 7921
3101 P p1241 Number 7924
3102 P p1243 Number 7926
3103 O o1295 apply p1203 p1243
3104 P p1295 Number 7923
3105 O o1296 apply p1203 p1295
3106 P p1296 Number 7920
3107 O o1297 apply p1203 p1296
3108 P p1297 Number 7892
3109 O o1298 lid p1203 p1297
3110 T t1315 o1298 b1194
3111 B b1338 t1315
3112 O o1340 apply p1213 p1238
3113 P p1340 Number 7917
3114 O o1341 proj p1213 p1340
3115 O o1342 uid p1213 p1340
3116 T t1345 o1342 b1199
3117 B b1345 t1345
3118 P p1347 Number 7903
3119 O o1347 lid p1347 p1340
3120 T t1360 o1347 b1201
3121 B b1381 t1360
3122 T t1381 o1341 b1345 b1381
3123 B b1388 t1381
3124 P p1390 Number 7918
3125 O o1390 lid p1390 p1238
3126 T t1403 o1390 b1204
3127 B b1424 t1403
3128 T t1424 o1340 b1388 b1424
3129 B b1431 t1424
3130 T t1431 o1297 b1338 b1431
3131 B b1491 t1431
3132 O o1493 lid p1239 p1295
3133 T t1498 o1493 b1208
3134 B b1498 t1498
3135 T t1545 o1296 b1491 b1498
3136 B b1586 t1545
3137 O o1588 lid p1241 p1243
3138 T t1593 o1588 b1211
3139 B b1593 t1593
3140 T t1594 o1295 b1586 b1593
3141 B b1594 t1594
3142 P p1596 Number 7927
3143 O o1596 lid p1596 p1254
3144 T t1655 o1596 b1204
3145 B b1699 t1655
3146 T t1699 o1294 b1594 b1699
3147 B b1706 t1699
3148 T t1706 o1290 b1706
3149 B b1800 t1706 p
3150 T t1800 o1293 b1800
3151 B b1883 t1800
3152 T t1883 o1286 b1883
3153 B b1910 t1883
3154 T t1910 o1285 b1910
3155 B b1989 t1910
3156 T t1990 o1290 b1989
3157 B b1990 t1990 t2
3158 T t1991 o1291 b1990
3159 B b1991 t1991
3160 T t1992 o1286 b1991
3161 B b1992 t1992
3162 T t1993 o1285 b1992
3163 B b1993 t1993
3164 T t1994 o1290 b1993
3165 B b1994 t1994 t1
3166 T t1995 o1287 b1994
3167 B b1995 t1995
3168 T t1996 o1286 b1995
3169 B b1996 t1996
3170 T t1997 o1285 b1996
3171 B b1997 t1997
3172 T t1998 o1257 b1283 b1997
3173 B b1998 t1998
3174 T t1999 o b1998 b4
3175 B b1999 t1999
3176 T t2000 o1257 b1999
3177 B b2000 t2000
3178 T t2001 o401 b2000
3179 B b2001 t2001
3180 T t2002 o1256 b2001
3181 B b2002 t2002
3182 P p2002 Number 7930
3183 P p2003 Number 8008
3184 O o2003 location p2002 p2003
3185 O o2004 str_let p2002 p2003
3186 P p2004 Number 7934
3187 O o2005 patt_var p2004 p2003
3188 O o2006 patt_done p2002 p2003
3189 T t2006 o2006
3190 B b2006 t2006 groupCancelRightT
3191 T t2007 o2005 b2006
3192 B b2007 t2007
3193 O o2007 fun p2004 p2003
3194 O o2008 patt_if p2004 p2003
3195 P p2008 Number 7952
3196 P p2009 Number 7954
3197 O o2009 patt_var p2008 p2009
3198 O o2010 patt_body p2004 p2003
3199 P p2010 Number 7955
3200 P p2011 Number 7957
3201 O o2011 patt_var p2010 p2011
3202 P p2012 Number 7958
3203 P p2013 Number 7959
3204 O o2013 patt_var p2012 p2013
3205 O o1249 lid p1081
3206 T t1249 o1249
3207 B b1249 t1249
3208 P p1255 Number 7965
3209 O o2014 apply p1255 p2003
3210 P p2014 Number 8006
3211 O o2015 apply p1255 p2014
3212 P p2015 Number 8003
3213 O o2016 apply p1255 p2015
3214 P p2016 Number 8000
3215 O o2017 apply p1255 p2016
3216 P p2017 Number 7972
3217 O o2018 lid p1255 p2017
3218 T t2018 o2018 b1249
3219 B b2018 t2018
3220 P p1262 Number 7974
3221 P p2018 Number 7999
3222 O o2019 apply p1262 p2018
3223 P p2019 Number 7997
3224 O o2020 proj p1262 p2019
3225 O o2021 uid p1262 p2019
3226 T t2021 o2021 b1199
3227 B b2021 t2021
3228 P p2021 Number 7983
3229 O o2022 lid p2021 p2019
3230 T t2022 o2022 b1201
3231 B b2022 t2022
3232 T t2023 o2020 b2021 b2022
3233 B b2023 t2023
3234 P p2023 Number 7998
3235 O o2023 lid p2023 p2018
3236 T t2024 o2023 b1204
3237 B b2024 t2024
3238 T t2025 o2019 b2023 b2024
3239 B b2025 t2025
3240 T t2026 o2017 b2018 b2025
3241 B b2026 t2026
3242 P p2026 Number 8001
3243 O o2026 lid p2026 p2015
3244 T t2027 o2026 b1208
3245 B b2027 t2027
3246 T t2028 o2016 b2026 b2027
3247 B b2028 t2028
3248 P p2028 Number 8004
3249 O o2028 lid p2028 p2014
3250 T t2029 o2028 b1211
3251 B b2029 t2029
3252 T t2030 o2015 b2028 b2029
3253 B b2030 t2030
3254 P p2030 Number 8007
3255 O o2030 lid p2030 p2003
3256 T t2031 o2030 b1204
3257 B b2031 t2031
3258 T t2032 o2014 b2030 b2031
3259 B b2032 t2032
3260 T t2033 o2010 b2032
3261 B b2033 t2033 p
3262 T t2034 o2013 b2033
3263 B b2034 t2034
3264 T t2035 o2008 b2034
3265 B b2035 t2035
3266 T t2036 o2007 b2035
3267 B b2036 t2036
3268 T t2037 o2010 b2036
3269 B b2037 t2037 t2
3270 T t2038 o2011 b2037
3271 B b2038 t2038
3272 T t2039 o2008 b2038
3273 B b2039 t2039
3274 T t2040 o2007 b2039
3275 B b2040 t2040
3276 T t2041 o2010 b2040
3277 B b2041 t2041 t1
3278 T t2042 o2009 b2041
3279 B b2042 t2042
3280 T t2043 o2008 b2042
3281 B b2043 t2043
3282 T t2044 o2007 b2043
3283 B b2044 t2044
3284 T t2045 o2004 b2007 b2044
3285 B b2045 t2045
3286 T t2046 o b2045 b4
3287 B b2046 t2046
3288 T t2047 o2004 b2046
3289 B b2047 t2047
3290 T t2048 o401 b2047
3291 B b2048 t2048
3292 T t2049 o2003 b2048
3293 B b2049 t2049
3294 P p2049 Number 8026
3295 P p2050 Number 8403
3296 O o2050 location p2049 p2050
3297 P p1283 String unique_id1
3298 O o1283 rule p1283
3299 P p1284 Var e2
3300 O o1284 var p1284
3301 T t1284 o1284
3302 B b1284 t1284
3303 T t1285 o689 b1284
3304 S s1285 t668 h
3305 G s1285 t1285
3306 B b1285 s1285
3307 T t1286 o666 b1285
3308 B b1286 t1286
3309 T t1287 o721 b1284 b570
3310 S s1287 t673 h
3311 G s1287 t1287
3312 B b1287 s1287
3313 T t1288 o666 b1287
3314 B b1288 t1288
3315 NCzf_itt_dall Czf_itt_dall Czf_itt_dall NIL
3316 NCzf_itt_dall!dall dall dall Czf_itt_dall
3317 O o1288 dall
3318 NItt_logic Itt_logic Itt_logic NIL
3319 NItt_logic!and and and Itt_logic
3320 O o1289 and
3321 T t1289 o575 b564 b1284 b589
3322 B b1289 t1289
3323 T t1290 o744 b1289 b589
3324 B b1290 t1290
3325 T t1291 o575 b564 b589 b1284
3326 B b1291 t1291
3327 T t1292 o744 b1291 b589
3328 B b1292 t1292
3329 T t1293 o1289 b1290 b1292
3330 B b1293 t1293 s
3331 T t1294 o1288 b570 b1293
3332 S s1294 t673 h
3333 G s1294 t1294
3334 B b1294 s1294
3335 T t1295 o666 b1294
3336 B b1295 t1295
3337 T t1296 o744 b1284 b583
3338 S s1296 t673 h
3339 G s1296 t1296
3340 B b1296 s1296
3341 T t1297 o666 b1296
3342 B b1297 t1297
3343 T t1298 o665 b1295 b1297
3344 B b1298 t1298
3345 T t1299 o665 b1288 b1298
3346 B b1299 t1299
3347 T t1300 o665 b689 b1299
3348 B b1300 t1300
3349 T t1301 o665 b671 b1300
3350 B b1301 t1301
3351 T t1302 o665 b1286 b1301
3352 B b1302 t1302
3353 P p1302 String "assumT 5 thenT withT << id{'g} >> (dT 2) thenT autoT"
3354 O o1302 ext_rule p1302
3355 T t1303 o b1294 b4
3356 B b1303 t1303
3357 T t1304 o b1287 b1303
3358 B b1304 t1304
3359 T t1305 o b688 b1304
3360 B b1305 t1305
3361 T t1306 o b670 b1305
3362 B b1306 t1306
3363 T t1307 o b1285 b1306
3364 B b1307 t1307
3365 T t1308 o1001 b1296 b1307
3366 B b1308 t1308
3367 T t1309 o1000 b1308 b4 b1011
3368 B b1309 t1309
3369 H h1309 v t1294
3370 T t1310 o575 b564 b1284 b583
3371 B b1310 t1310
3372 T t1311 o744 b1310 b583
3373 H h1311 y t1311
3374 T t1312 o575 b564 b583 b1284
3375 B b1312 t1312
3376 T t1313 o744 b1312 b583
3377 H h1313 z t1313
3378 S s1313 t673 h h1309 h1311 h1313
3379 G s1313 t1296
3380 B b1313 s1313
3381 T t1314 o1001 b1313 b1307
3382 B b1314 t1314
3383 B b1315 t1311
3384 B b1316 t1313
3385 T t1316 o1289 b1315 b1316
3386 H h1316 w t1316
3387 S s1316 t673 h h1309 h1316
3388 G s1316 t1296
3389 B b1317 s1316
3390 T t1317 o1001 b1317 b1307
3391 B b1318 t1317
3392 S s1318 t673 h h1309
3393 G s1318 t1296
3394 B b1319 s1318
3395 T t1319 o1001 b1319 b1307
3396 B b1320 t1319
3397 NSummary!arg_named arg_named arg_named Summary
3398 P p1320 String with
3399 O o1320 arg_named p1320
3400 NSummary!arg_term_list arg_term_list arg_term_list Summary
3401 O o1321 arg_term_list
3402 T t1321 o b583 b4
3403 B b1321 t1321
3404 T t1322 o1321 b1321
3405 B b1322 t1322
3406 T t1323 o1320 b1322
3407 B b1323 t1323
3408 T t1324 o b1323 b4
3409 B b1324 t1324
3410 T t1325 o2 b1309
3411 B b1325 t1325
3412 T t1326 o1000 b1320 b1324 b1325
3413 B b1326 t1326
3414 T t1327 o2 b1326
3415 B b1327 t1327
3416 T t1328 o1000 b1318 b4 b1327
3417 B b1328 t1328
3418 T t1329 o2 b1328
3419 B b1329 t1329
3420 T t1330 o1000 b1314 b4 b1329
3421 B b1330 t1330
3422 T t1331 o b1330 b4
3423 B b1331 t1331
3424 T t1332 o999 b1309 b1331
3425 B b1332 t1332
3426 P p1332 String "setSubstT << equal{op{'g; id{'g}; 'e2}; 'e2} >> 4 thenT autoT"
3427 O o1332 ext_rule p1332
3428 T t1333 o999 b1330 b4
3429 B b1333 t1333
3430 T t1334 o1332 b998 b1333 b4 b4
3431 B b1334 t1334
3432 T t1335 o b1334 b4
3433 B b1335 t1335
3434 T t1336 o1302 b998 b1332 b1335 b4
3435 B b1336 t1336
3436 T t1337 o996 b1336
3437 B b1337 t1337
3438 P p2051 Number 8052
3439 P p2052 Number 8060
3440 O o2052 resource_defs p2051 p2052 p204
3441 P p2053 Number 8058
3442 O o2053 uid p2053 p2052
3443 T t2053 o2053 b680
3444 B b2053 t2053
3445 T t2054 o b2053 b4
3446 B b2054 t2054
3447 T t2055 o2052 b2054
3448 B b2055 t2055
3449 T t2056 o b2055 b4
3450 B b2056 t2056
3451 T t2057 o1283 b665 b1302 b1337 b2056
3452 B b2057 t2057
3453 T t2058 o2050 b2057
3454 B b2058 t2058
3455 P p2058 Number 8405
3456 P p2059 Number 8750
3457 O o2059 location p2058 p2059
3458 P p1346 String unique_id2
3459 O o1346 rule p1346
3460 B b1346 t1290 s
3461 T t1346 o1288 b570 b1346
3462 S s1346 t673 h
3463 G s1346 t1346
3464 B b1347 s1346
3465 T t1347 o666 b1347
3466 B b1348 t1347
3467 T t1348 o665 b1348 b1297
3468 B b1349 t1348
3469 T t1349 o665 b1288 b1349
3470 B b1350 t1349
3471 T t1350 o665 b689 b1350
3472 B b1351 t1350
3473 T t1351 o665 b671 b1351
3474 B b1352 t1351
3475 T t1352 o665 b1286 b1352
3476 B b1353 t1352
3477 P p1353 String "assumT 5"
3478 O o1353 ext_rule p1353
3479 T t1353 o b1347 b4
3480 B b1354 t1353
3481 T t1354 o b1287 b1354
3482 B b1355 t1354
3483 T t1355 o b688 b1355
3484 B b1356 t1355
3485 T t1356 o b670 b1356
3486 B b1357 t1356
3487 T t1357 o b1285 b1357
3488 B b1358 t1357
3489 T t1358 o1001 b1296 b1358
3490 B b1359 t1358
3491 T t1359 o1000 b1359 b4 b1011
3492 B b1360 t1359
3493 H h1360 v t1346
3494 S s1360 t673 h h1360
3495 G s1360 t1296
3496 B b1361 s1360
3497 T t1361 o1001 b1361 b1358
3498 B b1362 t1361
3499 T t1362 o2 b1360
3500 B b1363 t1362
3501 T t1363 o1000 b1362 b4 b1363
3502 B b1364 t1363
3503 T t1364 o b1364 b4
3504 B b1365 t1364
3505 T t1365 o999 b1360 b1365
3506 B b1366 t1365
3507 P p1366 String "withT << id{'g} >> (dT 2) thenAT autoT"
3508 O o1366 ext_rule p1366
3509 H h1366 w t1311
3510 S s1366 t673 h h1360 h1366
3511 G s1366 t1296
3512 B b1367 s1366
3513 T t1367 o1001 b1367 b1358
3514 B b1368 t1367
3515 T t1368 o1000 b1362 b1324 b1363
3516 B b1369 t1368
3517 T t1369 o2 b1369
3518 B b1370 t1369
3519 T t1370 o1000 b1368 b4 b1370
3520 B b1371 t1370
3521 T t1371 o b1371 b4
3522 B b1372 t1371
3523 T t1372 o999 b1364 b1372
3524 B b1373 t1372
3525 P p1373 String "setSubstT << equal{op{'g; 'e2; id{'g}}; 'e2} >> 3 thenT autoT"
3526 O o1373 ext_rule p1373
3527 T t1373 o999 b1371 b4
3528 B b1374 t1373
3529 T t1374 o1373 b998 b1374 b4 b4
3530 B b1375 t1374
3531 T t1375 o b1375 b4
3532 B b1376 t1375
3533 T t1376 o1366 b998 b1373 b1376 b4
3534 B b1377 t1376
3535 T t1377 o b1377 b4
3536 B b1378 t1377
3537 T t1378 o1353 b998 b1366 b1378 b4
3538 B b1379 t1378
3539 T t1379 o996 b1379
3540 B b1380 t1379
3541 P p2060 Number 8431
3542 P p2061 Number 8439
3543 O o2061 resource_defs p2060 p2061 p204
3544 P p2062 Number 8437
3545 O o2062 uid p2062 p2061
3546 T t2062 o2062 b680
3547 B b2062 t2062
3548 T t2063 o b2062 b4
3549 B b2063 t2063
3550 T t2064 o2061 b2063
3551 B b2064 t2064
3552 T t2065 o b2064 b4
3553 B b2065 t2065
3554 T t2066 o1346 b665 b1353 b1380 b2065
3555 B b2066 t2066
3556 T t2067 o2059 b2066
3557 B b2067 t2067
3558 P p2067 Number 8752
3559 P p2068 Number 9097
3560 O o2068 location p2067 p2068
3561 P p1389 String unique_id3
3562 O o1389 rule p1389
3563 B b1389 t1292 s
3564 T t1389 o1288 b570 b1389
3565 S s1389 t673 h
3566 G s1389 t1389
3567 B b1390 s1389
3568 T t1390 o666 b1390
3569 B b1391 t1390
3570 T t1391 o665 b1391 b1297
3571 B b1392 t1391
3572 T t1392 o665 b1288 b1392
3573 B b1393 t1392
3574 T t1393 o665 b689 b1393
3575 B b1394 t1393
3576 T t1394 o665 b671 b1394
3577 B b1395 t1394
3578 T t1395 o665 b1286 b1395
3579 B b1396 t1395
3580 T t1396 o b1390 b4
3581 B b1397 t1396
3582 T t1397 o b1287 b1397
3583 B b1398 t1397
3584 T t1398 o b688 b1398
3585 B b1399 t1398
3586 T t1399 o b670 b1399
3587 B b1400 t1399
3588 T t1400 o b1285 b1400
3589 B b1401 t1400
3590 T t1401 o1001 b1296 b1401
3591 B b1402 t1401
3592 T t1402 o1000 b1402 b4 b1011
3593 B b1403 t1402
3594 H h1403 v t1389
3595 S s1403 t673 h h1403
3596 G s1403 t1296
3597 B b1404 s1403
3598 T t1404 o1001 b1404 b1401
3599 B b1405 t1404
3600 T t1405 o2 b1403
3601 B b1406 t1405
3602 T t1406 o1000 b1405 b4 b1406
3603 B b1407 t1406
3604 T t1407 o b1407 b4
3605 B b1408 t1407
3606 T t1408 o999 b1403 b1408
3607 B b1409 t1408
3608 H h1409 w t1313
3609 S s1409 t673 h h1403 h1409
3610 G s1409 t1296
3611 B b1410 s1409
3612 T t1410 o1001 b1410 b1401
3613 B b1411 t1410
3614 T t1411 o1000 b1405 b1324 b1406
3615 B b1412 t1411
3616 T t1412 o2 b1412
3617 B b1413 t1412
3618 T t1413 o1000 b1411 b4 b1413
3619 B b1414 t1413
3620 T t1414 o b1414 b4
3621 B b1415 t1414
3622 T t1415 o999 b1407 b1415
3623 B b1416 t1415
3624 P p1416 String "setSubstT << equal{op{'g; id{'g}; 'e2}; 'e2} >> 3 thenT autoT"
3625 O o1416 ext_rule p1416
3626 T t1416 o999 b1414 b4
3627 B b1417 t1416
3628 T t1417 o1416 b998 b1417 b4 b4
3629 B b1418 t1417
3630 T t1418 o b1418 b4
3631 B b1419 t1418
3632 T t1419 o1366 b998 b1416 b1419 b4
3633 B b1420 t1419
3634 T t1420 o b1420 b4
3635 B b1421 t1420
3636 T t1421 o1353 b998 b1409 b1421 b4
3637 B b1422 t1421
3638 T t1422 o996 b1422
3639 B b1423 t1422
3640 P p2069 Number 8778
3641 P p2070 Number 8786
3642 O o2070 resource_defs p2069 p2070 p204
3643 P p2071 Number 8784
3644 O o2071 uid p2071 p2070
3645 T t2071 o2071 b680
3646 B b2071 t2071
3647 T t2072 o b2071 b4
3648 B b2072 t2072
3649 T t2073 o2070 b2072
3650 B b2073 t2073
3651 T t2074 o b2073 b4
3652 B b2074 t2074
3653 T t2075 o1389 b665 b1396 b1423 b2074
3654 B b2075 t2075
3655 T t2076 o2068 b2075
3656 B b2076 t2076
3657 P p1432 String unique_inv1
3658 O o1432 rule p1432
3659 T t1432 o575 b564 b577 b589
3660 B b1432 t1432
3661 T t1433 o811 b1432 b583
3662 S s1433 t673 h
3663 G s1433 t1433
3664 B b1433 s1433
3665 T t1434 o666 b1433
3666 B b1434 t1434
3667 T t1435 o811 b577 b590
3668 S s1435 t673 h
3669 G s1435 t1435
3670 B b1435 s1435
3671 T t1436 o666 b1435
3672 B b1436 t1436
3673 T t1437 o665 b1434 b1436
3674 B b1437 t1437
3675 T t1438 o665 b724 b1437
3676 B b1438 t1438
3677 T t1439 o665 b875 b1438
3678 B b1439 t1439
3679 T t1440 o665 b689 b1439
3680 B b1440 t1440
3681 T t1441 o665 b671 b1440
3682 B b1441 t1441
3683 T t1442 o665 b705 b1441
3684 B b1442 t1442
3685 T t1443 o665 b784 b1442
3686 B b1443 t1443
3687 P p1443 String "assumT 7 thenT setSubstT << equal{id{'g}; op{'g; inv{'g; 's}; 's}}>> 2 thenAT autoT"
3688 O o1443 ext_rule p1443
3689 T t1444 o b1433 b4
3690 B b1444 t1444
3691 T t1445 o b723 b1444
3692 B b1445 t1445
3693 T t1446 o b874 b1445
3694 B b1446 t1446
3695 T t1447 o b688 b1446
3696 B b1447 t1447
3697 T t1448 o b670 b1447
3698 B b1448 t1448
3699 T t1449 o b704 b1448
3700 B b1449 t1449
3701 T t1450 o b783 b1449
3702 B b1450 t1450
3703 T t1451 o1001 b1435 b1450
3704 B b1451 t1451
3705 T t1452 o1000 b1451 b4 b1011
3706 B b1452 t1452
3707 P p1452 String eq
3708 O o1452 tactic_arg p1452
3709 H h1452 v t1433
3710 T t1453 o575 b564 b590 b589
3711 B b1453 t1453
3712 T t1454 o744 b583 b1453
3713 S s1454 t673 h h1452
3714 G s1454 t1454
3715 B b1454 s1454
3716 T t1455 o1001 b1454 b1450
3717 B b1455 t1455
3718 T t1456 o811 b583 b1453
3719 S s1456 t673 h h1452
3720 G s1456 t1456
3721 B b1456 s1456
3722 T t1457 o1001 b1456 b1450
3723 B b1457 t1457
3724 P p1457 String d_auto
3725 O o1457 arg_named p1457
3726 NSummary!arg_bool arg_bool arg_bool Summary
3727 P p1458 String true
3728 O o1458 arg_bool p1458
3729 T t1458 o1458
3730 B b1458 t1458
3731 T t1459 o1457 b1458
3732 B b1459 t1459
3733 T t1460 o b1459 b4
3734 B b1460 t1460
3735 S s1460 t673 h h1452
3736 G s1460 t1435
3737 B b1461 s1460
3738 T t1461 o1001 b1461 b1450
3739 B b1462 t1461
3740 T t1462 o2 b1452
3741 B b1463 t1462
3742 T t1463 o1000 b1462 b4 b1463
3743 B b1464 t1463
3744 T t1464 o2 b1464
3745 B b1465 t1464
3746 T t1465 o1452 b1457 b1460 b1465
3747 B b1466 t1465
3748 T t1466 o2 b1466
3749 B b1467 t1466
3750 T t1467 o1452 b1455 b4 b1467
3751 B b1468 t1467
3752 T t1468 o811 b1432 b1453
3753 H h1468 v_1 t1468
3754 S s1468 t673 h h1452 h1468
3755 G s1468 t1435
3756 B b1469 s1468
3757 T t1469 o1001 b1469 b1450
3758 B b1470 t1469
3759 T t1470 o1000 b1470 b4 b1465
3760 B b1471 t1470
3761 T t1471 o b1471 b4
3762 B b1472 t1471
3763 T t1472 o b1468 b1472
3764 B b1473 t1472
3765 T t1473 o999 b1452 b1473
3766 B b1474 t1473
3767 P p1474 String "assertT << equal{op{'g; inv{'g; 's}; 's}; id{'g}}>> thenT autoT"
3768 O o1474 ext_rule p1474
3769 T t1474 o811 b1453 b583
3770 H h1474 v_1 t1474
3771 S s1474 t673 h h1452 h1474
3772 G s1474 t1454
3773 B b1475 s1474
3774 T t1475 o1001 b1475 b1450
3775 B b1476 t1475
3776 T t1476 o2 b1468
3777 B b1477 t1476
3778 T t1477 o1000 b1476 b4 b1477
3779 B b1478 t1477
3780 T t1478 o b1478 b4
3781 B b1479 t1478
3782 T t1479 o999 b1468 b1479
3783 B b1480 t1479
3784 P p1480 String "rwh unfold_equal 3 thenT eqSetSymT thenT autoT"
3785 O o1480 ext_rule p1480
3786 T t1480 o999 b1478 b4
3787 B b1481 t1480
3788 T t1481 o1480 b998 b1481 b4 b4
3789 B b1482 t1481
3790 T t1482 o b1482 b4
3791 B b1483 t1482
3792 T t1483 o1474 b998 b1480 b1483 b4
3793 B b1484 t1483
3794 P p1484 String "groupCancelRightT << 'g >> << 's >> thenT autoT"
3795 O o1484 ext_rule p1484
3796 T t1484 o999 b1471 b4
3797 B b1485 t1484
3798 T t1485 o1484 b998 b1485 b4 b4
3799 B b1486 t1485
3800 T t1486 o b1486 b4
3801 B b1487 t1486
3802 T t1487 o b1484 b1487
3803 B b1488 t1487
3804 T t1488 o1443 b998 b1474 b1488 b4
3805 B b1489 t1488
3806 T t1489 o996 b1489
3807 B b1490 t1489
3808 P p1492 Number 9099
3809 P p2076 Number 9533
3810 O o2076 location p1492 p2076
3811 P p2077 Number 9126
3812 P p2078 Number 9134
3813 O o2078 resource_defs p2077 p2078 p204
3814 P p2079 Number 9132
3815 O o2079 uid p2079 p2078
3816 T t2079 o2079 b680
3817 B b2079 t2079
3818 T t2080 o b2079 b4
3819 B b2080 t2080
3820 T t2081 o2078 b2080
3821 B b2081 t2081
3822 T t2082 o b2081 b4
3823 B b2082 t2082
3824 T t2083 o1432 b665 b1443 b1490 b2082
3825 B b2083 t2083
3826 T t2084 o2076 b2083
3827 B b2084 t2084
3828 P p1499 String unique_inv2
3829 O o1499 rule p1499
3830 T t1499 o575 b564 b589 b577
3831 B b1499 t1499
3832 T t1500 o811 b1499 b583
3833 S s1500 t673 h
3834 G s1500 t1500
3835 B b1500 s1500
3836 T t1501 o666 b1500
3837 B b1501 t1501
3838 T t1502 o665 b1501 b1436
3839 B b1502 t1502
3840 T t1503 o665 b724 b1502
3841 B b1503 t1503
3842 T t1504 o665 b875 b1503
3843 B b1504 t1504
3844 T t1505 o665 b689 b1504
3845 B b1505 t1505
3846 T t1506 o665 b671 b1505
3847 B b1506 t1506
3848 T t1507 o665 b705 b1506
3849 B b1507 t1507
3850 T t1508 o665 b784 b1507
3851 B b1508 t1508
3852 P p1508 String "assumT 7 thenT setSubstT << equal{id{'g}; op{'g; 's; inv{'g; 's}}}>> 2 thenAT autoT"
3853 O o1508 ext_rule p1508
3854 T t1509 o b1500 b4
3855 B b1509 t1509
3856 T t1510 o b723 b1509
3857 B b1510 t1510
3858 T t1511 o b874 b1510
3859 B b1511 t1511
3860 T t1512 o b688 b1511
3861 B b1512 t1512
3862 T t1513 o b670 b1512
3863 B b1513 t1513
3864 T t1514 o b704 b1513
3865 B b1514 t1514
3866 T t1515 o b783 b1514
3867 B b1515 t1515
3868 T t1516 o1001 b1435 b1515
3869 B b1516 t1516
3870 T t1517 o1000 b1516 b4 b1011
3871 B b1517 t1517
3872 H h1517 v t1500
3873 T t1518 o575 b564 b589 b590
3874 B b1518 t1518
3875 T t1519 o744 b583 b1518
3876 S s1519 t673 h h1517
3877 G s1519 t1519
3878 B b1519 s1519
3879 T t1520 o1001 b1519 b1515
3880 B b1520 t1520
3881 T t1521 o811 b583 b1518
3882 S s1521 t673 h h1517
3883 G s1521 t1521
3884 B b1521 s1521
3885 T t1522 o1001 b1521 b1515
3886 B b1522 t1522
3887 S s1522 t673 h h1517
3888 G s1522 t1435
3889 B b1523 s1522
3890 T t1523 o1001 b1523 b1515
3891 B b1524 t1523
3892 T t1524 o2 b1517
3893 B b1525 t1524
3894 T t1525 o1000 b1524 b4 b1525
3895 B b1526 t1525
3896 T t1526 o2 b1526
3897 B b1527 t1526
3898 T t1527 o1452 b1522 b1460 b1527
3899 B b1528 t1527
3900 T t1528 o2 b1528
3901 B b1529 t1528
3902 T t1529 o1452 b1520 b4 b1529
3903 B b1530 t1529
3904 T t1530 o811 b1499 b1518
3905 H h1530 v_1 t1530
3906 S s1530 t673 h h1517 h1530
3907 G s1530 t1435
3908 B b1531 s1530
3909 T t1531 o1001 b1531 b1515
3910 B b1532 t1531
3911 T t1532 o1000 b1532 b4 b1527
3912 B b1533 t1532
3913 T t1533 o b1533 b4
3914 B b1534 t1533
3915 T t1534 o b1530 b1534
3916 B b1535 t1534
3917 T t1535 o999 b1517 b1535
3918 B b1536 t1535
3919 P p1536 String "assertT << equal{op{'g; 's; inv{'g; 's}}; id{'g}}>> thenT autoT"
3920 O o1536 ext_rule p1536
3921 T t1536 o811 b1518 b583
3922 H h1536 v_1 t1536
3923 S s1536 t673 h h1517 h1536
3924 G s1536 t1519
3925 B b1537 s1536
3926 T t1537 o1001 b1537 b1515
3927 B b1538 t1537
3928 T t1538 o2 b1530
3929 B b1539 t1538
3930 T t1539 o1000 b1538 b4 b1539
3931 B b1540 t1539
3932 T t1540 o b1540 b4
3933 B b1541 t1540
3934 T t1541 o999 b1530 b1541
3935 B b1542 t1541
3936 T t1542 o999 b1540 b4
3937 B b1543 t1542
3938 T t1543 o1480 b998 b1543 b4 b4
3939 B b1544 t1543
3940 T t1544 o b1544 b4
3941 B b1545 t1544
3942 P p1545 String "rwh unfold_equal 3 thenT eqSetSymT"
3943 O o1545 ext_rule p1545
3944 S s1545 t673 h h1517 h1474
3945 G s1545 t1519
3946 B b1546 s1545
3947 T t1546 o1001 b1546 b1515
3948 B b1547 t1546
3949 T t1547 o1000 b1547 b4 b1539
3950 B b1548 t1547
3951 P p1548 String wf
3952 O o1548 tactic_arg p1548
3953 T t1548 o689 b1453
3954 B b1549 t1548
3955 B b1550 t850
3956 T t1550 o1289 b1549 b1550
3957 B b1551 t1550
3958 T t1551 o744 b1453 b583
3959 B b1552 t1551
3960 T t1552 o1289 b1551 b1552
3961 H h1552 v_1 t1552
3962 S s1552 t668 h h1517 h1552
3963 G s1552 t850
3964 B b1553 s1552
3965 T t1553 o1001 b1553 b1515
3966 B b1554 t1553
3967 S s1554 t673 h h1517 h1552
3968 G s1554 t1519
3969 B b1555 s1554
3970 T t1555 o1001 b1555 b1515
3971 B b1556 t1555
3972 T t1556 o2 b1548
3973 B b1557 t1556
3974 T t1557 o1000 b1556 b4 b1557
3975 B b1558 t1557
3976 T t1558 o2 b1558
3977 B b1559 t1558
3978 T t1559 o1548 b1554 b4 b1559
3979 B b1560 t1559
3980 T t1560 o689 b1518
3981 S s1560 t668 h h1517 h1552
3982 G s1560 t1560
3983 B b1561 s1560
3984 T t1561 o1001 b1561 b1515
3985 B b1562 t1561
3986 T t1562 o1548 b1562 b4 b1559
3987 B b1563 t1562
3988 T t1563 o744 b1518 b583
3989 S s1563 t673 h h1517 h1552
3990 G s1563 t1563
3991 B b1564 s1563
3992 T t1564 o1001 b1564 b1515
3993 B b1565 t1564
3994 T t1565 o1000 b1565 b4 b1559
3995 B b1566 t1565
3996 T t1566 o b1566 b4
3997 B b1567 t1566
3998 T t1567 o b1563 b1567
3999 B b1568 t1567
4000 T t1568 o b1560 b1568
4001 B b1569 t1568
4002 T t1569 o999 b1548 b1569
4003 B b1570 t1569
4004 NSummary!ext_goal ext_goal ext_goal Summary
4005 O o1570 ext_goal
4006 T t1570 o1570 b1560
4007 B b1571 t1570
4008 T t1571 o1570 b1563
4009 B b1572 t1571
4010 T t1572 o1570 b1566
4011 B b1573 t1572
4012 T t1573 o b1573 b4
4013 B b1574 t1573
4014 T t1574 o b1572 b1574
4015 B b1575 t1574
4016 T t1575 o b1571 b1575
4017 B b1576 t1575
4018 T t1576 o1545 b998 b1570 b1576 b4
4019 B b1577 t1576
4020 T t1577 o b1577 b4
4021 B b1578 t1577
4022 T t1578 o1536 b998 b1542 b1545 b1578
4023 B b1579 t1578
4024 P p1579 String "groupCancelLeftT << 'g >> << 's >> thenT autoT"
4025 O o1579 ext_rule p1579
4026 T t1579 o999 b1533 b4
4027 B b1580 t1579
4028 T t1580 o1579 b998 b1580 b4 b4
4029 B b1581 t1580
4030 T t1581 o b1581 b4
4031 B b1582 t1581
4032 T t1582 o b1579 b1582
4033 B b1583 t1582
4034 T t1583 o1508 b998 b1536 b1583 b4
4035 B b1584 t1583
4036 T t1584 o996 b1584
4037 B b1585 t1584
4038 P p1587 Number 9535
4039 P p2084 Number 9969
4040 O o2084 location p1587 p2084
4041 P p2085 Number 9562
4042 P p2086 Number 9570
4043 O o2086 resource_defs p2085 p2086 p204
4044 P p2087 Number 9568
4045 O o2087 uid p2087 p2086
4046 T t2087 o2087 b680
4047 B b2087 t2087
4048 T t2088 o b2087 b4
4049 B b2088 t2088
4050 T t2089 o2086 b2088
4051 B b2089 t2089
4052 T t2090 o b2089 b4
4053 B b2090 t2090
4054 T t2091 o1499 b665 b1508 b1585 b2090
4055 B b2091 t2091
4056 T t2092 o2084 b2091
4057 B b2092 t2092
4058 P p1594 String unique_sol1
4059 O o1594 rule p1594
4060 P p1595 Var a
4061 O o1595 var p1595
4062 T t1595 o1595
4063 B b1595 t1595
4064 T t1596 o689 b1595
4065 S s1596 t668 h
4066 G s1596 t1596
4067 B b1596 s1596
4068 T t1597 o666 b1596
4069 B b1597 t1597
4070 P p1597 Var b
4071 O o1597 var p1597
4072 T t1598 o1597
4073 B b1598 t1598
4074 T t1599 o689 b1598
4075 S s1599 t668 h
4076 G s1599 t1599
4077 B b1599 s1599
4078 T t1600 o666 b1599
4079 B b1600 t1600
4080 P p1600 Var x
4081 O o1600 var p1600
4082 T t1601 o1600
4083 B b1601 t1601
4084 T t1602 o689 b1601
4085 S s1602 t668 h
4086 G s1602 t1602
4087 B b1602 s1602
4088 T t1603 o666 b1602
4089 B b1603 t1603
4090 T t1604 o721 b1595 b570
4091 S s1604 t673 h
4092 G s1604 t1604
4093 B b1604 s1604
4094 T t1605 o666 b1604
4095 B b1605 t1605
4096 T t1606 o721 b1598 b570
4097 S s1606 t673 h
4098 G s1606 t1606
4099 B b1606 s1606
4100 T t1607 o666 b1606
4101 B b1607 t1607
4102 T t1608 o721 b1601 b570
4103 S s1608 t673 h
4104 G s1608 t1608
4105 B b1608 s1608
4106 T t1609 o666 b1608
4107 B b1609 t1609
4108 T t1610 o575 b564 b1595 b1601
4109 B b1610 t1610
4110 T t1611 o811 b1610 b1598
4111 S s1611 t673 h
4112 G s1611 t1611
4113 B b1611 s1611
4114 T t1612 o666 b1611
4115 B b1612 t1612
4116 T t1613 o588 b564 b1595
4117 B b1613 t1613
4118 T t1614 o575 b564 b1613 b1598
4119 B b1614 t1614
4120 T t1615 o811 b1601 b1614
4121 S s1615 t673 h
4122 G s1615 t1615
4123 B b1615 s1615
4124 T t1616 o666 b1615
4125 B b1616 t1616
4126 T t1617 o665 b1612 b1616
4127 B b1617 t1617
4128 T t1618 o665 b1609 b1617
4129 B b1618 t1618
4130 T t1619 o665 b1607 b1618
4131 B b1619 t1619
4132 T t1620 o665 b1605 b1619
4133 B b1620 t1620
4134 T t1621 o665 b689 b1620
4135 B b1621 t1621
4136 T t1622 o665 b671 b1621
4137 B b1622 t1622
4138 T t1623 o665 b1603 b1622
4139 B b1623 t1623
4140 T t1624 o665 b1600 b1623
4141 B b1624 t1624
4142 T t1625 o665 b1597 b1624
4143 B b1625 t1625
4144 P p1625 String "assumT 9 thenT assertT << equal{op{'g; inv{'g; 'a}; op{'g; 'a; 'x}}; op{'g; inv{'g; 'a}; 'b}} >> thenT autoT"
4145 O o1625 ext_rule p1625
4146 T t1626 o b1611 b4
4147 B b1626 t1626
4148 T t1627 o b1608 b1626
4149 B b1627 t1627
4150 T t1628 o b1606 b1627
4151 B b1628 t1628
4152 T t1629 o b1604 b1628
4153 B b1629 t1629
4154 T t1630 o b688 b1629
4155 B b1630 t1630
4156 T t1631 o b670 b1630
4157 B b1631 t1631
4158 T t1632 o b1602 b1631
4159 B b1632 t1632
4160 T t1633 o b1599 b1632
4161 B b1633 t1633
4162 T t1634 o b1596 b1633
4163 B b1634 t1634
4164 T t1635 o1001 b1615 b1634
4165 B b1635 t1635
4166 T t1636 o1000 b1635 b4 b1011
4167 B b1636 t1636
4168 H h1636 v t1611
4169 T t1637 o744 b1610 b1598
4170 S s1637 t673 h h1636
4171 G s1637 t1637
4172 B b1637 s1637
4173 T t1638 o1001 b1637 b1634
4174 B b1638 t1638
4175 T t1639 o575 b564 b1613 b1610
4176 B b1639 t1639
4177 T t1640 o744 b1639 b1614
4178 S s1640 t673 h h1636
4179 G s1640 t1640
4180 B b1640 s1640
4181 T t1641 o1001 b1640 b1634
4182 B b1641 t1641
4183 T t1642 o811 b1639 b1614
4184 S s1642 t673 h h1636
4185 G s1642 t1642
4186 B b1642 s1642
4187 T t1643 o1001 b1642 b1634
4188 B b1643 t1643
4189 S s1643 t673 h h1636
4190 G s1643 t1615
4191 B b1644 s1643
4192 T t1644 o1001 b1644 b1634
4193 B b1645 t1644
4194 T t1645 o2 b1636
4195 B b1646 t1645
4196 T t1646 o1000 b1645 b4 b1646
4197 B b1647 t1646
4198 T t1647 o2 b1647
4199 B b1648 t1647
4200 T t1648 o1012 b1643 b1460 b1648
4201 B b1649 t1648
4202 T t1649 o2 b1649
4203 B b1650 t1649
4204 T t1650 o1012 b1641 b1460 b1650
4205 B b1651 t1650
4206 T t1651 o2 b1651
4207 B b1652 t1651
4208 T t1652 o1012 b1638 b4 b1652
4209 B b1653 t1652
4210 H h1653 v_1 t1642
4211 T t1653 o744 b1601 b1614
4212 S s1653 t673 h h1636 h1653
4213 G s1653 t1653
4214 B b1654 s1653
4215 T t1654 o1001 b1654 b1634
4216 B b1655 t1654
4217 S s1655 t673 h h1636 h1653
4218 G s1655 t1615
4219 B b1656 s1655
4220 T t1656 o1001 b1656 b1634
4221 B b1657 t1656
4222 T t1657 o1000 b1657 b1460 b1648
4223 B b1658 t1657
4224 T t1658 o2 b1658
4225 B b1659 t1658
4226 T t1659 o1000 b1655 b4 b1659
4227 B b1660 t1659
4228 T t1660 o b1660 b4
4229 B b1661 t1660
4230 T t1661 o b1653 b1661
4231 B b1662 t1661
4232 T t1662 o999 b1636 b1662
4233 B b1663 t1662
4234 P p1663 String "rwh unfold_equal 2 thenT autoT"
4235 O o1663 ext_rule p1663
4236 T t1663 o999 b1653 b4
4237 B b1664 t1663
4238 T t1664 o1663 b998 b1664 b4 b4
4239 B b1665 t1664
4240 P p1665 String "setSubstT << equal{op{'g; inv{'g; 'a}; op{'g; 'a; 'x}}; op{'g; op{'g; inv{'g; 'a}; 'a}; 'x}} >> 3 thenT autoT"
4241 O o1665 ext_rule p1665
4242 T t1665 o575 b564 b1613 b1595
4243 B b1666 t1665
4244 T t1666 o575 b564 b1666 b1601
4245 B b1667 t1666
4246 T t1667 o811 b1667 b1614
4247 H h1667 v_2 t1667
4248 S s1667 t673 h h1636 h1653 h1667
4249 G s1667 t1653
4250 B b1668 s1667
4251 T t1668 o1001 b1668 b1634
4252 B b1669 t1668
4253 T t1669 o2 b1660
4254 B b1670 t1669
4255 T t1670 o1000 b1669 b4 b1670
4256 B b1671 t1670
4257 T t1671 o b1671 b4
4258 B b1672 t1671
4259 T t1672 o999 b1660 b1672
4260 B b1673 t1672
4261 P p1673 String "setSubstT << equal{op{'g; inv{'g; 'a}; 'a}; id{'g}} >> 4 thenT autoT"
4262 O o1673 ext_rule p1673
4263 T t1673 o575 b564 b583 b1601
4264 B b1674 t1673
4265 T t1674 o811 b1674 b1614
4266 H h1674 v_3 t1674
4267 S s1674 t673 h h1636 h1653 h1667 h1674
4268 G s1674 t1653
4269 B b1675 s1674
4270 T t1675 o1001 b1675 b1634
4271 B b1676 t1675
4272 T t1676 o2 b1671
4273 B b1677 t1676
4274 T t1677 o1000 b1676 b4 b1677
4275 B b1678 t1677
4276 T t1678 o b1678 b4
4277 B b1679 t1678
4278 T t1679 o999 b1671 b1679
4279 B b1680 t1679
4280 P p1680 String "setSubstT << equal{op{'g; id{'g}; 'x}; 'x} >> 5 thenT autoT"
4281 O o1680 ext_rule p1680
4282 H h1680 v_4 t1615
4283 S s1680 t673 h h1636 h1653 h1667 h1674 h1680
4284 G s1680 t1653
4285 B b1681 s1680
4286 T t1681 o1001 b1681 b1634
4287 B b1682 t1681
4288 T t1682 o2 b1678
4289 B b1683 t1682
4290 T t1683 o1000 b1682 b4 b1683
4291 B b1684 t1683
4292 T t1684 o b1684 b4
4293 B b1685 t1684
4294 T t1685 o999 b1678 b1685
4295 B b1686 t1685
4296 P p1686 String "rwh unfold_equal 6 thenT autoT"
4297 O o1686 ext_rule p1686
4298 T t1686 o999 b1684 b4
4299 B b1687 t1686
4300 T t1687 o1686 b998 b1687 b4 b4
4301 B b1688 t1687
4302 T t1688 o b1688 b4
4303 B b1689 t1688
4304 T t1689 o1680 b998 b1686 b1689 b4
4305 B b1690 t1689
4306 T t1690 o b1690 b4
4307 B b1691 t1690
4308 T t1691 o1673 b998 b1680 b1691 b4
4309 B b1692 t1691
4310 T t1692 o b1692 b4
4311 B b1693 t1692
4312 T t1693 o1665 b998 b1673 b1693 b4
4313 B b1694 t1693
4314 T t1694 o b1694 b4
4315 B b1695 t1694
4316 T t1695 o b1665 b1695
4317 B b1696 t1695
4318 T t1696 o1625 b998 b1663 b1696 b4
4319 B b1697 t1696
4320 T t1697 o996 b1697
4321 B b1698 t1697
4322 P p1700 Number 10020
4323 P p2092 Number 10551
4324 O o2092 location p1700 p2092
4325 P p2093 Number 10047
4326 P p2094 Number 10055
4327 O o2094 resource_defs p2093 p2094 p204
4328 P p2095 Number 10053
4329 O o2095 uid p2095 p2094
4330 T t2095 o2095 b680
4331 B b2095 t2095
4332 T t2096 o b2095 b4
4333 B b2096 t2096
4334 T t2097 o2094 b2096
4335 B b2097 t2097
4336 T t2098 o b2097 b4
4337 B b2098 t2098
4338 T t2099 o1594 b665 b1625 b1698 b2098
4339 B b2099 t2099
4340 T t2100 o2092 b2099
4341 B b2100 t2100
4342 O o1705 location p p
4343 P p1705 String unique_sol2
4344 O o1706 rule p1705
4345 P p1706 Var y
4346 O o1707 var p1706
4347 T t1707 o1707
4348 B b1707 t1707
4349 T t1708 o689 b1707
4350 S s1708 t668 h
4351 G s1708 t1708
4352 B b1708 s1708
4353 T t1709 o666 b1708
4354 B b1709 t1709
4355 T t1710 o721 b1707 b570
4356 S s1710 t673 h
4357 G s1710 t1710
4358 B b1710 s1710
4359 T t1711 o666 b1710
4360 B b1711 t1711
4361 T t1712 o575 b564 b1707 b1595
4362 B b1712 t1712
4363 T t1713 o811 b1712 b1598
4364 S s1713 t673 h
4365 G s1713 t1713
4366 B b1713 s1713
4367 T t1714 o666 b1713
4368 B b1714 t1714
4369 T t1715 o575 b564 b1598 b1613
4370 B b1715 t1715
4371 T t1716 o811 b1707 b1715
4372 S s1716 t673 h
4373 G s1716 t1716
4374 B b1716 s1716
4375 T t1717 o666 b1716
4376 B b1717 t1717
4377 T t1718 o665 b1714 b1717
4378 B b1718 t1718
4379 T t1719 o665 b1711 b1718
4380 B b1719 t1719
4381 T t1720 o665 b1607 b1719
4382 B b1720 t1720
4383 T t1721 o665 b1605 b1720
4384 B b1721 t1721
4385 T t1722 o665 b689 b1721
4386 B b1722 t1722
4387 T t1723 o665 b671 b1722
4388 B b1723 t1723
4389 T t1724 o665 b1709 b1723
4390 B b1724 t1724
4391 T t1725 o665 b1600 b1724
4392 B b1725 t1725
4393 T t1726 o665 b1597 b1725
4394 B b1726 t1726
4395 P p1726 String "assumT 9 thenT assertT << equal{op{'g; op{'g; 'y; 'a}; inv{'g; 'a}}; op{'g; 'b; inv{'g; 'a}}} >> thenT autoT"
4396 O o1726 ext_rule p1726
4397 T t1727 o b1713 b4
4398 B b1727 t1727
4399 T t1728 o b1710 b1727
4400 B b1728 t1728
4401 T t1729 o b1606 b1728
4402 B b1729 t1729
4403 T t1730 o b1604 b1729
4404 B b1730 t1730
4405 T t1731 o b688 b1730
4406 B b1731 t1731
4407 T t1732 o b670 b1731
4408 B b1732 t1732
4409 T t1733 o b1708 b1732
4410 B b1733 t1733
4411 T t1734 o b1599 b1733
4412 B b1734 t1734
4413 T t1735 o b1596 b1734
4414 B b1735 t1735
4415 T t1736 o1001 b1716 b1735
4416 B b1736 t1736
4417 T t1737 o1000 b1736 b4 b1011
4418 B b1737 t1737
4419 H h1737 v t1713
4420 T t1738 o744 b1712 b1598
4421 S s1738 t673 h h1737
4422 G s1738 t1738
4423 B b1738 s1738
4424 T t1739 o1001 b1738 b1735
4425 B b1739 t1739
4426 T t1740 o575 b564 b1712 b1613
4427 B b1740 t1740
4428 T t1741 o744 b1740 b1715
4429 S s1741 t673 h h1737
4430 G s1741 t1741
4431 B b1741 s1741
4432 T t1742 o1001 b1741 b1735
4433 B b1742 t1742
4434 T t1743 o811 b1740 b1715
4435 S s1743 t673 h h1737
4436 G s1743 t1743
4437 B b1743 s1743
4438 T t1744 o1001 b1743 b1735
4439 B b1744 t1744
4440 S s1744 t673 h h1737
4441 G s1744 t1716
4442 B b1745 s1744
4443 T t1745 o1001 b1745 b1735
4444 B b1746 t1745
4445 T t1746 o2 b1737
4446 B b1747 t1746
4447 T t1747 o1000 b1746 b4 b1747
4448 B b1748 t1747
4449 T t1748 o2 b1748
4450 B b1749 t1748
4451 T t1749 o1012 b1744 b1460 b1749
4452 B b1750 t1749
4453 T t1750 o2 b1750
4454 B b1751 t1750
4455 T t1751 o1012 b1742 b1460 b1751
4456 B b1752 t1751
4457 T t1752 o2 b1752
4458 B b1753 t1752
4459 T t1753 o1012 b1739 b4 b1753
4460 B b1754 t1753
4461 H h1754 v_1 t1743
4462 T t1754 o744 b1707 b1715
4463 S s1754 t673 h h1737 h1754
4464 G s1754 t1754
4465 B b1755 s1754
4466 T t1755 o1001 b1755 b1735
4467 B b1756 t1755
4468 S s1756 t673 h h1737 h1754
4469 G s1756 t1716
4470 B b1757 s1756
4471 T t1757 o1001 b1757 b1735
4472 B b1758 t1757
4473 T t1758 o1000 b1758 b1460 b1749
4474 B b1759 t1758
4475 T t1759 o2 b1759
4476 B b1760 t1759
4477 T t1760 o1000 b1756 b4 b1760
4478 B b1761 t1760
4479 T t1761 o b1761 b4
4480 B b1762 t1761
4481 T t1762 o b1754 b1762
4482 B b1763 t1762
4483 T t1763 o999 b1737 b1763
4484 B b1764 t1763
4485 T t1764 o999 b1754 b4
4486 B b1765 t1764
4487 T t1765 o1663 b998 b1765 b4 b4
4488 B b1766 t1765
4489 P p1766 String "setSubstT << equal{op{'g; op{'g; 'y; 'a}; inv{'g; 'a}}; op{'g; 'y; op{'g; 'a; inv{'g; 'a}}}} >> 3 thenT autoT"
4490 O o1766 ext_rule p1766
4491 T t1766 o575 b564 b1595 b1613
4492 B b1767 t1766
4493 T t1767 o575 b564 b1707 b1767
4494 B b1768 t1767
4495 T t1768 o811 b1768 b1715
4496 H h1768 v_2 t1768
4497 S s1768 t673 h h1737 h1754 h1768
4498 G s1768 t1754
4499 B b1769 s1768
4500 T t1769 o1001 b1769 b1735
4501 B b1770 t1769
4502 T t1770 o2 b1761
4503 B b1771 t1770
4504 T t1771 o1000 b1770 b4 b1771
4505 B b1772 t1771
4506 T t1772 o b1772 b4
4507 B b1773 t1772
4508 T t1773 o999 b1761 b1773
4509 B b1774 t1773
4510 P p1774 String "setSubstT << equal{op{'g; 'a; inv{'g; 'a}}; id{'g}} >> 4 thenT autoT"
4511 O o1774 ext_rule p1774
4512 T t1774 o575 b564 b1707 b583
4513 B b1775 t1774
4514 T t1775 o811 b1775 b1715
4515 H h1775 v_3 t1775
4516 S s1775 t673 h h1737 h1754 h1768 h1775
4517 G s1775 t1754
4518 B b1776 s1775
4519 T t1776 o1001 b1776 b1735
4520 B b1777 t1776
4521 T t1777 o2 b1772
4522 B b1778 t1777
4523 T t1778 o1000 b1777 b4 b1778
4524 B b1779 t1778
4525 T t1779 o b1779 b4
4526 B b1780 t1779
4527 T t1780 o999 b1772 b1780
4528 B b1781 t1780
4529 P p1781 String "setSubstT << equal{op{'g; 'y; id{'g}}; 'y}>> 5 thenT autoT"
4530 O o1781 ext_rule p1781
4531 H h1781 v_4 t1716
4532 S s1781 t673 h h1737 h1754 h1768 h1775 h1781
4533 G s1781 t1754
4534 B b1782 s1781
4535 T t1782 o1001 b1782 b1735
4536 B b1783 t1782
4537 T t1783 o2 b1779
4538 B b1784 t1783
4539 T t1784 o1000 b1783 b4 b1784
4540 B b1785 t1784
4541 T t1785 o b1785 b4
4542 B b1786 t1785
4543 T t1786 o999 b1779 b1786
4544 B b1787 t1786
4545 T t1787 o999 b1785 b4
4546 B b1788 t1787
4547 T t1788 o1686 b998 b1788 b4 b4
4548 B b1789 t1788
4549 T t1789 o b1789 b4
4550 B b1790 t1789
4551 T t1790 o1781 b998 b1787 b1790 b4
4552 B b1791 t1790
4553 T t1791 o b1791 b4
4554 B b1792 t1791
4555 T t1792 o1774 b998 b1781 b1792 b4
4556 B b1793 t1792
4557 T t1793 o b1793 b4
4558 B b1794 t1793
4559 T t1794 o1766 b998 b1774 b1794 b4
4560 B b1795 t1794
4561 T t1795 o b1795 b4
4562 B b1796 t1795
4563 T t1796 o b1766 b1796
4564 B b1797 t1796
4565 T t1797 o1726 b998 b1764 b1797 b4
4566 B b1798 t1797
4567 T t1798 o996 b1798
4568 B b1799 t1798
4569 P p1801 Number 10602
4570 P p2100 Number 11133
4571 O o2100 location p1801 p2100
4572 P p2101 Number 10629
4573 P p2102 Number 10637
4574 O o2102 resource_defs p2101 p2102 p204
4575 P p2103 Number 10635
4576 O o2103 uid p2103 p2102
4577 T t2103 o2103 b680
4578 B b2103 t2103
4579 T t2104 o b2103 b4
4580 B b2104 t2104
4581 T t2105 o2102 b2104
4582 B b2105 t2105
4583 T t2106 o b2105 b4
4584 B b2106 t2106
4585 T t2107 o1706 b665 b1726 b1799 b2106
4586 B b2107 t2107
4587 T t2108 o2100 b2107
4588 B b2108 t2108
4589 P p2108 Number 11161
4590 P p2109 Number 11572
4591 O o2109 location p2108 p2109
4592 P p1806 String inv_simplify
4593 O o1806 rule p1806
4594 T t1807 o575 b564 b1595 b1598
4595 B b1807 t1807
4596 T t1808 o588 b564 b1807
4597 B b1808 t1808
4598 T t1809 o588 b564 b1598
4599 B b1809 t1809
4600 T t1810 o575 b564 b1809 b1613
4601 B b1810 t1810
4602 T t1811 o811 b1808 b1810
4603 S s1811 t673 h
4604 G s1811 t1811
4605 B b1811 s1811
4606 T t1812 o666 b1811
4607 B b1812 t1812
4608 T t1813 o665 b1607 b1812
4609 B b1813 t1813
4610 T t1814 o665 b1605 b1813
4611 B b1814 t1814
4612 T t1815 o665 b689 b1814
4613 B b1815 t1815
4614 T t1816 o665 b671 b1815
4615 B b1816 t1816
4616 T t1817 o665 b1600 b1816
4617 B b1817 t1817
4618 T t1818 o665 b1597 b1817
4619 B b1818 t1818
4620 P p1818 String "assertT << equal{op{'g; inv{'g; op{'g; 'a; 'b}}; op{'g; 'a; 'b}}; op{'g; op{'g; inv{'g; 'b}; inv{'g; 'a}}; op{'g; 'a; 'b}}} >>"
4621 O o1818 ext_rule p1818
4622 T t1819 o b1606 b4
4623 B b1819 t1819
4624 T t1820 o b1604 b1819
4625 B b1820 t1820
4626 T t1821 o b688 b1820
4627 B b1821 t1821
4628 T t1822 o b670 b1821
4629 B b1822 t1822
4630 T t1823 o b1599 b1822
4631 B b1823 t1823
4632 T t1824 o b1596 b1823
4633 B b1824 t1824
4634 T t1825 o1001 b1811 b1824
4635 B b1825 t1825
4636 T t1826 o1000 b1825 b4 b1011
4637 B b1826 t1826
4638 T t1827 o575 b564 b1808 b1807
4639 B b1827 t1827
4640 T t1828 o575 b564 b1810 b1807
4641 B b1828 t1828
4642 T t1829 o811 b1827 b1828
4643 S s1829 t673 h
4644 G s1829 t1829
4645 B b1829 s1829
4646 T t1830 o1001 b1829 b1824
4647 B b1830 t1830
4648 T t1831 o2 b1826
4649 B b1831 t1831
4650 T t1832 o1012 b1830 b4 b1831
4651 B b1832 t1832
4652 H h1832 v t1829
4653 S s1832 t673 h h1832
4654 G s1832 t1811
4655 B b1833 s1832
4656 T t1833 o1001 b1833 b1824
4657 B b1834 t1833
4658 T t1834 o1000 b1834 b4 b1831
4659 B b1835 t1834
4660 T t1835 o b1835 b4
4661 B b1836 t1835
4662 T t1836 o b1832 b1836
4663 B b1837 t1836
4664 T t1837 o999 b1826 b1837
4665 B b1838 t1837
4666 P p1838 String "setSubstT << equal{op{'g; inv{'g; op{'g; 'a; 'b}}; op{'g; 'a; 'b}}; id{'g}} >> 0 thenAT autoT"
4667 O o1838 ext_rule p1838
4668 T t1838 o811 b583 b1828
4669 S s1838 t673 h
4670 G s1838 t1838
4671 B b1839 s1838
4672 T t1839 o1001 b1839 b1824
4673 B b1840 t1839
4674 T t1840 o2 b1832
4675 B b1841 t1840
4676 T t1841 o1000 b1840 b4 b1841
4677 B b1842 t1841
4678 T t1842 o b1842 b4
4679 B b1843 t1842
4680 T t1843 o999 b1832 b1843
4681 B b1844 t1843
4682 P p1844 String "setSubstT << equal{op{'g; op{'g; inv{'g; 'b}; inv{'g; 'a}}; op{'g; 'a; 'b}}; op{'g; inv{'g; 'b}; op{'g; inv{'g; 'a}; op{'g; 'a; 'b}}}} >> 0 thenT autoT"
4683 O o1844 ext_rule p1844
4684 T t1844 o575 b564 b1598 b583
4685 B b1845 t1844
4686 T t1845 o744 b1845 b1598
4687 S s1845 t673 h
4688 G s1845 t1845
4689 B b1846 s1845
4690 T t1846 o1001 b1846 b1824
4691 B b1847 t1846
4692 T t1847 o575 b564 b1595 b1845
4693 B b1848 t1847
4694 T t1848 o744 b1848 b1807
4695 S s1848 t673 h
4696 G s1848 t1848
4697 B b1849 s1848
4698 T t1849 o1001 b1849 b1824
4699 B b1850 t1849
4700 T t1850 o811 b1848 b1807
4701 S s1850 t673 h
4702 G s1850 t1850
4703 B b1851 s1850
4704 T t1851 o1001 b1851 b1824
4705 B b1852 t1851
4706 T t1852 o575 b564 b1613 b1807
4707 B b1853 t1852
4708 T t1853 o811 b1845 b1853
4709 S s1853 t673 h
4710 G s1853 t1853
4711 B b1854 s1853
4712 T t1854 o1001 b1854 b1824
4713 B b1855 t1854
4714 T t1855 o575 b564 b1809 b1853
4715 B b1856 t1855
4716 T t1856 o811 b583 b1856
4717 S s1856 t673 h
4718 G s1856 t1856
4719 B b1857 s1856
4720 T t1857 o1001 b1857 b1824
4721 B b1858 t1857
4722 T t1858 o2 b1842
4723 B b1859 t1858
4724 T t1859 o1000 b1858 b1460 b1859
4725 B b1860 t1859
4726 T t1860 o2 b1860
4727 B b1861 t1860
4728 T t1861 o1000 b1855 b1460 b1861
4729 B b1862 t1861
4730 T t1862 o2 b1862
4731 B b1863 t1862
4732 T t1863 o1000 b1852 b1460 b1863
4733 B b1864 t1863
4734 T t1864 o2 b1864
4735 B b1865 t1864
4736 T t1865 o1000 b1850 b1460 b1865
4737 B b1866 t1865
4738 T t1866 o2 b1866
4739 B b1867 t1866
4740 T t1867 o1000 b1847 b4 b1867
4741 B b1868 t1867
4742 T t1868 o b1868 b4
4743 B b1869 t1868
4744 T t1869 o999 b1842 b1869
4745 B b1870 t1869
4746 P p1870 String "setSubstT << equal{op{'g; 'b; id{'g}}; 'b} >> 0 thenT autoT"
4747 O o1870 ext_rule p1870
4748 T t1870 o999 b1868 b4
4749 B b1871 t1870
4750 T t1871 o1870 b998 b1871 b4 b4
4751 B b1872 t1871
4752 T t1872 o b1872 b4
4753 B b1873 t1872
4754 T t1873 o1844 b998 b1870 b1873 b4
4755 B b1874 t1873
4756 T t1874 o b1874 b4
4757 B b1875 t1874
4758 T t1875 o1838 b998 b1844 b1875 b4
4759 B b1876 t1875
4760 P p1876 String "groupCancelRightT << 'g >> << op{'g; 'a; 'b} >> thenT autoT"
4761 O o1876 ext_rule p1876
4762 T t1876 o999 b1835 b4
4763 B b1877 t1876
4764 T t1877 o1876 b998 b1877 b4 b4
4765 B b1878 t1877
4766 T t1878 o b1878 b4
4767 B b1879 t1878
4768 T t1879 o b1876 b1879
4769 B b1880 t1879
4770 T t1880 o1818 b998 b1838 b1880 b4
4771 B b1881 t1880
4772 T t1881 o996 b1881
4773 B b1882 t1881
4774 P p2110 Number 11189
4775 P p2111 Number 11197
4776 O o2111 resource_defs p2110 p2111 p204
4777 P p2112 Number 11195
4778 O o2112 uid p2112 p2111
4779 T t2112 o2112 b680
4780 B b2112 t2112
4781 T t2113 o b2112 b4
4782 B b2113 t2113
4783 T t2114 o2111 b2113
4784 B b2114 t2114
4785 T t2115 o b2114 b4
4786 B b2115 t2115
4787 T t2116 o1806 b665 b1818 b1882 b2115
4788 B b2116 t2116
4789 T t2117 o2109 b2116
4790 B b2117 t2117
4791 P p1889 String inv_of_id
4792 O o1889 rule p1889
4793 T t1890 o588 b564 b583
4794 B b1890 t1890
4795 T t1891 o744 b1890 b583
4796 S s1891 t673 h
4797 G s1891 t1891
4798 B b1891 s1891
4799 T t1892 o666 b1891
4800 B b1892 t1892
4801 T t1893 o665 b689 b1892
4802 B b1893 t1893
4803 T t1894 o665 b671 b1893
4804 B b1894 t1894
4805 P p1894 String "assertT << equal{id{'g}; inv{'g; id{'g}}} >> thenAT autoT"
4806 O o1894 ext_rule p1894
4807 T t1895 o b688 b4
4808 B b1895 t1895
4809 T t1896 o b670 b1895
4810 B b1896 t1896
4811 T t1897 o1001 b1891 b1896
4812 B b1897 t1897
4813 T t1898 o1000 b1897 b4 b1011
4814 B b1898 t1898
4815 T t1899 o811 b583 b1890
4816 H h1899 v t1899
4817 S s1899 t673 h h1899
4818 G s1899 t1891
4819 B b1899 s1899
4820 T t1900 o1001 b1899 b1896
4821 B b1900 t1900
4822 T t1901 o2 b1898
4823 B b1901 t1901
4824 T t1902 o1000 b1900 b4 b1901
4825 B b1902 t1902
4826 T t1903 o b1902 b4
4827 B b1903 t1903
4828 T t1904 o999 b1898 b1903
4829 B b1904 t1904
4830 P p1904 String "rwh unfold_equal 2 thenT eqSetSymT thenT autoT"
4831 O o1904 ext_rule p1904
4832 T t1905 o999 b1902 b4
4833 B b1905 t1905
4834 T t1906 o1904 b998 b1905 b4 b4
4835 B b1906 t1906
4836 T t1907 o b1906 b4
4837 B b1907 t1907
4838 T t1908 o1894 b998 b1904 b1907 b4
4839 B b1908 t1908
4840 T t1909 o996 b1908
4841 B b1909 t1909
4842 P p1910 Number 11594
4843 P p2117 Number 11779
4844 O o2117 location p1910 p2117
4845 P p2118 Number 11619
4846 P p2119 Number 11627
4847 O o2119 resource_defs p2118 p2119 p204
4848 P p2120 Number 11625
4849 O o2120 uid p2120 p2119
4850 T t2120 o2120 b680
4851 B b2120 t2120
4852 T t2121 o b2120 b4
4853 B b2121 t2121
4854 T t2122 o2119 b2121
4855 B b2122 t2122
4856 T t2123 o b2122 b4
4857 B b2123 t2123
4858 T t2124 o1889 b665 b1894 b1909 b2123
4859 B b2124 t2124
4860 T t2125 o2117 b2124
4861 B b2125 t2125
4862 NSummary!id id1916 id Summary
4863 P p1916 Number 646427455
4864 O o1916 id1916 p1916
4865 T t1917 o1916
4866 B b1917 t1917
4867 T t1918 o1705 b1917
4868 B b1918 t1918
4869 T t1919 o b1918 b4
4870 B b1919 t1919
4871 T t2126 o b2125 b1919
4872 B b2126 t2126
4873 T t2127 o b2117 b2126
4874 B b2127 t2127
4875 T t2128 o b2108 b2127
4876 B b2128 t2128
4877 T t2129 o b2100 b2128
4878 B b2129 t2129
4879 T t2130 o b2092 b2129
4880 B b2130 t2130
4881 T t2131 o b2084 b2130
4882 B b2131 t2131
4883 T t2132 o b2076 b2131
4884 B b2132 t2132
4885 T t2133 o b2067 b2132
4886 B b2133 t2133
4887 T t2134 o b2058 b2133
4888 B b2134 t2134
4889 T t2135 o b2049 b2134
4890 B b2135 t2135
4891 T t2136 o b2002 b2135
4892 B b2136 t2136
4893 T t2137 o b1240 b2136
4894 B b2137 t2137
4895 T t2138 o b1192 b2137
4896 B b2138 t2138
4897 T t2139 o b1171 b2138
4898 B b2139 t2139
4899 T t2140 o b970 b2139
4900 B b2140 t2140
4901 T t2141 o b920 b2140
4902 B b2141 t2141
4903 T t2142 o b873 b2141
4904 B b2142 t2142
4905 T t2143 o b831 b2142
4906 B b2143 t2143
4907 T t2144 o b775 b2143
4908 B b2144 t2144
4909 T t2145 o b712 b2144
4910 B b2145 t2145
4911 T t2146 o b663 b2145
4912 B b2146 t2146
4913 T t2147 o b627 b2146
4914 B b2147 t2147
4915 T t2148 o b598 b2147
4916 B b2148 t2148
4917 T t2149 o b573 b2148
4918 B b2149 t2149
4919 T t2150 o b555 b2149
4920 B b2150 t2150
4921 T t2151 o b534 b2150
4922 B b2151 t2151
4923 T t2152 o b503 b2151
4924 B b2152 t2152
4925 T t2153 o b480 b2152
4926 B b2153 t2153
4927 T t2154 o b453 b2153
4928 B b2154 t2154
4929 T t2155 o b426 b2154
4930 B b2155 t2155
4931 T t2156 o b401 b2155
4932 B b2156 t2156
4933 T t2157 o b280 b2156
4934 B b2157 t2157
4935 T t2158 o b240 b2157
4936 B b2158 t2158
4937 T t2159 o b229 b2158
4938 B b2159 t2159
4939 T t2160 o b210 b2159
4940 B b2160 t2160
4941 T t2161 o b191 b2160
4942 B b2161 t2161
4943 T t2162 o b177 b2161
4944 B b2162 t2162
4945 T t2163 o b169 b2162
4946 B b2163 t2163
4947 T t2164 o b155 b2163
4948 B b2164 t2164
4949 T t2165 o b597 b2164
4950 B b2165 t2165
4951 T t2166 o b592 b2165
4952 B b2166 t2166
4953 T t2167 o b585 b2166
4954 B b2167 t2167
4955 T t2168 o b580 b2167
4956 B b2168 t2168
4957 T t2169 o b572 b2168
4958 B b2169 t2169
4959 T t2170 o b567 b2169
4960 B b2170 t2170
4961 T t2171 o b560 b2170
4962 B b2171 t2171
4963 T t2172 o b553 b2171
4964 B b2172 t2172
4965 T t2173 o b546 b2172
4966 B b2173 t2173
4967 T t2174 o b539 b2173
4968 B b2174 t2174
4969 T t2175 o b532 b2174
4970 B b2175 t2175
4971 T t2176 o b524 b2175
4972 B b2176 t2176
4973 T t2177 o b516 b2176
4974 B b2177 t2177
4975 T t2178 o b508 b2177
4976 B b2178 t2178
4977 T t2179 o b501 b2178
4978 B b2179 t2179
4979 T t2180 o b494 b2179
4980 B b2180 t2180
4981 T t2181 o b487 b2180
4982 B b2181 t2181
4983 T t2182 o b478 b2181
4984 B b2182 t2182
4985 T t2183 o b469 b2182
4986 B b2183 t2183
4987 T t2184 o b460 b2183
4988 B b2184 t2184
4989 T t2185 o b451 b2184
4990 B b2185 t2185
4991 T t2186 o b442 b2185
4992 B b2186 t2186
4993 T t2187 o b433 b2186
4994 B b2187 t2187
4995 T t2188 o b424 b2187
4996 B b2188 t2188
4997 T t2189 o b414 b2188
4998 B b2189 t2189
4999 T t2190 o b407 b2189
5000 B b2190 t2190
5001 T t2191 o b399 b2190
5002 B b2191 t2191
5003 T t2192 o b393 b2191
5004 B b2192 t2192
5005 T t2193 o b378 b2192
5006 B b2193 t2193
5007 T t2194 o b376 b2193
5008 B b2194 t2194
5009 T t2195 o b367 b2194
5010 B b2195 t2195
5011 T t2196 o b298 b2195

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26