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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3570 - (hide 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 xiny 3404 #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 xiny 3502 P p59 String Itt_atom_bool
185 xiny 3404 O o59 parent p59
186     T t60 o59
187     B b60 t60
188     T t61 o b60 b4
189     B b61 t61
190 xiny 3502 P p61 String Itt_atom
191 xiny 3404 O o61 parent p61
192     T t62 o61
193     B b62 t62
194     T t63 o b62 b4
195     B b63 t63
196 xiny 3502 P p63 String Itt_record_label0
197 xiny 3404 O o63 parent p63
198     T t64 o63
199     B b64 t64
200     T t65 o b64 b4
201     B b65 t65
202 xiny 3502 P p65 String Itt_nat
203 xiny 3404 O o65 parent p65
204     T t66 o65
205     B b66 t66
206     T t67 o b66 b4
207     B b67 t67
208 xiny 3502 P p67 String Itt_int_ext
209 xiny 3404 O o67 parent p67
210     T t68 o67
211     B b68 t68
212     T t69 o b68 b4
213     B b69 t69
214 xiny 3502 P p69 String Itt_int_base
215 xiny 3404 O o69 parent p69
216     T t70 o69
217     B b70 t70
218     T t71 o b70 b4
219     B b71 t71
220 xiny 3502 P p71 String Itt_bool
221 xiny 3404 O o71 parent p71
222     T t72 o71
223     B b72 t72
224     T t73 o b72 b4
225     B b73 t73
226 xiny 3502 P p73 String Itt_decidable
227 xiny 3404 O o73 parent p73
228     T t74 o73
229     B b74 t74
230     T t75 o b74 b4
231     B b75 t75
232 xiny 3502 P p75 String Itt_logic
233 xiny 3404 O o75 parent p75
234     T t76 o75
235     B b76 t76
236     T t77 o b76 b4
237     B b77 t77
238 xiny 3502 P p77 String Itt_union
239 xiny 3404 O o77 parent p77
240     T t78 o77
241     B b78 t78
242     T t79 o b78 b4
243     B b79 t79
244 xiny 3502 P p79 String Itt_prod
245 xiny 3404 O o79 parent p79
246     T t80 o79
247     B b80 t80
248     T t81 o b80 b4
249     B b81 t81
250 xiny 3502 P p81 String Itt_dprod
251 xiny 3404 O o81 parent p81
252     T t82 o81
253     B b82 t82
254     T t83 o b82 b4
255     B b83 t83
256 xiny 3502 P p83 String Itt_fun
257 xiny 3404 O o83 parent p83
258     T t84 o83
259     B b84 t84
260     T t85 o b84 b4
261     B b85 t85
262 xiny 3502 P p85 String Itt_dfun
263 xiny 3404 O o85 parent p85
264     T t86 o85
265     B b86 t86
266     T t87 o b86 b4
267     B b87 t87
268 xiny 3502 P p87 String Itt_rfun
269 xiny 3404 O o87 parent p87
270     T t88 o87
271     B b88 t88
272     T t89 o b88 b4
273     B b89 t89
274 xiny 3502 P p89 String Itt_void
275 xiny 3404 O o89 parent p89
276     T t90 o89
277     B b90 t90
278     T t91 o b90 b4
279     B b91 t91
280 xiny 3502 P p91 String Itt_set
281 xiny 3404 O o91 parent p91
282     T t92 o91
283     B b92 t92
284     T t93 o b92 b4
285     B b93 t93
286 xiny 3502 P p93 String Itt_unit
287 xiny 3404 O o93 parent p93
288     T t94 o93
289     B b94 t94
290     T t95 o b94 b4
291     B b95 t95
292 xiny 3502 P p95 String Itt_squiggle
293 xiny 3404 O o95 parent p95
294     T t96 o95
295     B b96 t96
296     T t97 o b96 b4
297     B b97 t97
298 xiny 3502 P p97 String Itt_subtype
299 xiny 3404 O o97 parent p97
300     T t98 o97
301     B b98 t98
302     T t99 o b98 b4
303     B b99 t99
304 xiny 3502 P p99 String Itt_squash
305 xiny 3404 O o99 parent p99
306     T t100 o99
307     B b100 t100
308     T t101 o b100 b4
309     B b101 t101
310 xiny 3502 P p101 String Itt_struct
311 xiny 3404 O o101 parent p101
312     T t102 o101
313     B b102 t102
314     T t103 o b102 b4
315     B b103 t103
316 xiny 3502 P p103 String Itt_equal
317 xiny 3404 O o103 parent p103
318     T t104 o103
319     B b104 t104
320     T t105 o b104 b4
321     B b105 t105
322 xiny 3502 P p105 String Itt_comment
323 xiny 3404 O o105 parent p105
324     T t106 o105
325     B b106 t106
326     T t107 o b106 b4
327     B b107 t107
328 xiny 3502 P p107 String Base_theory
329 xiny 3404 O o107 parent p107
330     T t108 o107
331     B b108 t108
332     T t109 o b108 b4
333     B b109 t109
334 xiny 3502 P p109 String Base_meta
335 xiny 3404 O o109 parent p109
336     T t110 o109
337     B b110 t110
338     T t111 o b110 b4
339     B b111 t111
340 xiny 3502 P p111 String Base_cache
341 xiny 3404 O o111 parent p111
342     T t112 o111
343     B b112 t112
344     T t113 o b112 b4
345     B b113 t113
346 xiny 3502 P p113 String Tactic_cache
347 xiny 3404 O o113 parent p113
348     T t114 o113
349     B b114 t114
350     T t115 o b114 b4
351     B b115 t115
352 xiny 3502 P p115 String Typeinf
353 xiny 3404 O o115 parent p115
354     T t116 o115
355     B b116 t116
356     T t117 o b116 b4
357     B b117 t117
358 xiny 3502 P p117 String Ocaml_df
359 xiny 3404 O o117 parent p117
360     T t118 o117
361     B b118 t118
362     T t119 o b118 b4
363     B b119 t119
364 xiny 3502 P p119 String Ocaml_str_df
365 xiny 3404 O o119 parent p119
366     T t120 o119
367     B b120 t120
368     T t121 o b120 b4
369     B b121 t121
370 xiny 3502 P p121 String Ocaml_sig_df
371 xiny 3404 O o121 parent p121
372     T t122 o121
373     B b122 t122
374     T t123 o b122 b4
375     B b123 t123
376 xiny 3502 P p123 String Ocaml_me_df
377 xiny 3404 O o123 parent p123
378     T t124 o123
379     B b124 t124
380     T t125 o b124 b4
381     B b125 t125
382 xiny 3502 P p125 String Ocaml_mt_df
383 xiny 3404 O o125 parent p125
384     T t126 o125
385     B b126 t126
386     T t127 o b126 b4
387     B b127 t127
388 xiny 3502 P p127 String Ocaml_type_df
389 xiny 3404 O o127 parent p127
390     T t128 o127
391     B b128 t128
392     T t129 o b128 b4
393     B b129 t129
394 xiny 3502 P p129 String Ocaml_patt_df
395 xiny 3404 O o129 parent p129
396     T t130 o129
397     B b130 t130
398     T t131 o b130 b4
399     B b131 t131
400 xiny 3502 P p131 String Ocaml_expr_df
401 xiny 3404 O o131 parent p131
402     T t132 o131
403     B b132 t132
404     T t133 o b132 b4
405     B b133 t133
406 xiny 3502 P p133 String Ocaml_base_df
407 xiny 3404 O o133 parent p133
408     T t134 o133
409     B b134 t134
410     T t135 o b134 b4
411     B b135 t135
412 xiny 3502 P p135 String Ocaml
413 xiny 3404 O o135 parent p135
414     T t136 o135
415     B b136 t136
416     T t137 o b136 b4
417     B b137 t137
418 xiny 3502 P p137 String Base_rewrite
419 xiny 3404 O o137 parent p137
420     T t138 o137
421     B b138 t138
422     T t139 o b138 b4
423     B b139 t139
424 xiny 3502 P p139 String Base_dtactic
425 xiny 3404 O o139 parent p139
426     T t140 o139
427     B b140 t140
428     T t141 o b140 b4
429     B b141 t141
430 xiny 3502 P p141 String Base_auto_tactic
431 xiny 3404 O o141 parent p141
432     T t142 o141
433     B b142 t142
434     T t143 o b142 b4
435     B b143 t143
436 xiny 3502 P p143 String Base_trivial
437 xiny 3404 O o143 parent p143
438     T t144 o143
439     B b144 t144
440     T t145 o b144 b4
441     B b145 t145
442 xiny 3502 P p145 String Top_conversionals
443 xiny 3404 O o145 parent p145
444     T t146 o145
445     B b146 t146
446     T t147 o b146 b4
447     B b147 t147
448 xiny 3502 P p147 String Top_tacticals
449 xiny 3404 O o147 parent p147
450     T t148 o147
451     B b148 t148
452     T t149 o b148 b4
453     B b149 t149
454 xiny 3502 P p149 String Var
455 xiny 3404 O o149 parent p149
456     T t150 o149
457     B b150 t150
458     T t151 o b150 b4
459     B b151 t151
460 xiny 3502 P p151 String Mptop
461 xiny 3404 O o151 parent p151
462     T t152 o151
463     B b152 t152
464     T t153 o b152 b4
465     B b153 t153
466 xiny 3502 P p153 String Summary
467 xiny 3404 O o153 parent p153
468     T t154 o153
469     B b154 t154
470     T t155 o b154 b4
471     B b155 t155
472 xiny 3502 P p155 String Comment
473 xiny 3404 O o155 parent p155
474     T t156 o155
475     B b156 t156
476     T t157 o b156 b4
477     B b157 t157
478 xiny 3502 P p157 String Base_dform
479 xiny 3404 O o157 parent p157
480     T t158 o157
481     B b158 t158
482     T t159 o b158 b4
483     B b159 t159
484 xiny 3502 P p159 String Nuprl_font
485     O o159 parent p159
486     T t160 o159
487 xiny 3404 B b160 t160
488 xiny 3502 T t161 o b160 b4
489 xiny 3404 B b161 t161
490 xiny 3502 P p161 String Perv
491     O o161 parent p161
492     T t162 o161
493 xiny 3404 B b162 t162
494 xiny 3502 T t163 o b162 b4
495 xiny 3404 B b163 t163
496 xiny 3502 T t164 o b163 b4
497 xiny 3404 B b164 t164
498 xiny 3502 T t165 o b161 b164
499 xiny 3404 B b165 t165
500 xiny 3502 T t166 o b159 b165
501 xiny 3404 B b166 t166
502 xiny 3502 T t167 o b157 b166
503 xiny 3404 B b167 t167
504 xiny 3502 T t168 o b155 b167
505 xiny 3404 B b168 t168
506 xiny 3502 T t169 o b153 b168
507 xiny 3404 B b169 t169
508 xiny 3502 T t170 o b151 b169
509 xiny 3404 B b170 t170
510 xiny 3502 T t171 o b149 b170
511 xiny 3404 B b171 t171
512 xiny 3502 T t172 o b147 b171
513 xiny 3404 B b172 t172
514 xiny 3502 T t173 o b145 b172
515 xiny 3404 B b173 t173
516 xiny 3502 T t174 o b143 b173
517 xiny 3404 B b174 t174
518 xiny 3502 T t175 o b141 b174
519 xiny 3404 B b175 t175
520 xiny 3502 T t176 o b139 b175
521 xiny 3404 B b176 t176
522 xiny 3502 T t177 o b137 b176
523 xiny 3404 B b177 t177
524 xiny 3502 T t178 o b135 b177
525 xiny 3404 B b178 t178
526 xiny 3502 T t179 o b133 b178
527 xiny 3404 B b179 t179
528 xiny 3502 T t180 o b131 b179
529 xiny 3404 B b180 t180
530 xiny 3502 T t181 o b129 b180
531 xiny 3404 B b181 t181
532 xiny 3502 T t182 o b127 b181
533 xiny 3404 B b182 t182
534 xiny 3502 T t183 o b125 b182
535 xiny 3404 B b183 t183
536 xiny 3502 T t184 o b123 b183
537 xiny 3404 B b184 t184
538 xiny 3502 T t185 o b121 b184
539 xiny 3404 B b185 t185
540 xiny 3502 T t186 o b119 b185
541 xiny 3404 B b186 t186
542 xiny 3502 T t187 o b117 b186
543 xiny 3404 B b187 t187
544 xiny 3502 T t188 o b115 b187
545 xiny 3404 B b188 t188
546 xiny 3502 T t189 o b113 b188
547 xiny 3404 B b189 t189
548 xiny 3502 T t190 o b111 b189
549 xiny 3404 B b190 t190
550 xiny 3502 T t191 o b109 b190
551 xiny 3404 B b191 t191
552 xiny 3502 T t192 o b107 b191
553 xiny 3404 B b192 t192
554 xiny 3502 T t193 o b105 b192
555 xiny 3404 B b193 t193
556 xiny 3502 T t194 o b103 b193
557 xiny 3404 B b194 t194
558 xiny 3502 T t195 o b101 b194
559 xiny 3404 B b195 t195
560 xiny 3502 T t196 o b99 b195
561 xiny 3404 B b196 t196
562 xiny 3502 T t197 o b97 b196
563 xiny 3404 B b197 t197
564 xiny 3502 T t198 o b95 b197
565 xiny 3404 B b198 t198
566 xiny 3502 T t199 o b93 b198
567 xiny 3404 B b199 t199
568 xiny 3502 T t200 o b91 b199
569 xiny 3404 B b200 t200
570 xiny 3502 T t201 o b89 b200
571 xiny 3404 B b201 t201
572 xiny 3502 T t202 o b87 b201
573 xiny 3404 B b202 t202
574 xiny 3502 T t203 o b85 b202
575 xiny 3404 B b203 t203
576 xiny 3502 T t204 o b83 b203
577 xiny 3404 B b204 t204
578 xiny 3502 T t205 o b81 b204
579 xiny 3404 B b205 t205
580 xiny 3502 T t206 o b79 b205
581 xiny 3404 B b206 t206
582 xiny 3502 T t207 o b77 b206
583 xiny 3404 B b207 t207
584 xiny 3502 T t208 o b75 b207
585 xiny 3404 B b208 t208
586 xiny 3502 T t209 o b73 b208
587 xiny 3404 B b209 t209
588 xiny 3502 T t210 o b71 b209
589 xiny 3404 B b210 t210
590 xiny 3502 T t211 o b69 b210
591 xiny 3404 B b211 t211
592 xiny 3502 T t212 o b67 b211
593 xiny 3404 B b212 t212
594 xiny 3502 T t213 o b65 b212
595 xiny 3404 B b213 t213
596 xiny 3502 T t214 o b63 b213
597 xiny 3404 B b214 t214
598 xiny 3502 T t215 o b61 b214
599 xiny 3404 B b215 t215
600 xiny 3502 T t216 o b59 b215
601 xiny 3404 B b216 t216
602 xiny 3502 T t217 o b57 b216
603 xiny 3404 B b217 t217
604 xiny 3502 T t218 o b55 b217
605 xiny 3404 B b218 t218
606 xiny 3502 T t219 o b53 b218
607 xiny 3404 B b219 t219
608 xiny 3502 T t220 o b51 b219
609 xiny 3404 B b220 t220
610 xiny 3502 T t221 o b49 b220
611 xiny 3404 B b221 t221
612 xiny 3502 T t222 o b47 b221
613 xiny 3404 B b222 t222
614 xiny 3502 T t223 o b45 b222
615 xiny 3404 B b223 t223
616 xiny 3502 T t224 o b43 b223
617 xiny 3404 B b224 t224
618 xiny 3502 T t225 o b41 b224
619 xiny 3404 B b225 t225
620 xiny 3502 T t226 o b39 b225
621 xiny 3404 B b226 t226
622 xiny 3502 T t227 o b37 b226
623 xiny 3404 B b227 t227
624 xiny 3502 T t228 o b35 b227
625 xiny 3404 B b228 t228
626 xiny 3502 T t229 o b33 b228
627 xiny 3404 B b229 t229
628 xiny 3502 T t230 o b31 b229
629 xiny 3404 B b230 t230
630 xiny 3502 T t231 o b29 b230
631 xiny 3404 B b231 t231
632 xiny 3502 T t232 o b27 b231
633 xiny 3404 B b232 t232
634 xiny 3502 T t233 o b25 b232
635 xiny 3404 B b233 t233
636 xiny 3502 T t234 o b23 b233
637 xiny 3404 B b234 t234
638 xiny 3502 T t235 o b21 b234
639 xiny 3404 B b235 t235
640 xiny 3502 T t236 o b19 b235
641 xiny 3404 B b236 t236
642 xiny 3502 T t237 o b17 b236
643 xiny 3404 B b237 t237
644 xiny 3502 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 xiny 3404 NSummary!resource resource resource Summary
655 xiny 3502 P p243 String auto
656     O o243 resource p243
657 xiny 3404 NOcaml Ocaml Ocaml NIL
658     NOcaml!type_lid type_lid type_lid Ocaml
659 xiny 3502 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 xiny 3404 B b246 t246
666 xiny 3502 T t247 o245 b246
667 xiny 3404 B b247 t247
668 xiny 3502 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 xiny 3404 B b250 t250
678 xiny 3502 T t251 o249 b250
679 xiny 3404 B b251 t251
680 xiny 3502 P p251 Number 2352
681     P p252 Number 2358
682     O o252 type_lid p251 p252
683     T t252 o252 b250
684 xiny 3404 B b252 t252
685 xiny 3502 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 xiny 3404 B b255 t255
693 xiny 3502 T t256 o b251 b255
694 xiny 3404 B b256 t256
695 xiny 3502 T t257 o248 b256
696     B b257 t257
697     T t258 o243 b247 b257
698 xiny 3404 B b258 t258
699 xiny 3502 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 xiny 3404 T t264 o264
715     B b264 t264
716     T t265 o263 b264
717     B b265 t265
718 xiny 3502 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 xiny 3404 B b270 t270
731 xiny 3502 T t271 o269 b270
732 xiny 3404 B b271 t271
733 xiny 3502 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 xiny 3404 B b274 t274
743 xiny 3502 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 xiny 3404 B b276 t276
749 xiny 3502 T t277 o272 b275 b276
750 xiny 3404 B b277 t277
751 xiny 3502 T t278 o b277 b4
752 xiny 3404 B b278 t278
753 xiny 3502 T t279 o b271 b278
754 xiny 3404 B b279 t279
755 xiny 3502 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 xiny 3404 O o282 type_lid p280 p282
762 xiny 3502 T t282 o282 b274
763 xiny 3404 B b282 t282
764 xiny 3502 P p283 Number 1792
765 xiny 3404 O o283 type_lid p283 p281
766 xiny 3502 T t283 o283 b250
767 xiny 3404 B b283 t283
768 xiny 3502 T t284 o281 b282 b283
769 xiny 3404 B b284 t284
770 xiny 3502 T t285 o266 b280 b284
771 xiny 3404 B b285 t285
772 xiny 3502 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 xiny 3404 B b288 t288
781 xiny 3502 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 xiny 3404 B b291 t291
789 xiny 3502 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 xiny 3404 B b301 t301
816 xiny 3502 T t302 o300 b301
817 xiny 3404 B b302 t302
818 xiny 3502 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 xiny 3404 B b305 t305
828 xiny 3502 T t306 o304 b305
829 xiny 3404 B b306 t306
830 xiny 3502 P p306 Number 1835
831     O o306 type_lid p302 p306
832     T t307 o306 b274
833 xiny 3404 B b307 t307
834 xiny 3502 T t308 o303 b306 b307
835 xiny 3404 B b308 t308
836 xiny 3502 P p308 Number 1845
837     O o308 type_lid p308 p299
838     T t309 o308 b250
839 xiny 3404 B b309 t309
840 xiny 3502 T t310 o b309 b4
841 xiny 3404 B b310 t310
842 xiny 3502 T t311 o b308 b310
843 xiny 3404 B b311 t311
844 xiny 3502 T t312 o b302 b311
845 xiny 3404 B b312 t312
846 xiny 3502 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 xiny 3404 B b315 t315
852 xiny 3502 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 xiny 3404 B b317 t317
859 xiny 3502 T t318 o294 b316 b317
860 xiny 3404 B b318 t318
861 xiny 3502 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 xiny 3404 B b321 t321
870 xiny 3502 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 xiny 3404 B b323 t323
876 xiny 3502 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 xiny 3404 B b326 t326
882 xiny 3502 T t327 o320 b326
883 xiny 3404 B b327 t327
884 xiny 3502 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 xiny 3404 B b329 t329
891 xiny 3502 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 xiny 3404 B b332 t332
900 xiny 3502 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 xiny 3404 B b335 t335
909 xiny 3502 P p336 Number 4037
910     O o336 type_lid p336 p334
911     T t336 o336 b250
912 xiny 3404 B b336 t336
913 xiny 3502 T t337 o334 b335 b336
914 xiny 3404 B b337 t337
915 xiny 3502 T t338 o329 b333 b337
916 xiny 3404 B b338 t338
917 xiny 3502 P p338 String sub
918 xiny 3404 O o338 resource p338
919 xiny 3502 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 xiny 3404 B b341 t341
926 xiny 3502 T t342 o340 b341
927     B b342 t342
928     P p342 Number 4901
929     P p343 Number 4907
930 xiny 3404 O o343 type_lid p342 p343
931 xiny 3502 T t343 o343 b250
932 xiny 3404 B b343 t343
933 xiny 3502 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 xiny 3404 B b347 t347
944 xiny 3502 P p348 Number 2454
945     P p349 Number 2460
946     O o349 type_lid p348 p349
947     T t349 o349 b301
948 xiny 3404 B b349 t349
949 xiny 3502 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 xiny 3404 B b352 t352
957 xiny 3502 T t353 o b352 b4
958 xiny 3404 B b353 t353
959 xiny 3502 T t354 o b349 b353
960 xiny 3404 B b354 t354
961 xiny 3502 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 xiny 3404 B b358 t358
972 xiny 3502 T t359 o357 b358
973     B b359 t359
974     T t360 o344 b356 b359
975 xiny 3404 B b360 t360
976 xiny 3502 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 xiny 3404 B b366 t366
994 xiny 3502 T t367 o365 b366
995 xiny 3404 B b367 t367
996 xiny 3502 T t368 o360 b364 b367
997 xiny 3404 B b368 t368
998 xiny 3502 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 xiny 3404 B b371 t371
1007 xiny 3502 T t372 o370 b371
1008 xiny 3404 B b372 t372
1009 xiny 3502 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 xiny 3404 B b373 t373
1015 xiny 3502 T t374 o372 b373
1016 xiny 3404 B b374 t374
1017 xiny 3502 T t375 o368 b372 b374
1018 xiny 3404 B b375 t375
1019 xiny 3502 T t376 o b375 b4
1020 xiny 3404 B b376 t376
1021 xiny 3502 T t377 o b368 b376
1022 xiny 3404 B b377 t377
1023 xiny 3502 T t378 o b360 b377
1024 xiny 3404 B b378 t378
1025 xiny 3502 T t379 o b344 b378
1026 xiny 3404 B b379 t379
1027 xiny 3502 T t380 o b338 b379
1028 xiny 3404 B b380 t380
1029 xiny 3502 T t381 o b329 b380
1030 xiny 3404 B b381 t381
1031 xiny 3502 T t382 o b318 b381
1032 xiny 3404 B b382 t382
1033 xiny 3502 T t383 o b294 b382
1034     B b383 t383
1035     T t384 o b285 b383
1036 xiny 3404 B b384 t384
1037 xiny 3502 T t385 o b266 b384
1038 xiny 3404 B b385 t385
1039 xiny 3502 T t386 o b258 b385
1040     B b386 t386
1041     P p388 Number 22
1042 xiny 3539 P p390 String Czf_itt_equiv
1043 xiny 3404 O o390 parent p390
1044     T t390 o390
1045     B b390 t390
1046     T t391 o b390 b4
1047     B b391 t391
1048 xiny 3539 P p391 String Czf_itt_pair
1049 xiny 3502 O o391 parent p391
1050     T t392 o391
1051 xiny 3404 B b392 t392
1052 xiny 3502 T t393 o b392 b4
1053     B b393 t393
1054 xiny 3539 P p393 String Czf_itt_singleton
1055 xiny 3502 O o393 parent p393
1056     T t394 o393
1057     B b394 t394
1058     T t395 o b394 b4
1059     B b395 t395
1060 xiny 3539 P p395 String Czf_itt_union
1061 xiny 3502 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 xiny 3491 B b398 t398
1070 xiny 3502 T t399 o b398 b4
1071 xiny 3491 B b399 t399
1072 xiny 3539 P p399 String Czf_itt_dexists
1073     O o399 parent p399
1074     T t400 o399
1075 xiny 3502 B b400 t400
1076 xiny 3539 T t401 o b400 b4
1077 xiny 3502 B b401 t401
1078 xiny 3557 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 xiny 3570 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 xiny 3557 T t594 o2 b391 b4 b386
1112     B b599 t594
1113 xiny 3539 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 xiny 3404 B b414 t414
1125 xiny 3539 T t415 o b414 b4
1126 xiny 3404 B b415 t415
1127 xiny 3539 T t416 o b412 b415
1128 xiny 3404 B b416 t416
1129 xiny 3539 T t417 o2 b412 b416 b386
1130 xiny 3404 B b417 t417
1131 xiny 3539 P p418 Number 69
1132 xiny 3570 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 xiny 3539 T t419 o2 b399 b4 b386
1144 xiny 3502 B b419 t419
1145 xiny 3570 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 xiny 3539 T t421 o2 b71 b4 b386
1151 xiny 3502 B b421 t421
1152 xiny 3570 T t402 o392 b421
1153     B b402 t402
1154     P p402 Number 140
1155 xiny 3539 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 xiny 3404 B b426 t426
1163 xiny 3539 P p426 String TermType
1164     O o427 string p426
1165     T t427 o427
1166 xiny 3404 B b427 t427
1167 xiny 3539 T t428 o b427 b4
1168 xiny 3502 B b428 t428
1169 xiny 3539 T t429 o b426 b428
1170 xiny 3502 B b429 t429
1171 xiny 3539 T t430 o b426 b429
1172 xiny 3502 B b430 t430
1173 xiny 3539 P p434 Number 169
1174 xiny 3570 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 xiny 3539 P p435 String Term
1183     O o436 string p435
1184     T t436 o436
1185 xiny 3404 B b436 t436
1186 xiny 3539 T t437 o b436 b4
1187 xiny 3502 B b437 t437
1188 xiny 3539 T t438 o b426 b437
1189 xiny 3502 B b438 t438
1190 xiny 3539 T t439 o b426 b438
1191 xiny 3502 B b439 t439
1192 xiny 3539 P p442 Number 170
1193 xiny 3570 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 xiny 3539 P p444 String TermOp
1207     O o445 string p444
1208     T t445 o445
1209 xiny 3404 B b445 t445
1210 xiny 3539 T t446 o b445 b4
1211 xiny 3502 B b446 t446
1212 xiny 3539 T t447 o b426 b446
1213 xiny 3502 B b447 t447
1214 xiny 3539 T t448 o b426 b447
1215 xiny 3502 B b448 t448
1216 xiny 3570 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 xiny 3539 P p453 String TermAddr
1227     O o454 string p453
1228     T t454 o454
1229 xiny 3404 B b454 t454
1230 xiny 3539 T t455 o b454 b4
1231 xiny 3502 B b455 t455
1232 xiny 3539 T t456 o b426 b455
1233 xiny 3502 B b456 t456
1234 xiny 3539 T t457 o b426 b456
1235 xiny 3502 B b457 t457
1236 xiny 3570 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 xiny 3539 P p462 String TermMan
1247     O o463 string p462
1248     T t463 o463
1249 xiny 3404 B b463 t463
1250 xiny 3539 T t464 o b463 b4
1251 xiny 3502 B b464 t464
1252 xiny 3539 T t465 o b426 b464
1253 xiny 3502 B b465 t465
1254 xiny 3539 T t466 o b426 b465
1255 xiny 3502 B b466 t466
1256 xiny 3570 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 xiny 3539 P p471 String TermSubst
1267     O o472 string p471
1268     T t472 o472
1269 xiny 3404 B b472 t472
1270 xiny 3539 T t473 o b472 b4
1271 xiny 3502 B b473 t473
1272 xiny 3539 T t474 o b426 b473
1273 xiny 3502 B b474 t474
1274 xiny 3539 T t475 o b426 b474
1275 xiny 3502 B b475 t475
1276 xiny 3570 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 xiny 3539 P p480 String Refine
1287     O o481 string p480
1288     T t481 o481
1289 xiny 3404 B b481 t481
1290 xiny 3539 T t482 o b481 b4
1291 xiny 3502 B b482 t482
1292 xiny 3539 T t483 o b426 b482
1293 xiny 3502 B b483 t483
1294 xiny 3539 T t484 o b426 b483
1295 xiny 3502 B b484 t484
1296 xiny 3570 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 xiny 3539 P p489 String RefineError
1307     O o490 string p489
1308     T t490 o490
1309 xiny 3502 B b490 t490
1310 xiny 3539 T t491 o b490 b4
1311 xiny 3502 B b491 t491
1312 xiny 3539 T t492 o b426 b491
1313     B b492 t492
1314     T t493 o b426 b492
1315     B b493 t493
1316 xiny 3570 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 xiny 3539 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 xiny 3570 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 xiny 3539 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 xiny 3570 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 xiny 3539 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 xiny 3570 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 xiny 3539 P p526 String Tactic_type
1391     O o527 string p526
1392     T t527 o527
1393 xiny 3404 B b527 t527
1394 xiny 3539 T t528 o b527 b4
1395     B b528 t528
1396 xiny 3570 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 xiny 3539 P p532 Number 454
1403     P p533 String Tacticals
1404     O o534 string p533
1405     T t534 o534
1406 xiny 3404 B b534 t534
1407 xiny 3539 T t535 o b534 b4
1408 xiny 3404 B b535 t535
1409 xiny 3539 T t536 o b527 b535
1410     B b536 t536
1411     P p541 String Sequent
1412     O o542 string p541
1413     T t542 o542
1414 xiny 3404 B b542 t542
1415 xiny 3539 T t543 o b542 b4
1416 xiny 3404 B b543 t543
1417 xiny 3539 T t544 o b527 b543
1418     B b544 t544
1419     P p547 Number 480
1420 xiny 3570 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 xiny 3539 P p549 String Conversionals
1443     O o550 string p549
1444     T t550 o550
1445 xiny 3404 B b550 t550
1446 xiny 3539 T t551 o b550 b4
1447     B b551 t551
1448     T t552 o b527 b551
1449     B b552 t552
1450 xiny 3570 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 xiny 3539 O o558 string p151
1461     T t558 o558
1462     B b558 t558
1463     T t559 o b558 b4
1464     B b559 t559
1465 xiny 3570 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 xiny 3539 O o565 string p149
1476     T t565 o565
1477     B b565 t565
1478     T t566 o b565 b4
1479     B b566 t566
1480 xiny 3570 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 xiny 3539 O o572 string p139
1491     T t572 o572
1492     B b572 t572
1493     T t573 o b572 b4
1494     B b573 t573
1495 xiny 3570 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 xiny 3539 O o579 string p141
1506     T t579 o579
1507     B b579 t579
1508     T t580 o b579 b4
1509     B b580 t580
1510 xiny 3570 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 xiny 3502 NSummary!opname opname opname Summary
1517 xiny 3539 P p585 String power
1518     O o585 opname p585
1519 xiny 3502 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 xiny 3539 O o586 power
1522 xiny 3502 Nvar var var NIL
1523 xiny 3539 P p586 Var g
1524     O o587 var p586
1525     T t587 o587
1526 xiny 3502 B b587 t587
1527 xiny 3539 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 xiny 3570 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 xiny 3539 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 xiny 3404 NSummary!rewrite rewrite rewrite Summary
1556 xiny 3539 P p601 String unfold_power
1557     O o601 rewrite p601
1558 xiny 3404 NItt_int_base Itt_int_base Itt_int_base NIL
1559     NItt_int_base!ind ind ind Itt_int_base
1560 xiny 3539 O o602 ind
1561 xiny 3404 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1562     NCzf_itt_group!op op op Czf_itt_group
1563 xiny 3539 O o603 op
1564 xiny 3404 NCzf_itt_group!inv inv inv Czf_itt_group
1565 xiny 3539 O o604 inv
1566     T t604 o604 b587 b588
1567     B b604 t604
1568 xiny 3404 NItt_int_base!add add add Itt_int_base
1569 xiny 3539 O o605 add
1570 xiny 3404 NItt_int_base!number number number Itt_int_base
1571 xiny 3539 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 xiny 3404 NCzf_itt_group!id id id Czf_itt_group
1582 xiny 3539 O o609 id
1583     T t610 o609 b587
1584     B b610 t610
1585 xiny 3404 NItt_int_base!sub sub sub Itt_int_base
1586 xiny 3539 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 xiny 3404 NSummary!prim prim prim Summary
1596 xiny 3539 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 xiny 3404 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1602     NCzf_itt_set!collect collect collect Czf_itt_set
1603 xiny 3539 O o620 collect
1604 xiny 3404 NItt_int_base!int int int Itt_int_base
1605 xiny 3539 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 xiny 3404 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 xiny 3539 P p634 String makeFoldC
1622     O o634 lid p634
1623     T t634 o634
1624     B b634 t634
1625 xiny 3404 NOcaml!proj proj proj Ocaml
1626     NOcaml!uid uid uid Ocaml
1627 xiny 3539 P p637 String Ml_term
1628     O o638 uid p637
1629     T t638 o638
1630 xiny 3502 B b638 t638
1631 xiny 3539 P p639 String term_of_string
1632     O o640 lid p639
1633     T t640 o640
1634 xiny 3502 B b640 t640
1635 xiny 3539 O o646 lid p601
1636     T t646 o646
1637 xiny 3502 B b646 t646
1638     NSummary!dform dform dform Summary
1639 xiny 3539 P p681 String power_df
1640     O o681 dform p681
1641 xiny 3502 NSummary!except_mode_df except_mode_df except_mode_df Summary
1642 xiny 3539 P p682 String src
1643     O o682 except_mode_df p682
1644     T t682 o682
1645     B b682 t682
1646 xiny 3502 NSummary!parens_df parens_df parens_df Summary
1647 xiny 3539 O o684 parens_df
1648     T t684 o684
1649 xiny 3502 B b684 t684
1650 xiny 3539 T t685 o b684 b4
1651 xiny 3502 B b685 t685
1652 xiny 3539 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 xiny 3502 B b688 t688
1659 xiny 3539 Nslot slot slot NIL
1660     O o689 slot
1661     T t689 o689 b587
1662 xiny 3502 B b689 t689
1663 xiny 3539 P p689 String "; "
1664     O o690 string687 p689
1665     T t690 o690
1666 xiny 3502 B b690 t690
1667 xiny 3539 T t691 o689 b588
1668 xiny 3502 B b691 t691
1669 xiny 3539 T t692 o689 b589
1670     B b692 t692
1671     P p692 String )
1672     O o692 string687 p692
1673     T t693 o692
1674 xiny 3502 B b693 t693
1675 xiny 3539 T t694 o b693 b4
1676 xiny 3502 B b694 t694
1677 xiny 3539 T t695 o b692 b694
1678 xiny 3502 B b695 t695
1679 xiny 3539 T t696 o b690 b695
1680 xiny 3502 B b696 t696
1681 xiny 3539 T t697 o b691 b696
1682 xiny 3502 B b697 t697
1683 xiny 3539 T t698 o b690 b697
1684 xiny 3502 B b698 t698
1685 xiny 3539 T t699 o b689 b698
1686 xiny 3502 B b699 t699
1687 xiny 3539 T t700 o b688 b699
1688 xiny 3502 B b700 t700
1689 xiny 3539 T t701 o687 b700
1690 xiny 3502 B b701 t701
1691 xiny 3539 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 xiny 3404 NSummary!rule rule rule Summary
1700 xiny 3539 P p716 String power_wf1
1701     O o716 rule p716
1702 xiny 3404 NSummary!context_param context_param context_param Summary
1703 xiny 3539 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 xiny 3502 NSummary!meta_implies meta_implies meta_implies Summary
1710 xiny 3539 O o718 meta_implies
1711 xiny 3404 NSummary!meta_theorem meta_theorem meta_theorem Summary
1712 xiny 3539 O o719 meta_theorem
1713 xiny 3502 NBase_trivial Base_trivial Base_trivial NIL
1714     NBase_trivial!squash squash squash Base_trivial
1715 xiny 3539 O o720 squash
1716     T t720 o720
1717     B b720 t720
1718     T t721 o b720 b4
1719 xiny 3404 C h H
1720 xiny 3502 NItt_equal Itt_equal Itt_equal NIL
1721     NItt_equal!equal equal equal Itt_equal
1722 xiny 3539 O o721 equal
1723 xiny 3502 NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1724     NItt_record_label0!label label label Itt_record_label0
1725 xiny 3539 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 xiny 3502 NCzf_itt_group!group group group Czf_itt_group
1740 xiny 3539 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 xiny 3404 NCzf_itt_set!isset isset isset Czf_itt_set
1752 xiny 3539 O o730 isset
1753     T t731 o730 b588
1754 xiny 3404 NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1755     NCzf_itt_member!mem mem mem Czf_itt_member
1756 xiny 3539 O o732 mem
1757 xiny 3404 NCzf_itt_group!car car car Czf_itt_group
1758 xiny 3539 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 xiny 3404 B b735 t735
1767 xiny 3539 T t736 o730 b590
1768     S s736 t726 h
1769     G s736 t736
1770     B b736 s736
1771     T t737 o719 b736
1772 xiny 3502 B b737 t737
1773 xiny 3539 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 xiny 3502 B b744 t744
1782 xiny 3539 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 xiny 3502 B b747 t747
1791 xiny 3539 NSummary!parent_none parent_none parent_none Summary
1792     O o752 parent_none
1793     T t753 o752
1794 xiny 3502 B b753 t753
1795 xiny 3539 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 xiny 3502 B b755 t755
1802 xiny 3539 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 xiny 3502 B b758 t758
1809 xiny 3539 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 xiny 3488 B b762 t762
1817 xiny 3539 T t763 o586 b587 b588 b762
1818 xiny 3488 B b763 t763
1819 xiny 3539 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 xiny 3502 B b768 t768
1829 xiny 3539 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 xiny 3488 B b778 t778
1858 xiny 3539 T t779 o777 b778
1859     B b779 t779
1860     T t780 o b779 b4
1861 xiny 3502 B b780 t780
1862 xiny 3539 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 xiny 3502 B b816 t816
1884 xiny 3539 P p824 String power_wf2
1885     O o824 rule p824
1886     T t824 o732 b590 b733
1887     S s824 t726 h
1888 xiny 3502 G s824 t824
1889     B b824 s824
1890 xiny 3539 T t825 o719 b824
1891 xiny 3502 B b825 t825
1892 xiny 3539 T t826 o718 b735 b825
1893 xiny 3502 B b826 t826
1894 xiny 3539 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 xiny 3502 B b886 t886
1982 xiny 3539 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 xiny 3502 B b894 t894
2003 xiny 3539 T t895 o586 b587 b622 b607
2004 xiny 3502 B b895 t895
2005 xiny 3539 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 xiny 3502 B b898 t898
2011 xiny 3539 T t899 o888 b733 b886 b897 b898
2012     S s899 t726 h
2013 xiny 3502 G s899 t899
2014     B b899 s899
2015 xiny 3539 T t908 o b893 b4
2016 xiny 3502 B b908 t908
2017 xiny 3539 T t909 o b891 b908
2018 xiny 3502 B b909 t909
2019 xiny 3539 T t910 o b729 b909
2020 xiny 3502 B b910 t910
2021 xiny 3539 T t911 o b889 b910
2022 xiny 3493 B b911 t911
2023 xiny 3539 T t912 o b727 b911
2024     B b912 t912
2025     T t913 o b723 b912
2026 xiny 3493 B b913 t913
2027 xiny 3539 T t914 o b887 b913
2028 xiny 3493 B b914 t914
2029 xiny 3539 T t915 o747 b899 b914
2030 xiny 3493 B b915 t915
2031 xiny 3539 T t916 o746 b915 b4 b753
2032 xiny 3493 B b916 t916
2033 xiny 3539 T t917 o605 b758 b606
2034 xiny 3502 B b917 t917
2035 xiny 3539 T t918 o586 b587 b622 b917
2036 xiny 3502 B b918 t918
2037 xiny 3539 T t919 o603 b587 b918 b896
2038 xiny 3502 B b919 t919
2039 xiny 3539 T t920 o586 b587 b622 b758
2040 xiny 3493 B b920 t920
2041 xiny 3539 T t921 o888 b733 b886 b919 b920
2042     H h921 z t921
2043     T t922 o603 b587 b920 b896
2044 xiny 3502 B b922 t922
2045 xiny 3539 T t923 o586 b587 b622 b755
2046 xiny 3502 B b923 t923
2047 xiny 3539 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 xiny 3502 B b925 t925
2053 xiny 3539 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