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

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

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

revision 3494 by xiny, Thu Feb 7 23:19:33 2002 UTC revision 3498 by xiny, Sun Feb 17 02:09:08 2002 UTC
# Line 5  Line 5 
5  NSummary        Summary Summary NIL  NSummary        Summary Summary NIL
6  NSummary!location       location        location Summary  NSummary!location       location        location Summary
7  P       p       Number 0  P       p       Number 0
8  P       p1      Number 19  P       p1      Number 25
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       p2      String Czf_itt_set  P       p2      String Itt_record_label0
13  O       o3      parent p2  O       o3      parent p2
14  T       t       o3  T       t       o3
15  B       b       t  B       b       t
# Line 19  Line 19 
19  B       b4      t4  B       b4      t4
20  T       t5      o b b4  T       t5      o b b4
21  B       b5      t5  B       b5      t5
22  P       p5      String Czf_itt_comment  P       p5      String Itt_nat
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 Itt_theory  P       p7      String Itt_int_ext
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 Itt_fset  P       p9      String Itt_int_base
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 Itt_prop_decide  P       p11     String Itt_bool
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 Itt_derive  P       p13     String Itt_decidable
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 Itt_list2  P       p15     String Itt_logic
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 Itt_list  P       p17     String Itt_union
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 Itt_quotient  P       p19     String Itt_prod
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 Itt_esquash  P       p21     String Itt_dprod
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_srec  P       p23     String Itt_fun
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_prec  P       p25     String Itt_dfun
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_w  P       p27     String Itt_rfun
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_bunion  P       p29     String Itt_void
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_bisect  P       p31     String Itt_set
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_tunion  P       p33     String Itt_unit
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_isect  P       p35     String Itt_squiggle
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_struct2  P       p37     String Itt_subtype
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_well_founded  P       p39     String Itt_squash
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_int_arith  P       p41     String Itt_struct
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_int_ext  P       p43     String Itt_equal
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_int_base  P       p45     String Itt_comment
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_atom_bool  P       p47     String Base_theory
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_atom  P       p49     String Base_meta
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_bool  P       p51     String Base_cache
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_decidable  P       p53     String Tactic_cache
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_logic  P       p55     String Typeinf
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_prod  P       p57     String Ocaml_df
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_dprod  P       p59     String Ocaml_str_df
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_fun  P       p61     String Ocaml_sig_df
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_dfun  P       p63     String Ocaml_me_df
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_rfun  P       p65     String Ocaml_mt_df
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       p67     String Itt_set  P       p67     String Ocaml_type_df
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_unit  P       p69     String Ocaml_patt_df
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_squiggle  P       p71     String Ocaml_expr_df
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_squash  P       p73     String Ocaml_base_df
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_union  P       p75     String Ocaml
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_void  P       p77     String Base_rewrite
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_subtype  P       p79     String Base_dtactic
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_struct  P       p81     String Base_auto_tactic
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_equal  P       p83     String Base_trivial
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_comment  P       p85     String Top_conversionals
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 Base_theory  P       p87     String Top_tacticals
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 Base_meta  P       p89     String Var
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 Base_cache  P       p91     String Mptop
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 Tactic_cache  P       p93     String Summary
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 Typeinf  P       p95     String Comment
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 Ocaml_df  P       p97     String Base_dform
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 Ocaml_str_df  P       p99     String Nuprl_font
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 Ocaml_sig_df  P       p101    String Perv
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 Ocaml_me_df  T       t104    o b103 b4
 O       o103    parent p103  
 T       t104    o103  
317  B       b104    t104  B       b104    t104
318  T       t105    o b104 b4  T       t105    o b101 b104
319  B       b105    t105  B       b105    t105
320  P       p105    String Ocaml_mt_df  T       t106    o b99 b105
 O       o105    parent p105  
 T       t106    o105  
321  B       b106    t106  B       b106    t106
322  T       t107    o b106 b4  T       t107    o b97 b106
323  B       b107    t107  B       b107    t107
324  P       p107    String Ocaml_type_df  T       t108    o b95 b107
 O       o107    parent p107  
 T       t108    o107  
325  B       b108    t108  B       b108    t108
326  T       t109    o b108 b4  T       t109    o b93 b108
327  B       b109    t109  B       b109    t109
328  P       p109    String Ocaml_patt_df  T       t110    o b91 b109
 O       o109    parent p109  
 T       t110    o109  
329  B       b110    t110  B       b110    t110
330  T       t111    o b110 b4  T       t111    o b89 b110
331  B       b111    t111  B       b111    t111
332  P       p111    String Ocaml_expr_df  T       t112    o b87 b111
 O       o111    parent p111  
 T       t112    o111  
333  B       b112    t112  B       b112    t112
334  T       t113    o b112 b4  T       t113    o b85 b112
335  B       b113    t113  B       b113    t113
336  P       p113    String Ocaml_base_df  T       t114    o b83 b113
 O       o113    parent p113  
 T       t114    o113  
337  B       b114    t114  B       b114    t114
338  T       t115    o b114 b4  T       t115    o b81 b114
339  B       b115    t115  B       b115    t115
340  P       p115    String Ocaml  T       t116    o b79 b115
 O       o115    parent p115  
 T       t116    o115  
341  B       b116    t116  B       b116    t116
342  T       t117    o b116 b4  T       t117    o b77 b116
343  B       b117    t117  B       b117    t117
344  P       p117    String Base_rewrite  T       t118    o b75 b117
 O       o117    parent p117  
 T       t118    o117  
345  B       b118    t118  B       b118    t118
346  T       t119    o b118 b4  T       t119    o b73 b118
347  B       b119    t119  B       b119    t119
348  P       p119    String Base_dtactic  T       t120    o b71 b119
 O       o119    parent p119  
 T       t120    o119  
349  B       b120    t120  B       b120    t120
350  T       t121    o b120 b4  T       t121    o b69 b120
351  B       b121    t121  B       b121    t121
352  P       p121    String Base_auto_tactic  T       t122    o b67 b121
 O       o121    parent p121  
 T       t122    o121  
353  B       b122    t122  B       b122    t122
354  T       t123    o b122 b4  T       t123    o b65 b122
355  B       b123    t123  B       b123    t123
356  P       p123    String Base_trivial  T       t124    o b63 b123
 O       o123    parent p123  
 T       t124    o123  
357  B       b124    t124  B       b124    t124
358  T       t125    o b124 b4  T       t125    o b61 b124
359  B       b125    t125  B       b125    t125
360  P       p125    String Top_conversionals  T       t126    o b59 b125
 O       o125    parent p125  
 T       t126    o125  
361  B       b126    t126  B       b126    t126
362  T       t127    o b126 b4  T       t127    o b57 b126
363  B       b127    t127  B       b127    t127
364  P       p127    String Top_tacticals  T       t128    o b55 b127
 O       o127    parent p127  
 T       t128    o127  
365  B       b128    t128  B       b128    t128
366  T       t129    o b128 b4  T       t129    o b53 b128
367  B       b129    t129  B       b129    t129
368  P       p129    String Var  T       t130    o b51 b129
 O       o129    parent p129  
 T       t130    o129  
369  B       b130    t130  B       b130    t130
370  T       t131    o b130 b4  T       t131    o b49 b130
371  B       b131    t131  B       b131    t131
372  P       p131    String Mptop  T       t132    o b47 b131
 O       o131    parent p131  
 T       t132    o131  
373  B       b132    t132  B       b132    t132
374  T       t133    o b132 b4  T       t133    o b45 b132
375  B       b133    t133  B       b133    t133
376  P       p133    String Summary  T       t134    o b43 b133
 O       o133    parent p133  
 T       t134    o133  
377  B       b134    t134  B       b134    t134
378  T       t135    o b134 b4  T       t135    o b41 b134
379  B       b135    t135  B       b135    t135
380  P       p135    String Comment  T       t136    o b39 b135
 O       o135    parent p135  
 T       t136    o135  
381  B       b136    t136  B       b136    t136
382  T       t137    o b136 b4  T       t137    o b37 b136
383  B       b137    t137  B       b137    t137
384  P       p137    String Base_dform  T       t138    o b35 b137
 O       o137    parent p137  
 T       t138    o137  
385  B       b138    t138  B       b138    t138
386  T       t139    o b138 b4  T       t139    o b33 b138
387  B       b139    t139  B       b139    t139
388  P       p139    String Nuprl_font  T       t140    o b31 b139
 O       o139    parent p139  
 T       t140    o139  
389  B       b140    t140  B       b140    t140
390  T       t141    o b140 b4  T       t141    o b29 b140
391  B       b141    t141  B       b141    t141
392  P       p141    String Perv  T       t142    o b27 b141
 O       o141    parent p141  
 T       t142    o141  
393  B       b142    t142  B       b142    t142
394  T       t143    o b142 b4  T       t143    o b25 b142
395  B       b143    t143  B       b143    t143
396  T       t144    o b143 b4  T       t144    o b23 b143
397  B       b144    t144  B       b144    t144
398  T       t145    o b141 b144  T       t145    o b21 b144
399  B       b145    t145  B       b145    t145
400  T       t146    o b139 b145  T       t146    o b19 b145
401  B       b146    t146  B       b146    t146
402  T       t147    o b137 b146  T       t147    o b17 b146
403  B       b147    t147  B       b147    t147
404  T       t148    o b135 b147  T       t148    o b15 b147
405  B       b148    t148  B       b148    t148
406  T       t149    o b133 b148  T       t149    o b13 b148
407  B       b149    t149  B       b149    t149
408  T       t150    o b131 b149  T       t150    o b11 b149
409  B       b150    t150  B       b150    t150
410  T       t151    o b129 b150  T       t151    o b9 b150
411  B       b151    t151  B       b151    t151
412  T       t152    o b127 b151  T       t152    o b7 b151
413  B       b152    t152  B       b152    t152
414  T       t153    o b125 b152  T       t153    o b5 b152
415  B       b153    t153  B       b153    t153
416  T       t154    o b123 b153  NSummary!resource       resource        resource Summary
417  B       b154    t154  P       p153    String auto
418  T       t155    o b121 b154  O       o153    resource p153
419  B       b155    t155  NOcaml  Ocaml   Ocaml NIL
420  T       t156    o b119 b155  NOcaml!type_lid type_lid        type_lid Ocaml
421    P       p154    Number 2332
422    P       p155    Number 2341
423    O       o155    type_lid p154 p155
424    P       p156    String auto_info
425    O       o156    type_lid p156
426    T       t156    o156
427  B       b156    t156  B       b156    t156
428  T       t157    o b117 b156  T       t157    o155 b156
429  B       b157    t157  B       b157    t157
430  T       t158    o b115 b157  NOcaml!type_prod        type_prod       type_prod Ocaml
431  B       b158    t158  P       p157    Number 2343
432  T       t159    o b113 b158  P       p158    Number 2367
433  B       b159    t159  O       o158    type_prod p157 p158
434  T       t160    o b111 b159  P       p159    Number 2349
435    O       o159    type_lid p157 p159
436    P       p160    String tactic
437    O       o160    type_lid p160
438    T       t160    o160
439  B       b160    t160  B       b160    t160
440  T       t161    o b109 b160  T       t161    o159 b160
441  B       b161    t161  B       b161    t161
442  T       t162    o b107 b161  P       p161    Number 2352
443    P       p162    Number 2358
444    O       o162    type_lid p161 p162
445    T       t162    o162 b160
446  B       b162    t162  B       b162    t162
447  T       t163    o b105 b162  P       p163    Number 2361
448    O       o163    type_lid p163 p158
449    T       t163    o163 b160
450  B       b163    t163  B       b163    t163
451  T       t164    o b103 b163  T       t164    o b163 b4
452  B       b164    t164  B       b164    t164
453  T       t165    o b101 b164  T       t165    o b162 b164
454  B       b165    t165  B       b165    t165
455  T       t166    o b99 b165  T       t166    o b161 b165
456  B       b166    t166  B       b166    t166
457  T       t167    o b97 b166  T       t167    o158 b166
458  B       b167    t167  B       b167    t167
459  T       t168    o b95 b167  T       t168    o153 b157 b167
460  B       b168    t168  B       b168    t168
461  T       t169    o b93 b168  P       p168    String cache
462  B       b169    t169  O       o168    resource p168
463  T       t170    o b91 b169  P       p169    Number 1424
464  B       b170    t170  P       p170    Number 1434
465  T       t171    o b89 b170  O       o170    type_lid p169 p170
466    P       p171    String cache_rule
467    O       o171    type_lid p171
468    T       t171    o171
469  B       b171    t171  B       b171    t171
470  T       t172    o b87 b171  T       t172    o170 b171
471  B       b172    t172  B       b172    t172
472  T       t173    o b85 b172  P       p172    Number 1436
473  B       b173    t173  P       p173    Number 1441
474  T       t174    o b83 b173  O       o173    type_lid p172 p173
475    O       o174    type_lid p168
476    T       t174    o174
477  B       b174    t174  B       b174    t174
478  T       t175    o b81 b174  T       t175    o173 b174
479  B       b175    t175  B       b175    t175
480  T       t176    o b79 b175  T       t176    o168 b172 b175
481  B       b176    t176  B       b176    t176
482  T       t177    o b77 b176  P       p176    String elim
483  B       b177    t177  O       o176    resource p176
484  T       t178    o b75 b177  P       p177    Number 1761
485  B       b178    t178  P       p178    Number 1783
486  T       t179    o b73 b178  O       o178    type_prod p177 p178
487  B       b179    t179  P       p179    Number 1765
488  T       t180    o b71 b179  O       o179    type_lid p177 p179
489    P       p180    String term
490    O       o180    type_lid p180
491    T       t180    o180
492  B       b180    t180  B       b180    t180
493  T       t181    o b69 b180  T       t181    o179 b180
494  B       b181    t181  B       b181    t181
495  T       t182    o b67 b181  NOcaml!type_fun type_fun        type_fun Ocaml
496  B       b182    t182  P       p181    Number 1769
497  T       t183    o b65 b182  P       p182    Number 1782
498  B       b183    t183  O       o182    type_fun p181 p182
499  T       t184    o b63 b183  P       p183    Number 1772
500    O       o183    type_lid p181 p183
501    P       p184    String int
502    O       o184    type_lid p184
503    T       t184    o184
504  B       b184    t184  B       b184    t184
505  T       t185    o b61 b184  T       t185    o183 b184
506  B       b185    t185  B       b185    t185
507  T       t186    o b59 b185  P       p185    Number 1776
508    O       o185    type_lid p185 p182
509    T       t186    o185 b160
510  B       b186    t186  B       b186    t186
511  T       t187    o b57 b186  T       t187    o182 b185 b186
512  B       b187    t187  B       b187    t187
513  T       t188    o b55 b187  T       t188    o b187 b4
514  B       b188    t188  B       b188    t188
515  T       t189    o b53 b188  T       t189    o b181 b188
516  B       b189    t189  B       b189    t189
517  T       t190    o b51 b189  T       t190    o178 b189
518  B       b190    t190  B       b190    t190
519  T       t191    o b49 b190  P       p190    Number 1785
520  B       b191    t191  P       p191    Number 1798
521  T       t192    o b47 b191  O       o191    type_fun p190 p191
522    P       p192    Number 1788
523    O       o192    type_lid p190 p192
524    T       t192    o192 b184
525  B       b192    t192  B       b192    t192
526  T       t193    o b45 b192  P       p193    Number 1792
527    O       o193    type_lid p193 p191
528    T       t193    o193 b160
529  B       b193    t193  B       b193    t193
530  T       t194    o b43 b193  T       t194    o191 b192 b193
531  B       b194    t194  B       b194    t194
532  T       t195    o b41 b194  T       t195    o176 b190 b194
533  B       b195    t195  B       b195    t195
534  T       t196    o b39 b195  P       p195    String eqcd
535  B       b196    t196  O       o195    resource p195
536  T       t197    o b37 b196  P       p196    Number 6168
537  B       b197    t197  P       p197    Number 6181
538  T       t198    o b35 b197  O       o197    type_prod p196 p197
539    P       p198    Number 6172
540    O       o198    type_lid p196 p198
541    T       t198    o198 b180
542  B       b198    t198  B       b198    t198
543  T       t199    o b33 b198  P       p199    Number 6175
544    O       o199    type_lid p199 p197
545    T       t199    o199 b160
546  B       b199    t199  B       b199    t199
547  T       t200    o b31 b199  T       t200    o b199 b4
548  B       b200    t200  B       b200    t200
549  T       t201    o b29 b200  T       t201    o b198 b200
550  B       b201    t201  B       b201    t201
551  T       t202    o b27 b201  T       t202    o197 b201
552  B       b202    t202  B       b202    t202
553  T       t203    o b25 b202  P       p202    Number 6183
554    P       p203    Number 6189
555    O       o203    type_lid p202 p203
556    T       t203    o203 b160
557  B       b203    t203  B       b203    t203
558  T       t204    o b23 b203  T       t204    o195 b202 b203
559  B       b204    t204  B       b204    t204
560  T       t205    o b21 b204  P       p204    String intro
561  B       b205    t205  O       o204    resource p204
562  T       t206    o b19 b205  P       p205    Number 1815
563  B       b206    t206  P       p206    Number 1852
564  T       t207    o b17 b206  O       o206    type_prod p205 p206
565    P       p207    Number 1819
566    O       o207    type_lid p205 p207
567    T       t207    o207 b180
568  B       b207    t207  B       b207    t207
569  T       t208    o b15 b207  P       p208    Number 1823
570  B       b208    t208  P       p209    Number 1851
571  T       t209    o b13 b208  O       o209    type_prod p208 p209
572  B       b209    t209  P       p210    Number 1829
573  T       t210    o b11 b209  O       o210    type_lid p208 p210
574  B       b210    t210  P       p211    String string
575  T       t211    o b9 b210  O       o211    type_lid p211
576    T       t211    o211
577  B       b211    t211  B       b211    t211
578  T       t212    o b7 b211  T       t212    o210 b211
579  B       b212    t212  B       b212    t212
580  T       t213    o b5 b212  NOcaml!type_apply       type_apply      type_apply Ocaml
581  B       b213    t213  P       p212    Number 1832
582  NSummary!resource       resource        resource Summary  P       p213    Number 1842
583  P       p213    String auto  O       o213    type_apply p212 p213
584  O       o213    resource p213  P       p214    Number 1836
585  NOcaml  Ocaml   Ocaml NIL  O       o214    type_lid p214 p213
586  NOcaml!type_lid type_lid        type_lid Ocaml  P       p215    String option
587  P       p214    Number 2332  O       o215    type_lid p215
588  P       p215    Number 2341  T       t215    o215
589  O       o215    type_lid p214 p215  B       b215    t215
590  P       p216    String auto_info  T       t216    o214 b215
 O       o216    type_lid p216  
 T       t216    o216  
591  B       b216    t216  B       b216    t216
592  T       t217    o215 b216  P       p216    Number 1835
593    O       o216    type_lid p212 p216
594    T       t217    o216 b184
595  B       b217    t217  B       b217    t217
596  NOcaml!type_prod        type_prod       type_prod Ocaml  T       t218    o213 b216 b217
597  P       p217    Number 2343  B       b218    t218
598  P       p218    Number 2367  P       p218    Number 1845
599  O       o218    type_prod p217 p218  O       o218    type_lid p218 p209
600  P       p219    Number 2349  T       t219    o218 b160
601  O       o219    type_lid p217 p219  B       b219    t219
602  P       p220    String tactic  T       t220    o b219 b4
 O       o220    type_lid p220  
 T       t220    o220  
603  B       b220    t220  B       b220    t220
604  T       t221    o219 b220  T       t221    o b218 b220
605  B       b221    t221  B       b221    t221
606  P       p221    Number 2352  T       t222    o b212 b221
 P       p222    Number 2358  
 O       o222    type_lid p221 p222  
 T       t222    o222 b220  
607  B       b222    t222  B       b222    t222
608  P       p223    Number 2361  T       t223    o209 b222
 O       o223    type_lid p223 p218  
 T       t223    o223 b220  
609  B       b223    t223  B       b223    t223
610  T       t224    o b223 b4  T       t224    o b223 b4
611  B       b224    t224  B       b224    t224
612  T       t225    o b222 b224  T       t225    o b207 b224
613  B       b225    t225  B       b225    t225
614  T       t226    o b221 b225  T       t226    o206 b225
615  B       b226    t226  B       b226    t226
616  T       t227    o218 b226  P       p226    Number 1854
617    P       p227    Number 1860
618    O       o227    type_lid p226 p227
619    T       t227    o227 b160
620  B       b227    t227  B       b227    t227
621  T       t228    o213 b217 b227  T       t228    o204 b226 b227
622  B       b228    t228  B       b228    t228
623  P       p228    String cache  P       p228    String reduce
624  O       o228    resource p228  O       o228    resource p228
625  P       p229    Number 1424  P       p229    Number 2920
626  P       p230    Number 1434  P       p230    Number 2931
627  O       o230    type_lid p229 p230  O       o230    type_prod p229 p230
628  P       p231    String cache_rule  P       p231    Number 2924
629  O       o231    type_lid p231  O       o231    type_lid p229 p231
630  T       t231    o231  T       t231    o231 b180
631  B       b231    t231  B       b231    t231
632  T       t232    o230 b231  P       p232    Number 2927
633  B       b232    t232  O       o232    type_lid p232 p230
634  P       p232    Number 1436  P       p233    String conv
635  P       p233    Number 1441  O       o233    type_lid p233
636  O       o233    type_lid p232 p233  T       t233    o233
637  O       o234    type_lid p228  B       b233    t233
638  T       t234    o234  T       t234    o232 b233
639  B       b234    t234  B       b234    t234
640  T       t235    o233 b234  T       t235    o b234 b4
641  B       b235    t235  B       b235    t235
642  T       t236    o228 b232 b235  T       t236    o b231 b235
643  B       b236    t236  B       b236    t236
644  P       p236    String elim  T       t237    o230 b236
645  O       o236    resource p236  B       b237    t237
646  P       p237    Number 1761  P       p237    Number 2933
647  P       p238    Number 1783  P       p238    Number 2937
648  O       o238    type_prod p237 p238  O       o238    type_lid p237 p238
649  P       p239    Number 1765  T       t238    o238 b233
650  O       o239    type_lid p237 p239  B       b238    t238
651  P       p240    String term  T       t239    o228 b237 b238
652  O       o240    type_lid p240  B       b239    t239
653  T       t240    o240  P       p239    String squash
654  B       b240    t240  O       o239    resource p239
655  T       t241    o239 b240  P       p240    Number 4017
656  B       b241    t241  P       p241    Number 4028
657  NOcaml!type_fun type_fun        type_fun Ocaml  O       o241    type_lid p240 p241
658  P       p241    Number 1769  P       p242    String squash_info
659  P       p242    Number 1782  O       o242    type_lid p242
660  O       o242    type_fun p241 p242  T       t242    o242
661  P       p243    Number 1772  B       b242    t242
662  O       o243    type_lid p241 p243  T       t243    o241 b242
663  P       p244    String int  B       b243    t243
664  O       o244    type_lid p244  P       p243    Number 4030
665  T       t244    o244  P       p244    Number 4043
666  B       b244    t244  O       o244    type_fun p243 p244
667  T       t245    o243 b244  P       p245    Number 4033
668    O       o245    type_lid p243 p245
669    T       t245    o245 b184
670  B       b245    t245  B       b245    t245
671  P       p245    Number 1776  P       p246    Number 4037
672  O       o245    type_lid p245 p242  O       o246    type_lid p246 p244
673  T       t246    o245 b220  T       t246    o246 b160
674  B       b246    t246  B       b246    t246
675  T       t247    o242 b245 b246  T       t247    o244 b245 b246
676  B       b247    t247  B       b247    t247
677  T       t248    o b247 b4  T       t248    o239 b243 b247
678  B       b248    t248  B       b248    t248
679  T       t249    o b241 b248  P       p248    String sub
680  B       b249    t249  O       o248    resource p248
681  T       t250    o238 b249  P       p249    Number 4882
682  B       b250    t250  P       p250    Number 4899
683  P       p250    Number 1785  O       o250    type_lid p249 p250
684  P       p251    Number 1798  P       p251    String sub_resource_info
685  O       o251    type_fun p250 p251  O       o251    type_lid p251
686  P       p252    Number 1788  T       t251    o251
687  O       o252    type_lid p250 p252  B       b251    t251
688  T       t252    o252 b244  T       t252    o250 b251
689  B       b252    t252  B       b252    t252
690  P       p253    Number 1792  P       p252    Number 4901
691  O       o253    type_lid p253 p251  P       p253    Number 4907
692  T       t253    o253 b220  O       o253    type_lid p252 p253
693    T       t253    o253 b160
694  B       b253    t253  B       b253    t253
695  T       t254    o251 b252 b253  T       t254    o248 b252 b253
696  B       b254    t254  B       b254    t254
697  T       t255    o236 b250 b254  P       p254    String toploop
698  B       b255    t255  O       o254    resource p254
699  P       p255    String eqcd  P       p255    Number 2445
700  O       o255    resource p255  P       p256    Number 2467
701  P       p256    Number 6168  O       o256    type_prod p255 p256
702  P       p257    Number 6181  P       p257    Number 2451
703  O       o257    type_prod p256 p257  O       o257    type_lid p255 p257
704  P       p258    Number 6172  T       t257    o257 b211
705  O       o258    type_lid p256 p258  B       b257    t257
706  T       t258    o258 b240  P       p258    Number 2454
707  B       b258    t258  P       p259    Number 2460
708  P       p259    Number 6175  O       o259    type_lid p258 p259
709  O       o259    type_lid p259 p257  T       t259    o259 b211
 T       t259    o259 b220  
710  B       b259    t259  B       b259    t259
711  T       t260    o b259 b4  P       p260    Number 2463
712  B       b260    t260  O       o260    type_lid p260 p256
713  T       t261    o b258 b260  P       p261    String expr
714    O       o261    type_lid p261
715    T       t261    o261
716  B       b261    t261  B       b261    t261
717  T       t262    o257 b261  T       t262    o260 b261
718  B       b262    t262  B       b262    t262
719  P       p262    Number 6183  T       t263    o b262 b4
 P       p263    Number 6189  
 O       o263    type_lid p262 p263  
 T       t263    o263 b220  
720  B       b263    t263  B       b263    t263
721  T       t264    o255 b262 b263  T       t264    o b259 b263
722  B       b264    t264  B       b264    t264
723  P       p264    String intro  T       t265    o b257 b264
724  O       o264    resource p264  B       b265    t265
725  P       p265    Number 1815  T       t266    o256 b265
726  P       p266    Number 1852  B       b266    t266
727  O       o266    type_prod p265 p266  P       p266    Number 2469
728  P       p267    Number 1819  P       p267    Number 2478
729  O       o267    type_lid p265 p267  O       o267    type_lid p266 p267
730  T       t267    o267 b240  P       p268    String top_table
731  B       b267    t267  O       o268    type_lid p268
732  P       p268    Number 1823  T       t268    o268
733  P       p269    Number 1851  B       b268    t268
734  O       o269    type_prod p268 p269  T       t269    o267 b268
735  P       p270    Number 1829  B       b269    t269
736  O       o270    type_lid p268 p270  T       t270    o254 b266 b269
737  P       p271    String string  B       b270    t270
738  O       o271    type_lid p271  P       p270    String typeinf
739  T       t271    o271  O       o270    resource p270
740  B       b271    t271  P       p271    Number 2151
741  T       t272    o270 b271  P       p272    Number 2172
742  B       b272    t272  O       o272    type_lid p271 p272
743  NOcaml!type_apply       type_apply      type_apply Ocaml  P       p273    String typeinf_resource_info
744  P       p272    Number 1832  O       o273    type_lid p273
745  P       p273    Number 1842  T       t273    o273
746  O       o273    type_apply p272 p273  B       b273    t273
747  P       p274    Number 1836  T       t274    o272 b273
748  O       o274    type_lid p274 p273  B       b274    t274
749  P       p275    String option  P       p274    Number 2174
750  O       o275    type_lid p275  P       p275    Number 2186
751  T       t275    o275  O       o275    type_lid p274 p275
752  B       b275    t275  P       p276    String typeinf_func
753  T       t276    o274 b275  O       o276    type_lid p276
754    T       t276    o276
755  B       b276    t276  B       b276    t276
756  P       p276    Number 1835  T       t277    o275 b276
 O       o276    type_lid p272 p276  
 T       t277    o276 b244  
757  B       b277    t277  B       b277    t277
758  T       t278    o273 b276 b277  T       t278    o270 b274 b277
759  B       b278    t278  B       b278    t278
760  P       p278    Number 1845  P       p278    String typeinf_subst
761  O       o278    type_lid p278 p269  O       o278    resource p278
762  T       t279    o278 b220  P       p279    Number 1825
763  B       b279    t279  P       p280    Number 1843
764  T       t280    o b279 b4  O       o280    type_lid p279 p280
765  B       b280    t280  P       p281    String typeinf_subst_info
766  T       t281    o b278 b280  O       o281    type_lid p281
767    T       t281    o281
768  B       b281    t281  B       b281    t281
769  T       t282    o b272 b281  T       t282    o280 b281
770  B       b282    t282  B       b282    t282
771  T       t283    o269 b282  P       p282    Number 1862
772    O       o282    type_lid p218 p282
773    P       p283    String typeinf_subst_fun
774    O       o283    type_lid p283
775    T       t283    o283
776  B       b283    t283  B       b283    t283
777  T       t284    o b283 b4  T       t284    o282 b283
778  B       b284    t284  B       b284    t284
779  T       t285    o b267 b284  T       t285    o278 b282 b284
780  B       b285    t285  B       b285    t285
781  T       t286    o266 b285  T       t286    o b285 b4
782  B       b286    t286  B       b286    t286
783  P       p286    Number 1854  T       t287    o b278 b286
 P       p287    Number 1860  
 O       o287    type_lid p286 p287  
 T       t287    o287 b220  
784  B       b287    t287  B       b287    t287
785  T       t288    o264 b286 b287  T       t288    o b270 b287
786  B       b288    t288  B       b288    t288
787  P       p288    String reduce  T       t289    o b254 b288
788  O       o288    resource p288  B       b289    t289
789  P       p289    Number 2920  T       t290    o b248 b289
790  P       p290    Number 2931  B       b290    t290
791  O       o290    type_prod p289 p290  T       t291    o b239 b290
 P       p291    Number 2924  
 O       o291    type_lid p289 p291  
 T       t291    o291 b240  
792  B       b291    t291  B       b291    t291
793  P       p292    Number 2927  T       t292    o b228 b291
794  O       o292    type_lid p292 p290  B       b292    t292
795  P       p293    String conv  T       t293    o b204 b292
 O       o293    type_lid p293  
 T       t293    o293  
796  B       b293    t293  B       b293    t293
797  T       t294    o292 b293  T       t294    o b195 b293
798  B       b294    t294  B       b294    t294
799  T       t295    o b294 b4  T       t295    o b176 b294
800  B       b295    t295  B       b295    t295
801  T       t296    o b291 b295  T       t296    o b168 b295
802  B       b296    t296  B       b296    t296
803  T       t297    o290 b296  T       t297    o2 b5 b153 b296
804  B       b297    t297  B       b297    t297
805  P       p297    Number 2933  T       t298    o1 b297
 P       p298    Number 2937  
 O       o298    type_lid p297 p298  
 T       t298    o298 b293  
806  B       b298    t298  B       b298    t298
807  T       t299    o288 b297 b298  P       p298    Number 26
808  B       b299    t299  P       p299    Number 45
809  P       p299    String squash  O       o299    location p298 p299
810  O       o299    resource p299  P       p300    String Czf_itt_set
811  P       p300    Number 4017  O       o300    parent p300
812  P       p301    Number 4028  T       t300    o300
813  O       o301    type_lid p300 p301  B       b300    t300
814  P       p302    String squash_info  T       t301    o b300 b4
815  O       o302    type_lid p302  B       b301    t301
816  T       t302    o302  P       p301    String Czf_itt_comment
817    O       o301    parent p301
818    T       t302    o301
819  B       b302    t302  B       b302    t302
820  T       t303    o301 b302  T       t303    o b302 b4
821  B       b303    t303  B       b303    t303
822  P       p303    Number 4030  P       p303    String Itt_theory
823  P       p304    Number 4043  O       o303    parent p303
824  O       o304    type_fun p303 p304  T       t304    o303
825  P       p305    Number 4033  B       b304    t304
826  O       o305    type_lid p303 p305  T       t305    o b304 b4
 T       t305    o305 b244  
827  B       b305    t305  B       b305    t305
828  P       p306    Number 4037  P       p305    String Itt_fset
829  O       o306    type_lid p306 p304  O       o305    parent p305
830  T       t306    o306 b220  T       t306    o305
831  B       b306    t306  B       b306    t306
832  T       t307    o304 b305 b306  T       t307    o b306 b4
833  B       b307    t307  B       b307    t307
834  T       t308    o299 b303 b307  P       p307    String Itt_prop_decide
835    O       o307    parent p307
836    T       t308    o307
837  B       b308    t308  B       b308    t308
838  P       p308    String sub  T       t309    o b308 b4
839  O       o308    resource p308  B       b309    t309
840  P       p309    Number 4882  P       p309    String Itt_derive
841  P       p310    Number 4899  O       o309    parent p309
842  O       o310    type_lid p309 p310  T       t310    o309
843  P       p311    String sub_resource_info  B       b310    t310
844  O       o311    type_lid p311  T       t311    o b310 b4
 T       t311    o311  
845  B       b311    t311  B       b311    t311
846  T       t312    o310 b311  P       p311    String Itt_list2
847    O       o311    parent p311
848    T       t312    o311
849  B       b312    t312  B       b312    t312
850  P       p312    Number 4901  T       t313    o b312 b4
 P       p313    Number 4907  
 O       o313    type_lid p312 p313  
 T       t313    o313 b220  
851  B       b313    t313  B       b313    t313
852  T       t314    o308 b312 b313  P       p313    String Itt_list
853    O       o313    parent p313
854    T       t314    o313
855  B       b314    t314  B       b314    t314
856  P       p314    String toploop  T       t315    o b314 b4
857  O       o314    resource p314  B       b315    t315
858  P       p315    Number 2445  P       p315    String Itt_quotient
859  P       p316    Number 2467  O       o315    parent p315
860  O       o316    type_prod p315 p316  T       t316    o315
861  P       p317    Number 2451  B       b316    t316
862  O       o317    type_lid p315 p317  T       t317    o b316 b4
 T       t317    o317 b271  
863  B       b317    t317  B       b317    t317
864  P       p318    Number 2454  P       p317    String Itt_esquash
865  P       p319    Number 2460  O       o317    parent p317
866  O       o319    type_lid p318 p319  T       t318    o317
867  T       t319    o319 b271  B       b318    t318
868    T       t319    o b318 b4
869  B       b319    t319  B       b319    t319
870  P       p320    Number 2463  P       p319    String Itt_srec
871  O       o320    type_lid p320 p316  O       o319    parent p319
872  P       p321    String expr  T       t320    o319
873  O       o321    type_lid p321  B       b320    t320
874  T       t321    o321  T       t321    o b320 b4
875  B       b321    t321  B       b321    t321
876  T       t322    o320 b321  P       p321    String Itt_prec
877    O       o321    parent p321
878    T       t322    o321
879  B       b322    t322  B       b322    t322
880  T       t323    o b322 b4  T       t323    o b322 b4
881  B       b323    t323  B       b323    t323
882  T       t324    o b319 b323  P       p323    String Itt_w
883    O       o323    parent p323
884    T       t324    o323
885  B       b324    t324  B       b324    t324
886  T       t325    o b317 b324  T       t325    o b324 b4
887  B       b325    t325  B       b325    t325
888  T       t326    o316 b325  P       p325    String Itt_bunion
889    O       o325    parent p325
890    T       t326    o325
891  B       b326    t326  B       b326    t326
892  P       p326    Number 2469  T       t327    o b326 b4
893  P       p327    Number 2478  B       b327    t327
894  O       o327    type_lid p326 p327  P       p327    String Itt_bisect
895  P       p328    String top_table  O       o327    parent p327
896  O       o328    type_lid p328  T       t328    o327
 T       t328    o328  
897  B       b328    t328  B       b328    t328
898  T       t329    o327 b328  T       t329    o b328 b4
899  B       b329    t329  B       b329    t329
900  T       t330    o314 b326 b329  P       p329    String Itt_tunion
901    O       o329    parent p329
902    T       t330    o329
903  B       b330    t330  B       b330    t330
904  P       p330    String typeinf  T       t331    o b330 b4
905  O       o330    resource p330  B       b331    t331
906  P       p331    Number 2151  P       p331    String Itt_isect
907  P       p332    Number 2172  O       o331    parent p331
908  O       o332    type_lid p331 p332  T       t332    o331
909  P       p333    String typeinf_resource_info  B       b332    t332
910  O       o333    type_lid p333  T       t333    o b332 b4
 T       t333    o333  
911  B       b333    t333  B       b333    t333
912  T       t334    o332 b333  P       p333    String Itt_struct2
913    O       o333    parent p333
914    T       t334    o333
915  B       b334    t334  B       b334    t334
916  P       p334    Number 2174  T       t335    o b334 b4
917  P       p335    Number 2186  B       b335    t335
918  O       o335    type_lid p334 p335  P       p335    String Itt_well_founded
919  P       p336    String typeinf_func  O       o335    parent p335
920  O       o336    type_lid p336  T       t336    o335
 T       t336    o336  
921  B       b336    t336  B       b336    t336
922  T       t337    o335 b336  T       t337    o b336 b4
923  B       b337    t337  B       b337    t337
924  T       t338    o330 b334 b337  P       p337    String Itt_int_arith
925    O       o337    parent p337
926    T       t338    o337
927  B       b338    t338  B       b338    t338
928  P       p338    String typeinf_subst  T       t339    o b338 b4
929  O       o338    resource p338  B       b339    t339
930  P       p339    Number 1825  P       p339    String Itt_atom_bool
931  P       p340    Number 1843  O       o339    parent p339
932  O       o340    type_lid p339 p340  T       t340    o339
933  P       p341    String typeinf_subst_info  B       b340    t340
934  O       o341    type_lid p341  T       t341    o b340 b4
 T       t341    o341  
935  B       b341    t341  B       b341    t341
936  T       t342    o340 b341  P       p341    String Itt_atom
937    O       o341    parent p341
938    T       t342    o341
939  B       b342    t342  B       b342    t342
940  P       p342    Number 1862  T       t343    o b342 b4
 O       o342    type_lid p278 p342  
 P       p343    String typeinf_subst_fun  
 O       o343    type_lid p343  
 T       t343    o343  
941  B       b343    t343  B       b343    t343
942  T       t344    o342 b343  T       t344    o b343 b4
943  B       b344    t344  B       b344    t344
944  T       t345    o338 b342 b344  T       t345    o b341 b344
945  B       b345    t345  B       b345    t345
946  T       t346    o b345 b4  T       t346    o b339 b345
947  B       b346    t346  B       b346    t346
948  T       t347    o b338 b346  T       t347    o b337 b346
949  B       b347    t347  B       b347    t347
950  T       t348    o b330 b347  T       t348    o b335 b347
951  B       b348    t348  B       b348    t348
952  T       t349    o b314 b348  T       t349    o b333 b348
953  B       b349    t349  B       b349    t349
954  T       t350    o b308 b349  T       t350    o b331 b349
955  B       b350    t350  B       b350    t350
956  T       t351    o b299 b350  T       t351    o b329 b350
957  B       b351    t351  B       b351    t351
958  T       t352    o b288 b351  T       t352    o b327 b351
959  B       b352    t352  B       b352    t352
960  T       t353    o b264 b352  T       t353    o b325 b352
961  B       b353    t353  B       b353    t353
962  T       t354    o b255 b353  T       t354    o b323 b353
963  B       b354    t354  B       b354    t354
964  T       t355    o b236 b354  T       t355    o b321 b354
965  B       b355    t355  B       b355    t355
966  T       t356    o b228 b355  T       t356    o b319 b355
967  B       b356    t356  B       b356    t356
968  T       t357    o2 b5 b213 b356  T       t357    o b317 b356
969  B       b357    t357  B       b357    t357
970  T       t358    o1 b357  T       t358    o b315 b357
971  B       b358    t358  B       b358    t358
972  P       p358    Number 20  T       t359    o b313 b358
973  P       p359    Number 42  B       b359    t359
974  O       o359    location p358 p359  T       t360    o b311 b359
 P       p360    String Czf_itt_member  
 O       o360    parent p360  
 T       t360    o360  
975  B       b360    t360  B       b360    t360
976  T       t361    o b360 b4  T       t361    o b309 b360
977  B       b361    t361  B       b361    t361
978  P       p361    String Czf_itt_eq  T       t362    o b307 b361
 O       o361    parent p361  
 T       t362    o361  
979  B       b362    t362  B       b362    t362
980  T       t363    o b362 b4  T       t363    o b305 b362
981  B       b363    t363  B       b363    t363
982  T       t364    o b363 b4  T       t364    o b303 b363
983  B       b364    t364  B       b364    t364
984  T       t365    o b361 b364  T       t365    o b301 b364
985  B       b365    t365  B       b365    t365
986  T       t366    o2 b361 b365 b356  T       t366    o2 b301 b365 b296
987  B       b366    t366  B       b366    t366
988  T       t367    o359 b366  T       t367    o299 b366
989  B       b367    t367  B       b367    t367
990  P       p367    Number 43  P       p367    Number 46
991  P       p368    Number 61  P       p368    Number 68
992  O       o368    location p367 p368  O       o368    location p367 p368
993  T       t368    o2 b363 b4 b356  P       p369    String Czf_itt_member
994  B       b368    t368  O       o369    parent p369
995  T       t369    o368 b368  T       t369    o369
996  B       b369    t369  B       b369    t369
997  P       p369    Number 62  T       t370    o b369 b4
998  P       p370    Number 82  B       b370    t370
999  O       o370    location p369 p370  P       p370    String Czf_itt_eq
1000  P       p371    String Czf_itt_dall  O       o370    parent p370
1001  O       o371    parent p371  T       t371    o370
 T       t371    o371  
1002  B       b371    t371  B       b371    t371
1003  T       t372    o b371 b4  T       t372    o b371 b4
1004  B       b372    t372  B       b372    t372
1005  P       p372    String Czf_itt_set_ind  T       t373    o b372 b4
 O       o372    parent p372  
 T       t373    o372  
1006  B       b373    t373  B       b373    t373
1007  T       t374    o b373 b4  T       t374    o b370 b373
1008  B       b374    t374  B       b374    t374
1009  P       p374    String Czf_itt_all  T       t375    o2 b370 b374 b296
 O       o374    parent p374  
 T       t375    o374  
1010  B       b375    t375  B       b375    t375
1011  T       t376    o b375 b4  T       t376    o368 b375
1012  B       b376    t376  B       b376    t376
1013  P       p376    String Czf_itt_sep  P       p376    Number 69
1014  O       o376    parent p376  P       p377    Number 87
1015  T       t377    o376  O       o377    location p376 p377
1016    T       t377    o2 b372 b4 b296
1017  B       b377    t377  B       b377    t377
1018  T       t378    o b377 b4  T       t378    o377 b377
1019  B       b378    t378  B       b378    t378
1020  T       t379    o b378 b4  P       p378    Number 88
1021  B       b379    t379  P       p379    Number 108
1022  T       t380    o b376 b379  O       o379    location p378 p379
1023    P       p380    String Czf_itt_dall
1024    O       o380    parent p380
1025    T       t380    o380
1026  B       b380    t380  B       b380    t380
1027  T       t381    o b374 b380  T       t381    o b380 b4
1028  B       b381    t381  B       b381    t381
1029  T       t382    o b372 b381  P       p381    String Czf_itt_set_ind
1030    O       o381    parent p381
1031    T       t382    o381
1032  B       b382    t382  B       b382    t382
1033  T       t383    o2 b372 b382 b356  T       t383    o b382 b4
1034  B       b383    t383  B       b383    t383
1035  T       t384    o370 b383  P       p383    String Czf_itt_all
1036    O       o383    parent p383
1037    T       t384    o383
1038  B       b384    t384  B       b384    t384
1039  P       p384    Number 83  T       t385    o b384 b4
1040  P       p385    Number 102  B       b385    t385
1041  O       o385    location p384 p385  P       p385    String Czf_itt_sep
1042  P       p386    String Czf_itt_and  O       o385    parent p385
1043  O       o386    parent p386  T       t386    o385
 T       t386    o386  
1044  B       b386    t386  B       b386    t386
1045  T       t387    o b386 b4  T       t387    o b386 b4
1046  B       b387    t387  B       b387    t387
1047  T       t388    o b387 b4  T       t388    o b387 b4
1048  B       b388    t388  B       b388    t388
1049  T       t389    o2 b387 b388 b356  T       t389    o b385 b388
1050  B       b389    t389  B       b389    t389
1051  T       t390    o385 b389  T       t390    o b383 b389
1052  B       b390    t390  B       b390    t390
1053  P       p390    Number 104  T       t391    o b381 b390
1054  P       p391    Number 115  B       b391    t391
1055  O       o391    location p390 p391  T       t392    o2 b381 b391 b296
1056  NSummary!summary_item   summary_item    summary_item Summary  B       b392    t392
1057  O       o392    summary_item  T       t393    o379 b392
1058  NOcaml!str_open str_open        str_open Ocaml  B       b393    t393
1059  O       o393    str_open p390 p391  P       p393    Number 109
1060  NOcaml!string   string  string Ocaml  P       p394    Number 128
1061  P       p393    String Printf  O       o394    location p393 p394
1062  O       o394    string p393  P       p395    String Czf_itt_and
1063  T       t394    o394  O       o395    parent p395
1064  B       b394    t394  T       t395    o395
 T       t395    o b394 b4  
1065  B       b395    t395  B       b395    t395
1066  T       t396    o393 b395  T       t396    o b395 b4
1067  B       b396    t396  B       b396    t396
1068  T       t397    o392 b396  T       t397    o b396 b4
1069  B       b397    t397  B       b397    t397
1070  T       t398    o391 b397  T       t398    o2 b396 b397 b296
1071  B       b398    t398  B       b398    t398
1072  P       p398    Number 116  T       t399    o394 b398
1073  P       p399    Number 129  B       b399    t399
1074  O       o399    location p398 p399  P       p399    Number 130
1075  O       o400    str_open p398 p399  P       p400    Number 141
1076  P       p400    String Mp_debug  O       o400    location p399 p400
1077  O       o401    string p400  NSummary!summary_item   summary_item    summary_item Summary
1078  T       t401    o401  O       o401    summary_item
1079  B       b401    t401  NOcaml!str_open str_open        str_open Ocaml
1080  T       t402    o b401 b4  O       o402    str_open p399 p400
1081  B       b402    t402  NOcaml!string   string  string Ocaml
1082  T       t403    o400 b402  P       p402    String Printf
1083    O       o403    string p402
1084    T       t403    o403
1085  B       b403    t403  B       b403    t403
1086  T       t404    o392 b403  T       t404    o b403 b4
1087  B       b404    t404  B       b404    t404
1088  T       t405    o399 b404  T       t405    o402 b404
1089  B       b405    t405  B       b405    t405
1090  P       p405    Number 130  T       t406    o401 b405
1091  P       p406    Number 159  B       b406    t406
1092  O       o406    location p405 p406  T       t407    o400 b406
1093  O       o407    str_open p405 p406  B       b407    t407
1094  P       p407    String Refiner  P       p407    Number 142
1095  O       o408    string p407  P       p408    Number 155
1096  T       t408    o408  O       o408    location p407 p408
1097  B       b408    t408  O       o409    str_open p407 p408
1098  P       p408    String TermType  P       p409    String Mp_debug
1099  O       o409    string p408  O       o410    string p409
1100  T       t409    o409  T       t410    o410
 B       b409    t409  
 T       t410    o b409 b4  
1101  B       b410    t410  B       b410    t410
1102  T       t411    o b408 b410  T       t411    o b410 b4
1103  B       b411    t411  B       b411    t411
1104  T       t412    o b408 b411  T       t412    o409 b411
1105  B       b412    t412  B       b412    t412
1106  T       t413    o407 b412  T       t413    o401 b412
1107  B       b413    t413  B       b413    t413
1108  T       t414    o392 b413  T       t414    o408 b413
1109  B       b414    t414  B       b414    t414
1110  T       t415    o406 b414  P       p414    Number 156
1111  B       b415    t415  P       p415    Number 185
1112  P       p415    Number 160  O       o415    location p414 p415
1113  P       p416    Number 185  O       o416    str_open p414 p415
1114  O       o416    location p415 p416  P       p416    String Refiner
1115  O       o417    str_open p415 p416  O       o417    string p416
1116  P       p417    String Term  T       t417    o417
1117    B       b417    t417
1118    P       p417    String TermType
1119  O       o418    string p417  O       o418    string p417
1120  T       t418    o418  T       t418    o418
1121  B       b418    t418  B       b418    t418
1122  T       t419    o b418 b4  T       t419    o b418 b4
1123  B       b419    t419  B       b419    t419
1124  T       t420    o b408 b419  T       t420    o b417 b419
1125  B       b420    t420  B       b420    t420
1126  T       t421    o b408 b420  T       t421    o b417 b420
1127  B       b421    t421  B       b421    t421
1128  T       t422    o417 b421  T       t422    o416 b421
1129  B       b422    t422  B       b422    t422
1130  T       t423    o392 b422  T       t423    o401 b422
1131  B       b423    t423  B       b423    t423
1132  T       t424    o416 b423  T       t424    o415 b423
1133  B       b424    t424  B       b424    t424
1134  P       p424    Number 186  P       p424    Number 186
1135  P       p425    Number 213  P       p425    Number 211
1136  O       o425    location p424 p425  O       o425    location p424 p425
1137  O       o426    str_open p424 p425  O       o426    str_open p424 p425
1138  P       p426    String TermOp  P       p426    String Term
1139  O       o427    string p426  O       o427    string p426
1140  T       t427    o427  T       t427    o427
1141  B       b427    t427  B       b427    t427
1142  T       t428    o b427 b4  T       t428    o b427 b4
1143  B       b428    t428  B       b428    t428
1144  T       t429    o b408 b428  T       t429    o b417 b428
1145  B       b429    t429  B       b429    t429
1146  T       t430    o b408 b429  T       t430    o b417 b429
1147  B       b430    t430  B       b430    t430
1148  T       t431    o426 b430  T       t431    o426 b430
1149  B       b431    t431  B       b431    t431
1150  T       t432    o392 b431  T       t432    o401 b431
1151  B       b432    t432  B       b432    t432
1152  T       t433    o425 b432  T       t433    o425 b432
1153  B       b433    t433  B       b433    t433
1154  P       p433    Number 214  P       p433    Number 212
1155  P       p434    Number 243  P       p434    Number 239
1156  O       o434    location p433 p434  O       o434    location p433 p434
1157  O       o435    str_open p433 p434  O       o435    str_open p433 p434
1158  P       p435    String TermAddr  P       p435    String TermOp
1159  O       o436    string p435  O       o436    string p435
1160  T       t436    o436  T       t436    o436
1161  B       b436    t436  B       b436    t436
1162  T       t437    o b436 b4  T       t437    o b436 b4
1163  B       b437    t437  B       b437    t437
1164  T       t438    o b408 b437  T       t438    o b417 b437
1165  B       b438    t438  B       b438    t438
1166  T       t439    o b408 b438  T       t439    o b417 b438
1167  B       b439    t439  B       b439    t439
1168  T       t440    o435 b439  T       t440    o435 b439
1169  B       b440    t440  B       b440    t440
1170  T       t441    o392 b440  T       t441    o401 b440
1171  B       b441    t441  B       b441    t441
1172  T       t442    o434 b441  T       t442    o434 b441
1173  B       b442    t442  B       b442    t442
1174  P       p442    Number 244  P       p442    Number 240
1175  P       p443    Number 272  P       p443    Number 269
1176  O       o443    location p442 p443  O       o443    location p442 p443
1177  O       o444    str_open p442 p443  O       o444    str_open p442 p443
1178  P       p444    String TermMan  P       p444    String TermAddr
1179  O       o445    string p444  O       o445    string p444
1180  T       t445    o445  T       t445    o445
1181  B       b445    t445  B       b445    t445
1182  T       t446    o b445 b4  T       t446    o b445 b4
1183  B       b446    t446  B       b446    t446
1184  T       t447    o b408 b446  T       t447    o b417 b446
1185  B       b447    t447  B       b447    t447
1186  T       t448    o b408 b447  T       t448    o b417 b447
1187  B       b448    t448  B       b448    t448
1188  T       t449    o444 b448  T       t449    o444 b448
1189  B       b449    t449  B       b449    t449
1190  T       t450    o392 b449  T       t450    o401 b449
1191  B       b450    t450  B       b450    t450
1192  T       t451    o443 b450  T       t451    o443 b450
1193  B       b451    t451  B       b451    t451
1194  P       p451    Number 273  P       p451    Number 270
1195  P       p452    Number 303  P       p452    Number 298
1196  O       o452    location p451 p452  O       o452    location p451 p452
1197  O       o453    str_open p451 p452  O       o453    str_open p451 p452
1198  P       p453    String TermSubst  P       p453    String TermMan
1199  O       o454    string p453  O       o454    string p453
1200  T       t454    o454  T       t454    o454
1201  B       b454    t454  B       b454    t454
1202  T       t455    o b454 b4  T       t455    o b454 b4
1203  B       b455    t455  B       b455    t455
1204  T       t456    o b408 b455  T       t456    o b417 b455
1205  B       b456    t456  B       b456    t456
1206  T       t457    o b408 b456  T       t457    o b417 b456
1207  B       b457    t457  B       b457    t457
1208  T       t458    o453 b457  T       t458    o453 b457
1209  B       b458    t458  B       b458    t458
1210  T       t459    o392 b458  T       t459    o401 b458
1211  B       b459    t459  B       b459    t459
1212  T       t460    o452 b459  T       t460    o452 b459
1213  B       b460    t460  B       b460    t460
1214  P       p460    Number 304  P       p460    Number 299
1215  P       p461    Number 331  P       p461    Number 329
1216  O       o461    location p460 p461  O       o461    location p460 p461
1217  O       o462    str_open p460 p461  O       o462    str_open p460 p461
1218  P       p462    String Refine  P       p462    String TermSubst
1219  O       o463    string p462  O       o463    string p462
1220  T       t463    o463  T       t463    o463
1221  B       b463    t463  B       b463    t463
1222  T       t464    o b463 b4  T       t464    o b463 b4
1223  B       b464    t464  B       b464    t464
1224  T       t465    o b408 b464  T       t465    o b417 b464
1225  B       b465    t465  B       b465    t465
1226  T       t466    o b408 b465  T       t466    o b417 b465
1227  B       b466    t466  B       b466    t466
1228  T       t467    o462 b466  T       t467    o462 b466
1229  B       b467    t467  B       b467    t467
1230  T       t468    o392 b467  T       t468    o401 b467
1231  B       b468    t468  B       b468    t468
1232  T       t469    o461 b468  T       t469    o461 b468
1233  B       b469    t469  B       b469    t469
1234  P       p469    Number 332  P       p469    Number 330
1235  P       p470    Number 364  P       p470    Number 357
1236  O       o470    location p469 p470  O       o470    location p469 p470
1237  O       o471    str_open p469 p470  O       o471    str_open p469 p470
1238  P       p471    String RefineError  P       p471    String Refine
1239  O       o472    string p471  O       o472    string p471
1240  T       t472    o472  T       t472    o472
1241  B       b472    t472  B       b472    t472
1242  T       t473    o b472 b4  T       t473    o b472 b4
1243  B       b473    t473  B       b473    t473
1244  T       t474    o b408 b473  T       t474    o b417 b473
1245  B       b474    t474  B       b474    t474
1246  T       t475    o b408 b474  T       t475    o b417 b474
1247  B       b475    t475  B       b475    t475
1248  T       t476    o471 b475  T       t476    o471 b475
1249  B       b476    t476  B       b476    t476
1250  T       t477    o392 b476  T       t477    o401 b476
1251  B       b477    t477  B       b477    t477
1252  T       t478    o470 b477  T       t478    o470 b477
1253  B       b478    t478  B       b478    t478
1254  P       p478    Number 365  P       p478    Number 358
1255  P       p479    Number 381  P       p479    Number 390
1256  O       o479    location p478 p479  O       o479    location p478 p479
1257  O       o480    str_open p478 p479  O       o480    str_open p478 p479
1258  P       p480    String Mp_resource  P       p480    String RefineError
1259  O       o481    string p480  O       o481    string p480
1260  T       t481    o481  T       t481    o481
1261  B       b481    t481  B       b481    t481
1262  T       t482    o b481 b4  T       t482    o b481 b4
1263  B       b482    t482  B       b482    t482
1264  T       t483    o480 b482  T       t483    o b417 b482
1265  B       b483    t483  B       b483    t483
1266  T       t484    o392 b483  T       t484    o b417 b483
1267  B       b484    t484  B       b484    t484
1268  T       t485    o479 b484  T       t485    o480 b484
1269  B       b485    t485  B       b485    t485
1270  P       p485    Number 382  T       t486    o401 b485
1271  P       p486    Number 399  B       b486    t486
1272  O       o486    location p485 p486  T       t487    o479 b486
1273  O       o487    str_open p485 p486  B       b487    t487
1274  P       p487    String Simple_print  P       p487    Number 391
1275  O       o488    string p487  P       p488    Number 407
1276  T       t488    o488  O       o488    location p487 p488
1277  B       b488    t488  O       o489    str_open p487 p488
1278  T       t489    o b488 b4  P       p489    String Mp_resource
1279  B       b489    t489  O       o490    string p489
1280  T       t490    o487 b489  T       t490    o490
1281  B       b490    t490  B       b490    t490
1282  T       t491    o392 b490  T       t491    o b490 b4
1283  B       b491    t491  B       b491    t491
1284  T       t492    o486 b491  T       t492    o489 b491
1285  B       b492    t492  B       b492    t492
1286  P       p492    Number 401  T       t493    o401 b492
1287  P       p493    Number 417  B       b493    t493
1288  O       o493    location p492 p493  T       t494    o488 b493
1289  O       o494    str_open p492 p493  B       b494    t494
1290  P       p494    String Tactic_type  P       p494    Number 408
1291  O       o495    string p494  P       p495    Number 425
1292  T       t495    o495  O       o495    location p494 p495
1293  B       b495    t495  O       o496    str_open p494 p495
1294  T       t496    o b495 b4  P       p496    String Simple_print
1295  B       b496    t496  O       o497    string p496
1296  T       t497    o494 b496  T       t497    o497
1297  B       b497    t497  B       b497    t497
1298  T       t498    o392 b497  T       t498    o b497 b4
1299  B       b498    t498  B       b498    t498
1300  T       t499    o493 b498  T       t499    o496 b498
1301  B       b499    t499  B       b499    t499
1302  P       p499    Number 418  T       t500    o401 b499
1303  P       p500    Number 444  B       b500    t500
1304  O       o500    location p499 p500  T       t501    o495 b500
1305  O       o501    str_open p499 p500  B       b501    t501
1306  P       p501    String Tacticals  P       p501    Number 427
1307  O       o502    string p501  P       p502    Number 443
1308  T       t502    o502  O       o502    location p501 p502
1309  B       b502    t502  O       o503    str_open p501 p502
1310  T       t503    o b502 b4  P       p503    String Tactic_type
1311  B       b503    t503  O       o504    string p503
1312  T       t504    o b495 b503  T       t504    o504
1313  B       b504    t504  B       b504    t504
1314  T       t505    o501 b504  T       t505    o b504 b4
1315  B       b505    t505  B       b505    t505
1316  T       t506    o392 b505  T       t506    o503 b505
1317  B       b506    t506  B       b506    t506
1318  T       t507    o500 b506  T       t507    o401 b506
1319  B       b507    t507  B       b507    t507
1320  P       p507    Number 445  T       t508    o502 b507
1321  P       p508    Number 469  B       b508    t508
1322  O       o508    location p507 p508  P       p508    Number 444
1323  O       o509    str_open p507 p508  P       p509    Number 470
1324  P       p509    String Sequent  O       o509    location p508 p509
1325  O       o510    string p509  O       o510    str_open p508 p509
1326  T       t510    o510  P       p510    String Tacticals
1327  B       b510    t510  O       o511    string p510
1328  T       t511    o b510 b4  T       t511    o511
1329  B       b511    t511  B       b511    t511
1330  T       t512    o b495 b511  T       t512    o b511 b4
1331  B       b512    t512  B       b512    t512
1332  T       t513    o509 b512  T       t513    o b504 b512
1333  B       b513    t513  B       b513    t513
1334  T       t514    o392 b513  T       t514    o510 b513
1335  B       b514    t514  B       b514    t514
1336  T       t515    o508 b514  T       t515    o401 b514
1337  B       b515    t515  B       b515    t515
1338  P       p515    Number 470  T       t516    o509 b515
1339  P       p516    Number 500  B       b516    t516
1340  O       o516    location p515 p516  P       p516    Number 471
1341  O       o517    str_open p515 p516  P       p517    Number 495
1342  P       p517    String Conversionals  O       o517    location p516 p517
1343  O       o518    string p517  O       o518    str_open p516 p517
1344  T       t518    o518  P       p518    String Sequent
1345  B       b518    t518  O       o519    string p518
1346  T       t519    o b518 b4  T       t519    o519
1347  B       b519    t519  B       b519    t519
1348  T       t520    o b495 b519  T       t520    o b519 b4
1349  B       b520    t520  B       b520    t520
1350  T       t521    o517 b520  T       t521    o b504 b520
1351  B       b521    t521  B       b521    t521
1352  T       t522    o392 b521  T       t522    o518 b521
1353  B       b522    t522  B       b522    t522
1354  T       t523    o516 b522  T       t523    o401 b522
1355  B       b523    t523  B       b523    t523
1356  P       p523    Number 501  T       t524    o517 b523
1357  P       p524    Number 511  B       b524    t524
1358  O       o524    location p523 p524  P       p524    Number 496
1359  O       o525    str_open p523 p524  P       p525    Number 526
1360  O       o526    string p131  O       o525    location p524 p525
1361  T       t526    o526  O       o526    str_open p524 p525
1362  B       b526    t526  P       p526    String Conversionals
1363  T       t527    o b526 b4  O       o527    string p526
1364    T       t527    o527
1365  B       b527    t527  B       b527    t527
1366  T       t528    o525 b527  T       t528    o b527 b4
1367  B       b528    t528  B       b528    t528
1368  T       t529    o392 b528  T       t529    o b504 b528
1369  B       b529    t529  B       b529    t529
1370  T       t530    o524 b529  T       t530    o526 b529
1371  B       b530    t530  B       b530    t530
1372  P       p530    Number 512  T       t531    o401 b530
1373  P       p531    Number 520  B       b531    t531
1374  O       o531    location p530 p531  T       t532    o525 b531
1375  O       o532    str_open p530 p531  B       b532    t532
1376  O       o533    string p129  P       p532    Number 527
1377  T       t533    o533  P       p533    Number 537
1378  B       b533    t533  O       o533    location p532 p533
1379  T       t534    o b533 b4  O       o534    str_open p532 p533
1380  B       b534    t534  O       o535    string p91
1381  T       t535    o532 b534  T       t535    o535
1382  B       b535    t535  B       b535    t535
1383  T       t536    o392 b535  T       t536    o b535 b4
1384  B       b536    t536  B       b536    t536
1385  T       t537    o531 b536  T       t537    o534 b536
1386  B       b537    t537  B       b537    t537
1387  P       p537    Number 522  T       t538    o401 b537
1388  P       p538    Number 539  B       b538    t538
1389  O       o538    location p537 p538  T       t539    o533 b538
1390  O       o539    str_open p537 p538  B       b539    t539
1391  O       o540    string p119  P       p539    Number 538
1392  T       t540    o540  P       p540    Number 546
1393  B       b540    t540  O       o540    location p539 p540
1394  T       t541    o b540 b4  O       o541    str_open p539 p540
1395  B       b541    t541  O       o542    string p89
1396  T       t542    o539 b541  T       t542    o542
1397  B       b542    t542  B       b542    t542
1398  T       t543    o392 b542  T       t543    o b542 b4
1399  B       b543    t543  B       b543    t543
1400  T       t544    o538 b543  T       t544    o541 b543
1401  B       b544    t544  B       b544    t544
1402  P       p544    Number 540  T       t545    o401 b544
1403  P       p545    Number 561  B       b545    t545
1404  O       o545    location p544 p545  T       t546    o540 b545
1405  O       o546    str_open p544 p545  B       b546    t546
1406  O       o547    string p121  P       p546    Number 548
1407  T       t547    o547  P       p547    Number 565
1408  B       b547    t547  O       o547    location p546 p547
1409  T       t548    o b547 b4  O       o548    str_open p546 p547
1410  B       b548    t548  O       o549    string p79
1411  T       t549    o546 b548  T       t549    o549
1412  B       b549    t549  B       b549    t549
1413  T       t550    o392 b549  T       t550    o b549 b4
1414  B       b550    t550  B       b550    t550
1415  T       t551    o545 b550  T       t551    o548 b550
1416  B       b551    t551  B       b551    t551
1417  P       p551    Number 563  T       t552    o401 b551
1418  P       p552    Number 574  B       b552    t552
1419  O       o552    location p551 p552  T       t553    o547 b552
1420    B       b553    t553
1421    P       p553    Number 566
1422    P       p554    Number 587
1423    O       o554    location p553 p554
1424    O       o555    str_open p553 p554
1425    O       o556    string p81
1426    T       t556    o556
1427    B       b556    t556
1428    T       t557    o b556 b4
1429    B       b557    t557
1430    T       t558    o555 b557
1431    B       b558    t558
1432    T       t559    o401 b558
1433    B       b559    t559
1434    T       t560    o554 b559
1435    B       b560    t560
1436    P       p560    Number 589
1437    P       p561    Number 606
1438    O       o561    location p560 p561
1439  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1440  P       p553    String car  P       p562    String group
1441  O       o553    opname p553  O       o562    opname p562
1442  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1443  NCzf_itt_group!car      car     car Czf_itt_group  NCzf_itt_group!group    group   group Czf_itt_group
1444  O       o554    car  O       o563    group
 T       t554    o554  
 B       b554    t554  
 T       t555    o553 b554  
 B       b555    t555  
 T       t556    o552 b555  
 B       b556    t556  
 P       p556    Number 615  
 P       p557    Number 635  
 O       o557    location p556 p557  
 P       p558    String op  
 O       o558    opname p558  
 NCzf_itt_group!op       op      op Czf_itt_group  
 O       o559    op  
1445  Nvar    var     var NIL  Nvar    var     var NIL
1446  P       p559    Var s1  P       p563    Var g
1447  O       o560    var p559  O       o564    var p563
1448  T       t560    o560  T       t564    o564
 B       b560    t560  
 P       p560    Var s2  
 O       o561    var p560  
 T       t561    o561  
 B       b561    t561  
 T       t562    o559 b560 b561  
 B       b562    t562  
 T       t563    o558 b562  
 B       b563    t563  
 T       t564    o557 b563  
1449  B       b564    t564  B       b564    t564
1450  P       p564    Number 636  T       t565    o563 b564
1451  P       p565    Number 646  B       b565    t565
1452  O       o565    location p564 p565  T       t566    o562 b565
1453  P       p566    String id  B       b566    t566
1454  O       o566    opname p566  T       t567    o561 b566
 NCzf_itt_group!id       id      id Czf_itt_group  
 O       o567    id  
 T       t567    o567  
1455  B       b567    t567  B       b567    t567
1456  T       t568    o566 b567  P       p567    Number 607
1457  B       b568    t568  P       p568    Number 622
1458  T       t569    o565 b568  O       o568    location p567 p568
1459  B       b569    t569  P       p569    String car
1460  P       p569    Number 647  O       o569    opname p569
1461  P       p570    Number 662  NCzf_itt_group!car      car     car Czf_itt_group
1462  O       o570    location p569 p570  O       o570    car
1463  P       p571    String inv  T       t570    o570 b564
1464  O       o571    opname p571  B       b570    t570
1465  NCzf_itt_group!inv      inv     inv Czf_itt_group  T       t571    o569 b570
1466  O       o572    inv  B       b571    t571
1467  P       p572    Var s  T       t572    o568 b571
1468  O       o573    var p572  B       b572    t572
1469  T       t573    o573  P       p572    Number 663
1470  B       b573    t573  P       p573    Number 687
1471  T       t574    o572 b573  O       o573    location p572 p573
1472  B       b574    t574  P       p574    String op
1473  T       t575    o571 b574  O       o574    opname p574
1474  B       b575    t575  NCzf_itt_group!op       op      op Czf_itt_group
1475  T       t576    o570 b575  O       o575    op
1476    P       p575    Var s1
1477    O       o576    var p575
1478    T       t576    o576
1479  B       b576    t576  B       b576    t576
1480  P       p576    Number 664  P       p576    Var s2
1481  P       p577    Number 712  O       o577    var p576
1482  O       o577    location p576 p577  T       t577    o577
1483  NSummary!dform  dform   dform Summary  B       b577    t577
1484  P       p578    String car_df  T       t578    o575 b564 b576 b577
1485  O       o578    dform p578  B       b578    t578
1486  NSummary!except_mode_df except_mode_df  except_mode_df Summary  T       t579    o574 b578
 P       p579    String src  
 O       o579    except_mode_df p579  
 T       t579    o579  
1487  B       b579    t579  B       b579    t579
1488  T       t580    o b579 b4  T       t580    o573 b579
1489  B       b580    t580  B       b580    t580
1490  NSummary!df_term        df_term df_term Summary  P       p580    Number 688
1491  O       o580    df_term  P       p581    Number 702
1492  NPerv!string    string580       string Perv  O       o581    location p580 p581
1493  P       p580    String G  P       p582    String id
1494  O       o581    string580 p580  O       o582    opname p582
1495  T       t581    o581  NCzf_itt_group!id       id      id Czf_itt_group
1496  B       b581    t581  O       o583    id
1497  T       t582    o b581 b4  T       t583    o583 b564
 B       b582    t582  
 T       t583    o580 b582  
1498  B       b583    t583  B       b583    t583
1499  T       t584    o578 b580 b554 b583  T       t584    o582 b583
1500  B       b584    t584  B       b584    t584
1501  T       t585    o577 b584  T       t585    o581 b584
1502  B       b585    t585  B       b585    t585
1503  P       p585    Number 714  P       p585    Number 703
1504  P       p586    Number 760  P       p586    Number 722
1505  O       o586    location p585 p586  O       o586    location p585 p586
1506  P       p587    String id_df  P       p587    String inv
1507  O       o587    dform p587  O       o587    opname p587
1508  P       p588    String e  NCzf_itt_group!inv      inv     inv Czf_itt_group
1509  O       o588    string580 p588  O       o588    inv
1510  T       t588    o588  P       p588    Var s
1511  B       b588    t588  O       o589    var p588
1512  T       t589    o b588 b4  T       t589    o589
1513  B       b589    t589  B       b589    t589
1514  T       t590    o580 b589  T       t590    o588 b564 b589
1515  B       b590    t590  B       b590    t590
1516  T       t591    o587 b580 b567 b590  T       t591    o587 b590
1517  B       b591    t591  B       b591    t591
1518  T       t592    o586 b591  T       t592    o586 b591
1519  B       b592    t592  B       b592    t592
1520  P       p592    Number 762  P       p592    Number 723
1521  P       p593    Number 862  P       p593    Number 751
1522  O       o593    location p592 p593  O       o593    location p592 p593
1523  P       p594    String op_df  P       p594    String eqElem
1524  O       o594    dform p594  O       o594    opname p594
1525  NSummary!parens_df      parens_df       parens_df Summary  NCzf_itt_group!eqElem   eqElem  eqElem Czf_itt_group
1526  O       o595    parens_df  O       o595    eqElem
1527  T       t595    o595  T       t595    o595 b564 b576 b577
1528  B       b595    t595  B       b595    t595
1529  T       t596    o b595 b4  T       t596    o594 b595
1530  B       b596    t596  B       b596    t596
1531  T       t597    o b579 b596  T       t597    o593 b596
1532  B       b597    t597  B       b597    t597
1533  Nslot   slot    slot NIL  P       p597    Number 753
1534  P       p597    String le  P       p3      Number 765
1535  O       o597    slot p597  O       o6      location p597 p3
1536  T       t598    o597 b560  NSummary!prec   prec    prec Summary
1537  B       b598    t598  P       p6      String prec_op
1538  P       p598    String " * "  O       o8      prec p6
1539  O       o598    string580 p598  T       t154    o8
1540  T       t599    o598  B       b154    t154
1541  B       b599    t599  T       t155    o6 b154
1542  T       t600    o597 b561  B       b155    t155
1543    P       p164    Number 767
1544    P       p165    Number 837
1545    O       o165    location p164 p165
1546    NSummary!dform  dform   dform Summary
1547    P       p599    String group_df
1548    O       o599    dform p599
1549    NSummary!except_mode_df except_mode_df  except_mode_df Summary
1550    P       p600    String src
1551    O       o600    except_mode_df p600
1552    T       t600    o600
1553  B       b600    t600  B       b600    t600
1554  T       t601    o b600 b4  T       t601    o b600 b4
1555  B       b601    t601  B       b601    t601
1556  T       t602    o b599 b601  NSummary!df_term        df_term df_term Summary
1557    O       o601    df_term
1558    Nslot   slot    slot NIL
1559    O       o602    slot
1560    T       t602    o602 b564
1561  B       b602    t602  B       b602    t602
1562  T       t603    o b598 b602  NPerv!string    string602       string Perv
1563    P       p602    String " group"
1564    O       o603    string602 p602
1565    T       t603    o603
1566  B       b603    t603  B       b603    t603
1567  T       t604    o580 b603  T       t604    o b603 b4
1568  B       b604    t604  B       b604    t604
1569  T       t605    o594 b597 b562 b604  T       t605    o b602 b604
1570  B       b605    t605  B       b605    t605
1571  T       t606    o593 b605  T       t606    o601 b605
1572  B       b606    t606  B       b606    t606
1573  P       p606    Number 864  T       t607    o599 b601 b565 b606
1574  P       p607    Number 941  B       b607    t607
1575  O       o607    location p606 p607  T       t169    o165 b607
1576  P       p608    String inv_df  B       b169    t169
1577  O       o608    dform p608  P       p174    Number 839
1578  T       t608    o597 b573  P       p175    Number 908
1579  B       b608    t608  O       o175    location p174 p175
1580  P       p609    String '  P       p610    String car_df
1581  O       o609    string580 p609  O       o610    dform p610
1582  T       t609    o609  P       p611    String car(
1583  B       b609    t609  O       o611    string602 p611
1584  T       t610    o b609 b4  T       t611    o611
 B       b610    t610  
 T       t611    o b608 b610  
1585  B       b611    t611  B       b611    t611
1586  T       t612    o580 b611  P       p612    String )
1587    O       o612    string602 p612
1588    T       t612    o612
1589  B       b612    t612  B       b612    t612
1590  T       t613    o608 b597 b574 b612  T       t613    o b612 b4
1591  B       b613    t613  B       b613    t613
1592  T       t614    o607 b613  T       t614    o b602 b613
1593  B       b614    t614  B       b614    t614
1594  P       p12     Number 960  T       t615    o b611 b614
1595  P       p14     Number 1036  B       b615    t615
1596  O       o14     location p12 p14  T       t616    o601 b615
1597  NSummary!rule   rule    rule Summary  B       b616    t616
1598  P       p616    String car_wf  T       t617    o610 b601 b570 b616
 O       o616    rule p616  
 NSummary!context_param  context_param   context_param Summary  
 P       p617    String H  
 O       o617    context_param p617  
 T       t617    o617  
1599  B       b617    t617  B       b617    t617
1600  T       t618    o b617 b4  T       t177    o175 b617
1601  B       b618    t618  B       b177    t177
1602  NSummary!meta_theorem   meta_theorem    meta_theorem Summary  P       p186    Number 910
1603  O       o618    meta_theorem  P       p187    Number 976
1604  P       p618    Var ext  O       o187    location p186 p187
1605  O       o619    var p618  P       p620    String id_df
1606  T       t619    o619  O       o620    dform p620
1607  B       b619    t619  P       p621    String id(
1608  T       t620    o b619 b4  O       o621    string602 p621
1609  C       h       H  T       t621    o621
1610  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL  B       b621    t621
1611  NCzf_itt_set!isset      isset   isset Czf_itt_set  T       t622    o b621 b614
 O       o620    isset  
 T       t621    o620 b554  
 S       s       t620 h  
 G       s       t621  
 B       b621    s  
 T       t622    o618 b621  
1612  B       b622    t622  B       b622    t622
1613  NSummary!incomplete     incomplete      incomplete Summary  T       t623    o601 b622
 O       o622    incomplete  
 T       t623    o622  
1614  B       b623    t623  B       b623    t623
1615  NSummary!resource_defs  resource_defs   resource_defs Summary  T       t624    o620 b601 b583 b623
1616  P       p16     Number 982  B       b624    t624
1617  P       p18     Number 989  T       t191    o187 b624
1618  O       o18     resource_defs p16 p18 p264  B       b191    t191
1619  NOcaml!uid      uid     uid Ocaml  P       p194    Number 978
1620  P       p20     Number 987  P       p200    Number 1116
1621  O       o20     uid p20 p18  O       o200    location p194 p200
1622  P       p626    String []  P       p627    String op_df
1623  O       o626    uid p626  O       o627    dform p627
1624  T       t626    o626  NSummary!prec_df        prec_df prec_df Summary
1625  B       b626    t626  O       o201    prec_df p6
1626  T       t370    o20 b626  T       t205    o201
1627  B       b370    t370  B       b205    t205
1628  T       t385    o b370 b4  NSummary!parens_df      parens_df       parens_df Summary
1629  B       b385    t385  O       o628    parens_df
1630  T       t462    o18 b385  T       t628    o628
1631  B       b462    t462  B       b628    t628
1632  T       t470    o b462 b4  T       t629    o b628 b4
1633  B       b470    t470  B       b629    t629
1634  T       t525    o616 b618 b622 b623 b470  T       t206    o b205 b629
1635  B       b525    t525  B       b206    t206
1636  T       t531    o14 b525  T       t208    o b600 b206
1637  B       b531    t531  B       b208    t208
1638  P       p532    Number 1038  T       t630    o b600 b629
1639  P       p533    Number 1213  B       b630    t630
1640  O       o534    location p532 p533  P       p630    String op(
1641  P       p634    String op_wf1  O       o630    string602 p630
1642  O       o634    rule p634  T       t631    o630
1643  NSummary!meta_implies   meta_implies    meta_implies Summary  B       b631    t631
1644  O       o635    meta_implies  P       p631    String "; "
1645  NBase_trivial   Base_trivial    Base_trivial NIL  O       o631    string602 p631
1646  NBase_trivial!squash    squash  squash Base_trivial  T       t632    o631
1647  O       o636    squash  B       b632    t632
1648  T       t636    o636  T       t633    o602 b576
1649    B       b633    t633
1650    T       t634    o602 b577
1651    B       b634    t634
1652    T       t635    o b634 b613
1653    B       b635    t635
1654    T       t636    o b632 b635
1655  B       b636    t636  B       b636    t636
1656  T       t637    o b636 b4  T       t637    o b633 b636
1657  T       t638    o620 b560  B       b637    t637
1658  S       s638    t637 h  T       t638    o b632 b637
1659  G       s638    t638  B       b638    t638
1660  B       b638    s638  T       t639    o b602 b638
 T       t639    o618 b638  
1661  B       b639    t639  B       b639    t639
1662  T       t640    o620 b561  T       t640    o b631 b639
1663  S       s640    t637 h  B       b640    t640
1664  G       s640    t640  T       t641    o601 b640
 B       b640    s640  
 T       t641    o618 b640  
1665  B       b641    t641  B       b641    t641
1666  T       t642    o620 b562  T       t209    o627 b208 b578 b641
1667  S       s642    t620 h  B       b209    t209
1668  G       s642    t642  T       t210    o200 b209
1669  B       b642    s642  B       b210    t210
1670  T       t643    o618 b642  P       p217    Number 1118
1671  B       b643    t643  P       p219    Number 1216
1672  T       t644    o635 b641 b643  O       o219    location p217 p219
1673  B       b644    t644  P       p645    String inv_df
1674  T       t645    o635 b639 b644  O       o645    dform p645
1675  B       b645    t645  P       p646    String inv(
1676  P       p534    Number 1060  O       o646    string602 p646
1677  P       p535    Number 1067  T       t646    o646
1678  O       o535    resource_defs p534 p535 p264  B       b646    t646
1679  P       p536    Number 1065  T       t647    o602 b589
1680  O       o536    uid p536 p535  B       b647    t647
1681  T       t538    o536 b626  T       t648    o b647 b613
1682  B       b538    t538  B       b648    t648
1683  T       t539    o b538 b4  T       t649    o b632 b648
1684  B       b539    t539  B       b649    t649
1685  T       t545    o535 b539  T       t650    o b602 b649
1686  B       b545    t545  B       b650    t650
1687  T       t546    o b545 b4  T       t651    o b646 b650
1688  B       b546    t546  B       b651    t651
1689  T       t552    o634 b618 b645 b623 b546  T       t652    o601 b651
1690  B       b552    t552  B       b652    t652
1691  T       t553    o534 b552  T       t653    o645 b630 b590 b652
1692  B       b553    t553  B       b653    t653
1693  P       p554    Number 1215  T       t229    o219 b653
1694  P       p555    Number 1485  B       b229    t229
1695  O       o555    location p554 p555  P       p234    Number 1218
1696  P       p654    String op_wf2  P       p235    Number 1344
1697  O       o654    rule p654  O       o235    location p234 p235
1698  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  P       p656    String eqElem_df
1699  NCzf_itt_member!mem     mem     mem Czf_itt_member  O       o656    dform p656
1700  O       o655    mem  P       p657    String eq(
1701  T       t655    o655 b560 b554  O       o657    string602 p657
1702  S       s655    t620 h  T       t657    o657
1703  G       s655    t655  B       b657    t657
1704  B       b655    s655  T       t658    o b657 b639
 T       t656    o618 b655  
 B       b656    t656  
 T       t657    o655 b561 b554  
 S       s657    t620 h  
 G       s657    t657  
 B       b657    s657  
 T       t658    o618 b657  
1705  B       b658    t658  B       b658    t658
1706  T       t659    o655 b562 b554  T       t659    o601 b658
1707  S       s659    t620 h  B       b659    t659
1708  G       s659    t659  T       t660    o656 b630 b595 b659
 B       b659    s659  
 T       t660    o618 b659  
1709  B       b660    t660  B       b660    t660
1710  T       t661    o635 b658 b660  T       t240    o235 b660
1711  B       b661    t661  B       b240    t240
1712  T       t662    o635 b656 b661  P       p247    Number 1363
1713  B       b662    t662  P       p262    Number 1497
1714  T       t663    o635 b641 b662  O       o262    location p247 p262
1715  B       b663    t663  NSummary!rule   rule    rule Summary
1716  T       t664    o635 b639 b663  P       p663    String group_type
1717    O       o663    rule p663
1718    NSummary!context_param  context_param   context_param Summary
1719    P       p664    String H
1720    O       o664    context_param p664
1721    T       t664    o664
1722  B       b664    t664  B       b664    t664
1723  P       p561    Number 1237  T       t665    o b664 b4
 P       p562    Number 1244  
 O       o562    resource_defs p561 p562 p264  
 P       p563    Number 1242  
 O       o563    uid p563 p562  
 T       t565    o563 b626  
 B       b565    t565  
 T       t665    o b565 b4  
1724  B       b665    t665  B       b665    t665
1725  T       t672    o562 b665  NSummary!meta_implies   meta_implies    meta_implies Summary
1726    O       o665    meta_implies
1727    NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1728    O       o666    meta_theorem
1729    NBase_trivial   Base_trivial    Base_trivial NIL
1730    NBase_trivial!squash    squash  squash Base_trivial
1731    O       o667    squash
1732    T       t667    o667
1733    B       b667    t667
1734    T       t668    o b667 b4
1735    C       h       H
1736    NItt_equal      Itt_equal       Itt_equal NIL
1737    NItt_equal!equal        equal   equal Itt_equal
1738    O       o668    equal
1739    NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1740    NItt_record_label0!label        label   label Itt_record_label0
1741    O       o669    label
1742    T       t669    o669
1743    B       b669    t669
1744    T       t670    o668 b669 b564 b564
1745    S       s       t668 h
1746    G       s       t670
1747    B       b670    s
1748    T       t671    o666 b670
1749    B       b671    t671
1750    P       p671    Var ext
1751    O       o671    var p671
1752    T       t672    o671
1753  B       b672    t672  B       b672    t672
1754  T       t688    o b672 b4  T       t673    o b672 b4
1755  B       b688    t688  NItt_equal!type type    type Itt_equal
1756  T       t689    o654 b618 b664 b623 b688  O       o673    type
1757  B       b689    t689  T       t674    o673 b565
1758  T       t690    o555 b689  S       s674    t673 h
1759  B       b690    t690  G       s674    t674
1760  P       p690    Number 1574  B       b674    s674
1761  O       o690    location p690 p269  T       t675    o666 b674
1762  P       p673    String op_eq1  B       b675    t675
1763  O       o673    rule p673  T       t676    o665 b671 b675
 P       p674    Var s3  
 O       o674    var p674  
 T       t674    o674  
 B       b674    t674  
 T       t675    o620 b674  
 S       s675    t637 h  
 G       s675    t675  
 B       b675    s675  
 T       t676    o618 b675  
1764  B       b676    t676  B       b676    t676
1765  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  NSummary!incomplete     incomplete      incomplete Summary
1766  NCzf_itt_eq!eq  eq      eq Czf_itt_eq  O       o676    incomplete
1767  O       o676    eq  T       t677    o676
1768  T       t677    o676 b560 b561  B       b677    t677
1769  S       s677    t620 h  NSummary!resource_defs  resource_defs   resource_defs Summary
1770  G       s677    t677  P       p263    Number 1389
1771  B       b677    s677  P       p264    Number 1397
1772  T       t678    o618 b677  O       o264    resource_defs p263 p264 p204
1773  B       b678    t678  NOcaml!uid      uid     uid Ocaml
1774  T       t679    o559 b674 b560  P       p265    Number 1395
1775  B       b679    t679  O       o265    uid p265 p264
1776  T       t680    o559 b674 b561  P       p680    String []
1777    O       o680    uid p680
1778    T       t680    o680
1779  B       b680    t680  B       b680    t680
1780  T       t681    o676 b679 b680  T       t267    o265 b680
1781  S       s681    t620 h  B       b267    t267
1782  G       s681    t681  T       t271    o b267 b4
1783  B       b681    s681  B       b271    t271
1784  T       t682    o618 b681  T       t272    o264 b271
1785  B       b682    t682  B       b272    t272
1786  T       t683    o635 b678 b682  T       t275    o b272 b4
1787  B       b683    t683  B       b275    t275
1788  T       t684    o635 b676 b683  T       t279    o663 b665 b676 b677 b275
1789  B       b684    t684  B       b279    t279
1790  T       t685    o635 b641 b684  T       t280    o262 b279
1791  B       b685    t685  B       b280    t280
1792  T       t686    o635 b639 b685  P       p284    Number 1499
1793  B       b686    t686  P       p285    Number 1667
1794  P       p691    Number 1596  O       o285    location p284 p285
1795  P       p692    Number 1603  P       p688    String car_wf
1796  O       o692    resource_defs p691 p692 p264  O       o688    rule p688
1797  P       p693    Number 1601  S       s688    t673 h
1798  O       o693    uid p693 p692  G       s688    t565
1799  T       t693    o693 b626  B       b688    s688
1800  B       b693    t693  T       t688    o666 b688
1801  T       t704    o b693 b4  B       b689    t688
1802  B       b704    t704  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL
1803  T       t705    o692 b704  NCzf_itt_set!isset      isset   isset Czf_itt_set
1804    O       o689    isset
1805    T       t689    o689 b570
1806    S       s689    t673 h
1807    G       s689    t689
1808    B       b690    s689
1809    T       t690    o666 b690
1810    B       b691    t690
1811    T       t691    o665 b689 b691
1812    B       b692    t691
1813    T       t692    o665 b671 b692
1814    B       b693    t692
1815    P       p286    Number 1521
1816    P       p287    Number 1528
1817    O       o287    resource_defs p286 p287 p204
1818    P       p288    Number 1526
1819    O       o288    uid p288 p287
1820    T       t299    o288 b680
1821    B       b299    t299
1822    T       t368    o b299 b4
1823    B       b368    t368
1824    T       t379    o287 b368
1825    B       b379    t379
1826    T       t394    o b379 b4
1827    B       b394    t394
1828    T       t400    o688 b665 b693 b677 b394
1829    B       b400    t400
1830    T       t401    o285 b400
1831    B       b401    t401
1832    P       p401    Number 1669
1833    P       p403    Number 1936
1834    O       o404    location p401 p403
1835    P       p702    String op_wf1
1836    O       o702    rule p702
1837    T       t702    o689 b576
1838    S       s702    t668 h
1839    G       s702    t702
1840    B       b702    s702
1841    T       t703    o666 b702
1842    B       b703    t703
1843    T       t704    o689 b577
1844    S       s704    t668 h
1845    G       s704    t704
1846    B       b704    s704
1847    T       t705    o666 b704
1848  B       b705    t705  B       b705    t705
1849  T       t706    o b705 b4  T       t706    o689 b578
1850  B       b706    t706  S       s706    t673 h
1851  T       t707    o673 b618 b686 b623 b706  G       s706    t706
1852    B       b706    s706
1853    T       t707    o666 b706
1854  B       b707    t707  B       b707    t707
1855  T       t708    o690 b707  T       t708    o665 b705 b707
1856  B       b708    t708  B       b708    t708
1857  P       p708    Number 1853  T       t709    o665 b703 b708
1858  P       p709    Number 2130  B       b709    t709
1859  O       o709    location p708 p709  T       t710    o665 b689 b709
1860  P       p695    String op_eq2  B       b710    t710
1861  O       o695    rule p695  T       t711    o665 b671 b710
 T       t695    o559 b560 b674  
 B       b695    t695  
 T       t696    o559 b561 b674  
 B       b696    t696  
 T       t697    o676 b695 b696  
 S       s697    t620 h  
 G       s697    t697  
 B       b697    s697  
 T       t698    o618 b697  
 B       b698    t698  
 T       t699    o635 b678 b698  
 B       b699    t699  
 T       t700    o635 b676 b699  
 B       b700    t700  
 T       t701    o635 b641 b700  
 B       b701    t701  
 T       t702    o635 b639 b701  
 B       b702    t702  
 P       p712    Number 1875  
 P       p713    Number 1882  
 O       o713    resource_defs p712 p713 p264  
 P       p714    Number 1880  
 O       o714    uid p714 p713  
 T       t718    o714 b626  
 B       b718    t718  
 T       t719    o b718 b4  
 B       b719    t719  
 T       t720    o713 b719  
 B       b720    t720  
 T       t721    o b720 b4  
 B       b721    t721  
 T       t722    o695 b618 b702 b623 b721  
 B       b722    t722  
 T       t723    o709 b722  
 B       b723    t723  
 P       p723    Number 2132  
 P       p724    Number 2265  
 O       o724    location p723 p724  
 P       p710    String op_fun1  
 O       o710    rule p710  
 T       t710    o620 b573  
 S       s710    t637 h  
 G       s710    t710  
 B       b710    s710  
 T       t711    o618 b710  
1862  B       b711    t711  B       b711    t711
1863  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq  P       p404    Number 1691
1864  O       o711    fun_set  P       p405    Number 1698
1865  P       p711    Var z  O       o405    resource_defs p404 p405 p204
1866  O       o712    var p711  P       p406    Number 1696
1867  T       t712    o712  O       o406    uid p406 p405
1868  B       b712    t712  T       t408    o406 b680
1869  T       t713    o559 b712 b573  B       b408    t408
1870  B       b713    t713 z  T       t409    o b408 b4
1871  T       t714    o711 b713  B       b409    t409
1872  S       s714    t620 h  T       t415    o405 b409
1873  G       s714    t714  B       b415    t415
1874  B       b714    s714  T       t416    o b415 b4
1875  T       t715    o618 b714  B       b416    t416
1876  B       b715    t715  T       t425    o702 b665 b711 b677 b416
1877  T       t716    o635 b711 b715  B       b425    t425
1878  B       b716    t716  T       t426    o404 b425
1879  P       p726    Number 2155  B       b426    t426
1880  P       p727    Number 2162  P       p427    Number 1938
1881  O       o727    resource_defs p726 p727 p264  P       p428    Number 2312
1882  P       p728    Number 2160  O       o428    location p427 p428
1883  O       o728    uid p728 p727  P       p720    String op_wf2
1884  T       t730    o728 b626  O       o720    rule p720
1885    NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1886    NCzf_itt_member!mem     mem     mem Czf_itt_member
1887    O       o721    mem
1888    T       t721    o721 b576 b570
1889    S       s721    t673 h
1890    G       s721    t721
1891    B       b721    s721
1892    T       t722    o666 b721
1893    B       b722    t722
1894    T       t723    o721 b577 b570
1895    S       s723    t673 h
1896    G       s723    t723
1897    B       b723    s723
1898    T       t724    o666 b723
1899    B       b724    t724
1900    T       t725    o721 b578 b570
1901    S       s725    t673 h
1902    G       s725    t725
1903    B       b725    s725
1904    T       t726    o666 b725
1905    B       b726    t726
1906    T       t727    o665 b724 b726
1907    B       b727    t727
1908    T       t728    o665 b722 b727
1909    B       b728    t728
1910    T       t729    o665 b689 b728
1911    B       b729    t729
1912    T       t730    o665 b671 b729
1913  B       b730    t730  B       b730    t730
1914  T       t731    o b730 b4  T       t731    o665 b705 b730
1915  B       b731    t731  B       b731    t731
1916  T       t732    o727 b731  T       t732    o665 b703 b731
1917  B       b732    t732  B       b732    t732
1918  T       t733    o b732 b4  P       p429    Number 1960
1919  B       b733    t733  P       p430    Number 1967
1920  T       t734    o710 b618 b716 b623 b733  O       o430    resource_defs p429 p430 p204
1921  B       b734    t734  P       p431    Number 1965
1922  T       t735    o724 b734  O       o431    uid p431 p430
1923  B       b735    t735  T       t434    o431 b680
1924  P       p735    Number 2267  B       b434    t434
1925  P       p736    Number 2400  T       t435    o b434 b4
1926  O       o736    location p735 p736  B       b435    t435
1927  P       p725    String op_fun2  T       t443    o430 b435
1928  O       o725    rule p725  B       b443    t443
1929  T       t725    o559 b573 b712  T       t444    o b443 b4
1930  B       b725    t725 z  B       b444    t444
1931  T       t726    o711 b725  T       t452    o720 b665 b732 b677 b444
1932  S       s726    t620 h  B       b452    t452
1933  G       s726    t726  T       t453    o428 b452
1934  B       b726    s726  B       b453    t453
1935  T       t727    o618 b726  P       p454    Number 2401
1936  B       b727    t727  P       p455    Number 2774
1937  T       t728    o635 b711 b727  O       o455    location p454 p455
1938  B       b728    t728  P       p741    String op_eq1
1939  P       p738    Number 2290  O       o741    rule p741
1940  P       p739    Number 2297  P       p742    Var s3
1941  O       o739    resource_defs p738 p739 p264  O       o742    var p742
1942  P       p740    Number 2295  T       t742    o742
1943  O       o740    uid p740 p739  B       b742    t742
1944  T       t750    o740 b626  T       t743    o689 b742
1945    S       s743    t668 h
1946    G       s743    t743
1947    B       b743    s743
1948    T       t744    o666 b743
1949    B       b744    t744
1950    NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
1951    NCzf_itt_eq!eq  eq      eq Czf_itt_eq
1952    O       o744    eq
1953    T       t745    o744 b576 b577
1954    S       s745    t673 h
1955    G       s745    t745
1956    B       b745    s745
1957    T       t746    o666 b745
1958    B       b746    t746
1959    T       t747    o575 b564 b742 b576
1960    B       b747    t747
1961    T       t748    o575 b564 b742 b577
1962    B       b748    t748
1963    T       t749    o744 b747 b748
1964    S       s749    t673 h
1965    G       s749    t749
1966    B       b749    s749
1967    T       t750    o666 b749
1968  B       b750    t750  B       b750    t750
1969  T       t751    o b750 b4  T       t751    o665 b746 b750
1970  B       b751    t751  B       b751    t751
1971  T       t752    o739 b751  T       t752    o665 b689 b751
1972  B       b752    t752  B       b752    t752
1973  T       t753    o b752 b4  T       t753    o665 b671 b752
1974  B       b753    t753  B       b753    t753
1975  T       t754    o725 b618 b728 b623 b753  T       t754    o665 b744 b753
1976  B       b754    t754  B       b754    t754
1977  T       t755    o736 b754  T       t755    o665 b705 b754
1978  B       b755    t755  B       b755    t755
1979  P       p755    Number 2402  T       t756    o665 b703 b755
1980  P       p758    Number 2795  B       b756    t756
1981  O       o758    location p755 p758  P       p456    Number 2423
1982  P       p737    String op_assoc1  P       p457    Number 2430
1983  O       o737    rule p737  O       o457    resource_defs p456 p457 p204
1984  T       t737    o655 b674 b554  P       p458    Number 2428
1985  S       s737    t620 h  O       o458    uid p458 p457
1986  G       s737    t737  T       t461    o458 b680
1987  B       b737    s737  B       b461    t461
1988  T       t738    o618 b737  T       t462    o b461 b4
1989  B       b738    t738  B       b462    t462
1990  NCzf_itt_eq!equal       equal   equal Czf_itt_eq  T       t470    o457 b462
1991  O       o738    equal  B       b470    t470
1992  T       t739    o559 b562 b674  T       t471    o b470 b4
1993  B       b739    t739  B       b471    t471
1994  T       t740    o559 b560 b696  T       t479    o741 b665 b756 b677 b471
1995  B       b740    t740  B       b479    t479
1996  T       t741    o738 b739 b740  T       t480    o455 b479
1997  S       s741    t620 h  B       b480    t480
1998  G       s741    t741  P       p481    Number 2776
1999  B       b741    s741  P       p482    Number 3149
2000  T       t742    o618 b741  O       o482    location p481 p482
2001  B       b742    t742  P       p765    String op_eq2
2002  T       t743    o635 b738 b742  O       o765    rule p765
2003  B       b743    t743  T       t765    o575 b564 b576 b742
2004  T       t744    o635 b658 b743  B       b765    t765
2005  B       b744    t744  T       t766    o575 b564 b577 b742
 T       t745    o635 b656 b744  
 B       b745    t745  
 T       t746    o635 b676 b745  
 B       b746    t746  
 T       t747    o635 b641 b746  
 B       b747    t747  
 T       t748    o635 b639 b747  
 B       b748    t748  
 P       p759    Number 2427  
 P       p760    Number 2434  
 O       o760    resource_defs p759 p760 p264  
 P       p761    Number 2432  
 O       o761    uid p761 p760  
 T       t766    o761 b626  
2006  B       b766    t766  B       b766    t766
2007  T       t767    o b766 b4  T       t767    o744 b765 b766
2008  B       b767    t767  S       s767    t673 h
2009  T       t768    o760 b767  G       s767    t767
2010    B       b767    s767
2011    T       t768    o666 b767
2012  B       b768    t768  B       b768    t768
2013  T       t769    o b768 b4  T       t769    o665 b746 b768
2014  B       b769    t769  B       b769    t769
2015  T       t770    o737 b618 b748 b623 b769  T       t770    o665 b689 b769
2016  B       b770    t770  B       b770    t770
2017  T       t771    o758 b770  T       t771    o665 b671 b770
2018  B       b771    t771  B       b771    t771
2019  P       p771    Number 2797  T       t772    o665 b744 b771
2020  P       p772    Number 3190  B       b772    t772
2021  O       o772    location p771 p772  T       t773    o665 b705 b772
2022  P       p757    String op_assoc2  B       b773    t773
2023  O       o757    rule p757  T       t774    o665 b703 b773
 T       t757    o738 b740 b739  
 S       s757    t620 h  
 G       s757    t757  
 B       b757    s757  
 T       t758    o618 b757  
 B       b758    t758  
 T       t759    o635 b738 b758  
 B       b759    t759  
 T       t760    o635 b658 b759  
 B       b760    t760  
 T       t761    o635 b656 b760  
 B       b761    t761  
 T       t762    o635 b676 b761  
 B       b762    t762  
 T       t763    o635 b641 b762  
 B       b763    t763  
 T       t764    o635 b639 b763  
 B       b764    t764  
 P       p774    Number 2822  
 P       p775    Number 2829  
 O       o775    resource_defs p774 p775 p264  
 P       p776    Number 2827  
 O       o776    uid p776 p775  
 T       t776    o776 b626  
 B       b776    t776  
 T       t777    o b776 b4  
 B       b777    t777  
 T       t778    o775 b777  
 B       b778    t778  
 T       t779    o b778 b4  
 B       b779    t779  
 T       t780    o757 b618 b764 b623 b779  
 B       b780    t780  
 T       t781    o772 b780  
 B       b781    t781  
 P       p781    Number 3192  
 P       p782    Number 3268  
 O       o782    location p781 p782  
 P       p773    String id_wf1  
 O       o773    rule p773  
 T       t773    o620 b567  
 S       s773    t620 h  
 G       s773    t773  
 B       b773    s773  
 T       t774    o618 b773  
2024  B       b774    t774  B       b774    t774
2025  P       p784    Number 3214  P       p483    Number 2798
2026  P       p785    Number 3222  P       p484    Number 2805
2027  O       o785    resource_defs p784 p785 p264  O       o484    resource_defs p483 p484 p204
2028  P       p786    Number 3220  P       p485    Number 2803
2029  O       o786    uid p786 p785  O       o485    uid p485 p484
2030  T       t786    o786 b626  T       t488    o485 b680
2031  B       b786    t786  B       b488    t488
2032  T       t787    o b786 b4  T       t489    o b488 b4
2033  B       b787    t787  B       b489    t489
2034  T       t788    o785 b787  T       t495    o484 b489
2035  B       b788    t788  B       b495    t495
2036  T       t789    o b788 b4  T       t496    o b495 b4
2037  B       b789    t789  B       b496    t496
2038  T       t790    o773 b618 b774 b623 b789  T       t502    o765 b665 b774 b677 b496
2039  B       b790    t790  B       b502    t502
2040  T       t791    o782 b790  T       t503    o482 b502
2041  B       b791    t791  B       b503    t503
2042  P       p791    Number 3270  P       p504    Number 3151
2043  P       p792    Number 3348  P       p505    Number 3288
2044  O       o792    location p791 p792  O       o505    location p504 p505
2045  P       p783    String id_wf2  P       p783    String op_fun1
2046  O       o783    rule p783  O       o783    rule p783
2047  T       t783    o655 b567 b554  T       t783    o689 b589
2048  S       s783    t620 h  S       s783    t668 h
2049  G       s783    t783  G       s783    t783
2050  B       b783    s783  B       b783    s783
2051  T       t784    o618 b783  T       t784    o666 b783
2052  B       b784    t784  B       b784    t784
2053  P       p795    Number 3292  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq
2054  P       p796    Number 3299  O       o784    fun_set
2055  O       o796    resource_defs p795 p796 p264  P       p784    Var z
2056  P       p797    Number 3297  O       o785    var p784
2057  O       o797    uid p797 p796  T       t785    o785
2058  T       t801    o797 b626  B       b785    t785
2059    T       t786    o575 b564 b785 b589
2060    B       b786    t786 z
2061    T       t787    o784 b786
2062    S       s787    t673 h
2063    G       s787    t787
2064    B       b787    s787
2065    T       t788    o666 b787
2066    B       b788    t788
2067    T       t789    o665 b784 b788
2068    B       b789    t789
2069    P       p506    Number 3174
2070    P       p507    Number 3181
2071    O       o507    resource_defs p506 p507 p204
2072    P       p511    Number 3179
2073    O       o512    uid p511 p507
2074    T       t517    o512 b680
2075    B       b517    t517
2076    T       t518    o b517 b4
2077    B       b518    t518
2078    T       t525    o507 b518
2079    B       b525    t525
2080    T       t526    o b525 b4
2081    B       b526    t526
2082    T       t533    o783 b665 b789 b677 b526
2083    B       b533    t533
2084    T       t534    o505 b533
2085    B       b534    t534
2086    P       p534    Number 3290
2087    P       p535    Number 3427
2088    O       o536    location p534 p535
2089    P       p798    String op_fun2
2090    O       o798    rule p798
2091    T       t798    o575 b564 b589 b785
2092    B       b798    t798 z
2093    T       t799    o784 b798
2094    S       s799    t673 h
2095    G       s799    t799
2096    B       b799    s799
2097    T       t800    o666 b799
2098    B       b800    t800
2099    T       t801    o665 b784 b800
2100  B       b801    t801  B       b801    t801
2101  T       t802    o b801 b4  P       p536    Number 3313
2102  B       b802    t802  P       p537    Number 3320
2103  T       t803    o796 b802  O       o537    resource_defs p536 p537 p204
2104  B       b803    t803  P       p538    Number 3318
2105  T       t804    o b803 b4  O       o538    uid p538 p537
2106  B       b804    t804  T       t540    o538 b680
2107  T       t805    o783 b618 b784 b623 b804  B       b540    t540
2108  B       b805    t805  T       t541    o b540 b4
2109  T       t806    o792 b805  B       b541    t541
2110  B       b806    t806  T       t547    o537 b541
2111  P       p806    Number 3350  B       b547    t547
2112  P       p807    Number 3526  T       t548    o b547 b4
2113  O       o807    location p806 p807  B       b548    t548
2114  P       p793    String id_eq1  T       t554    o798 b665 b801 b677 b548
2115  O       o793    rule p793  B       b554    t554
2116  T       t793    o655 b573 b554  T       t555    o536 b554
2117  S       s793    t620 h  B       b555    t555
2118  G       s793    t793  P       p555    Number 3429
2119  B       b793    s793  P       p556    Number 3938
2120  T       t794    o618 b793  O       o557    location p555 p556
2121  B       b794    t794  P       p810    String op_assoc1
2122  T       t795    o559 b567 b573  O       o810    rule p810
2123  B       b795    t795  T       t810    o721 b742 b570
2124  T       t796    o738 b795 b573  S       s810    t673 h
2125  S       s796    t620 h  G       s810    t810
2126  G       s796    t796  B       b810    s810
2127  B       b796    s796  T       t811    o666 b810
2128  T       t797    o618 b796  B       b811    t811
2129  B       b797    t797  NCzf_itt_eq!equal       equal811        equal Czf_itt_eq
2130  T       t798    o635 b794 b797  O       o811    equal811
2131  B       b798    t798  T       t812    o575 b564 b578 b742
2132  T       t799    o635 b711 b798  B       b812    t812
2133  B       b799    t799  T       t813    o575 b564 b576 b766
2134  P       p809    Number 3372  B       b813    t813
2135  P       p810    Number 3379  T       t814    o811 b812 b813
2136  O       o810    resource_defs p809 p810 p264  S       s814    t673 h
2137  P       p811    Number 3377  G       s814    t814
2138  O       o811    uid p811 p810  B       b814    s814
2139  T       t814    o811 b626  T       t815    o666 b814
 B       b814    t814  
 T       t815    o b814 b4  
2140  B       b815    t815  B       b815    t815
2141  T       t816    o810 b815  T       t816    o665 b811 b815
2142  B       b816    t816  B       b816    t816
2143  T       t817    o b816 b4  T       t817    o665 b724 b816
2144  B       b817    t817  B       b817    t817
2145  T       t818    o793 b618 b799 b623 b817  T       t818    o665 b722 b817
2146  B       b818    t818  B       b818    t818
2147  T       t819    o807 b818  T       t819    o665 b689 b818
2148  B       b819    t819  B       b819    t819
2149  P       p819    Number 3528  T       t820    o665 b671 b819
2150  P       p820    Number 3704  B       b820    t820
2151  O       o820    location p819 p820  T       t821    o665 b744 b820
2152  P       p808    String id_eq2  B       b821    t821
2153  O       o808    rule p808  T       t822    o665 b705 b821
2154  T       t808    o559 b573 b567  B       b822    t822
2155  B       b808    t808  T       t823    o665 b703 b822
 T       t809    o738 b808 b573  
 S       s809    t620 h  
 G       s809    t809  
 B       b809    s809  
 T       t810    o618 b809  
 B       b810    t810  
 T       t811    o635 b794 b810  
 B       b811    t811  
 T       t812    o635 b711 b811  
 B       b812    t812  
 P       p821    Number 3550  
 P       p822    Number 3557  
 O       o822    resource_defs p821 p822 p264  
 P       p823    Number 3555  
 O       o823    uid p823 p822  
 T       t823    o823 b626  
2156  B       b823    t823  B       b823    t823
2157  T       t824    o b823 b4  P       p557    Number 3454
2158  B       b824    t824  P       p558    Number 3461
2159  T       t832    o822 b824  O       o558    resource_defs p557 p558 p204
2160  B       b832    t832  P       p559    Number 3459
2161  T       t837    o b832 b4  O       o559    uid p559 p558
2162    T       t561    o559 b680
2163    B       b561    t561
2164    T       t562    o b561 b4
2165    B       b562    t562
2166    T       t563    o558 b562
2167    B       b563    t563
2168    T       t568    o b563 b4
2169    B       b568    t568
2170    T       t569    o810 b665 b823 b677 b568
2171    B       b569    t569
2172    T       t573    o557 b569
2173    B       b573    t573
2174    P       p577    Number 3940
2175    P       p578    Number 4449
2176    O       o578    location p577 p578
2177    P       p832    String op_assoc2
2178    O       o832    rule p832
2179    T       t832    o811 b813 b812
2180    S       s832    t673 h
2181    G       s832    t832
2182    B       b832    s832
2183    T       t833    o666 b832
2184    B       b833    t833
2185    T       t834    o665 b811 b833
2186    B       b834    t834
2187    T       t835    o665 b724 b834
2188    B       b835    t835
2189    T       t836    o665 b722 b835
2190    B       b836    t836
2191    T       t837    o665 b689 b836
2192  B       b837    t837  B       b837    t837
2193  T       t839    o808 b618 b812 b623 b837  T       t838    o665 b671 b837
2194    B       b838    t838
2195    T       t839    o665 b744 b838
2196  B       b839    t839  B       b839    t839
2197  T       t840    o820 b839  T       t840    o665 b705 b839
2198  B       b840    t840  B       b840    t840
2199  P       p840    Number 3706  T       t841    o665 b703 b840
 P       p842    Number 3879  
 O       o842    location p840 p842  
 NOcaml!str_let  str_let str_let Ocaml  
 NOcaml!patt_var patt_var        patt_var Ocaml  
 NOcaml!patt_done        patt_done       patt_done Ocaml  
 NOcaml!fun      fun     fun Ocaml  
 NOcaml!patt_if  patt_if patt_if Ocaml  
 NOcaml!patt_body        patt_body       patt_body Ocaml  
 NOcaml!apply    apply   apply Ocaml  
 NOcaml!lid      lid     lid Ocaml  
 NOcaml!proj     proj    proj Ocaml  
 O       o836    uid p509  
 T       t836    o836  
 B       b836    t836  
 P       p838    String hyp_count_addr  
 O       o838    lid p838  
 T       t838    o838  
 B       b838    t838  
 P       p841    Var p  
 O       o841    var p841  
 T       t841    o841  
2200  B       b841    t841  B       b841    t841
2201  P       p857    String inv_wf1  P       p579    Number 3965
2202  O       o857    rule p857  P       p583    Number 3972
2203  T       t857    o572 b560  O       o584    resource_defs p579 p583 p204
2204  B       b857    t857  P       p584    Number 3970
2205  T       t858    o620 b857  O       o585    uid p584 p583
2206  S       s858    t620 h  T       t586    o585 b680
2207  G       s858    t858  B       b586    t586
2208  B       b858    s858  T       t587    o b586 b4
2209  T       t859    o618 b858  B       b587    t587
2210  B       b859    t859  T       t588    o584 b587
2211  T       t860    o635 b656 b859  B       b588    t588
2212  B       b860    t860  T       t593    o b588 b4
2213  T       t861    o635 b639 b860  B       b593    t593
2214  B       b861    t861  T       t594    o832 b665 b841 b677 b593
2215  P       p843    Number 3729  B       b594    t594
2216  P       p844    Number 3736  T       t598    o578 b594
2217  O       o844    resource_defs p843 p844 p264  B       b598    t598
2218  P       p845    Number 3734  P       p601    Number 4451
2219  O       o845    uid p845 p844  P       p603    Number 4619
2220  T       t845    o845 b626  O       o604    location p601 p603
2221  B       b845    t845  P       p850    String id_wf1
2222  T       t846    o b845 b4  O       o850    rule p850
2223  B       b846    t846  T       t850    o689 b583
2224  T       t847    o844 b846  S       s850    t673 h
2225  B       b847    t847  G       s850    t850
2226  T       t848    o b847 b4  B       b850    s850
2227  B       b848    t848  T       t851    o666 b850
2228  T       t849    o857 b618 b861 b623 b848  B       b851    t851
2229  B       b849    t849  T       t852    o665 b689 b851
2230  T       t850    o842 b849  B       b852    t852
2231  B       b850    t850  T       t853    o665 b671 b852
2232  P       p850    Number 3881  B       b853    t853
2233  P       p851    Number 4057  P       p604    Number 4473
2234  O       o851    location p850 p851  P       p605    Number 4481
2235  P       p870    String inv_wf2  O       o605    resource_defs p604 p605 p204
2236  O       o870    rule p870  P       p606    Number 4479
2237  T       t870    o655 b857 b554  O       o606    uid p606 p605
2238  S       s870    t620 h  T       t609    o606 b680
2239  G       s870    t870  B       b609    t609
2240  B       b870    s870  T       t610    o b609 b4
2241  T       t871    o618 b870  B       b610    t610
2242  B       b871    t871  T       t619    o605 b610
2243  T       t872    o635 b656 b871  B       b619    t619
2244  B       b872    t872  T       t620    o b619 b4
2245  T       t873    o635 b639 b872  B       b620    t620
2246  B       b873    t873  T       t626    o850 b665 b853 b677 b620
2247  P       p852    Number 3904  B       b626    t626
2248  P       p853    Number 3911  T       t627    o604 b626
2249  O       o853    resource_defs p852 p853 p264  B       b627    t627
2250  P       p854    Number 3909  P       p628    Number 4621
2251  O       o854    uid p854 p853  P       p629    Number 4795
2252  T       t854    o854 b626  O       o629    location p628 p629
2253  B       b854    t854  P       p862    String id_wf2
2254  T       t855    o b854 b4  O       o862    rule p862
2255  B       b855    t855  T       t862    o721 b583 b570
2256  T       t856    o853 b855  S       s862    t673 h
2257  B       b856    t856  G       s862    t862
2258  T       t862    o b856 b4  B       b862    s862
2259  B       b862    t862  T       t863    o666 b862
 T       t863    o870 b618 b873 b623 b862  
2260  B       b863    t863  B       b863    t863
2261  T       t864    o851 b863  T       t864    o665 b689 b863
2262  B       b864    t864  B       b864    t864
2263  P       p864    Number 4059  T       t865    o665 b671 b864
2264  P       p865    Number 4146  B       b865    t865
2265  O       o865    location p864 p865  P       p632    Number 4643
2266  P       p882    String inv_fun1  P       p633    Number 4650
2267  O       o882    rule p882  O       o633    resource_defs p632 p633 p204
2268  T       t882    o572 b712  P       p634    Number 4648
2269  B       b882    t882 z  O       o634    uid p634 p633
2270  T       t883    o711 b882  T       t644    o634 b680
2271  S       s883    t620 h  B       b644    t644
2272  G       s883    t883  T       t645    o b644 b4
2273  B       b883    s883  B       b645    t645
2274  T       t884    o618 b883  T       t655    o633 b645
2275  B       b884    t884  B       b655    t655
2276  P       p866    Number 4083  T       t656    o b655 b4
2277  P       p867    Number 4090  B       b656    t656
2278  O       o867    resource_defs p866 p867 p264  T       t662    o862 b665 b865 b677 b656
2279  P       p868    Number 4088  B       b662    t662
2280  O       o868    uid p868 p867  T       t663    o629 b662
2281  T       t868    o868 b626  B       b663    t663
2282  B       b868    t868  P       p665    Number 4797
2283  T       t869    o b868 b4  P       p666    Number 5073
2284  B       b869    t869  O       o670    location p665 p666
2285  T       t874    o867 b869  P       p874    String id_eq1
2286  B       b874    t874  O       o874    rule p874
2287  T       t875    o b874 b4  T       t874    o721 b589 b570
2288    S       s874    t673 h
2289    G       s874    t874
2290    B       b874    s874
2291    T       t875    o666 b874
2292  B       b875    t875  B       b875    t875
2293  T       t876    o882 b618 b884 b623 b875  T       t876    o575 b564 b583 b589
2294  B       b876    t876  B       b876    t876
2295  T       t877    o865 b876  T       t877    o811 b876 b589
2296  B       b877    t877  S       s877    t673 h
2297  P       p877    Number 4148  G       s877    t877
2298  P       p878    Number 4334  B       b877    s877
2299  O       o878    location p877 p878  T       t878    o666 b877
2300  P       p1840   Number 4366  B       b878    t878
2301  P       p1894   Number 4617  T       t879    o665 b875 b878
2302  P       p893    String inv_id1  B       b879    t879
2303  O       o893    rule p893  T       t880    o665 b689 b879
2304  T       t893    o559 b857 b560  B       b880    t880
2305    T       t881    o665 b671 b880
2306    B       b881    t881
2307    T       t882    o665 b784 b881
2308    B       b882    t882
2309    P       p670    Number 4819
2310    P       p672    Number 4826
2311    O       o672    resource_defs p670 p672 p204
2312    P       p673    Number 4824
2313    O       o674    uid p673 p672
2314    T       t678    o674 b680
2315    B       b678    t678
2316    T       t679    o b678 b4
2317    B       b679    t679
2318    T       t687    o672 b679
2319    B       b687    t687
2320    T       t693    o b687 b4
2321    B       b694    t693
2322    T       t694    o874 b665 b882 b677 b694
2323    B       b701    t694
2324    T       t701    o670 b701
2325    B       b712    t701
2326    P       p714    Number 5075
2327    P       p715    Number 5351
2328    O       o715    location p714 p715
2329    P       p891    String id_eq2
2330    O       o891    rule p891
2331    T       t891    o575 b564 b589 b583
2332    B       b891    t891
2333    T       t892    o811 b891 b589
2334    S       s892    t673 h
2335    G       s892    t892
2336    B       b892    s892
2337    T       t893    o666 b892
2338  B       b893    t893  B       b893    t893
2339  T       t894    o738 b893 b567  T       t894    o665 b875 b893
2340  S       s894    t620 h  B       b894    t894
2341  G       s894    t894  T       t895    o665 b689 b894
 B       b894    s894  
 T       t895    o618 b894  
2342  B       b895    t895  B       b895    t895
2343  T       t896    o635 b656 b895  T       t896    o665 b671 b895
2344  B       b896    t896  B       b896    t896
2345  T       t897    o635 b639 b896  T       t897    o665 b784 b896
2346  B       b897    t897  B       b897    t897
2347  P       p879    Number 4171  P       p716    Number 5097
2348  P       p880    Number 4178  P       p717    Number 5104
2349  O       o880    resource_defs p879 p880 p264  O       o717    resource_defs p716 p717 p204
2350  P       p881    Number 4176  P       p721    Number 5102
2351  O       o881    uid p881 p880  O       o722    uid p721 p717
2352  T       t881    o881 b626  T       t733    o722 b680
2353  B       b881    t881  B       b733    t733
2354  T       t885    o b881 b4  T       t740    o b733 b4
2355  B       b885    t885  B       b740    t740
2356  T       t886    o880 b885  T       t741    o717 b740
2357  B       b886    t886  B       b741    t741
2358  T       t887    o b886 b4  T       t757    o b741 b4
2359  B       b887    t887  B       b757    t757
2360  T       t888    o893 b618 b897 b623 b887  T       t764    o891 b665 b897 b677 b757
2361  B       b888    t888  B       b764    t764
2362  T       t889    o878 b888  T       t775    o715 b764
2363  B       b889    t889  B       b775    t775
2364  P       p889    Number 4336  P       p777    Number 5353
2365  P       p890    Number 4522  P       p778    Number 5622
2366  O       o890    location p889 p890  O       o778    location p777 p778
2367  P       p1907   Number 4619  P       p906    String inv_wf1
 P       p906    String inv_id2  
2368  O       o906    rule p906  O       o906    rule p906
2369  T       t906    o559 b560 b857  T       t906    o588 b564 b576
2370  B       b906    t906  B       b906    t906
2371  T       t907    o738 b906 b567  T       t907    o689 b906
2372  S       s907    t620 h  S       s907    t673 h
2373  G       s907    t907  G       s907    t907
2374  B       b907    s907  B       b907    s907
2375  T       t908    o618 b907  T       t908    o666 b907
2376  B       b908    t908  B       b908    t908
2377  T       t909    o635 b656 b908  T       t909    o665 b722 b908
2378  B       b909    t909  B       b909    t909
2379  T       t910    o635 b639 b909  T       t910    o665 b689 b909
2380  B       b910    t910  B       b910    t910
2381  P       p891    Number 4359  T       t911    o665 b671 b910
2382  O       o891    resource_defs p891 p1840 p264  B       b911    t911
2383  P       p892    Number 4364  T       t912    o665 b703 b911
2384  O       o892    uid p892 p1840  B       b912    t912
2385  T       t892    o892 b626  P       p779    Number 5376
2386  B       b892    t892  P       p780    Number 5383
2387  T       t898    o b892 b4  O       o780    resource_defs p779 p780 p204
2388  B       b898    t898  P       p785    Number 5381
2389  T       t899    o891 b898  O       o786    uid p785 p780
2390  B       b899    t899  T       t790    o786 b680
2391  T       t900    o b899 b4  B       b790    t790
2392  B       b900    t900  T       t797    o b790 b4
2393  T       t901    o906 b618 b910 b623 b900  B       b797    t797
2394  B       b901    t901  T       t802    o780 b797
2395  T       t902    o890 b901  B       b802    t802
2396  B       b902    t902  T       t809    o b802 b4
2397  P       p902    Number 4588  B       b809    t809
2398  P       p903    Number 5014  T       t824    o906 b665 b912 b677 b809
2399  O       o903    location p902 p903  B       b824    t824
2400  P       p919    String cancel1  T       t831    o778 b824
2401  O       o919    rule p919  B       b831    t831
2402  NSummary!term_param     term_param      term_param Summary  P       p833    Number 5624
2403  O       o920    term_param  P       p921    String inv_wf2
2404  T       t920    o920 b560  O       o921    rule p921
2405  B       b920    t920  T       t921    o721 b906 b570
2406  T       t921    o b920 b4  S       s921    t673 h
2407  B       b921    t921  G       s921    t921
2408  T       t922    o b617 b921  B       b921    s921
2409    T       t922    o666 b921
2410  B       b922    t922  B       b922    t922
2411  T       t923    o738 b562 b695  T       t923    o665 b722 b922
2412  S       s923    t620 h  B       b923    t923
2413  G       s923    t923  T       t924    o665 b689 b923
 B       b923    s923  
 T       t924    o618 b923  
2414  B       b924    t924  B       b924    t924
2415  T       t925    o738 b561 b674  T       t925    o665 b671 b924
2416  S       s925    t620 h  B       b925    t925
2417  G       s925    t925  T       t926    o665 b703 b925
 B       b925    s925  
 T       t926    o618 b925  
2418  B       b926    t926  B       b926    t926
2419  T       t927    o635 b924 b926  P       p935    String inv_fun1
2420  B       b927    t927  O       o935    rule p935
2421  T       t928    o635 b738 b927  T       t935    o588 b564 b785
2422  B       b928    t928  B       b935    t935 z
2423  T       t929    o635 b658 b928  T       t936    o784 b935
2424  B       b929    t929  S       s936    t673 h
2425  T       t930    o635 b656 b929  G       s936    t936
2426  B       b930    t930  B       b936    s936
2427  T       t931    o635 b676 b930  T       t937    o666 b936
2428  B       b931    t931  B       b937    t937
2429  T       t932    o635 b641 b931  T       t938    o665 b689 b937
 B       b932    t932  
 T       t933    o635 b639 b932  
 B       b933    t933  
 NSummary!interactive    interactive     interactive Summary  
 O       o933    interactive  
 NSummary!ext_rule       ext_rule        ext_rule Summary  
 P       p933    String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"  
 O       o934    ext_rule p933  
 NSummary!status_incomplete      status_incomplete       status_incomplete Summary  
 O       o935    status_incomplete  
 T       t935    o935  
 B       b935    t935  
 NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  
 O       o936    ext_unjustified  
 NSummary!tactic_arg     tactic_arg      tactic_arg Summary  
 P       p936    String main  
 O       o937    tactic_arg p936  
 NSummary!msequent       msequent        msequent Summary  
 O       o938    msequent  
 T       t938    o b923 b4  
2430  B       b938    t938  B       b938    t938
2431  T       t939    o b737 b938  T       t939    o665 b671 b938
2432  B       b939    t939  B       b939    t939
2433  T       t940    o b657 b939  P       p940    Number 5900
2434  B       b940    t940  O       o833    location p833 p940
2435  T       t941    o b655 b940  P       p834    Number 5647
2436  B       b941    t941  P       p835    Number 5654
2437  T       t942    o b675 b941  O       o835    resource_defs p834 p835 p204
2438  B       b942    t942  P       p836    Number 5652
2439  T       t943    o b640 b942  O       o836    uid p836 p835
2440  B       b943    t943  T       t842    o836 b680
2441  T       t944    o b638 b943  B       b842    t842
2442  B       b944    t944  T       t849    o b842 b4
2443  T       t945    o938 b925 b944  B       b849    t849
2444  B       b945    t945  T       t854    o835 b849
2445  NSummary!parent_none    parent_none     parent_none Summary  B       b854    t854
2446  O       o945    parent_none  T       t861    o b854 b4
2447  T       t946    o945  B       b861    t861
2448  B       b946    t946  T       t866    o921 b665 b926 b677 b861
2449  T       t947    o937 b945 b4 b946  B       b866    t866
2450  B       b947    t947  T       t873    o833 b866
2451  P       p947    String assertion  B       b873    t873
2452  O       o947    tactic_arg p947  P       p875    Number 5902
2453  H       h947    v t923  P       p876    Number 6081
2454  T       t948    o559 b857 b562  O       o876    location p875 p876
2455    P       p877    Number 5926
2456    P       p878    Number 5933
2457    O       o878    resource_defs p877 p878 p204
2458    P       p879    Number 5931
2459    O       o879    uid p879 p878
2460    T       t883    o879 b680
2461    B       b883    t883
2462    T       t890    o b883 b4
2463    B       b890    t890
2464    T       t898    o878 b890
2465    B       b898    t898
2466    T       t905    o b898 b4
2467    B       b905    t905
2468    T       t913    o935 b665 b939 b677 b905
2469    B       b913    t913
2470    T       t920    o876 b913
2471    B       b920    t920
2472    P       p922    Number 6083
2473    P       p923    Number 6373
2474    O       o923    location p922 p923
2475    P       p948    String inv_id1
2476    O       o948    rule p948
2477    T       t948    o575 b564 b906 b576
2478  B       b948    t948  B       b948    t948
2479  T       t949    o559 b857 b695  T       t949    o811 b948 b583
2480  B       b949    t949  S       s949    t673 h
2481  T       t950    o738 b948 b949  G       s949    t949
2482  S       s950    t620 h h947  B       b949    s949
2483  G       s950    t950  T       t950    o666 b949
2484  B       b950    s950  B       b950    t950
2485  T       t951    o938 b950 b944  T       t951    o665 b722 b950
2486  B       b951    t951  B       b951    t951
2487  S       s951    t620 h h947  T       t952    o665 b689 b951
2488  G       s951    t925  B       b952    t952
2489  B       b952    s951  T       t953    o665 b671 b952
2490  T       t952    o938 b952 b944  B       b953    t953
2491  B       b953    t952  T       t954    o665 b703 b953
2492  T       t953    o2 b947  B       b954    t954
2493  B       b954    t953  P       p924    Number 6106
2494  T       t954    o937 b953 b4 b954  P       p925    Number 6113
2495  B       b955    t954  O       o925    resource_defs p924 p925 p204
2496  T       t955    o2 b955  P       p929    Number 6111
2497  B       b956    t955  O       o929    uid p929 p925
2498  T       t956    o947 b951 b4 b956  T       t934    o929 b680
2499  B       b957    t956  B       b934    t934
2500  H       h957    v_1 t950  T       t940    o b934 b4
2501  S       s957    t620 h h947 h957  B       b940    t940
2502  G       s957    t925  T       t947    o925 b940
2503  B       b958    s957  B       b947    t947
2504  T       t958    o938 b958 b944  T       t955    o b947 b4
2505  B       b959    t958  B       b955    t955
2506  T       t959    o937 b959 b4 b956  T       t962    o948 b665 b954 b677 b955
2507  B       b960    t959  B       b962    t962
2508  T       t960    o b960 b4  T       t970    o923 b962
2509  B       b961    t960  B       b970    t970
2510  T       t961    o b957 b961  P       p972    Number 6375
2511  B       b962    t961  P       p973    Number 6665
2512  T       t962    o936 b947 b962  O       o973    location p972 p973
2513  B       b963    t962  P       p963    String inv_id2
2514  P       p963    String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"  O       o963    rule p963
2515  O       o963    ext_rule p963  T       t963    o575 b564 b576 b906
2516  T       t963    o936 b957 b4  B       b963    t963
2517  B       b964    t963  T       t964    o811 b963 b583
2518  T       t964    o963 b935 b964 b4 b4  S       s964    t673 h
2519  B       b965    t964  G       s964    t964
2520  P       p965    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"  B       b964    s964
2521  O       o965    ext_rule p965  T       t965    o666 b964
2522  P       p966    String eq  B       b965    t965
2523  O       o966    tactic_arg p966  T       t966    o665 b722 b965
 T       t966    o559 b893 b561  
2524  B       b966    t966  B       b966    t966
2525  T       t967    o738 b948 b966  T       t967    o665 b689 b966
2526  S       s967    t620 h h947 h957  B       b967    t967
2527  G       s967    t967  T       t968    o665 b671 b967
 B       b967    s967  
 T       t968    o938 b967 b944  
2528  B       b968    t968  B       b968    t968
2529  T       t969    o2 b960  T       t969    o665 b703 b968
2530  B       b969    t969  B       b969    t969
2531  T       t970    o966 b968 b4 b969  P       p974    Number 6398
2532  B       b970    t970  P       p975    Number 6405
2533  T       t971    o738 b966 b949  O       o975    resource_defs p974 p975 p204
2534  H       h971    v_2 t971  P       p979    Number 6403
2535  S       s971    t620 h h947 h957 h971  O       o980    uid p979 p975
2536  G       s971    t925  T       t997    o980 b680
2537  B       b971    s971  B       b997    t997
2538  T       t972    o938 b971 b944  T       t999    o b997 b4
2539  B       b972    t972  B       b999    t999
2540  T       t973    o937 b972 b4 b969  T       t1000   o975 b999
2541  B       b973    t973  B       b1000   t1000
2542  T       t1      o b973 b4  T       t1022   o b1000 b4
2543  B       b1      t1  B       b1073   t1022
2544  T       t2      o b970 b1  T       t1073   o963 b665 b969 b677 b1073
2545  B       b2      t2  B       b1080   t1073
2546  T       t3      o936 b960 b2  T       t1080   o973 b1080
2547  B       b3      t3  B       b1171   t1080
2548  P       p973    String wf  P       p1173   Number 6730
2549  O       o973    tactic_arg p973  P       p1174   Number 7267
2550  B       b974    t949 v_2  O       o1174   location p1173 p1174
2551  T       t974    o711 b974  P       p978    String cancel1
2552  S       s974    t620 h h947 h957  O       o978    rule p978
2553  G       s974    t974  NSummary!term_param     term_param      term_param Summary
2554  B       b975    s974  O       o979    term_param
2555  T       t975    o938 b975 b944  T       t979    o979 b564
2556  B       b976    t975  B       b979    t979
2557  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq  T       t980    o979 b576
 O       o976    fun_prop  
 P       p976    Var v_2  
 O       o977    var p976  
 T       t977    o977  
 B       b977    t977  
 T       t978    o738 b977 b949  
 B       b978    t978 v_2  
 T       t979    o976 b978  
 S       s979    t620 h h947 h957  
 G       s979    t979  
 B       b979    s979  
 T       t980    o938 b979 b944  
2558  B       b980    t980  B       b980    t980
2559  NSummary!arg_named      arg_named       arg_named Summary  T       t981    o b980 b4
 P       p980    String d_auto  
 O       o980    arg_named p980  
 NSummary!arg_bool       arg_bool        arg_bool Summary  
 P       p981    String true  
 O       o981    arg_bool p981  
 T       t981    o981  
2560  B       b981    t981  B       b981    t981
2561  T       t982    o980 b981  T       t982    o b979 b981
2562  B       b982    t982  B       b982    t982
2563  T       t983    o b982 b4  T       t983    o b664 b982
2564  B       b983    t983  B       b983    t983
2565  T       t984    o973 b980 b983 b969  T       t984    o811 b578 b765
2566  B       b984    t984  S       s984    t673 h
2567  T       t985    o2 b984  G       s984    t984
2568    B       b984    s984
2569    T       t985    o666 b984
2570  B       b985    t985  B       b985    t985
2571  T       t986    o973 b976 b4 b985  T       t986    o811 b577 b742
2572  B       b986    t986  S       s986    t673 h
2573  P       p990    String autoT  G       s986    t986
2574  O       o990    ext_rule p990  B       b986    s986
2575  T       t991    o936 b970 b4  T       t987    o666 b986
2576    B       b987    t987
2577    T       t988    o665 b985 b987
2578    B       b988    t988
2579    T       t989    o665 b811 b988
2580    B       b989    t989
2581    T       t990    o665 b724 b989
2582    B       b990    t990
2583    T       t991    o665 b722 b990
2584  B       b991    t991  B       b991    t991
2585  T       t992    o990 b935 b991 b4 b4  T       t992    o665 b689 b991
2586  B       b992    t992  B       b992    t992
2587  P       p992    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"  T       t993    o665 b671 b992
 O       o992    ext_rule p992  
 T       t993    o559 b893 b674  
2588  B       b993    t993  B       b993    t993
2589  T       t994    o738 b949 b993  T       t994    o665 b744 b993
2590  S       s994    t620 h h947 h957 h971  B       b994    t994
2591  G       s994    t994  T       t995    o665 b705 b994
 B       b994    s994  
 T       t995    o938 b994 b944  
2592  B       b995    t995  B       b995    t995
2593  T       t996    o2 b973  T       t996    o665 b703 b995
2594  B       b996    t996  B       b996    t996
2595  T       t997    o966 b995 b4 b996  NSummary!interactive    interactive     interactive Summary
2596  B       b997    t997  O       o996    interactive
2597  T       t998    o738 b966 b993  NSummary!ext_rule       ext_rule        ext_rule Summary
2598  H       h998    v_3 t998  P       p996    String "assumT 9 thenT assertT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenWT autoT"
2599  S       s998    t620 h h947 h957 h971 h998  O       o997    ext_rule p996
2600  G       s998    t925  NSummary!status_incomplete      status_incomplete       status_incomplete Summary
2601  B       b998    s998  O       o998    status_incomplete
2602  T       t999    o938 b998 b944  T       t998    o998
2603  B       b999    t999  B       b998    t998
2604  T       t1000   o937 b999 b4 b996  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
2605  B       b1000   t1000  O       o999    ext_unjustified
2606  T       t214    o b1000 b4  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
2607  B       b214    t214  P       p999    String main
2608  T       t215    o b997 b214  O       o1000   tactic_arg p999
2609  B       b215    t215  NSummary!msequent       msequent        msequent Summary
2610  T       t218    o936 b973 b215  O       o1001   msequent
2611  B       b218    t218  T       t1001   o b984 b4
2612  B       b1001   t966 v_3  B       b1001   t1001
2613  T       t1001   o711 b1001  T       t1002   o b810 b1001
2614  S       s1001   t620 h h947 h957 h971  B       b1002   t1002
2615  G       s1001   t1001  T       t1003   o b723 b1002
2616  B       b1002   s1001  B       b1003   t1003
2617  T       t1002   o938 b1002 b944  T       t1004   o b721 b1003
2618  B       b1003   t1002  B       b1004   t1004
2619  P       p1003   Var v_3  T       t1005   o b688 b1004
2620  O       o1003   var p1003  B       b1005   t1005
2621  T       t1003   o1003  T       t1006   o b670 b1005
2622  B       b1004   t1003  B       b1006   t1006
2623  T       t1004   o738 b966 b1004  T       t1007   o b743 b1006
2624  B       b1005   t1004 v_3  B       b1007   t1007
2625  T       t1005   o976 b1005  T       t1008   o b704 b1007
2626  S       s1005   t620 h h947 h957 h971  B       b1008   t1008
2627  G       s1005   t1005  T       t1009   o b702 b1008
2628  B       b1006   s1005  B       b1009   t1009
2629  T       t1006   o938 b1006 b944  T       t1010   o1001 b986 b1009
2630  B       b1007   t1006  B       b1010   t1010
2631  T       t1007   o973 b1007 b983 b996  NSummary!parent_none    parent_none     parent_none Summary
2632  B       b1008   t1007  O       o1010   parent_none
2633  T       t1008   o2 b1008  T       t1011   o1010
2634  B       b1009   t1008  B       b1011   t1011
2635  T       t1009   o973 b1003 b4 b1009  T       t1012   o1000 b1010 b4 b1011
2636  B       b1010   t1009  B       b1012   t1012
2637  T       t1014   o936 b997 b4  P       p1012   String assertion
2638  B       b1015   t1014  O       o1012   tactic_arg p1012
2639  T       t1015   o990 b935 b1015 b4 b4  H       h1012   v t984
2640  B       b1016   t1015  T       t1013   o575 b564 b906 b578
2641  P       p1016   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"  B       b1013   t1013
2642  O       o1016   ext_rule p1016  T       t1014   o575 b564 b906 b765
2643  T       t1016   o559 b567 b561  B       b1014   t1014
2644  B       b1017   t1016  T       t1015   o811 b1013 b1014
2645  T       t1017   o559 b567 b674  S       s1015   t673 h h1012
2646    G       s1015   t1015
2647    B       b1015   s1015
2648    T       t1016   o1001 b1015 b1009
2649    B       b1016   t1016
2650    S       s1016   t673 h h1012
2651    G       s1016   t986
2652    B       b1017   s1016
2653    T       t1017   o1001 b1017 b1009
2654  B       b1018   t1017  B       b1018   t1017
2655  T       t1018   o738 b1017 b1018  T       t1018   o2 b1012
2656  H       h1018   v_4 t1018  B       b1019   t1018
2657  S       s1018   t620 h h947 h957 h971 h998 h1018  T       t1019   o1000 b1018 b4 b1019
 G       s1018   t925  
 B       b1019   s1018  
 T       t1019   o938 b1019 b944  
2658  B       b1020   t1019  B       b1020   t1019
2659  T       t1020   o2 b1000  T       t1020   o2 b1020
2660  B       b1021   t1020  B       b1021   t1020
2661  T       t1021   o937 b1020 b4 b1021  T       t1021   o1012 b1016 b4 b1021
2662  B       b1022   t1021  B       b1022   t1021
2663  T       t1022   o b1022 b4  H       h1022   v_1 t1015
2664  B       b1023   t1022  S       s1022   t673 h h1012 h1022
2665  T       t1023   o936 b1000 b1023  G       s1022   t986
2666    B       b1023   s1022
2667    T       t1023   o1001 b1023 b1009
2668  B       b1024   t1023  B       b1024   t1023
2669  P       p1024   String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"  T       t1024   o1000 b1024 b4 b1021
2670  O       o1024   ext_rule p1024  B       b1025   t1024
2671  T       t1024   o738 b561 b1018  T       t1025   o b1025 b4
 H       h1024   v_5 t1024  
 S       s1024   t620 h h947 h957 h971 h998 h1018 h1024  
 G       s1024   t925  
 B       b1025   s1024  
 T       t1025   o938 b1025 b944  
2672  B       b1026   t1025  B       b1026   t1025
2673  T       t1026   o2 b1022  T       t1026   o b1022 b1026
2674  B       b1027   t1026  B       b1027   t1026
2675  T       t1027   o937 b1026 b4 b1027  T       t1027   o999 b1012 b1027
2676  B       b1028   t1027  B       b1028   t1027
2677  T       t219    o b1028 b4  P       p1028   String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2678  B       b219    t219  O       o1028   ext_rule p1028
2679  T       t229    o936 b1022 b219  T       t1028   o999 b1022 b4
2680  B       b229    t229  B       b1029   t1028
2681  B       b1029   t1017 v_5  T       t1029   o1028 b998 b1029 b4 b4
2682  T       t1029   o711 b1029  B       b1030   t1029
2683  S       s1029   t620 h h947 h957 h971 h998 h1018  P       p1030   String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 3 thenAT autoT"
2684  G       s1029   t1029  O       o1030   ext_rule p1030
2685  B       b1030   s1029  T       t1030   o575 b564 b948 b577
 T       t1030   o938 b1030 b944  
2686  B       b1031   t1030  B       b1031   t1030
2687  P       p1031   Var v_5  T       t1031   o811 b1031 b1014
2688  O       o1031   var p1031  H       h1031   v_2 t1031
2689  T       t1031   o1031  S       s1031   t673 h h1012 h1022 h1031
2690  B       b1032   t1031  G       s1031   t986
2691  T       t1032   o738 b1032 b1018  B       b1032   s1031
2692  B       b1033   t1032 v_5  T       t1032   o1001 b1032 b1009
2693  T       t1033   o976 b1033  B       b1033   t1032
2694  S       s1033   t620 h h947 h957 h971 h998 h1018  T       t1033   o2 b1025
2695  G       s1033   t1033  B       b1034   t1033
2696  B       b1034   s1033  T       t1034   o1000 b1033 b4 b1034
 T       t1034   o938 b1034 b944  
2697  B       b1035   t1034  B       b1035   t1034
2698  T       t1035   o973 b1035 b983 b1027  T       t1035   o b1035 b4
2699  B       b1036   t1035  B       b1036   t1035
2700  T       t1036   o2 b1036  T       t1036   o999 b1025 b1036
2701  B       b1037   t1036  B       b1037   t1036
2702  T       t1037   o973 b1031 b4 b1037  P       p1037   String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 4 thenAT autoT"
2703    O       o1037   ext_rule p1037
2704    T       t1037   o575 b564 b948 b742
2705  B       b1038   t1037  B       b1038   t1037
2706  P       p1041   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"  T       t1038   o811 b1031 b1038
2707  O       o1041   ext_rule p1041  H       h1038   v_3 t1038
2708  H       h1041   v_6 t925  S       s1038   t673 h h1012 h1022 h1031 h1038
2709  S       s1041   t620 h h947 h957 h971 h998 h1018 h1024 h1041  G       s1038   t986
2710  G       s1041   t925  B       b1039   s1038
2711  B       b1042   s1041  T       t1039   o1001 b1039 b1009
2712  T       t1042   o938 b1042 b944  B       b1040   t1039
2713    T       t1040   o2 b1035
2714    B       b1041   t1040
2715    T       t1041   o1000 b1040 b4 b1041
2716    B       b1042   t1041
2717    T       t1042   o b1042 b4
2718  B       b1043   t1042  B       b1043   t1042
2719  T       t1043   o2 b1028  T       t1043   o999 b1035 b1043
2720  B       b1044   t1043  B       b1044   t1043
2721  T       t1044   o937 b1043 b4 b1044  P       p1044   String "setSubstT << equal{op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 thenAT autoT"
2722    O       o1044   ext_rule p1044
2723    T       t1044   o575 b564 b583 b577
2724  B       b1045   t1044  B       b1045   t1044
2725  T       t1045   o b1045 b4  T       t1045   o575 b564 b583 b742
2726  B       b1046   t1045  B       b1046   t1045
2727  T       t1046   o936 b1028 b1046  T       t1046   o811 b1045 b1046
2728  B       b1047   t1046  H       h1046   v_4 t1046
2729  P       p1047   String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"  S       s1046   t673 h h1012 h1022 h1031 h1038 h1046
2730  O       o1047   ext_rule p1047  G       s1046   t986
2731  T       t1047   o936 b1045 b4  B       b1047   s1046
2732    T       t1047   o1001 b1047 b1009
2733  B       b1048   t1047  B       b1048   t1047
2734  T       t1048   o1047 b935 b1048 b4 b4  T       t1048   o2 b1042
2735  B       b1049   t1048  B       b1049   t1048
2736  T       t1049   o b1049 b4  T       t1049   o1000 b1048 b4 b1049
2737  B       b1050   t1049  B       b1050   t1049
2738  P       p1050   String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"  T       t1050   o b1050 b4
2739  O       o1050   ext_rule p1050  B       b1051   t1050
2740  B       b1051   t1016 v_6  T       t1051   o999 b1042 b1051
2741  T       t1051   o711 b1051  B       b1052   t1051
2742  S       s1051   t620 h h947 h957 h971 h998 h1018 h1024  P       p1052   String "setSubstT << equal{op{'g; id{'g}; 's2}; 's2} >> 6 thenAT autoT"
2743  G       s1051   t1051  O       o1052   ext_rule p1052
2744  B       b1052   s1051  T       t1052   o811 b577 b1046
2745  T       t1052   o938 b1052 b944  H       h1052   v_5 t1052
2746  B       b1053   t1052  S       s1052   t673 h h1012 h1022 h1031 h1038 h1046 h1052
2747  P       p1053   Var v_6  G       s1052   t986
2748  O       o1053   var p1053  B       b1053   s1052
2749  T       t1053   o1053  T       t1053   o1001 b1053 b1009
2750  B       b1054   t1053  B       b1054   t1053
2751  T       t1054   o738 b1017 b1054  T       t1054   o2 b1050
2752  B       b1055   t1054 v_6  B       b1055   t1054
2753  T       t1055   o976 b1055  T       t1055   o1000 b1054 b4 b1055
2754  S       s1055   t620 h h947 h957 h971 h998 h1018 h1024  B       b1056   t1055
2755  G       s1055   t1055  T       t1056   o b1056 b4
 B       b1056   s1055  
 T       t1056   o938 b1056 b944  
2756  B       b1057   t1056  B       b1057   t1056
2757  T       t1057   o973 b1057 b983 b1044  T       t1057   o999 b1050 b1057
2758  B       b1058   t1057  B       b1058   t1057
2759  T       t1058   o2 b1058  P       p1058   String "setSubstT << equal{op{'g; id{'g}; 's3}; 's3} >> 7 thenT autoT"
2760    O       o1058   ext_rule p1058