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

Diff of /metaprl/theories/czf/czf_itt_cyclic_group.prla

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3557 by xiny, Mon Mar 11 10:04:22 2002 UTC revision 3558 by xiny, Tue Apr 2 08:27:06 2002 UTC
# Line 9  Line 9 
9  O       o1      location p p1  O       o1      location p p1
10  NSummary!parent parent  parent Summary  NSummary!parent parent  parent Summary
11  O       o2      parent  O       o2      parent
12  P       p8      String Czf_itt_equiv  P       p2      String Czf_itt_equiv
 O       o12     parent p8  
 T       t191    o12  
 B       b191    t191  
 P       p2      String Czf_itt_group  
13  O       o3      parent p2  O       o3      parent p2
14  T       t       o3  T       t       o3
15  B       b       t  B       b       t
# Line 21  Line 17 
17  O       o4      nil3  O       o4      nil3
18  T       t4      o4  T       t4      o4
19  B       b4      t4  B       b4      t4
 T       t192    o b191 b4  
 B       b192    t192  
 P       p192    String Czf_itt_pair  
 O       o192    parent p192  
 T       t193    o192  
 B       b193    t193  
 T       t194    o b193 b4  
 B       b194    t194  
 P       p194    String Czf_itt_singleton  
 O       o194    parent p194  
 T       t195    o194  
 B       b195    t195  
 T       t196    o b195 b4  
 B       b196    t196  
20  T       t5      o b b4  T       t5      o b b4
21  B       b5      t5  B       b5      t5
22  P       p5      String Czf_itt_and  P       p5      String Czf_itt_pair
23  O       o5      parent p5  O       o5      parent p5
24  T       t6      o5  T       t6      o5
25  B       b6      t6  B       b6      t6
26  T       t7      o b6 b4  T       t7      o b6 b4
27  B       b7      t7  B       b7      t7
28  P       p7      String Czf_itt_dall  P       p7      String Czf_itt_singleton
29  O       o7      parent p7  O       o7      parent p7
30  T       t8      o7  T       t8      o7
31  B       b8      t8  B       b8      t8
32  T       t9      o b8 b4  T       t9      o b8 b4
33  B       b9      t9  B       b9      t9
34  P       p9      String Czf_itt_set_ind  P       p9      String Czf_itt_union
35  O       o9      parent p9  O       o9      parent p9
36  T       t10     o9  T       t10     o9
37  B       b10     t10  B       b10     t10
38  T       t11     o b10 b4  T       t11     o b10 b4
39  B       b11     t11  B       b11     t11
40  P       p11     String Czf_itt_all  P       p11     String Czf_itt_subset
41  O       o11     parent p11  O       o11     parent p11
42  T       t12     o11  T       t12     o11
43  B       b12     t12  B       b12     t12
44  T       t13     o b12 b4  T       t13     o b12 b4
45  B       b13     t13  B       b13     t13
46  P       p13     String Czf_itt_sep  P       p13     String Czf_itt_dall
47  O       o13     parent p13  O       o13     parent p13
48  T       t14     o13  T       t14     o13
49  B       b14     t14  B       b14     t14
50  T       t15     o b14 b4  T       t15     o b14 b4
51  B       b15     t15  B       b15     t15
52  P       p15     String Czf_itt_member  P       p15     String Czf_itt_all
53  O       o15     parent p15  O       o15     parent p15
54  T       t16     o15  T       t16     o15
55  B       b16     t16  B       b16     t16
56  T       t17     o b16 b4  T       t17     o b16 b4
57  B       b17     t17  B       b17     t17
58  P       p17     String Czf_itt_eq  P       p17     String Czf_itt_dexists
59  O       o17     parent p17  O       o17     parent p17
60  T       t18     o17  T       t18     o17
61  B       b18     t18  B       b18     t18
62  T       t19     o b18 b4  T       t19     o b18 b4
63  B       b19     t19  B       b19     t19
64  P       p19     String Czf_itt_set  P       p19     String Czf_itt_set_ind
65  O       o19     parent p19  O       o19     parent p19
66  T       t20     o19  T       t20     o19
67  B       b20     t20  B       b20     t20
68  T       t21     o b20 b4  T       t21     o b20 b4
69  B       b21     t21  B       b21     t21
70  P       p21     String Czf_itt_comment  P       p21     String Czf_itt_sep
71  O       o21     parent p21  O       o21     parent p21
72  T       t22     o21  T       t22     o21
73  B       b22     t22  B       b22     t22
74  T       t23     o b22 b4  T       t23     o b22 b4
75  B       b23     t23  B       b23     t23
76  P       p23     String Itt_theory  P       p23     String Czf_itt_member
77  O       o23     parent p23  O       o23     parent p23
78  T       t24     o23  T       t24     o23
79  B       b24     t24  B       b24     t24
80  T       t25     o b24 b4  T       t25     o b24 b4
81  B       b25     t25  B       b25     t25
82  P       p25     String Itt_fset  P       p25     String Czf_itt_eq
83  O       o25     parent p25  O       o25     parent p25
84  T       t26     o25  T       t26     o25
85  B       b26     t26  B       b26     t26
86  T       t27     o b26 b4  T       t27     o b26 b4
87  B       b27     t27  B       b27     t27
88  P       p27     String Itt_prop_decide  P       p27     String Czf_itt_set
89  O       o27     parent p27  O       o27     parent p27
90  T       t28     o27  T       t28     o27
91  B       b28     t28  B       b28     t28
92  T       t29     o b28 b4  T       t29     o b28 b4
93  B       b29     t29  B       b29     t29
94  P       p29     String Itt_derive  P       p29     String Czf_itt_comment
95  O       o29     parent p29  O       o29     parent p29
96  T       t30     o29  T       t30     o29
97  B       b30     t30  B       b30     t30
98  T       t31     o b30 b4  T       t31     o b30 b4
99  B       b31     t31  B       b31     t31
100  P       p31     String Itt_list2  P       p31     String Itt_theory
101  O       o31     parent p31  O       o31     parent p31
102  T       t32     o31  T       t32     o31
103  B       b32     t32  B       b32     t32
104  T       t33     o b32 b4  T       t33     o b32 b4
105  B       b33     t33  B       b33     t33
106  P       p33     String Itt_list  P       p33     String Itt_fset
107  O       o33     parent p33  O       o33     parent p33
108  T       t34     o33  T       t34     o33
109  B       b34     t34  B       b34     t34
110  T       t35     o b34 b4  T       t35     o b34 b4
111  B       b35     t35  B       b35     t35
112  P       p35     String Itt_quotient  P       p35     String Itt_prop_decide
113  O       o35     parent p35  O       o35     parent p35
114  T       t36     o35  T       t36     o35
115  B       b36     t36  B       b36     t36
116  T       t37     o b36 b4  T       t37     o b36 b4
117  B       b37     t37  B       b37     t37
118  P       p37     String Itt_esquash  P       p37     String Itt_derive
119  O       o37     parent p37  O       o37     parent p37
120  T       t38     o37  T       t38     o37
121  B       b38     t38  B       b38     t38
122  T       t39     o b38 b4  T       t39     o b38 b4
123  B       b39     t39  B       b39     t39
124  P       p39     String Itt_srec  P       p39     String Itt_list2
125  O       o39     parent p39  O       o39     parent p39
126  T       t40     o39  T       t40     o39
127  B       b40     t40  B       b40     t40
128  T       t41     o b40 b4  T       t41     o b40 b4
129  B       b41     t41  B       b41     t41
130  P       p41     String Itt_prec  P       p41     String Itt_list
131  O       o41     parent p41  O       o41     parent p41
132  T       t42     o41  T       t42     o41
133  B       b42     t42  B       b42     t42
134  T       t43     o b42 b4  T       t43     o b42 b4
135  B       b43     t43  B       b43     t43
136  P       p43     String Itt_w  P       p43     String Itt_quotient
137  O       o43     parent p43  O       o43     parent p43
138  T       t44     o43  T       t44     o43
139  B       b44     t44  B       b44     t44
140  T       t45     o b44 b4  T       t45     o b44 b4
141  B       b45     t45  B       b45     t45
142  P       p45     String Itt_bunion  P       p45     String Itt_esquash
143  O       o45     parent p45  O       o45     parent p45
144  T       t46     o45  T       t46     o45
145  B       b46     t46  B       b46     t46
146  T       t47     o b46 b4  T       t47     o b46 b4
147  B       b47     t47  B       b47     t47
148  P       p47     String Itt_bisect  P       p47     String Itt_srec
149  O       o47     parent p47  O       o47     parent p47
150  T       t48     o47  T       t48     o47
151  B       b48     t48  B       b48     t48
152  T       t49     o b48 b4  T       t49     o b48 b4
153  B       b49     t49  B       b49     t49
154  P       p49     String Itt_tunion  P       p49     String Itt_prec
155  O       o49     parent p49  O       o49     parent p49
156  T       t50     o49  T       t50     o49
157  B       b50     t50  B       b50     t50
158  T       t51     o b50 b4  T       t51     o b50 b4
159  B       b51     t51  B       b51     t51
160  P       p51     String Itt_isect  P       p51     String Itt_w
161  O       o51     parent p51  O       o51     parent p51
162  T       t52     o51  T       t52     o51
163  B       b52     t52  B       b52     t52
164  T       t53     o b52 b4  T       t53     o b52 b4
165  B       b53     t53  B       b53     t53
166  P       p53     String Itt_struct2  P       p53     String Itt_bunion
167  O       o53     parent p53  O       o53     parent p53
168  T       t54     o53  T       t54     o53
169  B       b54     t54  B       b54     t54
170  T       t55     o b54 b4  T       t55     o b54 b4
171  B       b55     t55  B       b55     t55
172  P       p55     String Itt_well_founded  P       p55     String Itt_bisect
173  O       o55     parent p55  O       o55     parent p55
174  T       t56     o55  T       t56     o55
175  B       b56     t56  B       b56     t56
176  T       t57     o b56 b4  T       t57     o b56 b4
177  B       b57     t57  B       b57     t57
178  P       p57     String Itt_int_arith  P       p57     String Itt_tunion
179  O       o57     parent p57  O       o57     parent p57
180  T       t58     o57  T       t58     o57
181  B       b58     t58  B       b58     t58
182  T       t59     o b58 b4  T       t59     o b58 b4
183  B       b59     t59  B       b59     t59
184  P       p59     String Itt_int_ext  P       p59     String Itt_isect
185  O       o59     parent p59  O       o59     parent p59
186  T       t60     o59  T       t60     o59
187  B       b60     t60  B       b60     t60
188  T       t61     o b60 b4  T       t61     o b60 b4
189  B       b61     t61  B       b61     t61
190  P       p61     String Itt_int_base  P       p61     String Itt_struct2
191  O       o61     parent p61  O       o61     parent p61
192  T       t62     o61  T       t62     o61
193  B       b62     t62  B       b62     t62
194  T       t63     o b62 b4  T       t63     o b62 b4
195  B       b63     t63  B       b63     t63
196  P       p63     String Itt_atom_bool  P       p63     String Itt_well_founded
197  O       o63     parent p63  O       o63     parent p63
198  T       t64     o63  T       t64     o63
199  B       b64     t64  B       b64     t64
200  T       t65     o b64 b4  T       t65     o b64 b4
201  B       b65     t65  B       b65     t65
202  P       p65     String Itt_atom  P       p65     String Itt_int_arith
203  O       o65     parent p65  O       o65     parent p65
204  T       t66     o65  T       t66     o65
205  B       b66     t66  B       b66     t66
206  T       t67     o b66 b4  T       t67     o b66 b4
207  B       b67     t67  B       b67     t67
208  P       p6      String Itt_record_label0  P       p67     String Itt_int_ext
 O       o10     parent p6  
 T       t363    o10  
 B       b363    t363  
 T       t364    o b363 b4  
 B       b364    t364  
 P       p371    String Itt_nat  
 O       o371    parent p371  
 T       t388    o371  
 B       b388    t388  
 T       t389    o b388 b4  
 B       b389    t389  
 P       p67     String Itt_bool  
209  O       o67     parent p67  O       o67     parent p67
210  T       t68     o67  T       t68     o67
211  B       b68     t68  B       b68     t68
212  T       t69     o b68 b4  T       t69     o b68 b4
213  B       b69     t69  B       b69     t69
214  P       p69     String Itt_decidable  P       p69     String Itt_int_base
215  O       o69     parent p69  O       o69     parent p69
216  T       t70     o69  T       t70     o69
217  B       b70     t70  B       b70     t70
218  T       t71     o b70 b4  T       t71     o b70 b4
219  B       b71     t71  B       b71     t71
220  P       p71     String Itt_logic  P       p71     String Itt_atom_bool
221  O       o71     parent p71  O       o71     parent p71
222  T       t72     o71  T       t72     o71
223  B       b72     t72  B       b72     t72
224  T       t73     o b72 b4  T       t73     o b72 b4
225  B       b73     t73  B       b73     t73
226  P       p73     String Itt_prod  P       p73     String Itt_atom
227  O       o73     parent p73  O       o73     parent p73
228  T       t74     o73  T       t74     o73
229  B       b74     t74  B       b74     t74
230  T       t75     o b74 b4  T       t75     o b74 b4
231  B       b75     t75  B       b75     t75
232  P       p75     String Itt_dprod  P       p75     String Itt_bool
233  O       o75     parent p75  O       o75     parent p75
234  T       t76     o75  T       t76     o75
235  B       b76     t76  B       b76     t76
236  T       t77     o b76 b4  T       t77     o b76 b4
237  B       b77     t77  B       b77     t77
238  P       p77     String Itt_fun  P       p77     String Itt_decidable
239  O       o77     parent p77  O       o77     parent p77
240  T       t78     o77  T       t78     o77
241  B       b78     t78  B       b78     t78
242  T       t79     o b78 b4  T       t79     o b78 b4
243  B       b79     t79  B       b79     t79
244  P       p79     String Itt_dfun  P       p79     String Itt_logic
245  O       o79     parent p79  O       o79     parent p79
246  T       t80     o79  T       t80     o79
247  B       b80     t80  B       b80     t80
248  T       t81     o b80 b4  T       t81     o b80 b4
249  B       b81     t81  B       b81     t81
250  P       p81     String Itt_rfun  P       p81     String Itt_prod
251  O       o81     parent p81  O       o81     parent p81
252  T       t82     o81  T       t82     o81
253  B       b82     t82  B       b82     t82
254  T       t83     o b82 b4  T       t83     o b82 b4
255  B       b83     t83  B       b83     t83
256  P       p83     String Itt_set  P       p83     String Itt_dprod
257  O       o83     parent p83  O       o83     parent p83
258  T       t84     o83  T       t84     o83
259  B       b84     t84  B       b84     t84
260  T       t85     o b84 b4  T       t85     o b84 b4
261  B       b85     t85  B       b85     t85
262  P       p85     String Itt_unit  P       p85     String Itt_fun
263  O       o85     parent p85  O       o85     parent p85
264  T       t86     o85  T       t86     o85
265  B       b86     t86  B       b86     t86
266  T       t87     o b86 b4  T       t87     o b86 b4
267  B       b87     t87  B       b87     t87
268  P       p87     String Itt_squiggle  P       p87     String Itt_dfun
269  O       o87     parent p87  O       o87     parent p87
270  T       t88     o87  T       t88     o87
271  B       b88     t88  B       b88     t88
272  T       t89     o b88 b4  T       t89     o b88 b4
273  B       b89     t89  B       b89     t89
274  P       p89     String Itt_squash  P       p89     String Itt_rfun
275  O       o89     parent p89  O       o89     parent p89
276  T       t90     o89  T       t90     o89
277  B       b90     t90  B       b90     t90
278  T       t91     o b90 b4  T       t91     o b90 b4
279  B       b91     t91  B       b91     t91
280  P       p91     String Itt_union  P       p91     String Itt_set
281  O       o91     parent p91  O       o91     parent p91
282  T       t92     o91  T       t92     o91
283  B       b92     t92  B       b92     t92
284  T       t93     o b92 b4  T       t93     o b92 b4
285  B       b93     t93  B       b93     t93
286  P       p93     String Itt_void  P       p93     String Itt_unit
287  O       o93     parent p93  O       o93     parent p93
288  T       t94     o93  T       t94     o93
289  B       b94     t94  B       b94     t94
290  T       t95     o b94 b4  T       t95     o b94 b4
291  B       b95     t95  B       b95     t95
292  P       p95     String Itt_subtype  P       p95     String Itt_squiggle
293  O       o95     parent p95  O       o95     parent p95
294  T       t96     o95  T       t96     o95
295  B       b96     t96  B       b96     t96
296  T       t97     o b96 b4  T       t97     o b96 b4
297  B       b97     t97  B       b97     t97
298  P       p97     String Itt_struct  P       p97     String Itt_squash
299  O       o97     parent p97  O       o97     parent p97
300  T       t98     o97  T       t98     o97
301  B       b98     t98  B       b98     t98
302  T       t99     o b98 b4  T       t99     o b98 b4
303  B       b99     t99  B       b99     t99
304  P       p99     String Itt_equal  P       p99     String Itt_union
305  O       o99     parent p99  O       o99     parent p99
306  T       t100    o99  T       t100    o99
307  B       b100    t100  B       b100    t100
308  T       t101    o b100 b4  T       t101    o b100 b4
309  B       b101    t101  B       b101    t101
310  P       p101    String Itt_comment  P       p101    String Itt_void
311  O       o101    parent p101  O       o101    parent p101
312  T       t102    o101  T       t102    o101
313  B       b102    t102  B       b102    t102
314  T       t103    o b102 b4  T       t103    o b102 b4
315  B       b103    t103  B       b103    t103
316  P       p103    String Base_theory  P       p103    String Itt_subtype
317  O       o103    parent p103  O       o103    parent p103
318  T       t104    o103  T       t104    o103
319  B       b104    t104  B       b104    t104
320  T       t105    o b104 b4  T       t105    o b104 b4
321  B       b105    t105  B       b105    t105
322  P       p105    String Base_meta  P       p105    String Itt_struct
323  O       o105    parent p105  O       o105    parent p105
324  T       t106    o105  T       t106    o105
325  B       b106    t106  B       b106    t106
326  T       t107    o b106 b4  T       t107    o b106 b4
327  B       b107    t107  B       b107    t107
328  P       p107    String Base_cache  P       p107    String Itt_equal
329  O       o107    parent p107  O       o107    parent p107
330  T       t108    o107  T       t108    o107
331  B       b108    t108  B       b108    t108
332  T       t109    o b108 b4  T       t109    o b108 b4
333  B       b109    t109  B       b109    t109
334  P       p109    String Tactic_cache  P       p109    String Itt_comment
335  O       o109    parent p109  O       o109    parent p109
336  T       t110    o109  T       t110    o109
337  B       b110    t110  B       b110    t110
338  T       t111    o b110 b4  T       t111    o b110 b4
339  B       b111    t111  B       b111    t111
340  P       p111    String Typeinf  P       p111    String Base_theory
341  O       o111    parent p111  O       o111    parent p111
342  T       t112    o111  T       t112    o111
343  B       b112    t112  B       b112    t112
344  T       t113    o b112 b4  T       t113    o b112 b4
345  B       b113    t113  B       b113    t113
346  P       p113    String Ocaml_df  P       p113    String Base_meta
347  O       o113    parent p113  O       o113    parent p113
348  T       t114    o113  T       t114    o113
349  B       b114    t114  B       b114    t114
350  T       t115    o b114 b4  T       t115    o b114 b4
351  B       b115    t115  B       b115    t115
352  P       p115    String Ocaml_str_df  P       p115    String Base_cache
353  O       o115    parent p115  O       o115    parent p115
354  T       t116    o115  T       t116    o115
355  B       b116    t116  B       b116    t116
356  T       t117    o b116 b4  T       t117    o b116 b4
357  B       b117    t117  B       b117    t117
358  P       p117    String Ocaml_sig_df  P       p117    String Tactic_cache
359  O       o117    parent p117  O       o117    parent p117
360  T       t118    o117  T       t118    o117
361  B       b118    t118  B       b118    t118
362  T       t119    o b118 b4  T       t119    o b118 b4
363  B       b119    t119  B       b119    t119
364  P       p119    String Ocaml_me_df  P       p119    String Typeinf
365  O       o119    parent p119  O       o119    parent p119
366  T       t120    o119  T       t120    o119
367  B       b120    t120  B       b120    t120
368  T       t121    o b120 b4  T       t121    o b120 b4
369  B       b121    t121  B       b121    t121
370  P       p121    String Ocaml_mt_df  P       p121    String Ocaml_df
371  O       o121    parent p121  O       o121    parent p121
372  T       t122    o121  T       t122    o121
373  B       b122    t122  B       b122    t122
374  T       t123    o b122 b4  T       t123    o b122 b4
375  B       b123    t123  B       b123    t123
376  P       p123    String Ocaml_type_df  P       p123    String Ocaml_str_df
377  O       o123    parent p123  O       o123    parent p123
378  T       t124    o123  T       t124    o123
379  B       b124    t124  B       b124    t124
380  T       t125    o b124 b4  T       t125    o b124 b4
381  B       b125    t125  B       b125    t125
382  P       p125    String Ocaml_patt_df  P       p125    String Ocaml_sig_df
383  O       o125    parent p125  O       o125    parent p125
384  T       t126    o125  T       t126    o125
385  B       b126    t126  B       b126    t126
386  T       t127    o b126 b4  T       t127    o b126 b4
387  B       b127    t127  B       b127    t127
388  P       p127    String Ocaml_expr_df  P       p127    String Ocaml_me_df
389  O       o127    parent p127  O       o127    parent p127
390  T       t128    o127  T       t128    o127
391  B       b128    t128  B       b128    t128
392  T       t129    o b128 b4  T       t129    o b128 b4
393  B       b129    t129  B       b129    t129
394  P       p129    String Ocaml_base_df  P       p129    String Ocaml_mt_df
395  O       o129    parent p129  O       o129    parent p129
396  T       t130    o129  T       t130    o129
397  B       b130    t130  B       b130    t130
398  T       t131    o b130 b4  T       t131    o b130 b4
399  B       b131    t131  B       b131    t131
400  P       p131    String Ocaml  P       p131    String Ocaml_type_df
401  O       o131    parent p131  O       o131    parent p131
402  T       t132    o131  T       t132    o131
403  B       b132    t132  B       b132    t132
404  T       t133    o b132 b4  T       t133    o b132 b4
405  B       b133    t133  B       b133    t133
406  P       p133    String Base_rewrite  P       p133    String Ocaml_patt_df
407  O       o133    parent p133  O       o133    parent p133
408  T       t134    o133  T       t134    o133
409  B       b134    t134  B       b134    t134
410  T       t135    o b134 b4  T       t135    o b134 b4
411  B       b135    t135  B       b135    t135
412  P       p135    String Base_dtactic  P       p135    String Ocaml_expr_df
413  O       o135    parent p135  O       o135    parent p135
414  T       t136    o135  T       t136    o135
415  B       b136    t136  B       b136    t136
416  T       t137    o b136 b4  T       t137    o b136 b4
417  B       b137    t137  B       b137    t137
418  P       p137    String Base_auto_tactic  P       p137    String Ocaml_base_df
419  O       o137    parent p137  O       o137    parent p137
420  T       t138    o137  T       t138    o137
421  B       b138    t138  B       b138    t138
422  T       t139    o b138 b4  T       t139    o b138 b4
423  B       b139    t139  B       b139    t139
424  P       p139    String Base_trivial  P       p139    String Ocaml
425  O       o139    parent p139  O       o139    parent p139
426  T       t140    o139  T       t140    o139
427  B       b140    t140  B       b140    t140
428  T       t141    o b140 b4  T       t141    o b140 b4
429  B       b141    t141  B       b141    t141
430  P       p141    String Top_conversionals  P       p141    String Base_rewrite
431  O       o141    parent p141  O       o141    parent p141
432  T       t142    o141  T       t142    o141
433  B       b142    t142  B       b142    t142
434  T       t143    o b142 b4  T       t143    o b142 b4
435  B       b143    t143  B       b143    t143
436  P       p143    String Top_tacticals  P       p143    String Base_dtactic
437  O       o143    parent p143  O       o143    parent p143
438  T       t144    o143  T       t144    o143
439  B       b144    t144  B       b144    t144
440  T       t145    o b144 b4  T       t145    o b144 b4
441  B       b145    t145  B       b145    t145
442  P       p145    String Var  P       p145    String Base_auto_tactic
443  O       o145    parent p145  O       o145    parent p145
444  T       t146    o145  T       t146    o145
445  B       b146    t146  B       b146    t146
446  T       t147    o b146 b4  T       t147    o b146 b4
447  B       b147    t147  B       b147    t147
448  P       p147    String Mptop  P       p147    String Base_trivial
449  O       o147    parent p147  O       o147    parent p147
450  T       t148    o147  T       t148    o147
451  B       b148    t148  B       b148    t148
452  T       t149    o b148 b4  T       t149    o b148 b4
453  B       b149    t149  B       b149    t149
454  P       p149    String Summary  P       p149    String Top_conversionals
455  O       o149    parent p149  O       o149    parent p149
456  T       t150    o149  T       t150    o149
457  B       b150    t150  B       b150    t150
458  T       t151    o b150 b4  T       t151    o b150 b4
459  B       b151    t151  B       b151    t151
460  P       p151    String Comment  P       p151    String Top_tacticals
461  O       o151    parent p151  O       o151    parent p151
462  T       t152    o151  T       t152    o151
463  B       b152    t152  B       b152    t152
464  T       t153    o b152 b4  T       t153    o b152 b4
465  B       b153    t153  B       b153    t153
466  P       p153    String Base_dform  P       p153    String Var
467  O       o153    parent p153  O       o153    parent p153
468  T       t154    o153  T       t154    o153
469  B       b154    t154  B       b154    t154
470  T       t155    o b154 b4  T       t155    o b154 b4
471  B       b155    t155  B       b155    t155
472  P       p155    String Nuprl_font  P       p155    String Mptop
473  O       o155    parent p155  O       o155    parent p155
474  T       t156    o155  T       t156    o155
475  B       b156    t156  B       b156    t156
476  T       t157    o b156 b4  T       t157    o b156 b4
477  B       b157    t157  B       b157    t157
478  P       p157    String Perv  P       p157    String Summary
479  O       o157    parent p157  O       o157    parent p157
480  T       t158    o157  T       t158    o157
481  B       b158    t158  B       b158    t158
482  T       t159    o b158 b4  T       t159    o b158 b4
483  B       b159    t159  B       b159    t159
484  T       t160    o b159 b4  P       p159    String Comment
485    O       o159    parent p159
486    T       t160    o159
487  B       b160    t160  B       b160    t160
488  T       t161    o b157 b160  T       t161    o b160 b4
489  B       b161    t161  B       b161    t161
490  T       t162    o b155 b161  P       p161    String Base_dform
491    O       o161    parent p161
492    T       t162    o161
493  B       b162    t162  B       b162    t162
494  T       t163    o b153 b162  T       t163    o b162 b4
495  B       b163    t163  B       b163    t163
496  T       t164    o b151 b163  P       p163    String Nuprl_font
497    O       o163    parent p163
498    T       t164    o163
499  B       b164    t164  B       b164    t164
500  T       t165    o b149 b164  T       t165    o b164 b4
501  B       b165    t165  B       b165    t165
502  T       t166    o b147 b165  P       p165    String Perv
503    O       o165    parent p165
504    T       t166    o165
505  B       b166    t166  B       b166    t166
506  T       t167    o b145 b166  T       t167    o b166 b4
507  B       b167    t167  B       b167    t167
508  T       t168    o b143 b167  T       t168    o b167 b4
509  B       b168    t168  B       b168    t168
510  T       t169    o b141 b168  T       t169    o b165 b168
511  B       b169    t169  B       b169    t169
512  T       t170    o b139 b169  T       t170    o b163 b169
513  B       b170    t170  B       b170    t170
514  T       t171    o b137 b170  T       t171    o b161 b170
515  B       b171    t171  B       b171    t171
516  T       t172    o b135 b171  T       t172    o b159 b171
517  B       b172    t172  B       b172    t172
518  T       t173    o b133 b172  T       t173    o b157 b172
519  B       b173    t173  B       b173    t173
520  T       t174    o b131 b173  T       t174    o b155 b173
521  B       b174    t174  B       b174    t174
522  T       t175    o b129 b174  T       t175    o b153 b174
523  B       b175    t175  B       b175    t175
524  T       t176    o b127 b175  T       t176    o b151 b175
525  B       b176    t176  B       b176    t176
526  T       t177    o b125 b176  T       t177    o b149 b176
527  B       b177    t177  B       b177    t177
528  T       t178    o b123 b177  T       t178    o b147 b177
529  B       b178    t178  B       b178    t178
530  T       t179    o b121 b178  T       t179    o b145 b178
531  B       b179    t179  B       b179    t179
532  T       t180    o b119 b179  T       t180    o b143 b179
533  B       b180    t180  B       b180    t180
534  T       t181    o b117 b180  T       t181    o b141 b180
535  B       b181    t181  B       b181    t181
536  T       t182    o b115 b181  T       t182    o b139 b181
537  B       b182    t182  B       b182    t182
538  T       t183    o b113 b182  T       t183    o b137 b182
539  B       b183    t183  B       b183    t183
540  T       t184    o b111 b183  T       t184    o b135 b183
541  B       b184    t184  B       b184    t184
542  T       t185    o b109 b184  T       t185    o b133 b184
543  B       b185    t185  B       b185    t185
544  T       t186    o b107 b185  T       t186    o b131 b185
545  B       b186    t186  B       b186    t186
546  T       t187    o b105 b186  T       t187    o b129 b186
547  B       b187    t187  B       b187    t187
548  T       t188    o b103 b187  T       t188    o b127 b187
549  B       b188    t188  B       b188    t188
550  T       t189    o b101 b188  T       t189    o b125 b188
551  B       b189    t189  B       b189    t189
552  T       t190    o b99 b189  T       t190    o b123 b189
553  B       b190    t190  B       b190    t190
554  NSummary!resource       resource        resource Summary  T       t191    o b121 b190
555  P       p237    String auto  B       b191    t191
556  O       o237    resource p237  T       t192    o b119 b191
557  NOcaml  Ocaml   Ocaml NIL  B       b192    t192
558  NOcaml!type_lid type_lid        type_lid Ocaml  T       t193    o b117 b192
559  P       p238    Number 2332  B       b193    t193
560  P       p239    Number 2341  T       t194    o b115 b193
561  O       o239    type_lid p238 p239  B       b194    t194
562  P       p240    String auto_info  T       t195    o b113 b194
563  O       o240    type_lid p240  B       b195    t195
564  T       t240    o240  T       t196    o b111 b195
565    B       b196    t196
566    T       t197    o b109 b196
567    B       b197    t197
568    T       t198    o b107 b197
569    B       b198    t198
570    T       t199    o b105 b198
571    B       b199    t199
572    T       t200    o b103 b199
573    B       b200    t200
574    T       t201    o b101 b200
575    B       b201    t201
576    T       t202    o b99 b201
577    B       b202    t202
578    T       t203    o b97 b202
579    B       b203    t203
580    T       t204    o b95 b203
581    B       b204    t204
582    T       t205    o b93 b204
583    B       b205    t205
584    T       t206    o b91 b205
585    B       b206    t206
586    T       t207    o b89 b206
587    B       b207    t207
588    T       t208    o b87 b207
589    B       b208    t208
590    T       t209    o b85 b208
591    B       b209    t209
592    T       t210    o b83 b209
593    B       b210    t210
594    T       t211    o b81 b210
595    B       b211    t211
596    T       t212    o b79 b211
597    B       b212    t212
598    T       t213    o b77 b212
599    B       b213    t213
600    T       t214    o b75 b213
601    B       b214    t214
602    T       t215    o b73 b214
603    B       b215    t215
604    T       t216    o b71 b215
605    B       b216    t216
606    T       t217    o b69 b216
607    B       b217    t217
608    T       t218    o b67 b217
609    B       b218    t218
610    T       t219    o b65 b218
611    B       b219    t219
612    T       t220    o b63 b219
613    B       b220    t220
614    T       t221    o b61 b220
615    B       b221    t221
616    T       t222    o b59 b221
617    B       b222    t222
618    T       t223    o b57 b222
619    B       b223    t223
620    T       t224    o b55 b223
621    B       b224    t224
622    T       t225    o b53 b224
623    B       b225    t225
624    T       t226    o b51 b225
625    B       b226    t226
626    T       t227    o b49 b226
627    B       b227    t227
628    T       t228    o b47 b227
629    B       b228    t228
630    T       t229    o b45 b228
631    B       b229    t229
632    T       t230    o b43 b229
633    B       b230    t230
634    T       t231    o b41 b230
635    B       b231    t231
636    T       t232    o b39 b231
637    B       b232    t232
638    T       t233    o b37 b232
639    B       b233    t233
640    T       t234    o b35 b233
641    B       b234    t234
642    T       t235    o b33 b234
643    B       b235    t235
644    T       t236    o b31 b235
645    B       b236    t236
646    T       t237    o b29 b236
647    B       b237    t237
648    T       t238    o b27 b237
649    B       b238    t238
650    T       t239    o b25 b238
651    B       b239    t239
652    T       t240    o b23 b239
653  B       b240    t240  B       b240    t240
654  T       t241    o239 b240  T       t241    o b21 b240
655  B       b241    t241  B       b241    t241
656  NOcaml!type_prod        type_prod       type_prod Ocaml  T       t242    o b19 b241
657  P       p241    Number 2343  B       b242    t242
658  P       p242    Number 2367  T       t243    o b17 b242
659  O       o242    type_prod p241 p242  B       b243    t243
660  P       p243    Number 2349  T       t244    o b15 b243
 O       o243    type_lid p241 p243  
 P       p244    String tactic  
 O       o244    type_lid p244  
 T       t244    o244  
661  B       b244    t244  B       b244    t244
662  T       t245    o243 b244  T       t245    o b13 b244
663  B       b245    t245  B       b245    t245
664  P       p245    Number 2352  T       t246    o b11 b245
 P       p246    Number 2358  
 O       o246    type_lid p245 p246  
 T       t246    o246 b244  
665  B       b246    t246  B       b246    t246
666  P       p247    Number 2361  T       t247    o b9 b246
 O       o247    type_lid p247 p242  
 T       t247    o247 b244  
667  B       b247    t247  B       b247    t247
668  T       t248    o b247 b4  T       t248    o b7 b247
669  B       b248    t248  B       b248    t248
670  T       t249    o b246 b248  T       t249    o b5 b248
671  B       b249    t249  B       b249    t249
672  T       t250    o b245 b249  NSummary!resource       resource        resource Summary
673  B       b250    t250  P       p249    String auto
674  T       t251    o242 b250  O       o249    resource p249
675  B       b251    t251  NOcaml  Ocaml   Ocaml NIL
676  T       t252    o237 b241 b251  NOcaml!type_lid type_lid        type_lid Ocaml
677    P       p250    Number 2332
678    P       p251    Number 2341
679    O       o251    type_lid p250 p251
680    P       p252    String auto_info
681    O       o252    type_lid p252
682    T       t252    o252
683  B       b252    t252  B       b252    t252
684  P       p252    String cache  T       t253    o251 b252
685  O       o252    resource p252  B       b253    t253
686  P       p253    Number 1424  NOcaml!type_prod        type_prod       type_prod Ocaml
687  P       p254    Number 1434  P       p253    Number 2343
688  O       o254    type_lid p253 p254  P       p254    Number 2367
689  P       p255    String cache_rule  O       o254    type_prod p253 p254
690  O       o255    type_lid p255  P       p255    Number 2349
691  T       t255    o255  O       o255    type_lid p253 p255
692  B       b255    t255  P       p256    String tactic
693  T       t256    o254 b255  O       o256    type_lid p256
694    T       t256    o256
695  B       b256    t256  B       b256    t256
696  P       p256    Number 1436  T       t257    o255 b256
697  P       p257    Number 1441  B       b257    t257
698  O       o257    type_lid p256 p257  P       p257    Number 2352
699  O       o258    type_lid p252  P       p258    Number 2358
700  T       t258    o258  O       o258    type_lid p257 p258
701    T       t258    o258 b256
702  B       b258    t258  B       b258    t258
703  T       t259    o257 b258  P       p259    Number 2361
704    O       o259    type_lid p259 p254
705    T       t259    o259 b256
706  B       b259    t259  B       b259    t259
707  T       t260    o252 b256 b259  T       t260    o b259 b4
708  B       b260    t260  B       b260    t260
709  P       p260    String elim  T       t261    o b258 b260
710  O       o260    resource p260  B       b261    t261
711  P       p261    Number 1761  T       t262    o b257 b261
712  P       p262    Number 1783  B       b262    t262
713  O       o262    type_prod p261 p262  T       t263    o254 b262
714  P       p263    Number 1765  B       b263    t263
715  O       o263    type_lid p261 p263  T       t264    o249 b253 b263
 P       p264    String term  
 O       o264    type_lid p264  
 T       t264    o264  
716  B       b264    t264  B       b264    t264
717  T       t265    o263 b264  P       p264    String cache
718  B       b265    t265  O       o264    resource p264
719  NOcaml!type_fun type_fun        type_fun Ocaml  P       p265    Number 1424
720  P       p265    Number 1769  P       p266    Number 1434
721  P       p266    Number 1782  O       o266    type_lid p265 p266
722  O       o266    type_fun p265 p266  P       p267    String cache_rule
723  P       p267    Number 1772  O       o267    type_lid p267
724  O       o267    type_lid p265 p267  T       t267    o267
725  P       p268    String int  B       b267    t267
726  O       o268    type_lid p268  T       t268    o266 b267
 T       t268    o268  
727  B       b268    t268  B       b268    t268
728  T       t269    o267 b268  P       p268    Number 1436
729  B       b269    t269  P       p269    Number 1441
730  P       p269    Number 1776  O       o269    type_lid p268 p269
731  O       o269    type_lid p269 p266  O       o270    type_lid p264
732  T       t270    o269 b244  T       t270    o270
733  B       b270    t270  B       b270    t270
734  T       t271    o266 b269 b270  T       t271    o269 b270
735  B       b271    t271  B       b271    t271
736  T       t272    o b271 b4  T       t272    o264 b268 b271
737  B       b272    t272  B       b272    t272
738  T       t273    o b265 b272  P       p272    String elim
739  B       b273    t273  O       o272    resource p272
740  T       t274    o262 b273  P       p273    Number 1761
741  B       b274    t274  P       p274    Number 1783
742  P       p274    Number 1785  O       o274    type_prod p273 p274
743  P       p275    Number 1798  P       p275    Number 1765
744  O       o275    type_fun p274 p275  O       o275    type_lid p273 p275
745  P       p276    Number 1788  P       p276    String term
746  O       o276    type_lid p274 p276  O       o276    type_lid p276
747  T       t276    o276 b268  T       t276    o276
748  B       b276    t276  B       b276    t276
749  P       p277    Number 1792  T       t277    o275 b276
 O       o277    type_lid p277 p275  
 T       t277    o277 b244  
750  B       b277    t277  B       b277    t277
751  T       t278    o275 b276 b277  NOcaml!type_fun type_fun        type_fun Ocaml
752  B       b278    t278  P       p277    Number 1769
753  T       t279    o260 b274 b278  P       p278    Number 1782
754  B       b279    t279  O       o278    type_fun p277 p278
755  P       p279    String eqcd  P       p279    Number 1772
756  O       o279    resource p279  O       o279    type_lid p277 p279
757  P       p280    Number 6168  P       p280    String int
758  P       p281    Number 6181  O       o280    type_lid p280
759  O       o281    type_prod p280 p281  T       t280    o280
760  P       p282    Number 6172  B       b280    t280
761  O       o282    type_lid p280 p282  T       t281    o279 b280
762  T       t282    o282 b264  B       b281    t281
763    P       p281    Number 1776
764    O       o281    type_lid p281 p278
765    T       t282    o281 b256
766  B       b282    t282  B       b282    t282
767  P       p283    Number 6175  T       t283    o278 b281 b282
 O       o283    type_lid p283 p281  
 T       t283    o283 b244  
768  B       b283    t283  B       b283    t283
769  T       t284    o b283 b4  T       t284    o b283 b4
770  B       b284    t284  B       b284    t284
771  T       t285    o b282 b284  T       t285    o b277 b284
772  B       b285    t285  B       b285    t285
773  T       t286    o281 b285  T       t286    o274 b285
774  B       b286    t286  B       b286    t286
775  P       p286    Number 6183  P       p286    Number 1785
776  P       p287    Number 6189  P       p287    Number 1798
777  O       o287    type_lid p286 p287  O       o287    type_fun p286 p287
778  T       t287    o287 b244  P       p288    Number 1788
779  B       b287    t287  O       o288    type_lid p286 p288
780  T       t288    o279 b286 b287  T       t288    o288 b280
781  B       b288    t288  B       b288    t288
782  P       p288    String intro  P       p289    Number 1792
783  O       o288    resource p288  O       o289    type_lid p289 p287
784  P       p289    Number 1815  T       t289    o289 b256
785  P       p290    Number 1852  B       b289    t289
786  O       o290    type_prod p289 p290  T       t290    o287 b288 b289
787  P       p291    Number 1819  B       b290    t290
788  O       o291    type_lid p289 p291  T       t291    o272 b286 b290
 T       t291    o291 b264  
789  B       b291    t291  B       b291    t291
790  P       p292    Number 1823  P       p291    String eqcd
791  P       p293    Number 1851  O       o291    resource p291
792    P       p292    Number 6168
793    P       p293    Number 6181
794  O       o293    type_prod p292 p293  O       o293    type_prod p292 p293
795  P       p294    Number 1829  P       p294    Number 6172
796  O       o294    type_lid p292 p294  O       o294    type_lid p292 p294
797  P       p295    String string  T       t294    o294 b276
798  O       o295    type_lid p295  B       b294    t294
799  T       t295    o295  P       p295    Number 6175
800    O       o295    type_lid p295 p293
801    T       t295    o295 b256
802  B       b295    t295  B       b295    t295
803  T       t296    o294 b295  T       t296    o b295 b4
804  B       b296    t296  B       b296    t296
805  NOcaml!type_apply       type_apply      type_apply Ocaml  T       t297    o b294 b296
806  P       p296    Number 1832  B       b297    t297
807  P       p297    Number 1842  T       t298    o293 b297
808  O       o297    type_apply p296 p297  B       b298    t298
809  P       p298    Number 1836  P       p298    Number 6183
810  O       o298    type_lid p298 p297  P       p299    Number 6189
811  P       p299    String option  O       o299    type_lid p298 p299
812  O       o299    type_lid p299  T       t299    o299 b256
 T       t299    o299  
813  B       b299    t299  B       b299    t299
814  T       t300    o298 b299  T       t300    o291 b298 b299
815  B       b300    t300  B       b300    t300
816  P       p300    Number 1835  P       p300    String intro
817  O       o300    type_lid p296 p300  O       o300    resource p300
818  T       t301    o300 b268  P       p301    Number 1815
819  B       b301    t301  P       p302    Number 1852
820  T       t302    o297 b300 b301  O       o302    type_prod p301 p302
821  B       b302    t302  P       p303    Number 1819
822  P       p302    Number 1845  O       o303    type_lid p301 p303
823  O       o302    type_lid p302 p293  T       t303    o303 b276
 T       t303    o302 b244  
824  B       b303    t303  B       b303    t303
825  T       t304    o b303 b4  P       p304    Number 1823
826  B       b304    t304  P       p305    Number 1851
827  T       t305    o b302 b304  O       o305    type_prod p304 p305
828  B       b305    t305  P       p306    Number 1829
829  T       t306    o b296 b305  O       o306    type_lid p304 p306
830  B       b306    t306  P       p307    String string
831  T       t307    o293 b306  O       o307    type_lid p307
832    T       t307    o307
833  B       b307    t307  B       b307    t307
834  T       t308    o b307 b4  T       t308    o306 b307
835  B       b308    t308  B       b308    t308
836  T       t309    o b291 b308  NOcaml!type_apply       type_apply      type_apply Ocaml
837  B       b309    t309  P       p308    Number 1832
838  T       t310    o290 b309  P       p309    Number 1842
839  B       b310    t310  O       o309    type_apply p308 p309
840  P       p310    Number 1854  P       p310    Number 1836
841  P       p311    Number 1860  O       o310    type_lid p310 p309
842  O       o311    type_lid p310 p311  P       p311    String option
843  T       t311    o311 b244  O       o311    type_lid p311
844    T       t311    o311
845  B       b311    t311  B       b311    t311
846  T       t312    o288 b310 b311  T       t312    o310 b311
847  B       b312    t312  B       b312    t312
848  P       p312    String reduce  P       p312    Number 1835
849  O       o312    resource p312  O       o312    type_lid p308 p312
850  P       p313    Number 2920  T       t313    o312 b280
851  P       p314    Number 2931  B       b313    t313
852  O       o314    type_prod p313 p314  T       t314    o309 b312 b313
853  P       p315    Number 2924  B       b314    t314
854  O       o315    type_lid p313 p315  P       p314    Number 1845
855  T       t315    o315 b264  O       o314    type_lid p314 p305
856    T       t315    o314 b256
857  B       b315    t315  B       b315    t315
858  P       p316    Number 2927  T       t316    o b315 b4
859  O       o316    type_lid p316 p314  B       b316    t316
860  P       p317    String conv  T       t317    o b314 b316
 O       o317    type_lid p317  
 T       t317    o317  
861  B       b317    t317  B       b317    t317
862  T       t318    o316 b317  T       t318    o b308 b317
863  B       b318    t318  B       b318    t318
864  T       t319    o b318 b4  T       t319    o305 b318
865  B       b319    t319  B       b319    t319
866  T       t320    o b315 b319  T       t320    o b319 b4
867  B       b320    t320  B       b320    t320
868  T       t321    o314 b320  T       t321    o b303 b320
869  B       b321    t321  B       b321    t321
870  P       p321    Number 2933  T       t322    o302 b321
 P       p322    Number 2937  
 O       o322    type_lid p321 p322  
 T       t322    o322 b317  
871  B       b322    t322  B       b322    t322
872  T       t323    o312 b321 b322  P       p322    Number 1854
873    P       p323    Number 1860
874    O       o323    type_lid p322 p323
875    T       t323    o323 b256
876  B       b323    t323  B       b323    t323
877  P       p323    String squash  T       t324    o300 b322 b323
878  O       o323    resource p323  B       b324    t324
879  P       p324    Number 4017  P       p324    String reduce
880  P       p325    Number 4028  O       o324    resource p324
881  O       o325    type_lid p324 p325  P       p325    Number 2920
882  P       p326    String squash_info  P       p326    Number 2931
883  O       o326    type_lid p326  O       o326    type_prod p325 p326
884  T       t326    o326  P       p327    Number 2924
885  B       b326    t326  O       o327    type_lid p325 p327
886  T       t327    o325 b326  T       t327    o327 b276
887  B       b327    t327  B       b327    t327
888  P       p327    Number 4030  P       p328    Number 2927
889  P       p328    Number 4043  O       o328    type_lid p328 p326
890  O       o328    type_fun p327 p328  P       p329    String conv
891  P       p329    Number 4033  O       o329    type_lid p329
892  O       o329    type_lid p327 p329  T       t329    o329
 T       t329    o329 b268  
893  B       b329    t329  B       b329    t329
894  P       p330    Number 4037  T       t330    o328 b329
 O       o330    type_lid p330 p328  
 T       t330    o330 b244  
895  B       b330    t330  B       b330    t330
896  T       t331    o328 b329 b330  T       t331    o b330 b4
897  B       b331    t331  B       b331    t331
898  T       t332    o323 b327 b331  T       t332    o b327 b331
899  B       b332    t332  B       b332    t332
900  P       p332    String sub  T       t333    o326 b332
901  O       o332    resource p332  B       b333    t333
902  P       p333    Number 4882  P       p333    Number 2933
903  P       p334    Number 4899  P       p334    Number 2937
904  O       o334    type_lid p333 p334  O       o334    type_lid p333 p334
905  P       p335    String sub_resource_info  T       t334    o334 b329
906  O       o335    type_lid p335  B       b334    t334
907  T       t335    o335  T       t335    o324 b333 b334
908  B       b335    t335  B       b335    t335
909  T       t336    o334 b335  P       p335    String squash
910  B       b336    t336  O       o335    resource p335
911  P       p336    Number 4901  P       p336    Number 4017
912  P       p337    Number 4907  P       p337    Number 4028
913  O       o337    type_lid p336 p337  O       o337    type_lid p336 p337
914  T       t337    o337 b244  P       p338    String squash_info
915  B       b337    t337  O       o338    type_lid p338
916  T       t338    o332 b336 b337  T       t338    o338
917  B       b338    t338  B       b338    t338
918  P       p338    String toploop  T       t339    o337 b338
919  O       o338    resource p338  B       b339    t339
920  P       p339    Number 2445  P       p339    Number 4030
921  P       p340    Number 2467  P       p340    Number 4043
922  O       o340    type_prod p339 p340  O       o340    type_fun p339 p340
923  P       p341    Number 2451  P       p341    Number 4033
924  O       o341    type_lid p339 p341  O       o341    type_lid p339 p341
925  T       t341    o341 b295  T       t341    o341 b280
926  B       b341    t341  B       b341    t341
927  P       p342    Number 2454  P       p342    Number 4037
928  P       p343    Number 2460  O       o342    type_lid p342 p340
929  O       o343    type_lid p342 p343  T       t342    o342 b256
930  T       t343    o343 b295  B       b342    t342
931    T       t343    o340 b341 b342
932  B       b343    t343  B       b343    t343
933  P       p344    Number 2463  T       t344    o335 b339 b343
934  O       o344    type_lid p344 p340  B       b344    t344
935  P       p345    String expr  P       p344    String sub
936  O       o345    type_lid p345  O       o344    resource p344
937  T       t345    o345  P       p345    Number 4882
938  B       b345    t345  P       p346    Number 4899
939  T       t346    o344 b345  O       o346    type_lid p345 p346
940  B       b346    t346  P       p347    String sub_resource_info
941  T       t347    o b346 b4  O       o347    type_lid p347
942    T       t347    o347
943  B       b347    t347  B       b347    t347
944  T       t348    o b343 b347  T       t348    o346 b347
945  B       b348    t348  B       b348    t348
946  T       t349    o b341 b348  P       p348    Number 4901
947    P       p349    Number 4907
948    O       o349    type_lid p348 p349
949    T       t349    o349 b256
950  B       b349    t349  B       b349    t349
951  T       t350    o340 b349  T       t350    o344 b348 b349
952  B       b350    t350  B       b350    t350
953  P       p350    Number 2469  P       p350    String toploop
954  P       p351    Number 2478  O       o350    resource p350
955  O       o351    type_lid p350 p351  P       p351    Number 2445
956  P       p352    String top_table  P       p352    Number 2467
957  O       o352    type_lid p352  O       o352    type_prod p351 p352
958  T       t352    o352  P       p353    Number 2451
959  B       b352    t352  O       o353    type_lid p351 p353
960  T       t353    o351 b352  T       t353    o353 b307
961  B       b353    t353  B       b353    t353
962  T       t354    o338 b350 b353  P       p354    Number 2454
963  B       b354    t354  P       p355    Number 2460
964  P       p354    String typeinf  O       o355    type_lid p354 p355
965  O       o354    resource p354  T       t355    o355 b307
966  P       p355    Number 2151  B       b355    t355
967  P       p356    Number 2172  P       p356    Number 2463
968  O       o356    type_lid p355 p356  O       o356    type_lid p356 p352
969  P       p357    String typeinf_resource_info  P       p357    String expr
970  O       o357    type_lid p357  O       o357    type_lid p357
971  T       t357    o357  T       t357    o357
972  B       b357    t357  B       b357    t357
973  T       t358    o356 b357  T       t358    o356 b357
974  B       b358    t358  B       b358    t358
975  P       p358    Number 2174  T       t359    o b358 b4
976  P       p359    Number 2186  B       b359    t359
977  O       o359    type_lid p358 p359  T       t360    o b355 b359
 P       p360    String typeinf_func  
 O       o360    type_lid p360  
 T       t360    o360  
978  B       b360    t360  B       b360    t360
979  T       t361    o359 b360  T       t361    o b353 b360
980  B       b361    t361  B       b361    t361
981  T       t362    o354 b358 b361  T       t362    o352 b361
982  B       b362    t362  B       b362    t362
983  P       p362    String typeinf_subst  P       p362    Number 2469
984  O       o362    resource p362  P       p363    Number 2478
985  P       p363    Number 1825  O       o363    type_lid p362 p363
986  P       p364    Number 1843  P       p364    String top_table
987  O       o364    type_lid p363 p364  O       o364    type_lid p364
988  P       p365    String typeinf_subst_info  T       t364    o364
989  O       o365    type_lid p365  B       b364    t364
990  T       t365    o365  T       t365    o363 b364
991  B       b365    t365  B       b365    t365
992  T       t366    o364 b365  T       t366    o350 b362 b365
993  B       b366    t366  B       b366    t366
994  P       p366    Number 1862  P       p366    String typeinf
995  O       o366    type_lid p302 p366  O       o366    resource p366
996  P       p367    String typeinf_subst_fun  P       p367    Number 2151
997  O       o367    type_lid p367  P       p368    Number 2172
998  T       t367    o367  O       o368    type_lid p367 p368
999  B       b367    t367  P       p369    String typeinf_resource_info
1000  T       t368    o366 b367  O       o369    type_lid p369
1001  B       b368    t368  T       t369    o369
 T       t369    o362 b366 b368  
1002  B       b369    t369  B       b369    t369
1003  T       t370    o b369 b4  T       t370    o368 b369
1004  B       b370    t370  B       b370    t370
1005  T       t371    o b362 b370  P       p370    Number 2174
1006  B       b371    t371  P       p371    Number 2186
1007  T       t372    o b354 b371  O       o371    type_lid p370 p371
1008    P       p372    String typeinf_func
1009    O       o372    type_lid p372
1010    T       t372    o372
1011  B       b372    t372  B       b372    t372
1012  T       t373    o b338 b372  T       t373    o371 b372
1013  B       b373    t373  B       b373    t373
1014  T       t374    o b332 b373  T       t374    o366 b370 b373
1015  B       b374    t374  B       b374    t374
1016  T       t375    o b323 b374  P       p374    String typeinf_subst
1017  B       b375    t375  O       o374    resource p374
1018  T       t376    o b312 b375  P       p375    Number 1825
1019  B       b376    t376  P       p376    Number 1843
1020  T       t377    o b288 b376  O       o376    type_lid p375 p376
1021    P       p377    String typeinf_subst_info
1022    O       o377    type_lid p377
1023    T       t377    o377
1024  B       b377    t377  B       b377    t377
1025  T       t378    o b279 b377  T       t378    o376 b377
1026  B       b378    t378  B       b378    t378
1027  T       t379    o b260 b378  P       p378    Number 1862
1028    O       o378    type_lid p314 p378
1029    P       p379    String typeinf_subst_fun
1030    O       o379    type_lid p379
1031    T       t379    o379
1032  B       b379    t379  B       b379    t379
1033  T       t380    o b252 b379  T       t380    o378 b379
1034  B       b380    t380  B       b380    t380
1035  P       p382    Number 22  T       t381    o374 b378 b380
1036  P       p384    String Czf_itt_cyclic_subgroup  B       b381    t381
1037  O       o384    parent p384  T       t382    o b381 b4
1038  T       t384    o384  B       b382    t382
1039    T       t383    o b374 b382
1040    B       b383    t383
1041    T       t384    o b366 b383
1042  B       b384    t384  B       b384    t384
1043  T       t385    o b384 b4  T       t385    o b350 b384
1044  B       b385    t385  B       b385    t385
1045  P       p385    String Czf_itt_subgroup  T       t386    o b344 b385
 O       o385    parent p385  
 T       t386    o385  
1046  B       b386    t386  B       b386    t386
1047  T       t387    o b386 b4  T       t387    o b335 b386
1048  B       b387    t387  B       b387    t387
1049  P       p4      String Czf_itt_isect  T       t388    o b324 b387
1050  O       o8      parent p4  B       b388    t388
1051  T       t242    o8  T       t389    o b300 b388
1052  B       b242    t242  B       b389    t389
1053  T       t243    o b242 b4  T       t390    o b291 b389
1054  B       b243    t243  B       b390    t390
1055  P       p250    String Czf_itt_union  T       t391    o b272 b390
1056  O       o251    parent p250  B       b391    t391
1057  T       t266    o251  T       t392    o b264 b391
 B       b266    t266  
 T       t267    o b266 b4  
 B       b267    t267  
 P       p272    String Czf_itt_dexists  
 O       o273    parent p272  
 T       t293    o273  
 B       b293    t293  
 T       t294    o b293 b4  
 B       b294    t294  
 T       t392    o2 b387 b4 b380  
1058  B       b392    t392  B       b392    t392
1059  P       p394    Number 101  T       t393    o2 b5 b249 b392
1060  P       p395    String Czf_itt_subset  B       b393    t393
1061  O       o395    parent p395  T       t394    o1 b393
1062  T       t395    o395  B       b394    t394
1063  B       b395    t395  P       p394    Number 22
1064  T       t396    o b395 b4  P       p395    Number 43
1065    O       o395    location p394 p395
1066    P       p396    String Czf_itt_group
1067    O       o396    parent p396
1068    T       t396    o396
1069  B       b396    t396  B       b396    t396
1070  T       t197    o b97 b190  T       t397    o b396 b4
1071  B       b197    t197  B       b397    t397
1072  T       t198    o b95 b197  P       p397    String Czf_itt_and
1073  B       b198    t198  O       o397    parent p397
1074  T       t199    o b93 b198  T       t398    o397
1075  B       b199    t199  B       b398    t398
1076  T       t200    o b91 b199  T       t399    o b398 b4
1077  B       b200    t200  B       b399    t399
1078  T       t201    o b89 b200  P       p399    String Itt_record_label0
1079  B       b201    t201  O       o399    parent p399
1080  T       t202    o b87 b201  T       t400    o399
1081  B       b202    t202  B       b400    t400
1082  T       t203    o b85 b202  T       t401    o b400 b4
 B       b203    t203  
 T       t204    o b83 b203  
 B       b204    t204  
 T       t205    o b81 b204  
 B       b205    t205  
 T       t206    o b79 b205  
 B       b206    t206  
 T       t207    o b77 b206  
 B       b207    t207  
 T       t208    o b75 b207  
 B       b208    t208  
 T       t209    o b73 b208  
 B       b209    t209  
 T       t210    o b71 b209  
 B       b210    t210  
 T       t211    o b69 b210  
 B       b211    t211  
 T       t212    o b67 b211  
 B       b212    t212  
 T       t213    o b65 b212  
 B       b213    t213  
 T       t214    o b63 b213  
 B       b214    t214  
 T       t215    o b61 b214  
 B       b215    t215  
 T       t216    o b59 b215  
 B       b216    t216  
 T       t217    o b57 b216  
 B       b217    t217  
 T       t218    o b55 b217  
 B       b218    t218  
 T       t219    o b53 b218  
 B       b219    t219  
 T       t220    o b51 b219  
 B       b220    t220  
 T       t221    o b49 b220  
 B       b221    t221  
 T       t222    o b47 b221  
 B       b222    t222  
 T       t223    o b45 b222  
 B       b223    t223  
 T       t224    o b43 b223  
 B       b224    t224  
 T       t225    o b41 b224  
 B       b225    t225  
 T       t226    o b39 b225  
 B       b226    t226  
 T       t227    o b37 b226  
 B       b227    t227  
 T       t228    o b35 b227  
 B       b228    t228  
 T       t229    o b33 b228  
 B       b229    t229  
 T       t230    o b31 b229  
 B       b230    t230  
 T       t231    o b29 b230  
 B       b231    t231  
 T       t232    o b27 b231  
 B       b232    t232  
 T       t233    o b25 b232  
 B       b233    t233  
 T       t234    o b23 b233  
 B       b234    t234  
 T       t235    o b21 b234  
 B       b235    t235  
 T       t236    o b19 b235  
 B       b236    t236  
 T       t237    o b17 b236  
 B       b237    t237  
 T       t381    o b15 b237  
 B       b381    t381  
 T       t382    o b11 b381  
 B       b382    t382  
 T       t401    o b294 b382  
1083  B       b401    t401  B       b401    t401
1084  T       t405    o b13 b401  P       p401    String Itt_nat
1085    O       o401    parent p401
1086    T       t402    o401
1087    B       b402    t402
1088    T       t403    o b402 b4
1089    B       b403    t403
1090    T       t404    o b403 b4
1091    B       b404    t404
1092    T       t405    o b401 b404
1093  B       b405    t405  B       b405    t405
1094  T       t411    o b9 b405  T       t406    o b399 b405
1095    B       b406    t406
1096    T       t407    o b397 b406
1097    B       b407    t407
1098    T       t408    o2 b397 b407 b392
1099    B       b408    t408
1100    T       t409    o395 b408
1101    B       b409    t409
1102    P       p409    Number 44
1103    P       p410    Number 75
1104    O       o410    location p409 p410
1105    P       p411    String Czf_itt_cyclic_subgroup
1106    O       o411    parent p411
1107    T       t411    o411
1108  B       b411    t411  B       b411    t411
1109  T       t412    o b396 b411  T       t412    o b411 b4
1110  B       b412    t412  B       b412    t412
1111  T       t418    o b267 b412  P       p412    String Czf_itt_subgroup
1112    O       o412    parent p412
1113    T       t413    o412
1114    B       b413    t413
1115    T       t414    o b413 b4
1116    B       b414    t414
1117    P       p414    String Czf_itt_isect
1118    O       o414    parent p414
1119    T       t415    o414
1120    B       b415    t415
1121    T       t416    o b415 b4
1122    B       b416    t416
1123    T       t417    o b416 b4
1124    B       b417    t417
1125    T       t418    o b414 b417
1126  B       b418    t418  B       b418    t418
1127  T       t419    o b196 b418  T       t419    o b412 b418
1128  B       b419    t419  B       b419    t419
1129  T       t420    o b194 b419  T       t420    o2 b412 b419 b392
1130  B       b420    t420  B       b420    t420
1131  T       t422    o b192 b420  T       t421    o410 b420
1132  B       b422    t422  B       b421    t421
1133  T       t428    o2 b192 b422 b380  P       p421    Number 76
1134  B       b428    t428  P       p422    Number 102
1135  T       t429    o1 b428  O       o422    location p421 p422
1136  B       b429    t429  P       p423    String Czf_itt_abel_group
1137  P       p429    Number 43  O       o423    parent p423
1138  O       o429    location p382 p429  T       t423    o423
1139  T       t430    o b389 b4  B       b423    t423
1140  B       b430    t430  T       t424    o b423 b4
1141  T       t437    o b364 b430  B       b424    t424
1142  B       b437    t437  T       t425    o b424 b4
1143  T       t438    o b7 b437  B       b425    t425
1144    T       t426    o2 b424 b425 b392
1145    B       b426    t426
1146    T       t427    o422 b426
1147    B       b427    t427
1148    P       p427    Number 104
1149    P       p428    Number 115
1150    O       o428    location p427 p428
1151    NSummary!summary_item   summary_item    summary_item Summary
1152    O       o429    summary_item
1153    NOcaml!str_open str_open        str_open Ocaml
1154    O       o430    str_open p427 p428
1155    NOcaml!string   string  string Ocaml
1156    P       p430    String Printf
1157    O       o431    string p430
1158    T       t431    o431
1159    B       b431    t431
1160    T       t432    o b431 b4
1161    B       b432    t432
1162    T       t433    o430 b432
1163    B       b433    t433
1164    T       t434    o429 b433
1165    B       b434    t434
1166    T       t435    o428 b434
1167    B       b435    t435
1168    P       p435    Number 116
1169    P       p436    Number 129
1170    O       o436    location p435 p436
1171    O       o437    str_open p435 p436
1172    P       p437    String Mp_debug
1173    O       o438    string p437
1174    T       t438    o438
1175  B       b438    t438  B       b438    t438
1176  T       t439    o b5 b438  T       t439    o b438 b4
1177  B       b439    t439  B       b439    t439
1178  T       t441    o2 b5 b439 b380  T       t440    o437 b439
1179    B       b440    t440
1180    T       t441    o429 b440
1181  B       b441    t441  B       b441    t441
1182  T       t446    o429 b441  T       t442    o436 b441
1183    B       b442    t442
1184    P       p442    Number 130
1185    P       p443    Number 159
1186    O       o443    location p442 p443
1187    O       o444    str_open p442 p443
1188    P       p444    String Refiner
1189    O       o445    string p444
1190    T       t445    o445
1191    B       b445    t445
1192    P       p445    String TermType
1193    O       o446    string p445
1194    T       t446    o446
1195  B       b446    t446  B       b446    t446
1196  P       p446    Number 44  T       t447    o b446 b4
 P       p447    Number 75  
 O       o447    location p446 p447  
 T       t447    o b243 b4  
1197  B       b447    t447  B       b447    t447
1198  T       t448    o b387 b447  T       t448    o b445 b447
1199  B       b448    t448  B       b448    t448
1200  T       t455    o b385 b448  T       t449    o b445 b448
1201    B       b449    t449
1202    T       t450    o444 b449
1203    B       b450    t450
1204    T       t451    o429 b450
1205    B       b451    t451
1206    T       t452    o443 b451
1207    B       b452    t452
1208    P       p452    Number 160
1209    P       p453    Number 185
1210    O       o453    location p452 p453
1211    O       o454    str_open p452 p453
1212    P       p454    String Term
1213    O       o455    string p454
1214    T       t455    o455
1215  B       b455    t455  B       b455    t455
1216  T       t456    o2 b385 b455 b380  T       t456    o b455 b4
1217  B       b456    t456  B       b456    t456
1218  T       t457    o447 b456  T       t457    o b445 b456
1219  B       b457    t457  B       b457    t457
1220  P       p457    Number 76  T       t458    o b445 b457
1221  P       p458    Number 100  B       b458    t458
1222  O       o458    location p457 p458  T       t459    o454 b458
 T       t459    o458 b392  
1223  B       b459    t459  B       b459    t459
1224  P       p462    Number 123  T       t460    o429 b459
1225  O       o463    location p394 p462  B       b460    t460
1226  T       t344    o2 b396 b4 b380  T       t461    o453 b460
1227  B       b344    t344  B       b461    t461
1228  T       t464    o463 b344  P       p461    Number 186
1229    P       p462    Number 213
1230    O       o462    location p461 p462
1231    O       o463    str_open p461 p462
1232    P       p463    String TermOp
1233    O       o464    string p463
1234    T       t464    o464
1235  B       b464    t464  B       b464    t464
1236  P       p464    Number 124  T       t465    o b464 b4
 P       p465    Number 141  
 O       o465    location p464 p465  
 T       t238    o2 b73 b4 b380  
 B       b238    t238  
 T       t465    o465 b238  
1237  B       b465    t465  B       b465    t465
1238  P       p466    Number 143  T       t466    o b445 b465
1239  P       p467    Number 154  B       b466    t466
1240  O       o467    location p466 p467  T       t467    o b445 b466
1241  NSummary!summary_item   summary_item    summary_item Summary  B       b467    t467
1242  O       o407    summary_item  T       t468    o463 b467
1243  NOcaml!str_open str_open        str_open Ocaml  B       b468    t468
1244  O       o468    str_open p466 p467  T       t469    o429 b468
1245  NOcaml!string   string  string Ocaml  B       b469    t469
1246  P       p408    String Printf  T       t470    o462 b469
1247  O       o409    string p408  B       b470    t470
1248  T       t409    o409  P       p470    Number 214
1249  B       b409    t409  P       p471    Number 243
1250  T       t410    o b409 b4  O       o471    location p470 p471
1251  B       b410    t410  O       o472    str_open p470 p471
1252  T       t473    o468 b410  P       p472    String TermAddr
1253    O       o473    string p472
1254    T       t473    o473
1255  B       b473    t473  B       b473    t473
1256  T       t474    o407 b473  T       t474    o b473 b4
1257  B       b474    t474  B       b474    t474
1258  T       t475    o467 b474  T       t475    o b445 b474
1259  B       b475    t475  B       b475    t475
1260  P       p475    Number 155  T       t476    o b445 b475
1261  P       p476    Number 168  B       b476    t476
1262  O       o476    location p475 p476  T       t477    o472 b476
 O       o477    str_open p475 p476  
 P       p415    String Mp_debug  
 O       o416    string p415  
 T       t416    o416  
 B       b416    t416  
 T       t417    o b416 b4  
 B       b417    t417  
 T       t477    o477 b417  
1263  B       b477    t477  B       b477    t477
1264  T       t482    o407 b477  T       t478    o429 b477
1265    B       b478    t478
1266    T       t479    o471 b478
1267    B       b479    t479
1268    P       p479    Number 244
1269    P       p480    Number 272
1270    O       o480    location p479 p480
1271    O       o481    str_open p479 p480
1272    P       p481    String TermMan
1273    O       o482    string p481
1274    T       t482    o482
1275  B       b482    t482  B       b482    t482
1276  T       t483    o476 b482  T       t483    o b482 b4
1277  B       b483    t483  B       b483    t483
1278  P       p483    Number 169  T       t484    o b445 b483
1279  P       p484    Number 198  B       b484    t484
1280  O       o484    location p483 p484  T       t485    o b445 b484
1281  O       o485    str_open p483 p484  B       b485    t485
1282  P       p422    String Refiner  T       t486    o481 b485
1283  O       o423    string p422  B       b486    t486
1284  T       t423    o423  T       t487    o429 b486
1285  B       b423    t423  B       b487    t487
1286  P       p423    String TermType  T       t488    o480 b487
1287  O       o424    string p423  B       b488    t488
1288  T       t424    o424  P       p488    Number 273
1289  B       b424    t424  P       p489    Number 303
1290  T       t425    o b424 b4  O       o489    location p488 p489
1291  B       b425    t425  O       o490    str_open p488 p489
1292  T       t426    o b423 b425  P       p490    String TermSubst
1293  B       b426    t426  O       o491    string p490
1294  T       t427    o b423 b426  T       t491    o491
 B       b427    t427  
 T       t491    o485 b427  
1295  B       b491    t491  B       b491    t491
1296  T       t492    o407 b491  T       t492    o b491 b4
1297  B       b492    t492  B       b492    t492
1298  T       t493    o484 b492  T       t493    o b445 b492
1299  B       b493    t493  B       b493    t493
1300  P       p493    Number 199  T       t494    o b445 b493
1301  P       p494    Number 224  B       b494    t494
1302  O       o494    location p493 p494  T       t495    o490 b494
 O       o495    str_open p493 p494  
 P       p432    String Term  
 O       o433    string p432  
 T       t433    o433  
 B       b433    t433  
 T       t434    o b433 b4  
 B       b434    t434  
 T       t435    o b423 b434  
 B       b435    t435  
 T       t436    o b423 b435  
 B       b436    t436  
 T       t495    o495 b436  
1303  B       b495    t495  B       b495    t495
1304  T       t498    o407 b495  T       t496    o429 b495
1305  B       b498    t498  B       b496    t496
1306  T       t499    o494 b498  T       t497    o489 b496
1307  B       b499    t499  B       b497    t497
1308  P       p499    Number 225  P       p497    Number 304
1309  P       p500    Number 252  P       p498    Number 331
1310  O       o500    location p499 p500  O       o498    location p497 p498
1311  O       o501    str_open p499 p500  O       o499    str_open p497 p498
1312  P       p441    String TermOp  P       p499    String Refine
1313  O       o442    string p441  O       o500    string p499
1314  T       t442    o442  T       t500    o500
1315  B       b442    t442  B       b500    t500
1316  T       t443    o b442 b4  T       t501    o b500 b4
1317  B       b443    t443  B       b501    t501
1318  T       t444    o b423 b443  T       t502    o b445 b501
1319  B       b444    t444  B       b502    t502
1320  T       t445    o b423 b444  T       t503    o b445 b502
1321  B       b445    t445  B       b503    t503
1322  T       t505    o501 b445  T       t504    o499 b503
1323    B       b504    t504
1324    T       t505    o429 b504
1325  B       b505    t505  B       b505    t505
1326  T       t506    o407 b505  T       t506    o498 b505
1327  B       b506    t506  B       b506    t506
1328  T       t507    o500 b506  P       p506    Number 332
1329  B       b507    t507  P       p507    Number 364
1330  P       p507    Number 253  O       o507    location p506 p507
1331  P       p508    Number 282  O       o508    str_open p506 p507
1332  O       o508    location p507 p508  P       p508    String RefineError
1333  O       o509    str_open p507 p508  O       o509    string p508
1334  P       p450    String TermAddr  T       t509    o509
 O       o451    string p450  
 T       t451    o451  
 B       b451    t451  
 T       t452    o b451 b4  
 B       b452    t452  
 T       t453    o b423 b452  
 B       b453    t453  
 T       t454    o b423 b453  
 B       b454    t454  
 T       t509    o509 b454  
1335  B       b509    t509  B       b509    t509
1336  T       t512    o407 b509  T       t510    o b509 b4
1337    B       b510    t510
1338    T       t511    o b445 b510
1339    B       b511    t511
1340    T       t512    o b445 b511
1341  B       b512    t512  B       b512    t512
1342  T       t513    o508 b512  T       t513    o508 b512
1343  B       b513    t513  B       b513    t513
1344  P       p513    Number 283  T       t514    o429 b513
1345  P       p514    Number 311  B       b514    t514
1346  O       o514    location p513 p514  T       t515    o507 b514
1347  O       o515    str_open p513 p514  B       b515    t515
1348  P       p459    String TermMan  P       p515    Number 365
1349  O       o460    string p459  P       p516    Number 381
1350  T       t460    o460  O       o516    location p515 p516
1351  B       b460    t460  O       o517    str_open p515 p516
1352  T       t461    o b460 b4  P       p517    String Mp_resource
1353  B       b461    t461  O       o518    string p517
1354  T       t462    o b423 b461  T       t518    o518
1355  B       b462    t462  B       b518    t518
1356  T       t463    o b423 b462  T       t519    o b518 b4
1357  B       b463    t463  B       b519    t519
1358  T       t520    o515 b463  T       t520    o517 b519
1359  B       b520    t520  B       b520    t520
1360  T       t521    o407 b520  T       t521    o429 b520
1361  B       b521    t521  B       b521    t521
1362  T       t522    o514 b521  T       t522    o516 b521
1363  B       b522    t522  B       b522    t522
1364  P       p522    Number 312  P       p522    Number 382
1365  P       p523    Number 342  P       p523    Number 399
1366  O       o523    location p522 p523  O       o523    location p522 p523
1367  O       o524    str_open p522 p523  O       o524    str_open p522 p523
1368  P       p468    String TermSubst  P       p524    String Simple_print
 O       o469    string p468  
 T       t469    o469  
 B       b469    t469  
 T       t470    o b469 b4  
 B       b470    t470  
 T       t471    o b423 b470  
 B       b471    t471  
 T       t472    o b423 b471  
 B       b472    t472  
 T       t524    o524 b472  
 B       b524    t524  
 T       t528    o407 b524  
 B       b528    t528  
 T       t599    o523 b528  
 B       b599    t599  
 P       p599    Number 343  
 P       p600    Number 370  
 O       o600    location p599 p600  
 O       o601    str_open p599 p600  
 P       p477    String Refine  
 O       o478    string p477  
 T       t478    o478  
 B       b478    t478  
 T       t479    o b478 b4  
 B       b479    t479  
 T       t480    o b423 b479  
 B       b480    t480  
 T       t481    o b423 b480  
 B       b481    t481  
 T       t603    o601 b481  
 B       b603    t603  
 T       t604    o407 b603  
 B       b604    t604  
 T       t618    o600 b604  
 B       b618    t618  
 P       p622    Number 371  
 P       p624    Number 403  
 O       o625    location p622 p624  
 O       o629    str_open p622 p624  
 P       p486    String RefineError  
 O       o487    string p486  
 T       t487    o487  
 B       b487    t487  
 T       t488    o b487 b4  
 B       b488    t488  
 T       t489    o b423 b488  
 B       b489    t489  
 T       t490    o b423 b489  
 B       b490    t490  
 T       t629    o629 b490  
 B       b629    t629  
 T       t633    o407 b629  
 B       b633    t633  
 T       t635    o625 b633  
 B       b635    t635  
 P       p635    Number 404  
 P       p636    Number 420  
 O       o638    location p635 p636  
 O       o647    str_open p635 p636  
 P       p495    String Mp_resource  
 O       o496    string p495  
 T       t496    o496  
 B       b496    t496  
 T       t497    o b496 b4  
 B       b497    t497  
 T       t648    o647 b497  
 B       b648    t648  
 T       t649    o407 b648  
 B       b649    t649  
 T       t650    o638 b649  
 B       b650    t650  
 P       p650    Number 421  
 P       p651    Number 438  
 O       o651    location p650 p651  
 O       o652    str_open p650 p651  
 P       p502    String Simple_print  
 O       o503    string p502  
 T       t503    o503  
 B       b503    t503  
 T       t504    o b503 b4  
 B       b504    t504  
 T       t652    o652 b504  
 B       b652    t652  
 T       t653    o407 b652  
 B       b653    t653  
 T       t654    o651 b653  
 B       b654    t654  
 P       p654    Number 440  
 P       p655    Number 456  
 O       o655    location p654 p655  
 O       o656    str_open p654 p655  
 P       p509    String Tactic_type  
 O       o510    string p509  
 T       t510    o510  
 B       b510    t510  
 T       t511    o b510 b4  
 B       b511    t511  
 T       t657    o656 b511  
 B       b657    t657  
 T       t658    o407 b657  
 B       b658    t658  
 T       t659    o655 b658  
 B       b659    t659  
 P       p659    Number 457  
 P       p660    Number 483  
 O       o660    location p659 p660  
 O       o661    str_open p659 p660  
 P       p516    String Tacticals  
 O       o517    string p516  
 T       t517    o517  
 B       b517    t517  
 T       t518    o b517 b4  
 B       b518    t518  
 T       t519    o b510 b518  
 B       b519    t519  
 T       t662    o661 b519  
 B       b662    t662  
 T       t669    o407 b662  
 B       b669    t669  
 T       t681    o660 b669  
 B       b681    t681  
 P       p681    Number 484  
 P       p682    Number 508  
 O       o682    location p681 p682  
 O       o684    str_open p681 p682  
 P       p524    String Sequent  
1369  O       o525    string p524  O       o525    string p524
1370  T       t525    o525  T       t525    o525
1371  B       b525    t525  B       b525    t525
1372  T       t526    o b525 b4  T       t526    o b525 b4
1373  B       b526    t526  B       b526    t526
1374  T       t527    o b510 b526  T       t527    o524 b526
1375  B       b527    t527  B       b527    t527
1376  T       t686    o684 b527  T       t528    o429 b527
1377  B       b686    t686  B       b528    t528
1378  T       t687    o407 b686  T       t529    o523 b528
1379  B       b687    t687  B       b529    t529
1380  T       t688    o682 b687  P       p529    Number 401
1381  B       b688    t688  P       p530    Number 417
1382  P       p688    Number 509  O       o530    location p529 p530
1383  P       p532    String Conversionals  O       o531    str_open p529 p530
1384  O       o533    string p532  P       p531    String Tactic_type
1385  T       t533    o533  O       o532    string p531
1386    T       t532    o532
1387    B       b532    t532
1388    T       t533    o b532 b4
1389  B       b533    t533  B       b533    t533
1390  T       t534    o b533 b4  T       t534    o531 b533
1391  B       b534    t534  B       b534    t534
1392  T       t535    o b510 b534  T       t535    o429 b534
1393  B       b535    t535  B       b535    t535
1394  O       o541    string p147  T       t536    o530 b535
1395  T       t541    o541  B       b536    t536
1396    P       p536    Number 418
1397    P       p537    Number 444
1398    O       o537    location p536 p537
1399    O       o538    str_open p536 p537
1400    P       p538    String Tacticals
1401    O       o539    string p538
1402    T       t539    o539
1403    B       b539    t539
1404    T       t540    o b539 b4
1405    B       b540    t540
1406    T       t541    o b532 b540
1407  B       b541    t541  B       b541    t541
1408  T       t542    o b541 b4  T       t542    o538 b541
1409  B       b542    t542  B       b542    t542
1410  O       o548    string p145  T       t543    o429 b542
1411  T       t548    o548  B       b543    t543
1412    T       t544    o537 b543
1413    B       b544    t544
1414    P       p544    Number 445
1415    P       p545    Number 469
1416    O       o545    location p544 p545
1417    O       o546    str_open p544 p545
1418    P       p546    String Sequent
1419    O       o547    string p546
1420    T       t547    o547
1421    B       b547    t547
1422    T       t548    o b547 b4
1423  B       b548    t548  B       b548    t548
1424  T       t549    o b548 b4  T       t549    o b532 b548
1425  B       b549    t549  B       b549    t549
1426  P       p554    Number 539  T       t550    o546 b549
1427  O       o688    location p688 p554  B       b550    t550
1428  O       o689    str_open p688 p554  T       t551    o429 b550
1429  T       t689    o689 b535  B       b551    t551
1430  B       b689    t689  T       t552    o545 b551
1431  T       t690    o407 b689  B       b552    t552
1432  B       b690    t690  P       p552    Number 470
1433  T       t700    o688 b690  P       p553    Number 500
1434  B       b700    t700  O       o553    location p552 p553
1435  P       p700    Number 540  O       o554    str_open p552 p553
1436  P       p702    Number 550  P       p554    String Conversionals
1437  O       o702    location p700 p702  O       o555    string p554
 O       o703    str_open p700 p702  
 T       t703    o703 b542  
 B       b703    t703  
 T       t704    o407 b703  
 B       b704    t704  
 T       t707    o702 b704  
 B       b707    t707  
 P       p709    Number 551  
 P       p710    Number 559  
 O       o710    location p709 p710  
 O       o713    str_open p709 p710  
 T       t717    o713 b549  
 B       b717    t717  
 T       t724    o407 b717  
 B       b724    t724  
 T       t729    o710 b724  
 B       b729    t729  
 P       p729    Number 561  
 O       o555    string p135  
1438  T       t555    o555  T       t555    o555
1439  B       b555    t555  B       b555    t555
1440  T       t556    o b555 b4  T       t556    o b555 b4
1441  B       b556    t556  B       b556    t556
1442  P       p570    Number 578  T       t557    o b532 b556
1443  O       o729    location p729 p570  B       b557    t557
1444  O       o731    str_open p729 p570  T       t558    o554 b557
1445  T       t732    o731 b556  B       b558    t558
1446  B       b732    t732  T       t559    o429 b558
1447  T       t733    o407 b732  B       b559    t559
1448  B       b733    t733  T       t560    o553 b559
1449  T       t734    o729 b733  B       b560    t560
1450  B       b734    t734  P       p560    Number 501
1451  P       p734    Number 579  P       p561    Number 511
1452  P       p735    Number 600  O       o561    location p560 p561
1453  O       o735    location p734 p735  O       o562    str_open p560 p561
1454  O       o736    str_open p734 p735  O       o563    string p155
1455  O       o562    string p137  T       t563    o563
 T       t562    o562  
 B       b562    t562  
 T       t563    o b562 b4  
1456  B       b563    t563  B       b563    t563
1457  T       t736    o736 b563  T       t564    o b563 b4
1458  B       b736    t736  B       b564    t564
1459  T       t737    o407 b736  T       t565    o562 b564
1460  B       b737    t737  B       b565    t565
1461  T       t738    o735 b737  T       t566    o429 b565
1462  B       b738    t738  B       b566    t566
1463  P       p602    Number 602  T       t567    o561 b566
1464  P       p738    Number 626  B       b567    t567
1465  O       o738    location p602 p738  P       p567    Number 512
1466    P       p568    Number 520
1467    O       o568    location p567 p568
1468    O       o569    str_open p567 p568
1469    O       o570    string p153
1470    T       t570    o570
1471    B       b570    t570
1472    T       t571    o b570 b4
1473    B       b571    t571
1474    T       t572    o569 b571
1475    B       b572    t572
1476    T       t573    o429 b572
1477    B       b573    t573
1478    T       t574    o568 b573
1479    B       b574    t574
1480    P       p574    Number 522
1481    P       p575    Number 539
1482    O       o575    location p574 p575
1483    O       o576    str_open p574 p575
1484    O       o577    string p143
1485    T       t577    o577
1486    B       b577    t577
1487    T       t578    o b577 b4
1488    B       b578    t578
1489    T       t579    o576 b578
1490    B       b579    t579
1491    T       t580    o429 b579
1492    B       b580    t580
1493    T       t581    o575 b580
1494    B       b581    t581
1495    P       p581    Number 540
1496    P       p582    Number 561
1497    O       o582    location p581 p582
1498    O       o583    str_open p581 p582
1499    O       o584    string p145
1500    T       t584    o584
1501    B       b584    t584
1502    T       t585    o b584 b4
1503    B       b585    t585
1504    T       t586    o583 b585
1505    B       b586    t586
1506    T       t587    o429 b586
1507    B       b587    t587
1508    T       t588    o582 b587
1509    B       b588    t588
1510    P       p588    Number 563
1511    P       p589    Number 587
1512    O       o589    location p588 p589
1513  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1514  P       p739    String cycgroup  P       p590    String cycgroup
1515  O       o739    opname p739  O       o590    opname p590
1516  NCzf_itt_cyclic_group   Czf_itt_cyclic_group    Czf_itt_cyclic_group NIL  NCzf_itt_cyclic_group   Czf_itt_cyclic_group    Czf_itt_cyclic_group NIL
1517  NCzf_itt_cyclic_group!cycgroup  cycgroup        cycgroup Czf_itt_cyclic_group  NCzf_itt_cyclic_group!cycgroup  cycgroup        cycgroup Czf_itt_cyclic_group
1518  O       o740    cycgroup  O       o591    cycgroup
1519  NCzf_itt_cyclic_subgroup        Czf_itt_cyclic_subgroup Czf_itt_cyclic_subgroup NIL  Nvar    var     var NIL
1520    P       p591    Var g
1521    O       o592    var p591
1522    T       t592    o592
1523    B       b592    t592
1524    P       p592    Var a
1525    O       o593    var p592
1526    T       t593    o593
1527    B       b593    t593
1528    T       t594    o591 b592 b593
1529    B       b594    t594
1530    T       t595    o590 b594
1531    B       b595    t595
1532    T       t596    o589 b595
1533    B       b596    t596
1534    P       p596    Number 589
1535    P       p597    Number 723
1536    O       o597    location p596 p597
1537  NSummary!rewrite        rewrite rewrite Summary  NSummary!rewrite        rewrite rewrite Summary
1538    P       p598    String unfold_cycgroup
1539    O       o598    rewrite p598
1540    NItt_logic      Itt_logic       Itt_logic NIL
1541    NItt_logic!and  and     and Itt_logic
1542    O       o599    and
1543    NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1544    NCzf_itt_group!group    group   group Czf_itt_group
1545    O       o600    group
1546    T       t600    o600 b592
1547    B       b600    t600
1548    NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1549    NCzf_itt_member!mem     mem     mem Czf_itt_member
1550    O       o601    mem
1551    NCzf_itt_group!car      car     car Czf_itt_group
1552    O       o602    car
1553    T       t602    o602 b592
1554    B       b602    t602
1555    T       t603    o601 b593 b602
1556    B       b603    t603
1557    NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
1558    NCzf_itt_eq!equal       equal   equal Czf_itt_eq
1559    O       o603    equal
1560    NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL
1561    NCzf_itt_set!collect    collect collect Czf_itt_set
1562    O       o604    collect
1563    NItt_int_base   Itt_int_base    Itt_int_base NIL
1564    NItt_int_base!int       int     int Itt_int_base
1565    O       o605    int
1566    T       t605    o605
1567    B       b605    t605
1568    NCzf_itt_cyclic_subgroup        Czf_itt_cyclic_subgroup Czf_itt_cyclic_subgroup NIL
1569    NCzf_itt_cyclic_subgroup!power  power   power Czf_itt_cyclic_subgroup
1570    O       o606    power
1571    P       p606    Var x
1572    O       o607    var p606
1573    T       t607    o607
1574    B       b607    t607
1575    T       t608    o606 b592 b593 b607
1576    B       b608    t608 x
1577    T       t609    o604 b605 b608
1578    B       b609    t609
1579    T       t610    o603 b602 b609
1580    B       b610    t610
1581    T       t611    o599 b603 b610
1582    B       b611    t611
1583    T       t612    o599 b600 b611
1584    B       b612    t612
1585  NSummary!prim   prim    prim Summary  NSummary!prim   prim    prim Summary
1586  O       o577    prim  O       o612    prim
1587  T       t577    o577 b4  T       t613    o612 b4
1588  B       b577    t577  B       b613    t613
1589    T       t614    o598 b594 b612 b613 b4
1590    B       b614    t614
1591    T       t615    o597 b614
1592    B       b615    t615
1593    P       p615    Number 725
1594    P       p616    Number 793
1595    O       o616    location p615 p616
1596  NOcaml!str_let  str_let str_let Ocaml  NOcaml!str_let  str_let str_let Ocaml
1597    O       o617    str_let p615 p616
1598  NOcaml!patt_var patt_var        patt_var Ocaml  NOcaml!patt_var patt_var        patt_var Ocaml
1599    P       p617    Number 729
1600    P       p618    Number 742
1601    O       o618    patt_var p617 p618
1602  NOcaml!patt_done        patt_done       patt_done Ocaml  NOcaml!patt_done        patt_done       patt_done Ocaml
1603    O       o619    patt_done p615 p616
1604    T       t619    o619
1605    B       b619    t619 fold_cycgroup
1606    T       t620    o618 b619
1607    B       b620    t620
1608  NOcaml!apply    apply   apply Ocaml  NOcaml!apply    apply   apply Ocaml
1609    P       p620    Number 745
1610    O       o620    apply p620 p616
1611    P       p621    Number 777
1612    O       o621    apply p620 p621
1613  NOcaml!lid      lid     lid Ocaml  NOcaml!lid      lid     lid Ocaml
1614  P       p587    String makeFoldC  P       p622    Number 754
1615  O       o587    lid p587  O       o622    lid p620 p622
1616  T       t587    o587  P       p623    String makeFoldC
1617  B       b587    t587  O       o623    lid p623
1618    T       t623    o623
1619    B       b623    t623
1620    T       t624    o622 b623
1621    B       b624    t624
1622    P       p624    Number 755
1623    O       o624    apply p624 p621
1624  NOcaml!proj     proj    proj Ocaml  NOcaml!proj     proj    proj Ocaml
1625    O       o625    proj p624 p621
1626  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
1627  P       p590    String Ml_term  O       o626    uid p624 p621
1628  O       o591    uid p590  P       p626    String Ml_term
1629  T       t591    o591  O       o627    uid p626
1630  B       b591    t591  T       t627    o627
1631  P       p592    String term_of_string  B       b627    t627
1632  O       o593    lid p592  T       t628    o626 b627
1633  T       t593    o593  B       b628    t628
1634  B       b593    t593  O       o628    lid p624 p621
1635    P       p628    String term_of_string
1636    O       o629    lid p628
1637    T       t629    o629
1638    B       b629    t629
1639    T       t630    o628 b629
1640    B       b630    t630
1641    T       t631    o625 b628 b630
1642    B       b631    t631
1643    P       p631    String "MP-Caml3.02 term:\\132\\149\\166\\190\\000\\000\\000O\\000\\000\\000\\026\\000\\000\\000N\\000\\000\\000I\\160\\160\\160$\\000\\000\\000\\000\\160(cycgroup\\1604Czf_itt_cyclic_group@@\\160\\160@\\160\\160\\160\\004\\n\\160#var@\\160\\148!g@@\\160\\160@\\160\\160\\160\\004\\020\\004\\n\\160\\148!a@@@"
1644    O       o631    string p624 p621 p631
1645    T       t632    o631
1646    B       b632    t632
1647    T       t633    o624 b631 b632
1648    B       b633    t633
1649    T       t634    o621 b624 b633
1650    B       b634    t634
1651    P       p634    Number 778
1652    O       o634    lid p634 p616
1653    O       o635    lid p598
1654    T       t635    o635
1655    B       b635    t635
1656    T       t636    o634 b635
1657    B       b636    t636
1658    T       t637    o620 b634 b636
1659    B       b637    t637
1660    T       t638    o617 b620 b637
1661    B       b638    t638
1662    T       t639    o b638 b4
1663    B       b639    t639
1664    T       t640    o617 b639
1665    B       b640    t640
1666    T       t641    o429 b640
1667    B       b641    t641
1668    T       t642    o616 b641
1669    B       b642    t642
1670    P       p642    Number 795
1671    P       p643    Number 906
1672    O       o643    location p642 p643
1673  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
1674  P       p608    String cyclic_group_df  P       p644    String cyclic_group_df
1675  O       o608    dform p608  O       o644    dform p644
1676  NSummary!except_mode_df except_mode_df  except_mode_df Summary  NSummary!except_mode_df except_mode_df  except_mode_df Summary
1677  P       p609    String src  P       p645    String src
1678  O       o609    except_mode_df p609  O       o645    except_mode_df p645
1679  T       t609    o609  T       t645    o645
1680  B       b609    t609  B       b645    t645
1681  T       t610    o b609 b4  T       t646    o b645 b4
1682  B       b610    t610  B       b646    t646
1683  NSummary!df_term        df_term df_term Summary  NSummary!df_term        df_term df_term Summary
1684  O       o610    df_term  O       o646    df_term
1685  NPerv!string    string610       string Perv  NPerv!string    string646       string Perv
1686    P       p646    String cyclic_group(
1687    O       o647    string646 p646
1688    T       t647    o647
1689    B       b647    t647
1690    Nslot   slot    slot NIL
1691    O       o648    slot
1692    T       t648    o648 b592
1693    B       b648    t648
1694    P       p648    String "; "
1695    O       o649    string646 p648
1696    T       t649    o649
1697    B       b649    t649
1698    T       t650    o648 b593
1699    B       b650    t650
1700    P       p650    String )
1701    O       o650    string646 p650
1702    T       t651    o650
1703    B       b651    t651
1704    T       t652    o b651 b4
1705    B       b652    t652
1706    T       t653    o b650 b652
1707    B       b653    t653
1708    T       t654    o b649 b653
1709    B       b654    t654
1710    T       t655    o b648 b654
1711    B       b655    t655
1712    T       t656    o b647 b655
1713    B       b656    t656
1714    T       t657    o646 b656
1715    B       b657    t657
1716    T       t658    o644 b646 b594 b657
1717    B       b658    t658
1718    T       t659    o643 b658
1719    B       b659    t659
1720    P       p3      Number 908
1721    P       p4      Number 1094
1722    O       o6      location p3 p4
1723    O       o659    location p p
1724  NSummary!rule   rule    rule Summary  NSummary!rule   rule    rule Summary
1725    P       p659    String cycgroup_wf
1726    O       o660    rule p659
1727  NSummary!context_param  context_param   context_param Summary  NSummary!context_param  context_param   context_param Summary
1728  P       p620    String H  P       p660    String H
1729  O       o620    context_param p620  O       o661    context_param p660
1730  T       t620    o620  T       t661    o661
1731  B       b620    t620  B       b661    t661
1732  T       t621    o b620 b4  T       t662    o b661 b4
1733  B       b621    t621  B       b662    t662
1734    NSummary!meta_implies   meta_implies    meta_implies Summary
1735    O       o662    meta_implies
1736  NSummary!meta_theorem   meta_theorem    meta_theorem Summary  NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1737  O       o621    meta_theorem  O       o663    meta_theorem
1738  Nvar    var     var NIL  NBase_trivial   Base_trivial    Base_trivial NIL
1739  P       p604    Var g  NBase_trivial!squash    squash  squash Base_trivial
1740  O       o605    var p604  O       o664    squash
1741  T       t605    o605  T       t664    o664
1742  B       b605    t605  B       b664    t664
1743  P       p594    Var a  T       t665    o b664 b4
1744  O       o596    var p594  C       h       H
1745  T       t607    o596  NItt_equal      Itt_equal       Itt_equal NIL
1746  B       b607    t607  NItt_equal!equal        equal665        equal Itt_equal
1747  T       t740    o740 b605 b607  O       o665    equal665
1748    NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1749    NItt_record_label0!label        label   label Itt_record_label0
1750    O       o666    label
1751    T       t666    o666
1752    B       b666    t666
1753    T       t667    o665 b666 b592 b592
1754    S       s       t665 h
1755    G       s       t667
1756    B       b667    s
1757    T       t668    o663 b667
1758    B       b668    t668
1759    NCzf_itt_set!isset      isset   isset Czf_itt_set
1760    O       o668    isset
1761    T       t669    o668 b593
1762    S       s669    t665 h
1763    G       s669    t669
1764    B       b669    s669
1765    T       t670    o663 b669
1766    B       b670    t670
1767    P       p670    Var ext
1768    O       o670    var p670
1769    T       t671    o670
1770    B       b671    t671
1771    T       t672    o b671 b4
1772    NItt_equal!type type    type Itt_equal
1773    O       o672    type
1774    T       t673    o672 b594
1775    S       s673    t672 h
1776    G       s673    t673
1777    B       b673    s673
1778    T       t674    o663 b673
1779    B       b674    t674
1780    T       t675    o662 b670 b674
1781    B       b675    t675
1782    T       t676    o662 b668 b675
1783    B       b676    t676
1784    NSummary!interactive    interactive     interactive Summary
1785    O       o676    interactive
1786    NSummary!ext_rule       ext_rule        ext_rule Summary
1787    P       p676    String "rwh unfold_cycgroup 0 thenT autoT"
1788    O       o677    ext_rule p676
1789    NSummary!status_incomplete      status_incomplete       status_incomplete Summary
1790    O       o678    status_incomplete
1791    T       t678    o678
1792    B       b678    t678
1793    NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
1794    O       o679    ext_unjustified
1795    NSummary!tactic_arg     tactic_arg      tactic_arg Summary
1796    P       p679    String main
1797    O       o680    tactic_arg p679
1798    NSummary!msequent       msequent        msequent Summary
1799    O       o681    msequent
1800    T       t681    o b669 b4
1801    B       b681    t681
1802    T       t682    o b667 b681
1803    B       b682    t682
1804    T       t683    o681 b673 b682
1805    B       b683    t683
1806    NSummary!parent_none    parent_none     parent_none Summary
1807    O       o683    parent_none
1808    T       t684    o683
1809    B       b684    t684
1810    T       t685    o680 b683 b4 b684
1811    B       b685    t685
1812    T       t686    o679 b685 b4
1813    B       b686    t686
1814    T       t687    o677 b678 b686 b4 b4
1815    B       b687    t687
1816    T       t688    o676 b687
1817    B       b688    t688
1818    NSummary!resource_defs  resource_defs   resource_defs Summary
1819    P       p688    Number 935
1820    P       p689    Number 943
1821    O       o689    resource_defs p688 p689 p300
1822    P       p690    Number 941
1823    O       o690    uid p690 p689
1824    P       p691    String []
1825    O       o691    uid p691
1826    T       t691    o691
1827    B       b691    t691
1828    T       t692    o690 b691
1829    B       b692    t692
1830    T       t693    o b692 b4
1831    B       b693    t693
1832    T       t694    o689 b693
1833    B       b694    t694
1834    T       t695    o b694 b4
1835    B       b695    t695
1836    T       t696    o660 b662 b676 b688 b695
1837    B       b696    t696
1838    T       t250    o6 b696
1839    B       b250    t250
1840    P       p260    Number 1096
1841    P       p261    Number 1451
1842    O       o261    location p260 p261
1843    P       p697    String cycgroup_intro
1844    O       o697    rule p697
1845    S       s697    t672 h
1846    G       s697    t600
1847    B       b698    s697
1848    T       t698    o663 b698
1849    B       b699    t698
1850    S       s699    t672 h
1851    G       s699    t603
1852    B       b700    s699
1853    T       t700    o663 b700
1854    B       b701    t700
1855    S       s701    t672 h
1856    G       s701    t610
1857    B       b702    s701
1858    T       t702    o663 b702
1859    B       b703    t702
1860    S       s703    t672 h
1861    G       s703    t594
1862    B       b704    s703
1863    T       t704    o663 b704
1864    B       b705    t704
1865    T       t705    o662 b703 b705
1866    B       b706    t705
1867    T       t706    o662 b701 b706
1868    B       b707    t706
1869    T       t707    o662 b670 b707
1870    B       b708    t707
1871    T       t708    o662 b699 b708
1872    B       b709    t708
1873    T       t709    o662 b668 b709
1874    B       b710    t709
1875    T       t710    o b702 b4
1876    B       b711    t710
1877    T       t711    o b700 b711
1878    B       b712    t711
1879    T       t712    o b669 b712
1880    B       b713    t712
1881    T       t713    o b698 b713
1882    B       b714    t713
1883    T       t714    o b667 b714
1884    B       b715    t714
1885    T       t715    o681 b704 b715
1886    B       b716    t715
1887    T       t716    o680 b716 b4 b684
1888    B       b717    t716
1889    T       t717    o679 b717 b4
1890    B       b718    t717
1891    T       t718    o677 b678 b718 b4 b4
1892    B       b719    t718
1893    T       t719    o676 b719
1894    B       b720    t719
1895    P       p720    Number 1126
1896    P       p721    Number 1134
1897    O       o721    resource_defs p720 p721 p300
1898    P       p722    Number 1132
1899    O       o722    uid p722 p721
1900    T       t722    o722 b691
1901    B       b722    t722
1902    T       t723    o b722 b4
1903    B       b723    t723
1904    T       t724    o721 b723
1905    B       b724    t724
1906    T       t725    o b724 b4
1907    B       b725    t725
1908    T       t726    o697 b662 b710 b720 b725
1909    B       b726    t726
1910    T       t265    o261 b726
1911    B       b265    t265
1912    P       p270    Number 1489
1913    P       p271    Number 1789
1914    O       o271    location p270 p271
1915    P       p727    String cycgroup_abel
1916    O       o727    rule p727
1917    NSummary!term_param     term_param      term_param Summary
1918    O       o728    term_param
1919    T       t728    o728 b593
1920    B       b728    t728
1921    T       t729    o b728 b4
1922    B       b729    t729
1923    T       t730    o b661 b729
1924    B       b730    t730
1925    NCzf_itt_abel_group     Czf_itt_abel_group      Czf_itt_abel_group NIL
1926    NCzf_itt_abel_group!abel        abel    abel Czf_itt_abel_group
1927    O       o730    abel
1928    T       t731    o730 b592
1929    S       s731    t672 h
1930    G       s731    t731
1931    B       b731    s731
1932    T       t732    o663 b731
1933    B       b732    t732
1934    T       t733    o662 b705 b732
1935    B       b733    t733
1936    T       t734    o662 b701 b733
1937    B       b734    t734
1938    T       t735    o662 b670 b734
1939    B       b735    t735
1940    T       t736    o662 b699 b735
1941    B       b736    t736
1942    T       t737    o662 b668 b736
1943    B       b737    t737
1944    P       p737    String "assumT 5 thenT rwh unfold_cycgroup 2 thenT autoT"
1945    O       o737    ext_rule p737
1946    T       t738    o b704 b4
1947    B       b738    t738
1948    T       t739    o b700 b738
1949    B       b739    t739
1950    T       t740    o b669 b739
1951  B       b740    t740  B       b740    t740
1952  T       t741    o739 b740  T       t741    o b698 b740
1953  B       b741    t741  B       b741    t741
1954  T       t742    o738 b741  T       t742    o b667 b741
1955  B       b742    t742  B       b742    t742
1956  P       p742    Number 628  T       t743    o681 b731 b742
1957  P       p743    Number 699  B       b743    t743
1958  O       o743    location p742 p743  T       t744    o680 b743 b4 b684
1959  P       p744    String unfold_cycgroup  B       b744    t744
1960  O       o744    rewrite p744  H       h744    y t600
1961  NCzf_itt_cyclic_subgroup!cyc_subg       cyc_subg        cyc_subg Czf_itt_cyclic_subgroup  H       h745    y_1 t603
1962  O       o745    cyc_subg  H       h746    z_1 t610
1963  T       t750    o745 b605 b605 b607  NCzf_itt_set!set        set     set Czf_itt_set
1964    O       o746    set
1965    T       t746    o746
1966    H       h747    a_1 t746
1967    H       h748    b t746
1968    P       p748    Var a_1
1969    O       o748    var p748
1970    T       t748    o748
1971    B       b748    t748
1972    T       t749    o601 b748 b602
1973    H       h749    x t749
1974    P       p749    Var b
1975    O       o749    var p749
1976    T       t750    o749
1977  B       b750    t750  B       b750    t750
1978  T       t753    o744 b740 b750 b577 b4  T       t751    o601 b750 b602
1979    H       h751    y t751
1980    NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1981    NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1982    O       o751    equiv
1983    NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
1984    O       o752    eqG
1985    T       t752    o752 b592
1986    B       b752    t752
1987    NCzf_itt_group!op       op      op Czf_itt_group
1988    O       o753    op
1989    T       t753    o753 b592 b748 b750
1990  B       b753    t753  B       b753    t753
1991  T       t754    o743 b753  T       t754    o753 b592 b750 b748
1992  B       b754    t754  B       b754    t754
1993  P       p754    Number 701  T       t755    o751 b602 b752 b753 b754
1994  P       p755    Number 769  S       s755    t672 h h744 h745 h746 h747 h748 h749 h751
1995  O       o755    location p754 p755  G       s755    t755
1996  O       o756    str_let p754 p755  B       b755    s755
1997  P       p756    Number 705  T       t756    o681 b755 b742
1998  P       p758    Number 718  B       b756    t756
1999  O       o758    patt_var p756 p758  S       s756    t672 h h744 h745 h746
2000  O       o763    patt_done p754 p755  G       s756    t731
2001  T       t768    o763  B       b757    s756
2002  B       b878    t768 fold_cycgroup  T       t757    o681 b757 b742
2003  T       t878    o758 b878  B       b758    t757
2004  B       b880    t878  NSummary!arg_named      arg_named       arg_named Summary
2005  P       p882    Number 721  P       p758    String d_auto
2006  O       o882    apply p882 p755  O       o758    arg_named p758
2007  P       p883    Number 753  NSummary!arg_bool       arg_bool        arg_bool Summary
2008  O       o883    apply p882 p883  P       p759    String true
2009  P       p884    Number 730  O       o759    arg_bool p759
2010  O       o884    lid p882 p884  T       t759    o759
2011  T       t885    o884 b587  B       b759    t759
2012    T       t760    o758 b759
2013    B       b760    t760
2014    T       t761    o b760 b4
2015    B       b761    t761
2016    H       h761    z t611
2017    S       s761    t672 h h744 h761
2018    G       s761    t731
2019    B       b762    s761
2020    T       t762    o681 b762 b742
2021    B       b763    t762
2022    H       h763    v t612
2023    S       s763    t672 h h763
2024    G       s763    t731
2025    B       b764    s763
2026    T       t764    o681 b764 b742
2027    B       b765    t764
2028    H       h765    v t594
2029    S       s765    t672 h h765
2030    G       s765    t731
2031    B       b766    s765
2032    T       t766    o681 b766 b742
2033    B       b767    t766
2034    T       t767    o2 b744
2035    B       b768    t767
2036    T       t768    o680 b767 b4 b768
2037    B       b769    t768
2038    T       t769    o2 b769
2039    B       b770    t769
2040    T       t770    o680 b765 b4 b770
2041    B       b771    t770
2042    T       t771    o2 b771
2043    B       b772    t771
2044    T       t772    o680 b763 b4 b772
2045    B       b773    t772
2046    T       t773    o2 b773
2047    B       b774    t773
2048    T       t774    o680 b758 b761 b774
2049    B       b775    t774
2050    T       t775    o2 b775
2051    B       b776    t775
2052    T       t776    o680 b756 b4 b776
2053    B       b777    t776
2054    T       t777    o b777 b4
2055    B       b778    t777
2056    T       t778    o679 b744 b778
2057    B       b779    t778
2058    P       p779    String "setSubstT << equal{car{'g}; collect{int; x. power{'g; 'a; 'x}}} >> 7 ttca thenT setSubstT << equal{car{'g}; collect{int; x. power{'g; 'a; 'x}}} >> 8 ttca"
2059    O       o779    ext_rule p779
2060    T       t779    o601 b748 b609
2061    H       h779    v t779
2062    T       t780    o601 b750 b609
2063    H       h780    v_1 t780
2064    S       s780    t672 h h744 h745 h746 h747 h748 h749 h751 h779 h780
2065    G       s780    t755
2066    B       b780    s780
2067    T       t781    o681 b780 b742
2068    B       b781    t781
2069    S       s781    t672 h h744 h745 h746 h747 h748 h749 h751 h779
2070    G       s781    t755
2071    B       b782    s781
2072    T       t782    o681 b782 b742
2073    B       b783    t782
2074    T       t783    o2 b777
2075    B       b784    t783
2076    T       t784    o680 b783 b4 b784
2077    B       b785    t784
2078    T       t785    o2 b785
2079    B       b786    t785
2080    T       t786    o680 b781 b4 b786
2081    B       b787    t786
2082    T       t787    o b787 b4
2083    B       b788    t787
2084    T       t788    o679 b777 b788
2085    B       b789    t788
2086    P       p789    String "rwh reduceC 10 thenT dT 10 ttca thenT rwh reduceC 9 thenT dT 9 ttca"
2087    O       o789    ext_rule p789
2088    H       h789    y_3 t605
2089    NCzf_itt_eq!eq  eq      eq Czf_itt_eq
2090    O       o790    eq
2091    P       p790    Var y_3
2092    O       o791    var p790
2093    T       t791    o791
2094    B       b791    t791
2095    T       t792    o606 b592 b593 b791
2096    B       b792    t792
2097    T       t793    o790 b748 b792
2098    H       h793    z_2 t793
2099    H       h794    y_2 t605
2100    P       p794    Var y_2
2101    O       o794    var p794
2102    T       t794    o794
2103    B       b794    t794
2104    T       t795    o606 b592 b593 b794
2105    B       b795    t795
2106    T       t796    o790 b750 b795
2107    H       h796    z t796
2108    S       s796    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2109    G       s796    t755
2110    B       b796    s796
2111    T       t797    o681 b796 b742
2112    B       b797    t797
2113    NItt_logic!exists       exists  exists Itt_logic
2114    O       o797    exists
2115    P       p797    Var t
2116    O       o798    var p797
2117    T       t798    o798
2118    B       b798    t798
2119    T       t799    o606 b592 b593 b798
2120    B       b799    t799
2121    T       t800    o790 b748 b799
2122    B       b800    t800 t
2123    T       t801    o797 b605 b800
2124    H       h801    v t801
2125    S       s801    t672 h h744 h745 h746 h747 h748 h749 h751 h801 h794 h796
2126    G       s801    t755
2127    B       b801    s801
2128    T       t802    o681 b801 b742
2129    B       b802    t802
2130    S       s802    t672 h h744 h745 h746 h747 h748 h749 h751 h779 h794 h796
2131    G       s802    t755
2132    B       b803    s802
2133    T       t803    o681 b803 b742
2134    B       b804    t803
2135    T       t804    o790 b750 b799
2136    B       b805    t804 t
2137    T       t805    o797 b605 b805
2138    H       h805    v_1 t805
2139    S       s805    t672 h h744 h745 h746 h747 h748 h749 h751 h779 h805
2140    G       s805    t755
2141    B       b806    s805
2142    T       t806    o681 b806 b742
2143    B       b807    t806
2144    T       t807    o2 b787
2145    B       b808    t807
2146    T       t808    o680 b807 b4 b808
2147    B       b809    t808
2148    T       t809    o2 b809
2149    B       b810    t809
2150    T       t810    o680 b804 b4 b810
2151    B       b811    t810
2152    T       t811    o2 b811
2153    B       b812    t811
2154    T       t812    o680 b802 b4 b812
2155    B       b813    t812
2156    T       t813    o2 b813
2157    B       b814    t813
2158    T       t814    o680 b797 b4 b814
2159    B       b815    t814
2160    T       t815    o b815 b4
2161    B       b816    t815
2162    T       t816    o679 b787 b816
2163    B       b817    t816
2164    P       p817    String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 'a_1; 'b}; op{'g; power{'g; 'a; 'y_3}; power{'g; 'a; 'y_2}}} >> 0 thenT autoT"
2165    O       o817    ext_rule p817
2166    T       t817    o753 b592 b792 b795
2167    B       b818    t817
2168    T       t818    o751 b602 b752 b753 b818
2169    S       s818    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2170    G       s818    t818
2171    B       b819    s818
2172    T       t819    o681 b819 b742
2173    B       b820    t819
2174    T       t820    o2 b815
2175    B       b821    t820
2176    T       t821    o680 b820 b4 b821
2177    B       b822    t821
2178    T       t822    o751 b602 b752 b818 b754
2179    S       s822    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2180    G       s822    t822
2181    B       b823    s822
2182    T       t823    o681 b823 b742
2183    B       b824    t823
2184    T       t824    o680 b824 b4 b821
2185    B       b825    t824
2186    T       t825    o b825 b4
2187    B       b826    t825
2188    T       t826    o b822 b826
2189    B       b827    t826
2190    T       t827    o679 b815 b827
2191    B       b828    t827
2192    P       p828    String "setSubstT << equal{'b; power{'g; 'a; 'y_2}} >> 0 thenT autoT"
2193    O       o828    ext_rule p828
2194    T       t828    o751 b602 b752 b748 b792
2195    S       s828    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2196    G       s828    t828
2197    B       b829    s828
2198    T       t829    o681 b829 b742
2199    B       b830    t829
2200    T       t830    o753 b592 b748 b795
2201    B       b831    t830
2202    T       t831    o751 b602 b752 b831 b818
2203    S       s831    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2204    G       s831    t831
2205    B       b832    s831
2206    T       t832    o681 b832 b742
2207    B       b833    t832
2208    T       t833    o2 b822
2209    B       b834    t833
2210    T       t834    o680 b833 b761 b834
2211    B       b835    t834
2212    T       t835    o2 b835
2213    B       b836    t835
2214    T       t836    o680 b830 b4 b836
2215    B       b837    t836
2216    T       t837    o b837 b4
2217    B       b838    t837
2218    T       t838    o679 b822 b838
2219    B       b839    t838
2220    P       p839    String "setSubstT << equal{'a_1; power{'g; 'a; 'y_3}} >> 0 thenT autoT"
2221    O       o839    ext_rule p839
2222    T       t839    o679 b837 b4
2223    B       b840    t839
2224    T       t840    o839 b678 b840 b4 b4
2225    B       b841    t840
2226    T       t841    o b841 b4
2227    B       b842    t841
2228    T       t842    o828 b678 b839 b842 b4
2229    B       b843    t842
2230    P       p843    String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; power{'g; 'a; 'y_3}; power{'g; 'a; 'y_2}}; power{'g; 'a; ('y_3 +@ 'y_2)}} >> 0 thenT autoT"
2231    O       o843    ext_rule p843
2232    NItt_int_base!add       add     add Itt_int_base
2233    O       o844    add
2234    T       t844    o844 b791 b794
2235    B       b844    t844
2236    T       t845    o606 b592 b593 b844
2237    B       b845    t845
2238    T       t846    o751 b602 b752 b845 b754
2239    S       s846    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2240    G       s846    t846
2241    B       b846    s846
2242    T       t847    o681 b846 b742
2243    B       b847    t847
2244    T       t848    o2 b825
2245    B       b848    t848
2246    T       t849    o680 b847 b4 b848
2247    B       b849    t849
2248    T       t850    o b849 b4
2249    B       b850    t850
2250    T       t851    o679 b825 b850
2251    B       b851    t851
2252    P       p851    String "rwh add_CommutC 0 thenT autoT"
2253    O       o851    ext_rule p851
2254    T       t852    o844 b794 b791
2255    B       b852    t852
2256    T       t853    o606 b592 b593 b852
2257    B       b853    t853
2258    T       t854    o751 b602 b752 b853 b754
2259    S       s854    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2260    G       s854    t854
2261    B       b854    s854
2262    T       t855    o681 b854 b742
2263    B       b855    t855
2264    T       t856    o2 b849
2265    B       b856    t856
2266    T       t857    o680 b855 b4 b856
2267    B       b857    t857
2268    T       t858    o b857 b4
2269    B       b858    t858
2270    T       t859    o679 b849 b858
2271    B       b859    t859
2272    P       p859    String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 'b; 'a_1}; op{'g; power{'g; 'a; 'y_2}; power{'g; 'a; 'y_3}}} >> 0 thenT autoT"
2273    O       o859    ext_rule p859
2274    T       t860    o753 b592 b795 b792
2275    B       b860    t860
2276    T       t861    o751 b602 b752 b754 b860
2277    S       s861    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2278    G       s861    t861
2279    B       b861    s861
2280    T       t862    o681 b861 b742
2281    B       b862    t862
2282    T       t863    o2 b857
2283    B       b863    t863
2284    T       t864    o680 b862 b4 b863
2285    B       b864    t864
2286    T       t865    o751 b602 b752 b853 b860
2287    S       s865    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2288    G       s865    t865
2289    B       b865    s865
2290    T       t866    o681 b865 b742
2291    B       b866    t866
2292    T       t867    o680 b866 b4 b863
2293    B       b867    t867
2294    T       t868    o b867 b4
2295    B       b868    t868
2296    T       t869    o b864 b868
2297    B       b869    t869
2298    T       t870    o679 b857 b869
2299    B       b870    t870
2300    T       t871    o751 b602 b752 b750 b795
2301    S       s871    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2302    G       s871    t871
2303    B       b871    s871
2304    T       t872    o681 b871 b742
2305    B       b872    t872
2306    T       t873    o753 b592 b750 b792
2307    B       b873    t873
2308    T       t874    o751 b602 b752 b873 b860
2309    S       s874    t672 h h744 h745 h746 h747 h748 h749 h751 h789 h793 h794 h796
2310    G       s874    t874
2311    B       b874    s874
2312    T       t875    o681 b874 b742
2313    B       b875    t875
2314    T       t876    o2 b864
2315    B       b876    t876
2316    T       t877    o680 b875 b761 b876
2317    B       b877    t877
2318    T       t878    o2 b877
2319    B       b878    t878
2320    T       t879    o680 b872 b4 b878
2321    B       b879    t879
2322    T       t880    o b879 b4
2323    B       b880    t880
2324    T       t881    o679 b864 b880
2325    B       b881    t881
2326    T       t882    o679 b879 b4
2327    B       b882    t882
2328    T       t883    o828 b678 b882 b4 b4
2329    B       b883    t883
2330    T       t884    o b883 b4
2331    B       b884    t884
2332    T       t885    o839 b678 b881 b884 b4
2333  B       b885    t885  B       b885    t885
2334  P       p885    Number 731  P       p885    String "equivSymT ttca"
2335  O       o885    apply p885 p883  O       o885    ext_rule p885
2336  O       o886    proj p885 p883  T       t886    o679 b867 b4
2337  O       o887    uid p885 p883  B       b886    t886
2338  T       t887    o887 b591  T       t887    o885 b678 b886 b4 b4
2339  B       b887    t887  B       b887    t887
2340  O       o888    lid p885 p883  T       t888    o b887 b4
 T       t888    o888 b593  
2341  B       b888    t888  B       b888    t888
2342  T       t889    o886 b887 b888  T       t889    o b885 b888
2343  B       b889    t889  B       b889    t889
2344  P       p889    String "MP-Caml3.02 term:\\132\\149\\166\\190\\000\\000\\000O\\000\\000\\000\\026\\000\\000\\000N\\000\\000\\000I\\160\\160\\160$\\000\\000\\000\\000\\160(cycgroup\\1604Czf_itt_cyclic_group@@\\160\\160@\\160\\160\\160\\004\\n\\160#var@\\160\\148!g@@\\160\\160@\\160\\160\\160\\004\\020\\004\\n\\160\\148!a@@@"  T       t890    o859 b678 b870 b889 b4
 O       o889    string p885 p883 p889  
 T       t890    o889  
2345  B       b890    t890  B       b890    t890
2346  T       t891    o885 b889 b890  T       t891    o b890 b4
2347  B       b891    t891  B       b891    t891
2348  T       t892    o883 b885 b891  T       t892    o851 b678 b859 b891 b4
2349  B       b892    t892  B       b892    t892
2350  P       p892    Number 754  T       t893    o b892 b4
 O       o892    lid p892 p755  
 O       o893    lid p744  
 T       t893    o893  
2351  B       b893    t893  B       b893    t893
2352  T       t894    o892 b893  T       t894    o843 b678 b851 b893 b4
2353  B       b894    t894  B       b894    t894
2354  T       t895    o882 b892 b894  T       t895    o b894 b4
2355  B       b895    t895  B       b895    t895
2356  T       t896    o756 b880 b895  T       t896    o b843 b895
2357  B       b896    t896  B       b896    t896
2358  T       t897    o b896 b4  T       t897    o817 b678 b828 b896 b4
2359  B       b897    t897  B       b897    t897
2360  T       t898    o756 b897  T       t898    o b897 b4
2361  B       b898    t898  B       b898    t898
2362  T       t899    o407 b898  T       t899    o789 b678 b817 b898 b4
2363  B       b899    t899  B       b899    t899
2364  T       t900    o755 b899  T       t900    o b899 b4
2365  B       b900    t900  B       b900    t900
2366  P       p900    Number 771  T       t901    o779 b678 b789 b900 b4
 Nslot   slot    slot NIL  
 O       o961    slot  
 T       t961    o961 b607  
 B       b961    t961  
 P       p621    Var ext  
 O       o622    var p621  
 T       t622    o622  
 B       b622    t622  
 T       t623    o b622 b4  
 C       h       H  
 NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  
 NCzf_itt_eq!equal       equal   equal Czf_itt_eq  
 O       o623    equal  
 NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  
 NCzf_itt_group!car      car     car Czf_itt_group  
 O       o624    car  
 NSummary!resource_defs  resource_defs   resource_defs Summary  
 P       p630    String []  
 O       o630    uid p630  
 T       t630    o630  
 B       b630    t630  
 NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL  
 NCzf_itt_set!isset      isset   isset Czf_itt_set  
 O       o639    isset  
 NSummary!interactive    interactive     interactive Summary  
 O       o640    interactive  
 NSummary!ext_rule       ext_rule        ext_rule Summary  
 NSummary!status_incomplete      status_incomplete       status_incomplete Summary  
 O       o642    status_incomplete  
 T       t642    o642  
 B       b642    t642  
 NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  
 O       o643    ext_unjustified  
 NSummary!tactic_arg     tactic_arg      tactic_arg Summary  
 P       p643    String main  
 O       o644    tactic_arg p643  
 NSummary!msequent       msequent        msequent Summary  
 O       o645    msequent  
 NSummary!parent_none    parent_none     parent_none Summary  
 O       o646    parent_none  
 T       t646    o646  
 B       b646    t646  
 NSummary!meta_implies   meta_implies    meta_implies Summary  
 O       o671    meta_implies  
 T       t980    o639 b607  
 S       s980    t623 h  
 G       s980    t980  
 B       b980    s980  
 NBase_trivial   Base_trivial    Base_trivial NIL  
 NBase_trivial!squash    squash  squash Base_trivial  
 O       o672    squash  
 T       t672    o672  
 B       b672    t672  
 T       t673    o b672 b4  
 NItt_equal      Itt_equal       Itt_equal NIL  
 NItt_equal!equal        equal707        equal Itt_equal  
 O       o711    equal707  
 NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL  
 NItt_record_label0!label        label   label Itt_record_label0  
 O       o712    label  
 T       t718    o712  
 B       b718    t718  
 T       t719    o711 b718 b605 b605  
 S       s719    t673 h  
 G       s719    t719  
 B       b719    s719  
 T       t720    o621 b719  
 B       b720    t720  
 NCzf_itt_group!group    group   group Czf_itt_group  
 O       o720    group  
 T       t721    o720 b605  
 S       s721    t623 h  
 G       s721    t721  
 B       b721    s721  
 T       t722    o621 b721  
 B       b722    t722  
 P       p673    Var s1  
 O       o673    var p673  
 T       t674    o673  
 B       b674    t674  
 T       t675    o639 b674  
 S       s675    t673 h  
 G       s675    t675  
 B       b675    s675  
 T       t676    o621 b675  
 B       b676    t676  
 P       p676    Var s2  
 O       o676    var p676  
 T       t677    o676  
 B       b677    t677  
 T       t678    o639 b677  
 S       s678    t673 h  
 G       s678    t678  
 B       b678    s678  
 T       t679    o621 b678  
 B       b679    t679  
 NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  
 NCzf_itt_member!mem     mem     mem Czf_itt_member  
 O       o679    mem  
 T       t723    o624 b605  
 B       b723    t723  
 T       t725    o679 b607 b723  
 S       s725    t623 h  
 G       s725    t725  
 B       b725    s725  
 T       t744    o621 b725  
 B       b744    t744  
 P       p880    Number 882  
 O       o900    location p900 p880  
 P       p901    String cyclic_group(  
 O       o901    string610 p901  
 T       t901    o901  
2367  B       b901    t901  B       b901    t901
2368  T       t902    o961 b605  T       t902    o b901 b4
2369  B       b902    t902  B       b902    t902
2370  P       p902    String "; "  T       t903    o737 b678 b779 b902 b4
 O       o902    string610 p902  
 T       t903    o902  
2371  B       b903    t903  B       b903    t903
2372  P       p903    String )  T       t904    o676 b903
2373  O       o903    string610 p903  B       b904    t904
2374  T       t906    o903  T       t905    o727 b730 b737 b904 b4
2375  B       b911    t906  B       b905    t905
2376  T       t911    o b911 b4  T       t273    o271 b905
2377  B       b912    t911  B       b273    t273
2378  T       t912    o b961 b912  P       p282    Number 1791
2379  B       b915    t912  O       o282    location p282 p322
2380  T       t915    o b903 b915  O       o283    str_let p282 p322
2381  B       b940    t915  P       p283    Number 1795
2382  T       t940    o b902 b940  O       o284    patt_var p283 p322
2383  B       b954    t940  O       o285    patt_done p282 p322
2384  T       t954    o b901 b954  T       t287    o285
2385  B       b957    t954  B       b287    t287 cycgroupAbelT
2386  T       t958    o610 b957  T       t292    o284 b287
 B       b958    t958  
 T       t967    o608 b610 b740 b958  
 B       b967    t967  
 T       t968    o900 b967  
 B       b968    t968  
 P       p968    Number 884  
 P       p971    String cycgroup_wf  
 O       o971    rule p971  
 NItt_equal!type type    type Itt_equal  
 O       o972    type  
 T       t972    o972 b740  
 S       s       t623 h  
 G       s       t972  
 B       b972    s  
 T       t973    o621 b972  
 B       b973    t973  
 T       t974    o671 b744 b973  
 B       b974    t974  
 P       p977    String "rwh unfold_cycgroup 0 ttca"  
 O       o977    ext_rule p977  
 T       t978    o b725 b4  
 B       b978    t978  
 T       t983    o b980 b978  
 B       b983    t983  
 T       t984    o b721 b983  
 B       b984    t984  
 T       t985    o b719 b984  
 B       b985    t985  
 T       t986    o645 b972 b985  
 B       b986    t986  
 T       t987    o644 b986 b4 b646  
 B       b987    t987  
 T       t989    o643 b987 b4  
 B       b989    t989  
 T       t990    o977 b642 b989 b4 b4  
 B       b990    t990  
 T       t991    o640 b990  
 B       b991    t991  
 P       p991    Number 911  
 P       p992    Number 919  
 O       o992    resource_defs p991 p992 p288  
 P       p993    Number 917  
 O       o993    uid p993 p992  
 T       t993    o993 b630  
 B       b993    t993  
 T       t994    o b993 b4  
 B       b994    t994  
 T       t999    o992 b994  
 B       b999    t999  
 T       t1000   o b999 b4  
 B       b1000   t1000  
 P       p1002   Number 1161  
 O       o6      location p968 p1002  
 S       s6      t673 h  
 G       s6      t980  
 B       b239    s6  
 T       t239    o621 b239  
 B       b253    t239  
 T       t253    o671 b253 b974  
 B       b254    t253  
 T       t254    o671 b722 b254  
 B       b257    t254  
 T       t257    o671 b720 b257  
 B       b261    t257  
 T       t261    o971 b621 b261 b991 b1000  
 B       b262    t261  
 T       t262    o6 b262  
 B       b263    t262  
 P       p270    Number 1163  
 P       p271    Number 1518  
 O       o271    location p270 p271  
 P       p1004   String cycgroup_intro  
 O       o1004   rule p1004  
 NCzf_itt_group!op       op      op Czf_itt_group  
 O       o683    op  
 NItt_int_base   Itt_int_base    Itt_int_base NIL  
 NItt_int_base!int       int     int Itt_int_base  
 O       o759    int  
 T       t760    o759  
 NCzf_itt_eq!eq  eq      eq Czf_itt_eq  
 O       o760    eq  
 NCzf_itt_cyclic_subgroup!power  power   power Czf_itt_cyclic_subgroup  
 O       o761    power  
 NSummary!arg_named      arg_named       arg_named Summary  
 P       p768    String d_auto  
 O       o768    arg_named p768  
 NSummary!arg_bool       arg_bool        arg_bool Summary  
 P       p769    String true  
 O       o769    arg_bool p769  
 T       t769    o769  
 B       b769    t769  
 T       t770    o768 b769  
 B       b770    t770  
 T       t771    o b770 b4  
 B       b771    t771  
 NItt_logic      Itt_logic       Itt_logic NIL  
 NItt_logic!exists       exists  exists Itt_logic  
 O       o771    exists  
 B       b772    t760  
 P       p772    Var t  
 O       o772    var p772  
 T       t772    o772  
 B       b773    t772  
 NCzf_itt_set!collect    collect collect Czf_itt_set  
 O       o777    collect  
 P       p777    Var x  
 O       o778    var p777  
 T       t778    o778  
 B       b778    t778  
 T       t1008   o761 b605 b607 b778  
 B       b1008   t1008 x  
 T       t1009   o777 b772 b1008  
 B       b1009   t1009  
 T       t1010   o623 b723 b1009  
 S       s1010   t623 h  
 G       s1010   t1010  
 B       b1010   s1010  
 T       t1011   o621 b1010  
 B       b1011   t1011  
 S       s1011   t623 h  
 G       s1011   t740  
 B       b1012   s1011  
 T       t1012   o621 b1012  
 B       b1013   t1012  
 T       t1013   o671 b1011 b1013  
 B       b1016   t1013  
 T       t1016   o671 b744 b1016  
 B       b1017   t1016  
 T       t275    o671 b253 b1017  
 B       b275    t275  
 T       t280    o671 b722 b275  
 B       b280    t280  
 T       t281    o671 b720 b280  
 B       b281    t281  
 T       t1020   o b1010 b4  
 B       b1021   t1020  
 T       t1021   o b725 b1021  
 B       b1024   t1021  
 T       t1024   o b980 b1024  
 B       b1025   t1024  
 T       t1025   o b721 b1025  
 B       b1026   t1025  
 T       t1026   o b719 b1026  
 B       b1027   t1026  
 T       t1027   o645 b1012 b1027  
 B       b1028   t1027  
 T       t1028   o644 b1028 b4 b646  
 B       b1029   t1028  
 T       t1029   o643 b1029 b4  
 B       b1030   t1029  
 T       t1030   o977 b642 b1030 b4 b4  
 B       b1031   t1030  
 T       t1031   o640 b1031  
 B       b1032   t1031  
 P       p284    Number 1193  
 P       p285    Number 1201  
 O       o285    resource_defs p284 p285 p288  
 P       p1033   Number 1199  
 O       o286    uid p1033 p285  
 T       t289    o286 b630  
 B       b289    t289  
 T       t290    o b289 b4  
 B       b290    t290  
 T       t292    o285 b290  
2387  B       b292    t292  B       b292    t292
 T       t297    o b292 b4  
 B       b297    t297  
 T       t298    o1004 b621 b281 b1032 b297  
 B       b298    t298  
 T       t313    o271 b298  
 B       b313    t313  
 P       p318    Number 1556  
 NItt_int_base!add       add     add Itt_int_base  
 O       o840    add  
 NSummary!ext_goal       ext_goal        ext_goal Summary  
 O       o865    ext_goal  
 O       o918    location p p  
 P       p1039   String cycgroup_abel  
 O       o1039   rule p1039  
 T       t929    o683 b605 b674 b677  
 B       b929    t929  
 NSummary!term_param     term_param      term_param Summary  
 O       o1116   term_param  
 T       t1118   o1116 b607  
 B       b1118   t1118  
 T       t1119   o b1118 b4  
 B       b1119   t1119  
 T       t1120   o b620 b1119  
 B       b1120   t1120  
 P       p1040   Var R  
 O       o1040   var p1040  
 T       t1040   o1040  
 B       b1040   t1040  
 T       t1041   o639 b1040  
 S       s1041   t673 h  
 G       s1041   t1041  
 B       b1041   s1041  
 T       t1043   o621 b1041  
 B       b1043   t1043  
 NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL  
 NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv  
 O       o1043   equiv  
 T       t1044   o1043 b723 b1040  
 S       s1044   t623 h  
 G       s1044   t1044  
 B       b1044   s1044  
 T       t1045   o621 b1044  
 B       b1045   t1045  
 T       t1046   o679 b674 b723  
 S       s1046   t623 h  
 G       s1046   t1046  
 B       b1046   s1046  
 T       t1047   o621 b1046  
 B       b1047   t1047  
 T       t1048   o679 b677 b723  
 S       s1048   t623 h  
 G       s1048   t1048  
 B       b1048   s1048  
 T       t1049   o621 b1048  
 B       b1049   t1049  
 T       t1121   o683 b605 b677 b674  
 B       b1121   t1121  
 T       t1050   o1043 b723 b1040 b929 b1121  
 S       s1050   t623 h  
 G       s1050   t1050  
 B       b1050   s1050  
 T       t1051   o621 b1050  
 B       b1051   t1051  
 T       t1052   o671 b1049 b1051  
 B       b1052   t1052  
 T       t1053   o671 b1047 b1052  
 B       b1053   t1053  
 T       t1054   o671 b679 b1053  
 B       b1054   t1054  
 T       t1055   o671 b676 b1054  
 B       b1055   t1055  
 T       t1056   o671 b1013 b1055  
 B       b1056   t1056  
 T       t1057   o671 b744 b1056  
 B       b1057   t1057  
 P       p1062   String "assumT 7 thenT assumT 10 thenT assumT 11 thenT rwh unfold_cycgroup 2 thenT rwh unfold_cyc_subg 2 ttca"  
 O       o1062   ext_rule p1062  
 T       t1063   o b1048 b4  
 B       b1063   t1063  
 T       t1064   o b1046 b1063  
 B       b1064   t1064  
 T       t1065   o b678 b1064  
 B       b1065   t1065  
 T       t1066   o b675 b1065  
 B       b1066   t1066  
 T       t1067   o b1012 b1066  
 B       b1067   t1067  
 T       t1068   o b725 b1067  
 B       b1068   t1068  
 T       t1069   o b980 b1068  
 B       b1069   t1069  
 T       t1070   o b1044 b1069  
 B       b1070   t1070  
 T       t1071   o b721 b1070  
 B       b1071   t1071  
 T       t1073   o b719 b1071  
 B       b1073   t1073  
 T       t1074   o b1041 b1073  
 B       b1074   t1074  
 T       t1075   o645 b1050 b1074  
 B       b1075   t1075  
 T       t1076   o644 b1075 b4 b646  
 B       b1076   t1076  
 NItt_logic!and  and     and Itt_logic  
 O       o1076   and  
 B       b1077   t721  
 B       b1079   t1010  
 NItt_logic!all  all     all Itt_logic  
 O       o1079   all  
 NCzf_itt_set!set        set     set Czf_itt_set  
 O       o1080   set  
 T       t1080   o1080  
 B       b1080   t1080  
 NItt_logic!implies      implies implies Itt_logic  
 O       o1081   implies  
 P       p1081   Var a_1  
 O       o1082   var p1081  
 T       t1082   o1082  
 B       b1082   t1082  
 T       t1083   o679 b1082 b723  
 B       b1083   t1083  
 P       p1083   Var b  
 O       o1083   var p1083  
 T       t1084   o1083  
 B       b1084   t1084  
 T       t1085   o679 b1084 b723  
 B       b1085   t1085  
 T       t1086   o683 b605 b1082 b1084  
 B       b1086   t1086  
 T       t1087   o623 b1086 b1086  
 B       b1087   t1087  
 T       t1089   o1081 b1085 b1087  
 B       b1089   t1089  
 T       t1090   o1081 b1083 b1089  
 B       b1090   t1090 b  
 T       t1091   o1079 b1080 b1090  
 B       b1091   t1091 a_1  
 T       t1092   o1079 b1080 b1091  
 B       b1092   t1092  
 T       t1093   o1076 b1079 b1092  
 B       b1093   t1093  
 T       t1096   o1076 b1077 b1093  
 B       b1096   t1096  
 T       t1098   o1076 b1077 b1096  
 H       h1098   v t1098  
 H       h1099   v_1 t1046  
 H       h1100   v_2 t1048  
 S       s1100   t623 h h1098 h1099 h1100  
 G       s1100   t1050  
 B       b1100   s1100  
 T       t1100   o645 b1100 b1074  
 B       b1101   t1100  
 H       h1101   v t750  
 S       s1101   t623 h h1101 h1099 h1100  
 G       s1101   t1050  
 B       b1102   s1101  
 T       t1102   o645 b1102 b1074  
 B       b1113   t1102  
 H       h1113   v t740  
 S       s1113   t623 h h1113 h1099 h1100  
 G       s1113   t1050  
 B       b1114   s1113  
 T       t1114   o645 b1114 b1074  
 B       b1115   t1114  
 S       s1115   t623 h h1113 h1099  
 G       s1115   t1050  
 B       b1116   s1115  
 T       t1116   o645 b1116 b1074  
 B       b1117   t1116  
 S       s1117   t623 h h1113  
 G       s1117   t1050  
 B       b1122   s1117  
 T       t1122   o645 b1122 b1074  
 B       b1123   t1122  
 T       t1123   o2 b1076  
 B       b1124   t1123  
 T       t1124   o644 b1123 b4 b1124  
 B       b1125   t1124  
 T       t1125   o2 b1125  
 B       b1126   t1125  
 T       t1126   o644 b1117 b4 b1126  
 B       b1127   t1126  
 T       t1127   o2 b1127  
 B       b1128   t1127  
 T       t1128   o644 b1115 b4 b1128  
 B       b1129   t1128  
 T       t1129   o2 b1129  
 B       b1130   t1129  
 T       t1130   o644 b1113 b4 b1130  
 B       b1131   t1130  
 T       t1131   o2 b1131  
 B       b1132   t1131  
 T       t1132   o644 b1101 b4 b1132  
 B       b1133   t1132  
 T       t1133   o b1133 b4  
 B       b1134   t1133  
 T       t1134   o643 b1076 b1134  
 B       b1145   t1134  
 P       p1147   String "dT 2 thenT dT 3 thenT dT 4"  
 O       o1147   ext_rule p1147  
 H       h1147   y t721  
 H       h1148   y_1 t721  
 H       h1149   y_2 t1010  
 H       h1150   z t1092  
 S       s1150   t623 h h1147 h1148 h1149 h1150 h1099 h1100  
 G       s1150   t1050  
 B       b1186   s1150  
 T       t1187   o645 b1186 b1074  
 B       b1187   t1187  
 H       h1187   z_1 t1093  
 S       s1187   t623 h h1147 h1148 h1187 h1099 h1100  
 G       s1187   t1050  
 B       b1188   s1187  
 T       t1188   o645 b1188 b1074  
 B       b1189   t1188  
 H       h1189   z t1096  
 S       s1189   t623 h h1147 h1189 h1099 h1100  
 G       s1189   t1050  
 B       b1190   s1189  
 T       t1190   o645 b1190 b1074  
 B       b1191   t1190  
 T       t1191   o2 b1133  
 B       b1192   t1191  
 T       t1192   o644 b1191 b4 b1192  
 B       b1193   t1192  
 T       t1193   o2 b1193  
 B       b1194   t1193  
 T       t1194   o644 b1189 b4 b1194  
 B       b1195   t1194  
 T       t1195   o2 b1195  
 B       b1196   t1195  
 T       t1196   o644 b1187 b4 b1196  
 B       b1197   t1196  
 T       t1197   o b1197 b4  
 B       b1198   t1197  
 T       t1198   o643 b1133 b1198  
 B       b1199   t1198  
 P       p1199   String "setSubstT << equal{car{'g}; collect{int; x. power{'g; 'a; 'x}}} >> 6 ttca thenT setSubstT << equal{car{'g}; collect{int; x. power{'g; 'a; 'x}}} >> 7 ttca"  
 O       o1199   ext_rule p1199  
 T       t1199   o679 b674 b1009  
 H       h1199   v t1199  
 T       t1200   o679 b677 b1009  
 H       h1200   v_3 t1200  
 S       s1200   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1199 h1200  
 G       s1200   t1050  
 B       b1200   s1200  
 T       t1201   o645 b1200 b1074  
 B       b1201   t1201  
 S       s1201   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1199  
 G       s1201   t1050  
 B       b1202   s1201  
 T       t1202   o645 b1202 b1074  
 B       b1203   t1202  
 T       t1203   o2 b1197  
 B       b1204   t1203  
 T       t1204   o644 b1203 b4 b1204  
 B       b1205   t1204  
 T       t1205   o2 b1205  
 B       b1206   t1205  
 T       t1206   o644 b1201 b4 b1206  
 B       b1207   t1206  
 T       t1207   o b1207 b4  
 B       b1208   t1207  
 T       t1208   o643 b1197 b1208  
 B       b1209   t1208  
 P       p1209   String "rwh reduceC 8 thenT dT 8 thenT rwh reduceC 10 thenT dT 10 ttca"  
 O       o1209   ext_rule p1209  
 H       h1209   y_3 t760  
 P       p1210   Var y_3  
 O       o1210   var p1210  
 T       t1210   o1210  
 B       b1210   t1210  
 T       t1211   o761 b605 b607 b1210  
 B       b1211   t1211  
 T       t1212   o760 b674 b1211  
 H       h1212   z_1 t1212  
 H       h1213   y_4 t760  
 P       p1213   Var y_4  
 O       o1213   var p1213  
 T       t1213   o1213  
 B       b1213   t1213  
 T       t1214   o761 b605 b607 b1213  
 B       b1214   t1214  
 T       t1215   o760 b677 b1214  
 H       h1215   z_2 t1215  
 S       s1215   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1215   t1050  
 B       b1215   s1215  
 T       t1216   o645 b1215 b1074  
 B       b1216   t1216  
 T       t1217   o761 b605 b607 b773  
 B       b1217   t1217  
 T       t1218   o760 b677 b1217  
 B       b1218   t1218 t  
 T       t1219   o771 b772 b1218  
 H       h1219   v_3 t1219  
 S       s1219   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1219  
 G       s1219   t1050  
 B       b1219   s1219  
 T       t1220   o645 b1219 b1074  
 B       b1220   t1220  
 S       s1220   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1200  
 G       s1220   t1050  
 B       b1221   s1220  
 T       t1221   o645 b1221 b1074  
 B       b1222   t1221  
 T       t1222   o760 b674 b1217  
 B       b1223   t1222 t  
 T       t1223   o771 b772 b1223  
 H       h1223   v t1223  
 S       s1223   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1223 h1200  
 G       s1223   t1050  
 B       b1224   s1223  
 T       t1224   o645 b1224 b1074  
 B       b1225   t1224  
 T       t1225   o2 b1207  
 B       b1226   t1225  
 T       t1226   o644 b1225 b4 b1226  
 B       b1227   t1226  
 T       t1227   o2 b1227  
 B       b1228   t1227  
 T       t1228   o644 b1222 b4 b1228  
 B       b1229   t1228  
 T       t1229   o2 b1229  
 B       b1230   t1229  
 T       t1230   o644 b1220 b4 b1230  
 B       b1231   t1230  
 T       t1231   o2 b1231  
 B       b1232   t1231  
 T       t1232   o644 b1216 b4 b1232  
 B       b1233   t1232  
 T       t1233   o b1233 b4  
 B       b1234   t1233  
 T       t1234   o643 b1207 b1234  
 B       b1235   t1234  
 P       p1235   String "setSubstT << equal{'s1; power{'g; 'a; 'y_3}} >> 0 ttca"  
 O       o1235   ext_rule p1235  
 T       t1235   o683 b605 b1211 b677  
 B       b1236   t1235  
 T       t1236   o683 b605 b677 b1211  
 B       b1237   t1236  
 T       t1237   o1043 b723 b1040 b1236 b1237  
 S       s1237   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1237   t1237  
 B       b1238   s1237  
 T       t1238   o645 b1238 b1074  
 B       b1239   t1238  
 T       t1239   o2 b1233  
 B       b1240   t1239  
 T       t1240   o644 b1239 b4 b1240  
 B       b1241   t1240  
 P       p1241   String wf  
 O       o1241   tactic_arg p1241  
 NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq  
 O       o1242   fun_prop  
 P       p1242   Var v  
 O       o1243   var p1242  
 T       t1243   o1243  
 B       b1243   t1243  
 T       t1244   o683 b605 b1243 b677  
 B       b1244   t1244  
 T       t1245   o683 b605 b677 b1243  
 B       b1245   t1245  
 T       t1246   o1043 b723 b1040 b1244 b1245  
 B       b1246   t1246 v  
 T       t1247   o1242 b1246  
 S       s1247   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1247   t1247  
 B       b1247   s1247  
 T       t1248   o645 b1247 b1074  
 B       b1248   t1248  
 T       t1249   o1241 b1248 b4 b1240  
 B       b1249   t1249  
 T       t1250   o b1249 b4  
 B       b1250   t1250  
 T       t1251   o b1241 b1250  
 B       b1251   t1251  
 T       t1252   o643 b1233 b1251  
 B       b1252   t1252  
 P       p1252   String "setSubstT << equal{'s2; power{'g; 'a; 'y_4}} >> 0 ttca"  
 O       o1252   ext_rule p1252  
 T       t1253   o683 b605 b1211 b1214  
 B       b1253   t1253  
 T       t1254   o683 b605 b1214 b1211  
 B       b1254   t1254  
 T       t1255   o1043 b723 b1040 b1253 b1254  
 S       s1255   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1255   t1255  
 B       b1255   s1255  
 T       t1256   o645 b1255 b1074  
 B       b1256   t1256  
 T       t1257   o2 b1241  
 B       b1257   t1257  
 T       t1258   o644 b1256 b4 b1257  
 B       b1258   t1258  
 T       t1259   o683 b605 b1211 b1243  
 B       b1259   t1259  
 T       t1260   o683 b605 b1243 b1211  
 B       b1260   t1260  
 T       t1261   o1043 b723 b1040 b1259 b1260  
 B       b1261   t1261 v  
 T       t1262   o1242 b1261  
 S       s1262   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1262   t1262  
 B       b1262   s1262  
 T       t1263   o645 b1262 b1074  
 B       b1263   t1263  
 T       t1264   o1241 b1263 b4 b1257  
 B       b1264   t1264  
 T       t1265   o b1264 b4  
 B       b1265   t1265  
 T       t1266   o b1258 b1265  
 B       b1266   t1266  
 T       t1267   o643 b1241 b1266  
 B       b1267   t1267  
 P       p1267   String "equivSubstT << equiv{car{'g}; 'R; op{'g; power{'g; 'a; 'y_3}; power{'g; 'a; 'y_4}}; power{'g; 'a; ('y_3 +@ 'y_4)}} >> 0 ttca"  
 O       o1267   ext_rule p1267  
 T       t1268   o840 b1210 b1213  
 B       b1268   t1268  
 T       t1269   o761 b605 b607 b1268  
 B       b1269   t1269  
 T       t1270   o1043 b723 b1040 b1269 b1254  
 S       s1270   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1270   t1270  
 B       b1270   s1270  
 T       t1271   o645 b1270 b1074  
 B       b1271   t1271  
 T       t1272   o2 b1258  
 B       b1272   t1272  
 T       t1273   o644 b1271 b4 b1272  
 B       b1273   t1273  
 T       t1274   o b1273 b4  
 B       b1274   t1274  
 T       t1275   o643 b1258 b1274  
 B       b1275   t1275  
 P       p1275   String "rwh add_CommutC 0 ttca"  
 O       o1275   ext_rule p1275  
 T       t1276   o840 b1213 b1210  
 B       b1276   t1276  
 T       t1277   o761 b605 b607 b1276  
 B       b1277   t1277  
 T       t1278   o1043 b723 b1040 b1277 b1254  
 S       s1278   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1278   t1278  
 B       b1278   s1278  
 T       t1279   o645 b1278 b1074  
 B       b1279   t1279  
 T       t1280   o2 b1273  
 B       b1280   t1280  
 T       t1281   o644 b1279 b4 b1280  
 B       b1281   t1281  
 T       t1282   o b1281 b4  
 B       b1282   t1282  
 T       t1283   o643 b1273 b1282  
 B       b1283   t1283  
 P       p1283   String "equivSym1T ttca"  
 O       o1283   ext_rule p1283  
 T       t1284   o643 b1281 b4  
 B       b1284   t1284  
 T       t1285   o1283 b642 b1284 b4 b4  
 B       b1285   t1285  
 T       t1286   o b1285 b4  
 B       b1286   t1286  
 T       t1287   o1043 b723 b1040 b1269 b1277  
 S       s1287   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1287   t1287  
 B       b1287   s1287  
 T       t1288   o645 b1287 b1074  
 B       b1288   t1288  
 T       t1289   o644 b1288 b4 b1280  
 B       b1289   t1289  
 T       t1290   o1043 b723 b1040 b1277 b1269  
 S       s1290   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1290   t1290  
 B       b1290   s1290  
 T       t1291   o645 b1290 b1074  
 B       b1291   t1291  
 T       t1292   o2 b1289  
 B       b1292   t1292  
 T       t1293   o644 b1291 b4 b1292  
 B       b1293   t1293  
 T       t1294   o b1293 b4  
 B       b1294   t1294  
 T       t1295   o643 b1289 b1294  
 B       b1295   t1295  
 T       t1296   o865 b1293  
 B       b1296   t1296  
 T       t1297   o b1296 b4  
 B       b1297   t1297  
 T       t1298   o1275 b642 b1295 b1297 b4  
 B       b1298   t1298  
 T       t1299   o b1298 b4  
 B       b1299   t1299  
 T       t1300   o1275 b642 b1283 b1286 b1299  
 B       b1300   t1300  
 T       t1301   o b1300 b4  
 B       b1301   t1301  
 T       t1302   o1267 b642 b1275 b1301 b4  
 B       b1302   t1302  
 P       p1302   String "rwh unfold_fun_prop 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"  
 O       o1302   ext_rule p1302  
 H       h1302   s1 t1080  
 H       h1303   s2 t1080  
 T       t1303   o623 b674 b677  
 H       h1304   x t1303  
 T       t1304   o683 b605 b1211 b674  
 B       b1304   t1304  
 T       t1305   o683 b605 b674 b1211  
 B       b1305   t1305  
 T       t1306   o1043 b723 b1040 b1304 b1305  
 H       h1306   x_1 t1306  
 S       s1306   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302 h1303 h1304 h1306  
 G       s1306   t1237  
 B       b1306   s1306  
 T       t1307   o645 b1306 b1074  
 B       b1307   t1307  
 B       b1308   t1306  
 B       b1309   t1237  
 T       t1309   o1081 b1308 b1309  
 S       s1309   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302 h1303 h1304  
 G       s1309   t1309  
 B       b1310   s1309  
 T       t1310   o645 b1310 b1074  
 B       b1311   t1310  
 B       b1312   t1303  
 B       b1313   t1309  
 T       t1313   o1081 b1312 b1313  
 S       s1313   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302 h1303  
 G       s1313   t1313  
 B       b1314   s1313  
 T       t1314   o645 b1314 b1074  
 B       b1315   t1314  
 B       b1316   t1313 s2  
 T       t1316   o1079 b1080 b1316  
 S       s1316   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302  
 G       s1316   t1316  
 B       b1317   s1316  
 T       t1317   o645 b1317 b1074  
 B       b1318   t1317  
 B       b1319   t1316 s1  
 T       t1319   o1079 b1080 b1319  
 S       s1319   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1319   t1319  
 B       b1320   s1319  
 T       t1320   o645 b1320 b1074  
 B       b1321   t1320  
 T       t1321   o2 b1264  
 B       b1322   t1321  
 T       t1322   o1241 b1321 b4 b1322  
 B       b1323   t1322  
 T       t1323   o2 b1323  
 B       b1324   t1323  
 T       t1324   o644 b1318 b4 b1324  
 B       b1325   t1324  
 T       t1325   o2 b1325  
 B       b1326   t1325  
 T       t1326   o644 b1315 b4 b1326  
 B       b1327   t1326  
 T       t1327   o2 b1327  
 B       b1328   t1327  
 T       t1328   o644 b1311 b4 b1328  
 B       b1329   t1328  
 T       t1329   o2 b1329  
 B       b1330   t1329  
 T       t1330   o644 b1307 b4 b1330  
 B       b1331   t1330  
 T       t1331   o b1331 b4  
 B       b1332   t1331  
 T       t1332   o643 b1264 b1332  
 B       b1333   t1332  
 P       p1333   String "equivTransT << op{'g; power{'g; 'a; 'y_3}; 's2} >> 15 ttca"  
 O       o1333   ext_rule p1333  
 T       t1333   o1043 b723 b1040 b1304 b1236  
 H       h1333   u t1333  
 T       t1334   o1043 b723 b1040 b1236 b1305  
 H       h1334   v t1334  
 S       s1334   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302 h1303 h1304 h1306 h1333 h1334  
 G       s1334   t1237  
 B       b1334   s1334  
 T       t1335   o645 b1334 b1074  
 B       b1335   t1335  
 T       t1336   o2 b1331  
 B       b1336   t1336  
 T       t1337   o644 b1335 b4 b1336  
 B       b1337   t1337  
 T       t1338   o b1337 b4  
 B       b1338   t1338  
 T       t1339   o643 b1331 b1338  
 B       b1339   t1339  
 P       p1339   String "equivTransT << op{'g; 's2; power{'g; 'a; 'y_3}} >> 17 ttca"  
 O       o1339   ext_rule p1339  
 T       t1340   o643 b1337 b4  
 B       b1340   t1340  
 T       t1341   o1339 b642 b1340 b4 b4  
 B       b1341   t1341  
 T       t1342   o b1341 b4  
 B       b1342   t1342  
 T       t1343   o1333 b642 b1339 b1342 b4  
 B       b1343   t1343  
 T       t1344   o b1343 b4  
 B       b1344   t1344  
 T       t1345   o1302 b642 b1333 b1344 b4  
 B       b1345   t1345  
 T       t1346   o b1345 b4  
 B       b1346   t1346  
 T       t1347   o b1302 b1346  
 B       b1347   t1347  
 T       t1348   o1252 b642 b1267 b1347 b4  
 B       b1348   t1348  
 H       h1348   s2_1 t1080  
 P       p1348   Var s2_1  
 O       o1348   var p1348  
 T       t1349   o1348  
 B       b1349   t1349  
 T       t1350   o623 b674 b1349  
 H       h1350   x t1350  
 H       h1351   x_1 t1050  
 T       t1351   o683 b605 b1349 b677  
 B       b1351   t1351  
 T       t1352   o683 b605 b677 b1349  
 B       b1352   t1352  
 T       t1353   o1043 b723 b1040 b1351 b1352  
 S       s1353   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302 h1348 h1350 h1351  
 G       s1353   t1353  
 B       b1353   s1353  
 T       t1354   o645 b1353 b1074  
 B       b1354   t1354  
 B       b1355   t1050  
 B       b1356   t1353  
 T       t1356   o1081 b1355 b1356  
 S       s1356   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302 h1348 h1350  
 G       s1356   t1356  
 B       b1357   s1356  
 T       t1357   o645 b1357 b1074  
 B       b1358   t1357  
 B       b1359   t1350  
 B       b1360   t1356  
 T       t1360   o1081 b1359 b1360  
 S       s1360   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302 h1348  
 G       s1360   t1360  
 B       b1361   s1360  
 T       t1361   o645 b1361 b1074  
 B       b1362   t1361  
 B       b1363   t1360 s2_1  
 T       t1363   o1079 b1080 b1363  
 S       s1363   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215 h1302  
 G       s1363   t1363  
 B       b1364   s1363  
 T       t1364   o645 b1364 b1074  
 B       b1365   t1364  
 B       b1366   t1363 s1  
 T       t1366   o1079 b1080 b1366  
 S       s1366   t623 h h1147 h1148 h1149 h1150 h1099 h1100 h1209 h1212 h1213 h1215  
 G       s1366   t1366  
 B       b1367   s1366  
 T       t1367   o645 b1367 b1074  
 B       b1368   t1367  
 T       t1368   o2 b1249  
 B       b1369   t1368  
 T       t1369   o1241 b1368 b4 b1369  
 B       b1370   t1369  
 T       t1370   o2 b1370  
 B       b1371   t1370  
 T       t1371   o644 b1365 b4 b1371  
 B       b1372   t1371  
 T       t1372   o2 b1372  
 B       b1373   t1372  
 T       t1373   o644 b1362 b4 b1373  
 B       b1374   t1373  
 T       t1374   o2 b1374  
 B       b1375   t1374  
 T       t1375   o644 b1358 b4 b1375  
 B       b1376   t1375  
 T       t1376   o2 b1376  
 B       b1377   t1376