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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3553 - (hide annotations) (download)
Tue Apr 2 07:45:26 2002 UTC (19 years, 3 months ago) by xiny
File size: 151041 byte(s)
1. Added "eqG" to the definition of groups which denotes the equivalence
   relation related with the group. Every group has an equivalence
   relation, which is now explicitly described.
2. Accordingly, all rules related with equivalence relations in groups
   are updated and reproved.
3. Added tactics "uniqueInvLeftT" and "uniqueInvRightT" which might not
   be very useful though.

1 xiny 3379 #PRL version 1.0.0 ASCII term
2     NPerv Perv Perv NIL
3     NPerv!cons cons cons Perv
4     O o cons
5     NSummary Summary Summary NIL
6     NSummary!location location location Summary
7     P p Number 0
8 xiny 3498 P p1 Number 25
9 xiny 3379 O o1 location p p1
10     NSummary!parent parent parent Summary
11     O o2 parent
12 xiny 3498 P p2 String Itt_record_label0
13 xiny 3379 O o3 parent p2
14     T t o3
15     B b t
16     NPerv!nil nil3 nil Perv
17     O o4 nil3
18     T t4 o4
19     B b4 t4
20     T t5 o b b4
21     B b5 t5
22 xiny 3498 P p5 String Itt_nat
23 xiny 3379 O o5 parent p5
24     T t6 o5
25     B b6 t6
26     T t7 o b6 b4
27     B b7 t7
28 xiny 3498 P p7 String Itt_int_ext
29 xiny 3379 O o7 parent p7
30     T t8 o7
31     B b8 t8
32     T t9 o b8 b4
33     B b9 t9
34 xiny 3498 P p9 String Itt_int_base
35 xiny 3379 O o9 parent p9
36     T t10 o9
37     B b10 t10
38     T t11 o b10 b4
39     B b11 t11
40 xiny 3498 P p11 String Itt_bool
41 xiny 3379 O o11 parent p11
42     T t12 o11
43     B b12 t12
44     T t13 o b12 b4
45     B b13 t13
46 xiny 3498 P p13 String Itt_decidable
47 xiny 3379 O o13 parent p13
48     T t14 o13
49     B b14 t14
50     T t15 o b14 b4
51     B b15 t15
52 xiny 3498 P p15 String Itt_logic
53 xiny 3379 O o15 parent p15
54     T t16 o15
55     B b16 t16
56     T t17 o b16 b4
57     B b17 t17
58 xiny 3498 P p17 String Itt_union
59 xiny 3379 O o17 parent p17
60     T t18 o17
61     B b18 t18
62     T t19 o b18 b4
63     B b19 t19
64 xiny 3498 P p19 String Itt_prod
65 xiny 3379 O o19 parent p19
66     T t20 o19
67     B b20 t20
68     T t21 o b20 b4
69     B b21 t21
70 xiny 3498 P p21 String Itt_dprod
71 xiny 3379 O o21 parent p21
72     T t22 o21
73     B b22 t22
74     T t23 o b22 b4
75     B b23 t23
76 xiny 3498 P p23 String Itt_fun
77 xiny 3379 O o23 parent p23
78     T t24 o23
79     B b24 t24
80     T t25 o b24 b4
81     B b25 t25
82 xiny 3498 P p25 String Itt_dfun
83 xiny 3379 O o25 parent p25
84     T t26 o25
85     B b26 t26
86     T t27 o b26 b4
87     B b27 t27
88 xiny 3498 P p27 String Itt_rfun
89 xiny 3379 O o27 parent p27
90     T t28 o27
91     B b28 t28
92     T t29 o b28 b4
93     B b29 t29
94 xiny 3498 P p29 String Itt_void
95 xiny 3379 O o29 parent p29
96     T t30 o29
97     B b30 t30
98     T t31 o b30 b4
99     B b31 t31
100 xiny 3498 P p31 String Itt_set
101 xiny 3379 O o31 parent p31
102     T t32 o31
103     B b32 t32
104     T t33 o b32 b4
105     B b33 t33
106 xiny 3498 P p33 String Itt_unit
107 xiny 3379 O o33 parent p33
108     T t34 o33
109     B b34 t34
110     T t35 o b34 b4
111     B b35 t35
112 xiny 3498 P p35 String Itt_squiggle
113 xiny 3379 O o35 parent p35
114     T t36 o35
115     B b36 t36
116     T t37 o b36 b4
117     B b37 t37
118 xiny 3498 P p37 String Itt_subtype
119 xiny 3379 O o37 parent p37
120     T t38 o37
121     B b38 t38
122     T t39 o b38 b4
123     B b39 t39
124 xiny 3498 P p39 String Itt_squash
125 xiny 3379 O o39 parent p39
126     T t40 o39
127     B b40 t40
128     T t41 o b40 b4
129     B b41 t41
130 xiny 3498 P p41 String Itt_struct
131 xiny 3379 O o41 parent p41
132     T t42 o41
133     B b42 t42
134     T t43 o b42 b4
135     B b43 t43
136 xiny 3498 P p43 String Itt_equal
137 xiny 3379 O o43 parent p43
138     T t44 o43
139     B b44 t44
140     T t45 o b44 b4
141     B b45 t45
142 xiny 3498 P p45 String Itt_comment
143 xiny 3379 O o45 parent p45
144     T t46 o45
145     B b46 t46
146     T t47 o b46 b4
147     B b47 t47
148 xiny 3498 P p47 String Base_theory
149 xiny 3379 O o47 parent p47
150     T t48 o47
151     B b48 t48
152     T t49 o b48 b4
153     B b49 t49
154 xiny 3498 P p49 String Base_meta
155 xiny 3379 O o49 parent p49
156     T t50 o49
157     B b50 t50
158     T t51 o b50 b4
159     B b51 t51
160 xiny 3498 P p51 String Base_cache
161 xiny 3379 O o51 parent p51
162     T t52 o51
163     B b52 t52
164     T t53 o b52 b4
165     B b53 t53
166 xiny 3498 P p53 String Tactic_cache
167 xiny 3379 O o53 parent p53
168     T t54 o53
169     B b54 t54
170     T t55 o b54 b4
171     B b55 t55
172 xiny 3498 P p55 String Typeinf
173 xiny 3379 O o55 parent p55
174     T t56 o55
175     B b56 t56
176     T t57 o b56 b4
177     B b57 t57
178 xiny 3498 P p57 String Ocaml_df
179 xiny 3379 O o57 parent p57
180     T t58 o57
181     B b58 t58
182     T t59 o b58 b4
183     B b59 t59
184 xiny 3498 P p59 String Ocaml_str_df
185 xiny 3379 O o59 parent p59
186     T t60 o59
187     B b60 t60
188     T t61 o b60 b4
189     B b61 t61
190 xiny 3498 P p61 String Ocaml_sig_df
191 xiny 3379 O o61 parent p61
192     T t62 o61
193     B b62 t62
194     T t63 o b62 b4
195     B b63 t63
196 xiny 3498 P p63 String Ocaml_me_df
197 xiny 3379 O o63 parent p63
198     T t64 o63
199     B b64 t64
200     T t65 o b64 b4
201     B b65 t65
202 xiny 3498 P p65 String Ocaml_mt_df
203 xiny 3379 O o65 parent p65
204     T t66 o65
205     B b66 t66
206     T t67 o b66 b4
207     B b67 t67
208 xiny 3498 P p67 String Ocaml_type_df
209 xiny 3379 O o67 parent p67
210     T t68 o67
211     B b68 t68
212     T t69 o b68 b4
213     B b69 t69
214 xiny 3498 P p69 String Ocaml_patt_df
215 xiny 3379 O o69 parent p69
216     T t70 o69
217     B b70 t70
218     T t71 o b70 b4
219     B b71 t71
220 xiny 3498 P p71 String Ocaml_expr_df
221 xiny 3379 O o71 parent p71
222     T t72 o71
223     B b72 t72
224     T t73 o b72 b4
225     B b73 t73
226 xiny 3498 P p73 String Ocaml_base_df
227 xiny 3379 O o73 parent p73
228     T t74 o73
229     B b74 t74
230     T t75 o b74 b4
231     B b75 t75
232 xiny 3498 P p75 String Ocaml
233 xiny 3379 O o75 parent p75
234     T t76 o75
235     B b76 t76
236     T t77 o b76 b4
237     B b77 t77
238 xiny 3498 P p77 String Base_rewrite
239 xiny 3379 O o77 parent p77
240     T t78 o77
241     B b78 t78
242     T t79 o b78 b4
243     B b79 t79
244 xiny 3498 P p79 String Base_dtactic
245 xiny 3379 O o79 parent p79
246     T t80 o79
247     B b80 t80
248     T t81 o b80 b4
249     B b81 t81
250 xiny 3498 P p81 String Base_auto_tactic
251 xiny 3379 O o81 parent p81
252     T t82 o81
253     B b82 t82
254     T t83 o b82 b4
255     B b83 t83
256 xiny 3498 P p83 String Base_trivial
257 xiny 3379 O o83 parent p83
258     T t84 o83
259     B b84 t84
260     T t85 o b84 b4
261     B b85 t85
262 xiny 3498 P p85 String Top_conversionals
263 xiny 3379 O o85 parent p85
264     T t86 o85
265     B b86 t86
266     T t87 o b86 b4
267     B b87 t87
268 xiny 3498 P p87 String Top_tacticals
269 xiny 3379 O o87 parent p87
270     T t88 o87
271     B b88 t88
272     T t89 o b88 b4
273     B b89 t89
274 xiny 3498 P p89 String Var
275 xiny 3379 O o89 parent p89
276     T t90 o89
277     B b90 t90
278     T t91 o b90 b4
279     B b91 t91
280 xiny 3498 P p91 String Mptop
281 xiny 3379 O o91 parent p91
282     T t92 o91
283     B b92 t92
284     T t93 o b92 b4
285     B b93 t93
286 xiny 3498 P p93 String Summary
287 xiny 3379 O o93 parent p93
288     T t94 o93
289     B b94 t94
290     T t95 o b94 b4
291     B b95 t95
292 xiny 3498 P p95 String Comment
293 xiny 3379 O o95 parent p95
294     T t96 o95
295     B b96 t96
296     T t97 o b96 b4
297     B b97 t97
298 xiny 3498 P p97 String Base_dform
299 xiny 3379 O o97 parent p97
300     T t98 o97
301     B b98 t98
302     T t99 o b98 b4
303     B b99 t99
304 xiny 3498 P p99 String Nuprl_font
305 xiny 3379 O o99 parent p99
306     T t100 o99
307     B b100 t100
308     T t101 o b100 b4
309     B b101 t101
310 xiny 3498 P p101 String Perv
311 xiny 3379 O o101 parent p101
312     T t102 o101
313     B b102 t102
314     T t103 o b102 b4
315     B b103 t103
316 xiny 3498 T t104 o b103 b4
317 xiny 3379 B b104 t104
318 xiny 3498 T t105 o b101 b104
319 xiny 3379 B b105 t105
320 xiny 3498 T t106 o b99 b105
321 xiny 3379 B b106 t106
322 xiny 3498 T t107 o b97 b106
323 xiny 3379 B b107 t107
324 xiny 3498 T t108 o b95 b107
325 xiny 3379 B b108 t108
326 xiny 3498 T t109 o b93 b108
327 xiny 3379 B b109 t109
328 xiny 3498 T t110 o b91 b109
329 xiny 3379 B b110 t110
330 xiny 3498 T t111 o b89 b110
331 xiny 3379 B b111 t111
332 xiny 3498 T t112 o b87 b111
333 xiny 3379 B b112 t112
334 xiny 3498 T t113 o b85 b112
335 xiny 3379 B b113 t113
336 xiny 3498 T t114 o b83 b113
337 xiny 3379 B b114 t114
338 xiny 3498 T t115 o b81 b114
339 xiny 3379 B b115 t115
340 xiny 3498 T t116 o b79 b115
341 xiny 3379 B b116 t116
342 xiny 3498 T t117 o b77 b116
343 xiny 3379 B b117 t117
344 xiny 3498 T t118 o b75 b117
345 xiny 3379 B b118 t118
346 xiny 3498 T t119 o b73 b118
347 xiny 3379 B b119 t119
348 xiny 3498 T t120 o b71 b119
349 xiny 3379 B b120 t120
350 xiny 3498 T t121 o b69 b120
351 xiny 3379 B b121 t121
352 xiny 3498 T t122 o b67 b121
353 xiny 3379 B b122 t122
354 xiny 3498 T t123 o b65 b122
355 xiny 3379 B b123 t123
356 xiny 3498 T t124 o b63 b123
357 xiny 3379 B b124 t124
358 xiny 3498 T t125 o b61 b124
359 xiny 3379 B b125 t125
360 xiny 3498 T t126 o b59 b125
361 xiny 3379 B b126 t126
362 xiny 3498 T t127 o b57 b126
363 xiny 3379 B b127 t127
364 xiny 3498 T t128 o b55 b127
365 xiny 3379 B b128 t128
366 xiny 3498 T t129 o b53 b128
367 xiny 3379 B b129 t129
368 xiny 3498 T t130 o b51 b129
369 xiny 3379 B b130 t130
370 xiny 3498 T t131 o b49 b130
371 xiny 3379 B b131 t131
372 xiny 3498 T t132 o b47 b131
373 xiny 3379 B b132 t132
374 xiny 3498 T t133 o b45 b132
375 xiny 3379 B b133 t133
376 xiny 3498 T t134 o b43 b133
377 xiny 3379 B b134 t134
378 xiny 3498 T t135 o b41 b134
379 xiny 3379 B b135 t135
380 xiny 3498 T t136 o b39 b135
381 xiny 3379 B b136 t136
382 xiny 3498 T t137 o b37 b136
383 xiny 3379 B b137 t137
384 xiny 3498 T t138 o b35 b137
385 xiny 3379 B b138 t138
386 xiny 3498 T t139 o b33 b138
387 xiny 3379 B b139 t139
388 xiny 3498 T t140 o b31 b139
389 xiny 3379 B b140 t140
390 xiny 3498 T t141 o b29 b140
391 xiny 3379 B b141 t141
392 xiny 3498 T t142 o b27 b141
393 xiny 3379 B b142 t142
394 xiny 3498 T t143 o b25 b142
395 xiny 3379 B b143 t143
396 xiny 3498 T t144 o b23 b143
397 xiny 3379 B b144 t144
398 xiny 3498 T t145 o b21 b144
399 xiny 3379 B b145 t145
400 xiny 3498 T t146 o b19 b145
401 xiny 3379 B b146 t146
402 xiny 3498 T t147 o b17 b146
403 xiny 3379 B b147 t147
404 xiny 3498 T t148 o b15 b147
405 xiny 3379 B b148 t148
406 xiny 3498 T t149 o b13 b148
407 xiny 3379 B b149 t149
408 xiny 3498 T t150 o b11 b149
409 xiny 3379 B b150 t150
410 xiny 3498 T t151 o b9 b150
411 xiny 3379 B b151 t151
412 xiny 3498 T t152 o b7 b151
413 xiny 3379 B b152 t152
414 xiny 3498 T t153 o b5 b152
415 xiny 3379 B b153 t153
416 xiny 3498 NSummary!resource resource resource Summary
417     P p153 String auto
418     O o153 resource p153
419     NOcaml Ocaml Ocaml NIL
420     NOcaml!type_lid type_lid type_lid Ocaml
421     P p154 Number 2332
422     P p155 Number 2341
423     O o155 type_lid p154 p155
424     P p156 String auto_info
425     O o156 type_lid p156
426     T t156 o156
427 xiny 3379 B b156 t156
428 xiny 3498 T t157 o155 b156
429 xiny 3379 B b157 t157
430 xiny 3498 NOcaml!type_prod type_prod type_prod Ocaml
431     P p157 Number 2343
432     P p158 Number 2367
433     O o158 type_prod p157 p158
434     P p159 Number 2349
435     O o159 type_lid p157 p159
436     P p160 String tactic
437     O o160 type_lid p160
438     T t160 o160
439 xiny 3379 B b160 t160
440 xiny 3498 T t161 o159 b160
441 xiny 3379 B b161 t161
442 xiny 3498 P p161 Number 2352
443     P p162 Number 2358
444     O o162 type_lid p161 p162
445     T t162 o162 b160
446 xiny 3379 B b162 t162
447 xiny 3498 P p163 Number 2361
448     O o163 type_lid p163 p158
449     T t163 o163 b160
450 xiny 3379 B b163 t163
451 xiny 3498 T t164 o b163 b4
452 xiny 3379 B b164 t164
453 xiny 3498 T t165 o b162 b164
454 xiny 3379 B b165 t165
455 xiny 3498 T t166 o b161 b165
456 xiny 3379 B b166 t166
457 xiny 3498 T t167 o158 b166
458 xiny 3379 B b167 t167
459 xiny 3498 T t168 o153 b157 b167
460 xiny 3379 B b168 t168
461 xiny 3498 P p168 String cache
462     O o168 resource p168
463     P p169 Number 1424
464     P p170 Number 1434
465     O o170 type_lid p169 p170
466     P p171 String cache_rule
467     O o171 type_lid p171
468     T t171 o171
469 xiny 3379 B b171 t171
470 xiny 3498 T t172 o170 b171
471 xiny 3379 B b172 t172
472 xiny 3498 P p172 Number 1436
473     P p173 Number 1441
474     O o173 type_lid p172 p173
475     O o174 type_lid p168
476     T t174 o174
477 xiny 3379 B b174 t174
478 xiny 3498 T t175 o173 b174
479 xiny 3379 B b175 t175
480 xiny 3498 T t176 o168 b172 b175
481 xiny 3379 B b176 t176
482 xiny 3498 P p176 String elim
483     O o176 resource p176
484     P p177 Number 1761
485     P p178 Number 1783
486     O o178 type_prod p177 p178
487     P p179 Number 1765
488     O o179 type_lid p177 p179
489     P p180 String term
490     O o180 type_lid p180
491     T t180 o180
492 xiny 3379 B b180 t180
493 xiny 3498 T t181 o179 b180
494 xiny 3379 B b181 t181
495 xiny 3498 NOcaml!type_fun type_fun type_fun Ocaml
496     P p181 Number 1769
497     P p182 Number 1782
498     O o182 type_fun p181 p182
499     P p183 Number 1772
500     O o183 type_lid p181 p183
501     P p184 String int
502     O o184 type_lid p184
503     T t184 o184
504 xiny 3379 B b184 t184
505 xiny 3498 T t185 o183 b184
506 xiny 3379 B b185 t185
507 xiny 3498 P p185 Number 1776
508     O o185 type_lid p185 p182
509     T t186 o185 b160
510 xiny 3379 B b186 t186
511 xiny 3498 T t187 o182 b185 b186
512 xiny 3379 B b187 t187
513 xiny 3498 T t188 o b187 b4
514 xiny 3379 B b188 t188
515 xiny 3498 T t189 o b181 b188
516 xiny 3379 B b189 t189
517 xiny 3498 T t190 o178 b189
518 xiny 3379 B b190 t190
519 xiny 3498 P p190 Number 1785
520     P p191 Number 1798
521     O o191 type_fun p190 p191
522     P p192 Number 1788
523     O o192 type_lid p190 p192
524     T t192 o192 b184
525 xiny 3379 B b192 t192
526 xiny 3498 P p193 Number 1792
527     O o193 type_lid p193 p191
528     T t193 o193 b160
529 xiny 3379 B b193 t193
530 xiny 3498 T t194 o191 b192 b193
531 xiny 3379 B b194 t194
532 xiny 3498 T t195 o176 b190 b194
533 xiny 3379 B b195 t195
534 xiny 3498 P p195 String eqcd
535     O o195 resource p195
536     P p196 Number 6168
537     P p197 Number 6181
538     O o197 type_prod p196 p197
539     P p198 Number 6172
540     O o198 type_lid p196 p198
541     T t198 o198 b180
542 xiny 3379 B b198 t198
543 xiny 3498 P p199 Number 6175
544     O o199 type_lid p199 p197
545     T t199 o199 b160
546 xiny 3379 B b199 t199
547 xiny 3498 T t200 o b199 b4
548 xiny 3379 B b200 t200
549 xiny 3498 T t201 o b198 b200
550 xiny 3379 B b201 t201
551 xiny 3498 T t202 o197 b201
552 xiny 3379 B b202 t202
553 xiny 3498 P p202 Number 6183
554     P p203 Number 6189
555     O o203 type_lid p202 p203
556     T t203 o203 b160
557 xiny 3379 B b203 t203
558 xiny 3498 T t204 o195 b202 b203
559 xiny 3379 B b204 t204
560 xiny 3498 P p204 String intro
561     O o204 resource p204
562     P p205 Number 1815
563     P p206 Number 1852
564     O o206 type_prod p205 p206
565     P p207 Number 1819
566     O o207 type_lid p205 p207
567     T t207 o207 b180
568 xiny 3379 B b207 t207
569 xiny 3498 P p208 Number 1823
570     P p209 Number 1851
571     O o209 type_prod p208 p209
572     P p210 Number 1829
573     O o210 type_lid p208 p210
574     P p211 String string
575     O o211 type_lid p211
576     T t211 o211
577 xiny 3379 B b211 t211
578 xiny 3498 T t212 o210 b211
579 xiny 3379 B b212 t212
580 xiny 3498 NOcaml!type_apply type_apply type_apply Ocaml
581     P p212 Number 1832
582     P p213 Number 1842
583     O o213 type_apply p212 p213
584     P p214 Number 1836
585     O o214 type_lid p214 p213
586     P p215 String option
587     O o215 type_lid p215
588     T t215 o215
589     B b215 t215
590     T t216 o214 b215
591 xiny 3379 B b216 t216
592 xiny 3498 P p216 Number 1835
593     O o216 type_lid p212 p216
594     T t217 o216 b184
595 xiny 3379 B b217 t217
596 xiny 3498 T t218 o213 b216 b217
597     B b218 t218
598     P p218 Number 1845
599     O o218 type_lid p218 p209
600     T t219 o218 b160
601     B b219 t219
602     T t220 o b219 b4
603 xiny 3379 B b220 t220
604 xiny 3498 T t221 o b218 b220
605 xiny 3379 B b221 t221
606 xiny 3498 T t222 o b212 b221
607 xiny 3379 B b222 t222
608 xiny 3498 T t223 o209 b222
609 xiny 3379 B b223 t223
610 xiny 3404 T t224 o b223 b4
611 xiny 3379 B b224 t224
612 xiny 3498 T t225 o b207 b224
613 xiny 3379 B b225 t225
614 xiny 3498 T t226 o206 b225
615 xiny 3379 B b226 t226
616 xiny 3498 P p226 Number 1854
617     P p227 Number 1860
618     O o227 type_lid p226 p227
619     T t227 o227 b160
620 xiny 3404 B b227 t227
621 xiny 3498 T t228 o204 b226 b227
622 xiny 3404 B b228 t228
623 xiny 3498 P p228 String reduce
624 xiny 3404 O o228 resource p228
625 xiny 3498 P p229 Number 2920
626     P p230 Number 2931
627     O o230 type_prod p229 p230
628     P p231 Number 2924
629     O o231 type_lid p229 p231
630     T t231 o231 b180
631 xiny 3404 B b231 t231
632 xiny 3498 P p232 Number 2927
633     O o232 type_lid p232 p230
634     P p233 String conv
635     O o233 type_lid p233
636     T t233 o233
637     B b233 t233
638     T t234 o232 b233
639 xiny 3379 B b234 t234
640 xiny 3498 T t235 o b234 b4
641 xiny 3404 B b235 t235
642 xiny 3498 T t236 o b231 b235
643 xiny 3404 B b236 t236
644 xiny 3498 T t237 o230 b236
645     B b237 t237
646     P p237 Number 2933
647     P p238 Number 2937
648     O o238 type_lid p237 p238
649     T t238 o238 b233
650     B b238 t238
651     T t239 o228 b237 b238
652     B b239 t239
653     P p239 String squash
654     O o239 resource p239
655     P p240 Number 4017
656     P p241 Number 4028
657     O o241 type_lid p240 p241
658     P p242 String squash_info
659     O o242 type_lid p242
660     T t242 o242
661     B b242 t242
662     T t243 o241 b242
663     B b243 t243
664     P p243 Number 4030
665     P p244 Number 4043
666     O o244 type_fun p243 p244
667     P p245 Number 4033
668     O o245 type_lid p243 p245
669     T t245 o245 b184
670 xiny 3379 B b245 t245
671 xiny 3498 P p246 Number 4037
672     O o246 type_lid p246 p244
673     T t246 o246 b160
674 xiny 3379 B b246 t246
675 xiny 3498 T t247 o244 b245 b246
676 xiny 3379 B b247 t247
677 xiny 3498 T t248 o239 b243 b247
678 xiny 3379 B b248 t248
679 xiny 3498 P p248 String sub
680     O o248 resource p248
681     P p249 Number 4882
682     P p250 Number 4899
683     O o250 type_lid p249 p250
684     P p251 String sub_resource_info
685     O o251 type_lid p251
686     T t251 o251
687     B b251 t251
688     T t252 o250 b251
689 xiny 3379 B b252 t252
690 xiny 3498 P p252 Number 4901
691     P p253 Number 4907
692     O o253 type_lid p252 p253
693     T t253 o253 b160
694 xiny 3379 B b253 t253
695 xiny 3498 T t254 o248 b252 b253
696 xiny 3404 B b254 t254
697 xiny 3498 P p254 String toploop
698     O o254 resource p254
699     P p255 Number 2445
700     P p256 Number 2467
701     O o256 type_prod p255 p256
702     P p257 Number 2451
703     O o257 type_lid p255 p257
704     T t257 o257 b211
705     B b257 t257
706     P p258 Number 2454
707     P p259 Number 2460
708     O o259 type_lid p258 p259
709     T t259 o259 b211
710 xiny 3379 B b259 t259
711 xiny 3498 P p260 Number 2463
712     O o260 type_lid p260 p256
713     P p261 String expr
714     O o261 type_lid p261
715     T t261 o261
716 xiny 3379 B b261 t261
717 xiny 3498 T t262 o260 b261
718 xiny 3379 B b262 t262
719 xiny 3498 T t263 o b262 b4
720 xiny 3404 B b263 t263
721 xiny 3498 T t264 o b259 b263
722 xiny 3404 B b264 t264
723 xiny 3498 T t265 o b257 b264
724     B b265 t265
725     T t266 o256 b265
726     B b266 t266
727     P p266 Number 2469
728     P p267 Number 2478
729     O o267 type_lid p266 p267
730     P p268 String top_table
731     O o268 type_lid p268
732     T t268 o268
733     B b268 t268
734     T t269 o267 b268
735     B b269 t269
736     T t270 o254 b266 b269
737     B b270 t270
738     P p270 String typeinf
739     O o270 resource p270
740     P p271 Number 2151
741     P p272 Number 2172
742     O o272 type_lid p271 p272
743     P p273 String typeinf_resource_info
744     O o273 type_lid p273
745     T t273 o273
746     B b273 t273
747     T t274 o272 b273
748     B b274 t274
749     P p274 Number 2174
750     P p275 Number 2186
751     O o275 type_lid p274 p275
752     P p276 String typeinf_func
753     O o276 type_lid p276
754     T t276 o276
755 xiny 3379 B b276 t276
756 xiny 3498 T t277 o275 b276
757 xiny 3379 B b277 t277
758 xiny 3498 T t278 o270 b274 b277
759 xiny 3379 B b278 t278
760 xiny 3498 P p278 String typeinf_subst
761     O o278 resource p278
762     P p279 Number 1825
763     P p280 Number 1843
764     O o280 type_lid p279 p280
765     P p281 String typeinf_subst_info
766     O o281 type_lid p281
767     T t281 o281
768 xiny 3379 B b281 t281
769 xiny 3498 T t282 o280 b281
770 xiny 3379 B b282 t282
771 xiny 3498 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 xiny 3379 B b283 t283
777 xiny 3498 T t284 o282 b283
778 xiny 3379 B b284 t284
779 xiny 3498 T t285 o278 b282 b284
780 xiny 3379 B b285 t285
781 xiny 3498 T t286 o b285 b4
782 xiny 3379 B b286 t286
783 xiny 3498 T t287 o b278 b286
784 xiny 3404 B b287 t287
785 xiny 3498 T t288 o b270 b287
786 xiny 3404 B b288 t288
787 xiny 3498 T t289 o b254 b288
788     B b289 t289
789     T t290 o b248 b289
790     B b290 t290
791     T t291 o b239 b290
792 xiny 3379 B b291 t291
793 xiny 3498 T t292 o b228 b291
794     B b292 t292
795     T t293 o b204 b292
796 xiny 3379 B b293 t293
797 xiny 3498 T t294 o b195 b293
798 xiny 3379 B b294 t294
799 xiny 3498 T t295 o b176 b294
800 xiny 3379 B b295 t295
801 xiny 3498 T t296 o b168 b295
802 xiny 3379 B b296 t296
803 xiny 3498 T t297 o2 b5 b153 b296
804 xiny 3379 B b297 t297
805 xiny 3498 T t298 o1 b297
806 xiny 3404 B b298 t298
807 xiny 3498 P p298 Number 26
808 xiny 3553 P p299 Number 48
809 xiny 3498 O o299 location p298 p299
810 xiny 3553 P p300 String Czf_itt_member
811 xiny 3498 O o300 parent p300
812     T t300 o300
813     B b300 t300
814     T t301 o b300 b4
815     B b301 t301
816 xiny 3553 P p301 String Czf_itt_eq
817 xiny 3498 O o301 parent p301
818     T t302 o301
819 xiny 3404 B b302 t302
820 xiny 3498 T t303 o b302 b4
821 xiny 3379 B b303 t303
822 xiny 3553 P p303 String Czf_itt_set
823 xiny 3498 O o303 parent p303
824     T t304 o303
825     B b304 t304
826     T t305 o b304 b4
827 xiny 3379 B b305 t305
828 xiny 3553 P p305 String Czf_itt_comment
829 xiny 3498 O o305 parent p305
830     T t306 o305
831 xiny 3379 B b306 t306
832 xiny 3498 T t307 o b306 b4
833 xiny 3404 B b307 t307
834 xiny 3553 P p307 String Itt_theory
835 xiny 3498 O o307 parent p307
836     T t308 o307
837 xiny 3404 B b308 t308
838 xiny 3498 T t309 o b308 b4
839     B b309 t309
840 xiny 3553 P p309 String Itt_fset
841 xiny 3498 O o309 parent p309
842     T t310 o309
843     B b310 t310
844     T t311 o b310 b4
845 xiny 3379 B b311 t311
846 xiny 3553 P p311 String Itt_prop_decide
847 xiny 3498 O o311 parent p311
848     T t312 o311
849 xiny 3379 B b312 t312
850 xiny 3498 T t313 o b312 b4
851 xiny 3404 B b313 t313
852 xiny 3553 P p313 String Itt_derive
853 xiny 3498 O o313 parent p313
854     T t314 o313
855 xiny 3404 B b314 t314
856 xiny 3498 T t315 o b314 b4
857     B b315 t315
858 xiny 3553 P p315 String Itt_list2
859 xiny 3498 O o315 parent p315
860     T t316 o315
861     B b316 t316
862     T t317 o b316 b4
863 xiny 3379 B b317 t317
864 xiny 3553 P p317 String Itt_list
865 xiny 3498 O o317 parent p317
866     T t318 o317
867     B b318 t318
868     T t319 o b318 b4
869 xiny 3379 B b319 t319
870 xiny 3553 P p319 String Itt_quotient
871 xiny 3498 O o319 parent p319
872     T t320 o319
873     B b320 t320
874     T t321 o b320 b4
875 xiny 3379 B b321 t321
876 xiny 3553 P p321 String Itt_esquash
877 xiny 3498 O o321 parent p321
878     T t322 o321
879 xiny 3379 B b322 t322
880 xiny 3404 T t323 o b322 b4
881 xiny 3379 B b323 t323
882 xiny 3553 P p323 String Itt_srec
883 xiny 3498 O o323 parent p323
884     T t324 o323
885 xiny 3379 B b324 t324
886 xiny 3498 T t325 o b324 b4
887 xiny 3404 B b325 t325
888 xiny 3553 P p325 String Itt_prec
889 xiny 3498 O o325 parent p325
890     T t326 o325
891 xiny 3379 B b326 t326
892 xiny 3498 T t327 o b326 b4
893     B b327 t327
894 xiny 3553 P p327 String Itt_w
895 xiny 3498 O o327 parent p327
896     T t328 o327
897 xiny 3379 B b328 t328
898 xiny 3498 T t329 o b328 b4
899 xiny 3404 B b329 t329
900 xiny 3553 P p329 String Itt_bunion
901 xiny 3498 O o329 parent p329
902     T t330 o329
903 xiny 3404 B b330 t330
904 xiny 3498 T t331 o b330 b4
905     B b331 t331
906 xiny 3553 P p331 String Itt_bisect
907 xiny 3498 O o331 parent p331
908     T t332 o331
909     B b332 t332
910     T t333 o b332 b4
911 xiny 3404 B b333 t333
912 xiny 3553 P p333 String Itt_tunion
913 xiny 3498 O o333 parent p333
914     T t334 o333
915 xiny 3379 B b334 t334
916 xiny 3498 T t335 o b334 b4
917     B b335 t335
918 xiny 3553 P p335 String Itt_isect
919 xiny 3498 O o335 parent p335
920     T t336 o335
921 xiny 3379 B b336 t336
922 xiny 3498 T t337 o b336 b4
923 xiny 3404 B b337 t337
924 xiny 3553 P p337 String Itt_struct2
925 xiny 3498 O o337 parent p337
926     T t338 o337
927 xiny 3404 B b338 t338
928 xiny 3498 T t339 o b338 b4
929     B b339 t339
930 xiny 3553 P p339 String Itt_well_founded
931 xiny 3498 O o339 parent p339
932     T t340 o339
933     B b340 t340
934     T t341 o b340 b4
935 xiny 3379 B b341 t341
936 xiny 3553 P p341 String Itt_int_arith
937 xiny 3498 O o341 parent p341
938     T t342 o341
939 xiny 3379 B b342 t342
940 xiny 3498 T t343 o b342 b4
941 xiny 3379 B b343 t343
942 xiny 3553 P p343 String Itt_atom_bool
943     O o343 parent p343
944     T t344 o343
945 xiny 3379 B b344 t344
946 xiny 3553 T t345 o b344 b4
947 xiny 3379 B b345 t345
948 xiny 3553 P p345 String Itt_atom
949     O o345 parent p345
950     T t346 o345
951 xiny 3379 B b346 t346
952 xiny 3553 T t347 o b346 b4
953 xiny 3379 B b347 t347
954 xiny 3553 T t348 o b347 b4
955 xiny 3379 B b348 t348
956 xiny 3553 T t349 o b345 b348
957 xiny 3379 B b349 t349
958 xiny 3553 T t350 o b343 b349
959 xiny 3379 B b350 t350
960 xiny 3553 T t351 o b341 b350
961 xiny 3379 B b351 t351
962 xiny 3553 T t352 o b339 b351
963 xiny 3379 B b352 t352
964 xiny 3553 T t353 o b337 b352
965 xiny 3379 B b353 t353
966 xiny 3553 T t354 o b335 b353
967 xiny 3379 B b354 t354
968 xiny 3553 T t355 o b333 b354
969 xiny 3379 B b355 t355
970 xiny 3553 T t356 o b331 b355
971 xiny 3379 B b356 t356
972 xiny 3553 T t357 o b329 b356
973 xiny 3404 B b357 t357
974 xiny 3553 T t358 o b327 b357
975 xiny 3379 B b358 t358
976 xiny 3553 T t359 o b325 b358
977 xiny 3498 B b359 t359
978 xiny 3553 T t360 o b323 b359
979 xiny 3379 B b360 t360
980 xiny 3553 T t361 o b321 b360
981 xiny 3379 B b361 t361
982 xiny 3553 T t362 o b319 b361
983 xiny 3379 B b362 t362
984 xiny 3553 T t363 o b317 b362
985 xiny 3379 B b363 t363
986 xiny 3553 T t364 o b315 b363
987 xiny 3379 B b364 t364
988 xiny 3553 T t365 o b313 b364
989 xiny 3379 B b365 t365
990 xiny 3553 T t366 o b311 b365
991 xiny 3379 B b366 t366
992 xiny 3553 T t367 o b309 b366
993 xiny 3379 B b367 t367
994 xiny 3553 T t368 o b307 b367
995     B b368 t368
996     T t369 o b305 b368
997 xiny 3379 B b369 t369
998 xiny 3553 T t370 o b303 b369
999 xiny 3498 B b370 t370
1000 xiny 3553 T t371 o b301 b370
1001 xiny 3379 B b371 t371
1002 xiny 3553 T t372 o2 b301 b371 b296
1003 xiny 3379 B b372 t372
1004 xiny 3553 T t373 o299 b372
1005 xiny 3379 B b373 t373
1006 xiny 3553 P p373 Number 49
1007     P p374 Number 67
1008     O o374 location p373 p374
1009     T t374 o2 b303 b4 b296
1010 xiny 3379 B b374 t374
1011 xiny 3553 T t375 o374 b374
1012 xiny 3379 B b375 t375
1013 xiny 3553 P p375 Number 68
1014     P p376 Number 88
1015     O o376 location p375 p376
1016     P p377 String Czf_itt_dall
1017     O o377 parent p377
1018     T t377 o377
1019 xiny 3379 B b377 t377
1020 xiny 3553 T t378 o b377 b4
1021 xiny 3379 B b378 t378
1022 xiny 3553 P p378 String Czf_itt_set_ind
1023     O o378 parent p378
1024     T t379 o378
1025     B b379 t379
1026     T t380 o b379 b4
1027     B b380 t380
1028     P p380 String Czf_itt_all
1029 xiny 3498 O o380 parent p380
1030 xiny 3553 T t381 o380
1031 xiny 3379 B b381 t381
1032 xiny 3553 T t382 o b381 b4
1033 xiny 3379 B b382 t382
1034 xiny 3553 P p382 String Czf_itt_sep
1035     O o382 parent p382
1036     T t383 o382
1037 xiny 3404 B b383 t383
1038 xiny 3553 T t384 o b383 b4
1039 xiny 3379 B b384 t384
1040 xiny 3498 T t385 o b384 b4
1041     B b385 t385
1042 xiny 3553 T t386 o b382 b385
1043 xiny 3379 B b386 t386
1044 xiny 3553 T t387 o b380 b386
1045 xiny 3379 B b387 t387
1046 xiny 3553 T t388 o b378 b387
1047 xiny 3379 B b388 t388
1048 xiny 3553 T t389 o2 b378 b388 b296
1049 xiny 3404 B b389 t389
1050 xiny 3553 T t390 o376 b389
1051 xiny 3404 B b390 t390
1052 xiny 3553 P p390 Number 89
1053     P p391 Number 108
1054     O o391 location p390 p391
1055     P p392 String Czf_itt_and
1056     O o392 parent p392
1057     T t392 o392
1058 xiny 3498 B b392 t392
1059 xiny 3553 T t393 o b392 b4
1060 xiny 3498 B b393 t393
1061 xiny 3553 T t394 o b393 b4
1062     B b394 t394
1063     T t395 o2 b393 b394 b296
1064 xiny 3379 B b395 t395
1065 xiny 3553 T t396 o391 b395
1066 xiny 3379 B b396 t396
1067 xiny 3553 P p396 Number 109
1068     P p397 Number 130
1069     O o397 location p396 p397
1070     P p398 String Czf_itt_equiv
1071     O o398 parent p398
1072     T t398 o398
1073 xiny 3404 B b398 t398
1074 xiny 3553 T t399 o b398 b4
1075 xiny 3498 B b399 t399
1076 xiny 3553 P p399 String Czf_itt_pair
1077     O o399 parent p399
1078     T t400 o399
1079     B b400 t400
1080     T t401 o b400 b4
1081     B b401 t401
1082     P p401 String Czf_itt_singleton
1083 xiny 3527 O o401 parent p401
1084 xiny 3553 T t402 o401
1085 xiny 3516 B b402 t402
1086 xiny 3553 T t403 o b402 b4
1087 xiny 3379 B b403 t403
1088 xiny 3553 P p403 String Czf_itt_union
1089     O o403 parent p403
1090     T t404 o403
1091 xiny 3404 B b404 t404
1092 xiny 3553 T t405 o b404 b4
1093 xiny 3527 B b405 t405
1094 xiny 3553 P p405 String Czf_itt_subset
1095     O o405 parent p405
1096     T t406 o405
1097 xiny 3527 B b406 t406
1098 xiny 3553 T t407 o b406 b4
1099 xiny 3527 B b407 t407
1100 xiny 3553 P p407 String Czf_itt_dexists
1101     O o407 parent p407
1102     T t408 o407
1103 xiny 3527 B b408 t408
1104 xiny 3553 T t409 o b408 b4
1105 xiny 3527 B b409 t409
1106     T t410 o b409 b4
1107 xiny 3379 B b410 t410
1108 xiny 3553 T t411 o b407 b410
1109 xiny 3379 B b411 t411
1110 xiny 3553 T t412 o b405 b411
1111 xiny 3527 B b412 t412
1112 xiny 3553 T t413 o b403 b412
1113 xiny 3527 B b413 t413
1114 xiny 3553 T t414 o b401 b413
1115 xiny 3527 B b414 t414
1116 xiny 3553 T t415 o b399 b414
1117 xiny 3527 B b415 t415
1118 xiny 3553 T t416 o2 b399 b415 b296
1119 xiny 3527 B b416 t416
1120 xiny 3553 T t417 o397 b416
1121 xiny 3498 B b417 t417
1122 xiny 3553 P p417 Number 132
1123     P p418 Number 143
1124     O o418 location p417 p418
1125 xiny 3527 NSummary!summary_item summary_item summary_item Summary
1126 xiny 3553 O o419 summary_item
1127 xiny 3527 NOcaml!str_open str_open str_open Ocaml
1128 xiny 3553 O o420 str_open p417 p418
1129 xiny 3527 NOcaml!string string string Ocaml
1130 xiny 3553 P p420 String Printf
1131     O o421 string p420
1132     T t421 o421
1133     B b421 t421
1134     T t422 o b421 b4
1135     B b422 t422
1136     T t423 o420 b422
1137     B b423 t423
1138     T t424 o419 b423
1139 xiny 3527 B b424 t424
1140 xiny 3553 T t425 o418 b424
1141 xiny 3527 B b425 t425
1142 xiny 3553 P p425 Number 144
1143     P p426 Number 157
1144     O o426 location p425 p426
1145     O o427 str_open p425 p426
1146     P p427 String Mp_debug
1147     O o428 string p427
1148     T t428 o428
1149 xiny 3379 B b428 t428
1150 xiny 3553 T t429 o b428 b4
1151     B b429 t429
1152     T t430 o427 b429
1153     B b430 t430
1154     T t431 o419 b430
1155 xiny 3527 B b431 t431
1156 xiny 3553 T t432 o426 b431
1157 xiny 3527 B b432 t432
1158 xiny 3553 P p432 Number 158
1159     P p433 Number 187
1160     O o433 location p432 p433
1161     O o434 str_open p432 p433
1162     P p434 String Refiner
1163     O o435 string p434
1164     T t435 o435
1165 xiny 3527 B b435 t435
1166 xiny 3553 P p435 String TermType
1167     O o436 string p435
1168     T t436 o436
1169     B b436 t436
1170     T t437 o b436 b4
1171     B b437 t437
1172     T t438 o b435 b437
1173 xiny 3379 B b438 t438
1174 xiny 3553 T t439 o b435 b438
1175 xiny 3379 B b439 t439
1176 xiny 3553 T t440 o434 b439
1177 xiny 3527 B b440 t440
1178 xiny 3553 T t441 o419 b440
1179 xiny 3527 B b441 t441
1180 xiny 3553 T t442 o433 b441
1181 xiny 3527 B b442 t442
1182 xiny 3553 P p442 Number 188
1183     P p443 Number 213
1184     O o443 location p442 p443
1185     O o444 str_open p442 p443
1186     P p444 String Term
1187     O o445 string p444
1188     T t445 o445
1189 xiny 3379 B b445 t445
1190 xiny 3553 T t446 o b445 b4
1191     B b446 t446
1192     T t447 o b435 b446
1193     B b447 t447
1194     T t448 o b435 b447
1195 xiny 3379 B b448 t448
1196 xiny 3553 T t449 o444 b448
1197 xiny 3527 B b449 t449
1198 xiny 3553 T t450 o419 b449
1199 xiny 3527 B b450 t450
1200 xiny 3553 T t451 o443 b450
1201 xiny 3527 B b451 t451
1202 xiny 3553 P p451 Number 214
1203     P p452 Number 241
1204     O o452 location p451 p452
1205     O o453 str_open p451 p452
1206     P p453 String TermOp
1207     O o454 string p453
1208     T t454 o454
1209 xiny 3379 B b454 t454
1210 xiny 3553 T t455 o b454 b4
1211     B b455 t455
1212     T t456 o b435 b455
1213     B b456 t456
1214     T t457 o b435 b456
1215 xiny 3379 B b457 t457
1216 xiny 3553 T t458 o453 b457
1217 xiny 3527 B b458 t458
1218 xiny 3553 T t459 o419 b458
1219 xiny 3527 B b459 t459
1220 xiny 3553 T t460 o452 b459
1221 xiny 3527 B b460 t460
1222 xiny 3553 P p460 Number 242
1223     P p461 Number 271
1224     O o461 location p460 p461
1225     O o462 str_open p460 p461
1226     P p462 String TermAddr
1227     O o463 string p462
1228     T t463 o463
1229 xiny 3379 B b463 t463
1230 xiny 3553 T t464 o b463 b4
1231     B b464 t464
1232     T t465 o b435 b464
1233     B b465 t465
1234     T t466 o b435 b465
1235 xiny 3379 B b466 t466
1236 xiny 3553 T t467 o462 b466
1237 xiny 3527 B b467 t467
1238 xiny 3553 T t468 o419 b467
1239 xiny 3527 B b468 t468
1240 xiny 3553 T t469 o461 b468
1241 xiny 3527 B b469 t469
1242 xiny 3553 P p469 Number 272
1243     P p470 Number 300
1244     O o470 location p469 p470
1245     O o471 str_open p469 p470
1246     P p471 String TermMan
1247     O o472 string p471
1248     T t472 o472
1249 xiny 3379 B b472 t472
1250 xiny 3553 T t473 o b472 b4
1251     B b473 t473
1252     T t474 o b435 b473
1253     B b474 t474
1254     T t475 o b435 b474
1255 xiny 3379 B b475 t475
1256 xiny 3553 T t476 o471 b475
1257 xiny 3527 B b476 t476
1258 xiny 3553 T t477 o419 b476
1259 xiny 3527 B b477 t477
1260 xiny 3553 T t478 o470 b477
1261 xiny 3527 B b478 t478
1262 xiny 3553 P p478 Number 301
1263     P p479 Number 331
1264     O o479 location p478 p479
1265     O o480 str_open p478 p479
1266     P p480 String TermSubst
1267     O o481 string p480
1268     T t481 o481
1269 xiny 3379 B b481 t481
1270 xiny 3553 T t482 o b481 b4
1271     B b482 t482
1272     T t483 o b435 b482
1273     B b483 t483
1274     T t484 o b435 b483
1275 xiny 3404 B b484 t484
1276 xiny 3553 T t485 o480 b484
1277 xiny 3527 B b485 t485
1278 xiny 3553 T t486 o419 b485
1279 xiny 3527 B b486 t486
1280 xiny 3553 T t487 o479 b486
1281 xiny 3527 B b487 t487
1282 xiny 3553 P p487 Number 332
1283     P p488 Number 359
1284     O o488 location p487 p488
1285     O o489 str_open p487 p488
1286     P p489 String Refine
1287     O o490 string p489
1288     T t490 o490
1289 xiny 3379 B b490 t490
1290 xiny 3553 T t491 o b490 b4
1291     B b491 t491
1292     T t492 o b435 b491
1293     B b492 t492
1294     T t493 o b435 b492
1295 xiny 3527 B b493 t493
1296 xiny 3553 T t494 o489 b493
1297 xiny 3527 B b494 t494
1298 xiny 3553 T t495 o419 b494
1299 xiny 3527 B b495 t495
1300 xiny 3553 T t496 o488 b495
1301 xiny 3527 B b496 t496
1302 xiny 3553 P p496 Number 360
1303     P p497 Number 392
1304     O o497 location p496 p497
1305     O o498 str_open p496 p497
1306     P p498 String RefineError
1307     O o499 string p498
1308     T t499 o499
1309 xiny 3527 B b499 t499
1310 xiny 3553 T t500 o b499 b4
1311     B b500 t500
1312     T t501 o b435 b500
1313     B b501 t501
1314     T t502 o b435 b501
1315 xiny 3527 B b502 t502
1316 xiny 3553 T t503 o498 b502
1317 xiny 3527 B b503 t503
1318 xiny 3553 T t504 o419 b503
1319 xiny 3379 B b504 t504
1320 xiny 3553 T t505 o497 b504
1321 xiny 3379 B b505 t505
1322 xiny 3553 P p505 Number 393
1323     P p506 Number 409
1324     O o506 location p505 p506
1325     O o507 str_open p505 p506
1326     P p507 String Mp_resource
1327     O o508 string p507
1328     T t508 o508
1329 xiny 3527 B b508 t508
1330 xiny 3553 T t509 o b508 b4
1331     B b509 t509
1332     T t510 o507 b509
1333     B b510 t510
1334     T t511 o419 b510
1335 xiny 3379 B b511 t511
1336 xiny 3553 T t512 o506 b511
1337 xiny 3379 B b512 t512
1338 xiny 3553 P p512 Number 410
1339     P p513 Number 427
1340     O o513 location p512 p513
1341     O o514 str_open p512 p513
1342     P p514 String Simple_print
1343     O o515 string p514
1344     T t515 o515
1345 xiny 3527 B b515 t515
1346 xiny 3553 T t516 o b515 b4
1347     B b516 t516
1348     T t517 o514 b516
1349     B b517 t517
1350     T t518 o419 b517
1351 xiny 3527 B b518 t518
1352 xiny 3553 T t519 o513 b518
1353 xiny 3379 B b519 t519
1354 xiny 3553 P p519 Number 429
1355     P p520 Number 445
1356     O o520 location p519 p520
1357     O o521 str_open p519 p520
1358     P p521 String Tactic_type
1359     O o522 string p521
1360     T t522 o522
1361 xiny 3527 B b522 t522
1362 xiny 3553 T t523 o b522 b4
1363     B b523 t523
1364     T t524 o521 b523
1365     B b524 t524
1366     T t525 o419 b524
1367 xiny 3527 B b525 t525
1368 xiny 3553 T t526 o520 b525
1369 xiny 3527 B b526 t526
1370 xiny 3553 P p526 Number 446
1371     P p527 Number 472
1372     O o527 location p526 p527
1373     O o528 str_open p526 p527
1374     P p528 String Tacticals
1375     O o529 string p528
1376     T t529 o529
1377 xiny 3404 B b529 t529
1378 xiny 3553 T t530 o b529 b4
1379     B b530 t530
1380     T t531 o b522 b530
1381     B b531 t531
1382     T t532 o528 b531
1383 xiny 3527 B b532 t532
1384 xiny 3553 T t533 o419 b532
1385 xiny 3527 B b533 t533
1386 xiny 3553 T t534 o527 b533
1387 xiny 3527 B b534 t534
1388 xiny 3553 P p534 Number 473
1389     P p535 Number 497
1390     O o535 location p534 p535
1391     O o536 str_open p534 p535
1392     P p536 String Sequent
1393     O o537 string p536
1394     T t537 o537
1395 xiny 3527 B b537 t537
1396 xiny 3553 T t538 o b537 b4
1397     B b538 t538
1398     T t539 o b522 b538
1399     B b539 t539
1400     T t540 o536 b539
1401 xiny 3527 B b540 t540
1402 xiny 3553 T t541 o419 b540
1403 xiny 3527 B b541 t541
1404 xiny 3553 T t542 o535 b541
1405 xiny 3379 B b542 t542
1406 xiny 3553 P p542 Number 498
1407     P p543 Number 528
1408     O o543 location p542 p543
1409     O o544 str_open p542 p543
1410     P p544 String Conversionals
1411     O o545 string p544
1412     T t545 o545
1413 xiny 3527 B b545 t545
1414 xiny 3553 T t546 o b545 b4
1415     B b546 t546
1416     T t547 o b522 b546
1417     B b547 t547
1418     T t548 o544 b547
1419 xiny 3527 B b548 t548
1420 xiny 3553 T t549 o419 b548
1421 xiny 3379 B b549 t549
1422 xiny 3553 T t550 o543 b549
1423 xiny 3404 B b550 t550
1424 xiny 3553 P p550 Number 529
1425     P p551 Number 539
1426     O o551 location p550 p551
1427     O o552 str_open p550 p551
1428     O o553 string p91
1429     T t553 o553
1430 xiny 3527 B b553 t553
1431 xiny 3553 T t554 o b553 b4
1432     B b554 t554
1433     T t555 o552 b554
1434     B b555 t555
1435     T t556 o419 b555
1436 xiny 3498 B b556 t556
1437 xiny 3553 T t557 o551 b556
1438 xiny 3498 B b557 t557
1439 xiny 3553 P p557 Number 540
1440     P p558 Number 548
1441     O o558 location p557 p558
1442     O o559 str_open p557 p558
1443     O o560 string p89
1444     T t560 o560
1445 xiny 3527 B b560 t560
1446 xiny 3553 T t561 o b560 b4
1447     B b561 t561
1448     T t562 o559 b561
1449     B b562 t562
1450     T t563 o419 b562
1451 xiny 3527 B b563 t563
1452 xiny 3553 T t564 o558 b563
1453 xiny 3404 B b564 t564
1454 xiny 3553 P p564 Number 550
1455     P p565 Number 567
1456     O o565 location p564 p565
1457     O o566 str_open p564 p565
1458     O o567 string p79
1459     T t567 o567
1460 xiny 3527 B b567 t567
1461 xiny 3553 T t568 o b567 b4
1462     B b568 t568
1463     T t569 o566 b568
1464     B b569 t569
1465     T t570 o419 b569
1466 xiny 3498 B b570 t570
1467 xiny 3553 T t571 o565 b570
1468 xiny 3498 B b571 t571
1469 xiny 3553 P p571 Number 568
1470     P p572 Number 589
1471     O o572 location p571 p572
1472     O o573 str_open p571 p572
1473     O o574 string p81
1474     T t574 o574
1475 xiny 3527 B b574 t574
1476 xiny 3553 T t575 o b574 b4
1477     B b575 t575
1478     T t576 o573 b575
1479     B b576 t576
1480     T t577 o419 b576
1481 xiny 3498 B b577 t577
1482 xiny 3553 T t578 o572 b577
1483 xiny 3498 B b578 t578
1484 xiny 3553 P p578 Number 591
1485     P p579 Number 608
1486     O o579 location p578 p579
1487 xiny 3527 NSummary!opname opname opname Summary
1488 xiny 3553 P p580 String group
1489     O o580 opname p580
1490 xiny 3527 NCzf_itt_group Czf_itt_group Czf_itt_group NIL
1491     NCzf_itt_group!group group group Czf_itt_group
1492 xiny 3553 O o581 group
1493 xiny 3527 Nvar var var NIL
1494 xiny 3553 P p581 Var g
1495     O o582 var p581
1496     T t582 o582
1497     B b582 t582
1498     T t583 o581 b582
1499     B b583 t583
1500     T t584 o580 b583
1501     B b584 t584
1502     T t585 o579 b584
1503 xiny 3527 B b585 t585
1504 xiny 3553 P p585 Number 609
1505     P p586 Number 624
1506     O o586 location p585 p586
1507     P p587 String car
1508     O o587 opname p587
1509     NCzf_itt_group!car car car Czf_itt_group
1510     O o588 car
1511     T t588 o588 b582
1512 xiny 3527 B b588 t588
1513 xiny 3553 T t589 o587 b588
1514     B b589 t589
1515     T t590 o586 b589
1516     B b590 t590
1517     P p590 Number 671
1518     P p591 Number 686
1519     O o591 location p590 p591
1520     P p592 String eqG
1521     O o592 opname p592
1522     NCzf_itt_group!eqG eqG eqG Czf_itt_group
1523     O o593 eqG
1524     T t593 o593 b582
1525 xiny 3527 B b593 t593
1526 xiny 3553 T t594 o592 b593
1527     B b594 t594
1528     T t595 o591 b594
1529     B b595 t595
1530     P p595 Number 812
1531     P p596 Number 834
1532     O o596 location p595 p596
1533     P p597 String op
1534     O o597 opname p597
1535 xiny 3527 NCzf_itt_group!op op op Czf_itt_group
1536 xiny 3553 O o598 op
1537     P p598 Var a
1538     O o599 var p598
1539     T t599 o599
1540 xiny 3527 B b599 t599
1541 xiny 3553 P p599 Var b
1542     O o600 var p599
1543     T t600 o600
1544 xiny 3379 B b600 t600
1545 xiny 3553 T t601 o598 b582 b599 b600
1546 xiny 3379 B b601 t601
1547 xiny 3553 T t602 o597 b601
1548     B b602 t602
1549     T t603 o596 b602
1550     B b603 t603
1551     P p603 Number 835
1552     P p604 Number 849
1553     O o604 location p603 p604
1554     P p605 String id
1555     O o605 opname p605
1556 xiny 3527 NCzf_itt_group!id id id Czf_itt_group
1557 xiny 3553 O o606 id
1558     T t606 o606 b582
1559 xiny 3379 B b606 t606
1560 xiny 3553 T t607 o605 b606
1561     B b607 t607
1562     T t608 o604 b607
1563     B b608 t608
1564     P p608 Number 850
1565     P p609 Number 869
1566     O o609 location p608 p609
1567     P p610 String inv
1568     O o610 opname p610
1569 xiny 3527 NCzf_itt_group!inv inv inv Czf_itt_group
1570 xiny 3553 O o611 inv
1571     T t611 o611 b582 b599
1572 xiny 3379 B b611 t611
1573 xiny 3553 T t612 o610 b611
1574     B b612 t612
1575     T t613 o609 b612
1576 xiny 3404 B b613 t613
1577 xiny 3553 P p613 Number 1012
1578     P p614 Number 1082
1579     O o614 location p613 p614
1580 xiny 3527 NSummary!dform dform dform Summary
1581 xiny 3553 P p615 String group_df
1582     O o615 dform p615
1583 xiny 3527 NSummary!except_mode_df except_mode_df except_mode_df Summary
1584 xiny 3553 P p616 String src
1585     O o616 except_mode_df p616
1586     T t616 o616
1587     B b616 t616
1588     T t617 o b616 b4
1589 xiny 3379 B b617 t617
1590 xiny 3527 NSummary!df_term df_term df_term Summary
1591 xiny 3553 O o617 df_term
1592 xiny 3527 Nslot slot slot NIL
1593 xiny 3553 O o618 slot
1594     T t618 o618 b582
1595     B b618 t618
1596     NPerv!string string618 string Perv
1597     P p618 String " group"
1598     O o619 string618 p618
1599     T t619 o619
1600 xiny 3527 B b619 t619
1601 xiny 3553 T t620 o b619 b4
1602 xiny 3527 B b620 t620
1603 xiny 3553 T t621 o b618 b620
1604 xiny 3498 B b621 t621
1605 xiny 3553 T t622 o617 b621
1606 xiny 3404 B b622 t622
1607 xiny 3553 T t623 o615 b617 b583 b622
1608 xiny 3404 B b623 t623
1609 xiny 3553 T t624 o614 b623
1610 xiny 3498 B b624 t624
1611 xiny 3553 P p624 Number 1084
1612     P p625 Number 1153
1613     O o625 location p624 p625
1614     P p626 String car_df
1615     O o626 dform p626
1616     P p627 String car(
1617     O o627 string618 p627
1618     T t627 o627
1619     B b627 t627
1620     P p628 String )
1621     O o628 string618 p628
1622 xiny 3498 T t628 o628
1623     B b628 t628
1624 xiny 3553 T t629 o b628 b4
1625 xiny 3498 B b629 t629
1626 xiny 3553 T t630 o b618 b629
1627 xiny 3498 B b630 t630
1628 xiny 3553 T t631 o b627 b630
1629 xiny 3498 B b631 t631
1630 xiny 3553 T t632 o617 b631
1631 xiny 3498 B b632 t632
1632 xiny 3553 T t633 o626 b617 b588 b632
1633 xiny 3527 B b633 t633
1634 xiny 3553 T t634 o625 b633
1635 xiny 3527 B b634 t634
1636 xiny 3553 P p634 Number 1155
1637     P p635 Number 1225
1638     O o635 location p634 p635
1639     P p636 String eqG_df1
1640     O o636 dform p636
1641     P p637 String eqG(
1642     O o637 string618 p637
1643     T t637 o637
1644     B b637 t637
1645     T t638 o b637 b630
1646 xiny 3527 B b638 t638
1647 xiny 3553 T t639 o617 b638
1648 xiny 3527 B b639 t639
1649 xiny 3553 T t640 o636 b617 b593 b639
1650 xiny 3527 B b640 t640
1651 xiny 3553 T t641 o635 b640
1652 xiny 3527 B b641 t641
1653 xiny 3553 P p641 Number 1342
1654     P p642 Number 1408
1655     O o642 location p641 p642
1656     P p643 String id_df
1657     O o643 dform p643
1658     P p644 String id(
1659     O o644 string618 p644
1660     T t644 o644
1661     B b644 t644
1662     T t645 o b644 b630
1663 xiny 3527 B b645 t645
1664 xiny 3553 T t646 o617 b645
1665 xiny 3498 B b646 t646
1666 xiny 3553 T t647 o643 b617 b606 b646
1667 xiny 3527 B b647 t647
1668 xiny 3553 T t648 o642 b647
1669 xiny 3527 B b648 t648
1670 xiny 3553 P p648 Number 1410
1671     P p649 Number 1525
1672     O o649 location p648 p649
1673     P p650 String op_df
1674     O o650 dform p650
1675     NSummary!parens_df parens_df parens_df Summary
1676     O o651 parens_df
1677     T t651 o651
1678 xiny 3527 B b651 t651
1679 xiny 3553 T t652 o b651 b4
1680 xiny 3527 B b652 t652
1681 xiny 3553 T t653 o b616 b652
1682 xiny 3527 B b653 t653
1683 xiny 3553 P p653 String op(
1684     O o653 string618 p653
1685     T t654 o653
1686 xiny 3527 B b654 t654
1687 xiny 3553 P p654 String "; "
1688     O o654 string618 p654
1689     T t655 o654
1690 xiny 3527 B b655 t655
1691 xiny 3553 T t656 o618 b599
1692 xiny 3527 B b656 t656
1693 xiny 3553 T t657 o618 b600
1694 xiny 3527 B b657 t657
1695 xiny 3553 T t658 o b657 b629
1696 xiny 3527 B b658 t658
1697 xiny 3553 T t659 o b655 b658
1698 xiny 3527 B b659 t659
1699 xiny 3553 T t660 o b656 b659
1700 xiny 3527 B b660 t660
1701 xiny 3553 T t661 o b655 b660
1702 xiny 3527 B b661 t661
1703 xiny 3553 T t662 o b618 b661
1704 xiny 3527 B b662 t662
1705 xiny 3553 T t663 o b654 b662
1706     B b663 t663
1707     T t664 o617 b663
1708 xiny 3527 B b664 t664
1709 xiny 3553 T t665 o650 b653 b601 b664
1710 xiny 3527 B b665 t665
1711 xiny 3553 T t666 o649 b665
1712 xiny 3527 B b666 t666
1713 xiny 3553 P p666 Number 1527
1714     P p667 Number 1625
1715     O o667 location p666 p667
1716     P p668 String inv_df
1717     O o668 dform p668
1718     P p669 String inv(
1719     O o669 string618 p669
1720     T t669 o669
1721 xiny 3527 B b669 t669
1722 xiny 3553 T t670 o b656 b629
1723 xiny 3527 B b670 t670
1724 xiny 3553 T t671 o b655 b670
1725 xiny 3527 B b671 t671
1726 xiny 3553 T t672 o b618 b671
1727 xiny 3527 B b672 t672
1728 xiny 3553 T t673 o b669 b672
1729     B b673 t673
1730     T t674 o617 b673
1731     B b674 t674
1732     T t675 o668 b653 b611 b674
1733     B b675 t675
1734     T t676 o667 b675
1735     B b676 t676
1736     P p676 Number 1644
1737     P p677 Number 1778
1738     O o677 location p676 p677
1739 xiny 3498 NSummary!rule rule rule Summary
1740 xiny 3553 P p678 String group_type
1741     O o678 rule p678
1742 xiny 3498 NSummary!context_param context_param context_param Summary
1743 xiny 3553 P p679 String H
1744     O o679 context_param p679
1745     T t679 o679
1746     B b679 t679
1747     T t680 o b679 b4
1748     B b680 t680
1749 xiny 3498 NSummary!meta_implies meta_implies meta_implies Summary
1750 xiny 3553 O o680 meta_implies
1751 xiny 3498 NSummary!meta_theorem meta_theorem meta_theorem Summary
1752 xiny 3553 O o681 meta_theorem
1753 xiny 3498 NBase_trivial Base_trivial Base_trivial NIL
1754     NBase_trivial!squash squash squash Base_trivial
1755 xiny 3553 O o682 squash
1756     T t682 o682
1757     B b682 t682
1758     T t683 o b682 b4
1759 xiny 3498 C h H
1760     NItt_equal Itt_equal Itt_equal NIL
1761     NItt_equal!equal equal equal Itt_equal
1762 xiny 3553 O o683 equal
1763 xiny 3498 NItt_record_label0 Itt_record_label0 Itt_record_label0 NIL
1764     NItt_record_label0!label label label Itt_record_label0
1765 xiny 3553 O o684 label
1766     T t684 o684
1767     B b684 t684
1768     T t685 o683 b684 b582 b582
1769     S s t683 h
1770     G s t685
1771     B b685 s
1772     T t686 o681 b685
1773 xiny 3527 B b686 t686
1774 xiny 3553 P p686 Var ext
1775     O o686 var p686
1776     T t687 o686
1777 xiny 3527 B b687 t687
1778 xiny 3553 T t688 o b687 b4
1779     NItt_equal!type type type Itt_equal
1780     O o688 type
1781     T t689 o688 b583
1782     S s689 t688 h
1783     G s689 t689
1784     B b689 s689
1785     T t690 o681 b689
1786     B b690 t690
1787     T t691 o680 b686 b690
1788     B b691 t691
1789 xiny 3498 NSummary!incomplete incomplete incomplete Summary
1790 xiny 3553 O o691 incomplete
1791     T t692 o691
1792     B b692 t692
1793 xiny 3498 NSummary!resource_defs resource_defs resource_defs Summary
1794 xiny 3553 P p692 Number 1670
1795     P p693 Number 1678
1796     O o693 resource_defs p692 p693 p204
1797 xiny 3498 NOcaml!uid uid uid Ocaml
1798 xiny 3553 P p694 Number 1676
1799     O o694 uid p694 p693
1800     P p695 String []
1801     O o695 uid p695
1802     T t695 o695
1803 xiny 3527 B b695 t695
1804 xiny 3553 T t696 o694 b695
1805 xiny 3527 B b696 t696
1806 xiny 3553 T t697 o b696 b4
1807 xiny 3527 B b697 t697
1808 xiny 3553 T t698 o693 b697
1809     B b698 t698
1810     T t699 o b698 b4
1811     B b699 t699
1812     T t700 o678 b680 b691 b692 b699
1813     B b700 t700
1814     T t701 o677 b700
1815     B b701 t701
1816     P p701 Number 1780
1817     P p702 Number 1906
1818     O o702 location p701 p702
1819     P p703 String car_wf
1820     O o703 rule p703
1821 xiny 3498 NCzf_itt_set Czf_itt_set Czf_itt_set NIL
1822     NCzf_itt_set!isset isset isset Czf_itt_set
1823 xiny 3553 O o704 isset
1824     T t704 o704 b588
1825     S s704 t688 h
1826     G s704 t704
1827     B b704 s704
1828     T t705 o681 b704
1829     B b705 t705
1830     T t706 o680 b686 b705
1831 xiny 3527 B b706 t706
1832 xiny 3553 P p706 Number 1802
1833     P p707 Number 1809
1834     O o707 resource_defs p706 p707 p204
1835     P p708 Number 1807
1836     O o708 uid p708 p707
1837     T t708 o708 b695
1838 xiny 3494 B b708 t708
1839 xiny 3527 T t709 o b708 b4
1840 xiny 3498 B b709 t709
1841 xiny 3553 T t710 o707 b709
1842 xiny 3498 B b710 t710
1843 xiny 3553 T t711 o b710 b4
1844 xiny 3498 B b711 t711
1845 xiny 3553 T t712 o703 b680 b706 b692 b711
1846     B b712 t712
1847     T t713 o702 b712
1848     B b713 t713
1849     P p713 Number 1908
1850     P p714 Number 2035
1851     O o714 location p713 p714
1852     P p715 String eqG_wf1
1853     O o715 rule p715
1854     T t715 o704 b593
1855     S s715 t688 h
1856 xiny 3527 G s715 t715
1857     B b715 s715
1858 xiny 3553 T t716 o681 b715
1859 xiny 3527 B b716 t716
1860 xiny 3553 T t717 o680 b686 b716
1861 xiny 3527 B b717 t717
1862 xiny 3553 P p717 Number 1931
1863     P p718 Number 1938
1864     O o718 resource_defs p717 p718 p204
1865     P p719 Number 1936
1866     O o719 uid p719 p718
1867     T t719 o719 b695
1868 xiny 3527 B b719 t719
1869 xiny 3553 T t720 o b719 b4
1870 xiny 3527 B b720 t720
1871 xiny 3553 T t721 o718 b720
1872     B b721 t721
1873     T t722 o b721 b4
1874 xiny 3494 B b722 t722
1875 xiny 3553 T t723 o715 b680 b717 b692 b722
1876 xiny 3527 B b723 t723
1877 xiny 3553 T t724 o714 b723
1878 xiny 3498 B b724 t724
1879 xiny 3553 P p724 Number 2037
1880     P p725 Number 2215
1881     O o725 location p724 p725
1882     P p726 String eqG_wf2
1883     O o726 rule p726
1884     S s726 t688 h
1885     G s726 t583
1886     B b726 s726
1887     T t726 o681 b726
1888     B b727 t726
1889     NCzf_itt_equiv Czf_itt_equiv Czf_itt_equiv NIL
1890     NCzf_itt_equiv!equiv equiv equiv Czf_itt_equiv
1891     O o727 equiv
1892     T t727 o727 b588 b593
1893     S s727 t688 h
1894     G s727 t727
1895     B b728 s727
1896     T t728 o681 b728
1897     B b729 t728
1898     T t729 o680 b727 b729
1899     B b730 t729
1900     T t730 o680 b686 b730
1901     B b731 t730
1902     P p731 Number 2060
1903     P p732 Number 2067
1904     O o732 resource_defs p731 p732 p204
1905     P p733 Number 2065
1906     O o733 uid p733 p732
1907     T t733 o733 b695
1908 xiny 3527 B b733 t733
1909 xiny 3553 T t734 o b733 b4
1910     B b734 t734
1911     T t735 o732 b734
1912     B b735 t735
1913     T t736 o b735 b4
1914     B b736 t736
1915     T t737 o726 b680 b731 b692 b736
1916 xiny 3527 B b737 t737
1917 xiny 3553 T t738 o725 b737
1918     B b738 t738
1919     P p738 Number 2910
1920     P p739 Number 3134
1921     O o739 location p738 p739
1922     P p740 String op_wf
1923     O o740 rule p740
1924     P p741 Var s1
1925     O o741 var p741
1926     T t741 o741
1927 xiny 3527 B b741 t741
1928 xiny 3553 T t742 o704 b741
1929     S s742 t683 h
1930     G s742 t742
1931     B b742 s742
1932     T t743 o681 b742
1933 xiny 3527 B b743 t743
1934 xiny 3553 P p743 Var s2
1935     O o743 var p743
1936     T t744 o743
1937 xiny 3498 B b744 t744
1938 xiny 3553 T t745 o704 b744
1939     S s745 t683 h
1940     G s745 t745
1941     B b745 s745
1942     T t746 o681 b745
1943 xiny 3527 B b746 t746
1944 xiny 3553 T t747 o598 b582 b741 b744
1945 xiny 3498 B b747 t747
1946 xiny 3553 T t748 o704 b747
1947     S s748 t688 h
1948     G s748 t748
1949     B b748 s748
1950     T t749 o681 b748
1951 xiny 3527 B b749 t749
1952 xiny 3553 T t750 o680 b746 b749
1953 xiny 3527 B b750 t750
1954 xiny 3553 T t751 o680 b743 b750
1955 xiny 3527 B b751 t751
1956 xiny 3553 T t752 o680 b686 b751
1957 xiny 3527 B b752 t752
1958 xiny 3553 P p752 Number 2938
1959     O o752 resource_defs p230 p752 p204
1960     P p753 Number 2936
1961     O o753 uid p753 p752
1962     T t753 o753 b695
1963 xiny 3527 B b753 t753
1964 xiny 3553 T t754 o b753 b4
1965     B b754 t754
1966     T t755 o752 b754
1967     B b755 t755
1968     T t756 o b755 b4
1969 xiny 3527 B b756 t756
1970 xiny 3553 T t757 o740 b680 b752 b692 b756
1971     B b757 t757
1972     T t758 o739 b757
1973 xiny 3527 B b758 t758
1974 xiny 3553 P p758 Number 3136
1975     P p759 Number 3514
1976     O o759 location p758 p759
1977     P p760 String op_closure
1978     O o760 rule p760
1979     NCzf_itt_member Czf_itt_member Czf_itt_member NIL
1980     NCzf_itt_member!mem mem mem Czf_itt_member
1981     O o761 mem
1982     T t761 o761 b741 b588
1983     S s761 t688 h
1984     G s761 t761
1985     B b761 s761
1986     T t762 o681 b761
1987     B b762 t762
1988     T t763 o761 b744 b588
1989     S s763 t688 h
1990     G s763 t763
1991     B b763 s763
1992     T t764 o681 b763
1993     B b764 t764
1994     T t765 o761 b747 b588
1995     S s765 t688 h
1996     G s765 t765
1997     B b765 s765
1998     T t766 o681 b765
1999     B b766 t766
2000     T t767 o680 b764 b766
2001 xiny 3527 B b767 t767
2002 xiny 3553 T t768 o680 b762 b767
2003 xiny 3527 B b768 t768
2004 xiny 3553 T t769 o680 b727 b768
2005 xiny 3527 B b769 t769
2006 xiny 3553 T t770 o680 b686 b769
2007     B b770 t770
2008     T t771 o680 b746 b770
2009 xiny 3527 B b771 t771
2010 xiny 3553 T t772 o680 b743 b771
2011 xiny 3527 B b772 t772
2012 xiny 3553 P p772 Number 3162
2013     P p773 Number 3169
2014     O o773 resource_defs p772 p773 p204
2015     P p774 Number 3167
2016     O o774 uid p774 p773
2017     T t774 o774 b695
2018 xiny 3527 B b774 t774
2019 xiny 3553 T t775 o b774 b4
2020 xiny 3527 B b775 t775
2021 xiny 3553 T t776 o773 b775
2022 xiny 3527 B b776 t776
2023 xiny 3553 T t777 o b776 b4
2024 xiny 3527 B b777 t777
2025 xiny 3553 T t778 o760 b680 b772 b692 b777
2026 xiny 3527 B b778 t778
2027 xiny 3553 T t779 o759 b778
2028 xiny 3527 B b779 t779
2029 xiny 3553 P p779 Number 3516
2030     P p780 Number 4081
2031     O o780 location p779 p780
2032     P p781 String op_eqG1
2033     O o781 rule p781
2034     P p782 Var s3
2035     O o782 var p782
2036     T t782 o782
2037 xiny 3527 B b782 t782
2038 xiny 3553 T t783 o704 b782
2039     S s783 t683 h
2040     G s783 t783
2041     B b783 s783
2042     T t784 o681 b783
2043 xiny 3405 B b784 t784
2044 xiny 3553 T t785 o761 b782 b588
2045     S s785 t688 h
2046     G s785 t785
2047     B b785 s785
2048     T t786 o681 b785
2049 xiny 3527 B b786 t786
2050 xiny 3553 T t787 o727 b588 b593 b741 b744
2051     S s787 t688 h
2052     G s787 t787
2053     B b787 s787
2054     T t788 o681 b787
2055 xiny 3498 B b788 t788
2056 xiny 3553 T t789 o598 b582 b782 b741
2057 xiny 3498 B b789 t789
2058 xiny 3553 T t790 o598 b582 b782 b744
2059     B b790 t790
2060     T t791 o727 b588 b593 b789 b790
2061     S s791 t688 h
2062     G s791 t791
2063     B b791 s791
2064     T t792 o681 b791
2065 xiny 3527 B b792 t792
2066 xiny 3553 T t793 o680 b788 b792
2067     B b793 t793
2068     T t794 o680 b786 b793
2069 xiny 3527 B b794 t794
2070 xiny 3553 T t795 o680 b764 b794
2071 xiny 3527 B b795 t795
2072 xiny 3553 T t796 o680 b762 b795
2073 xiny 3527 B b796 t796
2074 xiny 3553 T t797 o680 b727 b796
2075 xiny 3527 B b797 t797
2076 xiny 3553 T t798 o680 b686 b797
2077 xiny 3527 B b798 t798
2078 xiny 3553 T t799 o680 b784 b798
2079 xiny 3527 B b799 t799
2080 xiny 3553 T t800 o680 b746 b799
2081 xiny 3498 B b800 t800
2082 xiny 3553 T t801 o680 b743 b800
2083 xiny 3494 B b801 t801
2084 xiny 3553 P p801 Number 3539
2085     P p802 Number 3546
2086     O o802 resource_defs p801 p802 p204
2087     P p803 Number 3544
2088     O o803 uid p803 p802
2089     T t803 o803 b695
2090 xiny 3527 B b803 t803
2091 xiny 3553 T t804 o b803 b4
2092 xiny 3527 B b804 t804
2093 xiny 3553 T t805 o802 b804
2094 xiny 3527 B b805 t805
2095 xiny 3553 T t806 o b805 b4
2096     B b806 t806
2097     T t807 o781 b680 b801 b692 b806
2098 xiny 3527 B b807 t807
2099 xiny 3553 T t808 o780 b807
2100 xiny 3527 B b808 t808
2101 xiny 3553 P p808 Number 4083
2102     P p809 Number 4648
2103     O o809 location p808 p809
2104     P p810 String op_eqG2
2105     O o810 rule p810
2106     T t810 o598 b582 b741 b782
2107 xiny 3527 B b810 t810
2108 xiny 3553 T t811 o598 b582 b744 b782
2109 xiny 3498 B b811 t811
2110 xiny 3553 T t812 o727 b588 b593 b810 b811
2111     S s812 t688 h
2112     G s812 t812
2113     B b812 s812
2114     T t813 o681 b812
2115     B b813 t813
2116     T t814 o680 b788 b813
2117     B b814 t814
2118     T t815 o680 b786 b814
2119 xiny 3527 B b815 t815
2120 xiny 3553 T t816 o680 b764 b815
2121     B b816 t816
2122     T t817 o680 b762 b816
2123 xiny 3527 B b817 t817
2124 xiny 3553 T t818 o680 b727 b817
2125 xiny 3527 B b818 t818
2126 xiny 3553 T t819 o680 b686 b818
2127     B b819 t819
2128     T t820 o680 b784 b819
2129     B b820 t820
2130     T t821 o680 b746 b820
2131 xiny 3527 B b821 t821
2132 xiny 3553 T t822 o680 b743 b821
2133 xiny 3527 B b822 t822
2134 xiny 3553 P p822 Number 4106
2135     P p823 Number 4113
2136     O o823 resource_defs p822 p823 p204
2137     P p824 Number 4111
2138     O o824 uid p824 p823
2139     T t824 o824 b695
2140 xiny 3527 B b824 t824
2141 xiny 3553 T t825 o b824 b4
2142 xiny 3527 B b825 t825
2143 xiny 3553 T t826 o823 b825
2144 xiny 3527 B b826 t826
2145 xiny 3553 T t827 o b826 b4
2146     B b827 t827
2147     T t828 o810 b680 b822 b692 b827
2148 xiny 3527 B b828 t828
2149 xiny 3553 T t829 o809 b828
2150 xiny 3527 B b829 t829
2151 xiny 3553 P p829 Number 4650
2152     P p830 Number 4903
2153     O o830 location p829 p830
2154     P p831 String op_eqG_fun1
2155     O o831 rule p831
2156     P p832 Var s
2157     O o832 var p832
2158     T t832 o832
2159 xiny 3527 B b832 t832
2160 xiny 3553 T t833 o704 b832
2161     S s833 t683 h
2162     G s833 t833
2163     B b833 s833
2164     T t834 o681 b833
2165     B b834 t834
2166     NCzf_itt_equiv!equiv_fun_set equiv_fun_set equiv_fun_set Czf_itt_equiv
2167     O o834 equiv_fun_set
2168     P p834 Var z
2169     O o835 var p834
2170     T t835 o835
2171     B b835 t835
2172     T t836 o598 b582 b835 b832
2173     B b836 t836 z
2174     T t837 o834 b588 b593 b836
2175     S s837 t688 h
2176     G s837 t837
2177     B b837 s837
2178     T t838 o681 b837
2179 xiny 3527 B b838 t838
2180 xiny 3553 T t839 o680 b727 b838
2181 xiny 3527 B b839 t839
2182 xiny 3553 T t840 o680 b686 b839
2183 xiny 3527 B b840 t840
2184 xiny 3553 T t841 o680 b834 b840
2185 xiny 3527 B b841 t841
2186 xiny 3553 P p841 Number 4677
2187     P p842 Number 4684
2188     O o842 resource_defs p841 p842 p204
2189     P p843 Number 4682
2190     O o843 uid p843 p842
2191     T t843 o843 b695
2192     B b843 t843
2193     T t844 o b843 b4
2194 xiny 3527 B b844 t844
2195 xiny 3553 T t845 o842 b844
2196 xiny 3527 B b845 t845
2197 xiny 3553 T t846 o b845 b4
2198 xiny 3527 B b846 t846
2199 xiny 3553 T t847 o831 b680 b841 b692 b846
2200 xiny 3527 B b847 t847
2201 xiny 3553 T t848 o830 b847
2202 xiny 3527 B b848 t848
2203 xiny 3553 P p848 Number 4905
2204     P p849 Number 5160
2205     O o849 location p848 p849
2206     P p850 String op_equiv_fun2
2207     O o850 rule p850
2208     T t850 o598 b582 b832 b835
2209     B b850 t850 z
2210     T t851 o834 b588 b593 b850
2211     S s851 t688 h
2212     G s851 t851
2213     B b851 s851
2214     T t852 o681 b851
2215     B b852 t852
2216     T t853 o680 b727 b852
2217 xiny 3498 B b853 t853
2218 xiny 3553 T t854 o680 b686 b853
2219 xiny 3527 B b854 t854
2220 xiny 3553 T t855 o680 b834 b854
2221 xiny 3527 B b855 t855
2222 xiny 3553 P p855 Number 4934
2223     P p856 Number 4941
2224     O o856 resource_defs p855 p856 p204
2225     P p857 Number 4939
2226     O o857 uid p857 p856
2227     T t857 o857 b695
2228     B b857 t857
2229     T t858 o b857 b4
2230 xiny 3527 B b858 t858
2231 xiny 3553 T t859 o856 b858
2232 xiny 3527 B b859 t859
2233 xiny 3553 T t860 o b859 b4
2234 xiny 3527 B b860 t860
2235 xiny 3553 T t861 o850 b680 b855 b692 b860
2236 xiny 3527 B b861 t861
2237 xiny 3553 T t862 o849 b861
2238 xiny 3527 B b862 t862
2239 xiny 3553 P p862 Number 5162
2240     P p863 Number 5390
2241     O o863 location p862 p863
2242     P p864 String op_eq_fun1
2243     O o864 rule p864
2244     NCzf_itt_eq Czf_itt_eq Czf_itt_eq NIL
2245     NCzf_itt_eq!fun_set fun_set fun_set Czf_itt_eq
2246     O o865 fun_set
2247     T t865 o865 b836
2248     S s865 t688 h
2249 xiny 3527 G s865 t865
2250     B b865 s865
2251 xiny 3553 T t866 o681 b865
2252 xiny 3527 B b866 t866
2253 xiny 3553 T t867 o680 b727 b866
2254 xiny 3527 B b867 t867
2255 xiny 3553 T t868 o680 b686 b867
2256 xiny 3527 B b868 t868
2257 xiny 3553 T t869 o680 b834 b868
2258 xiny 3527 B b869 t869
2259 xiny 3553 P p869 Number 5188
2260     P p870 Number 5195
2261 xiny 3527 O o870 resource_defs p869 p870 p204
2262 xiny 3553 P p871 Number 5193
2263 xiny 3527 O o871 uid p871 p870
2264 xiny 3553 T t871 o871 b695
2265 xiny 3527 B b871 t871
2266     T t872 o b871 b4
2267     B b872 t872
2268     T t873 o870 b872
2269     B b873 t873
2270     T t874 o b873 b4
2271     B b874 t874
2272 xiny 3553 T t875 o864 b680 b869 b692 b874
2273 xiny 3494 B b875 t875
2274 xiny 3553 T t876 o863 b875
2275 xiny 3494 B b876 t876
2276 xiny 3553 P p876 Number 5392
2277     P p877 Number 5620
2278 xiny 3527 O o877 location p876 p877
2279 xiny 3553 P p878 String op_eq_fun2
2280 xiny 3527 O o878 rule p878
2281 xiny 3553 T t878 o865 b850
2282     S s878 t688 h
2283     G s878 t878
2284     B b878 s878
2285     T t879 o681 b878
2286 xiny 3527 B b879 t879
2287 xiny 3553 T t880 o680 b727 b879
2288     B b880 t880
2289     T t881 o680 b686 b880
2290 xiny 3527 B b881 t881
2291 xiny 3553 T t882 o680 b834 b881
2292 xiny 3527 B b882 t882
2293 xiny 3553 P p882 Number 5418
2294     P p883 Number 5425
2295     O o883 resource_defs p882 p883 p204
2296     P p884 Number 5423
2297     O o884 uid p884 p883
2298     T t884 o884 b695
2299 xiny 3527 B b884 t884
2300 xiny 3553 T t885 o b884 b4
2301 xiny 3527 B b885 t885
2302 xiny 3553 T t886 o883 b885
2303 xiny 3527 B b886 t886
2304 xiny 3553 T t887 o b886 b4
2305 xiny 3527 B b887 t887
2306 xiny 3553 T t888 o878 b680 b882 b692 b887
2307 xiny 3527 B b888 t888
2308 xiny 3553 T t889 o877 b888
2309 xiny 3527 B b889 t889
2310 xiny 3553 P p889 Number 5622
2311     P p890 Number 6149
2312     O o890 location p889 p890
2313     P p891 String op_assoc1
2314     O o891 rule p891
2315     T t891 o598 b582 b747 b782
2316 xiny 3498 B b891 t891
2317 xiny 3553 T t892 o598 b582 b741 b811
2318     B b892 t892
2319     T t893 o727 b588 b593 b891 b892
2320     S s893 t688 h
2321     G s893 t893
2322     B b893 s893
2323     T t894 o681 b893
2324 xiny 3527 B b894 t894
2325 xiny 3553 T t895 o680 b786 b894
2326 xiny 3527 B b895 t895
2327 xiny 3553 T t896 o680 b764 b895
2328 xiny 3527 B b896 t896
2329 xiny 3553 T t897 o680 b762 b896
2330 xiny 3527 B b897 t897
2331 xiny 3553 T t898 o680 b727 b897
2332 xiny 3527 B b898 t898
2333 xiny 3553 T t899 o680 b686 b898
2334     B b899 t899
2335     T t900 o680 b784 b899
2336     B b900 t900
2337     T t901 o680 b746 b900
2338 xiny 3527 B b901 t901
2339 xiny 3553 T t902 o680 b743 b901
2340 xiny 3527 B b902 t902
2341 xiny 3553 P p902 Number 5647
2342     P p903 Number 5654
2343     O o903 resource_defs p902 p903 p204
2344     P p904 Number 5652
2345     O o904 uid p904 p903
2346     T t904 o904 b695
2347 xiny 3527 B b904 t904
2348 xiny 3553 T t905 o b904 b4
2349 xiny 3527 B b905 t905
2350 xiny 3553 T t906 o903 b905
2351 xiny 3405 B b906 t906
2352 xiny 3553 T t907 o b906 b4
2353 xiny 3527 B b907 t907
2354 xiny 3553 T t908 o891 b680 b902 b692 b907
2355 xiny 3405 B b908 t908
2356 xiny 3553 T t909 o890 b908
2357 xiny 3379 B b909 t909
2358 xiny 3553 P p909 Number 6151
2359     P p910 Number 6678
2360     O o910 location p909 p910
2361     P p911 String op_assoc2
2362     O o911 rule p911
2363     T t911 o727 b588 b593 b892 b891
2364     S s911 t688 h
2365     G s911 t911
2366     B b911 s911
2367     T t912 o681 b911
2368     B b912 t912
2369     T t913 o680 b786 b912
2370 xiny 3527 B b913 t913
2371 xiny 3553 T t914 o680 b764 b913
2372 xiny 3527 B b914 t914
2373 xiny 3553 T t915 o680 b762 b914
2374 xiny 3527 B b915 t915
2375 xiny 3553 T t916 o680 b727 b915
2376 xiny 3527 B b916 t916
2377 xiny 3553 T t917 o680 b686 b916
2378 xiny 3527 B b917 t917
2379 xiny 3553 T t918 o680 b784 b917
2380 xiny 3527 B b918 t918
2381 xiny 3553 T t919 o680 b746 b918
2382     B b919 t919
2383     T t920 o680 b743 b919
2384     B b920 t920
2385     P p920 Number 6176
2386     O o920 resource_defs p920 p202 p204
2387     O o921 uid p197 p202
2388     T t921 o921 b695
2389 xiny 3527 B b921 t921
2390 xiny 3553 T t922 o b921 b4
2391 xiny 3379 B b922 t922
2392 xiny 3553 T t923 o920 b922
2393 xiny 3498 B b923 t923
2394 xiny 3553 T t924 o b923 b4
2395     B b924 t924
2396     T t925 o911 b680 b920 b692 b924
2397 xiny 3498 B b925 t925
2398 xiny 3553 T t926 o910 b925
2399 xiny 3405 B b926 t926
2400 xiny 3553 P p926 Number 6680
2401     P p927 Number 6806
2402     O o927 location p926 p927
2403     P p928 String id_wf1
2404     O o928 rule p928
2405     T t928 o704 b606
2406     S s928 t688 h
2407     G s928 t928
2408     B b928 s928
2409     T t929 o681 b928
2410 xiny 3527 B b929 t929
2411 xiny 3553 T t930 o680 b686 b929
2412 xiny 3527 B b930 t930
2413 xiny 3553 P p930 Number 6702
2414     P p931 Number 6710
2415     O o931 resource_defs p930 p931 p204
2416     P p932 Number 6708
2417     O o932 uid p932 p931
2418     T t932 o932 b695
2419     B b932 t932
2420     T t933 o b932 b4
2421 xiny 3527 B b933 t933
2422 xiny 3553 T t934 o931 b933
2423 xiny 3527 B b934 t934
2424 xiny 3553 T t935 o b934 b4
2425 xiny 3527 B b935 t935
2426 xiny 3553 T t936 o928 b680 b930 b692 b935
2427     B b936 t936
2428     T t937 o927 b936
2429 xiny 3498 B b937 t937
2430 xiny 3553 P p937 Number 6808
2431     P p938 Number 6982
2432     O o938 location p937 p938
2433     P p939 String id_wf2
2434     O o939 rule p939
2435     T t939 o761 b606 b588
2436     S s939 t688 h
2437     G s939 t939
2438     B b939 s939
2439     T t940 o681 b939
2440 xiny 3527 B b940 t940
2441 xiny 3553 T t941 o680 b727 b940
2442 xiny 3527 B b941 t941
2443 xiny 3553 T t942 o680 b686 b941
2444 xiny 3527 B b942 t942
2445 xiny 3553 P p942 Number 6830
2446     P p943 Number 6837
2447     O o943 resource_defs p942 p943 p204
2448     P p944 Number 6835
2449     O o944 uid p944 p943
2450     T t944 o944 b695
2451     B b944 t944
2452     T t945 o b944 b4
2453 xiny 3527 B b945 t945
2454 xiny 3553 T t946 o943 b945
2455 xiny 3527 B b946 t946
2456 xiny 3553 T t947 o b946 b4
2457     B b947 t947
2458     T t948 o939 b680 b942 b692 b947
2459 xiny 3498 B b948 t948
2460 xiny 3553 T t949 o938 b948
2461 xiny 3527 B b949 t949
2462 xiny 3553 P p949 Number 6984
2463     P p950 Number 7278
2464     O o950 location p949 p950
2465     P p951 String id_eq1
2466     O o951 rule p951
2467     T t951 o761 b832 b588
2468     S s951 t688 h
2469     G s951 t951
2470     B b951 s951
2471     T t952 o681 b951
2472 xiny 3527 B b952 t952
2473 xiny 3553 T t953 o598 b582 b606 b832
2474 xiny 3527 B b953 t953
2475 xiny 3553 T t954 o727 b588 b593 b953 b832
2476     S s954 t688 h
2477     G s954 t954
2478     B b954 s954
2479     T t955 o681 b954
2480     B b955 t955
2481     T t956 o680 b952 b955
2482 xiny 3527 B b956 t956
2483 xiny 3553 T t957 o680 b727 b956
2484 xiny 3527 B b957 t957
2485 xiny 3553 T t958 o680 b686 b957
2486 xiny 3527 B b958 t958
2487 xiny 3553 T t959 o680 b834 b958
2488 xiny 3527 B b959 t959
2489 xiny 3553 P p959 Number 7006
2490     P p960 Number 7013
2491     O o960 resource_defs p959 p960 p204
2492     P p961 Number 7011
2493     O o961 uid p961 p960
2494     T t961 o961 b695
2495 xiny 3527 B b961 t961
2496 xiny 3553 T t962 o b961 b4
2497     B b962 t962
2498     T t963 o960 b962
2499 xiny 3498 B b963 t963
2500 xiny 3553 T t964 o b963 b4
2501     B b964 t964
2502     T t965 o951 b680 b959 b692 b964
2503 xiny 3527 B b965 t965
2504 xiny 3553 T t966 o950 b965
2505 xiny 3527 B b966 t966
2506 xiny 3553 P p966 Number 7280
2507     P p967 Number 7457
2508     O o967 location p966 p967
2509     P p968 String inv_wf1
2510     O o968 rule p968
2511     T t968 o611 b582 b741
2512 xiny 3527 B b968 t968
2513 xiny 3553 T t969 o704 b968
2514     S s969 t688 h
2515     G s969 t969
2516     B b969 s969
2517     T t970 o681 b969
2518 xiny 3527 B b970 t970
2519 xiny 3553 T t971 o680 b686 b970
2520 xiny 3527 B b971 t971
2521 xiny 3553 T t972 o680 b743 b971
2522     B b972 t972
2523     P p972 Number 7303
2524     P p973 Number 7310
2525     O o973 resource_defs p972 p973 p204
2526     P p974 Number 7308
2527     O o974 uid p974 p973
2528     T t974 o974 b695
2529     B b974 t974
2530     T t975 o b974 b4
2531     B b975 t975
2532     T t976 o973 b975
2533     B b976 t976
2534     T t977 o b976 b4
2535     B b977 t977
2536     T t978 o968 b680 b972 b692 b977
2537     B b978 t978
2538     T t979 o967 b978
2539     B b979 t979
2540     P p979 Number 7459
2541     P p980 Number 7735
2542     O o980 location p979 p980
2543     P p981 String inv_wf2
2544     O o981 rule p981
2545     T t981 o761 b968 b588
2546     S s981 t688 h
2547 xiny 3527 G s981 t981
2548     B b981 s981
2549 xiny 3553 T t982 o681 b981
2550 xiny 3379 B b982 t982
2551 xiny 3553 T t983 o680 b762 b982
2552 xiny 3379 B b983 t983
2553 xiny 3553 T t984 o680 b727 b983
2554 xiny 3527 B b984 t984
2555 xiny 3553 T t985 o680 b686 b984
2556 xiny 3527 B b985 t985
2557 xiny 3553 T t986 o680 b743 b985
2558 xiny 3527 B b986 t986
2559 xiny 3553 P p986 Number 7482
2560     P p987 Number 7489
2561     O o987 resource_defs p986 p987 p204
2562     P p988 Number 7487
2563     O o988 uid p988 p987
2564     T t988 o988 b695
2565     B b988 t988
2566     T t989 o b988 b4
2567     B b989 t989
2568     T t990 o987 b989
2569     B b990 t990
2570     T t991 o b990 b4
2571     B b991 t991
2572     T t992 o981 b680 b986 b692 b991
2573     B b992 t992
2574     T t993 o980 b992
2575     B b993 t993
2576     P p993 Number 7737
2577     P p994 Number 7946
2578     O o994 location p993 p994
2579     P p995 String inv_equiv_fun1
2580 xiny 3527 O o995 rule p995
2581 xiny 3553 T t995 o611 b582 b835
2582     B b995 t995 z
2583     T t996 o834 b588 b593 b995
2584     S s996 t688 h
2585     G s996 t996
2586     B b996 s996
2587     T t997 o681 b996
2588 xiny 3527 B b997 t997
2589 xiny 3553 T t998 o680 b727 b997
2590 xiny 3498 B b998 t998
2591 xiny 3553 T t999 o680 b686 b998
2592 xiny 3527 B b999 t999
2593 xiny 3553 P p999 Number 7767
2594     P p1000 Number 7774
2595     O o1000 resource_defs p999 p1000 p204
2596     P p1001 Number 7772
2597     O o1001 uid p1001 p1000
2598     T t1001 o1001 b695
2599     B b1001 t1001
2600     T t1002 o b1001 b4
2601     B b1002 t1002
2602     T t1003 o1000 b1002
2603     B b1003 t1003
2604     T t1004 o b1003 b4
2605     B b1004 t1004
2606     T t1005 o995 b680 b999 b692 b1004
2607     B b1005 t1005
2608     T t1006 o994 b1005
2609     B b1006 t1006
2610     P p1006 Number 7948
2611     P p1007 Number 8130
2612     O o1007 location p1006 p1007
2613     P p1008 String inv_eq_fun1
2614     O o1008 rule p1008
2615     T t1008 o865 b995
2616     S s1008 t688 h
2617     G s1008 t1008
2618     B b1008 s1008
2619     T t1009 o681 b1008
2620     B b1009 t1009
2621     T t1010 o680 b727 b1009
2622     B b1010 t1010
2623     T t1011 o680 b686 b1010
2624 xiny 3498 B b1011 t1011
2625 xiny 3553 P p1011 Number 7975
2626     P p1012 Number 7982
2627     O o1012 resource_defs p1011 p1012 p204
2628     P p1013 Number 7980
2629     O o1013 uid p1013 p1012
2630     T t1013 o1013 b695
2631 xiny 3498 B b1013 t1013
2632 xiny 3553 T t1014 o b1013 b4
2633 xiny 3498 B b1014 t1014
2634 xiny 3553 T t1015 o1012 b1014
2635 xiny 3527 B b1015 t1015
2636 xiny 3553 T t1016 o b1015 b4
2637     B b1016 t1016
2638     T t1017 o1008 b680 b1011 b692 b1016
2639     B b1017 t1017
2640     T t1018 o1007 b1017
2641     B b1018 t1018
2642     P p1018 Number 8132
2643     P p1019 Number 8440
2644     O o1019 location p1018 p1019
2645     P p1020 String inv_id1
2646     O o1020 rule p1020
2647     T t1020 o598 b582 b968 b741
2648     B b1020 t1020
2649     T t1021 o727 b588 b593 b1020 b606
2650     S s1021 t688 h
2651     G s1021 t1021
2652     B b1021 s1021
2653     T t1022 o681 b1021
2654     B b1022 t1022
2655     T t1023 o680 b762 b1022
2656     B b1023 t1023
2657     T t1024 o680 b727 b1023
2658     B b1024 t1024
2659     T t1025 o680 b686 b1024
2660 xiny 3527 B b1025 t1025
2661 xiny 3553 T t1026 o680 b743 b1025
2662 xiny 3527 B b1026 t1026
2663 xiny 3553 P p1026 Number 8155
2664     P p1027 Number 8162
2665     O o1027 resource_defs p1026 p1027 p204
2666     P p1028 Number 8160
2667     O o1028 uid p1028 p1027
2668     T t1028 o1028 b695
2669     B b1028 t1028
2670     T t1029 o b1028 b4
2671     B b1029 t1029
2672     T t1030 o1027 b1029
2673     B b1030 t1030
2674     T t1031 o b1030 b4
2675     B b1031 t1031
2676     T t1032 o1020 b680 b1026 b692 b1031
2677     B b1032 t1032
2678     T t1033 o1019 b1032
2679     B b1033 t1033
2680     P p1033 Number 8459
2681     P p1034 Number 9032
2682     O o1034 location p1033 p1034
2683     P p1035 String id_judge_elim
2684     O o1035 rule p1035
2685     P p1036 String J
2686     O o1036 context_param p1036
2687     T t1036 o1036
2688 xiny 3527 B b1036 t1036
2689 xiny 3553 T t1037 o b1036 b4
2690     B b1037 t1037
2691     T t1038 o b679 b1037
2692 xiny 3527 B b1038 t1038
2693 xiny 3553 T t1039 o598 b582 b832 b832
2694 xiny 3527 B b1039 t1039
2695 xiny 3553 T t1040 o727 b588 b593 b1039 b832
2696     H h1040 x t1040
2697     P p1040 Var x
2698     O o1040 var p1040
2699     T t1041 o1040
2700     C h1041 J t1041
2701     S s1041 t683 h h1040 h1041
2702     G s1041 t833
2703     B b1041 s1041
2704     T t1042 o681 b1041
2705 xiny 3527 B b1042 t1042
2706 xiny 3553 S s1042 t683 h h1040 h1041
2707     G s1042 t685
2708     B b1043 s1042
2709     T t1043 o681 b1043
2710     B b1044 t1043
2711     S s1044 t688 h h1040 h1041
2712     G s1044 t583
2713     B b1045 s1044
2714     T t1045 o681 b1045
2715     B b1046 t1045
2716     T t1046 o727 b588 b593 b832 b606
2717     H h1046 y t1046
2718     P p1046 Var C
2719     O o1046 var p1046
2720     B b1047 t1041
2721     T t1047 o1046 b1047
2722     S s1047 t688 h h1040 h1041 h1046
2723     G s1047 t1047
2724     B b1048 s1047
2725     T t1048 o681 b1048
2726     B b1049 t1048
2727     S s1049 t688 h h1040 h1041
2728     G s1049 t1047
2729     B b1050 s1049
2730     T t1050 o681 b1050
2731     B b1051 t1050
2732     T t1051 o680 b1049 b1051
2733     B b1052 t1051
2734     T t1052 o680 b1046 b1052
2735     B b1053 t1052
2736     T t1053 o680 b1044 b1053
2737     B b1054 t1053
2738     T t1054 o680 b1042 b1054
2739     B b1055 t1054
2740 xiny 3527 NSummary!interactive interactive interactive Summary
2741 xiny 3553 O o1055 interactive
2742 xiny 3527 NSummary!ext_rule ext_rule ext_rule Summary
2743 xiny 3553 P p1055 String "assertT << equiv{car{'g}; eqG{'g}; 's; id{'g}} >> ttca"
2744     O o1056 ext_rule p1055
2745 xiny 3527 NSummary!status_incomplete status_incomplete status_incomplete Summary
2746 xiny 3553 O o1057 status_incomplete
2747     T t1057 o1057
2748     B b1057 t1057
2749 xiny 3527 NSummary!ext_unjustified ext_unjustified ext_unjustified Summary
2750 xiny 3553 O o1058 ext_unjustified
2751 xiny 3527 NSummary!tactic_arg tactic_arg tactic_arg Summary
2752 xiny 3553 P p1058 String main
2753     O o1059 tactic_arg p1058
2754 xiny 3527 NSummary!msequent msequent msequent Summary
2755 xiny 3553 O o1060 msequent
2756     T t1060 o b1048 b4
2757     B b1060 t1060
2758     T t1061 o b1045 b1060
2759     B b1061 t1061
2760     T t1062 o b1043 b1061
2761     B b1062 t1062
2762     T t1063 o b1041 b1062
2763     B b1063 t1063
2764     T t1064 o1060 b1050 b1063
2765     B b1064 t1064
2766 xiny 3527 NSummary!parent_none parent_none parent_none Summary
2767 xiny 3553 O o1064 parent_none
2768     T t1065 o1064
2769     B b1065 t1065
2770     T t1066 o1059 b1064 b4 b1065
2771     B b1066 t1066
2772     P p1066 String assertion
2773     O o1066 tactic_arg p1066
2774     S s1066 t688 h h1040 h1041
2775     G s1066 t1046
2776     B b1067 s1066
2777     T t1067 o1060 b1067 b1063
2778     B b1068 t1067
2779     T t1068 o2 b1066
2780     B b1069 t1068
2781     T t1069 o1066 b1068 b4 b1069
2782     B b1070 t1069
2783     T t1070 o b1070 b4
2784     B b1071 t1070
2785     T t1071 o1058 b1066 b1071
2786     B b1072 t1071
2787     P p1072 String "equivSubstT << equiv{car{'g}; eqG{'g}; 's; op{'g; id{'g}; 's}} >> 0 ttca"
2788     O o1072 ext_rule p1072
2789     T t1072 o727 b588 b593 b832 b953
2790     S s1072 t688 h h1040 h1041
2791     G s1072 t1072
2792     B b1073 s1072
2793     T t1073 o1060 b1073 b1063
2794     B b1074 t1073
2795     T t1074 o2 b1070
2796     B b1075 t1074
2797     T t1075 o1066 b1074 b4 b1075
2798     B b1076 t1075
2799     T t1076 o727 b588 b593 b953 b606
2800     S s1076 t688 h h1040 h1041
2801     G s1076 t1076
2802     B b1077 s1076
2803     T t1077 o1060 b1077 b1063
2804     B b1078 t1077
2805     T t1078 o1066 b1078 b4 b1075
2806     B b1079 t1078
2807     T t1079 o b1079 b4
2808     B b1080 t1079
2809     T t1080 o b1076 b1080
2810     B b1081 t1080
2811     T t1081 o1058 b1070 b1081
2812     B b1082 t1081
2813     P p1082 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 's}; 's} >> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
2814     O o1082 ext_rule p1082
2815     T t1082 o1058 b1076 b4
2816     B b1083 t1082
2817     T t1083 o1082 b1057 b1083 b4 b4
2818     B b1084 t1083
2819     P p1084 String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'g}; op{'g; inv{'g; 's}; 's}} >> 0 ttca"
2820     O o1084 ext_rule p1084
2821     T t1084 o611 b582 b832
2822     B b1085 t1084
2823     T t1085 o598 b582 b1085 b832
2824     B b1086 t1085
2825     T t1086 o727 b588 b593 b606 b1086
2826     S s1086 t688 h h1040 h1041
2827     G s1086 t1086
2828     B b1087 s1086
2829     T t1087 o1060 b1087 b1063
2830     B b1088 t1087
2831     T t1088 o2 b1079
2832     B b1089 t1088
2833     T t1089 o1066 b1088 b4 b1089
2834     B b1090 t1089
2835     T t1090 o598 b582 b1086 b832
2836     B b1091 t1090
2837     T t1091 o727 b588 b593 b1091 b1086
2838     S s1091 t688 h h1040 h1041
2839     G s1091 t1091
2840     B b1092 s1091
2841     T t1092 o1060 b1092 b1063
2842     B b1093 t1092
2843     T t1093 o1066 b1093 b4 b1089
2844     B b1094 t1093
2845     NCzf_itt_equiv!equiv_fun_prop equiv_fun_prop equiv_fun_prop Czf_itt_equiv
2846     O o1094 equiv_fun_prop
2847     B b1095 t836
2848     T t1095 o727 b588 b593 b1095 b835
2849     B b1096 t1095 z
2850     T t1096 o1094 b588 b593 b1096
2851     S s1096 t688 h h1040 h1041
2852     G s1096 t1096
2853     B b1097 s1096
2854     T t1097 o1060 b1097 b1063
2855     B b1098 t1097
2856     T t1098 o1066 b1098 b4 b1089
2857     B b1099 t1098
2858     T t1099 o b1099 b4
2859     B b1100 t1099
2860     T t1100 o b1094 b1100
2861     B b1101 t1100
2862     T t1101 o b1090 b1101
2863     B b1102 t1101
2864     T t1102 o1058 b1079 b1102
2865     B b1103 t1102
2866     P p1103 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT thenT rwh unfold_equiv 2 ttca"
2867     O o1103 ext_rule p1103
2868     T t1103 o1058 b1090 b4
2869     B b1104 t1103
2870     T t1104 o1103 b1057 b1104 b4 b4
2871     B b1105 t1104
2872     P p1105 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; inv{'g; 's}; 's}; 's}; op{'g; inv{'g; 's}; op{'g; 's; 's}}}>> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
2873     O o1105 ext_rule p1105
2874     T t1105 o1058 b1094 b4
2875     B b1106 t1105
2876     T t1106 o1105 b1057 b1106 b4 b4
2877     B b1107 t1106
2878     P p1107 String "rwh unfold_equiv_fun_prop 0 thenT autoT"
2879     O o1107 ext_rule p1107
2880 xiny 3527 NCzf_itt_set!set set set Czf_itt_set
2881 xiny 3553 O o1108 set
2882 xiny 3527 T t1108 o1108
2883 xiny 3553 H h1108 a t1108
2884     H h1109 b t1108
2885     H h1110 x_1 t727
2886     T t1110 o727 b588 b593 b599 b600
2887     H h1111 x_2 t1110
2888     T t1111 o598 b582 b599 b832
2889 xiny 3498 B b1111 t1111
2890 xiny 3553 T t1112 o727 b588 b593 b1111 b599
2891     H h1112 x_3 t1112
2892     T t1113 o598 b582 b600 b832
2893     B b1113 t1113
2894     T t1114 o727 b588 b593 b1113 b600
2895     S s1114 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
2896     G s1114 t1114
2897     B b1114 s1114
2898     T t1115 o1060 b1114 b1063
2899 xiny 3527 B b1115 t1115
2900     NItt_logic Itt_logic Itt_logic NIL
2901     NItt_logic!implies implies implies Itt_logic
2902 xiny 3553 O o1115 implies
2903     B b1116 t1112
2904     B b1117 t1114
2905     T t1117 o1115 b1116 b1117
2906     S s1117 t688 h h1040 h1041 h1108 h1109 h1110 h1111
2907     G s1117 t1117
2908     B b1118 s1117
2909     T t1118 o1060 b1118 b1063
2910     B b1119 t1118
2911     NSummary!arg_named arg_named arg_named Summary
2912     P p1119 String d_auto
2913     O o1119 arg_named p1119
2914     NSummary!arg_bool arg_bool arg_bool Summary
2915     P p1120 String true
2916     O o1120 arg_bool p1120
2917     T t1120 o1120
2918     B b1120 t1120
2919     T t1121 o1119 b1120
2920     B b1121 t1121
2921     T t1122 o b1121 b4
2922     B b1122 t1122
2923     B b1123 t1110
2924     B b1124 t1117
2925     T t1124 o1115 b1123 b1124
2926     S s1124 t688 h h1040 h1041 h1108 h1109 h1110
2927     G s1124 t1124
2928     B b1125 s1124
2929     T t1125 o1060 b1125 b1063
2930     B b1126 t1125
2931     B b1127 t727
2932     B b1128 t1124
2933     T t1128 o1115 b1127 b1128
2934     S s1128 t688 h h1040 h1041 h1108 h1109
2935     G s1128 t1128
2936     B b1129 s1128
2937     T t1129 o1060 b1129 b1063
2938     B b1130 t1129
2939 xiny 3527 NItt_logic!all all all Itt_logic
2940 xiny 3553 O o1130 all
2941     B b1131 t1108
2942     B b1132 t1128 b
2943     T t1132 o1130 b1131 b1132
2944     S s1132 t688 h h1040 h1041 h1108
2945     G s1132 t1132
2946     B b1133 s1132
2947     T t1133 o1060 b1133 b1063
2948     B b1134 t1133
2949     B b1135 t1132 a
2950     T t1135 o1130 b1131 b1135
2951     S s1135 t688 h h1040 h1041
2952     G s1135 t1135
2953     B b1136 s1135
2954     T t1136 o1060 b1136 b1063
2955 xiny 3527 B b1137 t1136
2956 xiny 3553 T t1137 o2 b1099
2957 xiny 3404 B b1138 t1137
2958 xiny 3553 T t1138 o1066 b1137 b1122 b1138
2959 xiny 3404 B b1139 t1138
2960 xiny 3553 T t1139 o2 b1139
2961 xiny 3379 B b1140 t1139
2962 xiny 3553 T t1140 o1059 b1134 b1122 b1140
2963 xiny 3379 B b1141 t1140
2964 xiny 3553 T t1141 o2 b1141
2965 xiny 3379 B b1142 t1141
2966 xiny 3553 T t1142 o1059 b1130 b1122 b1142
2967 xiny 3379 B b1143 t1142
2968 xiny 3553 T t1143 o2 b1143
2969 xiny 3498 B b1144 t1143
2970 xiny 3553 T t1144 o1059 b1126 b1122 b1144
2971 xiny 3527 B b1145 t1144
2972 xiny 3553 T t1145 o2 b1145
2973 xiny 3405 B b1146 t1145
2974 xiny 3553 T t1146 o1059 b1119 b1122 b1146
2975 xiny 3379 B b1147 t1146
2976 xiny 3553 T t1147 o2 b1147
2977 xiny 3498 B b1148 t1147
2978 xiny 3553 T t1148 o1059 b1115 b4 b1148
2979 xiny 3498 B b1149 t1148
2980 xiny 3553 T t1149 o b1149 b4
2981 xiny 3405 B b1150 t1149
2982 xiny 3553 T t1150 o1058 b1099 b1150
2983     B b1151 t1150
2984     P p1151 String "equivTransT << op{'g; 'a; 's} >> thenT autoT thenT rwh unfold_equiv 2 thenT rwh unfold_equiv 7 ttca thenT rwh fold_equiv 2 thenT rwh fold_equiv 7"
2985     O o1151 ext_rule p1151
2986     T t1151 o727 b588 b593 b600 b599
2987     S s1151 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
2988     G s1151 t1151
2989     B b1152 s1151
2990     T t1152 o1060 b1152 b1063
2991     B b1153 t1152
2992 xiny 3527 NItt_logic!and and and Itt_logic
2993 xiny 3553 O o1153 and
2994     B b1154 t704
2995     B b1155 t715
2996     T t1155 o704 b599
2997 xiny 3379 B b1156 t1155
2998 xiny 3553 T t1156 o704 b600
2999 xiny 3379 B b1157 t1156
3000 xiny 3553 T t1157 o1153 b1156 b1157
3001 xiny 3379 B b1158 t1157
3002 xiny 3553 T t1158 o1153 b1155 b1158
3003 xiny 3404 B b1159 t1158
3004 xiny 3553 T t1159 o1153 b1154 b1159
3005 xiny 3404 B b1160 t1159
3006 xiny 3553 T t1160 o761 b599 b588
3007 xiny 3498 B b1161 t1160
3008 xiny 3553 T t1161 o761 b600 b588
3009     B b1162 t1161
3010     T t1162 o1153 b1161 b1162
3011     B b1163 t1162
3012     T t1163 o1153 b1160 b1163
3013     B b1164 t1163
3014 xiny 3527 NCzf_itt_pair Czf_itt_pair Czf_itt_pair NIL
3015     NCzf_itt_pair!pair pair pair Czf_itt_pair
3016 xiny 3553 O o1164 pair
3017     T t1164 o1164 b599 b600
3018     B b1165 t1164
3019     T t1165 o761 b1165 b593
3020     B b1166 t1165
3021     T t1166 o1153 b1164 b1166
3022     H h1166 x_2 t1166
3023     S s1166 t688 h h1040 h1041 h1108 h1109 h1110 h1166 h1112
3024     G s1166 t1151
3025     B b1167 s1166
3026     T t1167 o1060 b1167 b1063
3027 xiny 3405 B b1168 t1167
3028 xiny 3553 T t1168 o704 b1039
3029 xiny 3379 B b1169 t1168
3030 xiny 3553 B b1170 t833
3031     T t1170 o1153 b1169 b1170
3032 xiny 3527 B b1171 t1170
3033 xiny 3553 T t1171 o1153 b1155 b1171
3034     B b1172 t1171
3035     T t1172 o1153 b1154 b1172
3036     B b1173 t1172
3037     T t1173 o761 b1039 b588
3038     B b1174 t1173
3039     B b1175 t951
3040     T t1175 o1153 b1174 b1175
3041 xiny 3527 B b1176 t1175
3042 xiny 3553 T t1176 o1153 b1173 b1176
3043 xiny 3527 B b1177 t1176
3044 xiny 3553 T t1177 o1164 b1039 b832
3045 xiny 3527 B b1178 t1177
3046 xiny 3553 T t1178 o761 b1178 b593
3047 xiny 3527 B b1179 t1178
3048 xiny 3553 T t1179 o1153 b1177 b1179
3049     H h1179 x t1179
3050     S s1179 t688 h h1179 h1041 h1108 h1109 h1110 h1166 h1112
3051     G s1179 t1151
3052     B b1180 s1179
3053     T t1180 o1060 b1180 b1063
3054 xiny 3527 B b1181 t1180
3055 xiny 3553 S s1181 t688 h h1179 h1041 h1108 h1109 h1110 h1111 h1112
3056     G s1181 t1151
3057     B b1182 s1181
3058     T t1182 o1060 b1182 b1063
3059 xiny 3527 B b1183 t1182
3060 xiny 3553 T t1183 o727 b588 b593 b1113 b1111
3061     S s1183 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
3062     G s1183 t1183
3063     B b1184 s1183
3064     T t1184 o1060 b1184 b1063
3065 xiny 3527 B b1185 t1184
3066 xiny 3553 T t1185 o2 b1149
3067 xiny 3527 B b1186 t1185
3068 xiny 3553 T t1186 o1059 b1185 b1122 b1186
3069 xiny 3527 B b1187 t1186
3070 xiny 3553 T t1187 o2 b1187
3071 xiny 3527 B b1188 t1187
3072 xiny 3553 T t1188 o1059 b1153 b4 b1188
3073 xiny 3527 B b1189 t1188
3074 xiny 3553 T t1189 o2 b1189
3075 xiny 3527 B b1190 t1189
3076 xiny 3553 T t1190 o1059 b1183 b4 b1190
3077 xiny 3527 B b1191 t1190
3078 xiny 3553 T t1191 o2 b1191
3079     B b1192 t1191
3080     T t1192 o1059 b1181 b4 b1192
3081     B b1193 t1192
3082     T t1193 o2 b1193
3083     B b1194 t1193
3084     T t1194 o1059 b1168 b4 b1194
3085     B b1195 t1194
3086     T t1195 o2 b1195
3087     B b1196 t1195
3088     T t1196 o1059 b1153 b4 b1196
3089     B b1197 t1196
3090     T t1197 o727 b588 b593 b1111 b600
3091     S s1197 t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
3092     G s1197 t1197
3093     B b1198 s1197
3094     T t1198 o1060 b1198 b1063
3095     B b1199 t1198
3096     S s1199 t688 h h1040 h1041 h1108 h1109 h1110 h1166 h1112
3097     G s1199 t1197
3098     B b1200 s1199
3099     T t1200 o1060 b1200 b1063
3100     B b1201 t1200
3101     S s1201 t688 h h1179 h1041 h1108 h1109 h1110 h1166 h1112
3102     G s1201 t1197
3103     B b1202 s1201
3104     T t1202 o1060 b1202 b1063
3105     B b1203 t1202
3106     S s1203 t688 h h1179 h1041 h1108 h1109 h1110 h1111 h1112
3107     G s1203 t1197
3108     B b1204 s1203
3109     T t1204 o1060 b1204 b1063
3110     B b1205 t1204
3111     T t1205 o1059 b1199 b4 b1186
3112     B b1206 t1205
3113     T t1206 o2 b1206
3114     B b1207 t1206
3115     T t1207 o1059 b1205 b4 b1207
3116     B b1208 t1207
3117     T t1208 o2 b1208
3118     B b1209 t1208
3119     T t1209 o1059 b1203 b4 b1209
3120     B b1210 t1209
3121     T t1210 o2 b1210
3122     B b1211 t1210
3123     T t1211 o1059 b1201 b4 b1211
3124     B b1212 t1211
3125     T t1212 o2 b1212
3126     B b1213 t1212
3127     T t1213 o1059 b1199 b4 b1213
3128     B b1214 t1213
3129     T t1214 o b1214 b4
3130     B b1215 t1214
3131     T t1215 o b1197 b1215
3132     B b1216 t1215
3133     T t1216 o1058 b1149 b1216
3134     B b1217 t1216
3135     P p1217 String "equivSymT ttca thenT rwh unfold_equiv 7 ttca"
3136     O o1217 ext_rule p1217
3137     T t1217 o1058 b1197 b4
3138     B b1218 t1217
3139     T t1218 o1217 b1057 b1218 b4 b4
3140     B b1219 t1218
3141     P p1219 String "equivTransT << 'a >> ttca thenT rwh unfold_equiv 7 thenT rwh unfold_equiv 8 ttca"
3142     O o1219 ext_rule p1219
3143     T t1219 o1058 b1214 b4
3144     B b1220 t1219
3145     T t1220 o1219 b1057 b1220 b4 b4
3146     B b1221 t1220
3147     T t1221 o b1221 b4
3148     B b1222 t1221
3149     T t1222 o b1219 b1222
3150     B b1223 t1222
3151     T t1223 o1151 b1057 b1217 b1223 b4
3152     B b1224 t1223
3153     T t1224 o b1224 b4
3154 xiny 3527 B b1225 t1224
3155 xiny 3553 T t1225 o1107 b1057 b1151 b1225 b4
3156     B b1226 t1225
3157     T t1226 o b1226 b4
3158     B b1227 t1226
3159     T t1227 o b1107 b1227
3160 xiny 3527 B b1228 t1227
3161 xiny 3553 T t1228 o b1105 b1228
3162     B b1229 t1228
3163     T t1229 o1084 b1057 b1103 b1229 b4
3164     B b1230 t1229
3165     T t1230 o b1230 b4
3166 xiny 3527 B b1231 t1230
3167 xiny 3553 T t1231 o b1084 b1231
3168     B b1232 t1231
3169     T t1232 o1072 b1057 b1082 b1232 b4
3170     B b1233 t1232
3171     T t1233 o b1233 b4
3172 xiny 3527 B b1234 t1233
3173 xiny 3553 T t1234 o1056 b1057 b1072 b1234 b4
3174     B b1235 t1234
3175     T t1235 o1055 b1235
3176     B b1236 t1235
3177     P p1236 Number 8488
3178     P p1237 Number 8495
3179     O o1237 resource_defs p1236 p1237 p176
3180     P p1238 Number 8493
3181     O o1238 uid p1238 p1237
3182     T t1238 o1238 b695
3183     B b1238 t1238
3184     T t1239 o b1238 b4
3185     B b1239 t1239
3186     T t1240 o1237 b1239
3187     B b1240 t1240
3188     T t1241 o b1240 b4
3189     B b1241 t1241
3190     T t1242 o1035 b1038 b1055 b1236 b1241
3191     B b1242 t1242
3192     T t1243 o1034 b1242
3193     B b1243 t1243
3194     P p1243 Number 9034
3195     P p1244 Number 9338
3196     O o1244 location p1243 p1244
3197     P p1245 String inv_id2
3198     O o1245 rule p1245
3199     T t1245 o598 b582 b832 b1085
3200     B b1245 t1245
3201     T t1246 o727 b588 b593 b1245 b606
3202     S s1246 t688 h
3203     G s1246 t1246
3204     B b1246 s1246
3205     T t1247 o681 b1246
3206     B b1247 t1247
3207     T t1248 o680 b952 b1247
3208     B b1248 t1248
3209     T t1249 o680 b727 b1248
3210     B b1249 t1249
3211     T t1250 o680 b686 b1249
3212     B b1250 t1250
3213     T t1251 o680 b834 b1250
3214     B b1251 t1251
3215     P p1251 String "assertT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's; inv{'g; 's}}; op{'g; 's; inv{'g; 's}}}; op{'g; 's; inv{'g; 's}}} >> ttca"
3216 xiny 3527 O o1251 ext_rule p1251
3217 xiny 3553 T t1252 o b951 b4
3218     B b1252 t1252
3219     T t1253 o b726 b1252
3220     B b1253 t1253
3221     T t1254 o b685 b1253
3222     B b1254 t1254
3223     T t1255 o b833 b1254
3224     B b1255 t1255
3225     T t1256 o1060 b1246 b1255
3226     B b1256 t1256
3227     T t1257 o1059 b1256 b4 b1065
3228     B b1257 t1257
3229     T t1258 o598 b582 b1245 b1245
3230     B b1258 t1258
3231     T t1259 o727 b588 b593 b1258 b1245
3232     S s1259 t688 h
3233     G s1259 t1259
3234     B b1259 s1259
3235     T t1260 o1060 b1259 b1255
3236     B b1260 t1260
3237     T t1261 o2 b1257
3238     B b1261 t1261
3239     T t1262 o1066 b1260 b4 b1261
3240     B b1262 t1262
3241     H h1262 v t1259
3242     S s1262 t688 h h1262
3243     G s1262 t1246
3244     B b1263 s1262
3245     T t1263 o1060 b1263 b1255
3246     B b1264 t1263
3247     T t1264 o1059 b1264 b4 b1261
3248     B b1265 t1264
3249     T t1265 o b1265 b4
3250 xiny 3527 B b1266 t1265
3251 xiny 3553 T t1266 o b1262 b1266
3252 xiny 3527 B b1267 t1266
3253 xiny 3553 T t1267 o1058 b1257 b1267
3254 xiny 3527 B b1268 t1267
3255 xiny 3553 P p1268 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's; inv{'g; 's}}; op{'g; 's; inv{'g; 's}}}; op{'g; 's; op{'g; inv{'g; 's}; op{'g; 's; inv{'g; 's}}}}} >> 0 ttca"
3256     O o1268 ext_rule p1268
3257     T t1268 o598 b582 b1085 b1245
3258 xiny 3527 B b1269 t1268
3259 xiny 3553 T t1269 o598 b582 b832 b1269
3260 xiny 3527 B b1270 t1269
3261 xiny 3553 T t1270 o727 b588 b593 b1270 b1245
3262     S s1270 t688 h
3263     G s1270 t1270
3264     B b1271 s1270
3265     T t1271 o1060 b1271 b1255
3266     B b1272 t1271
3267     T t1272 o2 b1262
3268     B b1273 t1272
3269     T t1273 o1066 b1272 b4 b1273
3270 xiny 3527 B b1274 t1273
3271 xiny 3553 T t1274 o b1274 b4
3272 xiny 3527 B b1275 t1274
3273 xiny 3553 T t1275 o1058 b1262 b1275
3274 xiny 3527 B b1276 t1275
3275 xiny 3553 P p1276 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; op{'g; inv{'g; 's}; op{'g; 's; inv{'g; 's}}}}; op{'g; 's; op{'g; op{'g; inv{'g; 's}; 's}; inv{'g; 's}}}} >> 0 ttca"
3276     O o1276 ext_rule p1276
3277     T t1276 o598 b582 b1086 b1085
3278 xiny 3527 B b1277 t1276
3279 xiny 3553 T t1277 o598 b582 b832 b1277
3280 xiny 3527 B b1278 t1277
3281 xiny 3553 T t1278 o727 b588 b593 b1278 b1245
3282     S s1278 t688 h
3283     G s1278 t1278
3284     B b1279 s1278
3285     T t1279 o1060 b1279 b1255
3286 xiny 3527 B b1280 t1279
3287 xiny 3553 T t1280 o2 b1274
3288 xiny 3527 B b1281 t1280
3289 xiny 3553 T t1281 o1066 b1280 b4 b1281
3290 xiny 3527 B b1282 t1281
3291 xiny 3553 T t1282 o b1282 b4
3292 xiny 3527 B b1283 t1282
3293 xiny 3553 T t1283 o1058 b1274 b1283
3294 xiny 3527 B b1284 t1283
3295 xiny 3553 P p1284 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT"
3296     O o1284 ext_rule p1284
3297     T t1284 o598 b582 b835 b1085
3298 xiny 3527 B b1285 t1284
3299 xiny 3553 T t1285 o598 b582 b832 b1285
3300     B b1286 t1285 z
3301     T t1286 o834 b588 b593 b1286
3302     S s1286 t688 h
3303     G s1286 t1286
3304     B b1287 s1286
3305     T t1287 o1060 b1287 b1255
3306 xiny 3527 B b1288 t1287
3307 xiny 3553 B b1289 t1285
3308     T t1289 o727 b588 b593 b1289 b1245
3309     B b1290 t1289 z
3310     T t1290 o1094 b588 b593 b1290
3311     S s1290 t688 h
3312     G s1290 t1290
3313     B b1291 s1290
3314     T t1291 o1060 b1291 b1255
3315     B b1292 t1291
3316     T t1292 o2 b1282
3317     B b1293 t1292
3318     T t1293 o1066 b1292 b1122 b1293
3319     B b1294 t1293
3320     T t1294 o2 b1294
3321     B b1295 t1294
3322     T t1295 o1066 b1288 b4 b1295
3323     B b1296 t1295
3324     T t1296 o b1296 b4
3325     B b1297 t1296
3326     T t1297 o1058 b1282 b1297
3327     B b1298 t1297
3328     P p1298 String "rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 5 ttca"
3329     O o1298 ext_rule p1298
3330     T t1298 o1058 b1296 b4
3331     B b1299 t1298
3332     T t1299 o1298 b1057 b1299 b4 b4
3333     B b1300 t1299
3334     T t1300 o b1300 b4
3335     B b1301 t1300
3336     T t1301 o1284 b1057 b1298 b1301 b4
3337     B b1302 t1301
3338     T t1302 o b1302 b4
3339     B b1303 t1302
3340     T t1303 o1276 b1057 b1284 b1303 b4
3341     B b1304 t1303
3342     T t1304 o b1304 b4
3343     B b1305 t1304
3344     T t1305 o1268 b1057 b1276 b1305 b4
3345     B b1306 t1305
3346     P p1306 String "dT 2 ttca"
3347     O o1306 ext_rule p1306
3348     T t1306 o1058 b1265 b4
3349 xiny 3527 B b1307 t1306
3350 xiny 3553 T t1307 o1306 b1057 b1307 b4 b4
3351     B b1308 t1307
3352     T t1308 o b1308 b4
3353 xiny 3527 B b1309 t1308
3354 xiny 3553 T t1309 o b1306 b1309
3355     B b1310 t1309
3356     T t1310 o1251 b1057 b1268 b1310 b4
3357 xiny 3527 B b1311 t1310
3358 xiny 3553 T t1311 o1055 b1311
3359     B b1312 t1311
3360     P p1312 Number 9057
3361     P p1313 Number 9064
3362     O o1313 resource_defs p1312 p1313 p204
3363     P p1314 Number 9062
3364     O o1314 uid p1314 p1313
3365     T t1314 o1314 b695
3366     B b1314 t1314
3367     T t1315 o b1314 b4
3368     B b1315 t1315
3369     T t1316 o1313 b1315
3370     B b1316 t1316
3371     T t1317 o b1316 b4
3372     B b1317 t1317
3373     T t1318 o1245 b680 b1251 b1312 b1317
3374     B b1318 t1318
3375     T t1319 o1244 b1318
3376     B b1319 t1319
3377     P p1319 Number 9340
3378     P p1320 Number 9634
3379     O o1320 location p1319 p1320
3380     P p1321 String id_eq2
3381     O o1321 rule p1321
3382     T t1321 o598 b582 b832 b606
3383     B b1321 t1321
3384     T t1322 o727 b588 b593 b1321 b832
3385     S s1322 t688 h
3386     G s1322 t1322
3387     B b1322 s1322
3388     T t1323 o681 b1322
3389     B b1323 t1323
3390     T t1324 o680 b952 b1323
3391     B b1324 t1324
3392     T t1325 o680 b727 b1324
3393     B b1325 t1325
3394     T t1326 o680 b686 b1325
3395     B b1326 t1326
3396     T t1327 o680 b834 b1326
3397     B b1327 t1327
3398     T t1328 o1060 b1322 b1255
3399     B b1328 t1328
3400     T t1329 o1059 b1328 b4 b1065
3401     B b1329 t1329
3402     S s1329 t688 h
3403     G s1329 t1086
3404     B b1330 s1329
3405     T t1330 o1060 b1330 b1255
3406 xiny 3527 B b1331 t1330
3407 xiny 3553 T t1331 o2 b1329
3408 xiny 3527 B b1332 t1331
3409 xiny 3553 T t1332 o1059 b1331 b4 b1332
3410 xiny 3527 B b1333 t1332
3411 xiny 3553 T t1333 o598 b582 b832 b1086
3412 xiny 3527 B b1334 t1333
3413 xiny 3553 T t1334 o727 b588 b593 b1334 b832
3414     S s1334 t688 h
3415     G s1334 t1334
3416     B b1335 s1334
3417     T t1335 o1060 b1335 b1255
3418 xiny 3527 B b1336 t1335
3419 xiny 3553 T t1336 o1059 b1336 b4 b1332
3420 xiny 3527 B b1337 t1336
3421 xiny 3553 T t1337 o b1337 b4
3422 xiny 3527 B b1338 t1337
3423 xiny 3553 T t1338 o b1333 b1338
3424 xiny 3527 B b1339 t1338
3425 xiny 3553 T t1339 o1058 b1329 b1339
3426 xiny 3527 B b1340 t1339
3427 xiny 3553 T t1340 o1058 b1333 b4
3428 xiny 3527 B b1341 t1340
3429 xiny 3553 T t1341 o1103 b1057 b1341 b4 b4
3430 xiny 3527 B b1342 t1341
3431 xiny 3553 P p1342 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; op{'g; inv{'g; 's}; 's}}; op{'g; op{'g; 's; inv{'g; 's}}; 's}}>> 0 ttca"
3432     O o1342 ext_rule p1342
3433     T t1342 o598 b582 b1245 b832
3434 xiny 3527 B b1343 t1342
3435 xiny 3553 T t1343 o727 b588 b593 b1343 b832
3436     S s1343 t688 h
3437     G s1343 t1343
3438     B b1344 s1343
3439     T t1344 o1060 b1344 b1255
3440 xiny 3527 B b1345 t1344
3441 xiny 3553 T t1345 o2 b1337
3442 xiny 3527 B b1346 t1345
3443 xiny 3553 T t1346 o1059 b1345 b4 b1346
3444 xiny 3527 B b1347 t1346
3445 xiny 3553 T t1347 o b1347 b4
3446 xiny 3527 B b1348 t1347
3447 xiny 3553 T t1348 o1058 b1337 b1348
3448 xiny 3527 B b1349 t1348
3449 xiny 3553 P p1349 String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; inv{'g; 's}}; id{'g}} >> 0 thenT autoT"
3450     O o1349 ext_rule p1349
3451     T t1349 o1058 b1347 b4
3452     B b1350 t1349
3453     T t1350 o1349 b1057 b1350 b4 b4
3454 xiny 3527 B b1351 t1350
3455 xiny 3553 T t1351 o b1351 b4
3456 xiny 3527 B b1352 t1351
3457 xiny 3553 T t1352 o1342 b1057 b1349 b1352 b4
3458 xiny 3527 B b1353 t1352
3459     T t1353 o b1353 b4
3460 xiny 3498 B b1354 t1353
3461 xiny 3553 T t1354 o b1342 b1354
3462 xiny 3498 B b1355 t1354
3463 xiny 3553 T t1355 o1084 b1057 b1340 b1355 b4
3464 xiny 3498 B b1356 t1355
3465 xiny 3553 T t1356 o1055 b1356
3466     B b1357 t1356
3467     P p1357 Number 9362
3468     P p1358 Number 9369
3469     O o1358 resource_defs p1357 p1358 p204
3470     P p1359 Number 9367
3471     O o1359 uid p1359 p1358
3472     T t1359 o1359 b695
3473     B b1359 t1359
3474     T t1360 o b1359 b4
3475     B b1360 t1360
3476     T t1361 o1358 b1360
3477     B b1361 t1361
3478     T t1362 o b1361 b4
3479     B b1362 t1362
3480     T t1363 o1321 b680 b1327 b1357 b1362
3481     B b1363 t1363
3482     T t1364 o1320 b1363
3483     B b1364 t1364
3484     P p1364 Number 9655
3485     P p1365 Number 10094
3486     O o1365 location p1364 p1365
3487     P p1366 String equiv_op_fun1
3488     O o1366 rule p1366
3489     S s1366 t683 h
3490     G s1366 t1155
3491     B b1366 s1366
3492     T t1366 o681 b1366
3493 xiny 3527 B b1367 t1366
3494 xiny 3553 S s1367 t683 h
3495     G s1367 t1156
3496     B b1368 s1367
3497     T t1368 o681 b1368
3498 xiny 3498 B b1369 t1368
3499 xiny 3553 S s1369 t688 h
3500     G s1369 t1160
3501     B b1370 s1369
3502     T t1370 o681 b1370
3503 xiny 3498 B b1371 t1370
3504 xiny 3553 S s1371 t688 h
3505     G s1371 t1161
3506 xiny 3527 B b1372 s1371
3507 xiny 3553 T t1372 o681 b1372
3508 xiny 3498 B b1373 t1372
3509 xiny 3553 T t1373 o598 b582 b835 b599
3510 xiny 3498 B b1374 t1373
3511 xiny 3553 T t1374 o598 b582 b835 b600
3512 xiny 3404 B b1375 t1374
3513 xiny 3553 T t1375 o727 b588 b593 b1374 b1375
3514     B b1376 t1375 z
3515     T t1376 o1094 b588 b593 b1376
3516     S s1376 t688