/[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 3535 by xiny, Mon Mar 11 09:57:39 2002 UTC revision 3553 by xiny, Tue Apr 2 07:45:26 2002 UTC
# Line 805  Line 805 
805  T       t298    o1 b297  T       t298    o1 b297
806  B       b298    t298  B       b298    t298
807  P       p298    Number 26  P       p298    Number 26
808  P       p299    Number 45  P       p299    Number 48
809  O       o299    location p298 p299  O       o299    location p298 p299
810  P       p300    String Czf_itt_set  P       p300    String Czf_itt_member
811  O       o300    parent p300  O       o300    parent p300
812  T       t300    o300  T       t300    o300
813  B       b300    t300  B       b300    t300
814  T       t301    o b300 b4  T       t301    o b300 b4
815  B       b301    t301  B       b301    t301
816  P       p301    String Czf_itt_comment  P       p301    String Czf_itt_eq
817  O       o301    parent p301  O       o301    parent p301
818  T       t302    o301  T       t302    o301
819  B       b302    t302  B       b302    t302
820  T       t303    o b302 b4  T       t303    o b302 b4
821  B       b303    t303  B       b303    t303
822  P       p303    String Itt_theory  P       p303    String Czf_itt_set
823  O       o303    parent p303  O       o303    parent p303
824  T       t304    o303  T       t304    o303
825  B       b304    t304  B       b304    t304
826  T       t305    o b304 b4  T       t305    o b304 b4
827  B       b305    t305  B       b305    t305
828  P       p305    String Itt_fset  P       p305    String Czf_itt_comment
829  O       o305    parent p305  O       o305    parent p305
830  T       t306    o305  T       t306    o305
831  B       b306    t306  B       b306    t306
832  T       t307    o b306 b4  T       t307    o b306 b4
833  B       b307    t307  B       b307    t307
834  P       p307    String Itt_prop_decide  P       p307    String Itt_theory
835  O       o307    parent p307  O       o307    parent p307
836  T       t308    o307  T       t308    o307
837  B       b308    t308  B       b308    t308
838  T       t309    o b308 b4  T       t309    o b308 b4
839  B       b309    t309  B       b309    t309
840  P       p309    String Itt_derive  P       p309    String Itt_fset
841  O       o309    parent p309  O       o309    parent p309
842  T       t310    o309  T       t310    o309
843  B       b310    t310  B       b310    t310
844  T       t311    o b310 b4  T       t311    o b310 b4
845  B       b311    t311  B       b311    t311
846  P       p311    String Itt_list2  P       p311    String Itt_prop_decide
847  O       o311    parent p311  O       o311    parent p311
848  T       t312    o311  T       t312    o311
849  B       b312    t312  B       b312    t312
850  T       t313    o b312 b4  T       t313    o b312 b4
851  B       b313    t313  B       b313    t313
852  P       p313    String Itt_list  P       p313    String Itt_derive
853  O       o313    parent p313  O       o313    parent p313
854  T       t314    o313  T       t314    o313
855  B       b314    t314  B       b314    t314
856  T       t315    o b314 b4  T       t315    o b314 b4
857  B       b315    t315  B       b315    t315
858  P       p315    String Itt_quotient  P       p315    String Itt_list2
859  O       o315    parent p315  O       o315    parent p315
860  T       t316    o315  T       t316    o315
861  B       b316    t316  B       b316    t316
862  T       t317    o b316 b4  T       t317    o b316 b4
863  B       b317    t317  B       b317    t317
864  P       p317    String Itt_esquash  P       p317    String Itt_list
865  O       o317    parent p317  O       o317    parent p317
866  T       t318    o317  T       t318    o317
867  B       b318    t318  B       b318    t318
868  T       t319    o b318 b4  T       t319    o b318 b4
869  B       b319    t319  B       b319    t319
870  P       p319    String Itt_srec  P       p319    String Itt_quotient
871  O       o319    parent p319  O       o319    parent p319
872  T       t320    o319  T       t320    o319
873  B       b320    t320  B       b320    t320
874  T       t321    o b320 b4  T       t321    o b320 b4
875  B       b321    t321  B       b321    t321
876  P       p321    String Itt_prec  P       p321    String Itt_esquash
877  O       o321    parent p321  O       o321    parent p321
878  T       t322    o321  T       t322    o321
879  B       b322    t322  B       b322    t322
880  T       t323    o b322 b4  T       t323    o b322 b4
881  B       b323    t323  B       b323    t323
882  P       p323    String Itt_w  P       p323    String Itt_srec
883  O       o323    parent p323  O       o323    parent p323
884  T       t324    o323  T       t324    o323
885  B       b324    t324  B       b324    t324
886  T       t325    o b324 b4  T       t325    o b324 b4
887  B       b325    t325  B       b325    t325
888  P       p325    String Itt_bunion  P       p325    String Itt_prec
889  O       o325    parent p325  O       o325    parent p325
890  T       t326    o325  T       t326    o325
891  B       b326    t326  B       b326    t326
892  T       t327    o b326 b4  T       t327    o b326 b4
893  B       b327    t327  B       b327    t327
894  P       p327    String Itt_bisect  P       p327    String Itt_w
895  O       o327    parent p327  O       o327    parent p327
896  T       t328    o327  T       t328    o327
897  B       b328    t328  B       b328    t328
898  T       t329    o b328 b4  T       t329    o b328 b4
899  B       b329    t329  B       b329    t329
900  P       p329    String Itt_tunion  P       p329    String Itt_bunion
901  O       o329    parent p329  O       o329    parent p329
902  T       t330    o329  T       t330    o329
903  B       b330    t330  B       b330    t330
904  T       t331    o b330 b4  T       t331    o b330 b4
905  B       b331    t331  B       b331    t331
906  P       p331    String Itt_isect  P       p331    String Itt_bisect
907  O       o331    parent p331  O       o331    parent p331
908  T       t332    o331  T       t332    o331
909  B       b332    t332  B       b332    t332
910  T       t333    o b332 b4  T       t333    o b332 b4
911  B       b333    t333  B       b333    t333
912  P       p333    String Itt_struct2  P       p333    String Itt_tunion
913  O       o333    parent p333  O       o333    parent p333
914  T       t334    o333  T       t334    o333
915  B       b334    t334  B       b334    t334
916  T       t335    o b334 b4  T       t335    o b334 b4
917  B       b335    t335  B       b335    t335
918  P       p335    String Itt_well_founded  P       p335    String Itt_isect
919  O       o335    parent p335  O       o335    parent p335
920  T       t336    o335  T       t336    o335
921  B       b336    t336  B       b336    t336
922  T       t337    o b336 b4  T       t337    o b336 b4
923  B       b337    t337  B       b337    t337
924  P       p337    String Itt_int_arith  P       p337    String Itt_struct2
925  O       o337    parent p337  O       o337    parent p337
926  T       t338    o337  T       t338    o337
927  B       b338    t338  B       b338    t338
928  T       t339    o b338 b4  T       t339    o b338 b4
929  B       b339    t339  B       b339    t339
930  P       p339    String Itt_atom_bool  P       p339    String Itt_well_founded
931  O       o339    parent p339  O       o339    parent p339
932  T       t340    o339  T       t340    o339
933  B       b340    t340  B       b340    t340
934  T       t341    o b340 b4  T       t341    o b340 b4
935  B       b341    t341  B       b341    t341
936  P       p341    String Itt_atom  P       p341    String Itt_int_arith
937  O       o341    parent p341  O       o341    parent p341
938  T       t342    o341  T       t342    o341
939  B       b342    t342  B       b342    t342
940  T       t343    o b342 b4  T       t343    o b342 b4
941  B       b343    t343  B       b343    t343
942  T       t344    o b343 b4  P       p343    String Itt_atom_bool
943    O       o343    parent p343
944    T       t344    o343
945  B       b344    t344  B       b344    t344
946  T       t345    o b341 b344  T       t345    o b344 b4
947  B       b345    t345  B       b345    t345
948  T       t346    o b339 b345  P       p345    String Itt_atom
949    O       o345    parent p345
950    T       t346    o345
951  B       b346    t346  B       b346    t346
952  T       t347    o b337 b346  T       t347    o b346 b4
953  B       b347    t347  B       b347    t347
954  T       t348    o b335 b347  T       t348    o b347 b4
955  B       b348    t348  B       b348    t348
956  T       t349    o b333 b348  T       t349    o b345 b348
957  B       b349    t349  B       b349    t349
958  T       t350    o b331 b349  T       t350    o b343 b349
959  B       b350    t350  B       b350    t350
960  T       t351    o b329 b350  T       t351    o b341 b350
961  B       b351    t351  B       b351    t351
962  T       t352    o b327 b351  T       t352    o b339 b351
963  B       b352    t352  B       b352    t352
964  T       t353    o b325 b352  T       t353    o b337 b352
965  B       b353    t353  B       b353    t353
966  T       t354    o b323 b353  T       t354    o b335 b353
967  B       b354    t354  B       b354    t354
968  T       t355    o b321 b354  T       t355    o b333 b354
969  B       b355    t355  B       b355    t355
970  T       t356    o b319 b355  T       t356    o b331 b355
971  B       b356    t356  B       b356    t356
972  T       t357    o b317 b356  T       t357    o b329 b356
973  B       b357    t357  B       b357    t357
974  T       t358    o b315 b357  T       t358    o b327 b357
975  B       b358    t358  B       b358    t358
976  T       t359    o b313 b358  T       t359    o b325 b358
977  B       b359    t359  B       b359    t359
978  T       t360    o b311 b359  T       t360    o b323 b359
979  B       b360    t360  B       b360    t360
980  T       t361    o b309 b360  T       t361    o b321 b360
981  B       b361    t361  B       b361    t361
982  T       t362    o b307 b361  T       t362    o b319 b361
983  B       b362    t362  B       b362    t362
984  T       t363    o b305 b362  T       t363    o b317 b362
985  B       b363    t363  B       b363    t363
986  T       t364    o b303 b363  T       t364    o b315 b363
987  B       b364    t364  B       b364    t364
988  T       t365    o b301 b364  T       t365    o b313 b364
989  B       b365    t365  B       b365    t365
990  T       t366    o2 b301 b365 b296  T       t366    o b311 b365
991  B       b366    t366  B       b366    t366
992  T       t367    o299 b366  T       t367    o b309 b366
993  B       b367    t367  B       b367    t367
994  P       p367    Number 46  T       t368    o b307 b367
995  P       p368    Number 68  B       b368    t368
996  O       o368    location p367 p368  T       t369    o b305 b368
 P       p369    String Czf_itt_member  
 O       o369    parent p369  
 T       t369    o369  
997  B       b369    t369  B       b369    t369
998  T       t370    o b369 b4  T       t370    o b303 b369
999  B       b370    t370  B       b370    t370
1000  P       p370    String Czf_itt_eq  T       t371    o b301 b370
 O       o370    parent p370  
 T       t371    o370  
1001  B       b371    t371  B       b371    t371
1002  T       t372    o b371 b4  T       t372    o2 b301 b371 b296
1003  B       b372    t372  B       b372    t372
1004  T       t373    o b372 b4  T       t373    o299 b372
1005  B       b373    t373  B       b373    t373
1006  T       t374    o b370 b373  P       p373    Number 49
1007    P       p374    Number 67
1008    O       o374    location p373 p374
1009    T       t374    o2 b303 b4 b296
1010  B       b374    t374  B       b374    t374
1011  T       t375    o2 b370 b374 b296  T       t375    o374 b374
1012  B       b375    t375  B       b375    t375
1013  T       t376    o368 b375  P       p375    Number 68
1014  B       b376    t376  P       p376    Number 88
1015  P       p376    Number 69  O       o376    location p375 p376
1016  P       p377    Number 87  P       p377    String Czf_itt_dall
1017  O       o377    location p376 p377  O       o377    parent p377
1018  T       t377    o2 b372 b4 b296  T       t377    o377
1019  B       b377    t377  B       b377    t377
1020  T       t378    o377 b377  T       t378    o b377 b4
1021  B       b378    t378  B       b378    t378
1022  P       p378    Number 88  P       p378    String Czf_itt_set_ind
1023  P       p379    Number 108  O       o378    parent p378
1024  O       o379    location p378 p379  T       t379    o378
1025  P       p380    String Czf_itt_dall  B       b379    t379
1026  O       o380    parent p380  T       t380    o b379 b4
 T       t380    o380  
1027  B       b380    t380  B       b380    t380
1028  T       t381    o b380 b4  P       p380    String Czf_itt_all
1029    O       o380    parent p380
1030    T       t381    o380
1031  B       b381    t381  B       b381    t381
1032  P       p381    String Czf_itt_set_ind  T       t382    o b381 b4
 O       o381    parent p381  
 T       t382    o381  
1033  B       b382    t382  B       b382    t382
1034  T       t383    o b382 b4  P       p382    String Czf_itt_sep
1035    O       o382    parent p382
1036    T       t383    o382
1037  B       b383    t383  B       b383    t383
1038  P       p383    String Czf_itt_all  T       t384    o b383 b4
 O       o383    parent p383  
 T       t384    o383  
1039  B       b384    t384  B       b384    t384
1040  T       t385    o b384 b4  T       t385    o b384 b4
1041  B       b385    t385  B       b385    t385
1042  P       p385    String Czf_itt_sep  T       t386    o b382 b385
 O       o385    parent p385  
 T       t386    o385  
1043  B       b386    t386  B       b386    t386
1044  T       t387    o b386 b4  T       t387    o b380 b386
1045  B       b387    t387  B       b387    t387
1046  T       t388    o b387 b4  T       t388    o b378 b387
1047  B       b388    t388  B       b388    t388
1048  T       t389    o b385 b388  T       t389    o2 b378 b388 b296
1049  B       b389    t389  B       b389    t389
1050  T       t390    o b383 b389  T       t390    o376 b389
1051  B       b390    t390  B       b390    t390
1052  T       t391    o b381 b390  P       p390    Number 89
1053  B       b391    t391  P       p391    Number 108
1054  T       t392    o2 b381 b391 b296  O       o391    location p390 p391
1055    P       p392    String Czf_itt_and
1056    O       o392    parent p392
1057    T       t392    o392
1058  B       b392    t392  B       b392    t392
1059  T       t393    o379 b392  T       t393    o b392 b4
1060  B       b393    t393  B       b393    t393
1061  P       p393    Number 109  T       t394    o b393 b4
1062  P       p394    Number 128  B       b394    t394
1063  O       o394    location p393 p394  T       t395    o2 b393 b394 b296
 P       p395    String Czf_itt_and  
 O       o395    parent p395  
 T       t395    o395  
1064  B       b395    t395  B       b395    t395
1065  T       t396    o b395 b4  T       t396    o391 b395
1066  B       b396    t396  B       b396    t396
1067  T       t397    o b396 b4  P       p396    Number 109
1068  B       b397    t397  P       p397    Number 130
1069  T       t398    o2 b396 b397 b296  O       o397    location p396 p397
1070    P       p398    String Czf_itt_equiv
1071    O       o398    parent p398
1072    T       t398    o398
1073  B       b398    t398  B       b398    t398
1074  T       t399    o394 b398  T       t399    o b398 b4
1075  B       b399    t399  B       b399    t399
1076  P       p399    Number 129  P       p399    String Czf_itt_pair
1077  P       p400    Number 150  O       o399    parent p399
1078  O       o400    location p399 p400  T       t400    o399
1079  P       p401    String Czf_itt_equiv  B       b400    t400
1080  O       o401    parent p401  T       t401    o b400 b4
 T       t401    o401  
1081  B       b401    t401  B       b401    t401
1082  T       t402    o b401 b4  P       p401    String Czf_itt_singleton
1083    O       o401    parent p401
1084    T       t402    o401
1085  B       b402    t402  B       b402    t402
1086  P       p402    String Czf_itt_pair  T       t403    o b402 b4
 O       o402    parent p402  
 T       t403    o402  
1087  B       b403    t403  B       b403    t403
1088  T       t404    o b403 b4  P       p403    String Czf_itt_union
1089    O       o403    parent p403
1090    T       t404    o403
1091  B       b404    t404  B       b404    t404
1092  P       p404    String Czf_itt_singleton  T       t405    o b404 b4
 O       o404    parent p404  
 T       t405    o404  
1093  B       b405    t405  B       b405    t405
1094  T       t406    o b405 b4  P       p405    String Czf_itt_subset
1095    O       o405    parent p405
1096    T       t406    o405
1097  B       b406    t406  B       b406    t406
1098  P       p406    String Czf_itt_union  T       t407    o b406 b4
 O       o406    parent p406  
 T       t407    o406  
1099  B       b407    t407  B       b407    t407
1100  T       t408    o b407 b4  P       p407    String Czf_itt_dexists
1101    O       o407    parent p407
1102    T       t408    o407
1103  B       b408    t408  B       b408    t408
1104  P       p408    String Czf_itt_subset  T       t409    o b408 b4
 O       o408    parent p408  
 T       t409    o408  
1105  B       b409    t409  B       b409    t409
1106  T       t410    o b409 b4  T       t410    o b409 b4
1107  B       b410    t410  B       b410    t410
1108  P       p410    String Czf_itt_dexists  T       t411    o b407 b410
 O       o410    parent p410  
 T       t411    o410  
1109  B       b411    t411  B       b411    t411
1110  T       t412    o b411 b4  T       t412    o b405 b411
1111  B       b412    t412  B       b412    t412
1112  T       t413    o b412 b4  T       t413    o b403 b412
1113  B       b413    t413  B       b413    t413
1114  T       t414    o b410 b413  T       t414    o b401 b413
1115  B       b414    t414  B       b414    t414
1116  T       t415    o b408 b414  T       t415    o b399 b414
1117  B       b415    t415  B       b415    t415
1118  T       t416    o b406 b415  T       t416    o2 b399 b415 b296
1119  B       b416    t416  B       b416    t416
1120  T       t417    o b404 b416  T       t417    o397 b416
1121  B       b417    t417  B       b417    t417
1122  T       t418    o b402 b417  P       p417    Number 132
1123  B       b418    t418  P       p418    Number 143
1124  T       t419    o2 b402 b418 b296  O       o418    location p417 p418
 B       b419    t419  
 T       t420    o400 b419  
 B       b420    t420  
 P       p420    Number 152  
 P       p421    Number 163  
 O       o421    location p420 p421  
1125  NSummary!summary_item   summary_item    summary_item Summary  NSummary!summary_item   summary_item    summary_item Summary
1126  O       o422    summary_item  O       o419    summary_item
1127  NOcaml!str_open str_open        str_open Ocaml  NOcaml!str_open str_open        str_open Ocaml
1128  O       o423    str_open p420 p421  O       o420    str_open p417 p418
1129  NOcaml!string   string  string Ocaml  NOcaml!string   string  string Ocaml
1130  P       p423    String Printf  P       p420    String Printf
1131  O       o424    string p423  O       o421    string p420
1132  T       t424    o424  T       t421    o421
1133    B       b421    t421
1134    T       t422    o b421 b4
1135    B       b422    t422
1136    T       t423    o420 b422
1137    B       b423    t423
1138    T       t424    o419 b423
1139  B       b424    t424  B       b424    t424
1140  T       t425    o b424 b4  T       t425    o418 b424
1141  B       b425    t425  B       b425    t425
1142  T       t426    o423 b425  P       p425    Number 144
1143  B       b426    t426  P       p426    Number 157
1144  T       t427    o422 b426  O       o426    location p425 p426
1145  B       b427    t427  O       o427    str_open p425 p426
1146  T       t428    o421 b427  P       p427    String Mp_debug
1147    O       o428    string p427
1148    T       t428    o428
1149  B       b428    t428  B       b428    t428
1150  P       p428    Number 164  T       t429    o b428 b4
1151  P       p429    Number 177  B       b429    t429
1152  O       o429    location p428 p429  T       t430    o427 b429
1153  O       o430    str_open p428 p429  B       b430    t430
1154  P       p430    String Mp_debug  T       t431    o419 b430
 O       o431    string p430  
 T       t431    o431  
1155  B       b431    t431  B       b431    t431
1156  T       t432    o b431 b4  T       t432    o426 b431
1157  B       b432    t432  B       b432    t432
1158  T       t433    o430 b432  P       p432    Number 158
1159  B       b433    t433  P       p433    Number 187
1160  T       t434    o422 b433  O       o433    location p432 p433
1161  B       b434    t434  O       o434    str_open p432 p433
1162  T       t435    o429 b434  P       p434    String Refiner
1163    O       o435    string p434
1164    T       t435    o435
1165  B       b435    t435  B       b435    t435
1166  P       p435    Number 178  P       p435    String TermType
1167  P       p436    Number 207  O       o436    string p435
1168  O       o436    location p435 p436  T       t436    o436
1169  O       o437    str_open p435 p436  B       b436    t436
1170  P       p437    String Refiner  T       t437    o b436 b4
1171  O       o438    string p437  B       b437    t437
1172  T       t438    o438  T       t438    o b435 b437
1173  B       b438    t438  B       b438    t438
1174  P       p438    String TermType  T       t439    o b435 b438
 O       o439    string p438  
 T       t439    o439  
1175  B       b439    t439  B       b439    t439
1176  T       t440    o b439 b4  T       t440    o434 b439
1177  B       b440    t440  B       b440    t440
1178  T       t441    o b438 b440  T       t441    o419 b440
1179  B       b441    t441  B       b441    t441
1180  T       t442    o b438 b441  T       t442    o433 b441
1181  B       b442    t442  B       b442    t442
1182  T       t443    o437 b442  P       p442    Number 188
1183  B       b443    t443  P       p443    Number 213
1184  T       t444    o422 b443  O       o443    location p442 p443
1185  B       b444    t444  O       o444    str_open p442 p443
1186  T       t445    o436 b444  P       p444    String Term
1187    O       o445    string p444
1188    T       t445    o445
1189  B       b445    t445  B       b445    t445
1190  P       p445    Number 208  T       t446    o b445 b4
1191  P       p446    Number 233  B       b446    t446
1192  O       o446    location p445 p446  T       t447    o b435 b446
1193  O       o447    str_open p445 p446  B       b447    t447
1194  P       p447    String Term  T       t448    o b435 b447
 O       o448    string p447  
 T       t448    o448  
1195  B       b448    t448  B       b448    t448
1196  T       t449    o b448 b4  T       t449    o444 b448
1197  B       b449    t449  B       b449    t449
1198  T       t450    o b438 b449  T       t450    o419 b449
1199  B       b450    t450  B       b450    t450
1200  T       t451    o b438 b450  T       t451    o443 b450
1201  B       b451    t451  B       b451    t451
1202  T       t452    o447 b451  P       p451    Number 214
1203  B       b452    t452  P       p452    Number 241
1204  T       t453    o422 b452  O       o452    location p451 p452
1205  B       b453    t453  O       o453    str_open p451 p452
1206  T       t454    o446 b453  P       p453    String TermOp
1207    O       o454    string p453
1208    T       t454    o454
1209  B       b454    t454  B       b454    t454
1210  P       p454    Number 234  T       t455    o b454 b4
1211  P       p455    Number 261  B       b455    t455
1212  O       o455    location p454 p455  T       t456    o b435 b455
1213  O       o456    str_open p454 p455  B       b456    t456
1214  P       p456    String TermOp  T       t457    o b435 b456
 O       o457    string p456  
 T       t457    o457  
1215  B       b457    t457  B       b457    t457
1216  T       t458    o b457 b4  T       t458    o453 b457
1217  B       b458    t458  B       b458    t458
1218  T       t459    o b438 b458  T       t459    o419 b458
1219  B       b459    t459  B       b459    t459
1220  T       t460    o b438 b459  T       t460    o452 b459
1221  B       b460    t460  B       b460    t460
1222  T       t461    o456 b460  P       p460    Number 242
1223  B       b461    t461  P       p461    Number 271
1224  T       t462    o422 b461  O       o461    location p460 p461
1225  B       b462    t462  O       o462    str_open p460 p461
1226  T       t463    o455 b462  P       p462    String TermAddr
1227    O       o463    string p462
1228    T       t463    o463
1229  B       b463    t463  B       b463    t463
1230  P       p463    Number 262  T       t464    o b463 b4
1231  P       p464    Number 291  B       b464    t464
1232  O       o464    location p463 p464  T       t465    o b435 b464
1233  O       o465    str_open p463 p464  B       b465    t465
1234  P       p465    String TermAddr  T       t466    o b435 b465
 O       o466    string p465  
 T       t466    o466  
1235  B       b466    t466  B       b466    t466
1236  T       t467    o b466 b4  T       t467    o462 b466
1237  B       b467    t467  B       b467    t467
1238  T       t468    o b438 b467  T       t468    o419 b467
1239  B       b468    t468  B       b468    t468
1240  T       t469    o b438 b468  T       t469    o461 b468
1241  B       b469    t469  B       b469    t469
1242  T       t470    o465 b469  P       p469    Number 272
1243  B       b470    t470  P       p470    Number 300
1244  T       t471    o422 b470  O       o470    location p469 p470
1245  B       b471    t471  O       o471    str_open p469 p470
1246  T       t472    o464 b471  P       p471    String TermMan
1247    O       o472    string p471
1248    T       t472    o472
1249  B       b472    t472  B       b472    t472
1250  P       p472    Number 292  T       t473    o b472 b4
1251  P       p473    Number 320  B       b473    t473
1252  O       o473    location p472 p473  T       t474    o b435 b473
1253  O       o474    str_open p472 p473  B       b474    t474
1254  P       p474    String TermMan  T       t475    o b435 b474
 O       o475    string p474  
 T       t475    o475  
1255  B       b475    t475  B       b475    t475
1256  T       t476    o b475 b4  T       t476    o471 b475
1257  B       b476    t476  B       b476    t476
1258  T       t477    o b438 b476  T       t477    o419 b476
1259  B       b477    t477  B       b477    t477
1260  T       t478    o b438 b477  T       t478    o470 b477
1261  B       b478    t478  B       b478    t478
1262  T       t479    o474 b478  P       p478    Number 301
1263  B       b479    t479  P       p479    Number 331
1264  T       t480    o422 b479  O       o479    location p478 p479
1265  B       b480    t480  O       o480    str_open p478 p479
1266  T       t481    o473 b480  P       p480    String TermSubst
1267    O       o481    string p480
1268    T       t481    o481
1269  B       b481    t481  B       b481    t481
1270  P       p481    Number 321  T       t482    o b481 b4
1271  P       p482    Number 351  B       b482    t482
1272  O       o482    location p481 p482  T       t483    o b435 b482
1273  O       o483    str_open p481 p482  B       b483    t483
1274  P       p483    String TermSubst  T       t484    o b435 b483
 O       o484    string p483  
 T       t484    o484  
1275  B       b484    t484  B       b484    t484
1276  T       t485    o b484 b4  T       t485    o480 b484
1277  B       b485    t485  B       b485    t485
1278  T       t486    o b438 b485  T       t486    o419 b485
1279  B       b486    t486  B       b486    t486
1280  T       t487    o b438 b486  T       t487    o479 b486
1281  B       b487    t487  B       b487    t487
1282  T       t488    o483 b487  P       p487    Number 332
1283  B       b488    t488  P       p488    Number 359
1284  T       t489    o422 b488  O       o488    location p487 p488
1285  B       b489    t489  O       o489    str_open p487 p488
1286  T       t490    o482 b489  P       p489    String Refine
1287    O       o490    string p489
1288    T       t490    o490
1289  B       b490    t490  B       b490    t490
1290  P       p490    Number 352  T       t491    o b490 b4
1291  P       p491    Number 379  B       b491    t491
1292  O       o491    location p490 p491  T       t492    o b435 b491
1293  O       o492    str_open p490 p491  B       b492    t492
1294  P       p492    String Refine  T       t493    o b435 b492
 O       o493    string p492  
 T       t493    o493  
1295  B       b493    t493  B       b493    t493
1296  T       t494    o b493 b4  T       t494    o489 b493
1297  B       b494    t494  B       b494    t494
1298  T       t495    o b438 b494  T       t495    o419 b494
1299  B       b495    t495  B       b495    t495
1300  T       t496    o b438 b495  T       t496    o488 b495
1301  B       b496    t496  B       b496    t496
1302  T       t497    o492 b496  P       p496    Number 360
1303  B       b497    t497  P       p497    Number 392
1304  T       t498    o422 b497  O       o497    location p496 p497
1305  B       b498    t498  O       o498    str_open p496 p497
1306  T       t499    o491 b498  P       p498    String RefineError
1307    O       o499    string p498
1308    T       t499    o499
1309  B       b499    t499  B       b499    t499
1310  P       p499    Number 380  T       t500    o b499 b4
1311  P       p500    Number 412  B       b500    t500
1312  O       o500    location p499 p500  T       t501    o b435 b500
1313  O       o501    str_open p499 p500  B       b501    t501
1314  P       p501    String RefineError  T       t502    o b435 b501
 O       o502    string p501  
 T       t502    o502  
1315  B       b502    t502  B       b502    t502
1316  T       t503    o b502 b4  T       t503    o498 b502
1317  B       b503    t503  B       b503    t503
1318  T       t504    o b438 b503  T       t504    o419 b503
1319  B       b504    t504  B       b504    t504
1320  T       t505    o b438 b504  T       t505    o497 b504
1321  B       b505    t505  B       b505    t505
1322  T       t506    o501 b505  P       p505    Number 393
1323  B       b506    t506  P       p506    Number 409
1324  T       t507    o422 b506  O       o506    location p505 p506
1325  B       b507    t507  O       o507    str_open p505 p506
1326  T       t508    o500 b507  P       p507    String Mp_resource
1327    O       o508    string p507
1328    T       t508    o508
1329  B       b508    t508  B       b508    t508
1330  P       p508    Number 413  T       t509    o b508 b4
1331  P       p509    Number 429  B       b509    t509
1332  O       o509    location p508 p509  T       t510    o507 b509
1333  O       o510    str_open p508 p509  B       b510    t510
1334  P       p510    String Mp_resource  T       t511    o419 b510
 O       o511    string p510  
 T       t511    o511  
1335  B       b511    t511  B       b511    t511
1336  T       t512    o b511 b4  T       t512    o506 b511
1337  B       b512    t512  B       b512    t512
1338  T       t513    o510 b512  P       p512    Number 410
1339  B       b513    t513  P       p513    Number 427
1340  T       t514    o422 b513  O       o513    location p512 p513
1341  B       b514    t514  O       o514    str_open p512 p513
1342  T       t515    o509 b514  P       p514    String Simple_print
1343    O       o515    string p514
1344    T       t515    o515
1345  B       b515    t515  B       b515    t515
1346  P       p515    Number 430  T       t516    o b515 b4
1347  P       p516    Number 447  B       b516    t516
1348  O       o516    location p515 p516  T       t517    o514 b516
1349  O       o517    str_open p515 p516  B       b517    t517
1350  P       p517    String Simple_print  T       t518    o419 b517
 O       o518    string p517  
 T       t518    o518  
1351  B       b518    t518  B       b518    t518
1352  T       t519    o b518 b4  T       t519    o513 b518
1353  B       b519    t519  B       b519    t519
1354  T       t520    o517 b519  P       p519    Number 429
1355  B       b520    t520  P       p520    Number 445
1356  T       t521    o422 b520  O       o520    location p519 p520
1357  B       b521    t521  O       o521    str_open p519 p520
1358  T       t522    o516 b521  P       p521    String Tactic_type
1359    O       o522    string p521
1360    T       t522    o522
1361  B       b522    t522  B       b522    t522
1362  P       p522    Number 449  T       t523    o b522 b4
1363  P       p523    Number 465  B       b523    t523
1364  O       o523    location p522 p523  T       t524    o521 b523
1365  O       o524    str_open p522 p523  B       b524    t524
1366  P       p524    String Tactic_type  T       t525    o419 b524
 O       o525    string p524  
 T       t525    o525  
1367  B       b525    t525  B       b525    t525
1368  T       t526    o b525 b4  T       t526    o520 b525
1369  B       b526    t526  B       b526    t526
1370  T       t527    o524 b526  P       p526    Number 446
1371  B       b527    t527  P       p527    Number 472
1372  T       t528    o422 b527  O       o527    location p526 p527
1373  B       b528    t528  O       o528    str_open p526 p527
1374  T       t529    o523 b528  P       p528    String Tacticals
1375    O       o529    string p528
1376    T       t529    o529
1377  B       b529    t529  B       b529    t529
1378  P       p529    Number 466  T       t530    o b529 b4
1379  P       p530    Number 492  B       b530    t530
1380  O       o530    location p529 p530  T       t531    o b522 b530
1381  O       o531    str_open p529 p530  B       b531    t531
1382  P       p531    String Tacticals  T       t532    o528 b531
 O       o532    string p531  
 T       t532    o532  
1383  B       b532    t532  B       b532    t532
1384  T       t533    o b532 b4  T       t533    o419 b532
1385  B       b533    t533  B       b533    t533
1386  T       t534    o b525 b533  T       t534    o527 b533
1387  B       b534    t534  B       b534    t534
1388  T       t535    o531 b534  P       p534    Number 473
1389  B       b535    t535  P       p535    Number 497
1390  T       t536    o422 b535  O       o535    location p534 p535
1391  B       b536    t536  O       o536    str_open p534 p535
1392  T       t537    o530 b536  P       p536    String Sequent
1393    O       o537    string p536
1394    T       t537    o537
1395  B       b537    t537  B       b537    t537
1396  P       p537    Number 493  T       t538    o b537 b4
1397  P       p538    Number 517  B       b538    t538
1398  O       o538    location p537 p538  T       t539    o b522 b538
1399  O       o539    str_open p537 p538  B       b539    t539
1400  P       p539    String Sequent  T       t540    o536 b539
 O       o540    string p539  
 T       t540    o540  
1401  B       b540    t540  B       b540    t540
1402  T       t541    o b540 b4  T       t541    o419 b540
1403  B       b541    t541  B       b541    t541
1404  T       t542    o b525 b541  T       t542    o535 b541
1405  B       b542    t542  B       b542    t542
1406  T       t543    o539 b542  P       p542    Number 498
1407  B       b543    t543  P       p543    Number 528
1408  T       t544    o422 b543  O       o543    location p542 p543
1409  B       b544    t544  O       o544    str_open p542 p543
1410  T       t545    o538 b544  P       p544    String Conversionals
1411    O       o545    string p544
1412    T       t545    o545
1413  B       b545    t545  B       b545    t545
1414  P       p545    Number 518  T       t546    o b545 b4
1415  P       p546    Number 548  B       b546    t546
1416  O       o546    location p545 p546  T       t547    o b522 b546
1417  O       o547    str_open p545 p546  B       b547    t547
1418  P       p547    String Conversionals  T       t548    o544 b547
 O       o548    string p547  
 T       t548    o548  
1419  B       b548    t548  B       b548    t548
1420  T       t549    o b548 b4  T       t549    o419 b548
1421  B       b549    t549  B       b549    t549
1422  T       t550    o b525 b549  T       t550    o543 b549
1423  B       b550    t550  B       b550    t550
1424  T       t551    o547 b550  P       p550    Number 529
1425  B       b551    t551  P       p551    Number 539
1426  T       t552    o422 b551  O       o551    location p550 p551
1427  B       b552    t552  O       o552    str_open p550 p551
1428  T       t553    o546 b552  O       o553    string p91
1429    T       t553    o553
1430  B       b553    t553  B       b553    t553
1431  P       p553    Number 549  T       t554    o b553 b4
1432  P       p554    Number 559  B       b554    t554
1433  O       o554    location p553 p554  T       t555    o552 b554
1434  O       o555    str_open p553 p554  B       b555    t555
1435  O       o556    string p91  T       t556    o419 b555
 T       t556    o556  
1436  B       b556    t556  B       b556    t556
1437  T       t557    o b556 b4  T       t557    o551 b556
1438  B       b557    t557  B       b557    t557
1439  T       t558    o555 b557  P       p557    Number 540
1440  B       b558    t558  P       p558    Number 548
1441  T       t559    o422 b558  O       o558    location p557 p558
1442  B       b559    t559  O       o559    str_open p557 p558
1443  T       t560    o554 b559  O       o560    string p89
1444    T       t560    o560
1445  B       b560    t560  B       b560    t560
1446  P       p560    Number 560  T       t561    o b560 b4
1447  P       p561    Number 568  B       b561    t561
1448  O       o561    location p560 p561  T       t562    o559 b561
1449  O       o562    str_open p560 p561  B       b562    t562
1450  O       o563    string p89  T       t563    o419 b562
 T       t563    o563  
1451  B       b563    t563  B       b563    t563
1452  T       t564    o b563 b4  T       t564    o558 b563
1453  B       b564    t564  B       b564    t564
1454  T       t565    o562 b564  P       p564    Number 550
1455  B       b565    t565  P       p565    Number 567
1456  T       t566    o422 b565  O       o565    location p564 p565
1457  B       b566    t566  O       o566    str_open p564 p565
1458  T       t567    o561 b566  O       o567    string p79
1459    T       t567    o567
1460  B       b567    t567  B       b567    t567
1461  P       p567    Number 570  T       t568    o b567 b4
1462  P       p568    Number 587  B       b568    t568
1463  O       o568    location p567 p568  T       t569    o566 b568
1464  O       o569    str_open p567 p568  B       b569    t569
1465  O       o570    string p79  T       t570    o419 b569
 T       t570    o570  
1466  B       b570    t570  B       b570    t570
1467  T       t571    o b570 b4  T       t571    o565 b570
1468  B       b571    t571  B       b571    t571
1469  T       t572    o569 b571  P       p571    Number 568
1470  B       b572    t572  P       p572    Number 589
1471  T       t573    o422 b572  O       o572    location p571 p572
1472  B       b573    t573  O       o573    str_open p571 p572
1473  T       t574    o568 b573  O       o574    string p81
1474    T       t574    o574
1475  B       b574    t574  B       b574    t574
1476  P       p574    Number 588  T       t575    o b574 b4
1477  P       p575    Number 609  B       b575    t575
1478  O       o575    location p574 p575  T       t576    o573 b575
1479  O       o576    str_open p574 p575  B       b576    t576
1480  O       o577    string p81  T       t577    o419 b576
 T       t577    o577  
1481  B       b577    t577  B       b577    t577
1482  T       t578    o b577 b4  T       t578    o572 b577
1483  B       b578    t578  B       b578    t578
1484  T       t579    o576 b578  P       p578    Number 591
1485  B       b579    t579  P       p579    Number 608
1486  T       t580    o422 b579  O       o579    location p578 p579
 B       b580    t580  
 T       t581    o575 b580  
 B       b581    t581  
 P       p581    Number 611  
 P       p582    Number 628  
 O       o582    location p581 p582  
1487  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1488  P       p583    String group  P       p580    String group
1489  O       o583    opname p583  O       o580    opname p580
1490  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1491  NCzf_itt_group!group    group   group Czf_itt_group  NCzf_itt_group!group    group   group Czf_itt_group
1492  O       o584    group  O       o581    group
1493  Nvar    var     var NIL  Nvar    var     var NIL
1494  P       p584    Var g  P       p581    Var g
1495  O       o585    var p584  O       o582    var p581
1496  T       t585    o585  T       t582    o582
1497    B       b582    t582
1498    T       t583    o581 b582
1499    B       b583    t583
1500    T       t584    o580 b583
1501    B       b584    t584
1502    T       t585    o579 b584
1503  B       b585    t585  B       b585    t585
1504  T       t586    o584 b585  P       p585    Number 609
1505  B       b586    t586  P       p586    Number 624
1506  T       t587    o583 b586  O       o586    location p585 p586
1507  B       b587    t587  P       p587    String car
1508  T       t588    o582 b587  O       o587    opname p587
 B       b588    t588  
 P       p588    Number 629  
 P       p589    Number 644  
 O       o589    location p588 p589  
 P       p590    String car  
 O       o590    opname p590  
1509  NCzf_itt_group!car      car     car Czf_itt_group  NCzf_itt_group!car      car     car Czf_itt_group
1510  O       o591    car  O       o588    car
1511  T       t591    o591 b585  T       t588    o588 b582
1512  B       b591    t591  B       b588    t588
1513  T       t592    o590 b591  T       t589    o587 b588
1514  B       b592    t592  B       b589    t589
1515  T       t593    o589 b592  T       t590    o586 b589
1516    B       b590    t590
1517    P       p590    Number 671
1518    P       p591    Number 686
1519    O       o591    location p590 p591
1520    P       p592    String eqG
1521    O       o592    opname p592
1522    NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
1523    O       o593    eqG
1524    T       t593    o593 b582
1525  B       b593    t593  B       b593    t593
1526  P       p593    Number 685  T       t594    o592 b593
1527  P       p594    Number 707  B       b594    t594
1528  O       o594    location p593 p594  T       t595    o591 b594
1529  P       p595    String op  B       b595    t595
1530  O       o595    opname p595  P       p595    Number 812
1531    P       p596    Number 834
1532    O       o596    location p595 p596
1533    P       p597    String op
1534    O       o597    opname p597
1535  NCzf_itt_group!op       op      op Czf_itt_group  NCzf_itt_group!op       op      op Czf_itt_group
1536  O       o596    op  O       o598    op
1537  P       p596    Var a  P       p598    Var a
1538  O       o597    var p596  O       o599    var p598
1539  T       t597    o597  T       t599    o599
 B       b597    t597  
 P       p597    Var b  
 O       o598    var p597  
 T       t598    o598  
 B       b598    t598  
 T       t599    o596 b585 b597 b598  
1540  B       b599    t599  B       b599    t599
1541  T       t600    o595 b599  P       p599    Var b
1542    O       o600    var p599
1543    T       t600    o600
1544  B       b600    t600  B       b600    t600
1545  T       t601    o594 b600  T       t601    o598 b582 b599 b600
1546  B       b601    t601  B       b601    t601
1547  P       p601    Number 708  T       t602    o597 b601
1548  P       p602    Number 722  B       b602    t602
1549  O       o602    location p601 p602  T       t603    o596 b602
1550  P       p603    String id  B       b603    t603
1551  O       o603    opname p603  P       p603    Number 835
1552    P       p604    Number 849
1553    O       o604    location p603 p604
1554    P       p605    String id
1555    O       o605    opname p605
1556  NCzf_itt_group!id       id      id Czf_itt_group  NCzf_itt_group!id       id      id Czf_itt_group
1557  O       o604    id  O       o606    id
1558  T       t604    o604 b585  T       t606    o606 b582
 B       b604    t604  
 T       t605    o603 b604  
 B       b605    t605  
 T       t606    o602 b605  
1559  B       b606    t606  B       b606    t606
1560  P       p606    Number 723  T       t607    o605 b606
1561  P       p607    Number 742  B       b607    t607
1562  O       o607    location p606 p607  T       t608    o604 b607
1563  P       p608    String inv  B       b608    t608
1564  O       o608    opname p608  P       p608    Number 850
1565    P       p609    Number 869
1566    O       o609    location p608 p609
1567    P       p610    String inv
1568    O       o610    opname p610
1569  NCzf_itt_group!inv      inv     inv Czf_itt_group  NCzf_itt_group!inv      inv     inv Czf_itt_group
1570  O       o609    inv  O       o611    inv
1571  T       t609    o609 b585 b597  T       t611    o611 b582 b599
 B       b609    t609  
 T       t610    o608 b609  
 B       b610    t610  
 T       t611    o607 b610  
1572  B       b611    t611  B       b611    t611
1573  P       p611    Number 744  T       t612    o610 b611
1574  P       p612    Number 756  B       b612    t612
1575  O       o612    location p611 p612  T       t613    o609 b612
 NSummary!prec   prec    prec Summary  
 P       p613    String prec_op  
 O       o613    prec p613  
 T       t613    o613  
1576  B       b613    t613  B       b613    t613
1577  T       t614    o612 b613  P       p613    Number 1012
1578  B       b614    t614  P       p614    Number 1082
1579  P       p614    Number 758  O       o614    location p613 p614
 P       p615    Number 828  
 O       o615    location p614 p615  
1580  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
1581  P       p616    String group_df  P       p615    String group_df
1582  O       o616    dform p616  O       o615    dform p615
1583  NSummary!except_mode_df except_mode_df  except_mode_df Summary  NSummary!except_mode_df except_mode_df  except_mode_df Summary
1584  P       p617    String src  P       p616    String src
1585  O       o617    except_mode_df p617  O       o616    except_mode_df p616
1586  T       t617    o617  T       t616    o616
1587    B       b616    t616
1588    T       t617    o b616 b4
1589  B       b617    t617  B       b617    t617
 T       t618    o b617 b4  
 B       b618    t618  
1590  NSummary!df_term        df_term df_term Summary  NSummary!df_term        df_term df_term Summary
1591  O       o618    df_term  O       o617    df_term
1592  Nslot   slot    slot NIL  Nslot   slot    slot NIL
1593  O       o619    slot  O       o618    slot
1594  T       t619    o619 b585  T       t618    o618 b582
1595    B       b618    t618
1596    NPerv!string    string618       string Perv
1597    P       p618    String " group"
1598    O       o619    string618 p618
1599    T       t619    o619
1600  B       b619    t619  B       b619    t619
1601  NPerv!string    string619       string Perv  T       t620    o b619 b4
 P       p619    String " group"  
 O       o620    string619 p619  
 T       t620    o620  
1602  B       b620    t620  B       b620    t620
1603  T       t621    o b620 b4  T       t621    o b618 b620
1604  B       b621    t621  B       b621    t621
1605  T       t622    o b619 b621  T       t622    o617 b621
1606  B       b622    t622  B       b622    t622
1607  T       t623    o618 b622  T       t623    o615 b617 b583 b622
1608  B       b623    t623  B       b623    t623
1609  T       t624    o616 b618 b586 b623  T       t624    o614 b623
1610  B       b624    t624  B       b624    t624
1611  T       t625    o615 b624  P       p624    Number 1084
1612  B       b625    t625  P       p625    Number 1153
1613  P       p625    Number 830  O       o625    location p624 p625
1614  P       p626    Number 899  P       p626    String car_df
1615  O       o626    location p625 p626  O       o626    dform p626
1616  P       p627    String car_df  P       p627    String car(
1617  O       o627    dform p627  O       o627    string618 p627
1618  P       p628    String car(  T       t627    o627
1619  O       o628    string619 p628  B       b627    t627
1620    P       p628    String )
1621    O       o628    string618 p628
1622  T       t628    o628  T       t628    o628
1623  B       b628    t628  B       b628    t628
1624  P       p629    String )  T       t629    o b628 b4
 O       o629    string619 p629  
 T       t629    o629  
1625  B       b629    t629  B       b629    t629
1626  T       t630    o b629 b4  T       t630    o b618 b629
1627  B       b630    t630  B       b630    t630
1628  T       t631    o b619 b630  T       t631    o b627 b630
1629  B       b631    t631  B       b631    t631
1630  T       t632    o b628 b631  T       t632    o617 b631
1631  B       b632    t632  B       b632    t632
1632  T       t633    o618 b632  T       t633    o626 b617 b588 b632
1633  B       b633    t633  B       b633    t633
1634  T       t634    o627 b618 b591 b633  T       t634    o625 b633
1635  B       b634    t634  B       b634    t634
1636  T       t635    o626 b634  P       p634    Number 1155
1637  B       b635    t635  P       p635    Number 1225
1638  P       p635    Number 901  O       o635    location p634 p635
1639  P       p636    Number 967  P       p636    String eqG_df1
1640  O       o636    location p635 p636  O       o636    dform p636
1641  P       p637    String id_df  P       p637    String eqG(
1642  O       o637    dform p637  O       o637    string618 p637
1643  P       p638    String id(  T       t637    o637
1644  O       o638    string619 p638  B       b637    t637
1645  T       t638    o638  T       t638    o b637 b630
1646  B       b638    t638  B       b638    t638
1647  T       t639    o b638 b631  T       t639    o617 b638
1648  B       b639    t639  B       b639    t639
1649  T       t640    o618 b639  T       t640    o636 b617 b593 b639
1650  B       b640    t640  B       b640    t640
1651  T       t641    o637 b618 b604 b640  T       t641    o635 b640
1652  B       b641    t641  B       b641    t641
1653  T       t642    o636 b641  P       p641    Number 1342
1654  B       b642    t642  P       p642    Number 1408
1655  P       p642    Number 969  O       o642    location p641 p642
1656  P       p643    Number 1103  P       p643    String id_df
1657  O       o643    location p642 p643  O       o643    dform p643
1658  P       p644    String op_df  P       p644    String id(
1659  O       o644    dform p644  O       o644    string618 p644
1660  NSummary!prec_df        prec_df prec_df Summary  T       t644    o644
1661  O       o645    prec_df p613  B       b644    t644
1662  T       t645    o645  T       t645    o b644 b630
1663  B       b645    t645  B       b645    t645
1664  NSummary!parens_df      parens_df       parens_df Summary  T       t646    o617 b645
 O       o646    parens_df  
 T       t646    o646  
1665  B       b646    t646  B       b646    t646
1666  T       t647    o b646 b4  T       t647    o643 b617 b606 b646
1667  B       b647    t647  B       b647    t647
1668  T       t648    o b645 b647  T       t648    o642 b647
1669  B       b648    t648  B       b648    t648
1670  T       t649    o b617 b648  P       p648    Number 1410
1671  B       b649    t649  P       p649    Number 1525
1672  P       p649    String op(  O       o649    location p648 p649
1673  O       o649    string619 p649  P       p650    String op_df
1674  T       t650    o649  O       o650    dform p650
1675  B       b650    t650  NSummary!parens_df      parens_df       parens_df Summary
1676  P       p650    String "; "  O       o651    parens_df
1677  O       o650    string619 p650  T       t651    o651
 T       t651    o650  
1678  B       b651    t651  B       b651    t651
1679  T       t652    o619 b597  T       t652    o b651 b4
1680  B       b652    t652  B       b652    t652
1681  T       t653    o619 b598  T       t653    o b616 b652
1682  B       b653    t653  B       b653    t653
1683  T       t654    o b653 b630  P       p653    String op(
1684    O       o653    string618 p653
1685    T       t654    o653
1686  B       b654    t654  B       b654    t654
1687  T       t655    o b651 b654  P       p654    String "; "
1688    O       o654    string618 p654
1689    T       t655    o654
1690  B       b655    t655  B       b655    t655
1691  T       t656    o b652 b655  T       t656    o618 b599
1692  B       b656    t656  B       b656    t656
1693  T       t657    o b651 b656  T       t657    o618 b600
1694  B       b657    t657  B       b657    t657
1695  T       t658    o b619 b657  T       t658    o b657 b629
1696  B       b658    t658  B       b658    t658
1697  T       t659    o b650 b658  T       t659    o b655 b658
1698  B       b659    t659  B       b659    t659
1699  T       t660    o618 b659  T       t660    o b656 b659
1700  B       b660    t660  B       b660    t660
1701  T       t661    o644 b649 b599 b660  T       t661    o b655 b660
1702  B       b661    t661  B       b661    t661
1703  T       t662    o643 b661  T       t662    o b618 b661
1704  B       b662    t662  B       b662    t662
1705  P       p662    Number 1105  T       t663    o b654 b662
1706  P       p663    Number 1203  B       b663    t663
1707  O       o663    location p662 p663  T       t664    o617 b663
 P       p664    String inv_df  
 O       o664    dform p664  
 T       t664    o b617 b647  
1708  B       b664    t664  B       b664    t664
1709  P       p665    String inv(  T       t665    o650 b653 b601 b664
 O       o665    string619 p665  
 T       t665    o665  
1710  B       b665    t665  B       b665    t665
1711  T       t666    o b652 b630  T       t666    o649 b665
1712  B       b666    t666  B       b666    t666
1713  T       t667    o b651 b666  P       p666    Number 1527
1714  B       b667    t667  P       p667    Number 1625
1715  T       t668    o b619 b667  O       o667    location p666 p667
1716  B       b668    t668  P       p668    String inv_df
1717  T       t669    o b665 b668  O       o668    dform p668
1718    P       p669    String inv(
1719    O       o669    string618 p669
1720    T       t669    o669
1721  B       b669    t669  B       b669    t669
1722  T       t670    o618 b669  T       t670    o b656 b629
1723  B       b670    t670  B       b670    t670
1724  T       t671    o664 b664 b609 b670  T       t671    o b655 b670
1725  B       b671    t671  B       b671    t671
1726  T       t672    o663 b671  T       t672    o b618 b671
1727  B       b672    t672  B       b672    t672
1728  P       p672    Number 1222  T       t673    o b669 b672
1729  P       p673    Number 1356  B       b673    t673
1730  O       o673    location p672 p673  T       t674    o617 b673
1731  NSummary!rule   rule    rule Summary  B       b674    t674
1732  P       p674    String group_type  T       t675    o668 b653 b611 b674
 O       o674    rule p674  
 NSummary!context_param  context_param   context_param Summary  
 P       p675    String H  
 O       o675    context_param p675  
 T       t675    o675  
1733  B       b675    t675  B       b675    t675
1734  T       t676    o b675 b4  T       t676    o667 b675
1735  B       b676    t676  B       b676    t676
1736    P       p676    Number 1644
1737    P       p677    Number 1778
1738    O       o677    location p676 p677
1739    NSummary!rule   rule    rule Summary
1740    P       p678    String group_type
1741    O       o678    rule p678
1742    NSummary!context_param  context_param   context_param Summary
1743    P       p679    String H
1744    O       o679    context_param p679
1745    T       t679    o679
1746    B       b679    t679
1747    T       t680    o b679 b4
1748    B       b680    t680
1749  NSummary!meta_implies   meta_implies    meta_implies Summary  NSummary!meta_implies   meta_implies    meta_implies Summary
1750  O       o676    meta_implies  O       o680    meta_implies
1751  NSummary!meta_theorem   meta_theorem    meta_theorem Summary  NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1752  O       o677    meta_theorem  O       o681    meta_theorem
1753  NBase_trivial   Base_trivial    Base_trivial NIL  NBase_trivial   Base_trivial    Base_trivial NIL
1754  NBase_trivial!squash    squash  squash Base_trivial  NBase_trivial!squash    squash  squash Base_trivial
1755  O       o678    squash  O       o682    squash
1756  T       t678    o678  T       t682    o682
1757  B       b678    t678  B       b682    t682
1758  T       t679    o b678 b4  T       t683    o b682 b4
1759  C       h       H  C       h       H
1760  NItt_equal      Itt_equal       Itt_equal NIL  NItt_equal      Itt_equal       Itt_equal NIL
1761  NItt_equal!equal        equal   equal Itt_equal  NItt_equal!equal        equal   equal Itt_equal
1762  O       o679    equal  O       o683    equal
1763  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1764  NItt_record_label0!label        label   label Itt_record_label0  NItt_record_label0!label        label   label Itt_record_label0
1765  O       o680    label  O       o684    label
1766  T       t680    o680  T       t684    o684
1767  B       b680    t680  B       b684    t684
1768  T       t681    o679 b680 b585 b585  T       t685    o683 b684 b582 b582
1769  S       s       t679 h  S       s       t683 h
1770  G       s       t681  G       s       t685
1771  B       b681    s  B       b685    s
1772  T       t682    o677 b681  T       t686    o681 b685
 B       b682    t682  
 P       p682    Var ext  
 O       o682    var p682  
 T       t683    o682  
 B       b683    t683  
 T       t684    o b683 b4  
 NItt_equal!type type    type Itt_equal  
 O       o684    type  
 T       t685    o684 b586  
 S       s685    t684 h  
 G       s685    t685  
 B       b685    s685  
 T       t686    o677 b685  
1773  B       b686    t686  B       b686    t686
1774  T       t687    o676 b682 b686  P       p686    Var ext
1775    O       o686    var p686
1776    T       t687    o686
1777  B       b687    t687  B       b687    t687
1778    T       t688    o b687 b4
1779    NItt_equal!type type    type Itt_equal
1780    O       o688    type
1781    T       t689    o688 b583
1782    S       s689    t688 h
1783    G       s689    t689
1784    B       b689    s689
1785    T       t690    o681 b689
1786    B       b690    t690
1787    T       t691    o680 b686 b690
1788    B       b691    t691
1789  NSummary!incomplete     incomplete      incomplete Summary  NSummary!incomplete     incomplete      incomplete Summary
1790  O       o687    incomplete  O       o691    incomplete
1791  T       t688    o687  T       t692    o691
1792  B       b688    t688  B       b692    t692
1793  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
1794  P       p688    Number 1248  P       p692    Number 1670
1795  P       p689    Number 1256  P       p693    Number 1678
1796  O       o689    resource_defs p688 p689 p204  O       o693    resource_defs p692 p693 p204
1797  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
1798  P       p690    Number 1254  P       p694    Number 1676
1799  O       o690    uid p690 p689  O       o694    uid p694 p693
1800  P       p691    String []  P       p695    String []
1801  O       o691    uid p691  O       o695    uid p695
1802  T       t691    o691  T       t695    o695
 B       b691    t691  
 T       t692    o690 b691  
 B       b692    t692  
 T       t693    o b692 b4  
 B       b693    t693  
 T       t694    o689 b693  
 B       b694    t694  
 T       t695    o b694 b4  
1803  B       b695    t695  B       b695    t695
1804  T       t696    o674 b676 b687 b688 b695  T       t696    o694 b695
1805  B       b696    t696  B       b696    t696
1806  T       t697    o673 b696  T       t697    o b696 b4
1807  B       b697    t697  B       b697    t697
1808  P       p697    Number 1358  T       t698    o693 b697
1809  P       p698    Number 1526  B       b698    t698
1810  O       o698    location p697 p698  T       t699    o b698 b4
1811  P       p699    String car_wf  B       b699    t699
1812  O       o699    rule p699  T       t700    o678 b680 b691 b692 b699
1813  S       s699    t684 h  B       b700    t700
1814  G       s699    t586  T       t701    o677 b700
1815  B       b699    s699  B       b701    t701
1816  T       t699    o677 b699  P       p701    Number 1780
1817  B       b700    t699  P       p702    Number 1906
1818    O       o702    location p701 p702
1819    P       p703    String car_wf
1820    O       o703    rule p703
1821  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL
1822  NCzf_itt_set!isset      isset   isset Czf_itt_set  NCzf_itt_set!isset      isset   isset Czf_itt_set
1823  O       o700    isset  O       o704    isset
1824  T       t700    o700 b591  T       t704    o704 b588
1825  S       s700    t684 h  S       s704    t688 h
1826  G       s700    t700  G       s704    t704
1827  B       b701    s700  B       b704    s704
1828  T       t701    o677 b701  T       t705    o681 b704
1829  B       b702    t701  B       b705    t705
1830  T       t702    o676 b700 b702  T       t706    o680 b686 b705
 B       b703    t702  
 T       t703    o676 b682 b703  
 B       b704    t703  
 P       p704    Number 1380  
 P       p705    Number 1387  
 O       o705    resource_defs p704 p705 p204  
 P       p706    Number 1385  
 O       o706    uid p706 p705  
 T       t706    o706 b691  
1831  B       b706    t706  B       b706    t706
1832  T       t707    o b706 b4  P       p706    Number 1802
1833  B       b707    t707  P       p707    Number 1809
1834  T       t708    o705 b707  O       o707    resource_defs p706 p707 p204
1835    P       p708    Number 1807
1836    O       o708    uid p708 p707
1837    T       t708    o708 b695
1838  B       b708    t708  B       b708    t708
1839  T       t709    o b708 b4  T       t709    o b708 b4
1840  B       b709    t709  B       b709    t709
1841  T       t710    o699 b676 b704 b688 b709  T       t710    o707 b709
1842  B       b710    t710  B       b710    t710
1843  T       t711    o698 b710  T       t711    o b710 b4
1844  B       b711    t711  B       b711    t711
1845  P       p711    Number 1528  T       t712    o703 b680 b706 b692 b711
1846  P       p712    Number 1795  B       b712    t712
1847  O       o712    location p711 p712  T       t713    o702 b712
1848  P       p713    String op_wf1  B       b713    t713
1849  O       o713    rule p713  P       p713    Number 1908
1850  P       p714    Var s1  P       p714    Number 2035
1851  O       o714    var p714  O       o714    location p713 p714
1852  T       t714    o714  P       p715    String eqG_wf1
1853  B       b714    t714  O       o715    rule p715
1854  T       t715    o700 b714  T       t715    o704 b593
1855  S       s715    t679 h  S       s715    t688 h
1856  G       s715    t715  G       s715    t715
1857  B       b715    s715  B       b715    s715
1858  T       t716    o677 b715  T       t716    o681 b715
1859  B       b716    t716  B       b716    t716
1860  P       p716    Var s2  T       t717    o680 b686 b716
 O       o716    var p716  
 T       t717    o716  
1861  B       b717    t717  B       b717    t717
1862  T       t718    o700 b717  P       p717    Number 1931
1863  S       s718    t679 h  P       p718    Number 1938
1864  G       s718    t718  O       o718    resource_defs p717 p718 p204
1865  B       b718    s718  P       p719    Number 1936
1866  T       t719    o677 b718  O       o719    uid p719 p718
1867    T       t719    o719 b695
1868  B       b719    t719  B       b719    t719
1869  T       t720    o596 b585 b714 b717  T       t720    o b719 b4
1870  B       b720    t720  B       b720    t720
1871  T       t721    o700 b720  T       t721    o718 b720
1872  S       s721    t684 h  B       b721    t721
1873  G       s721    t721  T       t722    o b721 b4
 B       b721    s721  
 T       t722    o677 b721  
1874  B       b722    t722  B       b722    t722
1875  T       t723    o676 b719 b722  T       t723    o715 b680 b717 b692 b722
1876  B       b723    t723  B       b723    t723
1877  T       t724    o676 b716 b723  T       t724    o714 b723
1878  B       b724    t724  B       b724    t724
1879  T       t725    o676 b700 b724  P       p724    Number 2037
1880  B       b725    t725  P       p725    Number 2215
1881  T       t726    o676 b682 b725  O       o725    location p724 p725
1882  B       b726    t726  P       p726    String eqG_wf2
1883  P       p726    Number 1550  O       o726    rule p726
1884  P       p727    Number 1557  S       s726    t688 h
1885  O       o727    resource_defs p726 p727 p204  G       s726    t583
1886  P       p728    Number 1555  B       b726    s726
1887  O       o728    uid p728 p727  T       t726    o681 b726
1888  T       t728    o728 b691  B       b727    t726
1889  B       b728    t728  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1890  T       t729    o b728 b4  NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1891  B       b729    t729  O       o727    equiv
1892  T       t730    o727 b729  T       t727    o727 b588 b593
1893  B       b730    t730  S       s727    t688 h
1894  T       t731    o b730 b4  G       s727    t727
1895  B       b731    t731  B       b728    s727
1896  T       t732    o713 b676 b726 b688 b731  T       t728    o681 b728
1897  B       b732    t732  B       b729    t728
1898  T       t733    o712 b732  T       t729    o680 b727 b729
1899    B       b730    t729
1900    T       t730    o680 b686 b730
1901    B       b731    t730
1902    P       p731    Number 2060
1903    P       p732    Number 2067
1904    O       o732    resource_defs p731 p732 p204
1905    P       p733    Number 2065
1906    O       o733    uid p733 p732
1907    T       t733    o733 b695
1908  B       b733    t733  B       b733    t733
1909  P       p733    Number 1797  T       t734    o b733 b4
1910  P       p734    Number 2171  B       b734    t734
1911  O       o734    location p733 p734  T       t735    o732 b734
1912  P       p735    String op_wf2  B       b735    t735
1913  O       o735    rule p735  T       t736    o b735 b4
1914  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  B       b736    t736
1915  NCzf_itt_member!mem     mem     mem Czf_itt_member  T       t737    o726 b680 b731 b692 b736
 O       o736    mem  
 T       t736    o736 b714 b591  
 S       s736    t684 h  
 G       s736    t736  
 B       b736    s736  
 T       t737    o677 b736  
1916  B       b737    t737  B       b737    t737
1917  T       t738    o736 b717 b591  T       t738    o725 b737
1918  S       s738    t684 h  B       b738    t738
1919  G       s738    t738  P       p738    Number 2910
1920  B       b738    s738  P       p739    Number 3134
1921  T       t739    o677 b738  O       o739    location p738 p739
1922  B       b739    t739  P       p740    String op_wf
1923  T       t740    o736 b720 b591  O       o740    rule p740
1924  S       s740    t684 h  P       p741    Var s1
1925  G       s740    t740  O       o741    var p741
1926  B       b740    s740  T       t741    o741
 T       t741    o677 b740  
1927  B       b741    t741  B       b741    t741
1928  T       t742    o676 b739 b741  T       t742    o704 b741
1929  B       b742    t742  S       s742    t683 h
1930  T       t743    o676 b737 b742  G       s742    t742
1931    B       b742    s742
1932    T       t743    o681 b742
1933  B       b743    t743  B       b743    t743
1934  T       t744    o676 b700 b743  P       p743    Var s2
1935    O       o743    var p743
1936    T       t744    o743
1937  B       b744    t744  B       b744    t744
1938  T       t745    o676 b682 b744  T       t745    o704 b744
1939  B       b745    t745  S       s745    t683 h
1940  T       t746    o676 b719 b745  G       s745    t745
1941    B       b745    s745
1942    T       t746    o681 b745
1943  B       b746    t746  B       b746    t746
1944  T       t747    o676 b716 b746  T       t747    o598 b582 b741 b744
1945  B       b747    t747  B       b747    t747
1946  P       p747    Number 1826  T       t748    o704 b747
1947  O       o747    resource_defs p207 p747 p204  S       s748    t688 h
1948  P       p748    Number 1824  G       s748    t748
1949  O       o748    uid p748 p747  B       b748    s748
1950  T       t748    o748 b691  T       t749    o681 b748
 B       b748    t748  
 T       t749    o b748 b4  
1951  B       b749    t749  B       b749    t749
1952  T       t750    o747 b749  T       t750    o680 b746 b749
1953  B       b750    t750  B       b750    t750
1954  T       t751    o b750 b4  T       t751    o680 b743 b750
1955  B       b751    t751  B       b751    t751
1956  T       t752    o735 b676 b747 b688 b751  T       t752    o680 b686 b751
1957  B       b752    t752  B       b752    t752
1958  T       t753    o734 b752  P       p752    Number 2938
1959    O       o752    resource_defs p230 p752 p204
1960    P       p753    Number 2936
1961    O       o753    uid p753 p752
1962    T       t753    o753 b695
1963  B       b753    t753  B       b753    t753
1964  P       p753    Number 2173  T       t754    o b753 b4
1965  P       p754    Number 2825  B       b754    t754
1966  O       o754    location p753 p754  T       t755    o752 b754
1967  P       p755    String op_equiv1  B       b755    t755
1968  O       o755    rule p755  T       t756    o b755 b4
 P       p756    Var s3  
 O       o756    var p756  
 T       t756    o756  
1969  B       b756    t756  B       b756    t756
1970  T       t757    o700 b756  T       t757    o740 b680 b752 b692 b756
1971  S       s757    t679 h  B       b757    t757
1972  G       s757    t757  T       t758    o739 b757
 B       b757    s757  
 T       t758    o677 b757  
1973  B       b758    t758  B       b758    t758
1974  P       p758    Var R  P       p758    Number 3136
1975  O       o758    var p758  P       p759    Number 3514
1976  T       t759    o758  O       o759    location p758 p759
1977  B       b759    t759  P       p760    String op_closure
1978  T       t760    o700 b759  O       o760    rule p760
1979  S       s760    t679 h  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1980  G       s760    t760  NCzf_itt_member!mem     mem     mem Czf_itt_member
1981  B       b760    s760  O       o761    mem
1982  T       t761    o677 b760  T       t761    o761 b741 b588
1983  B       b761    t761  S       s761    t688 h
1984  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL  G       s761    t761
1985  NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv  B       b761    s761
1986  O       o761    equiv  T       t762    o681 b761
1987  T       t762    o761 b591 b759  B       b762    t762
1988  S       s762    t684 h  T       t763    o761 b744 b588
1989  G       s762    t762  S       s763    t688 h
1990  B       b762    s762  G       s763    t763
1991  T       t763    o677 b762  B       b763    s763
1992  B       b763    t763  T       t764    o681 b763
1993  T       t764    o736 b756 b591  B       b764    t764
1994  S       s764    t684 h  T       t765    o761 b747 b588
1995  G       s764    t764  S       s765    t688 h
1996  B       b764    s764  G       s765    t765
1997  T       t765    o677 b764  B       b765    s765
1998  B       b765    t765  T       t766    o681 b765
1999  T       t766    o761 b591 b759 b714 b717  B       b766    t766
2000  S       s766    t684 h  T       t767    o680 b764 b766
 G       s766    t766  
 B       b766    s766  
 T       t767    o677 b766  
2001  B       b767    t767  B       b767    t767
2002  T       t768    o596 b585 b756 b714  T       t768    o680 b762 b767
2003  B       b768    t768  B       b768    t768
2004  T       t769    o596 b585 b756 b717  T       t769    o680 b727 b768
2005  B       b769    t769  B       b769    t769
2006  T       t770    o761 b591 b759 b768 b769  T       t770    o680 b686 b769
2007  S       s770    t684 h  B       b770    t770
2008  G       s770    t770  T       t771    o680 b746 b770
 B       b770    s770  
 T       t771    o677 b770  
2009  B       b771    t771  B       b771    t771
2010  T       t772    o676 b767 b771  T       t772    o680 b743 b771
2011  B       b772    t772  B       b772    t772
2012  T       t773    o676 b765 b772  P       p772    Number 3162
2013  B       b773    t773  P       p773    Number 3169
2014  T       t774    o676 b739 b773  O       o773    resource_defs p772 p773 p204
2015    P       p774    Number 3167
2016    O       o774    uid p774 p773
2017    T       t774    o774 b695
2018  B       b774    t774  B       b774    t774
2019  T       t775    o676 b737 b774  T       t775    o b774 b4
2020  B       b775    t775  B       b775    t775
2021  T       t776    o676 b763 b775  T       t776    o773 b775
2022  B       b776    t776  B       b776    t776
2023  T       t777    o676 b700 b776  T       t777    o b776 b4
2024  B       b777    t777  B       b777    t777
2025  T       t778    o676 b682 b777  T       t778    o760 b680 b772 b692 b777
2026  B       b778    t778  B       b778    t778
2027  T       t779    o676 b761 b778  T       t779    o759 b778
2028  B       b779    t779  B       b779    t779
2029  T       t780    o676 b758 b779  P       p779    Number 3516
2030  B       b780    t780  P       p780    Number 4081
2031  T       t781    o676 b719 b780  O       o780    location p779 p780
2032  B       b781    t781  P       p781    String op_eqG1
2033  T       t782    o676 b716 b781  O       o781    rule p781
2034    P       p782    Var s3
2035    O       o782    var p782
2036    T       t782    o782
2037  B       b782    t782  B       b782    t782
2038  P       p782    Number 2198  T       t783    o704 b782
2039  P       p783    Number 2205  S       s783    t683 h
2040  O       o783    resource_defs p782 p783 p204  G       s783    t783
2041  P       p784    Number 2203  B       b783    s783
2042  O       o784    uid p784 p783  T       t784    o681 b783
 T       t784    o784 b691  
2043  B       b784    t784  B       b784    t784
2044  T       t785    o b784 b4  T       t785    o761 b782 b588
2045  B       b785    t785  S       s785    t688 h
2046  T       t786    o783 b785  G       s785    t785
2047    B       b785    s785
2048    T       t786    o681 b785
2049  B       b786    t786  B       b786    t786
2050  T       t787    o b786 b4  T       t787    o727 b588 b593 b741 b744
2051  B       b787    t787  S       s787    t688 h
2052  T       t788    o755 b676 b782 b688 b787  G       s787    t787
2053    B       b787    s787
2054    T       t788    o681 b787
2055  B       b788    t788  B       b788    t788
2056  T       t789    o754 b788  T       t789    o598 b582 b782 b741
2057  B       b789    t789  B       b789    t789
2058  P       p789    Number 2827  T       t790    o598 b582 b782 b744
2059  P       p790    Number 3479  B       b790    t790
2060  O       o790    location p789 p790  T       t791    o727 b588 b593 b789 b790
2061  P       p791    String op_equiv2  S       s791    t688 h
2062  O       o791    rule p791  G       s791    t791
2063  T       t791    o596 b585 b714 b756  B       b791    s791
2064  B       b791    t791  T       t792    o681 b791
 T       t792    o596 b585 b717 b756  
2065  B       b792    t792  B       b792    t792
2066  T       t793    o761 b591 b759 b791 b792  T       t793    o680 b788 b792
2067  S       s793    t684 h  B       b793    t793
2068  G       s793    t793  T       t794    o680 b786 b793
 B       b793    s793  
 T       t794    o677 b793  
2069  B       b794    t794  B       b794    t794
2070  T       t795    o676 b767 b794  T       t795    o680 b764 b794
2071  B       b795    t795  B       b795    t795
2072  T       t796    o676 b765 b795  T       t796    o680 b762 b795
2073  B       b796    t796  B       b796    t796
2074  T       t797    o676 b739 b796  T       t797    o680 b727 b796
2075  B       b797    t797  B       b797    t797
2076  T       t798    o676 b737 b797  T       t798    o680 b686 b797
2077  B       b798    t798  B       b798    t798
2078  T       t799    o676 b763 b798  T       t799    o680 b784 b798
2079  B       b799    t799  B       b799    t799
2080  T       t800    o676 b700 b799  T       t800    o680 b746 b799
2081  B       b800    t800  B       b800    t800
2082  T       t801    o676 b682 b800  T       t801    o680 b743 b800
2083  B       b801    t801  B       b801    t801
2084  T       t802    o676 b761 b801  P       p801    Number 3539
2085  B       b802    t802  P       p802    Number 3546
2086  T       t803    o676 b758 b802  O       o802    resource_defs p801 p802 p204
2087    P       p803    Number 3544
2088    O       o803    uid p803 p802
2089    T       t803    o803 b695
2090  B       b803    t803  B       b803    t803
2091  T       t804    o676 b719 b803  T       t804    o b803 b4
2092  B       b804    t804  B       b804    t804
2093  T       t805    o676 b716 b804  T       t805    o802 b804
2094  B       b805    t805  B       b805    t805
2095  P       p805    Number 2852  T       t806    o b805 b4
2096  P       p806    Number 2859  B       b806    t806
2097  O       o806    resource_defs p805 p806 p204  T       t807    o781 b680 b801 b692 b806
 P       p807    Number 2857  
 O       o807    uid p807 p806  
 T       t807    o807 b691  
2098  B       b807    t807  B       b807    t807
2099  T       t808    o b807 b4  T       t808    o780 b807
2100  B       b808    t808  B       b808    t808
2101  T       t809    o806 b808  P       p808    Number 4083
2102  B       b809    t809  P       p809    Number 4648
2103  T       t810    o b809 b4  O       o809    location p808 p809
2104    P       p810    String op_eqG2
2105    O       o810    rule p810
2106    T       t810    o598 b582 b741 b782
2107  B       b810    t810  B       b810    t810
2108  T       t811    o791 b676 b805 b688 b810  T       t811    o598 b582 b744 b782
2109  B       b811    t811  B       b811    t811
2110  T       t812    o790 b811  T       t812    o727 b588 b593 b810 b811
2111  B       b812    t812  S       s812    t688 h
2112  P       p812    Number 3481  G       s812    t812
2113  P       p813    Number 3826  B       b812    s812
2114  O       o813    location p812 p813  T       t813    o681 b812
2115  P       p814    String op_equiv_fun1  B       b813    t813
2116  O       o814    rule p814  T       t814    o680 b788 b813
2117  P       p815    Var s  B       b814    t814
2118  O       o815    var p815  T       t815    o680 b786 b814
 T       t815    o815  
2119  B       b815    t815  B       b815    t815
2120  T       t816    o700 b815  T       t816    o680 b764 b815
2121  S       s816    t679 h  B       b816    t816
2122  G       s816    t816  T       t817    o680 b762 b816
 B       b816    s816  
 T       t817    o677 b816  
2123  B       b817    t817  B       b817    t817
2124  NCzf_itt_equiv!equiv_fun_set    equiv_fun_set   equiv_fun_set Czf_itt_equiv  T       t818    o680 b727 b817
 O       o817    equiv_fun_set  
 P       p817    Var z  
 O       o818    var p817  
 T       t818    o818  
2125  B       b818    t818  B       b818    t818
2126  T       t819    o596 b585 b818 b815  T       t819    o680 b686 b818
2127  B       b819    t819 z  B       b819    t819
2128  T       t820    o817 b591 b759 b819  T       t820    o680 b784 b819
2129  S       s820    t684 h  B       b820    t820
2130  G       s820    t820  T       t821    o680 b746 b820
 B       b820    s820  
 T       t821    o677 b820  
2131  B       b821    t821  B       b821    t821
2132  T       t822    o676 b763 b821  T       t822    o680 b743 b821
2133  B       b822    t822  B       b822    t822
2134  T       t823    o676 b700 b822  P       p822    Number 4106
2135  B       b823    t823  P       p823    Number 4113
2136  T       t824    o676 b682 b823  O       o823    resource_defs p822 p823 p204
2137    P       p824    Number 4111
2138    O       o824    uid p824 p823
2139    T       t824    o824 b695
2140  B       b824    t824  B       b824    t824
2141  T       t825    o676 b761 b824  T       t825    o b824 b4
2142  B       b825    t825  B       b825    t825
2143  T       t826    o676 b817 b825  T       t826    o823 b825
2144  B       b826    t826  B       b826    t826
2145  P       p826    Number 3510  T       t827    o b826 b4
2146  P       p827    Number 3517  B       b827    t827
2147  O       o827    resource_defs p826 p827 p204  T       t828    o810 b680 b822 b692 b827
 P       p828    Number 3515  
 O       o828    uid p828 p827  
 T       t828    o828 b691  
2148  B       b828    t828  B       b828    t828
2149  T       t829    o b828 b4  T       t829    o809 b828
2150  B       b829    t829  B       b829    t829
2151  T       t830    o827 b829  P       p829    Number 4650
2152  B       b830    t830  P       p830    Number 4903
2153  T       t831    o b830 b4  O       o830    location p829 p830
2154  B       b831    t831  P       p831    String op_eqG_fun1
2155  T       t832    o814 b676 b826 b688 b831  O       o831    rule p831
2156    P       p832    Var s
2157    O       o832    var p832
2158    T       t832    o832
2159  B       b832    t832  B       b832    t832
2160  T       t833    o813 b832  T       t833    o704 b832
2161  B       b833    t833  S       s833    t683 h
2162  P       p833    Number 3828  G       s833    t833
2163  P       p834    Number 4173  B       b833    s833
2164  O       o834    location p833 p834  T       t834    o681 b833
2165  P       p835    String op_equiv_fun2  B       b834    t834
2166  O       o835    rule p835  NCzf_itt_equiv!equiv_fun_set    equiv_fun_set   equiv_fun_set Czf_itt_equiv
2167  T       t835    o596 b585 b815 b818  O       o834    equiv_fun_set
2168  B       b835    t835 z  P       p834    Var z
2169  T       t836    o817 b591 b759 b835  O       o835    var p834
2170  S       s836    t684 h  T       t835    o835
2171  G       s836    t836  B       b835    t835
2172  B       b836    s836  T       t836    o598 b582 b835 b832
2173  T       t837    o677 b836  B       b836    t836 z
2174  B       b837    t837  T       t837    o834 b588 b593 b836
2175  T       t838    o676 b763 b837  S       s837    t688 h
2176    G       s837    t837
2177    B       b837    s837
2178    T       t838    o681 b837
2179  B       b838    t838  B       b838    t838
2180  T       t839    o676 b700 b838  T       t839    o680 b727 b838
2181  B       b839    t839  B       b839    t839
2182  T       t840    o676 b682 b839  T       t840    o680 b686 b839
2183  B       b840    t840  B       b840    t840
2184  T       t841    o676 b761 b840  T       t841    o680 b834 b840
2185  B       b841    t841  B       b841    t841
2186  T       t842    o676 b817 b841  P       p841    Number 4677
2187  B       b842    t842  P       p842    Number 4684
2188  P       p842    Number 3857  O       o842    resource_defs p841 p842 p204
2189  P       p843    Number 3864  P       p843    Number 4682
2190  O       o843    resource_defs p842 p843 p204  O       o843    uid p843 p842
2191  P       p844    Number 3862  T       t843    o843 b695
2192  O       o844    uid p844 p843  B       b843    t843
2193  T       t844    o844 b691  T       t844    o b843 b4
2194  B       b844    t844  B       b844    t844
2195  T       t845    o b844 b4  T       t845    o842 b844
2196  B       b845    t845  B       b845    t845
2197  T       t846    o843 b845  T       t846    o b845 b4
2198  B       b846    t846  B       b846    t846
2199  T       t847    o b846 b4  T       t847    o831 b680 b841 b692 b846
2200  B       b847    t847  B       b847    t847
2201  T       t848    o835 b676 b842 b688 b847  T       t848    o830 b847
2202  B       b848    t848  B       b848    t848
2203  T       t849    o834 b848  P       p848    Number 4905
2204  B       b849    t849  P       p849    Number 5160
2205  P       p849    Number 4175  O       o849    location p848 p849
2206  P       p850    Number 4403  P       p850    String op_equiv_fun2
2207  O       o850    location p849 p850  O       o850    rule p850
2208  P       p851    String op_eq_fun1  T       t850    o598 b582 b832 b835
2209  O       o851    rule p851  B       b850    t850 z
2210  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  T       t851    o834 b588 b593 b850
2211  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq  S       s851    t688 h
2212  O       o852    fun_set  G       s851    t851
2213  T       t852    o852 b819  B       b851    s851
2214  S       s852    t684 h  T       t852    o681 b851
2215  G       s852    t852  B       b852    t852
2216  B       b852    s852  T       t853    o680 b727 b852
 T       t853    o677 b852  
2217  B       b853    t853  B       b853    t853
2218  T       t854    o676 b700 b853  T       t854    o680 b686 b853
2219  B       b854    t854  B       b854    t854
2220  T       t855    o676 b682 b854  T       t855    o680 b834 b854
2221  B       b855    t855  B       b855    t855
2222  T       t856    o676 b817 b855  P       p855    Number 4934
2223  B       b856    t856  P       p856    Number 4941
2224  P       p856    Number 4201  O       o856    resource_defs p855 p856 p204
2225  P       p857    Number 4208  P       p857    Number 4939
2226  O       o857    resource_defs p856 p857 p204  O       o857    uid p857 p856
2227  P       p858    Number 4206  T       t857    o857 b695
2228  O       o858    uid p858 p857  B       b857    t857
2229  T       t858    o858 b691  T       t858    o b857 b4
2230  B       b858    t858  B       b858    t858
2231  T       t859    o b858 b4  T       t859    o856 b858
2232  B       b859    t859  B       b859    t859
2233  T       t860    o857 b859  T       t860    o b859 b4
2234  B       b860    t860  B       b860    t860
2235  T       t861    o b860 b4  T       t861    o850 b680 b855 b692 b860
2236  B       b861    t861  B       b861    t861
2237  T       t862    o851 b676 b856 b688 b861  T       t862    o849 b861
2238  B       b862    t862  B       b862    t862
2239  T       t863    o850 b862  P       p862    Number 5162
2240  B       b863    t863  P       p863    Number 5390
2241  P       p863    Number 4405  O       o863    location p862 p863
2242  P       p864    Number 4633  P       p864    String op_eq_fun1
2243  O       o864    location p863 p864  O       o864    rule p864
2244  P       p865    String op_eq_fun2  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
2245  O       o865    rule p865  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq
2246  T       t865    o852 b835  O       o865    fun_set
2247  S       s865    t684 h  T       t865    o865 b836
2248    S       s865    t688 h
2249  G       s865    t865  G       s865    t865
2250  B       b865    s865  B       b865    s865
2251  T       t866    o677 b865  T       t866    o681 b865
2252  B       b866    t866  B       b866    t866
2253  T       t867    o676 b700 b866  T       t867    o680 b727 b866
2254  B       b867    t867  B       b867    t867
2255  T       t868    o676 b682 b867  T       t868    o680 b686 b867
2256  B       b868    t868  B       b868    t868
2257  T       t869    o676 b817 b868  T       t869    o680 b834 b868
2258  B       b869    t869  B       b869    t869
2259  P       p869    Number 4431  P       p869    Number 5188
2260  P       p870    Number 4438  P       p870    Number 5195
2261  O       o870    resource_defs p869 p870 p204  O       o870    resource_defs p869 p870 p204
2262  P       p871    Number 4436  P       p871    Number 5193
2263  O       o871    uid p871 p870  O       o871    uid p871 p870
2264  T       t871    o871 b691  T       t871    o871 b695
2265  B       b871    t871  B       b871    t871
2266  T       t872    o b871 b4  T       t872    o b871 b4
2267  B       b872    t872  B       b872    t872
# Line 2272  Line 2269 
2269  B       b873    t873  B       b873    t873
2270  T       t874    o b873 b4  T       t874    o b873 b4
2271  B       b874    t874  B       b874    t874
2272  T       t875    o865 b676 b869 b688 b874  T       t875    o864 b680 b869 b692 b874
2273  B       b875    t875  B       b875    t875
2274  T       t876    o864 b875  T       t876    o863 b875
2275  B       b876    t876  B       b876    t876
2276  P       p876    Number 4635  P       p876    Number 5392
2277  P       p877    Number 5252  P       p877    Number 5620
2278  O       o877    location p876 p877  O       o877    location p876 p877
2279  P       p878    String op_assoc1  P       p878    String op_eq_fun2
2280  O       o878    rule p878  O       o878    rule p878
2281  T       t878    o596 b585 b720 b756  T       t878    o865 b850
2282  B       b878    t878  S       s878    t688 h
2283  T       t879    o596 b585 b714 b792  G       s878    t878
2284    B       b878    s878
2285    T       t879    o681 b878
2286  B       b879    t879  B       b879    t879
2287  T       t880    o761 b591 b759 b878 b879  T       t880    o680 b727 b879
2288  S       s880    t684 h  B       b880    t880
2289  G       s880    t880  T       t881    o680 b686 b880
 B       b880    s880  
 T       t881    o677 b880  
2290  B       b881    t881  B       b881    t881
2291  T       t882    o676 b765 b881  T       t882    o680 b834 b881
2292  B       b882    t882  B       b882    t882
2293  T       t883    o676 b739 b882  P       p882    Number 5418
2294  B       b883    t883  P       p883    Number 5425
2295  T       t884    o676 b737 b883  O       o883    resource_defs p882 p883 p204
2296    P       p884    Number 5423
2297    O       o884    uid p884 p883
2298    T       t884    o884 b695
2299  B       b884    t884  B       b884    t884
2300  T       t885    o676 b763 b884  T       t885    o b884 b4
2301  B       b885    t885  B       b885    t885
2302  T       t886    o676 b700 b885  T       t886    o883 b885
2303  B       b886    t886  B       b886    t886
2304  T       t887    o676 b682 b886  T       t887    o b886 b4
2305  B       b887    t887  B       b887    t887
2306  T       t888    o676 b761 b887  T       t888    o878 b680 b882 b692 b887
2307  B       b888    t888  B       b888    t888
2308  T       t889    o676 b758 b888  T       t889    o877 b888
2309  B       b889    t889  B       b889    t889
2310  T       t890    o676 b719 b889  P       p889    Number 5622
2311  B       b890    t890  P       p890    Number 6149
2312  T       t891    o676 b716 b890  O       o890    location p889 p890
2313    P       p891    String op_assoc1
2314    O       o891    rule p891
2315    T       t891    o598 b582 b747 b782
2316  B       b891    t891  B       b891    t891
2317  P       p891    Number 4660  T       t892    o598 b582 b741 b811
2318  P       p892    Number 4667  B       b892    t892
2319  O       o892    resource_defs p891 p892 p204  T       t893    o727 b588 b593 b891 b892
2320  P       p893    Number 4665  S       s893    t688 h
2321  O       o893    uid p893 p892  G       s893    t893
2322  T       t893    o893 b691  B       b893    s893
2323  B       b893    t893  T       t894    o681 b893
 T       t894    o b893 b4  
2324  B       b894    t894  B       b894    t894
2325  T       t895    o892 b894  T       t895    o680 b786 b894
2326  B       b895    t895  B       b895    t895
2327  T       t896    o b895 b4  T       t896    o680 b764 b895
2328  B       b896    t896  B       b896    t896
2329  T       t897    o878 b676 b891 b688 b896  T       t897    o680 b762 b896
2330  B       b897    t897  B       b897    t897
2331  T       t898    o877 b897  T       t898    o680 b727 b897
2332  B       b898    t898  B       b898    t898
2333  P       p898    Number 5254  T       t899    o680 b686 b898
2334  P       p899    Number 5871  B       b899    t899
2335  O       o899    location p898 p899  T       t900    o680 b784 b899
2336  P       p900    String op_assoc2  B       b900    t900
2337  O       o900    rule p900  T       t901    o680 b746 b900
 T       t900    o761 b591 b759 b879 b878  
 S       s900    t684 h  
 G       s900    t900  
 B       b900    s900  
 T       t901    o677 b900  
2338  B       b901    t901  B       b901    t901
2339  T       t902    o676 b765 b901  T       t902    o680 b743 b901
2340  B       b902    t902  B       b902    t902
2341  T       t903    o676 b739 b902  P       p902    Number 5647
2342  B       b903    t903  P       p903    Number 5654
2343  T       t904    o676 b737 b903  O       o903    resource_defs p902 p903 p204
2344    P       p904    Number 5652
2345    O       o904    uid p904 p903
2346    T       t904    o904 b695
2347  B       b904    t904  B       b904    t904
2348  T       t905    o676 b763 b904  T       t905    o b904 b4
2349  B       b905    t905  B       b905    t905
2350  T       t906    o676 b700 b905  T       t906    o903 b905
2351  B       b906    t906  B       b906    t906
2352  T       t907    o676 b682 b906  T       t907    o b906 b4
2353  B       b907    t907  B       b907    t907
2354  T       t908    o676 b761 b907  T       t908    o891 b680 b902 b692 b907
2355  B       b908    t908  B       b908    t908
2356  T       t909    o676 b758 b908  T       t909    o890 b908
2357  B       b909    t909  B       b909    t909
2358  T       t910    o676 b719 b909  P       p909    Number 6151
2359  B       b910    t910  P       p910    Number 6678
2360  T       t911    o676 b716 b910  O       o910    location p909 p910
2361  B       b911    t911  P       p911    String op_assoc2
2362  P       p911    Number 5279  O       o911    rule p911
2363  P       p912    Number 5286  T       t911    o727 b588 b593 b892 b891
2364  O       o912    resource_defs p911 p912 p204  S       s911    t688 h
2365  P       p913    Number 5284  G       s911    t911
2366  O       o913    uid p913 p912  B       b911    s911
2367  T       t913    o913 b691  T       t912    o681 b911
2368    B       b912    t912
2369    T       t913    o680 b786 b912
2370  B       b913    t913  B       b913    t913
2371  T       t914    o b913 b4  T       t914    o680 b764 b913
2372  B       b914    t914  B       b914    t914
2373  T       t915    o912 b914  T       t915    o680 b762 b914
2374  B       b915    t915  B       b915    t915
2375  T       t916    o b915 b4  T       t916    o680 b727 b915
2376  B       b916    t916  B       b916    t916
2377  T       t917    o900 b676 b911 b688 b916  T       t917    o680 b686 b916
2378  B       b917    t917  B       b917    t917
2379  T       t918    o899 b917  T       t918    o680 b784 b917
2380  B       b918    t918  B       b918    t918
2381  P       p918    Number 5873  T       t919    o680 b746 b918
2382  P       p919    Number 6041  B       b919    t919
2383  O       o919    location p918 p919  T       t920    o680 b743 b919
2384  P       p920    String id_wf1  B       b920    t920
2385  O       o920    rule p920  P       p920    Number 6176
2386  T       t920    o700 b604  O       o920    resource_defs p920 p202 p204
2387  S       s920    t684 h  O       o921    uid p197 p202
2388  G       s920    t920  T       t921    o921 b695
 B       b920    s920  
 T       t921    o677 b920  
2389  B       b921    t921  B       b921    t921
2390  T       t922    o676 b700 b921  T       t922    o b921 b4
2391  B       b922    t922  B       b922    t922
2392  T       t923    o676 b682 b922  T       t923    o920 b922
2393  B       b923    t923  B       b923    t923
2394  P       p923    Number 5895  T       t924    o b923 b4
2395  P       p924    Number 5903  B       b924    t924
2396  O       o924    resource_defs p923 p924 p204  T       t925    o911 b680 b920 b692 b924
 P       p925    Number 5901  
 O       o925    uid p925 p924  
 T       t925    o925 b691  
2397  B       b925    t925  B       b925    t925
2398  T       t926    o b925 b4  T       t926    o910 b925
2399  B       b926    t926  B       b926    t926
2400  T       t927    o924 b926  P       p926    Number 6680
2401  B       b927    t927  P       p927    Number 6806
2402  T       t928    o b927 b4  O       o927    location p926 p927
2403  B       b928    t928  P       p928    String id_wf1
2404  T       t929    o920 b676 b923 b688 b928  O       o928    rule p928
2405    T       t928    o704 b606
2406    S       s928    t688 h
2407    G       s928    t928
2408    B       b928    s928
2409    T       t929    o681 b928
2410  B       b929    t929  B       b929    t929
2411  T       t930    o919 b929  T       t930    o680 b686 b929
2412  B       b930    t930  B       b930    t930
2413  P       p930    Number 6043  P       p930    Number 6702
2414  P       p931    Number 6217  P       p931    Number 6710
2415  O       o931    location p930 p931  O       o931    resource_defs p930 p931 p204
2416  P       p932    String id_wf2  P       p932    Number 6708
2417  O       o932    rule p932  O       o932    uid p932 p931
2418  T       t932    o736 b604 b591  T       t932    o932 b695
2419  S       s932    t684 h  B       b932    t932
2420  G       s932    t932  T       t933    o b932 b4
 B       b932    s932  
 T       t933    o677 b932  
2421  B       b933    t933  B       b933    t933
2422  T       t934    o676 b700 b933  T       t934    o931 b933
2423  B       b934    t934  B       b934    t934
2424  T       t935    o676 b682 b934  T       t935    o b934 b4
2425  B       b935    t935  B       b935    t935
2426  P       p935    Number 6065  T       t936    o928 b680 b930 b692 b935
2427  P       p936    Number 6072  B       b936    t936
2428  O       o936    resource_defs p935 p936 p204  T       t937    o927 b936
 P       p937    Number 6070  
 O       o937    uid p937 p936  
 T       t937    o937 b691  
2429  B       b937    t937  B       b937    t937
2430  T       t938    o b937 b4  P       p937    Number 6808
2431  B       b938    t938  P       p938    Number 6982
2432  T       t939    o936 b938  O       o938    location p937 p938
2433  B       b939    t939  P       p939    String id_wf2
2434  T       t940    o b939 b4  O       o939    rule p939
2435    T       t939    o761 b606 b588
2436    S       s939    t688 h
2437    G       s939    t939
2438    B       b939    s939
2439    T       t940    o681 b939
2440  B       b940    t940  B       b940    t940
2441  T       t941    o932 b676 b935 b688 b940  T       t941    o680 b727 b940
2442  B       b941    t941  B       b941    t941
2443  T       t942    o931 b941  T       t942    o680 b686 b941
2444  B       b942    t942  B       b942    t942
2445  P       p942    Number 6219  P       p942    Number 6830
2446  P       p943    Number 6603  P       p943    Number 6837
2447  O       o943    location p942 p943  O       o943    resource_defs p942 p943 p204
2448  P       p944    String id_eq1  P       p944    Number 6835
2449  O       o944    rule p944  O       o944    uid p944 p943
2450  T       t944    o736 b815 b591  T       t944    o944 b695
2451  S       s944    t684 h  B       b944    t944
2452  G       s944    t944  T       t945    o b944 b4
 B       b944    s944  
 T       t945    o677 b944  
2453  B       b945    t945  B       b945    t945
2454  T       t946    o596 b585 b604 b815  T       t946    o943 b945
2455  B       b946    t946  B       b946    t946
2456  T       t947    o761 b591 b759 b946 b815  T       t947    o b946 b4
2457  S       s947    t684 h  B       b947    t947
2458  G       s947    t947  T       t948    o939 b680 b942 b692 b947
 B       b947    s947  
 T       t948    o677 b947  
2459  B       b948    t948  B       b948    t948
2460  T       t949    o676 b945 b948  T       t949    o938 b948
2461  B       b949    t949  B       b949    t949
2462  T       t950    o676 b763 b949  P       p949    Number 6984
2463  B       b950    t950  P       p950    Number 7278
2464  T       t951    o676 b700 b950  O       o950    location p949 p950
2465  B       b951    t951  P       p951    String id_eq1
2466  T       t952    o676 b682 b951  O       o951    rule p951
2467    T       t951    o761 b832 b588
2468    S       s951    t688 h
2469    G       s951    t951
2470    B       b951    s951
2471    T       t952    o681 b951
2472  B       b952    t952  B       b952    t952
2473  T       t953    o676 b761 b952  T       t953    o598 b582 b606 b832
2474  B       b953    t953  B       b953    t953
2475  T       t954    o676 b817 b953  T       t954    o727 b588 b593 b953 b832
2476  B       b954    t954  S       s954    t688 h
2477  P       p954    Number 6241  G       s954    t954
2478  P       p955    Number 6248  B       b954    s954
2479  O       o955    resource_defs p954 p955 p204  T       t955    o681 b954
2480  P       p956    Number 6246  B       b955    t955
2481  O       o956    uid p956 p955  T       t956    o680 b952 b955
 T       t956    o956 b691  
2482  B       b956    t956  B       b956    t956
2483  T       t957    o b956 b4  T       t957    o680 b727 b956
2484  B       b957    t957  B       b957    t957
2485  T       t958    o955 b957  T       t958    o680 b686 b957
2486  B       b958    t958  B       b958    t958
2487  T       t959    o b958 b4  T       t959    o680 b834 b958
2488  B       b959    t959  B       b959    t959
2489  T       t960    o944 b676 b954 b688 b959  P       p959    Number 7006
2490  B       b960    t960  P       p960    Number 7013
2491  T       t961    o943 b960  O       o960    resource_defs p959 p960 p204
2492    P       p961    Number 7011
2493    O       o961    uid p961 p960
2494    T       t961    o961 b695
2495  B       b961    t961  B       b961    t961
2496  P       p961    Number 6605  T       t962    o b961 b4
2497  P       p6      Number 6874  B       b962    t962
2498  O       o10     location p961 p6  T       t963    o960 b962
 P       p963    String id_eq2  
 O       o963    rule p963  
 T       t963    o596 b585 b815 b604  
2499  B       b963    t963  B       b963    t963
2500  T       t964    o761 b591 b759 b963 b815  T       t964    o b963 b4
2501  S       s964    t684 h  B       b964    t964
2502  G       s964    t964  T       t965    o951 b680 b959 b692 b964
 B       b964    s964  
 T       t965    o677 b964  
2503  B       b965    t965  B       b965    t965
2504  T       t966    o676 b945 b965  T       t966    o950 b965
2505  B       b966    t966  B       b966    t966
2506  T       t967    o676 b763 b966  P       p966    Number 7280
2507  B       b967    t967  P       p967    Number 7457
2508  T       t968    o676 b700 b967  O       o967    location p966 p967
2509    P       p968    String inv_wf1
2510    O       o968    rule p968
2511    T       t968    o611 b582 b741
2512  B       b968    t968  B       b968    t968
2513  T       t969    o676 b682 b968  T       t969    o704 b968
2514  B       b969    t969  S       s969    t688 h
2515  T       t970    o676 b761 b969  G       s969    t969
2516    B       b969    s969
2517    T       t970    o681 b969
2518  B       b970    t970  B       b970    t970
2519  T       t971    o676 b817 b970  T       t971    o680 b686 b970
2520  B       b971    t971  B       b971    t971
2521  P       p980    String inv_wf1  T       t972    o680 b743 b971
2522  O       o980    rule p980  B       b972    t972
2523  T       t980    o609 b585 b714  P       p972    Number 7303
2524  B       b980    t980  P       p973    Number 7310
2525  T       t981    o700 b980  O       o973    resource_defs p972 p973 p204
2526  S       s981    t684 h  P       p974    Number 7308
2527    O       o974    uid p974 p973
2528    T       t974    o974 b695
2529    B       b974    t974
2530    T       t975    o b974 b4
2531    B       b975    t975
2532    T       t976    o973 b975
2533    B       b976    t976
2534    T       t977    o b976 b4
2535    B       b977    t977
2536    T       t978    o968 b680 b972 b692 b977
2537    B       b978    t978
2538    T       t979    o967 b978
2539    B       b979    t979
2540    P       p979    Number 7459
2541    P       p980    Number 7735
2542    O       o980    location p979 p980
2543    P       p981    String inv_wf2
2544    O       o981    rule p981
2545    T       t981    o761 b968 b588
2546    S       s981    t688 h
2547  G       s981    t981  G       s981    t981
2548  B       b981    s981  B       b981    s981
2549  T       t982    o677 b981  T       t982    o681 b981
2550  B       b982    t982  B       b982    t982
2551  T       t983    o676 b737 b982  T       t983    o680 b762 b982
2552  B       b983    t983  B       b983    t983
2553  T       t984    o676 b700 b983  T       t984    o680 b727 b983
2554  B       b984    t984  B       b984    t984
2555  T       t985    o676 b682 b984  T       t985    o680 b686 b984
2556  B       b985    t985  B       b985    t985
2557  T       t986    o676 b716 b985  T       t986    o680 b743 b985
2558  B       b986    t986  B       b986    t986
2559  P       p10     Number 6628  P       p986    Number 7482
2560  P       p12     Number 6635  P       p987    Number 7489
2561  O       o12     resource_defs p10 p12 p204  O       o987    resource_defs p986 p987 p204
2562  P       p14     Number 6633  P       p988    Number 7487
2563  O       o14     uid p14 p12  O       o988    uid p988 p987
2564  T       t250    o14 b691  T       t988    o988 b695
2565  B       b250    t250  B       b988    t988
2566  T       t255    o b250 b4  T       t989    o b988 b4
2567  B       b255    t255  B       b989    t989
2568  T       t256    o12 b255  T       t990    o987 b989
2569  B       b256    t256  B       b990    t990
2570  T       t258    o b256 b4  T       t991    o b990 b4
2571  B       b258    t258  B       b991    t991
2572  T       t260    o980 b676 b986 b688 b258  T       t992    o981 b680 b986 b692 b991
2573  B       b260    t260  B       b992    t992
2574  T       t267    o10 b260  T       t993    o980 b992
2575  B       b267    t267  B       b993    t993
2576  P       p269    Number 6876  P       p993    Number 7737
2577  P       p277    Number 7152  P       p994    Number 7946
2578  O       o277    location p269 p277  O       o994    location p993 p994
2579  P       p995    String inv_wf2  P       p995    String inv_equiv_fun1
2580  O       o995    rule p995  O       o995    rule p995
2581  T       t995    o736 b980 b591  T       t995    o611 b582 b835
2582  S       s995    t684 h  B       b995    t995 z
2583  G       s995    t995  T       t996    o834 b588 b593 b995
2584  B       b995    s995  S       s996    t688 h
2585  T       t996    o677 b995  G       s996    t996
2586  B       b996    t996  B       b996    s996
2587  T       t997    o676 b737 b996  T       t997    o681 b996
2588  B       b997    t997  B       b997    t997
2589  T       t998    o676 b700 b997  T       t998    o680 b727 b997
2590  B       b998    t998  B       b998    t998
2591  T       t999    o676 b682 b998  T       t999    o680 b686 b998
2592  B       b999    t999  B       b999    t999
2593  T       t1000   o676 b716 b999  P       p999    Number 7767
2594  B       b1000   t1000  P       p1000   Number 7774
2595  P       p284    Number 6899  O       o1000   resource_defs p999 p1000 p204
2596  P       p285    Number 6906  P       p1001   Number 7772
2597  O       o285    resource_defs p284 p285 p204  O       o1001   uid p1001 p1000
2598  P       p286    Number 6904  T       t1001   o1001 b695
2599  O       o286    uid p286 p285  B       b1001   t1001
2600  T       t299    o286 b691  T       t1002   o b1001 b4
2601  B       b299    t299  B       b1002   t1002
2602  T       t368    o b299 b4  T       t1003   o1000 b1002
2603  B       b368    t368  B       b1003   t1003
2604  T       t379    o285 b368  T       t1004   o b1003 b4
2605  B       b379    t379  B       b1004   t1004
2606  T       t394    o b379 b4  T       t1005   o995 b680 b999 b692 b1004
2607  B       b394    t394  B       b1005   t1005
2608  T       t400    o995 b676 b1000 b688 b394  T       t1006   o994 b1005
2609  B       b400    t400  B       b1006   t1006
2610  T       t421    o277 b400  P       p1006   Number 7948
2611  B       b421    t421  P       p1007   Number 8130
2612  P       p422    Number 7154  O       o1007   location p1006 p1007
2613  P       p424    Number 7453  P       p1008   String inv_eq_fun1
2614  O       o425    location p422 p424  O       o1008   rule p1008
2615  P       p1009   String inv_equiv_fun1  T       t1008   o865 b995
2616  O       o1009   rule p1009  S       s1008   t688 h
2617  T       t1009   o609 b585 b818  G       s1008   t1008
2618  B       b1009   t1009 z  B       b1008   s1008
2619  T       t1010   o817 b591 b759 b1009  T       t1009   o681 b1008
2620  S       s1010   t684 h  B       b1009   t1009
2621  G       s1010   t1010  T       t1010   o680 b727 b1009
2622  B       b1010   s1010  B       b1010   t1010
2623  T       t1011   o677 b1010  T       t1011   o680 b686 b1010
2624  B       b1011   t1011  B       b1011   t1011
2625  T       t1012   o676 b763 b1011  P       p1011   Number 7975
2626  B       b1012   t1012  P       p1012   Number 7982
2627  T       t1013   o676 b700 b1012  O       o1012   resource_defs p1011 p1012 p204
2628    P       p1013   Number 7980
2629    O       o1013   uid p1013 p1012
2630    T       t1013   o1013 b695
2631  B       b1013   t1013  B       b1013   t1013
2632  T       t1014   o676 b682 b1013  T       t1014   o b1013 b4
2633  B       b1014   t1014  B       b1014   t1014
2634  T       t1015   o676 b761 b1014  T       t1015   o1012 b1014
2635  B       b1015   t1015  B       b1015   t1015
2636  P       p425    Number 7184  T       t1016   o b1015 b4
2637  P       p426    Number 7191  B       b1016   t1016
2638  O       o426    resource_defs p425 p426 p204  T       t1017   o1008 b680 b1011 b692 b1016
2639  P       p427    Number 7189  B       b1017   t1017
2640  O       o427    uid p427 p426  T       t1018   o1007 b1017
2641  T       t429    o427 b691  B       b1018   t1018
2642  B       b429    t429  P       p1018   Number 8132
2643  T       t430    o b429 b4  P       p1019   Number 8440
2644  B       b430    t430  O       o1019   location p1018 p1019
2645  T       t436    o426 b430  P       p1020   String inv_id1
2646  B       b436    t436  O       o1020   rule p1020
2647  T       t437    o b436 b4  T       t1020   o598 b582 b968 b741
2648  B       b437    t437  B       b1020   t1020
2649  T       t446    o1009 b676 b1015 b688 b437  T       t1021   o727 b588 b593 b1020 b606
2650  B       b446    t446  S       s1021   t688 h
2651  T       t447    o425 b446  G       s1021   t1021
2652  B       b447    t447  B       b1021   s1021
2653  P       p448    Number 7455  T       t1022   o681 b1021
2654  P       p449    Number 7637  B       b1022   t1022
2655  O       o449    location p448 p449  T       t1023   o680 b762 b1022
2656  P       p1024   String inv_eq_fun1  B       b1023   t1023
2657  O       o1024   rule p1024  T       t1024   o680 b727 b1023
2658  T       t1024   o852 b1009  B       b1024   t1024
2659  S       s1024   t684 h  T       t1025   o680 b686 b1024
 G       s1024   t1024  
 B       b1024   s1024  
 T       t1025   o677 b1024  
2660  B       b1025   t1025  B       b1025   t1025
2661  T       t1026   o676 b700 b1025  T       t1026   o680 b743 b1025
2662  B       b1026   t1026  B       b1026   t1026
2663  T       t1027   o676 b682 b1026  P       p1026   Number 8155
2664  B       b1027   t1027  P       p1027   Number 8162
2665  P       p450    Number 7482  O       o1027   resource_defs p1026 p1027 p204
2666  P       p451    Number 7489  P       p1028   Number 8160
2667  O       o451    resource_defs p450 p451 p204  O       o1028   uid p1028 p1027
2668  P       p452    Number 7487  T       t1028   o1028 b695
2669  O       o452    uid p452 p451  B       b1028   t1028
2670  T       t455    o452 b691  T       t1029   o b1028 b4
2671  B       b455    t455  B       b1029   t1029
2672  T       t456    o b455 b4  T       t1030   o1027 b1029
2673  B       b456    t456  B       b1030   t1030
2674  T       t464    o451 b456  T       t1031   o b1030 b4
2675  B       b464    t464  B       b1031   t1031
2676  T       t465    o b464 b4  T       t1032   o1020 b680 b1026 b692 b1031
2677  B       b465    t465  B       b1032   t1032
2678  T       t473    o1024 b676 b1027 b688 b465  T       t1033   o1019 b1032
2679  B       b473    t473  B       b1033   t1033
2680  T       t474    o449 b473  P       p1033   Number 8459
2681  B       b474    t474  P       p1034   Number 9032
2682  P       p475    Number 7639  O       o1034   location p1033 p1034
2683  P       p476    Number 8037  P       p1035   String id_judge_elim
2684  O       o476    location p475 p476  O       o1035   rule p1035
2685  P       p1036   String inv_id1  P       p1036   String J
2686  O       o1036   rule p1036  O       o1036   context_param p1036
2687  T       t1036   o596 b585 b980 b714  T       t1036   o1036
2688  B       b1036   t1036  B       b1036   t1036
2689  T       t1037   o761 b591 b759 b1036 b604  T       t1037   o b1036 b4
2690  S       s1037   t684 h  B       b1037   t1037
2691  G       s1037   t1037  T       t1038   o b679 b1037
 B       b1037   s1037  
 T       t1038   o677 b1037  
2692  B       b1038   t1038  B       b1038   t1038
2693  T       t1039   o676 b737 b1038  T       t1039   o598 b582 b832 b832
2694  B       b1039   t1039  B       b1039   t1039
2695  T       t1040   o676 b763 b1039  T       t1040   o727 b588 b593 b1039 b832
2696  B       b1040   t1040  H       h1040   x t1040
2697  T       t1041   o676 b700 b1040  P       p1040   Var x
2698  B       b1041   t1041  O       o1040   var p1040
2699  T       t1042   o676 b682 b1041  T       t1041   o1040
2700    C       h1041   J t1041
2701    S       s1041   t683 h h1040 h1041
2702    G       s1041   t833
2703    B       b1041   s1041
2704    T       t1042   o681 b1041
2705  B       b1042   t1042  B       b1042   t1042
2706  T       t1043   o676 b761 b1042  S       s1042   t683 h h1040 h1041
2707  B       b1043   t1043  G       s1042   t685
2708  T       t1044   o676 b716 b1043  B       b1043   s1042
2709  B       b1044   t1044  T       t1043   o681 b1043
2710  P       p477    Number 7662  B       b1044   t1043
2711  P       p478    Number 7669  S       s1044   t688 h h1040 h1041
2712  O       o478    resource_defs p477 p478 p204  G       s1044   t583
2713  P       p479    Number 7667  B       b1045   s1044
2714  O       o479    uid p479 p478  T       t1045   o681 b1045
2715  T       t482    o479 b691  B       b1046   t1045
2716  B       b482    t482  T       t1046   o727 b588 b593 b832 b606
2717  T       t483    o b482 b4  H       h1046   y t1046
2718  B       b483    t483  P       p1046   Var C
2719  T       t491    o478 b483  O       o1046   var p1046
2720  B       b491    t491  B       b1047   t1041
2721  T       t492    o b491 b4  T       t1047   o1046 b1047
2722  B       b492    t492  S       s1047   t688 h h1040 h1041 h1046
2723  T       t500    o1036 b676 b1044 b688 b492  G       s1047   t1047
2724  B       b500    t500  B       b1048   s1047
2725  T       t501    o476 b500  T       t1048   o681 b1048
2726  B       b501    t501  B       b1049   t1048
2727  P       p8      Number 8056  S       s1049   t688 h h1040 h1041
2728  P       p16     Number 8796  G       s1049   t1047
2729  O       o16     location p8 p16  B       b1050   s1049
2730  P       p1053   String inv_id2  T       t1050   o681 b1050
2731  O       o1053   rule p1053  B       b1051   t1050
2732  P       p1070   String equiv_op_fun1  T       t1051   o680 b1049 b1051
2733  O       o1070   rule p1070  B       b1052   t1051
2734  T       t1070   o700 b597  T       t1052   o680 b1046 b1052
2735  S       s1070   t679 h  B       b1053   t1052
2736  G       s1070   t1070  T       t1053   o680 b1044 b1053
2737  B       b1070   s1070  B       b1054   t1053
2738  T       t1071   o677 b1070  T       t1054   o680 b1042 b1054
2739  B       b1071   t1071  B       b1055   t1054
 T       t1072   o700 b598  
 S       s1072   t679 h  
 G       s1072   t1072  
 B       b1072   s1072  
 T       t1073   o677 b1072  
 B       b1073   t1073  
 T       t1074   o736 b597 b591  
 S       s1074   t684 h  
 G       s1074   t1074  
 B       b1074   s1074  
 T       t1075   o677 b1074  
 B       b1075   t1075  
 T       t1076   o736 b598 b591  
 S       s1076   t684 h  
 G       s1076   t1076  
 B       b1076   s1076  
 T       t1077   o677 b1076  
 B       b1077   t1077  
 NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv  
 O       o1077   equiv_fun_prop  
 T       t1078   o596 b585 b818 b597  
 B       b1078   t1078  
 T       t1079   o596 b585 b818 b598  
 B       b1079   t1079  
 T       t1080   o761 b591 b759 b1078 b1079  
 B       b1080   t1080 z  
 T       t1081   o1077 b591 b759 b1080  
 S       s1081   t684 h  
 G       s1081   t1081  
 B       b1081   s1081  
 T       t1082   o677 b1081  
 B       b1082   t1082  
 T       t1083   o676 b1077 b1082  
 B       b1083   t1083  
 T       t1084   o676 b1075 b1083  
 B       b1084   t1084  
 T       t1085   o676 b763 b1084  
 B       b1085   t1085  
 T       t1086   o676 b700 b1085  
 B       b1086   t1086  
 T       t1087   o676 b682 b1086  
 B       b1087   t1087  
 T       t1088   o676 b761 b1087  
 B       b1088   t1088  
 T       t1089   o676 b1073 b1088  
 B       b1089   t1089  
 T       t1090   o676 b1071 b1089  
 B       b1090   t1090  
2740  NSummary!interactive    interactive     interactive Summary  NSummary!interactive    interactive     interactive Summary
2741  O       o1090   interactive  O       o1055   interactive
2742  NSummary!ext_rule       ext_rule        ext_rule Summary  NSummary!ext_rule       ext_rule        ext_rule Summary
2743  P       p1090   String "rwh unfold_equiv_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"  P       p1055   String "assertT << equiv{car{'g}; eqG{'g}; 's; id{'g}} >> ttca"
2744  O       o1091   ext_rule p1090  O       o1056   ext_rule p1055
2745  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  NSummary!status_incomplete      status_incomplete       status_incomplete Summary
2746  O       o1092   status_incomplete  O       o1057   status_incomplete
2747  T       t1092   o1092  T       t1057   o1057
2748  B       b1092   t1092  B       b1057   t1057
2749  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
2750  O       o1093   ext_unjustified  O       o1058   ext_unjustified
2751  NSummary!tactic_arg     tactic_arg      tactic_arg Summary  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
2752  P       p1093   String main  P       p1058   String main
2753  O       o1094   tactic_arg p1093  O       o1059   tactic_arg p1058
2754  NSummary!msequent       msequent        msequent Summary  NSummary!msequent       msequent        msequent Summary
2755  O       o1095   msequent  O       o1060   msequent
2756  T       t1095   o b1076 b4  T       t1060   o b1048 b4
2757  B       b1095   t1095  B       b1060   t1060
2758  T       t1096   o b1074 b1095  T       t1061   o b1045 b1060
2759  B       b1096   t1096  B       b1061   t1061
2760  T       t1097   o b762 b1096  T       t1062   o b1043 b1061
2761  B       b1097   t1097  B       b1062   t1062
2762  T       t1098   o b699 b1097  T       t1063   o b1041 b1062
2763  B       b1098   t1098  B       b1063   t1063
2764  T       t1099   o b681 b1098  T       t1064   o1060 b1050 b1063
2765  B       b1099   t1099  B       b1064   t1064
 T       t1100   o b760 b1099  
 B       b1100   t1100  
 T       t1101   o b1072 b1100  
 B       b1101   t1101  
 T       t1102   o b1070 b1101  
 B       b1102   t1102  
 T       t1103   o1095 b1081 b1102  
 B       b1103   t1103  
2766  NSummary!parent_none    parent_none     parent_none Summary  NSummary!parent_none    parent_none     parent_none Summary
2767  O       o1103   parent_none  O       o1064   parent_none
2768  T       t1104   o1103  T       t1065   o1064
2769  B       b1104   t1104  B       b1065   t1065
2770  T       t1105   o1094 b1103 b4 b1104  T       t1066   o1059 b1064 b4 b1065
2771  B       b1105   t1105  B       b1066   t1066
2772    P       p1066   String assertion
2773    O       o1066   tactic_arg p1066
2774    S       s1066   t688 h h1040 h1041
2775    G       s1066   t1046
2776    B       b1067   s1066
2777    T       t1067   o1060 b1067 b1063
2778    B       b1068   t1067
2779    T       t1068   o2 b1066
2780    B       b1069   t1068
2781    T       t1069   o1066 b1068 b4 b1069
2782    B       b1070   t1069
2783    T       t1070   o b1070 b4
2784    B       b1071   t1070
2785    T       t1071   o1058 b1066 b1071
2786    B       b1072   t1071
2787    P       p1072   String "equivSubstT << equiv{car{'g}; eqG{'g}; 's; op{'g; id{'g}; 's}} >> 0 ttca"
2788    O       o1072   ext_rule p1072
2789    T       t1072   o727 b588 b593 b832 b953
2790    S       s1072   t688 h h1040 h1041
2791    G       s1072   t1072
2792    B       b1073   s1072
2793    T       t1073   o1060 b1073 b1063
2794    B       b1074   t1073
2795    T       t1074   o2 b1070
2796    B       b1075   t1074
2797    T       t1075   o1066 b1074 b4 b1075
2798    B       b1076   t1075
2799    T       t1076   o727 b588 b593 b953 b606
2800    S       s1076   t688 h h1040 h1041
2801    G       s1076   t1076
2802    B       b1077   s1076
2803    T       t1077   o1060 b1077 b1063
2804    B       b1078   t1077
2805    T       t1078   o1066 b1078 b4 b1075
2806    B       b1079   t1078
2807    T       t1079   o b1079 b4
2808    B       b1080   t1079
2809    T       t1080   o b1076 b1080
2810    B       b1081   t1080
2811    T       t1081   o1058 b1070 b1081
2812    B       b1082   t1081
2813    P       p1082   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; id{'g}; 's}; 's} >> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
2814    O       o1082   ext_rule p1082
2815    T       t1082   o1058 b1076 b4
2816    B       b1083   t1082
2817    T       t1083   o1082 b1057 b1083 b4 b4
2818    B       b1084   t1083
2819    P       p1084   String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'g}; op{'g; inv{'g; 's}; 's}} >> 0 ttca"
2820    O       o1084   ext_rule p1084
2821    T       t1084   o611 b582 b832
2822    B       b1085   t1084
2823    T       t1085   o598 b582 b1085 b832
2824    B       b1086   t1085
2825    T       t1086   o727 b588 b593 b606 b1086
2826    S       s1086   t688 h h1040 h1041
2827    G       s1086   t1086
2828    B       b1087   s1086
2829    T       t1087   o1060 b1087 b1063
2830    B       b1088   t1087
2831    T       t1088   o2 b1079
2832    B       b1089   t1088
2833    T       t1089   o1066 b1088 b4 b1089
2834    B       b1090   t1089
2835    T       t1090   o598 b582 b1086 b832
2836    B       b1091   t1090
2837    T       t1091   o727 b588 b593 b1091 b1086
2838    S       s1091   t688 h h1040 h1041
2839    G       s1091   t1091
2840    B       b1092   s1091
2841    T       t1092   o1060 b1092 b1063
2842    B       b1093   t1092
2843    T       t1093   o1066 b1093 b4 b1089
2844    B       b1094   t1093
2845    NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv
2846    O       o1094   equiv_fun_prop
2847    B       b1095   t836
2848    T       t1095   o727 b588 b593 b1095 b835
2849    B       b1096   t1095 z
2850    T       t1096   o1094 b588 b593 b1096
2851    S       s1096   t688 h h1040 h1041
2852    G       s1096   t1096
2853    B       b1097   s1096
2854    T       t1097   o1060 b1097 b1063
2855    B       b1098   t1097
2856    T       t1098   o1066 b1098 b4 b1089
2857    B       b1099   t1098
2858    T       t1099   o b1099 b4
2859    B       b1100   t1099
2860    T       t1100   o b1094 b1100
2861    B       b1101   t1100
2862    T       t1101   o b1090 b1101
2863    B       b1102   t1101
2864    T       t1102   o1058 b1079 b1102
2865    B       b1103   t1102
2866    P       p1103   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT thenT rwh unfold_equiv 2 ttca"
2867    O       o1103   ext_rule p1103
2868    T       t1103   o1058 b1090 b4
2869    B       b1104   t1103
2870    T       t1104   o1103 b1057 b1104 b4 b4
2871    B       b1105   t1104
2872    P       p1105   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; inv{'g; 's}; 's}; 's}; op{'g; inv{'g; 's}; op{'g; 's; 's}}}>> 0 thenAT autoT thenT rwh unfold_equiv 2 ttca"
2873    O       o1105   ext_rule p1105
2874    T       t1105   o1058 b1094 b4
2875    B       b1106   t1105
2876    T       t1106   o1105 b1057 b1106 b4 b4
2877    B       b1107   t1106
2878    P       p1107   String "rwh unfold_equiv_fun_prop 0 thenT autoT"
2879    O       o1107   ext_rule p1107
2880  NCzf_itt_set!set        set     set Czf_itt_set  NCzf_itt_set!set        set     set Czf_itt_set
2881  O       o1105   set  O       o1108   set
 T       t1106   o1105  
 H       h1106   a_1 t1106  
 H       h1107   b_1 t1106  
 H       h1108   x t762  
 P       p1108   Var a_1  
 O       o1108   var p1108  
2882  T       t1108   o1108  T       t1108   o1108
2883  B       b1108   t1108  H       h1108   a t1108
2884  P       p1109   Var b_1  H       h1109   b t1108
2885  O       o1109   var p1109  H       h1110   x_1 t727
2886  T       t1109   o1109  T       t1110   o727 b588 b593 b599 b600
2887  B       b1109   t1109  H       h1111   x_2 t1110
2888  T       t1110   o761 b591 b759 b1108 b1109  T       t1111   o598 b582 b599 b832
 H       h1110   x_1 t1110  
 T       t1111   o596 b585 b1108 b597  
2889  B       b1111   t1111  B       b1111   t1111
2890  T       t1112   o596 b585 b1108 b598  T       t1112   o727 b588 b593 b1111 b599
2891  B       b1112   t1112  H       h1112   x_3 t1112
2892  T       t1113   o761 b591 b759 b1111 b1112  T       t1113   o598 b582 b600 b832
2893  H       h1113   x_2 t1113  B       b1113   t1113
2894  T       t1114   o596 b585 b1109 b597  T       t1114   o727 b588 b593 b1113 b600
2895  B       b1114   t1114  S       s1114   t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
2896  T       t1115   o596 b585 b1109 b598  G       s1114   t1114
2897    B       b1114   s1114
2898    T       t1115   o1060 b1114 b1063
2899  B       b1115   t1115  B       b1115   t1115
 T       t1116   o761 b591 b759 b1114 b1115  
 S       s1116   t684 h h1106 h1107 h1108 h1110 h1113  
 G       s1116   t1116  
 B       b1116   s1116  
 T       t1117   o1095 b1116 b1102  
 B       b1117   t1117  
2900  NItt_logic      Itt_logic       Itt_logic NIL  NItt_logic      Itt_logic       Itt_logic NIL
2901  NItt_logic!implies      implies implies Itt_logic  NItt_logic!implies      implies implies Itt_logic
2902  O       o1117   implies  O       o1115   implies
2903  B       b1118   t1113  B       b1116   t1112
2904  B       b1119   t1116  B       b1117   t1114
2905  T       t1119   o1117 b1118 b1119  T       t1117   o1115 b1116 b1117
2906  S       s1119   t684 h h1106 h1107 h1108 h1110  S       s1117   t688 h h1040 h1041 h1108 h1109 h1110 h1111
2907  G       s1119   t1119  G       s1117   t1117
2908  B       b1120   s1119  B       b1118   s1117
2909  T       t1120   o1095 b1120 b1102  T       t1118   o1060 b1118 b1063
2910  B       b1121   t1120  B       b1119   t1118
2911  B       b1122   t1110  NSummary!arg_named      arg_named       arg_named Summary
2912  B       b1123   t1119  P       p1119   String d_auto
2913  T       t1123   o1117 b1122 b1123  O       o1119   arg_named p1119
2914  S       s1123   t684 h h1106 h1107 h1108  NSummary!arg_bool       arg_bool        arg_bool Summary
2915  G       s1123   t1123  P       p1120   String true
2916  B       b1124   s1123  O       o1120   arg_bool p1120
2917  T       t1124   o1095 b1124 b1102  T       t1120   o1120
2918  B       b1125   t1124  B       b1120   t1120
2919  B       b1126   t762  T       t1121   o1119 b1120
2920  B       b1127   t1123  B       b1121   t1121
2921  T       t1127   o1117 b1126 b1127  T       t1122   o b1121 b4
2922  S       s1127   t684 h h1106 h1107  B       b1122   t1122
2923  G       s1127   t1127  B       b1123   t1110
2924  B       b1128   s1127  B       b1124   t1117
2925  T       t1128   o1095 b1128 b1102  T       t1124   o1115 b1123 b1124
2926  B       b1129   t1128  S       s1124   t688 h h1040 h1041 h1108 h1109 h1110
2927    G       s1124   t1124
2928    B       b1125   s1124
2929    T       t1125   o1060 b1125 b1063
2930    B       b1126   t1125
2931    B       b1127   t727
2932    B       b1128   t1124
2933    T       t1128   o1115 b1127 b1128
2934    S       s1128   t688 h h1040 h1041 h1108 h1109
2935    G       s1128   t1128
2936    B       b1129   s1128
2937    T       t1129   o1060 b1129 b1063
2938    B       b1130   t1129
2939  NItt_logic!all  all     all Itt_logic  NItt_logic!all  all     all Itt_logic
2940  O       o1129   all  O       o1130   all
2941  B       b1130   t1106  B       b1131   t1108
2942  B       b1131   t1127 b_1  B       b1132   t1128 b
2943  T       t1131   o1129 b1130 b1131  T       t1132   o1130 b1131 b1132
2944  S       s1131   t684 h h1106  S       s1132   t688 h h1040 h1041 h1108
2945  G       s1131   t1131  G       s1132   t1132
2946  B       b1132   s1131  B       b1133   s1132
2947  T       t1132   o1095 b1132 b1102  T       t1133   o1060 b1133 b1063
2948  B       b1133   t1132  B       b1134   t1133
2949  B       b1134   t1131 a_1  B       b1135   t1132 a
2950  T       t1134   o1129 b1130 b1134  T       t1135   o1130 b1131 b1135
2951  S       s1134   t684 h  S       s1135   t688 h h1040 h1041
2952  G       s1134   t1134  G       s1135   t1135
2953  B       b1135   s1134  B       b1136   s1135
2954  T       t1135   o1095 b1135 b1102  T       t1136   o1060 b1136 b1063
 B       b1136   t1135  
 T       t1136   o2 b1105  
2955  B       b1137   t1136  B       b1137   t1136
2956  T       t1137   o1094 b1136 b4 b1137  T       t1137   o2 b1099
2957  B       b1138   t1137  B       b1138   t1137
2958  T       t1138   o2 b1138  T       t1138   o1066 b1137 b1122 b1138
2959  B       b1139   t1138  B       b1139   t1138
2960  T       t1139   o1094 b1133 b4 b1139  T       t1139   o2 b1139
2961  B       b1140   t1139  B       b1140   t1139
2962  T       t1140   o2 b1140  T       t1140   o1059 b1134 b1122 b1140
2963  B       b1141   t1140  B       b1141   t1140
2964  T       t1141   o1094 b1129 b4 b1141  T       t1141   o2 b1141
2965  B       b1142   t1141  B       b1142   t1141
2966  T       t1142   o2 b1142  T       t1142   o1059 b1130 b1122 b1142
2967  B       b1143   t1142  B       b1143   t1142
2968  T       t1143   o1094 b1125 b4 b1143  T       t1143   o2 b1143
2969  B       b1144   t1143  B       b1144   t1143
2970  T       t1144   o2 b1144  T       t1144   o1059 b1126 b1122 b1144
2971  B       b1145   t1144  B       b1145   t1144
2972  T       t1145   o1094 b1121 b4 b1145  T       t1145   o2 b1145
2973  B       b1146   t1145  B       b1146   t1145
2974  T       t1146   o2 b1146  T       t1146   o1059 b1119 b1122 b1146
2975  B       b1147   t1146  B       b1147   t1146
2976  T       t1147   o1094 b1117 b4 b1147  T       t1147   o2 b1147
2977  B       b1148   t1147  B       b1148   t1147
2978  T       t1148   o b1148 b4  T       t1148   o1059 b1115 b4 b1148
2979  B       b1149   t1148  B       b1149   t1148
2980  T       t1149   o1093 b1105 b1149  T       t1149   o b1149 b4
2981  B       b1150   t1149  B       b1150   t1149
2982  P       p1150   String "equivTransT << op{'g; 'b_1; 'a} >> 6 ttca thenT rwh unfold_equiv 6 ttca"  T       t1150   o1058 b1099 b1150
2983  O       o1150   ext_rule p1150  B       b1151   t1150
2984  NItt_logic!and  and     and Itt_logic  P       p1151   String "equivTransT << op{'g; 'a; 's} >> thenT autoT thenT rwh unfold_equiv 2 thenT rwh unfold_equiv 7 ttca thenT rwh fold_equiv 2 thenT rwh fold_equiv 7"
2985  O       o1151   and  O       o1151   ext_rule p1151
2986  B       b1151   t700  T       t1151   o727 b588 b593 b600 b599
2987  B       b1152   t760  S       s1151   t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
2988  T       t1152   o700 b1111  G       s1151   t1151
2989    B       b1152   s1151
2990    T       t1152   o1060 b1152 b1063
2991  B       b1153   t1152  B       b1153   t1152
2992  T       t1153   o700 b1112  NItt_logic!and  and     and Itt_logic
2993  B       b1154   t1153  O       o1153   and
2994  T       t1154   o1151 b1153 b1154  B       b1154   t704
2995  B       b1155   t1154  B       b1155   t715
2996  T       t1155   o1151 b1152 b1155  T       t1155   o704 b599
2997  B       b1156   t1155  B       b1156   t1155
2998  T       t1156   o1151 b1151 b1156  T       t1156   o704 b600
2999  B       b1157   t1156  B       b1157   t1156
3000  T       t1157   o736 b1111 b591  T       t1157   o1153 b1156 b1157
3001  B       b1158   t1157  B       b1158   t1157
3002  T       t1158   o736 b1112 b591  T       t1158   o1153 b1155 b1158
3003  B       b1159   t1158  B       b1159   t1158
3004  T       t1159   o1151 b1158 b1159  T       t1159   o1153 b1154 b1159
3005  B       b1160   t1159  B       b1160   t1159
3006  T       t1160   o1151 b1157 b1160  T       t1160   o761 b599 b588
3007  B       b1161   t1160  B       b1161   t1160
3008  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL  T       t1161   o761 b600 b588
 NCzf_itt_pair!pair      pair    pair Czf_itt_pair  
 O       o1161   pair  
 T       t1161   o1161 b1111 b1112  
3009  B       b1162   t1161  B       b1162   t1161
3010  T       t1162   o736 b1162 b759  T       t1162   o1153 b1161 b1162
3011  B       b1163   t1162  B       b1163   t1162
3012  T       t1163   o1151 b1161 b1163  T       t1163   o1153 b1160 b1163
3013  H       h1163   x_2 t1163  B       b1164   t1163
3014  T       t1164   o736 b1114 b591  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL
3015  S       s1164   t684 h h1106 h1107 h1108 h1110 h1163  NCzf_itt_pair!pair      pair    pair Czf_itt_pair
3016  G       s1164   t1164  O       o1164   pair
3017  B       b1164   s1164  T       t1164   o1164 b599 b600
3018  T       t1165   o1095 b1164 b1102  B       b1165   t1164
3019  B       b1165   t1165  T       t1165   o761 b1165 b593
3020  S       s1165   t684 h h1106 h1107 h1108 h1110 h1113  B       b1166   t1165
3021  G       s1165   t1164  T       t1166   o1153 b1164 b1166
3022  B       b1166   s1165  H       h1166   x_2 t1166
3023  T       t1166   o1095 b1166 b1102  S       s1166   t688 h h1040 h1041 h1108 h1109 h1110 h1166 h1112
3024  B       b1167   t1166  G       s1166   t1151
3025  T       t1167   o2 b1148  B       b1167   s1166
3026    T       t1167   o1060 b1167 b1063
3027  B       b1168   t1167  B       b1168   t1167
3028  T       t1168   o1094 b1167 b4 b1168  T       t1168   o704 b1039
3029  B       b1169   t1168  B       b1169   t1168
3030  T       t1169   o2 b1169  B       b1170   t833
3031  B       b1170   t1169  T       t1170   o1153 b1169 b1170
 T       t1170   o1094 b1165 b4 b1170  
3032  B       b1171   t1170  B       b1171   t1170
3033  T       t1171   o761 b591 b759 b1111 b1114  T       t1171   o1153 b1155 b1171
3034  H       h1171   u t1171  B       b1172   t1171
3035  T       t1172   o761 b591 b759 b1114 b1112  T       t1172   o1153 b1154 b1172
3036  H       h1172   v t1172  B       b1173   t1172
3037  S       s1172   t684 h h1106 h1107 h1108 h1110 h1163 h1171 h1172  T       t1173   o761 b1039 b588
3038  G       s1172   t1116  B       b1174   t1173
3039  B       b1172   s1172  B       b1175   t951
3040  T       t1173   o1095 b1172 b1102  T       t1175   o1153 b1174 b1175
 B       b1173   t1173  
 S       s1173   t684 h h1106 h1107 h1108 h1110 h1113 h1171 h1172  
 G       s1173   t1116  
 B       b1174   s1173  
 T       t1174   o1095 b1174 b1102  
 B       b1175   t1174  
 T       t1175   o1094 b1175 b4 b1168  
3041  B       b1176   t1175  B       b1176   t1175
3042  T       t1176   o2 b1176  T       t1176   o1153 b1173 b1176
3043  B       b1177   t1176  B       b1177   t1176
3044  T       t1177   o1094 b1173 b4 b1177  T       t1177   o1164 b1039 b832
3045  B       b1178   t1177  B       b1178   t1177
3046  T       t1178   o b1178 b4  T       t1178   o761 b1178 b593
3047  B       b1179   t1178  B       b1179   t1178
3048  T       t1179   o b1171 b1179  T       t1179   o1153 b1177 b1179
3049  B       b1180   t1179  H       h1179   x t1179
3050  T       t1180   o1093 b1148 b1180  S       s1179   t688 h h1179 h1041 h1108 h1109 h1110 h1166 h1112
3051    G       s1179   t1151
3052    B       b1180   s1179
3053    T       t1180   o1060 b1180 b1063
3054  B       b1181   t1180  B       b1181   t1180
3055  P       p1181   String "autoT thenT rwh unfold_equiv 5 ttca"  S       s1181   t688 h h1179 h1041 h1108 h1109 h1110 h1111 h1112
3056  O       o1181   ext_rule p1181  G       s1181   t1151
3057  T       t1181   o1093 b1171 b4  B       b1182   s1181
3058  B       b1182   t1181  T       t1182   o1060 b1182 b1063
 T       t1182   o1181 b1092 b1182 b4 b4  
3059  B       b1183   t1182  B       b1183   t1182
3060  P       p1183   String "equivTransT << op{'g; 'b_1; 'b} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"  T       t1183   o727 b588 b593 b1113 b1111
3061  O       o1183   ext_rule p1183  S       s1183   t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
3062  T       t1183   o1093 b1178 b4  G       s1183   t1183
3063  B       b1184   t1183  B       b1184   s1183
3064  T       t1184   o1183 b1092 b1184 b4 b4  T       t1184   o1060 b1184 b1063
3065  B       b1185   t1184  B       b1185   t1184
3066  T       t1185   o b1185 b4  T       t1185   o2 b1149
3067  B       b1186   t1185  B       b1186   t1185
3068  T       t1186   o b1183 b1186  T       t1186   o1059 b1185 b1122 b1186
3069  B       b1187   t1186  B       b1187   t1186
3070  T       t1187   o1150 b1092 b1181 b1187 b4  T       t1187   o2 b1187
3071  B       b1188   t1187  B       b1188   t1187
3072  T       t1188   o b1188 b4  T       t1188   o1059 b1153 b4 b1188
3073  B       b1189   t1188  B       b1189   t1188
3074  T       t1189   o1091 b1092 b1150 b1189 b4  T       t1189   o2 b1189
3075  B       b1190   t1189  B       b1190   t1189
3076  T       t1190   o1090 b1190  T       t1190   o1059 b1183 b4 b1190
3077  B       b1191   t1190  B       b1191   t1190
3078  P       p1200   String equiv_op_fun2  T       t1191   o2 b1191
3079  O       o1200   rule p1200  B       b1192   t1191
3080  T       t1200   o596 b585 b597 b818  T       t1192   o1059 b1181 b4 b1192
3081  B       b1200   t1200  B       b1193   t1192
3082  T       t1201   o596 b585 b598 b818  T       t1193   o2 b1193
3083  B       b1201   t1201  B       b1194   t1193
3084  T       t1202   o761 b591 b759 b1200 b1201  T       t1194   o1059 b1168 b4 b1194
3085  B       b1202   t1202 z  B       b1195   t1194
3086  T       t1203   o1077 b591 b759 b1202  T       t1195   o2 b1195
3087  S       s1203   t684 h  B       b1196   t1195
3088  G       s1203   t1203  T       t1196   o1059 b1153 b4 b1196
3089  B       b1203   s1203  B       b1197   t1196
3090  T       t1204   o677 b1203  T       t1197   o727 b588 b593 b1111 b600
3091  B       b1204   t1204  S       s1197   t688 h h1040 h1041 h1108 h1109 h1110 h1111 h1112
3092  T       t1205   o676 b1077 b1204  G       s1197   t1197
3093  B       b1205   t1205  B       b1198   s1197
3094  T       t1206   o676 b1075 b1205  T       t1198   o1060 b1198 b1063
3095  B       b1206   t1206  B       b1199   t1198
3096  T       t1207   o676 b763 b1206  S       s1199   t688 h h1040 h1041 h1108 h1109 h1110 h1166 h1112
3097  B       b1207   t1207  G       s1199   t1197
3098  T       t1208   o676 b700 b1207  B       b1200   s1199
3099  B       b1208   t1208  T       t1200   o1060 b1200 b1063
3100  T       t1209   o676 b682 b1208  B       b1201   t1200
3101  B       b1209   t1209  S       s1201   t688 h h1179 h1041 h1108 h1109 h1110 h1166 h1112
3102  T       t1210   o676 b761 b1209  G       s1201   t1197
3103  B       b1210   t1210  B       b1202   s1201
3104  T       t1211   o676 b1073 b1210  T       t1202   o1060 b1202 b1063
3105  B       b1211   t1211  B       b1203   t1202
3106  T       t1212   o676 b1071 b1211  S       s1203   t688 h h1179 h1041 h1108 h1109 h1110 h1111 h1112
3107  B       b1212   t1212  G       s1203   t1197
3108  T       t1213   o1095 b1203 b1102  B       b1204   s1203
3109  B       b1213   t1213  T       t1204   o1060 b1204 b1063
3110  T       t1214   o1094 b1213 b4 b1104  B       b1205   t1204
3111  B       b1214   t1214  T       t1205   o1059 b1199 b4 b1186
3112  T       t1215   o596 b585 b597 b1108  B       b1206   t1205
3113  B       b1215   t1215  T       t1206   o2 b1206
3114  T       t1216   o596 b585 b598 b1108  B       b1207   t1206
3115  B       b1216   t1216  T       t1207   o1059 b1205 b4 b1207
3116  T       t1217   o761 b591 b759 b1215 b1216  B       b1208   t1207
3117  H       h1217   x_2 t1217  T       t1208   o2 b1208
3118  T       t1218   o596 b585 b597 b1109  B       b1209   t1208
3119  B       b1218   t1218  T       t1209   o1059 b1203 b4 b1209
3120  T       t1219   o596 b585 b598 b1109  B       b1210   t1209
3121  B       b1219   t1219  T       t1210   o2 b1210
3122  T       t1220   o761 b591 b759 b1218 b1219  B       b1211   t1210
3123  S       s1220   t684 h h1106 h1107 h1108 h1110 h1217  T       t1211   o1059 b1201 b4 b1211
3124  G       s1220   t1220  B       b1212   t1211
3125  B       b1220   s1220  T       t1212   o2 b1212
3126  T       t1221   o1095 b1220 b1102  B       b1213   t1212
3127  B       b1221   t1221  T       t1213   o1059 b1199 b4 b1213
3128  B       b1222   t1217  B       b1214   t1213
3129  B       b1223   t1220  T       t1214   o b1214 b4
3130  T       t1223   o1117 b1222 b1223  B       b1215   t1214
3131  S       s1223   t684 h h1106 h1107 h1108 h1110  T       t1215   o b1197 b1215
3132  G       s1223   t1223  B       b1216   t1215
3133  B       b1224   s1223  T       t1216   o1058 b1149 b1216
3134  T       t1224   o1095 b1224 b1102  B       b1217   t1216
3135    P       p1217   String "equivSymT ttca thenT rwh unfold_equiv 7 ttca"
3136    O       o1217   ext_rule p1217
3137    T       t1217   o1058 b1197 b4
3138    B       b1218   t1217
3139    T       t1218   o1217 b1057 b1218 b4 b4
3140    B       b1219   t1218
3141    P       p1219   String "equivTransT << 'a >> ttca thenT rwh unfold_equiv 7 thenT rwh unfold_equiv 8 ttca"
3142    O       o1219   ext_rule p1219
3143    T       t1219   o1058 b1214 b4
3144    B       b1220   t1219
3145    T       t1220   o1219 b1057 b1220 b4 b4
3146    B       b1221   t1220
3147    T       t1221   o b1221 b4
3148    B       b1222   t1221
3149    T       t1222   o b1219 b1222
3150    B       b1223   t1222
3151    T       t1223   o1151 b1057 b1217 b1223 b4
3152    B       b1224   t1223
3153    T       t1224   o b1224 b4
3154  B       b1225   t1224  B       b1225   t1224
3155  B       b1226   t1223  T       t1225   o1107 b1057 b1151 b1225 b4
3156  T       t1226   o1117 b1122 b1226  B       b1226   t1225
3157  S       s1226   t684 h h1106 h1107 h1108  T       t1226   o b1226 b4
3158  G       s1226   t1226  B       b1227   t1226
3159  B       b1227   s1226  T       t1227   o b1107 b1227
 T       t1227   o1095 b1227 b1102  
3160  B       b1228   t1227  B       b1228   t1227
3161  B       b1229   t1226  T       t1228   o b1105 b1228
3162  T       t1229   o1117 b1126 b1229  B       b1229   t1228
3163  S       s1229   t684 h h1106 h1107  T       t1229   o1084 b1057 b1103 b1229 b4
3164  G       s1229   t1229  B       b1230   t1229
3165  B       b1230   s1229  T       t1230   o b1230 b4
 T       t1230   o1095 b1230 b1102  
3166  B       b1231   t1230  B       b1231   t1230
3167  B       b1232   t1229 b_1  T       t1231   o b1084 b1231
3168  T       t1232   o1129 b1130 b1232  B       b1232   t1231
3169  S       s1232   t684 h h1106  T       t1232   o1072 b1057 b1082 b1232 b4
3170  G       s1232   t1232  B       b1233   t1232
3171  B       b1233   s1232  T       t1233   o b1233 b4
 T       t1233   o1095 b1233 b1102  
3172  B       b1234   t1233  B       b1234   t1233
3173  B       b1235   t1232 a_1  T       t1234   o1056 b1057 b1072 b1234 b4
3174  T       t1235   o1129 b1130 b1235  B       b1235   t1234
3175  S       s1235   t684 h  T       t1235   o1055 b1235
3176  G       s1235   t1235  B       b1236   t1235
3177  B       b1236   s1235  P       p1236   Number 8488
3178  T       t1236   o1095 b1236 b1102  P       p1237   Number 8495
3179  B       b1237   t1236  O       o1237   resource_defs p1236 p1237 p176
3180  T       t1237   o2 b1214  P       p1238   Number 8493
3181  B       b1238   t1237  O       o1238   uid p1238 p1237
3182  T       t1238   o1094 b1237 b4 b1238  T       t1238   o1238 b695
3183  B       b1239   t1238  B       b1238   t1238
3184  T       t1239   o2 b1239  T       t1239   o b1238 b4
3185  B       b1240   t1239  B       b1239   t1239
3186  T       t1240   o1094 b1234 b4 b1240  T       t1240   o1237 b1239
3187  B       b1241   t1240  B       b1240   t1240
3188  T       t1241   o2 b1241  T       t1241   o b1240 b4
3189  B       b1242   t1241  B       b1241   t1241
3190  T       t1242   o1094 b1231 b4 b1242  T       t1242   o1035 b1038 b1055 b1236 b1241
3191  B       b1243   t1242  B       b1242   t1242
3192  T       t1243   o2 b1243  T       t1243   o1034 b1242
3193  B       b1244   t1243  B       b1243   t1243
3194  T       t1244   o1094 b1228 b4 b1244  P       p1243   Number 9034
3195  B       b1245   t1244  P       p1244   Number 9338
3196  T       t1245   o2 b1245  O       o1244   location p1243 p1244
3197  B       b1246   t1245  P       p1245   String inv_id2
3198  T       t1246   o1094 b1225 b4 b1246  O       o1245   rule p1245
3199  B       b1247   t1246  T       t1245   o598 b582 b832 b1085
3200  T       t1247   o2 b1247  B       b1245   t1245
3201  B       b1248   t1247  T       t1246   o727 b588 b593 b1245 b606
3202  T       t1248   o1094 b1221 b4 b1248  S       s1246   t688 h
3203  B       b1249   t1248  G       s1246   t1246
3204  T       t1249   o b1249 b4  B       b1246   s1246
3205  B       b1250   t1249  T       t1247   o681 b1246
3206  T       t1250   o1093 b1214 b1250  B       b1247   t1247
3207  B       b1251   t1250  T       t1248   o680 b952 b1247
3208  P       p1251   String "equivTransT << op{'g; 'a; 'b_1} >> 6 ttca thenT rwh unfold_equiv 6 ttca"  B       b1248   t1248
3209    T       t1249   o680 b727 b1248
3210    B       b1249   t1249
3211    T       t1250   o680 b686 b1249
3212    B       b1250   t1250
3213    T       t1251   o680 b834 b1250
3214    B       b1251   t1251
3215    P       p1251   String "assertT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's; inv{'g; 's}}; op{'g; 's; inv{'g; 's}}}; op{'g; 's; inv{'g; 's}}} >> ttca"
3216  O       o1251   ext_rule p1251  O       o1251   ext_rule p1251
3217  T       t1251   o700 b1215  T       t1252   o b951 b4
3218  B       b1252   t1251  B       b1252   t1252
3219  T       t1252   o700 b1216  T       t1253   o b726 b1252
3220  B       b1253   t1252  B       b1253   t1253
3221  T       t1253   o1151 b1252 b1253  T       t1254   o b685 b1253
3222  B       b1254   t1253  B       b1254   t1254
3223  T       t1254   o1151 b1152 b1254  T       t1255   o b833 b1254
3224  B       b1255   t1254  B       b1255   t1255
3225  T       t1255   o1151 b1151 b1255  T       t1256   o1060 b1246 b1255
3226  B       b1256   t1255  B       b1256   t1256
3227  T       t1256   o736 b1215 b591  T       t1257   o1059 b1256 b4 b1065
3228  B       b1257   t1256  B       b1257   t1257
3229  T       t1257   o736 b1216 b591  T       t1258   o598 b582 b1245 b1245
3230  B       b1258   t1257  B       b1258   t1258
3231  T       t1258   o1151 b1257 b1258  T       t1259   o727 b588 b593 b1258 b1245
3232  B       b1259   t1258  S       s1259   t688 h
3233  T       t1259   o1151 b1256 b1259  G       s1259   t1259
3234  B       b1260   t1259  B       b1259   s1259
3235  T       t1260   o1161 b1215 b1216  T       t1260   o1060 b1259 b1255
3236  B       b1261   t1260  B       b1260   t1260
3237  T       t1261   o736 b1261 b759  T       t1261   o2 b1257
3238  B       b1262   t1261  B       b1261   t1261
3239  T       t1262   o1151 b1260 b1262  T       t1262   o1066 b1260 b4 b1261
3240  H       h1262   x_2 t1262  B       b1262   t1262
3241  T       t1263   o736 b1218 b591  H       h1262   v t1259
3242  S       s1263   t684 h h1106 h1107 h1108 h1110 h1262  S       s1262   t688 h h1262
3243  G       s1263   t1263  G       s1262   t1246
3244  B       b1263   s1263  B       b1263   s1262
3245  T       t1264   o1095 b1263 b1102  T       t1263   o1060 b1263 b1255
3246  B       b1264   t1264  B       b1264   t1263
3247  S       s1264   t684 h h1106 h1107 h1108 h1110 h1217  T       t1264   o1059 b1264 b4 b1261
3248  G       s1264   t1263  B       b1265   t1264
3249  B       b1265   s1264  T       t1265   o b1265 b4
 T       t1265   o1095 b1265 b1102  
3250  B       b1266   t1265  B       b1266   t1265
3251  T       t1266   o2 b1249  T       t1266   o b1262 b1266
3252  B       b1267   t1266  B       b1267   t1266
3253  T       t1267   o1094 b1266 b4 b1267  T       t1267   o1058 b1257 b1267
3254  B       b1268   t1267  B       b1268   t1267
3255  T       t1268   o2 b1268  P       p1268   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; 's; inv{'g; 's}}; op{'g; 's; inv{'g; 's}}}; op{'g; 's; op{'g; inv{'g; 's}; op{'g; 's; inv{'g; 's}}}}} >> 0 ttca"
3256    O       o1268   ext_rule p1268
3257    T       t1268   o598 b582 b1085 b1245
3258  B       b1269   t1268  B       b1269   t1268
3259  T       t1269   o1094 b1264 b4 b1269  T       t1269   o598 b582 b832 b1269
3260  B       b1270   t1269  B       b1270   t1269
3261  T       t1270   o761 b591 b759 b1215 b1218  T       t1270   o727 b588 b593 b1270 b1245
3262  H       h1270   u t1270  S       s1270   t688 h
3263  T       t1271   o761 b591 b759 b1218 b1216  G       s1270   t1270
3264  H       h1271   v t1271  B       b1271   s1270
3265  S       s1271   t684 h h1106 h1107 h1108 h1110 h1262 h1270 h1271  T       t1271   o1060 b1271 b1255
3266  G       s1271   t1220  B       b1272   t1271
3267  B       b1271   s1271  T       t1272   o2 b1262
3268  T       t1272   o1095 b1271 b1102  B       b1273   t1272
3269  B       b1272   t1272  T       t1273   o1066 b1272 b4 b1273
 S       s1272   t684 h h1106 h1107 h1108 h1110 h1217 h1270 h1271  
 G       s1272   t1220  
 B       b1273   s1272  
 T       t1273   o1095 b1273 b1102  
3270  B       b1274   t1273  B       b1274   t1273
3271  T       t1274   o1094 b1274 b4 b1267  T       t1274   o b1274 b4
3272  B       b1275   t1274  B       b1275   t1274
3273  T       t1275   o2 b1275  T       t1275   o1058 b1262 b1275
3274  B       b1276   t1275  B       b1276   t1275
3275  T       t1276   o1094 b1272 b4 b1276  P       p1276   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; op{'g; inv{'g; 's}; op{'g; 's; inv{'g; 's}}}}; op{'g; 's; op{'g; op{'g; inv{'g; 's}; 's}; inv{'g; 's}}}} >> 0 ttca"
3276    O       o1276   ext_rule p1276
3277    T       t1276   o598 b582 b1086 b1085
3278  B       b1277   t1276  B       b1277   t1276
3279  T       t1277   o b1277 b4  T       t1277   o598 b582 b832 b1277
3280  B       b1278   t1277  B       b1278   t1277
3281  T       t1278   o b1270 b1278  T       t1278   o727 b588 b593 b1278 b1245
3282  B       b1279   t1278  S       s1278   t688 h
3283  T       t1279   o1093 b1249 b1279  G       s1278   t1278
3284    B       b1279   s1278
3285    T       t1279   o1060 b1279 b1255
3286  B       b1280   t1279  B       b1280   t1279
3287  T       t1280   o1093 b1270 b4  T       t1280   o2 b1274
3288  B       b1281   t1280  B       b1281   t1280
3289  T       t1281   o1181 b1092 b1281 b4 b4  T       t1281   o1066 b1280 b4 b1281
3290  B       b1282   t1281  B       b1282   t1281
3291  P       p1282   String "equivTransT << op{'g; 'b; 'b_1} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"  T       t1282   o b1282 b4
 O       o1282   ext_rule p1282  
 T       t1282   o1093 b1277 b4  
3292  B       b1283   t1282  B       b1283   t1282
3293  T       t1283   o1282 b1092 b1283 b4 b4  T       t1283   o1058 b1274 b1283
3294  B       b1284   t1283  B       b1284   t1283
3295  T       t1284   o b1284 b4  P       p1284   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; inv{'g; 's}; 's}; id{'g}} >> 0 thenT autoT"
3296    O       o1284   ext_rule p1284
3297    T       t1284   o598 b582 b835 b1085
3298  B       b1285   t1284  B       b1285   t1284
3299  T       t1285   o b1282 b1285  T       t1285   o598 b582 b832 b1285
3300  B       b1286   t1285  B       b1286   t1285 z
3301  T       t1286   o1251 b1092 b1280 b1286 b4  T       t1286   o834 b588 b593 b1286
3302  B       b1287   t1286  S       s1286   t688 h
3303  T       t1287   o b1287 b4  G       s1286   t1286
3304    B       b1287   s1286
3305    T       t1287   o1060 b1287 b1255
3306  B       b1288   t1287  B       b1288   t1287
3307  T       t1288   o1091 b1092 b1251 b1288 b4  B       b1289   t1285
3308  B       b1289   t1288  T       t1289   o727 b588 b593 b1289 b1245
3309  T       t1289   o1090 b1289  B       b1290   t1289 z
3310  B       b1290   t1289  T       t1290   o1094 b588 b593 b1290
3311  P       p1299   String cancel1  S       s1290   t688 h
3312  O       o1299   rule p1299  G       s1290   t1290
3313  P       p1300   String J  B       b1291   s1290
3314  O       o1300   context_param p1300  T       t1291   o1060 b1291 b1255
3315  T       t1300   o1300  B       b1292   t1291
3316  B       b1300   t1300  T       t1292   o2 b1282
3317  T       t1301   o b1300 b4  B       b1293   t1292
3318  B       b1301   t1301  T       t1293   o1066 b1292 b1122 b1293
3319  T       t1302   o b675 b1301  B       b1294   t1293
3320  B       b1302   t1302  T       t1294   o2 b1294
3321  T       t1303   o761 b591 b759 b720 b791  B       b1295   t1294
3322  H       h1303   x t1303  T       t1295   o1066 b1288 b4 b1295
3323  P       p1303   Var x  B       b1296   t1295
3324  O       o1303   var p1303  T       t1296   o b1296 b4
3325  T       t1304   o1303  B       b1297   t1296
3326  C       h1304   J t1304  T       t1297   o1058 b1282 b1297
3327  S       s1304   t679 h h1303 h1304  B       b1298   t1297
3328  G       s1304   t715  P       p1298   String "rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 5 ttca"
3329  B       b1304   s1304  O       o1298   ext_rule p1298
3330  T       t1305   o677 b1304  T       t1298   o1058 b1296 b4
3331  B       b1305   t1305  B       b1299   t1298
3332  S       s1305   t679 h h1303 h1304  T       t1299   o1298 b1057 b1299 b4 b4
3333  G       s1305   t718  B       b1300   t1299
3334  B       b1306   s1305  T       t1300   o b1300 b4
3335  T       t1306   o677 b1306  B       b1301   t1300
3336    T       t1301   o1284 b1057 b1298 b1301 b4
3337    B       b1302   t1301
3338    T       t1302   o b1302 b4
3339    B       b1303   t1302
3340    T       t1303   o1276 b1057 b1284 b1303 b4
3341    B       b1304   t1303
3342    T       t1304   o b1304 b4
3343    B       b1305   t1304
3344    T       t1305   o1268 b1057 b1276 b1305 b4
3345    B       b1306   t1305
3346    P       p1306   String "dT 2 ttca"
3347    O       o1306   ext_rule p1306
3348    T       t1306   o1058 b1265 b4
3349  B       b1307   t1306  B       b1307   t1306
3350  S       s1307   t679 h h1303 h1304  T       t1307   o1306 b1057 b1307 b4 b4
3351  G       s1307   t757  B       b1308   t1307
3352  B       b1308   s1307  T       t1308   o b1308 b4
 T       t1308   o677 b1308  
3353  B       b1309   t1308  B       b1309   t1308
3354  S       s1309   t679 h h1303 h1304  T       t1309   o b1306 b1309
3355  G       s1309   t760  B       b1310   t1309
3356  B       b1310   s1309  T       t1310   o1251 b1057 b1268 b1310 b4
 T       t1310   o677 b1310  
3357  B       b1311   t1310  B       b1311   t1310
3358  S       s1311   t679 h h1303 h1304  T       t1311   o1055 b1311
3359  G       s1311   t681  B       b1312   t1311
3360  B       b1312   s1311  P       p1312   Number 9057
3361  T       t1312   o677 b1312  P       p1313   Number 9064
3362  B       b1313   t1312  O       o1313   resource_defs p1312 p1313 p204
3363  S       s1313   t684 h h1303 h1304  P       p1314   Number 9062
3364  G       s1313   t586  O       o1314   uid p1314 p1313
3365  B       b1314   s1313  T       t1314   o1314 b695
3366  T       t1314   o677 b1314  B       b1314   t1314
3367  B       b1315   t1314  T       t1315   o b1314 b4
3368  S       s1315   t684 h h1303 h1304  B       b1315   t1315
3369  G       s1315   t762  T       t1316   o1313 b1315
3370  B       b1316   s1315  B       b1316   t1316
3371  T       t1316   o677 b1316  T       t1317   o b1316 b4
3372  B       b1317   t1316  B       b1317   t1317
3373  S       s1317   t684 h h1303 h1304  T       t1318   o1245 b680 b1251 b1312 b1317
3374  G       s1317   t736  B       b1318   t1318
3375  B       b1318   s1317  T       t1319   o1244 b1318
3376  T       t1318   o677 b1318  B       b1319   t1319
3377  B       b1319   t1318  P       p1319   Number 9340
3378  S       s1319   t684 h h1303 h1304  P       p1320   Number 9634
3379  G       s1319   t738  O       o1320   location p1319 p1320
3380  B       b1320   s1319  P       p1321   String id_eq2
3381  T       t1320   o677 b1320  O       o1321   rule p1321
3382  B       b1321   t1320  T       t1321   o598 b582 b832 b606
3383  S       s1321   t684 h h1303 h1304  B       b1321   t1321
3384  G       s1321   t764  T       t1322   o727 b588 b593 b1321 b832
3385  B       b1322   s1321  S       s1322   t688 h
3386  T       t1322   o677 b1322  G       s1322   t1322
3387  B       b1323   t1322  B       b1322   s1322
3388  T       t1323   o761 b591 b759 b717 b756  T       t1323   o681 b1322
3389  S       s1323   t684 h h1303 h1304  B       b1323   t1323
3390  G       s1323   t1323  T       t1324   o680 b952 b1323
3391  B       b1324   s1323  B       b1324   t1324
3392  T       t1324   o677 b1324  T       t1325   o680 b727 b1324
3393  B       b1325   t1324  B       b1325   t1325
3394  T       t1325   o676 b1323 b1325  T       t1326   o680 b686 b1325
3395  B       b1326   t1325  B       b1326   t1326
3396  T       t1326   o676 b1321 b1326  T       t1327   o680 b834 b1326
3397  B       b1327   t1326  B       b1327   t1327
3398  T       t1327   o676 b1319 b1327  T       t1328   o1060 b1322 b1255
3399  B       b1328   t1327  B       b1328   t1328
3400  T       t1328   o676 b1317 b1328  T       t1329   o1059 b1328 b4 b1065
3401  B       b1329   t1328  B       b1329   t1329
3402  T       t1329   o676 b1315 b1329  S       s1329   t688 h
3403  B       b1330   t1329  G       s1329   t1086
3404  T       t1330   o676 b1313 b1330  B       b1330   s1329
3405    T       t1330   o1060 b1330 b1255
3406  B       b1331   t1330  B       b1331   t1330
3407  T       t1331   o676 b1311 b1331  T       t1331   o2 b1329
3408  B       b1332   t1331  B       b1332   t1331
3409  T       t1332   o676 b1309 b1332  T       t1332   o1059 b1331 b4 b1332
3410  B       b1333   t1332  B       b1333   t1332
3411  T       t1333   o676 b1307 b1333  T       t1333   o598 b582 b832 b1086
3412  B       b1334   t1333  B       b1334   t1333
3413  T       t1334   o676 b1305 b1334  T       t1334   o727 b588 b593 b1334 b832
3414  B       b1335   t1334  S       s1334   t688 h
3415  P       p1335   String "assertT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenAT autoT"  G       s1334   t1334
3416  O       o1335   ext_rule p1335  B       b1335   s1334
3417  T       t1335   o b1322 b4  T       t1335   o1060 b1335 b1255
3418  B       b1336   t1335  B       b1336   t1335
3419  T       t1336   o b1320 b1336  T       t1336   o1059 b1336 b4 b1332
3420  B       b1337   t1336  B       b1337   t1336
3421  T       t1337   o b1318 b1337  T       t1337   o b1337 b4
3422  B       b1338   t1337  B       b1338   t1337
3423  T       t1338   o b1316 b1338  T       t1338   o b1333 b1338
3424  B       b1339   t1338  B       b1339   t1338
3425  T       t1339   o b1314 b1339  T       t1339   o1058 b1329 b1339
3426  B       b1340   t1339  B       b1340   t1339
3427  T       t1340   o b1312 b1340  T       t1340   o1058 b1333 b4
3428  B       b1341   t1340  B       b1341   t1340
3429  T       t1341   o b1310 b1341  T       t1341   o1103 b1057 b1341 b4 b4
3430  B       b1342   t1341  B       b1342   t1341
3431  T       t1342   o b1308 b1342  P       p1342   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; op{'g; inv{'g; 's}; 's}}; op{'g; op{'g; 's; inv{'g; 's}}; 's}}>> 0 ttca"
3432    O       o1342   ext_rule p1342
3433    T       t1342   o598 b582 b1245 b832
3434  B       b1343   t1342  B       b1343   t1342
3435  T       t1343   o b1306 b1343  T       t1343   o727 b588 b593 b1343 b832
3436  B       b1344   t1343  S       s1343   t688 h
3437  T       t1344   o b1304 b1344  G       s1343   t1343
3438    B       b1344   s1343
3439    T       t1344   o1060 b1344 b1255
3440  B       b1345   t1344  B       b1345   t1344
3441  T       t1345   o1095 b1324 b1345  T       t1345   o2 b1337
3442  B       b1346   t1345  B       b1346   t1345
3443  T       t1346   o1094 b1346 b4 b1104  T       t1346   o1059 b1345 b4 b1346
3444  B       b1347   t1346  B       b1347   t1346
3445  T       t1347   o596 b585 b980 b720  T       t1347   o b1347 b4
3446  B       b1348   t1347  B       b1348   t1347
3447  T       t1348   o596 b585 b980 b791  T       t1348   o1058 b1337 b1348
3448  B       b1349   t1348  B       b1349   t1348
3449  T       t1349   o761 b591 b759 b1348 b1349  P       p1349   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; 's; inv{'g; 's}}; id{'g}} >> 0 thenT autoT"
3450  H       h1349   v t1349  O       o1349   ext_rule p1349
3451  S       s1349   t684 h h1303 h1304 h1349  T       t1349   o1058 b1347 b4
3452  G       s1349   t1323  B       b1350   t1349
3453  B       b1350   s1349  T       t1350   o1349 b1057 b1350 b4 b4
 T       t1350   o1095 b1350 b1345  
3454  B       b1351   t1350  B       b1351   t1350
3455  T       t1351   o2 b1347  T       t1351   o b1351 b4
3456  B       b1352   t1351  B       b1352   t1351
3457  T       t1352   o1094 b1351 b4 b1352  T       t1352   o1342 b1057 b1349 b1352 b4
3458  B       b1353   t1352  B       b1353   t1352
3459  T       t1353   o b1353 b4  T       t1353   o b1353 b4
3460  B       b1354   t1353  B       b1354   t1353
3461  T       t1354   o1093 b1347 b1354  T       t1354   o b1342 b1354
3462  B       b1355   t1354  B       b1355   t1354
3463  P       p1355   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 4 ttca"  T       t1355   o1084 b1057 b1340 b1355 b4
 O       o1355   ext_rule p1355  
 T       t1355   o596 b585 b1036 b717  
3464  B       b1356   t1355  B       b1356   t1355
3465  T       t1356   o761 b591 b759 b1356 b1349  T       t1356   o1055 b1356
3466  H       h1356   z t1356  B       b1357   t1356
3467  S       s1356   t684 h h1303 h1304 h1349 h1356  P       p1357   Number 9362
3468  G       s1356   t1323  P       p1358   Number 9369
3469  B       b1357   s1356  O       o1358   resource_defs p1357 p1358 p204
3470  T       t1357   o1095 b1357 b1345  P       p1359   Number 9367
3471  B       b1358   t1357  O       o1359   uid p1359 p1358
3472  T       t1358   o2 b1353  T       t1359   o1359 b695
3473  B       b1359   t1358  B       b1359   t1359
3474  T       t1359   o1094 b1358 b4 b1359  T       t1360   o b1359 b4
3475  B       b1360   t1359  B       b1360   t1360
3476  T       t1360   o b1360 b4  T       t1361   o1358 b1360
3477  B       b1361   t1360  B       b1361   t1361
3478  T       t1361   o1093 b1353 b1361  T       t1362   o b1361 b4
3479  B       b1362   t1361  B       b1362   t1362
3480  P       p1362   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 5 ttca"  T       t1363   o1321 b680 b1327 b1357 b1362
3481  O       o1362   ext_rule p1362  B       b1363   t1363
3482  T       t1362   o596 b585 b1036 b756  T       t1364   o1320 b1363
3483  B       b1363   t1362  B       b1364   t1364
3484  T       t1363   o761 b591 b759 b1356 b1363  P       p1364   Number 9655
3485  H       h1363   z_1 t1363  P       p1365   Number 10094
3486  S       s1363   t684 h h1303 h1304 h1349 h1356 h1363  O       o1365   location p1364 p1365
3487  G       s1363   t1323  P       p1366   String equiv_op_fun1
3488  B       b1364   s1363  O       o1366   rule p1366
3489  T       t1364   o1095 b1364 b1345  S       s1366   t683 h
3490  B       b1365   t1364  G       s1366   t1155
3491  T       t1365   o2 b1360  B       b1366   s1366
3492  B       b1366   t1365  T       t1366   o681 b1366
 T       t1366   o1094 b1365 b4 b1366  
3493  B       b1367   t1366  B       b1367   t1366
3494  T       t1367   o b1367 b4  S       s1367   t683 h
3495  B       b1368   t1367  G       s1367   t1156
3496  T       t1368   o1093 b1360 b1368  B       b1368   s1367
3497    T       t1368   o681 b1368
3498  B       b1369   t1368  B       b1369   t1368
3499  P       p1369   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"  S       s1369   t688 h
3500  O       o1369   ext_rule p1369  G       s1369   t1160
3501  T       t1369   o596 b585 b604 b717  B       b1370   s1369
3502  B       b1370   t1369  T       t1370   o681 b1370
 T       t1370   o596 b585 b604 b756  
3503  B       b1371   t1370  B       b1371   t1370
3504  T       t1371   o761 b591 b759 b1370 b1371  S       s1371   t688 h
3505  H       h1371   z_2 t1371  G       s1371   t1161
 S       s1371   t684 h h1303 h1304 h1349 h1356 h1363 h1371  
 G       s1371   t1323  
3506  B       b1372   s1371  B       b1372   s1371
3507  T       t1372   o1095 b1372 b1345  T       t1372   o681 b1372
3508  B       b1373   t1372  B       b1373   t1372
3509  T       t1373   o2 b1367  T       t1373   o598 b582 b835 b599
3510  B       b1374   t1373  B       b1374   t1373
3511  T       t1374   o1094 b1373 b4 b1374  T       t1374   o598 b582 b835 b600
3512  B       b1375   t1374  B       b1375   t1374
3513  T       t1375   o b1375 b4  T       t1375   o727 b588 b593 b1374 b1375
3514  B       b1376   t1375  B       b1376   t1375 z
3515  T       t1376   o1093 b1367 b1376  T       t1376   o1094 b588 b593 b1376
3516  B       b1377   t1376  S       s1376   t688 h
3517  P       p1377   String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"  G       s1376   t1376
3518  O       o1377   ext_rule p1377  B       b1377   s1376
3519  T       t1377   o761 b591 b759 b717 b1371  T       t1377   o681 b1377
3520  H       h1377   z_3 t1377  B       b1378   t1377
3521  S       s1377   t684 h h1303 h1304 h1349 h1356 h1363 h1371 h1377  T       t1378   o680 b1373 b1378
 G       s1377   t1323  
 B       b1378   s1377  
 T       t1378   o1095 b1378 b1345  
3522  B       b1379   t1378  B       b1379   t1378
3523  T       t1379   o2 b1375  T       t1379   o680 b1371 b1379
3524  B       b1380   t1379  B       b1380   t1379
3525  T       t1380   o1094 b1379 b4 b1380  T       t1380   o680 b727 b1380
3526  B       b1381   t1380  B       b1381   t1380
3527  T       t1381   o b1381 b4  T       t1381   o680 b686 b1381
3528  B       b1382   t1381  B       b1382   t1381
3529  T       t1382   o1093 b1375 b1382  T       t1382   o680 b1369 b1382
3530  B       b1383   t1382  B       b1383   t1382
3531  P       p1383   String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"  T       t1383   o680 b1367 b1383
 O       o1383   ext_rule p1383  
 T       t1383   o1093 b1381 b4  
3532  B       b1384   t1383  B       b1384   t1383
3533  T       t1384   o1383 b1092 b1384 b4 b4  P       p1384   String "rwh unfold_equiv_fun_prop 0 ttca thenT dT 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca"
3534    O       o1384   ext_rule p1384
3535    T       t1384   o b1372 b4
3536  B       b1385   t1384  B       b1385   t1384
3537  T       t1385   o b1385 b4  T       t1385   o b1370 b1385
3538  B       b1386   t1385  B       b1386   t1385
3539  T       t1386   o1377 b1092 b1383 b1386 b4  T       t1386   o b726 b1386
3540  B       b1387   t1386  B       b1387   t1386
3541  T       t1387   o b1387 b4  T       t1387   o b685 b1387
3542  B       b1388   t1387  B       b1388   t1387
3543  T       t1388   o1369 b1092 b1377 b1388 b4  T       t1388   o b1368 b1388
3544  B       b1389   t1388  B       b1389   t1388
3545  T       t1389   o b1389 b4  T       t1389   o b1366 b1389
3546  B       b1390   t1389  B       b1390   t1389
3547  T       t1390   o1362 b1092 b1369 b1390 b4  T       t1390   o1060 b1377 b1390
3548  B       b1391   t1390  B       b1391   t1390
3549  T       t1391   o b1391 b4  T       t1391   o1059 b1391 b4 b1065
3550  B       b1392   t1391  B       b1392   t1391
3551  T       t1392   o1355 b1092 b1362 b1392 b4  H       h1392   a_1 t1108
3552  B       b1393   t1392  H       h1393   b_1 t1108
3553  T       t1393   o b1393 b4  H       h1394   x t727
3554  B       b1394   t1393  P       p1394   Var a_1
3555  P       p1394   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 3 ttca"  O       o1394   var p1394
3556  O       o1394   ext_rule p1394  T       t1394   o1394
3557  H       h1394   v t1303  B       b1394   t1394
3558  H       h1395   v_1 t1349  P       p1395   Var b_1
3559  S       s1395   t684 h h1394 h1395  O       o1395   var p1395
3560  G       s1395   t1323  T       t1395   o1395
3561  B       b1395   s1395  B       b1395   t1395
3562  S       s1396   t684 h  T       t1396   o727 b588 b593 b1394 b1395
3563  G       s1396   t1303  H       h1396   x_1 t1396
3564  B       b1396   s1396  T       t1397   o598 b582 b1394 b599
3565  T       t1396   o b1396 b4  B       b1397   t1397
3566  B       b1397   t1396  T       t1398   o598 b582 b1394 b600
3567  T       t1397   o b764 b1397  B       b1398   t1398
3568  B       b1398   t1397  T       t1399   o727 b588 b593 b1397 b1398
3569  T       t1398   o b738 b1398  H       h1399   x_2 t1399
3570  B       b1399   t1398  T       t1400   o598 b582 b1395 b599
3571  T       t1399   o b736 b1399  B       b1400   t1400
3572  B       b1400   t1399  T       t1401   o598 b582 b1395 b600
3573  T       t1400   o b762 b1400  B       b1401   t1401
3574  B       b1401   t1400  T       t1402   o727 b588 b593 b1400 b1401
3575  T       t1401   o b699 b1401  S       s1402   t688 h h1392 h1393 h1394 h1396 h1399
3576  B       b1402   t1401  G       s1402   t1402
3577  T       t1402   o b681 b1402  B       b1402   s1402
3578  B       b1403   t1402  T       t1403   o1060 b1402 b1390
3579  T       t1403   o b760 b1403  B       b1403   t1403
3580