/[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 3516 by xiny, Mon Feb 25 02:24:42 2002 UTC revision 3527 by xiny, Mon Mar 4 02:20:01 2002 UTC
# Line 1071  Line 1071 
1071  B       b398    t398  B       b398    t398
1072  T       t399    o394 b398  T       t399    o394 b398
1073  B       b399    t399  B       b399    t399
1074  P       p4      Number 129  P       p399    Number 129
1075  P       p8      Number 150  P       p400    Number 150
1076  O       o10     location p4 p8  O       o400    location p399 p400
1077  P       p10     String Czf_itt_equiv  P       p401    String Czf_itt_equiv
1078  O       o12     parent p10  O       o401    parent p401
1079  T       t158    o12  T       t401    o401
1080  B       b158    t158  B       b401    t401
1081  T       t159    o b158 b4  T       t402    o b401 b4
 B       b159    t159  
 P       p166    String Czf_itt_pair  
 O       o166    parent p166  
 T       t170    o166  
 B       b170    t170  
 T       t173    o b170 b4  
 B       b173    t173  
 P       p188    String Czf_itt_singleton  
 O       o188    parent p188  
 T       t196    o188  
 B       b196    t196  
 T       t197    o b196 b4  
 B       b197    t197  
 P       p201    String Czf_itt_union  
 O       o202    parent p201  
 T       t213    o202  
 B       b213    t213  
 T       t214    o b213 b4  
 B       b214    t214  
 P       p220    String Czf_itt_subset  
 O       o220    parent p220  
 T       t230    o220  
 B       b230    t230  
 T       t232    o b230 b4  
 B       b232    t232  
 P       p236    String Czf_itt_dexists  
 O       o236    parent p236  
 T       t241    o236  
 B       b241    t241  
 T       t244    o b241 b4  
 B       b244    t244  
 T       t249    o b244 b4  
 B       b249    t249  
 T       t250    o b232 b249  
 B       b250    t250  
 T       t255    o b214 b250  
 B       b255    t255  
 T       t256    o b197 b255  
 B       b256    t256  
 T       t258    o b173 b256  
 B       b258    t258  
 T       t260    o b159 b258  
 B       b260    t260  
 T       t402    o2 b159 b260 b296  
1082  B       b402    t402  B       b402    t402
1083  T       t509    o10 b402  P       p402    String Czf_itt_pair
1084  B       b509    t509  O       o402    parent p402
1085  P       p512    Number 152  T       t403    o402
 P       p513    Number 163  
 O       o513    location p512 p513  
 NSummary!summary_item   summary_item    summary_item Summary  
 O       o401    summary_item  
 NOcaml!str_open str_open        str_open Ocaml  
 O       o514    str_open p512 p513  
 NOcaml!string   string  string Ocaml  
 P       p402    String Printf  
 O       o403    string p402  
 T       t403    o403  
1086  B       b403    t403  B       b403    t403
1087  T       t404    o b403 b4  T       t404    o b403 b4
1088  B       b404    t404  B       b404    t404
1089  T       t574    o514 b404  P       p404    String Czf_itt_singleton
1090  B       b574    t574  O       o404    parent p404
1091  T       t575    o401 b574  T       t405    o404
1092  B       b575    t575  B       b405    t405
1093  T       t581    o513 b575  T       t406    o b405 b4
1094  B       b581    t581  B       b406    t406
1095  P       p589    Number 164  P       p406    String Czf_itt_union
1096  P       p590    Number 177  O       o406    parent p406
1097  O       o590    location p589 p590  T       t407    o406
1098  O       o591    str_open p589 p590  B       b407    t407
1099  P       p409    String Mp_debug  T       t408    o b407 b4
1100  O       o410    string p409  B       b408    t408
1101  T       t410    o410  P       p408    String Czf_itt_subset
1102    O       o408    parent p408
1103    T       t409    o408
1104    B       b409    t409
1105    T       t410    o b409 b4
1106  B       b410    t410  B       b410    t410
1107  T       t411    o b410 b4  P       p410    String Czf_itt_dexists
1108    O       o410    parent p410
1109    T       t411    o410
1110  B       b411    t411  B       b411    t411
1111  T       t599    o591 b411  T       t412    o b411 b4
1112  B       b599    t599  B       b412    t412
1113  T       t608    o401 b599  T       t413    o b412 b4
1114  B       b608    t608  B       b413    t413
1115  T       t618    o590 b608  T       t414    o b410 b413
1116  B       b618    t618  B       b414    t414
1117  P       p618    Number 178  T       t415    o b408 b414
1118  P       p619    Number 207  B       b415    t415
1119  O       o619    location p618 p619  T       t416    o b406 b415
1120  O       o622    str_open p618 p619  B       b416    t416
1121  P       p416    String Refiner  T       t417    o b404 b416
 O       o417    string p416  
 T       t417    o417  
1122  B       b417    t417  B       b417    t417
1123  P       p417    String TermType  T       t418    o b402 b417
 O       o418    string p417  
 T       t418    o418  
1124  B       b418    t418  B       b418    t418
1125  T       t419    o b418 b4  T       t419    o2 b402 b418 b296
1126  B       b419    t419  B       b419    t419
1127  T       t420    o b417 b419  T       t420    o400 b419
1128  B       b420    t420  B       b420    t420
1129  T       t421    o b417 b420  P       p420    Number 152
1130  B       b421    t421  P       p421    Number 163
1131  T       t625    o622 b421  O       o421    location p420 p421
1132  B       b625    t625  NSummary!summary_item   summary_item    summary_item Summary
1133  T       t642    o401 b625  O       o422    summary_item
1134  B       b642    t642  NOcaml!str_open str_open        str_open Ocaml
1135  T       t643    o619 b642  O       o423    str_open p420 p421
1136  B       b643    t643  NOcaml!string   string  string Ocaml
1137  P       p643    Number 208  P       p423    String Printf
1138  P       p644    Number 233  O       o424    string p423
1139  O       o644    location p643 p644  T       t424    o424
1140  O       o647    str_open p643 p644  B       b424    t424
1141  P       p426    String Term  T       t425    o b424 b4
1142  O       o427    string p426  B       b425    t425
1143  T       t427    o427  T       t426    o423 b425
1144    B       b426    t426
1145    T       t427    o422 b426
1146  B       b427    t427  B       b427    t427
1147  T       t428    o b427 b4  T       t428    o421 b427
1148  B       b428    t428  B       b428    t428
1149  T       t429    o b417 b428  P       p428    Number 164
1150  B       b429    t429  P       p429    Number 177
1151  T       t430    o b417 b429  O       o429    location p428 p429
1152  B       b430    t430  O       o430    str_open p428 p429
1153  T       t654    o647 b430  P       p430    String Mp_debug
1154  B       b654    t654  O       o431    string p430
1155  T       t661    o401 b654  T       t431    o431
1156  B       b661    t661  B       b431    t431
1157  T       t666    o644 b661  T       t432    o b431 b4
1158  B       b666    t666  B       b432    t432
1159  P       p667    Number 234  T       t433    o430 b432
1160  P       p668    Number 261  B       b433    t433
1161  O       o675    location p667 p668  T       t434    o422 b433
1162  O       o677    str_open p667 p668  B       b434    t434
1163  P       p435    String TermOp  T       t435    o429 b434
1164  O       o436    string p435  B       b435    t435
1165  T       t436    o436  P       p435    Number 178
1166  B       b436    t436  P       p436    Number 207
1167  T       t437    o b436 b4  O       o436    location p435 p436
1168  B       b437    t437  O       o437    str_open p435 p436
1169  T       t438    o b417 b437  P       p437    String Refiner
1170    O       o438    string p437
1171    T       t438    o438
1172  B       b438    t438  B       b438    t438
1173  T       t439    o b417 b438  P       p438    String TermType
1174    O       o439    string p438
1175    T       t439    o439
1176  B       b439    t439  B       b439    t439
1177  T       t681    o677 b439  T       t440    o b439 b4
1178  B       b681    t681  B       b440    t440
1179  T       t682    o401 b681  T       t441    o b438 b440
1180  B       b682    t682  B       b441    t441
1181  T       t683    o675 b682  T       t442    o b438 b441
1182  B       b683    t683  B       b442    t442
1183  P       p683    Number 262  T       t443    o437 b442
1184  P       p684    Number 291  B       b443    t443
1185  O       o684    location p683 p684  T       t444    o422 b443
1186  O       o685    str_open p683 p684  B       b444    t444
1187  P       p444    String TermAddr  T       t445    o436 b444
 O       o445    string p444  
 T       t445    o445  
1188  B       b445    t445  B       b445    t445
1189  T       t446    o b445 b4  P       p445    Number 208
1190  B       b446    t446  P       p446    Number 233
1191  T       t447    o b417 b446  O       o446    location p445 p446
1192  B       b447    t447  O       o447    str_open p445 p446
1193  T       t448    o b417 b447  P       p447    String Term
1194    O       o448    string p447
1195    T       t448    o448
1196  B       b448    t448  B       b448    t448
1197  T       t685    o685 b448  T       t449    o b448 b4
1198  B       b685    t685  B       b449    t449
1199  T       t686    o401 b685  T       t450    o b438 b449
1200  B       b686    t686  B       b450    t450
1201  T       t695    o684 b686  T       t451    o b438 b450
1202  B       b695    t695  B       b451    t451
1203  P       p695    Number 292  T       t452    o447 b451
1204  P       p696    Number 320  B       b452    t452
1205  O       o696    location p695 p696  T       t453    o422 b452
1206  O       o697    str_open p695 p696  B       b453    t453
1207  P       p453    String TermMan  T       t454    o446 b453
 O       o454    string p453  
 T       t454    o454  
1208  B       b454    t454  B       b454    t454
1209  T       t455    o b454 b4  P       p454    Number 234
1210  B       b455    t455  P       p455    Number 261
1211  T       t456    o b417 b455  O       o455    location p454 p455
1212  B       b456    t456  O       o456    str_open p454 p455
1213  T       t457    o b417 b456  P       p456    String TermOp
1214    O       o457    string p456
1215    T       t457    o457
1216  B       b457    t457  B       b457    t457
1217  T       t697    o697 b457  T       t458    o b457 b4
1218  B       b697    t697  B       b458    t458
1219  T       t698    o401 b697  T       t459    o b438 b458
1220  B       b698    t698  B       b459    t459
1221  T       t699    o696 b698  T       t460    o b438 b459
1222  B       b699    t699  B       b460    t460
1223  P       p699    Number 321  T       t461    o456 b460
1224  P       p700    Number 351  B       b461    t461
1225  O       o700    location p699 p700  T       t462    o422 b461
1226  O       o701    str_open p699 p700  B       b462    t462
1227  P       p462    String TermSubst  T       t463    o455 b462
 O       o463    string p462  
 T       t463    o463  
1228  B       b463    t463  B       b463    t463
1229  T       t464    o b463 b4  P       p463    Number 262
1230  B       b464    t464  P       p464    Number 291
1231  T       t465    o b417 b464  O       o464    location p463 p464
1232  B       b465    t465  O       o465    str_open p463 p464
1233  T       t466    o b417 b465  P       p465    String TermAddr
1234    O       o466    string p465
1235    T       t466    o466
1236  B       b466    t466  B       b466    t466
1237  T       t712    o701 b466  T       t467    o b466 b4
1238  B       b713    t712  B       b467    t467
1239  T       t713    o401 b713  T       t468    o b438 b467
1240  B       b714    t713  B       b468    t468
1241  T       t714    o700 b714  T       t469    o b438 b468
1242  B       b715    t714  B       b469    t469
1243  P       p718    Number 352  T       t470    o465 b469
1244  P       p719    Number 379  B       b470    t470
1245  O       o719    location p718 p719  T       t471    o422 b470
1246  O       o723    str_open p718 p719  B       b471    t471
1247  P       p471    String Refine  T       t472    o464 b471
 O       o472    string p471  
 T       t472    o472  
1248  B       b472    t472  B       b472    t472
1249  T       t473    o b472 b4  P       p472    Number 292
1250  B       b473    t473  P       p473    Number 320
1251  T       t474    o b417 b473  O       o473    location p472 p473
1252  B       b474    t474  O       o474    str_open p472 p473
1253  T       t475    o b417 b474  P       p474    String TermMan
1254    O       o475    string p474
1255    T       t475    o475
1256  B       b475    t475  B       b475    t475
1257  T       t734    o723 b475  T       t476    o b475 b4
1258  B       b734    t734  B       b476    t476
1259  T       t735    o401 b734  T       t477    o b438 b476
1260  B       b735    t735  B       b477    t477
1261  T       t736    o719 b735  T       t478    o b438 b477
1262  B       b736    t736  B       b478    t478
1263  P       p736    Number 380  T       t479    o474 b478
1264  P       p737    Number 412  B       b479    t479
1265  O       o737    location p736 p737  T       t480    o422 b479
1266  O       o738    str_open p736 p737  B       b480    t480
1267  P       p480    String RefineError  T       t481    o473 b480
 O       o481    string p480  
 T       t481    o481  
1268  B       b481    t481  B       b481    t481
1269  T       t482    o b481 b4  P       p481    Number 321
1270  B       b482    t482  P       p482    Number 351
1271  T       t483    o b417 b482  O       o482    location p481 p482
1272  B       b483    t483  O       o483    str_open p481 p482
1273  T       t484    o b417 b483  P       p483    String TermSubst
1274    O       o484    string p483
1275    T       t484    o484
1276  B       b484    t484  B       b484    t484
1277  T       t738    o738 b484  T       t485    o b484 b4
1278  B       b738    t738  B       b485    t485
1279  T       t739    o401 b738  T       t486    o b438 b485
1280  B       b739    t739  B       b486    t486
1281  T       t758    o737 b739  T       t487    o b438 b486
1282  B       b758    t758  B       b487    t487
1283  P       p758    Number 413  T       t488    o483 b487
1284  P       p759    Number 429  B       b488    t488
1285  O       o759    location p758 p759  T       t489    o422 b488
1286  O       o760    str_open p758 p759  B       b489    t489
1287  P       p489    String Mp_resource  T       t490    o482 b489
 O       o490    string p489  
 T       t490    o490  
1288  B       b490    t490  B       b490    t490
1289  T       t491    o b490 b4  P       p490    Number 352
1290  B       b491    t491  P       p491    Number 379
1291  T       t760    o760 b491  O       o491    location p490 p491
1292  B       b760    t760  O       o492    str_open p490 p491
1293  T       t761    o401 b760  P       p492    String Refine
1294  B       b761    t761  O       o493    string p492
1295  T       t762    o759 b761  T       t493    o493
1296  B       b762    t762  B       b493    t493
1297  P       p762    Number 430  T       t494    o b493 b4
1298  P       p763    Number 447  B       b494    t494
1299  O       o763    location p762 p763  T       t495    o b438 b494
1300  O       o764    str_open p762 p763  B       b495    t495
1301  P       p496    String Simple_print  T       t496    o b438 b495
1302  O       o497    string p496  B       b496    t496
1303  T       t497    o497  T       t497    o492 b496
1304  B       b497    t497  B       b497    t497
1305  T       t498    o b497 b4  T       t498    o422 b497
1306  B       b498    t498  B       b498    t498
1307  T       t776    o764 b498  T       t499    o491 b498
1308  B       b776    t776  B       b499    t499
1309  T       t777    o401 b776  P       p499    Number 380
1310  B       b777    t777  P       p500    Number 412
1311  T       t778    o763 b777  O       o500    location p499 p500
1312  B       b778    t778  O       o501    str_open p499 p500
1313  P       p781    Number 449  P       p501    String RefineError
1314  P       p782    Number 465  O       o502    string p501
1315  O       o782    location p781 p782  T       t502    o502
1316  O       o787    str_open p781 p782  B       b502    t502
1317  P       p503    String Tactic_type  T       t503    o b502 b4
1318  O       o504    string p503  B       b503    t503
1319  T       t504    o504  T       t504    o b438 b503
1320  B       b504    t504  B       b504    t504
1321  T       t505    o b504 b4  T       t505    o b438 b504
1322  B       b505    t505  B       b505    t505
1323  T       t791    o787 b505  T       t506    o501 b505
1324  B       b791    t791  B       b506    t506
1325  T       t792    o401 b791  T       t507    o422 b506
1326  B       b792    t792  B       b507    t507
1327  T       t793    o782 b792  T       t508    o500 b507
1328  B       b793    t793  B       b508    t508
1329  P       p793    Number 466  P       p508    Number 413
1330  P       p794    Number 492  P       p509    Number 429
1331  O       o794    location p793 p794  O       o509    location p508 p509
1332  O       o795    str_open p793 p794  O       o510    str_open p508 p509
1333  P       p510    String Tacticals  P       p510    String Mp_resource
1334  O       o511    string p510  O       o511    string p510
1335  T       t511    o511  T       t511    o511
1336  B       b511    t511  B       b511    t511
1337  T       t512    o b511 b4  T       t512    o b511 b4
1338  B       b512    t512  B       b512    t512
1339  T       t513    o b504 b512  T       t513    o510 b512
1340  B       b513    t513  B       b513    t513
1341  T       t795    o795 b513  T       t514    o422 b513
1342  B       b795    t795  B       b514    t514
1343  T       t796    o401 b795  T       t515    o509 b514
1344  B       b796    t796  B       b515    t515
1345  T       t803    o794 b796  P       p515    Number 430
1346  B       b803    t803  P       p516    Number 447
1347  P       p803    Number 493  O       o516    location p515 p516
1348  P       p804    Number 517  O       o517    str_open p515 p516
1349  O       o804    location p803 p804  P       p517    String Simple_print
1350  O       o805    str_open p803 p804  O       o518    string p517
1351  P       p518    String Sequent  T       t518    o518
1352  O       o519    string p518  B       b518    t518
1353  T       t519    o519  T       t519    o b518 b4
1354  B       b519    t519  B       b519    t519
1355  T       t520    o b519 b4  T       t520    o517 b519
1356  B       b520    t520  B       b520    t520
1357  T       t521    o b504 b520  T       t521    o422 b520
1358  B       b521    t521  B       b521    t521
1359  T       t805    o805 b521  T       t522    o516 b521
1360  B       b805    t805  B       b522    t522
1361  T       t806    o401 b805  P       p522    Number 449
1362  B       b806    t806  P       p523    Number 465
1363  T       t807    o804 b806  O       o523    location p522 p523
1364  B       b807    t807  O       o524    str_open p522 p523
1365  P       p807    Number 518  P       p524    String Tactic_type
1366  P       p526    String Conversionals  O       o525    string p524
1367  O       o527    string p526  T       t525    o525
1368  T       t527    o527  B       b525    t525
1369    T       t526    o b525 b4
1370    B       b526    t526
1371    T       t527    o524 b526
1372  B       b527    t527  B       b527    t527
1373  T       t528    o b527 b4  T       t528    o422 b527
1374  B       b528    t528  B       b528    t528
1375  T       t529    o b504 b528  T       t529    o523 b528
1376  B       b529    t529  B       b529    t529
1377  O       o535    string p91  P       p529    Number 466
1378  T       t535    o535  P       p530    Number 492
1379    O       o530    location p529 p530
1380    O       o531    str_open p529 p530
1381    P       p531    String Tacticals
1382    O       o532    string p531
1383    T       t532    o532
1384    B       b532    t532
1385    T       t533    o b532 b4
1386    B       b533    t533
1387    T       t534    o b525 b533
1388    B       b534    t534
1389    T       t535    o531 b534
1390  B       b535    t535  B       b535    t535
1391  T       t536    o b535 b4  T       t536    o422 b535
1392  B       b536    t536  B       b536    t536
1393  O       o542    string p89  T       t537    o530 b536
1394  T       t542    o542  B       b537    t537
1395    P       p537    Number 493
1396    P       p538    Number 517
1397    O       o538    location p537 p538
1398    O       o539    str_open p537 p538
1399    P       p539    String Sequent
1400    O       o540    string p539
1401    T       t540    o540
1402    B       b540    t540
1403    T       t541    o b540 b4
1404    B       b541    t541
1405    T       t542    o b525 b541
1406  B       b542    t542  B       b542    t542
1407  T       t543    o b542 b4  T       t543    o539 b542
1408  B       b543    t543  B       b543    t543
1409    T       t544    o422 b543
1410    B       b544    t544
1411    T       t545    o538 b544
1412    B       b545    t545
1413    P       p545    Number 518
1414  P       p546    Number 548  P       p546    Number 548
1415  O       o807    location p807 p546  O       o546    location p545 p546
1416  O       o808    str_open p807 p546  O       o547    str_open p545 p546
1417  T       t808    o808 b529  P       p547    String Conversionals
1418  B       b808    t808  O       o548    string p547
1419  T       t825    o401 b808  T       t548    o548
1420  B       b825    t825  B       b548    t548
1421  T       t826    o807 b825  T       t549    o b548 b4
 B       b826    t826  
 P       p826    Number 549  
 P       p827    Number 559  
 O       o827    location p826 p827  
 O       o828    str_open p826 p827  
 T       t828    o828 b536  
 B       b828    t828  
 T       t829    o401 b828  
 B       b829    t829  
 T       t830    o827 b829  
 B       b830    t830  
 P       p830    Number 560  
 P       p831    Number 568  
 O       o831    location p830 p831  
 O       o834    str_open p830 p831  
 T       t843    o834 b543  
 B       b843    t843  
 T       t844    o401 b843  
 B       b844    t844  
 T       t845    o831 b844  
 B       b845    t845  
 P       p845    Number 570  
 O       o549    string p79  
 T       t549    o549  
1422  B       b549    t549  B       b549    t549
1423  T       t550    o b549 b4  T       t550    o b525 b549
1424  B       b550    t550  B       b550    t550
1425  P       p554    Number 587  T       t551    o547 b550
1426  O       o845    location p845 p554  B       b551    t551
1427  O       o846    str_open p845 p554  T       t552    o422 b551
1428  T       t846    o846 b550  B       b552    t552
1429  B       b846    t846  T       t553    o546 b552
1430  T       t847    o401 b846  B       b553    t553
1431  B       b847    t847  P       p553    Number 549
1432  T       t848    o845 b847  P       p554    Number 559
1433  B       b848    t848  O       o554    location p553 p554
1434  P       p848    Number 588  O       o555    str_open p553 p554
1435  P       p849    Number 609  O       o556    string p91
 O       o849    location p848 p849  
 O       o851    str_open p848 p849  
 O       o556    string p81  
1436  T       t556    o556  T       t556    o556
1437  B       b556    t556  B       b556    t556
1438  T       t557    o b556 b4  T       t557    o b556 b4
1439  B       b557    t557  B       b557    t557
1440  T       t855    o851 b557  T       t558    o555 b557
1441  B       b855    t855  B       b558    t558
1442  T       t856    o401 b855  T       t559    o422 b558
1443  B       b856    t856  B       b559    t559
1444  T       t857    o849 b856  T       t560    o554 b559
1445  B       b857    t857  B       b560    t560
1446  P       p857    Number 611  P       p560    Number 560
1447  P       p858    Number 628  P       p561    Number 568
1448  O       o858    location p857 p858  O       o561    location p560 p561
1449  NSummary!opname opname  opname Summary  O       o562    str_open p560 p561
1450  P       p562    String group  O       o563    string p89
1451  O       o562    opname p562  T       t563    o563
1452  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  B       b563    t563
1453  NCzf_itt_group!group    group   group Czf_itt_group  T       t564    o b563 b4
 O       o563    group  
 Nvar    var     var NIL  
 P       p563    Var g  
 O       o564    var p563  
 T       t564    o564  
1454  B       b564    t564  B       b564    t564
1455  T       t565    o563 b564  T       t565    o562 b564
1456  B       b565    t565  B       b565    t565
1457  T       t566    o562 b565  T       t566    o422 b565
1458  B       b566    t566  B       b566    t566
1459  T       t858    o858 b566  T       t567    o561 b566
1460  B       b858    t858  B       b567    t567
1461  P       p859    Number 629  P       p567    Number 570
1462  P       p860    Number 644  P       p568    Number 587
1463  O       o860    location p859 p860  O       o568    location p567 p568
1464  P       p569    String car  O       o569    str_open p567 p568
1465  O       o569    opname p569  O       o570    string p79
1466  NCzf_itt_group!car      car     car Czf_itt_group  T       t570    o570
 O       o570    car  
 T       t570    o570 b564  
1467  B       b570    t570  B       b570    t570
1468  T       t571    o569 b570  T       t571    o b570 b4
1469  B       b571    t571  B       b571    t571
1470  T       t860    o860 b571  T       t572    o569 b571
1471  B       b860    t860  B       b572    t572
1472  P       p861    Number 685  T       t573    o422 b572
1473  P       p863    Number 707  B       b573    t573
1474  O       o863    location p861 p863  T       t574    o568 b573
1475  P       p574    String op  B       b574    t574
1476  O       o574    opname p574  P       p574    Number 588
1477  NCzf_itt_group!op       op      op Czf_itt_group  P       p575    Number 609
1478  O       o575    op  O       o575    location p574 p575
1479  P       p575    Var s1  O       o576    str_open p574 p575
1480  O       o576    var p575  O       o577    string p81
 T       t576    o576  
 B       b576    t576  
 P       p576    Var s2  
 O       o577    var p576  
1481  T       t577    o577  T       t577    o577
1482  B       b577    t577  B       b577    t577
1483  T       t578    o575 b564 b576 b577  T       t578    o b577 b4
1484  B       b578    t578  B       b578    t578
1485  P       p582    String id  T       t579    o576 b578
1486  O       o582    opname p582  B       b579    t579
1487  NCzf_itt_group!id       id      id Czf_itt_group  T       t580    o422 b579
1488  O       o583    id  B       b580    t580
1489  T       t583    o583 b564  T       t581    o575 b580
1490  B       b583    t583  B       b581    t581
1491  T       t584    o582 b583  P       p581    Number 611
1492  B       b584    t584  P       p582    Number 628
1493  P       p586    Number 722  O       o582    location p581 p582
1494  P       p587    String inv  NSummary!opname opname  opname Summary
1495  O       o587    opname p587  P       p583    String group
1496  NCzf_itt_group!inv      inv     inv Czf_itt_group  O       o583    opname p583
1497  O       o588    inv  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1498  P       p588    Var s  NCzf_itt_group!group    group   group Czf_itt_group
1499  O       o589    var p588  O       o584    group
1500  T       t589    o589  Nvar    var     var NIL
1501  B       b589    t589  P       p584    Var g
1502  T       t590    o588 b564 b589  O       o585    var p584
1503  B       b590    t590  T       t585    o585
1504  P       p592    Number 723  B       b585    t585
1505  NSummary!prec   prec    prec Summary  T       t586    o584 b585
1506  P       p6      String prec_op  B       b586    t586
1507  O       o8      prec p6  T       t587    o583 b586
1508  T       t154    o8  B       b587    t587
1509  B       b154    t154  T       t588    o582 b587
1510  NSummary!dform  dform   dform Summary  B       b588    t588
1511  P       p599    String group_df  P       p588    Number 629
1512  O       o599    dform p599  P       p589    Number 644
1513  NSummary!except_mode_df except_mode_df  except_mode_df Summary  O       o589    location p588 p589
1514  P       p600    String src  P       p590    String car
1515  O       o600    except_mode_df p600  O       o590    opname p590
1516  T       t600    o600  NCzf_itt_group!car      car     car Czf_itt_group
1517    O       o591    car
1518    T       t591    o591 b585
1519    B       b591    t591
1520    T       t592    o590 b591
1521    B       b592    t592
1522    T       t593    o589 b592
1523    B       b593    t593
1524    P       p593    Number 685
1525    P       p594    Number 707
1526    O       o594    location p593 p594
1527    P       p595    String op
1528    O       o595    opname p595
1529    NCzf_itt_group!op       op      op Czf_itt_group
1530    O       o596    op
1531    P       p596    Var a
1532    O       o597    var p596
1533    T       t597    o597
1534    B       b597    t597
1535    P       p597    Var b
1536    O       o598    var p597
1537    T       t598    o598
1538    B       b598    t598
1539    T       t599    o596 b585 b597 b598
1540    B       b599    t599
1541    T       t600    o595 b599
1542  B       b600    t600  B       b600    t600
1543  T       t601    o b600 b4  T       t601    o594 b600
1544  B       b601    t601  B       b601    t601
1545  NSummary!df_term        df_term df_term Summary  P       p601    Number 708
1546  O       o601    df_term  P       p602    Number 722
1547  Nslot   slot    slot NIL  O       o602    location p601 p602
1548  O       o602    slot  P       p603    String id
1549  T       t602    o602 b564  O       o603    opname p603
1550  B       b602    t602  NCzf_itt_group!id       id      id Czf_itt_group
1551  NPerv!string    string602       string Perv  O       o604    id
1552  P       p602    String " group"  T       t604    o604 b585
 O       o603    string602 p602  
 T       t603    o603  
 B       b603    t603  
 T       t604    o b603 b4  
1553  B       b604    t604  B       b604    t604
1554  T       t605    o b602 b604  T       t605    o603 b604
1555  B       b605    t605  B       b605    t605
1556  T       t606    o601 b605  T       t606    o602 b605
1557  B       b606    t606  B       b606    t606
1558  T       t607    o599 b601 b565 b606  P       p606    Number 723
1559  B       b607    t607  P       p607    Number 742
1560  P       p610    String car_df  O       o607    location p606 p607
1561  O       o610    dform p610  P       p608    String inv
1562  P       p611    String car(  O       o608    opname p608
1563  O       o611    string602 p611  NCzf_itt_group!inv      inv     inv Czf_itt_group
1564  T       t611    o611  O       o609    inv
1565    T       t609    o609 b585 b597
1566    B       b609    t609
1567    T       t610    o608 b609
1568    B       b610    t610
1569    T       t611    o607 b610
1570  B       b611    t611  B       b611    t611
1571  P       p612    String )  P       p611    Number 744
1572  O       o612    string602 p612  P       p612    Number 756
1573  T       t612    o612  O       o612    location p611 p612
1574  B       b612    t612  NSummary!prec   prec    prec Summary
1575  T       t613    o b612 b4  P       p613    String prec_op
1576    O       o613    prec p613
1577    T       t613    o613
1578  B       b613    t613  B       b613    t613
1579  T       t614    o b602 b613  T       t614    o612 b613
1580  B       b614    t614  B       b614    t614
1581  T       t615    o b611 b614  P       p614    Number 758
1582  B       b615    t615  P       p615    Number 828
1583  T       t616    o601 b615  O       o615    location p614 p615
1584  B       b616    t616  NSummary!dform  dform   dform Summary
1585  T       t617    o610 b601 b570 b616  P       p616    String group_df
1586    O       o616    dform p616
1587    NSummary!except_mode_df except_mode_df  except_mode_df Summary
1588    P       p617    String src
1589    O       o617    except_mode_df p617
1590    T       t617    o617
1591  B       b617    t617  B       b617    t617
1592  P       p620    String id_df  T       t618    o b617 b4
1593  O       o620    dform p620  B       b618    t618
1594  P       p621    String id(  NSummary!df_term        df_term df_term Summary
1595  O       o621    string602 p621  O       o618    df_term
1596  T       t621    o621  Nslot   slot    slot NIL
1597    O       o619    slot
1598    T       t619    o619 b585
1599    B       b619    t619
1600    NPerv!string    string619       string Perv
1601    P       p619    String " group"
1602    O       o620    string619 p619
1603    T       t620    o620
1604    B       b620    t620
1605    T       t621    o b620 b4
1606  B       b621    t621  B       b621    t621
1607  T       t622    o b621 b614  T       t622    o b619 b621
1608  B       b622    t622  B       b622    t622
1609  T       t623    o601 b622  T       t623    o618 b622
1610  B       b623    t623  B       b623    t623
1611  T       t624    o620 b601 b583 b623  T       t624    o616 b618 b586 b623
1612  B       b624    t624  B       b624    t624
1613  P       p627    String op_df  T       t625    o615 b624
1614    B       b625    t625
1615    P       p625    Number 830
1616    P       p626    Number 899
1617    O       o626    location p625 p626
1618    P       p627    String car_df
1619  O       o627    dform p627  O       o627    dform p627
1620  NSummary!prec_df        prec_df prec_df Summary  P       p628    String car(
1621  O       o201    prec_df p6  O       o628    string619 p628
 T       t205    o201  
 B       b205    t205  
 NSummary!parens_df      parens_df       parens_df Summary  
 O       o628    parens_df  
1622  T       t628    o628  T       t628    o628
1623  B       b628    t628  B       b628    t628
1624  T       t629    o b628 b4  P       p629    String )
1625    O       o629    string619 p629
1626    T       t629    o629
1627  B       b629    t629  B       b629    t629
1628  T       t206    o b205 b629  T       t630    o b629 b4
 B       b206    t206  
 T       t208    o b600 b206  
 B       b208    t208  
 T       t630    o b600 b629  
1629  B       b630    t630  B       b630    t630
1630  P       p630    String op(  T       t631    o b619 b630
 O       o630    string602 p630  
 T       t631    o630  
1631  B       b631    t631  B       b631    t631
1632  P       p631    String "; "  T       t632    o b628 b631
 O       o631    string602 p631  
 T       t632    o631  
1633  B       b632    t632  B       b632    t632
1634  P       p645    String inv_df  T       t633    o618 b632
1635  O       o645    dform p645  B       b633    t633
1636  P       p646    String inv(  T       t634    o627 b618 b591 b633
1637  O       o646    string602 p646  B       b634    t634
1638    T       t635    o626 b634
1639    B       b635    t635
1640    P       p635    Number 901
1641    P       p636    Number 967
1642    O       o636    location p635 p636
1643    P       p637    String id_df
1644    O       o637    dform p637
1645    P       p638    String id(
1646    O       o638    string619 p638
1647    T       t638    o638
1648    B       b638    t638
1649    T       t639    o b638 b631
1650    B       b639    t639
1651    T       t640    o618 b639
1652    B       b640    t640
1653    T       t641    o637 b618 b604 b640
1654    B       b641    t641
1655    T       t642    o636 b641
1656    B       b642    t642
1657    P       p642    Number 969
1658    P       p643    Number 1103
1659    O       o643    location p642 p643
1660    P       p644    String op_df
1661    O       o644    dform p644
1662    NSummary!prec_df        prec_df prec_df Summary
1663    O       o645    prec_df p613
1664    T       t645    o645
1665    B       b645    t645
1666    NSummary!parens_df      parens_df       parens_df Summary
1667    O       o646    parens_df
1668  T       t646    o646  T       t646    o646
1669  B       b646    t646  B       b646    t646
1670  NSummary!rule   rule    rule Summary  T       t647    o b646 b4
1671  P       p663    String group_type  B       b647    t647
1672  O       o663    rule p663  T       t648    o b645 b647
1673  NSummary!context_param  context_param   context_param Summary  B       b648    t648
1674  P       p664    String H  T       t649    o b617 b648
1675  O       o664    context_param p664  B       b649    t649
1676  T       t664    o664  P       p649    String op(
1677    O       o649    string619 p649
1678    T       t650    o649
1679    B       b650    t650
1680    P       p650    String "; "
1681    O       o650    string619 p650
1682    T       t651    o650
1683    B       b651    t651
1684    T       t652    o619 b597
1685    B       b652    t652
1686    T       t653    o619 b598
1687    B       b653    t653
1688    T       t654    o b653 b630
1689    B       b654    t654
1690    T       t655    o b651 b654
1691    B       b655    t655
1692    T       t656    o b652 b655
1693    B       b656    t656
1694    T       t657    o b651 b656
1695    B       b657    t657
1696    T       t658    o b619 b657
1697    B       b658    t658
1698    T       t659    o b650 b658
1699    B       b659    t659
1700    T       t660    o618 b659
1701    B       b660    t660
1702    T       t661    o644 b649 b599 b660
1703    B       b661    t661
1704    T       t662    o643 b661
1705    B       b662    t662
1706    P       p662    Number 1105
1707    P       p663    Number 1203
1708    O       o663    location p662 p663
1709    P       p664    String inv_df
1710    O       o664    dform p664
1711    T       t664    o b617 b647
1712  B       b664    t664  B       b664    t664
1713  T       t665    o b664 b4  P       p665    String inv(
1714    O       o665    string619 p665
1715    T       t665    o665
1716  B       b665    t665  B       b665    t665
1717    T       t666    o b652 b630
1718    B       b666    t666
1719    T       t667    o b651 b666
1720    B       b667    t667
1721    T       t668    o b619 b667
1722    B       b668    t668
1723    T       t669    o b665 b668
1724    B       b669    t669
1725    T       t670    o618 b669
1726    B       b670    t670
1727    T       t671    o664 b664 b609 b670
1728    B       b671    t671
1729    T       t672    o663 b671
1730    B       b672    t672
1731    P       p672    Number 1222
1732    P       p673    Number 1356
1733    O       o673    location p672 p673
1734    NSummary!rule   rule    rule Summary
1735    P       p674    String group_type
1736    O       o674    rule p674
1737    NSummary!context_param  context_param   context_param Summary
1738    P       p675    String H
1739    O       o675    context_param p675
1740    T       t675    o675
1741    B       b675    t675
1742    T       t676    o b675 b4
1743    B       b676    t676
1744  NSummary!meta_implies   meta_implies    meta_implies Summary  NSummary!meta_implies   meta_implies    meta_implies Summary
1745  O       o665    meta_implies  O       o676    meta_implies
1746  NSummary!meta_theorem   meta_theorem    meta_theorem Summary  NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1747  O       o666    meta_theorem  O       o677    meta_theorem
1748  NBase_trivial   Base_trivial    Base_trivial NIL  NBase_trivial   Base_trivial    Base_trivial NIL
1749  NBase_trivial!squash    squash  squash Base_trivial  NBase_trivial!squash    squash  squash Base_trivial
1750  O       o667    squash  O       o678    squash
1751  T       t667    o667  T       t678    o678
1752  B       b667    t667  B       b678    t678
1753  T       t668    o b667 b4  T       t679    o b678 b4
1754  C       h       H  C       h       H
1755  NItt_equal      Itt_equal       Itt_equal NIL  NItt_equal      Itt_equal       Itt_equal NIL
1756  NItt_equal!equal        equal   equal Itt_equal  NItt_equal!equal        equal   equal Itt_equal
1757  O       o668    equal  O       o679    equal
1758  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1759  NItt_record_label0!label        label   label Itt_record_label0  NItt_record_label0!label        label   label Itt_record_label0
1760  O       o669    label  O       o680    label
1761  T       t669    o669  T       t680    o680
1762  B       b669    t669  B       b680    t680
1763  T       t670    o668 b669 b564 b564  T       t681    o679 b680 b585 b585
1764  S       s       t668 h  S       s       t679 h
1765  G       s       t670  G       s       t681
1766  B       b670    s  B       b681    s
1767  T       t671    o666 b670  T       t682    o677 b681
1768  B       b671    t671  B       b682    t682
1769  P       p671    Var ext  P       p682    Var ext
1770  O       o671    var p671  O       o682    var p682
1771  T       t672    o671  T       t683    o682
1772  B       b672    t672  B       b683    t683
1773  T       t673    o b672 b4  T       t684    o b683 b4
1774  NItt_equal!type type    type Itt_equal  NItt_equal!type type    type Itt_equal
1775  O       o673    type  O       o684    type
1776  T       t674    o673 b565  T       t685    o684 b586
1777  S       s674    t673 h  S       s685    t684 h
1778  G       s674    t674  G       s685    t685
1779  B       b674    s674  B       b685    s685
1780  T       t675    o666 b674  T       t686    o677 b685
1781  B       b675    t675  B       b686    t686
1782  T       t676    o665 b671 b675  T       t687    o676 b682 b686
1783  B       b676    t676  B       b687    t687
1784  NSummary!incomplete     incomplete      incomplete Summary  NSummary!incomplete     incomplete      incomplete Summary
1785  O       o676    incomplete  O       o687    incomplete
1786  T       t677    o676  T       t688    o687
1787  B       b677    t677  B       b688    t688
1788  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
1789    P       p688    Number 1248
1790    P       p689    Number 1256
1791    O       o689    resource_defs p688 p689 p204
1792  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
1793  P       p680    String []  P       p690    Number 1254
1794  O       o680    uid p680  O       o690    uid p690 p689
1795  T       t680    o680  P       p691    String []
1796  B       b680    t680  O       o691    uid p691
1797  P       p688    String car_wf  T       t691    o691
1798  O       o688    rule p688  B       b691    t691
1799  S       s688    t673 h  T       t692    o690 b691
1800  G       s688    t565  B       b692    t692
1801  B       b688    s688  T       t693    o b692 b4
1802  T       t688    o666 b688  B       b693    t693
1803  B       b689    t688  T       t694    o689 b693
1804    B       b694    t694
1805    T       t695    o b694 b4
1806    B       b695    t695
1807    T       t696    o674 b676 b687 b688 b695
1808    B       b696    t696
1809    T       t697    o673 b696
1810    B       b697    t697
1811    P       p697    Number 1358
1812    P       p698    Number 1526
1813    O       o698    location p697 p698
1814    P       p699    String car_wf
1815    O       o699    rule p699
1816    S       s699    t684 h
1817    G       s699    t586
1818    B       b699    s699
1819    T       t699    o677 b699
1820    B       b700    t699
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       o689    isset  O       o700    isset
1824  T       t689    o689 b570  T       t700    o700 b591
1825  S       s689    t673 h  S       s700    t684 h
1826  G       s689    t689  G       s700    t700
1827  B       b690    s689  B       b701    s700
1828  T       t690    o666 b690  T       t701    o677 b701
1829  B       b691    t690  B       b702    t701
1830  T       t691    o665 b689 b691  T       t702    o676 b700 b702
1831  B       b692    t691  B       b703    t702
1832  T       t692    o665 b671 b692  T       t703    o676 b682 b703
1833  B       b693    t692  B       b704    t703
1834  P       p287    Number 1528  P       p704    Number 1380
1835  P       p288    Number 1526  P       p705    Number 1387
1836  P       p702    String op_wf1  O       o705    resource_defs p704 p705 p204
1837  O       o702    rule p702  P       p706    Number 1385
1838  T       t702    o689 b576  O       o706    uid p706 p705
1839  S       s702    t668 h  T       t706    o706 b691
1840  G       s702    t702  B       b706    t706
1841  B       b702    s702  T       t707    o b706 b4
 T       t703    o666 b702  
 B       b703    t703  
 T       t704    o689 b577  
 S       s704    t668 h  
 G       s704    t704  
 B       b704    s704  
 T       t705    o666 b704  
 B       b705    t705  
 T       t706    o689 b578  
 S       s706    t673 h  
 G       s706    t706  
 B       b706    s706  
 T       t707    o666 b706  
1842  B       b707    t707  B       b707    t707
1843  T       t708    o665 b705 b707  T       t708    o705 b707
1844  B       b708    t708  B       b708    t708
1845  T       t709    o665 b703 b708  T       t709    o b708 b4
1846  B       b709    t709  B       b709    t709
1847  T       t710    o665 b689 b709  T       t710    o699 b676 b704 b688 b709
1848  B       b710    t710  B       b710    t710
1849  T       t711    o665 b671 b710  T       t711    o698 b710
1850  B       b711    t711  B       b711    t711
1851  P       p720    String op_wf2  P       p711    Number 1528
1852  O       o720    rule p720  P       p712    Number 1795
1853  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  O       o712    location p711 p712
1854  NCzf_itt_member!mem     mem     mem Czf_itt_member  P       p713    String op_wf1
1855  O       o721    mem  O       o713    rule p713
1856  T       t721    o721 b576 b570  P       p714    Var s1
1857  S       s721    t673 h  O       o714    var p714
1858    T       t714    o714
1859    B       b714    t714
1860    T       t715    o700 b714
1861    S       s715    t679 h
1862    G       s715    t715
1863    B       b715    s715
1864    T       t716    o677 b715
1865    B       b716    t716
1866    P       p716    Var s2
1867    O       o716    var p716
1868    T       t717    o716
1869    B       b717    t717
1870    T       t718    o700 b717
1871    S       s718    t679 h
1872    G       s718    t718
1873    B       b718    s718
1874    T       t719    o677 b718
1875    B       b719    t719
1876    T       t720    o596 b585 b714 b717
1877    B       b720    t720
1878    T       t721    o700 b720
1879    S       s721    t684 h
1880  G       s721    t721  G       s721    t721
1881  B       b721    s721  B       b721    s721
1882  T       t722    o666 b721  T       t722    o677 b721
1883  B       b722    t722  B       b722    t722
1884  T       t723    o721 b577 b570  T       t723    o676 b719 b722
1885  S       s723    t673 h  B       b723    t723
1886  G       s723    t723  T       t724    o676 b716 b723
 B       b723    s723  
 T       t724    o666 b723  
1887  B       b724    t724  B       b724    t724
1888  T       t725    o721 b578 b570  T       t725    o676 b700 b724
1889  S       s725    t673 h  B       b725    t725
1890  G       s725    t725  T       t726    o676 b682 b725
 B       b725    s725  
 T       t726    o666 b725  
1891  B       b726    t726  B       b726    t726
1892  T       t727    o665 b724 b726  P       p726    Number 1550
1893  B       b727    t727  P       p727    Number 1557
1894  T       t728    o665 b722 b727  O       o727    resource_defs p726 p727 p204
1895    P       p728    Number 1555
1896    O       o728    uid p728 p727
1897    T       t728    o728 b691
1898  B       b728    t728  B       b728    t728
1899  T       t729    o665 b689 b728  T       t729    o b728 b4
1900  B       b729    t729  B       b729    t729
1901  T       t730    o665 b671 b729  T       t730    o727 b729
1902  B       b730    t730  B       b730    t730
1903  T       t731    o665 b705 b730  T       t731    o b730 b4
1904  B       b731    t731  B       b731    t731
1905  T       t732    o665 b703 b731  T       t732    o713 b676 b726 b688 b731
1906  B       b732    t732  B       b732    t732
1907  P       p742    Var s3  T       t733    o712 b732
1908  O       o742    var p742  B       b733    t733
1909  T       t742    o742  P       p733    Number 1797
1910    P       p734    Number 2171
1911    O       o734    location p733 p734
1912    P       p735    String op_wf2
1913    O       o735    rule p735
1914    NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1915    NCzf_itt_member!mem     mem     mem Czf_itt_member
1916    O       o736    mem
1917    T       t736    o736 b714 b591
1918    S       s736    t684 h
1919    G       s736    t736
1920    B       b736    s736
1921    T       t737    o677 b736
1922    B       b737    t737
1923    T       t738    o736 b717 b591
1924    S       s738    t684 h
1925    G       s738    t738
1926    B       b738    s738
1927    T       t739    o677 b738
1928    B       b739    t739
1929    T       t740    o736 b720 b591
1930    S       s740    t684 h
1931    G       s740    t740
1932    B       b740    s740
1933    T       t741    o677 b740
1934    B       b741    t741
1935    T       t742    o676 b739 b741
1936  B       b742    t742  B       b742    t742
1937  T       t743    o689 b742  T       t743    o676 b737 b742
1938  S       s743    t668 h  B       b743    t743
1939  G       s743    t743  T       t744    o676 b700 b743
 B       b743    s743  
 T       t744    o666 b743  
1940  B       b744    t744  B       b744    t744
1941  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  T       t745    o676 b682 b744
1942  NCzf_itt_eq!eq  eq      eq Czf_itt_eq  B       b745    t745
1943  O       o744    eq  T       t746    o676 b719 b745
1944  T       t747    o575 b564 b742 b576  B       b746    t746
1945    T       t747    o676 b716 b746
1946  B       b747    t747  B       b747    t747
1947  T       t748    o575 b564 b742 b577  P       p747    Number 1826
1948    O       o747    resource_defs p207 p747 p204
1949    P       p748    Number 1824
1950    O       o748    uid p748 p747
1951    T       t748    o748 b691
1952  B       b748    t748  B       b748    t748
1953  T       t765    o575 b564 b576 b742  T       t749    o b748 b4
1954    B       b749    t749
1955    T       t750    o747 b749
1956    B       b750    t750
1957    T       t751    o b750 b4
1958    B       b751    t751
1959    T       t752    o735 b676 b747 b688 b751
1960    B       b752    t752
1961    T       t753    o734 b752
1962    B       b753    t753
1963    P       p753    Number 2173
1964    P       p754    Number 2825
1965    O       o754    location p753 p754
1966    P       p755    String op_equiv1
1967    O       o755    rule p755
1968    P       p756    Var s3
1969    O       o756    var p756
1970    T       t756    o756
1971    B       b756    t756
1972    T       t757    o700 b756
1973    S       s757    t679 h
1974    G       s757    t757
1975    B       b757    s757
1976    T       t758    o677 b757
1977    B       b758    t758
1978    P       p758    Var R
1979    O       o758    var p758
1980    T       t759    o758
1981    B       b759    t759
1982    T       t760    o700 b759
1983    S       s760    t679 h
1984    G       s760    t760
1985    B       b760    s760
1986    T       t761    o677 b760
1987    B       b761    t761
1988    NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1989    NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1990    O       o761    equiv
1991    T       t762    o761 b591 b759
1992    S       s762    t684 h
1993    G       s762    t762
1994    B       b762    s762
1995    T       t763    o677 b762
1996    B       b763    t763
1997    T       t764    o736 b756 b591
1998    S       s764    t684 h
1999    G       s764    t764
2000    B       b764    s764
2001    T       t765    o677 b764
2002  B       b765    t765  B       b765    t765
2003  T       t766    o575 b564 b577 b742  T       t766    o761 b591 b759 b714 b717
2004  B       b766    t766  S       s766    t684 h
2005  P       p783    String op_fun1  G       s766    t766
2006  O       o783    rule p783  B       b766    s766
2007  T       t783    o689 b589  T       t767    o677 b766
2008  S       s783    t668 h  B       b767    t767
2009  G       s783    t783  T       t768    o596 b585 b756 b714
2010  B       b783    s783  B       b768    t768
2011  T       t784    o666 b783  T       t769    o596 b585 b756 b717
2012    B       b769    t769
2013    T       t770    o761 b591 b759 b768 b769
2014    S       s770    t684 h
2015    G       s770    t770
2016    B       b770    s770
2017    T       t771    o677 b770
2018    B       b771    t771
2019    T       t772    o676 b767 b771
2020    B       b772    t772
2021    T       t773    o676 b765 b772
2022    B       b773    t773
2023    T       t774    o676 b739 b773
2024    B       b774    t774
2025    T       t775    o676 b737 b774
2026    B       b775    t775
2027    T       t776    o676 b763 b775
2028    B       b776    t776
2029    T       t777    o676 b700 b776
2030    B       b777    t777
2031    T       t778    o676 b682 b777
2032    B       b778    t778
2033    T       t779    o676 b761 b778
2034    B       b779    t779
2035    T       t780    o676 b758 b779
2036    B       b780    t780
2037    T       t781    o676 b719 b780
2038    B       b781    t781
2039    T       t782    o676 b716 b781
2040    B       b782    t782
2041    P       p782    Number 2198
2042    P       p783    Number 2205
2043    O       o783    resource_defs p782 p783 p204
2044    P       p784    Number 2203
2045    O       o784    uid p784 p783
2046    T       t784    o784 b691
2047  B       b784    t784  B       b784    t784
2048  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq  T       t785    o b784 b4
 O       o784    fun_set  
 P       p784    Var z  
 O       o785    var p784  
 T       t785    o785  
2049  B       b785    t785  B       b785    t785
2050  T       t786    o575 b564 b785 b589  T       t786    o783 b785
2051  B       b786    t786 z  B       b786    t786
2052  T       t787    o784 b786  T       t787    o b786 b4
2053  S       s787    t673 h  B       b787    t787
2054  G       s787    t787  T       t788    o755 b676 b782 b688 b787
 B       b787    s787  
 T       t788    o666 b787  
2055  B       b788    t788  B       b788    t788
2056  T       t789    o665 b784 b788  T       t789    o754 b788
2057  B       b789    t789  B       b789    t789
2058  P       p798    String op_fun2  P       p789    Number 2827
2059  O       o798    rule p798  P       p790    Number 3479
2060  T       t798    o575 b564 b589 b785  O       o790    location p789 p790
2061  B       b798    t798 z  P       p791    String op_equiv2
2062  T       t799    o784 b798  O       o791    rule p791
2063  S       s799    t673 h  T       t791    o596 b585 b714 b756
2064  G       s799    t799  B       b791    t791
2065  B       b799    s799  T       t792    o596 b585 b717 b756
2066  T       t800    o666 b799  B       b792    t792
2067    T       t793    o761 b591 b759 b791 b792
2068    S       s793    t684 h
2069    G       s793    t793
2070    B       b793    s793
2071    T       t794    o677 b793
2072    B       b794    t794
2073    T       t795    o676 b767 b794
2074    B       b795    t795
2075    T       t796    o676 b765 b795
2076    B       b796    t796
2077    T       t797    o676 b739 b796
2078    B       b797    t797
2079    T       t798    o676 b737 b797
2080    B       b798    t798
2081    T       t799    o676 b763 b798
2082    B       b799    t799
2083    T       t800    o676 b700 b799
2084  B       b800    t800  B       b800    t800
2085  T       t801    o665 b784 b800  T       t801    o676 b682 b800
2086  B       b801    t801  B       b801    t801
2087  P       p810    String op_assoc1  T       t802    o676 b761 b801
2088  O       o810    rule p810  B       b802    t802
2089  T       t810    o721 b742 b570  T       t803    o676 b758 b802
2090  S       s810    t673 h  B       b803    t803
2091  G       s810    t810  T       t804    o676 b719 b803
2092  B       b810    s810  B       b804    t804
2093  T       t811    o666 b810  T       t805    o676 b716 b804
2094    B       b805    t805
2095    P       p805    Number 2852
2096    P       p806    Number 2859
2097    O       o806    resource_defs p805 p806 p204
2098    P       p807    Number 2857
2099    O       o807    uid p807 p806
2100    T       t807    o807 b691
2101    B       b807    t807
2102    T       t808    o b807 b4
2103    B       b808    t808
2104    T       t809    o806 b808
2105    B       b809    t809
2106    T       t810    o b809 b4
2107    B       b810    t810
2108    T       t811    o791 b676 b805 b688 b810
2109  B       b811    t811  B       b811    t811
2110  NCzf_itt_eq!equal       equal811        equal Czf_itt_eq  T       t812    o790 b811
 O       o811    equal811  
 T       t812    o575 b564 b578 b742  
2111  B       b812    t812  B       b812    t812
2112  T       t813    o575 b564 b576 b766  P       p812    Number 3481
2113  B       b813    t813  P       p813    Number 3826
2114  P       p832    String op_assoc2  O       o813    location p812 p813
2115  O       o832    rule p832  P       p814    String op_equiv_fun1
2116  P       p850    String id_wf1  O       o814    rule p814
2117  O       o850    rule p850  P       p815    Var s
2118  T       t850    o689 b583  O       o815    var p815
2119  S       s850    t673 h  T       t815    o815
2120  G       s850    t850  B       b815    t815
2121  B       b850    s850  T       t816    o700 b815
2122  T       t851    o666 b850  S       s816    t679 h
2123  B       b851    t851  G       s816    t816
2124  T       t852    o665 b689 b851  B       b816    s816
2125  B       b852    t852  T       t817    o677 b816
2126  T       t853    o665 b671 b852  B       b817    t817
2127    NCzf_itt_equiv!equiv_fun_set    equiv_fun_set   equiv_fun_set Czf_itt_equiv
2128    O       o817    equiv_fun_set
2129    P       p817    Var z
2130    O       o818    var p817
2131    T       t818    o818
2132    B       b818    t818
2133    T       t819    o596 b585 b818 b815
2134    B       b819    t819 z
2135    T       t820    o817 b591 b759 b819
2136    S       s820    t684 h
2137    G       s820    t820
2138    B       b820    s820
2139    T       t821    o677 b820
2140    B       b821    t821
2141    T       t822    o676 b763 b821
2142    B       b822    t822
2143    T       t823    o676 b700 b822
2144    B       b823    t823
2145    T       t824    o676 b682 b823
2146    B       b824    t824
2147    T       t825    o676 b761 b824
2148    B       b825    t825
2149    T       t826    o676 b817 b825
2150    B       b826    t826
2151    P       p826    Number 3510
2152    P       p827    Number 3517
2153    O       o827    resource_defs p826 p827 p204
2154    P       p828    Number 3515
2155    O       o828    uid p828 p827
2156    T       t828    o828 b691
2157    B       b828    t828
2158    T       t829    o b828 b4
2159    B       b829    t829
2160    T       t830    o827 b829
2161    B       b830    t830
2162    T       t831    o b830 b4
2163    B       b831    t831
2164    T       t832    o814 b676 b826 b688 b831
2165    B       b832    t832
2166    T       t833    o813 b832
2167    B       b833    t833
2168    P       p833    Number 3828
2169    P       p834    Number 4173
2170    O       o834    location p833 p834
2171    P       p835    String op_equiv_fun2
2172    O       o835    rule p835
2173    T       t835    o596 b585 b815 b818
2174    B       b835    t835 z
2175    T       t836    o817 b591 b759 b835
2176    S       s836    t684 h
2177    G       s836    t836
2178    B       b836    s836
2179    T       t837    o677 b836
2180    B       b837    t837
2181    T       t838    o676 b763 b837
2182    B       b838    t838
2183    T       t839    o676 b700 b838
2184    B       b839    t839
2185    T       t840    o676 b682 b839
2186    B       b840    t840
2187    T       t841    o676 b761 b840
2188    B       b841    t841
2189    T       t842    o676 b817 b841
2190    B       b842    t842
2191    P       p842    Number 3857
2192    P       p843    Number 3864
2193    O       o843    resource_defs p842 p843 p204
2194    P       p844    Number 3862
2195    O       o844    uid p844 p843
2196    T       t844    o844 b691
2197    B       b844    t844
2198    T       t845    o b844 b4
2199    B       b845    t845
2200    T       t846    o843 b845
2201    B       b846    t846
2202    T       t847    o b846 b4
2203    B       b847    t847
2204    T       t848    o835 b676 b842 b688 b847
2205    B       b848    t848
2206    T       t849    o834 b848
2207    B       b849    t849
2208    P       p849    Number 4175
2209    P       p850    Number 4403
2210    O       o850    location p849 p850
2211    P       p851    String op_eq_fun1
2212    O       o851    rule p851
2213    NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
2214    NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq
2215    O       o852    fun_set
2216    T       t852    o852 b819
2217    S       s852    t684 h
2218    G       s852    t852
2219    B       b852    s852
2220    T       t853    o677 b852
2221  B       b853    t853  B       b853    t853
2222  P       p862    String id_wf2  T       t854    o676 b700 b853
2223  O       o862    rule p862  B       b854    t854
2224  T       t862    o721 b583 b570  T       t855    o676 b682 b854
2225  S       s862    t673 h  B       b855    t855
2226  G       s862    t862  T       t856    o676 b817 b855
2227  B       b862    s862  B       b856    t856
2228  T       t863    o666 b862  P       p856    Number 4201
2229    P       p857    Number 4208
2230    O       o857    resource_defs p856 p857 p204
2231    P       p858    Number 4206
2232    O       o858    uid p858 p857
2233    T       t858    o858 b691
2234    B       b858    t858
2235    T       t859    o b858 b4
2236    B       b859    t859
2237    T       t860    o857 b859
2238    B       b860    t860
2239    T       t861    o b860 b4
2240    B       b861    t861
2241    T       t862    o851 b676 b856 b688 b861
2242    B       b862    t862
2243    T       t863    o850 b862
2244  B       b863    t863  B       b863    t863
2245  T       t864    o665 b689 b863  P       p863    Number 4405
2246  B       b864    t864  P       p864    Number 4633
2247  T       t865    o665 b671 b864  O       o864    location p863 p864
2248  B       b865    t865  P       p865    String op_eq_fun2
2249  P       p874    String id_eq1  O       o865    rule p865
2250  O       o874    rule p874  T       t865    o852 b835
2251  T       t874    o721 b589 b570  S       s865    t684 h
2252  S       s874    t673 h  G       s865    t865
2253  G       s874    t874  B       b865    s865
2254  B       b874    s874  T       t866    o677 b865
2255  T       t875    o666 b874  B       b866    t866
2256    T       t867    o676 b700 b866
2257    B       b867    t867
2258    T       t868    o676 b682 b867
2259    B       b868    t868
2260    T       t869    o676 b817 b868
2261    B       b869    t869
2262    P       p869    Number 4431
2263    P       p870    Number 4438
2264    O       o870    resource_defs p869 p870 p204
2265    P       p871    Number 4436
2266    O       o871    uid p871 p870
2267    T       t871    o871 b691
2268    B       b871    t871
2269    T       t872    o b871 b4
2270    B       b872    t872
2271    T       t873    o870 b872
2272    B       b873    t873
2273    T       t874    o b873 b4
2274    B       b874    t874
2275    T       t875    o865 b676 b869 b688 b874
2276  B       b875    t875  B       b875    t875
2277  T       t876    o575 b564 b583 b589  T       t876    o864 b875
2278  B       b876    t876  B       b876    t876
2279  P       p891    String id_eq2  P       p876    Number 4635
2280  O       o891    rule p891  P       p877    Number 5252
2281  T       t891    o575 b564 b589 b583  O       o877    location p876 p877
2282    P       p878    String op_assoc1
2283    O       o878    rule p878
2284    T       t878    o596 b585 b720 b756
2285    B       b878    t878
2286    T       t879    o596 b585 b714 b792
2287    B       b879    t879
2288    T       t880    o761 b591 b759 b878 b879
2289    S       s880    t684 h
2290    G       s880    t880
2291    B       b880    s880
2292    T       t881    o677 b880
2293    B       b881    t881
2294    T       t882    o676 b765 b881
2295    B       b882    t882
2296    T       t883    o676 b739 b882
2297    B       b883    t883
2298    T       t884    o676 b737 b883
2299    B       b884    t884
2300    T       t885    o676 b763 b884
2301    B       b885    t885
2302    T       t886    o676 b700 b885
2303    B       b886    t886
2304    T       t887    o676 b682 b886
2305    B       b887    t887
2306    T       t888    o676 b761 b887
2307    B       b888    t888
2308    T       t889    o676 b758 b888
2309    B       b889    t889
2310    T       t890    o676 b719 b889
2311    B       b890    t890
2312    T       t891    o676 b716 b890
2313  B       b891    t891  B       b891    t891
2314  P       p906    String inv_wf1  P       p891    Number 4660
2315  O       o906    rule p906  P       p892    Number 4667
2316  T       t906    o588 b564 b576  O       o892    resource_defs p891 p892 p204
2317    P       p893    Number 4665
2318    O       o893    uid p893 p892
2319    T       t893    o893 b691
2320    B       b893    t893
2321    T       t894    o b893 b4
2322    B       b894    t894
2323    T       t895    o892 b894
2324    B       b895    t895
2325    T       t896    o b895 b4
2326    B       b896    t896
2327    T       t897    o878 b676 b891 b688 b896
2328    B       b897    t897
2329    T       t898    o877 b897
2330    B       b898    t898
2331    P       p898    Number 5254
2332    P       p899    Number 5871
2333    O       o899    location p898 p899
2334    P       p900    String op_assoc2
2335    O       o900    rule p900
2336    T       t900    o761 b591 b759 b879 b878
2337    S       s900    t684 h
2338    G       s900    t900
2339    B       b900    s900
2340    T       t901    o677 b900
2341    B       b901    t901
2342    T       t902    o676 b765 b901
2343    B       b902    t902
2344    T       t903    o676 b739 b902
2345    B       b903    t903
2346    T       t904    o676 b737 b903
2347    B       b904    t904
2348    T       t905    o676 b763 b904
2349    B       b905    t905
2350    T       t906    o676 b700 b905
2351  B       b906    t906  B       b906    t906
2352  T       t907    o689 b906  T       t907    o676 b682 b906
2353  S       s907    t673 h  B       b907    t907
2354  G       s907    t907  T       t908    o676 b761 b907
 B       b907    s907  
 T       t908    o666 b907  
2355  B       b908    t908  B       b908    t908
2356  T       t909    o665 b722 b908  T       t909    o676 b758 b908
2357  B       b909    t909  B       b909    t909
2358  T       t910    o665 b689 b909  T       t910    o676 b719 b909
2359  B       b910    t910  B       b910    t910
2360  T       t911    o665 b671 b910  T       t911    o676 b716 b910
2361  B       b911    t911  B       b911    t911
2362  T       t912    o665 b703 b911  P       p911    Number 5279
2363  B       b912    t912  P       p912    Number 5286
2364  P       p921    String inv_wf2  O       o912    resource_defs p911 p912 p204
2365  O       o921    rule p921  P       p913    Number 5284
2366  T       t921    o721 b906 b570  O       o913    uid p913 p912
2367  S       s921    t673 h  T       t913    o913 b691
2368  G       s921    t921  B       b913    t913
2369  B       b921    s921  T       t914    o b913 b4
2370  T       t922    o666 b921  B       b914    t914
2371    T       t915    o912 b914
2372    B       b915    t915
2373    T       t916    o b915 b4
2374    B       b916    t916
2375    T       t917    o900 b676 b911 b688 b916
2376    B       b917    t917
2377    T       t918    o899 b917
2378    B       b918    t918
2379    P       p918    Number 5873
2380    P       p919    Number 6041
2381    O       o919    location p918 p919
2382    P       p920    String id_wf1
2383    O       o920    rule p920
2384    T       t920    o700 b604
2385    S       s920    t684 h
2386    G       s920    t920
2387    B       b920    s920
2388    T       t921    o677 b920
2389    B       b921    t921
2390    T       t922    o676 b700 b921
2391  B       b922    t922  B       b922    t922
2392  T       t923    o665 b722 b922  T       t923    o676 b682 b922
2393  B       b923    t923  B       b923    t923
2394  T       t924    o665 b689 b923  P       p923    Number 5895
2395  B       b924    t924  P       p924    Number 5903
2396  T       t925    o665 b671 b924  O       o924    resource_defs p923 p924 p204
2397    P       p925    Number 5901
2398    O       o925    uid p925 p924
2399    T       t925    o925 b691
2400  B       b925    t925  B       b925    t925
2401  T       t926    o665 b703 b925  T       t926    o b925 b4
2402  B       b926    t926  B       b926    t926
2403  P       p935    String inv_fun1  T       t927    o924 b926
2404  O       o935    rule p935  B       b927    t927
2405  T       t935    o588 b564 b785  T       t928    o b927 b4
2406  B       b935    t935 z  B       b928    t928
2407  T       t936    o784 b935  T       t929    o920 b676 b923 b688 b928
2408  S       s936    t673 h  B       b929    t929
2409  G       s936    t936  T       t930    o919 b929
2410  B       b936    s936  B       b930    t930
2411  T       t937    o666 b936  P       p930    Number 6043
2412    P       p931    Number 6217
2413    O       o931    location p930 p931
2414    P       p932    String id_wf2
2415    O       o932    rule p932
2416    T       t932    o736 b604 b591
2417    S       s932    t684 h
2418    G       s932    t932
2419    B       b932    s932
2420    T       t933    o677 b932
2421    B       b933    t933
2422    T       t934    o676 b700 b933
2423    B       b934    t934
2424    T       t935    o676 b682 b934
2425    B       b935    t935
2426    P       p935    Number 6065
2427    P       p936    Number 6072
2428    O       o936    resource_defs p935 p936 p204
2429    P       p937    Number 6070
2430    O       o937    uid p937 p936
2431    T       t937    o937 b691
2432  B       b937    t937  B       b937    t937
2433  T       t938    o665 b689 b937  T       t938    o b937 b4
2434  B       b938    t938  B       b938    t938
2435  T       t939    o665 b671 b938  T       t939    o936 b938
2436  B       b939    t939  B       b939    t939
2437  P       p948    String inv_id1  T       t940    o b939 b4
2438  O       o948    rule p948  B       b940    t940
2439  T       t948    o575 b564 b906 b576  T       t941    o932 b676 b935 b688 b940
2440    B       b941    t941
2441    T       t942    o931 b941
2442    B       b942    t942
2443    P       p942    Number 6219
2444    P       p943    Number 6603
2445    O       o943    location p942 p943
2446    P       p944    String id_eq1
2447    O       o944    rule p944
2448    T       t944    o736 b815 b591
2449    S       s944    t684 h
2450    G       s944    t944
2451    B       b944    s944
2452    T       t945    o677 b944
2453    B       b945    t945
2454    T       t946    o596 b585 b604 b815
2455    B       b946    t946
2456    T       t947    o761 b591 b759 b946 b815
2457    S       s947    t684 h
2458    G       s947    t947
2459    B       b947    s947
2460    T       t948    o677 b947
2461  B       b948    t948  B       b948    t948
2462  P       p925    Number 6113  T       t949    o676 b945 b948
2463  P       p963    String inv_id2  B       b949    t949
2464    T       t950    o676 b763 b949
2465    B       b950    t950
2466    T       t951    o676 b700 b950
2467    B       b951    t951
2468    T       t952    o676 b682 b951
2469    B       b952    t952
2470    T       t953    o676 b761 b952
2471    B       b953    t953
2472    T       t954    o676 b817 b953
2473    B       b954    t954
2474    P       p954    Number 6241
2475    P       p955    Number 6248
2476    O       o955    resource_defs p954 p955 p204
2477    P       p956    Number 6246
2478    O       o956    uid p956 p955
2479    T       t956    o956 b691
2480    B       b956    t956
2481    T       t957    o b956 b4
2482    B       b957    t957
2483    T       t958    o955 b957
2484    B       b958    t958
2485    T       t959    o b958 b4
2486    B       b959    t959
2487    T       t960    o944 b676 b954 b688 b959
2488    B       b960    t960
2489    T       t961    o943 b960
2490    B       b961    t961
2491    P       p961    Number 6605
2492    P       p962    Number 6989
2493    O       o962    location p961 p962
2494    P       p963    String id_eq2
2495  O       o963    rule p963  O       o963    rule p963
2496  T       t963    o575 b564 b576 b906  T       t963    o596 b585 b815 b604
2497  B       b963    t963  B       b963    t963
2498  P       p978    String cancel1  T       t964    o761 b591 b759 b963 b815
2499  O       o978    rule p978  S       s964    t684 h
2500  NSummary!term_param     term_param      term_param Summary  G       s964    t964
2501  O       o979    term_param  B       b964    s964
2502  T       t979    o979 b564  T       t965    o677 b964
2503  B       b979    t979  B       b965    t965
2504  T       t980    o979 b576  T       t966    o676 b945 b965
2505    B       b966    t966
2506    T       t967    o676 b763 b966
2507    B       b967    t967
2508    T       t968    o676 b700 b967
2509    B       b968    t968
2510    T       t969    o676 b682 b968
2511    B       b969    t969
2512    T       t970    o676 b761 b969
2513    B       b970    t970
2514    T       t971    o676 b817 b970
2515    B       b971    t971
2516    P       p971    Number 6627
2517    P       p972    Number 6634
2518    O       o972    resource_defs p971 p972 p204
2519    P       p973    Number 6632
2520    O       o973    uid p973 p972
2521    T       t973    o973 b691
2522    B       b973    t973
2523    T       t974    o b973 b4
2524    B       b974    t974
2525    T       t975    o972 b974
2526    B       b975    t975
2527    T       t976    o b975 b4
2528    B       b976    t976
2529    T       t977    o963 b676 b971 b688 b976
2530    B       b977    t977
2531    T       t978    o962 b977
2532    B       b978    t978
2533    P       p978    Number 6991
2534    P       p979    Number 7260
2535    O       o979    location p978 p979
2536    P       p980    String inv_wf1
2537    O       o980    rule p980
2538    T       t980    o609 b585 b714
2539  B       b980    t980  B       b980    t980
2540  T       t981    o b980 b4  T       t981    o700 b980
2541  B       b981    t981  S       s981    t684 h
2542  T       t982    o b979 b981  G       s981    t981
2543    B       b981    s981
2544    T       t982    o677 b981
2545  B       b982    t982  B       b982    t982
2546  T       t983    o b664 b982  T       t983    o676 b737 b982
2547  B       b983    t983  B       b983    t983
2548  T       t984    o811 b578 b765  T       t984    o676 b700 b983
2549  S       s984    t673 h  B       b984    t984
2550  G       s984    t984  T       t985    o676 b682 b984
2551  B       b984    s984  B       b985    t985
2552  T       t986    o811 b577 b742  T       t986    o676 b716 b985
2553  S       s986    t673 h  B       b986    t986
2554  G       s986    t986  P       p986    Number 7014
2555  B       b986    s986  P       p987    Number 7021
2556  NSummary!interactive    interactive     interactive Summary  O       o987    resource_defs p986 p987 p204
2557  O       o996    interactive  P       p988    Number 7019
2558  NSummary!ext_rule       ext_rule        ext_rule Summary  O       o988    uid p988 p987
2559  P       p996    String "assumT 9 thenT assertT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}} >> thenWT autoT"  T       t988    o988 b691
2560  O       o997    ext_rule p996  B       b988    t988
2561  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  T       t989    o b988 b4
2562  O       o998    status_incomplete  B       b989    t989
2563  T       t998    o998  T       t990    o987 b989
2564    B       b990    t990
2565    T       t991    o b990 b4
2566    B       b991    t991
2567    T       t992    o980 b676 b986 b688 b991
2568    B       b992    t992
2569    T       t993    o979 b992
2570    B       b993    t993
2571    P       p993    Number 7262
2572    P       p994    Number 7538
2573    O       o994    location p993 p994
2574    P       p995    String inv_wf2
2575    O       o995    rule p995
2576    T       t995    o736 b980 b591
2577    S       s995    t684 h
2578    G       s995    t995
2579    B       b995    s995
2580    T       t996    o677 b995
2581    B       b996    t996
2582    T       t997    o676 b737 b996
2583    B       b997    t997
2584    T       t998    o676 b700 b997
2585  B       b998    t998  B       b998    t998
2586  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  T       t999    o676 b682 b998
2587  O       o999    ext_unjustified  B       b999    t999
2588  NSummary!tactic_arg     tactic_arg      tactic_arg Summary  T       t1000   o676 b716 b999
2589  P       p999    String main  B       b1000   t1000
2590  O       o1000   tactic_arg p999  P       p1000   Number 7285
2591  NSummary!msequent       msequent        msequent Summary  P       p1001   Number 7292
2592  O       o1001   msequent  O       o1001   resource_defs p1000 p1001 p204
2593  T       t1001   o b984 b4  P       p1002   Number 7290
2594  B       b1001   t1001  O       o1002   uid p1002 p1001
2595  T       t1002   o b810 b1001  T       t1002   o1002 b691
2596  B       b1002   t1002  B       b1002   t1002
2597  T       t1003   o b723 b1002  T       t1003   o b1002 b4
2598  B       b1003   t1003  B       b1003   t1003
2599  T       t1004   o b721 b1003  T       t1004   o1001 b1003
2600  B       b1004   t1004  B       b1004   t1004
2601  T       t1005   o b688 b1004  T       t1005   o b1004 b4
2602  B       b1005   t1005  B       b1005   t1005
2603  T       t1006   o b670 b1005  T       t1006   o995 b676 b1000 b688 b1005
2604  B       b1006   t1006  B       b1006   t1006
2605  T       t1007   o b743 b1006  T       t1007   o994 b1006
2606  B       b1007   t1007  B       b1007   t1007
2607  T       t1008   o b704 b1007  P       p1007   Number 7540
2608  B       b1008   t1008  P       p1008   Number 7839
2609  T       t1009   o b702 b1008  O       o1008   location p1007 p1008
2610  B       b1009   t1009  P       p1009   String inv_equiv_fun1
2611  T       t1010   o1001 b986 b1009  O       o1009   rule p1009
2612  B       b1010   t1010  T       t1009   o609 b585 b818
2613  NSummary!parent_none    parent_none     parent_none Summary  B       b1009   t1009 z
2614  O       o1010   parent_none  T       t1010   o817 b591 b759 b1009
2615  T       t1011   o1010  S       s1010   t684 h
2616    G       s1010   t1010
2617    B       b1010   s1010
2618    T       t1011   o677 b1010
2619  B       b1011   t1011  B       b1011   t1011
2620  T       t1012   o1000 b1010 b4 b1011  T       t1012   o676 b763 b1011
2621  B       b1012   t1012  B       b1012   t1012
2622  P       p1012   String assertion  T       t1013   o676 b700 b1012
 O       o1012   tactic_arg p1012  
 H       h1012   v t984  
 T       t1013   o575 b564 b906 b578  
2623  B       b1013   t1013  B       b1013   t1013
2624  T       t1014   o575 b564 b906 b765  T       t1014   o676 b682 b1013
2625  B       b1014   t1014  B       b1014   t1014
2626  T       t1015   o811 b1013 b1014  T       t1015   o676 b761 b1014
2627  S       s1015   t673 h h1012  B       b1015   t1015
2628  G       s1015   t1015  P       p1015   Number 7570
2629  B       b1015   s1015  P       p1016   Number 7577
2630  T       t1016   o1001 b1015 b1009  O       o1016   resource_defs p1015 p1016 p204
2631  B       b1016   t1016  P       p1017   Number 7575
2632  S       s1016   t673 h h1012  O       o1017   uid p1017 p1016
2633  G       s1016   t986  T       t1017   o1017 b691
2634  B       b1017   s1016  B       b1017   t1017
2635  T       t1017   o1001 b1017 b1009  T       t1018   o b1017 b4
2636  B       b1018   t1017  B       b1018   t1018
2637  T       t1018   o2 b1012  T       t1019   o1016 b1018
2638  B       b1019   t1018  B       b1019   t1019
2639  T       t1019   o1000 b1018 b4 b1019  T       t1020   o b1019 b4
2640  B       b1020   t1019  B       b1020   t1020
2641  T       t1020   o2 b1020  T       t1021   o1009 b676 b1015 b688 b1020
2642  B       b1021   t1020  B       b1021   t1021
2643  T       t1021   o1012 b1016 b4 b1021  T       t1022   o1008 b1021
2644  B       b1022   t1021  B       b1022   t1022
2645  H       h1022   v_1 t1015  P       p1022   Number 7841
2646  S       s1022   t673 h h1012 h1022  P       p1023   Number 8023
2647  G       s1022   t986  O       o1023   location p1022 p1023
2648  B       b1023   s1022  P       p1024   String inv_eq_fun1
2649  T       t1023   o1001 b1023 b1009  O       o1024   rule p1024
2650  B       b1024   t1023  T       t1024   o852 b1009
2651  T       t1024   o1000 b1024 b4 b1021  S       s1024   t684 h
2652  B       b1025   t1024  G       s1024   t1024
2653  T       t1025   o b1025 b4  B       b1024   s1024
2654  B       b1026   t1025  T       t1025   o677 b1024
2655  T       t1026   o b1022 b1026  B       b1025   t1025
2656  B       b1027   t1026  T       t1026   o676 b700 b1025
2657  T       t1027   o999 b1012 b1027  B       b1026   t1026
2658  B       b1028   t1027  T       t1027   o676 b682 b1026
2659  P       p1028   String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"  B       b1027   t1027
2660  O       o1028   ext_rule p1028  P       p1027   Number 7868
2661  T       t1028   o999 b1022 b4  P       p1028   Number 7875
2662  B       b1029   t1028  O       o1028   resource_defs p1027 p1028 p204
2663  T       t1029   o1028 b998 b1029 b4 b4  P       p1029   Number 7873
2664  B       b1030   t1029  O       o1029   uid p1029 p1028
2665  P       p1030   String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's2}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's2}} >> 3 thenAT autoT"  T       t1029   o1029 b691
2666  O       o1030   ext_rule p1030  B       b1029   t1029
2667  T       t1030   o575 b564 b948 b577  T       t1030   o b1029 b4
2668  B       b1031   t1030  B       b1030   t1030
2669  T       t1031   o811 b1031 b1014  T       t1031   o1028 b1030
2670  H       h1031   v_2 t1031  B       b1031   t1031
2671  S       s1031   t673 h h1012 h1022 h1031  T       t1032   o b1031 b4
2672  G       s1031   t986  B       b1032   t1032
2673  B       b1032   s1031  T       t1033   o1024 b676 b1027 b688 b1032
2674  T       t1032   o1001 b1032 b1009  B       b1033   t1033
2675  B       b1033   t1032  T       t1034   o1023 b1033
2676  T       t1033   o2 b1025  B       b1034   t1034
2677  B       b1034   t1033  P       p1034   Number 8025
2678  T       t1034   o1000 b1033 b4 b1034  P       p1035   Number 8423
2679  B       b1035   t1034  O       o1035   location p1034 p1035
2680  T       t1035   o b1035 b4  P       p1036   String inv_id1
2681  B       b1036   t1035  O       o1036   rule p1036
2682  T       t1036   o999 b1025 b1036  T       t1036   o596 b585 b980 b714
2683  B       b1037   t1036  B       b1036   t1036
2684  P       p1037   String "setSubstT << equal{op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 4 thenAT autoT"  T       t1037   o761 b591 b759 b1036 b604
2685  O       o1037   ext_rule p1037  S       s1037   t684 h
2686  T       t1037   o575 b564 b948 b742  G       s1037   t1037
2687  B       b1038   t1037  B       b1037   s1037
2688  T       t1038   o811 b1031 b1038  T       t1038   o677 b1037
2689  H       h1038   v_3 t1038  B       b1038   t1038
2690  S       s1038   t673 h h1012 h1022 h1031 h1038  T       t1039   o676 b737 b1038
2691  G       s1038   t986  B       b1039   t1039
2692  B       b1039   s1038  T       t1040   o676 b763 b1039
2693  T       t1039   o1001 b1039 b1009  B       b1040   t1040
2694  B       b1040   t1039  T       t1041   o676 b700 b1040
2695  T       t1040   o2 b1035  B       b1041   t1041
2696  B       b1041   t1040  T       t1042   o676 b682 b1041
2697  T       t1041   o1000 b1040 b4 b1041  B       b1042   t1042
2698  B       b1042   t1041  T       t1043   o676 b761 b1042
2699  T       t1042   o b1042 b4  B       b1043   t1043
2700  B       b1043   t1042  T       t1044   o676 b716 b1043
2701  T       t1043   o999 b1035 b1043  B       b1044   t1044
2702  B       b1044   t1043  P       p1044   Number 8048
2703  P       p1044   String "setSubstT << equal{op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 thenAT autoT"  P       p1045   Number 8055
2704  O       o1044   ext_rule p1044  O       o1045   resource_defs p1044 p1045 p204
2705  T       t1044   o575 b564 b583 b577  P       p1046   Number 8053
2706  B       b1045   t1044  O       o1046   uid p1046 p1045
2707  T       t1045   o575 b564 b583 b742  T       t1046   o1046 b691
2708  B       b1046   t1045  B       b1046   t1046
2709  T       t1046   o811 b1045 b1046  T       t1047   o b1046 b4
2710  H       h1046   v_4 t1046  B       b1047   t1047
2711  S       s1046   t673 h h1012 h1022 h1031 h1038 h1046  T       t1048   o1045 b1047
2712  G       s1046   t986  B       b1048   t1048
2713  B       b1047   s1046  T       t1049   o b1048 b4
2714  T       t1047   o1001 b1047 b1009  B       b1049   t1049
2715  B       b1048   t1047  T       t1050   o1036 b676 b1044 b688 b1049
2716  T       t1048   o2 b1042  B       b1050   t1050
2717  B       b1049   t1048  T       t1051   o1035 b1050
2718  T       t1049   o1000 b1048 b4 b1049  B       b1051   t1051
2719  B       b1050   t1049  P       p1051   Number 8425
2720  T       t1050   o b1050 b4  P       p1052   Number 8823
2721  B       b1051   t1050  O       o1052   location p1051 p1052
2722  T       t1051   o999 b1042 b1051  P       p1053   String inv_id2
2723  B       b1052   t1051  O       o1053   rule p1053
2724  P       p1052   String "setSubstT << equal{op{'g; id{'g}; 's2}; 's2} >> 6 thenAT autoT"  T       t1053   o596 b585 b714 b980
2725  O       o1052   ext_rule p1052  B       b1053   t1053
2726  T       t1052   o811 b577 b1046  T       t1054   o761 b591 b759 b1053 b604
2727  H       h1052   v_5 t1052  S       s1054   t684 h
2728  S       s1052   t673 h h1012 h1022 h1031 h1038 h1046 h1052  G       s1054   t1054
2729  G       s1052   t986  B       b1054   s1054
2730  B       b1053   s1052  T       t1055   o677 b1054
2731  T       t1053   o1001 b1053 b1009  B       b1055   t1055
2732  B       b1054   t1053  T       t1056   o676 b737 b1055
2733  T       t1054   o2 b1050  B       b1056   t1056
2734  B       b1055   t1054  T       t1057   o676 b763 b1056
2735  T       t1055   o1000 b1054 b4 b1055  B       b1057   t1057
2736  B       b1056   t1055  T       t1058   o676 b700 b1057
2737  T       t1056   o b1056 b4  B       b1058   t1058
2738  B       b1057   t1056  T       t1059   o676 b682 b1058
2739  T       t1057   o999 b1050 b1057  B       b1059   t1059
2740  B       b1058   t1057  T       t1060   o676 b761 b1059
2741  P       p1058   String "setSubstT << equal{op{'g; id{'g}; 's3}; 's3} >> 7 thenT autoT"  B       b1060   t1060
2742  O       o1058   ext_rule p1058  T       t1061   o676 b716 b1060
2743  T       t1058   o999 b1056 b4  B       b1061   t1061
2744  B       b1059   t1058  P       p1061   Number 8448
2745  T       t1059   o1058 b998 b1059 b4 b4  P       p1062   Number 8455
2746  B       b1060   t1059  O       o1062   resource_defs p1061 p1062 p204
2747  T       t1060   o b1060 b4  P       p1063   Number 8453
2748  B       b1061   t1060  O       o1063   uid p1063 p1062
2749  T       t1061   o1052 b998 b1058 b1061 b4  T       t1063   o1063 b691
2750  B       b1062   t1061  B       b1063   t1063
2751  T       t1062   o b1062 b4  T       t1064   o b1063 b4
2752  B       b1063   t1062  B       b1064   t1064
2753  T       t1063   o1044 b998 b1052 b1063 b4  T       t1065   o1062 b1064
2754  B       b1064   t1063  B       b1065   t1065
2755  T       t1064   o b1064 b4  T       t1066   o b1065 b4
2756  B       b1065   t1064  B       b1066   t1066
2757  T       t1065   o1037 b998 b1044 b1065 b4  T       t1067   o1053 b676 b1061 b688 b1066
2758  B       b1066   t1065  B       b1067   t1067
2759  T       t1066   o b1066 b4  T       t1068   o1052 b1067
2760  B       b1067   t1066  B       b1068   t1068
2761  T       t1067   o1030 b998 b1037 b1067 b4  P       p1068   Number 8845
2762  B       b1068   t1067  P       p1069   Number 9369
2763  T       t1068   o b1068 b4  O       o1069   location p1068 p1069
2764  B       b1069   t1068  P       p1070   String equiv_op_fun1
2765  T       t1069   o b1030 b1069  O       o1070   rule p1070
2766  B       b1070   t1069  T       t1070   o700 b597
2767  T       t1070   o997 b998 b1028 b1070 b4  S       s1070   t679 h
2768  B       b1071   t1070  G       s1070   t1070
2769  T       t1071   o996 b1071  B       b1070   s1070
2770  B       b1072   t1071  T       t1071   o677 b1070
2771  P       p1081   String cancel2  B       b1071   t1071
2772  O       o1081   rule p1081  T       t1072   o700 b598
2773  T       t1081   o979 b742  S       s1072   t679 h
2774  B       b1081   t1081  G       s1072   t1072
2775  T       t1082   o b1081 b4  B       b1072   s1072
2776    T       t1073   o677 b1072
2777    B       b1073   t1073
2778    T       t1074   o736 b597 b591
2779    S       s1074   t684 h
2780    G       s1074   t1074
2781    B       b1074   s1074
2782    T       t1075   o677 b1074
2783    B       b1075   t1075
2784    T       t1076   o736 b598 b591
2785    S       s1076   t684 h
2786    G       s1076   t1076
2787    B       b1076   s1076
2788    T       t1077   o677 b1076
2789    B       b1077   t1077
2790    NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv
2791    O       o1077   equiv_fun_prop
2792    T       t1078   o596 b585 b818 b597
2793    B       b1078   t1078
2794    T       t1079   o596 b585 b818 b598
2795    B       b1079   t1079
2796    T       t1080   o761 b591 b759 b1078 b1079
2797    B       b1080   t1080 z
2798    T       t1081   o1077 b591 b759 b1080
2799    S       s1081   t684 h
2800    G       s1081   t1081
2801    B       b1081   s1081
2802    T       t1082   o677 b1081
2803  B       b1082   t1082  B       b1082   t1082
2804  T       t1083   o b979 b1082  T       t1083   o676 b1077 b1082
2805  B       b1083   t1083  B       b1083   t1083
2806  T       t1084   o b664 b1083  T       t1084   o676 b1075 b1083
2807  B       b1084   t1084  B       b1084   t1084
2808  T       t1085   o811 b765 b766  T       t1085   o676 b763 b1084
2809  S       s1085   t673 h  B       b1085   t1085
2810  G       s1085   t1085  T       t1086   o676 b700 b1085
2811  B       b1085   s1085  B       b1086   t1086
2812  T       t1087   o811 b576 b577  T       t1087   o676 b682 b1086
2813  S       s1087   t673 h  B       b1087   t1087
2814  G       s1087   t1087  T       t1088   o676 b761 b1087
2815  B       b1087   s1087  B       b1088   t1088
2816  P       p1097   String "assumT 9 thenT assertT << equal{op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}} >> thenT autoT"  T       t1089   o676 b1073 b1088
2817  O       o1097   ext_rule p1097  B       b1089   t1089
2818  T       t1098   o b1085 b4  T       t1090   o676 b1071 b1089
2819    B       b1090   t1090
2820    NSummary!interactive    interactive     interactive Summary
2821    O       o1090   interactive
2822    NSummary!ext_rule       ext_rule        ext_rule Summary
2823    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"
2824    O       o1091   ext_rule p1090
2825    NSummary!status_incomplete      status_incomplete       status_incomplete Summary
2826    O       o1092   status_incomplete
2827    T       t1092   o1092
2828    B       b1092   t1092
2829    NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
2830    O       o1093   ext_unjustified
2831    NSummary!tactic_arg     tactic_arg      tactic_arg Summary
2832    P       p1093   String main
2833    O       o1094   tactic_arg p1093
2834    NSummary!msequent       msequent        msequent Summary
2835    O       o1095   msequent
2836    T       t1095   o b1076 b4
2837    B       b1095   t1095
2838    T       t1096   o b1074 b1095
2839    B       b1096   t1096
2840    T       t1097   o b762 b1096
2841    B       b1097   t1097
2842    T       t1098   o b699 b1097
2843  B       b1098   t1098  B       b1098   t1098
2844  T       t1099   o b810 b1098  T       t1099   o b681 b1098
2845  B       b1099   t1099  B       b1099   t1099
2846  T       t1100   o b723 b1099  T       t1100   o b760 b1099
2847  B       b1100   t1100  B       b1100   t1100
2848  T       t1101   o b721 b1100  T       t1101   o b1072 b1100
2849  B       b1101   t1101  B       b1101   t1101
2850  T       t1102   o b688 b1101  T       t1102   o b1070 b1101
2851  B       b1102   t1102  B       b1102   t1102
2852  T       t1103   o b670 b1102  T       t1103   o1095 b1081 b1102
2853  B       b1103   t1103  B       b1103   t1103
2854  T       t1104   o b743 b1103  NSummary!parent_none    parent_none     parent_none Summary
2855    O       o1103   parent_none
2856    T       t1104   o1103
2857  B       b1104   t1104  B       b1104   t1104
2858  T       t1105   o b704 b1104  T       t1105   o1094 b1103 b4 b1104
2859  B       b1105   t1105  B       b1105   t1105
2860  T       t1106   o b702 b1105  NCzf_itt_set!set        set     set Czf_itt_set
2861  B       b1106   t1106  O       o1105   set
2862  T       t1107   o1001 b1087 b1106  T       t1106   o1105
2863  B       b1107   t1107  H       h1106   a_1 t1106
2864  T       t1108   o1000 b1107 b4 b1011  H       h1107   b_1 t1106
2865    H       h1108   x t762
2866    P       p1108   Var a_1
2867    O       o1108   var p1108
2868    T       t1108   o1108
2869  B       b1108   t1108  B       b1108   t1108
2870  H       h1108   v t1085  P       p1109   Var b_1
2871  T       t1109   o588 b564 b742  O       o1109   var p1109
2872    T       t1109   o1109
2873  B       b1109   t1109  B       b1109   t1109
2874  T       t1110   o575 b564 b765 b1109  T       t1110   o761 b591 b759 b1108 b1109
2875  B       b1110   t1110  H       h1110   x_1 t1110
2876  T       t1111   o575 b564 b766 b1109  T       t1111   o596 b585 b1108 b597
2877  B       b1111   t1111  B       b1111   t1111
2878  T       t1112   o811 b1110 b1111  T       t1112   o596 b585 b1108 b598
2879  S       s1112   t673 h h1108  B       b1112   t1112
2880  G       s1112   t1112  T       t1113   o761 b591 b759 b1111 b1112
2881  B       b1112   s1112  H       h1113   x_2 t1113
2882  T       t1113   o1001 b1112 b1106  T       t1114   o596 b585 b1109 b597
2883  B       b1113   t1113  B       b1114   t1114
2884  S       s1113   t673 h h1108  T       t1115   o596 b585 b1109 b598
2885  G       s1113   t1087  B       b1115   t1115
2886  B       b1114   s1113  T       t1116   o761 b591 b759 b1114 b1115
2887  T       t1114   o1001 b1114 b1106  S       s1116   t684 h h1106 h1107 h1108 h1110 h1113
2888  B       b1115   t1114  G       s1116   t1116
2889  T       t1115   o2 b1108  B       b1116   s1116
2890  B       b1116   t1115  T       t1117   o1095 b1116 b1102
2891  T       t1116   o1000 b1115 b4 b1116  B       b1117   t1117
2892  B       b1117   t1116  NItt_logic      Itt_logic       Itt_logic NIL
2893  T       t1117   o2 b1117  NItt_logic!implies      implies implies Itt_logic
2894  B       b1118   t1117  O       o1117   implies
2895  T       t1118   o1012 b1113 b4 b1118  B       b1118   t1113
2896  B       b1119   t1118  B       b1119   t1116
2897  H       h1119   v_1 t1112  T       t1119   o1117 b1118 b1119
2898  S       s1119   t673 h h1108 h1119  S       s1119   t684 h h1106 h1107 h1108 h1110
2899  G       s1119   t1087  G       s1119   t1119
2900  B       b1120   s1119  B       b1120   s1119
2901  T       t1120   o1001 b1120 b1106  T       t1120   o1095 b1120 b1102
2902  B       b1121   t1120  B       b1121   t1120
2903  T       t1121   o1000 b1121 b4 b1118  B       b1122   t1110
2904  B       b1122   t1121  B       b1123   t1119
2905  T       t1122   o b1122 b4  T       t1123   o1117 b1122 b1123
2906  B       b1123   t1122  S       s1123   t684 h h1106 h1107 h1108
2907  T       t1123   o b1119 b1123  G       s1123   t1123
2908  B       b1124   t1123  B       b1124   s1123
2909  T       t1124   o999 b1108 b1124  T       t1124   o1095 b1124 b1102
2910  B       b1125   t1124  B       b1125   t1124
2911  T       t1125   o999 b1119 b4  B       b1126   t762
2912  B       b1126   t1125  B       b1127   t1123
2913  T       t1126   o1028 b998 b1126 b4 b4  T       t1127   o1117 b1126 b1127
2914  B       b1127   t1126  S       s1127   t684 h h1106 h1107
2915  P       p1127   String "setSubstT << equal{op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 3 thenT autoT"  G       s1127   t1127
2916  O       o1127   ext_rule p1127  B       b1128   s1127
2917  T       t1127   o575 b564 b742 b1109  T       t1128   o1095 b1128 b1102
 B       b1128   t1127  
 T       t1128   o575 b564 b576 b1128  
2918  B       b1129   t1128  B       b1129   t1128
2919  T       t1129   o811 b1129 b1111  NItt_logic!all  all     all Itt_logic
2920  H       h1129   v_2 t1129  O       o1129   all
2921  S       s1129   t673 h h1108 h1119 h1129  B       b1130   t1106
2922  G       s1129   t1087  B       b1131   t1127 b_1
2923  B       b1130   s1129  T       t1131   o1129 b1130 b1131
2924  T       t1130   o1001 b1130 b1106  S       s1131   t684 h h1106
2925  B       b1131   t1130  G       s1131   t1131
2926  T       t1131   o2 b1122  B       b1132   s1131
2927  B       b1132   t1131  T       t1132   o1095 b1132 b1102
 T       t1132   o1000 b1131 b4 b1132  
2928  B       b1133   t1132  B       b1133   t1132
2929  T       t1133   o b1133 b4  B       b1134   t1131 a_1
2930  B       b1134   t1133  T       t1134   o1129 b1130 b1134
2931  T       t1134   o999 b1122 b1134  S       s1134   t684 h
2932  B       b1135   t1134  G       s1134   t1134
2933  P       p1135   String "setSubstT << equal{op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 4 thenT autoT"  B       b1135   s1134
2934  O       o1135   ext_rule p1135  T       t1135   o1095 b1135 b1102
 T       t1135   o575 b564 b577 b1128  
2935  B       b1136   t1135  B       b1136   t1135
2936  T       t1136   o811 b1129 b1136  T       t1136   o2 b1105
2937  H       h1136   v_3 t1136  B       b1137   t1136
2938  S       s1136   t673 h h1108 h1119 h1129 h1136  T       t1137   o1094 b1136 b4 b1137
 G       s1136   t1087  
 B       b1137   s1136  
 T       t1137   o1001 b1137 b1106  
2939  B       b1138   t1137  B       b1138   t1137
2940  T       t1138   o2 b1133  T       t1138   o2 b1138
2941  B       b1139   t1138  B       b1139   t1138
2942  T       t1139   o1000 b1138 b4 b1139  T       t1139   o1094 b1133 b4 b1139
2943  B       b1140   t1139  B       b1140   t1139
2944  T       t1140   o b1140 b4  T       t1140   o2 b1140
2945  B       b1141   t1140  B       b1141   t1140
2946  T       t1141   o999 b1133 b1141  T       t1141   o1094 b1129 b4 b1141
2947  B       b1142   t1141  B       b1142   t1141
2948  P       p1142   String "setSubstT << equal{op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 5 thenT autoT"  T       t1142   o2 b1142
 O       o1142   ext_rule p1142  
 T       t1142   o575 b564 b576 b583  
2949  B       b1143   t1142  B       b1143   t1142
2950  T       t1143   o575 b564 b577 b583  T       t1143   o1094 b1125 b4 b1143
2951  B       b1144   t1143  B       b1144   t1143
2952  T       t1144   o811 b1143 b1144  T       t1144   o2 b1144
2953  H       h1144   v_4 t1144  B       b1145   t1144
2954  S       s1144   t673 h h1108 h1119 h1129 h1136 h1144  T       t1145   o1094 b1121 b4 b1145
 G       s1144   t1087  
 B       b1145   s1144  
 T       t1145   o1001 b1145 b1106  
2955  B       b1146   t1145  B       b1146   t1145
2956  T       t1146   o2 b1140  T       t1146   o2 b1146
2957  B       b1147   t1146  B       b1147   t1146
2958  T       t1147   o1000 b1146 b4 b1147  T       t1147   o1094 b1117 b4 b1147
2959  B       b1148   t1147  B       b1148   t1147
2960  T       t1148   o b1148 b4  T       t1148   o b1148 b4
2961  B       b1149   t1148  B       b1149   t1148
2962  T       t1149   o999 b1140 b1149  T       t1149   o1093 b1105 b1149
2963  B       b1150   t1149  B       b1150   t1149
2964  P       p1150   String "setSubstT << equal{op{'g; 's1; id{'g}}; 's1} >> 6 thenT autoT"  P       p1150   String "equivTransT << op{'g; 'b_1; 'a} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
2965  O       o1150   ext_rule p1150  O       o1150   ext_rule p1150
2966  T       t1150   o811 b576 b1144  NItt_logic!and  and     and Itt_logic
2967  H       h1150   v_5 t1150  O       o1151   and
2968  S       s1150   t673 h h1108 h1119 h1129 h1136 h1144 h1150  B       b1151   t700
2969  G       s1150   t1087  B       b1152   t760
2970  B       b1151   s1150  T       t1152   o700 b1111
 T       t1151   o1001 b1151 b1106  
 B       b1152   t1151  
 T       t1152   o2 b1148  
2971  B       b1153   t1152  B       b1153   t1152
2972  T       t1153   o1000 b1152 b4 b1153  T       t1153   o700 b1112
2973  B       b1154   t1153  B       b1154   t1153
2974  T       t1154   o b1154 b4  T       t1154   o1151 b1153 b1154
2975  B       b1155   t1154  B       b1155   t1154
2976  T       t1155   o999 b1148 b1155  T       t1155   o1151 b1152 b1155
2977  B       b1156   t1155  B       b1156   t1155
2978  P       p1156   String "setSubstT << equal{op{'g; 's2; id{'g}}; 's2} >> 7 thenT autoT"  T       t1156   o1151 b1151 b1156
 O       o1156   ext_rule p1156  
 T       t1156   o999 b1154 b4  
2979  B       b1157   t1156  B       b1157   t1156
2980  T       t1157   o1156 b998 b1157 b4 b4  T       t1157   o736 b1111 b591
2981  B       b1158   t1157  B       b1158   t1157
2982  T       t1158   o b1158 b4  T       t1158   o736 b1112 b591
2983  B       b1159   t1158  B       b1159   t1158
2984  T       t1159   o1150 b998 b1156 b1159 b4  T       t1159   o1151 b1158 b1159
2985  B       b1160   t1159  B       b1160   t1159
2986  T       t1160   o b1160 b4  T       t1160   o1151 b1157 b1160
2987  B       b1161   t1160  B       b1161   t1160
2988  T       t1161   o1142 b998 b1150 b1161 b4  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL
2989    NCzf_itt_pair!pair      pair    pair Czf_itt_pair
2990    O       o1161   pair
2991    T       t1161   o1161 b1111 b1112
2992  B       b1162   t1161  B       b1162   t1161
2993  T       t1162   o b1162 b4  T       t1162   o736 b1162 b759
2994  B       b1163   t1162  B       b1163   t1162
2995  T       t1163   o1135 b998 b1142 b1163 b4  T       t1163   o1151 b1161 b1163
2996  B       b1164   t1163  H       h1163   x_2 t1163
2997  T       t1164   o b1164 b4  T       t1164   o736 b1114 b591
2998  B       b1165   t1164  S       s1164   t684 h h1106 h1107 h1108 h1110 h1163
2999  T       t1165   o1127 b998 b1135 b1165 b4  G       s1164   t1164
3000  B       b1166   t1165  B       b1164   s1164
3001  T       t1166   o b1166 b4  T       t1165   o1095 b1164 b1102
3002    B       b1165   t1165
3003    S       s1165   t684 h h1106 h1107 h1108 h1110 h1113
3004    G       s1165   t1164
3005    B       b1166   s1165
3006    T       t1166   o1095 b1166 b1102
3007  B       b1167   t1166  B       b1167   t1166
3008  T       t1167   o b1127 b1167  T       t1167   o2 b1148
3009  B       b1168   t1167  B       b1168   t1167
3010  T       t1168   o1097 b998 b1125 b1168 b4  T       t1168   o1094 b1167 b4 b1168
3011  B       b1169   t1168  B       b1169   t1168
3012  T       t1169   o996 b1169  T       t1169   o2 b1169
3013  B       b1170   t1169  B       b1170   t1169
3014  NOcaml!str_let  str_let str_let Ocaml  T       t1170   o1094 b1165 b4 b1170
3015  NOcaml!patt_var patt_var        patt_var Ocaml  B       b1171   t1170
3016  NOcaml!patt_done        patt_done       patt_done Ocaml  T       t1171   o761 b591 b759 b1111 b1114
3017  NOcaml!fun      fun     fun Ocaml  H       h1171   u t1171
3018  NOcaml!patt_if  patt_if patt_if Ocaml  T       t1172   o761 b591 b759 b1114 b1112
3019  NOcaml!patt_body        patt_body       patt_body Ocaml  H       h1172   v t1172
3020  NOcaml!apply    apply   apply Ocaml  S       s1172   t684 h h1106 h1107 h1108 h1110 h1163 h1171 h1172
3021  NOcaml!lid      lid     lid Ocaml  G       s1172   t1116
3022  O       o1194   lid p978  B       b1172   s1172
3023  T       t1194   o1194  T       t1173   o1095 b1172 b1102
3024    B       b1173   t1173
3025    S       s1173   t684 h h1106 h1107 h1108 h1110 h1113 h1171 h1172
3026    G       s1173   t1116
3027    B       b1174   s1173
3028    T       t1174   o1095 b1174 b1102
3029    B       b1175   t1174
3030    T       t1175   o1094 b1175 b4 b1168
3031    B       b1176   t1175
3032    T       t1176   o2 b1176
3033    B       b1177   t1176
3034    T       t1177   o1094 b1173 b4 b1177
3035    B       b1178   t1177
3036    T       t1178   o b1178 b4
3037    B       b1179   t1178
3038    T       t1179   o b1171 b1179
3039    B       b1180   t1179
3040    T       t1180   o1093 b1148 b1180
3041    B       b1181   t1180
3042    P       p1181   String "autoT thenT rwh unfold_equiv 5 ttca"
3043    O       o1181   ext_rule p1181
3044    T       t1181   o1093 b1171 b4
3045    B       b1182   t1181
3046    T       t1182   o1181 b1092 b1182 b4 b4
3047    B       b1183   t1182
3048    P       p1183   String "equivTransT << op{'g; 'b_1; 'b} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3049    O       o1183   ext_rule p1183
3050    T       t1183   o1093 b1178 b4
3051    B       b1184   t1183
3052    T       t1184   o1183 b1092 b1184 b4 b4
3053    B       b1185   t1184
3054    T       t1185   o b1185 b4
3055    B       b1186   t1185
3056    T       t1186   o b1183 b1186
3057    B       b1187   t1186
3058    T       t1187   o1150 b1092 b1181 b1187 b4
3059    B       b1188   t1187
3060    T       t1188   o b1188 b4
3061    B       b1189   t1188
3062    T       t1189   o1091 b1092 b1150 b1189 b4
3063    B       b1190   t1189
3064    T       t1190   o1090 b1190
3065    B       b1191   t1190
3066    P       p1191   Number 8874
3067    P       p1192   Number 8881
3068    O       o1192   resource_defs p1191 p1192 p204
3069    P       p1193   Number 8879
3070    O       o1193   uid p1193 p1192
3071    T       t1193   o1193 b691
3072    B       b1193   t1193
3073    T       t1194   o b1193 b4
3074  B       b1194   t1194  B       b1194   t1194
3075  NOcaml!proj     proj    proj Ocaml  T       t1195   o1192 b1194
3076  O       o1199   uid p518  B       b1195   t1195
3077  T       t1199   o1199  T       t1196   o b1195 b4
3078  B       b1199   t1199  B       b1196   t1196
3079  P       p1201   String hyp_count_addr  T       t1197   o1070 b676 b1090 b1191 b1196
3080  O       o1201   lid p1201  B       b1197   t1197
3081  T       t1201   o1201  T       t1198   o1069 b1197
3082    B       b1198   t1198
3083    P       p1198   Number 9371
3084    P       p1199   Number 9895
3085    O       o1199   location p1198 p1199
3086    P       p1200   String equiv_op_fun2
3087    O       o1200   rule p1200
3088    T       t1200   o596 b585 b597 b818
3089    B       b1200   t1200
3090    T       t1201   o596 b585 b598 b818
3091  B       b1201   t1201  B       b1201   t1201
3092  P       p1204   Var p  T       t1202   o761 b591 b759 b1200 b1201
3093  O       o1204   var p1204  B       b1202   t1202 z
3094  T       t1204   o1204  T       t1203   o1077 b591 b759 b1202
3095    S       s1203   t684 h
3096    G       s1203   t1203
3097    B       b1203   s1203
3098    T       t1204   o677 b1203
3099  B       b1204   t1204  B       b1204   t1204
3100  P       p1208   Var t1  T       t1205   o676 b1077 b1204
3101  O       o1208   var p1208  B       b1205   t1205
3102  T       t1208   o1208  T       t1206   o676 b1075 b1205
3103    B       b1206   t1206
3104    T       t1207   o676 b763 b1206
3105    B       b1207   t1207
3106    T       t1208   o676 b700 b1207
3107  B       b1208   t1208  B       b1208   t1208
3108  P       p1211   Var t2  T       t1209   o676 b682 b1208
3109  O       o1211   var p1211  B       b1209   t1209
3110  T       t1211   o1211  T       t1210   o676 b761 b1209
3111    B       b1210   t1210
3112    T       t1211   o676 b1073 b1210
3113  B       b1211   t1211  B       b1211   t1211
3114  O       o1249   lid p1081  T       t1212   o676 b1071 b1211
3115  T       t1249   o1249  B       b1212   t1212
3116  B       b1249   t1249  T       t1213   o1095 b1203 b1102
3117  P       p1283   String unique_id1  B       b1213   t1213
3118  O       o1283   rule p1283  T       t1214   o1094 b1213 b4 b1104
3119  P       p1284   Var e2  B       b1214   t1214
3120  O       o1284   var p1284  T       t1215   o596 b585 b597 b1108
3121  T       t1284   o1284  B       b1215   t1215
3122  B       b1284   t1284  T       t1216   o596 b585 b598 b1108
3123  T       t1285   o689 b1284  B       b1216   t1216
3124  S       s1285   t668 h  T       t1217   o761 b591 b759 b1215 b1216
3125  G       s1285   t1285  H       h1217   x_2 t1217
3126  B       b1285   s1285  T       t1218   o596 b585 b597 b1109
3127  T       t1286   o666 b1285  B       b1218   t1218
3128  B       b1286   t1286  T       t1219   o596 b585 b598 b1109
3129  T       t1287   o721 b1284 b570  B       b1219   t1219
3130  S       s1287   t673 h  T       t1220   o761 b591 b759 b1218 b1219
3131  G       s1287   t1287  S       s1220   t684 h h1106 h1107 h1108 h1110 h1217
3132  B       b1287   s1287  G       s1220   t1220
3133  T       t1288   o666 b1287  B       b1220   s1220
3134  B       b1288   t1288  T       t1221   o1095 b1220 b1102
3135  NCzf_itt_dall   Czf_itt_dall    Czf_itt_dall NIL  B       b1221   t1221
3136  NCzf_itt_dall!dall      dall    dall Czf_itt_dall  B       b1222   t1217
3137  O       o1288   dall  B       b1223   t1220
3138  NItt_logic      Itt_logic       Itt_logic NIL  T       t1223   o1117 b1222 b1223
3139  NItt_logic!and  and     and Itt_logic  S       s1223   t684 h h1106 h1107 h1108 h1110
3140  O       o1289   and  G       s1223   t1223
3141  T       t1289   o575 b564 b1284 b589  B       b1224   s1223
3142  B       b1289   t1289  T       t1224   o1095 b1224 b1102
3143  T       t1290   o744 b1289 b589  B       b1225   t1224
3144  B       b1290   t1290  B       b1226   t1223
3145  T       t1291   o575 b564 b589 b1284  T       t1226   o1117 b1122 b1226
3146  B       b1291   t1291  S       s1226   t684 h h1106 h1107 h1108
3147  T       t1292   o744 b1291 b589  G       s1226   t1226
3148    B       b1227   s1226
3149    T       t1227   o1095 b1227 b1102
3150    B       b1228   t1227
3151    B       b1229   t1226
3152    T       t1229   o1117 b1126 b1229
3153    S       s1229   t684 h h1106 h1107
3154    G       s1229   t1229
3155    B       b1230   s1229
3156    T       t1230   o1095 b1230 b1102
3157    B       b1231   t1230
3158    B       b1232   t1229 b_1
3159    T       t1232   o1129 b1130 b1232
3160    S       s1232   t684 h h1106
3161    G       s1232   t1232
3162    B       b1233   s1232
3163    T       t1233   o1095 b1233 b1102
3164    B       b1234   t1233
3165    B       b1235   t1232 a_1
3166    T       t1235   o1129 b1130 b1235
3167    S       s1235   t684 h
3168    G       s1235   t1235
3169    B       b1236   s1235
3170    T       t1236   o1095 b1236 b1102
3171    B       b1237   t1236
3172    T       t1237   o2 b1214
3173    B       b1238   t1237
3174    T       t1238   o1094 b1237 b4 b1238
3175    B       b1239   t1238
3176    T       t1239   o2 b1239
3177    B       b1240   t1239
3178    T       t1240   o1094 b1234 b4 b1240
3179    B       b1241   t1240
3180    T       t1241   o2 b1241
3181    B       b1242   t1241
3182    T       t1242   o1094 b1231 b4 b1242
3183    B       b1243   t1242
3184    T       t1243   o2 b1243
3185    B       b1244   t1243
3186    T       t1244   o1094 b1228 b4 b1244
3187    B       b1245   t1244
3188    T       t1245   o2 b1245
3189    B       b1246   t1245
3190    T       t1246   o1094 b1225 b4 b1246
3191    B       b1247   t1246
3192    T       t1247   o2 b1247
3193    B       b1248   t1247
3194    T       t1248   o1094 b1221 b4 b1248
3195    B       b1249   t1248
3196    T       t1249   o b1249 b4
3197    B       b1250   t1249
3198    T       t1250   o1093 b1214 b1250
3199    B       b1251   t1250
3200    P       p1251   String "equivTransT << op{'g; 'a; 'b_1} >> 6 ttca thenT rwh unfold_equiv 6 ttca"
3201    O       o1251   ext_rule p1251
3202    T       t1251   o700 b1215
3203    B       b1252   t1251
3204    T       t1252   o700 b1216
3205    B       b1253   t1252
3206    T       t1253   o1151 b1252 b1253
3207    B       b1254   t1253
3208    T       t1254   o1151 b1152 b1254
3209    B       b1255   t1254
3210    T       t1255   o1151 b1151 b1255
3211    B       b1256   t1255
3212    T       t1256   o736 b1215 b591
3213    B       b1257   t1256
3214    T       t1257   o736 b1216 b591
3215    B       b1258   t1257
3216    T       t1258   o1151 b1257 b1258
3217    B       b1259   t1258
3218    T       t1259   o1151 b1256 b1259
3219    B       b1260   t1259
3220    T       t1260   o1161 b1215 b1216
3221    B       b1261   t1260
3222    T       t1261   o736 b1261 b759
3223    B       b1262   t1261
3224    T       t1262   o1151 b1260 b1262
3225    H       h1262   x_2 t1262
3226    T       t1263   o736 b1218 b591
3227    S       s1263   t684 h h1106 h1107 h1108 h1110 h1262
3228    G       s1263   t1263
3229    B       b1263   s1263
3230    T       t1264   o1095 b1263 b1102
3231    B       b1264   t1264
3232    S       s1264   t684 h h1106 h1107 h1108 h1110 h1217
3233    G       s1264   t1263
3234    B       b1265   s1264
3235    T       t1265   o1095 b1265 b1102
3236    B       b1266   t1265
3237    T       t1266   o2 b1249
3238    B       b1267   t1266
3239    T       t1267   o1094 b1266 b4 b1267
3240    B       b1268   t1267
3241    T       t1268   o2 b1268
3242    B       b1269   t1268
3243    T       t1269   o1094 b1264 b4 b1269
3244    B       b1270   t1269
3245    T       t1270   o761 b591 b759 b1215 b1218
3246    H       h1270   u t1270
3247    T       t1271   o761 b591 b759 b1218 b1216
3248    H       h1271   v t1271
3249    S       s1271   t684 h h1106 h1107 h1108 h1110 h1262 h1270 h1271
3250    G       s1271   t1220
3251    B       b1271   s1271
3252    T       t1272   o1095 b1271 b1102
3253    B       b1272   t1272
3254    S       s1272   t684 h h1106 h1107 h1108 h1110 h1217 h1270 h1271
3255    G       s1272   t1220
3256    B       b1273   s1272
3257    T       t1273   o1095 b1273 b1102
3258    B       b1274   t1273
3259    T       t1274   o1094 b1274 b4 b1267
3260    B       b1275   t1274
3261    T       t1275   o2 b1275
3262    B       b1276   t1275
3263    T       t1276   o1094 b1272 b4 b1276
3264    B       b1277   t1276
3265    T       t1277   o b1277 b4
3266    B       b1278   t1277
3267    T       t1278   o b1270 b1278
3268    B       b1279   t1278
3269    T       t1279   o1093 b1249 b1279
3270    B       b1280   t1279
3271    T       t1280   o1093 b1270 b4
3272    B       b1281   t1280
3273    T       t1281   o1181 b1092 b1281 b4 b4
3274    B       b1282   t1281
3275    P       p1282   String "equivTransT << op{'g; 'b; 'b_1} >> 8 ttca thenT rwh unfold_equiv 8 thenT autoT thenT rwh unfold_equiv 5 ttca"
3276    O       o1282   ext_rule p1282
3277    T       t1282   o1093 b1277 b4
3278    B       b1283   t1282
3279    T       t1283   o1282 b1092 b1283 b4 b4
3280    B       b1284   t1283
3281    T       t1284   o b1284 b4
3282    B       b1285   t1284
3283    T       t1285   o b1282 b1285
3284    B       b1286   t1285
3285    T       t1286   o1251 b1092 b1280 b1286 b4
3286    B       b1287   t1286
3287    T       t1287   o b1287 b4
3288    B       b1288   t1287
3289    T       t1288   o1091 b1092 b1251 b1288 b4
3290    B       b1289   t1288
3291    T       t1289   o1090 b1289
3292    B       b1290   t1289
3293    P       p1290   Number 9400
3294    P       p1291   Number 9407
3295    O       o1291   resource_defs p1290 p1291 p204
3296    P       p1292   Number 9405
3297    O       o1292   uid p1292 p1291
3298    T       t1292   o1292 b691
3299  B       b1292   t1292  B       b1292   t1292
3300  T       t1293   o1289 b1290 b1292  T       t1293   o b1292 b4
3301  B       b1293   t1293 s  B       b1293   t1293
3302  T       t1294   o1288 b570 b1293  T       t1294   o1291 b1293
3303  S       s1294   t673 h  B       b1294   t1294
3304  G       s1294   t1294  T       t1295   o b1294 b4
3305  B       b1294   s1294  B       b1295   t1295
3306  T       t1296   o744 b1284 b583  T       t1296   o1200 b676 b1212 b1290 b1295
3307  S       s1296   t673 h  B       b1296   t1296
3308  G       s1296   t1296  T       t1297   o1199 b1296
3309  B       b1296   s1296  B       b1297   t1297
3310  P       p1302   String "assumT 5 thenT withT << id{'g} >> (dT 2) thenT autoT"  P       p1297   Number 11515
3311  O       o1302   ext_rule p1302  P       p1298   Number 12822
3312  T       t1303   o b1294 b4  O       o1298   location p1297 p1298
3313  B       b1303   t1303  P       p1299   String cancel1
3314  T       t1304   o b1287 b1303  O       o1299   rule p1299
3315  B       b1304   t1304  P       p1300   String J
3316  T       t1305   o b688 b1304  O       o1300   context_param p1300
3317    T       t1300   o1300
3318    B       b1300   t1300
3319    T       t1301   o b1300 b4
3320    B       b1301   t1301
3321    T       t1302   o b675 b1301
3322    B       b1302   t1302
3323    T       t1303   o761 b591 b759 b720 b791
3324    H       h1303   x t1303
3325    P       p1303   Var x
3326    O       o1303   var p1303
3327    T       t1304   o1303
3328    C       h1304   J t1304
3329    S       s1304   t679 h h1303 h1304
3330    G       s1304   t715
3331    B       b1304   s1304
3332    T       t1305   o677 b1304
3333  B       b1305   t1305  B       b1305   t1305
3334  T       t1306   o b670 b1305  S       s1305   t679 h h1303 h1304
3335  B       b1306   t1306  G       s1305   t718
3336  T       t1307   o b1285 b1306  B       b1306   s1305
3337  B       b1307   t1307  T       t1306   o677 b1306
3338  T       t1308   o1001 b1296 b1307  B       b1307   t1306
3339  B       b1308   t1308  S       s1307   t679 h h1303 h1304
3340  T       t1309   o1000 b1308 b4 b1011  G       s1307   t757
3341  B       b1309   t1309  B       b1308   s1307
3342  H       h1309   v t1294  T       t1308   o677 b1308
3343  T       t1310   o575 b564 b1284 b583  B       b1309   t1308
3344  B       b1310   t1310  S       s1309   t679 h h1303 h1304
3345  T       t1311   o744 b1310 b583  G       s1309   t760
3346  H       h1311   y t1311  B       b1310   s1309
3347  T       t1312   o575 b564 b583 b1284  T       t1310   o677 b1310
3348  B       b1312   t1312  B       b1311   t1310
3349  T       t1313   o744 b1312 b583  S       s1311   t679 h h1303 h1304
3350  H       h1313   z t1313  G       s1311   t681
3351  S       s1313   t673 h h1309 h1311 h1313  B       b1312   s1311
3352  G       s1313   t1296  T       t1312   o677 b1312
3353  B       b1313   s1313  B       b1313   t1312
3354  T       t1314   o1001 b1313 b1307  S       s1313   t684 h h1303 h1304
3355  B       b1314   t1314  G       s1313   t586
3356  B       b1315   t1311  B       b1314   s1313
3357  B       b1316   t1313  T       t1314   o677 b1314
3358  T       t1316   o1289 b1315 b1316  B       b1315   t1314
3359  H       h1316   w t1316  S       s1315   t684 h h1303 h1304
3360  S       s1316   t673 h h1309 h1316  G       s1315   t762
3361  G       s1316   t1296  B       b1316   s1315
3362  B       b1317   s1316  T       t1316   o677 b1316
3363  T       t1317   o1001 b1317 b1307  B       b1317   t1316
3364  B       b1318   t1317  S       s1317   t684 h h1303 h1304
3365  S       s1318   t673 h h1309  G       s1317   t736
3366  G       s1318   t1296  B       b1318   s1317
3367  B       b1319   s1318  T       t1318   o677 b1318
3368  T       t1319   o1001 b1319 b1307  B       b1319   t1318
3369  B       b1320   t1319  S       s1319   t684 h h1303 h1304
3370  NSummary!arg_named      arg_named       arg_named Summary  G       s1319   t738
3371  P       p1320   String with  B       b1320   s1319
3372  O       o1320   arg_named p1320  T       t1320   o677 b1320
3373  NSummary!arg_term_list  arg_term_list   arg_term_list Summary  B       b1321   t1320
3374  O       o1321   arg_term_list  S       s1321   t684 h h1303 h1304
3375  T       t1321   o b583 b4  G       s1321   t764
3376  B       b1321   t1321  B       b1322   s1321
3377  T       t1322   o1321 b1321  T       t1322   o677 b1322
3378  B       b1322   t1322  B       b1323   t1322
3379  T       t1323   o1320 b1322  T       t1323   o761 b591 b759 b717 b756
3380  B       b1323   t1323  S       s1323   t684 h h1303 h1304
3381  T       t1324   o b1323 b4  G       s1323   t1323
3382  B       b1324   t1324  B       b1324   s1323
3383  T       t1325   o2 b1309  T       t1324   o677 b1324
3384  B       b1325   t1325  B       b1325   t1324
3385  T       t1326   o1000 b1320 b1324 b1325  T       t1325   o676 b1323 b1325
3386  B       b1326   t1326  B       b1326   t1325
3387  T       t1327   o2 b1326  T       t1326   o676 b1321 b1326
3388  B       b1327   t1327  B       b1327   t1326
3389  T       t1328   o1000 b1318 b4 b1327  T       t1327   o676 b1319 b1327
3390  B       b1328   t1328  B       b1328   t1327
3391  T       t1329   o2 b1328  T       t1328   o676 b1317 b1328
3392  B       b1329   t1329  B       b1329   t1328
3393  T       t1330   o1000 b1314 b4 b1329  T       t1329   o676 b1315 b1329
3394  B       b1330   t1330  B       b1330   t1329
3395  T       t1331   o b1330 b4  T       t1330   o676 b1313 b1330
3396  B       b1331   t1331  B       b1331   t1330
3397  T       t1332   o999 b1309 b1331  T       t1331   o676 b1311 b1331
3398  B       b1332   t1332  B       b1332   t1331
3399  P       p1332   String "setSubstT << equal{op{'g; id{'g}; 'e2}; 'e2} >> 4 thenT autoT"  T       t1332   o676 b1309 b1332
3400  O       o1332   ext_rule p1332  B       b1333   t1332
3401  T       t1333   o999 b1330 b4  T       t1333   o676 b1307 b1333
3402  B       b1333   t1333  B       b1334   t1333
3403  T       t1334   o1332 b998 b1333 b4 b4  T       t1334   o676 b1305 b1334
3404  B       b1334   t1334  B       b1335   t1334
3405  T       t1335   o b1334 b4  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"
3406  B       b1335   t1335  O       o1335   ext_rule p1335
3407  T       t1336   o1302 b998 b1332 b1335 b4  T       t1335   o b1322 b4
3408  B       b1336   t1336  B       b1336   t1335
3409  T       t1337   o996 b1336  T       t1336   o b1320 b1336
3410  B       b1337   t1337  B       b1337   t1336
3411  P       p1346   String unique_id2  T       t1337   o b1318 b1337
3412  O       o1346   rule p1346  B       b1338   t1337
3413  B       b1346   t1290 s  T       t1338   o b1316 b1338
3414  T       t1346   o1288 b570 b1346  B       b1339   t1338
3415  S       s1346   t673 h  T       t1339   o b1314 b1339
3416  G       s1346   t1346  B       b1340   t1339
3417  B       b1347   s1346  T       t1340   o b1312 b1340
3418  P       p1353   String "assumT 5"  B       b1341   t1340
3419  O       o1353   ext_rule p1353  T       t1341   o b1310 b1341
3420  T       t1353   o b1347 b4  B       b1342   t1341
3421    T       t1342   o b1308 b1342
3422    B       b1343   t1342
3423    T       t1343   o b1306 b1343
3424    B       b1344   t1343
3425    T       t1344   o b1304 b1344
3426    B       b1345   t1344
3427    T       t1345   o1095 b1324 b1345
3428    B       b1346   t1345
3429    T       t1346   o1094 b1346 b4 b1104
3430    B       b1347   t1346
3431    T       t1347   o596 b585 b980 b720
3432    B       b1348   t1347
3433    T       t1348   o596 b585 b980 b791
3434    B       b1349   t1348
3435    T       t1349   o761 b591 b759 b1348 b1349
3436    H       h1349   v t1349
3437    S       s1349   t684 h h1303 h1304 h1349
3438    G       s1349   t1323
3439    B       b1350   s1349
3440    T       t1350   o1095 b1350 b1345
3441    B       b1351   t1350
3442    T       t1351   o2 b1347
3443    B       b1352   t1351
3444    T       t1352   o1094 b1351 b4 b1352
3445    B       b1353   t1352
3446    T       t1353   o b1353 b4
3447  B       b1354   t1353  B       b1354   t1353
3448  T       t1354   o b1287 b1354  T       t1354   o1093 b1347 b1354
3449  B       b1355   t1354  B       b1355   t1354
3450  T       t1355   o b688 b1355  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"
3451    O       o1355   ext_rule p1355
3452    T       t1355   o596 b585 b1036 b717
3453  B       b1356   t1355  B       b1356   t1355
3454  T       t1356   o b670 b1356  T       t1356   o761 b591 b759 b1356 b1349
3455  B       b1357   t1356  H       h1356   z t1356
3456  T       t1357   o b1285 b1357  S       s1356   t684 h h1303 h1304 h1349 h1356
3457    G       s1356   t1323
3458    B       b1357   s1356
3459    T       t1357   o1095 b1357 b1345
3460  B       b1358   t1357  B       b1358   t1357
3461  T       t1358   o1001 b1296 b1358  T       t1358   o2 b1353
3462  B       b1359   t1358  B       b1359   t1358
3463  T       t1359   o1000 b1359 b4 b1011  T       t1359   o1094 b1358 b4 b1359
3464  B       b1360   t1359  B       b1360   t1359
3465  H       h1360   v t1346  T       t1360   o b1360 b4
3466  S       s1360   t673 h h1360  B       b1361   t1360
3467  G       s1360   t1296  T       t1361   o1093 b1353 b1361
 B       b1361   s1360  
 T       t1361   o1001 b1361 b1358  
3468  B       b1362   t1361  B       b1362   t1361
3469  T       t1362   o2 b1360  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"
3470    O       o1362   ext_rule p1362
3471    T       t1362   o596 b585 b1036 b756
3472  B       b1363   t1362  B       b1363   t1362
3473  T       t1363   o1000 b1362 b4 b1363  T       t1363   o761 b591 b759 b1356 b1363
3474  B       b1364   t1363  H       h1363   z_1 t1363
3475  T       t1364   o b1364 b4  S       s1363   t684 h h1303 h1304 h1349 h1356 h1363
3476    G       s1363   t1323
3477    B       b1364   s1363
3478    T       t1364   o1095 b1364 b1345
3479  B       b1365   t1364  B       b1365   t1364
3480  T       t1365   o999 b1360 b1365  T       t1365   o2 b1360
3481  B       b1366   t1365  B       b1366   t1365
3482  P       p1366   String "withT << id{'g} >> (dT 2) thenAT autoT"  T       t1366   o1094 b1365 b4 b1366
3483  O       o1366   ext_rule p1366  B       b1367   t1366
3484  H       h1366   w t1311  T       t1367   o b1367 b4
 S       s1366   t673 h h1360 h1366  
 G       s1366   t1296  
 B       b1367   s1366  
 T       t1367   o1001 b1367 b1358  
3485  B       b1368   t1367  B       b1368   t1367
3486  T       t1368   o1000 b1362 b1324 b1363  T       t1368   o1093 b1360 b1368
3487  B       b1369   t1368  B       b1369   t1368
3488  T       t1369   o2 b1369  P       p1369   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 6 ttca"
3489    O       o1369   ext_rule p1369
3490    T       t1369   o596 b585 b604 b717
3491  B       b1370   t1369  B       b1370   t1369
3492  T       t1370   o1000 b1368 b4 b1370  T       t1370   o596 b585 b604 b756
3493  B       b1371   t1370  B       b1371   t1370
3494  T       t1371   o b1371 b4  T       t1371   o761 b591 b759 b1370 b1371
3495  B       b1372   t1371  H       h1371   z_2 t1371
3496  T       t1372   o999 b1364 b1372  S       s1371   t684 h h1303 h1304 h1349 h1356 h1363 h1371
3497    G       s1371   t1323
3498    B       b1372   s1371
3499    T       t1372   o1095 b1372 b1345
3500  B       b1373   t1372  B       b1373   t1372
3501  P       p1373   String "setSubstT << equal{op{'g; 'e2; id{'g}}; 'e2} >> 3 thenT autoT"  T       t1373   o2 b1367
 O       o1373   ext_rule p1373  
 T       t1373   o999 b1371 b4  
3502  B       b1374   t1373  B       b1374   t1373
3503  T       t1374   o1373 b998 b1374 b4 b4  T       t1374   o1094 b1373 b4 b1374
3504  B       b1375   t1374  B       b1375   t1374
3505  T       t1375   o b1375 b4  T       t1375   o b1375 b4
3506  B       b1376   t1375  B       b1376   t1375
3507  T       t1376   o1366 b998 b1373 b1376 b4  T       t1376   o1093 b1367 b1376
3508  B       b1377   t1376  B       b1377   t1376
3509  T       t1377   o b1377 b4  P       p1377   String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 7 ttca"
3510  B       b1378   t1377  O       o1377   ext_rule p1377
3511  T       t1378   o1353 b998 b1366 b1378 b4  T       t1377   o761 b591 b759 b717 b1371
3512    H       h1377   z_3 t1377
3513    S       s1377   t684 h h1303 h1304 h1349 h1356 h1363 h1371 h1377
3514    G       s1377   t1323
3515    B       b1378   s1377
3516    T       t1378   o1095 b1378 b1345
3517  B       b1379   t1378  B       b1379   t1378
3518  T       t1379   o996 b1379  T       t1379   o2 b1375
3519  B       b1380   t1379  B       b1380   t1379
3520  P       p2068   Number 9097  T       t1380   o1094 b1379 b4 b1380
3521  P       p1432   String unique_inv1  B       b1381   t1380
3522  O       o1432   rule p1432  T       t1381   o b1381 b4
3523  T       t1432   o575 b564 b577 b589  B       b1382   t1381
3524  B       b1432   t1432  T       t1382   o1093 b1375 b1382
3525  T       t1433   o811 b1432 b583  B       b1383   t1382
3526  S       s1433   t673 h  P       p1383   String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 8 ttca"
3527  G       s1433   t1433  O       o1383   ext_rule p1383
3528  B       b1433   s1433  T       t1383   o1093 b1381 b4
3529  T       t1435   o811 b577 b590  B       b1384   t1383
3530  S       s1435   t673 h  T       t1384   o1383 b1092 b1384 b4 b4
3531  G       s1435   t1435  B       b1385   t1384
3532  B       b1435   s1435  T       t1385   o b1385 b4
3533  P       p1443   String "assumT 7 thenT setSubstT << equal{id{'g}; op{'g; inv{'g; 's}; 's}}>> 2 thenAT autoT"  B       b1386   t1385
3534  O       o1443   ext_rule p1443  T       t1386   o1377 b1092 b1383 b1386 b4
3535  T       t1444   o b1433 b4  B       b1387   t1386
3536  B       b1444   t1444  T       t1387   o b1387 b4
3537  T       t1445   o b723 b1444  B       b1388   t1387
3538  B       b1445   t1445  T       t1388   o1369 b1092 b1377 b1388 b4
3539  T       t1446   o b874 b1445  B       b1389   t1388
3540  B       b1446   t1446  T       t1389   o b1389 b4
3541  T       t1447   o b688 b1446  B       b1390   t1389
3542  B       b1447   t1447  T       t1390   o1362 b1092 b1369 b1390 b4
3543  T       t1448   o b670 b1447  B       b1391   t1390
3544  B       b1448   t1448  T       t1391   o b1391 b4
3545  T       t1449   o b704 b1448  B       b1392   t1391
3546  B       b1449   t1449  T       t1392   o1355 b1092 b1362 b1392 b4
3547  T       t1450   o b783 b1449  B       b1393   t1392
3548  B       b1450   t1450  T       t1393   o b1393 b4
3549  T       t1451   o1001 b1435 b1450  B       b1394   t1393
3550  B       b1451   t1451  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"
3551  T       t1452   o1000 b1451 b4 b1011  O       o1394   ext_rule p1394
3552  B       b1452   t1452  H       h1394   v t1303
3553  P       p1452   String eq  H       h1395   v_1 t1349
3554  O       o1452   tactic_arg p1452  S       s1395   t684 h h1394 h1395
3555  H       h1452   v t1433  G       s1395   t1323
3556  T       t1453   o575 b564 b590 b589  B       b1395   s1395
3557  B       b1453   t1453  S       s1396   t684 h
3558  T       t1454   o744 b583 b1453  G       s1396   t1303
3559  S       s1454   t673 h h1452  B       b1396   s1396
3560  G       s1454   t1454  T       t1396   o b1396 b4
3561  B       b1454   s1454  B       b1397   t1396
3562  T       t1455   o1001 b1454 b1450  T       t1397   o b764 b1397
3563  B       b1455   t1455  B       b1398   t1397
3564  T       t1456   o811 b583 b1453  T       t1398   o b738 b1398
3565  S       s1456   t673 h h1452  B       b1399   t1398
3566  G       s1456   t1456  T       t1399   o b736 b1399
3567  B       b1456   s1456  B       b1400   t1399
3568  T       t1457   o1001 b1456 b1450  T       t1400   o b762 b1400
3569  B       b1457   t1457  B       b1401   t1400
3570  P       p1457   String d_auto  T       t1401   o b699 b1401
3571  O       o1457   arg_named p1457  B       b1402   t1401
3572  NSummary!arg_bool       arg_bool        arg_bool Summary  T       t1402   o b681 b1402
3573  P       p1458   String true  B       b1403   t1402
3574  O       o1458   arg_bool p1458  T       t1403   o b760 b1403
3575  T       t1458   o1458  B       b1404   t1403
3576  B       b1458   t1458  T       t1404   o b757 b1404
3577  T       t1459   o1457 b1458  B       b1405   t1404
3578  B       b1459   t1459  T       t1405   o b718 b1405
3579  T       t1460   o b1459 b4  B       b1406   t1405
3580  B       b1460   t1460  T       t1406   o b715 b1406
3581  S       s1460   t673 h h1452  B       b1407   t1406
3582  G       s1460   t1435  T       t1407   o1095 b1395 b1407
3583  B       b1461   s1460  B       b1408   t1407
3584  T       t1461   o1001 b1461 b1450  S       s1408   t684 h h1394
3585  B       b1462   t1461  G       s1408   t1323
3586  T       t1462   o2 b1452  B       b1409   s1408
3587    T       t1409   o1095 b1409 b1407
3588    B       b1410   t1409
3589    S       s1410   t684 h
3590    G       s1410   t1323
3591    B       b1411   s1410
3592    T       t1411   o1095 b1411 b1407
3593    B       b1412   t1411
3594    T       t1412   o1094 b1412 b4 b1104
3595    B       b1413   t1412
3596    T       t1413   o2 b1413
3597    B       b1414   t1413
3598    T       t1414   o1094 b1410 b4 b1414
3599    B       b1415   t1414
3600    T       t1415   o2 b1415
3601    B       b1416   t1415
3602    T       t1416   o1094 b1408 b4 b1416
3603    B       b1417   t1416
3604    S       s1417   t684 h h1394 h1395 h1356
3605    G       s1417   t1323
3606    B       b1418   s1417
3607    T       t1418   o1095 b1418 b1407
3608    B       b1419   t1418
3609    T       t1419   o2 b1417
3610    B       b1420   t1419
3611    T       t1420   o1094 b1419 b4 b1420
3612    B       b1421   t1420
3613    T       t1421   o b1421 b4
3614    B       b1422   t1421
3615    T       t1422   o1093 b1417 b1422
3616    B       b1423   t1422
3617    P       p1423   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; op{'g; 's1; 's3}}; op{'g; op{'g; inv{'g; 's1}; 's1}; 's3}} >> 4 ttca"
3618    O       o1423   ext_rule p1423
3619    S       s1423   t684 h h1394 h1395 h1356 h1363
3620    G       s1423   t1323
3621    B       b1424   s1423
3622    T       t1424   o1095 b1424 b1407
3623    B       b1425   t1424
3624    T       t1425   o2 b1421
3625    B       b1426   t1425
3626    T       t1426   o1094 b1425 b4 b1426
3627    B       b1427   t1426
3628    T       t1427   o b1427 b4
3629    B       b1428   t1427
3630    T       t1428   o1093 b1421 b1428
3631    B       b1429   t1428
3632    P       p1429   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 's1}; 's1}; id{'g}} >> 5 ttca"
3633    O       o1429   ext_rule p1429
3634    S       s1429   t684 h h1394 h1395 h1356 h1363 h1371
3635    G       s1429   t1323
3636    B       b1430   s1429
3637    T       t1430   o1095 b1430 b1407
3638    B       b1431   t1430
3639    T       t1431   o2 b1427
3640    B       b1432   t1431
3641    T       t1432   o1094 b1431 b4 b1432
3642    B       b1433   t1432
3643    T       t1433   o b1433 b4
3644    B       b1434   t1433
3645    T       t1434   o1093 b1427 b1434
3646    B       b1435   t1434
3647    P       p1435   String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's2}; 's2} >> 6 ttca"
3648    O       o1435   ext_rule p1435
3649    S       s1435   t684 h h1394 h1395 h1356 h1363 h1371 h1377
3650    G       s1435   t1323
3651    B       b1436   s1435
3652    T       t1436   o1095 b1436 b1407
3653    B       b1437   t1436
3654    T       t1437   o2 b1433
3655    B       b1438   t1437
3656    T       t1438   o1094 b1437 b4 b1438
3657    B       b1439   t1438
3658    T       t1439   o b1439 b4
3659    B       b1440   t1439
3660    T       t1440   o1093 b1433 b1440
3661    B       b1441   t1440
3662    P       p1441   String "equivSubstT << equiv{car{'g}; 'R; op{'g; id{'g}; 's3}; 's3} >> 7 ttca"
3663    O       o1441   ext_rule p1441
3664    T       t1441   o1093 b1439 b4
3665    B       b1442   t1441
3666    T       t1442   o1441 b1092 b1442 b4 b4
3667    B       b1443   t1442
3668    T       t1443   o b1443 b4
3669    B       b1444   t1443
3670    T       t1444   o1435 b1092 b1441 b1444 b4
3671    B       b1445   t1444
3672    T       t1445   o b1445 b4
3673    B       b1446   t1445
3674    T       t1446   o1429 b1092 b1435 b1446 b4
3675    B       b1447   t1446
3676    T       t1447   o b1447 b4
3677    B       b1448   t1447
3678    T       t1448   o1423 b1092 b1429 b1448 b4
3679    B       b1449   t1448
3680    T       t1449   o b1449 b4
3681    B       b1450   t1449
3682    T       t1450   o1394 b1092 b1423 b1450 b4
3683    B       b1451   t1450
3684    T       t1451   o b1451 b4
3685    B       b1452   t1451
3686    T       t1452   o1335 b1092 b1355 b1394 b1452
3687    B       b1453   t1452
3688    T       t1453   o1090 b1453
3689    B       b1454   t1453
3690    T       t1454   o1299 b1302 b1335 b1454 b4
3691    B       b1455   t1454
3692    T       t1455   o1298 b1455
3693    B       b1456   t1455
3694    P       p1456   Number 12867
3695    P       p1457   Number 14174
3696    O       o1457   location p1456 p1457
3697    P       p1458   String cancel2
3698    O       o1458   rule p1458
3699    H       h1458   x t793
3700    S       s1458   t679 h h1458 h1304
3701    G       s1458   t715
3702    B       b1458   s1458
3703    T       t1458   o677 b1458
3704    B       b1459   t1458
3705    S       s1459   t679 h h1458 h1304
3706    G       s1459   t718
3707    B       b1460   s1459
3708    T       t1460   o677 b1460
3709    B       b1461   t1460
3710    S       s1461   t679 h h1458 h1304
3711    G       s1461   t757
3712    B       b1462   s1461
3713    T       t1462   o677 b1462
3714  B       b1463   t1462  B       b1463   t1462
3715  T       t1463   o1000 b1462 b4 b1463  S       s1463   t679 h h1458 h1304
3716  B       b1464   t1463  G       s1463   t760
3717  T       t1464   o2 b1464  B       b1464   s1463
3718    T       t1464   o677 b1464
3719  B       b1465   t1464  B       b1465   t1464
3720  T       t1465   o1452 b1457 b1460 b1465  S       s1465   t679 h h1458 h1304
3721  B       b1466   t1465  G       s1465   t681
3722  T       t1466   o2 b1466  B       b1466   s1465
3723    T       t1466   o677 b1466
3724  B       b1467   t1466  B       b1467   t1466
3725  T       t1467   o1452 b1455 b4 b1467  S       s1467   t684 h h1458 h1304
3726  B       b1468   t1467  G       s1467   t586
3727  T       t1468   o811 b1432 b1453  B       b1468   s1467
3728  H       h1468   v_1 t1468  T       t1468   o677 b1468
3729  S       s1468   t673 h h1452 h1468  B       b1469   t1468
3730  G       s1468   t1435  S       s1469   t684 h h1458 h1304
3731  B       b1469   s1468  G       s1469   t762
3732  T       t1469   o1001 b1469 b1450  B       b1470   s1469
3733  B       b1470   t1469  T       t1470   o677 b1470
 T       t1470   o1000 b1470 b4 b1465  
3734  B       b1471   t1470  B       b1471   t1470
3735  T       t1471   o b1471 b4  S       s1471   t684 h h1458 h1304
3736  B       b1472   t1471  G       s1471   t736
3737  T       t1472   o b1468 b1472  B       b1472   s1471
3738    T       t1472   o677 b1472
3739  B       b1473   t1472  B       b1473   t1472
3740  T       t1473   o999 b1452 b1473  S       s1473   t684 h h1458 h1304
3741  B       b1474   t1473  G       s1473   t738
3742  P       p1474   String "assertT << equal{op{'g; inv{'g; 's}; 's}; id{'g}}>> thenT autoT"  B       b1474   s1473
3743  O       o1474   ext_rule p1474  T       t1474   o677 b1474
3744  T       t1474   o811 b1453 b583  B       b1475   t1474
3745  H       h1474   v_1 t1474  S       s1475   t684 h h1458 h1304
3746  S       s1474   t673 h h1452 h1474  G       s1475   t764
3747  G       s1474   t1454  B       b1476   s1475
3748  B       b1475   s1474  T       t1476   o677 b1476
 T       t1475   o1001 b1475 b1450  
 B       b1476   t1475  
 T       t1476   o2 b1468  
3749  B       b1477   t1476  B       b1477   t1476
3750  T       t1477   o1000 b1476 b4 b1477  S       s1477   t684 h h1458 h1304
3751  B       b1478   t1477  G       s1477   t766
3752  T       t1478   o b1478 b4  B       b1478   s1477
3753    T       t1478   o677 b1478
3754  B       b1479   t1478  B       b1479   t1478
3755  T       t1479   o999 b1468 b1479  T       t1479   o676 b1477 b1479
3756  B       b1480   t1479  B       b1480   t1479
3757  P       p1480   String "rwh unfold_equal 3 thenT eqSetSymT thenT autoT"  T       t1480   o676 b1475 b1480
 O       o1480   ext_rule p1480  
 T       t1480   o999 b1478 b4  
3758  B       b1481   t1480  B       b1481   t1480
3759  T       t1481   o1480 b998 b1481 b4 b4  T       t1481   o676 b1473 b1481
3760  B       b1482   t1481  B       b1482   t1481
3761  T       t1482   o b1482 b4  T       t1482   o676 b1471 b1482
3762  B       b1483   t1482  B       b1483   t1482
3763  T       t1483   o1474 b998 b1480 b1483 b4  T       t1483   o676 b1469 b1483
3764  B       b1484   t1483  B       b1484   t1483
3765  P       p1484   String "groupCancelRightT << 'g >> << 's >> thenT autoT"  T       t1484   o676 b1467 b1484
 O       o1484   ext_rule p1484  
 T       t1484   o999 b1471 b4  
3766  B       b1485   t1484  B       b1485   t1484
3767  T       t1485   o1484 b998 b1485 b4 b4  T       t1485   o676 b1465 b1485
3768  B       b1486   t1485  B       b1486   t1485
3769  T       t1486   o b1486 b4  T       t1486   o676 b1463 b1486
3770  B       b1487   t1486  B       b1487   t1486
3771  T       t1487   o b1484 b1487  T       t1487   o676 b1461 b1487
3772  B       b1488   t1487  B       b1488   t1487
3773  T       t1488   o1443 b998 b1474 b1488 b4  T       t1488   o676 b1459 b1488
3774  B       b1489   t1488  B       b1489   t1488
3775  T       t1489   o996 b1489  P       p1489   String "assertT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}} >> thenAT autoT"
3776    O       o1489   ext_rule p1489
3777    T       t1489   o b1476 b4
3778  B       b1490   t1489  B       b1490   t1489
3779  P       p1492   Number 9099  T       t1490   o b1474 b1490
3780  P       p1499   String unique_inv2  B       b1491   t1490
3781  O       o1499   rule p1499  T       t1491   o b1472 b1491
3782  T       t1499   o575 b564 b589 b577  B       b1492   t1491
3783  B       b1499   t1499  T       t1492   o b1470 b1492
3784  T       t1500   o811 b1499 b583  B       b1493   t1492
3785  S       s1500   t673 h  T       t1493   o b1468 b1493
3786  G       s1500   t1500  B       b1494   t1493
3787  B       b1500   s1500  T       t1494   o b1466 b1494
3788  P       p1508   String "assumT 7 thenT setSubstT << equal{id{'g}; op{'g; 's; inv{'g; 's}}}>> 2 thenAT autoT"  B       b1495   t1494
3789  O       o1508   ext_rule p1508  T       t1495   o b1464 b1495
3790  T       t1509   o b1500 b4  B       b1496   t1495
3791  B       b1509   t1509  T       t1496   o b1462 b1496
3792  T       t1510   o b723 b1509  B       b1497   t1496
3793  B       b1510   t1510  T       t1497   o b1460 b1497
3794  T       t1511   o b874 b1510  B       b1498   t1497
3795  B       b1511   t1511  T       t1498   o b1458 b1498
3796  T       t1512   o b688 b1511  B       b1499   t1498
3797  B       b1512   t1512  T       t1499   o1095 b1478 b1499
3798  T       t1513   o b670 b1512  B       b1500   t1499
3799  B       b1513   t1513  T       t1500   o1094 b1500 b4 b1104
3800  T       t1514   o b704 b1513  B       b1501   t1500
3801  B       b1514   t1514  T       t1501   o609 b585 b756
3802  T       t1515   o b783 b1514  B       b1502   t1501
3803  B       b1515   t1515  T       t1502   o596 b585 b791 b1502
3804  T       t1516   o1001 b1435 b1515  B       b1503   t1502
3805  B       b1516   t1516  T       t1503   o596 b585 b792 b1502
3806  T       t1517   o1000 b1516 b4 b1011  B       b1504   t1503
3807  B       b1517   t1517  T       t1504   o761 b591 b759 b1503 b1504
3808  H       h1517   v t1500  H       h1504   v t1504
3809  T       t1518   o575 b564 b589 b590  S       s1504   t684 h h1458 h1304 h1504
3810  B       b1518   t1518  G       s1504   t766
3811  T       t1519   o744 b583 b1518  B       b1505   s1504
3812  S       s1519   t673 h h1517  T       t1505   o1095 b1505 b1499
3813  G       s1519   t1519  B       b1506   t1505
3814  B       b1519   s1519  T       t1506   o2 b1501
3815  T       t1520   o1001 b1519 b1515  B       b1507   t1506
3816  B       b1520   t1520  T       t1507   o1094 b1506 b4 b1507
3817  T       t1521   o811 b583 b1518  B       b1508   t1507
3818  S       s1521   t673 h h1517  T       t1508   o b1508 b4
3819  G       s1521   t1521  B       b1509   t1508
3820  B       b1521   s1521  T       t1509   o1093 b1501 b1509
3821  T       t1522   o1001 b1521 b1515  B       b1510   t1509
3822  B       b1522   t1522  P       p1510   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 4 ttca"
3823  S       s1522   t673 h h1517  O       o1510   ext_rule p1510
3824  G       s1522   t1435  T       t1510   o596 b585 b756 b1502
3825  B       b1523   s1522  B       b1511   t1510
3826  T       t1523   o1001 b1523 b1515  T       t1511   o596 b585 b714 b1511
3827    B       b1512   t1511
3828    T       t1512   o761 b591 b759 b1512 b1504
3829    H       h1512   z t1512
3830    S       s1512   t684 h h1458 h1304 h1504 h1512
3831    G       s1512   t766
3832    B       b1513   s1512
3833    T       t1513   o1095 b1513 b1499
3834    B       b1514   t1513
3835    T       t1514   o2 b1508
3836    B       b1515   t1514
3837    T       t1515   o1094 b1514 b4 b1515
3838    B       b1516   t1515
3839    T       t1516   o b1516 b4
3840    B       b1517   t1516
3841    T       t1517   o1093 b1508 b1517
3842    B       b1518   t1517
3843    P       p1518   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 5 ttca"
3844    O       o1518   ext_rule p1518
3845    T       t1518   o596 b585 b717 b1511
3846    B       b1519   t1518
3847    T       t1519   o761 b591 b759 b1512 b1519
3848    H       h1519   z_1 t1519
3849    S       s1519   t684 h h1458 h1304 h1504 h1512 h1519
3850    G       s1519   t766
3851    B       b1520   s1519
3852    T       t1520   o1095 b1520 b1499
3853    B       b1521   t1520
3854    T       t1521   o2 b1516
3855    B       b1522   t1521
3856    T       t1522   o1094 b1521 b4 b1522
3857    B       b1523   t1522
3858    T       t1523   o b1523 b4
3859  B       b1524   t1523  B       b1524   t1523
3860  T       t1524   o2 b1517  T       t1524   o1093 b1516 b1524
3861  B       b1525   t1524  B       b1525   t1524
3862  T       t1525   o1000 b1524 b4 b1525  P       p1525   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 6 ttca"
3863    O       o1525   ext_rule p1525
3864    T       t1525   o596 b585 b714 b604
3865  B       b1526   t1525  B       b1526   t1525
3866  T       t1526   o2 b1526  T       t1526   o596 b585 b717 b604
3867  B       b1527   t1526  B       b1527   t1526
3868  T       t1527   o1452 b1522 b1460 b1527  T       t1527   o761 b591 b759 b1526 b1527
3869  B       b1528   t1527  H       h1527   z_2 t1527
3870  T       t1528   o2 b1528  S       s1527   t684 h h1458 h1304 h1504 h1512 h1519 h1527
3871    G       s1527   t766
3872    B       b1528   s1527
3873    T       t1528   o1095 b1528 b1499
3874  B       b1529   t1528  B       b1529   t1528
3875  T       t1529   o1452 b1520 b4 b1529  T       t1529   o2 b1523
3876  B       b1530   t1529  B       b1530   t1529
3877  T       t1530   o811 b1499 b1518  T       t1530   o1094 b1529 b4 b1530
3878  H       h1530   v_1 t1530  B       b1531   t1530
3879  S       s1530   t673 h h1517 h1530  T       t1531   o b1531 b4
 G       s1530   t1435  
 B       b1531   s1530  
 T       t1531   o1001 b1531 b1515  
3880  B       b1532   t1531  B       b1532   t1531
3881  T       t1532   o1000 b1532 b4 b1527  T       t1532   o1093 b1523 b1532
3882  B       b1533   t1532  B       b1533   t1532
3883  T       t1533   o b1533 b4  P       p1533   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's1; id{'g}}; 's1} >> 7 ttca"
3884  B       b1534   t1533  O       o1533   ext_rule p1533
3885  T       t1534   o b1530 b1534  T       t1533   o761 b591 b759 b714 b1527
3886    H       h1533   z_3 t1533
3887    S       s1533   t684 h h1458 h1304 h1504 h1512 h1519 h1527 h1533
3888    G       s1533   t766
3889    B       b1534   s1533
3890    T       t1534   o1095 b1534 b1499
3891  B       b1535   t1534  B       b1535   t1534
3892  T       t1535   o999 b1517 b1535  T       t1535   o2 b1531
3893  B       b1536   t1535  B       b1536   t1535
3894  P       p1536   String "assertT << equal{op{'g; 's; inv{'g; 's}}; id{'g}}>> thenT autoT"  T       t1536   o1094 b1535 b4 b1536
3895  O       o1536   ext_rule p1536  B       b1537   t1536
3896  T       t1536   o811 b1518 b583  T       t1537   o b1537 b4
 H       h1536   v_1 t1536  
 S       s1536   t673 h h1517 h1536  
 G       s1536   t1519  
 B       b1537   s1536  
 T       t1537   o1001 b1537 b1515  
3897  B       b1538   t1537  B       b1538   t1537
3898  T       t1538   o2 b1530  T       t1538   o1093 b1531 b1538
3899  B       b1539   t1538  B       b1539   t1538
3900  T       t1539   o1000 b1538 b4 b1539  P       p1539   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's2; id{'g}}; 's2} >> 8 ttca"
3901    O       o1539   ext_rule p1539
3902    T       t1539   o1093 b1537 b4
3903  B       b1540   t1539  B       b1540   t1539
3904  T       t1540   o b1540 b4  T       t1540   o1539 b1092 b1540 b4 b4
3905  B       b1541   t1540  B       b1541   t1540
3906  T       t1541   o999 b1530 b1541  T       t1541   o b1541 b4
3907  B       b1542   t1541  B       b1542   t1541
3908  T       t1542   o999 b1540 b4  T       t1542   o1533 b1092 b1539 b1542 b4
3909  B       b1543   t1542  B       b1543   t1542
3910  T       t1543   o1480 b998 b1543 b4 b4  T       t1543   o b1543 b4
3911  B       b1544   t1543  B       b1544   t1543
3912  T       t1544   o b1544 b4  T       t1544   o1525 b1092 b1533 b1544 b4
3913  B       b1545   t1544  B       b1545   t1544
3914  P       p1545   String "rwh unfold_equal 3 thenT eqSetSymT"  T       t1545   o b1545 b4
3915  O       o1545   ext_rule p1545  B       b1546   t1545
3916  S       s1545   t673 h h1517 h1474  T       t1546   o1518 b1092 b1525 b1546 b4
 G       s1545   t1519  
 B       b1546   s1545  
 T       t1546   o1001 b1546 b1515  
3917  B       b1547   t1546  B       b1547   t1546
3918  T       t1547   o1000 b1547 b4 b1539  T       t1547   o b1547 b4
3919  B       b1548   t1547  B       b1548   t1547
3920  P       p1548   String wf  T       t1548   o1510 b1092 b1518 b1548 b4
 O       o1548   tactic_arg p1548  
 T       t1548   o689 b1453  
3921  B       b1549   t1548  B       b1549   t1548
3922  B       b1550   t850  T       t1549   o b1549 b4
3923  T       t1550   o1289 b1549 b1550  B       b1550   t1549
3924  B       b1551   t1550  P       p1550   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's1; 's3}; inv{'g; 's3}}; op{'g; 's1; op{'g; 's3; inv{'g; 's3}}}} >> 3 ttca"
3925  T       t1551   o744 b1453 b583  O       o1550   ext_rule p1550
3926    H       h1550   v t793
3927    H       h1551   v_1 t1504
3928    S       s1551   t684 h h1550 h1551
3929    G       s1551   t766
3930    B       b1551   s1551
3931    T       t1551   o b793 b4
3932  B       b1552   t1551  B       b1552   t1551
3933  T       t1552   o1289 b1551 b1552  T       t1552   o b764 b1552
3934  H       h1552   v_1 t1552  B       b1553   t1552
3935  S       s1552   t668 h h1517 h1552  T       t1553   o b738 b1553
 G       s1552   t850  
 B       b1553   s1552  
 T       t1553   o1001 b1553 b1515  
3936  B       b1554   t1553  B       b1554   t1553
3937  S       s1554   t673 h h1517 h1552  T       t1554   o b736 b1554
3938  G       s1554   t1519  B       b1555   t1554
3939  B       b1555   s1554  T       t1555   o b762 b1555
 T       t1555   o1001 b1555 b1515  
3940  B       b1556   t1555  B       b1556   t1555
3941  T       t1556   o2 b1548  T       t1556   o b699 b1556
3942  B       b1557   t1556  B       b1557   t1556
3943  T       t1557   o1000 b1556 b4 b1557  T       t1557   o b681 b1557
3944  B       b1558   t1557  B       b1558   t1557
3945  T       t1558   o2 b1558  T       t1558   o b760 b1558
3946  B       b1559   t1558  B       b1559   t1558
3947  T       t1559   o1548 b1554 b4 b1559  T       t1559   o b757 b1559
3948  B       b1560   t1559  B       b1560   t1559
3949  T       t1560   o689 b1518  T       t1560   o b718 b1560
3950  S       s1560   t668 h h1517 h1552  B       b1561   t1560
3951  G       s1560   t1560  T       t1561   o b715 b1561
 B       b1561   s1560  
 T       t1561   o1001 b1561 b1515  
3952  B       b1562   t1561  B       b1562   t1561
3953  T       t1562   o1548 b1562 b4 b1559  T       t1562   o1095 b1551 b1562
3954  B       b1563   t1562  B       b1563   t1562
3955  T       t1563   o744 b1518 b583  S       s1563   t684 h h1550
3956  S       s1563   t673 h h1517 h1552  G       s1563   t766
 G       s1563   t1563  
3957  B       b1564   s1563  B       b1564   s1563
3958  T       t1564   o1001 b1564 b1515  T       t1564   o1095 b1564 b1562
3959  B       b1565   t1564  B       b1565   t1564
3960  T       t1565   o1000 b1565 b4 b1559  T       t1565   o1095 b766 b1562
3961  B       b1566   t1565  B       b1566   t1565
3962  T       t1566   o b1566 b4  T       t1566   o1094 b1566 b4 b1104
3963  B       b1567   t1566  B       b1567   t1566
3964  T       t1567   o b1563 b1567  T       t1567   o2 b1567
3965  B       b1568   t1567  B       b1568   t1567
3966  T       t1568   o b1560 b1568  T       t1568   o1094 b1565 b4 b1568
3967  B       b1569   t1568  B       b1569   t1568
3968  T       t1569   o999 b1548 b1569  T       t1569   o2 b1569
3969  B       b1570   t1569  B       b1570   t1569
3970  NSummary!ext_goal       ext_goal        ext_goal Summary  T       t1570   o1094 b1563 b4 b1570
 O       o1570   ext_goal  
 T       t1570   o1570 b1560  
3971  B       b1571   t1570  B       b1571   t1570
3972  T       t1571   o1570 b1563  S       s1571   t684 h h1550 h1551 h1512
3973  B       b1572   t1571  G       s1571   t766
3974  T       t1572   o1570 b1566  B       b1572   s1571
3975    T       t1572   o1095 b1572 b1562
3976  B       b1573   t1572  B       b1573   t1572
3977  T       t1573   o b1573 b4  T       t1573   o2 b1571
3978  B       b1574   t1573  B       b1574   t1573
3979  T       t1574   o b1572 b1574  T       t1574   o1094 b1573 b4 b1574
3980  B       b1575   t1574  B       b1575   t1574
3981  T       t1575   o b1571 b1575  T       t1575   o b1575 b4
3982  B       b1576   t1575  B       b1576   t1575
3983  T       t1576   o1545 b998 b1570 b1576 b4  T       t1576   o1093 b1571 b1576
3984  B       b1577   t1576  B       b1577   t1576
3985  T       t1577   o b1577 b4  P       p1577   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 's2; 's3}; inv{'g; 's3}}; op{'g; 's2; op{'g; 's3; inv{'g; 's3}}}} >> 4 ttca"
3986  B       b1578   t1577  O       o1577   ext_rule p1577
3987  T       t1578   o1536 b998 b1542 b1545 b1578  S       s1577   t684 h h1550 h1551 h1512 h1519
3988    G       s1577   t766
3989    B       b1578   s1577
3990    T       t1578   o1095 b1578 b1562
3991  B       b1579   t1578  B       b1579   t1578
3992  P       p1579   String "groupCancelLeftT << 'g >> << 's >> thenT autoT"  T       t1579   o2 b1575
 O       o1579   ext_rule p1579  
 T       t1579   o999 b1533 b4  
3993  B       b1580   t1579  B       b1580   t1579
3994  T       t1580   o1579 b998 b1580 b4 b4  T       t1580   o1094 b1579 b4 b1580
3995  B       b1581   t1580  B       b1581   t1580
3996  T       t1581   o b1581 b4  T       t1581   o b1581 b4
3997  B       b1582   t1581  B       b1582   t1581
3998  T       t1582   o b1579 b1582  T       t1582   o1093 b1575 b1582
3999  B       b1583   t1582  B       b1583   t1582
4000  T       t1583   o1508 b998 b1536 b1583 b4  P       p1583   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 's3; inv{'g; 's3}}; id{'g}} >> 5 ttca"
4001  B       b1584   t1583  O       o1583   ext_rule p1583
4002  T       t1584   o996 b1584  S       s1583   t684 h h1550 h1551 h1512 h1519 h1527
4003    G       s1583   t766
4004    B       b1584   s1583
4005    T       t1584   o1095 b1584 b1562
4006  B       b1585   t1584  B       b1585   t1584
4007  P       p1594   String unique_sol1  T       t1585   o2 b1581
4008  O       o1594   rule p1594  B       b1586   t1585