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

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

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

revision 3569 by xiny, Wed Apr 3 05:27:01 2002 UTC revision 3570 by xiny, Tue Apr 9 05:59:41 2002 UTC
# Line 1128  Line 1128 
1128  B       b418    t418  B       b418    t418
1129  T       t419    o414 b418  T       t419    o414 b418
1130  B       b419    t419  B       b419    t419
1131  P       p419    Number 109  P       p419    Number 108
1132  P       p420    Number 120  P       p420    Number 133
1133  O       o420    location p419 p420  O       o420    location p419 p420
1134  NSummary!summary_item   summary_item    summary_item Summary  P       p421    String Czf_itt_group_bvd
1135  O       o421    summary_item  O       o421    parent p421
1136  NOcaml!str_open str_open        str_open Ocaml  T       t421    o421
1137  O       o422    str_open p419 p420  B       b421    t421
1138  NOcaml!string   string  string Ocaml  T       t422    o b421 b4
1139  P       p422    String Printf  B       b422    t422
1140  O       o423    string p422  T       t423    o b422 b4
 T       t423    o423  
1141  B       b423    t423  B       b423    t423
1142  T       t424    o b423 b4  T       t424    o2 b422 b423 b392
1143  B       b424    t424  B       b424    t424
1144  T       t425    o422 b424  T       t425    o420 b424
1145  B       b425    t425  B       b425    t425
1146  T       t426    o421 b425  P       p425    Number 135
1147  B       b426    t426  P       p426    Number 146
1148  T       t427    o420 b426  O       o426    location p425 p426
1149  B       b427    t427  NSummary!summary_item   summary_item    summary_item Summary
1150  P       p427    Number 121  O       o427    summary_item
1151  P       p428    Number 134  NOcaml!str_open str_open        str_open Ocaml
1152  O       o428    location p427 p428  O       o428    str_open p425 p426
1153  O       o429    str_open p427 p428  NOcaml!string   string  string Ocaml
1154  P       p429    String Mp_debug  P       p428    String Printf
1155  O       o430    string p429  O       o429    string p428
1156  T       t430    o430  T       t429    o429
1157    B       b429    t429
1158    T       t430    o b429 b4
1159  B       b430    t430  B       b430    t430
1160  T       t431    o b430 b4  T       t431    o428 b430
1161  B       b431    t431  B       b431    t431
1162  T       t432    o429 b431  T       t432    o427 b431
1163  B       b432    t432  B       b432    t432
1164  T       t433    o421 b432  T       t433    o426 b432
1165  B       b433    t433  B       b433    t433
1166  T       t434    o428 b433  P       p433    Number 147
1167  B       b434    t434  P       p434    Number 160
1168  P       p434    Number 135  O       o434    location p433 p434
1169  P       p435    Number 155  O       o435    str_open p433 p434
1170  O       o435    location p434 p435  P       p435    String Mp_debug
1171  O       o436    str_open p434 p435  O       o436    string p435
1172  P       p436    String Refiner  T       t436    o436
1173  O       o437    string p436  B       b436    t436
1174  T       t437    o437  T       t437    o b436 b4
1175  B       b437    t437  B       b437    t437
1176  T       t438    o b437 b4  T       t438    o435 b437
1177  B       b438    t438  B       b438    t438
1178  T       t439    o b437 b438  T       t439    o427 b438
1179  B       b439    t439  B       b439    t439
1180  T       t440    o436 b439  T       t440    o434 b439
1181  B       b440    t440  B       b440    t440
1182  T       t441    o421 b440  P       p440    Number 161
1183  B       b441    t441  P       p441    Number 181
1184  T       t442    o435 b441  O       o441    location p440 p441
1185  B       b442    t442  O       o442    str_open p440 p441
1186  P       p442    Number 156  P       p442    String Refiner
1187  P       p443    Number 181  O       o443    string p442
1188  O       o443    location p442 p443  T       t443    o443
1189  O       o444    str_open p442 p443  B       b443    t443
1190  P       p444    String Term  T       t444    o b443 b4
1191  O       o445    string p444  B       b444    t444
1192  T       t445    o445  T       t445    o b443 b444
1193  B       b445    t445  B       b445    t445
1194  T       t446    o b445 b4  T       t446    o442 b445
1195  B       b446    t446  B       b446    t446
1196  T       t447    o b437 b446  T       t447    o427 b446
1197  B       b447    t447  B       b447    t447
1198  T       t448    o b437 b447  T       t448    o441 b447
1199  B       b448    t448  B       b448    t448
1200  T       t449    o444 b448  P       p448    Number 182
1201  B       b449    t449  P       p449    Number 207
1202  T       t450    o421 b449  O       o449    location p448 p449
1203  B       b450    t450  O       o450    str_open p448 p449
1204  T       t451    o443 b450  P       p450    String Term
1205    O       o451    string p450
1206    T       t451    o451
1207  B       b451    t451  B       b451    t451
1208  P       p451    Number 182  T       t452    o b451 b4
1209  P       p452    Number 209  B       b452    t452
1210  O       o452    location p451 p452  T       t453    o b443 b452
1211  O       o453    str_open p451 p452  B       b453    t453
1212  P       p453    String TermOp  T       t454    o b443 b453
 O       o454    string p453  
 T       t454    o454  
1213  B       b454    t454  B       b454    t454
1214  T       t455    o b454 b4  T       t455    o450 b454
1215  B       b455    t455  B       b455    t455
1216  T       t456    o b437 b455  T       t456    o427 b455
1217  B       b456    t456  B       b456    t456
1218  T       t457    o b437 b456  T       t457    o449 b456
1219  B       b457    t457  B       b457    t457
1220  T       t458    o453 b457  P       p457    Number 208
1221  B       b458    t458  P       p458    Number 235
1222  T       t459    o421 b458  O       o458    location p457 p458
1223  B       b459    t459  O       o459    str_open p457 p458
1224  T       t460    o452 b459  P       p459    String TermOp
1225    O       o460    string p459
1226    T       t460    o460
1227  B       b460    t460  B       b460    t460
1228  P       p460    Number 210  T       t461    o b460 b4
1229  P       p461    Number 238  B       b461    t461
1230  O       o461    location p460 p461  T       t462    o b443 b461
1231  O       o462    str_open p460 p461  B       b462    t462
1232  P       p462    String TermMan  T       t463    o b443 b462
 O       o463    string p462  
 T       t463    o463  
1233  B       b463    t463  B       b463    t463
1234  T       t464    o b463 b4  T       t464    o459 b463
1235  B       b464    t464  B       b464    t464
1236  T       t465    o b437 b464  T       t465    o427 b464
1237  B       b465    t465  B       b465    t465
1238  T       t466    o b437 b465  T       t466    o458 b465
1239  B       b466    t466  B       b466    t466
1240  T       t467    o462 b466  P       p466    Number 236
1241  B       b467    t467  P       p467    Number 264
1242  T       t468    o421 b467  O       o467    location p466 p467
1243  B       b468    t468  O       o468    str_open p466 p467
1244  T       t469    o461 b468  P       p468    String TermMan
1245    O       o469    string p468
1246    T       t469    o469
1247  B       b469    t469  B       b469    t469
1248  P       p469    Number 239  T       t470    o b469 b4
1249  P       p470    Number 269  B       b470    t470
1250  O       o470    location p469 p470  T       t471    o b443 b470
1251  O       o471    str_open p469 p470  B       b471    t471
1252  P       p471    String TermSubst  T       t472    o b443 b471
 O       o472    string p471  
 T       t472    o472  
1253  B       b472    t472  B       b472    t472
1254  T       t473    o b472 b4  T       t473    o468 b472
1255  B       b473    t473  B       b473    t473
1256  T       t474    o b437 b473  T       t474    o427 b473
1257  B       b474    t474  B       b474    t474
1258  T       t475    o b437 b474  T       t475    o467 b474
1259  B       b475    t475  B       b475    t475
1260  T       t476    o471 b475  P       p475    Number 265
1261  B       b476    t476  P       p476    Number 295
1262  T       t477    o421 b476  O       o476    location p475 p476
1263  B       b477    t477  O       o477    str_open p475 p476
1264  T       t478    o470 b477  P       p477    String TermSubst
1265    O       o478    string p477
1266    T       t478    o478
1267  B       b478    t478  B       b478    t478
1268  P       p478    Number 270  T       t479    o b478 b4
1269  P       p479    Number 302  B       b479    t479
1270  O       o479    location p478 p479  T       t480    o b443 b479
1271  O       o480    str_open p478 p479  B       b480    t480
1272  P       p480    String RefineError  T       t481    o b443 b480
 O       o481    string p480  
 T       t481    o481  
1273  B       b481    t481  B       b481    t481
1274  T       t482    o b481 b4  T       t482    o477 b481
1275  B       b482    t482  B       b482    t482
1276  T       t483    o b437 b482  T       t483    o427 b482
1277  B       b483    t483  B       b483    t483
1278  T       t484    o b437 b483  T       t484    o476 b483
1279  B       b484    t484  B       b484    t484
1280  T       t485    o480 b484  P       p484    Number 296
1281  B       b485    t485  P       p485    Number 328
1282  T       t486    o421 b485  O       o485    location p484 p485
1283  B       b486    t486  O       o486    str_open p484 p485
1284  T       t487    o479 b486  P       p486    String RefineError
1285    O       o487    string p486
1286    T       t487    o487
1287  B       b487    t487  B       b487    t487
1288  P       p487    Number 303  T       t488    o b487 b4
1289  P       p488    Number 319  B       b488    t488
1290  O       o488    location p487 p488  T       t489    o b443 b488
1291  O       o489    str_open p487 p488  B       b489    t489
1292  P       p489    String Mp_resource  T       t490    o b443 b489
 O       o490    string p489  
 T       t490    o490  
1293  B       b490    t490  B       b490    t490
1294  T       t491    o b490 b4  T       t491    o486 b490
1295  B       b491    t491  B       b491    t491
1296  T       t492    o489 b491  T       t492    o427 b491
1297  B       b492    t492  B       b492    t492
1298  T       t493    o421 b492  T       t493    o485 b492
1299  B       b493    t493  B       b493    t493
1300  T       t494    o488 b493  P       p493    Number 329
1301  B       b494    t494  P       p494    Number 345
1302  P       p494    Number 321  O       o494    location p493 p494
1303  P       p495    Number 337  O       o495    str_open p493 p494
1304  O       o495    location p494 p495  P       p495    String Mp_resource
1305  O       o496    str_open p494 p495  O       o496    string p495
1306  P       p496    String Tactic_type  T       t496    o496
1307  O       o497    string p496  B       b496    t496
1308  T       t497    o497  T       t497    o b496 b4
1309  B       b497    t497  B       b497    t497
1310  T       t498    o b497 b4  T       t498    o495 b497
1311  B       b498    t498  B       b498    t498
1312  T       t499    o496 b498  T       t499    o427 b498
1313  B       b499    t499  B       b499    t499
1314  T       t500    o421 b499  T       t500    o494 b499
1315  B       b500    t500  B       b500    t500
1316  T       t501    o495 b500  P       p500    Number 347
1317  B       b501    t501  P       p501    Number 363
1318  P       p501    Number 338  O       o501    location p500 p501
1319  P       p502    Number 362  O       o502    str_open p500 p501
1320  O       o502    location p501 p502  P       p502    String Tactic_type
1321  O       o503    str_open p501 p502  O       o503    string p502
1322  P       p503    String Sequent  T       t503    o503
1323  O       o504    string p503  B       b503    t503
1324  T       t504    o504  T       t504    o b503 b4
1325  B       b504    t504  B       b504    t504
1326  T       t505    o b504 b4  T       t505    o502 b504
1327  B       b505    t505  B       b505    t505
1328  T       t506    o b497 b505  T       t506    o427 b505
1329  B       b506    t506  B       b506    t506
1330  T       t507    o503 b506  T       t507    o501 b506
1331  B       b507    t507  B       b507    t507
1332  T       t508    o421 b507  P       p507    Number 364
1333  B       b508    t508  P       p508    Number 388
1334  T       t509    o502 b508  O       o508    location p507 p508
1335  B       b509    t509  O       o509    str_open p507 p508
1336  P       p509    Number 363  P       p509    String Sequent
1337  P       p510    Number 389  O       o510    string p509
1338  O       o510    location p509 p510  T       t510    o510
1339  O       o511    str_open p509 p510  B       b510    t510
1340  P       p511    String Tacticals  T       t511    o b510 b4
1341  O       o512    string p511  B       b511    t511
1342  T       t512    o512  T       t512    o b503 b511
1343  B       b512    t512  B       b512    t512
1344  T       t513    o b512 b4  T       t513    o509 b512
1345  B       b513    t513  B       b513    t513
1346  T       t514    o b497 b513  T       t514    o427 b513
1347  B       b514    t514  B       b514    t514
1348  T       t515    o511 b514  T       t515    o508 b514
1349  B       b515    t515  B       b515    t515
1350  T       t516    o421 b515  P       p515    Number 389
1351  B       b516    t516  P       p516    Number 415
1352  T       t517    o510 b516  O       o516    location p515 p516
1353  B       b517    t517  O       o517    str_open p515 p516
1354  P       p517    Number 390  P       p517    String Tacticals
1355  P       p518    Number 398  O       o518    string p517
1356  O       o518    location p517 p518  T       t518    o518
1357  O       o519    str_open p517 p518  B       b518    t518
1358  O       o520    string p153  T       t519    o b518 b4
1359  T       t520    o520  B       b519    t519
1360    T       t520    o b503 b519
1361  B       b520    t520  B       b520    t520
1362  T       t521    o b520 b4  T       t521    o517 b520
1363  B       b521    t521  B       b521    t521
1364  T       t522    o519 b521  T       t522    o427 b521
1365  B       b522    t522  B       b522    t522
1366  T       t523    o421 b522  T       t523    o516 b522
1367  B       b523    t523  B       b523    t523
1368  T       t524    o518 b523  P       p523    Number 416
1369  B       b524    t524  P       p524    Number 424
1370  P       p524    Number 399  O       o524    location p523 p524
1371  P       p525    Number 409  O       o525    str_open p523 p524
1372  O       o525    location p524 p525  O       o526    string p153
1373  O       o526    str_open p524 p525  T       t526    o526
1374  O       o527    string p155  B       b526    t526
1375  T       t527    o527  T       t527    o b526 b4
1376  B       b527    t527  B       b527    t527
1377  T       t528    o b527 b4  T       t528    o525 b527
1378  B       b528    t528  B       b528    t528
1379  T       t529    o526 b528  T       t529    o427 b528
1380  B       b529    t529  B       b529    t529
1381  T       t530    o421 b529  T       t530    o524 b529
1382  B       b530    t530  B       b530    t530
1383  T       t531    o525 b530  P       p530    Number 425
1384  B       b531    t531  P       p531    Number 435
1385  P       p531    Number 411  O       o531    location p530 p531
1386  P       p532    Number 428  O       o532    str_open p530 p531
1387  O       o532    location p531 p532  O       o533    string p155
1388  O       o533    str_open p531 p532  T       t533    o533
1389  O       o534    string p143  B       b533    t533
1390  T       t534    o534  T       t534    o b533 b4
1391  B       b534    t534  B       b534    t534
1392  T       t535    o b534 b4  T       t535    o532 b534
1393  B       b535    t535  B       b535    t535
1394  T       t536    o533 b535  T       t536    o427 b535
1395  B       b536    t536  B       b536    t536
1396  T       t537    o421 b536  T       t537    o531 b536
1397  B       b537    t537  B       b537    t537
1398  T       t538    o532 b537  P       p537    Number 437
1399  B       b538    t538  P       p538    Number 454
1400  P       p538    Number 429  O       o538    location p537 p538
1401  P       p539    Number 450  O       o539    str_open p537 p538
1402  O       o539    location p538 p539  O       o540    string p143
1403  O       o540    str_open p538 p539  T       t540    o540
1404  O       o541    string p145  B       b540    t540
1405  T       t541    o541  T       t541    o b540 b4
1406  B       b541    t541  B       b541    t541
1407  T       t542    o b541 b4  T       t542    o539 b541
1408  B       b542    t542  B       b542    t542
1409  T       t543    o540 b542  T       t543    o427 b542
1410  B       b543    t543  B       b543    t543
1411  T       t544    o421 b543  T       t544    o538 b543
1412  B       b544    t544  B       b544    t544
1413  T       t545    o539 b544  P       p544    Number 455
1414  B       b545    t545  P       p545    Number 476
1415  P       p545    Number 626  O       o545    location p544 p545
1416  P       p546    Number 650  O       o546    str_open p544 p545
1417  O       o546    location p545 p546  O       o547    string p145
1418    T       t547    o547
1419    B       b547    t547
1420    T       t548    o b547 b4
1421    B       b548    t548
1422    T       t549    o546 b548
1423    B       b549    t549
1424    T       t550    o427 b549
1425    B       b550    t550
1426    T       t551    o545 b550
1427    B       b551    t551
1428    P       p551    Number 652
1429    P       p552    Number 676
1430    O       o552    location p551 p552
1431  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1432  P       p547    String subgroup  P       p553    String subgroup
1433  O       o547    opname p547  O       o553    opname p553
1434  NCzf_itt_subgroup       Czf_itt_subgroup        Czf_itt_subgroup NIL  NCzf_itt_subgroup       Czf_itt_subgroup        Czf_itt_subgroup NIL
1435  NCzf_itt_subgroup!subgroup      subgroup        subgroup Czf_itt_subgroup  NCzf_itt_subgroup!subgroup      subgroup        subgroup Czf_itt_subgroup
1436  O       o548    subgroup  O       o554    subgroup
1437  Nvar    var     var NIL  Nvar    var     var NIL
1438  P       p548    Var s  P       p554    Var s
1439  O       o549    var p548  O       o555    var p554
1440  T       t549    o549  T       t555    o555
1441  B       b549    t549  B       b555    t555
1442  P       p549    Var g  P       p555    Var g
1443  O       o550    var p549  O       o556    var p555
1444  T       t550    o550  T       t556    o556
1445  B       b550    t550  B       b556    t556
1446  T       t551    o548 b549 b550  T       t557    o554 b555 b556
1447  B       b551    t551  B       b557    t557
1448  T       t552    o547 b551  T       t558    o553 b557
1449  B       b552    t552  B       b558    t558
1450  T       t553    o546 b552  T       t559    o552 b558
1451  B       b553    t553  B       b559    t559
1452  P       p553    Number 652  P       p559    Number 678
1453  P       p554    Number 1113  P       p560    Number 808
1454  O       o554    location p553 p554  O       o560    location p559 p560
1455  NSummary!rewrite        rewrite rewrite Summary  NSummary!rewrite        rewrite rewrite Summary
1456  P       p555    String unfold_subgroup  P       p561    String unfold_subgroup
1457  O       o555    rewrite p555  O       o561    rewrite p561
1458  NItt_logic      Itt_logic       Itt_logic NIL  NItt_logic      Itt_logic       Itt_logic NIL
1459  NItt_logic!and  and     and Itt_logic  NItt_logic!and  and     and Itt_logic
1460  O       o556    and  O       o562    and
1461  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1462  NCzf_itt_group!group    group   group Czf_itt_group  NCzf_itt_group!group    group   group Czf_itt_group
1463  O       o557    group  O       o563    group
1464  T       t557    o557 b549  T       t563    o563 b555
1465  B       b557    t557  B       b563    t563
1466  T       t558    o557 b550  T       t564    o563 b556
1467  B       b558    t558  B       b564    t564
1468  NCzf_itt_subset Czf_itt_subset  Czf_itt_subset NIL  NCzf_itt_subset Czf_itt_subset  Czf_itt_subset NIL
1469  NCzf_itt_subset!subset  subset  subset Czf_itt_subset  NCzf_itt_subset!subset  subset  subset Czf_itt_subset
1470  O       o558    subset  O       o564    subset
1471  NCzf_itt_group!car      car     car Czf_itt_group  NCzf_itt_group!car      car     car Czf_itt_group
1472  O       o559    car  O       o565    car
1473  T       t559    o559 b549  T       t565    o565 b555
 B       b559    t559  
 T       t560    o559 b550  
 B       b560    t560  
 T       t561    o558 b559 b560  
 B       b561    t561  
 NItt_logic!all  all     all Itt_logic  
 O       o561    all  
 NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL  
 NCzf_itt_set!set        set     set Czf_itt_set  
 O       o562    set  
 T       t562    o562  
 B       b562    t562  
 NItt_logic!implies      implies implies Itt_logic  
 O       o563    implies  
 NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  
 NCzf_itt_member!mem     mem     mem Czf_itt_member  
 O       o564    mem  
 P       p564    Var a  
 O       o565    var p564  
 T       t565    o565  
1474  B       b565    t565  B       b565    t565
1475  T       t566    o564 b565 b559  T       t566    o565 b556
1476  B       b566    t566  B       b566    t566
1477  P       p566    Var b  T       t567    o564 b565 b566
 O       o566    var p566  
 T       t567    o566  
1478  B       b567    t567  B       b567    t567
1479  T       t568    o564 b567 b559  NCzf_itt_group_bvd      Czf_itt_group_bvd       Czf_itt_group_bvd NIL
1480    NCzf_itt_group_bvd!group_bvd    group_bvd       group_bvd Czf_itt_group_bvd
1481    O       o567    group_bvd
1482    T       t568    o567 b555 b556 b565
1483  B       b568    t568  B       b568    t568
1484  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL  T       t569    o562 b567 b568
 NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv  
 O       o568    equiv  
 NCzf_itt_group!eqG      eqG     eqG Czf_itt_group  
 O       o569    eqG  
 T       t569    o569 b549  
1485  B       b569    t569  B       b569    t569
1486  NCzf_itt_group!op       op      op Czf_itt_group  T       t570    o562 b564 b569
 O       o570    op  
 T       t570    o570 b549 b565 b567  
1487  B       b570    t570  B       b570    t570
1488  T       t571    o570 b550 b565 b567  T       t571    o562 b563 b570
1489  B       b571    t571  B       b571    t571
1490  T       t572    o568 b559 b569 b570 b571  NSummary!prim   prim    prim Summary
1491    O       o571    prim
1492    T       t572    o571 b4
1493  B       b572    t572  B       b572    t572
1494  T       t573    o563 b568 b572  T       t573    o561 b557 b571 b572 b4
1495  B       b573    t573  B       b573    t573
1496  T       t574    o563 b566 b573  T       t574    o560 b573
1497  B       b574    t574 b  B       b574    t574
1498  T       t575    o561 b562 b574  P       p574    Number 810
1499  B       b575    t575 a  P       p575    Number 913
1500  T       t576    o561 b562 b575  O       o575    location p574 p575
1501  B       b576    t576  NSummary!dform  dform   dform Summary
1502  T       t577    o568 b559 b569 b565 b567  P       p576    String subgroup_df
1503    O       o576    dform p576
1504    NSummary!except_mode_df except_mode_df  except_mode_df Summary
1505    P       p577    String src
1506    O       o577    except_mode_df p577
1507    T       t577    o577
1508  B       b577    t577  B       b577    t577
1509  T       t578    o569 b550  T       t578    o b577 b4
1510  B       b578    t578  B       b578    t578
1511  T       t579    o568 b560 b578 b565 b567  NSummary!df_term        df_term df_term Summary
1512    O       o578    df_term
1513    NPerv!string    string578       string Perv
1514    P       p578    String subgroup(
1515    O       o579    string578 p578
1516    T       t579    o579
1517  B       b579    t579  B       b579    t579
1518  T       t580    o563 b577 b579  Nslot   slot    slot NIL
1519  B       b580    t580 b  O       o580    slot
1520  T       t581    o561 b562 b580  T       t580    o580 b555
1521  B       b581    t581 a  B       b580    t580
1522  T       t582    o561 b562 b581  P       p580    String "; "
1523    O       o581    string578 p580
1524    T       t581    o581
1525    B       b581    t581
1526    T       t582    o580 b556
1527  B       b582    t582  B       b582    t582
1528  T       t583    o563 b579 b577  P       p582    String )
1529    O       o582    string578 p582
1530    T       t583    o582
1531  B       b583    t583  B       b583    t583
1532  T       t584    o563 b568 b583  T       t584    o b583 b4
1533  B       b584    t584  B       b584    t584
1534  T       t585    o563 b566 b584  T       t585    o b582 b584
1535  B       b585    t585 b  B       b585    t585
1536  T       t586    o561 b562 b585  T       t586    o b581 b585
1537  B       b586    t586 a  B       b586    t586
1538  T       t587    o561 b562 b586  T       t587    o b580 b586
1539  B       b587    t587  B       b587    t587
1540  T       t588    o556 b582 b587  T       t588    o b579 b587
1541  B       b588    t588  B       b588    t588
1542  T       t589    o556 b576 b588  T       t589    o578 b588
1543  B       b589    t589  B       b589    t589
1544  T       t590    o556 b561 b589  T       t590    o576 b578 b557 b589
1545  B       b590    t590  B       b590    t590
1546  T       t591    o556 b558 b590  T       t591    o575 b590
1547  B       b591    t591  B       b591    t591
1548  T       t592    o556 b557 b591  O       o591    location p p
1549  B       b592    t592  NSummary!rule   rule    rule Summary
1550  NSummary!prim   prim    prim Summary  P       p591    String subgroup_wf
1551  O       o592    prim  O       o592    rule p591
1552  T       t593    o592 b4  NSummary!context_param  context_param   context_param Summary
1553    P       p592    String H
1554    O       o593    context_param p592
1555    T       t593    o593
1556  B       b593    t593  B       b593    t593
1557  T       t594    o555 b551 b592 b593 b4  T       t594    o b593 b4
1558  B       b594    t594  B       b594    t594
1559  T       t595    o554 b594  NSummary!meta_implies   meta_implies    meta_implies Summary
1560  B       b595    t595  O       o594    meta_implies
1561  P       p595    Number 1115  NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1562  P       p596    Number 1218  O       o595    meta_theorem
1563  O       o596    location p595 p596  NBase_trivial   Base_trivial    Base_trivial NIL
1564  NSummary!dform  dform   dform Summary  NBase_trivial!squash    squash  squash Base_trivial
1565  P       p597    String subgroup_df  O       o596    squash
1566  O       o597    dform p597  T       t596    o596
1567  NSummary!except_mode_df except_mode_df  except_mode_df Summary  B       b596    t596
1568  P       p598    String src  T       t597    o b596 b4
1569  O       o598    except_mode_df p598  C       h       H
1570    NItt_equal      Itt_equal       Itt_equal NIL
1571    NItt_equal!equal        equal   equal Itt_equal
1572    O       o597    equal
1573    NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1574    NItt_record_label0!label        label   label Itt_record_label0
1575    O       o598    label
1576  T       t598    o598  T       t598    o598
1577  B       b598    t598  B       b598    t598
1578  T       t599    o b598 b4  T       t599    o597 b598 b555 b555
1579  B       b599    t599  S       s       t597 h
1580  NSummary!df_term        df_term df_term Summary  G       s       t599
1581  O       o599    df_term  B       b599    s
1582  NPerv!string    string599       string Perv  T       t600    o595 b599
 P       p599    String subgroup(  
 O       o600    string599 p599  
 T       t600    o600  
1583  B       b600    t600  B       b600    t600
1584  Nslot   slot    slot NIL  T       t601    o597 b598 b556 b556
1585  O       o601    slot  S       s601    t597 h
1586  T       t601    o601 b549  G       s601    t601
1587  B       b601    t601  B       b601    s601
1588  P       p601    String "; "  T       t602    o595 b601
 O       o602    string599 p601  
 T       t602    o602  
1589  B       b602    t602  B       b602    t602
1590  T       t603    o601 b550  P       p602    Var ext
1591    O       o602    var p602
1592    T       t603    o602
1593  B       b603    t603  B       b603    t603
1594  P       p603    String )  T       t604    o b603 b4
1595  O       o603    string599 p603  NItt_equal!type type    type Itt_equal
1596  T       t604    o603  O       o604    type
1597  B       b604    t604  T       t605    o604 b557
1598  T       t605    o b604 b4  S       s605    t604 h
1599  B       b605    t605  G       s605    t605
1600  T       t606    o b603 b605  B       b605    s605
1601    T       t606    o595 b605
1602  B       b606    t606  B       b606    t606
1603  T       t607    o b602 b606  T       t607    o594 b602 b606
1604  B       b607    t607  B       b607    t607
1605  T       t608    o b601 b607  T       t608    o594 b600 b607
1606  B       b608    t608  B       b608    t608
1607  T       t609    o b600 b608  NSummary!interactive    interactive     interactive Summary
1608  B       b609    t609  O       o608    interactive
1609  T       t610    o599 b609  NSummary!ext_rule       ext_rule        ext_rule Summary
1610    P       p608    String "rwh unfold_subgroup 0 ttca"
1611    O       o609    ext_rule p608
1612    NSummary!status_incomplete      status_incomplete       status_incomplete Summary
1613    O       o610    status_incomplete
1614    T       t610    o610
1615  B       b610    t610  B       b610    t610
1616  T       t611    o597 b599 b551 b610  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
1617  B       b611    t611  O       o611    ext_unjustified
1618  T       t612    o596 b611  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
1619  B       b612    t612  P       p611    String main
1620  P       p612    Number 1237  O       o612    tactic_arg p611
1621  P       p613    Number 1425  NSummary!msequent       msequent        msequent Summary
1622  O       o613    location p612 p613  O       o613    msequent
1623  NSummary!rule   rule    rule Summary  T       t613    o b601 b4
1624  P       p614    String subgroup_wf  B       b613    t613
1625  O       o614    rule p614  T       t614    o b599 b613
1626  NSummary!context_param  context_param   context_param Summary  B       b614    t614
1627  P       p615    String H  T       t615    o613 b605 b614
 O       o615    context_param p615  
 T       t615    o615  
1628  B       b615    t615  B       b615    t615
1629  T       t616    o b615 b4  NSummary!parent_none    parent_none     parent_none Summary
1630    O       o615    parent_none
1631    T       t616    o615
1632  B       b616    t616  B       b616    t616
1633  NSummary!meta_implies   meta_implies    meta_implies Summary  T       t617    o612 b615 b4 b616
1634  O       o616    meta_implies  B       b617    t617
1635  NSummary!meta_theorem   meta_theorem    meta_theorem Summary  T       t618    o611 b617 b4
 O       o617    meta_theorem  
 NBase_trivial   Base_trivial    Base_trivial NIL  
 NBase_trivial!squash    squash  squash Base_trivial  
 O       o618    squash  
 T       t618    o618  
1636  B       b618    t618  B       b618    t618
1637  T       t619    o b618 b4  T       t619    o609 b610 b618 b4 b4
1638  C       h       H  B       b619    t619
1639  NItt_equal      Itt_equal       Itt_equal NIL  T       t620    o608 b619
 NItt_equal!equal        equal   equal Itt_equal  
 O       o619    equal  
 NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL  
 NItt_record_label0!label        label   label Itt_record_label0  
 O       o620    label  
 T       t620    o620  
1640  B       b620    t620  B       b620    t620
1641  T       t621    o619 b620 b549 b549  NSummary!resource_defs  resource_defs   resource_defs Summary
1642  S       s       t619 h  P       p620    Number 959
1643  G       s       t621  P       p621    Number 967
1644  B       b621    s  O       o621    resource_defs p620 p621 p300
1645  T       t622    o617 b621  NOcaml!uid      uid     uid Ocaml
1646  B       b622    t622  P       p622    Number 965
1647  T       t623    o619 b620 b550 b550  O       o622    uid p622 p621
1648  S       s623    t619 h  P       p623    String []
1649  G       s623    t623  O       o623    uid p623
1650  B       b623    s623  T       t623    o623
1651  T       t624    o617 b623  B       b623    t623
1652    T       t624    o622 b623
1653  B       b624    t624  B       b624    t624
1654  P       p624    Var ext  T       t625    o b624 b4
 O       o624    var p624  
 T       t625    o624  
1655  B       b625    t625  B       b625    t625
1656  T       t626    o b625 b4  T       t626    o621 b625
1657  NItt_equal!type type    type Itt_equal  B       b626    t626
1658  O       o626    type  T       t627    o b626 b4
1659  T       t627    o626 b551  B       b627    t627
1660  S       s627    t626 h  T       t628    o592 b594 b608 b620 b627
 G       s627    t627  
 B       b627    s627  
 T       t628    o617 b627  
1661  B       b628    t628  B       b628    t628
1662  T       t629    o616 b624 b628  T       t629    o591 b628
1663  B       b629    t629  B       b629    t629
1664  T       t630    o616 b622 b629  P       p629    String subgroup_intro
1665  B       b630    t630  O       o629    rule p629
1666  NSummary!interactive    interactive     interactive Summary  S       s629    t604 h
1667  O       o630    interactive  G       s629    t563
1668  NSummary!ext_rule       ext_rule        ext_rule Summary  B       b630    s629
1669  P       p630    String "rwh unfold_subgroup 0 ttca"  T       t630    o595 b630
1670  O       o631    ext_rule p630  B       b631    t630
1671  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  S       s631    t604 h
1672  O       o632    status_incomplete  G       s631    t564
1673  T       t632    o632  B       b632    s631
1674  B       b632    t632  T       t632    o595 b632
1675  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  B       b633    t632
1676  O       o633    ext_unjustified  S       s633    t604 h
1677  NSummary!tactic_arg     tactic_arg      tactic_arg Summary  G       s633    t567
1678  P       p633    String main  B       b634    s633
1679  O       o634    tactic_arg p633  T       t634    o595 b634
1680  NSummary!msequent       msequent        msequent Summary  B       b635    t634
1681  O       o635    msequent  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL
1682  T       t635    o b623 b4  NCzf_itt_set!set        set     set Czf_itt_set
1683  B       b635    t635  O       o635    set
1684  T       t636    o b621 b635  T       t635    o635
1685  B       b636    t636  H       h635    a t635
1686  T       t637    o635 b627 b636  H       h636    b t635
1687    NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1688    NCzf_itt_member!mem     mem     mem Czf_itt_member
1689    O       o636    mem
1690    P       p636    Var a
1691    O       o637    var p636
1692    T       t637    o637
1693  B       b637    t637  B       b637    t637
1694  NSummary!parent_none    parent_none     parent_none Summary  T       t638    o636 b637 b565
1695  O       o637    parent_none  H       h638    x t638
1696  T       t638    o637  P       p638    Var b
1697  B       b638    t638  O       o638    var p638
1698  T       t639    o634 b637 b4 b638  T       t639    o638
1699  B       b639    t639  B       b639    t639
1700  T       t640    o633 b639 b4  T       t640    o636 b639 b565
1701  B       b640    t640  H       h640    y t640
1702  T       t641    o631 b632 b640 b4 b4  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1703    NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1704    O       o640    equiv
1705    NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
1706    O       o641    eqG
1707    T       t641    o641 b555
1708  B       b641    t641  B       b641    t641
1709  T       t642    o630 b641  NCzf_itt_group!op       op      op Czf_itt_group
1710    O       o642    op
1711    T       t642    o642 b555 b637 b639
1712  B       b642    t642  B       b642    t642
1713  NSummary!resource_defs  resource_defs   resource_defs Summary  T       t643    o642 b556 b637 b639
1714  P       p642    Number 1264  B       b643    t643
1715  P       p643    Number 1272  T       t644    o640 b565 b641 b642 b643
1716  O       o643    resource_defs p642 p643 p300  S       s644    t604 h h635 h636 h638 h640
1717  NOcaml!uid      uid     uid Ocaml  G       s644    t644
1718  P       p644    Number 1270  B       b644    s644
1719  O       o644    uid p644 p643  T       t645    o595 b644
 P       p645    String []  
 O       o645    uid p645  
 T       t645    o645  
1720  B       b645    t645  B       b645    t645
1721  T       t646    o644 b645  H       h645    c t635
1722    H       h646    d t635
1723    P       p646    Var c
1724    O       o646    var p646
1725    T       t646    o646
1726  B       b646    t646  B       b646    t646
1727  T       t647    o b646 b4  P       p647    Var d
1728    O       o647    var p647
1729    T       t647    o647
1730  B       b647    t647  B       b647    t647
1731  T       t648    o643 b647  T       t648    o640 b565 b641 b646 b647
1732  B       b648    t648  H       h648    u t648
1733  T       t649    o b648 b4  T       t649    o641 b556
1734  B       b649    t649  B       b649    t649
1735  T       t650    o614 b616 b630 b642 b649  T       t650    o640 b566 b649 b646 b647
1736  B       b650    t650  S       s650    t604 h h645 h646 h648
1737  T       t651    o613 b650  G       s650    t650
1738    B       b650    s650
1739    T       t651    o595 b650
1740  B       b651    t651  B       b651    t651
1741  P       p651    Number 1427  H       h651    p t635
1742  P       p652    Number 2171  H       h652    q t635
1743  O       o652    location p651 p652  P       p652    Var p
1744  P       p653    String subgroup_intro  O       o652    var p652
1745  O       o653    rule p653  T       t652    o652
1746  S       s653    t626 h  B       b652    t652
1747  G       s653    t557  T       t653    o636 b652 b565
1748  B       b653    s653  H       h653    x t653
1749  T       t653    o617 b653  P       p653    Var q
1750  B       b654    t653  O       o653    var p653
1751  S       s654    t626 h  T       t654    o653
1752  G       s654    t558  B       b654    t654
1753  B       b655    s654  T       t655    o636 b654 b565
1754  T       t655    o617 b655  H       h655    y t655
1755  B       b656    t655  T       t656    o640 b566 b649 b652 b654
1756  S       s656    t626 h  H       h656    v t656
1757  G       s656    t561  T       t657    o640 b565 b641 b652 b654
1758  B       b657    s656  S       s657    t604 h h651 h652 h653 h655 h656
1759  T       t657    o617 b657  G       s657    t657
1760  B       b658    t657  B       b657    s657
1761  H       h658    a t562  T       t658    o595 b657
1762  H       h659    b t562  B       b658    t658
1763  H       h660    x t566  S       s658    t604 h
1764  H       h661    y t568  G       s658    t557
1765  S       s661    t626 h h658 h659 h660 h661  B       b659    s658
1766  G       s661    t572  T       t659    o595 b659
1767  B       b661    s661  B       b660    t659
1768  T       t661    o617 b661  T       t660    o594 b658 b660
1769    B       b661    t660
1770    T       t661    o594 b651 b661
1771  B       b662    t661  B       b662    t661
1772  H       h662    c t562  T       t662    o594 b645 b662
1773  H       h663    d t562  B       b663    t662
1774  P       p663    Var c  T       t663    o594 b635 b663
1775  O       o663    var p663  B       b664    t663
1776  T       t663    o663  T       t664    o594 b633 b664
1777  B       b663    t663  B       b665    t664
1778  P       p664    Var d  T       t665    o594 b631 b665
1779  O       o664    var p664  B       b666    t665
1780  T       t664    o664  T       t666    o594 b602 b666
1781  B       b664    t664  B       b667    t666
1782  T       t665    o568 b559 b569 b663 b664  T       t667    o594 b600 b667
1783  H       h665    u t665  B       b668    t667
1784  T       t666    o568 b560 b578 b663 b664  T       t668    o b657 b4
1785  S       s666    t626 h h662 h663 h665  B       b669    t668
1786  G       s666    t666  T       t669    o b650 b669
1787  B       b666    s666  B       b670    t669
1788  T       t667    o617 b666  T       t670    o b644 b670
1789  B       b667    t667  B       b671    t670
1790  H       h667    p t562  T       t671    o b634 b671
1791  H       h668    q t562  B       b672    t671
1792  P       p668    Var p  T       t672    o b632 b672
1793  O       o668    var p668  B       b673    t672
1794  T       t668    o668  T       t673    o b630 b673
1795  B       b668    t668  B       b674    t673
1796  T       t669    o564 b668 b559  T       t674    o b601 b674
1797  H       h669    x t669  B       b675    t674
1798  P       p669    Var q  T       t675    o b599 b675
 O       o669    var p669  
 T       t670    o669  
 B       b670    t670  
 T       t671    o564 b670 b559  
 H       h671    y t671  
 T       t672    o568 b560 b578 b668 b670  
 H       h672    v t672  
 T       t673    o568 b559 b569 b668 b670  
 S       s673    t626 h h667 h668 h669 h671 h672  
 G       s673    t673  
 B       b673    s673  
 T       t674    o617 b673  
 B       b674    t674  
 S       s674    t626 h  
 G       s674    t551  
 B       b675    s674  
 T       t675    o617 b675  
1799  B       b676    t675  B       b676    t675
1800  T       t676    o616 b674 b676  T       t676    o613 b659 b676
1801  B       b677    t676  B       b677    t676
1802  T       t677    o616 b667 b677  T       t677    o612 b677 b4 b616
1803  B       b678    t677  B       b678    t677
1804  T       t678    o616 b662 b678  T       t678    o611 b678 b4
1805  B       b679    t678  B       b679    t678
1806  T       t679    o616 b658 b679  T       t679    o609 b610 b679 b4 b4
1807  B       b680    t679  B       b680    t679
1808  T       t680    o616 b656 b680  T       t680    o608 b680
1809  B       b681    t680  B       b681    t680
1810  T       t681    o616 b654 b681  P       p681    Number 1152
1811  B       b682    t681  P       p682    Number 1160
1812  T       t682    o616 b624 b682  O       o682    resource_defs p681 p682 p300
1813  B       b683    t682  P       p683    Number 1158
1814  T       t683    o616 b622 b683  O       o683    uid p683 p682
1815  B       b684    t683  T       t683    o683 b623
1816  T       t684    o b673 b4  B       b683    t683
1817  B       b685    t684  T       t684    o b683 b4
1818  T       t685    o b666 b685  B       b684    t684
1819  B       b686    t685  T       t685    o682 b684
1820  T       t686    o b661 b686  B       b685    t685
1821  B       b687    t686  T       t686    o b685 b4
1822  T       t687    o b657 b687  B       b686    t686
1823  B       b688    t687  T       t687    o629 b594 b668 b681 b686
1824  T       t688    o b655 b688  B       b687    t687
1825  B       b689    t688  T       t688    o591 b687
1826  T       t689    o b653 b689  B       b688    t688
1827  B       b690    t689  P       p688    String subgroup_equiv
1828  T       t690    o b623 b690  O       o688    rule p688
1829  B       b691    t690  T       t689    o640 b565 b649
1830  T       t691    o b621 b691  S       s689    t604 h
1831  B       b692    t691  G       s689    t689
1832  T       t692    o635 b675 b692  B       b689    s689
1833  B       b693    t692  T       t690    o595 b689
1834  T       t693    o634 b693 b4 b638  B       b690    t690
1835  B       b694    t693  T       t691    o594 b660 b690
1836  T       t694    o633 b694 b4  B       b691    t691
1837  B       b695    t694  T       t692    o594 b602 b691
1838  T       t695    o631 b632 b695 b4 b4  B       b692    t692
1839  B       b696    t695  T       t693    o594 b600 b692
1840  T       t696    o630 b696  B       b693    t693
1841  B       b697    t696  P       p693    String "assumT 3 thenT rwh unfold_subgroup 2 thenT rwh unfold_group_bvd 2 thenT autoT"
1842  P       p697    Number 1457  O       o693    ext_rule p693
1843  P       p698    Number 1465  T       t694    o b659 b4
1844  O       o698    resource_defs p697 p698 p300  B       b694    t694
1845  P       p699    Number 1463  T       t695    o b601 b694
1846  O       o699    uid p699 p698  B       b695    t695
1847  T       t699    o699 b645  T       t696    o b599 b695
1848  B       b699    t699  B       b696    t696
1849  T       t700    o b699 b4  T       t697    o613 b689 b696
1850  B       b700    t700  B       b697    t697
1851  T       t701    o698 b700  T       t698    o612 b697 b4 b616
1852  B       b701    t701  B       b698    t698
1853  T       t702    o b701 b4  H       h698    y t563
1854  B       b702    t702  H       h699    y_1 t564
1855  T       t703    o653 b616 b684 b697 b702  H       h700    y_2 t567
1856  B       b703    t703  H       h701    y_3 t563
1857  T       t704    o652 b703  H       h702    y_4 t564
1858  B       b704    t704  NCzf_itt_set!isset      isset   isset Czf_itt_set
1859  P       p704    Number 2173  O       o702    isset
1860  P       p705    Number 2412  T       t702    o702 b565
1861  O       o705    location p704 p705  H       h703    y_5 t702
1862  P       p706    String subgroup_equiv  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
1863  O       o706    rule p706  NCzf_itt_eq!equal       equal703        equal Czf_itt_eq
1864  T       t706    o568 b559 b578  O       o703    equal703
1865  S       s706    t626 h  T       t703    o703 b565 b565
1866  G       s706    t706  H       h704    y_6 t703
1867  B       b706    s706  NItt_logic!all  all     all Itt_logic
1868  T       t707    o617 b706  O       o704    all
1869  B       b707    t707  B       b704    t635
1870  T       t708    o616 b676 b707  NItt_logic!implies      implies implies Itt_logic
1871  B       b708    t708  O       o705    implies
1872  T       t709    o616 b624 b708  B       b705    t638
1873  B       b709    t709  B       b706    t640
1874  T       t710    o616 b622 b709  B       b707    t644
1875  B       b710    t710  T       t707    o705 b706 b707
1876  P       p710    String "assumT 3 thenT rwh unfold_subgroup 2 thenT autoT"  B       b708    t707
1877  O       o710    ext_rule p710  T       t708    o705 b705 b708
1878  T       t711    o b675 b4  B       b709    t708 b
1879    T       t709    o704 b704 b709
1880    B       b710    t709 a
1881    T       t710    o704 b704 b710
1882    H       h710    y_7 t710
1883    T       t711    o640 b565 b641 b637 b639
1884  B       b711    t711  B       b711    t711
1885  T       t712    o b623 b711  T       t712    o640 b566 b649 b637 b639
1886  B       b712    t712  B       b712    t712
1887  T       t713    o b621 b712  T       t713    o705 b711 b712
1888  B       b713    t713  B       b713    t713 b
1889  T       t714    o635 b706 b713  T       t714    o704 b704 b713
1890  B       b714    t714  B       b714    t714 a
1891  T       t715    o634 b714 b4 b638  T       t715    o704 b704 b714
1892  B       b715    t715  H       h715    y_8 t715
1893  H       h715    y t557  T       t716    o705 b712 b711
1894  H       h716    y_1 t558  B       b716    t716
1895  H       h717    y_2 t561  T       t717    o705 b706 b716
1896  H       h718    y_3 t576  B       b717    t717
1897  H       h719    y_4 t582  T       t718    o705 b705 b717
1898  H       h720    z t587  B       b718    t718 b
1899  H       h721    x t568  T       t719    o704 b704 b718
1900  T       t721    o564 b663 b559  B       b719    t719 a
1901    T       t720    o704 b704 b719
1902    H       h720    z t720
1903    H       h721    x t640
1904    T       t721    o636 b646 b565
1905  H       h722    y t721  H       h722    y t721
1906  T       t722    o568 b559 b578 b567 b663  T       t722    o640 b565 b649 b639 b646
1907  H       h723    u t722  H       h723    u t722
1908  T       t723    o568 b559 b578 b663 b567  T       t723    o640 b565 b649 b646 b639
1909  S       s723    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723  S       s723    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h636 h645 h721 h722 h723
1910  G       s723    t723  G       s723    t723
1911  B       b723    s723  B       b723    s723
1912  T       t724    o635 b723 b713  T       t724    o613 b723 b696
1913  B       b724    t724  B       b724    t724
1914  S       s724    t626 h h715 h716 h717 h718 h719 h720  S       s724    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720
1915  G       s724    t706  G       s724    t689
1916  B       b725    s724  B       b725    s724
1917  T       t725    o635 b725 b713  T       t725    o613 b725 b696
1918  B       b726    t725  B       b726    t725
1919  NSummary!arg_named      arg_named       arg_named Summary  NSummary!arg_named      arg_named       arg_named Summary
1920  P       p726    String d_auto  P       p726    String d_auto
# Line 1912  Line 1928 
1928  B       b728    t728  B       b728    t728
1929  T       t729    o b728 b4  T       t729    o b728 b4
1930  B       b729    t729  B       b729    t729
1931  H       h729    z_1 t588  B       b730    t715
1932  S       s729    t626 h h715 h716 h717 h718 h729  B       b731    t720
1933  G       s729    t706  T       t731    o562 b730 b731
1934  B       b730    s729  H       h731    z_1 t731
1935  T       t730    o635 b730 b713  S       s731    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h731
1936  B       b731    t730  G       s731    t689
 H       h731    z t589  
 S       s731    t626 h h715 h716 h717 h731  
 G       s731    t706  
1937  B       b732    s731  B       b732    s731
1938  T       t732    o635 b732 b713  T       t732    o613 b732 b696
1939  B       b733    t732  B       b733    t732
1940  H       h733    z_1 t590  B       b734    t710
1941  S       s733    t626 h h715 h716 h733  B       b735    t731
1942  G       s733    t706  T       t735    o562 b734 b735
1943  B       b734    s733  H       h735    z t735
1944  T       t734    o635 b734 b713  S       s735    t604 h h698 h699 h700 h701 h702 h703 h704 h735
1945  B       b735    t734  G       s735    t689
 H       h735    z t591  
 S       s735    t626 h h715 h735  
 G       s735    t706  
1946  B       b736    s735  B       b736    s735
1947  T       t736    o635 b736 b713  T       t736    o613 b736 b696
1948  B       b737    t736  B       b737    t736
1949  H       h737    v t592  B       b738    t703
1950  S       s737    t626 h h737  B       b739    t735
1951  G       s737    t706  T       t739    o562 b738 b739
1952  B       b738    s737  H       h739    z_1 t739
1953  T       t738    o635 b738 b713  S       s739    t604 h h698 h699 h700 h701 h702 h703 h739
1954  B       b739    t738  G       s739    t689
 H       h739    v t551  
 S       s739    t626 h h739  
 G       s739    t706  
1955  B       b740    s739  B       b740    s739
1956  T       t740    o635 b740 b713  T       t740    o613 b740 b696
1957  B       b741    t740  B       b741    t740
1958  T       t741    o2 b715  B       b742    t702
1959  B       b742    t741  B       b743    t739
1960  T       t742    o634 b741 b4 b742  T       t743    o562 b742 b743
1961  B       b743    t742  H       h743    z t743
1962  T       t743    o2 b743  S       s743    t604 h h698 h699 h700 h701 h702 h743
1963  B       b744    t743  G       s743    t689
1964  T       t744    o634 b739 b4 b744  B       b744    s743
1965    T       t744    o613 b744 b696
1966  B       b745    t744  B       b745    t744
1967  T       t745    o2 b745  B       b746    t743
1968  B       b746    t745  T       t746    o562 b564 b746
1969  T       t746    o634 b737 b4 b746  H       h746    z_1 t746
1970  B       b747    t746  S       s746    t604 h h698 h699 h700 h701 h746
1971  T       t747    o2 b747  G       s746    t689
1972    B       b747    s746
1973    T       t747    o613 b747 b696
1974  B       b748    t747  B       b748    t747
1975  T       t748    o634 b735 b4 b748  B       b749    t746
1976  B       b749    t748  T       t749    o562 b563 b749
1977  T       t749    o2 b749  H       h749    z t749
1978  B       b750    t749  S       s749    t604 h h698 h699 h700 h749
1979  T       t750    o634 b733 b4 b750  G       s749    t689
1980    B       b750    s749
1981    T       t750    o613 b750 b696
1982  B       b751    t750  B       b751    t750
1983  T       t751    o2 b751  B       b752    t749
1984  B       b752    t751  T       t752    o562 b567 b752
1985  T       t752    o634 b731 b4 b752  H       h752    z_1 t752
1986  B       b753    t752  S       s752    t604 h h698 h699 h752
1987  T       t753    o2 b753  G       s752    t689
1988    B       b753    s752
1989    T       t753    o613 b753 b696
1990  B       b754    t753  B       b754    t753
1991  T       t754    o634 b726 b729 b754  B       b755    t752
1992  B       b755    t754  T       t755    o562 b564 b755
1993  T       t755    o2 b755  H       h755    z t755
1994  B       b756    t755  S       s755    t604 h h698 h755
1995  T       t756    o634 b724 b4 b756  G       s755    t689
1996    B       b756    s755
1997    T       t756    o613 b756 b696
1998  B       b757    t756  B       b757    t756
1999  H       h757    e t562  B       b758    t755
2000  H       h758    f t562  T       t758    o562 b563 b758
2001  T       t758    o564 b664 b559  H       h758    v t758
2002  H       h759    x t758  S       s758    t604 h h758
2003  P       p759    Var e  G       s758    t689
2004  O       o759    var p759  B       b759    s758
2005  T       t759    o759  T       t759    o613 b759 b696
2006  B       b759    t759  B       b760    t759
2007  T       t760    o564 b759 b559  H       h760    v t571
2008  H       h760    y t760  S       s760    t604 h h760
2009  P       p760    Var f  G       s760    t689
2010  O       o760    var p760  B       b761    s760
2011  T       t761    o760  T       t761    o613 b761 b696
2012  B       b761    t761  B       b762    t761
2013  T       t762    o564 b761 b559  H       h762    v t557
2014  H       h762    z t762  S       s762    t604 h h762
2015  T       t763    o568 b559 b578 b664 b759  G       s762    t689
2016  H       h763    u t763  B       b763    s762
2017  T       t764    o568 b559 b578 b759 b761  T       t763    o613 b763 b696
2018  H       h764    v t764  B       b764    t763
2019  T       t765    o568 b559 b578 b664 b761  T       t764    o2 b698
2020  S       s765    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764  B       b765    t764
2021  G       s765    t765  T       t765    o612 b764 b4 b765
2022  B       b765    s765  B       b766    t765
2023  T       t766    o635 b765 b713  T       t766    o2 b766
2024  B       b766    t766  B       b767    t766
2025  T       t767    o634 b766 b4 b756  T       t767    o612 b762 b4 b767
2026  B       b767    t767  B       b768    t767
2027  T       t768    o b767 b4  T       t768    o2 b768
2028  B       b768    t768  B       b769    t768
2029  T       t769    o b757 b768  T       t769    o612 b760 b4 b769
2030  B       b769    t769  B       b770    t769
2031  T       t770    o633 b715 b769  T       t770    o2 b770
2032  B       b770    t770  B       b771    t770
2033  P       p770    String "assertT << equiv{car{'g}; eqG{'g}; 'b; 'c} >> thenT autoT"  T       t771    o612 b757 b4 b771
2034  O       o770    ext_rule p770  B       b772    t771
2035  P       p771    String assertion  T       t772    o2 b772
2036  O       o771    tactic_arg p771  B       b773    t772
2037  T       t771    o568 b560 b578 b567 b663  T       t773    o612 b754 b4 b773
2038  S       s771    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723  B       b774    t773
2039  G       s771    t771  T       t774    o2 b774
2040  B       b771    s771  B       b775    t774
2041  T       t772    o635 b771 b713  T       t775    o612 b751 b4 b775
 B       b772    t772  
 T       t773    o2 b757  
 B       b773    t773  
 T       t774    o771 b772 b4 b773  
 B       b774    t774  
 H       h774    v t771  
 S       s774    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723 h774  
 G       s774    t723  
 B       b775    s774  
 T       t775    o635 b775 b713  
2042  B       b776    t775  B       b776    t775
2043  T       t776    o634 b776 b4 b773  T       t776    o2 b776
2044  B       b777    t776  B       b777    t776
2045  T       t777    o b777 b4  T       t777    o612 b748 b4 b777
2046  B       b778    t777  B       b778    t777
2047  T       t778    o b774 b778  T       t778    o2 b778
2048  B       b779    t778  B       b779    t778
2049  T       t779    o633 b757 b779  T       t779    o612 b745 b4 b779
2050  B       b780    t779  B       b780    t779
2051  P       p780    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 12 thenT autoT"  T       t780    o2 b780
2052  O       o780    ext_rule p780  B       b781    t780
2053  NCzf_itt_set!isset      isset   isset Czf_itt_set  T       t781    o612 b741 b4 b781
2054  O       o781    isset  B       b782    t781
2055  T       t781    o781 b559  T       t782    o2 b782
2056  H       h781    y_7 t781  B       b783    t782
2057  T       t782    o781 b578  T       t783    o612 b737 b4 b783
2058  H       h782    y_6 t782  B       b784    t783
2059  T       t783    o781 b567  T       t784    o2 b784
2060  H       h783    y_8 t783  B       b785    t784
2061  T       t784    o781 b663  T       t785    o612 b733 b4 b785
2062  H       h784    z_2 t784  B       b786    t785
2063  H       h785    y_5 t568  T       t786    o2 b786
2064  H       h786    z_3 t721  B       b787    t786
2065  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL  T       t787    o612 b726 b729 b787
2066  NCzf_itt_pair!pair      pair    pair Czf_itt_pair  B       b788    t787
2067  O       o786    pair  T       t788    o2 b788
2068  T       t786    o786 b567 b663  B       b789    t788
2069  B       b786    t786  T       t789    o612 b724 b4 b789
2070  T       t787    o564 b786 b578  B       b790    t789
2071  H       h787    z_1 t787  H       h790    e t635
2072  T       t788    o564 b567 b560  H       h791    f t635
2073  S       s788    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787  T       t791    o636 b647 b565
2074  G       s788    t788  H       h792    x t791
2075  B       b788    s788  P       p792    Var e
2076  T       t789    o635 b788 b713  O       o792    var p792
2077  B       b789    t789  T       t792    o792
2078  B       b790    t788  B       b792    t792
2079  T       t790    o564 b663 b560  T       t793    o636 b792 b565
2080  B       b791    t790  H       h793    y t793
2081  T       t791    o556 b790 b791  P       p793    Var f
2082  S       s791    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787  O       o793    var p793
2083  G       s791    t791  T       t794    o793
2084  B       b792    s791  B       b794    t794
2085  T       t792    o635 b792 b713  T       t795    o636 b794 b565
2086  B       b793    t792  H       h795    z t795
2087  T       t793    o781 b560  T       t796    o640 b565 b649 b647 b792
2088  B       b794    t793  H       h796    u t796
2089  B       b795    t782  T       t797    o640 b565 b649 b792 b794
2090  B       b796    t783  H       h797    v t797
2091  B       b797    t784  T       t798    o640 b565 b649 b647 b794
2092  T       t797    o556 b796 b797  S       s798    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h646 h790 h791 h792 h793 h795 h796 h797
2093  B       b798    t797  G       s798    t798
2094  T       t798    o556 b795 b798  B       b798    s798
2095  B       b799    t798  T       t799    o613 b798 b696
2096  T       t799    o556 b794 b799  B       b799    t799
2097  B       b800    t799  T       t800    o612 b799 b4 b789
2098  B       b801    t791  B       b800    t800
2099  T       t801    o556 b800 b801  T       t801    o b800 b4
2100  S       s801    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787  B       b801    t801
2101  G       s801    t801  T       t802    o b790 b801
2102  B       b802    s801  B       b802    t802
2103  T       t802    o635 b802 b713  T       t803    o611 b698 b802
2104  B       b803    t802  B       b803    t803
2105  B       b804    t801  P       p803    String "assertT << equiv{car{'g}; eqG{'g}; 'c; 'b} >> thenT autoT"
2106  B       b805    t787  O       o803    ext_rule p803
2107  T       t805    o556 b804 b805  P       p804    String assertion
2108  S       s805    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787  O       o804    tactic_arg p804
2109  G       s805    t805  T       t804    o640 b566 b649 b646 b639
2110  B       b806    s805  S       s804    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h636 h645 h721 h722 h723
2111  T       t806    o635 b806 b713  G       s804    t804
2112  B       b807    t806  B       b804    s804
2113  H       h807    z_4 t797  T       t805    o613 b804 b696
2114  S       s807    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h807 h785 h786 h787  B       b805    t805
2115  G       s807    t805  T       t806    o2 b790
2116    B       b806    t806
2117    T       t807    o804 b805 b4 b806
2118    B       b807    t807
2119    H       h807    v t804
2120    S       s807    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h636 h645 h721 h722 h723 h807
2121    G       s807    t723
2122  B       b808    s807  B       b808    s807
2123  T       t808    o635 b808 b713  T       t808    o613 b808 b696
2124  B       b809    t808  B       b809    t808
2125  H       h809    z_2 t798  T       t809    o612 b809 b4 b806
2126  S       s809    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h809 h785 h786 h787  B       b810    t809
2127  G       s809    t805  T       t810    o b810 b4
 B       b810    s809  
 T       t810    o635 b810 b713  
2128  B       b811    t810  B       b811    t810
2129  B       b812    t781  T       t811    o b807 b811
2130  T       t812    o556 b812 b799  B       b812    t811
2131  H       h812    y_6 t812  T       t812    o611 b790 b812
2132  S       s812    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h812 h785 h786 h787  B       b813    t812
2133  G       s812    t805  P       p813    String "withT << 'b >> (dT 4) ttca thenT withT << 'c >> (dT 4) ttca"
2134  B       b813    s812  O       o813    ext_rule p813
2135  T       t813    o635 b813 b713  T       t813    o636 b639 b566
2136  B       b814    t813  H       h813    z_1 t813
2137  B       b815    t721  T       t814    o636 b646 b566
2138  T       t815    o556 b568 b815  H       h814    z_2 t814
2139  H       h815    z_2 t815  S       s814    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h636 h645 h721 h722 h723 h813 h814
2140  S       s815    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h812 h815 h787  G       s814    t804
2141  G       s815    t805  B       b814    s814
2142    T       t815    o613 b814 b696
2143    B       b815    t815
2144    S       s815    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h636 h645 h721 h722 h723 h813
2145    G       s815    t804
2146  B       b816    s815  B       b816    s815
2147  T       t816    o635 b816 b713  T       t816    o613 b816 b696
2148  B       b817    t816  B       b817    t816
2149  B       b818    t812  P       p817    String with
2150  B       b819    t815  O       o817    arg_named p817
2151  T       t819    o556 b818 b819  NSummary!arg_term_list  arg_term_list   arg_term_list Summary
2152  H       h819    y_5 t819  O       o818    arg_term_list
2153  S       s819    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h819 h787  T       t818    o b646 b4
2154  G       s819    t805  B       b818    t818
2155  B       b820    s819  T       t819    o818 b818
2156  T       t820    o635 b820 b713  B       b819    t819
2157  B       b821    t820  T       t820    o817 b819
2158  B       b822    t819  B       b820    t820
2159  T       t822    o556 b822 b805  T       t821    o b820 b4
2160  H       h822    u t822  B       b821    t821
2161  S       s822    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h822  T       t822    o b639 b4
2162  G       s822    t805  B       b822    t822
2163  B       b823    s822  T       t823    o818 b822
2164  T       t823    o635 b823 b713  B       b823    t823
2165  B       b824    t823  T       t824    o817 b823
2166  S       s824    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723  B       b824    t824
2167  G       s824    t805  T       t825    o b824 b4
2168  B       b825    s824  B       b825    t825
2169  T       t825    o635 b825 b713  T       t826    o804 b805 b825 b806
2170  B       b826    t825  B       b826    t826
2171  T       t826    o2 b774  T       t827    o2 b826
2172  B       b827    t826  B       b827    t827
2173  T       t827    o771 b826 b4 b827  T       t828    o612 b817 b821 b827
2174  B       b828    t827  B       b828    t828
2175  T       t828    o2 b828  T       t829    o2 b828
2176  B       b829    t828  B       b829    t829
2177  T       t829    o771 b824 b4 b829  T       t830    o612 b815 b4 b829
2178  B       b830    t829  B       b830    t830
2179  T       t830    o2 b830  T       t831    o b830 b4
2180  B       b831    t830  B       b831    t831
2181  T       t831    o634 b821 b4 b831  T       t832    o611 b807 b831
2182  B       b832    t831  B       b832    t832
2183  T       t832    o2 b832  P       p832    String "equivSymT ttca thenT rwh unfold_equiv 16 thenT rwh unfold_equiv 0 ttca"
2184  B       b833    t832  O       o832    ext_rule p832
2185  T       t833    o634 b817 b4 b833  T       t833    o611 b830 b4
2186  B       b834    t833  B       b833    t833
2187  T       t834    o2 b834  T       t834    o832 b610 b833 b4 b4
2188  B       b835    t834  B       b834    t834
2189  T       t835    o634 b814 b4 b835  T       t835    o b834 b4
2190  B       b836    t835  B       b835    t835
2191  T       t836    o2 b836  T       t836    o813 b610 b832 b835 b4
2192  B       b837    t836  B       b836    t836
2193  T       t837    o634 b811 b4 b837  P       p836    String "rwh unfold_equiv 17 thenT rwh unfold_equiv 0 ttca"
2194  B       b838    t837  O       o836    ext_rule p836
2195  T       t838    o2 b838  T       t837    o611 b810 b4
2196  B       b839    t838  B       b837    t837
2197  T       t839    o634 b809 b4 b839  T       t838    o836 b610 b837 b4 b4
2198  B       b840    t839  B       b838    t838
2199  T       t840    o2 b840  T       t839    o b838 b4
2200  B       b841    t840  B       b839    t839
2201  T       t841    o634 b807 b729 b841  T       t840    o b836 b839
2202  B       b842    t841  B       b840    t840
2203  T       t842    o2 b842  T       t841    o803 b610 b813 b840 b4
2204  B       b843    t842  B       b841    t841
2205  T       t843    o634 b803 b729 b843  P       p841    String "withT << 'd >> (dT 4) ttca thenT withT << 'e >> (dT 4) ttca thenT withT << 'f >> (dT 4) ttca"
2206  B       b844    t843  O       o841    ext_rule p841
2207  T       t844    o2 b844  T       t842    o636 b647 b566
2208  B       b845    t844  H       h842    z_1 t842
2209  T       t845    o634 b793 b729 b845  T       t843    o636 b792 b566
2210  B       b846    t845  H       h843    z_2 t843
2211  T       t846    o2 b846  T       t844    o636 b794 b566
2212    H       h844    z_3 t844
2213    S       s844    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h646 h790 h791 h792 h793 h795 h796 h797 h842 h843 h844
2214    G       s844    t798
2215    B       b844    s844
2216    T       t845    o613 b844 b696
2217    B       b845    t845
2218    S       s845    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h646 h790 h791 h792 h793 h795 h796 h797 h842 h843
2219    G       s845    t798
2220    B       b846    s845
2221    T       t846    o613 b846 b696
2222  B       b847    t846  B       b847    t846
2223  T       t847    o634 b789 b4 b847  T       t847    o b794 b4
2224  B       b848    t847  B       b848    t847
2225  S       s848    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787  T       t848    o818 b848
2226  G       s848    t790  B       b849    t848
2227  B       b849    s848  T       t849    o817 b849
 T       t849    o635 b849 b713  
2228  B       b850    t849  B       b850    t849
2229  T       t850    o634 b850 b4 b847  T       t850    o b850 b4
2230  B       b851    t850  B       b851    t850
2231  T       t851    o b851 b4  S       s851    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h646 h790 h791 h792 h793 h795 h796 h797 h842
2232  B       b852    t851  G       s851    t798
2233  T       t852    o b848 b852  B       b852    s851
2234    T       t852    o613 b852 b696
2235  B       b853    t852  B       b853    t852
2236  T       t853    o633 b774 b853  T       t853    o b792 b4
2237  B       b854    t853  B       b854    t853
2238  P       p854    String "withT << 'b >> (dT 4) ttca"  T       t854    o818 b854
 O       o854    ext_rule p854  
 T       t854    o633 b848 b4  
2239  B       b855    t854  B       b855    t854
2240  T       t855    o854 b632 b855 b4 b4  T       t855    o817 b855
2241  B       b856    t855  B       b856    t855
2242  P       p856    String "withT << 'c >> (dT 4) ttca"  T       t856    o b856 b4
 O       o856    ext_rule p856  
 T       t856    o633 b851 b4  
2243  B       b857    t856  B       b857    t856
2244  T       t857    o856 b632 b857 b4 b4  T       t857    o b647 b4
2245  B       b858    t857  B       b858    t857
2246  T       t858    o b858 b4  T       t858    o818 b858
2247  B       b859    t858  B       b859    t858
2248  T       t859    o b856 b859  T       t859    o817 b859
2249  B       b860    t859  B       b860    t859
2250  T       t860    o780 b632 b854 b860 b4  T       t860    o b860 b4
2251  B       b861    t860  B       b861    t860
2252  P       p861    String "assertT << equiv{car{'g}; eqG{'g}; 'c; 'b} >> thenT autoT"  T       t861    o612 b799 b861 b789
2253  O       o861    ext_rule p861  B       b862    t861
2254  T       t861    o568 b560 b578 b663 b567  T       t862    o2 b862
 S       s861    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723 h774  
 G       s861    t861  
 B       b862    s861  
 T       t862    o635 b862 b713  
2255  B       b863    t862  B       b863    t862
2256  T       t863    o2 b777  T       t863    o612 b853 b857 b863
2257  B       b864    t863  B       b864    t863
2258  T       t864    o771 b863 b4 b864  T       t864    o2 b864
2259  B       b865    t864  B       b865    t864
2260  H       h865    v_1 t861  T       t865    o612 b847 b851 b865
2261  S       s865    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723 h774 h865  B       b866    t865
2262  G       s865    t723  T       t866    o2 b866
 B       b866    s865  
 T       t866    o635 b866 b713  
2263  B       b867    t866  B       b867    t866
2264  T       t867    o634 b867 b4 b864  T       t867    o612 b845 b4 b867
2265  B       b868    t867  B       b868    t867
2266  T       t868    o b868 b4  T       t868    o b868 b4
2267  B       b869    t868  B       b869    t868
2268  T       t869    o b865 b869  T       t869    o611 b800 b869
2269  B       b870    t869  B       b870    t869
2270  T       t870    o633 b777 b870  P       p870    String "assertT << equiv{car{'g}; eqG{'g}; 'd; 'f} >> thenT autoT"
2271  B       b871    t870  O       o870    ext_rule p870
2272  P       p871    String "equivSymT ttca thenT rwh unfold_equiv 13 ttca"  T       t870    o640 b566 b649 b647 b794
2273  O       o871    ext_rule p871  S       s870    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h646 h790 h791 h792 h793 h795 h796 h797 h842 h843 h844
2274  T       t871    o633 b865 b4  G       s870    t870
2275    B       b871    s870
2276    T       t871    o613 b871 b696
2277  B       b872    t871  B       b872    t871
2278  T       t872    o871 b632 b872 b4 b4  T       t872    o2 b868
2279  B       b873    t872  B       b873    t872
2280  P       p873    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 14 thenT autoT"  T       t873    o804 b872 b4 b873
 O       o873    ext_rule p873  
 T       t873    o633 b868 b4  
2281  B       b874    t873  B       b874    t873
2282  T       t874    o873 b632 b874 b4 b4  H       h874    v_1 t870
2283  B       b875    t874  S       s874    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h646 h790 h791 h792 h793 h795 h796 h797 h842 h843 h844 h874
2284  T       t875    o b875 b4  G       s874    t798
2285    B       b875    s874
2286    T       t875    o613 b875 b696
2287  B       b876    t875  B       b876    t875
2288  T       t876    o b873 b876  T       t876    o612 b876 b4 b873
2289  B       b877    t876  B       b877    t876
2290  T       t877    o861 b632 b871 b877 b4  T       t877    o b877 b4
2291  B       b878    t877  B       b878    t877
2292  T       t878    o b878 b4  T       t878    o b874 b878
2293  B       b879    t878  B       b879    t878
2294  T       t879    o b861 b879  T       t879    o611 b868 b879
2295  B       b880    t879  B       b880    t879
2296  T       t880    o770 b632 b780 b880 b4  P       p880    String "equivTransT << 'e >> ttca thenT rwh unfold_equiv 0 thenT rwh unfold_equiv 18 thenT rwh unfold_equiv 19 ttca"
2297    O       o880    ext_rule p880
2298    T       t880    o611 b874 b4
2299  B       b881    t880  B       b881    t880
2300  P       p881    String "withT << 'd >> (dT 4) ttca thenT withT << 'e >> (dT 4) ttca thenT withT << 'f >> (dT 4) ttca"  T       t881    o880 b610 b881 b4 b4
2301  O       o881    ext_rule p881  B       b882    t881
2302  T       t881    o564 b664 b560  P       p882    String "rwh unfold_equiv 23 thenT rwh unfold_equiv 0 ttca"
2303  H       h881    z_1 t881  O       o882    ext_rule p882
2304  T       t882    o564 b759 b560  T       t882    o611 b877 b4
2305  H       h882    z_2 t882  B       b883    t882
2306  T       t883    o564 b761 b560  T       t883    o882 b610 b883 b4 b4
2307  H       h883    z_3 t883  B       b884    t883
2308  S       s883    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882 h883  T       t884    o b884 b4
2309  G       s883    t765  B       b885    t884
2310  B       b883    s883  T       t885    o b882 b885
 T       t884    o635 b883 b713  
 B       b884    t884  
 S       s884    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882  
 G       s884    t765  
 B       b885    s884  
 T       t885    o635 b885 b713  
2311  B       b886    t885  B       b886    t885
2312  P       p886    String with  T       t886    o870 b610 b880 b886 b4
2313  O       o886    arg_named p886  B       b887    t886
2314  NSummary!arg_term_list  arg_term_list   arg_term_list Summary  T       t887    o b887 b4
2315  O       o887    arg_term_list  B       b888    t887
2316  T       t887    o b761 b4  T       t888    o841 b610 b870 b888 b4
2317  B       b887    t887  B       b889    t888
2318  T       t888    o887 b887  T       t889    o b889 b4
2319  B       b888    t888  B       b890    t889
2320  T       t889    o886 b888  T       t890    o b841 b890
2321  B       b889    t889  B       b891    t890
2322  T       t890    o b889 b4  T       t891    o693 b610 b803 b891 b4
 B       b890    t890  
 S       s890    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881  
 G       s890    t765  
 B       b891    s890  
 T       t891    o635 b891 b713  
2323  B       b892    t891  B       b892    t891
2324  T       t892    o b759 b4  T       t892    o608 b892
2325  B       b893    t892  B       b893    t892
2326  T       t893    o887 b893  P       p893    Number 1920
2327  B       b894    t893  P       p894    Number 1928
2328  T       t894    o886 b894  O       o894    resource_defs p893 p894 p300
2329  B       b895    t894  P       p895    Number 1926
2330  T       t895    o b895 b4  O       o895    uid p895 p894
2331  B       b896    t895  T       t895    o895 b623
2332  T       t896    o b664 b4  B       b895    t895
2333  B       b897    t896  T       t896    o b895 b4
2334  T       t897    o887 b897  B       b896    t896
2335  B       b898    t897  T       t897    o894 b896
2336  T       t898    o886 b898  B       b897    t897
2337  B       b899    t898  T       t898    o b897 b4
2338  T       t899    o b899 b4  B       b898    t898
2339  B       b900    t899  T       t899    o688 b594 b693 b893 b898
2340  T       t900    o634 b766 b900 b756  B       b899    t899
2341  B       b901    t900  T       t900    o591 b899
2342  T       t901    o2 b901  B       b900    t900
2343  B       b902    t901  P       p900    String subgroup_id
2344  T       t902    o634 b892 b896 b902  O       o900    rule p900
2345  B       b903    t902  NCzf_itt_group!id       id      id Czf_itt_group
2346  T       t903    o2 b903  O       o901    id
2347  B       b904    t903  T       t901    o901 b555
2348  T       t904    o634 b886 b890 b904  B       b901    t901
2349  B       b905    t904  T       t902    o901 b556
2350  T       t905    o2 b905  B       b902    t902
2351  B       b906    t905  T       t903    o640 b566 b649 b901 b902
2352  T       t906    o634 b884 b4 b906  S       s903    t604 h
2353  B       b907    t906  G       s903    t903
2354  T       t907    o b907 b4  B       b903    s903
2355  B       b908    t907  T       t904    o595 b903
2356  T       t908    o633 b767 b908  B       b904    t904
2357  B       b909    t908  T       t905    o594 b660 b904
2358  P       p909    String "assertT << equiv{car{'g}; eqG{'g}; 'd; 'f} >> thenT autoT"  B       b905    t905
2359  O       o909    ext_rule p909  T       t906    o594 b602 b905
2360  T       t909    o568 b560 b578 b664 b761  B       b906    t906
2361  S       s909    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882 h883  T       t907    o594 b600 b906
2362  G       s909    t909  B       b907    t907
2363    T       t908    o613 b903 b696
2364    B       b908    t908
2365    T       t909    o612 b908 b4 b616
2366    B       b909    t909
2367    S       s909    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720
2368    G       s909    t903
2369  B       b910    s909  B       b910    s909
2370  T       t910    o635 b910 b713  T       t910    o613 b910 b696
2371  B       b911    t910  B       b911    t910
2372  T       t911    o2 b907  S       s911    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h731
2373  B       b912    t911  G       s911    t903
2374  T       t912    o771 b911 b4 b912  B       b912    s911
2375    T       t912    o613 b912 b696
2376  B       b913    t912  B       b913    t912
2377  H       h913    v_1 t909  S       s913    t604 h h698 h699 h700 h701 h702 h703 h704 h735
2378  S       s913    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882 h883 h913  G       s913    t903
 G       s913    t765  
2379  B       b914    s913  B       b914    s913
2380  T       t914    o635 b914 b713  T       t914    o613 b914 b696
2381  B       b915    t914  B       b915    t914
2382  T       t915    o634 b915 b4 b912  S       s915    t604 h h698 h699 h700 h701 h702 h703 h739
2383  B       b916    t915  G       s915    t903
2384  T       t916    o b916 b4  B       b916    s915
2385    T       t916    o613 b916 b696
2386  B       b917    t916  B       b917    t916
2387  T       t917    o b913 b917  S       s917    t604 h h698 h699 h700 h701 h702 h743
2388  B       b918    t917  G       s917    t903
2389  T       t918    o633 b907 b918  B       b918    s917
2390    T       t918    o613 b918 b696
2391  B       b919    t918  B       b919    t918
2392  P       p919    String "equivTransT << 'e >> ttca thenT rwh unfold_equiv 0 thenT rwh unfold_equiv 14 thenT rwh unfold_equiv 15 ttca"  S       s919    t604 h h698 h699 h700 h701 h746
2393  O       o919    ext_rule p919  G       s919    t903
2394  T       t919    o633 b913 b4  B       b920    s919
2395  B       b920    t919  T       t920    o613 b920 b696
 T       t920    o919 b632 b920 b4 b4  
2396  B       b921    t920  B       b921    t920
2397  P       p921    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 19 ttca"  S       s921    t604 h h698 h699 h700 h749
2398  O       o921    ext_rule p921  G       s921    t903
2399  T       t921    o633 b916 b4  B       b922    s921
2400  B       b922    t921  T       t922    o613 b922 b696
 T       t922    o921 b632 b922 b4 b4  
2401  B       b923    t922  B       b923    t922
2402  T       t923    o b923 b4  S       s923    t604 h h698 h699 h752
2403  B       b924    t923  G       s923    t903
2404  T       t924    o b921 b924  B       b924    s923
2405    T       t924    o613 b924 b696
2406  B       b925    t924  B       b925    t924
2407  T       t925    o909 b632 b919 b925 b4  S       s925    t604 h h698 h755
2408  B       b926    t925  G       s925    t903
2409  T       t926    o b926 b4  B       b926    s925
2410    T       t926    o613 b926 b696
2411  B       b927    t926  B       b927    t926
2412  T       t927    o881 b632 b909 b927 b4  S       s927    t604 h h758
2413  B       b928    t927  G       s927    t903
2414  T       t928    o b928 b4  B       b928    s927
2415    T       t928    o613 b928 b696
2416  B       b929    t928  B       b929    t928
2417  T       t929    o b881 b929  S       s929    t604 h h760
2418  B       b930    t929  G       s929    t903
2419  T       t930    o710 b632 b770 b930 b4  B       b930    s929
2420    T       t930    o613 b930 b696
2421  B       b931    t930  B       b931    t930
2422  T       t931    o630 b931  S       s931    t604 h h762
2423  B       b932    t931  G       s931    t903
2424  P       p932    Number 2203  B       b932    s931
2425  P       p933    Number 2211  T       t932    o613 b932 b696
2426  O       o933    resource_defs p932 p933 p300  B       b933    t932
2427  P       p934    Number 2209  T       t933    o2 b909
2428  O       o934    uid p934 p933  B       b934    t933
2429  T       t934    o934 b645  T       t934    o612 b933 b4 b934
2430  B       b934    t934  B       b935    t934
2431  T       t935    o b934 b4  T       t935    o2 b935
2432  B       b935    t935  B       b936    t935
2433  T       t936    o933 b935  T       t936    o612 b931 b4 b936
2434  B       b936    t936  B       b937    t936
2435  T       t937    o b936 b4  T       t937    o2 b937
2436  B       b937    t937  B       b938    t937
2437  T       t938    o706 b616 b710 b932 b937  T       t938    o612 b929 b4 b938
2438  B       b938    t938  B       b939    t938
2439  T       t939    o705 b938  T       t939    o2 b939
2440  B       b939    t939  B       b940    t939
2441  P       p939    Number 2414  T       t940    o612 b927 b4 b940
2442  P       p940    Number 2666  B       b941    t940
2443  O       o940    location p939 p940  T       t941    o2 b941
2444  P       p941    String subgroup_id  B       b942    t941
2445  O       o941    rule p941  T       t942    o612 b925 b4 b942
2446  NCzf_itt_group!id       id      id Czf_itt_group  B       b943    t942
2447  O       o942    id  T       t943    o2 b943
2448  T       t942    o942 b549  B       b944    t943
2449  B       b942    t942  T       t944    o612 b923 b4 b944
2450  T       t943    o942 b550  B       b945    t944
2451  B       b943    t943  T       t945    o2 b945
2452  T       t944    o568 b560 b578 b942 b943  B       b946    t945
2453  S       s944    t626 h  T       t946    o612 b921 b4 b946
2454  G       s944    t944  B       b947    t946
2455  B       b944    s944  T       t947    o2 b947
2456  T       t945    o617 b944  B       b948    t947
2457  B       b945    t945  T       t948    o612 b919 b4 b948
2458  T       t946    o616 b676 b945  B       b949    t948
2459  B       b946    t946  T       t949    o2 b949
2460  T       t947    o616 b624 b946  B       b950    t949
2461  B       b947    t947  T       t950    o612 b917 b4 b950
2462  T       t948    o616 b622 b947  B       b951    t950
2463  B       b948    t948  T       t951    o2 b951
 T       t949    o635 b944 b713  
 B       b949    t949  
 T       t950    o634 b949 b4 b638  
 B       b950    t950  
 S       s950    t626 h h715 h716 h717 h718 h719 h720  
 G       s950    t944  
 B       b951    s950  
 T       t951    o635 b951 b713  
2464  B       b952    t951  B       b952    t951
2465  S       s952    t626 h h715 h716 h717 h718 h729  T       t952    o612 b915 b4 b952
2466  G       s952    t944  B       b953    t952
2467  B       b953    s952  T       t953    o2 b953
 T       t953    o635 b953 b713  
2468  B       b954    t953  B       b954    t953
2469  S       s954    t626 h h715 h716 h717 h731  T       t954    o612 b913 b4 b954
2470  G       s954    t944  B       b955    t954
2471  B       b955    s954  T       t955    o2 b955
 T       t955    o635 b955 b713  
2472  B       b956    t955  B       b956    t955
2473  S       s956    t626 h h715 h716 h733  T       t956    o612 b911 b4 b956
2474  G       s956    t944  B       b957    t956
2475  B       b957    s956  T       t957    o b957 b4
 T       t957    o635 b957 b713  
2476  B       b958    t957  B       b958    t957
2477  S       s958    t626 h h715 h735  T       t958    o611 b909 b958
2478  G       s958    t944  B       b959    t958
2479  B       b959    s958  P       p959    String "instHypT [<< op{'g; id{'s}; id{'s}} >>; << id{'s} >>] 10 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 12 ttca"
2480  T       t959    o635 b959 b713  O       o959    ext_rule p959
2481    T       t959    o642 b556 b901 b901
2482  B       b960    t959  B       b960    t959
2483  S       s960    t626 h h737  T       t960    o640 b565 b641 b960 b901
2484  G       s960    t944  S       s960    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720
2485    G       s960    t960
2486  B       b961    s960  B       b961    s960
2487  T       t961    o635 b961 b713  T       t961    o613 b961 b696
2488  B       b962    t961  B       b962    t961
2489  S       s962    t626 h h739  B       b963    t960
2490  G       s962    t944  T       t963    o640 b566 b649 b960 b901
 B       b963    s962  
 T       t963    o635 b963 b713  
2491  B       b964    t963  B       b964    t963
2492  T       t964    o2 b950  T       t964    o705 b963 b964
2493  B       b965    t964  H       h964    w_1 t964
2494  T       t965    o634 b964 b4 b965  S       s964    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h964
2495    G       s964    t960
2496    B       b965    s964
2497    T       t965    o613 b965 b696
2498  B       b966    t965  B       b966    t965
2499  T       t966    o2 b966  S       s966    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h964
2500  B       b967    t966  G       s966    t903
2501  T       t967    o634 b962 b4 b967  B       b967    s966
2502    T       t967    o613 b967 b696
2503  B       b968    t967  B       b968    t967
2504  T       t968    o2 b968  T       t968    o640 b565 b641 b960 b639
2505  B       b969    t968  B       b969    t968
2506  T       t969    o634 b960 b4 b969  T       t969    o640 b566 b649 b960 b639
2507  B       b970    t969  B       b970    t969
2508  T       t970    o2 b970  T       t970    o705 b969 b970
2509  B       b971    t970  B       b971    t970 b
2510  T       t971    o634 b958 b4 b971  T       t971    o704 b704 b971
2511  B       b972    t971  H       h971    w t971
2512  T       t972    o2 b972  S       s971    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h971 h964
2513    G       s971    t903
2514    B       b972    s971
2515    T       t972    o613 b972 b696
2516  B       b973    t972  B       b973    t972
2517  T       t973    o634 b956 b4 b973  P       p973    String thin
2518  B       b974    t973  O       o973    arg_named p973
2519  T       t974    o2 b974  P       p974    String false
2520  B       b975    t974  O       o974    arg_bool p974
2521  T       t975    o634 b954 b4 b975  T       t974    o974
2522  B       b976    t975  B       b974    t974
2523  T       t976    o2 b976  T       t975    o973 b974
2524  B       b977    t976  B       b975    t975
2525  T       t977    o634 b952 b4 b977  T       t976    o b975 b4
2526    B       b976    t976
2527    S       s976    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h971
2528    G       s976    t903
2529    B       b977    s976
2530    T       t977    o613 b977 b696
2531  B       b978    t977  B       b978    t977
2532  T       t978    o b978 b4  T       t978    o b901 b4
2533  B       b979    t978  B       b979    t978
2534  T       t979    o633 b950 b979  T       t979    o818 b979
2535  B       b980    t979  B       b980    t979
2536  P       p980    String "instHypT [<< op{'g; id{'s}; id{'s}} >>; << id{'s} >>] 6 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca"  T       t980    o817 b980
 O       o980    ext_rule p980  
 T       t980    o570 b550 b942 b942  
2537  B       b981    t980  B       b981    t980
2538  T       t981    o568 b559 b569 b981 b942  T       t981    o b981 b976
2539  S       s981    t626 h h715 h716 h717 h718 h719 h720  B       b982    t981
2540  G       s981    t981  T       t982    o b960 b4
 B       b982    s981  
 T       t982    o635 b982 b713  
2541  B       b983    t982  B       b983    t982
2542  B       b984    t981  T       t983    o818 b983
2543  T       t984    o568 b560 b578 b981 b942  B       b984    t983
2544    T       t984    o817 b984
2545  B       b985    t984  B       b985    t984
2546  T       t985    o563 b984 b985  T       t985    o b985 b976
2547  H       h985    w_1 t985  B       b986    t985
2548  S       s985    t626 h h715 h716 h717 h718 h719 h720 h985  T       t986    o612 b911 b986 b956
 G       s985    t981  
 B       b986    s985  
 T       t986    o635 b986 b713  
2549  B       b987    t986  B       b987    t986
2550  S       s987    t626 h h715 h716 h717 h718 h719 h720 h985  T       t987    o2 b987
2551  G       s987    t944  B       b988    t987
2552  B       b988    s987  T       t988    o612 b978 b982 b988
 T       t988    o635 b988 b713  
2553  B       b989    t988  B       b989    t988
2554  T       t989    o568 b559 b569 b981 b567  T       t989    o2 b989
2555  B       b990    t989  B       b990    t989
2556  T       t990    o568 b560 b578 b981 b567  T       t990    o612 b973 b976 b990
2557  B       b991    t990  B       b991    t990
2558  T       t991    o563 b990 b991  T       t991    o2 b991
2559  B       b992    t991 b  B       b992    t991
2560  T       t992    o561 b562 b992  T       t992    o612 b968 b4 b992
2561  H       h992    w t992  B       b993    t992
2562  S       s992    t626 h h715 h716 h717 h718 h719 h720 h992 h985  T       t993    o2 b993
 G       s992    t944  
 B       b993    s992  
 T       t993    o635 b993 b713  
2563  B       b994    t993  B       b994    t993
2564  P       p994    String thin  T       t994    o804 b966 b4 b994
2565  O       o994    arg_named p994  B       b995    t994
2566  P       p995    String false  T       t995    o2 b995
2567  O       o995    arg_bool p995  B       b996    t995
2568  T       t995    o995  T       t996    o804 b962 b4 b996
2569  B       b995    t995  B       b997    t996
2570  T       t996    o994 b995  H       h997    y_9 t963
2571  B       b996    t996  S       s997    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h997
2572  T       t997    o b996 b4  G       s997    t903
 B       b997    t997  
 S       s997    t626 h h715 h716 h717 h718 h719 h720 h992  
 G       s997    t944  
2573  B       b998    s997  B       b998    s997
2574  T       t998    o635 b998 b713  T       t998    o613 b998 b696
2575  B       b999    t998  B       b999    t998
2576  T       t999    o b942 b4  S       s999    t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h964 h997
2577  B       b1000   t999  G       s999    t903
2578  T       t1000   o887 b1000  B       b1000   s999
2579    T       t1000   o613 b1000 b696
2580  B       b1001   t1000  B       b1001   t1000
2581  T       t1001   o886 b1001  T       t1001   o612 b1001 b4 b994
2582  B       b1002   t1001  B       b1002   t1001
2583  T       t1002   o b1002 b997  T       t1002   o2 b1002
2584  B       b1003   t1002  B       b1003   t1002
2585  T       t1003   o b981 b4  T       t1003   o612 b999 b4 b1003
2586  B       b1004   t1003  B       b1004   t1003
2587  T       t1004   o887 b1004  T       t1004   o b1004 b4
2588  B       b1005   t1004  B       b1005   t1004
2589  T       t1005   o886 b1005  T       t1005   o b997 b1005
2590  B       b1006   t1005  B       b1006   t1005
2591  T       t1006   o b1006 b997  T       t1006   o611 b957 b1006
2592  B       b1007   t1006  B       b1007   t1006
2593  T       t1007   o634 b952 b1007 b977  P       p1007   String "instHypT [<< id{'s} >>; << id{'s} >>] 9 thenT rwh fold_isset 0 thenT autoT thenT dT 12 ttca thenT dT 12 ttca"
2594    O       o1007   ext_rule p1007
2595    T       t1007   o642 b555 b901 b901
2596  B       b1008   t1007  B       b1008   t1007
2597  T       t1008   o2 b1008  T       t1008   o640 b565 b641 b1008 b960
2598  B       b1009   t1008  H       h1008   y_10 t1008
2599  T       t1009   o634 b999 b1003 b1009  S       s1008   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1008
2600    G       s1008   t960
2601    B       b1009   s1008
2602    T       t1009   o613 b1009 b696
2603  B       b1010   t1009  B       b1010   t1009
2604  T       t1010   o2 b1010  T       t1010   o636 b901 b565
2605  B       b1011   t1010  B       b1011   t1010
2606  T       t1011   o634 b994 b997 b1011  B       b1012   t1008
2607  B       b1012   t1011  T       t1012   o705 b1011 b1012
2608  T       t1012   o2 b1012  H       h1012   y_9 t1012
2609  B       b1013   t1012  S       s1012   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1012 h1008
2610  T       t1013   o634 b989 b4 b1013  G       s1012   t960
2611    B       b1013   s1012
2612    T       t1013   o613 b1013 b696
2613  B       b1014   t1013  B       b1014   t1013
2614  T       t1014   o2 b1014  S       s1014   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1012
2615  B       b1015   t1014  G       s1014   t960
2616  T       t1015   o771 b987 b4 b1015  B       b1015   s1014
2617    T       t1015   o613 b1015 b696
2618  B       b1016   t1015  B       b1016   t1015
2619  T       t1016   o2 b1016  B       b1017   t1012
2620  B       b1017   t1016  T       t1017   o705 b1011 b1017
2621  T       t1017   o771 b983 b4 b1017  H       h1017   w_1 t1017
2622  B       b1018   t1017  S       s1017   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1017 h1012
2623  H       h1018   y_5 t984  G       s1017   t960
2624  S       s1018   t626 h h715 h716 h717 h718 h719 h720 h1018  B       b1018   s1017
2625  G       s1018   t944  T       t1018   o613 b1018 b696
2626  B       b1019   s1018  B       b1019   t1018
2627  T       t1019   o635 b1019 b713  S       s1019   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1017
2628  B       b1020   t1019  G       s1019   t960
2629  S       s1020   t626 h h715 h716 h717 h718 h719 h720 h985 h1018  B       b1020   s1019
2630  G       s1020   t944  T       t1020   o613 b1020 b696
2631  B       b1021   s1020  B       b1021   t1020
2632  T       t1021   o635 b1021 b713  T       t1021   o642 b555 b901 b639
2633  B       b1022   t1021  B       b1022   t1021
2634  T       t1022   o634 b1022 b4 b1015  T       t1022   o642 b556 b901 b639
2635  B       b1023   t1022  B       b1023   t1022
2636  T       t1023   o2 b1023  T       t1023   o640 b565 b641 b1022 b1023
2637  B       b1024   t1023  B       b1024   t1023
2638  T       t1024   o634 b1020 b4 b1024  T       t1024   o705 b706 b1024
2639  B       b1025   t1024  B       b1025   t1024
2640  T       t1025   o b1025 b4  T       t1025   o705 b1011 b1025
2641  B       b1026   t1025  B       b1026   t1025 b
2642  T       t1026   o b1018 b1026  T       t1026   o704 b704 b1026
2643  B       b1027   t1026  H       h1026   w t1026
2644  T       t1027   o633 b978 b1027  S       s1026   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1026 h1017
2645    G       s1026   t960
2646    B       b1027   s1026
2647    T       t1027   o613 b1027 b696
2648  B       b1028   t1027  B       b1028   t1027
2649  P       p1028   String "instHypT [<< id{'s} >>; << id{'s} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca thenT dT 8 ttca"  S       s1028   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1026
2650  O       o1028   ext_rule p1028  G       s1028   t960
2651  T       t1028   o570 b549 b942 b942  B       b1029   s1028
2652  B       b1029   t1028  T       t1029   o613 b1029 b696
2653  T       t1029   o568 b559 b569 b1029 b981  B       b1030   t1029
2654  H       h1029   y_6 t1029  T       t1030   o804 b962 b982 b996
 S       s1029   t626 h h715 h716 h717 h718 h719 h720 h1029  
 G       s1029   t981  
 B       b1030   s1029  
 T       t1030   o635 b1030 b713  
2655  B       b1031   t1030  B       b1031   t1030
2656  T       t1031   o564 b942 b559  T       t1031   o2 b1031
2657  B       b1032   t1031  B       b1032   t1031
2658  B       b1033   t1029  T       t1032   o612 b1030 b982 b1032
2659  T       t1033   o563 b1032 b1033  B       b1033   t1032
2660  H       h1033   y_5 t1033  T       t1033   o2 b1033
2661  S       s1033   t626 h h715 h716 h717 h718 h719 h720 h1033 h1029  B       b1034   t1033
2662  G       s1033   t981  T       t1034   o612 b1028 b976 b1034
 B       b1034   s1033  
 T       t1034   o635 b1034 b713  
2663  B       b1035   t1034  B       b1035   t1034
2664  S       s1035   t626 h h715 h716 h717 h718 h719 h720 h1033  T       t1035   o2 b1035
2665  G       s1035   t981  B       b1036   t1035
2666  B       b1036   s1035  T       t1036   o612 b1021 b4 b1036
 T       t1036   o635 b1036 b713  
2667  B       b1037   t1036  B       b1037   t1036
2668  B       b1038   t1033  T       t1037   o2 b1037
2669  T       t1038   o563 b1032 b1038  B       b1038   t1037
2670  H       h1038   w_1 t1038  T       t1038   o612 b1019 b4 b1038
2671  S       s1038   t626 h h715 h716 h717 h718 h719 h720 h1038 h1033  B       b1039   t1038
2672  G       s1038   t981  T       t1039   o2 b1039
 B       b1039   s1038  
 T       t1039   o635 b1039 b713  
2673  B       b1040   t1039  B       b1040   t1039
2674  S       s1040   t626 h h715 h716 h717 h718 h719 h720 h1038  T       t1040   o612 b1016 b4 b1040
2675  G       s1040   t981  B       b1041   t1040
2676  B       b1041   s1040  T       t1041   o2 b1041
 T       t1041   o635 b1041 b713  
2677  B       b1042   t1041  B       b1042   t1041
2678  T       t1042   o570 b549 b942 b567  T       t1042   o612 b1014 b4 b1042
2679  B       b1043   t1042  B       b1043   t1042
2680  T       t1043   o570 b550 b942 b567  T       t1043   o2 b1043
2681  B       b1044   t1043  B       b1044   t1043
2682  T       t1044   o568 b559 b569 b1043 b1044  T       t1044   o612 b1010 b4 b1044
2683  B       b1045   t1044  B       b1045   t1044
2684  T       t1045   o563 b568 b1045  T       t1045   o b1045 b4
2685  B       b1046   t1045  B       b1046   t1045
2686  T       t1046   o563 b1032 b1046  T       t1046   o611 b997 b1046
2687  B       b1047   t1046 b  B       b1047   t1046
2688  T       t1047   o561 b562 b1047  P       p1047   String "equivSubstT << equiv{car{'s}; eqG{'s}; op{'g; id{'s}; id{'s}}; op{'s; id{'s}; id{'s}}} >> 0 ttca thenT equivSymT ttca thenT rwh unfold_equiv 12 ttca"
2689  H       h1047   w t1047  O       o1047   ext_rule p1047
2690  S       s1047   t626 h h715 h716 h717 h718 h719 h720 h1047 h1038  T       t1047   o611 b1045 b4
2691  G       s1047   t981  B       b1048   t1047
2692  B       b1048   s1047  T       t1048   o1047 b610 b1048 b4 b4
 T       t1048   o635 b1048 b713  
2693  B       b1049   t1048  B       b1049   t1048
2694  S       s1049   t626 h h715 h716 h717 h718 h719 h720 h1047  T       t1049   o b1049 b4
2695  G       s1049   t981  B       b1050   t1049
2696  B       b1050   s1049  T       t1050   o1007 b610 b1047 b1050 b4
 T       t1050   o635 b1050 b713  
2697  B       b1051   t1050  B       b1051   t1050
2698  T       t1051   o771 b983 b1003 b1017  P       p1051   String "dT 12 ttca"
2699    O       o1051   ext_rule p1051
2700    T       t1051   o611 b1004 b4
2701  B       b1052   t1051  B       b1052   t1051
2702  T       t1052   o2 b1052  T       t1052   o1051 b610 b1052 b4 b4
2703  B       b1053   t1052  B       b1053   t1052
2704  T       t1053   o634 b1051 b1003 b1053  T       t1053   o b1053 b4
2705  B       b1054   t1053  B       b1054   t1053
2706  T       t1054   o2 b1054  T       t1054   o b1051 b1054
2707  B       b1055   t1054  B       b1055   t1054
2708  T       t1055   o634 b1049 b997 b1055  T       t1055   o959 b610 b1007 b1055 b4
2709  B       b1056   t1055  B       b1056   t1055
2710  T       t1056   o2 b1056  T       t1056   o b1056 b4
2711  B       b1057   t1056  B       b1057   t1056
2712  T       t1057   o634 b1042 b4 b1057  T       t1057   o693 b610 b959 b1057 b4
2713  B       b1058   t1057  B       b1058   t1057
2714  T       t1058   o2 b1058  T       t1058   o608 b1058
2715  B       b1059   t1058  B       b1059   t1058
2716  T       t1059   o634 b1040 b4 b1059  P       p1059   Number 2158
2717  B       b1060   t1059  P       p1060   Number 2166
2718  T       t1060   o2 b1060  O       o1060   resource_defs p1059 p1060 p300
2719  B       b1061   t1060  P       p1061   Number 2164
2720  T       t1061   o634 b1037 b4 b1061  O       o1061   uid p1061 p1060
2721  B       b1062   t1061  T       t1061   o1061 b623
2722  T       t1062   o2 b1062  B       b1061   t1061
2723  B       b1063   t1062  T       t1062   o b1061 b4
2724  T       t1063   o634 b1035 b4 b1063  B       b1062   t1062
2725  B       b1064   t1063  T       t1063   o1060 b1062
2726  T       t1064   o2 b1064  B       b1063   t1063
2727  B       b1065   t1064  T       t1064   o b1063 b4
2728  T       t1065   o634 b1031 b4 b1065  B       b1064   t1064
2729  B       b1066   t1065  T       t1065   o900 b594 b907 b1059 b1064
2730  T       t1066   o b1066 b4  B       b1065   t1065
2731  B       b1067   t1066  T       t1066   o591 b1065
2732  T       t1067   o633 b1018 b1067  B       b1066   t1066
2733  B       b1068   t1067  P       p1066   String subgroup_inv
2734  P       p1068   String "equivSubstT << equiv{car{'s}; eqG{'s}; op{'g; id{'s}; id{'s}}; op{'s; id{'s}; id{'s}}} >> 0 ttca thenT equivSymT ttca thenT rwh unfold_equiv 8 ttca"  O       o1066   rule p1066
2735  O       o1068   ext_rule p1068  T       t1067   o702 b637
2736  T       t1068   o633 b1066 b4  S       s1067   t597 h
2737  B       b1069   t1068  G       s1067   t1067
2738  T       t1069   o1068 b632 b1069 b4 b4  B       b1067   s1067
2739    T       t1068   o595 b1067
2740    B       b1068   t1068
2741    S       s1068   t604 h
2742    G       s1068   t638
2743    B       b1069   s1068
2744    T       t1069   o595 b1069
2745  B       b1070   t1069  B       b1070   t1069
2746  T       t1070   o b1070 b4  NCzf_itt_group!inv      inv     inv Czf_itt_group
2747    O       o1070   inv
2748    T       t1070   o1070 b555 b637
2749  B       b1071   t1070  B       b1071   t1070
2750  T       t1071   o1028 b632 b1068 b1071 b4  T       t1071   o1070 b556 b637
2751  B       b1072   t1071  B       b1072   t1071
2752  P       p1072   String "dT 8 ttca"  T       t1072   o640 b566 b649 b1071 b1072
2753  O       o1072   ext_rule p1072  S       s1072   t604 h
2754  T       t1072   o633 b1025 b4  G       s1072   t1072
2755  B       b1073   t1072  B       b1073   s1072
2756  T       t1073   o1072 b632 b1073 b4 b4  T       t1073   o595 b1073
2757  B       b1074   t1073  B       b1074   t1073
2758  T       t1074   o b1074 b4  T       t1074   o594 b660 b1074
2759  B       b1075   t1074  B       b1075   t1074
2760  T       t1075   o b1072 b1075  T       t1075   o594 b1070 b1075
2761  B       b1076   t1075  B       b1076   t1075
2762  T       t1076   o980 b632 b1028 b1076 b4  T       t1076   o594 b1068 b1076
2763  B       b1077   t1076  B       b1077   t1076
2764  T       t1077   o b1077 b4  T       t1077   o594 b602 b1077
2765  B       b1078   t1077  B       b1078   t1077
2766  T       t1078   o710 b632 b980 b1078 b4  T       t1078   o594 b600 b1078
2767  B       b1079   t1078  B       b1079   t1078
2768  T       t1079   o630 b1079  P       p1079   String "assumT 5 thenT rwh unfold_subgroup 2 thenT rwh unfold_group_bvd 2 thenT autoT"
2769    O       o1079   ext_rule p1079
2770    T       t1079   o b1069 b694
2771  B       b1080   t1079  B       b1080   t1079
2772  P       p1080   Number 2441  T       t1080   o b1067 b1080
2773  P       p1081   Number 2449  B       b1081   t1080
2774  O       o1081   resource_defs p1080 p1081 p300  T       t1081   o b601 b1081
2775  P       p1082   Number 2447  B       b1082   t1081
2776  O       o1082   uid p1082 p1081  T       t1082   o b599 b1082
2777  T       t1082   o1082 b645  B       b1083   t1082
2778  B       b1082   t1082  T       t1083   o613 b1073 b1083
2779  T       t1083   o b1082 b4  B       b1084   t1083
2780  B       b1083   t1083  T       t1084   o612 b1084 b4 b616
2781  T       t1084   o1081 b1083  B       b1085   t1084
2782  B       b1084   t1084  T       t1085   o636 b637 b566
2783  T       t1085   o b1084 b4  S       s1085   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720
2784  B       b1085   t1085  G       s1085   t1085
2785  T       t1086   o941 b616 b948 b1080 b1085  B       b1086   s1085
2786  B       b1086   t1086  T       t1086   o613 b1086 b1083
2787  T       t1087   o940 b1086  B       b1087   t1086
2788  B       b1087   t1087  S       s1087   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720
2789  P       p1087   Number 2668  G       s1087   t1072
2790  P       p1088   Number 3024  B       b1088   s1087
2791  O       o1088   location p1087 p1088  T       t1088   o613 b1088 b1083
2792  P       p1089   String subgroup_inv  B       b1089   t1088
2793  O       o1089   rule p1089  S       s1089   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h731
2794  T       t1089   o781 b565  G       s1089   t1072
2795  S       s1089   t619 h  B       b1090   s1089
2796  G       s1089   t1089  T       t1090   o613 b1090 b1083
2797  B       b1089   s1089  B       b1091   t1090
2798  T       t1090   o617 b1089  S       s1091   t604 h h698 h699 h700 h701 h702 h703 h704 h735
2799  B       b1090   t1090  G       s1091   t1072
2800  S       s1090   t626 h  B       b1092   s1091
2801  G       s1090   t566  T       t1092   o613 b1092 b1083
 B       b1091   s1090  
 T       t1091   o617 b1091  
 B       b1092   t1091  
 NCzf_itt_group!inv      inv     inv Czf_itt_group  
 O       o1092   inv  
 T       t1092   o1092 b549 b565  
2802  B       b1093   t1092  B       b1093   t1092
2803  T       t1093   o1092 b550 b565  S       s1093   t604 h h698 h699 h700 h701 h702 h703 h739
2804  B       b1094   t1093  G       s1093   t1072
2805  T       t1094   o568 b560 b578 b1093 b1094  B       b1094   s1093
2806  S       s1094   t626 h  T       t1094   o613 b1094 b1083
2807  G       s1094   t1094  B       b1095   t1094
2808  B       b1095   s1094  S       s1095   t604 h h698 h699 h700 h701 h702 h743
2809  T       t1095   o617 b1095  G       s1095   t1072
2810  B       b1096   t1095  B       b1096   s1095
2811  T       t1096   o616 b676 b1096  T       t1096   o613 b1096 b1083
2812  B       b1097   t1096  B       b1097   t1096
2813  T       t1097   o616 b1092 b1097  S       s1097   t604 h h698 h699 h700 h701 h746
2814  B       b1098   t1097  G       s1097   t1072
2815  T       t1098   o616 b1090 b1098  B       b1098   s1097
2816    T       t1098   o613 b1098 b1083
2817  B       b1099   t1098  B       b1099   t1098
2818  T       t1099   o616 b624 b1099  S       s1099   t604 h h698 h699 h700 h749
2819  B       b1100   t1099  G       s1099   t1072
2820  T       t1100   o616 b622 b1100  B       b1100   s1099
2821    T       t1100   o613 b1100 b1083
2822  B       b1101   t1100  B       b1101   t1100
2823  P       p1101   String "assumT 5 thenT rwh unfold_subgroup 2 thenT autoT"  S       s1101   t604 h h698 h699 h752
2824  O       o1101   ext_rule p1101  G       s1101   t1072
2825  T       t1101   o b1091 b711  B       b1102   s1101
2826  B       b1102   t1101  T       t1102   o613 b1102 b1083
 T       t1102   o b1089 b1102  
2827  B       b1103   t1102  B       b1103   t1102
2828  T       t1103   o b623 b1103  S       s1103   t604 h h698 h755
2829  B       b1104   t1103  G       s1103   t1072
2830  T       t1104   o b621 b1104  B       b1104   s1103
2831    T       t1104   o613 b1104 b1083
2832  B       b1105   t1104  B       b1105   t1104
2833  T       t1105   o635 b1095 b1105  S       s1105   t604 h h758
2834  B       b1106   t1105  G       s1105   t1072
2835  T       t1106   o634 b1106 b4 b638  B       b1106   s1105
2836    T       t1106   o613 b1106 b1083
2837  B       b1107   t1106  B       b1107   t1106
2838  T       t1107   o564 b565 b560  S       s1107   t604 h h760
2839  S       s1107   t626 h h715 h716 h717 h718 h719 h720  G       s1107   t1072
 G       s1107   t1107  
2840  B       b1108   s1107  B       b1108   s1107
2841  T       t1108   o635 b1108 b1105  T       t1108   o613 b1108 b1083
2842  B       b1109   t1108  B       b1109   t1108
2843  S       s1109   t626 h h715 h716 h717 h718 h719 h720  S       s1109   t604 h h762
2844  G       s1109   t1094  G       s1109   t1072
2845  B       b1110   s1109  B       b1110   s1109
2846  T       t1110   o635 b1110 b1105  T       t1110   o613 b1110 b1083
2847  B       b1111   t1110  B       b1111   t1110
2848  S       s1111   t626 h h715 h716 h717 h718 h729  T       t1111   o2 b1085
2849  G       s1111   t1094  B       b1112   t1111
2850  B       b1112   s1111  T       t1112   o612 b1111 b4 b1112
 T       t1112   o635 b1112 b1105  
2851  B       b1113   t1112  B       b1113   t1112
2852  S       s1113   t626 h h715 h716 h717 h731  T       t1113   o2 b1113
2853  G       s1113   t1094  B       b1114   t1113
2854  B       b1114   s1113  T       t1114   o612 b1109 b4 b1114
 T       t1114   o635 b1114 b1105  
2855  B       b1115   t1114  B       b1115   t1114
2856  S       s1115   t626 h h715 h716 h733  T       t1115   o2 b1115
2857  G       s1115   t1094  B       b1116   t1115
2858  B       b1116   s1115  T       t1116   o612 b1107 b4 b1116
 T       t1116   o635 b1116 b1105  
2859  B       b1117   t1116  B       b1117   t1116
2860  S       s1117   t626 h h715 h735  T       t1117   o2 b1117
2861  G       s1117   t1094  B       b1118   t1117
2862  B       b1118   s1117  T       t1118   o612 b1105 b4 b1118
 T       t1118   o635 b1118 b1105  
2863  B       b1119   t1118  B       b1119   t1118
2864  S       s1119   t626 h h737  T       t1119   o2 b1119
2865  G       s1119   t1094  B       b1120   t1119
2866  B       b1120   s1119  T       t1120   o612 b1103 b4 b1120
 T       t1120   o635 b1120 b1105  
2867  B       b1121   t1120  B       b1121   t1120
2868  S       s1121   t626 h h739  T       t1121   o2 b1121
2869  G       s1121   t1094  B       b1122   t1121
2870  B       b1122   s1121  T       t1122   o612 b1101 b4 b1122
 T       t1122   o635 b1122 b1105  
2871  B       b1123   t1122  B       b1123   t1122
2872  T       t1123   o2 b1107  T       t1123   o2 b1123
2873  B       b1124   t1123  B       b1124   t1123
2874  T       t1124   o634 b1123 b4 b1124  T       t1124   o612 b1099 b4 b1124
2875  B       b1125   t1124  B       b1125   t1124
2876  T       t1125   o2 b1125  T       t1125   o2 b1125
2877  B       b1126   t1125  B       b1126   t1125
2878  T       t1126   o634 b1121 b4 b1126  T       t1126   o612 b1097 b4 b1126
2879  B       b1127   t1126  B       b1127   t1126
2880  T       t1127   o2 b1127  T       t1127   o2 b1127
2881  B       b1128   t1127  B       b1128   t1127
2882  T       t1128   o634 b1119 b4 b1128  T       t1128   o612 b1095 b4 b1128
2883  B       b1129   t1128  B       b1129   t1128
2884  T       t1129   o2 b1129  T       t1129   o2 b1129
2885  B       b1130   t1129  B       b1130   t1129
2886  T       t1130   o634 b1117 b4 b1130  T       t1130   o612 b1093 b4 b1130
2887  B       b1131   t1130  B       b1131   t1130
2888  T       t1131   o2 b1131  T       t1131   o2 b1131
2889  B       b1132   t1131  B       b1132   t1131
2890  T       t1132   o634 b1115 b4 b1132  T       t1132   o612 b1091 b4 b1132
2891  B       b1133   t1132  B       b1133   t1132
2892  T       t1133   o2 b1133  T       t1133   o2 b1133
2893  B       b1134   t1133  B       b1134   t1133
2894  T       t1134   o634 b1113 b4 b1134  T       t1134   o612 b1089 b729 b1134
2895  B       b1135   t1134  B       b1135   t1134
2896  T       t1135   o2 b1135  T       t1135   o2 b1135
2897  B       b1136   t1135  B       b1136   t1135
2898  T       t1136   o634 b1111 b729 b1136  T       t1136   o612 b1087 b4 b1136
2899  B       b1137   t1136  B       b1137   t1136
2900  T       t1137   o2 b1137  T       t1137   o636 b1071 b566
2901  B       b1138   t1137  S       s1137   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720
2902  T       t1138   o634 b1109 b4 b1138  G       s1137   t1137
2903    B       b1138   s1137
2904    T       t1138   o613 b1138 b1083
2905  B       b1139   t1138  B       b1139   t1138
2906  T       t1139   o564 b1093 b560  T       t1139   o612 b1139 b4 b1136
2907  S       s1139   t626 h h715 h716 h717 h718 h719 h720  B       b1140   t1139
2908  G       s1139   t1139  T       t1140   o642 b556 b637 b1071
 B       b1140   s1139  
 T       t1140   o635 b1140 b1105  
2909  B       b1141   t1140  B       b1141   t1140
2910  T       t1141   o634 b1141 b4 b1138  T       t1141   o640 b566 b649 b1141 b902
2911  B       b1142   t1141  S       s1141   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720
2912  T       t1142   o570 b550 b565 b1093  G       s1141   t1141
2913    B       b1142   s1141
2914    T       t1142   o613 b1142 b1083
2915  B       b1143   t1142  B       b1143   t1142
2916  T       t1143   o568 b560 b578 b1143 b943  T       t1143   o612 b1143 b4 b1136
2917  S       s1143   t626 h h715 h716 h717 h718 h719 h720  B       b1144   t1143
2918  G       s1143   t1143  T       t1144   o b1144 b4
 B       b1144   s1143  
 T       t1144   o635 b1144 b1105  
2919  B       b1145   t1144  B       b1145   t1144
2920  T       t1145   o634 b1145 b4 b1138  T       t1145   o b1140 b1145
2921  B       b1146   t1145  B       b1146   t1145
2922  T       t1146   o b1146 b4  T       t1146   o b1137 b1146
2923  B       b1147   t1146  B       b1147   t1146
2924  T       t1147   o b1142 b1147  T       t1147   o611 b1085 b1147
2925  B       b1148   t1147  B       b1148   t1147
2926  T       t1148   o b1139 b1148  P       p1148   String "withT << 'a >> (dT 4) ttca"
2927    O       o1148   ext_rule p1148
2928    T       t1148   o611 b1137 b4
2929  B       b1149   t1148  B       b1149   t1148
2930  T       t1149   o633 b1107 b1149  T       t1149   o1148 b610 b1149 b4 b4
2931  B       b1150   t1149  B       b1150   t1149
2932  P       p1150   String "withT << 'a >> (dT 4) ttca"  P       p1150   String "withT << inv{'s; 'a} >> (dT 4) ttca"
2933  O       o1150   ext_rule p1150  O       o1150   ext_rule p1150
2934  T       t1150   o633 b1139 b4  T       t1150   o611 b1140 b4
2935  B       b1151   t1150  B       b1151   t1150
2936  T       t1151   o1150 b632 b1151 b4 b4  T       t1151   o1150 b610 b1151 b4 b4
2937  B       b1152   t1151  B       b1152   t1151
2938  P       p1152   String "withT << inv{'s; 'a} >> (dT 4) ttca"  P       p1152   String "instHypT [<< op{'s; 'a; inv{'s; 'a}} >>; << id{'s} >>] 10 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 12 ttca"
2939  O       o1152   ext_rule p1152  O       o1152   ext_rule p1152
2940  T       t1152   o633 b1142 b4  T       t1152   o642 b555 b637 b1071
2941  B       b1153   t1152  B       b1153   t1152
2942  T       t1153   o1152 b632 b1153 b4 b4  T       t1153   o640 b566 b649 b1153 b901
2943  B       b1154   t1153  H       h1153   y_9 t1153
2944  P       p1154   String "instHypT [<< op{'s; 'a; inv{'s; 'a}} >>; << id{'s} >>] 6 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca"  S       s1153   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153
2945  O       o1154   ext_rule p1154  G       s1153   t1141
2946  T       t1154   o570 b549 b565 b1093  B       b1154   s1153
2947    T       t1154   o613 b1154 b1083
2948  B       b1155   t1154  B       b1155   t1154
2949  T       t1155   o568 b560 b578 b1155 b942  T       t1155   o640 b565 b641 b1153 b901
2950  H       h1155   y_5 t1155  B       b1156   t1155
2951  S       s1155   t626 h h715 h716 h717 h718 h719 h720 h1155  B       b1157   t1153
2952  G       s1155   t1143  T       t1157   o705 b1156 b1157
2953  B       b1156   s1155  H       h1157   w_1 t1157
2954  T       t1156   o635 b1156 b1105  S       s1157   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1157 h1153
2955  B       b1157   t1156  G       s1157   t1141
2956  T       t1157   o568 b559 b569 b1155 b942  B       b1158   s1157
2957  B       b1158   t1157  T       t1158   o613 b1158 b1083
2958  B       b1159   t1155  B       b1159   t1158
2959  T       t1159   o563 b1158 b1159  S       s1159   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1157
2960  H       h1159   w_1 t1159  G       s1159   t1141
 S       s1159   t626 h h715 h716 h717 h718 h719 h720 h1159 h1155  
 G       s1159   t1143  
2961  B       b1160   s1159  B       b1160   s1159
2962  T       t1160   o635 b1160 b1105  T       t1160   o613 b1160 b1083
2963  B       b1161   t1160  B       b1161   t1160
2964  S       s1161   t626 h h715 h716 h717 h718 h719 h720 h1159  T       t1161   o640 b565 b641 b1153 b639
2965  G       s1161   t1143  B       b1162   t1161
2966  B       b1162   s1161  T       t1162   o640 b566 b649 b1153 b639
 T       t1162   o635 b1162 b1105  
2967  B       b1163   t1162  B       b1163   t1162
2968  T       t1163   o568 b559 b569 b1155 b567  T       t1163   o705 b1162 b1163
2969  B       b1164   t1163  B       b1164   t1163 b
2970  T       t1164   o568 b560 b578 b1155 b567  T       t1164   o704 b704 b1164
2971  B       b1165   t1164  H       h1164   w t1164
2972  T       t1165   o563 b1164 b1165  S       s1164   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1164 h1157
2973  B       b1166   t1165 b  G       s1164   t1141
2974  T       t1166   o561 b562 b1166  B       b1165   s1164
2975  H       h1166   w t1166  T       t1165   o613 b1165 b1083
2976  S       s1166   t626 h h715 h716 h717 h718 h719 h720 h1166 h1159  B       b1166   t1165
2977  G       s1166   t1143  S       s1166   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1164
2978    G       s1166   t1141
2979  B       b1167   s1166  B       b1167   s1166
2980  T       t1167   o635 b1167 b1105  T       t1167   o613 b1167 b1083
2981  B       b1168   t1167  B       b1168   t1167
2982  S       s1168   t626 h h715 h716 h717 h718 h719 h720 h1166  T       t1168   o b1153 b4
2983  G       s1168   t1143  B       b1169   t1168
2984  B       b1169   s1168  T       t1169   o818 b1169
 T       t1169   o635 b1169 b1105  
2985  B       b1170   t1169  B       b1170   t1169
2986  T       t1170   o b1155 b4  T       t1170   o817 b1170
2987  B       b1171   t1170  B       b1171   t1170
2988  T       t1171   o887 b1171  T       t1171   o b1171 b976
2989  B       b1172   t1171  B       b1172   t1171
2990  T       t1172   o886 b1172  T       t1172   o612 b1143 b1172 b1136
2991  B       b1173   t1172  B       b1173   t1172
2992  T       t1173   o b1173 b997  T       t1173   o2 b1173
2993  B       b1174   t1173  B       b1174   t1173
2994  T       t1174   o634 b1145 b1174 b1138  T       t1174   o612 b1168 b982 b1174
2995  B       b1175   t1174  B       b1175   t1174
2996  T       t1175   o2 b1175  T       t1175   o2 b1175
2997  B       b1176   t1175  B       b1176   t1175
2998  T       t1176   o634 b1170 b1003 b1176  T       t1176   o612 b1166 b976 b1176
2999  B       b1177   t1176  B       b1177   t1176
3000  T       t1177   o2 b1177  T       t1177   o2 b1177
3001  B       b1178   t1177  B       b1178   t1177
3002  T       t1178   o634 b1168 b997 b1178  T       t1178   o612 b1161 b4 b1178
3003  B       b1179   t1178  B       b1179   t1178
3004  T       t1179   o2 b1179  T       t1179   o2 b1179
3005  B       b1180   t1179  B       b1180   t1179
3006  T       t1180   o634 b1163 b4 b1180  T       t1180   o612 b1159 b4 b1180
3007  B       b1181   t1180  B       b1181   t1180
3008  T       t1181   o2 b1181  T       t1181   o2 b1181
3009  B       b1182   t1181  B       b1182   t1181
3010  T       t1182   o634 b1161 b4 b1182  T       t1182   o612 b1155 b4 b1182
3011  B       b1183   t1182  B       b1183   t1182
3012  T       t1183   o2 b1183  T       t1183   o b1183 b4
3013  B       b1184   t1183  B       b1184   t1183
3014  T       t1184   o634 b1157 b4 b1184  T       t1184   o611 b1144 b1184
3015  B       b1185   t1184  B       b1185   t1184
3016  T       t1185   o b1185 b4  P       p1185   String "instHypT [<< 'a >>; << inv{'s; 'a} >>] 9 thenT rwh fold_isset 0 thenT autoT thenT dT 13 ttca thenT dT 13 ttca"
3017  B       b1186   t1185  O       o1185   ext_rule p1185
3018  T       t1186   o633 b1146 b1186  T       t1185   o640 b565 b641 b1153 b1141
3019    H       h1185   y_11 t1185
3020    S       s1185   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185
3021    G       s1185   t1141
3022    B       b1186   s1185
3023    T       t1186   o613 b1186 b1083
3024  B       b1187   t1186  B       b1187   t1186
3025  P       p1187   String "instHypT [<< 'a >>; << inv{'s; 'a} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 9 ttca thenT dT 9 ttca"  T       t1187   o636 b1071 b565
3026  O       o1187   ext_rule p1187  B       b1188   t1187
3027  T       t1187   o568 b559 b569 b1155 b1143  B       b1189   t1185
3028  H       h1187   y_7 t1187  T       t1189   o705 b1188 b1189
3029  S       s1187   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187  H       h1189   y_10 t1189
3030  G       s1187   t1143  S       s1189   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1189 h1185
3031  B       b1188   s1187  G       s1189   t1141
3032  T       t1188   o635 b1188 b1105  B       b1190   s1189
3033  B       b1189   t1188  T       t1190   o613 b1190 b1083
3034  T       t1189   o564 b1093 b559  B       b1191   t1190
3035  B       b1190   t1189  S       s1191   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1189
3036  B       b1191   t1187  G       s1191   t1141
 T       t1191   o563 b1190 b1191  
 H       h1191   y_6 t1191  
 S       s1191   t626 h h715 h716 h717 h718 h719 h720 h1155 h1191 h1187  
 G       s1191   t1143  
3037  B       b1192   s1191  B       b1192   s1191
3038  T       t1192   o635 b1192 b1105  T       t1192   o613 b1192 b1083
3039  B       b1193   t1192  B       b1193   t1192
3040  S       s1193   t626 h h715 h716 h717 h718 h719 h720 h1155 h1191  B       b1194   t1189
3041  G       s1193   t1143  T       t1194   o705 b705 b1194
3042  B       b1194   s1193  H       h1194   w_1 t1194
3043  T       t1194   o635 b1194 b1105  S       s1194   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1194 h1189
3044  B       b1195   t1194  G       s1194   t1141
3045  B       b1196   t1191  B       b1195   s1194
3046  T       t1196   o563 b566 b1196  T       t1195   o613 b1195 b1083
3047  H       h1196   w_1 t1196  B       b1196   t1195
3048  S       s1196   t626 h h715 h716 h717 h718 h719 h720 h1155 h1196 h1191  S       s1196   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1194
3049  G       s1196   t1143  G       s1196   t1141
3050  B       b1197   s1196  B       b1197   s1196
3051  T       t1197   o635 b1197 b1105  T       t1197   o613 b1197 b1083
3052  B       b1198   t1197  B       b1198   t1197
3053  S       s1198   t626 h h715 h716 h717 h718 h719 h720 h1155 h1196  H       h1198   w t709
3054  G       s1198   t1143  S       s1198   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1198 h1194
3055    G       s1198   t1141
3056  B       b1199   s1198  B       b1199   s1198
3057  T       t1199   o635 b1199 b1105  T       t1199   o613 b1199 b1083
3058  B       b1200   t1199  B       b1200   t1199
3059  H       h1200   w t575  S       s1200   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1198
3060  S       s1200   t626 h h715 h716 h717 h718 h719 h720 h1155 h1200 h1196  G       s1200   t1141
 G       s1200   t1143  
3061  B       b1201   s1200  B       b1201   s1200
3062  T       t1201   o635 b1201 b1105  T       t1201   o613 b1201 b1083
3063  B       b1202   t1201  B       b1202   t1201
3064  S       s1202   t626 h h715 h716 h717 h718 h719 h720 h1155 h1200  T       t1202   o b1071 b4
3065  G       s1202   t1143  B       b1203   t1202
3066  B       b1203   s1202  T       t1203   o818 b1203
 T       t1203   o635 b1203 b1105  
3067  B       b1204   t1203  B       b1204   t1203
3068  T       t1204   o b1093 b4  T       t1204   o817 b1204
3069  B       b1205   t1204  B       b1205   t1204
3070  T       t1205   o887 b1205  T       t1205   o b1205 b976
3071  B       b1206   t1205  B       b1206   t1205
3072  T       t1206   o886 b1206  T       t1206   o b637 b4
3073  B       b1207   t1206  B       b1207   t1206
3074  T       t1207   o b1207 b997  T       t1207   o818 b1207
3075  B       b1208   t1207  B       b1208   t1207
3076  T       t1208   o b565 b4  T       t1208   o817 b1208
3077  B       b1209   t1208  B       b1209   t1208
3078  T       t1209   o887 b1209  T       t1209   o b1209 b976
3079  B       b1210   t1209  B       b1210   t1209
3080  T       t1210   o886 b1210  T       t1210   o612 b1155 b1210 b1182
3081  B       b1211   t1210  B       b1211   t1210
3082  T       t1211   o b1211 b997  T       t1211   o2 b1211
3083  B       b1212   t1211  B       b1212   t1211
3084  T       t1212   o634 b1157 b1212 b1184  T       t1212   o612 b1202 b1206 b1212
3085  B       b1213   t1212  B       b1213   t1212
3086  T       t1213   o2 b1213  T       t1213   o2 b1213
3087  B       b1214   t1213  B       b1214   t1213
3088  T       t1214   o634 b1204 b1208 b1214  T       t1214   o612 b1200 b976 b1214
3089  B       b1215   t1214  B       b1215   t1214
3090  T       t1215   o2 b1215  T       t1215   o2 b1215
3091  B       b1216   t1215  B       b1216   t1215
3092  T       t1216   o634 b1202 b997 b1216  T       t1216   o612 b1198 b4 b1216
3093  B       b1217   t1216  B       b1217   t1216
3094  T       t1217   o2 b1217  T       t1217   o2 b1217
3095  B       b1218   t1217  B       b1218   t1217
3096  T       t1218   o634 b1200 b4 b1218  T       t1218   o612 b1196 b4 b1218
3097  B       b1219   t1218  B       b1219   t1218
3098  T       t1219   o2 b1219  T       t1219   o2 b1219
3099  B       b1220   t1219  B       b1220   t1219
3100  T       t1220   o634 b1198 b4 b1220  T       t1220   o612 b1193 b4 b1220
3101  B       b1221   t1220  B       b1221   t1220
3102  T       t1221   o2 b1221  T       t1221   o2 b1221
3103  B       b1222   t1221  B       b1222   t1221
3104  T       t1222   o634 b1195 b4 b1222  T       t1222   o612 b1191 b4 b1222
3105  B       b1223   t1222  B       b1223   t1222
3106  T       t1223   o2 b1223  T       t1223   o2 b1223
3107  B       b1224   t1223  B       b1224   t1223
3108  T       t1224   o634 b1193 b4 b1224  T       t1224   o612 b1187 b4 b1224
3109  B       b1225   t1224  B       b1225   t1224
3110  T       t1225   o2 b1225  T       t1225   o b1225 b4
3111  B       b1226   t1225  B       b1226   t1225
3112  T       t1226   o634 b1189 b4 b1226  T       t1226   o611 b1183 b1226
3113  B       b1227   t1226  B       b1227   t1226
3114  T       t1227   o b1227 b4  P       p1227   String "equivSubstT << equiv{car{'s}; eqG{'s}; op{'s; 'a; inv{'s; 'a}}; op{'g; 'a; inv{'s; 'a}}} >> 12 thenT autoT"
3115  B       b1228   t1227  O       o1227   ext_rule p1227
3116  T       t1228   o633 b1185 b1228  T       t1227   o640 b566 b649 b1141 b901
3117    H       h1227   z_1 t1227
3118    S       s1227   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h1227
3119    G       s1227   t1141
3120    B       b1228   s1227
3121    T       t1228   o613 b1228 b1083
3122  B       b1229   t1228  B       b1229   t1228
3123  P       p1229   String "equivSubstT << equiv{car{'s}; eqG{'s}; op{'s; 'a; inv{'s; 'a}}; op{'g; 'a; inv{'s; 'a}}} >> 8 thenT autoT"  T       t1229   o2 b1225
3124  O       o1229   ext_rule p1229  B       b1230   t1229
3125  T       t1229   o568 b560 b578 b1143 b942  T       t1230   o612 b1229 b4 b1230
 H       h1229   z_1 t1229  
 S       s1229   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229  
 G       s1229   t1143  
 B       b1230   s1229  
 T       t1230   o635 b1230 b1105  
3126  B       b1231   t1230  B       b1231   t1230
 T       t1231   o2 b1227  
 B       b1232   t1231  
 T       t1232   o634 b1231 b4 b1232  
 B       b1233   t1232  
3127  NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv  NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv
3128  O       o1233   equiv_fun_prop  O       o1231   equiv_fun_prop
3129  P       p1233   Var z_1  P       p1231   Var z_1
3130  O       o1234   var p1233  O       o1232   var p1231
3131  T       t1234   o1234  T       t1232   o1232
3132  B       b1234   t1234  B       b1232   t1232
3133  T       t1235   o568 b560 b578 b1234 b942  T       t1233   o640 b566 b649 b1232 b901
3134  B       b1235   t1235 z_1  B       b1233   t1233 z_1
3135  T       t1236   o1233 b559 b569 b1235  T       t1234   o1231 b565 b641 b1233
3136  S       s1236   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187  S       s1234   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185
3137  G       s1236   t1236  G       s1234   t1234
3138  B       b1236   s1236  B       b1234   s1234
3139  T       t1237   o635 b1236 b1105  T       t1235   o613 b1234 b1083
3140    B       b1235   t1235
3141    T       t1236   o612 b1235 b4 b1230
3142    B       b1236   t1236
3143    T       t1237   o b1236 b4
3144  B       b1237   t1237  B       b1237   t1237
3145  T       t1238   o634 b1237 b4 b1232  T       t1238   o b1231 b1237
3146  B       b1238   t1238  B       b1238   t1238
3147  T       t1239   o b1238 b4  T       t1239   o611 b1225 b1238
3148  B       b1239   t1239  B       b1239   t1239
3149  T       t1240   o b1233 b1239  P       p1239   String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'s}; id{'g}} >> 14 thenT autoT"
3150  B       b1240   t1240  O       o1239   ext_rule p1239
3151  T       t1241   o633 b1227 b1240  S       s1239   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h1227
3152  B       b1241   t1241  G       s1239   t1085
3153  P       p1241   String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'s}; id{'g}} >> 10 thenT autoT"  B       b1240   s1239
3154  O       o1241   ext_rule p1241  T       t1240   o613 b1240 b1083
3155  S       s1241   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229  B       b1241   t1240
3156  G       s1241   t1107  T       t1241   o636 b1141 b566
3157    S       s1241   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h1227
3158    G       s1241   t1241
3159  B       b1242   s1241  B       b1242   s1241
3160  T       t1242   o635 b1242 b1105  T       t1242   o613 b1242 b1083
3161  B       b1243   t1242  B       b1243   t1242
3162  T       t1243   o564 b1143 b560  P       p1243   Var z_2
3163  S       s1243   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229  O       o1243   var p1243
3164  G       s1243   t1243  T       t1243   o1243
3165  B       b1244   s1243  B       b1244   t1243
3166  T       t1244   o635 b1244 b1105  T       t1244   o640 b566 b649 b1141 b1244
3167  B       b1245   t1244  B       b1245   t1244 z_2
3168  P       p1245   Var z_2  T       t1245   o1231 b566 b649 b1245
3169  O       o1245   var p1245  S       s1245   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h1227
3170  T       t1245   o1245  G       s1245   t1245
3171  B       b1246   t1245  B       b1246   s1245
3172  T       t1246   o568 b560 b578 b1143 b1246  T       t1246   o613 b1246 b1083
3173  B       b1247   t1246 z_2  B       b1247   t1246
3174  T       t1247   o1233 b560 b578 b1247  T       t1247   o2 b1231
3175  S       s1247   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229  B       b1248   t1247
3176  G       s1247   t1247  T       t1248   o612 b1247 b729 b1248
 B       b1248   s1247  
 T       t1248   o635 b1248 b1105  
3177  B       b1249   t1248  B       b1249   t1248
3178  T       t1249   o2 b1233  T       t1249   o2 b1249
3179  B       b1250   t1249  B       b1250   t1249
3180  T       t1250   o634 b1249 b729 b1250  T       t1250   o612 b1243 b729 b1250
3181  B       b1251   t1250  B       b1251   t1250
3182  T       t1251   o2 b1251  T       t1251   o2 b1251
3183  B       b1252   t1251  B       b1252   t1251
3184  T       t1252   o634 b1245 b729 b1252  T       t1252   o612 b1241 b4 b1252
3185  B       b1253   t1252  B       b1253   t1252
3186  T       t1253   o2 b1253  S       s1253   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h1227
3187  B       b1254   t1253  G       s1253   t1137
3188  T       t1254   o634 b1243 b4 b1254  B       b1254   s1253
3189    T       t1254   o613 b1254 b1083
3190  B       b1255   t1254  B       b1255   t1254
3191  S       s1255   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229  T       t1255   o612 b1255 b4 b1252
3192  G       s1255   t1139  B       b1256   t1255
3193  B       b1256   s1255  T       t1256   o b1256 b4
 T       t1256   o635 b1256 b1105  
3194  B       b1257   t1256  B       b1257   t1256
3195  T       t1257   o634 b1257 b4 b1254  T       t1257   o b1253 b1257
3196  B       b1258   t1257  B       b1258   t1257
3197  T       t1258   o b1258 b4  T       t1258   o611 b1231 b1258
3198  B       b1259   t1258  B       b1259   t1258
3199  T       t1259   o b1255 b1259  T       t1259   o611 b1253 b4
3200  B       b1260   t1259  B       b1260   t1259
3201  T       t1260   o633 b1233 b1260  T       t1260   o1148 b610 b1260 b4 b4
3202  B       b1261   t1260  B       b1261   t1260
3203  T       t1261   o633 b1255 b4  T       t1261   o611 b1256 b4
3204  B       b1262   t1261  B       b1262   t1261
3205  T       t1262   o1150 b632 b1262 b4 b4  T       t1262   o1150 b610 b1262 b4 b4
3206  B       b1263   t1262  B       b1263   t1262
3207  T       t1263   o633 b1258 b4  T       t1263   o b1263 b4
3208  B       b1264   t1263  B       b1264   t1263
3209  T       t1264   o1152 b632 b1264 b4 b4  T       t1264   o b1261 b1264
3210  B       b1265   t1264  B       b1265   t1264
3211  T       t1265   o b1265 b4  T       t1265   o1239 b610 b1259 b1265 b4
3212  B       b1266   t1265  B       b1266   t1265
3213  T       t1266   o b1263 b1266  P       p1266   String "rwh unfold_equiv_fun_prop 0 thenT autoT"
3214  B       b1267   t1266  O       o1266   ext_rule p1266
3215  T       t1267   o1241 b632 b1261 b1267 b4  T       t1266   o640 b565 b641
3216  B       b1268   t1267  H       h1266   x t1266
3217  P       p1268   String "rwh unfold_equiv_fun_prop 0 thenT autoT"  H       h1267   x_1 t711
3218  O       o1268   ext_rule p1268  T       t1267   o640 b566 b649 b637 b901
3219  T       t1268   o568 b559 b569  H       h1268   x_2 t1267
3220  H       h1268   x t1268  T       t1268   o640 b566 b649 b639 b901
3221  H       h1269   x_1 t577  S       s1268   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h635 h636 h1266 h1267 h1268
3222  T       t1269   o568 b560 b578 b565 b942  G       s1268   t1268
3223  H       h1270   x_2 t1269  B       b1268   s1268
3224  T       t1270   o568 b560 b578 b567 b942  T       t1269   o613 b1268 b1083
3225  S       s1270   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659 h1268 h1269 h1270  B       b1269   t1269
3226  G       s1270   t1270  B       b1270   t1267
3227  B       b1270   s1270  B       b1271   t1268
3228  T       t1271   o635 b1270 b1105  T       t1271   o705 b1270 b1271
3229  B       b1271   t1271  S       s1271   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h635 h636 h1266 h1267
3230  B       b1272   t1269  G       s1271   t1271
3231  B       b1273   t1270  B       b1272   s1271
3232  T       t1273   o563 b1272 b1273  T       t1272   o613 b1272 b1083
3233  S       s1273   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659 h1268 h1269  B       b1273   t1272
3234  G       s1273   t1273  B       b1274   t1271
3235  B       b1274   s1273  T       t1274   o705 b711 b1274
3236  T       t1274   o635 b1274 b1105  S       s1274   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h635 h636 h1266
3237  B       b1275   t1274  G       s1274   t1274
3238  B       b1276   t1273  B       b1275   s1274
3239  T       t1276   o563 b577 b1276  T       t1275   o613 b1275 b1083
3240  S       s1276   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659 h1268  B       b1276   t1275
3241  G       s1276   t1276  B       b1277   t1266
3242  B       b1277   s1276  B       b1278   t1274
3243  T       t1277   o635 b1277 b1105  T       t1278   o705 b1277 b1278
3244  B       b1278   t1277  S       s1278   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h635 h636
3245  B       b1279   t1268  G       s1278   t1278
3246  B       b1280   t1276  B       b1279   s1278
3247  T       t1280   o563 b1279 b1280  T       t1279   o613 b1279 b1083
3248  S       s1280   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659  B       b1280   t1279
3249  G       s1280   t1280  B       b1281   t1278 b
3250  B       b1281   s1280  T       t1281   o704 b704 b1281
3251  T       t1281   o635 b1281 b1105  S       s1281   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185 h635
3252  B       b1282   t1281  G       s1281   t1281
3253  B       b1283   t1280 b  B       b1282   s1281
3254  T       t1283   o561 b562 b1283  T       t1282   o613 b1282 b1083
3255  S       s1283   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658  B       b1283   t1282
3256  G       s1283   t1283  B       b1284   t1281 a
3257  B       b1284   s1283  T       t1284   o704 b704 b1284
3258  T       t1284   o635 b1284 b1105  S       s1284   t604 h h698 h699 h700 h701 h702 h703 h704 h710 h715 h720 h1153 h1185
3259  B       b1285   t1284  G       s1284   t1284
3260  B       b1286   t1283 a  B       b1285   s1284
3261  T       t1286   o561 b562 b1286  T       t1285   o613 b1285 b1083
3262  S       s1286   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187  B       b1286   t1285
3263  G       s1286   t1286  T       t1286   o2 b1236
3264  B       b1287   s1286  B       b1287   t1286
3265  T       t1287   o635 b1287 b1105  T       t1287   o612 b1286 b729 b1287
3266  B       b1288   t1287  B       b1288   t1287
3267  T       t1288   o2 b1238  T       t1288   o2 b1288
3268  B       b1289   t1288  B       b1289   t1288
3269  T       t1289   o634 b1288 b729 b1289  T       t1289   o612 b1283 b729 b1289
3270  B       b1290   t1289  B       b1290   t1289
3271  T       t1290   o2 b1290  T       t1290   o2 b1290
3272  B       b1291   t1290  B       b1291   t1290
3273  T       t1291   o634 b1285 b729 b1291  T       t1291   o612 b1280 b729 b1291
3274  B       b1292   t1291  B       b1292   t1291
3275  T       t1292   o2 b1292  T       t1292   o2 b1292
3276  B       b1293   t1292  B       b1293   t1292
3277  T       t1293   o634 b1282 b729 b1293  T       t1293   o612 b1276 b729 b1293
3278  B       b1294   t1293  B       b1294   t1293
3279  T       t1294   o2 b1294  T       t1294   o2 b1294
3280  B       b1295   t1294  B       b1295   t1294
3281  T       t1295   o634 b1278 b729 b1295  T       t1295   o612 b1273 b729 b1295
3282  B       b1296   t1295  B       b1296   t1295
3283  T       t1296   o2 b1296  T       t1296   o2 b1296
3284  B       b1297   t1296  B       b1297   t1296
3285  T       t1297   o634 b1275 b729 b1297  T       t1297   o612 b1269 b4 b1297
3286  B       b1298   t1297  B       b1298   t1297
3287  T       t1298   o2 b1298  T       t1298   o b1298 b4
3288  B       b1299   t1298  B       b1299   t1298
3289  T       t1299   o634 b1271 b4 b1299  T       t1299   o611 b1236 b1299
3290  B       b1300   t1299  B       b1300   t1299
3291  T       t1300   o b1300 b4  P       p1300   String "instHypT [<< 'a >>; << 'b >>] 10 ttca thenT dT 19 ttca thenT equivTransT << 'a >> thenT autoT thenT rwh unfold_equiv 18 thenT rwh unfold_equiv 19 ttca thenT equivSymT ttca"
3292    O       o1300   ext_rule p1300
3293    T       t1300   o611 b1298 b4
3294  B       b1301   t1300  B       b1301   t1300
3295  T       t1301   o633 b1238 b1301  T       t1301   o1300 b610 b1301 b4 b4
3296  B       b1302   t1301  B       b1302   t1301
3297  P       p1302   String "instHypT [<< 'a >>; << 'b >>] 6 ttca thenT dT 15 ttca thenT equivTransT << 'a >> thenT autoT thenT rwh unfold_equiv 14 thenT rwh unfold_equiv 15 ttca thenT equivSymT ttca"  T       t1302   o b1302 b4
 O       o1302   ext_rule p1302  
 T       t1302   o633 b1300 b4  
3298  B       b1303   t1302  B       b1303   t1302
3299  T       t1303   o1302 b632 b1303 b4 b4  T       t1303   o1266 b610 b1300 b1303 b4
3300  B       b1304   t1303  B       b1304   t1303
3301  T       t1304   o b1304 b4  T       t1304   o b1304 b4
3302  B       b1305   t1304  B       b1305   t1304
3303  T       t1305   o1268 b632 b1302 b1305 b4  T       t1305   o b1266 b1305
3304  B       b1306   t1305  B       b1306   t1305
3305  T       t1306   o b1306 b4  T       t1306   o1227 b610 b1239 b1306 b4
3306  B       b1307   t1306  B       b1307   t1306
3307  T       t1307   o b1268 b1307  T       t1307   o b1307 b4
3308  B       b1308   t1307  B       b1308   t1307
3309  T       t1308   o1229 b632 b1241 b1308 b4  T       t1308   o1185 b610 b1227 b1308 b4
3310  B       b1309   t1308  B       b1309   t1308
3311  T       t1309   o b1309 b4  T       t1309   o b1309 b4
3312  B       b1310   t1309  B       b1310   t1309
3313  T       t1310   o1187 b632 b1229 b1310 b4  T       t1310   o1152 b610 b1185 b1310 b4
3314  B       b1311   t1310  B       b1311   t1310
3315  T       t1311   o b1311 b4  T       t1311   o b1311 b4
3316  B       b1312   t1311  B       b1312   t1311
3317  T       t1312   o1154 b632 b1187 b1312 b4  T       t1312   o b1152 b1312
3318  B       b1313   t1312  B       b1313   t1312
3319  T       t1313   o b1313 b4  T       t1313   o b1150 b1313
3320  B       b1314   t1313  B       b1314   t1313
3321  T       t1314   o b1154 b1314  T       t1314   o1079 b610 b1148 b1314 b4
3322  B       b1315   t1314  B       b1315   t1314
3323  T       t1315   o b1152 b1315  T       t1315   o608 b1315
3324  B       b1316   t1315  B       b1316   t1315
3325  T       t1316   o1101 b632 b1150 b1316 b4  P       p1316   Number 2413
3326  B       b1317   t1316  P       p1317   Number 2421
3327  T       t1317   o630 b1317  O       o1317   resource_defs p1316 p1317 p300
3328  B       b1318   t1317  P       p1318   Number 2419
3329  P       p1318   Number 2696  O       o1318   uid p1318 p1317
3330  P       p1319   Number 2704  T       t1318   o1318 b623
3331  O       o1319   resource_defs p1318 p1319 p300  B       b1318   t1318
3332  P       p1320   Number 2702  T       t1319   o b1318 b4
3333  O       o1320   uid p1320 p1319  B       b1319   t1319
3334  T       t1320   o1320 b645  T       t1320   o1317 b1319
3335  B       b1320   t1320  B       b1320   t1320
3336  T       t1321   o b1320 b4  T       t1321   o b1320 b4
3337  B       b1321   t1321  B       b1321   t1321
3338  T       t1322   o1319 b1321  T       t1322   o1066 b594 b1079 b1316 b1321
3339  B       b1322   t1322  B       b1322   t1322
3340  T       t1323   o b1322 b4  T       t1323   o591 b1322
3341  B       b1323   t1323  B       b1323   t1323
3342  T       t1324   o1089 b616 b1101 b1318 b1323  P       p1323   String subgroup_isect
3343  B       b1324   t1324  O       o1323   rule p1323
 T       t1325   o1088 b1324  
 B       b1325   t1325  
 O       o1325   location p p  
 P       p1325   String subgroup_isect  
 O       o1326   rule p1325  
3344  NSummary!term_param     term_param      term_param Summary  NSummary!term_param     term_param      term_param Summary
3345  O       o1327   term_param  O       o1324   term_param
3346  P       p1327   Var h1  P       p1324   Var h1
3347  O       o1328   var p1327  O       o1325   var p1324
3348  T       t1328   o1328  T       t1325   o1325
3349    B       b1325   t1325
3350    T       t1326   o1324 b1325
3351    B       b1326   t1326
3352    P       p1326   Var h2
3353    O       o1326   var p1326
3354    T       t1327   o1326
3355    B       b1327   t1327
3356    T       t1328   o1324 b1327
3357  B       b1328   t1328  B       b1328   t1328
3358  T       t1329   o1327 b1328  T       t1329   o b1328 b4
3359  B       b1329   t1329  B       b1329   t1329
3360  P       p1329   Var h2  T       t1330   o b1326 b1329
 O       o1329   var p1329  
 T       t1330   o1329  
3361  B       b1330   t1330  B       b1330   t1330
3362  T       t1331   o1327 b1330  T       t1331   o b593 b1330
3363  B       b1331   t1331  B       b1331   t1331
3364  T       t1332   o b1331 b4  T       t1332   o597 b598 b1325 b1325
3365  B       b1332   t1332  S       s1332   t597 h
3366  T       t1333   o b1329 b1332  G       s1332   t1332
3367    B       b1332   s1332
3368    T       t1333   o595 b1332
3369  B       b1333   t1333  B       b1333   t1333
3370  T       t1334   o b615 b1333  T       t1334   o597 b598 b1327 b1327
3371  B       b1334   t1334  S       s1334   t597 h
3372  T       t1335   o619 b620 b1328 b1328  G       s1334   t1334
3373  S       s1335   t619 h  B       b1334   s1334
3374  G       s1335   t1335  T       t1335   o595 b1334
3375  B       b1335   s1335  B       b1335   t1335
3376  T       t1336   o617 b1335  P       p1335   Var h
3377    O       o1335   var p1335
3378    T       t1336   o1335
3379  B       b1336   t1336  B       b1336   t1336
3380  T       t1337   o619 b620 b1330 b1330  T       t1337   o597 b598 b1336 b1336
3381  S       s1337   t619 h  S       s1337   t597 h
3382  G       s1337   t1337  G       s1337   t1337
3383  B       b1337   s1337  B       b1337   s1337
3384  T       t1338   o617 b1337  T       t1338   o595 b1337
3385  B       b1338   t1338  B       b1338   t1338
3386  P       p1338   Var h  T       t1339   o554 b1325 b556
3387  O       o1338   var p1338  S       s1339   t604 h
3388  T       t1339   o1338  G       s1339   t1339
3389  B       b1339   t1339  B       b1339   s1339
3390  T       t1340   o619 b620 b1339 b1339  T       t1340   o595 b1339
3391  S       s1340   t619 h  B       b1340   t1340
3392  G       s1340   t1340  T       t1341   o554 b1327 b556
3393  B       b1340   s1340  S       s1341   t604 h
3394  T       t1341   o617 b1340  G       s1341   t1341
3395  B       b1341   t1341  B       b1341   s1341
3396  T       t1342   o557 b1339  T       t1342   o595 b1341
3397  S       s1342   t626 h  B       b1342   t1342
3398  G       s1342   t1342  NCzf_itt_isect  Czf_itt_isect   Czf_itt_isect NIL
3399  B       b1342   s1342  NCzf_itt_isect!isect    isect   isect Czf_itt_isect
3400  T       t1343   o617 b1342  O       o1342   isect
3401    T       t1343   o565 b1325
3402  B       b1343   t1343  B       b1343   t1343
3403  T       t1344   o548 b1328 b550  T       t1344   o565 b1327
3404  S       s1344   t626 h  B       b1344   t1344
3405  G       s1344   t1344  T       t1345   o1342 b1343 b1344
 B       b1344   s1344  
 T       t1345   o617 b1344  
3406  B       b1345   t1345  B       b1345   t1345
3407  T       t1346   o548 b1330 b550  T       t1346   o567 b1336 b1325 b1345
3408  S       s1346   t626 h  S       s1346   t604 h
3409  G       s1346   t1346  G       s1346   t1346
3410  B       b1346   s1346  B       b1346   s1346
3411  T       t1347   o617 b1346  T       t1347   o595 b1346
3412  B       b1347   t1347  B       b1347   t1347
3413  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  T       t1348   o554 b1336 b556
3414  NCzf_itt_eq!equal       equal1347       equal Czf_itt_eq  S       s1348   t604 h
3415  O       o1347   equal1347  G       s1348   t1348
3416  T       t1348   o559 b1339  B       b1348   s1348
3417  B       b1348   t1348  T       t1349   o595 b1348
 NCzf_itt_isect  Czf_itt_isect   Czf_itt_isect NIL  
 NCzf_itt_isect!isect    isect   isect Czf_itt_isect  
 O       o1348   isect  
 T       t1349   o559 b1328  
3418  B       b1349   t1349  B       b1349   t1349
3419  T       t1350   o559 b1330  T       t1350   o594 b1347 b1349
3420  B       b1350   t1350  B       b1350   t1350
3421  T       t1351   o1348 b1349 b1350  T       t1351   o594 b1342 b1350
3422  B       b1351   t1351  B       b1351   t1351
3423  T       t1352   o1347 b1348 b1351  T       t1352   o594 b1340 b1351
3424  S       s1352   t626 h  B       b1352   t1352
3425  G       s1352   t1352  T       t1353   o594 b1338 b1352
 B       b1352   s1352  
 T       t1353   o617 b1352  
3426  B       b1353   t1353  B       b1353   t1353
3427  T       t1354   o564 b565 b1348  T       t1354   o594 b1335 b1353
3428  H       h1354   x t1354  B       b1354   t1354
3429  T       t1355   o564 b567 b1348  T       t1355   o594 b1333 b1354
3430  H       h1355   y t1355  B       b1355   t1355
3431  T       t1356   o569 b1339  T       t1356   o594 b602 b1355
3432  B       b1356   t1356  B       b1356   t1356
3433  T       t1357   o570 b1339 b565 b567  P       p1356   String "assumT 5 thenT assumT 7 thenT rwh unfold_subgroup 2 thenT rwh unfold_group_bvd 2 thenT rwh unfold_group_bvd 3 thenT autoT"
3434    O       o1356   ext_rule p1356
3435    T       t1357   o b1346 b4
3436  B       b1357   t1357  B       b1357   t1357
3437  T       t1358   o570 b1328 b565 b567  T       t1358   o b1341 b1357
3438  B       b1358   t1358  B       b1358   t1358
3439  T       t1359   o568 b1348 b1356 b1357 b1358  T       t1359   o b1339 b1358
3440  S       s1359   t626 h h658 h659 h1354 h1355  B       b1359   t1359
3441  G       s1359   t1359  T       t1360   o b1337 b1359
 B       b1359   s1359  
 T       t1360   o617 b1359  
3442  B       b1360   t1360  B       b1360   t1360
3443  T       t1361   o568 b1348 b1356 b663 b664  T       t1361   o b1334 b1360
3444  H       h1361   u t1361  B       b1361   t1361
3445  T       t1362   o569 b1328  T       t1362   o b1332 b1361
3446  B       b1362   t1362  B       b1362   t1362
3447  T       t1363   o568 b1349 b1362 b663 b664  T       t1363   o b601 b1362
3448  S       s1363   t626 h h662 h663 h1361  B       b1363   t1363
3449  G       s1363   t1363  T       t1364   o613 b1348 b1363
 B       b1363   s1363  
 T       t1364   o617 b1363  
3450  B       b1364   t1364  B       b1364   t1364
3451  T       t1365   o564 b759 b1348  T       t1365   o612 b1364 b4 b616
3452  H       h1365   x1 t1365  B       b1365   t1365
3453  T       t1366   o564 b761 b1348  T       t1366   o563 b1325
3454  H       h1366   y1 t1366  H       h1366   y_6 t1366
3455  T       t1367   o568 b1349 b1362 b759 b761  H       h1367   y_7 t564
3456  H       h1367   v t1367  T       t1367   o564 b1343 b566
3457  T       t1368   o568 b1348 b1356 b759 b761  H       h1368   y_8 t1367
3458  S       s1368   t626 h h757 h758 h1365 h1366 h1367  H       h1369   y_9 t1366
3459  G       s1368   t1368  H       h1370   y_10 t564
3460  B       b1368   s1368  T       t1370   o702 b1343
3461  T       t1369   o617 b1368  H       h1371   y_11 t1370
3462  B       b1369   t1369  T       t1371   o703 b1343 b1343
3463  T       t1370   o548 b1339 b550  H       h1372   y_12 t1371
3464  S       s1370   t626 h  T       t1372   o636 b637 b1343
 G       s1370   t1370  
 B       b1370   s1370  
 T       t1371   o617 b1370  
 B       b1371   t1371  
 T       t1372   o616 b1369 b1371  
3465  B       b1372   t1372  B       b1372   t1372
3466  T       t1373   o616 b1364 b1372  T       t1373   o636 b639 b1343
3467  B       b1373   t1373  B       b1373   t1373
3468  T       t1374   o616 b1360 b1373  T       t1374   o641 b1325
3469  B       b1374   t1374  B       b1374   t1374
3470  T       t1375   o616 b1353 b1374  T       t1375   o642 b1325 b637 b639
3471  B       b1375   t1375  B       b1375   t1375
3472  T       t1376   o616 b1347 b1375  T       t1376   o640 b1343 b1374 b1375 b643
3473  B       b1376   t1376  B       b1376   t1376
3474  T       t1377   o616 b1345 b1376  T       t1377   o705 b1373 b1376
3475  B       b1377   t1377  B       b1377   t1377
3476  T       t1378   o616 b1343 b1377  T       t1378   o705 b1372 b1377
3477  B       b1378   t1378  B       b1378   t1378 b
3478  T       t1379   o616 b1341 b1378  T       t1379   o704 b704 b1378
3479  B       b1379   t1379  B       b1379   t1379 a
3480  T       t1380   o616 b1338 b1379  T       t1380   o704 b704 b1379
3481  B       b1380   t1380  H       h1380   y_13 t1380
3482  T       t1381   o616 b1336 b1380  T       t1381   o640 b1343 b1374 b637 b639
3483  B       b1381   t1381  B       b1381   t1381
3484  T       t1382   o616 b624 b1381  T       t1382   o705 b1381 b712
3485  B       b1382   t1382  B       b1382   t1382 b
3486  P       p1382   String "assumT 6 thenT assumT 8 thenT rwh unfold_subgroup 2 thenT autoT"  T       t1383   o704 b704 b1382
3487  O       o1382   ext_rule p1382  B       b1383   t1383 a
3488  T       t1383   o b1368 b4  T       t1384   o704 b704 b1383
3489  B       b1383   t1383  H       h1384   y_14 t1384
3490  T       t1384   o b1363 b1383  T       t1385   o705 b712 b1381
 B       b1384   t1384  
 T       t1385   o b1359 b1384  
3491  B       b1385   t1385  B       b1385   t1385
3492  T       t1386   o b1352 b1385  T       t1386   o705 b1373 b1385
3493  B       b1386   t1386  B       b1386   t1386
3494  T       t1387   o b1346 b1386  T       t1387   o705 b1372 b1386
3495  B       b1387   t1387  B       b1387   t1387 b
3496  T       t1388   o b1344 b1387  T       t1388   o704 b704 b1387
3497  B       b1388   t1388  B       b1388   t1388 a
3498  T       t1389   o b1342 b1388  T       t1389   o704 b704 b1388
3499  B       b1389   t1389  H       h1389   z t1389
3500  T       t1390   o b1340 b1389  T       t1390   o563 b1336
3501  B       b1390   t1390  H       h1390   y t1390
3502  T       t1391   o b1337 b1390  H       h1391   y_1 t1366
3503  B       b1391   t1391  T       t1391   o702 b1345
3504  T       t1392   o b1335 b1391  H       h1392   y_2 t1391
3505    T       t1392   o565 b1336
3506  B       b1392   t1392  B       b1392   t1392
3507  T       t1393   o b623 b1392  T       t1393   o703 b1392 b1345
3508  B       b1393   t1393  H       h1393   y_3 t1393
3509  T       t1394   o635 b1370 b1393  T       t1394   o636 b637 b1392
3510  B       b1394   t1394  B       b1394   t1394
3511  T       t1395   o634 b1394 b4 b638  T       t1395   o636 b639 b1392
3512  B       b1395   t1395  B       b1395   t1395
3513  T       t1396   o557 b1328  T       t1396   o641 b1336
3514  H       h1396   y t1396  B       b1396   t1396
3515  T       t1397   o558 b1349 b560  T       t1397   o642 b1336 b637 b639
3516  H       h1397   y_2 t1397  B       b1397   t1397
3517  T       t1398   o564 b565 b1349  T       t1398   o640 b1392 b1396 b1397 b1375
3518  B       b1398   t1398  B       b1398   t1398
3519  T       t1399   o564 b567 b1349  T       t1399   o705 b1395 b1398
3520  B       b1399   t1399  B       b1399   t1399
3521  T       t1400   o568 b1349 b1362 b1358 b571  T       t1400   o705 b1394 b1399
3522  B       b1400   t1400  B       b1400   t1400 b
3523  T       t1401   o563 b1399 b1400  T       t1401   o704 b704 b1400
3524  B       b1401   t1401  B       b1401   t1401 a
3525  T       t1402   o563 b1398 b1401  T       t1402   o704 b704 b1401
3526  B       b1402   t1402 b  H       h1402   y_4 t1402
3527  T       t1403   o561 b562 b1402  T       t1403   o640 b1392 b1396 b637 b639
3528  B       b1403   t1403 a  B       b1403   t1403
3529  T       t1404   o561 b562 b1403  T       t1404   o705 b1403 b1381
3530  H       h1404   y_3 t1404  B       b1404   t1404 b
3531  T       t1405   o568 b1349 b1362 b565 b567  T       t1405   o704 b704 b1404
3532  B       b1405   t1405  B       b1405   t1405 a
3533  T       t1406   o563 b1405 b579  T       t1406   o704 b704 b1405
3534  B       b1406   t1406 b  H       h1406   y_5 t1406
3535  T       t1407   o561 b562 b1406  T       t1407   o705 b1381 b1403
3536  B       b1407   t1407 a  B       b1407   t1407
3537  T       t1408   o561 b562 b1407  T       t1408   o705 b1395 b1407
3538  H       h1408   y_4 t1408  B       b1408   t1408
3539  T       t1409   o563 b579 b1405  T       t1409   o705 b1394 b1408
3540  B       b1409   t1409  B       b1409   t1409 b
3541  T       t1410   o563 b1399 b1409  T       t1410   o704 b704 b1409
3542  B       b1410   t1410  B       b1410   t1410 a
3543  T       t1411   o563 b1398 b1410  T       t1411   o704 b704 b1410
3544  B       b1411   t1411 b  H       h1411   z_1 t1411
3545  T       t1412   o561 b562 b1411  H       h1412   x t635
3546  B       b1412   t1412 a  P       p1412   Var x
3547  T       t1413   o561 b562 b1412  O       o1412   var p1412
3548  H       h1413   z t1413  T       t1412   o1412
3549  H       h1414   v_1 t1352  B       b1412   t1412
3550  H       h1415   x t562  T       t1413   o636 b1412 b1392
3551  P       p1415   Var x  H       h1413   y t1413
3552  O       o1415   var p1415  T       t1414   o636 b1412 b566
3553  T       t1415   o1415  S       s1414   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1384 h1389 h1390 h1391 h1392 h1393 h1402 h1406 h1411 h1412 h1413
3554    G       s1414   t1414
3555    B       b1414   s1414
3556    T       t1415   o613 b1414 b1363
3557  B       b1415   t1415  B       b1415   t1415
3558  T       t1416   o564 b1415 b1348  T       t1416   o564 b1392 b566
3559  H       h1416   y t1416  S       s1416   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1384 h1389 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3560  T       t1417   o564 b1415 b560  G       s1416   t1416
3561  S       s1417   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416  B       b1416   s1416
3562  G       s1417   t1417  T       t1417   o613 b1416 b1363
3563  B       b1417   s1417  B       b1417   t1417
3564  T       t1418   o635 b1417 b1393  S       s1417   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1384 h1389 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3565  B       b1418   t1418  G       s1417   t1348
3566  T       t1419   o558 b1348 b560  B       b1418   s1417
3567  S       s1419   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414  T       t1418   o613 b1418 b1363
3568  G       s1419   t1419  B       b1419   t1418
3569  B       b1419   s1419  B       b1420   t1384
3570  T       t1420   o635 b1419 b1393  B       b1421   t1389
3571  B       b1420   t1420  T       t1421   o562 b1420 b1421
3572  S       s1420   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414  H       h1421   z_2 t1421
3573  G       s1420   t1370  S       s1421   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1421 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3574  B       b1421   s1420  G       s1421   t1348
3575  T       t1421   o635 b1421 b1393  B       b1422   s1421
3576  B       b1422   t1421  T       t1422   o613 b1422 b1363
3577  B       b1423   t1408  B       b1423   t1422
3578  B       b1424   t1413  B       b1424   t1380
3579  T       t1424   o556 b1423 b1424  B       b1425   t1421
3580  H       h1424   z_1 t1424  T       t1425   o562 b1424 b1425
3581  S       s1424   t626 h h1396 h716 h1397 h1404 h1424 h1414  H       h1425   z t1425
3582  G       s1424   t1370  S       s1425   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1425 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3583  B       b1425   s1424  G       s1425   t1348
3584  T       t1425   o635 b1425 b1393  B       b1426   s1425
3585  B       b1426   t1425  T       t1426   o613 b1426 b1363
3586  B       b1427   t1404  B       b1427   t1426
3587  B       b1428   t1424  B       b1428   t1371
3588  T       t1428   o556 b1427 b1428  B       b1429   t1425
3589  H       h1428   z t1428  T       t1429   o562 b1428 b1429
3590  S       s1428   t626 h h1396 h716 h1397 h1428 h1414  H       h1429   z_2 t1429
3591  G       s1428   t1370  S       s1429   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1429 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3592  B       b1429   s1428  G       s1429   t1348
3593  T       t1429   o635 b1429 b1393  B       b1430   s1429
3594  B       b1430   t1429  T       t1430   o613 b1430 b1363
3595  B       b1431   t1397  B       b1431   t1430
3596  B       b1432   t1428  B       b1432   t1370
3597  T       t1432   o556 b1431 b1432  B       b1433   t1429
3598  H       h1432   z_1 t1432  T       t1433   o562 b1432 b1433
3599  S       s1432   t626 h h1396 h716 h1432 h1414  H       h1433   z t1433
3600  G       s1432   t1370  S       s1433   t604 h h1366 h1367 h1368 h1369 h1370 h1433 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3601  B       b1433   s1432  G       s1433   t1348
3602  T       t1433   o635 b1433 b1393  B       b1434   s1433
3603  B       b1434   t1433  T       t1434   o613 b1434 b1363
3604  B       b1435   t1432  B       b1435   t1434
3605  T       t1435   o556 b558 b1435  B       b1436   t1433
3606  H       h1435   z t1435  T       t1436   o562 b564 b1436
3607  S       s1435   t626 h h1396 h1435 h1414  H       h1436   z_2 t1436
3608  G       s1435   t1370  S       s1436   t604 h h1366 h1367 h1368 h1369 h1436 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3609  B       b1436   s1435  G       s1436   t1348
3610  T       t1436   o635 b1436 b1393  B       b1437   s1436
3611  B       b1437   t1436  T       t1437   o613 b1437 b1363
3612  B       b1438   t1396  B       b1438   t1437
3613  B       b1439   t1435  B       b1439   t1366
3614  T       t1439   o556 b1438 b1439  B       b1440   t1436
3615  H       h1439   v t1439  T       t1440   o562 b1439 b1440
3616  S       s1439   t626 h h1439 h1414  H       h1440   z t1440
3617  G       s1439   t1370  S       s1440   t604 h h1366 h1367 h1368 h1440 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3618  B       b1440   s1439  G       s1440   t1348
3619  T       t1440   o635 b1440 b1393  B       b1441   s1440
3620  B       b1441   t1440  T       t1441   o613 b1441 b1363
3621  H       h1441   v t1344  B       b1442   t1441
3622  S       s1441   t626 h h1441 h1414  B       b1443   t1367
3623  G       s1441   t1370  B       b1444   t1440
3624  B       b1442   s1441  T       t1444   o562 b1443 b1444
3625  T       t1442   o635 b1442 b1393  H       h1444   z_2 t1444
3626  B       b1443   t1442  S       s1444   t604 h h1366 h1367 h1444 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3627  S       s1443   t626 h h1441  G       s1444   t1348
3628  G       s1443   t1370  B       b1445   s1444
3629  B       b1444   s1443  T       t1445   o613 b1445 b1363
 T       t1444   o635 b1444 b1393  
 B       b1445   t1444  
 T       t1445   o2 b1395  
3630  B       b1446   t1445  B       b1446   t1445
3631  T       t1446   o634 b1445 b4 b1446  B       b1447   t1444
3632  B       b1447   t1446  T       t1447   o562 b564 b1447
3633  T       t1447   o2 b1447  H       h1447   z t1447
3634  B       b1448   t1447  S       s1447   t604 h h1366 h1447 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3635  T       t1448   o634 b1443 b4 b1448  G       s1447   t1348
3636    B       b1448   s1447
3637    T       t1448   o613 b1448 b1363
3638  B       b1449   t1448  B       b1449   t1448
3639  T       t1449   o2 b1449  B       b1450   t1447
3640  B       b1450   t1449  T       t1450   o562 b1439 b1450
3641  T       t1450   o634 b1441 b4 b1450  H       h1450   v t1450
3642  B       b1451   t1450  S       s1450   t604 h h1450 h1390 h1391 h1392 h1393 h1402 h1406 h1411
3643  T       t1451   o2 b1451  G       s1450   t1348
3644    B       b1451   s1450
3645    T       t1451   o613 b1451 b1363
3646  B       b1452   t1451  B       b1452   t1451
3647  T       t1452   o634 b1437 b4 b1452  B       b1453   t1406
3648  B       b1453   t1452  B       b1454   t1411
3649  T       t1453   o2 b1453  T       t1454   o562 b1453 b1454
3650  B       b1454   t1453  H       h1454   z t1454
3651  T       t1454   o634 b1434 b4 b1454  S       s1454   t604 h h1450 h1390 h1391 h1392 h1393 h1402 h1454
3652  B       b1455   t1454  G       s1454   t1348
3653  T       t1455   o2 b1455  B       b1455   s1454
3654    T       t1455   o613 b1455 b1363
3655  B       b1456   t1455  B       b1456   t1455
3656  T       t1456   o634 b1430 b4 b1456  B       b1457   t1402
3657  B       b1457   t1456  B       b1458   t1454
3658  T       t1457   o2 b1457  T       t1458   o562 b1457 b1458
3659  B       b1458   t1457  H       h1458   z_1 t1458
3660  T       t1458   o634 b1426 b4 b1458  S       s1458   t604 h h1450 h1390 h1391 h1392 h1393 h1458
3661  B       b1459   t1458  G       s1458   t1348
3662  T       t1459   o2 b1459  B       b1459   s1458
3663    T       t1459   o613 b1459 b1363
3664  B       b1460   t1459  B       b1460   t1459
3665  T       t1460   o634 b1422 b729 b1460  B       b1461   t1393
3666  B       b1461   t1460  B       b1462   t1458
3667  T       t1461   o2 b1461  T       t1462   o562 b1461 b1462
3668  B       b1462   t1461  H       h1462   z t1462
3669  T       t1462   o634 b1420 b729 b1462  S       s1462   t604 h h1450 h1390 h1391 h1392 h1462
3670  B       b1463   t1462  G       s1462   t1348
3671  T       t1463   o2 b1463  B       b1463   s1462
3672    T       t1463   o613 b1463 b1363
3673  B       b1464   t1463  B       b1464   t1463
3674  T       t1464   o634 b1418 b4 b1464  B       b1465   t1391
3675  B       b1465   t1464  B       b1466   t1462
3676  T       t1465   o568 b1348 b1356 b1357 b571  T       t1466   o562 b1465 b1466
3677  S       s1465   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355  H       h1466   z_1 t1466
3678  G       s1465   t1465  S       s1466   t604 h h1450 h1390 h1391 h1466
3679  B       b1466   s1465  G       s1466   t1348
3680  T       t1466   o635 b1466 b1393  B       b1467   s1466
3681  B       b1467   t1466  T       t1467   o613 b1467 b1363
 T       t1467   o634 b1467 b4 b1462  
3682  B       b1468   t1467  B       b1468   t1467
3683  T       t1468   o564 b668 b1348  B       b1469   t1466
3684  H       h1468   x t1468  T       t1469   o562 b1439 b1469
3685  T       t1469   o564 b670 b1348  H       h1469   z t1469
3686  H       h1469   y t1469  S       s1469   t604 h h1450 h1390 h1469
3687  T       t1470   o568 b1348 b1356 b668 b670  G       s1469   t1348
3688  S       s1470   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h667 h668 h1468 h1469 h672  B       b1470   s1469
3689  G       s1470   t1470  T       t1470   o613 b1470 b1363
3690  B       b1470   s1470  B       b1471   t1470
3691  T       t1471   o635 b1470 b1393  B       b1472   t1390
3692  B       b1471   t1471  B       b1473   t1469
3693  T       t1472   o634 b1471 b4 b1462  T       t1473   o562 b1472 b1473
3694  B       b1472   t1472  H       h1473   v_1 t1473
3695  T       t1473   o b1472 b4  S       s1473   t604 h h1450 h1473
3696  B       b1473   t1473  G       s1473   t1348
3697  T       t1474   o b1468 b1473  B       b1474   s1473
3698  B       b1474   t1474  T       t1474   o613 b1474 b1363
3699  T       t1475   o b1465 b1474  B       b1475   t1474
3700  B       b1475   t1475  H       h1475   v_1 t1346
3701  T       t1476   o633 b1395 b1475  S       s1475   t604 h h1450 h1475
3702  B       b1476   t1476  G       s1475   t1348
3703  P       p1476   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 10 ttca"  B       b1476   s1475
3704  O       o1476   ext_rule p1476  T       t1476   o613 b1476 b1363
3705  T       t1477   o564 b1415 b1351  B       b1477   t1476
3706  H       h1477   v t1477  T       t1477   o567 b1325 b556 b1343
3707  S       s1477   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416 h1477  B       b1478   t1477
3708  G       s1477   t1417  T       t1478   o562 b1443 b1478
3709  B       b1477   s1477  B       b1479   t1478
3710  T       t1478   o635 b1477 b1393  T       t1479   o562 b564 b1479
3711  B       b1478   t1478  B       b1480   t1479
3712  T       t1479   o2 b1465  T       t1480   o562 b1439 b1480
3713  B       b1479   t1479  H       h1480   v t1480
3714  T       t1480   o634 b1478 b4 b1479  S       s1480   t604 h h1480 h1475
3715  B       b1480   t1480  G       s1480   t1348
3716  T       t1481   o b1480 b4  B       b1481   s1480
3717  B       b1481   t1481  T       t1481   o613 b1481 b1363
3718  T       t1482   o633 b1465 b1481  B       b1482   t1481
3719  B       b1482   t1482  H       h1482   v t1339
3720  P       p1482   String "rwh unfold_bisect 11 thenT dT 11 ttca"  S       s1482   t604 h h1482 h1475
3721  O       o1482   ext_rule p1482  G       s1482   t1348
3722  NCzf_itt_sep    Czf_itt_sep     Czf_itt_sep NIL  B       b1483   s1482
3723  NCzf_itt_sep!sep        sep     sep Czf_itt_sep  T       t1483   o613 b1483 b1363
3724  O       o1483   sep  B       b1484   t1483
3725  T       t1483   o564 b1415 b1350  S       s1484   t604 h h1482
3726  B       b1483   t1483 x  G       s1484   t1348
3727  T       t1484   o1483 b1349 b1483  B       b1485   s1484
3728  B       b1484   t1484  T       t1485   o613 b1485 b1363
3729  T       t1485   o564 b1415 b1484  B       b1486   t1485
3730  H       h1485   v t1485  T       t1486   o2 b1365
3731  T       t1486   o564 b1415 b1349  B       b1487   t1486
3732  H       h1486   u t1486  T       t1487   o612 b1486 b4 b1487
 H       h1487   v_2 t1483  
 S       s1487   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416 h1485 h1486 h1487  
 G       s1487   t1417  
 B       b1487   s1487  
 T       t1487   o635 b1487 b1393  
3733  B       b1488   t1487  B       b1488   t1487
3734  S       s1488   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416 h1485  T       t1488   o2 b1488
3735  G       s1488   t1417  B       b1489   t1488
3736  B       b1489   s1488  T       t1489   o612 b1484 b4 b1489
 T       t1489   o635 b1489 b1393  
3737  B       b1490   t1489  B       b1490   t1489
3738  T       t1490   o2 b1480  T       t1490   o2 b1490
3739  B       b1491   t1490  B       b1491   t1490
3740  T       t1491   o634 b1490 b4 b1491  T       t1491   o612 b1482 b4 b1491
3741  B       b1492   t1491  B       b1492   t1491
3742  T       t1492   o2 b1492  T       t1492   o2 b1492
3743  B       b1493   t1492  B       b1493   t1492
3744  T       t1493   o634 b1488 b4 b1493  T       t1493   o612 b1477 b4 b1493
3745  B       b1494   t1493  B       b1494   t1493
3746  T       t1494   o b1494 b4  T       t1494   o2 b1494
3747  B       b1495   t1494  B       b1495   t1494
3748  T       t1495   o633 b1480 b1495  T       t1495   o612 b1475 b4 b1495
3749  B       b1496   t1495  B       b1496   t1495
3750  P       p1496   String "withT << 'x >> (dT 4) ttca"  T       t1496   o2 b1496
 O       o1496   ext_rule p1496  
 T       t1496   o633 b1494 b4  
3751  B       b1497   t1496  B       b1497   t1496
3752  T       t1497   o1496 b632 b1497 b4 b4  T       t1497   o612 b1471 b4 b1497
3753  B       b1498   t1497  B       b1498   t1497
3754  T       t1498   o b1498 b4  T       t1498   o2 b1498
3755  B       b1499   t1498  B       b1499   t1498
3756  T       t1499   o1482 b632 b1496 b1499 b4  T       t1499   o612 b1468 b4 b1499
3757  B       b1500   t1499  B       b1500   t1499
3758  T       t1500   o b1500 b4  T       t1500   o2 b1500
3759  B       b1501   t1500  B       b1501   t1500
3760  T       t1501   o1476 b632 b1482 b1501 b4  T       t1501   o612 b1464 b4 b1501
3761  B       b1502   t1501  B       b1502   t1501
3762  P       p1502   String "assumT 9 thenT assumT 11 ttca"  T       t1502   o2 b1502
3763  O       o1502   ext_rule p1502  B       b1503   t1502
3764  B       b1503   t1354  T       t1503   o612 b1460 b4 b1503
3765  B       b1504   t1355  B       b1504   t1503
3766  B       b1505   t1359  T       t1504   o2 b1504
3767  T       t1505   o563 b1504 b1505  B       b1505   t1504
3768    T       t1505   o612 b1456 b4 b1505
3769  B       b1506   t1505  B       b1506   t1505
3770  T       t1506   o563 b1503 b1506  T       t1506   o2 b1506
3771  B       b1507   t1506 b  B       b1507   t1506
3772  T       t1507   o561 b562 b1507  T       t1507   o612 b1452 b4 b1507
3773  B       b1508   t1507 a  B       b1508   t1507
3774  T       t1508   o561 b562 b1508  T       t1508   o2 b1508
3775  H       h1508   v t1508  B       b1509   t1508
3776  B       b1509   t1365  T       t1509   o612 b1449 b4 b1509
3777  B       b1510   t1366  B       b1510   t1509
3778  B       b1511   t1367  T       t1510   o2 b1510
3779  B       b1512   t1368  B       b1511   t1510
3780  T       t1512   o563 b1511 b1512  T       t1511   o612 b1446 b4 b1511
3781    B       b1512   t1511
3782    T       t1512   o2 b1512
3783  B       b1513   t1512  B       b1513   t1512
3784  T       t1513   o563 b1510 b1513  T       t1513   o612 b1442 b4 b1513
3785  B       b1514   t1513  B       b1514   t1513
3786  T       t1514   o563 b1509 b1514  T       t1514   o2 b1514
3787  B       b1515   t1514 f  B       b1515   t1514
3788  T       t1515   o561 b562 b1515  T       t1515   o612 b1438 b4 b1515
3789  B       b1516   t1515 e  B       b1516   t1515
3790  T       t1516   o561 b562 b1516  T       t1516   o2 b1516
3791  H       h1516   v_2 t1516  B       b1517   t1516
3792  S       s1516   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516  T       t1517   o612 b1435 b4 b1517
 G       s1516   t1465  
 B       b1517   s1516  
 T       t1517   o635 b1517 b1393  
3793  B       b1518   t1517  B       b1518   t1517
3794  S       s1518   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508  T       t1518   o2 b1518
3795  G       s1518   t1465  B       b1519   t1518
3796  B       b1519   s1518  T       t1519   o612 b1431 b4 b1519
 T       t1519   o635 b1519 b1393  
3797  B       b1520   t1519  B       b1520   t1519
3798  T       t1520   o2 b1468  T       t1520   o2 b1520
3799  B       b1521   t1520  B       b1521   t1520
3800  T       t1521   o634 b1520 b4 b1521  T       t1521   o612 b1427 b4 b1521
3801  B       b1522   t1521  B       b1522   t1521
3802  T       t1522   o2 b1522  T       t1522   o2 b1522
3803  B       b1523   t1522  B       b1523   t1522
3804  T       t1523   o634 b1518 b4 b1523  T       t1523   o612 b1423 b4 b1523
3805  B       b1524   t1523  B       b1524   t1523
3806  T       t1524   o b1524 b4  T       t1524   o2 b1524
3807  B       b1525   t1524  B       b1525   t1524
3808  T       t1525   o633 b1468 b1525  T       t1525   o612 b1419 b729 b1525
3809  B       b1526   t1525  B       b1526   t1525
3810  P       p1526   String "instHypT [<< 'a >>; << 'b >>] 13 ttca thenT dT 15 ttca thenT dT 15 ttca"  T       t1526   o2 b1526
3811  O       o1526   ext_rule p1526  B       b1527   t1526
3812  H       h1526   y_6 t1359  T       t1527   o612 b1417 b729 b1527
 S       s1526   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526  
 G       s1526   t1465  
 B       b1527   s1526  
 T       t1527   o635 b1527 b1393  
3813  B       b1528   t1527  B       b1528   t1527
3814  H       h1528   y_5 t1505  T       t1528   o2 b1528
3815  S       s1528   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1528 h1526  B       b1529   t1528
3816  G       s1528   t1465  T       t1529   o612 b1415 b4 b1529
 B       b1529   s1528  
 T       t1529   o635 b1529 b1393  
3817  B       b1530   t1529  B       b1530   t1529
3818  S       s1530   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1528  H       h1530   x t1394
3819  G       s1530   t1465  H       h1531   y t1395
3820  B       b1531   s1530  T       t1531   o640 b1392 b1396 b1397 b643
3821  T       t1531   o635 b1531 b1393  S       s1531   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1384 h1389 h1390 h1391 h1392 h1393 h1402 h1406 h1411 h635 h636 h1530 h1531
3822  B       b1532   t1531  G       s1531   t1531
3823  H       h1532   w_1 t1506  B       b1531   s1531
3824  S       s1532   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1532 h1528  T       t1532   o613 b1531 b1363
3825  G       s1532   t1465  B       b1532   t1532
3826  B       b1533   s1532  T       t1533   o612 b1532 b4 b1527
3827  T       t1533   o635 b1533 b1393  B       b1533   t1533
3828  B       b1534   t1533  T       t1534   o636 b652 b1392
3829  S       s1534   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1532  H       h1534   x t1534
3830  G       s1534   t1465  T       t1535   o636 b654 b1392
3831  B       b1535   s1534  H       h1535   y t1535
3832  T       t1535   o635 b1535 b1393  T       t1536   o640 b1392 b1396 b652 b654
3833  B       b1536   t1535  S       s1536   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1384 h1389 h1390 h1391 h1392 h1393 h1402 h1406 h1411 h651 h652 h1534 h1535 h656
3834  H       h1536   w t1507  G       s1536   t1536
3835  S       s1536   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1536 h1532  B       b1536   s1536
3836  G       s1536   t1465  T       t1537   o613 b1536 b1363
3837  B       b1537   s1536  B       b1537   t1537
3838  T       t1537   o635 b1537 b1393  T       t1538   o612 b1537 b4 b1527
3839  B       b1538   t1537  B       b1538   t1538
3840  S       s1538   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1536  T       t1539   o b1538 b4
3841  G       s1538   t1465  B       b1539   t1539
3842  B       b1539   s1538  T       t1540   o b1533 b1539
3843  T       t1539   o635 b1539 b1393  B       b1540   t1540
3844  B       b1540   t1539  T       t1541   o b1530 b1540
3845  T       t1540   o b567 b4  B       b1541   t1541
3846  B       b1541   t1540  T       t1542   o611 b1365 b1541
3847  T       t1541   o887 b1541  B       b1542   t1542
3848  B       b1542   t1541  P       p1542   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 20 ttca"
3849  T       t1542   o886 b1542  O       o1542   ext_rule p1542
3850  B       b1543   t1542  T       t1543   o636 b1412 b1345
3851  T       t1543   o b1543 b997  H       h1543   v t1543
3852  B       b1544   t1543  S       s1543   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1384 h1389 h1390 h1391 h1392 h1393 h1402 h1406 h1411 h1412 h1413 h1543
3853  T       t1544   o634 b1518 b1212 b1523  G       s1543   t1414
3854  B       b1545   t1544  B       b1543   s1543
3855  T       t1545   o2 b1545  T       t1544   o613 b1543 b1363
3856  B       b1546   t1545  B       b1544   t1544
3857  T       t1546   o634 b1540 b1544 b1546  T       t1545   o2 b1530
3858  B       b1547   t1546  B       b1545   t1545
3859  T       t1547   o2 b1547  T       t1546   o612 b1544 b4 b1545
3860  B       b1548   t1547  B       b1546   t1546
3861  T       t1548   o634 b1538 b997 b1548  T       t1547   o b1546 b4
3862  B       b1549   t1548  B       b1547   t1547
3863  T       t1549   o2 b1549  T       t1548   o611 b1530 b1547
3864  B       b1550   t1549  B       b1548   t1548
3865  T       t1550   o634 b1536 b4 b1550  P       p1548   String "rwh unfold_bisect 21 thenT dT 21 ttca"
3866  B       b1551   t1550  O       o1548   ext_rule p1548
3867  T       t1551   o2 b1551  NCzf_itt_sep    Czf_itt_sep     Czf_itt_sep NIL
3868  B       b1552   t1551  NCzf_itt_sep!sep        sep     sep Czf_itt_sep
3869  T       t1552   o634 b1534 b4 b1552  O       o1549   sep
3870  B       b1553   t1552  T       t1549   o636 b1412 b1344
3871  T       t1553   o2 b1553  B       b1549   t1549 x
3872    T       t1550   o1549 b1343 b1549
3873    B       b1550   t1550
3874    T       t1551   o636 b1412 b1550
3875    H       h1551   v t1551
3876    T       t1552   o636 b1412 b1343
3877    H       h1552   u t1552
3878    H       h1553   v_1 t1549
3879    S       s1553   t604 h h1366 h1367 h1368 h1369 h1370 h1371 h1372 h1380 h1384 h1389 h1390 h1391 h1392 h1393 h1402 h1406 h1411 h1412 h1413 h1551 h1552 h1553
3880    G       s1553   t1414