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

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

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

revision 3379 by xiny, Fri Sep 14 07:00:13 2001 UTC revision 3404 by xiny, Sun Sep 23 07:25:28 2001 UTC
# Line 589  Line 589 
589  B       b217    t217  B       b217    t217
590  NOcaml!type_prod        type_prod       type_prod Ocaml  NOcaml!type_prod        type_prod       type_prod Ocaml
591  P       p217    Number 2343  P       p217    Number 2343
592  P       p218    Number 2358  P       p218    Number 2367
593  O       o218    type_prod p217 p218  O       o218    type_prod p217 p218
594  P       p219    Number 2349  P       p219    Number 2349
595  O       o219    type_lid p217 p219  O       o219    type_lid p217 p219
# Line 600  Line 600 
600  T       t221    o219 b220  T       t221    o219 b220
601  B       b221    t221  B       b221    t221
602  P       p221    Number 2352  P       p221    Number 2352
603  O       o221    type_lid p221 p218  P       p222    Number 2358
604  T       t222    o221 b220  O       o222    type_lid p221 p222
605    T       t222    o222 b220
606  B       b222    t222  B       b222    t222
607  T       t223    o b222 b4  P       p223    Number 2361
608    O       o223    type_lid p223 p218
609    T       t223    o223 b220
610  B       b223    t223  B       b223    t223
611  T       t224    o b221 b223  T       t224    o b223 b4
612  B       b224    t224  B       b224    t224
613  T       t225    o218 b224  T       t225    o b222 b224
614  B       b225    t225  B       b225    t225
615  T       t226    o213 b217 b225  T       t226    o b221 b225
616  B       b226    t226  B       b226    t226
617  P       p226    String cache  T       t227    o218 b226
618  O       o226    resource p226  B       b227    t227
619  P       p227    Number 1424  T       t228    o213 b217 b227
620  P       p228    Number 1434  B       b228    t228
621  O       o228    type_lid p227 p228  P       p228    String cache
622  P       p229    String cache_rule  O       o228    resource p228
623  O       o229    type_lid p229  P       p229    Number 1424
624  T       t229    o229  P       p230    Number 1434
625  B       b229    t229  O       o230    type_lid p229 p230
626  T       t230    o228 b229  P       p231    String cache_rule
627  B       b230    t230  O       o231    type_lid p231
628  P       p230    Number 1436  T       t231    o231
629  P       p231    Number 1441  B       b231    t231
630  O       o231    type_lid p230 p231  T       t232    o230 b231
 O       o232    type_lid p226  
 T       t232    o232  
631  B       b232    t232  B       b232    t232
632  T       t233    o231 b232  P       p232    Number 1436
633  B       b233    t233  P       p233    Number 1441
634  T       t234    o226 b230 b233  O       o233    type_lid p232 p233
635    O       o234    type_lid p228
636    T       t234    o234
637  B       b234    t234  B       b234    t234
638  P       p234    String elim  T       t235    o233 b234
639  O       o234    resource p234  B       b235    t235
640  P       p235    Number 1761  T       t236    o228 b232 b235
641  P       p236    Number 1783  B       b236    t236
642  O       o236    type_prod p235 p236  P       p236    String elim
643  P       p237    Number 1765  O       o236    resource p236
644  O       o237    type_lid p235 p237  P       p237    Number 1761
645  P       p238    String term  P       p238    Number 1783
646  O       o238    type_lid p238  O       o238    type_prod p237 p238
647  T       t238    o238  P       p239    Number 1765
648  B       b238    t238  O       o239    type_lid p237 p239
649  T       t239    o237 b238  P       p240    String term
650  B       b239    t239  O       o240    type_lid p240
651    T       t240    o240
652    B       b240    t240
653    T       t241    o239 b240
654    B       b241    t241
655  NOcaml!type_fun type_fun        type_fun Ocaml  NOcaml!type_fun type_fun        type_fun Ocaml
656  P       p239    Number 1769  P       p241    Number 1769
657  P       p240    Number 1782  P       p242    Number 1782
658  O       o240    type_fun p239 p240  O       o242    type_fun p241 p242
659  P       p241    Number 1772  P       p243    Number 1772
660  O       o241    type_lid p239 p241  O       o243    type_lid p241 p243
661  P       p242    String int  P       p244    String int
662  O       o242    type_lid p242  O       o244    type_lid p244
663  T       t242    o242  T       t244    o244
 B       b242    t242  
 T       t243    o241 b242  
 B       b243    t243  
 P       p243    Number 1776  
 O       o243    type_lid p243 p240  
 T       t244    o243 b220  
664  B       b244    t244  B       b244    t244
665  T       t245    o240 b243 b244  T       t245    o243 b244
666  B       b245    t245  B       b245    t245
667  T       t246    o b245 b4  P       p245    Number 1776
668    O       o245    type_lid p245 p242
669    T       t246    o245 b220
670  B       b246    t246  B       b246    t246
671  T       t247    o b239 b246  T       t247    o242 b245 b246
672  B       b247    t247  B       b247    t247
673  T       t248    o236 b247  T       t248    o b247 b4
674  B       b248    t248  B       b248    t248
675  P       p248    Number 1785  T       t249    o b241 b248
676  P       p249    Number 1798  B       b249    t249
677  O       o249    type_fun p248 p249  T       t250    o238 b249
 P       p250    Number 1788  
 O       o250    type_lid p248 p250  
 T       t250    o250 b242  
678  B       b250    t250  B       b250    t250
679  P       p251    Number 1792  P       p250    Number 1785
680  O       o251    type_lid p251 p249  P       p251    Number 1798
681  T       t251    o251 b220  O       o251    type_fun p250 p251
682  B       b251    t251  P       p252    Number 1788
683  T       t252    o249 b250 b251  O       o252    type_lid p250 p252
684    T       t252    o252 b244
685  B       b252    t252  B       b252    t252
686  T       t253    o234 b248 b252  P       p253    Number 1792
687    O       o253    type_lid p253 p251
688    T       t253    o253 b220
689  B       b253    t253  B       b253    t253
690  P       p253    String eqcd  T       t254    o251 b252 b253
691  O       o253    resource p253  B       b254    t254
692  P       p254    Number 6168  T       t255    o236 b250 b254
693  P       p255    Number 6181  B       b255    t255
694  O       o255    type_prod p254 p255  P       p255    String eqcd
695  P       p256    Number 6172  O       o255    resource p255
696  O       o256    type_lid p254 p256  P       p256    Number 6168
697  T       t256    o256 b238  P       p257    Number 6181
698  B       b256    t256  O       o257    type_prod p256 p257
699  P       p257    Number 6175  P       p258    Number 6172
700  O       o257    type_lid p257 p255  O       o258    type_lid p256 p258
701  T       t257    o257 b220  T       t258    o258 b240
 B       b257    t257  
 T       t258    o b257 b4  
702  B       b258    t258  B       b258    t258
703  T       t259    o b256 b258  P       p259    Number 6175
704    O       o259    type_lid p259 p257
705    T       t259    o259 b220
706  B       b259    t259  B       b259    t259
707  T       t260    o255 b259  T       t260    o b259 b4
708  B       b260    t260  B       b260    t260
709  P       p260    Number 6183  T       t261    o b258 b260
 P       p261    Number 6189  
 O       o261    type_lid p260 p261  
 T       t261    o261 b220  
710  B       b261    t261  B       b261    t261
711  T       t262    o253 b260 b261  T       t262    o257 b261
712  B       b262    t262  B       b262    t262
713  P       p262    String intro  P       p262    Number 6183
714  O       o262    resource p262  P       p263    Number 6189
715  P       p263    Number 1815  O       o263    type_lid p262 p263
716  P       p264    Number 1852  T       t263    o263 b220
717  O       o264    type_prod p263 p264  B       b263    t263
718  P       p265    Number 1819  T       t264    o255 b262 b263
719  O       o265    type_lid p263 p265  B       b264    t264
720  T       t265    o265 b238  P       p264    String intro
721  B       b265    t265  O       o264    resource p264
722  P       p266    Number 1823  P       p265    Number 1815
723  P       p267    Number 1851  P       p266    Number 1852
724  O       o267    type_prod p266 p267  O       o266    type_prod p265 p266
725  P       p268    Number 1829  P       p267    Number 1819
726  O       o268    type_lid p266 p268  O       o267    type_lid p265 p267
727  P       p269    String string  T       t267    o267 b240
728  O       o269    type_lid p269  B       b267    t267
729  T       t269    o269  P       p268    Number 1823
730  B       b269    t269  P       p269    Number 1851
731  T       t270    o268 b269  O       o269    type_prod p268 p269
732  B       b270    t270  P       p270    Number 1829
733    O       o270    type_lid p268 p270
734    P       p271    String string
735    O       o271    type_lid p271
736    T       t271    o271
737    B       b271    t271
738    T       t272    o270 b271
739    B       b272    t272
740  NOcaml!type_apply       type_apply      type_apply Ocaml  NOcaml!type_apply       type_apply      type_apply Ocaml
741  P       p270    Number 1832  P       p272    Number 1832
742  P       p271    Number 1842  P       p273    Number 1842
743  O       o271    type_apply p270 p271  O       o273    type_apply p272 p273
744  P       p272    Number 1836  P       p274    Number 1836
745  O       o272    type_lid p272 p271  O       o274    type_lid p274 p273
746  P       p273    String option  P       p275    String option
747  O       o273    type_lid p273  O       o275    type_lid p275
748  T       t273    o273  T       t275    o275
 B       b273    t273  
 T       t274    o272 b273  
 B       b274    t274  
 P       p274    Number 1835  
 O       o274    type_lid p270 p274  
 T       t275    o274 b242  
749  B       b275    t275  B       b275    t275
750  T       t276    o271 b274 b275  T       t276    o274 b275
751  B       b276    t276  B       b276    t276
752  P       p276    Number 1845  P       p276    Number 1835
753  O       o276    type_lid p276 p267  O       o276    type_lid p272 p276
754  T       t277    o276 b220  T       t277    o276 b244
755  B       b277    t277  B       b277    t277
756  T       t278    o b277 b4  T       t278    o273 b276 b277
757  B       b278    t278  B       b278    t278
758  T       t279    o b276 b278  P       p278    Number 1845
759    O       o278    type_lid p278 p269
760    T       t279    o278 b220
761  B       b279    t279  B       b279    t279
762  T       t280    o b270 b279  T       t280    o b279 b4
763  B       b280    t280  B       b280    t280
764  T       t281    o267 b280  T       t281    o b278 b280
765  B       b281    t281  B       b281    t281
766  T       t282    o b281 b4  T       t282    o b272 b281
767  B       b282    t282  B       b282    t282
768  T       t283    o b265 b282  T       t283    o269 b282
769  B       b283    t283  B       b283    t283
770  T       t284    o264 b283  T       t284    o b283 b4
771  B       b284    t284  B       b284    t284
772  P       p284    Number 1854  T       t285    o b267 b284
 P       p285    Number 1860  
 O       o285    type_lid p284 p285  
 T       t285    o285 b220  
773  B       b285    t285  B       b285    t285
774  T       t286    o262 b284 b285  T       t286    o266 b285
775  B       b286    t286  B       b286    t286
776  P       p286    String reduce  P       p286    Number 1854
777  O       o286    resource p286  P       p287    Number 1860
778  P       p287    Number 2920  O       o287    type_lid p286 p287
779  P       p288    Number 2931  T       t287    o287 b220
780  O       o288    type_prod p287 p288  B       b287    t287
781  P       p289    Number 2924  T       t288    o264 b286 b287
782  O       o289    type_lid p287 p289  B       b288    t288
783  T       t289    o289 b238  P       p288    String reduce
784  B       b289    t289  O       o288    resource p288
785  P       p290    Number 2927  P       p289    Number 2920
786  O       o290    type_lid p290 p288  P       p290    Number 2931
787  P       p291    String conv  O       o290    type_prod p289 p290
788  O       o291    type_lid p291  P       p291    Number 2924
789  T       t291    o291  O       o291    type_lid p289 p291
790    T       t291    o291 b240
791  B       b291    t291  B       b291    t291
792  T       t292    o290 b291  P       p292    Number 2927
793  B       b292    t292  O       o292    type_lid p292 p290
794  T       t293    o b292 b4  P       p293    String conv
795    O       o293    type_lid p293
796    T       t293    o293
797  B       b293    t293  B       b293    t293
798  T       t294    o b289 b293  T       t294    o292 b293
799  B       b294    t294  B       b294    t294
800  T       t295    o288 b294  T       t295    o b294 b4
801  B       b295    t295  B       b295    t295
802  P       p295    Number 2933  T       t296    o b291 b295
 P       p296    Number 2937  
 O       o296    type_lid p295 p296  
 T       t296    o296 b291  
803  B       b296    t296  B       b296    t296
804  T       t297    o286 b295 b296  T       t297    o290 b296
805  B       b297    t297  B       b297    t297
806  P       p297    String squash  P       p297    Number 2933
807  O       o297    resource p297  P       p298    Number 2937
808  P       p298    Number 4017  O       o298    type_lid p297 p298
809  P       p299    Number 4028  T       t298    o298 b293
810  O       o299    type_lid p298 p299  B       b298    t298
811  P       p300    String squash_info  T       t299    o288 b297 b298
812  O       o300    type_lid p300  B       b299    t299
813  T       t300    o300  P       p299    String squash
814  B       b300    t300  O       o299    resource p299
815  T       t301    o299 b300  P       p300    Number 4017
816  B       b301    t301  P       p301    Number 4028
817  P       p301    Number 4030  O       o301    type_lid p300 p301
818  P       p302    Number 4043  P       p302    String squash_info
819  O       o302    type_fun p301 p302  O       o302    type_lid p302
820  P       p303    Number 4033  T       t302    o302
821  O       o303    type_lid p301 p303  B       b302    t302
822  T       t303    o303 b242  T       t303    o301 b302
823  B       b303    t303  B       b303    t303
824  P       p304    Number 4037  P       p303    Number 4030
825  O       o304    type_lid p304 p302  P       p304    Number 4043
826  T       t304    o304 b220  O       o304    type_fun p303 p304
827  B       b304    t304  P       p305    Number 4033
828  T       t305    o302 b303 b304  O       o305    type_lid p303 p305
829    T       t305    o305 b244
830  B       b305    t305  B       b305    t305
831  T       t306    o297 b301 b305  P       p306    Number 4037
832    O       o306    type_lid p306 p304
833    T       t306    o306 b220
834  B       b306    t306  B       b306    t306
835  P       p306    String sub  T       t307    o304 b305 b306
836  O       o306    resource p306  B       b307    t307
837  P       p307    Number 4871  T       t308    o299 b303 b307
838  P       p308    Number 4888  B       b308    t308
839  O       o308    type_lid p307 p308  P       p308    String sub
840  P       p309    String sub_resource_info  O       o308    resource p308
841  O       o309    type_lid p309  P       p309    Number 4882
842  T       t309    o309  P       p310    Number 4899
843  B       b309    t309  O       o310    type_lid p309 p310
844  T       t310    o308 b309  P       p311    String sub_resource_info
845  B       b310    t310  O       o311    type_lid p311
846  P       p310    Number 4890  T       t311    o311
 P       p311    Number 4896  
 O       o311    type_lid p310 p311  
 T       t311    o311 b220  
847  B       b311    t311  B       b311    t311
848  T       t312    o306 b310 b311  T       t312    o310 b311
849  B       b312    t312  B       b312    t312
850  P       p312    String toploop  P       p312    Number 4901
851  O       o312    resource p312  P       p313    Number 4907
852  P       p313    Number 2445  O       o313    type_lid p312 p313
853  P       p314    Number 2467  T       t313    o313 b220
854  O       o314    type_prod p313 p314  B       b313    t313
855  P       p315    Number 2451  T       t314    o308 b312 b313
856  O       o315    type_lid p313 p315  B       b314    t314
857  T       t315    o315 b269  P       p314    String toploop
858  B       b315    t315  O       o314    resource p314
859  P       p316    Number 2454  P       p315    Number 2445
860  P       p317    Number 2460  P       p316    Number 2467
861  O       o317    type_lid p316 p317  O       o316    type_prod p315 p316
862  T       t317    o317 b269  P       p317    Number 2451
863    O       o317    type_lid p315 p317
864    T       t317    o317 b271
865  B       b317    t317  B       b317    t317
866  P       p318    Number 2463  P       p318    Number 2454
867  O       o318    type_lid p318 p314  P       p319    Number 2460
868  P       p319    String expr  O       o319    type_lid p318 p319
869  O       o319    type_lid p319  T       t319    o319 b271
 T       t319    o319  
870  B       b319    t319  B       b319    t319
871  T       t320    o318 b319  P       p320    Number 2463
872  B       b320    t320  O       o320    type_lid p320 p316
873  T       t321    o b320 b4  P       p321    String expr
874    O       o321    type_lid p321
875    T       t321    o321
876  B       b321    t321  B       b321    t321
877  T       t322    o b317 b321  T       t322    o320 b321
878  B       b322    t322  B       b322    t322
879  T       t323    o b315 b322  T       t323    o b322 b4
880  B       b323    t323  B       b323    t323
881  T       t324    o314 b323  T       t324    o b319 b323
882  B       b324    t324  B       b324    t324
883  P       p324    Number 2469  T       t325    o b317 b324
884  P       p325    Number 2478  B       b325    t325
885  O       o325    type_lid p324 p325  T       t326    o316 b325
 P       p326    String top_table  
 O       o326    type_lid p326  
 T       t326    o326  
886  B       b326    t326  B       b326    t326
887  T       t327    o325 b326  P       p326    Number 2469
888  B       b327    t327  P       p327    Number 2478
889  T       t328    o312 b324 b327  O       o327    type_lid p326 p327
890    P       p328    String top_table
891    O       o328    type_lid p328
892    T       t328    o328
893  B       b328    t328  B       b328    t328
894  P       p328    String typeinf  T       t329    o327 b328
895  O       o328    resource p328  B       b329    t329
896  P       p329    Number 2151  T       t330    o314 b326 b329
897  P       p330    Number 2172  B       b330    t330
898  O       o330    type_lid p329 p330  P       p330    String typeinf
899  P       p331    String typeinf_resource_info  O       o330    resource p330
900  O       o331    type_lid p331  P       p331    Number 2151
901  T       t331    o331  P       p332    Number 2172
902  B       b331    t331  O       o332    type_lid p331 p332
903  T       t332    o330 b331  P       p333    String typeinf_resource_info
904  B       b332    t332  O       o333    type_lid p333
905  P       p332    Number 2174  T       t333    o333
906  P       p333    Number 2186  B       b333    t333
907  O       o333    type_lid p332 p333  T       t334    o332 b333
 P       p334    String typeinf_func  
 O       o334    type_lid p334  
 T       t334    o334  
908  B       b334    t334  B       b334    t334
909  T       t335    o333 b334  P       p334    Number 2174
910  B       b335    t335  P       p335    Number 2186
911  T       t336    o328 b332 b335  O       o335    type_lid p334 p335
912    P       p336    String typeinf_func
913    O       o336    type_lid p336
914    T       t336    o336
915  B       b336    t336  B       b336    t336
916  P       p336    String typeinf_subst  T       t337    o335 b336
917  O       o336    resource p336  B       b337    t337
918  P       p337    Number 1825  T       t338    o330 b334 b337
919  P       p338    Number 1843  B       b338    t338
920  O       o338    type_lid p337 p338  P       p338    String typeinf_subst
921  P       p339    String typeinf_subst_info  O       o338    resource p338
922  O       o339    type_lid p339  P       p339    Number 1825
923  T       t339    o339  P       p340    Number 1843
924  B       b339    t339  O       o340    type_lid p339 p340
925  T       t340    o338 b339  P       p341    String typeinf_subst_info
 B       b340    t340  
 P       p340    Number 1862  
 O       o340    type_lid p276 p340  
 P       p341    String typeinf_subst_fun  
926  O       o341    type_lid p341  O       o341    type_lid p341
927  T       t341    o341  T       t341    o341
928  B       b341    t341  B       b341    t341
929  T       t342    o340 b341  T       t342    o340 b341
930  B       b342    t342  B       b342    t342
931  T       t343    o336 b340 b342  P       p342    Number 1862
932    O       o342    type_lid p278 p342
933    P       p343    String typeinf_subst_fun
934    O       o343    type_lid p343
935    T       t343    o343
936  B       b343    t343  B       b343    t343
937  T       t344    o b343 b4  T       t344    o342 b343
938  B       b344    t344  B       b344    t344
939  T       t345    o b336 b344  T       t345    o338 b342 b344
940  B       b345    t345  B       b345    t345
941  T       t346    o b328 b345  T       t346    o b345 b4
942  B       b346    t346  B       b346    t346
943  T       t347    o b312 b346  T       t347    o b338 b346
944  B       b347    t347  B       b347    t347
945  T       t348    o b306 b347  T       t348    o b330 b347
946  B       b348    t348  B       b348    t348
947  T       t349    o b297 b348  T       t349    o b314 b348
948  B       b349    t349  B       b349    t349
949  T       t350    o b286 b349  T       t350    o b308 b349
950  B       b350    t350  B       b350    t350
951  T       t351    o b262 b350  T       t351    o b299 b350
952  B       b351    t351  B       b351    t351
953  T       t352    o b253 b351  T       t352    o b288 b351
954  B       b352    t352  B       b352    t352
955  T       t353    o b234 b352  T       t353    o b264 b352
956  B       b353    t353  B       b353    t353
957  T       t354    o b226 b353  T       t354    o b255 b353
958  B       b354    t354  B       b354    t354
959  T       t355    o2 b5 b213 b354  T       t355    o b236 b354
960  B       b355    t355  B       b355    t355
961  T       t356    o1 b355  T       t356    o b228 b355
962  B       b356    t356  B       b356    t356
963  P       p356    Number 20  T       t357    o2 b5 b213 b356
964  P       p357    Number 42  B       b357    t357
965  O       o357    location p356 p357  T       t358    o1 b357
 P       p358    String Czf_itt_member  
 O       o358    parent p358  
 T       t358    o358  
966  B       b358    t358  B       b358    t358
967  T       t359    o b358 b4  P       p358    Number 20
968  B       b359    t359  P       p359    Number 42
969  P       p359    String Czf_itt_eq  O       o359    location p358 p359
970  O       o359    parent p359  P       p360    String Czf_itt_member
971  T       t360    o359  O       o360    parent p360
972    T       t360    o360
973  B       b360    t360  B       b360    t360
974  T       t361    o b360 b4  T       t361    o b360 b4
975  B       b361    t361  B       b361    t361
976  T       t362    o b361 b4  P       p361    String Czf_itt_eq
977    O       o361    parent p361
978    T       t362    o361
979  B       b362    t362  B       b362    t362
980  T       t363    o b359 b362  T       t363    o b362 b4
981  B       b363    t363  B       b363    t363
982  T       t364    o2 b359 b363 b354  T       t364    o b363 b4
983  B       b364    t364  B       b364    t364
984  T       t365    o357 b364  T       t365    o b361 b364
985  B       b365    t365  B       b365    t365
986  P       p365    Number 43  T       t366    o2 b361 b365 b356
 P       p366    Number 61  
 O       o366    location p365 p366  
 T       t366    o2 b361 b4 b354  
987  B       b366    t366  B       b366    t366
988  T       t367    o366 b366  T       t367    o359 b366
989  B       b367    t367  B       b367    t367
990  P       p367    Number 62  P       p367    Number 43
991  P       p368    Number 82  P       p368    Number 61
992  O       o368    location p367 p368  O       o368    location p367 p368
993  P       p369    String Czf_itt_dall  T       t368    o2 b363 b4 b356
994  O       o369    parent p369  B       b368    t368
995  T       t369    o369  T       t369    o368 b368
996  B       b369    t369  B       b369    t369
997  T       t370    o b369 b4  P       p369    Number 62
998  B       b370    t370  P       p370    Number 82
999  P       p370    String Czf_itt_set_ind  O       o370    location p369 p370
1000  O       o370    parent p370  P       p371    String Czf_itt_dall
1001  T       t371    o370  O       o371    parent p371
1002    T       t371    o371
1003  B       b371    t371  B       b371    t371
1004  T       t372    o b371 b4  T       t372    o b371 b4
1005  B       b372    t372  B       b372    t372
1006  P       p372    String Czf_itt_all  P       p372    String Czf_itt_set_ind
1007  O       o372    parent p372  O       o372    parent p372
1008  T       t373    o372  T       t373    o372
1009  B       b373    t373  B       b373    t373
1010  T       t374    o b373 b4  T       t374    o b373 b4
1011  B       b374    t374  B       b374    t374
1012  P       p374    String Czf_itt_sep  P       p374    String Czf_itt_all
1013  O       o374    parent p374  O       o374    parent p374
1014  T       t375    o374  T       t375    o374
1015  B       b375    t375  B       b375    t375
1016  T       t376    o b375 b4  T       t376    o b375 b4
1017  B       b376    t376  B       b376    t376
1018  T       t377    o b376 b4  P       p376    String Czf_itt_sep
1019    O       o376    parent p376
1020    T       t377    o376
1021  B       b377    t377  B       b377    t377
1022  T       t378    o b374 b377  T       t378    o b377 b4
1023  B       b378    t378  B       b378    t378
1024  T       t379    o b372 b378  T       t379    o b378 b4
1025  B       b379    t379  B       b379    t379
1026  T       t380    o b370 b379  T       t380    o b376 b379
1027  B       b380    t380  B       b380    t380
1028  T       t381    o2 b370 b380 b354  T       t381    o b374 b380
1029  B       b381    t381  B       b381    t381
1030  T       t382    o368 b381  T       t382    o b372 b381
1031  B       b382    t382  B       b382    t382
1032  P       p382    Number 83  T       t383    o2 b372 b382 b356
1033  P       p383    Number 102  B       b383    t383
1034  O       o383    location p382 p383  T       t384    o370 b383
 P       p384    String Czf_itt_and  
 O       o384    parent p384  
 T       t384    o384  
1035  B       b384    t384  B       b384    t384
1036  T       t385    o b384 b4  P       p384    Number 83
1037  B       b385    t385  P       p385    Number 102
1038  T       t386    o b385 b4  O       o385    location p384 p385
1039    P       p386    String Czf_itt_and
1040    O       o386    parent p386
1041    T       t386    o386
1042  B       b386    t386  B       b386    t386
1043  T       t387    o2 b385 b386 b354  T       t387    o b386 b4
1044  B       b387    t387  B       b387    t387
1045  T       t388    o383 b387  T       t388    o b387 b4
1046  B       b388    t388  B       b388    t388
1047  P       p388    Number 104  T       t389    o2 b387 b388 b356
1048  P       p389    Number 115  B       b389    t389
1049  O       o389    location p388 p389  T       t390    o385 b389
1050    B       b390    t390
1051    P       p390    Number 104
1052    P       p391    Number 115
1053    O       o391    location p390 p391
1054  NSummary!summary_item   summary_item    summary_item Summary  NSummary!summary_item   summary_item    summary_item Summary
1055  O       o390    summary_item  O       o392    summary_item
1056  NOcaml!str_open str_open        str_open Ocaml  NOcaml!str_open str_open        str_open Ocaml
1057  O       o391    str_open p388 p389  O       o393    str_open p390 p391
1058  NOcaml!string   string  string Ocaml  NOcaml!string   string  string Ocaml
1059  P       p391    String Printf  P       p393    String Printf
1060  O       o392    string p391  O       o394    string p393
1061  T       t392    o392  T       t394    o394
 B       b392    t392  
 T       t393    o b392 b4  
 B       b393    t393  
 T       t394    o391 b393  
1062  B       b394    t394  B       b394    t394
1063  T       t395    o390 b394  T       t395    o b394 b4
1064  B       b395    t395  B       b395    t395
1065  T       t396    o389 b395  T       t396    o393 b395
1066  B       b396    t396  B       b396    t396
1067  P       p396    Number 116  T       t397    o392 b396
1068  P       p397    Number 129  B       b397    t397
1069  O       o397    location p396 p397  T       t398    o391 b397
1070  O       o398    str_open p396 p397  B       b398    t398
1071  P       p398    String Mp_debug  P       p398    Number 116
1072  O       o399    string p398  P       p399    Number 129
1073  T       t399    o399  O       o399    location p398 p399
1074  B       b399    t399  O       o400    str_open p398 p399
1075  T       t400    o b399 b4  P       p400    String Mp_debug
1076  B       b400    t400  O       o401    string p400
1077  T       t401    o398 b400  T       t401    o401
1078  B       b401    t401  B       b401    t401
1079  T       t402    o390 b401  T       t402    o b401 b4
1080  B       b402    t402  B       b402    t402
1081  T       t403    o397 b402  T       t403    o400 b402
1082  B       b403    t403  B       b403    t403
1083  P       p403    Number 130  T       t404    o392 b403
1084  P       p404    Number 159  B       b404    t404
1085  O       o404    location p403 p404  T       t405    o399 b404
1086  O       o405    str_open p403 p404  B       b405    t405
1087  P       p405    String Refiner  P       p405    Number 130
1088  O       o406    string p405  P       p406    Number 159
1089  T       t406    o406  O       o406    location p405 p406
1090  B       b406    t406  O       o407    str_open p405 p406
1091  P       p406    String TermType  P       p407    String Refiner
1092  O       o407    string p406  O       o408    string p407
1093  T       t407    o407  T       t408    o408
 B       b407    t407  
 T       t408    o b407 b4  
1094  B       b408    t408  B       b408    t408
1095  T       t409    o b406 b408  P       p408    String TermType
1096    O       o409    string p408
1097    T       t409    o409
1098  B       b409    t409  B       b409    t409
1099  T       t410    o b406 b409  T       t410    o b409 b4
1100  B       b410    t410  B       b410    t410
1101  T       t411    o405 b410  T       t411    o b408 b410
1102  B       b411    t411  B       b411    t411
1103  T       t412    o390 b411  T       t412    o b408 b411
1104  B       b412    t412  B       b412    t412
1105  T       t413    o404 b412  T       t413    o407 b412
1106  B       b413    t413  B       b413    t413
1107  P       p413    Number 160  T       t414    o392 b413
1108  P       p414    Number 185  B       b414    t414
1109  O       o414    location p413 p414  T       t415    o406 b414
1110  O       o415    str_open p413 p414  B       b415    t415
1111  P       p415    String Term  P       p415    Number 160
1112  O       o416    string p415  P       p416    Number 185
1113  T       t416    o416  O       o416    location p415 p416
1114  B       b416    t416  O       o417    str_open p415 p416
1115  T       t417    o b416 b4  P       p417    String Term
1116  B       b417    t417  O       o418    string p417
1117  T       t418    o b406 b417  T       t418    o418
1118  B       b418    t418  B       b418    t418
1119  T       t419    o b406 b418  T       t419    o b418 b4
1120  B       b419    t419  B       b419    t419
1121  T       t420    o415 b419  T       t420    o b408 b419
1122  B       b420    t420  B       b420    t420
1123  T       t421    o390 b420  T       t421    o b408 b420
1124  B       b421    t421  B       b421    t421
1125  T       t422    o414 b421  T       t422    o417 b421
1126  B       b422    t422  B       b422    t422
1127  P       p422    Number 186  T       t423    o392 b422
1128  P       p423    Number 213  B       b423    t423
1129  O       o423    location p422 p423  T       t424    o416 b423
1130  O       o424    str_open p422 p423  B       b424    t424
1131  P       p424    String TermOp  P       p424    Number 186
1132  O       o425    string p424  P       p425    Number 213
1133  T       t425    o425  O       o425    location p424 p425
1134  B       b425    t425  O       o426    str_open p424 p425
1135  T       t426    o b425 b4  P       p426    String TermOp
1136  B       b426    t426  O       o427    string p426
1137  T       t427    o b406 b426  T       t427    o427
1138  B       b427    t427  B       b427    t427
1139  T       t428    o b406 b427  T       t428    o b427 b4
1140  B       b428    t428  B       b428    t428
1141  T       t429    o424 b428  T       t429    o b408 b428
1142  B       b429    t429  B       b429    t429
1143  T       t430    o390 b429  T       t430    o b408 b429
1144  B       b430    t430  B       b430    t430
1145  T       t431    o423 b430  T       t431    o426 b430
1146  B       b431    t431  B       b431    t431
1147  P       p431    Number 214  T       t432    o392 b431
1148  P       p432    Number 243  B       b432    t432
1149  O       o432    location p431 p432  T       t433    o425 b432
1150  O       o433    str_open p431 p432  B       b433    t433
1151  P       p433    String TermAddr  P       p433    Number 214
1152  O       o434    string p433  P       p434    Number 243
1153  T       t434    o434  O       o434    location p433 p434
1154  B       b434    t434  O       o435    str_open p433 p434
1155  T       t435    o b434 b4  P       p435    String TermAddr
1156  B       b435    t435  O       o436    string p435
1157  T       t436    o b406 b435  T       t436    o436
1158  B       b436    t436  B       b436    t436
1159  T       t437    o b406 b436  T       t437    o b436 b4
1160  B       b437    t437  B       b437    t437
1161  T       t438    o433 b437  T       t438    o b408 b437
1162  B       b438    t438  B       b438    t438
1163  T       t439    o390 b438  T       t439    o b408 b438
1164  B       b439    t439  B       b439    t439
1165  T       t440    o432 b439  T       t440    o435 b439
1166  B       b440    t440  B       b440    t440
1167  P       p440    Number 244  T       t441    o392 b440
1168  P       p441    Number 272  B       b441    t441
1169  O       o441    location p440 p441  T       t442    o434 b441
1170  O       o442    str_open p440 p441  B       b442    t442
1171  P       p442    String TermMan  P       p442    Number 244
1172  O       o443    string p442  P       p443    Number 272
1173  T       t443    o443  O       o443    location p442 p443
1174  B       b443    t443  O       o444    str_open p442 p443
1175  T       t444    o b443 b4  P       p444    String TermMan
1176  B       b444    t444  O       o445    string p444
1177  T       t445    o b406 b444  T       t445    o445
1178  B       b445    t445  B       b445    t445
1179  T       t446    o b406 b445  T       t446    o b445 b4
1180  B       b446    t446  B       b446    t446
1181  T       t447    o442 b446  T       t447    o b408 b446
1182  B       b447    t447  B       b447    t447
1183  T       t448    o390 b447  T       t448    o b408 b447
1184  B       b448    t448  B       b448    t448
1185  T       t449    o441 b448  T       t449    o444 b448
1186  B       b449    t449  B       b449    t449
1187  P       p449    Number 273  T       t450    o392 b449
1188  P       p450    Number 303  B       b450    t450
1189  O       o450    location p449 p450  T       t451    o443 b450
1190  O       o451    str_open p449 p450  B       b451    t451
1191  P       p451    String TermSubst  P       p451    Number 273
1192  O       o452    string p451  P       p452    Number 303
1193  T       t452    o452  O       o452    location p451 p452
1194  B       b452    t452  O       o453    str_open p451 p452
1195  T       t453    o b452 b4  P       p453    String TermSubst
1196  B       b453    t453  O       o454    string p453
1197  T       t454    o b406 b453  T       t454    o454
1198  B       b454    t454  B       b454    t454
1199  T       t455    o b406 b454  T       t455    o b454 b4
1200  B       b455    t455  B       b455    t455
1201  T       t456    o451 b455  T       t456    o b408 b455
1202  B       b456    t456  B       b456    t456
1203  T       t457    o390 b456  T       t457    o b408 b456
1204  B       b457    t457  B       b457    t457
1205  T       t458    o450 b457  T       t458    o453 b457
1206  B       b458    t458  B       b458    t458
1207  P       p458    Number 304  T       t459    o392 b458
1208  P       p459    Number 331  B       b459    t459
1209  O       o459    location p458 p459  T       t460    o452 b459
1210  O       o460    str_open p458 p459  B       b460    t460
1211  P       p460    String Refine  P       p460    Number 304
1212  O       o461    string p460  P       p461    Number 331
1213  T       t461    o461  O       o461    location p460 p461
1214  B       b461    t461  O       o462    str_open p460 p461
1215  T       t462    o b461 b4  P       p462    String Refine
1216  B       b462    t462  O       o463    string p462
1217  T       t463    o b406 b462  T       t463    o463
1218  B       b463    t463  B       b463    t463
1219  T       t464    o b406 b463  T       t464    o b463 b4
1220  B       b464    t464  B       b464    t464
1221  T       t465    o460 b464  T       t465    o b408 b464
1222  B       b465    t465  B       b465    t465
1223  T       t466    o390 b465  T       t466    o b408 b465
1224  B       b466    t466  B       b466    t466
1225  T       t467    o459 b466  T       t467    o462 b466
1226  B       b467    t467  B       b467    t467
1227  P       p467    Number 332  T       t468    o392 b467
1228  P       p468    Number 364  B       b468    t468
1229  O       o468    location p467 p468  T       t469    o461 b468
1230  O       o469    str_open p467 p468  B       b469    t469
1231  P       p469    String RefineError  P       p469    Number 332
1232  O       o470    string p469  P       p470    Number 364
1233  T       t470    o470  O       o470    location p469 p470
1234  B       b470    t470  O       o471    str_open p469 p470
1235  T       t471    o b470 b4  P       p471    String RefineError
1236  B       b471    t471  O       o472    string p471
1237  T       t472    o b406 b471  T       t472    o472
1238  B       b472    t472  B       b472    t472
1239  T       t473    o b406 b472  T       t473    o b472 b4
1240  B       b473    t473  B       b473    t473
1241  T       t474    o469 b473  T       t474    o b408 b473
1242  B       b474    t474  B       b474    t474
1243  T       t475    o390 b474  T       t475    o b408 b474
1244  B       b475    t475  B       b475    t475
1245  T       t476    o468 b475  T       t476    o471 b475
1246  B       b476    t476  B       b476    t476
1247  P       p476    Number 365  T       t477    o392 b476
1248  P       p477    Number 381  B       b477    t477
1249  O       o477    location p476 p477  T       t478    o470 b477
1250  O       o478    str_open p476 p477  B       b478    t478
1251  P       p478    String Mp_resource  P       p478    Number 365
1252  O       o479    string p478  P       p479    Number 381
1253  T       t479    o479  O       o479    location p478 p479
1254  B       b479    t479  O       o480    str_open p478 p479
1255  T       t480    o b479 b4  P       p480    String Mp_resource
1256  B       b480    t480  O       o481    string p480
1257  T       t481    o478 b480  T       t481    o481
1258  B       b481    t481  B       b481    t481
1259  T       t482    o390 b481  T       t482    o b481 b4
1260  B       b482    t482  B       b482    t482
1261  T       t483    o477 b482  T       t483    o480 b482
1262  B       b483    t483  B       b483    t483
1263  P       p483    Number 382  T       t484    o392 b483
1264  P       p484    Number 399  B       b484    t484
1265  O       o484    location p483 p484  T       t485    o479 b484
1266  O       o485    str_open p483 p484  B       b485    t485
1267  P       p485    String Simple_print  P       p485    Number 382
1268  O       o486    string p485  P       p486    Number 399
1269  T       t486    o486  O       o486    location p485 p486
1270  B       b486    t486  O       o487    str_open p485 p486
1271  T       t487    o b486 b4  P       p487    String Simple_print
1272  B       b487    t487  O       o488    string p487
1273  T       t488    o485 b487  T       t488    o488
1274  B       b488    t488  B       b488    t488
1275  T       t489    o390 b488  T       t489    o b488 b4
1276  B       b489    t489  B       b489    t489
1277  T       t490    o484 b489  T       t490    o487 b489
1278  B       b490    t490  B       b490    t490
1279  P       p490    Number 401  T       t491    o392 b490
1280  P       p491    Number 417  B       b491    t491
1281  O       o491    location p490 p491  T       t492    o486 b491
1282  O       o492    str_open p490 p491  B       b492    t492
1283  P       p492    String Tactic_type  P       p492    Number 401
1284  O       o493    string p492  P       p493    Number 417
1285  T       t493    o493  O       o493    location p492 p493
1286  B       b493    t493  O       o494    str_open p492 p493
1287  T       t494    o b493 b4  P       p494    String Tactic_type
1288  B       b494    t494  O       o495    string p494
1289  T       t495    o492 b494  T       t495    o495
1290  B       b495    t495  B       b495    t495
1291  T       t496    o390 b495  T       t496    o b495 b4
1292  B       b496    t496  B       b496    t496
1293  T       t497    o491 b496  T       t497    o494 b496
1294  B       b497    t497  B       b497    t497
1295  P       p497    Number 418  T       t498    o392 b497
1296  P       p498    Number 444  B       b498    t498
1297  O       o498    location p497 p498  T       t499    o493 b498
1298  O       o499    str_open p497 p498  B       b499    t499
1299  P       p499    String Tacticals  P       p499    Number 418
1300  O       o500    string p499  P       p500    Number 444
1301  T       t500    o500  O       o500    location p499 p500
1302  B       b500    t500  O       o501    str_open p499 p500
1303  T       t501    o b500 b4  P       p501    String Tacticals
1304  B       b501    t501  O       o502    string p501
1305  T       t502    o b493 b501  T       t502    o502
1306  B       b502    t502  B       b502    t502
1307  T       t503    o499 b502  T       t503    o b502 b4
1308  B       b503    t503  B       b503    t503
1309  T       t504    o390 b503  T       t504    o b495 b503
1310  B       b504    t504  B       b504    t504
1311  T       t505    o498 b504  T       t505    o501 b504
1312  B       b505    t505  B       b505    t505
1313  P       p505    Number 445  T       t506    o392 b505
1314  P       p506    Number 469  B       b506    t506
1315  O       o506    location p505 p506  T       t507    o500 b506
1316  O       o507    str_open p505 p506  B       b507    t507
1317  P       p507    String Sequent  P       p507    Number 445
1318  O       o508    string p507  P       p508    Number 469
1319  T       t508    o508  O       o508    location p507 p508
1320  B       b508    t508  O       o509    str_open p507 p508
1321  T       t509    o b508 b4  P       p509    String Sequent
1322  B       b509    t509  O       o510    string p509
1323  T       t510    o b493 b509  T       t510    o510
1324  B       b510    t510  B       b510    t510
1325  T       t511    o507 b510  T       t511    o b510 b4
1326  B       b511    t511  B       b511    t511
1327  T       t512    o390 b511  T       t512    o b495 b511
1328  B       b512    t512  B       b512    t512
1329  T       t513    o506 b512  T       t513    o509 b512
1330  B       b513    t513  B       b513    t513
1331  P       p513    Number 470  T       t514    o392 b513
1332  P       p514    Number 500  B       b514    t514
1333  O       o514    location p513 p514  T       t515    o508 b514
1334  O       o515    str_open p513 p514  B       b515    t515
1335  P       p515    String Conversionals  P       p515    Number 470
1336  O       o516    string p515  P       p516    Number 500
1337  T       t516    o516  O       o516    location p515 p516
1338  B       b516    t516  O       o517    str_open p515 p516
1339  T       t517    o b516 b4  P       p517    String Conversionals
1340  B       b517    t517  O       o518    string p517
1341  T       t518    o b493 b517  T       t518    o518
1342  B       b518    t518  B       b518    t518
1343  T       t519    o515 b518  T       t519    o b518 b4
1344  B       b519    t519  B       b519    t519
1345  T       t520    o390 b519  T       t520    o b495 b519
1346  B       b520    t520  B       b520    t520
1347  T       t521    o514 b520  T       t521    o517 b520
1348  B       b521    t521  B       b521    t521
1349  P       p521    Number 501  T       t522    o392 b521
1350  P       p522    Number 511  B       b522    t522
1351  O       o522    location p521 p522  T       t523    o516 b522
1352  O       o523    str_open p521 p522  B       b523    t523
1353  O       o524    string p131  P       p523    Number 501
1354  T       t524    o524  P       p524    Number 511
1355  B       b524    t524  O       o524    location p523 p524
1356  T       t525    o b524 b4  O       o525    str_open p523 p524
1357  B       b525    t525  O       o526    string p131
1358  T       t526    o523 b525  T       t526    o526
1359  B       b526    t526  B       b526    t526
1360  T       t527    o390 b526  T       t527    o b526 b4
1361  B       b527    t527  B       b527    t527
1362  T       t528    o522 b527  T       t528    o525 b527
1363  B       b528    t528  B       b528    t528
1364  P       p528    Number 512  T       t529    o392 b528
1365  P       p529    Number 520  B       b529    t529
1366  O       o529    location p528 p529  T       t530    o524 b529
1367  O       o530    str_open p528 p529  B       b530    t530
1368  O       o531    string p129  P       p530    Number 512
1369  T       t531    o531  P       p531    Number 520
1370  B       b531    t531  O       o531    location p530 p531
1371  T       t532    o b531 b4  O       o532    str_open p530 p531
1372  B       b532    t532  O       o533    string p129
1373  T       t533    o530 b532  T       t533    o533
1374  B       b533    t533  B       b533    t533
1375  T       t534    o390 b533  T       t534    o b533 b4
1376  B       b534    t534  B       b534    t534
1377  T       t535    o529 b534  T       t535    o532 b534
1378  B       b535    t535  B       b535    t535
1379  P       p535    Number 522  T       t536    o392 b535
1380  P       p536    Number 539  B       b536    t536
1381  O       o536    location p535 p536  T       t537    o531 b536
1382  O       o537    str_open p535 p536  B       b537    t537
1383  O       o538    string p119  P       p537    Number 522
1384  T       t538    o538  P       p538    Number 539
1385  B       b538    t538  O       o538    location p537 p538
1386  T       t539    o b538 b4  O       o539    str_open p537 p538
1387  B       b539    t539  O       o540    string p119
1388  T       t540    o537 b539  T       t540    o540
1389  B       b540    t540  B       b540    t540
1390  T       t541    o390 b540  T       t541    o b540 b4
1391  B       b541    t541  B       b541    t541
1392  T       t542    o536 b541  T       t542    o539 b541
1393  B       b542    t542  B       b542    t542
1394  P       p542    Number 540  T       t543    o392 b542
1395  P       p543    Number 561  B       b543    t543
1396  O       o543    location p542 p543  T       t544    o538 b543
1397  O       o544    str_open p542 p543  B       b544    t544
1398  O       o545    string p121  P       p544    Number 540
1399  T       t545    o545  P       p545    Number 561
1400  B       b545    t545  O       o545    location p544 p545
1401  T       t546    o b545 b4  O       o546    str_open p544 p545
1402  B       b546    t546  O       o547    string p121
1403  T       t547    o544 b546  T       t547    o547
1404  B       b547    t547  B       b547    t547
1405  T       t548    o390 b547  T       t548    o b547 b4
1406  B       b548    t548  B       b548    t548
1407  T       t549    o543 b548  T       t549    o546 b548
1408  B       b549    t549  B       b549    t549
1409  P       p549    Number 563  T       t550    o392 b549
1410  P       p550    Number 574  B       b550    t550
1411  O       o550    location p549 p550  T       t551    o545 b550
1412    B       b551    t551
1413    P       p551    Number 563
1414    P       p552    Number 574
1415    O       o552    location p551 p552
1416  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1417  P       p551    String car  P       p553    String car
1418  O       o551    opname p551  O       o553    opname p553
1419  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1420  NCzf_itt_group!car      car     car Czf_itt_group  NCzf_itt_group!car      car     car Czf_itt_group
1421  O       o552    car  O       o554    car
1422  T       t552    o552  T       t554    o554
 B       b552    t552  
 T       t553    o551 b552  
 B       b553    t553  
 T       t554    o550 b553  
1423  B       b554    t554  B       b554    t554
1424  P       p554    Number 615  T       t555    o553 b554
1425  P       p555    Number 635  B       b555    t555
1426  O       o555    location p554 p555  T       t556    o552 b555
1427  P       p556    String op  B       b556    t556
1428  O       o556    opname p556  P       p556    Number 615
1429    P       p557    Number 635
1430    O       o557    location p556 p557
1431    P       p558    String op
1432    O       o558    opname p558
1433  NCzf_itt_group!op       op      op Czf_itt_group  NCzf_itt_group!op       op      op Czf_itt_group
1434  O       o557    op  O       o559    op
1435  Nvar    var     var NIL  Nvar    var     var NIL
1436  P       p557    Var s1  P       p559    Var s1
1437  O       o558    var p557  O       o560    var p559
1438  T       t558    o558  T       t560    o560
 B       b558    t558  
 P       p558    Var s2  
 O       o559    var p558  
 T       t559    o559  
 B       b559    t559  
 T       t560    o557 b558 b559  
1439  B       b560    t560  B       b560    t560
1440  T       t561    o556 b560  P       p560    Var s2
1441    O       o561    var p560
1442    T       t561    o561
1443  B       b561    t561  B       b561    t561
1444  T       t562    o555 b561  T       t562    o559 b560 b561
1445  B       b562    t562  B       b562    t562
1446  P       p562    Number 636  T       t563    o558 b562
1447  P       p563    Number 646  B       b563    t563
1448  O       o563    location p562 p563  T       t564    o557 b563
1449  P       p564    String id  B       b564    t564
1450  O       o564    opname p564  P       p564    Number 636
1451    P       p565    Number 646
1452    O       o565    location p564 p565
1453    P       p566    String id
1454    O       o566    opname p566
1455  NCzf_itt_group!id       id      id Czf_itt_group  NCzf_itt_group!id       id      id Czf_itt_group
1456  O       o565    id  O       o567    id
1457  T       t565    o565  T       t567    o567
 B       b565    t565  
 T       t566    o564 b565  
 B       b566    t566  
 T       t567    o563 b566  
1458  B       b567    t567  B       b567    t567
1459  P       p567    Number 647  T       t568    o566 b567
1460  P       p568    Number 662  B       b568    t568
1461  O       o568    location p567 p568  T       t569    o565 b568
1462  P       p569    String inv  B       b569    t569
1463  O       o569    opname p569  P       p569    Number 647
1464    P       p570    Number 662
1465    O       o570    location p569 p570
1466    P       p571    String inv
1467    O       o571    opname p571
1468  NCzf_itt_group!inv      inv     inv Czf_itt_group  NCzf_itt_group!inv      inv     inv Czf_itt_group
1469  O       o570    inv  O       o572    inv
1470  P       p570    Var s  P       p572    Var s
1471  O       o571    var p570  O       o573    var p572
1472  T       t571    o571  T       t573    o573
 B       b571    t571  
 T       t572    o570 b571  
 B       b572    t572  
 T       t573    o569 b572  
1473  B       b573    t573  B       b573    t573
1474  T       t574    o568 b573  T       t574    o572 b573
1475  B       b574    t574  B       b574    t574
1476  P       p574    Number 664  T       t575    o571 b574
1477  P       p575    Number 713  B       b575    t575
1478  O       o575    location p574 p575  T       t576    o570 b575
1479    B       b576    t576
1480    P       p576    Number 664
1481    P       p577    Number 713
1482    O       o577    location p576 p577
1483  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
1484  P       p576    String car_df  P       p578    String car_df
1485  O       o576    dform p576  O       o578    dform p578
1486  NSummary!except_mode_df except_mode_df  except_mode_df Summary  NSummary!except_mode_df except_mode_df  except_mode_df Summary
1487  P       p577    String src  P       p579    String src
1488  O       o577    except_mode_df p577  O       o579    except_mode_df p579
 T       t577    o577  
 B       b577    t577  
 T       t578    o b577 b4  
 B       b578    t578  
 NSummary!df_term        df_term df_term Summary  
 O       o578    df_term  
 NPerv!string    string578       string Perv  
 P       p578    String S  
 O       o579    string578 p578  
1489  T       t579    o579  T       t579    o579
1490  B       b579    t579  B       b579    t579
1491  T       t580    o b579 b4  T       t580    o b579 b4
1492  B       b580    t580  B       b580    t580
1493  T       t581    o578 b580  NSummary!df_term        df_term df_term Summary
1494    O       o580    df_term
1495    NPerv!string    string580       string Perv
1496    P       p580    String G
1497    O       o581    string580 p580
1498    T       t581    o581
1499  B       b581    t581  B       b581    t581
1500  T       t582    o576 b578 b552 b581  T       t582    o b581 b4
1501  B       b582    t582  B       b582    t582
1502  T       t583    o575 b582  T       t583    o580 b582
1503  B       b583    t583  B       b583    t583
1504  P       p583    Number 715  T       t584    o578 b580 b554 b583
1505  P       p584    Number 762  B       b584    t584
1506  O       o584    location p583 p584  T       t585    o577 b584
1507  P       p585    String id_df  B       b585    t585
1508  O       o585    dform p585  P       p585    Number 715
1509  P       p586    String e  P       p586    Number 762
1510  O       o586    string578 p586  O       o586    location p585 p586
1511  T       t586    o586  P       p587    String id_df
1512  B       b586    t586  O       o587    dform p587
1513  T       t587    o b586 b4  P       p588    String e
1514  B       b587    t587  O       o588    string580 p588
1515  T       t588    o578 b587  T       t588    o588
1516  B       b588    t588  B       b588    t588
1517  T       t589    o585 b578 b565 b588  T       t589    o b588 b4
1518  B       b589    t589  B       b589    t589
1519  T       t590    o584 b589  T       t590    o580 b589
1520  B       b590    t590  B       b590    t590
1521  P       p590    Number 765  T       t591    o587 b580 b567 b590
1522  P       p591    Number 866  B       b591    t591
1523  O       o591    location p590 p591  T       t592    o586 b591
1524  P       p592    String op_df  B       b592    t592
1525  O       o592    dform p592  P       p592    Number 765
1526    P       p593    Number 866
1527    O       o593    location p592 p593
1528    P       p594    String op_df
1529    O       o594    dform p594
1530  NSummary!parens_df      parens_df       parens_df Summary  NSummary!parens_df      parens_df       parens_df Summary
1531  O       o593    parens_df  O       o595    parens_df
1532  T       t593    o593  T       t595    o595
 B       b593    t593  
 T       t594    o b593 b4  
 B       b594    t594  
 T       t595    o b577 b594  
1533  B       b595    t595  B       b595    t595
1534  Nslot   slot    slot NIL  T       t596    o b595 b4
 P       p595    String le  
 O       o595    slot p595  
 T       t596    o595 b558  
1535  B       b596    t596  B       b596    t596
1536  P       p596    String " * "  T       t597    o b579 b596
 O       o596    string578 p596  
 T       t597    o596  
1537  B       b597    t597  B       b597    t597
1538  T       t598    o595 b559  Nslot   slot    slot NIL
1539    P       p597    String le
1540    O       o597    slot p597
1541    T       t598    o597 b560
1542  B       b598    t598  B       b598    t598
1543  T       t599    o b598 b4  P       p598    String " * "
1544    O       o598    string580 p598
1545    T       t599    o598
1546  B       b599    t599  B       b599    t599
1547  T       t600    o b597 b599  T       t600    o597 b561
1548  B       b600    t600  B       b600    t600
1549  T       t601    o b596 b600  T       t601    o b600 b4
1550  B       b601    t601  B       b601    t601
1551  T       t602    o578 b601  T       t602    o b599 b601
1552  B       b602    t602  B       b602    t602
1553  T       t603    o592 b595 b560 b602  T       t603    o b598 b602
1554  B       b603    t603  B       b603    t603
1555  T       t604    o591 b603  T       t604    o580 b603
1556  B       b604    t604  B       b604    t604
1557  P       p604    Number 868  T       t605    o594 b597 b562 b604
1558  P       p605    Number 946  B       b605    t605
1559  O       o605    location p604 p605  T       t606    o593 b605
 P       p606    String inv_df  
 O       o606    dform p606  
 T       t606    o595 b571  
1560  B       b606    t606  B       b606    t606
1561  P       p607    String '  P       p606    Number 868
1562  O       o607    string578 p607  P       p607    Number 946
1563  T       t607    o607  O       o607    location p606 p607
1564  B       b607    t607  P       p608    String inv_df
1565  T       t608    o b607 b4  O       o608    dform p608
1566    T       t608    o597 b573
1567  B       b608    t608  B       b608    t608
1568  T       t609    o b606 b608  P       p609    String '
1569    O       o609    string580 p609
1570    T       t609    o609
1571  B       b609    t609  B       b609    t609
1572  T       t610    o578 b609  T       t610    o b609 b4
1573  B       b610    t610  B       b610    t610
1574  T       t611    o606 b595 b572 b610  T       t611    o b608 b610
1575  B       b611    t611  B       b611    t611
1576  T       t612    o605 b611  T       t612    o580 b611
1577  B       b612    t612  B       b612    t612
1578  P       p612    Number 961  T       t613    o608 b597 b574 b612
1579  P       p613    Number 1037  B       b613    t613
1580  O       o613    location p612 p613  T       t614    o607 b613
1581    B       b614    t614
1582    P       p614    Number 961
1583    P       p615    Number 1037
1584    O       o615    location p614 p615
1585  NSummary!rule   rule    rule Summary  NSummary!rule   rule    rule Summary
1586  P       p614    String car_wf  P       p616    String car_wf
1587  O       o614    rule p614  O       o616    rule p616
1588  NSummary!context_param  context_param   context_param Summary  NSummary!context_param  context_param   context_param Summary
1589  P       p615    String H  P       p617    String H
1590  O       o615    context_param p615  O       o617    context_param p617
 T       t615    o615  
 B       b615    t615  
 T       t616    o b615 b4  
 B       b616    t616  
 NSummary!meta_theorem   meta_theorem    meta_theorem Summary  
 O       o616    meta_theorem  
 P       p616    Var ext  
 O       o617    var p616  
1591  T       t617    o617  T       t617    o617
1592  B       b617    t617  B       b617    t617
1593  T       t618    o b617 b4  T       t618    o b617 b4
1594    B       b618    t618
1595    NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1596    O       o618    meta_theorem
1597    P       p618    Var ext
1598    O       o619    var p618
1599    T       t619    o619
1600    B       b619    t619
1601    T       t620    o b619 b4
1602  C       h       H  C       h       H
1603  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL
1604  NCzf_itt_set!isset      isset   isset Czf_itt_set  NCzf_itt_set!isset      isset   isset Czf_itt_set
1605  O       o618    isset  O       o620    isset
1606  T       t619    o618 b552  T       t621    o620 b554
1607  S       s       t618 h  S       s       t620 h
1608  G       s       t619  G       s       t621
1609  B       b619    s  B       b621    s
1610  T       t620    o616 b619  T       t622    o618 b621
1611  B       b620    t620  B       b622    t622
1612  NSummary!incomplete     incomplete      incomplete Summary  NSummary!incomplete     incomplete      incomplete Summary
1613  O       o620    incomplete  O       o622    incomplete
1614  T       t621    o620  T       t623    o622
1615  B       b621    t621  B       b623    t623
1616  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
1617  P       p621    Number 983  P       p623    Number 983
1618  P       p622    Number 990  P       p624    Number 990
1619  O       o622    resource_defs p621 p622 p262  O       o624    resource_defs p623 p624 p264
1620  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
1621  P       p623    Number 988  P       p625    Number 988
1622  O       o623    uid p623 p622  O       o625    uid p625 p624
1623  P       p624    String []  P       p626    String []
1624  O       o624    uid p624  O       o626    uid p626
1625  T       t624    o624  T       t626    o626
 B       b624    t624  
 T       t625    o623 b624  
 B       b625    t625  
 T       t626    o b625 b4  
1626  B       b626    t626  B       b626    t626
1627  T       t627    o622 b626  T       t627    o625 b626
1628  B       b627    t627  B       b627    t627
1629  T       t628    o b627 b4  T       t628    o b627 b4
1630  B       b628    t628  B       b628    t628
1631  T       t629    o614 b616 b620 b621 b628  T       t629    o624 b628
1632  B       b629    t629  B       b629    t629
1633  T       t630    o613 b629  T       t630    o b629 b4
1634  B       b630    t630  B       b630    t630
1635  P       p630    Number 1039  T       t631    o616 b618 b622 b623 b630
1636  P       p631    Number 1214  B       b631    t631
1637  O       o631    location p630 p631  T       t632    o615 b631
1638  P       p632    String op_wf1  B       b632    t632
1639  O       o632    rule p632  P       p632    Number 1039
1640    P       p633    Number 1214
1641    O       o633    location p632 p633
1642    P       p634    String op_wf1
1643    O       o634    rule p634
1644  NSummary!meta_implies   meta_implies    meta_implies Summary  NSummary!meta_implies   meta_implies    meta_implies Summary
1645  O       o633    meta_implies  O       o635    meta_implies
1646  NBase_trivial   Base_trivial    Base_trivial NIL  NBase_trivial   Base_trivial    Base_trivial NIL
1647  NBase_trivial!squash    squash  squash Base_trivial  NBase_trivial!squash    squash  squash Base_trivial
1648  O       o634    squash  O       o636    squash
1649  T       t634    o634  T       t636    o636
1650  B       b634    t634  B       b636    t636
1651  T       t635    o b634 b4  T       t637    o b636 b4
1652  T       t636    o618 b558  T       t638    o620 b560
1653  S       s636    t635 h  S       s638    t637 h
 G       s636    t636  
 B       b636    s636  
 T       t637    o616 b636  
 B       b637    t637  
 T       t638    o618 b559  
 S       s638    t635 h  
1654  G       s638    t638  G       s638    t638
1655  B       b638    s638  B       b638    s638
1656  T       t639    o616 b638  T       t639    o618 b638
1657  B       b639    t639  B       b639    t639
1658  T       t640    o618 b560  T       t640    o620 b561
1659  S       s640    t618 h  S       s640    t637 h
1660  G       s640    t640  G       s640    t640
1661  B       b640    s640  B       b640    s640
1662  T       t641    o616 b640  T       t641    o618 b640
1663  B       b641    t641  B       b641    t641
1664  T       t642    o633 b639 b641  T       t642    o620 b562
1665  B       b642    t642  S       s642    t620 h
1666  T       t643    o633 b637 b642  G       s642    t642
1667    B       b642    s642
1668    T       t643    o618 b642
1669  B       b643    t643  B       b643    t643
1670  P       p643    Number 1061  T       t644    o635 b641 b643
1671  P       p644    Number 1068  B       b644    t644
1672  O       o644    resource_defs p643 p644 p262  T       t645    o635 b639 b644
 P       p645    Number 1066  
 O       o645    uid p645 p644  
 T       t645    o645 b624  
1673  B       b645    t645  B       b645    t645
1674  T       t646    o b645 b4  P       p645    Number 1061
1675  B       b646    t646  P       p646    Number 1068
1676  T       t647    o644 b646  O       o646    resource_defs p645 p646 p264
1677    P       p647    Number 1066
1678    O       o647    uid p647 p646
1679    T       t647    o647 b626
1680  B       b647    t647  B       b647    t647
1681  T       t648    o b647 b4  T       t648    o b647 b4
1682  B       b648    t648  B       b648    t648
1683  T       t649    o632 b616 b643 b621 b648  T       t649    o646 b648
1684  B       b649    t649  B       b649    t649
1685  T       t650    o631 b649  T       t650    o b649 b4
1686  B       b650    t650  B       b650    t650
1687  P       p650    Number 1216  T       t651    o634 b618 b645 b623 b650
1688  P       p651    Number 1486  B       b651    t651
1689  O       o651    location p650 p651  T       t652    o633 b651
1690  P       p652    String op_wf2  B       b652    t652
1691  O       o652    rule p652  P       p652    Number 1216
1692    P       p653    Number 1486
1693    O       o653    location p652 p653
1694    P       p654    String op_wf2
1695    O       o654    rule p654
1696  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1697  NCzf_itt_member!mem     mem     mem Czf_itt_member  NCzf_itt_member!mem     mem     mem Czf_itt_member
1698  O       o653    mem  O       o655    mem
1699  T       t653    o653 b558 b552  T       t655    o655 b560 b554
1700  S       s653    t618 h  S       s655    t620 h
 G       s653    t653  
 B       b653    s653  
 T       t654    o616 b653  
 B       b654    t654  
 T       t655    o653 b559 b552  
 S       s655    t618 h  
1701  G       s655    t655  G       s655    t655
1702  B       b655    s655  B       b655    s655
1703  T       t656    o616 b655  T       t656    o618 b655
1704  B       b656    t656  B       b656    t656
1705  T       t657    o653 b560 b552  T       t657    o655 b561 b554
1706  S       s657    t618 h  S       s657    t620 h
1707  G       s657    t657  G       s657    t657
1708  B       b657    s657  B       b657    s657
1709  T       t658    o616 b657  T       t658    o618 b657
1710  B       b658    t658  B       b658    t658
1711  T       t659    o633 b656 b658  T       t659    o655 b562 b554
1712  B       b659    t659  S       s659    t620 h
1713  T       t660    o633 b654 b659  G       s659    t659
1714    B       b659    s659
1715    T       t660    o618 b659
1716  B       b660    t660  B       b660    t660
1717  T       t661    o633 b639 b660  T       t661    o635 b658 b660
1718  B       b661    t661  B       b661    t661
1719  T       t662    o633 b637 b661  T       t662    o635 b656 b661
1720  B       b662    t662  B       b662    t662
1721  P       p662    Number 1238  T       t663    o635 b641 b662
1722  P       p663    Number 1245  B       b663    t663
1723  O       o663    resource_defs p662 p663 p262  T       t664    o635 b639 b663
 P       p664    Number 1243  
 O       o664    uid p664 p663  
 T       t664    o664 b624  
1724  B       b664    t664  B       b664    t664
1725  T       t665    o b664 b4  P       p664    Number 1238
1726  B       b665    t665  P       p665    Number 1245
1727  T       t666    o663 b665  O       o665    resource_defs p664 p665 p264
1728    P       p666    Number 1243
1729    O       o666    uid p666 p665
1730    T       t666    o666 b626
1731  B       b666    t666  B       b666    t666
1732  T       t667    o b666 b4  T       t667    o b666 b4
1733  B       b667    t667  B       b667    t667
1734  T       t668    o652 b616 b662 b621 b667  T       t668    o665 b667
1735  B       b668    t668  B       b668    t668
1736  T       t669    o651 b668  T       t669    o b668 b4
1737  B       b669    t669  B       b669    t669
1738  P       p669    Number 1488  T       t670    o654 b618 b664 b623 b669
1739  P       p670    Number 1766  B       b670    t670
1740  O       o670    location p669 p670  T       t671    o653 b670
1741  P       p671    String op_eq1  B       b671    t671
1742  O       o671    rule p671  P       p671    Number 1488
1743  P       p672    Var s3  P       p672    Number 1766
1744  O       o672    var p672  O       o672    location p671 p672
1745  T       t672    o672  P       p673    String op_eq1
1746  B       b672    t672  O       o673    rule p673
1747  T       t673    o618 b672  P       p674    Var s3
1748  S       s673    t635 h  O       o674    var p674
1749  G       s673    t673  T       t674    o674
 B       b673    s673  
 T       t674    o616 b673  
1750  B       b674    t674  B       b674    t674
1751  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  T       t675    o620 b674
1752  NCzf_itt_eq!eq  eq      eq Czf_itt_eq  S       s675    t637 h
 O       o674    eq  
 T       t675    o674 b558 b559  
 S       s675    t618 h  
1753  G       s675    t675  G       s675    t675
1754  B       b675    s675  B       b675    s675
1755  T       t676    o616 b675  T       t676    o618 b675
1756  B       b676    t676  B       b676    t676
1757  T       t677    o557 b672 b558  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
1758  B       b677    t677  NCzf_itt_eq!eq  eq      eq Czf_itt_eq
1759  T       t678    o557 b672 b559  O       o676    eq
1760    T       t677    o676 b560 b561
1761    S       s677    t620 h
1762    G       s677    t677
1763    B       b677    s677
1764    T       t678    o618 b677
1765  B       b678    t678  B       b678    t678
1766  T       t679    o674 b677 b678  T       t679    o559 b674 b560
1767  S       s679    t618 h  B       b679    t679
1768  G       s679    t679  T       t680    o559 b674 b561
 B       b679    s679  
 T       t680    o616 b679  
1769  B       b680    t680  B       b680    t680
1770  T       t681    o633 b676 b680  T       t681    o676 b679 b680
1771  B       b681    t681  S       s681    t620 h
1772  T       t682    o633 b674 b681  G       s681    t681
1773    B       b681    s681
1774    T       t682    o618 b681
1775  B       b682    t682  B       b682    t682
1776  T       t683    o633 b639 b682  T       t683    o635 b678 b682
1777  B       b683    t683  B       b683    t683
1778  T       t684    o633 b637 b683  T       t684    o635 b676 b683
1779  B       b684    t684  B       b684    t684
1780  P       p684    Number 1510  T       t685    o635 b641 b684
1781  P       p685    Number 1517  B       b685    t685
1782  O       o685    resource_defs p684 p685 p262  T       t686    o635 b639 b685
 P       p686    Number 1515  
 O       o686    uid p686 p685  
 T       t686    o686 b624  
1783  B       b686    t686  B       b686    t686
1784  T       t687    o b686 b4  P       p686    Number 1510
1785  B       b687    t687  P       p687    Number 1517
1786  T       t688    o685 b687  O       o687    resource_defs p686 p687 p264
1787    P       p688    Number 1515
1788    O       o688    uid p688 p687
1789    T       t688    o688 b626
1790  B       b688    t688  B       b688    t688
1791  T       t689    o b688 b4  T       t689    o b688 b4
1792  B       b689    t689  B       b689    t689
1793  T       t690    o671 b616 b684 b621 b689  T       t690    o687 b689
1794  B       b690    t690  B       b690    t690
1795  T       t691    o670 b690  T       t691    o b690 b4
1796  B       b691    t691  B       b691    t691
1797  P       p691    Number 1768  T       t692    o673 b618 b686 b623 b691
1798  P       p692    Number 2046  B       b692    t692
1799  O       o692    location p691 p692  T       t693    o672 b692
 P       p693    String op_eq2  
 O       o693    rule p693  
 T       t693    o557 b558 b672  
1800  B       b693    t693  B       b693    t693
1801  T       t694    o557 b559 b672  P       p693    Number 1768
1802  B       b694    t694  P       p694    Number 2046
1803  T       t695    o674 b693 b694  O       o694    location p693 p694
1804  S       s695    t618 h  P       p695    String op_eq2
1805  G       s695    t695  O       o695    rule p695
1806  B       b695    s695  T       t695    o559 b560 b674
1807  T       t696    o616 b695  B       b695    t695
1808    T       t696    o559 b561 b674
1809  B       b696    t696  B       b696    t696
1810  T       t697    o633 b676 b696  T       t697    o676 b695 b696
1811  B       b697    t697  S       s697    t620 h
1812  T       t698    o633 b674 b697  G       s697    t697
1813    B       b697    s697
1814    T       t698    o618 b697
1815  B       b698    t698  B       b698    t698
1816  T       t699    o633 b639 b698  T       t699    o635 b678 b698
1817  B       b699    t699  B       b699    t699
1818  T       t700    o633 b637 b699  T       t700    o635 b676 b699
1819  B       b700    t700  B       b700    t700
1820  P       p700    Number 1790  T       t701    o635 b641 b700
1821  P       p701    Number 1797  B       b701    t701
1822  O       o701    resource_defs p700 p701 p262  T       t702    o635 b639 b701
 P       p702    Number 1795  
 O       o702    uid p702 p701  
 T       t702    o702 b624  
1823  B       b702    t702  B       b702    t702
1824  T       t703    o b702 b4  P       p702    Number 1790
1825  B       b703    t703  P       p703    Number 1797
1826  T       t704    o701 b703  O       o703    resource_defs p702 p703 p264
1827    P       p704    Number 1795
1828    O       o704    uid p704 p703
1829    T       t704    o704 b626
1830  B       b704    t704  B       b704    t704
1831  T       t705    o b704 b4  T       t705    o b704 b4
1832  B       b705    t705  B       b705    t705
1833  T       t706    o693 b616 b700 b621 b705  T       t706    o703 b705
1834  B       b706    t706  B       b706    t706
1835  T       t707    o692 b706  T       t707    o b706 b4
1836  B       b707    t707  B       b707    t707
1837  P       p707    Number 2048  T       t708    o695 b618 b702 b623 b707
1838  P       p708    Number 2181  B       b708    t708
1839  O       o708    location p707 p708  T       t709    o694 b708
1840  P       p709    String op_fun1  B       b709    t709
1841  O       o709    rule p709  P       p709    Number 2048
1842  T       t709    o618 b571  P       p710    Number 2181
1843  S       s709    t635 h  O       o710    location p709 p710
1844  G       s709    t709  P       p711    String op_fun1
1845  B       b709    s709  O       o711    rule p711
1846  T       t710    o616 b709  T       t711    o620 b573
1847  B       b710    t710  S       s711    t637 h
1848    G       s711    t711
1849    B       b711    s711
1850    T       t712    o618 b711
1851    B       b712    t712
1852  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq
1853  O       o710    fun_set  O       o712    fun_set
1854  P       p710    Var z  P       p712    Var z
1855  O       o711    var p710  O       o713    var p712
1856  T       t711    o711  T       t713    o713
1857  B       b711    t711  B       b713    t713
1858  T       t712    o557 b711 b571  T       t714    o559 b713 b573
1859  B       b712    t712 z  B       b714    t714 z
1860  T       t713    o710 b712  T       t715    o712 b714
1861  S       s713    t618 h  S       s715    t620 h
1862  G       s713    t713  G       s715    t715
1863  B       b713    s713  B       b715    s715
1864  T       t714    o616 b713  T       t716    o618 b715
1865  B       b714    t714  B       b716    t716
1866  T       t715    o633 b710 b714  T       t717    o635 b712 b716
 B       b715    t715  
 P       p715    Number 2071  
 P       p716    Number 2078  
 O       o716    resource_defs p715 p716 p262  
 P       p717    Number 2076  
 O       o717    uid p717 p716  
 T       t717    o717 b624  
1867  B       b717    t717  B       b717    t717
1868  T       t718    o b717 b4  P       p717    Number 2071
1869  B       b718    t718  P       p718    Number 2078
1870  T       t719    o716 b718  O       o718    resource_defs p717 p718 p264
1871    P       p719    Number 2076
1872    O       o719    uid p719 p718
1873    T       t719    o719 b626
1874  B       b719    t719  B       b719    t719
1875  T       t720    o b719 b4  T       t720    o b719 b4
1876  B       b720    t720  B       b720    t720
1877  T       t721    o709 b616 b715 b621 b720  T       t721    o718 b720
1878  B       b721    t721  B       b721    t721
1879  T       t722    o708 b721  T       t722    o b721 b4
1880  B       b722    t722  B       b722    t722
1881  P       p722    Number 2183  T       t723    o711 b618 b717 b623 b722
1882  P       p723    Number 2316  B       b723    t723
1883  O       o723    location p722 p723  T       t724    o710 b723
1884  P       p724    String op_fun2  B       b724    t724
1885  O       o724    rule p724  P       p724    Number 2183
1886  T       t724    o557 b571 b711  P       p725    Number 2316
1887  B       b724    t724 z  O       o725    location p724 p725
1888  T       t725    o710 b724  P       p726    String op_fun2
1889  S       s725    t618 h  O       o726    rule p726
1890  G       s725    t725  T       t726    o559 b573 b713
1891  B       b725    s725  B       b726    t726 z
1892  T       t726    o616 b725  T       t727    o712 b726
1893  B       b726    t726  S       s727    t620 h
1894  T       t727    o633 b710 b726  G       s727    t727
1895  B       b727    t727  B       b727    s727
1896  P       p727    Number 2206  T       t728    o618 b727
1897  P       p728    Number 2213  B       b728    t728
1898  O       o728    resource_defs p727 p728 p262  T       t729    o635 b712 b728
 P       p729    Number 2211  
 O       o729    uid p729 p728  
 T       t729    o729 b624  
1899  B       b729    t729  B       b729    t729
1900  T       t730    o b729 b4  P       p729    Number 2206
1901  B       b730    t730  P       p730    Number 2213
1902  T       t731    o728 b730  O       o730    resource_defs p729 p730 p264
1903    P       p731    Number 2211
1904    O       o731    uid p731 p730
1905    T       t731    o731 b626
1906  B       b731    t731  B       b731    t731
1907  T       t732    o b731 b4  T       t732    o b731 b4
1908  B       b732    t732  B       b732    t732
1909  T       t733    o724 b616 b727 b621 b732  T       t733    o730 b732
1910  B       b733    t733  B       b733    t733
1911  T       t734    o723 b733  T       t734    o b733 b4
1912  B       b734    t734  B       b734    t734
1913  P       p734    Number 2506  T       t735    o726 b618 b729 b623 b734
1914  P       p735    Number 2899  B       b735    t735
1915  O       o735    location p734 p735  T       t736    o725 b735
1916  P       p736    String op_assoc1  B       b736    t736
1917  O       o736    rule p736  P       p736    Number 2506
1918  T       t736    o653 b672 b552  P       p737    Number 2899
1919  S       s736    t618 h  O       o737    location p736 p737
1920  G       s736    t736  P       p738    String op_assoc1
1921  B       b736    s736  O       o738    rule p738
1922  T       t737    o616 b736  T       t738    o655 b674 b554
1923  B       b737    t737  S       s738    t620 h
1924  NCzf_itt_eq!equal       equal   equal Czf_itt_eq  G       s738    t738
1925  O       o737    equal  B       b738    s738
1926  T       t738    o557 b560 b672  T       t739    o618 b738
 B       b738    t738  
 T       t739    o557 b558 b694  
1927  B       b739    t739  B       b739    t739
1928  T       t740    o737 b738 b739  NCzf_itt_eq!equal       equal   equal Czf_itt_eq
1929  S       s740    t618 h  O       o739    equal
1930  G       s740    t740  T       t740    o559 b562 b674
1931  B       b740    s740  B       b740    t740
1932  T       t741    o616 b740  T       t741    o559 b560 b696
1933  B       b741    t741  B       b741    t741
1934  T       t742    o633 b737 b741  T       t742    o739 b740 b741
1935  B       b742    t742  S       s742    t620 h
1936  T       t743    o633 b656 b742  G       s742    t742
1937    B       b742    s742
1938    T       t743    o618 b742
1939  B       b743    t743  B       b743    t743
1940  T       t744    o633 b654 b743  T       t744    o635 b739 b743
1941  B       b744    t744  B       b744    t744
1942  T       t745    o633 b674 b744  T       t745    o635 b658 b744
1943  B       b745    t745  B       b745    t745
1944  T       t746    o633 b639 b745  T       t746    o635 b656 b745
1945  B       b746    t746  B       b746    t746
1946  T       t747    o633 b637 b746  T       t747    o635 b676 b746
1947  B       b747    t747  B       b747    t747
1948  P       p747    Number 2531  T       t748    o635 b641 b747
1949  P       p748    Number 2538  B       b748    t748
1950  O       o748    resource_defs p747 p748 p262  T       t749    o635 b639 b748
 P       p749    Number 2536  
 O       o749    uid p749 p748  
 T       t749    o749 b624  
1951  B       b749    t749  B       b749    t749
1952  T       t750    o b749 b4  P       p749    Number 2531
1953  B       b750    t750  P       p750    Number 2538
1954  T       t751    o748 b750  O       o750    resource_defs p749 p750 p264
1955    P       p751    Number 2536
1956    O       o751    uid p751 p750
1957    T       t751    o751 b626
1958  B       b751    t751  B       b751    t751
1959  T       t752    o b751 b4  T       t752    o b751 b4
1960  B       b752    t752  B       b752    t752
1961  T       t753    o736 b616 b747 b621 b752  T       t753    o750 b752
1962  B       b753    t753  B       b753    t753
1963  T       t754    o735 b753  T       t754    o b753 b4
1964  B       b754    t754  B       b754    t754
1965  P       p754    Number 2972  T       t755    o738 b618 b749 b623 b754
1966  P       p755    Number 3365  B       b755    t755
1967  O       o755    location p754 p755  T       t756    o737 b755
1968  P       p756    String op_assoc2  B       b756    t756
1969  O       o756    rule p756  P       p756    Number 2972
1970  T       t756    o737 b739 b738  P       p757    Number 3365
1971  S       s756    t618 h  O       o757    location p756 p757
1972  G       s756    t756  P       p758    String op_assoc2
1973  B       b756    s756  O       o758    rule p758
1974  T       t757    o616 b756  T       t758    o739 b741 b740
1975  B       b757    t757  S       s758    t620 h
1976  T       t758    o633 b737 b757  G       s758    t758
1977  B       b758    t758  B       b758    s758
1978  T       t759    o633 b656 b758  T       t759    o618 b758
1979  B       b759    t759  B       b759    t759
1980  T       t760    o633 b654 b759  T       t760    o635 b739 b759
1981  B       b760    t760  B       b760    t760
1982  T       t761    o633 b674 b760  T       t761    o635 b658 b760
1983  B       b761    t761  B       b761    t761
1984  T       t762    o633 b639 b761  T       t762    o635 b656 b761
1985  B       b762    t762  B       b762    t762
1986  T       t763    o633 b637 b762  T       t763    o635 b676 b762
1987  B       b763    t763  B       b763    t763
1988  P       p763    Number 2997  T       t764    o635 b641 b763
1989  P       p764    Number 3004  B       b764    t764
1990  O       o764    resource_defs p763 p764 p262  T       t765    o635 b639 b764
 P       p765    Number 3002  
 O       o765    uid p765 p764  
 T       t765    o765 b624  
1991  B       b765    t765  B       b765    t765
1992  T       t766    o b765 b4  P       p765    Number 2997
1993  B       b766    t766  P       p766    Number 3004
1994  T       t767    o764 b766  O       o766    resource_defs p765 p766 p264
1995    P       p767    Number 3002
1996    O       o767    uid p767 p766
1997    T       t767    o767 b626
1998  B       b767    t767  B       b767    t767
1999  T       t768    o b767 b4  T       t768    o b767 b4
2000  B       b768    t768  B       b768    t768
2001  T       t769    o756 b616 b763 b621 b768  T       t769    o766 b768
2002  B       b769    t769  B       b769    t769
2003  T       t770    o755 b769  T       t770    o b769 b4
2004  B       b770    t770  B       b770    t770
2005  P       p770    Number 3438  T       t771    o758 b618 b765 b623 b770
2006  P       p771    Number 3514  B       b771    t771
2007  O       o771    location p770 p771  T       t772    o757 b771
2008  P       p772    String id_wf1  B       b772    t772
2009  O       o772    rule p772  P       p772    Number 3438
2010  T       t772    o618 b565  P       p773    Number 3514
2011  S       s772    t618 h  O       o773    location p772 p773
2012  G       s772    t772  P       p774    String id_wf1
2013  B       b772    s772  O       o774    rule p774
2014  T       t773    o616 b772  T       t774    o620 b567
2015  B       b773    t773  S       s774    t620 h
2016  P       p773    Number 3460  G       s774    t774
2017  P       p774    Number 3468  B       b774    s774
2018  O       o774    resource_defs p773 p774 p262  T       t775    o618 b774
 P       p775    Number 3466  
 O       o775    uid p775 p774  
 T       t775    o775 b624  
2019  B       b775    t775  B       b775    t775
2020  T       t776    o b775 b4  P       p775    Number 3460
2021  B       b776    t776  P       p776    Number 3468
2022  T       t777    o774 b776  O       o776    resource_defs p775 p776 p264
2023    P       p777    Number 3466
2024    O       o777    uid p777 p776
2025    T       t777    o777 b626
2026  B       b777    t777  B       b777    t777
2027  T       t778    o b777 b4  T       t778    o b777 b4
2028  B       b778    t778  B       b778    t778
2029  T       t779    o772 b616 b773 b621 b778  T       t779    o776 b778
2030  B       b779    t779  B       b779    t779
2031  T       t780    o771 b779  T       t780    o b779 b4
2032  B       b780    t780  B       b780    t780
2033  P       p780    Number 3517  T       t781    o774 b618 b775 b623 b780
2034  P       p781    Number 3595  B       b781    t781
2035  O       o781    location p780 p781  T       t782    o773 b781
2036  P       p782    String id_wf2  B       b782    t782
2037  O       o782    rule p782  P       p782    Number 3517
2038  T       t782    o653 b565 b552  P       p783    Number 3595
2039  S       s782    t618 h  O       o783    location p782 p783
2040  G       s782    t782  P       p784    String id_wf2
2041  B       b782    s782  O       o784    rule p784
2042  T       t783    o616 b782  T       t784    o655 b567 b554
2043  B       b783    t783  S       s784    t620 h
2044  P       p783    Number 3539  G       s784    t784
2045  P       p784    Number 3546  B       b784    s784
2046  O       o784    resource_defs p783 p784 p262  T       t785    o618 b784
 P       p785    Number 3544  
 O       o785    uid p785 p784  
 T       t785    o785 b624  
2047  B       b785    t785  B       b785    t785
2048  T       t786    o b785 b4  P       p785    Number 3539
2049  B       b786    t786  P       p786    Number 3546
2050  T       t787    o784 b786  O       o786    resource_defs p785 p786 p264
2051    P       p787    Number 3544
2052    O       o787    uid p787 p786
2053    T       t787    o787 b626
2054  B       b787    t787  B       b787    t787
2055  T       t788    o b787 b4  T       t788    o b787 b4
2056  B       b788    t788  B       b788    t788
2057  T       t789    o782 b616 b783 b621 b788  T       t789    o786 b788
2058  B       b789    t789  B       b789    t789
2059  T       t790    o781 b789  T       t790    o b789 b4
2060  B       b790    t790  B       b790    t790
2061  P       p790    Number 3683  T       t791    o784 b618 b785 b623 b790
2062  P       p791    Number 3859  B       b791    t791
2063  O       o791    location p790 p791  T       t792    o783 b791
2064  P       p792    String id_eq1  B       b792    t792
2065  O       o792    rule p792  P       p792    Number 3684
2066  T       t792    o653 b571 b552  P       p793    Number 3860
2067  S       s792    t618 h  O       o793    location p792 p793
2068  G       s792    t792  P       p794    String id_eq1
2069  B       b792    s792  O       o794    rule p794
2070  T       t793    o616 b792  T       t794    o655 b573 b554
2071  B       b793    t793  S       s794    t620 h
2072  T       t794    o557 b565 b571  G       s794    t794
2073  B       b794    t794  B       b794    s794
2074  T       t795    o737 b794 b571  T       t795    o618 b794
2075  S       s795    t618 h  B       b795    t795
2076  G       s795    t795  T       t796    o559 b567 b573
 B       b795    s795  
 T       t796    o616 b795  
2077  B       b796    t796  B       b796    t796
2078  T       t797    o633 b793 b796  T       t797    o739 b796 b573
2079  B       b797    t797  S       s797    t620 h
2080  T       t798    o633 b710 b797  G       s797    t797
2081    B       b797    s797
2082    T       t798    o618 b797
2083  B       b798    t798  B       b798    t798
2084  P       p798    Number 3705  T       t799    o635 b795 b798
2085  P       p799    Number 3712  B       b799    t799
2086  O       o799    resource_defs p798 p799 p262  T       t800    o635 b712 b799
 P       p800    Number 3710  
 O       o800    uid p800 p799  
 T       t800    o800 b624  
2087  B       b800    t800  B       b800    t800
2088  T       t801    o b800 b4  P       p800    Number 3706
2089  B       b801    t801  P       p801    Number 3713
2090  T       t802    o799 b801  O       o801    resource_defs p800 p801 p264
2091    P       p802    Number 3711
2092    O       o802    uid p802 p801
2093    T       t802    o802 b626
2094  B       b802    t802  B       b802    t802
2095  T       t803    o b802 b4  T       t803    o b802 b4
2096  B       b803    t803  B       b803    t803
2097  T       t804    o792 b616 b798 b621 b803  T       t804    o801 b803
2098  B       b804    t804  B       b804    t804
2099  T       t805    o791 b804  T       t805    o b804 b4
2100  B       b805    t805  B       b805    t805
2101  P       p805    Number 3861  T       t806    o794 b618 b800 b623 b805
 O       o805    location p805 p304  
 P       p806    String id_eq2  
 O       o806    rule p806  
 T       t806    o557 b571 b565  
2102  B       b806    t806  B       b806    t806
2103  T       t807    o737 b806 b571  T       t807    o793 b806
2104  S       s807    t618 h  B       b807    t807
2105  G       s807    t807  P       p807    Number 3862
2106  B       b807    s807  P       p808    Number 4038
2107  T       t808    o616 b807  O       o808    location p807 p808
2108  B       b808    t808  P       p809    String id_eq2
2109  T       t809    o633 b793 b808  O       o809    rule p809
2110    T       t809    o559 b573 b567
2111  B       b809    t809  B       b809    t809
2112  T       t810    o633 b710 b809  T       t810    o739 b809 b573
2113  B       b810    t810  S       s810    t620 h
2114  P       p810    Number 3883  G       s810    t810
2115  P       p811    Number 3890  B       b810    s810
2116  O       o811    resource_defs p810 p811 p262  T       t811    o618 b810
2117  P       p812    Number 3888  B       b811    t811
2118  O       o812    uid p812 p811  T       t812    o635 b795 b811
 T       t812    o812 b624  
2119  B       b812    t812  B       b812    t812
2120  T       t813    o b812 b4  T       t813    o635 b712 b812
2121  B       b813    t813  B       b813    t813
2122  T       t814    o811 b813  P       p813    Number 3884
2123  B       b814    t814  P       p814    Number 3891
2124  T       t815    o b814 b4  O       o814    resource_defs p813 p814 p264
2125    P       p815    Number 3889
2126    O       o815    uid p815 p814
2127    T       t815    o815 b626
2128  B       b815    t815  B       b815    t815
2129  T       t816    o806 b616 b810 b621 b815  T       t816    o b815 b4
2130  B       b816    t816  B       b816    t816
2131  T       t817    o805 b816  T       t817    o814 b816
2132  B       b817    t817  B       b817    t817
2133  P       p817    Number 4039  T       t818    o b817 b4
2134  P       p818    Number 4096  B       b818    t818
2135  O       o818    location p817 p818  T       t819    o809 b618 b813 b623 b818
2136    B       b819    t819
2137    T       t820    o808 b819
2138    B       b820    t820
2139    P       p820    Number 4040
2140    P       p821    Number 4097
2141    O       o821    location p820 p821
2142  NOcaml!str_let  str_let str_let Ocaml  NOcaml!str_let  str_let str_let Ocaml
2143  O       o819    str_let p817 p818  O       o822    str_let p820 p821
2144  NOcaml!patt_var patt_var        patt_var Ocaml  NOcaml!patt_var patt_var        patt_var Ocaml
2145  O       o820    patt_var p302 p818  P       p822    Number 4044
2146    O       o823    patt_var p822 p821
2147  NOcaml!patt_done        patt_done       patt_done Ocaml  NOcaml!patt_done        patt_done       patt_done Ocaml
2148  O       o821    patt_done p817 p818  O       o824    patt_done p820 p821
2149  T       t821    o821  T       t824    o824
2150  B       b821    t821 id_elim2T  B       b824    t824 id_elim2T
2151  T       t822    o820 b821  T       t825    o823 b824
2152  B       b822    t822  B       b825    t825
2153  NOcaml!fun      fun     fun Ocaml  NOcaml!fun      fun     fun Ocaml
2154  O       o822    fun p302 p818  O       o825    fun p822 p821
2155  NOcaml!patt_if  patt_if patt_if Ocaml  NOcaml!patt_if  patt_if patt_if Ocaml
2156  O       o823    patt_if p302 p818  O       o826    patt_if p822 p821
2157  P       p823    Number 4053  P       p826    Number 4054
2158  P       p824    Number 4054  P       p827    Number 4055
2159  O       o824    patt_var p823 p824  O       o827    patt_var p826 p827
2160  NOcaml!patt_body        patt_body       patt_body Ocaml  NOcaml!patt_body        patt_body       patt_body Ocaml
2161  O       o825    patt_body p302 p818  O       o828    patt_body p822 p821
2162  NOcaml!apply    apply   apply Ocaml  NOcaml!apply    apply   apply Ocaml
2163  P       p825    Number 4060  P       p828    Number 4061
2164  O       o826    apply p825 p818  O       o829    apply p828 p821
2165  P       p826    Number 4094  P       p829    Number 4095
2166  O       o827    apply p825 p826  O       o830    apply p828 p829
2167  NOcaml!lid      lid     lid Ocaml  NOcaml!lid      lid     lid Ocaml
2168  P       p827    Number 4066  P       p830    Number 4067
2169  O       o828    lid p825 p827  O       o831    lid p828 p830
2170  O       o829    lid p792  O       o832    lid p794
2171  T       t829    o829  T       t832    o832
2172  B       b829    t829  B       b832    t832
2173  T       t830    o828 b829  T       t833    o831 b832
2174  B       b830    t830  B       b833    t833
2175  P       p830    Number 4068  P       p833    Number 4069
2176  P       p831    Number 4093  P       p834    Number 4094
2177  O       o831    apply p830 p831  O       o834    apply p833 p834
2178  NOcaml!proj     proj    proj Ocaml  NOcaml!proj     proj    proj Ocaml
2179  P       p832    Number 4091  P       p835    Number 4092
2180  O       o832    proj p830 p832  O       o835    proj p833 p835
2181  O       o833    uid p830 p832  O       o836    uid p833 p835
2182  O       o834    uid p507  O       o837    uid p509
2183  T       t834    o834  T       t837    o837
 B       b834    t834  
 T       t835    o833 b834  
 B       b835    t835  
 P       p835    Number 4077  
 O       o835    lid p835 p832  
 P       p836    String hyp_count_addr  
 O       o836    lid p836  
 T       t836    o836  
 B       b836    t836  
 T       t837    o835 b836  
2184  B       b837    t837  B       b837    t837
2185  T       t838    o832 b835 b837  T       t838    o836 b837
2186  B       b838    t838  B       b838    t838
2187  P       p838    Number 4092  P       p838    Number 4078
2188  O       o838    lid p838 p831  O       o838    lid p838 p835
2189  P       p839    Var p  P       p839    String hyp_count_addr
2190  O       o839    var p839  O       o839    lid p839
2191  T       t839    o839  T       t839    o839
2192  B       b839    t839  B       b839    t839
2193  T       t840    o838 b839  T       t840    o838 b839
2194  B       b840    t840  B       b840    t840
2195  T       t841    o831 b838 b840  T       t841    o835 b838 b840
2196  B       b841    t841  B       b841    t841
2197  T       t842    o827 b830 b841  P       p841    Number 4093
2198    O       o841    lid p841 p834
2199    P       p842    Var p
2200    O       o842    var p842
2201    T       t842    o842
2202  B       b842    t842  B       b842    t842
2203  P       p842    Number 4095  T       t843    o841 b842
 O       o842    lid p842 p818  
 T       t843    o842 b839  
2204  B       b843    t843  B       b843    t843
2205  T       t844    o826 b842 b843  T       t844    o834 b841 b843
2206  B       b844    t844  B       b844    t844
2207  T       t845    o825 b844  T       t845    o830 b833 b844
2208  B       b845    t845 p  B       b845    t845
2209  T       t846    o824 b845  P       p845    Number 4096
2210    O       o845    lid p845 p821
2211    T       t846    o845 b842
2212  B       b846    t846  B       b846    t846
2213  T       t847    o823 b846  T       t847    o829 b845 b846
2214  B       b847    t847  B       b847    t847
2215  T       t848    o822 b847  T       t848    o828 b847
2216  B       b848    t848  B       b848    t848 p
2217  T       t849    o819 b822 b848  T       t849    o827 b848
2218  B       b849    t849  B       b849    t849
2219  T       t850    o b849 b4  T       t850    o826 b849
2220  B       b850    t850  B       b850    t850
2221  T       t851    o819 b850  T       t851    o825 b850
2222  B       b851    t851  B       b851    t851
2223  T       t852    o390 b851  T       t852    o822 b825 b851
2224  B       b852    t852  B       b852    t852
2225  T       t853    o818 b852  T       t853    o b852 b4
2226  B       b853    t853  B       b853    t853
2227  P       p853    Number 4098  T       t854    o822 b853
2228  P       p854    Number 4271  B       b854    t854
2229  O       o854    location p853 p854  T       t855    o392 b854
 P       p855    String inv_wf1  
 O       o855    rule p855  
 T       t855    o570 b558  
2230  B       b855    t855  B       b855    t855
2231  T       t856    o618 b855  T       t856    o821 b855
2232  S       s856    t618 h  B       b856    t856
2233  G       s856    t856  P       p856    Number 4099
2234  B       b856    s856  P       p857    Number 4272
2235  T       t857    o616 b856  O       o857    location p856 p857
2236  B       b857    t857  P       p858    String inv_wf1
2237  T       t858    o633 b654 b857  O       o858    rule p858
2238    T       t858    o572 b560
2239  B       b858    t858  B       b858    t858
2240  T       t859    o633 b637 b858  T       t859    o620 b858
2241  B       b859    t859  S       s859    t620 h
2242  P       p859    Number 4121  G       s859    t859
2243  P       p860    Number 4128  B       b859    s859
2244  O       o860    resource_defs p859 p860 p262  T       t860    o618 b859
2245  P       p861    Number 4126  B       b860    t860
2246  O       o861    uid p861 p860  T       t861    o635 b656 b860
 T       t861    o861 b624  
2247  B       b861    t861  B       b861    t861
2248  T       t862    o b861 b4  T       t862    o635 b639 b861
2249  B       b862    t862  B       b862    t862
2250  T       t863    o860 b862  P       p862    Number 4122
2251  B       b863    t863  P       p863    Number 4129
2252  T       t864    o b863 b4  O       o863    resource_defs p862 p863 p264
2253    P       p864    Number 4127
2254    O       o864    uid p864 p863
2255    T       t864    o864 b626
2256  B       b864    t864  B       b864    t864
2257  T       t865    o855 b616 b859 b621 b864  T       t865    o b864 b4
2258  B       b865    t865  B       b865    t865
2259  T       t866    o854 b865  T       t866    o863 b865
2260  B       b866    t866  B       b866    t866
2261  P       p866    Number 4273  T       t867    o b866 b4
2262  P       p867    Number 4449  B       b867    t867
2263  O       o867    location p866 p867  T       t868    o858 b618 b862 b623 b867
2264  P       p868    String inv_wf2  B       b868    t868
2265  O       o868    rule p868  T       t869    o857 b868
 T       t868    o653 b855 b552  
 S       s868    t618 h  
 G       s868    t868  
 B       b868    s868  
 T       t869    o616 b868  
2266  B       b869    t869  B       b869    t869
2267  T       t870    o633 b654 b869  P       p869    Number 4274
2268  B       b870    t870  P       p870    Number 4450
2269  T       t871    o633 b637 b870  O       o870    location p869 p870
2270  B       b871    t871  P       p871    String inv_wf2
2271  P       p871    Number 4296  O       o871    rule p871
2272  P       p872    Number 4303  T       t871    o655 b858 b554
2273  O       o872    resource_defs p871 p872 p262  S       s871    t620 h
2274  P       p873    Number 4301  G       s871    t871
2275  O       o873    uid p873 p872  B       b871    s871
2276  T       t873    o873 b624  T       t872    o618 b871
2277    B       b872    t872
2278    T       t873    o635 b656 b872
2279  B       b873    t873  B       b873    t873
2280  T       t874    o b873 b4  T       t874    o635 b639 b873
2281  B       b874    t874  B       b874    t874
2282  T       t875    o872 b874  P       p874    Number 4297
2283  B       b875    t875  P       p875    Number 4304
2284  T       t876    o b875 b4  O       o875    resource_defs p874 p875 p264
2285    P       p876    Number 4302
2286    O       o876    uid p876 p875
2287    T       t876    o876 b626
2288  B       b876    t876  B       b876    t876
2289  T       t877    o868 b616 b871 b621 b876  T       t877    o b876 b4
2290  B       b877    t877  B       b877    t877
2291  T       t878    o867 b877  T       t878    o875 b877
2292  B       b878    t878  B       b878    t878
2293  P       p878    Number 4451  T       t879    o b878 b4
2294  P       p879    Number 4637  B       b879    t879
2295  O       o879    location p878 p879  T       t880    o871 b618 b874 b623 b879
 P       p880    String inv_id1  
 O       o880    rule p880  
 T       t880    o557 b855 b558  
2296  B       b880    t880  B       b880    t880
2297  T       t881    o737 b880 b565  T       t881    o870 b880
2298  S       s881    t618 h  B       b881    t881
2299  G       s881    t881  P       p881    Number 4452
2300  B       b881    s881  P       p882    Number 4539
2301  T       t882    o616 b881  O       o882    location p881 p882
2302  B       b882    t882  P       p883    String inv_fun1
2303  T       t883    o633 b654 b882  O       o883    rule p883
2304  B       b883    t883  T       t883    o572 b713
2305  T       t884    o633 b637 b883  B       b883    t883 z
2306  B       b884    t884  T       t884    o712 b883
2307  P       p884    Number 4474  S       s884    t620 h
2308  P       p885    Number 4481  G       s884    t884
2309  O       o885    resource_defs p884 p885 p262  B       b884    s884
2310  P       p886    Number 4479  T       t885    o618 b884
2311  O       o886    uid p886 p885  B       b885    t885
2312  T       t886    o886 b624  P       p885    Number 4476
2313  B       b886    t886  P       p886    Number 4483
2314  T       t887    o b886 b4  O       o886    resource_defs p885 p886 p264
2315    P       p887    Number 4481
2316    O       o887    uid p887 p886
2317    T       t887    o887 b626
2318  B       b887    t887  B       b887    t887
2319  T       t888    o885 b887  T       t888    o b887 b4
2320  B       b888    t888  B       b888    t888
2321  T       t889    o b888 b4  T       t889    o886 b888
2322  B       b889    t889  B       b889    t889
2323  T       t890    o880 b616 b884 b621 b889  T       t890    o b889 b4
2324  B       b890    t890  B       b890    t890
2325  T       t891    o879 b890  T       t891    o883 b618 b885 b623 b890
2326  B       b891    t891  B       b891    t891
2327  P       p891    Number 4639  T       t892    o882 b891
2328  P       p892    Number 4825  B       b892    t892
2329  O       o892    location p891 p892  P       p892    Number 4541
2330  P       p893    String inv_id2  P       p893    Number 4727
2331  O       o893    rule p893  O       o893    location p892 p893
2332  T       t893    o557 b558 b855  P       p894    String inv_id1
2333  B       b893    t893  O       o894    rule p894
2334  T       t894    o737 b893 b565  T       t894    o559 b858 b560
2335  S       s894    t618 h  B       b894    t894
2336  G       s894    t894  T       t895    o739 b894 b567
2337  B       b894    s894  S       s895    t620 h
2338  T       t895    o616 b894  G       s895    t895
2339  B       b895    t895  B       b895    s895
2340  T       t896    o633 b654 b895  T       t896    o618 b895
2341  B       b896    t896  B       b896    t896
2342  T       t897    o633 b637 b896  T       t897    o635 b656 b896
2343  B       b897    t897  B       b897    t897
2344  P       p897    Number 4662  T       t898    o635 b639 b897
2345  P       p898    Number 4669  B       b898    t898
2346  O       o898    resource_defs p897 p898 p262  P       p898    Number 4564
2347  P       p899    Number 4667  P       p899    Number 4571
2348  O       o899    uid p899 p898  O       o899    resource_defs p898 p899 p264
2349  T       t899    o899 b624  P       p900    Number 4569
2350  B       b899    t899  O       o900    uid p900 p899
2351  T       t900    o b899 b4  T       t900    o900 b626
2352  B       b900    t900  B       b900    t900
2353  T       t901    o898 b900  T       t901    o b900 b4
2354  B       b901    t901  B       b901    t901
2355  T       t902    o b901 b4  T       t902    o899 b901
2356  B       b902    t902  B       b902    t902
2357  T       t903    o893 b616 b897 b621 b902  T       t903    o b902 b4
2358  B       b903    t903  B       b903    t903
2359  T       t904    o892 b903  T       t904    o894 b618 b898 b623 b903
2360  B       b904    t904  B       b904    t904
2361  P       p904    Number 4885  T       t905    o893 b904
2362  P       p905    Number 5314  B       b905    t905
2363  O       o905    location p904 p905  P       p905    Number 4729
2364  P       p906    String cancelLeft  P       p906    Number 4915
2365  O       o906    rule p906  O       o906    location p905 p906
2366  NSummary!term_param     term_param      term_param Summary  P       p907    String inv_id2
2367  O       o907    term_param  O       o907    rule p907
2368  T       t907    o907 b558  T       t907    o559 b560 b858
2369  B       b907    t907  B       b907    t907
2370  T       t908    o b907 b4  T       t908    o739 b907 b567
2371  B       b908    t908  S       s908    t620 h
2372  T       t909    o b615 b908  G       s908    t908
2373    B       b908    s908
2374    T       t909    o618 b908
2375  B       b909    t909  B       b909    t909
2376  T       t910    o737 b560 b693  T       t910    o635 b656 b909
2377  S       s910    t618 h  B       b910    t910
2378  G       s910    t910  T       t911    o635 b639 b910
 B       b910    s910  
 T       t911    o616 b910  
2379  B       b911    t911  B       b911    t911
2380  T       t912    o737 b559 b672  P       p911    Number 4752
2381  S       s912    t618 h  P       p912    Number 4759
2382  G       s912    t912  O       o912    resource_defs p911 p912 p264
2383  B       b912    s912  P       p913    Number 4757
2384  T       t913    o616 b912  O       o913    uid p913 p912
2385    T       t913    o913 b626
2386  B       b913    t913  B       b913    t913
2387  T       t914    o633 b911 b913  T       t914    o b913 b4
2388  B       b914    t914  B       b914    t914
2389  T       t915    o633 b737 b914  T       t915    o912 b914
2390  B       b915    t915  B       b915    t915
2391  T       t916    o633 b656 b915  T       t916    o b915 b4
2392  B       b916    t916  B       b916    t916
2393  T       t917    o633 b654 b916  T       t917    o907 b618 b911 b623 b916
2394  B       b917    t917  B       b917    t917
2395  T       t918    o633 b674 b917  T       t918    o906 b917
2396  B       b918    t918  B       b918    t918
2397  T       t919    o633 b639 b918  P       p918    Number 5376
2398  B       b919    t919  P       p919    Number 5802
2399  T       t920    o633 b637 b919  O       o919    location p918 p919
2400  B       b920    t920  P       p920    String cancel1
2401  NSummary!interactive    interactive     interactive Summary  O       o920    rule p920
2402  O       o920    interactive  NSummary!term_param     term_param      term_param Summary
2403  NSummary!ext_rule       ext_rule        ext_rule Summary  O       o921    term_param
2404  P       p920    String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"  T       t921    o921 b560
2405  O       o921    ext_rule p920  B       b921    t921
2406  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  T       t922    o b921 b4
 O       o922    status_incomplete  
 T       t922    o922  
2407  B       b922    t922  B       b922    t922
2408  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  T       t923    o b617 b922
2409  O       o923    ext_unjustified  B       b923    t923
2410  NSummary!tactic_arg     tactic_arg      tactic_arg Summary  T       t924    o739 b562 b695
2411  P       p923    String main  S       s924    t620 h
2412  O       o924    tactic_arg p923  G       s924    t924
2413  NSummary!msequent       msequent        msequent Summary  B       b924    s924
2414  O       o925    msequent  T       t925    o618 b924
 T       t925    o b910 b4  
2415  B       b925    t925  B       b925    t925
2416  T       t926    o b736 b925  T       t926    o739 b561 b674
2417  B       b926    t926  S       s926    t620 h
2418  T       t927    o b655 b926  G       s926    t926
2419    B       b926    s926
2420    T       t927    o618 b926
2421  B       b927    t927  B       b927    t927
2422  T       t928    o b653 b927  T       t928    o635 b925 b927
2423  B       b928    t928  B       b928    t928
2424  T       t929    o b673 b928  T       t929    o635 b739 b928
2425  B       b929    t929  B       b929    t929
2426  T       t930    o b638 b929  T       t930    o635 b658 b929
2427  B       b930    t930  B       b930    t930
2428  T       t931    o b636 b930  T       t931    o635 b656 b930
2429  B       b931    t931  B       b931    t931
2430  T       t932    o925 b912 b931  T       t932    o635 b676 b931
2431  B       b932    t932  B       b932    t932
2432  NSummary!parent_none    parent_none     parent_none Summary  T       t933    o635 b641 b932
 O       o932    parent_none  
 T       t933    o932  
2433  B       b933    t933  B       b933    t933
2434  T       t934    o924 b932 b4 b933  T       t934    o635 b639 b933
2435  B       b934    t934  B       b934    t934
2436  P       p934    String assertion  NSummary!interactive    interactive     interactive Summary
2437  O       o934    tactic_arg p934  O       o934    interactive
2438  H       h934    v t910  NSummary!ext_rule       ext_rule        ext_rule Summary
2439  T       t935    o557 b855 b560  P       p934    String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2440  B       b935    t935  O       o935    ext_rule p934
2441  T       t936    o557 b855 b693  NSummary!status_incomplete      status_incomplete       status_incomplete Summary
2442    O       o936    status_incomplete
2443    T       t936    o936
2444  B       b936    t936  B       b936    t936
2445  T       t937    o737 b935 b936  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
2446  S       s937    t618 h h934  O       o937    ext_unjustified
2447  G       s937    t937  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
2448  B       b937    s937  P       p937    String main
2449  T       t938    o925 b937 b931  O       o938    tactic_arg p937
2450  B       b938    t938  NSummary!msequent       msequent        msequent Summary
2451  S       s938    t618 h h934  O       o939    msequent
2452  G       s938    t912  T       t939    o b924 b4
2453  B       b939    s938  B       b939    t939
2454  T       t939    o925 b939 b931  T       t940    o b738 b939
2455  B       b940    t939  B       b940    t940
2456  T       t940    o2 b934  T       t941    o b657 b940
2457  B       b941    t940  B       b941    t941
2458  T       t941    o924 b940 b4 b941  T       t942    o b655 b941
2459  B       b942    t941  B       b942    t942
2460  T       t942    o2 b942  T       t943    o b675 b942
2461  B       b943    t942  B       b943    t943
2462  T       t943    o934 b938 b4 b943  T       t944    o b640 b943
2463  B       b944    t943  B       b944    t944
2464  H       h944    v_1 t937  T       t945    o b638 b944
2465  S       s944    t618 h h934 h944  B       b945    t945
2466  G       s944    t912  T       t946    o939 b926 b945
2467  B       b945    s944  B       b946    t946
2468  T       t945    o925 b945 b931  NSummary!parent_none    parent_none     parent_none Summary
2469  B       b946    t945  O       o946    parent_none
2470  T       t946    o924 b946 b4 b943  T       t947    o946
2471  B       b947    t946  B       b947    t947
2472  T       t947    o b947 b4  T       t948    o938 b946 b4 b947
2473  B       b948    t947  B       b948    t948
2474  T       t948    o b944 b948  P       p948    String assertion
2475  B       b949    t948  O       o948    tactic_arg p948
2476  T       t949    o923 b934 b949  H       h948    v t924
2477  B       b950    t949  T       t949    o559 b858 b562
2478  P       p950    String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"  B       b949    t949
2479  O       o950    ext_rule p950  T       t950    o559 b858 b695
2480  T       t950    o923 b944 b4  B       b950    t950
2481  B       b951    t950  T       t951    o739 b949 b950
2482  T       t951    o950 b922 b951 b4 b4  S       s951    t620 h h948
2483  B       b952    t951  G       s951    t951
2484  P       p952    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"  B       b951    s951
2485  O       o952    ext_rule p952  T       t952    o939 b951 b945
2486  P       p953    String eq  B       b952    t952
2487  O       o953    tactic_arg p953  S       s952    t620 h h948
2488  T       t953    o557 b880 b559  G       s952    t926
2489  B       b953    t953  B       b953    s952
2490  T       t954    o737 b935 b953  T       t953    o939 b953 b945
2491  S       s954    t618 h h934 h944  B       b954    t953
2492  G       s954    t954  T       t954    o2 b948
2493  B       b954    s954  B       b955    t954
2494  T       t955    o925 b954 b931  T       t955    o938 b954 b4 b955
2495  B       b955    t955  B       b956    t955
2496  T       t956    o2 b947  T       t956    o2 b956
2497  B       b956    t956  B       b957    t956
2498  T       t957    o953 b955 b4 b956  T       t957    o948 b952 b4 b957
2499  B       b957    t957  B       b958    t957
2500  T       t958    o737 b953 b936  H       h958    v_1 t951
2501  H       h958    v_2 t958  S       s958    t620 h h948 h958
2502  S       s958    t618 h h934 h944 h958  G       s958    t926
2503  G       s958    t912  B       b959    s958
2504  B       b958    s958  T       t959    o939 b959 b945
2505  T       t959    o925 b958 b931  B       b960    t959
2506  B       b959    t959  T       t960    o938 b960 b4 b957
2507  T       t960    o924 b959 b4 b956  B       b961    t960
2508  B       b960    t960  T       t961    o b961 b4
2509  P       p960    String wf  B       b962    t961
2510  O       o960    tactic_arg p960  T       t962    o b958 b962
 B       b961    t936 v_2  
 T       t961    o710 b961  
 S       s961    t618 h h934 h944  
 G       s961    t961  
 B       b962    s961  
 T       t962    o925 b962 b931  
2511  B       b963    t962  B       b963    t962
2512  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq  T       t963    o937 b948 b963
2513  O       o963    fun_prop  B       b964    t963
2514  P       p963    Var v_2  P       p964    String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2515  O       o964    var p963  O       o964    ext_rule p964
2516  T       t964    o964  T       t964    o937 b958 b4
2517  B       b964    t964  B       b965    t964
2518  T       t965    o737 b964 b936  T       t965    o964 b936 b965 b4 b4
2519  B       b965    t965 v_2  B       b966    t965
2520  T       t966    o963 b965  P       p966    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2521  S       s966    t618 h h934 h944  O       o966    ext_rule p966
2522  G       s966    t966  P       p967    String eq
2523  B       b966    s966  O       o967    tactic_arg p967
2524  T       t967    o925 b966 b931  T       t967    o559 b894 b561
2525  B       b967    t967  B       b967    t967
2526  NSummary!arg_named      arg_named       arg_named Summary  T       t968    o739 b949 b967
2527  P       p967    String d_auto  S       s968    t620 h h948 h958
2528  O       o967    arg_named p967  G       s968    t968
2529  NSummary!arg_bool       arg_bool        arg_bool Summary  B       b968    s968
2530  P       p968    String true  T       t969    o939 b968 b945
 O       o968    arg_bool p968  
 T       t968    o968  
 B       b968    t968  
 T       t969    o967 b968  
2531  B       b969    t969  B       b969    t969
2532  T       t970    o b969 b4  T       t970    o2 b961
2533  B       b970    t970  B       b970    t970
2534  T       t971    o960 b967 b970 b956  T       t971    o967 b969 b4 b970
2535  B       b971    t971  B       b971    t971
2536  T       t972    o2 b971  T       t972    o739 b967 b950
2537  B       b972    t972  H       h972    v_2 t972
2538  T       t973    o960 b963 b4 b972  S       s972    t620 h h948 h958 h972
2539    G       s972    t926
2540    B       b972    s972
2541    T       t973    o939 b972 b945
2542  B       b973    t973  B       b973    t973
2543  T       t974    o b973 b4  T       t974    o938 b973 b4 b970
2544  B       b974    t974  B       b974    t974
2545  T       t975    o b960 b974  P       p974    String wf
2546  B       b975    t975  O       o974    tactic_arg p974
2547  T       t976    o b957 b975  B       b975    t950 v_2
2548  B       b976    t976  T       t975    o712 b975
2549  T       t977    o923 b947 b976  S       s975    t620 h h948 h958
2550  B       b977    t977  G       s975    t975
2551  P       p977    String autoT  B       b976    s975
2552  O       o977    ext_rule p977  T       t976    o939 b976 b945
2553  T       t978    o923 b957 b4  B       b977    t976
2554    NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq
2555    O       o977    fun_prop
2556    P       p977    Var v_2
2557    O       o978    var p977
2558    T       t978    o978
2559  B       b978    t978  B       b978    t978
2560  T       t979    o977 b922 b978 b4 b4  T       t979    o739 b978 b950
2561  B       b979    t979  B       b979    t979 v_2
2562  P       p979    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"  T       t980    o977 b979
2563  O       o979    ext_rule p979  S       s980    t620 h h948 h958
2564  T       t980    o557 b880 b672  G       s980    t980
2565  B       b980    t980  B       b980    s980
2566  T       t981    o737 b936 b980  T       t981    o939 b980 b945
2567  S       s981    t618 h h934 h944 h958  B       b981    t981
2568  G       s981    t981  NSummary!arg_named      arg_named       arg_named Summary
2569  B       b981    s981  P       p981    String d_auto
2570  T       t982    o925 b981 b931  O       o981    arg_named p981
2571    NSummary!arg_bool       arg_bool        arg_bool Summary
2572    P       p982    String true
2573    O       o982    arg_bool p982
2574    T       t982    o982
2575  B       b982    t982  B       b982    t982
2576  T       t983    o2 b960  T       t983    o981 b982
2577  B       b983    t983  B       b983    t983
2578  T       t984    o953 b982 b4 b983  T       t984    o b983 b4
2579  B       b984    t984  B       b984    t984
2580  T       t985    o737 b953 b980  T       t985    o974 b981 b984 b970
2581  H       h985    v_3 t985  B       b985    t985
2582  S       s985    t618 h h934 h944 h958 h985  T       t986    o2 b985
 G       s985    t912  
 B       b985    s985  
 T       t986    o925 b985 b931  
2583  B       b986    t986  B       b986    t986
2584  T       t987    o924 b986 b4 b983  T       t987    o974 b977 b4 b986
2585  B       b987    t987  B       b987    t987
2586  B       b988    t953 v_3  T       t988    o b987 b4
2587  T       t988    o710 b988  B       b988    t988
2588  S       s988    t618 h h934 h944 h958  T       t989    o b974 b988
2589  G       s988    t988  B       b989    t989
2590  B       b989    s988  T       t990    o b971 b989
2591  T       t989    o925 b989 b931  B       b990    t990
2592  B       b990    t989  T       t991    o937 b961 b990
2593  P       p990    Var v_3  B       b991    t991
2594  O       o990    var p990  P       p991    String autoT
2595  T       t990    o990  O       o991    ext_rule p991
2596  B       b991    t990  T       t992    o937 b971 b4
2597  T       t991    o737 b953 b991  B       b992    t992
2598  B       b992    t991 v_3  T       t993    o991 b936 b992 b4 b4
2599  T       t992    o963 b992  B       b993    t993
2600  S       s992    t618 h h934 h944 h958  P       p993    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2601  G       s992    t992  O       o993    ext_rule p993
2602  B       b993    s992  T       t994    o559 b894 b674
2603  T       t993    o925 b993 b931  B       b994    t994
2604  B       b994    t993  T       t995    o739 b950 b994
2605  T       t994    o960 b994 b970 b983  S       s995    t620 h h948 h958 h972
2606  B       b995    t994  G       s995    t995
2607  T       t995    o2 b995  B       b995    s995
2608  B       b996    t995  T       t996    o939 b995 b945
2609  T       t996    o960 b990 b4 b996  B       b996    t996
2610  B       b997    t996  T       t997    o2 b974
2611  T       t997    o b997 b4  B       b997    t997
2612  B       b998    t997  T       t998    o967 b996 b4 b997
2613  T       t998    o b987 b998  B       b998    t998
2614  B       b999    t998  T       t999    o739 b967 b994
2615  T       t999    o b984 b999  H       h999    v_3 t999
2616  B       b1000   t999  S       s999    t620 h h948 h958 h972 h999
2617  T       t1000   o923 b960 b1000  G       s999    t926
2618  B       b1001   t1000  B       b999    s999
2619  T       t1001   o923 b984 b4  T       t1000   o939 b999 b945
2620  B       b1002   t1001  B       b1000   t1000
2621  T       t1002   o977 b922 b1002 b4 b4  T       t1001   o938 b1000 b4 b997
2622  B       b1003   t1002  B       b1001   t1001
2623  P       p1003   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"  B       b1002   t967 v_3
2624  O       o1003   ext_rule p1003  T       t1002   o712 b1002
2625  T       t1003   o557 b565 b559  S       s1002   t620 h h948 h958 h972
2626    G       s1002   t1002
2627    B       b1003   s1002
2628    T       t1003   o939 b1003 b945
2629  B       b1004   t1003  B       b1004   t1003
2630  T       t1004   o557 b565 b672  P       p1004   Var v_3
2631    O       o1004   var p1004
2632    T       t1004   o1004
2633  B       b1005   t1004  B       b1005   t1004
2634  T       t1005   o737 b1004 b1005  T       t1005   o739 b967 b1005
2635  H       h1005   v_4 t1005  B       b1006   t1005 v_3
2636  S       s1005   t618 h h934 h944 h958 h985 h1005  T       t1006   o977 b1006
2637  G       s1005   t912  S       s1006   t620 h h948 h958 h972
2638  B       b1006   s1005  G       s1006   t1006
2639  T       t1006   o925 b1006 b931  B       b1007   s1006
2640  B       b1007   t1006  T       t1007   o939 b1007 b945
 T       t1007   o2 b987  
2641  B       b1008   t1007  B       b1008   t1007
2642  T       t1008   o924 b1007 b4 b1008  T       t1008   o974 b1008 b984 b997
2643  B       b1009   t1008  B       b1009   t1008
2644  T       t1009   o b1009 b4  T       t1009   o2 b1009
2645  B       b1010   t1009  B       b1010   t1009
2646  T       t1010   o923 b987 b1010  T       t1010   o974 b1004 b4 b1010
2647  B       b1011   t1010  B       b1011   t1010
2648  P       p1011   String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"  T       t1011   o b1011 b4
2649  O       o1011   ext_rule p1011  B       b1012   t1011
2650  T       t1011   o737 b559 b1005  T       t1012   o b1001 b1012
 H       h1011   v_5 t1011  
 S       s1011   t618 h h934 h944 h958 h985 h1005 h1011  
 G       s1011   t912  
 B       b1012   s1011  
 T       t1012   o925 b1012 b931  
2651  B       b1013   t1012  B       b1013   t1012
2652  T       t1013   o2 b1009  T       t1013   o b998 b1013
2653  B       b1014   t1013  B       b1014   t1013
2654  T       t1014   o924 b1013 b4 b1014  T       t1014   o937 b974 b1014
2655  B       b1015   t1014  B       b1015   t1014
2656  B       b1016   t1004 v_5  T       t1015   o937 b998 b4
2657  T       t1016   o710 b1016  B       b1016   t1015
2658  S       s1016   t618 h h934 h944 h958 h985 h1005  T       t1016   o991 b936 b1016 b4 b4
2659  G       s1016   t1016  B       b1017   t1016
2660  B       b1017   s1016  P       p1017   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2661  T       t1017   o925 b1017 b931  O       o1017   ext_rule p1017
2662    T       t1017   o559 b567 b561
2663  B       b1018   t1017  B       b1018   t1017
2664  P       p1018   Var v_5  T       t1018   o559 b567 b674
 O       o1018   var p1018  
 T       t1018   o1018  
2665  B       b1019   t1018  B       b1019   t1018
2666  T       t1019   o737 b1019 b1005  T       t1019   o739 b1018 b1019
2667  B       b1020   t1019 v_5  H       h1019   v_4 t1019
2668  T       t1020   o963 b1020  S       s1019   t620 h h948 h958 h972 h999 h1019
2669  S       s1020   t618 h h934 h944 h958 h985 h1005  G       s1019   t926
2670  G       s1020   t1020  B       b1020   s1019
2671  B       b1021   s1020  T       t1020   o939 b1020 b945
2672  T       t1021   o925 b1021 b931  B       b1021   t1020
2673    T       t1021   o2 b1001
2674  B       b1022   t1021  B       b1022   t1021
2675  T       t1022   o960 b1022 b970 b1014  T       t1022   o938 b1021 b4 b1022
2676  B       b1023   t1022  B       b1023   t1022
2677  T       t1023   o2 b1023  T       t1023   o b1023 b4
2678  B       b1024   t1023  B       b1024   t1023
2679  T       t1024   o960 b1018 b4 b1024  T       t1024   o937 b1001 b1024
2680  B       b1025   t1024  B       b1025   t1024
2681  T       t1025   o b1025 b4  P       p1025   String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2682  B       b1026   t1025  O       o1025   ext_rule p1025
2683  T       t1026   o b1015 b1026  T       t1025   o739 b561 b1019
2684    H       h1025   v_5 t1025
2685    S       s1025   t620 h h948 h958 h972 h999 h1019 h1025
2686    G       s1025   t926
2687    B       b1026   s1025
2688    T       t1026   o939 b1026 b945
2689  B       b1027   t1026  B       b1027   t1026
2690  T       t1027   o923 b1009 b1027  T       t1027   o2 b1023
2691  B       b1028   t1027  B       b1028   t1027
2692  P       p1028   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"  T       t1028   o938 b1027 b4 b1028
2693  O       o1028   ext_rule p1028  B       b1029   t1028
2694  H       h1028   v_6 t912  B       b1030   t1018 v_5
2695  S       s1028   t618 h h934 h944 h958 h985 h1005 h1011 h1028  T       t1030   o712 b1030
2696  G       s1028   t912  S       s1030   t620 h h948 h958 h972 h999 h1019
2697  B       b1029   s1028  G       s1030   t1030
2698  T       t1029   o925 b1029 b931  B       b1031   s1030
2699  B       b1030   t1029  T       t1031   o939 b1031 b945
 T       t1030   o2 b1015  
 B       b1031   t1030  
 T       t1031   o924 b1030 b4 b1031  
2700  B       b1032   t1031  B       b1032   t1031
2701  T       t1032   o b1032 b4  P       p1032   Var v_5
2702    O       o1032   var p1032
2703    T       t1032   o1032
2704  B       b1033   t1032  B       b1033   t1032
2705  T       t1033   o923 b1015 b1033  T       t1033   o739 b1033 b1019
2706  B       b1034   t1033  B       b1034   t1033 v_5
2707  P       p1034   String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"  T       t1034   o977 b1034
2708  O       o1034   ext_rule p1034  S       s1034   t620 h h948 h958 h972 h999 h1019
2709  T       t1034   o923 b1032 b4  G       s1034   t1034
2710  B       b1035   t1034  B       b1035   s1034
2711  T       t1035   o1034 b922 b1035 b4 b4  T       t1035   o939 b1035 b945
2712  B       b1036   t1035  B       b1036   t1035
2713  T       t1036   o b1036 b4  T       t1036   o974 b1036 b984 b1028
2714  B       b1037   t1036  B       b1037   t1036
2715  T       t1037   o1028 b922 b1034 b1037 b4  T       t1037   o2 b1037
2716  B       b1038   t1037  B       b1038   t1037
2717  P       p1038   String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"  T       t1038   o974 b1032 b4 b1038
 O       o1038   ext_rule p1038  
 T       t1038   o923 b1025 b4  
2718  B       b1039   t1038  B       b1039   t1038
2719  T       t1039   o1038 b922 b1039 b4 b4  T       t1039   o b1039 b4
2720  B       b1040   t1039  B       b1040   t1039
2721  T       t1040   o b1040 b4  T       t1040   o b1029 b1040
2722  B       b1041   t1040  B       b1041   t1040
2723  T       t1041   o b1038 b1041  T       t1041   o937 b1023 b1041
2724  B       b1042   t1041  B       b1042   t1041
2725  T       t1042   o1011 b922 b1028 b1042 b4  P       p1042   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2726  B       b1043   t1042  O       o1042   ext_rule p1042
2727  T       t1043   o b1043 b4  H       h1042   v_6 t926
2728    S       s1042   t620 h h948 h958 h972 h999 h1019 h1025 h1042
2729    G       s1042   t926
2730    B       b1043   s1042
2731    T       t1043   o939 b1043 b945
2732  B       b1044   t1043  B       b1044   t1043
2733  T       t1044   o1003 b922 b1011 b1044 b4  T       t1044   o2 b1029
2734  B       b1045   t1044  B       b1045   t1044
2735  T       t1045   o923 b997 b4  T       t1045   o938 b1044 b4 b1045
2736  B       b1046   t1045  B       b1046   t1045
2737  T       t1046   o1038 b922 b1046 b4 b4  T       t1046   o b1046 b4
2738  B       b1047   t1046  B       b1047   t1046
2739  T       t1047   o b1047 b4  T       t1047   o937 b1029 b1047
2740  B       b1048   t1047  B       b1048   t1047
2741  T       t1048   o b1045 b1048  P       p1048   String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2742    O       o1048   ext_rule p1048
2743    T       t1048   o937 b1046 b4
2744  B       b1049   t1048  B       b1049   t1048
2745  T       t1049   o b1003 b1049  T       t1049   o1048 b936 b1049 b4 b4
2746  B       b1050   t1049  B       b1050   t1049
2747  T       t1050   o979 b922 b1001 b1050 b4  T       t1050   o b1050 b4
2748  B       b1051   t1050  B       b1051   t1050
2749  T       t1051   o923 b973 b4  P       p1051   String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2750  B       b1052   t1051  O       o1051   ext_rule p1051
2751  T       t1052   o1038 b922 b1052 b4 b4  B       b1052   t1017 v_6
2752  B       b1053   t1052  T       t1052   o712 b1052
2753  T       t1053   o b1053 b4  S       s1052   t620 h h948 h958 h972 h999 h1019 h1025
2754    G       s1052   t1052
2755    B       b1053   s1052
2756    T       t1053   o939 b1053 b945
2757  B       b1054   t1053  B       b1054   t1053
2758  T       t1054   o b1051 b1054  P       p1054   Var v_6
2759    O       o1054   var p1054
2760    T       t1054   o1054
2761  B       b1055   t1054  B       b1055   t1054
2762  T       t1055   o b979 b1055  T       t1055   o739 b1018 b1055
2763  B       b1056   t1055  B       b1056   t1055 v_6
2764  T       t1056   o952 b922 b977 b1056 b4  T       t1056   o977 b1056
2765  B       b1057   t1056  S       s1056   t620 h h948 h958 h972 h999 h1019 h1025
2766  T       t1057   o b1057 b4  G       s1056   t1056
2767    B       b1057   s1056
2768    T       t1057   o939 b1057 b945
2769  B       b1058   t1057  B       b1058   t1057
2770  T       t1058   o b952 b1058  T       t1058   o974 b1058 b984 b1045
2771  B       b1059   t1058  B       b1059   t1058
2772  T       t1059   o921 b922 b950 b1059 b4  T       t1059   o2 b1059
2773  B       b1060   t1059  B       b1060   t1059
2774  T       t1060   o920 b1060  T       t1060   o974 b1054 b4 b1060
2775  B       b1061   t1060  B       b1061   t1060
2776  P       p1061   Number 4911  T       t1061   o937 b1061 b4
2777  P       p1062   Number 4919  B       b1062   t1061
2778  O       o1062   resource_defs p1061 p1062 p262  T       t1062   o1051 b936 b1062 b4 b4
2779  P       p1063   Number 4917  B       b1063   t1062
2780  O       o1063   uid p1063 p1062  T       t1063   o b1063 b4
2781  T       t1063   o1063 b624  B       b1064   t1063
2782  B       b1063   t1063  T       t1064   o1042 b936 b1048 b1051 b1064
2783  T       t1064   o b1063 b4  B       b1065   t1064
2784  B       b1064   t1064  T       t1065   o937 b1039 b4
2785  T       t1065   o1062 b1064  B       b1066   t1065
2786  B       b1065   t1065  T       t1066   o1051 b936 b1066 b4 b4
2787  T       t1066   o b1065 b4  B       b1067   t1066
2788  B       b1066   t1066  T       t1067   o b1067 b4
2789  T       t1067   o906 b909 b920 b1061 b1066  B       b1068   t1067
2790  B       b1067   t1067  T       t1068   o b1065 b1068
2791  T       t1068   o905 b1067  B       b1069   t1068
2792  B       b1068   t1068  T       t1069   o1025 b936 b1042 b1069 b4
2793  P       p1068   Number 5359  B       b1070   t1069
2794  P       p1069   Number 5789  T       t1070   o b1070 b4
2795  O       o1069   location p1068 p1069  B       b1071   t1070
2796  P       p1070   String cancelRight  T       t1071   o1017 b936 b1025 b1071 b4
2797  O       o1070   rule p1070  B       b1072   t1071
2798  T       t1070   o907 b672  P       p1072   String "rwh unfold_fun_set 0 thenT autoT"
2799  B       b1070   t1070  O       o1072   ext_rule p1072
2800  T       t1071   o b1070 b4  T       t1072   o937 b1011 b4
2801  B       b1071   t1071  B       b1073   t1072
2802  T       t1072   o b615 b1071  T       t1073   o1072 b936 b1073 b4 b4
2803  B       b1072   t1072  B       b1074   t1073
2804  T       t1073   o737 b693 b694  T       t1074   o b1074 b4
2805  S       s1073   t618 h  B       b1075   t1074
2806  G       s1073   t1073  T       t1075   o b1072 b1075
2807  B       b1073   s1073  B       b1076   t1075
2808  T       t1074   o616 b1073  T       t1076   o b1017 b1076
2809  B       b1074   t1074  B       b1077   t1076
2810  T       t1075   o737 b558 b559  T       t1077   o993 b936 b1015 b1077 b4
2811  S       s1075   t618 h  B       b1078   t1077
2812  G       s1075   t1075  T       t1078   o937 b987 b4
2813  B       b1075   s1075  B       b1079   t1078
2814  T       t1076   o616 b1075  T       t1079   o1072 b936 b1079 b4 b4
2815  B       b1076   t1076  B       b1080   t1079
2816  T       t1077   o633 b1074 b1076  T       t1080   o b1080 b4
2817  B       b1077   t1077  B       b1081   t1080
2818  T       t1078   o633 b737 b1077  T       t1081   o b1078 b1081
2819  B       b1078   t1078  B       b1082   t1081
2820  T       t1079   o633 b656 b1078  T       t1082   o b993 b1082
2821  B       b1079   t1079  B       b1083   t1082
2822  T       t1080   o633 b654 b1079  T       t1083   o966 b936 b991 b1083 b4
2823  B       b1080   t1080  B       b1084   t1083
2824  T       t1081   o633 b674 b1080  T       t1084   o b1084 b4
2825  B       b1081   t1081  B       b1085   t1084
2826  T       t1082   o633 b639 b1081  T       t1085   o b966 b1085
2827  B       b1082   t1082  B       b1086   t1085
2828  T       t1083   o633 b637 b1082  NSummary!ext_goal       ext_goal        ext_goal Summary
2829  B       b1083   t1083  O       o1086   ext_goal
2830  P       p1083   String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenWT autoT"  S       s1086   t620 h
2831  O       o1083   ext_rule p1083  G       s1086   t951
2832  T       t1084   o b1073 b4  B       b1087   s1086
2833  B       b1084   t1084  T       t1087   o939 b1087 b945
2834  T       t1085   o b736 b1084  B       b1088   t1087
2835  B       b1085   t1085  T       t1088   o948 b1088 b4 b955
2836  T       t1086   o b655 b1085  B       b1089   t1088
2837  B       b1086   t1086  T       t1089   o1086 b1089
2838  T       t1087   o b653 b1086  B       b1090   t1089
2839  B       b1087   t1087  T       t1090   o b1090 b4
2840  T       t1088   o b673 b1087  B       b1091   t1090
2841  B       b1088   t1088  T       t1091   o964 b936 b1090 b1091 b4
2842  T       t1089   o b638 b1088  B       b1092   t1091
2843  B       b1089   t1089  P       p1092   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2844  T       t1090   o b636 b1089  O       o1092   ext_rule p1092
2845  B       b1090   t1090  H       h1092   v t951
2846  T       t1091   o925 b1075 b1090  S       s1092   t620 h h1092
2847  B       b1091   t1091  G       s1092   t926
2848  T       t1092   o924 b1091 b4 b933  B       b1093   s1092
2849  B       b1092   t1092  T       t1093   o939 b1093 b945
2850  H       h1092   v t1073  B       b1094   t1093
2851  T       t1093   o570 b672  T       t1094   o938 b1094 b4 b955
2852  B       b1093   t1093  B       b1095   t1094
2853  T       t1094   o557 b693 b1093  T       t1095   o1086 b1095
2854  B       b1094   t1094  B       b1096   t1095
2855  T       t1095   o557 b694 b1093  P       p1096   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2856  B       b1095   t1095  O       o1096   ext_rule p1096
2857  T       t1096   o737 b1094 b1095  P       p1097   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2858  S       s1096   t618 h h1092  O       o1097   ext_rule p1097
2859  G       s1096   t1096  T       t1097   o b1096 b4
 B       b1096   s1096  
 T       t1097   o925 b1096 b1090  
2860  B       b1097   t1097  B       b1097   t1097
2861  S       s1097   t618 h h1092  H       h1097   x t924
2862  G       s1097   t1075  H       h1098   v_1 t972
2863  B       b1098   s1097  H       h1099   v_2 t999
2864  T       t1098   o925 b1098 b1090  H       h1100   v_3 t1019
2865  B       b1099   t1098  H       h1101   v_4 t1025
2866  T       t1099   o2 b1092  B       b1101   t1017 v_5
2867  B       b1100   t1099  T       t1101   o712 b1101
2868  T       t1100   o924 b1099 b4 b1100  S       s1101   t620 h h1097 h1092 h1098 h1099 h1100 h1101
2869  B       b1101   t1100  G       s1101   t1101
2870  T       t1101   o2 b1101  B       b1102   s1101
2871  B       b1102   t1101  T       t1102   o b738 b4
 T       t1102   o934 b1097 b4 b1102  
2872  B       b1103   t1102  B       b1103   t1102
2873  H       h1103   v_1 t1096  T       t1103   o b657 b1103
2874  S       s1103   t618 h h1092 h1103  B       b1104   t1103
2875  G       s1103   t1075  T       t1104   o b655 b1104
 B       b1104   s1103  
 T       t1104   o925 b1104 b1090  
2876  B       b1105   t1104  B       b1105   t1104
2877  T       t1105   o924 b1105 b4 b1102  T       t1105   o b675 b1105
2878  B       b1106   t1105  B       b1106   t1105
2879  T       t1106   o b1106 b4  T       t1106   o b640 b1106
2880  B       b1107   t1106  B       b1107   t1106
2881  T       t1107   o b1103 b1107  T       t1107   o b638 b1107
2882  B       b1108   t1107  B       b1108   t1107
2883  T       t1108   o923 b1092 b1108  T       t1108   o939 b1102 b1108
2884  B       b1109   t1108  B       b1109   t1108
2885  T       t1109   o923 b1103 b4  T       t1109   o739 b1018 b1033
2886  B       b1110   t1109  B       b1110   t1109 v_5
2887  T       t1110   o950 b922 b1110 b4 b4  T       t1110   o977 b1110
2888  B       b1111   t1110  S       s1110   t620 h h1097 h1092 h1098 h1099 h1100 h1101
2889  P       p1111   String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"  G       s1110   t1110
2890  O       o1111   ext_rule p1111  B       b1111   s1110
2891  T       t1111   o557 b672 b1093  T       t1111   o939 b1111 b1108
2892  B       b1112   t1111  B       b1112   t1111
2893  T       t1112   o557 b558 b1112  S       s1112   t620 h h1097 h1092 h1098 h1099 h1100 h1101
2894  B       b1113   t1112  G       s1112   t926
2895  T       t1113   o737 b1113 b1095  B       b1113   s1112
2896  H       h1113   v_2 t1113  T       t1113   o939 b1113 b1108
2897  S       s1113   t618 h h1092 h1103 h1113  B       b1114   t1113
2898  G       s1113   t1075  S       s1114   t620 h h1097 h1092 h1098 h1099 h1100
2899  B       b1114   s1113  G       s1114   t926
2900  T       t1114   o925 b1114 b1090  B       b1115   s1114
2901  B       b1115   t1114  T       t1115   o939 b1115 b1108
 T       t1115   o2 b1106  
2902  B       b1116   t1115  B       b1116   t1115
2903  T       t1116   o924 b1115 b4 b1116  S       s1116   t620 h h1097 h1092 h1098 h1099
2904  B       b1117   t1116  G       s1116   t926
2905  B       b1118   t1095 v_2  B       b1117   s1116
2906  T       t1118   o710 b1118  T       t1117   o939 b1117 b1108
2907  S       s1118   t618 h h1092 h1103  B       b1118   t1117
2908  G       s1118   t1118  S       s1118   t620 h h1097 h1092 h1098
2909    G       s1118   t926
2910  B       b1119   s1118  B       b1119   s1118
2911  T       t1119   o925 b1119 b1090  T       t1119   o939 b1119 b1108
2912  B       b1120   t1119  B       b1120   t1119
2913  T       t1120   o737 b964 b1095  S       s1120   t620 h h1097 h1092
2914  B       b1121   t1120 v_2  G       s1120   t926
2915  T       t1121   o963 b1121  B       b1121   s1120
2916  S       s1121   t618 h h1092 h1103  T       t1121   o939 b1121 b1108
2917  G       s1121   t1121  B       b1122   t1121
2918  B       b1122   s1121  S       s1122   t620 h h1097
2919  T       t1122   o925 b1122 b1090  G       s1122   t926
2920  B       b1123   t1122  B       b1123   s1122
2921  T       t1123   o960 b1123 b970 b1116  T       t1123   o939 b1123 b1108
2922  B       b1124   t1123  B       b1124   t1123
2923  T       t1124   o2 b1124  T       t1124   o938 b1124 b4 b947
2924  B       b1125   t1124  B       b1125   t1124
2925  T       t1125   o960 b1120 b4 b1125  T       t1125   o2 b1125
2926  B       b1126   t1125  B       b1126   t1125
2927  T       t1126   o b1126 b4  T       t1126   o938 b1122 b4 b1126
2928  B       b1127   t1126  B       b1127   t1126
2929  T       t1127   o b1117 b1127  T       t1127   o2 b1127
2930  B       b1128   t1127  B       b1128   t1127
2931  T       t1128   o923 b1106 b1128  T       t1128   o938 b1120 b4 b1128
2932  B       b1129   t1128  B       b1129   t1128
2933  P       p1129   String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"  T       t1129   o2 b1129
 O       o1129   ext_rule p1129  
 T       t1129   o557 b559 b1112  
2934  B       b1130   t1129  B       b1130   t1129
2935  T       t1130   o737 b1113 b1130  T       t1130   o938 b1118 b4 b1130
2936  H       h1130   v_3 t1130  B       b1131   t1130
2937  S       s1130   t618 h h1092 h1103 h1113 h1130  T       t1131   o2 b1131
 G       s1130   t1075  
 B       b1131   s1130  
 T       t1131   o925 b1131 b1090  
2938  B       b1132   t1131  B       b1132   t1131
2939  T       t1132   o2 b1117  T       t1132   o938 b1116 b4 b1132
2940  B       b1133   t1132  B       b1133   t1132
2941  T       t1133   o924 b1132 b4 b1133  T       t1133   o2 b1133
2942  B       b1134   t1133  B       b1134   t1133
2943  B       b1135   t1112 v_3  T       t1134   o938 b1114 b4 b1134
2944  T       t1135   o710 b1135  B       b1135   t1134
2945  S       s1135   t618 h h1092 h1103 h1113  T       t1135   o2 b1135
2946  G       s1135   t1135  B       b1136   t1135
2947  B       b1136   s1135  T       t1136   o974 b1112 b984 b1136
 T       t1136   o925 b1136 b1090  
2948  B       b1137   t1136  B       b1137   t1136
2949  T       t1137   o737 b1113 b991  T       t1137   o2 b1137
2950  B       b1138   t1137 v_3  B       b1138   t1137
2951  T       t1138   o963 b1138  T       t1138   o974 b1109 b4 b1138
2952  S       s1138   t618 h h1092 h1103 h1113  B       b1139   t1138
2953  G       s1138   t1138  T       t1139   o937 b1139 b4
 B       b1139   s1138  
 T       t1139   o925 b1139 b1090  
2954  B       b1140   t1139  B       b1140   t1139
2955  T       t1140   o960 b1140 b970 b1133  T       t1140   o1051 b936 b1140 b4 b4
2956  B       b1141   t1140  B       b1141   t1140
2957  T       t1141   o2 b1141  T       t1141   o b1141 b4
2958  B       b1142   t1141  B       b1142   t1141
2959  T       t1142   o960 b1137 b4 b1142  T       t1142   o1097 b936 b1096 b1097 b1142
2960  B       b1143   t1142  B       b1143   t1142
2961  T       t1143   o b1143 b4  T       t1143   o b1143 b4
2962  B       b1144   t1143  B       b1144   t1143
2963  T       t1144   o b1134 b1144  B       b1145   t1018 v_4
2964  B       b1145   t1144  T       t1145   o712 b1145
2965  T       t1145   o923 b1117 b1145  S       s1145   t620 h h1097 h1092 h1098 h1099 h1100
2966  B       b1146   t1145  G       s1145   t1145
2967  P       p1146   String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"  B       b1146   s1145
2968  O       o1146   ext_rule p1146  T       t1146   o939 b1146 b1108
 T       t1146   o557 b558 b565  
2969  B       b1147   t1146  B       b1147   t1146
2970  T       t1147   o557 b559 b565  P       p1147   Var v_4
2971    O       o1147   var p1147
2972    T       t1147   o1147
2973  B       b1148   t1147  B       b1148   t1147
2974  T       t1148   o737 b1147 b1148  T       t1148   o739 b1148 b1019
2975  H       h1148   v_4 t1148  B       b1149   t1148 v_4
2976  S       s1148   t618 h h1092 h1103 h1113 h1130 h1148  T       t1149   o977 b1149
2977  G       s1148   t1075  S       s1149   t620 h h1097 h1092 h1098 h1099 h1100
2978  B       b1149   s1148  G       s1149   t1149
2979  T       t1149   o925 b1149 b1090  B       b1150   s1149
2980  B       b1150   t1149  T       t1150   o939 b1150 b1108
 T       t1150   o2 b1134  
2981  B       b1151   t1150  B       b1151   t1150
2982  T       t1151   o924 b1150 b4 b1151  T       t1151   o974 b1151 b984 b1134
2983  B       b1152   t1151  B       b1152   t1151
2984  T       t1152   o b1152 b4  T       t1152   o2 b1152
2985  B       b1153   t1152  B       b1153   t1152
2986  T       t1153   o923 b1134 b1153  T       t1153   o974 b1147 b4 b1153
2987  B       b1154   t1153  B       b1154   t1153
2988  P       p1154   String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"  T       t1154   o937 b1154 b4
2989  O       o1154   ext_rule p1154  B       b1155   t1154
2990  T       t1154   o737 b558 b1148  T       t1155   o1051 b936 b1155 b4 b4
 H       h1154   v_5 t1154  
 S       s1154   t618 h h1092 h1103 h1113 h1130 h1148 h1154  
 G       s1154   t1075  
 B       b1155   s1154  
 T       t1155   o925 b1155 b1090  
2991  B       b1156   t1155  B       b1156   t1155
2992  T       t1156   o2 b1152  T       t1156   o b1156 b4
2993  B       b1157   t1156  B       b1157   t1156
2994  T       t1157   o924 b1156 b4 b1157  T       t1157   o1025 b936 b1096 b1144 b1157
2995  B       b1158   t1157  B       b1158   t1157
2996  B       b1159   t1147 v_5  T       t1158   o b1158 b4
2997  T       t1159   o710 b1159  B       b1159   t1158
2998  S       s1159   t618 h h1092 h1103 h1113 h1130 h1148  T       t1159   o1017 b936 b1096 b1159 b4
2999  G       s1159   t1159  B       b1160   t1159
3000  B       b1160   s1159  T       t1160   o b1160 b4
 T       t1160   o925 b1160 b1090  
3001  B       b1161   t1160  B       b1161   t1160
3002  T       t1161   o737 b1019 b1148  S       s1161   t620 h h1097 h1092 h1098
3003  B       b1162   t1161 v_5  G       s1161   t995
3004  T       t1162   o963 b1162  B       b1162   s1161
3005  S       s1162   t618 h h1092 h1103 h1113 h1130 h1148  T       t1162   o939 b1162 b1108
3006  G       s1162   t1162  B       b1163   t1162
3007  B       b1163   s1162  T       t1163   o967 b1163 b4 b1130
 T       t1163   o925 b1163 b1090  
3008  B       b1164   t1163  B       b1164   t1163
3009  T       t1164   o960 b1164 b970 b1157  T       t1164   o937 b1164 b4
3010  B       b1165   t1164  B       b1165   t1164
3011  T       t1165   o2 b1165  T       t1165   o991 b936 b1165 b4 b4
3012  B       b1166   t1165  B       b1166   t1165
3013  T       t1166   o960 b1161 b4 b1166  P       p1166   String "rwh unfold_fun_prop 0 thenT autoT"
3014  B       b1167   t1166  O       o1166   ext_rule p1166
3015  T       t1167   o b1167 b4  T       t1166   o739 b967 b978
3016  B       b1168   t1167  B       b1167   t1166 v_2
3017  T       t1168   o b1158 b1168  T       t1167   o977 b1167
3018    S       s1167   t620 h h1097 h1092 h1098
3019    G       s1167   t1167
3020    B       b1168   s1167
3021    T       t1168   o939 b1168 b1108
3022  B       b1169   t1168  B       b1169   t1168
3023  T       t1169   o923 b1152 b1169  T       t1169   o974 b1169 b4 b1130
3024  B       b1170   t1169  B       b1170   t1169
3025  P       p1170   String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"  NCzf_itt_set!set        set     set Czf_itt_set
3026  O       o1170   ext_rule p1170  O       o1170   set
3027  T       t1170   o923 b1158 b4  T       t1170   o1170
3028  B       b1171   t1170  H       h1170   s1_1 t1170
3029  T       t1171   o1170 b922 b1171 b4 b4  H       h1171   s2_1 t1170
3030  B       b1172   t1171  P       p1171   Var s1_1
3031  P       p1172   String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"  O       o1171   var p1171
3032  O       o1172   ext_rule p1172  T       t1171   o1171
3033  T       t1172   o923 b1167 b4  B       b1171   t1171
3034  B       b1173   t1172  P       p1172   Var s2_1
3035  T       t1173   o1172 b922 b1173 b4 b4  O       o1172   var p1172
3036  B       b1174   t1173  T       t1172   o1172
3037  T       t1174   o b1174 b4  B       b1172   t1172
3038  B       b1175   t1174  T       t1173   o739 b1171 b1172
3039  T       t1175   o b1172 b1175  H       h1173   x_1 t1173
3040  B       b1176   t1175  T       t1174   o739 b967 b1171
3041  T       t1176   o1154 b922 b1170 b1176 b4  H       h1174   x_2 t1174
3042  B       b1177   t1176  T       t1175   o676 b967 b1172
3043  T       t1177   o b1177 b4  S       s1175   t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174
3044  B       b1178   t1177  G       s1175   t1175
3045  T       t1178   o1146 b922 b1154 b1178 b4  B       b1175   s1175
3046  B       b1179   t1178  T       t1176   o939 b1175 b1108
3047  T       t1179   o923 b1143 b4  B       b1176   t1176
3048  B       b1180   t1179  T       t1177   o739 b967 b1172
3049  T       t1180   o1172 b922 b1180 b4 b4  S       s1177   t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174
3050  B       b1181   t1180  G       s1177   t1177
3051  T       t1181   o b1181 b4  B       b1177   s1177
3052    T       t1178   o939 b1177 b1108
3053    B       b1178   t1178
3054    NItt_logic      Itt_logic       Itt_logic NIL
3055    NItt_logic!implies      implies implies Itt_logic
3056    O       o1178   implies
3057    B       b1179   t1174
3058    B       b1180   t1177
3059    T       t1180   o1178 b1179 b1180
3060    S       s1180   t620 h h1097 h1092 h1098 h1170 h1171 h1173
3061    G       s1180   t1180
3062    B       b1181   s1180
3063    T       t1181   o939 b1181 b1108
3064  B       b1182   t1181  B       b1182   t1181
3065  T       t1182   o b1179 b1182  B       b1183   t1173
3066  B       b1183   t1182  B       b1184   t1180
3067  T       t1183   o1129 b922 b1146 b1183 b4  T       t1184   o1178 b1183 b1184
3068  B       b1184   t1183  S       s1184   t620 h h1097 h1092 h1098 h1170 h1171
3069  T       t1184   o923 b1126 b4  G       s1184   t1184
3070  B       b1185   t1184  B       b1185   s1184
3071  T       t1185   o1172 b922 b1185 b4 b4  T       t1185   o939 b1185 b1108
3072  B       b1186   t1185  B       b1186   t1185
3073  T       t1186   o b1186 b4  NItt_logic!all  all     all Itt_logic
3074  B       b1187   t1186  O       o1186   all
3075  T       t1187   o b1184 b1187  B       b1187   t1170
3076  B       b1188   t1187  B       b1188   t1184 s2_1
3077  S       s1188   t618 h h1092 h1103 h1113  T       t1188   o1186 b1187 b1188
3078  G       s1188   t675  S       s1188   t620 h h1097 h1092 h1098 h1170
3079    G       s1188   t1188
3080  B       b1189   s1188  B       b1189   s1188
3081  T       t1189   o925 b1189 b1090  T       t1189   o939 b1189 b1108
3082  B       b1190   t1189  B       b1190   t1189
3083  T       t1190   o924 b1115 b970 b1116  B       b1191   t1188 s1_1
3084  B       b1191   t1190  T       t1191   o1186 b1187 b1191
3085  T       t1191   o2 b1191  S       s1191   t620 h h1097 h1092 h1098
3086  B       b1192   t1191  G       s1191   t1191
3087  T       t1192   o924 b1190 b4 b1192  B       b1192   s1191
3088    T       t1192   o939 b1192 b1108
3089  B       b1193   t1192  B       b1193   t1192
3090  S       s1193   t618 h h1092 h1103 h1113 h1130  T       t1193   o2 b1170
3091  G       s1193   t675  B       b1194   t1193
3092  B       b1194   s1193  T       t1194   o974 b1193 b984 b1194
 T       t1194   o925 b1194 b1090  
3093  B       b1195   t1194  B       b1195   t1194
3094  T       t1195   o2 b1193  T       t1195   o2 b1195
3095  B       b1196   t1195  B       b1196   t1195
3096  T       t1196   o924 b1195 b4 b1196  T       t1196   o938 b1190 b984 b1196
3097  B       b1197   t1196  B       b1197   t1196
3098  T       t1197   o960 b1140 b970 b1196  T       t1197   o2 b1197
3099  B       b1198   t1197  B       b1198   t1197
3100  T       t1198   o2 b1198  T       t1198   o938 b1186 b984 b1198
3101  B       b1199   t1198  B       b1199   t1198
3102  T       t1199   o960 b1137 b4 b1199  T       t1199   o2 b1199
3103  B       b1200   t1199  B       b1200   t1199
3104  T       t1200   o b1200 b4  T       t1200   o938 b1182 b984 b1200
3105  B       b1201   t1200  B       b1201   t1200
3106  T       t1201   o b1197 b1201  T       t1201   o2 b1201
3107  B       b1202   t1201  B       b1202   t1201
3108  T       t1202   o923 b1193 b1202  T       t1202   o938 b1178 b984 b1202
3109  B       b1203   t1202  B       b1203   t1202
3110  S       s1203   t618 h h1092 h1103 h1113 h1130 h1148  T       t1203   o2 b1203
3111  G       s1203   t675  B       b1204   t1203
3112  B       b1204   s1203  T       t1204   o938 b1176 b4 b1204
 T       t1204   o925 b1204 b1090  
3113  B       b1205   t1204  B       b1205   t1204
3114  T       t1205   o2 b1197  T       t1205   o b1205 b4
3115  B       b1206   t1205  B       b1206   t1205
3116  T       t1206   o924 b1205 b4 b1206  T       t1206   o937 b1170 b1206
3117  B       b1207   t1206  B       b1207   t1206
3118  T       t1207   o b1207 b4  P       p1207   String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3119    O       o1207   ext_rule p1207
3120    T       t1207   o937 b1205 b4
3121  B       b1208   t1207  B       b1208   t1207
3122  T       t1208   o923 b1197 b1208  T       t1208   o1207 b936 b1208 b4 b4
3123  B       b1209   t1208  B       b1209   t1208
3124  S       s1209   t618 h h1092 h1103 h1113 h1130 h1148 h1154  T       t1209   o b1209 b4
3125  G       s1209   t675  B       b1210   t1209
3126  B       b1210   s1209  T       t1210   o1166 b936 b1207 b1210 b4
 T       t1210   o925 b1210 b1090  
3127  B       b1211   t1210  B       b1211   t1210
3128  T       t1211   o2 b1207  T       t1211   o b1211 b4
3129  B       b1212   t1211  B       b1212   t1211
3130  T       t1212   o924 b1211 b4 b1212  T       t1212   o b1166 b1212
3131  B       b1213   t1212  B       b1213   t1212
3132  T       t1213   o960 b1164 b970 b1212  T       t1213   o1096 b936 b1096 b1161 b1213
3133  B       b1214   t1213  B       b1214   t1213
3134  T       t1214   o2 b1214  T       t1214   o b1214 b4
3135  B       b1215   t1214  B       b1215   t1214
3136  T       t1215   o960 b1161 b4 b1215  S       s1215   t620 h h1097 h1092
3137  B       b1216   t1215  G       s1215   t968
3138  T       t1216   o b1216 b4  B       b1216   s1215
3139    T       t1216   o939 b1216 b1108
3140  B       b1217   t1216  B       b1217   t1216
3141  T       t1217   o b1213 b1217  T       t1217   o967 b1217 b4 b1128
3142  B       b1218   t1217  B       b1218   t1217
3143  T       t1218   o923 b1207 b1218  T       t1218   o937 b1218 b4
3144  B       b1219   t1218  B       b1219   t1218
3145  P       p1219   String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT thenT rwh unfold_equal 8 thenT autoT"  T       t1219   o991 b936 b1219 b4 b4
 O       o1219   ext_rule p1219  
 T       t1219   o923 b1213 b4  
3146  B       b1220   t1219  B       b1220   t1219
3147  T       t1220   o1219 b922 b1220 b4 b4  P       p1220   Var v_1
3148    O       o1220   var p1220
3149    T       t1220   o1220
3150  B       b1221   t1220  B       b1221   t1220
3151  T       t1221   o923 b1216 b4  T       t1221   o739 b1221 b950
3152  B       b1222   t1221  B       b1222   t1221 v_1
3153  T       t1222   o1038 b922 b1222 b4 b4  T       t1222   o977 b1222
3154  B       b1223   t1222  S       s1222   t620 h h1097 h1092
3155  T       t1223   o b1223 b4  G       s1222   t1222
3156    B       b1223   s1222
3157    T       t1223   o939 b1223 b1108
3158  B       b1224   t1223  B       b1224   t1223
3159  T       t1224   o b1221 b1224  T       t1224   o974 b1224 b4 b1128
3160  B       b1225   t1224  B       b1225   t1224
3161  T       t1225   o1154 b922 b1219 b1225 b4  H       h1225   s2 t1170
3162  B       b1226   t1225  T       t1225   o739 b1171 b561
3163  T       t1226   o b1226 b4  H       h1226   x_1 t1225
3164  B       b1227   t1226  T       t1226   o739 b1171 b950
3165  T       t1227   o1146 b922 b1209 b1227 b4  H       h1227   x_2 t1226
3166  B       b1228   t1227  T       t1227   o676 b561 b950
3167  P       p1228   String "rwh unfold_fun_set 0 thenT autoT"  S       s1227   t620 h h1097 h1092 h1170 h1225 h1226 h1227
3168  O       o1228   ext_rule p1228  G       s1227   t1227
3169  NCzf_itt_set!set        set     set Czf_itt_set  B       b1227   s1227
3170  O       o1229   set  T       t1228   o939 b1227 b1108
3171  T       t1229   o1229  B       b1228   t1228
3172  H       h1229   s1_1 t1229  T       t1229   o739 b561 b950
3173  H       h1230   s2 t1229  S       s1229   t620 h h1097 h1092 h1170 h1225 h1226 h1227
3174  P       p1230   Var s1_1  G       s1229   t1229
3175  O       o1230   var p1230  B       b1229   s1229
3176  T       t1230   o1230  T       t1230   o939 b1229 b1108
3177  B       b1230   t1230  B       b1230   t1230
3178  T       t1231   o737 b1230 b559  B       b1231   t1226
3179  H       h1231   x t1231  B       b1232   t1229
3180  T       t1232   o737 b1113 b1113  T       t1232   o1178 b1231 b1232
3181  S       s1232   t618 h h1092 h1103 h1113 h1229 h1230 h1231  S       s1232   t620 h h1097 h1092 h1170 h1225 h1226
3182  G       s1232   t1232  G       s1232   t1232
3183  B       b1232   s1232  B       b1233   s1232
3184  T       t1233   o925 b1232 b1090  T       t1233   o939 b1233 b1108
3185  B       b1233   t1233  B       b1234   t1233
3186  NItt_logic      Itt_logic       Itt_logic NIL  B       b1235   t1225
3187  NItt_logic!implies      implies implies Itt_logic  B       b1236   t1232
3188  O       o1233   implies  T       t1236   o1178 b1235 b1236
3189  B       b1234   t1231  S       s1236   t620 h h1097 h1092 h1170 h1225
3190  B       b1235   t1232  G       s1236   t1236
3191  T       t1235   o1233 b1234 b1235  B       b1237   s1236
3192  S       s1235   t618 h h1092 h1103 h1113 h1229 h1230  T       t1237   o939 b1237 b1108
3193  G       s1235   t1235  B       b1238   t1237
3194  B       b1236   s1235  B       b1239   t1236 s2
3195  T       t1236   o925 b1236 b1090  T       t1239   o1186 b1187 b1239
3196  B       b1237   t1236  S       s1239   t620 h h1097 h1092 h1170
 NItt_logic!all  all     all Itt_logic  
 O       o1237   all  
 B       b1238   t1229  
 B       b1239   t1235 s2  
 T       t1239   o1237 b1238 b1239  
 S       s1239   t618 h h1092 h1103 h1113 h1229  
3197  G       s1239   t1239  G       s1239   t1239
3198  B       b1240   s1239  B       b1240   s1239
3199  T       t1240   o925 b1240 b1090  T       t1240   o939 b1240 b1108
3200  B       b1241   t1240  B       b1241   t1240
3201  B       b1242   t1239 s1_1  B       b1242   t1239 s1_1
3202  T       t1242   o1237 b1238 b1242  T       t1242   o1186 b1187 b1242
3203  S       s1242   t618 h h1092 h1103 h1113  S       s1242   t620 h h1097 h1092
3204  G       s1242   t1242  G       s1242   t1242
3205  B       b1243   s1242  B       b1243   s1242
3206  T       t1243   o925 b1243 b1090  T       t1243   o939 b1243 b1108
3207  B       b1244   t1243  B       b1244   t1243
3208  T       t1244   o2 b1200  T       t1244   o2 b1225
3209  B       b1245   t1244  B       b1245   t1244
3210  T       t1245   o960 b1244 b970 b1245  T       t1245   o974 b1244 b984 b1245
3211  B       b1246   t1245  B       b1246   t1245
3212  T       t1246   o2 b1246  T       t1246   o2 b1246
3213  B       b1247   t1246  B       b1247   t1246
3214  T       t1247   o924 b1241 b970 b1247  T       t1247   o938 b1241 b984 b1247
3215  B       b1248   t1247  B       b1248   t1247
3216  T       t1248   o2 b1248  T       t1248   o2 b1248
3217  B       b1249   t1248  B       b1249   t1248
3218  T       t1249   o924 b1237 b970 b1249  T       t1249   o938 b1238 b984 b1249
3219  B       b1250   t1249  B       b1250   t1249
3220  T       t1250   o2 b1250  T       t1250   o2 b1250
3221  B       b1251   t1250  B       b1251   t1250
3222  T       t1251   o924 b1233 b4 b1251  T       t1251   o938 b1234 b984 b1251
3223  B       b1252   t1251  B       b1252   t1251
3224  T       t1252   o b1252 b4  T       t1252   o2 b1252
3225  B       b1253   t1252  B       b1253   t1252
3226  T       t1253   o923 b1200 b1253  T       t1253   o938 b1230 b984 b1253
3227  B       b1254   t1253  B       b1254   t1253
3228  NSummary!ext_goal       ext_goal        ext_goal Summary  T       t1254   o2 b1254
 O       o1254   ext_goal  
 T       t1254   o1254 b1252  
3229  B       b1255   t1254  B       b1255   t1254
3230  T       t1255   o b1255 b4  T       t1255   o938 b1228 b4 b1255
3231  B       b1256   t1255  B       b1256   t1255
3232  T       t1256   o1228 b922 b1254 b1256 b4  T       t1256   o b1256 b4
3233  B       b1257   t1256  B       b1257   t1256
3234  T       t1257   o b1257 b4  T       t1257   o937 b1225 b1257
3235  B       b1258   t1257  B       b1258   t1257
3236  T       t1258   o b1228 b1258  P       p1258   String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3237    O       o1258   ext_rule p1258
3238    T       t1258   o937 b1256 b4
3239  B       b1259   t1258  B       b1259   t1258
3240  T       t1259   o1129 b922 b1203 b1259 b4  T       t1259   o1258 b936 b1259 b4 b4
3241  B       b1260   t1259  B       b1260   t1259
3242  T       t1260   o b1260 b4  T       t1260   o b1260 b4
3243  B       b1261   t1260  B       b1261   t1260
3244  T       t1261   o1111 b922 b1129 b1188 b1261  T       t1261   o1166 b936 b1258 b1261 b4
3245  B       b1262   t1261  B       b1262   t1261
3246  T       t1262   o b1262 b4  T       t1262   o b1262 b4
3247  B       b1263   t1262  B       b1263   t1262
3248  T       t1263   o b1111 b1263  T       t1263   o b1220 b1263
3249  B       b1264   t1263  B       b1264   t1263
3250  T       t1264   o1083 b922 b1109 b1264 b4  T       t1264   o1092 b936 b1096 b1215 b1264
3251  B       b1265   t1264  B       b1265   t1264
3252  T       t1265   o920 b1265  P       p1265   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3253  B       b1266   t1265  O       o1265   ext_rule p1265
3254  P       p1266   Number 5386  H       h1265   y_1 t642
3255  P       p1267   Number 5394  T       t1265   o620 b695
3256  O       o1267   resource_defs p1266 p1267 p262  H       h1266   z_1 t1265
3257  P       p1268   Number 5392  T       t1266   o676 b562 b695
3258  O       o1268   uid p1268 p1267  H       h1267   z t1266
3259  T       t1268   o1268 b624  T       t1267   o676 b949 b950
3260  B       b1268   t1268  H       h1268   v t1267
3261  T       t1269   o b1268 b4  T       t1268   o676 b561 b674
3262    S       s1268   t620 h h1265 h1266 h1267 h1268
3263    G       s1268   t1268
3264    B       b1268   s1268
3265    T       t1269   o939 b1268 b1108
3266  B       b1269   t1269  B       b1269   t1269
3267  T       t1270   o1267 b1269  S       s1269   t620 h h1265 h1266 h1267 h1268
3268  B       b1270   t1270  G       s1269   t926
3269  T       t1271   o b1270 b4  B       b1270   s1269
3270  B       b1271   t1271  T       t1270   o939 b1270 b1108
3271  T       t1272   o1070 b1072 b1083 b1266 b1271  B       b1271   t1270
 B       b1272   t1272  
 T       t1273   o1069 b1272  
 B       b1273   t1273  
 P       p1273   Number 5791  
 P       p1274   Number 5863  
 O       o1274   location p1273 p1274  
 O       o1275   str_let p1273 p1274  
 P       p1275   Number 5795  
 O       o1276   patt_var p1275 p1274  
 O       o1277   patt_done p1273 p1274  
 T       t1277   o1277  
 B       b1277   t1277 groupCancelLeftT  
 T       t1278   o1276 b1277  
 B       b1278   t1278  
 O       o1278   fun p1275 p1274  
 O       o1279   patt_if p1275 p1274  
 P       p1279   Number 5812  
 P       p1280   Number 5813  
 O       o1280   patt_var p1279 p1280  
 O       o1281   patt_body p1275 p1274  
 P       p1281   Number 5814  
 P       p1282   Number 5815  
 O       o1282   patt_var p1281 p1282  
 P       p1283   Number 5821  
 O       o1283   apply p1283 p1274  
 P       p1284   Number 5861  
 O       o1284   apply p1283 p1284  
 P       p1285   Number 5859  
 O       o1285   apply p1283 p1285  
 P       p1286   Number 5831  
 O       o1286   lid p1283 p1286  
 O       o1287   lid p906  
 T       t1287   o1287  
 B       b1287   t1287  
 T       t1288   o1286 b1287  
 B       b1288   t1288  
 P       p1288   Number 5833  
 P       p1289   Number 5858  
 O       o1289   apply p1288 p1289  
 P       p1290   Number 5856  
 O       o1290   proj p1288 p1290  
 O       o1291   uid p1288 p1290  
 T       t1291   o1291 b834  
 B       b1291   t1291  
 P       p1291   Number 5842  
 O       o1292   lid p1291 p1290  
 T       t1292   o1292 b836  
 B       b1292   t1292  
 T       t1293   o1290 b1291 b1292  
 B       b1293   t1293  
 P       p1293   Number 5857  
 O       o1293   lid p1293 p1289  
 T       t1294   o1293 b839  
 B       b1294   t1294  
 T       t1295   o1289 b1293 b1294  
 B       b1295   t1295  
 T       t1296   o1285 b1288 b1295  
 B       b1296   t1296  
 P       p1296   Number 5860  
 O       o1296   lid p1296 p1284  
 P       p1297   Var t  
 O       o1297   var p1297  
 T       t1297   o1297  
 B       b1297   t1297  
 T       t1298   o1296 b1297  
 B       b1298   t1298  
 T       t1299   o1284 b1296 b1298  
 B       b1299   t1299  
 P       p1299   Number 5862  
 O       o1299   lid p1299 p1274  
 T       t1300   o1299 b839  
 B       b1300   t1300  
 T       t1301   o1283 b1299 b1300  
 B       b1301   t1301  
 T       t1302   o1281 b1301  
 B       b1302   t1302 p  
 T       t1303   o1282 b1302  
 B       b1303   t1303  
 T       t1304   o1279 b1303  
 B       b1304   t1304  
 T       t1305   o1278 b1304  
 B       b1305   t1305  
 T       t1306   o1281 b1305  
 B       b1306   t1306 t  
 T       t1307   o1280 b1306  
 B       b1307   t1307  
 T       t1308   o1279 b1307  
 B       b1308   t1308  
 T       t1309   o1278 b1308  
 B       b1309   t1309  
 T       t1310   o1275 b1278 b1309  
 B       b1310   t1310  
 T       t1311   o b1310 b4  
 B       b1311   t1311  
 T       t1312   o1275 b1311  
 B       b1312   t1312  
 T       t1313   o390 b1312  
 B       b1313   t1313  
 T       t1314   o1274 b1313  
 B       b1314   t1314  
 P       p1314   Number 5865  
 P       p1315   Number 5939  
 O       o1315   location p1314 p1315  
 O       o1316   str_let p1314 p1315  
 P       p1316   Number 5869  
 O       o1317   patt_var p1316 p1315  
 O       o1318   patt_done p1314 p1315  
 T       t1318   o1318  
 B       b1318   t1318 groupCancelRightT  
 T       t1319   o1317 b1318  
 B       b1319   t1319  
 O       o1319   fun p1316 p1315  
 O       o1320   patt_if p1316 p1315  
 P       p1320   Number 5887  
 P       p1321   Number 5888  
 O       o1321   patt_var p1320 p1321  
 O       o1322   patt_body p1316 p1315  
 P       p1322   Number 5889  
 P       p1323   Number 5890  
 O       o1323   patt_var p1322 p1323  
 P       p1324   Number 5896  
 O       o1324   apply p1324 p1315  
 P       p1325   Number 5937  
 O       o1325   apply p1324 p1325  
 P       p1326   Number 5935  
 O       o1326   apply p1324 p1326  
 P       p1327   Number 5907  
 O       o1327   lid p1324 p1327  
 O       o1328   lid p1070  
 T       t1328   o1328  
 B       b1328   t1328  
 T       t1329   o1327 b1328  
 B       b1329   t1329  
 P       p1329   Number 5909  
 P       p1330   Number 5934  
 O       o1330   apply p1329 p1330  
 P       p1331   Number 5932  
 O       o1331   proj p1329 p1331  
 O       o1332   uid p1329 p1331  
 T       t1332   o1332 b834  
 B       b1332   t1332  
 P       p1332   Number 5918  
 O       o1333   lid p1332 p1331  
 T       t1333   o1333 b836  
 B       b1333   t1333  
 T       t1334   o1331 b1332 b1333  
 B       b1334   t1334  
 P       p1334   Number 5933  
 O       o1334   lid p1334 p1330  
 T       t1335   o1334 b839  
 B       b1335   t1335  
 T       t1336   o1330 b1334 b1335  
 B       b1336   t1336  
 T       t1337   o1326 b1329 b1336  
 B       b1337   t1337  
 P       p1337   Number 5936  
 O       o1337   lid p1337 p1325  
 T       t1338   o1337 b1297  
 B       b1338   t1338  
 T       t1339   o1325 b1337 b1338  
 B       b1339   t1339  
 P       p1339   Number 5938  
 O       o1339   lid p1339 p1315  
 T       t1340   o1339 b839  
 B       b1340   t1340  
 T       t1341   o1324 b1339 b1340  
 B       b1341   t1341  
 T       t1342   o1322 b1341  
 B       b1342   t1342 p  
 T       t1343   o1323 b1342  
 B       b1343   t1343  
 T       t1344   o1320 b1343  
 B       b1344   t1344  
 T       t1345   o1319 b1344  
 B       b1345   t1345  
 T       t1346   o1322 b1345  
 B       b1346   t1346 t  
 T       t1347   o1321 b1346  
 B       b1347   t1347  
 T       t1348   o1320 b1347  
 B       b1348   t1348  
 T       t1349   o1319 b1348  
 B       b1349   t1349  
 T       t1350   o1316 b1319 b1349  
 B       b1350   t1350  
 T       t1351   o b1350 b4  
 B       b1351   t1351  
 T       t1352   o1316 b1351  
 B       b1352   t1352  
 T       t1353   o390 b1352  
 B       b1353   t1353  
 T       t1354   o1315 b1353  
 B       b1354   t1354  
 P       p1354   Number 5957  
 P       p1355   Number 6198  
 O       o1355   location p1354 p1355  
 P       p1356   String unique_id1  
 O       o1356   rule p1356  
 P       p1357   Var e2  
 O       o1357   var p1357  
 T       t1357   o1357  
 B       b1357   t1357  
 T       t1358   o618 b1357  
 S       s1358   t635 h  
 G       s1358   t1358  
 B       b1358   s1358  
 T       t1359   o616 b1358  
 B       b1359   t1359  
 T       t1360   o653 b1357 b552  
 S       s1360   t618 h  
 G       s1360   t1360  
 B       b1360   s1360  
 T       t1361   o616 b1360  
 B       b1361   t1361  
 NCzf_itt_dall   Czf_itt_dall    Czf_itt_dall NIL  
 NCzf_itt_dall!dall      dall    dall Czf_itt_dall  
 O       o1361   dall  
3272  NItt_logic!and  and     and Itt_logic  NItt_logic!and  and     and Itt_logic
3273  O       o1362   and  O       o1271   and