/[mojave]/metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
ViewVC logotype

Contents of /metaprl/theories/czf/czf_itt_cyclic_subgroup.prla

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3570 - (show annotations) (download)
Tue Apr 9 05:59:41 2002 UTC (19 years, 3 months ago) by xiny
File size: 258597 byte(s)
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. They look much cleaner now.
Also updated related rules and their proofs.

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 21
9 O o1 location p p1
10 NSummary!parent parent parent Summary
11 O o2 parent
12 P p2 String Czf_itt_group
13 O o3 parent p2
14 T t o3
15 B b t
16 NPerv!nil nil3 nil Perv
17 O o4 nil3
18 T t4 o4
19 B b4 t4
20 T t5 o b b4
21 B b5 t5
22 P p5 String Czf_itt_and
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 Czf_itt_dall
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 Czf_itt_set_ind
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 Czf_itt_all
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 Czf_itt_sep
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 Czf_itt_member
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 Czf_itt_eq
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 Czf_itt_set
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 Czf_itt_comment
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_theory
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_fset
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_prop_decide
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_derive
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_list2
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_list
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_quotient
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_esquash
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_srec
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_prec
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_w
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_bunion
143 O o45 parent p45
144 T t46 o45
145 B b46 t46
146 T t47 o b46 b4
147 B b47 t47
148 P p47 String Itt_bisect
149 O o47 parent p47
150 T t48 o47
151 B b48 t48
152 T t49 o b48 b4
153 B b49 t49
154 P p49 String Itt_tunion
155 O o49 parent p49
156 T t50 o49
157 B b50 t50
158 T t51 o b50 b4
159 B b51 t51
160 P p51 String Itt_isect
161 O o51 parent p51
162 T t52 o51
163 B b52 t52
164 T t53 o b52 b4
165 B b53 t53
166 P p53 String Itt_struct2
167 O o53 parent p53
168 T t54 o53
169 B b54 t54
170 T t55 o b54 b4
171 B b55 t55
172 P p55 String Itt_well_founded
173 O o55 parent p55
174 T t56 o55
175 B b56 t56
176 T t57 o b56 b4
177 B b57 t57
178 P p57 String Itt_int_arith
179 O o57 parent p57
180 T t58 o57
181 B b58 t58
182 T t59 o b58 b4
183 B b59 t59
184 P p59 String Itt_atom_bool
185 O o59 parent p59
186 T t60 o59
187 B b60 t60
188 T t61 o b60 b4
189 B b61 t61
190 P p61 String Itt_atom
191 O o61 parent p61
192 T t62 o61
193 B b62 t62
194 T t63 o b62 b4
195 B b63 t63
196 P p63 String Itt_record_label0
197 O o63 parent p63
198 T t64 o63
199 B b64 t64
200 T t65 o b64 b4
201 B b65 t65
202 P p65 String Itt_nat
203 O o65 parent p65
204 T t66 o65
205 B b66 t66
206 T t67 o b66 b4
207 B b67 t67
208 P p67 String Itt_int_ext
209 O o67 parent p67
210 T t68 o67
211 B b68 t68
212 T t69 o b68 b4
213 B b69 t69
214 P p69 String Itt_int_base
215 O o69 parent p69
216 T t70 o69
217 B b70 t70
218 T t71 o b70 b4
219 B b71 t71
220 P p71 String Itt_bool
221 O o71 parent p71
222 T t72 o71
223 B b72 t72
224 T t73 o b72 b4
225 B b73 t73
226 P p73 String Itt_decidable
227 O o73 parent p73
228 T t74 o73
229 B b74 t74
230 T t75 o b74 b4
231 B b75 t75
232 P p75 String Itt_logic
233 O o75 parent p75
234 T t76 o75
235 B b76 t76
236 T t77 o b76 b4
237 B b77 t77
238 P p77 String Itt_union
239 O o77 parent p77
240 T t78 o77
241 B b78 t78
242 T t79 o b78 b4
243 B b79 t79
244 P p79 String Itt_prod
245 O o79 parent p79
246 T t80 o79
247 B b80 t80
248 T t81 o b80 b4
249 B b81 t81
250 P p81 String Itt_dprod
251 O o81 parent p81
252 T t82 o81
253 B b82 t82
254 T t83 o b82 b4
255 B b83 t83
256 P p83 String Itt_fun
257 O o83 parent p83
258 T t84 o83
259 B b84 t84
260 T t85 o b84 b4
261 B b85 t85
262 P p85 String Itt_dfun
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 Itt_rfun
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 Itt_void
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 Itt_set
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 Itt_unit
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 Itt_squiggle
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 Itt_subtype
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 Itt_squash
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 Itt_struct
311 O o101 parent p101
312 T t102 o101
313 B b102 t102
314 T t103 o b102 b4
315 B b103 t103
316 P p103 String Itt_equal
317 O o103 parent p103
318 T t104 o103
319 B b104 t104
320 T t105 o b104 b4
321 B b105 t105
322 P p105 String Itt_comment
323 O o105 parent p105
324 T t106 o105
325 B b106 t106
326 T t107 o b106 b4
327 B b107 t107
328 P p107 String Base_theory
329 O o107 parent p107
330 T t108 o107
331 B b108 t108
332 T t109 o b108 b4
333 B b109 t109
334 P p109 String Base_meta
335 O o109 parent p109
336 T t110 o109
337 B b110 t110
338 T t111 o b110 b4
339 B b111 t111
340 P p111 String Base_cache
341 O o111 parent p111
342 T t112 o111
343 B b112 t112
344 T t113 o b112 b4
345 B b113 t113
346 P p113 String Tactic_cache
347 O o113 parent p113
348 T t114 o113
349 B b114 t114
350 T t115 o b114 b4
351 B b115 t115
352 P p115 String Typeinf
353 O o115 parent p115
354 T t116 o115
355 B b116 t116
356 T t117 o b116 b4
357 B b117 t117
358 P p117 String Ocaml_df
359 O o117 parent p117
360 T t118 o117
361 B b118 t118
362 T t119 o b118 b4
363 B b119 t119
364 P p119 String Ocaml_str_df
365 O o119 parent p119
366 T t120 o119
367 B b120 t120
368 T t121 o b120 b4
369 B b121 t121
370 P p121 String Ocaml_sig_df
371 O o121 parent p121
372 T t122 o121
373 B b122 t122
374 T t123 o b122 b4
375 B b123 t123
376 P p123 String Ocaml_me_df
377 O o123 parent p123
378 T t124 o123
379 B b124 t124
380 T t125 o b124 b4
381 B b125 t125
382 P p125 String Ocaml_mt_df
383 O o125 parent p125
384 T t126 o125
385 B b126 t126
386 T t127 o b126 b4
387 B b127 t127
388 P p127 String Ocaml_type_df
389 O o127 parent p127
390 T t128 o127
391 B b128 t128
392 T t129 o b128 b4
393 B b129 t129
394 P p129 String Ocaml_patt_df
395 O o129 parent p129
396 T t130 o129
397 B b130 t130
398 T t131 o b130 b4
399 B b131 t131
400 P p131 String Ocaml_expr_df
401 O o131 parent p131
402 T t132 o131
403 B b132 t132
404 T t133 o b132 b4
405 B b133 t133
406 P p133 String Ocaml_base_df
407 O o133 parent p133
408 T t134 o133
409 B b134 t134
410 T t135 o b134 b4
411 B b135 t135
412 P p135 String Ocaml
413 O o135 parent p135
414 T t136 o135
415 B b136 t136
416 T t137 o b136 b4
417 B b137 t137
418 P p137 String Base_rewrite
419 O o137 parent p137
420 T t138 o137
421 B b138 t138
422 T t139 o b138 b4
423 B b139 t139
424 P p139 String Base_dtactic
425 O o139 parent p139
426 T t140 o139
427 B b140 t140
428 T t141 o b140 b4
429 B b141 t141
430 P p141 String Base_auto_tactic
431 O o141 parent p141
432 T t142 o141
433 B b142 t142
434 T t143 o b142 b4
435 B b143 t143
436 P p143 String Base_trivial
437 O o143 parent p143
438 T t144 o143
439 B b144 t144
440 T t145 o b144 b4
441 B b145 t145
442 P p145 String Top_conversionals
443 O o145 parent p145
444 T t146 o145
445 B b146 t146
446 T t147 o b146 b4
447 B b147 t147
448 P p147 String Top_tacticals
449 O o147 parent p147
450 T t148 o147
451 B b148 t148
452 T t149 o b148 b4
453 B b149 t149
454 P p149 String Var
455 O o149 parent p149
456 T t150 o149
457 B b150 t150
458 T t151 o b150 b4
459 B b151 t151
460 P p151 String Mptop
461 O o151 parent p151
462 T t152 o151
463 B b152 t152
464 T t153 o b152 b4
465 B b153 t153
466 P p153 String Summary
467 O o153 parent p153
468 T t154 o153
469 B b154 t154
470 T t155 o b154 b4
471 B b155 t155
472 P p155 String Comment
473 O o155 parent p155
474 T t156 o155
475 B b156 t156
476 T t157 o b156 b4
477 B b157 t157
478 P p157 String Base_dform
479 O o157 parent p157
480 T t158 o157
481 B b158 t158
482 T t159 o b158 b4
483 B b159 t159
484 P p159 String Nuprl_font
485 O o159 parent p159
486 T t160 o159
487 B b160 t160
488 T t161 o b160 b4
489 B b161 t161
490 P p161 String Perv
491 O o161 parent p161
492 T t162 o161
493 B b162 t162
494 T t163 o b162 b4
495 B b163 t163
496 T t164 o b163 b4
497 B b164 t164
498 T t165 o b161 b164
499 B b165 t165
500 T t166 o b159 b165
501 B b166 t166
502 T t167 o b157 b166
503 B b167 t167
504 T t168 o b155 b167
505 B b168 t168
506 T t169 o b153 b168
507 B b169 t169
508 T t170 o b151 b169
509 B b170 t170
510 T t171 o b149 b170
511 B b171 t171
512 T t172 o b147 b171
513 B b172 t172
514 T t173 o b145 b172
515 B b173 t173
516 T t174 o b143 b173
517 B b174 t174
518 T t175 o b141 b174
519 B b175 t175
520 T t176 o b139 b175
521 B b176 t176
522 T t177 o b137 b176
523 B b177 t177
524 T t178 o b135 b177
525 B b178 t178
526 T t179 o b133 b178
527 B b179 t179
528 T t180 o b131 b179
529 B b180 t180
530 T t181 o b129 b180
531 B b181 t181
532 T t182 o b127 b181
533 B b182 t182
534 T t183 o b125 b182
535 B b183 t183
536 T t184 o b123 b183
537 B b184 t184
538 T t185 o b121 b184
539 B b185 t185
540 T t186 o b119 b185
541 B b186 t186
542 T t187 o b117 b186
543 B b187 t187
544 T t188 o b115 b187
545 B b188 t188
546 T t189 o b113 b188
547 B b189 t189
548 T t190 o b111 b189
549 B b190 t190
550 T t191 o b109 b190
551 B b191 t191
552 T t192 o b107 b191
553 B b192 t192
554 T t193 o b105 b192
555 B b193 t193
556 T t194 o b103 b193
557 B b194 t194
558 T t195 o b101 b194
559 B b195 t195
560 T t196 o b99 b195
561 B b196 t196
562 T t197 o b97 b196
563 B b197 t197
564 T t198 o b95 b197
565 B b198 t198
566 T t199 o b93 b198
567 B b199 t199
568 T t200 o b91 b199
569 B b200 t200
570 T t201 o b89 b200
571 B b201 t201
572 T t202 o b87 b201
573 B b202 t202
574 T t203 o b85 b202
575 B b203 t203
576 T t204 o b83 b203
577 B b204 t204
578 T t205 o b81 b204
579 B b205 t205
580 T t206 o b79 b205
581 B b206 t206
582 T t207 o b77 b206
583 B b207 t207
584 T t208 o b75 b207
585 B b208 t208
586 T t209 o b73 b208
587 B b209 t209
588 T t210 o b71 b209
589 B b210 t210
590 T t211 o b69 b210
591 B b211 t211
592 T t212 o b67 b211
593 B b212 t212
594 T t213 o b65 b212
595 B b213 t213
596 T t214 o b63 b213
597 B b214 t214
598 T t215 o b61 b214
599 B b215 t215
600 T t216 o b59 b215
601 B b216 t216
602 T t217 o b57 b216
603 B b217 t217
604 T t218 o b55 b217
605 B b218 t218
606 T t219 o b53 b218
607 B b219 t219
608 T t220 o b51 b219
609 B b220 t220
610 T t221 o b49 b220
611 B b221 t221
612 T t222 o b47 b221
613 B b222 t222
614 T t223 o b45 b222
615 B b223 t223
616 T t224 o b43 b223
617 B b224 t224
618 T t225 o b41 b224
619 B b225 t225
620 T t226 o b39 b225
621 B b226 t226
622 T t227 o b37 b226
623 B b227 t227
624 T t228 o b35 b227
625 B b228 t228
626 T t229 o b33 b228
627 B b229 t229
628 T t230 o b31 b229
629 B b230 t230
630 T t231 o b29 b230
631 B b231 t231
632 T t232 o b27 b231
633 B b232 t232
634 T t233 o b25 b232
635 B b233 t233
636 T t234 o b23 b233
637 B b234 t234
638 T t235 o b21 b234
639 B b235 t235
640 T t236 o b19 b235
641 B b236 t236
642 T t237 o b17 b236
643 B b237 t237
644 T t238 o b15 b237
645 B b238 t238
646 T t239 o b13 b238
647 B b239 t239
648 T t240 o b11 b239
649 B b240 t240
650 T t241 o b9 b240
651 B b241 t241
652 T t242 o b7 b241
653 B b242 t242
654 NSummary!resource resource resource Summary
655 P p243 String auto
656 O o243 resource p243
657 NOcaml Ocaml Ocaml NIL
658 NOcaml!type_lid type_lid type_lid Ocaml
659 P p244 Number 2332
660 P p245 Number 2341
661 O o245 type_lid p244 p245
662 P p246 String auto_info
663 O o246 type_lid p246
664 T t246 o246
665 B b246 t246
666 T t247 o245 b246
667 B b247 t247
668 NOcaml!type_prod type_prod type_prod Ocaml
669 P p247 Number 2343
670 P p248 Number 2367
671 O o248 type_prod p247 p248
672 P p249 Number 2349
673 O o249 type_lid p247 p249
674 P p250 String tactic
675 O o250 type_lid p250
676 T t250 o250
677 B b250 t250
678 T t251 o249 b250
679 B b251 t251
680 P p251 Number 2352
681 P p252 Number 2358
682 O o252 type_lid p251 p252
683 T t252 o252 b250
684 B b252 t252
685 P p253 Number 2361
686 O o253 type_lid p253 p248
687 T t253 o253 b250
688 B b253 t253
689 T t254 o b253 b4
690 B b254 t254
691 T t255 o b252 b254
692 B b255 t255
693 T t256 o b251 b255
694 B b256 t256
695 T t257 o248 b256
696 B b257 t257
697 T t258 o243 b247 b257
698 B b258 t258
699 P p258 String cache
700 O o258 resource p258
701 P p259 Number 1424
702 P p260 Number 1434
703 O o260 type_lid p259 p260
704 P p261 String cache_rule
705 O o261 type_lid p261
706 T t261 o261
707 B b261 t261
708 T t262 o260 b261
709 B b262 t262
710 P p262 Number 1436
711 P p263 Number 1441
712 O o263 type_lid p262 p263
713 O o264 type_lid p258
714 T t264 o264
715 B b264 t264
716 T t265 o263 b264
717 B b265 t265
718 T t266 o258 b262 b265
719 B b266 t266
720 P p266 String elim
721 O o266 resource p266
722 P p267 Number 1761
723 P p268 Number 1783
724 O o268 type_prod p267 p268
725 P p269 Number 1765
726 O o269 type_lid p267 p269
727 P p270 String term
728 O o270 type_lid p270
729 T t270 o270
730 B b270 t270
731 T t271 o269 b270
732 B b271 t271
733 NOcaml!type_fun type_fun type_fun Ocaml
734 P p271 Number 1769
735 P p272 Number 1782
736 O o272 type_fun p271 p272
737 P p273 Number 1772
738 O o273 type_lid p271 p273
739 P p274 String int
740 O o274 type_lid p274
741 T t274 o274
742 B b274 t274
743 T t275 o273 b274
744 B b275 t275
745 P p275 Number 1776
746 O o275 type_lid p275 p272
747 T t276 o275 b250
748 B b276 t276
749 T t277 o272 b275 b276
750 B b277 t277
751 T t278 o b277 b4
752 B b278 t278
753 T t279 o b271 b278
754 B b279 t279
755 T t280 o268 b279
756 B b280 t280
757 P p280 Number 1785
758 P p281 Number 1798
759 O o281 type_fun p280 p281
760 P p282 Number 1788
761 O o282 type_lid p280 p282
762 T t282 o282 b274
763 B b282 t282
764 P p283 Number 1792
765 O o283 type_lid p283 p281
766 T t283 o283 b250
767 B b283 t283
768 T t284 o281 b282 b283
769 B b284 t284
770 T t285 o266 b280 b284
771 B b285 t285
772 P p285 String eqcd
773 O o285 resource p285
774 P p286 Number 6168
775 P p287 Number 6181
776 O o287 type_prod p286 p287
777 P p288 Number 6172
778 O o288 type_lid p286 p288
779 T t288 o288 b270
780 B b288 t288
781 P p289 Number 6175
782 O o289 type_lid p289 p287
783 T t289 o289 b250
784 B b289 t289
785 T t290 o b289 b4
786 B b290 t290
787 T t291 o b288 b290
788 B b291 t291
789 T t292 o287 b291
790 B b292 t292
791 P p292 Number 6183
792 P p293 Number 6189
793 O o293 type_lid p292 p293
794 T t293 o293 b250
795 B b293 t293
796 T t294 o285 b292 b293
797 B b294 t294
798 P p294 String intro
799 O o294 resource p294
800 P p295 Number 1815
801 P p296 Number 1852
802 O o296 type_prod p295 p296
803 P p297 Number 1819
804 O o297 type_lid p295 p297
805 T t297 o297 b270
806 B b297 t297
807 P p298 Number 1823
808 P p299 Number 1851
809 O o299 type_prod p298 p299
810 P p300 Number 1829
811 O o300 type_lid p298 p300
812 P p301 String string
813 O o301 type_lid p301
814 T t301 o301
815 B b301 t301
816 T t302 o300 b301
817 B b302 t302
818 NOcaml!type_apply type_apply type_apply Ocaml
819 P p302 Number 1832
820 P p303 Number 1842
821 O o303 type_apply p302 p303
822 P p304 Number 1836
823 O o304 type_lid p304 p303
824 P p305 String option
825 O o305 type_lid p305
826 T t305 o305
827 B b305 t305
828 T t306 o304 b305
829 B b306 t306
830 P p306 Number 1835
831 O o306 type_lid p302 p306
832 T t307 o306 b274
833 B b307 t307
834 T t308 o303 b306 b307
835 B b308 t308
836 P p308 Number 1845
837 O o308 type_lid p308 p299
838 T t309 o308 b250
839 B b309 t309
840 T t310 o b309 b4
841 B b310 t310
842 T t311 o b308 b310
843 B b311 t311
844 T t312 o b302 b311
845 B b312 t312
846 T t313 o299 b312
847 B b313 t313
848 T t314 o b313 b4
849 B b314 t314
850 T t315 o b297 b314
851 B b315 t315
852 T t316 o296 b315
853 B b316 t316
854 P p316 Number 1854
855 P p317 Number 1860
856 O o317 type_lid p316 p317
857 T t317 o317 b250
858 B b317 t317
859 T t318 o294 b316 b317
860 B b318 t318
861 P p318 String reduce
862 O o318 resource p318
863 P p319 Number 2920
864 P p320 Number 2931
865 O o320 type_prod p319 p320
866 P p321 Number 2924
867 O o321 type_lid p319 p321
868 T t321 o321 b270
869 B b321 t321
870 P p322 Number 2927
871 O o322 type_lid p322 p320
872 P p323 String conv
873 O o323 type_lid p323
874 T t323 o323
875 B b323 t323
876 T t324 o322 b323
877 B b324 t324
878 T t325 o b324 b4
879 B b325 t325
880 T t326 o b321 b325
881 B b326 t326
882 T t327 o320 b326
883 B b327 t327
884 P p327 Number 2933
885 P p328 Number 2937
886 O o328 type_lid p327 p328
887 T t328 o328 b323
888 B b328 t328
889 T t329 o318 b327 b328
890 B b329 t329
891 P p329 String squash
892 O o329 resource p329
893 P p330 Number 4017
894 P p331 Number 4028
895 O o331 type_lid p330 p331
896 P p332 String squash_info
897 O o332 type_lid p332
898 T t332 o332
899 B b332 t332
900 T t333 o331 b332
901 B b333 t333
902 P p333 Number 4030
903 P p334 Number 4043
904 O o334 type_fun p333 p334
905 P p335 Number 4033
906 O o335 type_lid p333 p335
907 T t335 o335 b274
908 B b335 t335
909 P p336 Number 4037
910 O o336 type_lid p336 p334
911 T t336 o336 b250
912 B b336 t336
913 T t337 o334 b335 b336
914 B b337 t337
915 T t338 o329 b333 b337
916 B b338 t338
917 P p338 String sub
918 O o338 resource p338
919 P p339 Number 4882
920 P p340 Number 4899
921 O o340 type_lid p339 p340
922 P p341 String sub_resource_info
923 O o341 type_lid p341
924 T t341 o341
925 B b341 t341
926 T t342 o340 b341
927 B b342 t342
928 P p342 Number 4901
929 P p343 Number 4907
930 O o343 type_lid p342 p343
931 T t343 o343 b250
932 B b343 t343
933 T t344 o338 b342 b343
934 B b344 t344
935 P p344 String toploop
936 O o344 resource p344
937 P p345 Number 2445
938 P p346 Number 2467
939 O o346 type_prod p345 p346
940 P p347 Number 2451
941 O o347 type_lid p345 p347
942 T t347 o347 b301
943 B b347 t347
944 P p348 Number 2454
945 P p349 Number 2460
946 O o349 type_lid p348 p349
947 T t349 o349 b301
948 B b349 t349
949 P p350 Number 2463
950 O o350 type_lid p350 p346
951 P p351 String expr
952 O o351 type_lid p351
953 T t351 o351
954 B b351 t351
955 T t352 o350 b351
956 B b352 t352
957 T t353 o b352 b4
958 B b353 t353
959 T t354 o b349 b353
960 B b354 t354
961 T t355 o b347 b354
962 B b355 t355
963 T t356 o346 b355
964 B b356 t356
965 P p356 Number 2469
966 P p357 Number 2478
967 O o357 type_lid p356 p357
968 P p358 String top_table
969 O o358 type_lid p358
970 T t358 o358
971 B b358 t358
972 T t359 o357 b358
973 B b359 t359
974 T t360 o344 b356 b359
975 B b360 t360
976 P p360 String typeinf
977 O o360 resource p360
978 P p361 Number 2151
979 P p362 Number 2172
980 O o362 type_lid p361 p362
981 P p363 String typeinf_resource_info
982 O o363 type_lid p363
983 T t363 o363
984 B b363 t363
985 T t364 o362 b363
986 B b364 t364
987 P p364 Number 2174
988 P p365 Number 2186
989 O o365 type_lid p364 p365
990 P p366 String typeinf_func
991 O o366 type_lid p366
992 T t366 o366
993 B b366 t366
994 T t367 o365 b366
995 B b367 t367
996 T t368 o360 b364 b367
997 B b368 t368
998 P p368 String typeinf_subst
999 O o368 resource p368
1000 P p369 Number 1825
1001 P p370 Number 1843
1002 O o370 type_lid p369 p370
1003 P p371 String typeinf_subst_info
1004 O o371 type_lid p371
1005 T t371 o371
1006 B b371 t371
1007 T t372 o370 b371
1008 B b372 t372
1009 P p372 Number 1862
1010 O o372 type_lid p308 p372
1011 P p373 String typeinf_subst_fun
1012 O o373 type_lid p373
1013 T t373 o373
1014 B b373 t373
1015 T t374 o372 b373
1016 B b374 t374
1017 T t375 o368 b372 b374
1018 B b375 t375
1019 T t376 o b375 b4
1020 B b376 t376
1021 T t377 o b368 b376
1022 B b377 t377
1023 T t378 o b360 b377
1024 B b378 t378
1025 T t379 o b344 b378
1026 B b379 t379
1027 T t380 o b338 b379
1028 B b380 t380
1029 T t381 o b329 b380
1030 B b381 t381
1031 T t382 o b318 b381
1032 B b382 t382
1033 T t383 o b294 b382
1034 B b383 t383
1035 T t384 o b285 b383
1036 B b384 t384
1037 T t385 o b266 b384
1038 B b385 t385
1039 T t386 o b258 b385
1040 B b386 t386
1041 P p388 Number 22
1042 P p390 String Czf_itt_equiv
1043 O o390 parent p390
1044 T t390 o390
1045 B b390 t390
1046 T t391 o b390 b4
1047 B b391 t391
1048 P p391 String Czf_itt_pair
1049 O o391 parent p391
1050 T t392 o391
1051 B b392 t392
1052 T t393 o b392 b4
1053 B b393 t393
1054 P p393 String Czf_itt_singleton
1055 O o393 parent p393
1056 T t394 o393
1057 B b394 t394
1058 T t395 o b394 b4
1059 B b395 t395
1060 P p395 String Czf_itt_union
1061 O o395 parent p395
1062 T t396 o395
1063 B b396 t396
1064 T t397 o b396 b4
1065 B b397 t397
1066 P p397 String Czf_itt_subset
1067 O o397 parent p397
1068 T t398 o397
1069 B b398 t398
1070 T t399 o b398 b4
1071 B b399 t399
1072 P p399 String Czf_itt_dexists
1073 O o399 parent p399
1074 T t400 o399
1075 B b400 t400
1076 T t401 o b400 b4
1077 B b401 t401
1078 T t1 o b401 b242
1079 B b1 t1
1080 T t2 o b399 b1
1081 B b2 t2
1082 T t3 o b397 b2
1083 B b3 t3
1084 T t249 o b395 b3
1085 B b249 t249
1086 T t281 o b393 b249
1087 B b281 t281
1088 T t286 o b391 b281
1089 B b286 t286
1090 T t287 o b5 b286
1091 B b287 t287
1092 T t350 o2 b5 b287 b386
1093 B b533 t350
1094 T t533 o1 b533
1095 B b594 t533
1096 P p4 Number 47
1097 O o14 location p388 p4
1098 P p14 String Czf_itt_group_bvd
1099 O o20 parent p14
1100 T t243 o20
1101 B b243 t243
1102 T t298 o b243 b4
1103 B b298 t298
1104 T t299 o b298 b4
1105 B b299 t299
1106 T t300 o2 b298 b299 b386
1107 B b300 t300
1108 T t303 o14 b300
1109 B b303 t303
1110 P p309 Number 48
1111 T t594 o2 b391 b4 b386
1112 B b599 t594
1113 P p411 String Czf_itt_subgroup
1114 O o411 parent p411
1115 T t411 o411
1116 B b411 t411
1117 T t412 o b411 b4
1118 B b412 t412
1119 P p412 String Czf_itt_isect
1120 O o412 parent p412
1121 T t413 o412
1122 B b413 t413
1123 T t414 o b413 b4
1124 B b414 t414
1125 T t415 o b414 b4
1126 B b415 t415
1127 T t416 o b412 b415
1128 B b416 t416
1129 T t417 o2 b412 b416 b386
1130 B b417 t417
1131 P p418 Number 69
1132 O o310 location p309 p418
1133 T t330 o310 b599
1134 B b330 t330
1135 P p337 Number 70
1136 P p352 Number 94
1137 O o352 location p337 p352
1138 T t361 o352 b417
1139 B b362 t361
1140 P p367 Number 95
1141 P p374 Number 117
1142 O o374 location p367 p374
1143 T t419 o2 b399 b4 b386
1144 B b419 t419
1145 T t387 o374 b419
1146 B b387 t387
1147 P p387 Number 118
1148 P p392 Number 138
1149 O o392 location p387 p392
1150 T t421 o2 b71 b4 b386
1151 B b421 t421
1152 T t402 o392 b421
1153 B b402 t402
1154 P p402 Number 140
1155 NSummary!summary_item summary_item summary_item Summary
1156 O o424 summary_item
1157 NOcaml!str_open str_open str_open Ocaml
1158 NOcaml!string string string Ocaml
1159 P p425 String Refiner
1160 O o426 string p425
1161 T t426 o426
1162 B b426 t426
1163 P p426 String TermType
1164 O o427 string p426
1165 T t427 o427
1166 B b427 t427
1167 T t428 o b427 b4
1168 B b428 t428
1169 T t429 o b426 b428
1170 B b429 t429
1171 T t430 o b426 b429
1172 B b430 t430
1173 P p434 Number 169
1174 O o402 location p402 p434
1175 O o403 str_open p402 p434
1176 T t403 o403 b430
1177 B b403 t403
1178 T t404 o424 b403
1179 B b404 t404
1180 T t405 o402 b404
1181 B b405 t405
1182 P p435 String Term
1183 O o436 string p435
1184 T t436 o436
1185 B b436 t436
1186 T t437 o b436 b4
1187 B b437 t437
1188 T t438 o b426 b437
1189 B b438 t438
1190 T t439 o b426 b438
1191 B b439 t439
1192 P p442 Number 170
1193 P p405 Number 195
1194 O o405 location p442 p405
1195 O o406 str_open p442 p405
1196 T t406 o406 b439
1197 B b406 t406
1198 T t423 o424 b406
1199 B b424 t423
1200 T t424 o405 b424
1201 B b425 t424
1202 P p427 Number 196
1203 P p428 Number 223
1204 O o428 location p427 p428
1205 O o429 str_open p427 p428
1206 P p444 String TermOp
1207 O o445 string p444
1208 T t445 o445
1209 B b445 t445
1210 T t446 o b445 b4
1211 B b446 t446
1212 T t447 o b426 b446
1213 B b447 t447
1214 T t448 o b426 b447
1215 B b448 t448
1216 T t434 o429 b448
1217 B b434 t434
1218 T t435 o424 b434
1219 B b435 t435
1220 T t443 o428 b435
1221 B b443 t443
1222 P p445 Number 224
1223 P p446 Number 253
1224 O o446 location p445 p446
1225 O o447 str_open p445 p446
1226 P p453 String TermAddr
1227 O o454 string p453
1228 T t454 o454
1229 B b454 t454
1230 T t455 o b454 b4
1231 B b455 t455
1232 T t456 o b426 b455
1233 B b456 t456
1234 T t457 o b426 b456
1235 B b457 t457
1236 T t452 o447 b457
1237 B b452 t452
1238 T t453 o424 b452
1239 B b453 t453
1240 T t461 o446 b453
1241 B b461 t461
1242 P p463 Number 254
1243 P p464 Number 282
1244 O o464 location p463 p464
1245 O o465 str_open p463 p464
1246 P p462 String TermMan
1247 O o463 string p462
1248 T t463 o463
1249 B b463 t463
1250 T t464 o b463 b4
1251 B b464 t464
1252 T t465 o b426 b464
1253 B b465 t465
1254 T t466 o b426 b465
1255 B b466 t466
1256 T t470 o465 b466
1257 B b470 t470
1258 T t471 o424 b470
1259 B b471 t471
1260 T t480 o464 b471
1261 B b488 t480
1262 P p490 Number 283
1263 P p491 Number 313
1264 O o491 location p490 p491
1265 O o492 str_open p490 p491
1266 P p471 String TermSubst
1267 O o472 string p471
1268 T t472 o472
1269 B b472 t472
1270 T t473 o b472 b4
1271 B b473 t473
1272 T t474 o b426 b473
1273 B b474 t474
1274 T t475 o b426 b474
1275 B b475 t475
1276 T t497 o492 b475
1277 B b497 t497
1278 T t498 o424 b497
1279 B b498 t498
1280 T t504 o491 b498
1281 B b504 t504
1282 P p506 Number 314
1283 P p507 Number 341
1284 O o508 location p506 p507
1285 O o509 str_open p506 p507
1286 P p480 String Refine
1287 O o481 string p480
1288 T t481 o481
1289 B b481 t481
1290 T t482 o b481 b4
1291 B b482 t482
1292 T t483 o b426 b482
1293 B b483 t483
1294 T t484 o b426 b483
1295 B b484 t484
1296 T t512 o509 b484
1297 B b512 t512
1298 T t525 o424 b512
1299 B b525 t525
1300 T t526 o508 b525
1301 B b526 t526
1302 P p527 Number 342
1303 P p528 Number 374
1304 O o528 location p527 p528
1305 O o529 str_open p527 p528
1306 P p489 String RefineError
1307 O o490 string p489
1308 T t490 o490
1309 B b490 t490
1310 T t491 o b490 b4
1311 B b491 t491
1312 T t492 o b426 b491
1313 B b492 t492
1314 T t493 o b426 b492
1315 B b493 t493
1316 T t532 o529 b493
1317 B b532 t532
1318 T t540 o424 b532
1319 B b540 t540
1320 T t541 o528 b540
1321 B b541 t541
1322 P p543 Number 375
1323 P p544 Number 391
1324 O o544 location p543 p544
1325 O o545 str_open p543 p544
1326 P p498 String Mp_resource
1327 O o499 string p498
1328 T t499 o499
1329 B b499 t499
1330 T t500 o b499 b4
1331 B b500 t500
1332 T t548 o545 b500
1333 B b548 t548
1334 T t549 o424 b548
1335 B b549 t549
1336 T t556 o544 b549
1337 B b557 t556
1338 P p557 Number 392
1339 P p505 String Simple_print
1340 O o506 string p505
1341 T t506 o506
1342 B b506 t506
1343 T t507 o b506 b4
1344 B b507 t507
1345 P p512 String Printf
1346 O o513 string p512
1347 T t513 o513
1348 B b513 t513
1349 T t514 o b513 b4
1350 B b514 t514
1351 P p518 Number 409
1352 O o559 location p557 p518
1353 O o560 str_open p557 p518
1354 T t563 o560 b507
1355 B b563 t563
1356 T t564 o424 b563
1357 B b564 t564
1358 T t570 o559 b564
1359 B b571 t570
1360 P p571 Number 410
1361 P p572 Number 421
1362 O o573 location p571 p572
1363 O o574 str_open p571 p572
1364 T t577 o574 b514
1365 B b577 t577
1366 T t578 o424 b577
1367 B b578 t578
1368 T t584 o573 b578
1369 B b584 t584
1370 P p589 Number 422
1371 P p590 Number 435
1372 O o590 location p589 p590
1373 O o591 str_open p589 p590
1374 P p519 String Mp_debug
1375 O o520 string p519
1376 T t520 o520
1377 B b520 t520
1378 T t521 o b520 b4
1379 B b521 t521
1380 T t593 o591 b521
1381 B b593 t593
1382 T t595 o424 b593
1383 B b595 t595
1384 T t597 o590 b595
1385 B b597 t597
1386 P p597 Number 437
1387 P p598 Number 453
1388 O o598 location p597 p598
1389 O o599 str_open p597 p598
1390 P p526 String Tactic_type
1391 O o527 string p526
1392 T t527 o527
1393 B b527 t527
1394 T t528 o b527 b4
1395 B b528 t528
1396 T t600 o599 b528
1397 B b601 t600
1398 T t601 o424 b601
1399 B b602 t601
1400 T t602 o598 b602
1401 B b603 t602
1402 P p532 Number 454
1403 P p533 String Tacticals
1404 O o534 string p533
1405 T t534 o534
1406 B b534 t534
1407 T t535 o b534 b4
1408 B b535 t535
1409 T t536 o b527 b535
1410 B b536 t536
1411 P p541 String Sequent
1412 O o542 string p541
1413 T t542 o542
1414 B b542 t542
1415 T t543 o b542 b4
1416 B b543 t543
1417 T t544 o b527 b543
1418 B b544 t544
1419 P p547 Number 480
1420 O o607 location p532 p547
1421 O o608 str_open p532 p547
1422 T t618 o608 b536
1423 B b618 t618
1424 T t619 o424 b618
1425 B b619 t619
1426 T t620 o607 b619
1427 B b620 t620
1428 P p622 Number 481
1429 P p623 Number 505
1430 O o624 location p622 p623
1431 O o625 str_open p622 p623
1432 T t625 o625 b544
1433 B b625 t625
1434 T t626 o424 b625
1435 B b626 t626
1436 T t627 o624 b626
1437 B b627 t627
1438 P p627 Number 506
1439 P p628 Number 536
1440 O o628 location p627 p628
1441 O o629 str_open p627 p628
1442 P p549 String Conversionals
1443 O o550 string p549
1444 T t550 o550
1445 B b550 t550
1446 T t551 o b550 b4
1447 B b551 t551
1448 T t552 o b527 b551
1449 B b552 t552
1450 T t629 o629 b552
1451 B b629 t629
1452 T t630 o424 b629
1453 B b630 t630
1454 T t631 o628 b630
1455 B b631 t631
1456 P p631 Number 537
1457 P p632 Number 547
1458 O o632 location p631 p632
1459 O o633 str_open p631 p632
1460 O o558 string p151
1461 T t558 o558
1462 B b558 t558
1463 T t559 o b558 b4
1464 B b559 t559
1465 T t633 o633 b559
1466 B b635 t633
1467 T t637 o424 b635
1468 B b637 t637
1469 T t639 o632 b637
1470 B b639 t639
1471 P p640 Number 548
1472 P p641 Number 556
1473 O o642 location p640 p641
1474 O o643 str_open p640 p641
1475 O o565 string p149
1476 T t565 o565
1477 B b565 t565
1478 T t566 o b565 b4
1479 B b566 t566
1480 T t643 o643 b566
1481 B b643 t643
1482 T t644 o424 b643
1483 B b644 t644
1484 T t645 o642 b644
1485 B b645 t645
1486 P p645 Number 558
1487 P p646 Number 575
1488 O o647 location p645 p646
1489 O o648 str_open p645 p646
1490 O o572 string p139
1491 T t572 o572
1492 B b572 t572
1493 T t573 o b572 b4
1494 B b573 t573
1495 T t648 o648 b573
1496 B b648 t648
1497 T t649 o424 b648
1498 B b649 t649
1499 T t650 o647 b649
1500 B b650 t650
1501 P p650 Number 576
1502 P p651 Number 597
1503 O o651 location p650 p651
1504 O o652 str_open p650 p651
1505 O o579 string p141
1506 T t579 o579
1507 B b579 t579
1508 T t580 o b579 b4
1509 B b580 t580
1510 T t652 o652 b580
1511 B b652 t652
1512 T t657 o424 b652
1513 B b657 t657
1514 T t658 o651 b657
1515 B b658 t658
1516 NSummary!opname opname opname Summary
1517 P p585 String power
1518 O o585 opname p585
1519 NCzf_itt_cyclic_subgroup Czf_itt_cyclic_subgroup Czf_itt_cyclic_subgroup NIL
1520 NCzf_itt_cyclic_subgroup!power power power Czf_itt_cyclic_subgroup
1521 O o586 power
1522 Nvar var var NIL
1523 P p586 Var g
1524 O o587 var p586
1525 T t587 o587
1526 B b587 t587
1527 P p587 Var z
1528 O o588 var p587
1529 T t588 o588
1530 B b588 t588
1531 P p588 Var n
1532 O o589 var p588
1533 T t589 o589
1534 B b589 t589
1535 T t590 o586 b587 b588 b589
1536 B b590 t590
1537 T t591 o585 b590
1538 B b591 t591
1539 P p592 Number 599
1540 P p658 Number 624
1541 O o658 location p592 p658
1542 T t660 o658 b591
1543 B b660 t660
1544 P p660 Number 625
1545 P p661 Number 653
1546 O o661 location p660 p661
1547 P p12 String cyc_subg
1548 O o16 opname p12
1549 NCzf_itt_cyclic_subgroup!cyc_subg cyc_subg cyc_subg Czf_itt_cyclic_subgroup
1550 O o18 cyc_subg
1551 P p595 Var a
1552 O o596 var p595
1553 T t596 o596
1554 B b596 t596
1555 NSummary!rewrite rewrite rewrite Summary
1556 P p601 String unfold_power
1557 O o601 rewrite p601
1558 NItt_int_base Itt_int_base Itt_int_base NIL
1559 NItt_int_base!ind ind ind Itt_int_base
1560 O o602 ind
1561 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1562 NCzf_itt_group!op op op Czf_itt_group
1563 O o603 op
1564 NCzf_itt_group!inv inv inv Czf_itt_group
1565 O o604 inv
1566 T t604 o604 b587 b588
1567 B b604 t604
1568 NItt_int_base!add add add Itt_int_base
1569 O o605 add
1570 NItt_int_base!number number number Itt_int_base
1571 P p605 Number 1
1572 O o606 number p605
1573 T t606 o606
1574 B b606 t606
1575 T t607 o605 b589 b606
1576 B b607 t607
1577 T t608 o586 b587 b588 b607
1578 B b608 t608
1579 T t609 o603 b587 b604 b608
1580 B b609 t609 i j
1581 NCzf_itt_group!id id id Czf_itt_group
1582 O o609 id
1583 T t610 o609 b587
1584 B b610 t610
1585 NItt_int_base!sub sub sub Itt_int_base
1586 O o610 sub
1587 T t611 o610 b589 b606
1588 B b611 t611
1589 T t612 o586 b587 b588 b611
1590 B b612 t612
1591 T t613 o603 b587 b588 b612
1592 B b613 t613 k l
1593 T t614 o602 b589 b609 b610 b613
1594 B b614 t614
1595 NSummary!prim prim prim Summary
1596 O o614 prim
1597 T t615 o614 b4
1598 B b615 t615
1599 T t616 o601 b590 b614 b615 b4
1600 B b616 t616
1601 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1602 NCzf_itt_set!collect collect collect Czf_itt_set
1603 O o620 collect
1604 NItt_int_base!int int int Itt_int_base
1605 O o621 int
1606 T t621 o621
1607 B b621 t621
1608 P p621 Var x
1609 O o622 var p621
1610 T t622 o622
1611 B b622 t622
1612 T t623 o586 b587 b596 b622
1613 B b623 t623 x
1614 T t624 o620 b621 b623
1615 B b624 t624
1616 NOcaml!str_let str_let str_let Ocaml
1617 NOcaml!patt_var patt_var patt_var Ocaml
1618 NOcaml!patt_done patt_done patt_done Ocaml
1619 NOcaml!apply apply apply Ocaml
1620 NOcaml!lid lid lid Ocaml
1621 P p634 String makeFoldC
1622 O o634 lid p634
1623 T t634 o634
1624 B b634 t634
1625 NOcaml!proj proj proj Ocaml
1626 NOcaml!uid uid uid Ocaml
1627 P p637 String Ml_term
1628 O o638 uid p637
1629 T t638 o638
1630 B b638 t638
1631 P p639 String term_of_string
1632 O o640 lid p639
1633 T t640 o640
1634 B b640 t640
1635 O o646 lid p601
1636 T t646 o646
1637 B b646 t646
1638 NSummary!dform dform dform Summary
1639 P p681 String power_df
1640 O o681 dform p681
1641 NSummary!except_mode_df except_mode_df except_mode_df Summary
1642 P p682 String src
1643 O o682 except_mode_df p682
1644 T t682 o682
1645 B b682 t682
1646 NSummary!parens_df parens_df parens_df Summary
1647 O o684 parens_df
1648 T t684 o684
1649 B b684 t684
1650 T t685 o b684 b4
1651 B b685 t685
1652 NSummary!df_term df_term df_term Summary
1653 O o687 df_term
1654 NPerv!string string687 string Perv
1655 P p687 String power(
1656 O o688 string687 p687
1657 T t688 o688
1658 B b688 t688
1659 Nslot slot slot NIL
1660 O o689 slot
1661 T t689 o689 b587
1662 B b689 t689
1663 P p689 String "; "
1664 O o690 string687 p689
1665 T t690 o690
1666 B b690 t690
1667 T t691 o689 b588
1668 B b691 t691
1669 T t692 o689 b589
1670 B b692 t692
1671 P p692 String )
1672 O o692 string687 p692
1673 T t693 o692
1674 B b693 t693
1675 T t694 o b693 b4
1676 B b694 t694
1677 T t695 o b692 b694
1678 B b695 t695
1679 T t696 o b690 b695
1680 B b696 t696
1681 T t697 o b691 b696
1682 B b697 t697
1683 T t698 o b690 b697
1684 B b698 t698
1685 T t699 o b689 b698
1686 B b699 t699
1687 T t700 o b688 b699
1688 B b700 t700
1689 T t701 o687 b700
1690 B b701 t701
1691 T t705 o b682 b4
1692 B b705 t705
1693 T t707 o689 b596
1694 B b707 t707
1695 T t708 o b707 b694
1696 B b708 t708
1697 T t709 o b690 b708
1698 B b709 t709
1699 NSummary!rule rule rule Summary
1700 P p716 String power_wf1
1701 O o716 rule p716
1702 NSummary!context_param context_param context_param Summary
1703 P p717 String H
1704 O o717 context_param p717
1705 T t717 o717
1706 B b717 t717
1707 T t718 o b717 b4
1708 B b718 t718
1709 NSummary!meta_implies meta_implies meta_implies Summary
1710 O o718 meta_implies
1711 NSummary!meta_theorem meta_theorem meta_theorem Summary
1712 O o719 meta_theorem
1713 NBase_trivial Base_trivial Base_trivial NIL
1714 NBase_trivial!squash squash squash Base_trivial
1715 O o720 squash
1716 T t720 o720
1717 B b720 t720
1718 T t721 o b720 b4
1719 C h H
1720 NItt_equal Itt_equal Itt_equal NIL
1721 NItt_equal!equal equal equal Itt_equal
1722 O o721 equal
1723 NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1724 NItt_record_label0!label label label Itt_record_label0
1725 O o722 label
1726 T t722 o722
1727 B b722 t722
1728 T t723 o721 b722 b587 b587
1729 S s t721 h
1730 G s t723
1731 B b723 s
1732 T t724 o719 b723
1733 B b724 t724
1734 P p724 Var ext
1735 O o724 var p724
1736 T t725 o724
1737 B b725 t725
1738 T t726 o b725 b4
1739 NCzf_itt_group!group group group Czf_itt_group
1740 O o726 group
1741 T t727 o726 b587
1742 S s727 t726 h
1743 G s727 t727
1744 B b727 s727
1745 T t728 o719 b727
1746 B b728 t728
1747 T t729 o721 b621 b589 b589
1748 S s729 t726 h
1749 G s729 t729
1750 B b729 s729
1751 NCzf_itt_set!isset isset isset Czf_itt_set
1752 O o730 isset
1753 T t731 o730 b588
1754 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1755 NCzf_itt_member!mem mem mem Czf_itt_member
1756 O o732 mem
1757 NCzf_itt_group!car car car Czf_itt_group
1758 O o733 car
1759 T t733 o733 b587
1760 B b733 t733
1761 T t734 o732 b588 b733
1762 S s734 t726 h
1763 G s734 t734
1764 B b734 s734
1765 T t735 o719 b734
1766 B b735 t735
1767 T t736 o730 b590
1768 S s736 t726 h
1769 G s736 t736
1770 B b736 s736
1771 T t737 o719 b736
1772 B b737 t737
1773 NSummary!interactive interactive interactive Summary
1774 O o742 interactive
1775 NSummary!ext_rule ext_rule ext_rule Summary
1776 P p742 String "genAssumT [3] thenT autoT thenT dT 2 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
1777 O o743 ext_rule p742
1778 NSummary!status_incomplete status_incomplete status_incomplete Summary
1779 O o744 status_incomplete
1780 T t744 o744
1781 B b744 t744
1782 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
1783 O o745 ext_unjustified
1784 NSummary!tactic_arg tactic_arg tactic_arg Summary
1785 P p745 String main
1786 O o746 tactic_arg p745
1787 NSummary!msequent msequent msequent Summary
1788 O o747 msequent
1789 T t747 o b734 b4
1790 B b747 t747
1791 NSummary!parent_none parent_none parent_none Summary
1792 O o752 parent_none
1793 T t753 o752
1794 B b753 t753
1795 H h754 m t621
1796 NItt_int_base!lt lt lt Itt_int_base
1797 O o754 lt
1798 P p754 Var m
1799 O o755 var p754
1800 T t755 o755
1801 B b755 t755
1802 O o756 number p
1803 T t756 o756
1804 B b756 t756
1805 T t757 o754 b755 b756
1806 H h757 v t757
1807 T t758 o605 b755 b606
1808 B b758 t758
1809 T t759 o586 b587 b588 b758
1810 B b759 t759
1811 T t760 o730 b759
1812 H h760 z_1 t760
1813 T t761 o603 b587 b604 b759
1814 B b761 t761 i j
1815 T t762 o610 b755 b606
1816 B b762 t762
1817 T t763 o586 b587 b588 b762
1818 B b763 t763
1819 T t764 o603 b587 b588 b763
1820 B b764 t764 k l
1821 T t765 o602 b755 b761 b610 b764
1822 B b765 t765
1823 T t766 o730 b765
1824 S s766 t726 h h754 h757 h760
1825 G s766 t766
1826 B b766 s766
1827 T t768 o586 b587 b588 b755
1828 B b768 t768
1829 T t769 o730 b768
1830 S s769 t726 h h754 h757 h760
1831 G s769 t769
1832 B b769 s769
1833 H h770 n t621
1834 S s770 t726 h h770 h754 h757 h760
1835 G s770 t769
1836 B b771 s770
1837 S s772 t726 h h770
1838 G s772 t736
1839 B b773 s772
1840 P p774 String assertion
1841 O o774 tactic_arg p774
1842 NItt_logic Itt_logic Itt_logic NIL
1843 NItt_logic!all all all Itt_logic
1844 O o775 all
1845 B b775 t736 n
1846 T t775 o775 b621 b775
1847 S s775 t726 h
1848 G s775 t775
1849 B b776 s775
1850 NSummary!arg_named arg_named arg_named Summary
1851 P p777 String d_auto
1852 O o777 arg_named p777
1853 NSummary!arg_bool arg_bool arg_bool Summary
1854 P p778 String true
1855 O o778 arg_bool p778
1856 T t778 o778
1857 B b778 t778
1858 T t779 o777 b778
1859 B b779 t779
1860 T t780 o b779 b4
1861 B b780 t780
1862 T t791 o754 b756 b755
1863 H h791 v t791
1864 T t792 o730 b763
1865 H h792 z_1 t792
1866 S s792 t726 h h754 h791 h792
1867 G s792 t766
1868 B b792 s792
1869 S s793 t726 h h754 h791 h792
1870 G s793 t769
1871 B b794 s793
1872 S s795 t726 h h770 h754 h791 h792
1873 G s795 t769
1874 B b796 s795
1875 P p805 String "rwh reduce_ind_down 0 ttca"
1876 O o805 ext_rule p805
1877 P p807 String "rwh reduce_ind_up 0 ttca"
1878 O o807 ext_rule p807
1879 NSummary!resource_defs resource_defs resource_defs Summary
1880 P p816 String []
1881 O o816 uid p816
1882 T t816 o816
1883 B b816 t816
1884 P p824 String power_wf2
1885 O o824 rule p824
1886 T t824 o732 b590 b733
1887 S s824 t726 h
1888 G s824 t824
1889 B b824 s824
1890 T t825 o719 b824
1891 B b825 t825
1892 T t826 o718 b735 b825
1893 B b826 t826
1894 T t833 o732 b759 b733
1895 H h833 z_1 t833
1896 T t834 o732 b765 b733
1897 S s834 t726 h h754 h757 h833
1898 G s834 t834
1899 B b834 s834
1900 T t836 o732 b768 b733
1901 S s836 t726 h h754 h757 h833
1902 G s836 t836
1903 B b836 s836
1904 S s837 t726 h h770 h754 h757 h833
1905 G s837 t836
1906 B b838 s837
1907 S s839 t726 h h770
1908 G s839 t824
1909 B b840 s839
1910 B b842 t824 n
1911 T t842 o775 b621 b842
1912 S s842 t726 h
1913 G s842 t842
1914 B b843 s842
1915 T t854 o732 b763 b733
1916 H h854 z_1 t854
1917 S s854 t726 h h754 h791 h854
1918 G s854 t834
1919 B b855 s854
1920 S s856 t726 h h754 h791 h854
1921 G s856 t836
1922 B b857 s856
1923 S s858 t726 h h770 h754 h791 h854
1924 G s858 t836
1925 B b859 s858
1926 P p6 String power_fun
1927 O o8 rule p6
1928 NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
1929 NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
1930 O o10 fun_set
1931 P p10 Var f
1932 O o12 var p10
1933 T t244 o12 b588
1934 B b244 t244 z
1935 T t245 o10 b244
1936 S s245 t726 h
1937 G s245 t245
1938 B b245 s245
1939 T t248 o719 b245
1940 B b248 t248
1941 NCzf_itt_set!set set set Czf_itt_set
1942 O o251 set
1943 T t259 o251
1944 H h259 z t259
1945 B b259 t244
1946 T t260 o732 b259 b733
1947 S s260 t726 h h259
1948 G s260 t260
1949 B b260 s260
1950 T t263 o719 b260
1951 B b263 t263
1952 T t267 o586 b587 b259 b589
1953 B b267 t267 z
1954 T t268 o10 b267
1955 S s268 t726 h
1956 G s268 t268
1957 B b268 s268
1958 T t269 o719 b268
1959 B b269 t269
1960 T t272 o718 b263 b269
1961 B b272 t272
1962 T t273 o718 b248 b272
1963 B b273 t273
1964 P p290 String "rwh unfold_fun_set 0 thenT autoT"
1965 O o290 ext_rule p290
1966 T t295 o b260 b4
1967 B b295 t295
1968 T t296 o b245 b295
1969 B b296 t296
1970 P p307 String wf
1971 O o307 tactic_arg p307
1972 H h307 s1 t259
1973 H h308 s2 t259
1974 NCzf_itt_eq!equal equal308 equal Czf_itt_eq
1975 O o309 equal308
1976 P p885 String power_property1
1977 O o885 rule p885
1978 P p886 Var R
1979 O o886 var p886
1980 T t886 o886
1981 B b886 t886
1982 T t887 o730 b886
1983 S s887 t721 h
1984 G s887 t887
1985 B b887 s887
1986 NCzf_itt_equiv Czf_itt_equiv Czf_itt_equiv NIL
1987 NCzf_itt_equiv!equiv equiv equiv Czf_itt_equiv
1988 O o888 equiv
1989 T t889 o888 b733 b886
1990 S s889 t726 h
1991 G s889 t889
1992 B b889 s889
1993 T t891 o730 b622
1994 S s891 t726 h
1995 G s891 t891
1996 B b891 s891
1997 T t893 o732 b622 b733
1998 S s893 t726 h
1999 G s893 t893
2000 B b893 s893
2001 T t894 o719 b893
2002 B b894 t894
2003 T t895 o586 b587 b622 b607
2004 B b895 t895
2005 T t896 o604 b587 b622
2006 B b896 t896
2007 T t897 o603 b587 b895 b896
2008 B b897 t897
2009 T t898 o586 b587 b622 b589
2010 B b898 t898
2011 T t899 o888 b733 b886 b897 b898
2012 S s899 t726 h
2013 G s899 t899
2014 B b899 s899
2015 T t908 o b893 b4
2016 B b908 t908
2017 T t909 o b891 b908
2018 B b909 t909
2019 T t910 o b729 b909
2020 B b910 t910
2021 T t911 o b889 b910
2022 B b911 t911
2023 T t912 o b727 b911
2024 B b912 t912
2025 T t913 o b723 b912
2026 B b913 t913
2027 T t914 o b887 b913
2028 B b914 t914
2029 T t915 o747 b899 b914
2030 B b915 t915
2031 T t916 o746 b915 b4 b753
2032 B b916 t916
2033 T t917 o605 b758 b606
2034 B b917 t917
2035 T t918 o586 b587 b622 b917
2036 B b918 t918
2037 T t919 o603 b587 b918 b896
2038 B b919 t919
2039 T t920 o586 b587 b622 b758
2040 B b920 t920
2041 T t921 o888 b733 b886 b919 b920
2042 H h921 z t921
2043 T t922 o603 b587 b920 b896
2044 B b922 t922
2045 T t923 o586 b587 b622 b755
2046 B b923 t923
2047 T t924 o888 b733 b886 b922 b923
2048 S s924 t726 h h754 h757 h921
2049 G s924 t924
2050 B b924 s924
2051 T t925 o747 b924 b914
2052 B b925 t925
2053 S s925 t726 h h770 h754 h757 h921
2054 G s925 t924
2055 B b926 s925
2056 T t926 o747 b926 b914
2057 B b927 t926
2058 S s927 t726 h h770
2059 G s927 t899
2060 B b928 s927
2061 T t928 o747 b928 b914
2062 B b929 t928
2063 B b930 t899 n
2064 T t930 o775 b621 b930
2065 S s930 t726 h
2066 G s930 t930
2067 B b931 s930
2068 T t931 o747 b931 b914
2069 B b932 t931
2070 T t932 o2 b916
2071 B b933 t932
2072 T t933 o774 b932 b4 b933
2073 B b934 t933
2074 T t934 o2 b934
2075 B b935 t934
2076 T t935 o746 b929 b4 b935
2077 B b936 t935
2078 T t936 o2 b936
2079 B b937 t936
2080 T t937 o746 b927 b4 b937
2081 B b938 t937
2082 T t938 o2 b938
2083 B b939 t938
2084 T t939 o746 b925 b4 b939
2085 B b940 t939
2086 T t940 o605 b756 b606
2087 B b941 t940
2088 T t941 o586 b587 b622 b941
2089 B b942 t941
2090 T t942 o603 b587 b942 b896
2091 B b943 t942
2092 T t943 o586 b587 b622 b756
2093 B b944 t943
2094 T t944 o888 b733 b886 b943 b944
2095 S s944 t726 h
2096 G s944 t944
2097 B b945 s944
2098 T t945 o747 b945 b914
2099 B b946 t945
2100 S s946 t726 h h770
2101 G s946 t944
2102 B b947 s946
2103 T t947 o747 b947 b914
2104 B b948 t947
2105 T t948 o746 b948 b4 b937
2106 B b949 t948
2107 T t949 o2 b949
2108 B b950 t949
2109 T t950 o746 b946 b4 b950
2110 B b951 t950
2111 T t951 o605 b762 b606
2112 B b952 t951
2113 T t952 o586 b587 b622 b952
2114 B b953 t952
2115 T t953 o603 b587 b953 b896
2116 B b954 t953
2117 T t954 o586 b587 b622 b762
2118 B b955 t954
2119 T t955 o888 b733 b886 b954 b955
2120 H h955 z t955
2121 S s955 t726 h h754 h791 h955
2122 G s955 t924
2123 B b956 s955
2124 T t956 o747 b956 b914
2125 B b957 t956
2126 S s957 t726 h h770 h754 h791 h955
2127 G s957 t924
2128 B b958 s957
2129 T t958 o747 b958 b914
2130 B b959 t958
2131 T t959 o746 b959 b4 b937
2132 B b960 t959
2133 T t960 o2 b960
2134 B b961 t960
2135 T t961 o746 b957 b4 b961
2136 B b962 t961
2137 P p966 String "decideT << 'm = -1 in int >> ttca"
2138 O o966 ext_rule p966
2139 NItt_int_base!minus minus minus Itt_int_base
2140 O o967 minus
2141 T t967 o967 b606
2142 B b967 t967
2143 T t968 o721 b621 b755 b967
2144 H h968 x_1 t968
2145 S s968 t726 h h754 h757 h921 h968
2146 G s968 t924
2147 B b968 s968
2148 T t969 o747 b968 b914
2149 B b969 t969
2150 T t970 o2 b940
2151 B b970 t970
2152 T t971 o746 b969 b4 b970
2153 B b971 t971
2154 NItt_logic!not not not Itt_logic
2155 O o971 not
2156 B b972 t968
2157 T t972 o971 b972
2158 H h972 x_1 t972
2159 S s972 t726 h h754 h757 h921 h972
2160 G s972 t924
2161 B b973 s972
2162 T t973 o747 b973 b914
2163 B b974 t973
2164 T t974 o746 b974 b4 b970
2165 B b975 t974
2166 T t975 o b975 b4
2167 B b976 t975
2168 T t976 o b971 b976
2169 B b977 t976
2170 T t977 o745 b940 b977
2171 B b978 t977
2172 P p978 String "hypSubstT 5 0 ttca thenT rwh reduceC 0 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
2173 O o978 ext_rule p978
2174 P p980 String "rwh unfold_power 0 thenT rwh reduce_ind_down 0 ttca"
2175 O o980 ext_rule p980
2176 T t980 o603 b587 b896 b918
2177 B b981 t980
2178 T t981 o603 b587 b981 b896
2179 B b982 t981
2180 T t982 o603 b587 b896 b920
2181 B b983 t982
2182 T t983 o888 b733 b886 b982 b983
2183 S s983 t726 h h754 h757 h921 h972
2184 G s983 t983
2185 B b984 s983
2186 T t984 o747 b984 b914
2187 B b985 t984
2188 B b986 t980 i j
2189 T t986 o610 b758 b606
2190 B b987 t986
2191 T t987 o586 b587 b622 b987
2192 B b988 t987
2193 T t988 o603 b587 b622 b988
2194 B b989 t988 k l
2195 T t989 o602 b758 b986 b610 b989
2196 B b990 t989
2197 T t990 o603 b587 b990 b896
2198 B b991 t990
2199 B b992 t982 i j
2200 T t992 o603 b587 b622 b955
2201 B b993 t992 k l
2202 T t993 o602 b755 b992 b610 b993
2203 B b994 t993
2204 T t994 o888 b733 b886 b991 b994
2205 S s994 t726 h h754 h757 h921 h972
2206 G s994 t994
2207 B b995 s994
2208 T t995 o747 b995 b914
2209 B b996 t995
2210 T t996 o2 b975
2211 B b997 t996
2212 T t997 o746 b996 b4 b997
2213 B b998 t997
2214 T t998 o2 b998
2215 B b999 t998
2216 T t999 o746 b985 b4 b999
2217 B b1000 t999
2218 T t1000 o754 b758 b756
2219 S s1000 t726 h h754 h757 h921 h972
2220 G s1000 t1000
2221 B b1001 s1000
2222 T t1001 o747 b1001 b914
2223 B b1002 t1001
2224 T t1002 o774 b1002 b4 b999
2225 B b1003 t1002
2226 T t1003 o b1003 b4
2227 B b1004 t1003
2228 T t1004 o b1000 b1004
2229 B b1005 t1004
2230 T t1005 o745 b975 b1005
2231 B b1006 t1005
2232 P p1006 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; inv{'g; 'x}; power{'g; 'x; (('m +@ 1) +@ 1)}}; inv{'g; 'x}}; op{'g; inv{'g; 'x}; op{'g; power{'g; 'x; (('m +@ 1) +@ 1)}; inv{'g; 'x}}}} >> 0 ttca"
2233 O o1006 ext_rule p1006
2234 P p1008 String "splitIntT << 'm >> << minus{1} >> thenT autoT"
2235 O o1008 ext_rule p1008
2236 T t1008 o754 b755 b967
2237 H h1008 w t1008
2238 S s1008 t721 h h754 h757 h921 h972 h1008
2239 G s1008 t1000
2240 B b1009 s1008
2241 T t1009 o747 b1009 b914
2242 B b1010 t1009
2243 NItt_squash Itt_squash Itt_squash NIL
2244 NItt_squash!squash squash1010 squash Itt_squash
2245 O o1010 squash1010
2246 B b1011 t1000
2247 T t1011 o1010 b1011
2248 S s1011 t721 h h754 h757 h921 h972 h1008
2249 G s1011 t1011
2250 B b1012 s1011
2251 T t1012 o747 b1012 b914
2252 B b1013 t1012
2253 S s1013 t726 h h754 h757 h921 h972 h1008
2254 G s1013 t1000
2255 B b1014 s1013
2256 T t1014 o747 b1014 b914
2257 B b1015 t1014
2258 T t1015 o2 b1003
2259 B b1016 t1015
2260 T t1016 o746 b1015 b4 b1016
2261 B b1017 t1016
2262 T t1017 o2 b1017
2263 B b1018 t1017
2264 T t1018 o746 b1013 b4 b1018
2265 B b1019 t1018
2266 T t1019 o2 b1019
2267 B b1020 t1019
2268 T t1020 o746 b1010 b4 b1020
2269 B b1021 t1020
2270 T t1021 o754 b967 b755
2271 H h1021 w t1021
2272 S s1021 t721 h h754 h757 h921 h972 h1021
2273 G s1021 t1000
2274 B b1022 s1021
2275 T t1022 o747 b1022 b914
2276 B b1023 t1022
2277 S s1023 t721 h h754 h757 h921 h972 h1021
2278 G s1023 t1011
2279 B b1024 s1023
2280 T t1024 o747 b1024 b914
2281 B b1025 t1024
2282 S s1025 t726 h h754 h757 h921 h972 h1021
2283 G s1025 t1000
2284 B b1026 s1025
2285 T t1026 o747 b1026 b914
2286 B b1027 t1026
2287 T t1027 o746 b1027 b4 b1016
2288 B b1028 t1027
2289 T t1028 o2 b1028
2290 B b1029 t1028
2291 T t1029 o746 b1025 b4 b1029
2292 B b1030 t1029
2293 T t1030 o2 b1030
2294 B b1031 t1030
2295 T t1031 o746 b1023 b4 b1031
2296 B b1032 t1031
2297 T t1032 o b1032 b4
2298 B b1033 t1032
2299 T t1033 o b1021 b1033
2300 B b1034 t1033
2301 T t1034 o745 b1003 b1034
2302 B b1035 t1034
2303 P p1035 String "rwh unfold_lt 6 thenT rwh (lt_addMonoC << 1 >>) 6 thenT autoT thenT rwh reduceC 6 thenT rwh unfold_lt 0 thenT autoT"
2304 O o1035 ext_rule p1035
2305 T t1035 o745 b1021 b4
2306 B b1036 t1035
2307 T t1036 o1035 b744 b1036 b4 b4
2308 B b1037 t1036
2309 P p1037 String "assertT << \"false\">> ttca thenT rwh unfold_lt 6 thenT rwh lt_DiscretC 6 thenT autoT thenT rwh reduceC 6 thenT dT 6 ttca"
2310 O o1037 ext_rule p1037
2311 NItt_bool Itt_bool Itt_bool NIL
2312 NItt_bool!assert assert assert Itt_bool
2313 O o1038 assert
2314 NItt_int_base!beq_int beq_int beq_int Itt_int_base
2315 O o1039 beq_int
2316 T t1039 o1039 b756 b755
2317 B b1039 t1039
2318 T t1040 o1038 b1039
2319 H h1040 w t1040
2320 NItt_logic!false false false Itt_logic
2321 O o1040 false
2322 T t1041 o1040
2323 S s1041 t721 h h754 h757 h921 h972 h1040
2324 G s1041 t1041
2325 B b1041 s1041
2326 T t1042 o747 b1041 b914
2327 B b1042 t1042
2328 NItt_bool!bor bor bor Itt_bool
2329 O o1042 bor
2330 NItt_int_base!lt_bool lt_bool lt_bool Itt_int_base
2331 O o1043 lt_bool
2332 T t1043 o1043 b756 b755
2333 B b1043 t1043
2334 T t1044 o1042 b1039 b1043
2335 B b1044 t1044
2336 T t1045 o1038 b1044
2337 H h1045 w t1045
2338 S s1045 t721 h h754 h757 h921 h972 h1045
2339 G s1045 t1041
2340 B b1045 s1045
2341 T t1046 o747 b1045 b914
2342 B b1046 t1046
2343 P p1046 Number -1
2344 O o1046 number p1046
2345 T t1047 o1046
2346 B b1047 t1047
2347 T t1048 o605 b1047 b606
2348 B b1048 t1048
2349 T t1049 o1043 b1048 b755
2350 B b1049 t1049
2351 T t1050 o1042 b1039 b1049
2352 B b1050 t1050
2353 T t1051 o1038 b1050
2354 H h1051 w t1051
2355 S s1051 t721 h h754 h757 h921 h972 h1051
2356 G s1051 t1041
2357 B b1051 s1051
2358 T t1052 o747 b1051 b914
2359 B b1052 t1052
2360 T t1053 o1039 b1048 b755
2361 B b1053 t1053
2362 T t1054 o1042 b1053 b1049
2363 B b1054 t1054
2364 T t1055 o1038 b1054
2365 H h1055 w t1055
2366 S s1055 t721 h h754 h757 h921 h972 h1055
2367 G s1055 t1041
2368 B b1055 s1055
2369 T t1056 o747 b1055 b914
2370 B b1056 t1056
2371 T t1057 o605 b967 b606
2372 B b1057 t1057
2373 T t1058 o1043 b1057 b755
2374 B b1058 t1058
2375 T t1059 o1042 b1053 b1058
2376 B b1059 t1059
2377 T t1060 o1038 b1059
2378 H h1060 w t1060
2379 S s1060 t721 h h754 h757 h921 h972 h1060
2380 G s1060 t1041
2381 B b1060 s1060
2382 T t1061 o747 b1060 b914
2383 B b1061 t1061
2384 T t1062 o1039 b1057 b755
2385 B b1062 t1062
2386 T t1063 o1042 b1062 b1058
2387 B b1063 t1063
2388 T t1064 o1038 b1063
2389 H h1064 w t1064
2390 S s1064 t721 h h754 h757 h921 h972 h1064
2391 G s1064 t1041
2392 B b1064 s1064
2393 T t1065 o747 b1064 b914
2394 B b1065 t1065
2395 T t1066 o1043 b967 b755
2396 B b1066 t1066
2397 T t1067 o1038 b1066
2398 H h1067 w t1067
2399 S s1067 t721 h h754 h757 h921 h972 h1067
2400 G s1067 t1041
2401 B b1067 s1067
2402 T t1068 o747 b1067 b914
2403 B b1068 t1068
2404 S s1068 t721 h h754 h757 h921 h972 h1021
2405 G s1068 t1041
2406 B b1069 s1068
2407 T t1069 o747 b1069 b914
2408 B b1070 t1069
2409 T t1070 o2 b1032
2410 B b1071 t1070
2411 T t1071 o774 b1070 b4 b1071
2412 B b1072 t1071
2413 T t1072 o2 b1072
2414 B b1073 t1072
2415 T t1073 o774 b1068 b4 b1073
2416 B b1074 t1073
2417 T t1074 o2 b1074
2418 B b1075 t1074
2419 T t1075 o774 b1065 b4 b1075
2420 B b1076 t1075
2421 T t1076 o2 b1076
2422 B b1077 t1076
2423 T t1077 o774 b1061 b4 b1077
2424 B b1078 t1077
2425 T t1078 o2 b1078
2426 B b1079 t1078
2427 T t1079 o774 b1056 b4 b1079
2428 B b1080 t1079
2429 T t1080 o2 b1080
2430 B b1081 t1080
2431 T t1081 o774 b1052 b4 b1081
2432 B b1082 t1081
2433 T t1082 o2 b1082
2434 B b1083 t1082
2435 T t1083 o774 b1046 b4 b1083
2436 B b1084 t1083
2437 T t1084 o2 b1084
2438 B b1085 t1084
2439 T t1085 o746 b1042 b4 b1085
2440 B b1086 t1085
2441 T t1086 o1038 b1043
2442 H h1086 w t1086
2443 S s1086 t721 h h754 h757 h921 h972 h1086
2444 G s1086 t1041
2445 B b1087 s1086
2446 T t1087 o747 b1087 b914
2447 B b1088 t1087
2448 T t1088 o746 b1088 b4 b1085
2449 B b1089 t1088
2450 T t1089 o b1089 b4
2451 B b1090 t1089
2452 T t1090 o b1086 b1090
2453 B b1091 t1090
2454 T t1091 o745 b1032 b1091
2455 B b1092 t1091
2456 P p1092 String "dT 6 ttca thenT hypSubstT 6 3 ttca thenT lt_AsymT << 'm >> << 'm >> ttca"
2457 O o1092 ext_rule p1092
2458 T t1092 o745 b1086 b4
2459 B b1093 t1092
2460 T t1093 o1092 b744 b1093 b4 b4
2461 B b1094 t1093
2462 P p1094 String "lt_AsymT << 'm >> << 0 >> ttca thenT rwh unfold_lt 0 ttca"
2463 O o1094 ext_rule p1094
2464 T t1094 o745 b1089 b4
2465 B b1095 t1094
2466 T t1095 o1094 b744 b1095 b4 b4
2467 B b1096 t1095
2468 T t1096 o b1096 b4
2469 B b1097 t1096
2470 T t1097 o b1094 b1097
2471 B b1098 t1097
2472 T t1098 o1037 b744 b1092 b1098 b4
2473 B b1099 t1098
2474 T t1099 o b1099 b4
2475 B b1100 t1099
2476 T t1100 o b1037 b1100
2477 B b1101 t1100
2478 T t1101 o1008 b744 b1035 b1101 b4
2479 B b1102 t1101
2480 T t1102 o b1102 b4
2481 B b1103 t1102
2482 P p1108 String "rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
2483 O o1108 ext_rule p1108
2484 T t1108 o603 b587 b622 b610
2485 B b1109 t1108
2486 T t1109 o603 b587 b1109 b896
2487 B b1110 t1109
2488 T t1110 o888 b733 b886 b1110 b610
2489 S s1110 t726 h
2490 G s1110 t1110
2491 B b1111 s1110
2492 T t1111 o747 b1111 b914
2493 B b1112 t1111
2494 NItt_bool!ifthenelse ifthenelse ifthenelse Itt_bool
2495 O o1112 ifthenelse
2496 NItt_bool!btrue btrue btrue Itt_bool
2497 O o1113 btrue
2498 T t1113 o1113
2499 B b1113 t1113
2500 T t1114 o603 b587 b896 b942
2501 B b1114 t1114
2502 T t1115 o1112 b1113 b610 b1114
2503 B b1115 t1115
2504 T t1116 o603 b587 b622 b1115
2505 B b1116 t1116
2506 T t1117 o603 b587 b1116 b896
2507 B b1117 t1117
2508 T t1118 o888 b733 b886 b1117 b610
2509 S s1118 t726 h
2510 G s1118 t1118
2511 B b1118 s1118
2512 T t1119 o747 b1118 b914
2513 B b1119 t1119
2514 T t1120 o1039 b756 b756
2515 B b1120 t1120
2516 T t1121 o1112 b1120 b610 b1114
2517 B b1121 t1121
2518 T t1122 o603 b587 b622 b1121
2519 B b1122 t1122
2520 T t1123 o603 b587 b1122 b896
2521 B b1123 t1123
2522 T t1124 o888 b733 b886 b1123 b610
2523 S s1124 t726 h
2524 G s1124 t1124
2525 B b1124 s1124
2526 T t1125 o747 b1124 b914
2527 B b1125 t1125
2528 NItt_bool!bfalse bfalse bfalse Itt_bool
2529 O o1125 bfalse
2530 T t1126 o1125
2531 B b1126 t1126
2532 T t1127 o610 b756 b606
2533 B b1127 t1127
2534 T t1128 o586 b587 b622 b1127
2535 B b1128 t1128
2536 T t1129 o603 b587 b622 b1128
2537 B b1129 t1129
2538 T t1130 o1112 b1126 b1129 b1114
2539 B b1130 t1130
2540 T t1131 o1112 b1120 b610 b1130
2541 B b1131 t1131
2542 T t1132 o603 b587 b622 b1131
2543 B b1132 t1132
2544 T t1133 o603 b587 b1132 b896
2545 B b1133 t1133
2546 T t1134 o888 b733 b886 b1133 b610
2547 S s1134 t726 h
2548 G s1134 t1134
2549 B b1134 s1134
2550 T t1135 o747 b1134 b914
2551 B b1135 t1135
2552 B b1136 t1114 i j
2553 B b1137 t1129 k l
2554 T t1137 o602 b756 b1136 b610 b1137
2555 B b1138 t1137
2556 T t1138 o603 b587 b622 b1138
2557 B b1139 t1138
2558 T t1139 o603 b587 b1139 b896
2559 B b1140 t1139
2560 T t1140 o888 b733 b886 b1140 b610
2561 S s1140 t726 h
2562 G s1140 t1140
2563 B b1141 s1140
2564 T t1141 o747 b1141 b914
2565 B b1142 t1141
2566 T t1142 o603 b587 b622 b944
2567 B b1143 t1142
2568 T t1143 o603 b587 b1143 b896
2569 B b1144 t1143
2570 T t1144 o888 b733 b886 b1144 b610
2571 S s1144 t726 h
2572 G s1144 t1144
2573 B b1145 s1144
2574 T t1145 o747 b1145 b914
2575 B b1146 t1145
2576 T t1146 o610 b606 b606
2577 B b1147 t1146
2578 T t1147 o586 b587 b622 b1147
2579 B b1148 t1147
2580 T t1148 o603 b587 b622 b1148
2581 B b1149 t1148
2582 T t1149 o603 b587 b1149 b896
2583 B b1150 t1149
2584 T t1150 o888 b733 b886 b1150 b610
2585 S s1150 t726 h
2586 G s1150 t1150
2587 B b1151 s1150
2588 T t1151 o747 b1151 b914
2589 B b1152 t1151
2590 T t1152 o888 b733 b886 b1150 b1115
2591 S s1152 t726 h
2592 G s1152 t1152
2593 B b1153 s1152
2594 T t1153 o747 b1153 b914
2595 B b1154 t1153
2596 T t1154 o888 b733 b886 b1150 b1121
2597 S s1154 t726 h
2598 G s1154 t1154
2599 B b1155 s1154
2600 T t1155 o747 b1155 b914
2601 B b1156 t1155
2602 T t1156 o888 b733 b886 b1150 b1131
2603 S s1156 t726 h
2604 G s1156 t1156
2605 B b1157 s1156
2606 T t1157 o747 b1157 b914
2607 B b1158 t1157
2608 T t1158 o888 b733 b886 b1150 b1138
2609 S s1158 t726 h
2610 G s1158 t1158
2611 B b1159 s1158
2612 T t1159 o747 b1159 b914
2613 B b1160 t1159
2614 T t1160 o1112 b1126 b610 b1149
2615 B b1161 t1160
2616 T t1161 o603 b587 b1161 b896
2617 B b1162 t1161
2618 T t1162 o888 b733 b886 b1162 b1138
2619 S s1162 t726 h
2620 G s1162 t1162
2621 B b1163 s1162
2622 T t1163 o747 b1163 b914
2623 B b1164 t1163
2624 T t1164 o1039 b606 b756
2625 B b1165 t1164
2626 T t1165 o1112 b1165 b610 b1149
2627 B b1166 t1165
2628 T t1166 o603 b587 b1166 b896
2629 B b1167 t1166
2630 T t1167 o888 b733 b886 b1167 b1138
2631 S s1167 t726 h
2632 G s1167 t1167
2633 B b1168 s1167
2634 T t1168 o747 b1168 b914
2635 B b1169 t1168
2636 T t1169 o605 b606 b606
2637 B b1170 t1169
2638 T t1170 o586 b587 b622 b1170
2639 B b1171 t1170
2640 T t1171 o603 b587 b896 b1171
2641 B b1172 t1171
2642 T t1172 o1112 b1113 b1149 b1172
2643 B b1173 t1172
2644 T t1173 o1112 b1165 b610 b1173
2645 B b1174 t1173
2646 T t1174 o603 b587 b1174 b896
2647 B b1175 t1174
2648 T t1175 o888 b733 b886 b1175 b1138
2649 S s1175 t726 h
2650 G s1175 t1175
2651 B b1176 s1175
2652 T t1176 o747 b1176 b914
2653 B b1177 t1176
2654 B b1178 t1171 i j
2655 B b1179 t1148 k l
2656 T t1179 o602 b606 b1178 b610 b1179
2657 B b1180 t1179
2658 T t1180 o603 b587 b1180 b896
2659 B b1181 t1180
2660 T t1181 o888 b733 b886 b1181 b1138
2661 S s1181 t726 h
2662 G s1181 t1181
2663 B b1182 s1181
2664 T t1182 o747 b1182 b914
2665 B b1183 t1182
2666 T t1183 o586 b587 b622 b606
2667 B b1184 t1183
2668 T t1184 o603 b587 b1184 b896
2669 B b1185 t1184
2670 T t1185 o888 b733 b886 b1185 b944
2671 S s1185 t726 h
2672 G s1185 t1185
2673 B b1186 s1185
2674 T t1186 o747 b1186 b914
2675 B b1187 t1186
2676 T t1187 o2 b951
2677 B b1188 t1187
2678 T t1188 o746 b1187 b4 b1188
2679 B b1189 t1188
2680 T t1189 o2 b1189
2681 B b1190 t1189
2682 T t1190 o746 b1183 b4 b1190
2683 B b1191 t1190
2684 T t1191 o2 b1191
2685 B b1192 t1191
2686 T t1192 o746 b1177 b4 b1192
2687 B b1193 t1192
2688 T t1193 o2 b1193
2689 B b1194 t1193
2690 T t1194 o746 b1169 b4 b1194
2691 B b1195 t1194
2692 T t1195 o2 b1195
2693 B b1196 t1195
2694 T t1196 o746 b1164 b4 b1196
2695 B b1197 t1196
2696 T t1197 o2 b1197
2697 B b1198 t1197
2698 T t1198 o746 b1160 b4 b1198
2699 B b1199 t1198
2700 T t1199 o2 b1199
2701 B b1200 t1199
2702 T t1200 o746 b1158 b4 b1200
2703 B b1201 t1200
2704 T t1201 o2 b1201
2705 B b1202 t1201
2706 T t1202 o746 b1156 b4 b1202
2707 B b1203 t1202
2708 T t1203 o2 b1203
2709 B b1204 t1203
2710 T t1204 o746 b1154 b4 b1204
2711 B b1205 t1204
2712 T t1205 o2 b1205
2713 B b1206 t1205
2714 T t1206 o746 b1152 b4 b1206
2715 B b1207 t1206
2716 T t1207 o2 b1207
2717 B b1208 t1207
2718 T t1208 o746 b1146 b4 b1208
2719 B b1209 t1208
2720 T t1209 o2 b1209
2721 B b1210 t1209
2722 T t1210 o746 b1142 b4 b1210
2723 B b1211 t1210
2724 T t1211 o2 b1211
2725 B b1212 t1211
2726 T t1212 o746 b1135 b4 b1212
2727 B b1213 t1212
2728 T t1213 o2 b1213
2729 B b1214 t1213
2730 T t1214 o746 b1125 b4 b1214
2731 B b1215 t1214
2732 T t1215 o2 b1215
2733 B b1216 t1215
2734 T t1216 o746 b1119 b4 b1216
2735 B b1217 t1216
2736 T t1217 o2 b1217
2737 B b1218 t1217
2738 T t1218 o746 b1112 b4 b1218
2739 B b1219 t1218
2740 T t1219 o b1219 b4
2741 B b1220 t1219
2742 T t1220 o745 b951 b1220
2743 B b1221 t1220
2744 P p1221 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; id{'g}}; 'x} >> 0 ttca"
2745 O o1221 ext_rule p1221
2746 P p1225 String "decideT << 'm = 1 in int >> ttca"
2747 O o1225 ext_rule p1225
2748 T t1225 o721 b621 b755 b606
2749 H h1225 x_1 t1225
2750 S s1225 t726 h h754 h791 h955 h1225
2751 G s1225 t924
2752 B b1226 s1225
2753 T t1226 o747 b1226 b914
2754 B b1227 t1226
2755 T t1227 o2 b962
2756 B b1228 t1227
2757 T t1228 o746 b1227 b4 b1228
2758 B b1229 t1228
2759 B b1230 t1225
2760 T t1230 o971 b1230
2761 H h1230 x_1 t1230
2762 S s1230 t726 h h754 h791 h955 h1230
2763 G s1230 t924
2764 B b1231 s1230
2765 T t1231 o747 b1231 b914
2766 B b1232 t1231
2767 T t1232 o746 b1232 b4 b1228
2768 B b1233 t1232
2769 T t1233 o b1233 b4
2770 B b1234 t1233
2771 T t1234 o b1229 b1234
2772 B b1235 t1234
2773 T t1235 o745 b962 b1235
2774 B b1236 t1235
2775 P p1236 String "hypSubstT 5 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 thenT rwh unfold_power 0 thenT rwh reduceC 0"
2776 O o1236 ext_rule p1236
2777 T t1236 o603 b587 b622 b1143
2778 B b1237 t1236
2779 T t1237 o603 b587 b1237 b896
2780 B b1238 t1237
2781 T t1238 o888 b733 b886 b1238 b1109
2782 S s1238 t726 h h754 h791 h955 h1225
2783 G s1238 t1238
2784 B b1239 s1238
2785 T t1239 o747 b1239 b914
2786 B b1240 t1239
2787 T t1240 o603 b587 b622 b1149
2788 B b1241 t1240
2789 T t1241 o603 b587 b1241 b896
2790 B b1242 t1241
2791 T t1242 o888 b733 b886 b1242 b1109
2792 S s1242 t726 h h754 h791 h955 h1225
2793 G s1242 t1242
2794 B b1243 s1242
2795 T t1243 o747 b1243 b914
2796 B b1244 t1243
2797 T t1244 o888 b733 b886 b1242 b1116
2798 S s1244 t726 h h754 h791 h955 h1225
2799 G s1244 t1244
2800 B b1245 s1244
2801 T t1245 o747 b1245 b914
2802 B b1246 t1245
2803 T t1246 o888 b733 b886 b1242 b1122
2804 S s1246 t726 h h754 h791 h955 h1225
2805 G s1246 t1246
2806 B b1247 s1246
2807 T t1247 o747 b1247 b914
2808 B b1248 t1247
2809 T t1248 o888 b733 b886 b1242 b1132
2810 S s1248 t726 h h754 h791 h955 h1225
2811 G s1248 t1248
2812 B b1249 s1248
2813 T t1249 o747 b1249 b914
2814 B b1250 t1249
2815 T t1250 o888 b733 b886 b1242 b1139
2816 S s1250 t726 h h754 h791 h955 h1225
2817 G s1250 t1250
2818 B b1251 s1250
2819 T t1251 o747 b1251 b914
2820 B b1252 t1251
2821 T t1252 o603 b587 b622 b1161
2822 B b1253 t1252
2823 T t1253 o603 b587 b1253 b896
2824 B b1254 t1253
2825 T t1254 o888 b733 b886 b1254 b1139
2826 S s1254 t726 h h754 h791 h955 h1225
2827 G s1254 t1254
2828 B b1255 s1254
2829 T t1255 o747 b1255 b914
2830 B b1256 t1255
2831 T t1256 o603 b587 b622 b1166
2832 B b1257 t1256
2833 T t1257 o603 b587 b1257 b896
2834 B b1258 t1257
2835 T t1258 o888 b733 b886 b1258 b1139
2836 S s1258 t726 h h754 h791 h955 h1225
2837 G s1258 t1258
2838 B b1259 s1258
2839 T t1259 o747 b1259 b914
2840 B b1260 t1259
2841 T t1260 o603 b587 b622 b1174
2842 B b1261 t1260
2843 T t1261 o603 b587 b1261 b896
2844 B b1262 t1261
2845 T t1262 o888 b733 b886 b1262 b1139
2846 S s1262 t726 h h754 h791 h955 h1225
2847 G s1262 t1262
2848 B b1263 s1262
2849 T t1263 o747 b1263 b914
2850 B b1264 t1263
2851 T t1264 o603 b587 b622 b1180
2852 B b1265 t1264
2853 T t1265 o603 b587 b1265 b896
2854 B b1266 t1265
2855 T t1266 o888 b733 b886 b1266 b1139
2856 S s1266 t726 h h754 h791 h955 h1225
2857 G s1266 t1266
2858 B b1267 s1266
2859 T t1267 o747 b1267 b914
2860 B b1268 t1267
2861 T t1268 o603 b587 b622 b1184
2862 B b1269 t1268
2863 T t1269 o603 b587 b1269 b896
2864 B b1270 t1269
2865 T t1270 o888 b733 b886 b1270 b1143
2866 S s1270 t726 h h754 h791 h955 h1225
2867 G s1270 t1270
2868 B b1271 s1270
2869 T t1271 o747 b1271 b914
2870 B b1272 t1271
2871 P p1272 Number 2
2872 O o1272 number p1272
2873 T t1272 o1272
2874 B b1273 t1272
2875 T t1273 o610 b1273 b606
2876 B b1274 t1273
2877 T t1274 o586 b587 b622 b1274
2878 B b1275 t1274
2879 T t1275 o603 b587 b622 b1275
2880 B b1276 t1275
2881 T t1276 o603 b587 b1276 b896
2882 B b1277 t1276
2883 T t1277 o888 b733 b886 b1277 b1143
2884 S s1277 t726 h h754 h791 h955 h1225
2885 G s1277 t1277
2886 B b1278 s1277
2887 T t1278 o747 b1278 b914
2888 B b1279 t1278
2889 T t1279 o888 b733 b886 b1277 b1149
2890 S s1279 t726 h h754 h791 h955 h1225
2891 G s1279 t1279
2892 B b1280 s1279
2893 T t1280 o747 b1280 b914
2894 B b1281 t1280
2895 T t1281 o1112 b1126 b610 b1276
2896 B b1282 t1281
2897 T t1282 o603 b587 b1282 b896
2898 B b1283 t1282
2899 T t1283 o888 b733 b886 b1283 b1149
2900 S s1283 t726 h h754 h791 h955 h1225
2901 G s1283 t1283
2902 B b1284 s1283
2903 T t1284 o747 b1284 b914
2904 B b1285 t1284
2905 T t1285 o1039 b1273 b756
2906 B b1286 t1285
2907 T t1286 o1112 b1286 b610 b1276
2908 B b1287 t1286
2909 T t1287 o603 b587 b1287 b896
2910 B b1288 t1287
2911 T t1288 o888 b733 b886 b1288 b1149
2912 S s1288 t726 h h754 h791 h955 h1225
2913 G s1288 t1288
2914 B b1289 s1288
2915 T t1289 o747 b1289 b914
2916 B b1290 t1289
2917 T t1290 o605 b1273 b606
2918 B b1291 t1290
2919 T t1291 o586 b587 b622 b1291
2920 B b1292 t1291
2921 T t1292 o603 b587 b896 b1292
2922 B b1293 t1292
2923 T t1293 o1112 b1113 b1276 b1293
2924 B b1294 t1293
2925 T t1294 o1112 b1286 b610 b1294
2926 B b1295 t1294
2927 T t1295 o603 b587 b1295 b896
2928 B b1296 t1295
2929 T t1296 o888 b733 b886 b1296 b1149
2930 S s1296 t726 h h754 h791 h955 h1225
2931 G s1296 t1296
2932 B b1297 s1296
2933 T t1297 o747 b1297 b914
2934 B b1298 t1297
2935 B b1299 t1292 i j
2936 B b1300 t1275 k l
2937 T t1300 o602 b1273 b1299 b610 b1300
2938 B b1301 t1300
2939 T t1301 o603 b587 b1301 b896
2940 B b1302 t1301
2941 T t1302 o888 b733 b886 b1302 b1149
2942 S s1302 t726 h h754 h791 h955 h1225
2943 G s1302 t1302
2944 B b1303 s1302
2945 T t1303 o747 b1303 b914
2946 B b1304 t1303
2947 T t1304 o888 b733 b886 b1302 b1161
2948 S s1304 t726 h h754 h791 h955 h1225
2949 G s1304 t1304
2950 B b1305 s1304
2951 T t1305 o747 b1305 b914
2952 B b1306 t1305
2953 T t1306 o888 b733 b886 b1302 b1166
2954 S s1306 t726 h h754 h791 h955 h1225
2955 G s1306 t1306
2956 B b1307 s1306
2957 T t1307 o747 b1307 b914
2958 B b1308 t1307
2959 T t1308 o888 b733 b886 b1302 b1174
2960 S s1308 t726 h h754 h791 h955 h1225
2961 G s1308 t1308
2962 B b1309 s1308
2963 T t1309 o747 b1309 b914
2964 B b1310 t1309
2965 T t1310 o888 b733 b886 b1302 b1180
2966 S s1310 t726 h h754 h791 h955 h1225
2967 G s1310 t1310
2968 B b1311 s1310
2969 T t1311 o747 b1311 b914
2970 B b1312 t1311
2971 T t1312 o610 b1170 b606
2972 B b1313 t1312
2973 T t1313 o586 b587 b622 b1313
2974 B b1314 t1313
2975 T t1314 o603 b587 b622 b1314
2976 B b1315 t1314 k l
2977 T t1315 o602 b1273 b1299 b610 b1315
2978 B b1316 t1315
2979 T t1316 o603 b587 b1316 b896
2980 B b1317 t1316
2981 T t1317 o888 b733 b886 b1317 b1180
2982 S s1317 t726 h h754 h791 h955 h1225
2983 G s1317 t1317
2984 B b1318 s1317
2985 T t1318 o747 b1318 b914
2986 B b1319 t1318
2987 T t1319 o605 b1170 b606
2988 B b1320 t1319
2989 T t1320 o586 b587 b622 b1320
2990 B b1321 t1320
2991 T t1321 o603 b587 b896 b1321
2992 B b1322 t1321 i j
2993 T t1322 o602 b1273 b1322 b610 b1315
2994 B b1323 t1322
2995 T t1323 o603 b587 b1323 b896
2996 B b1324 t1323
2997 T t1324 o888 b733 b886 b1324 b1180
2998 S s1324 t726 h h754 h791 h955 h1225
2999 G s1324 t1324
3000 B b1325 s1324
3001 T t1325 o747 b1325 b914
3002 B b1326 t1325
3003 T t1326 o602 b1170 b1322 b610 b1315
3004 B b1327 t1326
3005 T t1327 o603 b587 b1327 b896
3006 B b1328 t1327
3007 T t1328 o888 b733 b886 b1328 b1180
3008 S s1328 t726 h h754 h791 h955 h1225
3009 G s1328 t1328
3010 B b1329 s1328
3011 T t1329 o747 b1329 b914
3012 B b1330 t1329
3013 T t1330 o603 b587 b1171 b896
3014 B b1331 t1330
3015 T t1331 o888 b733 b886 b1331 b1184
3016 S s1331 t726 h h754 h791 h955 h1225
3017 G s1331 t1331
3018 B b1332 s1331
3019 T t1332 o747 b1332 b914
3020 B b1333 t1332
3021 T t1333 o2 b1229
3022 B b1334 t1333
3023 T t1334 o746 b1333 b4 b1334
3024 B b1335 t1334
3025 T t1335 o2 b1335
3026 B b1336 t1335
3027 T t1336 o746 b1330 b4 b1336
3028 B b1337 t1336
3029 T t1337 o2 b1337
3030 B b1338 t1337
3031 T t1338 o746 b1326 b4 b1338
3032 B b1339 t1338
3033 T t1339 o2 b1339
3034 B b1340 t1339
3035 T t1340 o746 b1319 b4 b1340
3036 B b1341 t1340
3037 T t1341 o2 b1341
3038 B b1342 t1341
3039 T t1342 o746 b1312 b4 b1342
3040 B b1343 t1342
3041 T t1343 o2 b1343
3042 B b1344 t1343
3043 T t1344 o746 b1310 b4 b1344
3044 B b1345 t1344
3045 T t1345 o2 b1345
3046 B b1346 t1345
3047 T t1346 o746 b1308 b4 b1346
3048 B b1347 t1346
3049 T t1347 o2 b1347
3050 B b1348 t1347
3051 T t1348 o746 b1306 b4 b1348
3052 B b1349 t1348
3053 T t1349 o2 b1349
3054 B b1350 t1349
3055 T t1350 o746 b1304 b4 b1350
3056 B b1351 t1350
3057 T t1351 o2 b1351
3058 B b1352 t1351
3059 T t1352 o746 b1298 b4 b1352
3060 B b1353 t1352
3061 T t1353 o2 b1353
3062 B b1354 t1353
3063 T t1354 o746 b1290 b4 b1354
3064 B b1355 t1354
3065 T t1355 o2 b1355
3066 B b1356 t1355
3067 T t1356 o746 b1285 b4 b1356
3068 B b1357 t1356
3069 T t1357 o2 b1357
3070 B b1358 t1357
3071 T t1358 o746 b1281 b4 b1358
3072 B b1359 t1358
3073 T t1359 o2 b1359
3074 B b1360 t1359
3075 T t1360 o746 b1279 b4 b1360
3076 B b1361 t1360
3077 T t1361 o2 b1361
3078 B b1362 t1361
3079 T t1362 o746 b1272 b4 b1362
3080 B b1363 t1362
3081 T t1363 o2 b1363
3082 B b1364 t1363
3083 T t1364 o746 b1268 b4 b1364
3084 B b1365 t1364
3085 T t1365 o2 b1365
3086 B b1366 t1365
3087 T t1366 o746 b1264 b4 b1366
3088 B b1367 t1366
3089 T t1367 o2 b1367
3090 B b1368 t1367
3091 T t1368 o746 b1260 b4 b1368
3092 B b1369 t1368
3093 T t1369 o2 b1369
3094 B b1370 t1369
3095 T t1370 o746 b1256 b4 b1370
3096 B b1371 t1370
3097 T t1371 o2 b1371
3098 B b1372 t1371
3099 T t1372 o746 b1252 b4 b1372
3100 B b1373 t1372
3101 T t1373 o2 b1373
3102 B b1374 t1373
3103 T t1374 o746 b1250 b4 b1374
3104 B b1375 t1374
3105 T t1375 o2 b1375
3106 B b1376 t1375
3107 T t1376 o746 b1248 b4 b1376
3108 B b1377 t1376
3109 T t1377 o2 b1377
3110 B b1378 t1377
3111 T t1378 o746 b1246 b4 b1378
3112 B b1379 t1378
3113 T t1379 o2 b1379
3114 B b1380 t1379
3115 T t1380 o746 b1244 b4 b1380
3116 B b1381 t1380
3117 T t1381 o2 b1381
3118 B b1382 t1381
3119 T t1382 o746 b1240 b4 b1382
3120 B b1383 t1382
3121 T t1383 o b1383 b4
3122 B b1384 t1383
3123 T t1384 o745 b1229 b1384
3124 B b1385 t1384
3125 P p1385 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; id{'g}}; 'x} >> 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0"
3126 O o1385 ext_rule p1385
3127 T t1385 o603 b587 b622 b1109
3128 B b1386 t1385
3129 T t1386 o603 b587 b1386 b896
3130 B b1387 t1386
3131 T t1387 o888 b733 b886 b1387 b622
3132 S s1387 t726 h h754 h791 h955 h1225
3133 G s1387 t1387
3134 B b1388 s1387
3135 T t1388 o747 b1388 b914
3136 B b1389 t1388
3137 T t1389 o603 b587 b622 b1116
3138 B b1390 t1389
3139 T t1390 o603 b587 b1390 b896
3140 B b1391 t1390
3141 T t1391 o888 b733 b886 b1391 b622
3142 S s1391 t726 h h754 h791 h955 h1225
3143 G s1391 t1391
3144 B b1392 s1391
3145 T t1392 o747 b1392 b914
3146 B b1393 t1392
3147 T t1393 o603 b587 b622 b1122
3148 B b1394 t1393
3149 T t1394 o603 b587 b1394 b896
3150 B b1395 t1394
3151 T t1395 o888 b733 b886 b1395 b622
3152 S s1395 t726 h h754 h791 h955 h1225
3153 G s1395 t1395
3154 B b1396 s1395
3155 T t1396 o747 b1396 b914
3156 B b1397 t1396
3157 T t1397 o603 b587 b622 b1132
3158 B b1398 t1397
3159 T t1398 o603 b587 b1398 b896
3160 B b1399 t1398
3161 T t1399 o888 b733 b886 b1399 b622
3162 S s1399 t726 h h754 h791 h955 h1225
3163 G s1399 t1399
3164 B b1400 s1399
3165 T t1400 o747 b1400 b914
3166 B b1401 t1400
3167 T t1401 o603 b587 b622 b1139
3168 B b1402 t1401
3169 T t1402 o603 b587 b1402 b896
3170 B b1403 t1402
3171 T t1403 o888 b733 b886 b1403 b622
3172 S s1403 t726 h h754 h791 h955 h1225
3173 G s1403 t1403
3174 B b1404 s1403
3175 T t1404 o747 b1404 b914
3176 B b1405 t1404
3177 T t1405 o888 b733 b886 b1238 b622
3178 S s1405 t726 h h754 h791 h955 h1225
3179 G s1405 t1405
3180 B b1406 s1405
3181 T t1406 o747 b1406 b914
3182 B b1407 t1406
3183 T t1407 o2 b1383
3184 B b1408 t1407
3185 T t1408 o746 b1407 b4 b1408
3186 B b1409 t1408
3187 T t1409 o2 b1409
3188 B b1410 t1409
3189 T t1410 o746 b1405 b4 b1410
3190 B b1411 t1410
3191 T t1411 o2 b1411
3192 B b1412 t1411
3193 T t1412 o746 b1401 b4 b1412
3194 B b1413 t1412
3195 T t1413 o2 b1413
3196 B b1414 t1413
3197 T t1414 o746 b1397 b4 b1414
3198 B b1415 t1414
3199 T t1415 o2 b1415
3200 B b1416 t1415
3201 T t1416 o746 b1393 b4 b1416
3202 B b1417 t1416
3203 T t1417 o2 b1417
3204 B b1418 t1417
3205 T t1418 o746 b1389 b4 b1418
3206 B b1419 t1418
3207 T t1419 o b1419 b4
3208 B b1420 t1419
3209 T t1421 o603 b587 b622 b622
3210 B b1422 t1421
3211 T t1422 o603 b587 b1422 b896
3212 B b1423 t1422
3213 T t1423 o888 b733 b886 b1423 b622
3214 S s1423 t726 h h754 h791 h955 h1225
3215 G s1423 t1423
3216 B b1424 s1423
3217 T t1424 o747 b1424 b914
3218 B b1425 t1424
3219 T t1425 o2 b1419
3220 B b1426 t1425
3221 T t1426 o746 b1425 b4 b1426
3222 B b1427 t1426
3223 NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
3224 O o1427 equiv_fun_prop
3225 T t1427 o603 b587 b622 b588
3226 B b1428 t1427
3227 T t1428 o603 b587 b1428 b896
3228 B b1429 t1428
3229 T t1429 o888 b733 b886 b1429 b622
3230 B b1430 t1429 z
3231 T t1430 o1427 b733 b886 b1430
3232 S s1430 t726 h h754 h791 h955 h1225
3233 G s1430 t1430
3234 B b1431 s1430
3235 T t1431 o747 b1431 b914
3236 B b1432 t1431
3237 T t1432 o746 b1432 b4 b1426
3238 B b1433 t1432
3239 T t1433 o b1433 b4
3240 B b1434 t1433
3241 T t1434 o b1427 b1434
3242 B b1435 t1434
3243 P p1436 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; 'x}; inv{'g; 'x}}; op{'g; 'x; op{'g; 'x; inv{'g; 'x}}}} >> 0 ttca"
3244 O o1436 ext_rule p1436
3245 T t1436 o603 b587 b622 b896
3246 B b1437 t1436
3247 T t1437 o603 b587 b622 b1437
3248 B b1438 t1437
3249 T t1438 o888 b733 b886 b1438 b622
3250 S s1438 t726 h h754 h791 h955 h1225
3251 G s1438 t1438
3252 B b1439 s1438
3253 T t1439 o747 b1439 b914
3254 B b1440 t1439
3255 T t1440 o2 b1427
3256 B b1441 t1440
3257 T t1441 o746 b1440 b4 b1441
3258 B b1442 t1441
3259 T t1442 o b1442 b4
3260 B b1443 t1442
3261 P p1444 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; inv{'g; 'x}}; id{'g}} >> 0 ttca"
3262 O o1444 ext_rule p1444
3263 P p1448 String "autoT thenT rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 9 ttca"
3264 O o1448 ext_rule p1448
3265 P p1457 String "rwh unfold_power 0 thenT rwh reduce_ind_up 0 ttca"
3266 O o1457 ext_rule p1457
3267 B b1458 t988
3268 T t1458 o603 b587 b1458 b896
3269 B b1459 t1458
3270 B b1460 t992
3271 T t1460 o888 b733 b886 b1459 b1460
3272 S s1460 t726 h h754 h791 h955 h1230
3273 G s1460 t1460
3274 B b1461 s1460
3275 T t1461 o747 b1461 b914
3276 B b1462 t1461
3277 S s1462 t726 h h754 h791 h955 h1230
3278 G s1462 t994
3279 B b1463 s1462
3280 T t1463 o747 b1463 b914
3281 B b1464 t1463
3282 T t1464 o2 b1233
3283 B b1465 t1464
3284 T t1465 o746 b1464 b4 b1465
3285 B b1466 t1465
3286 T t1466 o2 b1466
3287 B b1467 t1466
3288 T t1467 o746 b1462 b4 b1467
3289 B b1468 t1467
3290 T t1468 o754 b756 b758
3291 S s1468 t726 h h754 h791 h955 h1230
3292 G s1468 t1468
3293 B b1469 s1468
3294 T t1469 o747 b1469 b914
3295 B b1470 t1469
3296 T t1470 o774 b1470 b4 b1467
3297 B b1471 t1470
3298 T t1471 o b1471 b4
3299 B b1472 t1471
3300 T t1472 o b1468 b1472
3301 B b1473 t1472
3302 T t1473 o745 b1233 b1473
3303 B b1474 t1473
3304 P p1474 String "rwh unfold_sub 4 thenT rwh add_normalizeC 4 thenT rwh reduceC 4 thenT rwh unfold_sub 0 thenT rwh add_normalizeC 0 ttca thenT rwh reduceC 0 ttca"
3305 O o1474 ext_rule p1474
3306 T t1474 o603 b587 b923 b896
3307 B b1475 t1474
3308 T t1475 o605 b1047 b755
3309 B b1476 t1475
3310 T t1476 o586 b587 b622 b1476
3311 B b1477 t1476
3312 T t1477 o888 b733 b886 b1475 b1477
3313 H h1477 z t1477
3314 T t1478 o603 b587 b622 b923
3315 B b1478 t1478
3316 T t1479 o603 b587 b1478 b896
3317 B b1479 t1479
3318 T t1480 o603 b587 b622 b1477
3319 B b1480 t1480
3320 T t1481 o888 b733 b886 b1479 b1480
3321 S s1481 t726 h h754 h791 h1477 h1230
3322 G s1481 t1481
3323 B b1481 s1481
3324 T t1482 o747 b1481 b914
3325 B b1482 t1482
3326 T t1483 o605 b756 b755
3327 B b1483 t1483
3328 T t1484 o586 b587 b622 b1483
3329 B b1484 t1484
3330 T t1485 o603 b587 b622 b1484
3331 B b1485 t1485
3332 T t1486 o603 b587 b1485 b896
3333 B b1486 t1486
3334 T t1487 o888 b733 b886 b1486 b1480
3335 S s1487 t726 h h754 h791 h1477 h1230
3336 G s1487 t1487
3337 B b1487 s1487
3338 T t1488 o747 b1487 b914
3339 B b1488 t1488
3340 T t1489 o605 b1048 b755
3341 B b1489 t1489
3342 T t1490 o586 b587 b622 b1489
3343 B b1490 t1490
3344 T t1491 o603 b587 b622 b1490
3345 B b1491 t1491
3346 T t1492 o603 b587 b1491 b896
3347 B b1492 t1492
3348 T t1493 o888 b733 b886 b1492 b1480
3349 S s1493 t726 h h754 h791 h1477 h1230
3350 G s1493 t1493
3351 B b1493 s1493
3352 T t1494 o747 b1493 b914
3353 B b1494 t1494
3354 T t1495 o605 b1057 b755
3355 B b1495 t1495
3356 T t1496 o586 b587 b622 b1495
3357 B b1496 t1496
3358 T t1497 o603 b587 b622 b1496
3359 B b1497 t1497
3360 T t1498 o603 b587 b1497 b896
3361 B b1498 t1498
3362 T t1499 o888 b733 b886 b1498 b1480
3363 S s1499 t726 h h754 h791 h1477 h1230
3364 G s1499 t1499
3365 B b1499 s1499
3366 T t1500 o747 b1499 b914
3367 B b1500 t1500
3368 T t1501 o605 b967 b755
3369 B b1501 t1501
3370 T t1502 o586 b587 b622 b1501
3371 B b1502 t1502
3372 T t1503 o603 b587 b622 b1502
3373 B b1503 t1503
3374 T t1504 o888 b733 b886 b1498 b1503
3375 S s1504 t726 h h754 h791 h1477 h1230
3376 G s1504 t1504
3377 B b1504 s1504
3378 T t1505 o747 b1504 b914
3379 B b1505 t1505
3380 T t1506 o605 b606 b755
3381 B b1506 t1506
3382 T t1507 o605 b967 b1506
3383 B b1507 t1507
3384 T t1508 o586 b587 b622 b1507
3385 B b1508 t1508
3386 T t1509 o603 b587 b622 b1508
3387 B b1509 t1509
3388 T t1510 o603 b587 b1509 b896
3389 B b1510 t1510
3390 T t1511 o888 b733 b886 b1510 b1503
3391 S s1511 t726 h h754 h791 h1477 h1230
3392 G s1511 t1511
3393 B b1511 s1511
3394 T t1512 o747 b1511 b914
3395 B b1512 t1512
3396 T t1513 o605 b606 b1501
3397 B b1513 t1513
3398 T t1514 o586 b587 b622 b1513
3399 B b1514 t1514
3400 T t1515 o603 b587 b622 b1514
3401 B b1515 t1515
3402 T t1516 o603 b587 b1515 b896
3403 B b1516 t1516
3404 T t1517 o888 b733 b886 b1516 b1503
3405 S s1517 t726 h h754 h791 h1477 h1230
3406 G s1517 t1517
3407 B b1517 s1517
3408 T t1518 o747 b1517 b914
3409 B b1518 t1518
3410 T t1519 o605 b755 b967
3411 B b1519 t1519
3412 T t1520 o586 b587 b622 b1519
3413 B b1520 t1520
3414 T t1521 o603 b587 b622 b1520
3415 B b1521 t1521
3416 T t1522 o888 b733 b886 b1516 b1521
3417 S s1522 t726 h h754 h791 h1477 h1230
3418 G s1522 t1522
3419 B b1522 s1522
3420 T t1523 o747 b1522 b914
3421 B b1523 t1523
3422 T t1524 o605 b606 b1519
3423 B b1524 t1524
3424 T t1525 o586 b587 b622 b1524
3425 B b1525 t1525
3426 T t1526 o603 b587 b622 b1525
3427 B b1526 t1526
3428 T t1527 o603 b587 b1526 b896
3429 B b1527 t1527
3430 T t1528 o888 b733 b886 b1527 b1521
3431 S s1528 t726 h h754 h791 h1477 h1230
3432 G s1528 t1528
3433 B b1528 s1528
3434 T t1529 o747 b1528 b914
3435 B b1529 t1529
3436 T t1530 o605 b606 b967
3437 B b1530 t1530
3438 T t1531 o605 b755 b1530
3439 B b1531 t1531
3440 T t1532 o586 b587 b622 b1531
3441 B b1532 t1532
3442 T t1533 o603 b587 b622 b1532
3443 B b1533 t1533
3444 T t1534 o603 b587 b1533 b896
3445 B b1534 t1534
3446 T t1535 o888 b733 b886 b1534 b1521
3447 S s1535 t726 h h754 h791 h1477 h1230
3448 G s1535 t1535
3449 B b1535 s1535
3450 T t1536 o747 b1535 b914
3451 B b1536 t1536
3452 T t1537 o605 b758 b967
3453 B b1537 t1537
3454 T t1538 o586 b587 b622 b1537
3455 B b1538 t1538
3456 T t1539 o603 b587 b622 b1538
3457 B b1539 t1539
3458 T t1540 o603 b587 b1539 b896
3459 B b1540 t1540
3460 T t1541 o888 b733 b886 b1540 b1521
3461 S s1541 t726 h h754 h791 h1477 h1230
3462 G s1541 t1541
3463 B b1541 s1541
3464 T t1542 o747 b1541 b914
3465 B b1542 t1542
3466 S s1542 t726 h h754 h791 h1477 h1230
3467 G s1542 t1460
3468 B b1543 s1542
3469 T t1543 o747 b1543 b914
3470 B b1544 t1543
3471 T t1544 o603 b587 b1484 b896
3472 B b1545 t1544
3473 T t1545 o888 b733 b886 b1545 b1477
3474 H h1545 z t1545
3475 S s1545 t726 h h754 h791 h1545 h1230
3476 G s1545 t1460
3477 B b1546 s1545
3478 T t1546 o747 b1546 b914
3479 B b1547 t1546
3480 T t1547 o603 b587 b1490 b896
3481 B b1548 t1547
3482 T t1548 o888 b733 b886 b1548 b1477
3483 H h1548 z t1548
3484 S s1548 t726 h h754 h791 h1548 h1230
3485 G s1548 t1460
3486 B b1549 s1548
3487 T t1549 o747 b1549 b914
3488 B b1550 t1549
3489 T t1550 o603 b587 b1496 b896
3490 B b1551 t1550
3491 T t1551 o888 b733 b886 b1551 b1477
3492 H h1551 z t1551
3493 S s1551 t726 h h754 h791 h1551 h1230
3494 G s1551 t1460
3495 B b1552 s1551
3496 T t1552 o747 b1552 b914
3497 B b1553 t1552
3498 T t1553 o888 b733 b886 b1551 b1502
3499 H h1553 z t1553
3500 S s1553 t726 h h754 h791 h1553 h1230
3501 G s1553 t1460
3502 B b1554 s1553
3503 T t1554 o747 b1554 b914
3504 B b1555 t1554
3505 T t1555 o603 b587 b1508 b896
3506 B b1556 t1555
3507 T t1556 o888 b733 b886 b1556 b1502
3508 H h1556 z t1556
3509 S s1556 t726 h h754 h791 h1556 h1230
3510 G s1556 t1460
3511 B b1557 s1556
3512 T t1557 o747 b1557 b914
3513 B b1558 t1557
3514 T t1558 o888 b733 b886 b1556 b1520
3515 H h1558 z t1558
3516 S s1558 t726 h h754 h791 h1558 h1230
3517 G s1558 t1460
3518 B b1559 s1558
3519 T t1559 o747 b1559 b914
3520 B b1560 t1559
3521 T t1560 o605 b967 b758
3522 B b1561 t1560
3523 T t1561 o586 b587 b622 b1561
3524 B b1562 t1561
3525 T t1562 o603 b587 b1562 b896
3526 B b1563 t1562
3527 T t1563 o888 b733 b886 b1563 b1520
3528 H h1563 z t1563
3529 S s1563 t726 h h754 h791 h1563 h1230
3530 G s1563 t1460
3531 B b1564 s1563
3532 T t1564 o747 b1564 b914
3533 B b1565 t1564
3534 T t1565 o605 b755 b1057
3535 B b1566 t1565
3536 T t1566 o586 b587 b622 b1566
3537 B b1567 t1566
3538 T t1567 o603 b587 b1567 b896
3539 B b1568 t1567
3540 T t1568 o888 b733 b886 b1568 b1520
3541 H h1568 z t1568
3542 S s1568 t726 h h754 h791 h1568 h1230
3543 G s1568 t1460
3544 B b1569 s1568
3545 T t1569 o747 b1569 b914
3546 B b1570 t1569
3547 T t1570 o605 b1519 b606
3548 B b1571 t1570
3549 T t1571 o586 b587 b622 b1571
3550 B b1572 t1571
3551 T t1572 o603 b587 b1572 b896
3552 B b1573 t1572
3553 T t1573 o888 b733 b886 b1573 b1520
3554 H h1573 z t1573
3555 S s1573 t726 h h754 h791 h1573 h1230
3556 G s1573 t1460
3557 B b1574 s1573
3558 T t1574 o747 b1574 b914
3559 B b1575 t1574
3560 T t1575 o2 b1468
3561 B b1576 t1575
3562 T t1576 o746 b1575 b4 b1576
3563 B b1577 t1576
3564 T t1577 o2 b1577
3565 B b1578 t1577
3566 T t1578 o746 b1570 b4 b1578
3567 B b1579 t1578
3568 T t1579 o2 b1579
3569 B b1580 t1579
3570 T t1580 o746 b1565 b4 b1580
3571 B b1581 t1580
3572 T t1581 o2 b1581
3573 B b1582 t1581
3574 T t1582 o746 b1560 b4 b1582
3575 B b1583 t1582
3576 T t1583 o2 b1583
3577 B b1584 t1583
3578 T t1584 o746 b1558 b4 b1584
3579 B b1585 t1584
3580 T t1585 o2 b1585
3581 B b1586 t1585
3582 T t1586 o746 b1555 b4 b1586
3583 B b1587 t1586
3584 T t1587 o2 b1587
3585 B b1588 t1587
3586 T t1588 o746 b1553 b4 b1588
3587 B b1589 t1588
3588 T t1589 o2 b1589
3589 B b1590 t1589
3590 T t1590 o746 b1550 b4 b1590
3591 B b1591 t1590
3592 T t1591 o2 b1591
3593 B b1592 t1591
3594 T t1592 o746 b1547 b4 b1592
3595 B b1593 t1592
3596 T t1593 o2 b1593
3597 B b1594 t1593
3598 T t1594 o746 b1544 b4 b1594
3599 B b1595 t1594
3600 T t1595 o2 b1595
3601 B b1596 t1595
3602 T t1596 o746 b1542 b4 b1596
3603 B b1597 t1596
3604 T t1597 o2 b1597
3605 B b1598 t1597
3606 T t1598 o746 b1536 b4 b1598
3607 B b1599 t1598
3608 T t1599 o2 b1599
3609 B b1600 t1599
3610 T t1600 o746 b1529 b4 b1600
3611 B b1601 t1600
3612 T t1601 o2 b1601
3613 B b1602 t1601
3614 T t1602 o746 b1523 b4 b1602
3615 B b1603 t1602
3616 T t1603 o2 b1603
3617 B b1604 t1603
3618 T t1604 o746 b1518 b4 b1604
3619 B b1605 t1604
3620 T t1605 o2 b1605
3621 B b1606 t1605
3622 T t1606 o746 b1512 b4 b1606
3623 B b1607 t1606
3624 T t1607 o2 b1607
3625 B b1608 t1607
3626 T t1608 o746 b1505 b4 b1608
3627 B b1609 t1608
3628 T t1609 o2 b1609
3629 B b1610 t1609
3630 T t1610 o746 b1500 b4 b1610
3631 B b1611 t1610
3632 T t1611 o2 b1611
3633 B b1612 t1611
3634 T t1612 o746 b1494 b4 b1612
3635 B b1613 t1612
3636 T t1613 o2 b1613
3637 B b1614 t1613
3638 T t1614 o746 b1488 b4 b1614
3639 B b1615 t1614
3640 T t1615 o2 b1615
3641 B b1616 t1615
3642 T t1616 o746 b1482 b4 b1616
3643 B b1617 t1616
3644 T t1617 o b1617 b4
3645 B b1618 t1617
3646 T t1618 o745 b1468 b1618
3647 B b1619 t1618
3648 P p1619 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; power{'g; 'x; 'm}}; inv{'g; 'x}}; op{'g; 'x; op{'g; power{'g; 'x; 'm}; inv{'g; 'x}}}} >> 0 ttca"
3649 O o1619 ext_rule p1619
3650 P p1623 String "assertT << (0 +@ 0) < ('m +@ 1) >> thenT autoT"
3651 O o1623 ext_rule p1623
3652 T t1623 o605 b756 b756
3653 B b1624 t1623
3654 T t1624 o754 b1624 b758
3655 S s1624 t721 h h754 h791 h955 h1230
3656 G s1624 t1624
3657 B b1625 s1624
3658 T t1625 o747 b1625 b914
3659 B b1626 t1625
3660 B b1627 t1624
3661 T t1627 o1010 b1627
3662 S s1627 t721 h h754 h791 h955 h1230
3663 G s1627 t1627
3664 B b1628 s1627
3665 T t1628 o747 b1628 b914
3666 B b1629 t1628
3667 S s1629 t726 h h754 h791 h955 h1230
3668 G s1629 t1624
3669 B b1630 s1629
3670 T t1630 o747 b1630 b914
3671 B b1631 t1630
3672 T t1631 o2 b1471
3673 B b1632 t1631
3674 T t1632 o774 b1631 b4 b1632
3675 B b1633 t1632
3676 T t1633 o2 b1633
3677 B b1634 t1633
3678 T t1634 o774 b1629 b4 b1634
3679 B b1635 t1634
3680 T t1635 o2 b1635
3681 B b1636 t1635
3682 T t1636 o774 b1626 b4 b1636
3683 B b1637 t1636
3684 H h1637 v_1 t1624
3685 S s1637 t721 h h754 h791 h955 h1230 h1637
3686 G s1637 t1468
3687 B b1638 s1637
3688 T t1638 o747 b1638 b914
3689 B b1639 t1638
3690 B b1640 t1468
3691 T t1640 o1010 b1640
3692 S s1640 t721 h h754 h791 h955 h1230 h1637
3693 G s1640 t1640
3694 B b1641 s1640
3695 T t1641 o747 b1641 b914
3696 B b1642 t1641
3697 S s1642 t726 h h754 h791 h955 h1230 h1637
3698 G s1642 t1468
3699 B b1643 s1642
3700 T t1643 o747 b1643 b914
3701 B b1644 t1643
3702 T t1644 o746 b1644 b4 b1632
3703 B b1645 t1644
3704 T t1645 o2 b1645
3705 B b1646 t1645
3706 T t1646 o746 b1642 b4 b1646
3707 B b1647 t1646
3708 T t1647 o2 b1647
3709 B b1648 t1647
3710 T t1648 o746 b1639 b4 b1648
3711 B b1649 t1648
3712 T t1649 o b1649 b4
3713 B b1650 t1649
3714 T t1650 o b1637 b1650
3715 B b1651 t1650
3716 T t1651 o745 b1471 b1651
3717 B b1652 t1651
3718 P p1652 String "lt_add_ltT thenT autoT"
3719 O o1652 ext_rule p1652
3720 T t1652 o754 b756 b606
3721 S s1652 t721 h h754 h791 h955 h1230
3722 G s1652 t1652
3723 B b1653 s1652
3724 T t1653 o747 b1653 b914
3725 B b1654 t1653
3726 T t1654 o2 b1637
3727 B b1655 t1654
3728 T t1655 o746 b1654 b4 b1655
3729 B b1656 t1655
3730 T t1656 o b1656 b4
3731 B b1657 t1656
3732 T t1657 o745 b1637 b1657
3733 B b1658 t1657
3734 P p1658 String "rwh unfold_lt 0 thenT rwh lt_DiscretC 0 ttca thenT rwh reduceC 0 ttca"
3735 O o1658 ext_rule p1658
3736 T t1658 o745 b1656 b4
3737 B b1659 t1658
3738 T t1659 o1658 b744 b1659 b4 b4
3739 B b1660 t1659
3740 T t1660 o b1660 b4
3741 B b1661 t1660
3742 T t1661 o1652 b744 b1658 b1661 b4
3743 B b1662 t1661
3744 P p1662 String "rwh reduceC 6 ttca"
3745 O o1662 ext_rule p1662
3746 T t1662 o745 b1649 b4
3747 B b1663 t1662
3748 T t1663 o1662 b744 b1663 b4 b4
3749 B b1664 t1663
3750 T t1664 o b1664 b4
3751 B b1665 t1664
3752 T t1665 o b1662 b1665
3753 B b1666 t1665
3754 T t1666 o1623 b744 b1652 b1666 b4
3755 B b1667 t1666
3756 T t1667 o b1667 b4
3757 B b1668 t1667
3758 O o1685 location p p
3759 P p1685 String power_property2
3760 O o1686 rule p1685
3761 T t1686 o603 b587 b898 b622
3762 B b1686 t1686
3763 T t1687 o888 b733 b886 b1686 b895
3764 S s1687 t726 h
3765 G s1687 t1687
3766 B b1687 s1687
3767 T t1696 o747 b1687 b914
3768 B b1696 t1696
3769 T t1697 o746 b1696 b4 b753
3770 B b1697 t1697
3771 T t1698 o603 b587 b920 b622
3772 B b1698 t1698
3773 T t1699 o888 b733 b886 b1698 b918
3774 H h1699 z t1699
3775 T t1700 o603 b587 b923 b622
3776 B b1700 t1700
3777 T t1701 o888 b733 b886 b1700 b920
3778 S s1701 t726 h h754 h757 h1699
3779 G s1701 t1701
3780 B b1701 s1701
3781 T t1702 o747 b1701 b914
3782 B b1702 t1702
3783 S s1702 t726 h h770 h754 h757 h1699
3784 G s1702 t1701
3785 B b1703 s1702
3786 T t1703 o747 b1703 b914
3787 B b1704 t1703
3788 S s1704 t726 h h770
3789 G s1704 t1687
3790 B b1705 s1704
3791 T t1705 o747 b1705 b914
3792 B b1706 t1705
3793 B b1707 t1687 n
3794 T t1707 o775 b621 b1707
3795 S s1707 t726 h
3796 G s1707 t1707
3797 B b1708 s1707
3798 T t1708 o747 b1708 b914
3799 B b1709 t1708
3800 T t1709 o2 b1697
3801 B b1710 t1709
3802 T t1710 o774 b1709 b4 b1710
3803 B b1711 t1710
3804 T t1711 o2 b1711
3805 B b1712 t1711
3806 T t1712 o746 b1706 b4 b1712
3807 B b1713 t1712
3808 T t1713 o2 b1713
3809 B b1714 t1713
3810 T t1714 o746 b1704 b4 b1714
3811 B b1715 t1714
3812 T t1715 o2 b1715
3813 B b1716 t1715
3814 T t1716 o746 b1702 b4 b1716
3815 B b1717 t1716
3816 T t1717 o603 b587 b944 b622
3817 B b1718 t1717
3818 T t1718 o888 b733 b886 b1718 b942
3819 S s1718 t726 h
3820 G s1718 t1718
3821 B b1719 s1718
3822 T t1719 o747 b1719 b914
3823 B b1720 t1719
3824 S s1720 t726 h h770
3825 G s1720 t1718
3826 B b1721 s1720
3827 T t1721 o747 b1721 b914
3828 B b1722 t1721
3829 T t1722 o746 b1722 b4 b1714
3830 B b1723 t1722
3831 T t1723 o2 b1723
3832 B b1724 t1723
3833 T t1724 o746 b1720 b4 b1724
3834 B b1725 t1724
3835 T t1725 o603 b587 b955 b622
3836 B b1726 t1725
3837 T t1726 o888 b733 b886 b1726 b953
3838 H h1726 z t1726
3839 S s1726 t726 h h754 h791 h1726
3840 G s1726 t1701
3841 B b1727 s1726
3842 T t1727 o747 b1727 b914
3843 B b1728 t1727
3844 S s1728 t726 h h770 h754 h791 h1726
3845 G s1728 t1701
3846 B b1729 s1728
3847 T t1729 o747 b1729 b914
3848 B b1730 t1729
3849 T t1730 o746 b1730 b4 b1714
3850 B b1731 t1730
3851 T t1731 o2 b1731
3852 B b1732 t1731
3853 T t1732 o746 b1728 b4 b1732
3854 B b1733 t1732
3855 S s1737 t726 h h754 h757 h1699 h968
3856 G s1737 t1701
3857 B b1738 s1737
3858 T t1738 o747 b1738 b914
3859 B b1739 t1738
3860 T t1739 o2 b1717
3861 B b1740 t1739
3862 T t1740 o746 b1739 b4 b1740
3863 B b1741 t1740
3864 S s1741 t726 h h754 h757 h1699 h972
3865 G s1741 t1701
3866 B b1742 s1741
3867 T t1742 o747 b1742 b914
3868 B b1743 t1742
3869 T t1743 o746 b1743 b4 b1740
3870 B b1744 t1743
3871 T t1744 o b1744 b4
3872 B b1745 t1744
3873 T t1745 o b1741 b1745
3874 B b1746 t1745
3875 T t1746 o745 b1717 b1746
3876 B b1747 t1746
3877 P p1747 String "hypSubstT 5 0 ttca thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
3878 O o1747 ext_rule p1747
3879 T t1747 o603 b587 b896 b610
3880 B b1748 t1747
3881 T t1748 o603 b587 b1748 b622
3882 B b1749 t1748
3883 T t1749 o888 b733 b886 b1749 b610
3884 S s1749 t726 h h754 h757 h1699 h968
3885 G s1749 t1749
3886 B b1750 s1749
3887 T t1750 o747 b1750 b914
3888 B b1751 t1750
3889 T t1751 o603 b587 b896 b1115
3890 B b1752 t1751
3891 T t1752 o603 b587 b1752 b622
3892 B b1753 t1752
3893 T t1753 o888 b733 b886 b1753 b610
3894 S s1753 t726 h h754 h757 h1699 h968
3895 G s1753 t1753
3896 B b1754 s1753
3897 T t1754 o747 b1754 b914
3898 B b1755 t1754
3899 T t1755 o603 b587 b896 b1121
3900 B b1756 t1755
3901 T t1756 o603 b587 b1756 b622
3902 B b1757 t1756
3903 T t1757 o888 b733 b886 b1757 b610
3904 S s1757 t726 h h754 h757 h1699 h968
3905 G s1757 t1757
3906 B b1758 s1757
3907 T t1758 o747 b1758 b914
3908 B b1759 t1758
3909 T t1759 o603 b587 b896 b1131
3910 B b1760 t1759
3911 T t1760 o603 b587 b1760 b622
3912 B b1761 t1760
3913 T t1761 o888 b733 b886 b1761 b610
3914 S s1761 t726 h h754 h757 h1699 h968
3915 G s1761 t1761
3916 B b1762 s1761
3917 T t1762 o747 b1762 b914
3918 B b1763 t1762
3919 T t1763 o603 b587 b896 b1138
3920 B b1764 t1763
3921 T t1764 o603 b587 b1764 b622
3922 B b1765 t1764
3923 T t1765 o888 b733 b886 b1765 b610
3924 S s1765 t726 h h754 h757 h1699 h968
3925 G s1765 t1765
3926 B b1766 s1765
3927 T t1766 o747 b1766 b914
3928 B b1767 t1766
3929 T t1767 o603 b587 b896 b944
3930 B b1768 t1767
3931 T t1768 o603 b587 b1768 b622
3932 B b1769 t1768
3933 T t1769 o888 b733 b886 b1769 b610
3934 S s1769 t726 h h754 h757 h1699 h968
3935 G s1769 t1769
3936 B b1770 s1769
3937 T t1770 o747 b1770 b914
3938 B b1771 t1770
3939 T t1771 o586 b587 b622 b1048
3940 B b1772 t1771
3941 T t1772 o603 b587 b896 b1772
3942 B b1773 t1772
3943 T t1773 o603 b587 b1773 b622
3944 B b1774 t1773
3945 T t1774 o888 b733 b886 b1774 b610
3946 S s1774 t726 h h754 h757 h1699 h968
3947 G s1774 t1774
3948 B b1775 s1774
3949 T t1775 o747 b1775 b914
3950 B b1776 t1775
3951 T t1776 o888 b733 b886 b1774 b1115
3952 S s1776 t726 h h754 h757 h1699 h968
3953 G s1776 t1776
3954 B b1777 s1776
3955 T t1777 o747 b1777 b914
3956 B b1778 t1777
3957 T t1778 o888 b733 b886 b1774 b1121
3958 S s1778 t726 h h754 h757 h1699 h968
3959 G s1778 t1778
3960 B b1779 s1778
3961 T t1779 o747 b1779 b914
3962 B b1780 t1779
3963 T t1780 o888 b733 b886 b1774 b1131
3964 S s1780 t726 h h754 h757 h1699 h968
3965 G s1780 t1780
3966 B b1781 s1780
3967 T t1781 o747 b1781 b914
3968 B b1782 t1781
3969 T t1782 o888 b733 b886 b1774 b1138
3970 S s1782 t726 h h754 h757 h1699 h968
3971 G s1782 t1782
3972 B b1783 s1782
3973 T t1783 o747 b1783 b914
3974 B b1784 t1783
3975 T t1784 o1112 b1126 b610 b1773
3976 B b1785 t1784
3977 T t1785 o603 b587 b1785 b622
3978 B b1786 t1785
3979 T t1786 o888 b733 b886 b1786 b1138
3980 S s1786 t726 h h754 h757 h1699 h968
3981 G s1786 t1786
3982 B b1787 s1786
3983 T t1787 o747 b1787 b914
3984 B b1788 t1787
3985 T t1788 o1039 b1047 b756
3986 B b1789 t1788
3987 T t1789 o1112 b1789 b610 b1773
3988 B b1790 t1789
3989 T t1790 o603 b587 b1790 b622
3990 B b1791 t1790
3991 T t1791 o888 b733 b886 b1791 b1138
3992 S s1791 t726 h h754 h757 h1699 h968
3993 G s1791 t1791
3994 B b1792 s1791
3995 T t1792 o747 b1792 b914
3996 B b1793 t1792
3997 T t1793 o610 b1047 b606
3998 B b1794 t1793
3999 T t1794 o586 b587 b622 b1794
4000 B b1795 t1794
4001 T t1795 o603 b587 b622 b1795
4002 B b1796 t1795
4003 T t1796 o1112 b1126 b1796 b1773
4004 B b1797 t1796
4005 T t1797 o1112 b1789 b610 b1797
4006 B b1798 t1797
4007 T t1798 o603 b587 b1798 b622
4008 B b1799 t1798
4009 T t1799 o888 b733 b886 b1799 b1138
4010 S s1799 t726 h h754 h757 h1699 h968
4011 G s1799 t1799
4012 B b1800 s1799
4013 T t1800 o747 b1800 b914
4014 B b1801 t1800
4015 B b1802 t1772 i j
4016 B b1803 t1795 k l
4017 T t1803 o602 b1047 b1802 b610 b1803
4018 B b1804 t1803
4019 T t1804 o603 b587 b1804 b622
4020 B b1805 t1804
4021 T t1805 o888 b733 b886 b1805 b1138
4022 S s1805 t726 h h754 h757 h1699 h968
4023 G s1805 t1805
4024 B b1806 s1805
4025 T t1806 o747 b1806 b914
4026 B b1807 t1806
4027 T t1807 o586 b587 b622 b1047
4028 B b1808 t1807
4029 T t1808 o603 b587 b1808 b622
4030 B b1809 t1808
4031 T t1809 o888 b733 b886 b1809 b944
4032 S s1809 t726 h h754 h757 h1699 h968
4033 G s1809 t1809
4034 B b1810 s1809
4035 T t1810 o747 b1810 b914
4036 B b1811 t1810
4037 T t1811 o888 b733 b886 b1809 b1772
4038 S s1811 t726 h h754 h757 h1699 h968
4039 G s1811 t1811
4040 B b1812 s1811
4041 T t1812 o747 b1812 b914
4042 B b1813 t1812
4043 T t1813 o586 b587 b622 b1057
4044 B b1814 t1813
4045 T t1814 o888 b733 b886 b1809 b1814
4046 S s1814 t726 h h754 h757 h1699 h968
4047 G s1814 t1814
4048 B b1815 s1814
4049 T t1815 o747 b1815 b914
4050 B b1816 t1815
4051 T t1816 o586 b587 b622 b967
4052 B b1817 t1816
4053 T t1817 o603 b587 b1817 b622
4054 B b1818 t1817
4055 T t1818 o888 b733 b886 b1818 b1814
4056 S s1818 t726 h h754 h757 h1699 h968
4057 G s1818 t1818
4058 B b1819 s1818
4059 T t1819 o747 b1819 b914
4060 B b1820 t1819
4061 T t1820 o2 b1741
4062 B b1821 t1820
4063 T t1821 o746 b1820 b4 b1821
4064 B b1822 t1821
4065 T t1822 o2 b1822
4066 B b1823 t1822
4067 T t1823 o746 b1816 b4 b1823
4068 B b1824 t1823
4069 T t1824 o2 b1824
4070 B b1825 t1824
4071 T t1825 o746 b1813 b4 b1825
4072 B b1826 t1825
4073 T t1826 o2 b1826
4074 B b1827 t1826
4075 T t1827 o746 b1811 b4 b1827
4076 B b1828 t1827
4077 T t1828 o2 b1828
4078 B b1829 t1828
4079 T t1829 o746 b1807 b4 b1829
4080 B b1830 t1829
4081 T t1830 o2 b1830
4082 B b1831 t1830
4083 T t1831 o746 b1801 b4 b1831
4084 B b1832 t1831
4085 T t1832 o2 b1832
4086 B b1833 t1832
4087 T t1833 o746 b1793 b4 b1833
4088 B b1834 t1833
4089 T t1834 o2 b1834
4090 B b1835 t1834
4091 T t1835 o746 b1788 b4 b1835
4092 B b1836 t1835
4093 T t1836 o2 b1836
4094 B b1837 t1836
4095 T t1837 o746 b1784 b4 b1837
4096 B b1838 t1837
4097 T t1838 o2 b1838
4098 B b1839 t1838
4099 T t1839 o746 b1782 b4 b1839
4100 B b1840 t1839
4101 T t1840 o2 b1840
4102 B b1841 t1840
4103 T t1841 o746 b1780 b4 b1841
4104 B b1842 t1841
4105 T t1842 o2 b1842
4106 B b1843 t1842
4107 T t1843 o746 b1778 b4 b1843
4108 B b1844 t1843
4109 T t1844 o2 b1844
4110 B b1845 t1844
4111 T t1845 o746 b1776 b4 b1845
4112 B b1846 t1845
4113 T t1846 o2 b1846
4114 B b1847 t1846
4115 T t1847 o746 b1771 b4 b1847
4116 B b1848 t1847
4117 T t1848 o2 b1848
4118 B b1849 t1848
4119 T t1849 o746 b1767 b4 b1849
4120 B b1850 t1849
4121 T t1850 o2 b1850
4122 B b1851 t1850
4123 T t1851 o746 b1763 b4 b1851
4124 B b1852 t1851
4125 T t1852 o2 b1852
4126 B b1853 t1852
4127 T t1853 o746 b1759 b4 b1853
4128 B b1854 t1853
4129 T t1854 o2 b1854
4130 B b1855 t1854
4131 T t1855 o746 b1755 b4 b1855
4132 B b1856 t1855
4133 T t1856 o2 b1856
4134 B b1857 t1856
4135 T t1857 o746 b1751 b4 b1857
4136 B b1858 t1857
4137 T t1858 o b1858 b4
4138 B b1859 t1858
4139 T t1859 o745 b1741 b1859
4140 B b1860 t1859
4141 P p1860 String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 'x}; id{'g}}; inv{'g; 'x}} >> 0 ttca"
4142 O o1860 ext_rule p1860
4143 T t1864 o603 b587 b983 b622
4144 B b1865 t1864
4145 T t1865 o888 b733 b886 b1865 b981
4146 S s1865 t726 h h754 h757 h1699 h972
4147 G s1865 t1865
4148 B b1866 s1865
4149 T t1866 o747 b1866 b914
4150 B b1867 t1866
4151 T t1867 o603 b587 b994 b622
4152 B b1868 t1867
4153 T t1868 o888 b733 b886 b1868 b990
4154 S s1868 t726 h h754 h757 h1699 h972
4155 G s1868 t1868
4156 B b1869 s1868
4157 T t1869 o747 b1869 b914
4158 B b1870 t1869
4159 T t1870 o2 b1744
4160 B b1871 t1870
4161 T t1871 o746 b1870 b4 b1871
4162 B b1872 t1871
4163 T t1872 o2 b1872
4164 B b1873 t1872
4165 T t1873 o746 b1867 b4 b1873
4166 B b1874 t1873
4167 S s1874 t726 h h754 h757 h1699 h972
4168 G s1874 t1000
4169 B b1875 s1874
4170 T t1875 o747 b1875 b914
4171 B b1876 t1875
4172 T t1876 o774 b1876 b4 b1873
4173 B b1877 t1876
4174 T t1877 o b1877 b4
4175 B b1878 t1877
4176 T t1878 o b1874 b1878
4177 B b1879 t1878
4178 T t1879 o745 b1744 b1879
4179 B b1880 t1879
4180 P p1880 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; inv{'g; 'x}; power{'g; 'x; ('m +@ 1)}}; 'x}; op{'g; inv{'g; 'x}; op{'g; power{'g; 'x; ('m +@ 1)}; 'x}}} >> 0 ttca"
4181 O o1880 ext_rule p1880
4182 P p1882 String "splitIntT << 'm >> << minus{1} >> ttca"
4183 O o1882 ext_rule p1882
4184 S s1882 t726 h h754 h757 h1699 h972 h1008
4185 G s1882 t1000
4186 B b1883 s1882
4187 T t1883 o747 b1883 b914
4188 B b1884 t1883
4189 T t1884 o2 b1877
4190 B b1885 t1884
4191 T t1885 o746 b1884 b4 b1885
4192 B b1886 t1885
4193 S s1886 t726 h h754 h757 h1699 h972 h1021
4194 G s1886 t1000
4195 B b1887 s1886
4196 T t1887 o747 b1887 b914
4197 B b1888 t1887
4198 T t1888 o746 b1888 b4 b1885
4199 B b1889 t1888
4200 T t1889 o b1889 b4
4201 B b1890 t1889
4202 T t1890 o b1886 b1890
4203 B b1891 t1890
4204 T t1891 o745 b1877 b1891
4205 B b1892 t1891
4206 T t1892 o745 b1886 b4
4207 B b1893 t1892
4208 T t1893 o1035 b744 b1893 b4 b4
4209 B b1894 t1893
4210 S s1894 t721 h h754 h757 h1699 h972 h1040
4211 G s1894 t1041
4212 B b1895 s1894
4213 T t1895 o747 b1895 b914
4214 B b1896 t1895
4215 S s1896 t721 h h754 h757 h1699 h972 h1045
4216 G s1896 t1041
4217 B b1897 s1896
4218 T t1897 o747 b1897 b914
4219 B b1898 t1897
4220 S s1898 t721 h h754 h757 h1699 h972 h1051
4221 G s1898 t1041
4222 B b1899 s1898
4223 T t1899 o747 b1899 b914
4224 B b1900 t1899
4225 S s1900 t721 h h754 h757 h1699 h972 h1055
4226 G s1900 t1041
4227 B b1901 s1900
4228 T t1901 o747 b1901 b914
4229 B b1902 t1901
4230 S s1902 t721 h h754 h757 h1699 h972 h1060
4231 G s1902 t1041
4232 B b1903 s1902
4233 T t1903 o747 b1903 b914
4234 B b1904 t1903
4235 S s1904 t721 h h754 h757 h1699 h972 h1064
4236 G s1904 t1041
4237 B b1905 s1904
4238 T t1905 o747 b1905 b914
4239 B b1906 t1905
4240 B b1907 t1041
4241 T t1907 o1010 b1907
4242 S s1907 t721 h h754 h757 h1699 h972 h1064
4243 G s1907 t1907
4244 B b1908 s1907
4245 T t1908 o747 b1908 b914
4246 B b1909 t1908
4247 S s1909 t726 h h754 h757 h1699 h972 h1064
4248 G s1909 t1041
4249 B b1910 s1909
4250 T t1910 o747 b1910 b914
4251 B b1911 t1910
4252 S s1911 t726 h h754 h757 h1699 h972 h1067
4253 G s1911 t1041
4254 B b1912 s1911
4255 T t1912 o747 b1912 b914
4256 B b1913 t1912
4257 S s1913 t726 h h754 h757 h1699 h972 h1021
4258 G s1913 t1041
4259 B b1914 s1913
4260 T t1914 o747 b1914 b914
4261 B b1915 t1914
4262 T t1915 o2 b1889
4263 B b1916 t1915
4264 T t1916 o774 b1915 b4 b1916
4265 B b1917 t1916
4266 T t1917 o2 b1917
4267 B b1918 t1917
4268 T t1918 o774 b1913 b4 b1918
4269 B b1919 t1918
4270 T t1919 o2 b1919
4271 B b1920 t1919
4272 T t1920 o774 b1911 b4 b1920
4273 B b1921 t1920
4274 T t1921 o2 b1921
4275 B b1922 t1921
4276 T t1922 o774 b1909 b4 b1922
4277 B b1923 t1922
4278 T t1923 o2 b1923
4279 B b1924 t1923
4280 T t1924 o774 b1906 b4 b1924
4281 B b1925 t1924
4282 T t1925 o2 b1925
4283 B b1926 t1925
4284 T t1926 o774 b1904 b4 b1926
4285 B b1927 t1926
4286 T t1927 o2 b1927
4287 B b1928 t1927
4288 T t1928 o774 b1902 b4 b1928
4289 B b1929 t1928
4290 T t1929 o2 b1929
4291 B b1930 t1929
4292 T t1930 o774 b1900 b4 b1930
4293 B b1931 t1930
4294 T t1931 o2 b1931
4295 B b1932 t1931
4296 T t1932 o774 b1898 b4 b1932
4297 B b1933 t1932
4298 T t1933 o2 b1933
4299 B b1934 t1933
4300 T t1934 o746 b1896 b4 b1934
4301 B b1935 t1934
4302 S s1935 t721 h h754 h757 h1699 h972 h1086
4303 G s1935 t1041
4304 B b1936 s1935
4305 T t1936 o747 b1936 b914
4306 B b1937 t1936
4307 T t1937 o746 b1937 b4 b1934
4308 B b1938 t1937
4309 T t1938 o b1938 b4
4310 B b1939 t1938
4311 T t1939 o b1935 b1939
4312 B b1940 t1939
4313 T t1940 o745 b1889 b1940
4314 B b1941 t1940
4315 T t1941 o745 b1935 b4
4316 B b1942 t1941
4317 T t1942 o1092 b744 b1942 b4 b4
4318 B b1943 t1942
4319 T t1943 o745 b1938 b4
4320 B b1944 t1943
4321 T t1944 o1094 b744 b1944 b4 b4
4322 B b1945 t1944
4323 T t1945 o b1945 b4
4324 B b1946 t1945
4325 T t1946 o b1943 b1946
4326 B b1947 t1946
4327 T t1947 o1037 b744 b1941 b1947 b4
4328 B b1948 t1947
4329 T t1948 o b1948 b4
4330 B b1949 t1948
4331 T t1949 o b1894 b1949
4332 B b1950 t1949
4333 T t1950 o1882 b744 b1892 b1950 b4
4334 B b1951 t1950
4335 T t1951 o b1951 b4
4336 B b1952 t1951
4337 S s1959 t726 h h754 h791 h1726 h1225
4338 G s1959 t1701
4339 B b1960 s1959
4340 T t1960 o747 b1960 b914
4341 B b1961 t1960
4342 T t1961 o2 b1733
4343 B b1962 t1961
4344 T t1962 o746 b1961 b4 b1962
4345 B b1963 t1962
4346 S s1963 t726 h h754 h791 h1726 h1230
4347 G s1963 t1701
4348 B b1964 s1963
4349 T t1964 o747 b1964 b914
4350 B b1965 t1964
4351 T t1965 o746 b1965 b4 b1962
4352 B b1966 t1965
4353 T t1966 o b1966 b4
4354 B b1967 t1966
4355 T t1967 o b1963 b1967
4356 B b1968 t1967
4357 T t1968 o745 b1733 b1968
4358 B b1969 t1968
4359 T t1969 o603 b587 b1109 b622
4360 B b1970 t1969
4361 T t1970 o888 b733 b886 b1970 b1237
4362 S s1970 t726 h h754 h791 h1726 h1225
4363 G s1970 t1970
4364 B b1971 s1970
4365 T t1971 o747 b1971 b914
4366 B b1972 t1971
4367 T t1972 o888 b733 b886 b1970 b1241
4368 S s1972 t726 h h754 h791 h1726 h1225
4369 G s1972 t1972
4370 B b1973 s1972
4371 T t1973 o747 b1973 b914
4372 B b1974 t1973
4373 T t1974 o888 b733 b886 b1970 b1253
4374 S s1974 t726 h h754 h791 h1726 h1225
4375 G s1974 t1974
4376 B b1975 s1974
4377 T t1975 o747 b1975 b914
4378 B b1976 t1975
4379 T t1976 o888 b733 b886 b1970 b1257
4380 S s1976 t726 h h754 h791 h1726 h1225
4381 G s1976 t1976
4382 B b1977 s1976
4383 T t1977 o747 b1977 b914
4384 B b1978 t1977
4385 T t1978 o888 b733 b886 b1970 b1261
4386 S s1978 t726 h h754 h791 h1726 h1225
4387 G s1978 t1978
4388 B b1979 s1978
4389 T t1979 o747 b1979 b914
4390 B b1980 t1979
4391 T t1980 o888 b733 b886 b1970 b1265
4392 S s1980 t726 h h754 h791 h1726 h1225
4393 G s1980 t1980
4394 B b1981 s1980
4395 T t1981 o747 b1981 b914
4396 B b1982 t1981
4397 T t1982 o603 b587 b1116 b622
4398 B b1983 t1982
4399 T t1983 o888 b733 b886 b1983 b1265
4400 S s1983 t726 h h754 h791 h1726 h1225
4401 G s1983 t1983
4402 B b1984 s1983
4403 T t1984 o747 b1984 b914
4404 B b1985 t1984
4405 T t1985 o603 b587 b1122 b622
4406 B b1986 t1985
4407 T t1986 o888 b733 b886 b1986 b1265
4408 S s1986 t726 h h754 h791 h1726 h1225
4409 G s1986 t1986
4410 B b1987 s1986
4411 T t1987 o747 b1987 b914
4412 B b1988 t1987
4413 T t1988 o603 b587 b1132 b622
4414 B b1989 t1988
4415 T t1989 o888 b733 b886 b1989 b1265
4416 S s1989 t726 h h754 h791 h1726 h1225
4417 G s1989 t1989
4418 B b1990 s1989
4419 T t1990 o747 b1990 b914
4420 B b1991 t1990
4421 T t1991 o603 b587 b1139 b622
4422 B b1992 t1991
4423 T t1992 o888 b733 b886 b1992 b1265
4424 S s1992 t726 h h754 h791 h1726 h1225
4425 G s1992 t1992
4426 B b1993 s1992
4427 T t1993 o747 b1993 b914
4428 B b1994 t1993
4429 T t1994 o603 b587 b1143 b622
4430 B b1995 t1994
4431 T t1995 o888 b733 b886 b1995 b1269
4432 S s1995 t726 h h754 h791 h1726 h1225
4433 G s1995 t1995
4434 B b1996 s1995
4435 T t1996 o747 b1996 b914
4436 B b1997 t1996
4437 T t1997 o888 b733 b886 b1995 b1276
4438 S s1997 t726 h h754 h791 h1726 h1225
4439 G s1997 t1997
4440 B b1998 s1997
4441 T t1998 o747 b1998 b914
4442 B b1999 t1998
4443 T t1999 o888 b733 b886 b1995 b1282
4444 S s1999 t726 h h754 h791 h1726 h1225
4445 G s1999 t1999
4446 B b2000 s1999
4447 T t2000 o747 b2000 b914
4448 B b2001 t2000
4449 T t2001 o888 b733 b886 b1995 b1287
4450 S s2001 t726 h h754 h791 h1726 h1225
4451 G s2001 t2001
4452 B b2002 s2001
4453 T t2002 o747 b2002 b914
4454 B b2003 t2002
4455 T t2003 o888 b733 b886 b1995 b1295
4456 S s2003 t726 h h754 h791 h1726 h1225
4457 G s2003 t2003
4458 B b2004 s2003
4459 T t2004 o747 b2004 b914
4460 B b2005 t2004
4461 T t2005 o888 b733 b886 b1995 b1301
4462 S s2005 t726 h h754 h791 h1726 h1225
4463 G s2005 t2005
4464 B b2006 s2005
4465 T t2006 o747 b2006 b914
4466 B b2007 t2006
4467 T t2007 o603 b587 b1149 b622
4468 B b2008 t2007
4469 T t2008 o888 b733 b886 b2008 b1301
4470 S s2008 t726 h h754 h791 h1726 h1225
4471 G s2008 t2008
4472 B b2009 s2008
4473 T t2009 o747 b2009 b914
4474 B b2010 t2009
4475 T t2010 o888 b733 b886 b2008 b1316
4476 S s2010 t726 h h754 h791 h1726 h1225
4477 G s2010 t2010
4478 B b2011 s2010
4479 T t2011 o747 b2011 b914
4480 B b2012 t2011
4481 T t2012 o888 b733 b886 b2008 b1323
4482 S s2012 t726 h h754 h791 h1726 h1225
4483 G s2012 t2012
4484 B b2013 s2012
4485 T t2013 o747 b2013 b914
4486 B b2014 t2013
4487 T t2014 o888 b733 b886 b2008 b1327
4488 S s2014 t726 h h754 h791 h1726 h1225
4489 G s2014 t2014
4490 B b2015 s2014
4491 T t2015 o747 b2015 b914
4492 B b2016 t2015
4493 T t2016 o603 b587 b1161 b622
4494 B b2017 t2016
4495 T t2017 o888 b733 b886 b2017 b1327
4496 S s2017 t726 h h754 h791 h1726 h1225
4497 G s2017 t2017
4498 B b2018 s2017
4499 T t2018 o747 b2018 b914
4500 B b2019 t2018
4501 T t2019 o603 b587 b1166 b622
4502 B b2020 t2019
4503 T t2020 o888 b733 b886 b2020 b1327
4504 S s2020 t726 h h754 h791 h1726 h1225
4505 G s2020 t2020
4506 B b2021 s2020
4507 T t2021 o747 b2021 b914
4508 B b2022 t2021
4509 T t2022 o603 b587 b1174 b622
4510 B b2023 t2022
4511 T t2023 o888 b733 b886 b2023 b1327
4512 S s2023 t726 h h754 h791 h1726 h1225
4513 G s2023 t2023
4514 B b2024 s2023
4515 T t2024 o747 b2024 b914
4516 B b2025 t2024
4517 T t2025 o603 b587 b1180 b622
4518 B b2026 t2025
4519 T t2026 o888 b733 b886 b2026 b1327
4520 S s2026 t726 h h754 h791 h1726 h1225
4521 G s2026 t2026
4522 B b2027 s2026
4523 T t2027 o747 b2027 b914
4524 B b2028 t2027
4525 T t2028 o603 b587 b1184 b622
4526 B b2029 t2028
4527 T t2029 o888 b733 b886 b2029 b1171
4528 S s2029 t726 h h754 h791 h1726 h1225
4529 G s2029 t2029
4530 B b2030 s2029
4531 T t2030 o747 b2030 b914
4532 B b2031 t2030
4533 T t2031 o2 b1963
4534 B b2032 t2031
4535 T t2032 o746 b2031 b4 b2032
4536 B b2033 t2032
4537 T t2033 o2 b2033
4538 B b2034 t2033
4539 T t2034 o746 b2028 b4 b2034
4540 B b2035 t2034
4541 T t2035 o2 b2035
4542 B b2036 t2035
4543 T t2036 o746 b2025 b4 b2036
4544 B b2037 t2036
4545 T t2037 o2 b2037
4546 B b2038 t2037
4547 T t2038 o746 b2022 b4 b2038
4548 B b2039 t2038
4549 T t2039 o2 b2039
4550 B b2040 t2039
4551 T t2040 o746 b2019 b4 b2040
4552 B b2041 t2040
4553 T t2041 o2 b2041
4554 B b2042 t2041
4555 T t2042 o746 b2016 b4 b2042
4556 B b2043 t2042
4557 T t2043 o2 b2043
4558 B b2044 t2043
4559 T t2044 o746 b2014 b4 b2044
4560 B b2045 t2044
4561 T t2045 o2 b2045
4562 B b2046 t2045
4563 T t2046 o746 b2012 b4 b2046
4564 B b2047 t2046
4565 T t2047 o2 b2047
4566 B b2048 t2047
4567 T t2048 o746 b2010 b4 b2048
4568 B b2049 t2048
4569 T t2049 o2 b2049
4570 B b2050 t2049
4571 T t2050 o746 b2007 b4 b2050
4572 B b2051 t2050
4573 T t2051 o2 b2051
4574 B b2052 t2051
4575 T t2052 o746 b2005 b4 b2052
4576 B b2053 t2052
4577 T t2053 o2 b2053
4578 B b2054 t2053
4579 T t2054 o746 b2003 b4 b2054
4580 B b2055 t2054
4581 T t2055 o2 b2055
4582 B b2056 t2055
4583 T t2056 o746 b2001 b4 b2056
4584 B b2057 t2056
4585 T t2057 o2 b2057
4586 B b2058 t2057
4587 T t2058 o746 b1999 b4 b2058
4588 B b2059 t2058
4589 T t2059 o2 b2059
4590 B b2060 t2059
4591 T t2060 o746 b1997 b4 b2060
4592 B b2061 t2060
4593 T t2061 o2 b2061
4594 B b2062 t2061
4595 T t2062 o746 b1994 b4 b2062
4596 B b2063 t2062
4597 T t2063 o2 b2063
4598 B b2064 t2063
4599 T t2064 o746 b1991 b4 b2064
4600 B b2065 t2064
4601 T t2065 o2 b2065
4602 B b2066 t2065
4603 T t2066 o746 b1988 b4 b2066
4604 B b2067 t2066
4605 T t2067 o2 b2067
4606 B b2068 t2067
4607 T t2068 o746 b1985 b4 b2068
4608 B b2069 t2068
4609 T t2069 o2 b2069
4610 B b2070 t2069
4611 T t2070 o746 b1982 b4 b2070
4612 B b2071 t2070
4613 T t2071 o2 b2071
4614 B b2072 t2071
4615 T t2072 o746 b1980 b4 b2072
4616 B b2073 t2072
4617 T t2073 o2 b2073
4618 B b2074 t2073
4619 T t2074 o746 b1978 b4 b2074
4620 B b2075 t2074
4621 T t2075 o2 b2075
4622 B b2076 t2075
4623 T t2076 o746 b1976 b4 b2076
4624 B b2077 t2076
4625 T t2077 o2 b2077
4626 B b2078 t2077
4627 T t2078 o746 b1974 b4 b2078
4628 B b2079 t2078
4629 T t2079 o2 b2079
4630 B b2080 t2079
4631 T t2080 o746 b1972 b4 b2080
4632 B b2081 t2080
4633 T t2081 o b2081 b4
4634 B b2082 t2081
4635 T t2082 o745 b1963 b2082
4636 B b2083 t2082
4637 P p2083 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; id{'g}}; 'x} >> 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0"
4638 O o2083 ext_rule p2083
4639 T t2083 o888 b733 b886 b1422 b1386
4640 S s2083 t726 h h754 h791 h1726 h1225
4641 G s2083 t2083
4642 B b2084 s2083
4643 T t2084 o747 b2084 b914
4644 B b2085 t2084
4645 T t2085 o888 b733 b886 b1422 b1390
4646 S s2085 t726 h h754 h791 h1726 h1225
4647 G s2085 t2085
4648 B b2086 s2085
4649 T t2086 o747 b2086 b914
4650 B b2087 t2086
4651 T t2087 o888 b733 b886 b1422 b1394
4652 S s2087 t726 h h754 h791 h1726 h1225
4653 G s2087 t2087
4654 B b2088 s2087
4655 T t2088 o747 b2088 b914
4656 B b2089 t2088
4657 T t2089 o888 b733 b886 b1422 b1398
4658 S s2089 t726 h h754 h791 h1726 h1225
4659 G s2089 t2089
4660 B b2090 s2089
4661 T t2090 o747 b2090 b914
4662 B b2091 t2090
4663 T t2091 o888 b733 b886 b1422 b1402
4664 S s2091 t726 h h754 h791 h1726 h1225
4665 G s2091 t2091
4666 B b2092 s2091
4667 T t2092 o747 b2092 b914
4668 B b2093 t2092
4669 T t2093 o888 b733 b886 b1422 b1237
4670 S s2093 t726 h h754 h791 h1726 h1225
4671 G s2093 t2093
4672 B b2094 s2093
4673 T t2094 o747 b2094 b914
4674 B b2095 t2094
4675 T t2095 o2 b2081
4676 B b2096 t2095
4677 T t2096 o746 b2095 b4 b2096
4678 B b2097 t2096
4679 T t2097 o2 b2097
4680 B b2098 t2097
4681 T t2098 o746 b2093 b4 b2098
4682 B b2099 t2098
4683 T t2099 o2 b2099
4684 B b2100 t2099
4685 T t2100 o746 b2091 b4 b2100
4686 B b2101 t2100
4687 T t2101 o2 b2101
4688 B b2102 t2101
4689 T t2102 o746 b2089 b4 b2102
4690 B b2103 t2102
4691 T t2103 o2 b2103
4692 B b2104 t2103
4693 T t2104 o746 b2087 b4 b2104
4694 B b2105 t2104
4695 T t2105 o2 b2105
4696 B b2106 t2105
4697 T t2106 o746 b2085 b4 b2106
4698 B b2107 t2106
4699 P p2109 String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; op{'g; 'x; id{'g}}}; op{'g; op{'g; 'x; 'x}; id{'g}}} >> 0 ttca thenT equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; 'x}; id{'g}}; op{'g; 'x; 'x}} >> 0 ttca"
4700 O o2109 ext_rule p2109
4701 T t2115 o603 b587 b1460 b622
4702 B b2116 t2115
4703 T t2116 o888 b733 b886 b2116 b1458
4704 S s2116 t726 h h754 h791 h1726 h1230
4705 G s2116 t2116
4706 B b2117 s2116
4707 T t2117 o747 b2117 b914
4708 B b2118 t2117
4709 S s2118 t726 h h754 h791 h1726 h1230
4710 G s2118 t1868
4711 B b2119 s2118
4712 T t2119 o747 b2119 b914
4713 B b2120 t2119
4714 T t2120 o2 b1966
4715 B b2121 t2120
4716 T t2121 o746 b2120 b4 b2121
4717 B b2122 t2121
4718 T t2122 o2 b2122
4719 B b2123 t2122
4720 T t2123 o746 b2118 b4 b2123
4721 B b2124 t2123
4722 S s2124 t726 h h754 h791 h1726 h1230
4723 G s2124 t1468
4724 B b2125 s2124
4725 T t2125 o747 b2125 b914
4726 B b2126 t2125
4727 T t2126 o774 b2126 b4 b2123
4728 B b2127 t2126
4729 T t2127 o b2127 b4
4730 B b2128 t2127
4731 T t2128 o b2124 b2128
4732 B b2129 t2128
4733 T t2129 o745 b1966 b2129
4734 B b2130 t2129
4735 P p2130 String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; power{'g; 'x; ('m -@ 1)}}; 'x}; op{'g; 'x; op{'g; power{'g; 'x; ('m -@ 1)}; 'x}}} >> 0 ttca"
4736 O o2130 ext_rule p2130
4737 T t2130 o603 b587 b622 b1726
4738 B b2131 t2130
4739 T t2131 o888 b733 b886 b2131 b1458
4740 S s2131 t726 h h754 h791 h1726 h1230
4741 G s2131 t2131
4742 B b2132 s2131
4743 T t2132 o747 b2132 b914
4744 B b2133 t2132
4745 T t2133 o2 b2124
4746 B b2134 t2133
4747 T t2134 o746 b2133 b4 b2134
4748 B b2135 t2134
4749 T t2135 o b2135 b4
4750 B b2136 t2135
4751 P p2137 String "rwh unfold_sub 4 thenT rwh add_normalizeC 4 thenT rwh reduceC 4 thenT rwh unfold_sub 0 thenT rwh add_normalizeC 0 thenT rwh reduceC 0 ttca"
4752 O o2137 ext_rule p2137
4753 S s2141 t721 h h754 h791 h1726 h1230
4754 G s2141 t1624
4755 B b2142 s2141
4756 T t2142 o747 b2142 b914
4757 B b2143 t2142
4758 S s2143 t721 h h754 h791 h1726 h1230
4759 G s2143 t1627
4760 B b2144 s2143
4761 T t2144 o747 b2144 b914
4762 B b2145 t2144
4763 S s2145 t726 h h754 h791 h1726 h1230
4764 G s2145 t1624
4765 B b2146 s2145
4766 T t2146 o747 b2146 b914
4767 B b2147 t2146
4768 T t2147 o2 b2127
4769 B b2148 t2147
4770 T t2148 o774 b2147 b4 b2148
4771 B b2149 t2148
4772 T t2149 o2 b2149
4773 B b2150 t2149
4774 T t2150 o774 b2145 b4 b2150
4775 B b2151 t2150
4776 T t2151 o2 b2151
4777 B b2152 t2151
4778 T t2152 o774 b2143 b4 b2152
4779 B b2153 t2152
4780 S s2153 t721 h h754 h791 h1726 h1230 h1637
4781 G s2153 t1468
4782 B b2154 s2153
4783 T t2154 o747 b2154 b914
4784 B b2155 t2154
4785 S s2155 t721 h h754 h791 h1726 h1230 h1637
4786 G s2155 t1640
4787 B b2156 s2155
4788 T t2156 o747 b2156 b914
4789 B b2157 t2156
4790 S s2157 t726 h h754 h791 h1726 h1230 h1637
4791 G s2157 t1468
4792 B b2158 s2157
4793 T t2158 o747 b2158 b914
4794 B b2159 t2158
4795 T t2159 o746 b2159 b4 b2148
4796 B b2160 t2159
4797 T t2160 o2 b2160
4798 B b2161 t2160
4799 T t2161 o746 b2157 b4 b2161
4800 B b2162 t2161
4801 T t2162 o2 b2162
4802 B b2163 t2162
4803 T t2163 o746 b2155 b4 b2163
4804 B b2164 t2163
4805 T t2164 o b2164 b4
4806 B b2165 t2164
4807 T t2165 o b2153 b2165
4808 B b2166 t2165
4809 T t2166 o745 b2127 b2166
4810 B b2167 t2166
4811 P p2167 String "lt_add_ltT ttca thenT rwh unfold_lt 0 thenT rwh lt_DiscretC 0 ttca thenT rwh reduceC 0 ttca"
4812 O o2167 ext_rule p2167
4813 T t2167 o745 b2153 b4
4814 B b2168 t2167
4815 T t2168 o2167 b744 b2168 b4 b4
4816 B b2169 t2168
4817 T t2169 o745 b2164 b4
4818 B b2170 t2169
4819 T t2170 o1662 b744 b2170 b4 b4
4820 B b2171 t2170
4821 T t2171 o b2171 b4
4822 B b2172 t2171
4823 T t2172 o b2169 b2172
4824 B b2173 t2172
4825 T t2173 o1623 b744 b2167 b2173 b4
4826 B b2174 t2173
4827 T t2174 o b2174 b4
4828 B b2175 t2174
4829 T t2193 o721 b621 b755 b755
4830 T t2195 o603 b587 b923 b898
4831 B b2195 t2195
4832 T t2196 o605 b755 b589
4833 B b2196 t2196
4834 T t2197 o586 b587 b622 b2196
4835 B b2197 t2197
4836 T t2224 o730 b596
4837 T t2226 o732 b596 b733
4838 S s2226 t726 h
4839 G s2226 t2226
4840 B b2226 s2226
4841 T t2227 o719 b2226
4842 B b2227 t2227
4843 NCzf_itt_subset Czf_itt_subset Czf_itt_subset NIL
4844 NCzf_itt_subset!subset subset subset Czf_itt_subset
4845 O o2250 subset
4846 P p2270 Var s1
4847 O o2270 var p2270
4848 T t2270 o2270
4849 B b2270 t2270
4850 P p2272 Var s2
4851 O o2272 var p2272
4852 T t2273 o2272
4853 B b2273 t2273
4854 T t319 o309 b2270 b2273
4855 H h319 x t319
4856 T t320 o12 b2270
4857 B b320 t320
4858 T t322 o730 b320
4859 S s322 t721 h h307 h308 h319
4860 G s322 t322
4861 B b322 s322
4862 T t331 o586 b587 b320 b589
4863 B b331 t331
4864 T t334 o730 b331
4865 S s334 t721 h h307 h308 h319
4866 G s334 t334
4867 B b334 s334
4868 T t340 o12 b2273
4869 B b340 t340
4870 T t345 o586 b587 b340 b589
4871 B b345 t345
4872 T t346 o309 b331 b345
4873 S s346 t726 h h307 h308 h319
4874 G s346 t346
4875 B b346 s346
4876 NItt_logic!implies implies implies Itt_logic
4877 O o348 implies
4878 B b350 t319
4879 B b357 t346
4880 T t357 o348 b350 b357
4881 S s357 t726 h h307 h308
4882 G s357 t357
4883 B b361 s357
4884 B b365 t259
4885 B b369 t357 s2
4886 T t369 o775 b365 b369
4887 S s369 t726 h h307
4888 G s369 t369
4889 B b370 s369
4890 B b410 t369 s1
4891 T t410 o775 b365 b410
4892 S s410 t726 h
4893 G s410 t410
4894 B b423 s410
4895 T t479 o730 b340
4896 S s479 t721 h h307 h308 h319
4897 G s479 t479
4898 B b480 s479
4899 T t488 o730 b345
4900 S s488 t721 h h307 h308 h319
4901 G s488 t488
4902 B b489 s488
4903 NCzf_itt_eq!eq eq eq Czf_itt_eq
4904 O o507 eq
4905 T t511 o507 b331 b345
4906 S s511 t726 h h307 h308 h319
4907 G s511 t511
4908 B b511 s511
4909 P p534 String "funSetT 2 ttca"
4910 O o535 ext_rule p534
4911 P p542 String "funSetT 3 ttca"
4912 O o543 ext_rule p542
4913 P p550 String "assertT << isset{'f['s1]} >> ttca"
4914 O o551 ext_rule p550
4915 S s551 t726 h h307 h308 h319
4916 G s551 t322
4917 B b556 s551
4918 H h564 v t322
4919 S s564 t726 h h307 h308 h319 h564
4920 G s564 t511
4921 B b570 s564
4922 P p596 String "assertT << isset{'f['s2]} >> ttca"
4923 O o597 ext_rule p596
4924 S s597 t726 h h307 h308 h319 h564
4925 G s597 t479
4926 B b600 s597
4927 H h603 v_1 t479
4928 S s603 t726 h h307 h308 h319 h564 h603
4929 G s603 t511
4930 B b605 s603
4931 P p636 String "genAssumT [3] thenT autoT thenT dT 7 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
4932 O o641 ext_rule p636
4933 H h641 v_2 t757
4934 T t654 o586 b587 b320 b758
4935 B b654 t654
4936 T t655 o586 b587 b340 b758
4937 B b655 t655
4938 T t656 o507 b654 b655
4939 H h656 z t656
4940 T t659 o604 b587 b320
4941 B b659 t659
4942 T t661 o603 b587 b659 b654
4943 B b661 t661 i j
4944 T t662 o586 b587 b320 b762
4945 B b662 t662
4946 T t677 o603 b587 b320 b662
4947 B b677 t677 k l
4948 T t680 o602 b755 b661 b610 b677
4949 B b680 t680
4950 T t681 o604 b587 b340
4951 B b681 t681
4952 T t704 o603 b587 b681 b655
4953 B b704 t704 i j
4954 T t715 o586 b587 b340 b762
4955 B b715 t715
4956 T t716 o603 b587 b340 b715
4957 B b716 t716 k l
4958 T t719 o602 b755 b704 b610 b716
4959 B b719 t719
4960 T t743 o507 b680 b719
4961 S s743 t726 h h307 h308 h319 h564 h603 h754 h641 h656
4962 G s743 t743
4963 B b743 s743
4964 T t746 o586 b587 b320 b755
4965 B b746 t746
4966 T t772 o586 b587 b340 b755
4967 B b791 t772
4968 T t795 o507 b746 b791
4969 S s796 t726 h h307 h308 h319 h564 h603 h754 h641 h656
4970 G s796 t795
4971 B b814 s796
4972 S s815 t726 h h307 h308 h319 h564 h603 h770 h754 h641 h656
4973 G s815 t795
4974 B b823 s815
4975 S s833 t726 h h307 h308 h319 h564 h603 h770
4976 G s833 t511
4977 B b877 s833
4978 B b885 t511 n
4979 T t885 o775 b621 b885
4980 S s885 t726 h h307 h308 h319 h564 h603
4981 G s885 t885
4982 B b921 s885
4983 H h2292 v_2 t791
4984 T t2292 o507 b662 b715
4985 H h2293 z t2292
4986 S s2293 t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
4987 G s2293 t743
4988 B b2299 s2293
4989 S s2312 t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
4990 G s2312 t795
4991 B b2313 s2312
4992 S s2328 t726 h h307 h308 h319 h564 h603 h770 h754 h2292 h2293
4993 G s2328 t795
4994 B b2381 s2328
4995 B b2391 t661
4996 B b2392 t704
4997 T t2392 o507 b2391 b2392
4998 S s2392 t726 h h307 h308 h319 h564 h603 h754 h641 h656
4999 G s2392 t2392
5000 B b2393 s2392
5001 P p2398 String "setSubstT << equal{power{'g; 'f['s1]; ('m +@ 1)}; power{'g; 'f['s2]; ('m +@ 1)}} >> 0 thenT autoT"
5002 O o2398 ext_rule p2398
5003 T t2398 o603 b587 b659 b655
5004 B b2399 t2398
5005 T t2399 o507 b2399 b2392
5006 S s2399 t726 h h307 h308 h319 h564 h603 h754 h641 h656
5007 G s2399 t2399
5008 B b2400 s2399
5009 P p2405 String "setSubstT << equal{inv{'g; 'f['s1]}; inv{'g; 'f['s2]}} >> 0 thenT autoT"
5010 O o2405 ext_rule p2405
5011 P p2406 String eq
5012 O o2406 tactic_arg p2406
5013 T t2406 o507 b659 b681
5014 S s2406 t726 h h307 h308 h319 h564 h603 h754 h641 h656
5015 G s2406 t2406
5016 B b2406 s2406
5017 T t2408 o309 b659 b681
5018 S s2408 t726 h h307 h308 h319 h564 h603 h754 h641 h656
5019 G s2408 t2408
5020 B b2408 s2408
5021 P p2415 String "setSubstT << equal{'f['s1]; 'f['s2]} >> 0 thenT autoT"
5022 O o2415 ext_rule p2415
5023 T t2416 o507 b320 b340
5024 S s2416 t726 h h307 h308 h319 h564 h603 h754 h641 h656
5025 G s2416 t2416
5026 B b2416 s2416
5027 T t2418 o309 b320 b340
5028 S s2418 t726 h h307 h308 h319 h564 h603 h754 h641 h656
5029 G s2418 t2418
5030 B b2418 s2418
5031 P p2425 String "assumT 4 thenT rwh unfold_fun_set 10 thenT instHypT [<< 's1 >>; << 's2 >>] 10 thenT autoT thenT dT 11 ttca thenT rwh unfold_equal 11 ttca"
5032 O o2425 ext_rule p2425
5033 B b2436 t677
5034 B b2437 t716
5035 T t2437 o507 b2436 b2437
5036 S s2437 t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
5037 G s2437 t2437
5038 B b2438 s2437
5039 P p2443 String "setSubstT << equal{power{'g; 'f['s1]; ('m -@ 1)}; power{'g; 'f['s2]; ('m -@ 1)}} >> 0 thenT autoT"
5040 O o2443 ext_rule p2443
5041 T t2443 o603 b587 b320 b715
5042 B b2444 t2443
5043 T t2444 o507 b2444 b2437
5044 S s2444 t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
5045 G s2444 t2444
5046 B b2445 s2444
5047 P p2450 String "setSubstT << equal{'f['s1]; 'f['s2]} >> 0 ttca"
5048 O o2450 ext_rule p2450
5049 S s2450 t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
5050 G s2450 t2418
5051 B b2451 s2450
5052 P p2456 String "assumT 4 thenT rwh unfold_fun_set 10 thenT instHypT [<< 's1 >>; << 's2 >>] 10 ttca thenT dT 11 ttca"
5053 O o2456 ext_rule p2456
5054 P p2487 String power_equiv_fun
5055 O o2487 rule p2487
5056 NCzf_itt_equiv!equiv_fun_set equiv_fun_set equiv_fun_set Czf_itt_equiv
5057 O o2488 equiv_fun_set
5058 T t2488 o2488 b733 b886 b244
5059 S s2488 t726 h
5060 G s2488 t2488
5061 B b2488 s2488
5062 T t2490 o2488 b733 b886 b267
5063 S s2490 t726 h
5064 G s2490 t2490
5065 B b2490 s2490
5066 T t2498 o b2488 b4
5067 B b2498 t2498
5068 T t2499 o b889 b2498
5069 B b2499 t2499
5070 T t2500 o b729 b2499
5071 B b2500 t2500
5072 T t2501 o b727 b2500
5073 B b2501 t2501
5074 T t2502 o b723 b2501
5075 B b2502 t2502
5076 T t2503 o b887 b2502
5077 B b2503 t2503
5078 T t2504 o747 b2490 b2503
5079 B b2504 t2504
5080 T t2505 o746 b2504 b4 b753
5081 B b2505 t2505
5082 B b2506 t889
5083 P p2506 Var b
5084 O o2506 var p2506
5085 T t2506 o2506
5086 B b2507 t2506
5087 T t2507 o888 b733 b886 b596 b2507
5088 B b2508 t2507
5089 T t2508 o12 b596
5090 B b2509 t2508
5091 T t2509 o12 b2507
5092 B b2510 t2509
5093 T t2510 o888 b733 b886 b2509 b2510
5094 B b2511 t2510
5095 T t2511 o348 b2508 b2511
5096 B b2512 t2511
5097 T t2512 o348 b2506 b2512
5098 B b2513 t2512 b
5099 T t2513 o775 b365 b2513
5100 B b2514 t2513 a
5101 T t2514 o775 b365 b2514
5102 H h2514 v t2514
5103 H h2515 a t259
5104 H h2516 b t259
5105 H h2517 x t889
5106 H h2518 x_1 t2507
5107 H h2519 y_1 t2510
5108 T t2519 o586 b587 b2509 b589
5109 B b2519 t2519
5110 T t2520 o586 b587 b2510 b589
5111 B b2520 t2520
5112 T t2521 o888 b733 b886 b2519 b2520
5113 S s2521 t726 h h2514 h2515 h2516 h2517 h2518 h2519
5114 G s2521 t2521
5115 B b2521 s2521
5116 T t2522 o747 b2521 b2503
5117 B b2522 t2522
5118 H h2522 y t2511
5119 S s2522 t726 h h2514 h2515 h2516 h2517 h2518 h2522 h2519
5120 G s2522 t2521
5121 B b2523 s2522
5122 T t2523 o747 b2523 b2503
5123 B b2524 t2523
5124 S s2524 t726 h h2514 h2515 h2516 h2517 h2518 h2522
5125 G s2524 t2521
5126 B b2525 s2524
5127 T t2525 o747 b2525 b2503
5128 B b2526 t2525
5129 H h2526 w_1 t2512
5130 S s2526 t726 h h2514 h2515 h2516 h2517 h2518 h2526 h2522
5131 G s2526 t2521
5132 B b2527 s2526
5133 T t2527 o747 b2527 b2503
5134 B b2528 t2527
5135 S s2528 t726 h h2514 h2515 h2516 h2517 h2518 h2526
5136 G s2528 t2521
5137 B b2529 s2528
5138 T t2529 o747 b2529 b2503
5139 B b2530 t2529
5140 H h2530 w t2513
5141 S s2530 t726 h h2514 h2515 h2516 h2517 h2518 h2530 h2526
5142 G s2530 t2521
5143 B b2531 s2530
5144 T t2531 o747 b2531 b2503
5145 B b2532 t2531
5146 P p2532 String thin
5147 O o2532 arg_named p2532
5148 P p2533 String false
5149 O o2533 arg_bool p2533
5150 T t2533 o2533
5151 B b2533 t2533
5152 T t2534 o2532 b2533
5153 B b2534 t2534
5154 T t2535 o b2534 b4
5155 B b2535 t2535
5156 S s2535 t726 h h2514 h2515 h2516 h2517 h2518 h2530
5157 G s2535 t2521
5158 B b2536 s2535
5159 T t2536 o747 b2536 b2503
5160 B b2537 t2536
5161 P p2537 String with
5162 O o2537 arg_named p2537
5163 NSummary!arg_term_list arg_term_list arg_term_list Summary
5164 O o2538 arg_term_list
5165 T t2538 o b2507 b4
5166 B b2538 t2538
5167 T t2539 o2538 b2538
5168 B b2539 t2539
5169 T t2540 o2537 b2539
5170 B b2540 t2540
5171 T t2541 o b2540 b2535
5172 B b2541 t2541
5173 S s2541 t726 h h2514 h2515 h2516 h2517 h2518
5174 G s2541 t2521
5175 B b2542 s2541
5176 T t2542 o747 b2542 b2503
5177 B b2543 t2542
5178 T t2543 o b596 b4
5179 B b2544 t2543
5180 T t2544 o2538 b2544
5181 B b2545 t2544
5182 T t2545 o2537 b2545
5183 B b2546 t2545
5184 T t2546 o b2546 b2535
5185 B b2547 t2546
5186 H h2547 v t2488
5187 S s2547 t726 h h2547 h2515 h2516 h2517 h2518
5188 G s2547 t2521
5189 B b2548 s2547
5190 T t2548 o747 b2548 b2503
5191 B b2549 t2548
5192 B b2550 t2521
5193 T t2550 o348 b2508 b2550
5194 S s2550 t726 h h2547 h2515 h2516 h2517
5195 G s2550 t2550
5196 B b2551 s2550
5197 T t2551 o747 b2551 b2503
5198 B b2552 t2551
5199 B b2553 t2550
5200 T t2553 o348 b2506 b2553
5201 S s2553 t726 h h2547 h2515 h2516
5202 G s2553 t2553
5203 B b2554 s2553
5204 T t2554 o747 b2554 b2503
5205 B b2555 t2554
5206 B b2556 t2553 b
5207 T t2556 o775 b365 b2556
5208 S s2556 t726 h h2547 h2515
5209 G s2556 t2556
5210 B b2557 s2556
5211 T t2557 o747 b2557 b2503
5212 B b2558 t2557
5213 B b2559 t2556 a
5214 T t2559 o775 b365 b2559
5215 S s2559 t726 h h2547
5216 G s2559 t2559
5217 B b2560 s2559
5218 T t2560 o747 b2560 b2503
5219 B b2561 t2560
5220 S s2561 t726 h h2547
5221 G s2561 t2490
5222 B b2562 s2561
5223 T t2562 o747 b2562 b2503
5224 B b2563 t2562
5225 T t2563 o2 b2505
5226 B b2564 t2563
5227 T t2564 o746 b2563 b4 b2564
5228 B b2565 t2564
5229 T t2565 o2 b2565
5230 B b2566 t2565
5231 T t2566 o746 b2561 b4 b2566
5232 B b2567 t2566
5233 T t2567 o2 b2567
5234 B b2568 t2567
5235 T t2568 o746 b2558 b4 b2568
5236 B b2569 t2568
5237 T t2569 o2 b2569
5238 B b2570 t2569
5239 T t2570 o746 b2555 b4 b2570
5240 B b2571 t2570
5241 T t2571 o2 b2571
5242 B b2572 t2571
5243 T t2572 o746 b2552 b4 b2572
5244 B b2573 t2572
5245 T t2573 o2 b2573
5246 B b2574 t2573
5247 T t2574 o746 b2549 b4 b2574
5248 B b2575 t2574
5249 T t2575 o2 b2575
5250 B b2576 t2575
5251 T t2576 o746 b2543 b2547 b2576
5252 B b2577 t2576
5253 T t2577 o2 b2577
5254 B b2578 t2577
5255 T t2578 o746 b2537 b2541 b2578
5256 B b2579 t2578
5257 T t2579 o2 b2579
5258 B b2580 t2579
5259 T t2580 o746 b2532 b2535 b2580
5260 B b2581 t2580
5261 T t2581 o2 b2581
5262 B b2582 t2581
5263 T t2582 o746 b2530 b4 b2582
5264 B b2583 t2582
5265 T t2583 o2 b2583
5266 B b2584 t2583
5267 T t2584 o746 b2528 b4 b2584
5268 B b2585 t2584
5269 T t2585 o2 b2585
5270 B b2586 t2585
5271 T t2586 o746 b2526 b4 b2586
5272 B b2587 t2586
5273 T t2587 o2 b2587
5274 B b2588 t2587
5275 T t2588 o746 b2524 b4 b2588
5276 B b2589 t2588
5277 T t2589 o2 b2589
5278 B b2590 t2589
5279 T t2590 o746 b2522 b4 b2590
5280 B b2591 t2590
5281 P p2593 String "genAssumT [4] thenT dT 0 ttca thenT dT 8 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
5282 O o2593 ext_rule p2593
5283 H h2593 v_1 t757
5284 T t2593 o586 b587 b2509 b758
5285 B b2594 t2593
5286 T t2594 o586 b587 b2510 b758
5287 B b2595 t2594
5288 T t2595 o888 b733 b886 b2594 b2595
5289 H h2595 z t2595
5290 T t2596 o604 b587 b2509
5291 B b2596 t2596
5292 T t2597 o603 b587 b2596 b2594
5293 B b2597 t2597 i j
5294 T t2598 o586 b587 b2509 b762
5295 B b2598 t2598
5296 T t2599 o603 b587 b2509 b2598
5297 B b2599 t2599 k l
5298 T t2600 o602 b755 b2597 b610 b2599
5299 B b2600 t2600
5300 T t2601 o604 b587 b2510
5301 B b2601 t2601
5302 T t2602 o603 b587 b2601 b2595
5303 B b2602 t2602 i j
5304 T t2603 o586 b587 b2510 b762
5305 B b2603 t2603
5306 T t2604 o603 b587 b2510 b2603
5307 B b2604 t2604 k l
5308 T t2605 o602 b755 b2602 b610 b2604
5309 B b2605 t2605
5310 T t2606 o888 b733 b886 b2600 b2605
5311 S s2606 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5312 G s2606 t2606
5313 B b2606 s2606
5314 T t2607 o747 b2606 b2503
5315 B b2607 t2607
5316 T t2608 o586 b587 b2509 b755
5317 B b2608 t2608
5318 T t2609 o586 b587 b2510 b755
5319 B b2609 t2609
5320 T t2610 o888 b733 b886 b2608 b2609
5321 S s2610 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5322 G s2610 t2610
5323 B b2610 s2610
5324 T t2611 o747 b2610 b2503
5325 B b2611 t2611
5326 S s2611 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h770 h754 h2593 h2595
5327 G s2611 t2610
5328 B b2612 s2611
5329 T t2612 o747 b2612 b2503
5330 B b2613 t2612
5331 S s2613 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h770
5332 G s2613 t2521
5333 B b2614 s2613
5334 T t2614 o747 b2614 b2503
5335 B b2615 t2614
5336 B b2616 t2521 n
5337 T t2616 o775 b621 b2616
5338 S s2616 t726 h h2514 h2515 h2516 h2517 h2518 h2519
5339 G s2616 t2616
5340 B b2617 s2616
5341 T t2617 o747 b2617 b2503
5342 B b2618 t2617
5343 T t2618 o2 b2591
5344 B b2619 t2618
5345 T t2619 o774 b2618 b4 b2619
5346 B b2620 t2619
5347 T t2620 o2 b2620
5348 B b2621 t2620
5349 T t2621 o746 b2615 b4 b2621
5350 B b2622 t2621
5351 T t2622 o2 b2622
5352 B b2623 t2622
5353 T t2623 o746 b2613 b4 b2623
5354 B b2624 t2623
5355 T t2624 o2 b2624
5356 B b2625 t2624
5357 T t2625 o746 b2611 b4 b2625
5358 B b2626 t2625
5359 T t2626 o2 b2626
5360 B b2627 t2626
5361 T t2627 o746 b2607 b4 b2627
5362 B b2628 t2627
5363 H h2628 v_1 t791
5364 T t2628 o888 b733 b886 b2598 b2603
5365 H h2629 z t2628
5366 S s2629 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
5367 G s2629 t2606
5368 B b2629 s2629
5369 T t2629 o747 b2629 b2503
5370 B b2630 t2629
5371 S s2630 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
5372 G s2630 t2610
5373 B b2631 s2630
5374 T t2631 o747 b2631 b2503
5375 B b2632 t2631
5376 S s2632 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h770 h754 h2628 h2629
5377 G s2632 t2610
5378 B b2633 s2632
5379 T t2633 o747 b2633 b2503
5380 B b2634 t2633
5381 T t2634 o746 b2634 b4 b2623
5382 B b2635 t2634
5383 T t2635 o2 b2635
5384 B b2636 t2635
5385 T t2636 o746 b2632 b4 b2636
5386 B b2637 t2636
5387 T t2637 o2 b2637
5388 B b2638 t2637
5389 T t2638 o746 b2630 b4 b2638
5390 B b2639 t2638
5391 T t2639 o b2639 b4
5392 B b2640 t2639
5393 T t2640 o b2628 b2640
5394 B b2641 t2640
5395 T t2641 o745 b2591 b2641
5396 B b2642 t2641
5397 B b2643 t2597
5398 B b2644 t2602
5399 T t2644 o888 b733 b886 b2643 b2644
5400 S s2644 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5401 G s2644 t2644
5402 B b2645 s2644
5403 T t2645 o747 b2645 b2503
5404 B b2646 t2645
5405 T t2646 o2 b2628
5406 B b2647 t2646
5407 T t2647 o746 b2646 b4 b2647
5408 B b2648 t2647
5409 T t2648 o b2648 b4
5410 B b2649 t2648
5411 T t2649 o745 b2628 b2649
5412 B b2650 t2649
5413 P p2650 String "equivSubstT << equiv{car{'g}; 'R; power{'g; 'f['a]; ('m +@ 1)}; power{'g; 'f['b]; ('m +@ 1)}} >> 0 ttca"
5414 O o2650 ext_rule p2650
5415 T t2650 o603 b587 b2596 b2595
5416 B b2651 t2650
5417 T t2651 o888 b733 b886 b2651 b2644
5418 S s2651 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5419 G s2651 t2651
5420 B b2652 s2651
5421 T t2652 o747 b2652 b2503
5422 B b2653 t2652
5423 T t2653 o2 b2648
5424 B b2654 t2653
5425 T t2654 o746 b2653 b4 b2654
5426 B b2655 t2654
5427 T t2655 o603 b587 b2596 b588
5428 B b2656 t2655
5429 T t2656 o888 b733 b886 b2656 b2644
5430 B b2657 t2656 z
5431 T t2657 o1427 b733 b886 b2657
5432 S s2657 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5433 G s2657 t2657
5434 B b2658 s2657
5435 T t2658 o747 b2658 b2503
5436 B b2659 t2658
5437 T t2659 o746 b2659 b4 b2654
5438 B b2660 t2659
5439 T t2660 o b2660 b4
5440 B b2661 t2660
5441 T t2661 o b2655 b2661
5442 B b2662 t2661
5443 T t2662 o745 b2648 b2662
5444 B b2663 t2662
5445 P p2663 String "equivSubstT << equiv{car{'g}; 'R; inv{'g; 'f['a]}; inv{'g; 'f['b]}} >> 0 ttca"
5446 O o2663 ext_rule p2663
5447 T t2663 o888 b733 b886 b2596 b2601
5448 S s2663 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5449 G s2663 t2663
5450 B b2664 s2663
5451 T t2664 o747 b2664 b2503
5452 B b2665 t2664
5453 T t2665 o2 b2655
5454 B b2666 t2665
5455 T t2666 o746 b2665 b4 b2666
5456 B b2667 t2666
5457 T t2667 o888 b733 b886 b2644 b2644
5458 S s2667 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5459 G s2667 t2667
5460 B b2668 s2667
5461 T t2668 o747 b2668 b2503
5462 B b2669 t2668
5463 T t2669 o746 b2669 b4 b2666
5464 B b2670 t2669
5465 T t2670 o603 b587 b588 b2595
5466 B b2671 t2670
5467 T t2671 o888 b733 b886 b2671 b2644
5468 B b2672 t2671 z
5469 T t2672 o1427 b733 b886 b2672
5470 S s2672 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
5471 G s2672 t2672
5472 B b2673 s2672
5473 T t2673 o747 b2673 b2503
5474 B b2674 t2673
5475 T t2674 o746 b2674 b4 b2666
5476 B b2675 t2674
5477 T t2675 o b2675 b4
5478 B b2676 t2675
5479 T t2676 o b2670 b2676
5480 B b2677 t2676
5481 T t2677 o b2667 b2677
5482 B b2678 t2677
5483 T t2678 o745 b2655 b2678
5484 B b2679 t2678
5485 P p2679 String "equivSubstT << equiv{car{'g}; 'R; 'f['a]; 'f['b]} >> 0 thenT autoT thenT rwh unfold_equiv 7 ttca"
5486 O o2679 ext_rule p2679
5487 P p2681 String "autoT thenT rwh unfold_equiv 7 ttca"
5488 O o2681 ext_rule p2681
5489 T t2681 o745 b2670 b4
5490 B b2682 t2681
5491 T t2682 o2681 b744 b2682 b4 b4
5492 B b2683 t2682
5493 B b2697 t2599
5494 B b2698 t2604
5495 T t2698 o888 b733 b886 b2697 b2698
5496 S s2698 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
5497 G s2698 t2698
5498 B b2699 s2698
5499 T t2699 o747 b2699 b2503
5500 B b2700 t2699
5501 T t2700 o2 b2639
5502 B b2701 t2700
5503 T t2701 o746 b2700 b4 b2701
5504 B b2702 t2701
5505 T t2702 o b2702 b4
5506 B b2703 t2702
5507 T t2703 o745 b2639 b2703
5508 B b2704 t2703
5509 P p2704 String "equivSubstT << equiv{car{'g}; 'R; power{'g; 'f['a]; ('m -@ 1)}; power{'g; 'f['b]; ('m -@ 1)}} >> 0 ttca"
5510 O o2704 ext_rule p2704
5511 T t2704 o603 b587 b2509 b2603
5512 B b2705 t2704
5513 T t2705 o888 b733 b886 b2705 b2698
5514 S s2705 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
5515 G s2705 t2705
5516 B b2706 s2705
5517 T t2706 o747 b2706 b2503
5518 B b2707 t2706
5519 T t2707 o2 b2702
5520 B b2708 t2707
5521 T t2708 o746 b2707 b4 b2708
5522 B b2709 t2708
5523 T t2709 o603 b587 b2509 b588
5524 B b2710 t2709
5525 T t2710 o888 b733 b886 b2710 b2698
5526 B b2711 t2710 z
5527 T t2711 o1427 b733 b886 b2711
5528 S s2711 t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
5529 G s2711 t2711
5530 B b2712 s2711
5531 T t2712 o747 b2712 b2503
5532 B b2713 t2712
5533 T t2713 o746 b2713 b4 b2708
5534 B b2714 t2713
5535 T t2714 o b2714 b4
5536 B b2715 t2714
5537 T t2715 o b2709 b2715
5538 B b2716 t2715
5539 T t2716 o745 b2702 b2716
5540 B b2717 t2716
5541 P p2739 String power_equiv_fun1
5542 O o2739 rule p2739
5543 B b2740 t590 z
5544 P p2747 String autoT
5545 O o2747 ext_rule p2747
5546 P p2799 String "dT 3 thenT rwh reduceC 0 ttca"
5547 O o2799 ext_rule p2799
5548 H h2799 m_1 t621
5549 P p2800 Var m_1
5550 O o2800 var p2800
5551 T t2800 o2800
5552 B b2800 t2800
5553 T t2801 o754 b2800 b756
5554 H h2801 v t2801
5555 T t2802 o605 b2800 b606
5556 B b2802 t2802
5557 T t2803 o586 b587 b622 b2802
5558 B b2803 t2803
5559 T t2804 o603 b587 b923 b2803
5560 B b2804 t2804
5561 T t2805 o605 b755 b2802
5562 B b2805 t2805
5563 T t2806 o586 b587 b622 b2805
5564 B b2806 t2806
5565 T t2808 o586 b587 b622 b2800
5566 B b2808 t2808
5567 T t2809 o603 b587 b923 b2808
5568 B b2809 t2809
5569 T t2810 o605 b755 b2800
5570 B b2810 t2810
5571 T t2811 o586 b587 b622 b2810
5572 B b2811 t2811
5573 T t2819 o603 b587 b923 b944
5574 B b2820 t2819
5575 T t2822 o605 b755 b756
5576 B b2823 t2822
5577 T t2823 o586 b587 b622 b2823
5578 B b2824 t2823
5579 T t2833 o754 b756 b2800
5580 H h2833 v t2833
5581 T t2834 o610 b2800 b606
5582 B b2834 t2834
5583 T t2835 o586 b587 b622 b2834
5584 B b2835 t2835
5585 T t2836 o603 b587 b923 b2835
5586 B b2836 t2836
5587 T t2837 o605 b755 b2834
5588 B b2837 t2837
5589 T t2838 o586 b587 b622 b2837
5590 B b2838 t2838
5591 T t2849 o603 b587 b2808 b622
5592 B b2850 t2849
5593 T t2854 o603 b587 b923 b2850
5594 B b2855 t2854
5595 T t2863 o603 b587 b2811 b622
5596 B b2864 t2863
5597 T t2876 o603 b587 b2809 b622
5598 B b2877 t2876
5599 P p2883 String "groupCancelRightT 8 ttca"
5600 O o2883 ext_rule p2883
5601 P p2893 String "rwh unfold_power 0 thenT rwh reduceC 0 thenT rwh fold_power 0 ttca"
5602 O o2893 ext_rule p2893
5603 T t2895 o605 b2834 b606
5604 B b2896 t2895
5605 T t2896 o586 b587 b622 b2896
5606 B b2897 t2896
5607 T t2897 o603 b587 b2897 b896
5608 B b2898 t2897
5609 T t2898 o603 b587 b923 b2898
5610 B b2899 t2898
5611 T t2905 o605 b2837 b606
5612 B b2906 t2905
5613 T t2906 o586 b587 b622 b2906
5614 B b2907 t2906
5615 T t2907 o603 b587 b2907 b896
5616 B b2908 t2907
5617 T t2914 o603 b587 b923 b2897
5618 B b2915 t2914
5619 T t2915 o603 b587 b2915 b896
5620 B b2916 t2915
5621 P p2922 String "rwh unfold_sub 8 thenT rwh add_normalizeC 8 thenT rwh reduceC 8 ttca"
5622 O o2922 ext_rule p2922
5623 T t2922 o603 b587 b2809 b896
5624 B b2923 t2922
5625 T t2923 o603 b587 b2811 b896
5626 B b2924 t2923
5627 T t2926 o605 b1483 b2800
5628 B b2927 t2926
5629 T t2927 o586 b587 b622 b2927
5630 B b2928 t2927
5631 T t2928 o603 b587 b2928 b896
5632 B b2929 t2928
5633 T t2931 o605 b1489 b2800
5634 B b2932 t2931
5635 T t2932 o586 b587 b622 b2932
5636 B b2933 t2932
5637 T t2933 o603 b587 b2933 b896
5638 B b2934 t2933
5639 T t2936 o605 b756 b2800
5640 B b2937 t2936
5641 T t2937 o586 b587 b622 b2937
5642 B b2938 t2937
5643 T t2938 o603 b587 b923 b2938
5644 B b2939 t2938
5645 T t2939 o603 b587 b2939 b896
5646 B b2940 t2939
5647 T t2942 o605 b1495 b2800
5648 B b2943 t2942
5649 T t2943 o586 b587 b622 b2943
5650 B b2944 t2943
5651 T t2944 o603 b587 b2944 b896
5652 B b2945 t2944
5653 T t2947 o605 b1048 b2800
5654 B b2948 t2947
5655 T t2948 o586 b587 b622 b2948
5656 B b2949 t2948
5657 T t2949 o603 b587 b923 b2949
5658 B b2950 t2949
5659 T t2950 o603 b587 b2950 b896
5660 B b2951 t2950
5661 T t2953 o605 b1057 b2810
5662 B b2954 t2953
5663 T t2954 o586 b587 b622 b2954
5664 B b2955 t2954
5665 T t2955 o603 b587 b2955 b896
5666 B b2956 t2955
5667 T t2958 o605 b1057 b2800
5668 B b2959 t2958
5669 T t2959 o586 b587 b622 b2959
5670 B b2960 t2959
5671 T t2960 o603 b587 b923 b2960
5672 B b2961 t2960
5673 T t2961 o603 b587 b2961 b896
5674 B b2962 t2961
5675 T t2964 o605 b606 b2810
5676 B b2965 t2964
5677 T t2965 o605 b967 b2965
5678 B b2966 t2965
5679 T t2966 o586 b587 b622 b2966
5680 B b2967 t2966
5681 T t2967 o603 b587 b2967 b896
5682 B b2968 t2967
5683 T t2970 o605 b606 b2800
5684 B b2971 t2970
5685 T t2971 o605 b967 b2971
5686 B b2972 t2971
5687 T t2972 o586 b587 b622 b2972
5688 B b2973 t2972
5689 T t2973 o603 b587 b923 b2973
5690 B b2974 t2973
5691 T t2974 o603 b587 b2974 b896
5692 B b2975 t2974
5693 T t2977 o605 b755 b2971
5694 B b2978 t2977
5695 T t2978 o605 b967 b2978
5696 B b2979 t2978
5697 T t2979 o586 b587 b622 b2979
5698 B b2980 t2979
5699 T t2980 o603 b587 b2980 b896
5700 B b2981 t2980
5701 T t2983 o605 b755 b2972
5702 B b2984 t2983
5703 T t2984 o586 b587 b622 b2984
5704 B b2985 t2984
5705 T t2985 o603 b587 b2985 b896
5706 B b2986 t2985
5707 T t2988 o605 b967 b2802
5708 B b2989 t2988
5709 T t2989 o605 b755 b2989
5710 B b2990 t2989
5711 T t2990 o586 b587 b622 b2990
5712 B b2991 t2990
5713 T t2991 o603 b587 b2991 b896
5714 B b2992 t2991
5715 T t2994 o605 b2800 b1057
5716 B b2995 t2994
5717 T t2995 o605 b755 b2995
5718 B b2996 t2995
5719 T t2996 o586 b587 b622 b2996
5720 B b2997 t2996
5721 T t2997 o603 b587 b2997 b896
5722 B b2998 t2997
5723 T t3000 o586 b587 b622 b2989
5724 B b3001 t3000
5725 T t3001 o603 b587 b923 b3001
5726 B b3002 t3001
5727 T t3002 o603 b587 b3002 b896
5728 B b3003 t3002
5729 T t3005 o586 b587 b622 b2995
5730 B b3006 t3005
5731 T t3006 o603 b587 b923 b3006
5732 B b3007 t3006
5733 T t3007 o603 b587 b3007 b896
5734 B b3008 t3007
5735 T t3010 o605 b2800 b967
5736 B b3011 t3010
5737 T t3011 o605 b3011 b606
5738 B b3012 t3011
5739 T t3012 o605 b755 b3012
5740 B b3013 t3012
5741 T t3013 o586 b587 b622 b3013
5742 B b3014 t3013
5743 T t3014 o603 b587 b3014 b896
5744 B b3015 t3014
5745 T t3017 o605 b755 b3011
5746 B b3018 t3017
5747 T t3018 o605 b3018 b606
5748 B b3019 t3018
5749 T t3019 o586 b587 b622 b3019
5750 B b3020 t3019
5751 T t3020 o603 b587 b3020 b896
5752 B b3021 t3020
5753 T t3023 o586 b587 b622 b3012
5754 B b3024 t3023
5755 T t3024 o603 b587 b923 b3024
5756 B b3025 t3024
5757 T t3025 o603 b587 b3025 b896
5758 B b3026 t3025
5759 P p2314 Var s
5760 O o2314 var p2314
5761 T t2314 o2314
5762 B b2314 t2314
5763 T t635 o18 b2314 b587 b596
5764 B b636 t635
5765 T t636 o16 b636
5766 B b653 t636
5767 T t663 o661 b653
5768 B b663 t663
5769 P p663 Number 655
5770 P p664 Number 816
5771 O o664 location p663 p664
5772 T t664 o664 b616
5773 B b664 t664
5774 P p665 Number 818
5775 P p666 Number 971
5776 O o666 location p665 p666
5777 P p620 String unfold_cyc_subg
5778 O o623 rewrite p620
5779 NItt_logic!and and and Itt_logic
5780 O o644 and
5781 B b656 t727
5782 T t774 o726 b2314
5783 B b1680 t774
5784 T t1680 o733 b2314
5785 B b1681 t1680
5786 T t1681 o309 b1681 b624
5787 B b1682 t1681
5788 T t1683 o732 b2507 b1681
5789 B b1684 t1683
5790 NCzf_itt_group!eqG eqG eqG Czf_itt_group
5791 O o671 eqG
5792 T t706 o671 b2314
5793 B b706 t706
5794 T t711 o671 b587
5795 B b711 t711
5796 T t712 o888 b733 b711 b596 b2507
5797 B b712 t712
5798 O o670 lid p620
5799 T t670 o670
5800 B b670 t670
5801 T t2256 o b682 b685
5802 B b2256 t2256
5803 T t2257 o681 b2256 b590 b701
5804 B b2257 t2257
5805 P p712 String cyc_subg_df
5806 O o712 dform p712
5807 P p2236 String cyclic_subgroup(
5808 O o2236 string687 p2236
5809 T t2242 o2236
5810 B b2242 t2242
5811 T t2351 o689 b2314
5812 B b2351 t2351
5813 T t2263 o b689 b709
5814 B b2263 t2263
5815 T t2264 o b690 b2263
5816 B b2264 t2264
5817 T t2272 o b2351 b2264
5818 B b2272 t2272
5819 T t2275 o b2242 b2272
5820 B b2275 t2275
5821 T t2276 o687 b2275
5822 B b2276 t2276
5823 T t2277 o712 b705 b636 b2276
5824 B b2277 t2277
5825 S s723 t721 h
5826 G s723 t729
5827 B b726 s723
5828 T t777 o719 b726
5829 B b817 t777
5830 S s817 t721 h
5831 G s817 t731
5832 B b818 s817
5833 T t818 o719 b818
5834 B b819 t818
5835 T t2284 o718 b817 b737
5836 B b2284 t2284
5837 T t2285 o718 b819 b2284
5838 B b2285 t2285
5839 T t2293 o718 b724 b2285
5840 B b2293 t2293
5841 T t2296 o b726 b4
5842 B b2296 t2296
5843 T t2297 o b818 b2296
5844 B b2297 t2297
5845 T t2298 o b723 b2297
5846 B b2298 t2298
5847 T t2300 o747 b736 b2298
5848 B b2300 t2300
5849 T t2301 o746 b2300 b4 b753
5850 B b2301 t2301
5851 T t2306 o747 b766 b2298
5852 B b2306 t2306
5853 T t2310 o747 b769 b2298
5854 B b2310 t2310
5855 T t2311 o747 b771 b2298
5856 B b2311 t2311
5857 T t2312 o747 b773 b2298
5858 B b2315 t2312
5859 T t2315 o747 b776 b2298
5860 B b2316 t2315
5861 T t2316 o2 b2301
5862 B b2317 t2316
5863 T t2317 o774 b2316 b780 b2317
5864 B b2318 t2317
5865 T t2318 o2 b2318
5866 B b2319 t2318
5867 T t2324 o746 b2315 b4 b2319
5868 B b2329 t2324
5869 T t2329 o2 b2329
5870 B b2331 t2329
5871 T t2331 o746 b2311 b4 b2331
5872 B b2332 t2331
5873 T t2332 o2 b2332
5874 B b2338 t2332
5875 T t2338 o746 b2310 b4 b2338
5876 B b2339 t2338
5877 T t2339 o2 b2339
5878 B b2340 t2339
5879 T t2340 o746 b2306 b4 b2340
5880 B b2341 t2340
5881 T t2341 o747 b792 b2298
5882 B b2342 t2341
5883 T t2342 o747 b794 b2298
5884 B b2343 t2342
5885 T t2343 o747 b796 b2298
5886 B b2347 t2343
5887 T t2347 o746 b2347 b4 b2331
5888 B b2349 t2347
5889 T t2349 o2 b2349
5890 B b2350 t2349
5891 T t2350 o746 b2343 b4 b2350
5892 B b2355 t2350
5893 T t2355 o2 b2355
5894 B b2356 t2355
5895 T t2356 o746 b2342 b4 b2356
5896 B b2357 t2356
5897 T t2357 o b2357 b4
5898 B b2358 t2357
5899 T t2362 o b2341 b2358
5900 B b2362 t2362
5901 T t2363 o745 b2301 b2362
5902 B b2363 t2363
5903 T t2364 o745 b2341 b4
5904 B b2364 t2364
5905 T t2365 o805 b744 b2364 b4 b4
5906 B b2365 t2365
5907 T t2366 o745 b2357 b4
5908 B b2366 t2366
5909 T t2367 o807 b744 b2366 b4 b4
5910 B b2367 t2367
5911 T t2369 o b2367 b4
5912 B b2370 t2369
5913 T t2370 o b2365 b2370
5914 B b2371 t2370
5915 T t2371 o743 b744 b2363 b2371 b4
5916 B b2372 t2371
5917 T t2372 o742 b2372
5918 B b2373 t2372
5919 T t2229 o718 b819 b826
5920 B b2229 t2229
5921 T t2230 o718 b817 b2229
5922 B b2230 t2230
5923 T t2231 o718 b728 b2230
5924 B b2232 t2231
5925 T t2232 o718 b724 b2232
5926 B b2233 t2232
5927 T t2480 o b818 b747
5928 B b2480 t2480
5929 T t2486 o b726 b2480
5930 B b2486 t2486
5931 T t2487 o b727 b2486
5932 B b2487 t2487
5933 T t2494 o b723 b2487
5934 B b2494 t2494
5935 T t2495 o747 b824 b2494
5936 B b2495 t2495
5937 T t2496 o746 b2495 b4 b753
5938 B b2496 t2496
5939 T t2497 o747 b834 b2494
5940 B b2497 t2497
5941 T t2515 o747 b836 b2494
5942 B b2515 t2515
5943 T t2516 o747 b838 b2494
5944 B b2517 t2516
5945 T t2517 o747 b840 b2494
5946 B b2733 t2517
5947 T t2733 o747 b843 b2494
5948 B b2744 t2733
5949 T t2744 o2 b2496
5950 B b2745 t2744
5951 T t2745 o774 b2744 b780 b2745
5952 B b2746 t2745
5953 T t2746 o2 b2746
5954 B b2747 t2746
5955 T t2758 o746 b2733 b4 b2747
5956 B b2758 t2758
5957 T t2760 o2 b2758
5958 B b2761 t2760
5959 T t2761 o746 b2517 b4 b2761
5960 B b2762 t2761
5961 T t2762 o2 b2762
5962 B b2763 t2762
5963 T t2763 o746 b2515 b4 b2763
5964 B b2764 t2763
5965 T t2764 o2 b2764
5966 B b2765 t2764
5967 T t2765 o746 b2497 b4 b2765
5968 B b2766 t2765
5969 T t2766 o747 b855 b2494
5970 B b2767 t2766
5971 T t2767 o747 b857 b2494
5972 B b2768 t2767
5973 T t2785 o747 b859 b2494
5974 B b2801 t2785
5975 T t2826 o746 b2801 b4 b2761
5976 B b3086 t2826
5977 T t3086 o2 b3086
5978 B b3093 t3086
5979 T t3093 o746 b2768 b4 b3093
5980 B b3094 t3093
5981 T t3094 o2 b3094
5982 B b3095 t3094
5983 T t3095 o746 b2767 b4 b3095
5984 B b3102 t3095
5985 T t3102 o b3102 b4
5986 B b3120 t3102
5987 T t3120 o b2766 b3120
5988 B b3121 t3120
5989 T t3121 o745 b2496 b3121
5990 B b3129 t3121
5991 T t3129 o745 b2766 b4
5992 B b3130 t3129
5993 T t3130 o805 b744 b3130 b4 b4
5994 B b3149 t3130
5995 T t3149 o745 b3102 b4
5996 B b3165 t3149
5997 T t3165 o807 b744 b3165 b4 b4
5998 B b3179 t3165
5999 T t3179 o b3179 b4
6000 B b3185 t3179
6001 T t3186 o b3149 b3185
6002 B b3187 t3186
6003 T t3187 o743 b744 b3129 b3187 b4
6004 B b3189 t3187
6005 T t3189 o742 b3189
6006 B b3191 t3189
6007 T t2253 o718 b817 b273
6008 B b2253 t2253
6009 T t2254 o718 b728 b2253
6010 B b2254 t2254
6011 T t2258 o718 b724 b2254
6012 B b2258 t2258
6013 T t3203 o b726 b296
6014 B b3204 t3203
6015 T t3204 o b727 b3204
6016 B b3205 t3204
6017 T t3205 o b723 b3205
6018 B b3206 t3205
6019 T t3206 o747 b268 b3206
6020 B b3207 t3206
6021 T t3207 o746 b3207 b4 b753
6022 B b3208 t3207
6023 T t3208 o747 b322 b3206
6024 B b3209 t3208
6025 T t3209 o747 b334 b3206
6026 B b3210 t3209
6027 T t3210 o747 b346 b3206
6028 B b3211 t3210
6029 T t3215 o747 b361 b3206
6030 B b3216 t3215
6031 T t3216 o747 b370 b3206
6032 B b3217 t3216
6033 T t3217 o747 b423 b3206
6034 B b3218 t3217
6035 T t3218 o2 b3208
6036 B b3219 t3218
6037 T t3219 o746 b3218 b780 b3219
6038 B b3220 t3219
6039 T t3222 o2 b3220
6040 B b3222 t3222
6041 T t3223 o746 b3217 b780 b3222
6042 B b3223 t3223
6043 T t3224 o2 b3223
6044 B b3224 t3224
6045 T t3225 o746 b3216 b780 b3224
6046 B b3225 t3225
6047 T t3226 o2 b3225
6048 B b3226 t3226
6049 T t3227 o746 b3211 b780 b3226
6050 B b3227 t3227
6051 T t3230 o2 b3227
6052 B b3233 t3230
6053 T t3233 o307 b3210 b780 b3233
6054 B b3234 t3233
6055 T t3234 o2 b3234
6056 B b3235 t3234
6057 T t3235 o307 b3209 b4 b3235
6058 B b3236 t3235
6059 T t3236 o747 b480 b3206
6060 B b3237 t3236
6061 T t3237 o747 b489 b3206
6062 B b3238 t3237
6063 T t3238 o307 b3238 b780 b3233
6064 B b3239 t3238
6065 T t3239 o2 b3239
6066 B b3240 t3239
6067 T t3240 o307 b3237 b4 b3240
6068 B b3241 t3240