/[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 3555 by xiny, Mon Mar 11 09:58:58 2002 UTC revision 3556 by xiny, Tue Apr 2 08:08:36 2002 UTC
# Line 1299  Line 1299 
1299  T       t494    o488 b493  T       t494    o488 b493
1300  B       b494    t494  B       b494    t494
1301  P       p494    Number 321  P       p494    Number 321
1302  P       p3      Number 337  P       p495    Number 337
1303  O       o6      location p494 p3  O       o495    location p494 p495
1304  O       o8      str_open p494 p3  O       o496    str_open p494 p495
1305  O       o497    string p153  P       p496    String Tactic_type
1306    O       o497    string p496
1307  T       t497    o497  T       t497    o497
1308  B       b497    t497  B       b497    t497
1309  T       t498    o b497 b4  T       t498    o b497 b4
1310  B       b498    t498  B       b498    t498
1311  P       p503    String Tactic_type  T       t499    o496 b498
1312    B       b499    t499
1313    T       t500    o421 b499
1314    B       b500    t500
1315    T       t501    o495 b500
1316    B       b501    t501
1317    P       p501    Number 338
1318    P       p502    Number 362
1319    O       o502    location p501 p502
1320    O       o503    str_open p501 p502
1321    P       p503    String Sequent
1322  O       o504    string p503  O       o504    string p503
1323  T       t504    o504  T       t504    o504
1324  B       b504    t504  B       b504    t504
1325  T       t505    o b504 b4  T       t505    o b504 b4
1326  B       b505    t505  B       b505    t505
1327  T       t250    o8 b505  T       t506    o b497 b505
1328  B       b250    t250  B       b506    t506
1329  T       t251    o421 b250  T       t507    o503 b506
1330  B       b251    t251  B       b507    t507
1331  T       t254    o6 b251  T       t508    o421 b507
1332  B       b254    t254  B       b508    t508
1333  P       p260    Number 338  T       t509    o502 b508
1334  P       p261    Number 362  B       b509    t509
1335  O       o261    location p260 p261  P       p509    Number 363
1336  O       o262    str_open p260 p261  P       p510    Number 389
1337  P       p262    String Sequent  O       o510    location p509 p510
1338  O       o263    string p262  O       o511    str_open p509 p510
1339  T       t265    o263  P       p511    String Tacticals
1340  B       b265    t265  O       o512    string p511
1341  T       t266    o b265 b4  T       t512    o512
 B       b266    t266  
 T       t269    o b504 b266  
 B       b269    t269  
 T       t273    o262 b269  
 B       b273    t273  
 T       t274    o421 b273  
 B       b274    t274  
 T       t275    o261 b274  
 B       b275    t275  
 P       p282    Number 363  
 P       p283    Number 389  
 O       o283    location p282 p283  
 O       o284    str_open p282 p283  
 P       p510    String Tacticals  
 O       o511    string p510  
 T       t511    o511  
 B       b511    t511  
 T       t512    o b511 b4  
1342  B       b512    t512  B       b512    t512
1343  T       t513    o b504 b512  T       t513    o b512 b4
1344  B       b513    t513  B       b513    t513
1345  T       t287    o284 b513  T       t514    o b497 b513
1346  B       b287    t287  B       b514    t514
1347  T       t292    o421 b287  T       t515    o511 b514
1348  B       b292    t292  B       b515    t515
1349  T       t293    o283 b292  T       t516    o421 b515
1350  B       b293    t293  B       b516    t516
1351  P       p296    Number 390  T       t517    o510 b516
1352  P       p297    Number 398  B       b517    t517
1353  O       o297    location p296 p297  P       p517    Number 390
1354  O       o298    str_open p296 p297  P       p518    Number 398
1355  T       t301    o298 b498  O       o518    location p517 p518
1356  B       b301    t301  O       o519    str_open p517 p518
1357  T       t302    o421 b301  O       o520    string p153
1358  B       b302    t302  T       t520    o520
 T       t304    o297 b302  
 B       b304    t304  
 P       p313    Number 399  
 P       p315    Number 409  
 O       o315    location p313 p315  
 O       o316    str_open p313 p315  
 O       o317    string p155  
 T       t325    o317  
 B       b325    t325  
 T       t326    o b325 b4  
 B       b326    t326  
 T       t328    o316 b326  
 B       b328    t328  
 T       t336    o421 b328  
 B       b336    t336  
 T       t337    o315 b336  
 B       b337    t337  
 P       p343    Number 411  
 P       p358    Number 428  
 O       o358    location p343 p358  
 O       o359    str_open p343 p358  
 O       o519    string p143  
 T       t519    o519  
 B       b519    t519  
 T       t520    o b519 b4  
1359  B       b520    t520  B       b520    t520
1360  T       t363    o359 b520  T       t521    o b520 b4
1361  B       b363    t363  B       b521    t521
1362  T       t367    o421 b363  T       t522    o519 b521
1363  B       b367    t367  B       b522    t522
1364  T       t368    o358 b367  T       t523    o421 b522
1365  B       b368    t368  B       b523    t523
1366  P       p373    Number 429  T       t524    o518 b523
1367  P       p380    Number 450  B       b524    t524
1368  O       o380    location p373 p380  P       p524    Number 399
1369  O       o381    str_open p373 p380  P       p525    Number 409
1370  O       o526    string p145  O       o525    location p524 p525
1371  T       t526    o526  O       o526    str_open p524 p525
1372  B       b526    t526  O       o527    string p155
1373  T       t527    o b526 b4  T       t527    o527
1374  B       b527    t527  B       b527    t527
1375  T       t397    o381 b527  T       t528    o b527 b4
1376  B       b397    t397  B       b528    t528
1377  T       t414    o421 b397  T       t529    o526 b528
1378  B       b414    t414  B       b529    t529
1379  T       t420    o380 b414  T       t530    o421 b529
1380  B       b420    t420  B       b530    t530
1381  P       p421    Number 627  T       t531    o525 b530
1382  P       p423    Number 651  B       b531    t531
1383  O       o424    location p421 p423  P       p531    Number 411
1384  NSummary!opname opname  opname Summary  P       p532    Number 428
1385  P       p532    String subgroup  O       o532    location p531 p532
1386  O       o532    opname p532  O       o533    str_open p531 p532
1387  NCzf_itt_subgroup       Czf_itt_subgroup        Czf_itt_subgroup NIL  O       o534    string p143
 NCzf_itt_subgroup!subgroup      subgroup        subgroup Czf_itt_subgroup  
 O       o533    subgroup  
 Nvar    var     var NIL  
 P       p533    Var g  
 O       o534    var p533  
1388  T       t534    o534  T       t534    o534
1389  B       b534    t534  B       b534    t534
1390  P       p534    Var s  T       t535    o b534 b4
 O       o535    var p534  
 T       t535    o535  
1391  B       b535    t535  B       b535    t535
1392  T       t536    o533 b534 b535  T       t536    o533 b535
1393  B       b536    t536  B       b536    t536
1394  T       t537    o532 b536  T       t537    o421 b536
1395  B       b537    t537  B       b537    t537
1396  T       t428    o424 b537  T       t538    o532 b537
1397  B       b428    t428  B       b538    t538
1398  P       p430    Number 653  P       p538    Number 429
1399  P       p431    Number 861  P       p539    Number 450
1400  O       o431    location p430 p431  O       o539    location p538 p539
1401    O       o540    str_open p538 p539
1402    O       o541    string p145
1403    T       t541    o541
1404    B       b541    t541
1405    T       t542    o b541 b4
1406    B       b542    t542
1407    T       t543    o540 b542
1408    B       b543    t543
1409    T       t544    o421 b543
1410    B       b544    t544
1411    T       t545    o539 b544
1412    B       b545    t545
1413    P       p545    Number 626
1414    P       p546    Number 650
1415    O       o546    location p545 p546
1416    NSummary!opname opname  opname Summary
1417    P       p547    String subgroup
1418    O       o547    opname p547
1419    NCzf_itt_subgroup       Czf_itt_subgroup        Czf_itt_subgroup NIL
1420    NCzf_itt_subgroup!subgroup      subgroup        subgroup Czf_itt_subgroup
1421    O       o548    subgroup
1422    Nvar    var     var NIL
1423    P       p548    Var s
1424    O       o549    var p548
1425    T       t549    o549
1426    B       b549    t549
1427    P       p549    Var g
1428    O       o550    var p549
1429    T       t550    o550
1430    B       b550    t550
1431    T       t551    o548 b549 b550
1432    B       b551    t551
1433    T       t552    o547 b551
1434    B       b552    t552
1435    T       t553    o546 b552
1436    B       b553    t553
1437    P       p553    Number 652
1438    P       p554    Number 958
1439    O       o554    location p553 p554
1440  NSummary!rewrite        rewrite rewrite Summary  NSummary!rewrite        rewrite rewrite Summary
1441  P       p540    String unfold_subgroup  P       p555    String unfold_subgroup
1442  O       o540    rewrite p540  O       o555    rewrite p555
1443  NItt_logic      Itt_logic       Itt_logic NIL  NItt_logic      Itt_logic       Itt_logic NIL
1444  NItt_logic!and  and     and Itt_logic  NItt_logic!and  and     and Itt_logic
1445  O       o541    and  O       o556    and
1446  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1447  NCzf_itt_group!group    group   group Czf_itt_group  NCzf_itt_group!group    group   group Czf_itt_group
1448  O       o542    group  O       o557    group
1449  T       t542    o542 b534  T       t557    o557 b549
1450  B       b542    t542  B       b557    t557
1451  T       t543    o542 b535  T       t558    o557 b550
1452  B       b543    t543  B       b558    t558
1453  NCzf_itt_subset Czf_itt_subset  Czf_itt_subset NIL  NCzf_itt_subset Czf_itt_subset  Czf_itt_subset NIL
1454  NCzf_itt_subset!subset  subset  subset Czf_itt_subset  NCzf_itt_subset!subset  subset  subset Czf_itt_subset
1455  O       o543    subset  O       o558    subset
1456  NCzf_itt_group!car      car     car Czf_itt_group  NCzf_itt_group!car      car     car Czf_itt_group
1457  O       o544    car  O       o559    car
1458  T       t544    o544 b535  T       t559    o559 b549
1459  B       b544    t544  B       b559    t559
1460  T       t545    o544 b534  T       t560    o559 b550
1461  B       b545    t545  B       b560    t560
1462  T       t546    o543 b544 b545  T       t561    o558 b559 b560
1463  B       b546    t546  B       b561    t561
1464  NItt_logic!all  all     all Itt_logic  NItt_logic!all  all     all Itt_logic
1465  O       o546    all  O       o561    all
1466  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL
1467  NCzf_itt_set!set        set     set Czf_itt_set  NCzf_itt_set!set        set     set Czf_itt_set
1468  O       o547    set  O       o562    set
1469  T       t547    o547  T       t562    o562
1470  B       b547    t547  B       b562    t562
1471  NItt_logic!implies      implies implies Itt_logic  NItt_logic!implies      implies implies Itt_logic
1472  O       o548    implies  O       o563    implies
1473  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1474  NCzf_itt_member!mem     mem     mem Czf_itt_member  NCzf_itt_member!mem     mem     mem Czf_itt_member
1475  O       o549    mem  O       o564    mem
1476  P       p549    Var a  P       p564    Var a
1477  O       o550    var p549  O       o565    var p564
1478  T       t550    o550  T       t565    o565
1479  B       b550    t550  B       b565    t565
1480  T       t551    o549 b550 b544  T       t566    o564 b565 b559
1481  B       b551    t551  B       b566    t566
1482  P       p551    Var b  P       p566    Var b
1483  O       o551    var p551  O       o566    var p566
1484  T       t552    o551  T       t567    o566
1485  B       b552    t552  B       b567    t567
1486  T       t553    o549 b552 b544  T       t568    o564 b567 b559
1487  B       b553    t553  B       b568    t568
1488  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
1489  NCzf_itt_eq!equal       equal   equal Czf_itt_eq  NCzf_itt_eq!equal       equal   equal Czf_itt_eq
1490  O       o553    equal  O       o568    equal
1491  NCzf_itt_group!op       op      op Czf_itt_group  NCzf_itt_group!op       op      op Czf_itt_group
1492  O       o554    op  O       o569    op
1493  T       t554    o554 b535 b550 b552  T       t569    o569 b549 b565 b567
 B       b554    t554  
 T       t555    o554 b534 b550 b552  
 B       b555    t555  
 T       t556    o553 b554 b555  
 B       b556    t556  
 T       t557    o548 b553 b556  
 B       b557    t557  
 T       t558    o548 b551 b557  
 B       b558    t558 b  
 T       t559    o546 b547 b558  
 B       b559    t559 a  
 T       t560    o546 b547 b559  
 B       b560    t560  
 T       t561    o541 b546 b560  
 B       b561    t561  
 T       t562    o541 b543 b561  
 B       b562    t562  
 T       t563    o541 b542 b562  
 B       b563    t563  
 NSummary!prim   prim    prim Summary  
 O       o563    prim  
 T       t564    o563 b4  
 B       b564    t564  
 T       t565    o540 b536 b563 b564 b4  
 B       b565    t565  
 T       t435    o431 b565  
 B       b435    t435  
 P       p437    Number 863  
 P       p438    Number 966  
 O       o438    location p437 p438  
 NSummary!dform  dform   dform Summary  
 P       p568    String subgroup_df  
 O       o568    dform p568  
 NSummary!except_mode_df except_mode_df  except_mode_df Summary  
 P       p569    String src  
 O       o569    except_mode_df p569  
 T       t569    o569  
1494  B       b569    t569  B       b569    t569
1495  T       t570    o b569 b4  T       t570    o569 b550 b565 b567
1496  B       b570    t570  B       b570    t570
1497  NSummary!df_term        df_term df_term Summary  T       t571    o568 b569 b570
 O       o570    df_term  
 NPerv!string    string570       string Perv  
 P       p570    String subgroup(  
 O       o571    string570 p570  
 T       t571    o571  
1498  B       b571    t571  B       b571    t571
1499  Nslot   slot    slot NIL  T       t572    o563 b568 b571
 O       o572    slot  
 T       t572    o572 b534  
1500  B       b572    t572  B       b572    t572
1501  P       p572    String "; "  T       t573    o563 b566 b572
1502  O       o573    string570 p572  B       b573    t573 b
1503  T       t573    o573  T       t574    o561 b562 b573
1504  B       b573    t573  B       b574    t574 a
1505  T       t574    o572 b535  T       t575    o561 b562 b574
 B       b574    t574  
 P       p574    String )  
 O       o574    string570 p574  
 T       t575    o574  
1506  B       b575    t575  B       b575    t575
1507  T       t576    o b575 b4  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1508    NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1509    O       o575    equiv
1510    NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
1511    O       o576    eqG
1512    T       t576    o576 b549
1513  B       b576    t576  B       b576    t576
1514  T       t577    o b574 b576  T       t577    o575 b559 b576 b565 b567
1515  B       b577    t577  B       b577    t577
1516  T       t578    o b573 b577  T       t578    o576 b550
1517  B       b578    t578  B       b578    t578
1518  T       t579    o b572 b578  T       t579    o575 b560 b578 b565 b567
1519  B       b579    t579  B       b579    t579
1520  T       t580    o b571 b579  T       t580    o563 b577 b579
1521  B       b580    t580  B       b580    t580 b
1522  T       t581    o570 b580  T       t581    o561 b562 b580
1523  B       b581    t581  B       b581    t581 a
1524  T       t582    o568 b570 b536 b581  T       t582    o561 b562 b581
1525  B       b582    t582  B       b582    t582
1526  T       t443    o438 b582  T       t583    o556 b575 b582
1527  B       b443    t443  B       b583    t583
1528  P       p445    Number 985  T       t584    o556 b561 b583
1529  P       p446    Number 1259  B       b584    t584
1530  O       o446    location p445 p446  T       t585    o556 b558 b584
1531  NSummary!rule   rule    rule Summary  B       b585    t585
1532  P       p585    String subgroup_type  T       t586    o556 b557 b585
 O       o585    rule p585  
 NSummary!context_param  context_param   context_param Summary  
 P       p586    String H  
 O       o586    context_param p586  
 T       t586    o586  
1533  B       b586    t586  B       b586    t586
1534  T       t587    o b586 b4  NSummary!prim   prim    prim Summary
1535    O       o586    prim
1536    T       t587    o586 b4
1537  B       b587    t587  B       b587    t587
1538    T       t588    o555 b551 b586 b587 b4
1539    B       b588    t588
1540    T       t589    o554 b588
1541    B       b589    t589
1542    P       p589    Number 960
1543    P       p590    Number 1063
1544    O       o590    location p589 p590
1545    NSummary!dform  dform   dform Summary
1546    P       p591    String subgroup_df
1547    O       o591    dform p591
1548    NSummary!except_mode_df except_mode_df  except_mode_df Summary
1549    P       p592    String src
1550    O       o592    except_mode_df p592
1551    T       t592    o592
1552    B       b592    t592
1553    T       t593    o b592 b4
1554    B       b593    t593
1555    NSummary!df_term        df_term df_term Summary
1556    O       o593    df_term
1557    NPerv!string    string593       string Perv
1558    P       p593    String subgroup(
1559    O       o594    string593 p593
1560    T       t594    o594
1561    B       b594    t594
1562    Nslot   slot    slot NIL
1563    O       o595    slot
1564    T       t595    o595 b549
1565    B       b595    t595
1566    P       p595    String "; "
1567    O       o596    string593 p595
1568    T       t596    o596
1569    B       b596    t596
1570    T       t597    o595 b550
1571    B       b597    t597
1572    P       p597    String )
1573    O       o597    string593 p597
1574    T       t598    o597
1575    B       b598    t598
1576    T       t599    o b598 b4
1577    B       b599    t599
1578    T       t600    o b597 b599
1579    B       b600    t600
1580    T       t601    o b596 b600
1581    B       b601    t601
1582    T       t602    o b595 b601
1583    B       b602    t602
1584    T       t603    o b594 b602
1585    B       b603    t603
1586    T       t604    o593 b603
1587    B       b604    t604
1588    T       t605    o591 b593 b551 b604
1589    B       b605    t605
1590    T       t606    o590 b605
1591    B       b606    t606
1592    P       p606    Number 1082
1593    P       p607    Number 1272
1594    O       o607    location p606 p607
1595    NSummary!rule   rule    rule Summary
1596    P       p608    String subgroup_type
1597    O       o608    rule p608
1598    NSummary!context_param  context_param   context_param Summary
1599    P       p609    String H
1600    O       o609    context_param p609
1601    T       t609    o609
1602    B       b609    t609
1603    T       t610    o b609 b4
1604    B       b610    t610
1605  NSummary!meta_implies   meta_implies    meta_implies Summary  NSummary!meta_implies   meta_implies    meta_implies Summary
1606  O       o587    meta_implies  O       o610    meta_implies
1607  NSummary!meta_theorem   meta_theorem    meta_theorem Summary  NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1608  O       o588    meta_theorem  O       o611    meta_theorem
1609  NBase_trivial   Base_trivial    Base_trivial NIL  NBase_trivial   Base_trivial    Base_trivial NIL
1610  NBase_trivial!squash    squash  squash Base_trivial  NBase_trivial!squash    squash  squash Base_trivial
1611  O       o589    squash  O       o612    squash
1612  T       t589    o589  T       t612    o612
1613  B       b589    t589  B       b612    t612
1614  T       t590    o b589 b4  T       t613    o b612 b4
1615  C       h       H  C       h       H
1616  NItt_equal      Itt_equal       Itt_equal NIL  NItt_equal      Itt_equal       Itt_equal NIL
1617  NItt_equal!equal        equal590        equal Itt_equal  NItt_equal!equal        equal613        equal Itt_equal
1618  O       o590    equal590  O       o613    equal613
1619  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1620  NItt_record_label0!label        label   label Itt_record_label0  NItt_record_label0!label        label   label Itt_record_label0
1621  O       o591    label  O       o614    label
1622  T       t591    o591  T       t614    o614
1623  B       b591    t591  B       b614    t614
1624  T       t592    o590 b591 b534 b534  T       t615    o613 b614 b549 b549
1625  S       s       t590 h  S       s       t613 h
1626  G       s       t592  G       s       t615
1627  B       b592    s  B       b615    s
1628  T       t593    o588 b592  T       t616    o611 b615
1629  B       b593    t593  B       b616    t616
1630  T       t594    o590 b591 b535 b535  T       t617    o613 b614 b550 b550
1631  S       s594    t590 h  S       s617    t613 h
1632  G       s594    t594  G       s617    t617
1633  B       b594    s594  B       b617    s617
1634  T       t595    o588 b594  T       t618    o611 b617
1635  B       b595    t595  B       b618    t618
1636  P       p595    Var ext  P       p618    Var ext
1637  O       o595    var p595  O       o618    var p618
1638  T       t596    o595  T       t619    o618
1639  B       b596    t596  B       b619    t619
1640  T       t597    o b596 b4  T       t620    o b619 b4
 S       s597    t597 h  
 G       s597    t542  
 B       b597    s597  
 T       t598    o588 b597  
 B       b598    t598  
 S       s598    t597 h  
 G       s598    t543  
 B       b599    s598  
 T       t599    o588 b599  
 B       b600    t599  
1641  NItt_equal!type type    type Itt_equal  NItt_equal!type type    type Itt_equal
1642  O       o600    type  O       o620    type
1643  T       t600    o600 b536  T       t621    o620 b551
1644  S       s600    t597 h  S       s621    t620 h
1645  G       s600    t600  G       s621    t621
1646  B       b601    s600  B       b621    s621
1647  T       t601    o588 b601  T       t622    o611 b621
1648  B       b602    t601  B       b622    t622
1649  T       t602    o587 b600 b602  T       t623    o610 b618 b622
1650  B       b603    t602  B       b623    t623
1651  T       t603    o587 b598 b603  T       t624    o610 b616 b623
1652  B       b604    t603  B       b624    t624
 T       t604    o587 b595 b604  
 B       b605    t604  
 T       t605    o587 b593 b605  
 B       b606    t605  
1653  NSummary!interactive    interactive     interactive Summary  NSummary!interactive    interactive     interactive Summary
1654  O       o606    interactive  O       o624    interactive
1655  NSummary!ext_rule       ext_rule        ext_rule Summary  NSummary!ext_rule       ext_rule        ext_rule Summary
1656  P       p606    String "rwh unfold_subgroup 0 thenT autoT"  P       p624    String "rwh unfold_subgroup 0 thenT autoT"
1657  O       o607    ext_rule p606  O       o625    ext_rule p624
1658  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  NSummary!status_incomplete      status_incomplete       status_incomplete Summary
1659  O       o608    status_incomplete  O       o626    status_incomplete
1660  T       t608    o608  T       t626    o626
1661  B       b608    t608  B       b626    t626
1662  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
1663  O       o609    ext_unjustified  O       o627    ext_unjustified
1664  NSummary!tactic_arg     tactic_arg      tactic_arg Summary  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
1665  P       p609    String main  P       p627    String main
1666  O       o610    tactic_arg p609  O       o628    tactic_arg p627
1667  NSummary!msequent       msequent        msequent Summary  NSummary!msequent       msequent        msequent Summary
1668  O       o611    msequent  O       o629    msequent
1669  T       t611    o b599 b4  T       t629    o b617 b4
1670  B       b611    t611  B       b629    t629
1671  T       t612    o b597 b611  T       t630    o b615 b629
1672  B       b612    t612  B       b630    t630
1673  T       t613    o b594 b612  T       t631    o629 b621 b630
1674  B       b613    t613  B       b631    t631
 T       t614    o b592 b613  
 B       b614    t614  
 T       t615    o611 b601 b614  
 B       b615    t615  
1675  NSummary!parent_none    parent_none     parent_none Summary  NSummary!parent_none    parent_none     parent_none Summary
1676  O       o615    parent_none  O       o631    parent_none
1677  T       t616    o615  T       t632    o631
1678  B       b616    t616  B       b632    t632
1679  T       t617    o610 b615 b4 b616  T       t633    o628 b631 b4 b632
1680  B       b617    t617  B       b633    t633
1681  T       t618    o609 b617 b4  T       t634    o627 b633 b4
1682  B       b618    t618  B       b634    t634
1683  T       t619    o607 b608 b618 b4 b4  T       t635    o625 b626 b634 b4 b4
1684  B       b619    t619  B       b635    t635
1685  T       t620    o606 b619  T       t636    o624 b635
1686  B       b620    t620  B       b636    t636
1687  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
1688  P       p447    Number 1014  P       p636    Number 1111
1689  P       p448    Number 1022  P       p637    Number 1119
1690  O       o448    resource_defs p447 p448 p300  O       o637    resource_defs p636 p637 p300
1691  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
1692  P       p449    Number 1020  P       p638    Number 1117
1693  O       o449    uid p449 p448  O       o638    uid p638 p637
1694  P       p623    String []  P       p639    String []
1695  O       o623    uid p623  O       o639    uid p639
1696  T       t623    o623  T       t639    o639
1697  B       b623    t623  B       b639    t639
1698  T       t452    o449 b623  T       t640    o638 b639
1699  B       b452    t452  B       b640    t640
1700  T       t453    o b452 b4  T       t641    o b640 b4
1701  B       b453    t453  B       b641    t641
1702  T       t461    o448 b453  T       t642    o637 b641
1703  B       b461    t461  B       b642    t642
1704  T       t462    o b461 b4  T       t643    o b642 b4
1705  B       b462    t462  B       b643    t643
1706  T       t470    o585 b587 b606 b620 b462  T       t644    o608 b610 b624 b636 b643
1707  B       b470    t470  B       b644    t644
1708  T       t471    o446 b470  T       t645    o607 b644
1709  B       b471    t471  B       b645    t645
1710  P       p631    String subgroup_intro  P       p645    Number 1274
1711  O       o631    rule p631  O       o645    location p645 p309
1712  S       s631    t597 h  P       p646    String subgroup_intro
1713  G       s631    t546  O       o646    rule p646
1714  B       b631    s631  S       s646    t620 h
1715  T       t631    o588 b631  G       s646    t557
1716  B       b632    t631  B       b646    s646
1717  H       h632    a t547  T       t646    o611 b646
 H       h633    b t547  
 H       h634    x t551  
 H       h635    y t553  
 S       s635    t597 h h632 h633 h634 h635  
 G       s635    t556  
 B       b635    s635  
 T       t635    o588 b635  
 B       b636    t635  
 S       s636    t597 h  
 G       s636    t536  
 B       b637    s636  
 T       t637    o588 b637  
 B       b638    t637  
 T       t638    o587 b636 b638  
 B       b639    t638  
 T       t639    o587 b632 b639  
 B       b640    t639  
 T       t640    o587 b600 b640  
 B       b641    t640  
 T       t641    o587 b598 b641  
 B       b642    t641  
 T       t642    o587 b595 b642  
 B       b643    t642  
 T       t643    o587 b593 b643  
 B       b644    t643  
 T       t644    o b635 b4  
 B       b645    t644  
 T       t645    o b631 b645  
 B       b646    t645  
 T       t646    o b599 b646  
1718  B       b647    t646  B       b647    t646
1719  T       t647    o b597 b647  S       s647    t620 h
1720  B       b648    t647  G       s647    t558
1721  T       t648    o b594 b648  B       b648    s647
1722    T       t648    o611 b648
1723  B       b649    t648  B       b649    t648
1724  T       t649    o b592 b649  S       s649    t620 h
1725  B       b650    t649  G       s649    t561
1726  T       t650    o611 b637 b650  B       b650    s649
1727    T       t650    o611 b650
1728  B       b651    t650  B       b651    t650
1729  T       t651    o610 b651 b4 b616  H       h651    a t562
1730  B       b652    t651  H       h652    b t562
1731  T       t652    o609 b652 b4  H       h653    x t566
1732  B       b653    t652  H       h654    y t568
1733  T       t653    o607 b608 b653 b4 b4  S       s654    t620 h h651 h652 h653 h654
1734  B       b654    t653  G       s654    t571
1735  T       t654    o606 b654  B       b654    s654
1736    T       t654    o611 b654
1737  B       b655    t654  B       b655    t654
1738  P       p657    Number 1261  H       h655    x t577
1739  P       p472    Number 1713  S       s655    t620 h h651 h652 h655
1740  O       o473    location p657 p472  G       s655    t579
1741  P       p473    Number 1291  B       b656    s655
1742  P       p474    Number 1299  T       t656    o611 b656
1743  O       o474    resource_defs p473 p474 p300  B       b657    t656
1744  P       p475    Number 1297  S       s657    t620 h
1745  O       o475    uid p475 p474  G       s657    t551
1746  T       t479    o475 b623  B       b658    s657
1747  B       b479    t479  T       t658    o611 b658
1748  T       t480    o b479 b4  B       b659    t658
1749  B       b480    t480  T       t659    o610 b657 b659
1750  T       t488    o474 b480  B       b660    t659
1751  B       b488    t488  T       t660    o610 b655 b660
1752  T       t489    o b488 b4  B       b661    t660
1753  B       b489    t489  T       t661    o610 b651 b661
1754  T       t495    o631 b587 b644 b655 b489  B       b662    t661
1755  B       b495    t495  T       t662    o610 b649 b662
1756  T       t496    o473 b495  B       b663    t662
1757  B       b496    t496  T       t663    o610 b647 b663
1758  P       p496    Number 1715  B       b664    t663
1759  P       p497    Number 2239  T       t664    o610 b618 b664
1760  O       o498    location p496 p497  B       b665    t664
1761  P       p664    String subgroup_equiv_elim  T       t665    o610 b616 b665
1762  O       o664    rule p664  B       b666    t665
1763  P       p665    String J  T       t666    o b656 b4
1764  O       o665    context_param p665  B       b667    t666
1765  T       t665    o665  T       t667    o b654 b667
1766  B       b665    t665  B       b668    t667
1767  NSummary!term_param     term_param      term_param Summary  T       t668    o b650 b668
1768  O       o666    term_param  B       b669    t668
1769  T       t666    o666 b535  T       t669    o b648 b669
1770  B       b666    t666  B       b670    t669
1771  T       t667    o b666 b4  T       t670    o b646 b670
1772  B       b667    t667  B       b671    t670
1773  T       t668    o b665 b667  T       t671    o b617 b671
1774  B       b668    t668  B       b672    t671
1775  T       t669    o b586 b668  T       t672    o b615 b672
1776  B       b669    t669  B       b673    t672
1777  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL  T       t673    o629 b658 b673
1778  NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv  B       b674    t673
1779  O       o669    equiv  T       t674    o628 b674 b4 b632
 P       p669    Var R  
 O       o670    var p669  
 T       t670    o670  
 B       b670    t670  
 T       t671    o669 b545 b670  
 H       h671    x t671  
 P       p671    Var x  
 O       o671    var p671  
 T       t672    o671  
 C       h672    J t672  
 S       s672    t590 h h671 h672  
 G       s672    t592  
 B       b672    s672  
 T       t673    o588 b672  
 B       b673    t673  
 S       s673    t590 h h671 h672  
 G       s673    t594  
 B       b674    s673  
 T       t674    o588 b674  
1780  B       b675    t674  B       b675    t674
1781  NCzf_itt_set!isset      isset   isset Czf_itt_set  T       t675    o627 b675 b4
1782  O       o675    isset  B       b676    t675
1783  T       t675    o675 b670  T       t676    o625 b626 b676 b4 b4
 S       s675    t590 h h671 h672  
 G       s675    t675  
 B       b676    s675  
 T       t676    o588 b676  
1784  B       b677    t676  B       b677    t676
1785  S       s677    t597 h h671 h672  T       t677    o624 b677
1786  G       s677    t536  B       b678    t677
1787  B       b678    s677  P       p678    Number 1304
1788  T       t678    o588 b678  P       p679    Number 1312
1789  B       b679    t678  O       o679    resource_defs p678 p679 p300
1790  T       t679    o669 b544 b670  P       p680    Number 1310
1791  H       h679    y t679  O       o680    uid p680 p679
1792  P       p679    Var C  T       t680    o680 b639
1793  O       o679    var p679  B       b680    t680
1794  B       b680    t672  T       t681    o b680 b4
1795  T       t680    o679 b680  B       b681    t681
1796  S       s680    t597 h h671 h672 h679  T       t682    o679 b681
1797  G       s680    t680  B       b682    t682
1798  B       b681    s680  T       t683    o b682 b4
1799  T       t681    o588 b681  B       b683    t683
1800  B       b682    t681  T       t684    o646 b610 b666 b678 b683
1801  S       s682    t597 h h671 h672  B       b684    t684
1802  G       s682    t680  T       t685    o645 b684
1803  B       b683    s682  B       b685    t685
1804  T       t683    o588 b683  P       p685    Number 1844
1805  B       b684    t683  P       p686    Number 2083
1806  T       t684    o587 b682 b684  O       o686    location p685 p686
1807  B       b685    t684  P       p687    String subgroup_equiv
1808  T       t685    o587 b679 b685  O       o687    rule p687
1809  B       b686    t685  T       t687    o575 b559 b578
1810  T       t686    o587 b677 b686  S       s687    t620 h
1811  B       b687    t686  G       s687    t687
1812  T       t687    o587 b675 b687  B       b687    s687
1813  B       b688    t687  T       t688    o611 b687
1814  T       t688    o587 b673 b688  B       b688    t688
1815  B       b689    t688  T       t689    o610 b659 b688
1816  P       p689    String "assertT << equiv{car{'s}; 'R} >> ttca thenT assertAtT 1 << subgroup{'g; 's} >> ttca"  B       b689    t689
1817  O       o689    ext_rule p689  T       t690    o610 b618 b689
1818  T       t689    o b681 b4  B       b690    t690
1819  B       b690    t689  T       t691    o610 b616 b690
1820  T       t690    o b678 b690  B       b691    t691
1821  B       b691    t690  P       p691    String "assumT 3 thenT rwh unfold_subgroup 2 thenT autoT"
1822  T       t691    o b676 b691  O       o691    ext_rule p691
1823  B       b692    t691  T       t692    o b658 b4
1824  T       t692    o b674 b692  B       b692    t692
1825  B       b693    t692  T       t693    o b617 b692
1826  T       t693    o b672 b693  B       b693    t693
1827  B       b694    t693  T       t694    o b615 b693
1828  T       t694    o611 b683 b694  B       b694    t694
1829  B       b695    t694  T       t695    o629 b687 b694
1830  T       t695    o610 b695 b4 b616  B       b695    t695
1831  B       b696    t695  T       t696    o628 b695 b4 b632
1832  H       h696    v t536  B       b696    t696
1833  S       s696    t597 h h696 h671 h672  H       h696    y t557
1834  G       s696    t679  H       h697    y_1 t558
1835  B       b697    s696  H       h698    y_2 t561
1836  T       t697    o611 b697 b694  H       h699    y_3 t575
1837  B       b698    t697  H       h700    z_1 t582
1838  P       p698    String assertion  H       h701    c t562
1839  O       o698    tactic_arg p698  H       h702    x t568
1840  S       s698    t597 h h671 h672  P       p702    Var c
1841  G       s698    t679  O       o702    var p702
1842  B       b699    s698  T       t702    o702
1843  T       t699    o611 b699 b694  B       b702    t702
1844  B       b700    t699  T       t703    o564 b702 b559
1845  T       t700    o2 b696  H       h703    y t703
1846  B       b701    t700  T       t704    o575 b559 b578 b567 b702
1847  T       t701    o698 b700 b4 b701  H       h704    u t704
1848  B       b702    t701  T       t705    o575 b559 b578 b702 b567
1849  T       t702    o2 b702  S       s705    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704
1850  B       b703    t702  G       s705    t705
1851  T       t703    o610 b698 b4 b703  B       b705    s705
1852  B       b704    t703  T       t706    o629 b705 b694
1853  T       t704    o b704 b4  B       b706    t706
1854  B       b705    t704  S       s706    t620 h h696 h697 h698 h699 h700
1855  T       t705    o609 b696 b705  G       s706    t687
1856  B       b706    t705  B       b707    s706
1857  P       p706    String "dT 0 thenT autoT thenT rwh unfold_subgroup 2 thenT autoT"  T       t707    o629 b707 b694
1858  O       o706    ext_rule p706  B       b708    t707
1859  H       h706    y_1 t542  NSummary!arg_named      arg_named       arg_named Summary
1860  H       h707    y_2 t543  P       p708    String d_auto
1861  H       h708    y_3 t546  O       o708    arg_named p708
1862  H       h709    z t560  NSummary!arg_bool       arg_bool        arg_bool Summary
1863  H       h710    c t547  P       p709    String true
1864  H       h711    x t553  O       o709    arg_bool p709
1865  P       p711    Var c  T       t709    o709
1866  O       o711    var p711  B       b709    t709
1867  T       t711    o711  T       t710    o708 b709
1868    B       b710    t710
1869    T       t711    o b710 b4
1870  B       b711    t711  B       b711    t711
1871  T       t712    o549 b711 b544  H       h711    z t583
1872  H       h712    y t712  S       s711    t620 h h696 h697 h698 h711
1873  T       t713    o669 b544 b670 b552 b711  G       s711    t687
1874  H       h713    u t713  B       b712    s711
1875  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL  T       t712    o629 b712 b694
1876  NCzf_itt_pair!pair      pair    pair Czf_itt_pair  B       b713    t712
1877  O       o713    pair  H       h713    z_1 t584
1878  T       t714    o713 b711 b552  S       s713    t620 h h696 h697 h713
1879  B       b714    t714  G       s713    t687
1880  T       t715    o549 b714 b670  B       b714    s713
1881  S       s715    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713  T       t714    o629 b714 b694
1882  G       s715    t715  B       b715    t714
1883  B       b715    s715  H       h715    z t585
1884  T       t716    o611 b715 b694  S       s715    t620 h h696 h715
1885  B       b716    t716  G       s715    t687
1886  H       h716    z_1 t561  B       b716    s715
1887  S       s716    t597 h h706 h707 h716 h671 h672 h633 h710 h711 h712 h713  T       t716    o629 b716 b694
1888  G       s716    t715  B       b717    t716
1889  B       b717    s716  H       h717    v t586
1890  T       t717    o611 b717 b694  S       s717    t620 h h717
1891  B       b718    t717  G       s717    t687
1892  H       h718    z t562  B       b718    s717
1893  S       s718    t597 h h706 h718 h671 h672 h633 h710 h711 h712 h713  T       t718    o629 b718 b694
1894  G       s718    t715  B       b719    t718
1895  B       b719    s718  H       h719    v t551
1896  T       t719    o611 b719 b694  S       s719    t620 h h719
1897  B       b720    t719  G       s719    t687
1898  H       h720    v t563  B       b720    s719
1899  S       s720    t597 h h720 h671 h672 h633 h710 h711 h712 h713  T       t720    o629 b720 b694
1900  G       s720    t715  B       b721    t720
1901  B       b721    s720  T       t721    o2 b696
 T       t721    o611 b721 b694  
1902  B       b722    t721  B       b722    t721
1903  S       s722    t597 h h696 h671 h672 h633 h710 h711 h712 h713  T       t722    o628 b721 b4 b722
1904  G       s722    t715  B       b723    t722
1905  B       b723    s722  T       t723    o2 b723
 T       t723    o611 b723 b694  
1906  B       b724    t723  B       b724    t723
1907  T       t724    o669 b544 b670 b711 b552  T       t724    o628 b719 b4 b724
1908  S       s724    t597 h h696 h671 h672 h633 h710 h711 h712 h713  B       b725    t724
1909  G       s724    t724  T       t725    o2 b725
 B       b725    s724  
 T       t725    o611 b725 b694  
1910  B       b726    t725  B       b726    t725
1911  NSummary!arg_named      arg_named       arg_named Summary  T       t726    o628 b717 b4 b726
1912  P       p726    String d_auto  B       b727    t726
1913  O       o726    arg_named p726  T       t727    o2 b727
1914  NSummary!arg_bool       arg_bool        arg_bool Summary  B       b728    t727
1915  P       p727    String true  T       t728    o628 b715 b4 b728
1916  O       o727    arg_bool p727  B       b729    t728
1917  T       t727    o727  T       t729    o2 b729
1918  B       b727    t727  B       b730    t729
1919  T       t728    o726 b727  T       t730    o628 b713 b4 b730
1920  B       b728    t728  B       b731    t730
1921  T       t729    o b728 b4  T       t731    o2 b731
1922  B       b729    t729  B       b732    t731
1923  T       t730    o2 b704  T       t732    o628 b708 b711 b732
1924  B       b730    t730  B       b733    t732
1925  T       t731    o610 b726 b729 b730  T       t733    o2 b733
1926  B       b731    t731  B       b734    t733
1927  T       t732    o2 b731  T       t734    o628 b706 b4 b734
1928  B       b732    t732  B       b735    t734
1929  T       t733    o610 b724 b4 b732  H       h735    d t562
1930  B       b733    t733  H       h736    e t562
1931  T       t734    o2 b733  H       h737    f t562
1932  B       b734    t734  P       p737    Var d
1933  T       t735    o610 b722 b4 b734  O       o737    var p737
1934  B       b735    t735  T       t737    o737
 T       t736    o2 b735  
 B       b736    t736  
 T       t737    o610 b720 b4 b736  
1935  B       b737    t737  B       b737    t737
1936  T       t738    o2 b737  T       t738    o564 b737 b559
1937  B       b738    t738  H       h738    x t738
1938  T       t739    o610 b718 b4 b738  P       p738    Var e
1939    O       o738    var p738
1940    T       t739    o738
1941  B       b739    t739  B       b739    t739
1942  T       t740    o2 b739  T       t740    o564 b739 b559
1943  B       b740    t740  H       h740    y t740
1944  T       t741    o610 b716 b4 b740  P       p740    Var f
1945    O       o740    var p740
1946    T       t741    o740
1947  B       b741    t741  B       b741    t741
1948  H       h741    z_1 t560  T       t742    o564 b741 b559
1949  H       h742    d t547  H       h742    z t742
1950  H       h743    e t547  T       t743    o575 b559 b578 b737 b739
1951  H       h744    f t547  H       h743    u t743
1952  P       p744    Var d  T       t744    o575 b559 b578 b739 b741
1953  O       o744    var p744  H       h744    v t744
1954  T       t744    o744  T       t745    o575 b559 b578 b737 b741
1955  B       b744    t744  S       s745    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744
1956  T       t745    o549 b744 b544  G       s745    t745
1957  H       h745    x t745  B       b745    s745
1958  P       p745    Var e  T       t746    o629 b745 b694
 O       o745    var p745  
 T       t746    o745  
1959  B       b746    t746  B       b746    t746
1960  T       t747    o549 b746 b544  T       t747    o628 b746 b4 b734
1961  H       h747    y t747  B       b747    t747
1962  P       p747    Var f  T       t748    o b747 b4
 O       o747    var p747  
 T       t748    o747  
1963  B       b748    t748  B       b748    t748
1964  T       t749    o549 b748 b544  T       t749    o b735 b748
1965  H       h749    z t749  B       b749    t749
1966  T       t750    o669 b544 b670 b744 b746  T       t750    o627 b696 b749
1967  H       h750    u t750  B       b750    t750
1968  T       t751    o669 b544 b670 b746 b748  P       p750    String "assertT << equiv{car{'g}; eqG{'g}; 'b; 'c} >> thenT autoT"
1969  H       h751    v t751  O       o750    ext_rule p750
1970  T       t752    o713 b744 b748  P       p751    String assertion
1971    O       o751    tactic_arg p751
1972    T       t751    o575 b560 b578 b567 b702
1973    S       s751    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704
1974    G       s751    t751
1975    B       b751    s751
1976    T       t752    o629 b751 b694
1977  B       b752    t752  B       b752    t752
1978  T       t753    o549 b752 b670  T       t753    o2 b735
1979  S       s753    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751  B       b753    t753
1980  G       s753    t753  T       t754    o751 b752 b4 b753
 B       b753    s753  
 T       t754    o611 b753 b694  
1981  B       b754    t754  B       b754    t754
1982  H       h754    z_2 t561  H       h754    v t751
1983  S       s754    t597 h h706 h707 h754 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751  S       s754    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754
1984  G       s754    t753  G       s754    t705
1985  B       b755    s754  B       b755    s754
1986  T       t755    o611 b755 b694  T       t755    o629 b755 b694
1987  B       b756    t755  B       b756    t755
1988  H       h756    z_1 t562  T       t756    o628 b756 b4 b753
1989  S       s756    t597 h h706 h756 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751  B       b757    t756
1990  G       s756    t753  T       t757    o b757 b4
 B       b757    s756  
 T       t757    o611 b757 b694  
1991  B       b758    t757  B       b758    t757
1992  S       s758    t597 h h720 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751  T       t758    o b754 b758
1993  G       s758    t753  B       b759    t758
1994  B       b759    s758  T       t759    o627 b735 b759
 T       t759    o611 b759 b694  
1995  B       b760    t759  B       b760    t759
1996  S       s760    t597 h h696 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751  P       p760    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 11 thenT autoT"
1997  G       s760    t753  O       o760    ext_rule p760
1998  B       b761    s760  NCzf_itt_set!isset      isset   isset Czf_itt_set
1999  T       t761    o611 b761 b694  O       o761    isset
2000  B       b762    t761  T       t761    o761 b559
2001  T       t762    o669 b544 b670 b744 b748  H       h761    y_6 t761
2002  S       s762    t597 h h696 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751  T       t762    o761 b578
2003  G       s762    t762  H       h762    y_5 t762
2004  B       b763    s762  T       t763    o761 b567
2005  T       t763    o611 b763 b694  H       h763    y_7 t763
2006  B       b764    t763  T       t764    o761 b702
2007  T       t764    o610 b764 b729 b730  H       h764    z_2 t764
2008  B       b765    t764  H       h765    y_4 t568
2009  T       t765    o2 b765  H       h766    z_3 t703
2010  B       b766    t765  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL
2011  T       t766    o610 b762 b4 b766  NCzf_itt_pair!pair      pair    pair Czf_itt_pair
2012  B       b767    t766  O       o766    pair
2013  T       t767    o2 b767  T       t766    o766 b567 b702
2014  B       b768    t767  B       b766    t766
2015  T       t768    o610 b760 b4 b768  T       t767    o564 b766 b578
2016  B       b769    t768  H       h767    z t767
2017  T       t769    o2 b769  T       t768    o564 b567 b560
2018  B       b770    t769  S       s768    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767
2019  T       t770    o610 b758 b4 b770  G       s768    t768
2020    B       b768    s768
2021    T       t769    o629 b768 b694
2022    B       b769    t769
2023    B       b770    t768
2024    T       t770    o564 b702 b560
2025  B       b771    t770  B       b771    t770
2026  T       t771    o2 b771  T       t771    o556 b770 b771
2027  B       b772    t771  S       s771    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767
2028  T       t772    o610 b756 b4 b772  G       s771    t771
2029    B       b772    s771
2030    T       t772    o629 b772 b694
2031  B       b773    t772  B       b773    t772
2032  T       t773    o2 b773  T       t773    o761 b560
2033  B       b774    t773  B       b774    t773
2034  T       t774    o610 b754 b4 b774  B       b775    t762
2035  B       b775    t774  B       b776    t763
2036  T       t775    o b775 b4  B       b777    t764
2037  B       b776    t775  T       t777    o556 b776 b777
 T       t776    o b741 b776  
 B       b777    t776  
 T       t777    o609 b704 b777  
2038  B       b778    t777  B       b778    t777
2039  P       p778    String "assertT << equiv{car{'g}; 'R; 'b; 'c} >> thenT autoT"  T       t778    o556 b775 b778
2040  O       o778    ext_rule p778  B       b779    t778
2041  T       t778    o549 b552 b545  T       t779    o556 b774 b779
 S       s778    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713  
 G       s778    t778  
 B       b779    s778  
 T       t779    o611 b779 b694  
2042  B       b780    t779  B       b780    t779
2043  T       t780    o669 b545 b670 b552 b711  B       b781    t771
2044  S       s780    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713  T       t781    o556 b780 b781
2045  G       s780    t780  S       s781    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767
2046  B       b781    s780  G       s781    t781
2047  T       t781    o611 b781 b694  B       b782    s781
2048  B       b782    t781  T       t782    o629 b782 b694
 T       t782    o2 b741  
2049  B       b783    t782  B       b783    t782
2050  T       t783    o698 b782 b729 b783  B       b784    t781
2051  B       b784    t783  B       b785    t767
2052  T       t784    o2 b784  T       t785    o556 b784 b785
2053  B       b785    t784  S       s785    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767
2054  T       t785    o698 b780 b4 b785  G       s785    t785
2055  B       b786    t785  B       b786    s785
2056  T       t786    o549 b711 b545  T       t786    o629 b786 b694
2057  S       s786    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713  B       b787    t786
2058  G       s786    t786  H       h787    z_4 t777
2059  B       b787    s786  S       s787    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h787 h765 h766 h767
2060  T       t787    o611 b787 b694  G       s787    t785
2061  B       b788    t787  B       b788    s787
2062  T       t788    o698 b788 b4 b785  T       t788    o629 b788 b694
2063  B       b789    t788  B       b789    t788
2064  T       t789    o713 b552 b711  H       h789    z_2 t778
2065  B       b790    t789  S       s789    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h789 h765 h766 h767
2066  T       t790    o549 b790 b670  G       s789    t785
2067  S       s790    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713  B       b790    s789
2068  G       s790    t790  T       t790    o629 b790 b694
2069  B       b791    s790  B       b791    t790
2070  T       t791    o611 b791 b694  B       b792    t761
2071  B       b792    t791  T       t792    o556 b792 b779
2072  T       t792    o698 b792 b4 b785  H       h792    y_5 t792
2073  B       b793    t792  S       s792    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h792 h765 h766 h767
2074  H       h793    v t780  G       s792    t785
2075  S       s793    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713 h793  B       b793    s792
2076  G       s793    t715  T       t793    o629 b793 b694
2077  B       b794    s793  B       b794    t793
2078  T       t794    o611 b794 b694  B       b795    t703
2079  B       b795    t794  T       t795    o556 b568 b795
2080  T       t795    o610 b795 b4 b783  H       h795    z_2 t795
2081  B       b796    t795  S       s795    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h792 h795 h767
2082  T       t796    o b796 b4  G       s795    t785
2083    B       b796    s795
2084    T       t796    o629 b796 b694
2085  B       b797    t796  B       b797    t796
2086  T       t797    o b793 b797  B       b798    t792
2087  B       b798    t797  B       b799    t795
2088  T       t798    o b789 b798  T       t799    o556 b798 b799
2089  B       b799    t798  H       h799    y_4 t799
2090  T       t799    o b786 b799  S       s799    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h799 h767
2091  B       b800    t799  G       s799    t785
2092  T       t800    o609 b741 b800  B       b800    s799
2093    T       t800    o629 b800 b694
2094  B       b801    t800  B       b801    t800
2095  P       p801    String "withT << 'b >> (dT 4) ttca"  B       b802    t799
2096  O       o801    ext_rule p801  T       t802    o556 b802 b785
2097  T       t801    o609 b786 b4  H       h802    u t802
2098  B       b802    t801  S       s802    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h802
2099  T       t802    o801 b608 b802 b4 b4  G       s802    t785
2100  B       b803    t802  B       b803    s802
2101  P       p803    String "withT << 'c >> (dT 4) ttca"  T       t803    o629 b803 b694
 O       o803    ext_rule p803  
 T       t803    o609 b789 b4  
2102  B       b804    t803  B       b804    t803
2103  T       t804    o803 b608 b804 b4 b4  S       s804    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704
2104  B       b805    t804  G       s804    t785
2105  P       p805    String "rwh unfold_equiv 12 ttca"  B       b805    s804
2106  O       o805    ext_rule p805  T       t805    o629 b805 b694
 T       t805    o609 b793 b4  
2107  B       b806    t805  B       b806    t805
2108  T       t806    o805 b608 b806 b4 b4  T       t806    o2 b754
2109  B       b807    t806  B       b807    t806
2110  P       p807    String "equivSymT 13 ttca"  T       t807    o751 b806 b4 b807
2111  O       o807    ext_rule p807  B       b808    t807
2112  S       s807    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713 h793  T       t808    o2 b808
 G       s807    t778  
 B       b808    s807  
 T       t808    o611 b808 b694  
2113  B       b809    t808  B       b809    t808
2114  T       t809    o2 b796  T       t809    o751 b804 b4 b809
2115  B       b810    t809  B       b810    t809
2116  T       t810    o610 b809 b4 b810  T       t810    o2 b810
2117  B       b811    t810  B       b811    t810
2118  S       s811    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713 h793  T       t811    o628 b801 b4 b811
2119  G       s811    t786  B       b812    t811
2120  B       b812    s811  T       t812    o2 b812
 T       t812    o611 b812 b694  
2121  B       b813    t812  B       b813    t812
2122  T       t813    o610 b813 b4 b810  T       t813    o628 b797 b4 b813
2123  B       b814    t813  B       b814    t813
2124  T       t814    o669 b545 b670 b711 b552  T       t814    o2 b814
2125  H       h814    u_1 t814  B       b815    t814
2126  S       s814    t597 h h706 h707 h708 h709 h671 h672 h633 h710 h711 h712 h713 h793 h814  T       t815    o628 b794 b4 b815
 G       s814    t715  
 B       b815    s814  
 T       t815    o611 b815 b694  
2127  B       b816    t815  B       b816    t815
2128  T       t816    o610 b816 b4 b810  T       t816    o2 b816
2129  B       b817    t816  B       b817    t816
2130  T       t817    o b817 b4  T       t817    o628 b791 b4 b817
2131  B       b818    t817  B       b818    t817
2132  T       t818    o b814 b818  T       t818    o2 b818
2133  B       b819    t818  B       b819    t818
2134  T       t819    o b811 b819  T       t819    o628 b789 b4 b819
2135  B       b820    t819  B       b820    t819
2136  T       t820    o609 b796 b820  T       t820    o2 b820
2137  B       b821    t820  B       b821    t820
2138  T       t821    o609 b811 b4  T       t821    o628 b787 b711 b821
2139  B       b822    t821  B       b822    t821
2140  T       t822    o801 b608 b822 b4 b4  T       t822    o2 b822
2141  B       b823    t822  B       b823    t822
2142  T       t823    o609 b814 b4  T       t823    o628 b783 b711 b823
2143  B       b824    t823  B       b824    t823
2144  T       t824    o803 b608 b824 b4 b4  T       t824    o2 b824
2145  B       b825    t824  B       b825    t824
2146  P       p825    String "rwh unfold_equiv 14 ttca"  T       t825    o628 b773 b711 b825
 O       o825    ext_rule p825  
 T       t825    o609 b817 b4  
2147  B       b826    t825  B       b826    t825
2148  T       t826    o825 b608 b826 b4 b4  T       t826    o2 b826
2149  B       b827    t826  B       b827    t826
2150  T       t827    o b827 b4  T       t827    o628 b769 b4 b827
2151  B       b828    t827  B       b828    t827
2152  T       t828    o b825 b828  S       s828    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767
2153  B       b829    t828  G       s828    t770
2154  T       t829    o b823 b829  B       b829    s828
2155    T       t829    o629 b829 b694
2156  B       b830    t829  B       b830    t829
2157  T       t830    o807 b608 b821 b830 b4  T       t830    o628 b830 b4 b827
2158  B       b831    t830  B       b831    t830
2159  T       t831    o b831 b4  T       t831    o b831 b4
2160  B       b832    t831  B       b832    t831
2161  T       t832    o b807 b832  T       t832    o b828 b832
2162  B       b833    t832  B       b833    t832
2163  T       t833    o b805 b833  T       t833    o627 b754 b833
2164  B       b834    t833  B       b834    t833
2165  T       t834    o b803 b834  P       p834    String "withT << 'b >> (dT 4) ttca"
2166    O       o834    ext_rule p834
2167    T       t834    o627 b828 b4
2168  B       b835    t834  B       b835    t834
2169  T       t835    o778 b608 b801 b835 b4  T       t835    o834 b626 b835 b4 b4
2170  B       b836    t835  B       b836    t835
2171  P       p836    String "assertT << mem{'d; car{'g}} >> ttca"  P       p836    String "withT << 'c >> (dT 4) ttca"
2172  O       o836    ext_rule p836  O       o836    ext_rule p836
2173  T       t836    o549 b744 b545  T       t836    o627 b831 b4
2174  S       s836    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751  B       b837    t836
2175  G       s836    t836  T       t837    o836 b626 b837 b4 b4
 B       b837    s836  
 T       t837    o611 b837 b694  
2176  B       b838    t837  B       b838    t837
2177  T       t838    o2 b775  T       t838    o b838 b4
2178  B       b839    t838  B       b839    t838
2179  T       t839    o698 b838 b4 b839  T       t839    o b836 b839
2180  B       b840    t839  B       b840    t839
2181  H       h840    v_1 t836  T       t840    o760 b626 b834 b840 b4
2182  S       s840    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751 h840  B       b841    t840
2183  G       s840    t753  P       p841    String "assertT << equiv{car{'g}; eqG{'g}; 'c; 'b} >> thenT autoT"
2184  B       b841    s840  O       o841    ext_rule p841
2185  T       t841    o611 b841 b694  T       t841    o575 b560 b578 b702 b567
2186  B       b842    t841  S       s841    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754
2187  T       t842    o610 b842 b4 b839  G       s841    t841
2188    B       b842    s841
2189    T       t842    o629 b842 b694
2190  B       b843    t842  B       b843    t842
2191  T       t843    o b843 b4  T       t843    o2 b757
2192  B       b844    t843  B       b844    t843
2193  T       t844    o b840 b844  T       t844    o751 b843 b4 b844
2194  B       b845    t844  B       b845    t844
2195  T       t845    o609 b775 b845  H       h845    v_1 t841
2196  B       b846    t845  S       s845    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754 h845
2197  P       p846    String "withT << 'd >> (dT 4) ttca"  G       s845    t705
2198  O       o846    ext_rule p846  B       b846    s845
2199  T       t846    o609 b840 b4  T       t846    o629 b846 b694
2200  B       b847    t846  B       b847    t846
2201  T       t847    o846 b608 b847 b4 b4  T       t847    o628 b847 b4 b844
2202  B       b848    t847  B       b848    t847
2203  P       p848    String "assertT << mem{'e; car{'g}} >> ttca"  T       t848    o b848 b4
2204  O       o848    ext_rule p848  B       b849    t848
2205  T       t848    o549 b746 b545  T       t849    o b845 b849
 S       s848    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751 h840  
 G       s848    t848  
 B       b849    s848  
 T       t849    o611 b849 b694  
2206  B       b850    t849  B       b850    t849
2207  T       t850    o2 b843  T       t850    o627 b757 b850
2208  B       b851    t850  B       b851    t850
2209  T       t851    o698 b850 b4 b851  P       p851    String "equivSymT ttca"
2210  B       b852    t851  O       o851    ext_rule p851
2211  H       h852    v_2 t848  S       s851    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754
2212  S       s852    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751 h840 h852  G       s851    t768
2213  G       s852    t753  B       b852    s851
2214  B       b853    s852  T       t852    o629 b852 b694
2215  T       t853    o611 b853 b694  B       b853    t852
2216    T       t853    o2 b845
2217  B       b854    t853  B       b854    t853
2218  T       t854    o610 b854 b4 b851  T       t854    o751 b853 b4 b854
2219  B       b855    t854  B       b855    t854
2220  T       t855    o b855 b4  S       s855    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754
2221  B       b856    t855  G       s855    t770
2222  T       t856    o b852 b856  B       b856    s855
2223    T       t856    o629 b856 b694
2224  B       b857    t856  B       b857    t856
2225  T       t857    o609 b843 b857  T       t857    o751 b857 b4 b854
2226  B       b858    t857  B       b858    t857
2227  P       p858    String "withT << 'e >> (dT 4) ttca"  T       t858    o b858 b4
 O       o858    ext_rule p858  
 T       t858    o609 b852 b4  
2228  B       b859    t858  B       b859    t858
2229  T       t859    o858 b608 b859 b4 b4  T       t859    o b855 b859
2230  B       b860    t859  B       b860    t859
2231  P       p860    String "assertT << mem{'f; car{'g}} >> ttca"  T       t860    o627 b845 b860
2232  O       o860    ext_rule p860  B       b861    t860
2233  T       t860    o549 b748 b545  T       t861    o627 b855 b4
 S       s860    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751 h840 h852  
 G       s860    t860  
 B       b861    s860  
 T       t861    o611 b861 b694  
2234  B       b862    t861  B       b862    t861
2235  T       t862    o2 b855  T       t862    o834 b626 b862 b4 b4
2236  B       b863    t862  B       b863    t862
2237  T       t863    o698 b862 b4 b863  T       t863    o627 b858 b4
2238  B       b864    t863  B       b864    t863
2239  H       h864    v_3 t860  T       t864    o836 b626 b864 b4 b4
2240  S       s864    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751 h840 h852 h864  B       b865    t864
2241  G       s864    t753  T       t865    o b865 b4
 B       b865    s864  
 T       t865    o611 b865 b694  
2242  B       b866    t865  B       b866    t865
2243  T       t866    o610 b866 b4 b863  T       t866    o b863 b866
2244  B       b867    t866  B       b867    t866
2245  T       t867    o b867 b4  T       t867    o851 b626 b861 b867 b4
2246  B       b868    t867  B       b868    t867
2247  T       t868    o b864 b868  P       p868    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 13 thenT autoT"
2248    O       o868    ext_rule p868
2249    T       t868    o627 b848 b4
2250  B       b869    t868  B       b869    t868
2251  T       t869    o609 b855 b869  T       t869    o868 b626 b869 b4 b4
2252  B       b870    t869  B       b870    t869
2253  P       p870    String "withT << 'f >> (dT 4) ttca"  T       t870    o b870 b4
 O       o870    ext_rule p870  
 T       t870    o609 b864 b4  
2254  B       b871    t870  B       b871    t870
2255  T       t871    o870 b608 b871 b4 b4  T       t871    o b868 b871
2256  B       b872    t871  B       b872    t871
2257  P       p872    String "assertT << equiv{car{'g}; 'R; 'd; 'e} >> thenT autoT thenT rwh unfold_equiv 14 ttca"  T       t872    o841 b626 b851 b872 b4
 O       o872    ext_rule p872  
 T       t872    o675 b544  
2258  B       b873    t872  B       b873    t872
2259  B       b874    t675  T       t873    o b873 b4
2260  T       t874    o675 b744  B       b874    t873
2261    T       t874    o b841 b874
2262  B       b875    t874  B       b875    t874
2263  T       t875    o675 b746  T       t875    o750 b626 b760 b875 b4
2264  B       b876    t875  B       b876    t875
2265  T       t876    o541 b875 b876  P       p876    String "withT << 'd >> (dT 4) ttca thenT withT << 'e >> (dT 4) ttca thenT withT << 'f >> (dT 4) ttca"
2266  B       b877    t876  O       o876    ext_rule p876
2267  T       t877    o541 b874 b877  T       t876    o564 b737 b560
2268  B       b878    t877  H       h876    z_2 t876
2269  T       t878    o541 b873 b878  T       t877    o564 b739 b560
2270  B       b879    t878  H       h877    z_3 t877
2271  B       b880    t745  T       t878    o564 b741 b560
2272  B       b881    t747  H       h878    z_4 t878
2273  T       t881    o541 b880 b881  S       s878    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878
2274  B       b882    t881  G       s878    t745
2275  T       t882    o541 b879 b882  B       b878    s878
2276  B       b883    t882  T       t879    o629 b878 b694
2277  T       t883    o713 b744 b746  B       b879    t879
2278  B       b884    t883  S       s879    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877
2279  T       t884    o549 b884 b670  G       s879    t745
2280  B       b885    t884  B       b880    s879
2281  T       t885    o541 b883 b885  T       t880    o629 b880 b694
2282  H       h885    u t885  B       b881    t880
2283  T       t886    o669 b545 b670 b744 b746  P       p881    String with
2284  H       h886    v_4 t886  O       o881    arg_named p881
2285  S       s886    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h885 h751 h840 h852 h864 h886  NSummary!arg_term_list  arg_term_list   arg_term_list Summary
2286  G       s886    t753  O       o882    arg_term_list
2287  B       b886    s886  T       t882    o b741 b4
2288  T       t887    o611 b886 b694  B       b882    t882
2289  B       b887    t887  T       t883    o882 b882
2290  S       s887    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h750 h751 h840 h852 h864 h886  B       b883    t883
2291  G       s887    t753  T       t884    o881 b883
2292  B       b888    s887  B       b884    t884
2293  T       t888    o611 b888 b694  T       t885    o b884 b4
2294    B       b885    t885
2295    S       s885    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876
2296    G       s885    t745
2297    B       b886    s885
2298    T       t886    o629 b886 b694
2299    B       b887    t886
2300    T       t887    o b739 b4
2301    B       b888    t887
2302    T       t888    o882 b888
2303  B       b889    t888  B       b889    t888
2304  T       t889    o2 b867  T       t889    o881 b889
2305  B       b890    t889  B       b890    t889
2306  T       t890    o610 b889 b4 b890  T       t890    o b890 b4
2307  B       b891    t890  B       b891    t890
2308  T       t891    o2 b891  T       t891    o b737 b4
2309  B       b892    t891  B       b892    t891
2310  T       t892    o610 b887 b4 b892  T       t892    o882 b892
2311  B       b893    t892  B       b893    t892
2312  T       t893    o b893 b4  T       t893    o881 b893
2313  B       b894    t893  B       b894    t893
2314  T       t894    o609 b867 b894  T       t894    o b894 b4
2315  B       b895    t894  B       b895    t894
2316  P       p895    String "assertT << equiv{car{'g}; 'R; 'e; 'f} >> thenT autoT thenT rwh unfold_equiv 21 ttca"  T       t895    o628 b746 b895 b734
2317  O       o895    ext_rule p895  B       b896    t895
2318  H       h895    y_6 t872  T       t896    o2 b896
2319  H       h896    y_5 t675  B       b897    t896
2320  H       h897    y_7 t874  T       t897    o628 b887 b891 b897
2321  H       h898    z_3 t875  B       b898    t897
2322  H       h899    y_4 t745  T       t898    o2 b898
2323  H       h900    z_4 t747  B       b899    t898
2324  H       h901    z_2 t884  T       t899    o628 b881 b885 b899
2325  T       t901    o675 b748  B       b900    t899
2326  B       b901    t901  T       t900    o2 b900
2327  T       t902    o541 b876 b901  B       b901    t900
2328  B       b902    t902  T       t901    o628 b879 b4 b901
2329  T       t903    o541 b874 b902  B       b902    t901
2330  B       b903    t903  T       t902    o b902 b4
2331  T       t904    o541 b873 b903  B       b903    t902
2332  B       b904    t904  T       t903    o627 b747 b903
2333  B       b905    t749  B       b904    t903
2334  T       t905    o541 b881 b905  P       p904    String "assertT << equiv{car{'g}; eqG{'g}; 'd; 'f} >> thenT autoT"
2335    O       o904    ext_rule p904
2336    T       t904    o575 b560 b578 b737 b741
2337    S       s904    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878
2338    G       s904    t904
2339    B       b905    s904
2340    T       t905    o629 b905 b694
2341  B       b906    t905  B       b906    t905
2342  T       t906    o541 b904 b906  T       t906    o2 b902
2343  B       b907    t906  B       b907    t906
2344  T       t907    o713 b746 b748  T       t907    o751 b906 b4 b907
2345  B       b908    t907  B       b908    t907
2346  T       t908    o549 b908 b670  H       h908    v_1 t904
2347  B       b909    t908  S       s908    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878 h908
2348  T       t909    o541 b907 b909  G       s908    t745
2349  H       h909    v t909  B       b909    s908
2350  T       t910    o669 b545 b670 b746 b748  T       t909    o629 b909 b694
2351  H       h910    v_5 t910  B       b910    t909
2352  S       s910    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h895 h896 h897 h898 h899 h900 h901 h909 h840 h852 h864 h886 h910  T       t910    o628 b910 b4 b907
2353  G       s910    t753  B       b911    t910
2354  B       b910    s910  T       t911    o b911 b4
2355  T       t911    o611 b910 b694  B       b912    t911
2356  B       b911    t911  T       t912    o b908 b912
 S       s911    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h895 h896 h897 h898 h899 h900 h901 h751 h840 h852 h864 h886 h910  
 G       s911    t753  
 B       b912    s911  
 T       t912    o611 b912 b694  
2357  B       b913    t912  B       b913    t912
2358  H       h913    z_5 t876  T       t913    o627 b902 b913
2359  S       s913    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h895 h896 h913 h899 h900 h901 h751 h840 h852 h864 h886 h910  B       b914    t913
2360  G       s913    t753  P       p914    String "equivTransT << 'e >> ttca"
2361  B       b914    s913  O       o914    ext_rule p914
2362  T       t914    o611 b914 b694  T       t914    o575 b560 b578 b737 b739
2363  B       b915    t914  S       s914    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878
2364  H       h915    z_3 t877  G       s914    t914
2365  S       s915    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h895 h915 h899 h900 h901 h751 h840 h852 h864 h886 h910  B       b915    s914
2366  G       s915    t753  T       t915    o629 b915 b694
2367  B       b916    s915  B       b916    t915
2368  T       t916    o611 b916 b694  T       t916    o2 b908
2369  B       b917    t916  B       b917    t916
2370  H       h917    y_5 t878  T       t917    o751 b916 b4 b917
2371  S       s917    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h917 h899 h900 h901 h751 h840 h852 h864 h886 h910  B       b918    t917
2372  G       s917    t753  T       t918    o575 b560 b578 b739 b741
2373  B       b918    s917  S       s918    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878
2374  T       t918    o611 b918 b694  G       s918    t918
2375  B       b919    t918  B       b919    s918
2376  H       h919    z_3 t881  T       t919    o629 b919 b694
2377  S       s919    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h917 h919 h901 h751 h840 h852 h864 h886 h910  B       b920    t919
2378  G       s919    t753  T       t920    o751 b920 b4 b917
 B       b920    s919  
 T       t920    o611 b920 b694  
2379  B       b921    t920  B       b921    t920
2380  H       h921    y_4 t882  T       t921    o b921 b4
2381  S       s921    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h921 h901 h751 h840 h852 h864 h886 h910  B       b922    t921
2382  G       s921    t753  T       t922    o b918 b922
 B       b922    s921  
 T       t922    o611 b922 b694  
2383  B       b923    t922  B       b923    t922
2384  S       s923    t597 h h706 h707 h708 h741 h671 h672 h742 h743 h744 h745 h747 h749 h885 h751 h840 h852 h864 h886 h910  T       t923    o627 b908 b923
2385  G       s923    t753  B       b924    t923
2386  B       b924    s923  T       t924    o627 b918 b4
 T       t924    o611 b924 b694  
2387  B       b925    t924  B       b925    t924
2388  T       t925    o2 b893  T       t925    o868 b626 b925 b4 b4
2389  B       b926    t925  B       b926    t925
2390  T       t926    o610 b925 b4 b926  P       p926    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 14 thenT autoT"
2391    O       o926    ext_rule p926
2392    T       t926    o627 b921 b4
2393  B       b927    t926  B       b927    t926
2394  T       t927    o2 b927  T       t927    o926 b626 b927 b4 b4
2395  B       b928    t927  B       b928    t927
2396  T       t928    o610 b923 b4 b928  T       t928    o b928 b4
2397  B       b929    t928  B       b929    t928
2398  T       t929    o2 b929  T       t929    o b926 b929
2399  B       b930    t929  B       b930    t929
2400  T       t930    o610 b921 b4 b930  T       t930    o914 b626 b924 b930 b4
2401  B       b931    t930  B       b931    t930
2402  T       t931    o2 b931  P       p931    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 18 thenT autoT"
2403    O       o931    ext_rule p931
2404    T       t931    o627 b911 b4
2405  B       b932    t931  B       b932    t931
2406  T       t932    o610 b919 b4 b932  T       t932    o931 b626 b932 b4 b4
2407  B       b933    t932  B       b933    t932
2408  T       t933    o2 b933  T       t933    o b933 b4
2409  B       b934    t933  B       b934    t933
2410  T       t934    o610 b917 b4 b934  T       t934    o b931 b934
2411  B       b935    t934  B       b935    t934
2412  T       t935    o2 b935  T       t935    o904 b626 b914 b935 b4
2413  B       b936    t935  B       b936    t935
2414  T       t936    o610 b915 b4 b936  T       t936    o b936 b4
2415  B       b937    t936  B       b937    t936
2416  T       t937    o2 b937  T       t937    o876 b626 b904 b937 b4
2417  B       b938    t937  B       b938    t937
2418  T       t938    o610 b913 b4 b938  T       t938    o b938 b4
2419  B       b939    t938  B       b939    t938
2420  T       t939    o2 b939  T       t939    o b876 b939
2421  B       b940    t939  B       b940    t939
2422  T       t940    o610 b911 b4 b940  T       t940    o691 b626 b750 b940 b4
2423  B       b941    t940  B       b941    t940
2424  T       t941    o b941 b4  T       t941    o624 b941
2425  B       b942    t941  B       b942    t941
2426  T       t942    o609 b893 b942  P       p942    Number 1874
2427  B       b943    t942  P       p943    Number 1882
2428  P       p943    String "equivTransT << 'f >> 25 ttca thenT rwh unfold_equiv 27 ttca"  O       o943    resource_defs p942 p943 p300
2429  O       o943    ext_rule p943  P       p944    Number 1880
2430  T       t943    o609 b941 b4  O       o944    uid p944 p943
2431  B       b944    t943  T       t944    o944 b639
2432  T       t944    o943 b608 b944 b4 b4  B       b944    t944
2433  B       b945    t944  T       t945    o b944 b4
2434  T       t945    o b945 b4  B       b945    t945
2435  B       b946    t945  T       t946    o943 b945
2436  T       t946    o895 b608 b943 b946 b4  B       b946    t946
2437  B       b947    t946  T       t947    o b946 b4
2438  T       t947    o b947 b4  B       b947    t947
2439  B       b948    t947  T       t948    o687 b610 b691 b942 b947
2440  T       t948    o872 b608 b895 b948 b4  B       b948    t948
2441  B       b949    t948  T       t949    o686 b948
2442  T       t949    o b949 b4  B       b949    t949
2443  B       b950    t949  P       p949    Number 2085
2444  T       t950    o b872 b950  P       p950    Number 2337
2445  B       b951    t950  O       o950    location p949 p950
2446  T       t951    o860 b608 b870 b951 b4  P       p951    String subgroup_id
2447  B       b952    t951  O       o951    rule p951
2448  T       t952    o b952 b4  NCzf_itt_group!id       id      id Czf_itt_group
2449  B       b953    t952  O       o952    id
2450  T       t953    o b860 b953  T       t952    o952 b549
2451  B       b954    t953  B       b952    t952
2452  T       t954    o848 b608 b858 b954 b4  T       t953    o952 b550
2453  B       b955    t954  B       b953    t953
2454  T       t955    o b955 b4  T       t954    o575 b560 b578 b952 b953
2455  B       b956    t955  S       s954    t620 h
2456  T       t956    o b848 b956  G       s954    t954
2457  B       b957    t956  B       b954    s954
2458  T       t957    o836 b608 b846 b957 b4  T       t955    o611 b954
2459  B       b958    t957  B       b955    t955
2460  T       t958    o b958 b4  T       t956    o610 b659 b955
2461  B       b959    t958  B       b956    t956
2462  T       t959    o b836 b959  T       t957    o610 b618 b956
2463  B       b960    t959  B       b957    t957
2464  T       t960    o706 b608 b778 b960 b4  T       t958    o610 b616 b957
2465  B       b961    t960  B       b958    t958
2466  T       t961    o b961 b4  T       t959    o629 b954 b694
2467    B       b959    t959
2468    T       t960    o628 b959 b4 b632
2469    B       b960    t960
2470    S       s960    t620 h h696 h697 h698 h699 h700
2471    G       s960    t954
2472    B       b961    s960
2473    T       t961    o629 b961 b694
2474  B       b962    t961  B       b962    t961
2475  T       t962    o689 b608 b706 b962 b4  S       s962    t620 h h696 h697 h698 h711
2476  B       b963    t962  G       s962    t954
2477  T       t963    o606 b963  B       b963    s962
2478    T       t963    o629 b963 b694
2479  B       b964    t963  B       b964    t963
2480  P       p498    Number 1750  S       s964    t620 h h696 h697 h713
2481  P       p499    Number 1757  G       s964    t954
2482  O       o499    resource_defs p498 p499 p272  B       b965    s964
2483  P       p500    Number 1755  T       t965    o629 b965 b694
2484  O       o500    uid p500 p499  B       b966    t965
2485  T       t502    o500 b623  S       s966    t620 h h696 h715
2486  B       b502    t502  G       s966    t954
2487  T       t503    o b502 b4  B       b967    s966
2488  B       b503    t503  T       t967    o629 b967 b694
2489  T       t509    o499 b503  B       b968    t967
2490  B       b509    t509  S       s968    t620 h h717
2491  T       t510    o b509 b4  G       s968    t954
2492  B       b510    t510  B       b969    s968
2493  T       t517    o664 b669 b689 b964 b510  T       t969    o629 b969 b694
2494  B       b517    t517  B       b970    t969
2495  T       t518    o498 b517  S       s970    t620 h h719
2496  B       b518    t518  G       s970    t954
2497  P       p518    Number 2241  B       b971    s970
2498  P       p973    String subgroup_id  T       t971    o629 b971 b694
2499  O       o973    rule p973  B       b972    t971
2500  S       s973    t590 h  T       t972    o2 b960
2501  G       s973    t675  B       b973    t972
2502  B       b973    s973  T       t973    o628 b972 b4 b973
 T       t973    o588 b973  
2503  B       b974    t973  B       b974    t973
2504  S       s974    t597 h  T       t974    o2 b974
2505  G       s974    t671  B       b975    t974
2506  B       b975    s974  T       t975    o628 b970 b4 b975
 T       t975    o588 b975  
2507  B       b976    t975  B       b976    t975
2508  NCzf_itt_group!id       id      id Czf_itt_group  T       t976    o2 b976
 O       o976    id  
 T       t976    o976 b535  
2509  B       b977    t976  B       b977    t976
2510  T       t977    o976 b534  T       t977    o628 b968 b4 b977
2511  B       b978    t977  B       b978    t977
2512  T       t978    o669 b545 b670 b977 b978  T       t978    o2 b978
2513  S       s978    t597 h  B       b979    t978
2514  G       s978    t978  T       t979    o628 b966 b4 b979
 B       b979    s978  
 T       t979    o588 b979  
2515  B       b980    t979  B       b980    t979
2516  T       t980    o587 b976 b980  T       t980    o2 b980
2517  B       b981    t980  B       b981    t980
2518  T       t981    o587 b638 b981  T       t981    o628 b964 b4 b981
2519  B       b982    t981  B       b982    t981
2520  T       t982    o587 b974 b982  T       t982    o2 b982
2521  B       b983    t982  B       b983    t982
2522  T       t983    o587 b595 b983  T       t983    o628 b962 b4 b983
2523  B       b984    t983  B       b984    t983
2524  T       t984    o587 b593 b984  T       t984    o b984 b4
2525  B       b985    t984  B       b985    t984
2526  P       p985    String "assumT 4 thenT assumT 5 thenT rwh unfold_subgroup 2 ttca thenT dT 2 thenT dT 3 thenT dT 4 thenT instHypT [<< id{'s} >>; << id{'s} >>] 5 thenT rwh fold_isset 0 ttca"  T       t985    o627 b960 b985
 O       o985    ext_rule p985  
 T       t985    o b975 b4  
2527  B       b986    t985  B       b986    t985
2528  T       t986    o b637 b986  P       p986    String "instHypT [<< op{'s; id{'s}; id{'s}} >>; << id{'s} >>] 6 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 7 ttca"
2529    O       o986    ext_rule p986
2530    T       t986    o569 b549 b952 b952
2531  B       b987    t986  B       b987    t986
2532  T       t987    o b973 b987  T       t987    o575 b560 b578 b987 b952
2533  B       b988    t987  H       h987    y_4 t987
2534  T       t988    o b594 b988  S       s987    t620 h h696 h697 h698 h699 h700 h987
2535    G       s987    t954
2536    B       b988    s987
2537    T       t988    o629 b988 b694
2538  B       b989    t988  B       b989    t988
2539  T       t989    o b592 b989  T       t989    o575 b559 b576 b987 b952
2540  B       b990    t989  B       b990    t989
2541  T       t990    o611 b979 b990  B       b991    t987
2542  B       b991    t990  T       t991    o563 b990 b991
2543  T       t991    o610 b991 b4 b616  H       h991    w_1 t991
2544  B       b992    t991  S       s991    t620 h h696 h697 h698 h699 h700 h991 h987
2545  H       h992    y t542  G       s991    t954
2546  H       h993    y_1 t543  B       b992    s991
2547  H       h994    y_2 t546  T       t992    o629 b992 b694
2548  H       h995    v_1 t671  B       b993    t992
2549  T       t995    o549 b977 b544  S       s993    t620 h h696 h697 h698 h699 h700 h991
2550  B       b995    t995  G       s993    t954
2551  T       t996    o554 b535 b977 b977  B       b994    s993
2552  B       b996    t996  T       t994    o629 b994 b694
2553  T       t997    o554 b534 b977 b977  B       b995    t994
2554  B       b997    t997  T       t995    o575 b559 b576 b987 b567
2555  T       t998    o553 b996 b997  B       b996    t995
2556  B       b998    t998  T       t996    o575 b560 b578 b987 b567
2557  T       t999    o548 b995 b998  B       b997    t996
2558  B       b999    t999  T       t997    o563 b996 b997
2559  T       t1000   o548 b995 b999  B       b998    t997 b
2560  H       h1000   w_1 t1000  T       t998    o561 b562 b998
2561  S       s1000   t597 h h992 h993 h994 h709 h995 h1000  H       h998    w t998
2562  G       s1000   t978  S       s998    t620 h h696 h697 h698 h699 h700 h998 h991
2563  B       b1000   s1000  G       s998    t954
2564  T       t1001   o611 b1000 b990  B       b999    s998
2565    T       t999    o629 b999 b694
2566    B       b1000   t999
2567    P       p1000   String thin
2568    O       o1000   arg_named p1000
2569    P       p1001   String false
2570    O       o1001   arg_bool p1001
2571    T       t1001   o1001
2572  B       b1001   t1001  B       b1001   t1001
2573  T       t1002   o554 b535 b977 b552  T       t1002   o1000 b1001
2574  B       b1002   t1002  B       b1002   t1002
2575  T       t1003   o554 b534 b977 b552  T       t1003   o b1002 b4
2576  B       b1003   t1003  B       b1003   t1003
2577  T       t1004   o553 b1002 b1003  S       s1003   t620 h h696 h697 h698 h699 h700 h998
2578  B       b1004   t1004  G       s1003   t954
2579  T       t1005   o548 b553 b1004  B       b1004   s1003
2580  B       b1005   t1005  T       t1004   o629 b1004 b694
2581  T       t1006   o548 b995 b1005  B       b1005   t1004
2582  B       b1006   t1006 b  T       t1005   o b952 b4
2583  T       t1007   o546 b547 b1006  B       b1006   t1005
2584  H       h1007   w t1007  T       t1006   o882 b1006
2585  S       s1007   t597 h h992 h993 h994 h709 h995 h1007 h1000  B       b1007   t1006
2586  G       s1007   t978  T       t1007   o881 b1007
2587  B       b1007   s1007  B       b1008   t1007
2588  T       t1008   o611 b1007 b990  T       t1008   o b1008 b1003
2589  B       b1008   t1008  B       b1009   t1008
2590  P       p1008   String thin  T       t1009   o b987 b4
2591  O       o1008   arg_named p1008  B       b1010   t1009
2592  P       p1009   String false  T       t1010   o882 b1010
2593  O       o1009   arg_bool p1009  B       b1011   t1010
2594  T       t1009   o1009  T       t1011   o881 b1011
2595  B       b1009   t1009  B       b1012   t1011
2596  T       t1010   o1008 b1009  T       t1012   o b1012 b1003
 B       b1010   t1010  
 T       t1011   o b1010 b4  
 B       b1011   t1011  
 S       s1011   t597 h h992 h993 h994 h709 h995 h1007  
 G       s1011   t978  
 B       b1012   s1011  
 T       t1012   o611 b1012 b990  
2597  B       b1013   t1012  B       b1013   t1012
2598  P       p1013   String with  T       t1013   o628 b962 b1013 b983
2599  O       o1013   arg_named p1013  B       b1014   t1013
2600  NSummary!arg_term_list  arg_term_list   arg_term_list Summary  T       t1014   o2 b1014
2601  O       o1014   arg_term_list  B       b1015   t1014
2602  T       t1014   o b977 b4  T       t1015   o628 b1005 b1009 b1015
2603  B       b1014   t1014  B       b1016   t1015
2604  T       t1015   o1014 b1014  T       t1016   o2 b1016
2605  B       b1015   t1015  B       b1017   t1016
2606  T       t1016   o1013 b1015  T       t1017   o628 b1000 b1003 b1017
2607  B       b1016   t1016  B       b1018   t1017
2608  T       t1017   o b1016 b1011  T       t1018   o2 b1018
 B       b1017   t1017  
 S       s1017   t597 h h992 h993 h994 h709 h995  
 G       s1017   t978  
 B       b1018   s1017  
 T       t1018   o611 b1018 b990  
2609  B       b1019   t1018  B       b1019   t1018
2610  S       s1019   t597 h h992 h993 h716 h995  T       t1019   o628 b995 b4 b1019
2611  G       s1019   t978  B       b1020   t1019
2612  B       b1020   s1019  T       t1020   o2 b1020
 T       t1020   o611 b1020 b990  
2613  B       b1021   t1020  B       b1021   t1020
2614  S       s1021   t597 h h992 h718 h995  T       t1021   o628 b993 b4 b1021
2615  G       s1021   t978  B       b1022   t1021
2616  B       b1022   s1021  T       t1022   o2 b1022
 T       t1022   o611 b1022 b990  
2617  B       b1023   t1022  B       b1023   t1022
2618  S       s1023   t597 h h720 h995  T       t1023   o628 b989 b4 b1023
2619  G       s1023   t978  B       b1024   t1023
2620  B       b1024   s1023  T       t1024   o b1024 b4
 T       t1024   o611 b1024 b990  
2621  B       b1025   t1024  B       b1025   t1024
2622  S       s1025   t597 h h696 h995  T       t1025   o627 b984 b1025
2623  G       s1025   t978  B       b1026   t1025
2624  B       b1026   s1025  P       p1026   String "instHypT [<< id{'s} >>; << id{'s} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca thenT dT 8 ttca"
2625  T       t1026   o611 b1026 b990  O       o1026   ext_rule p1026
2626    T       t1026   o569 b550 b952 b952
2627  B       b1027   t1026  B       b1027   t1026
2628  S       s1027   t597 h h696  T       t1027   o568 b987 b1027
2629  G       s1027   t978  H       h1027   y_6 t1027
2630    S       s1027   t620 h h696 h697 h698 h699 h700 h987 h1027
2631    G       s1027   t954
2632  B       b1028   s1027  B       b1028   s1027
2633  T       t1028   o611 b1028 b990  T       t1028   o629 b1028 b694
2634  B       b1029   t1028  B       b1029   t1028
2635  T       t1029   o2 b992  T       t1029   o564 b952 b559
2636  B       b1030   t1029  B       b1030   t1029
2637  T       t1030   o610 b1029 b4 b1030  B       b1031   t1027
2638  B       b1031   t1030  T       t1031   o563 b1030 b1031
2639  T       t1031   o2 b1031  H       h1031   y_5 t1031
2640  B       b1032   t1031  S       s1031   t620 h h696 h697 h698 h699 h700 h987 h1031 h1027
2641  T       t1032   o610 b1027 b4 b1032  G       s1031   t954
2642    B       b1032   s1031
2643    T       t1032   o629 b1032 b694
2644  B       b1033   t1032  B       b1033   t1032
2645  T       t1033   o2 b1033  S       s1033   t620 h h696 h697 h698 h699 h700 h987 h1031
2646  B       b1034   t1033  G       s1033   t954
2647  T       t1034   o610 b1025 b4 b1034  B       b1034   s1033
2648    T       t1034   o629 b1034 b694
2649  B       b1035   t1034  B       b1035   t1034
2650  T       t1035   o2 b1035  B       b1036   t1031
2651  B       b1036   t1035  T       t1036   o563 b1030 b1036
2652  T       t1036   o610 b1023 b4 b1036  H       h1036   w_1 t1036
2653  B       b1037   t1036  S       s1036   t620 h h696 h697 h698 h699 h700 h987 h1036 h1031
2654  T       t1037   o2 b1037  G       s1036   t954
2655    B       b1037   s1036
2656    T       t1037   o629 b1037 b694
2657  B       b1038   t1037  B       b1038   t1037
2658  T       t1038   o610 b1021 b4 b1038  S       s1038   t620 h h696 h697 h698 h699 h700 h987 h1036
2659  B       b1039   t1038  G       s1038   t954
2660  T       t1039   o2 b1039  B       b1039   s1038
2661    T       t1039   o629 b1039 b694
2662  B       b1040   t1039  B       b1040   t1039
2663  T       t1040   o610 b1019 b1017 b1040  T       t1040   o569 b549 b952 b567
2664  B       b1041   t1040  B       b1041   t1040
2665  T       t1041   o2 b1041  T       t1041   o569 b550 b952 b567
2666  B       b1042   t1041  B       b1042   t1041
2667  T       t1042   o610 b1013 b1017 b1042  T       t1042   o568 b1041 b1042
2668  B       b1043   t1042  B       b1043   t1042
2669  T       t1043   o2 b1043  T       t1043   o563 b568 b1043
2670  B       b1044   t1043  B       b1044   t1043
2671  T       t1044   o610 b1008 b1011 b1044  T       t1044   o563 b1030 b1044
2672  B       b1045   t1044  B       b1045   t1044 b
2673  T       t1045   o2 b1045  T       t1045   o561 b562 b1045
2674  B       b1046   t1045  H       h1045   w t1045
2675  T       t1046   o610 b1001 b4 b1046  S       s1045   t620 h h696 h697 h698 h699 h700 h987 h1045 h1036
2676    G       s1045   t954
2677    B       b1046   s1045
2678    T       t1046   o629 b1046 b694
2679  B       b1047   t1046  B       b1047   t1046
2680  T       t1047   o b1047 b4  S       s1047   t620 h h696 h697 h698 h699 h700 h987 h1045
2681  B       b1048   t1047  G       s1047   t954
2682  T       t1048   o609 b992 b1048  B       b1048   s1047
2683    T       t1048   o629 b1048 b694
2684  B       b1049   t1048  B       b1049   t1048
2685  P       p1049   String "dT 7 ttca thenT dT 7 ttca"  T       t1049   o628 b989 b1009 b1023
2686  O       o1049   ext_rule p1049  B       b1050   t1049
2687  H       h1049   y_4 t998  T       t1050   o2 b1050
 S       s1049   t597 h h992 h993 h994 h709 h995 h1049  
 G       s1049   t978  
 B       b1050   s1049  
 T       t1050   o611 b1050 b990  
2688  B       b1051   t1050  B       b1051   t1050
2689  H       h1051   y_3 t999  T       t1051   o628 b1049 b1009 b1051
2690  S       s1051   t597 h h992 h993 h994 h709 h995 h1051 h1049  B       b1052   t1051
2691  G       s1051   t978  T       t1052   o2 b1052
 B       b1052   s1051  
 T       t1052   o611 b1052 b990  
2692  B       b1053   t1052  B       b1053   t1052
2693  S       s1053   t597 h h992 h993 h994 h709 h995 h1051  T       t1053   o628 b1047 b1003 b1053
2694  G       s1053   t978  B       b1054   t1053
2695  B       b1054   s1053  T       t1054   o2 b1054
 T       t1054   o611 b1054 b990  
2696  B       b1055   t1054  B       b1055   t1054
2697  S       s1055   t597 h h992 h993 h994 h709 h995 h1000 h1051  T       t1055   o628 b1040 b4 b1055
2698  G       s1055   t978  B       b1056   t1055
2699  B       b1056   s1055  T       t1056   o2 b1056
 T       t1056   o611 b1056 b990  
2700  B       b1057   t1056  B       b1057   t1056
2701  T       t1057   o2 b1047  T       t1057   o628 b1038 b4 b1057
2702  B       b1058   t1057  B       b1058   t1057
2703  T       t1058   o610 b1057 b4 b1058  T       t1058   o2 b1058
2704  B       b1059   t1058  B       b1059   t1058
2705  T       t1059   o2 b1059  T       t1059   o628 b1035 b4 b1059
2706  B       b1060   t1059  B       b1060   t1059
2707  T       t1060   o610 b1055 b4 b1060  T       t1060   o2 b1060
2708  B       b1061   t1060  B       b1061   t1060
2709  T       t1061   o2 b1061  T       t1061   o628 b1033 b4 b1061
2710  B       b1062   t1061  B       b1062   t1061
2711  T       t1062   o610 b1053 b4 b1062  T       t1062   o2 b1062
2712  B       b1063   t1062  B       b1063   t1062
2713  T       t1063   o2 b1063  T       t1063   o628 b1029 b4 b1063
2714  B       b1064   t1063  B       b1064   t1063
2715  T       t1064   o610 b1051 b4 b1064  T       t1064   o b1064 b4
2716  B       b1065   t1064  B       b1065   t1064
2717  T       t1065   o b1065 b4  T       t1065   o627 b1024 b1065
2718  B       b1066   t1065  B       b1066   t1065
2719  T       t1066   o609 b1047 b1066  P       p1066   String "setSubstT << equal{op{'s; id{'s}; id{'s}}; op{'g; id{'s}; id{'s}}} >> 7 thenT autoT"
2720  B       b1067   t1066  O       o1066   ext_rule p1066
2721  P       p1067   String "assertT << equiv{car{'g}; 'R; op{'g; id{'s}; id{'s}}; id{'s}} >> ttca"  T       t1066   o575 b560 b578 b1027 b952
2722  O       o1067   ext_rule p1067  H       h1066   v t1066
2723  T       t1067   o669 b545 b670 b997 b977  S       s1066   t620 h h696 h697 h698 h699 h700 h987 h1027 h1066
2724  S       s1067   t597 h h992 h993 h994 h709 h995 h1049  G       s1066   t954
2725  G       s1067   t1067  B       b1067   s1066
2726  B       b1068   s1067  T       t1067   o629 b1067 b694
2727  T       t1068   o611 b1068 b990  B       b1068   t1067
2728    T       t1068   o2 b1064
2729  B       b1069   t1068  B       b1069   t1068
2730  T       t1069   o2 b1065  T       t1069   o628 b1068 b4 b1069
2731  B       b1070   t1069  B       b1070   t1069
2732  T       t1070   o698 b1069 b4 b1070  P       p1070   String wf
2733  B       b1071   t1070  O       o1070   tactic_arg p1070
2734  H       h1071   v t1067  T       t1070   o564 b952 b560
2735  S       s1071   t597 h h992 h993 h994 h709 h995 h1049 h1071  S       s1070   t620 h h696 h697 h698 h699 h700 h987 h1027
2736  G       s1071   t978  G       s1070   t1070
2737  B       b1072   s1071  B       b1071   s1070
2738  T       t1072   o611 b1072 b990  T       t1071   o629 b1071 b694
2739  B       b1073   t1072  B       b1072   t1071
2740  T       t1073   o610 b1073 b4 b1070  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq
2741  B       b1074   t1073  O       o1072   fun_prop
2742  T       t1074   o b1074 b4  P       p1072   Var v
2743  B       b1075   t1074  O       o1073   var p1072
2744  T       t1075   o b1071 b1075  T       t1073   o1073
2745  B       b1076   t1075  B       b1073   t1073
2746  T       t1076   o609 b1065 b1076  T       t1074   o575 b560 b578 b1073 b952
2747  B       b1077   t1076  B       b1074   t1074 v
2748  P       p1077   String "setSubstT << equal{op{'g; id{'s}; id{'s}}; op{'s; id{'s}; id{'s}}} >> 0 thenT autoT"  T       t1075   o1072 b1074
2749  O       o1077   ext_rule p1077  S       s1075   t620 h h696 h697 h698 h699 h700 h987 h1027
2750  P       p1078   String eq  G       s1075   t1075
2751  O       o1078   tactic_arg p1078  B       b1075   s1075
2752  NCzf_itt_eq!eq  eq      eq Czf_itt_eq  T       t1076   o629 b1075 b694
2753  O       o1079   eq  B       b1076   t1076
2754  T       t1079   o1079 b997 b996  T       t1077   o1070 b1076 b711 b1069
2755  S       s1079   t597 h h992 h993 h994 h709 h995 h1049  B       b1077   t1077
2756  G       s1079   t1079  T       t1078   o2 b1077
2757  B       b1079   s1079  B       b1078   t1078
2758  T       t1080   o611 b1079 b990  T       t1079   o1070 b1072 b4 b1078
2759    B       b1079   t1079
2760    T       t1080   o b1079 b4
2761  B       b1080   t1080  B       b1080   t1080
2762  T       t1081   o553 b997 b996  T       t1081   o b1070 b1080
2763  S       s1081   t597 h h992 h993 h994 h709 h995 h1049  B       b1081   t1081
2764  G       s1081   t1081  T       t1082   o627 b1064 b1081
 B       b1081   s1081  
 T       t1082   o611 b1081 b990  
2765  B       b1082   t1082  B       b1082   t1082
2766  T       t1083   o2 b1071  P       p1082   String "dT 9 ttca"
2767    O       o1082   ext_rule p1082
2768    T       t1083   o627 b1070 b4
2769  B       b1083   t1083  B       b1083   t1083
2770  T       t1084   o1078 b1082 b729 b1083  T       t1084   o1082 b626 b1083 b4 b4
2771  B       b1084   t1084  B       b1084   t1084
2772  T       t1085   o2 b1084  P       p1084   String "withT << id{'s} >> (dT 4) ttca"
2773    O       o1084   ext_rule p1084
2774    T       t1085   o627 b1079 b4
2775  B       b1085   t1085  B       b1085   t1085
2776  T       t1086   o1078 b1080 b4 b1085  T       t1086   o1084 b626 b1085 b4 b4
2777  B       b1086   t1086  B       b1086   t1086
2778  T       t1087   o549 b996 b545  T       t1087   o b1086 b4
2779  S       s1087   t597 h h992 h993 h994 h709 h995 h1049  B       b1087   t1087
2780  G       s1087   t1087  T       t1088   o b1084 b1087
 B       b1087   s1087  
 T       t1088   o611 b1087 b990  
2781  B       b1088   t1088  B       b1088   t1088
2782  T       t1089   o669 b545 b670 b996 b977  T       t1089   o1066 b626 b1082 b1088 b4
2783  S       s1089   t597 h h992 h993 h994 h709 h995 h1049  B       b1089   t1089
2784  G       s1089   t1089  T       t1090   o b1089 b4
 B       b1089   s1089  
 T       t1090   o611 b1089 b990  
2785  B       b1090   t1090  B       b1090   t1090
2786  T       t1091   o610 b1090 b729 b1083  T       t1091   o1026 b626 b1066 b1090 b4
2787  B       b1091   t1091  B       b1091   t1091
2788  T       t1092   o2 b1091  T       t1092   o b1091 b4
2789  B       b1092   t1092  B       b1092   t1092
2790  T       t1093   o610 b1088 b4 b1092  T       t1093   o986 b626 b1026 b1092 b4
2791  B       b1093   t1093  B       b1093   t1093
2792  T       t1094   o549 b977 b545  T       t1094   o b1093 b4
2793  S       s1094   t597 h h992 h993 h994 h709 h995 h1049  B       b1094   t1094
2794  G       s1094   t1094  T       t1095   o691 b626 b986 b1094 b4
 B       b1094   s1094  
 T       t1095   o611 b1094 b990  
2795  B       b1095   t1095  B       b1095   t1095
2796  T       t1096   o610 b1095 b4 b1092  T       t1096   o624 b1095
2797  B       b1096   t1096  B       b1096   t1096
2798  T       t1097   o713 b996 b977  P       p1096   Number 2112
2799  B       b1097   t1097  P       p1097   Number 2120
2800  T       t1098   o549 b1097 b670  O       o1097   resource_defs p1096 p1097 p300
2801  S       s1098   t597 h h992 h993 h994 h709 h995 h1049  P       p1098   Number 2118
2802  G       s1098   t1098  O       o1098   uid p1098 p1097
2803  B       b1098   s1098  T       t1098   o1098 b639
2804  T       t1099   o611 b1098 b990  B       b1098   t1098
2805    T       t1099   o b1098 b4
2806  B       b1099   t1099  B       b1099   t1099
2807  T       t1100   o610 b1099 b4 b1092  T       t1100   o1097 b1099
2808  B       b1100   t1100  B       b1100   t1100
2809  T       t1101   o b1100 b4  T       t1101   o b1100 b4
2810  B       b1101   t1101  B       b1101   t1101
2811  T       t1102   o b1096 b1101  T       t1102   o951 b610 b958 b1096 b1101
2812  B       b1102   t1102  B       b1102   t1102
2813  T       t1103   o b1093 b1102  T       t1103   o950 b1102
2814  B       b1103   t1103  B       b1103   t1103
2815  T       t1104   o b1086 b1103  P       p1103   Number 2339
2816  B       b1104   t1104  P       p1104   Number 2695
2817  T       t1105   o609 b1071 b1104  O       o1104   location p1103 p1104
2818  B       b1105   t1105  P       p1105   String subgroup_inv
2819  P       p1105   String "rwh unfold_equal 7 thenT autoT thenT eqSetSymT ttca"  O       o1105   rule p1105
2820  O       o1105   ext_rule p1105  T       t1105   o761 b565
2821  T       t1106   o609 b1086 b4  S       s1105   t613 h
2822    G       s1105   t1105
2823    B       b1105   s1105
2824    T       t1106   o611 b1105
2825  B       b1106   t1106  B       b1106   t1106
2826  T       t1107   o1105 b608 b1106 b4 b4  S       s1106   t620 h
2827  B       b1107   t1107  G       s1106   t566
2828  P       p1107   String "withT << op{'s; id{'s}; id{'s}} >> (dT 4) ttca"  B       b1107   s1106
2829  O       o1107   ext_rule p1107  T       t1107   o611 b1107
2830  T       t1108   o609 b1093 b4  B       b1108   t1107
 B       b1108   t1108  
 T       t1109   o1107 b608 b1108 b4 b4  
 B       b1109   t1109  
 P       p1109   String "withT << id{'s} >> (dT 4) ttca"  
 O       o1109   ext_rule p1109  
 T       t1110   o609 b1096 b4  
 B       b1110   t1110  
 T       t1111   o1109 b608 b1110 b4 b4  
 B       b1111   t1111  
 P       p1111   String "withT << 's >> (dT 6) ttca thenT assertT << equiv{car{'s}; 'R; op{'s; id{'s}; id{'s}}; id{'s}} >> ttca thenT rwh unfold_equiv 9 ttca"  
 O       o1111   ext_rule p1111  
 T       t1112   o609 b1100 b4  
 B       b1112   t1112  
 T       t1113   o1111 b608 b1112 b4 b4  
 B       b1113   t1113  
 T       t1114   o b1113 b4  
 B       b1114   t1114  
 T       t1115   o b1111 b1114  
 B       b1115   t1115  
 T       t1116   o b1109 b1115  
 B       b1116   t1116  
 T       t1117   o b1107 b1116  
 B       b1117   t1117  
 T       t1118   o1077 b608 b1105 b1117 b4  
 B       b1118   t1118  
 P       p1118   String "dT 8 ttca"  
 O       o1118   ext_rule p1118  
 T       t1119   o609 b1074 b4  
 B       b1119   t1119  
 T       t1120   o1118 b608 b1119 b4 b4  
 B       b1120   t1120  
 T       t1121   o b1120 b4  
 B       b1121   t1121  
 T       t1122   o b1118 b1121  
 B       b1122   t1122  
 T       t1123   o1067 b608 b1077 b1122 b4  
 B       b1123   t1123  
 T       t1124   o b1123 b4  
 B       b1124   t1124  
 T       t1125   o1049 b608 b1067 b1124 b4  
 B       b1125   t1125  
 T       t1126   o b1125 b4  
 B       b1126   t1126  
 T       t1127   o985 b608 b1049 b1126 b4  
 B       b1127   t1127  
 T       t1128   o606 b1127  
 B       b1128   t1128  
 P       p1137   String subgroup_inv  
 O       o1137   rule p1137  
 T       t1137   o675 b550  
 S       s1137   t590 h  
 G       s1137   t1137  
 B       b1137   s1137  
 T       t1138   o588 b1137  
 B       b1138   t1138  
 S       s1138   t597 h  
 G       s1138   t551  
 B       b1139   s1138  
 T       t1139   o588 b1139  
 B       b1140   t1139  
2831  NCzf_itt_group!inv      inv     inv Czf_itt_group  NCzf_itt_group!inv      inv     inv Czf_itt_group
2832  O       o1140   inv  O       o1108   inv
2833  T       t1140   o1140 b535 b550  T       t1108   o1108 b549 b565
2834    B       b1109   t1108
2835    T       t1109   o1108 b550 b565
2836    B       b1110   t1109
2837    T       t1110   o575 b560 b578 b1109 b1110
2838    S       s1110   t620 h
2839    G       s1110   t1110
2840    B       b1111   s1110
2841    T       t1111   o611 b1111
2842    B       b1112   t1111
2843    T       t1112   o610 b659 b1112
2844    B       b1113   t1112
2845    T       t1113   o610 b1108 b1113
2846    B       b1114   t1113
2847    T       t1114   o610 b1106 b1114
2848    B       b1115   t1114
2849    T       t1115   o610 b618 b1115
2850    B       b1116   t1115
2851    T       t1116   o610 b616 b1116
2852    B       b1117   t1116
2853    P       p1117   String "assumT 5 thenT rwh unfold_subgroup 2 thenT autoT"
2854    O       o1117   ext_rule p1117
2855    T       t1117   o b1107 b692
2856    B       b1118   t1117
2857    T       t1118   o b1105 b1118
2858    B       b1119   t1118
2859    T       t1119   o b617 b1119
2860    B       b1120   t1119
2861    T       t1120   o b615 b1120
2862    B       b1121   t1120
2863    T       t1121   o629 b1111 b1121
2864    B       b1122   t1121
2865    T       t1122   o628 b1122 b4 b632
2866    B       b1123   t1122
2867    T       t1123   o564 b565 b560
2868    S       s1123   t620 h h696 h697 h698 h699 h700
2869    G       s1123   t1123
2870    B       b1124   s1123
2871    T       t1124   o629 b1124 b1121
2872    B       b1125   t1124
2873    S       s1125   t620 h h696 h697 h698 h699 h700
2874    G       s1125   t1110
2875    B       b1126   s1125
2876    T       t1126   o629 b1126 b1121
2877    B       b1127   t1126
2878    S       s1127   t620 h h696 h697 h698 h711
2879    G       s1127   t1110
2880    B       b1128   s1127
2881    T       t1128   o629 b1128 b1121
2882    B       b1129   t1128
2883    S       s1129   t620 h h696 h697 h713
2884    G       s1129   t1110
2885    B       b1130   s1129
2886    T       t1130   o629 b1130 b1121
2887    B       b1131   t1130
2888    S       s1131   t620 h h696 h715
2889    G       s1131   t1110
2890    B       b1132   s1131
2891    T       t1132   o629 b1132 b1121
2892    B       b1133   t1132
2893    S       s1133   t620 h h717
2894    G       s1133   t1110
2895    B       b1134   s1133
2896    T       t1134   o629 b1134 b1121
2897    B       b1135   t1134
2898    S       s1135   t620 h h719
2899    G       s1135   t1110
2900    B       b1136   s1135
2901    T       t1136   o629 b1136 b1121
2902    B       b1137   t1136
2903    T       t1137   o2 b1123
2904    B       b1138   t1137
2905    T       t1138   o628 b1137 b4 b1138
2906    B       b1139   t1138
2907    T       t1139   o2 b1139
2908    B       b1140   t1139
2909    T       t1140   o628 b1135 b4 b1140
2910  B       b1141   t1140  B       b1141   t1140
2911  T       t1141   o1140 b534 b550  T       t1141   o2 b1141
2912  B       b1142   t1141  B       b1142   t1141
2913  T       t1142   o669 b545 b670 b1141 b1142  T       t1142   o628 b1133 b4 b1142
2914  S       s1142   t597 h  B       b1143   t1142
2915  G       s1142   t1142  T       t1143   o2 b1143
 B       b1143   s1142  
 T       t1143   o588 b1143  
2916  B       b1144   t1143  B       b1144   t1143
2917  T       t1144   o587 b976 b1144  T       t1144   o628 b1131 b4 b1144
2918  B       b1145   t1144  B       b1145   t1144
2919  T       t1145   o587 b638 b1145  T       t1145   o2 b1145
2920  B       b1146   t1145  B       b1146   t1145
2921  T       t1146   o587 b1140 b1146  T       t1146   o628 b1129 b4 b1146
2922  B       b1147   t1146  B       b1147   t1146
2923  T       t1147   o587 b1138 b1147  T       t1147   o2 b1147
2924  B       b1148   t1147  B       b1148   t1147
2925  T       t1148   o587 b974 b1148  T       t1148   o628 b1127 b711 b1148
2926  B       b1149   t1148  B       b1149   t1148
2927  T       t1149   o587 b595 b1149  T       t1149   o2 b1149
2928  B       b1150   t1149  B       b1150   t1149
2929  T       t1150   o587 b593 b1150  T       t1150   o628 b1125 b4 b1150
2930  B       b1151   t1150  B       b1151   t1150
2931  P       p1151   String "assumT 6 thenT assumT 7 thenT assertT << equiv{car{'g}; 'R; op{'g; inv{'s; 'a}; 'a}; id{'g}} >> ttca thenT rwh unfold_subgroup 2 ttca"  T       t1151   o564 b1109 b560
2932  O       o1151   ext_rule p1151  S       s1151   t620 h h696 h697 h698 h699 h700
2933  T       t1151   o b1139 b987  G       s1151   t1151
2934  B       b1152   t1151  B       b1152   s1151
2935  T       t1152   o b1137 b1152  T       t1152   o629 b1152 b1121
2936  B       b1153   t1152  B       b1153   t1152
2937  T       t1153   o b973 b1153  T       t1153   o628 b1153 b4 b1150
2938  B       b1154   t1153  B       b1154   t1153
2939  T       t1154   o b594 b1154  T       t1154   o569 b550 b565 b1109
2940  B       b1155   t1154  B       b1155   t1154
2941  T       t1155   o b592 b1155  T       t1155   o575 b560 b578 b1155 b953
2942  B       b1156   t1155  S       s1155   t620 h h696 h697 h698 h699 h700
2943  T       t1156   o611 b1143 b1156  G       s1155   t1155
2944    B       b1156   s1155
2945    T       t1156   o629 b1156 b1121
2946  B       b1157   t1156  B       b1157   t1156
2947  T       t1157   o610 b1157 b4 b616  T       t1157   o628 b1157 b4 b1150
2948  B       b1158   t1157  B       b1158   t1157
2949  T       t1158   o554 b534 b1141 b550  T       t1158   o b1158 b4
2950  B       b1159   t1158  B       b1159   t1158
2951  T       t1159   o669 b545 b670 b1159 b978  T       t1159   o b1154 b1159
2952  S       s1159   t597 h h720 h995  B       b1160   t1159
2953  G       s1159   t1159  T       t1160   o b1151 b1160
 B       b1160   s1159  
 T       t1160   o611 b1160 b1156  
2954  B       b1161   t1160  B       b1161   t1160
2955  S       s1161   t597 h h696 h995  T       t1161   o627 b1123 b1161
2956  G       s1161   t1159  B       b1162   t1161
2957  B       b1162   s1161  P       p1162   String "withT << 'a >> (dT 4) ttca"
2958  T       t1162   o611 b1162 b1156  O       o1162   ext_rule p1162
2959    T       t1162   o627 b1151 b4
2960  B       b1163   t1162  B       b1163   t1162
2961  S       s1163   t597 h h696 h995  T       t1163   o1162 b626 b1163 b4 b4
2962  G       s1163   t1142  B       b1164   t1163
2963  B       b1164   s1163  P       p1164   String "withT << inv{'s; 'a} >> (dT 4) ttca"
2964  T       t1164   o611 b1164 b1156  O       o1164   ext_rule p1164
2965    T       t1164   o627 b1154 b4
2966  B       b1165   t1164  B       b1165   t1164
2967  S       s1165   t597 h h696  T       t1165   o1164 b626 b1165 b4 b4
2968  G       s1165   t1142  B       b1166   t1165
2969  B       b1166   s1165  P       p1166   String "instHypT [<< op{'s; 'a; inv{'s; 'a}} >>; << id{'s} >>] 6 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 7 ttca"
2970  T       t1166   o611 b1166 b1156  O       o1166   ext_rule p1166
2971    T       t1166   o569 b549 b565 b1109
2972  B       b1167   t1166  B       b1167   t1166
2973  T       t1167   o2 b1158  T       t1167   o575 b560 b578 b1167 b952
2974  B       b1168   t1167  H       h1167   y_4 t1167
2975  T       t1168   o610 b1167 b4 b1168  S       s1167   t620 h h696 h697 h698 h699 h700 h1167
2976    G       s1167   t1155
2977    B       b1168   s1167
2978    T       t1168   o629 b1168 b1121
2979  B       b1169   t1168  B       b1169   t1168
2980  T       t1169   o2 b1169  T       t1169   o575 b559 b576 b1167 b952
2981  B       b1170   t1169  B       b1170   t1169
2982  T       t1170   o610 b1165 b4 b1170  B       b1171   t1167
2983  B       b1171   t1170  T       t1171   o563 b1170 b1171
2984  T       t1171   o2 b1171  H       h1171   w_1 t1171
2985  B       b1172   t1171  S       s1171   t620 h h696 h697 h698 h699 h700 h1171 h1167
2986  T       t1172   o698 b1163 b4 b1172  G       s1171   t1155
2987    B       b1172   s1171
2988    T       t1172   o629 b1172 b1121
2989  B       b1173   t1172  B       b1173   t1172
2990  T       t1173   o2 b1173  S       s1173   t620 h h696 h697 h698 h699 h700 h1171
2991  B       b1174   t1173  G       s1173   t1155
2992  T       t1174   o698 b1161 b4 b1174  B       b1174   s1173
2993    T       t1174   o629 b1174 b1121
2994  B       b1175   t1174  B       b1175   t1174
2995  H       h1175   v_2 t1159  T       t1175   o575 b559 b576 b1167 b567
2996  S       s1175   t597 h h720 h995 h1175  B       b1176   t1175
2997  G       s1175   t1142  T       t1176   o575 b560 b578 b1167 b567
 B       b1176   s1175  
 T       t1176   o611 b1176 b1156  
2998  B       b1177   t1176  B       b1177   t1176
2999  S       s1177   t597 h h696 h995 h1175  T       t1177   o563 b1176 b1177
3000  G       s1177   t1142  B       b1178   t1177 b
3001  B       b1178   s1177  T       t1178   o561 b562 b1178
3002  T       t1178   o611 b1178 b1156  H       h1178   w t1178
3003  B       b1179   t1178  S       s1178   t620 h h696 h697 h698 h699 h700 h1178 h1171
3004  T       t1179   o610 b1179 b4 b1172  G       s1178   t1155
3005    B       b1179   s1178
3006    T       t1179   o629 b1179 b1121
3007  B       b1180   t1179  B       b1180   t1179
3008  T       t1180   o2 b1180  S       s1180   t620 h h696 h697 h698 h699 h700 h1178
3009  B       b1181   t1180  G       s1180   t1155
3010  T       t1181   o610 b1177 b4 b1181  B       b1181   s1180
3011    T       t1181   o629 b1181 b1121
3012  B       b1182   t1181  B       b1182   t1181
3013  T       t1182   o b1182 b4  T       t1182   o b1167 b4
3014  B       b1183   t1182  B       b1183   t1182
3015  T       t1183   o b1175 b1183  T       t1183   o882 b1183
3016  B       b1184   t1183  B       b1184   t1183
3017  T       t1184   o609 b1158 b1184  T       t1184   o881 b1184
3018  B       b1185   t1184  B       b1185   t1184
3019  P       p1185   String "dT 2 thenT dT 3 thenT dT 4 thenT instHypT [<< inv{'s; 'a} >>; << 'a >>] 5 ttca thenT rwh fold_isset 0 ttca"  T       t1185   o b1185 b1003
 O       o1185   ext_rule p1185  
 T       t1185   o549 b1141 b544  
3020  B       b1186   t1185  B       b1186   t1185
3021  T       t1186   o554 b535 b1141 b550  T       t1186   o628 b1157 b1186 b1150
3022  B       b1187   t1186  B       b1187   t1186
3023  T       t1187   o553 b1187 b1159  T       t1187   o2 b1187
3024  B       b1188   t1187  B       b1188   t1187
3025  T       t1188   o548 b551 b1188  T       t1188   o628 b1182 b1009 b1188
3026  B       b1189   t1188  B       b1189   t1188
3027  T       t1189   o548 b1186 b1189  T       t1189   o2 b1189
3028  H       h1189   w_1 t1189  B       b1190   t1189
3029  S       s1189   t597 h h992 h993 h994 h709 h995 h1189  T       t1190   o628 b1180 b1003 b1190
 G       s1189   t1159  
 B       b1190   s1189  
 T       t1190   o611 b1190 b1156  
3030  B       b1191   t1190  B       b1191   t1190
3031  T       t1191   o554 b535 b1141 b552  T       t1191   o2 b1191
3032  B       b1192   t1191  B       b1192   t1191
3033  T       t1192   o554 b534 b1141 b552  T       t1192   o628 b1175 b4 b1192
3034  B       b1193   t1192  B       b1193   t1192
3035  T       t1193   o553 b1192 b1193  T       t1193   o2 b1193
3036  B       b1194   t1193  B       b1194   t1193
3037  T       t1194   o548 b553 b1194  T       t1194   o628 b1173 b4 b1194
3038  B       b1195   t1194  B       b1195   t1194
3039  T       t1195   o548 b1186 b1195  T       t1195   o2 b1195
3040  B       b1196   t1195 b  B       b1196   t1195
3041  T       t1196   o546 b547 b1196  T       t1196   o628 b1169 b4 b1196
3042  H       h1196   w t1196  B       b1197   t1196
3043  S       s1196   t597 h h992 h993 h994 h709 h995 h1196 h1189  T       t1197   o b1197 b4
 G       s1196   t1159  
 B       b1197   s1196  
 T       t1197   o611 b1197 b1156  
3044  B       b1198   t1197  B       b1198   t1197
3045  S       s1198   t597 h h992 h993 h994 h709 h995 h1196  T       t1198   o627 b1158 b1198
3046  G       s1198   t1159  B       b1199   t1198
3047  B       b1199   s1198  P       p1199   String "instHypT [<< 'a >>; << inv{'s; 'a} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca thenT dT 8 ttca"
3048  T       t1199   o611 b1199 b1156  O       o1199   ext_rule p1199
3049  B       b1200   t1199  T       t1199   o568 b1167 b1155
3050  T       t1200   o b550 b4  H       h1199   y_6 t1199
3051    S       s1199   t620 h h696 h697 h698 h699 h700 h1167 h1199
3052    G       s1199   t1155
3053    B       b1200   s1199
3054    T       t1200   o629 b1200 b1121
3055  B       b1201   t1200  B       b1201   t1200
3056  T       t1201   o1014 b1201  T       t1201   o564 b1109 b559
3057  B       b1202   t1201  B       b1202   t1201
3058  T       t1202   o1013 b1202  B       b1203   t1199
3059  B       b1203   t1202  T       t1203   o563 b1202 b1203
3060  T       t1203   o b1203 b1011  H       h1203   y_5 t1203
3061  B       b1204   t1203  S       s1203   t620 h h696 h697 h698 h699 h700 h1167 h1203 h1199
3062  S       s1204   t597 h h992 h993 h994 h709 h995  G       s1203   t1155
3063  G       s1204   t1159  B       b1204   s1203
3064  B       b1205   s1204  T       t1204   o629 b1204 b1121
3065  T       t1205   o611 b1205 b1156  B       b1205   t1204
3066  B       b1206   t1205  S       s1205   t620 h h696 h697 h698 h699 h700 h1167 h1203
3067  T       t1206   o b1141 b4  G       s1205   t1155
3068    B       b1206   s1205
3069    T       t1206   o629 b1206 b1121
3070  B       b1207   t1206  B       b1207   t1206
3071  T       t1207   o1014 b1207  B       b1208   t1203
3072  B       b1208   t1207  T       t1208   o563 b566 b1208
3073  T       t1208   o1013 b1208  H       h1208   w_1 t1208
3074  B       b1209   t1208  S       s1208   t620 h h696 h697 h698 h699 h700 h1167 h1208 h1203
3075  T       t1209   o b1209 b1011  G       s1208   t1155
3076    B       b1209   s1208
3077    T       t1209   o629 b1209 b1121
3078  B       b1210   t1209  B       b1210   t1209
3079  S       s1210   t597 h h992 h993 h716 h995  S       s1210   t620 h h696 h697 h698 h699 h700 h1167 h1208
3080  G       s1210   t1159  G       s1210   t1155
3081  B       b1211   s1210  B       b1211   s1210
3082  T       t1211   o611 b1211 b1156  T       t1211   o629 b1211 b1121
3083  B       b1212   t1211  B       b1212   t1211
3084  S       s1212   t597 h h992 h718 h995  H       h1212   w t574
3085  G       s1212   t1159  S       s1212   t620 h h696 h697 h698 h699 h700 h1167 h1212 h1208
3086    G       s1212   t1155
3087  B       b1213   s1212  B       b1213   s1212
3088  T       t1213   o611 b1213 b1156  T       t1213   o629 b1213 b1121
3089  B       b1214   t1213  B       b1214   t1213
3090  T       t1214   o2 b1175  S       s1214   t620 h h696 h697 h698 h699 h700 h1167 h1212
3091  B       b1215   t1214  G       s1214   t1155
3092  T       t1215   o610 b1214 b4 b1215  B       b1215   s1214
3093    T       t1215   o629 b1215 b1121
3094  B       b1216   t1215  B       b1216   t1215
3095  T       t1216   o2 b1216  T       t1216   o b1109 b4
3096  B       b1217   t1216  B       b1217   t1216
3097  T       t1217   o610 b1212 b4 b1217  T       t1217   o882 b1217
3098  B       b1218   t1217  B       b1218   t1217
3099  T       t1218   o2 b1218  T       t1218   o881 b1218
3100  B       b1219   t1218  B       b1219   t1218
3101  T       t1219   o610 b1206 b1210 b1219  T       t1219   o b1219 b1003
3102  B       b1220   t1219  B       b1220   t1219
3103  T       t1220   o2 b1220  T       t1220   o b565 b4
3104  B       b1221   t1220  B       b1221   t1220
3105  T       t1221   o610 b1200 b1204 b1221  T       t1221   o882 b1221
3106  B       b1222   t1221  B       b1222   t1221
3107  T       t1222   o2 b1222  T       t1222   o881 b1222
3108  B       b1223   t1222  B       b1223   t1222
3109  T       t1223   o610 b1198 b1011 b1223  T       t1223   o b1223 b1003
3110  B       b1224   t1223  B       b1224   t1223
3111  T       t1224   o2 b1224  T       t1224   o628 b1169 b1224 b1196
3112  B       b1225   t1224  B       b1225   t1224
3113  T       t1225   o610 b1191 b4 b1225  T       t1225   o2 b1225
3114  B       b1226   t1225  B       b1226   t1225
3115  T       t1226   o b1226 b4  T       t1226   o628 b1216 b1220 b1226
3116  B       b1227   t1226  B       b1227   t1226
3117  T       t1227   o609 b1175 b1227  T       t1227   o2 b1227
3118  B       b1228   t1227  B       b1228   t1227
3119  P       p1228   String "dT 7 ttca thenT dT 7 ttca thenT setSubstT << equal{op{'g; inv{'s; 'a}; 'a}; op{'s; inv{'s; 'a}; 'a}} >> 0 ttca"  T       t1228   o628 b1214 b1003 b1228
3120  O       o1228   ext_rule p1228  B       b1229   t1228
3121  H       h1228   y_4 t1187  T       t1229   o2 b1229
 T       t1228   o553 b1159 b1187  
 S       s1228   t597 h h992 h993 h994 h709 h995 h1228  
 G       s1228   t1228  
 B       b1229   s1228  
 T       t1229   o611 b1229 b1156  
3122  B       b1230   t1229  B       b1230   t1229
3123  S       s1230   t597 h h992 h993 h994 h709 h995 h1228  T       t1230   o628 b1212 b4 b1230
3124  G       s1230   t1159  B       b1231   t1230
3125  B       b1231   s1230  T       t1231   o2 b1231
 T       t1231   o611 b1231 b1156  
3126  B       b1232   t1231  B       b1232   t1231
3127  H       h1232   y_3 t1188  T       t1232   o628 b1210 b4 b1232
3128  S       s1232   t597 h h992 h993 h994 h709 h995 h1232 h1228  B       b1233   t1232
3129  G       s1232   t1159  T       t1233   o2 b1233
 B       b1233   s1232  
 T       t1233   o611 b1233 b1156  
3130  B       b1234   t1233  B       b1234   t1233
3131  S       s1234   t597 h h992 h993 h994 h709 h995 h1232  T       t1234   o628 b1207 b4 b1234
3132  G       s1234   t1159  B       b1235   t1234
3133  B       b1235   s1234  T       t1235   o2 b1235
 T       t1235   o611 b1235 b1156  
3134  B       b1236   t1235  B       b1236   t1235
3135  S       s1236   t597 h h992 h993 h994 h709 h995 h1189 h1232  T       t1236   o628 b1205 b4 b1236
3136  G       s1236   t1159  B       b1237   t1236
3137  B       b1237   s1236  T       t1237   o2 b1237
 T       t1237   o611 b1237 b1156  
3138  B       b1238   t1237  B       b1238   t1237
3139  T       t1238   o2 b1226  T       t1238   o628 b1201 b4 b1238
3140  B       b1239   t1238  B       b1239   t1238
3141  T       t1239   o610 b1238 b4 b1239  T       t1239   o b1239 b4
3142  B       b1240   t1239  B       b1240   t1239
3143  T       t1240   o2 b1240  T       t1240   o627 b1197 b1240
3144  B       b1241   t1240  B       b1241   t1240
3145  T       t1241   o610 b1236 b4 b1241  P       p1241   String "setSubstT << equal{op{'s; 'a; inv{'s; 'a}}; op{'g; 'a; inv{'s; 'a}}} >> 7 thenT autoT"
3146  B       b1242   t1241  O       o1241   ext_rule p1241
3147  T       t1242   o2 b1242  T       t1241   o575 b560 b578 b1155 b952
3148    H       h1241   v t1241
3149    S       s1241   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241
3150    G       s1241   t1155
3151    B       b1242   s1241
3152    T       t1242   o629 b1242 b1121
3153  B       b1243   t1242  B       b1243   t1242
3154  T       t1243   o610 b1234 b4 b1243  T       t1243   o2 b1239
3155  B       b1244   t1243  B       b1244   t1243
3156  T       t1244   o2 b1244  T       t1244   o628 b1243 b4 b1244
3157  B       b1245   t1244  B       b1245   t1244
3158  T       t1245   o610 b1232 b4 b1245  S       s1245   t620 h h696 h697 h698 h699 h700 h1167 h1199
3159  B       b1246   t1245  G       s1245   t1070
3160  T       t1246   o2 b1246  B       b1246   s1245
3161    T       t1246   o629 b1246 b1121
3162  B       b1247   t1246  B       b1247   t1246
3163  T       t1247   o1078 b1230 b4 b1247  S       s1247   t620 h h696 h697 h698 h699 h700 h1167 h1199
3164  B       b1248   t1247  G       s1247   t1075
3165  T       t1248   o669 b545 b670 b1187 b978  B       b1248   s1247
3166  S       s1248   t597 h h992 h993 h994 h709 h995 h1228  T       t1248   o629 b1248 b1121
3167  G       s1248   t1248  B       b1249   t1248
3168  B       b1249   s1248  T       t1249   o1070 b1249 b711 b1244
 T       t1249   o611 b1249 b1156  
3169  B       b1250   t1249  B       b1250   t1249
3170  T       t1250   o610 b1250 b4 b1247  T       t1250   o2 b1250
3171  B       b1251   t1250  B       b1251   t1250
3172  T       t1251   o b1251 b4  T       t1251   o1070 b1247 b4 b1251
3173  B       b1252   t1251  B       b1252   t1251
3174  T       t1252   o b1248 b1252  T       t1252   o b1252 b4
3175  B       b1253   t1252  B       b1253   t1252
3176  T       t1253   o609 b1226 b1253  T       t1253   o b1245 b1253
3177  B       b1254   t1253  B       b1254   t1253
3178  T       t1254   o609 b1248 b4  T       t1254   o627 b1239 b1254
3179  B       b1255   t1254  B       b1255   t1254
3180  T       t1255   o1105 b608 b1255 b4 b4  P       p1255   String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'s}; id{'g}} >> 9 thenT autoT"
3181  B       b1256   t1255  O       o1255   ext_rule p1255
3182  P       p1256   String "equivSubstT << equiv{car{'g}; 'R; id{'g}; id{'s}} >> 0 ttca"  S       s1255   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241
3183  O       o1256   ext_rule p1256  G       s1255   t1123
3184  T       t1256   o669 b545 b670 b978 b977  B       b1256   s1255
3185  S       s1256   t597 h h992 h993 h994 h709 h995 h1228  T       t1256   o629 b1256 b1121
3186  G       s1256   t1256  B       b1257   t1256
3187  B       b1257   s1256  T       t1257   o564 b1155 b560
3188  T       t1257   o611 b1257 b1156  S       s1257   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241
3189  B       b1258   t1257  G       s1257   t1257
3190  T       t1258   o2 b1251  B       b1258   s1257
3191    T       t1258   o629 b1258 b1121
3192  B       b1259   t1258  B       b1259   t1258
 T       t1259   o610 b1258 b4 b1259  
 B       b1260   t1259  
 T       t1260   o669 b545 b670 b1187 b977  
 S       s1260   t597 h h992 h993 h994 h709 h995 h1228  
 G       s1260   t1260  
 B       b1261   s1260  
 T       t1261   o611 b1261 b1156  
 B       b1262   t1261  
 T       t1262   o610 b1262 b4 b1259  
 B       b1263   t1262  
3193  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
3194  O       o1263   equiv_fun_prop  O       o1259   equiv_fun_prop
3195  P       p1263   Var z  P       p1259   Var z
3196  O       o1264   var p1263  O       o1260   var p1259
3197  T       t1264   o1264  T       t1260   o1260
3198    B       b1260   t1260
3199    T       t1261   o575 b560 b578 b1155 b1260
3200    B       b1261   t1261 z
3201    T       t1262   o1259 b560 b578 b1261
3202    S       s1262   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241
3203    G       s1262   t1262
3204    B       b1262   s1262
3205    T       t1263   o629 b1262 b1121
3206    B       b1263   t1263
3207    T       t1264   o2 b1245
3208  B       b1264   t1264  B       b1264   t1264
3209  T       t1265   o669 b545 b670 b1187 b1264  T       t1265   o628 b1263 b711 b1264
3210  B       b1265   t1265 z  B       b1265   t1265
3211  T       t1266   o1263 b545 b670 b1265  T       t1266   o2 b1265
3212  S       s1266   t597 h h992 h993 h994 h709 h995 h1228  B       b1266   t1266
3213  G       s1266   t1266  T       t1267   o628 b1259 b711 b1266
 B       b1266   s1266  
 T       t1267   o611 b1266 b1156  
3214  B       b1267   t1267  B       b1267   t1267
3215  T       t1268   o610 b1267 b4 b1259  T       t1268   o2 b1267
3216  B       b1268   t1268  B       b1268   t1268
3217  T       t1269   o b1268 b4  T       t1269   o628 b1257 b4 b1268
3218  B       b1269   t1269  B       b1269   t1269
3219  T       t1270   o b1263 b1269  S       s1269   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241
3220  B       b1270   t1270  G       s1269   t1151
3221  T       t1271   o b1260 b1270  B       b1270   s1269
3222  B       b1271   t1271  T       t1270   o629 b1270 b1121
3223  T       t1272   o609 b1251 b1271  B       b1271   t1270
3224  B       b1272   t1272  T       t1271   o628 b1271 b4 b1268
3225  P       p1272   String "assertT << equiv{car{'g}; 'R; id{'s}; id{'g}} >> ttca thenT equivSymT 8 ttca thenT withT << id{'s} >> (dT 4) ttca"  B       b1272   t1271
3226  O       o1272   ext_rule p1272  T       t1272   o b1272 b4
3227  T       t1273   o609 b1260 b4  B       b1273   t1272
3228  B       b1273   t1273  T       t1273   o b1269 b1273
3229  T       t1274   o1272 b608 b1273 b4 b4  B       b1274   t1273
3230  B       b1274   t1274  T       t1274   o627 b1245 b1274
3231  P       p1274   String autoT  B       b1275   t1274
3232  O       o1274   ext_rule p1274  T       t1275   o627 b1269 b4
3233  T       t1275   o549 b1187 b545  B       b1276   t1275
3234  S       s1275   t597 h h992 h993 h994 h709 h995 h1228  T       t1276   o1162 b626 b1276 b4 b4
3235  G       s1275   t1275  B       b1277   t1276
3236  B       b1275   s1275  T       t1277   o627 b1272 b4
3237  T       t1276   o611 b1275 b1156  B       b1278   t1277
3238  B       b1276   t1276  T       t1278   o1164 b626 b1278 b4 b4
3239  T       t1277   o610 b1262 b729 b1259  B       b1279   t1278
3240  B       b1277   t1277  T       t1279   o b1279 b4
3241  T       t1278   o2 b1277  B       b1280   t1279
3242  B       b1278   t1278  T       t1280   o b1277 b1280
 T       t1279   o610 b1276 b4 b1278  
 B       b1279   t1279  
 S       s1279   t597 h h992 h993 h994 h709 h995 h1228  
 G       s1279   t1094  
 B       b1280   s1279  
 T       t1280   o611 b1280 b1156  
3243  B       b1281   t1280  B       b1281   t1280
3244  T       t1281   o610 b1281 b4 b1278  T       t1281   o1255 b626 b1275 b1281 b4
3245  B       b1282   t1281  B       b1282   t1281
3246  T       t1282   o713 b1187 b977  T       t1282   o627 b1252 b4
3247  B       b1283   t1282  B       b1283   t1282
3248  T       t1283   o549 b1283 b670  T       t1283   o1084 b626 b1283 b4 b4
3249  S       s1283   t597 h h992 h993 h994 h709 h995 h1228  B       b1284   t1283
3250  G       s1283   t1283  T       t1284   o b1284 b4
 B       b1284   s1283  
 T       t1284   o611 b1284 b1156  
3251  B       b1285   t1284  B       b1285   t1284
3252  T       t1285   o610 b1285 b4 b1278  T       t1285   o b1282 b1285
3253  B       b1286   t1285  B       b1286   t1285
3254  T       t1286   o b1286 b4  T       t1286   o1241 b626 b1255 b1286 b4
3255  B       b1287   t1286  B       b1287   t1286
3256  T       t1287   o b1282 b1287  T       t1287   o b1287 b4
3257  B       b1288   t1287  B       b1288   t1287
3258  T       t1288   o b1279 b1288  T       t1288   o1199 b626 b1241 b1288 b4
3259  B       b1289   t1288  B       b1289   t1288
3260  T       t1289   o609 b1263 b1289  T       t1289   o b1289 b4
3261  B       b1290   t1289  B       b1290   t1289
3262  P       p1290   String "withT << op{'s; inv{'s; 'a}; 'a} >> (dT 4) ttca"  T       t1290   o1166 b626 b1199 b1290 b4
 O       o1290   ext_rule p1290  
 T       t1290   o609 b1279 b4  
3263  B       b1291   t1290  B       b1291   t1290
3264  T       t1291   o1290 b608 b1291 b4 b4  T       t1291   o b1291 b4
3265  B       b1292   t1291  B       b1292   t1291
3266  T       t1292   o609 b1282 b4  T       t1292   o b1166 b1292
3267  B       b1293   t1292  B       b1293   t1292
3268  T       t1293   o1109 b608 b1293 b4 b4  T       t1293   o b1164 b1293
3269  B       b1294   t1293  B       b1294   t1293
3270  P       p1294   String "assertT << equiv{car{'s}; 'R; op{'s; inv{'s; 'a}; 'a}; id{'s}} >> ttca"  T       t1294   o1117 b626 b1162 b1294 b4
3271  O       o1294   ext_rule p1294  B       b1295   t1294
3272  T       t1294   o669 b544 b670 b1187 b977  T       t1295   o624 b1295
 S       s1294   t597 h h992 h993 h994 h709 h995 h1228  
 G       s1294   t1294  
 B       b1295   s1294  
 T       t1295   o611 b1295 b1156  
3273  B       b1296   t1295  B       b1296   t1295
3274  T       t1296   o2 b1286  P       p1296   Number 2375
3275  B       b1297   t1296  O       o1296   resource_defs p254 p1296 p300
3276  T       t1297   o698 b1296 b4 b1297  P       p1297   Number 2373
3277  B       b1298   t1297  O       o1297   uid p1297 p1296
3278  H       h1298   v t1294  T       t1297   o1297 b639
3279  S       s1298   t597 h h992 h993 h994 h709 h995 h1228 h1298  B       b1297   t1297
3280  G       s1298   t1283  T       t1298   o b1297 b4
3281  B       b1299   s1298  B       b1298   t1298
3282  T       t1299   o611 b1299 b1156  T       t1299   o1296 b1298
3283  B       b1300   t1299  B       b1299   t1299
3284  T       t1300   o610 b1300 b4 b1297  T       t1300   o b1299 b4
3285  B       b1301   t1300  B       b1300   t1300
3286  T       t1301   o b1301 b4  T       t1301   o1105 b610 b1117 b1296 b1300
3287  B       b1302   t1301  B       b1301   t1301
3288  T       t1302   o b1298 b1302  T       t1302   o1104 b1301
3289  B       b1303   t1302  B       b1302   t1302
3290  T       t1303   o609 b1286 b1303  P       p1302   Number 2800
3291  B       b1304   t1303  P       p1303   Number 3536
3292  P       p1304   String "withT << 's >> (dT 6) ttca"  O       o1303   location p1302 p1303
3293  O       o1304   ext_rule p1304  P       p1304   String subgroup_isect
3294  T       t1304   o609 b1298 b4  O       o1304   rule p1304
3295  B       b1305   t1304  NSummary!term_param     term_param      term_param Summary
3296  T       t1305   o1304 b608 b1305 b4 b4  O       o1305   term_param
3297  B       b1306   t1305  P       p1305   Var h1
3298  P       p1306   String "rwh unfold_equiv 8 ttca"  O       o1306   var p1305
3299  O       o1306   ext_rule p1306  T       t1306   o1306
3300  T       t1306   o609 b1301 b4  B       b1306   t1306
3301  B       b1307   t1306  T       t1307   o1305 b1306
3302  T       t1307   o1306 b608 b1307 b4 b4  B       b1307   t1307
3303  B       b1308   t1307  P       p1307   Var h2
3304  T       t1308   o b1308 b4  O       o1307   var p1307
3305  B       b1309   t1308  T       t1308   o1307
3306  T       t1309   o b1306 b1309  B       b1308   t1308
3307  B       b1310   t1309  T       t1309   o1305 b1308
3308  T       t1310   o1294 b608 b1304 b1310 b4  B       b1309   t1309
3309  B       b1311   t1310  T       t1310   o b1309 b4
3310  T       t1311   o b1311 b4  B       b1310   t1310
3311  B       b1312   t1311  T       t1311   o b1307 b1310
3312  T       t1312   o b1294 b1312  B       b1311   t1311
3313  B       b1313   t1312  T       t1312   o b609 b1311
3314  T       t1313   o b1292 b1313  B       b1312   t1312
3315  B       b1314   t1313  T       t1313   o613 b614 b1306 b1306
3316  T       t1314   o1274 b608 b1290 b1314 b4  S       s1313   t613 h
3317  B       b1315   t1314  G       s1313   t1313
3318  P       p1315   String "autoT thenT withT << op{'s; inv{'s; 'a}; 'a} >> (dT 4) ttca"  B       b1313   s1313
3319  O       o1315   ext_rule p1315  T       t1314   o611 b1313
3320  T       t1315   o609 b1268 b4  B       b1314   t1314
3321  B       b1316   t1315  T       t1315   o613 b614 b1308 b1308
3322  T       t1316   o1315 b608 b1316 b4 b4  S       s1315   t613 h
3323  B       b1317   t1316  G       s1315   t1315
3324  T       t1317   o b1317 b4  B       b1315   s1315
3325  B       b1318   t1317  T       t1316   o611 b1315
3326  T       t1318   o b1315 b1318  B       b1316   t1316
3327  B       b1319   t1318  P       p1316   Var h
3328  T       t1319   o b1274 b1319  O       o1316   var p1316
3329  B       b1320   t1319  T       t1317   o1316
3330  T       t1320   o1256 b608 b1272 b1320 b4  B       b1317   t1317
3331  B       b1321   t1320  T       t1318   o613 b614 b1317 b1317
3332  T       t1321   o b1321 b4  S       s1318   t613 h
3333  B       b1322   t1321  G       s1318   t1318
3334  T       t1322   o b1256 b1322  B       b1318   s1318
3335  B       b1323   t1322  T       t1319   o611 b1318
3336  T       t1323   o1228 b608 b1254 b1323 b4  B       b1319   t1319
3337  B       b1324   t1323  T       t1320   o557 b1317
3338  T       t1324   o b1324 b4  S       s1320   t620 h
3339  B       b1325   t1324  G       s1320   t1320
3340  T       t1325   o1185 b608 b1228 b1325 b4  B       b1320   s1320
3341  B       b1326   t1325  T       t1321   o611 b1320
3342  P       p1326   String "dT 4 thenT autoT"  B       b1321   t1321
3343  O       o1326   ext_rule p1326  T       t1322   o548 b1306 b550
3344  T       t1326   o549 b550 b545  S       s1322   t620 h
3345  S       s1326   t597 h h992 h993 h994 h709 h995 h1175  G       s1322   t1322
3346  G       s1326   t1326  B       b1322   s1322
3347  B       b1327   s1326  T       t1323   o611 b1322
3348  T       t1327   o611 b1327 b1156  B       b1323   t1323
3349  B       b1328   t1327  T       t1324   o548 b1308 b550
3350  S       s1328   t597 h h992 h993 h716 h995 h1175  S       s1324   t620 h
3351  G       s1328   t1326  G       s1324   t1324
3352  B       b1329   s1328  B       b1324   s1324
3353  T       t1329   o611 b1329 b1156  T       t1325   o611 b1324
3354  B       b1330   t1329  B       b1325   t1325
3355  S       s1330   t597 h h992 h718 h995 h1175  T       t1326   o559 b1317
3356  G       s1330   t1326  B       b1326   t1326
3357  B       b1331   s1330  NCzf_itt_isect  Czf_itt_isect   Czf_itt_isect NIL
3358  T       t1331   o611 b1331 b1156  NCzf_itt_isect!isect    isect   isect Czf_itt_isect
3359  B       b1332   t1331  O       o1326   isect
3360  S       s1332   t597 h h720 h995 h1175  T       t1327   o559 b1306
3361  G       s1332   t1326  B       b1327   t1327
3362  B       b1333   s1332  T       t1328   o559 b1308
3363  T       t1333   o611 b1333 b1156  B       b1328   t1328
3364  B       b1334   t1333  T       t1329   o1326 b1327 b1328
3365  T       t1334   o2 b1182  B       b1329   t1329
3366  B       b1335   t1334  T       t1330   o568 b1326 b1329
3367  T       t1335   o610 b1334 b4 b1335  S       s1330   t620 h
3368  B       b1336   t1335  G       s1330   t1330
3369  T       t1336   o2 b1336  B       b1330   s1330
3370  B       b1337   t1336  T       t1331   o611 b1330
3371  T       t1337   o610 b1332 b4 b1337  B       b1331   t1331
3372  B       b1338   t1337  T       t1332   o564 b565 b1326
3373  T       t1338   o2 b1338  H       h1332   x t1332
3374  B       b1339   t1338  T       t1333   o564 b567 b1326
3375  T       t1339   o610 b1330 b4 b1339  H       h1333   x t1333
3376  B       b1340   t1339  T       t1334   o569 b1317 b565 b567
3377  T       t1340   o2 b1340  B       b1334   t1334
3378  B       b1341   t1340  T       t1335   o569 b1306 b565 b567
3379  T       t1341   o610 b1328 b4 b1341  B       b1335   t1335
3380  B       b1342   t1341  T       t1336   o568 b1334 b1335
3381  T       t1342   o549 b1141 b545  S       s1336   t620 h h651 h652 h1332 h1333
3382  S       s1342   t597 h h992 h993 h994 h709 h995 h1175  G       s1336   t1336
3383  G       s1342   t1342  B       b1336   s1336
3384  B       b1343   s1342  T       t1337   o611 b1336
3385  T       t1343   o611 b1343 b1156  B       b1337   t1337
3386  B       b1344   t1343  T       t1338   o576 b1317
3387  S       s1344   t597 h h992 h993 h716 h995 h1175  B       b1338   t1338
3388  G       s1344   t1342  T       t1339   o575 b1326 b1338 b565 b567
3389  B       b1345   s1344  H       h1339   x t1339
3390  T       t1345   o611 b1345 b1156  T       t1340   o576 b1306
3391  B       b1346   t1345  B       b1340   t1340
3392  S       s1346   t597 h h992 h718 h995 h1175  T       t1341   o575 b1327 b1340 b565 b567
3393  G       s1346   t1342  S       s1341   t620 h h651 h652 h1339
3394  B       b1347   s1346  G       s1341   t1341
3395  T       t1347   o611 b1347 b1156  B       b1341   s1341
3396  B       b1348   t1347  T       t1342   o611 b1341
3397  S       s1348   t597 h h720 h995 h1175  B       b1342   t1342
3398  G       s1348   t1342  T       t1343   o548 b1317 b550
3399  B       b1349   s1348  S       s1343   t620 h
3400  T       t1349   o611 b1349 b1156  G       s1343   t1343
3401  B       b1350   t1349  B       b1343   s1343
3402  T       t1350   o610 b1350 b4 b1335  T       t1344   o611 b1343
3403  B       b1351   t1350  B       b1344   t1344
3404  T       t1351   o2 b1351  T       t1345   o610 b1342 b1344
3405  B       b1352   t1351  B       b1345   t1345
3406  T       t1352   o610 b1348 b4 b1352  T       t1346   o610 b1337 b1345
3407  B       b1353   t1352  B       b1346   t1346
3408  T       t1353   o2 b1353  T       t1347   o610 b1331 b1346
3409  B       b1354   t1353  B       b1347   t1347
3410  T       t1354   o610 b1346 b4 b1354  T       t1348   o610 b1325 b1347
3411  B       b1355   t1354  B       b1348   t1348
3412  T       t1355   o2 b1355  T       t1349   o610 b1323 b1348
3413  B       b1356   t1355  B       b1349   t1349
3414  T       t1356   o610 b1344 b4 b1356  T       t1350   o610 b1321 b1349
3415  B       b1357   t1356  B       b1350   t1350
3416  T       t1357   o b1357 b4  T       t1351   o610 b1319 b1350
3417  B       b1358   t1357  B       b1351   t1351
3418  T       t1358   o b1342 b1358  T       t1352   o610 b1316 b1351
3419  B       b1359   t1358  B       b1352   t1352
3420  T       t1359   o609 b1182 b1359  T       t1353   o610 b1314 b1352
3421  B       b1360   t1359  B       b1353   t1353
3422  P       p1360   String "withT << 'a >> (dT 4) ttca"  T       t1354   o610 b618 b1353
3423  O       o1360   ext_rule p1360  B       b1354   t1354
3424  T       t1360   o609 b1342 b4  P       p1354   String "assumT 6 thenT assumT 7 thenT assumT 8 thenT rwh unfold_subgroup 2 thenT rwh unfold_subgroup 3 thenT autoT"
3425  B       b1361   t1360  O       o1354   ext_rule p1354
3426  T       t1361   o1360 b608 b1361 b4 b4  T       t1355   o b1341 b4
3427  B       b1362   t1361  B       b1355   t1355
3428  P       p1362   String "withT << inv{'s; 'a} >> (dT 4) ttca"  T       t1356   o b1336 b1355
3429  O       o1362   ext_rule p1362  B       b1356   t1356
3430  T       t1362   o609 b1357 b4  T       t1357   o b1330 b1356
3431  B       b1363   t1362  B       b1357   t1357
3432  T       t1363   o1362 b608 b1363 b4 b4  T       t1358   o b1324 b1357
3433  B       b1364   t1363  B       b1358   t1358
3434  T       t1364   o b1364 b4  T       t1359   o b1322 b1358
3435  B       b1365   t1364  B       b1359   t1359
3436  T       t1365   o b1362 b1365  T       t1360   o b1320 b1359
3437  B       b1366   t1365  B       b1360   t1360
3438  T       t1366   o1326 b608 b1360 b1366 b4  T       t1361   o b1318 b1360
3439  B       b1367   t1366  B       b1361   t1361
3440  T       t1367   o b1367 b4  T       t1362   o b1315 b1361
3441  B       b1368   t1367  B       b1362   t1362
3442  T       t1368   o b1326 b1368  T       t1363   o b1313 b1362
3443  B       b1369   t1368  B       b1363   t1363
3444  T       t1369   o1151 b608 b1185 b1369 b4  T       t1364   o b617 b1363
3445  B       b1370   t1369  B       b1364   t1364
3446  T       t1370   o606 b1370  T       t1365   o629 b1343 b1364
3447  B       b1371   t1370  B       b1365   t1365
3448  P       p1372   Number 2585  T       t1366   o628 b1365 b4 b632
3449  P       p1373   Number 2583  B       b1366   t1366
3450  O       o520    location p518 p1373  T       t1367   o557 b1306
3451  P       p520    Number 2268  H       h1367   y_4 t1367
3452  P       p521    Number 2276  H       h1368   y_5 t558
3453  O       o521    resource_defs p520 p521 p300  T       t1368   o558 b1327 b560
3454  P       p522    Number 2274  H       h1369   y_6 t1368
3455  O       o522    uid p522 p521  T       t1369   o564 b565 b1327
3456  T       t524    o522 b623  B       b1369   t1369
3457  B       b524    t524  T       t1370   o564 b567 b1327
3458  T       t525    o b524 b4  B       b1370   t1370
3459  B       b525    t525  T       t1371   o568 b1335 b570
3460  T       t531    o521 b525  B       b1371   t1371
3461  B       b531    t531  T       t1372   o563 b1370 b1371
3462  T       t532    o b531 b4  B       b1372   t1372
3463  B       b532    t532  T       t1373   o563 b1369 b1372
3464  T       t533    o973 b587 b985 b1128 b532  B       b1373   t1373 b
3465  B       b533    t533  T       t1374   o561 b562 b1373
3466  T       t539    o520 b533  B       b1374   t1374 a
3467  B       b539    t539  T       t1375   o561 b562 b1374
3468  P       p541    Number 3031  H       h1375   y_7 t1375
3469  O       o545    location p1372 p541  B       b1375   t1341
3470  P       p545    Number 2613  T       t1376   o563 b1375 b579
3471  P       p546    Number 2621  B       b1376   t1376 b
3472  O       o552    resource_defs p545 p546 p300  T       t1377   o561 b562 b1376
3473  P       p552    Number 2619  B       b1377   t1377 a
3474  O       o555    uid p552 p546  T       t1378   o561 b562 b1377
3475  T       t567    o555 b623  H       h1378   z_2 t1378
3476  B       b567    t567  T       t1379   o557 b1308
3477  T       t568    o b567 b4  H       h1379   y t1379
3478  B       b568    t568  T       t1380   o558 b1328 b560
3479  T       t584    o552 b568  H       h1380   y_2 t1380
3480  B       b584    t584  T       t1381   o564 b565 b1328
 T       t585    o b584 b4  
 B       b585    t585  
 T       t588    o1137 b587 b1151 b1371 b585  
 B       b588    t588  
 T       t606    o545 b588  
 B       b607    t606  
 O       o1378   location p p  
 P       p1378   String subgroup_isect  
 O       o1379   rule p1378  
 P       p1379   Var h1  
 O       o1380   var p1379  
 T       t1380   o1380  
 B       b1380   t1380  
 T       t1381   o666 b1380  
3481  B       b1381   t1381  B       b1381   t1381
3482  P       p1381   Var h2  T       t1382   o564 b567 b1328
 O       o1381   var p1381  
 T       t1382   o1381  
3483  B       b1382   t1382  B       b1382   t1382
3484  T       t1383   o666 b1382  T       t1383   o569 b1308 b565 b567
3485  B       b1383   t1383  B       b1383   t1383
3486  T       t1384   o b1383 b4  T       t1384   o568 b1383 b570
3487  B       b1384   t1384  B       b1384   t1384
3488  T       t1385   o b1381 b1384  T       t1385   o563 b1382 b1384
3489  B       b1385   t1385  B       b1385   t1385
3490  T       t1386   o b586 b1385  T       t1386   o563 b1381 b1385
3491  B       b1386   t1386  B       b1386   t1386 b
3492  T       t1387   o590 b591 b1380 b1380  T       t1387   o561 b562 b1386
3493  S       s1387   t590 h  B       b1387   t1387 a
3494  G       s1387   t1387  T       t1388   o561 b562 b1387
3495  B       b1387   s1387  H       h1388   y_3 t1388
3496  T       t1388   o588 b1387  T       t1389   o576 b1308
3497  B       b1388   t1388  B       b1389   t1389
3498  T       t1389   o590 b591 b1382 b1382  T       t1390   o575 b1328 b1389 b565 b567
 S       s1389   t590 h  
 G       s1389   t1389  
 B       b1389   s1389  
 T       t1390   o588 b1389  
3499  B       b1390   t1390  B       b1390   t1390
3500  P       p1390   Var h  T       t1391   o563 b1390 b579
3501  O       o1390   var p1390  B       b1391   t1391 b
3502  T       t1391   o1390  T       t1392   o561 b562 b1391
3503  B       b1391   t1391  B       b1392   t1392 a
3504  T       t1392   o590 b591 b1391 b1391  T       t1393   o561 b562 b1392
3505  S       s1392   t590 h  H       h1393   z_1 t1393
3506  G       s1392   t1392  H       h1394   v_2 t1330
3507  B       b1392   s1392  H       h1395   x t562
3508  T       t1393   o588 b1392  P       p1395   Var x
3509  B       b1393   t1393  O       o1395   var p1395
3510  T       t1394   o542 b1391  T       t1395   o1395
 S       s1394   t597 h  
 G       s1394   t1394  
 B       b1394   s1394  
 T       t1395   o588 b1394  
3511  B       b1395   t1395  B       b1395   t1395
3512  T       t1396   o533 b534 b1380  T       t1396   o564 b1395 b1326
3513  S       s1396   t597 h  H       h1396   y t1396
3514  G       s1396   t1396  T       t1397   o564 b1395 b560
3515  B       b1396   s1396  S       s1397   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396
3516  T       t1397   o588 b1396  G       s1397   t1397
3517  B       b1397   t1397  B       b1397   s1397
3518  T       t1398   o533 b534 b1382  T       t1398   o629 b1397 b1364
3519  S       s1398   t597 h  B       b1398   t1398
3520  G       s1398   t1398  T       t1399   o558 b1326 b560
3521  B       b1398   s1398  S       s1399   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394
3522  T       t1399   o588 b1398  G       s1399   t1399
3523  B       b1399   t1399  B       b1399   s1399
3524  T       t1400   o544 b1391  T       t1400   o629 b1399 b1364
3525  B       b1400   t1400  B       b1400   t1400
3526  NCzf_itt_isect  Czf_itt_isect   Czf_itt_isect NIL  S       s1400   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394
3527  NCzf_itt_isect!isect    isect   isect Czf_itt_isect  G       s1400   t1343
3528  O       o1400   isect  B       b1401   s1400
3529  T       t1401   o544 b1380  T       t1401   o629 b1401 b1364
3530  B       b1401   t1401  B       b1402   t1401
3531  T       t1402   o544 b1382  B       b1403   t1375
3532  B       b1402   t1402  B       b1404   t1378
3533  T       t1403   o1400 b1401 b1402  T       t1404   o556 b1403 b1404
3534  B       b1403   t1403  H       h1404   z t1404
3535  T       t1404   o553 b1400 b1403  S       s1404   t620 h h1367 h1368 h1369 h1404 h1379 h697 h1380 h1388 h1393 h1394
3536  S       s1404   t597 h  G       s1404   t1343
3537  G       s1404   t1404  B       b1405   s1404
3538  B       b1404   s1404  T       t1405   o629 b1405 b1364
3539  T       t1405   o588 b1404  B       b1406   t1405
3540  B       b1405   t1405  B       b1407   t1368
3541  T       t1406   o549 b550 b1400  B       b1408   t1404
3542  H       h1406   x t1406  T       t1408   o556 b1407 b1408
3543  T       t1407   o549 b552 b1400  H       h1408   z_2 t1408
3544  H       h1407   x t1407  S       s1408   t620 h h1367 h1368 h1408 h1379 h697 h1380 h1388 h1393 h1394
3545  T       t1408   o554 b1391 b550 b552  G       s1408   t1343
3546  B       b1408   t1408  B       b1409   s1408
3547  T       t1409   o553 b1408 b555  T       t1409   o629 b1409 b1364
3548  S       s1409   t597 h h632 h633 h1406 h1407  B       b1410   t1409
3549  G       s1409   t1409  B       b1411   t1408
3550  B       b1409   s1409  T       t1411   o556 b558 b1411
3551  T       t1410   o588 b1409  H       h1411   z t1411
3552  B       b1410   t1410  S       s1411   t620 h h1367 h1411 h1379 h697 h1380 h1388 h1393 h1394
3553  T       t1411   o533 b534 b1391  G       s1411   t1343
3554  S       s1411   t597 h  B       b1412   s1411
3555  G       s1411   t1411  T       t1412   o629 b1412 b1364
3556  B       b1411   s1411  B       b1413   t1412
3557  T       t1412   o588 b1411  B       b1414   t1367
3558  B       b1412   t1412  B       b1415   t1411
3559  T       t1413   o587 b1410 b1412  T       t1415   o556 b1414 b1415
3560  B       b1413   t1413  H       h1415   v t1415
3561  T       t1414   o587 b1405 b1413  S       s1415   t620 h h1415 h1379 h697 h1380 h1388 h1393 h1394
3562  B       b1414   t1414  G       s1415   t1343
3563  T       t1415   o587 b1399 b1414  B       b1416   s1415
3564  B       b1415   t1415  T       t1416   o629 b1416 b1364
3565  T       t1416   o587 b1397 b1415  B       b1417   t1416
3566  B       b1416   t1416  B       b1418   t1388
3567  T       t1417   o587 b1395 b1416  B       b1419   t1393
3568  B       b1417   t1417  T       t1419   o556 b1418 b1419
3569  T       t1418   o587 b1393 b1417  H       h1419   z t1419
3570  B       b1418   t1418  S       s1419   t620 h h1415 h1379 h697 h1380 h1419 h1394
3571  T       t1419   o587 b1390 b1418  G       s1419   t1343
3572  B       b1419   t1419  B       b1420   s1419
3573  T       t1420   o587 b1388 b1419  T       t1420   o629 b1420 b1364
3574  B       b1420   t1420  B       b1421   t1420
3575  T       t1421   o587 b593 b1420  B       b1422   t1380
3576  B       b1421   t1421  B       b1423   t1419
3577  P       p1421   String "assumT 6 thenT assumT 7 thenT assumT 8 thenT rwh unfold_subgroup 2 thenT rwh unfold_subgroup 3 thenT autoT"  T       t1423   o556 b1422 b1423
3578  O       o1421   ext_rule p1421  H       h1423   z_1 t1423
3579  T       t1422   o b1409 b4  S       s1423   t620 h h1415 h1379 h697 h1423 h1394
3580  B       b1422   t1422  G       s1423   t1343
3581  T       t1423   o b1404 b1422  B       b1424   s1423
3582  B       b1423   t1423  T       t1424   o629 b1424 b1364
3583  T       t1424   o b1398 b1423  B       b1425   t1424
3584  B       b1424   t1424  B       b1426   t1423
3585  T       t1425   o b1396 b1424  T       t1426   o556 b558 b1426
3586  B       b1425   t1425  H       h1426   z t1426
3587  T       t1426   o b1394 b1425  S       s1426   t620 h h1415 h1379 h1426 h1394
3588  B       b1426   t1426  G       s1426   t1343
3589  T       t1427   o b1392 b1426  B       b1427   s1426
3590  B       b1427   t1427  T       t1427   o629 b1427 b1364
3591  T       t1428   o b1389 b1427  B       b1428   t1427
3592  B       b1428   t1428  B       b1429   t1379
3593  T       t1429   o b1387 b1428  B       b1430   t1426
3594  B       b1429   t1429  T       t1430   o556 b1429 b1430
3595  T       t1430   o b592 b1429  H       h1430   v_1 t1430
3596  B       b1430   t1430  S       s1430   t620 h h1415 h1430 h1394
3597  T       t1431   o611 b1411 b1430  G       s1430   t1343
3598  B       b1431   t1431  B       b1431   s1430
3599  T       t1432   o610 b1431 b4 b616  T       t1431   o629 b1431 b1364
3600  B       b1432   t1432  B       b1432   t1431
3601  H       h1432   y_3 t542  H       h1432   v_1 t1324
3602  T       t1433   o542 b1380  S       s1432   t620 h h1415 h1432 h1394
3603  H       h1433   y_4 t1433  G       s1432   t1343
3604  T       t1434   o543 b1401 b545  B       b1433   s1432
3605  H       h1434   y_5 t1434  T       t1433   o629 b1433 b1364
3606  T       t1435   o549 b550 b1401  B       b1434   t1433
3607  B       b1435   t1435  H       h1434   v t1322
3608  T       t1436   o549 b552 b1401  S       s1434   t620 h h1434 h1432 h1394
3609  B       b1436   t1436  G       s1434   t1343
3610  T       t1437   o554 b1380 b550 b552  B       b1435   s1434
3611  B       b1437   t1437  T       t1435   o629 b1435 b1364
3612  T       t1438   o553 b1437 b555  B       b1436   t1435
3613  B       b1438   t1438  S       s1436   t620 h h1434 h1432
3614  T       t1439   o548 b1436 b1438  G       s1436   t1343
3615  B       b1439   t1439  B       b1437   s1436
3616  T       t1440   o548 b1435 b1439  T       t1437   o629 b1437 b1364
3617  B       b1440   t1440 b  B       b1438   t1437
3618  T       t1441   o546 b547 b1440  S       s1438   t620 h h1434
3619  B       b1441   t1441 a  G       s1438   t1343
3620  T       t1442   o546 b547 b1441  B       b1439   s1438
3621  H       h1442   z_1 t1442  T       t1439   o629 b1439 b1364
3622  T       t1443   o542 b1382  B       b1440   t1439
3623  H       h1443   y_1 t1443  T       t1440   o2 b1366
3624  T       t1444   o543 b1402 b545  B       b1441   t1440
3625  H       h1444   y_2 t1444  T       t1441   o628 b1440 b4 b1441
3626  T       t1445   o549 b550 b1402  B       b1442   t1441
3627  B       b1445   t1445  T       t1442   o2 b1442
3628  T       t1446   o549 b552 b1402  B       b1443   t1442
3629  B       b1446   t1446  T       t1443   o628 b1438 b4 b1443
3630  T       t1447   o554 b1382 b550 b552  B       b1444   t1443
3631  B       b1447   t1447  T       t1444   o2 b1444
3632  T       t1448   o553 b1447 b555  B       b1445   t1444
3633  B       b1448   t1448  T       t1445   o628 b1436 b4 b1445
3634  T       t1449   o548 b1446 b1448  B       b1446   t1445
3635  B       b1449   t1449  T       t1446   o2 b1446
3636  T       t1450   o548 b1445 b1449  B       b1447   t1446
3637  B       b1450   t1450 b  T       t1447   o628 b1434 b4 b1447
3638  T       t1451   o546 b547 b1450  B       b1448   t1447
3639  B       b1451   t1451 a  T       t1448   o2 b1448
3640  T       t1452   o546 b547 b1451  B       b1449   t1448
3641  H       h1452   z t1452  T       t1449   o628 b1432 b4 b1449
3642  H       h1453   v_2 t1404  B       b1450   t1449
3643  H       h1454   x t547  T       t1450   o2 b1450
3644  T       t1454   o549 b680 b1400  B       b1451   t1450
3645  H       h1455   y t1454  T       t1451   o628 b1428 b4 b1451
3646  T       t1455   o549 b680 b545  B       b1452   t1451
3647  S       s1455   t597 h h1432 h1433 h1434 h1442 h992 h1443 h1444 h1452 h1453 h1454 h1455  T       t1452   o2 b1452
3648  G       s1455   t1455  B       b1453   t1452
3649  B       b1455   s1455  T       t1453   o628 b1425 b4 b1453
3650  T       t1456   o611 b1455 b1430  B       b1454   t1453
3651  B       b1456   t1456  T       t1454   o2 b1454
3652  T       t1457   o543 b1400 b545  B       b1455   t1454
3653  S       s1457   t597 h h1432 h1433 h1434 h1442 h992 h1443 h1444 h1452 h1453  T       t1455   o628 b1421 b4 b1455
3654  G       s1457   t1457  B       b1456   t1455
3655  B       b1457   s1457  T       t1456   o2 b1456
3656  T       t1458   o611 b1457 b1430  B       b1457   t1456
3657  B       b1458   t1458  T       t1457   o628 b1417 b4 b1457
3658  S       s1458   t597 h h1432 h1433 h1434 h1442 h992 h1443 h1444 h1452 h1453  B       b1458   t1457
3659  G       s1458   t1411  T       t1458   o2 b1458
3660  B       b1459   s1458  B       b1459   t1458
3661  T       t1459   o611 b1459 b1430  T       t1459   o628 b1413 b4 b1459
3662  B       b1460   t1459  B       b1460   t1459
3663  B       b1461   t1434  T       t1460   o2 b1460
3664  B       b1462   t1442  B       b1461   t1460
3665  T       t1462   o541 b1461 b1462  T       t1461   o628 b1410 b4 b1461
3666  H       h1462   z_2 t1462  B       b1462   t1461
3667  S       s1462   t597 h h1432 h1433 h1462 h992 h1443 h1444 h1452 h1453  T       t1462   o2 b1462
3668  G       s1462   t1411  B       b1463   t1462
3669  B       b1463   s1462  T       t1463   o628 b1406 b4 b1463
 T       t1463   o611 b1463 b1430  
3670  B       b1464   t1463  B       b1464   t1463
3671  B       b1465   t1433  T       t1464   o2 b1464
3672  B       b1466   t1462  B       b1465   t1464
3673  T       t1466   o541 b1465 b1466  T       t1465   o628 b1402 b711 b1465
3674  H       h1466   z_1 t1466  B       b1466   t1465
3675  S       s1466   t597 h h1432 h1466 h992 h1443 h1444 h1452 h1453  T       t1466   o2 b1466
3676  G       s1466   t1411  B       b1467   t1466
3677  B       b1467   s1466  T       t1467   o628 b1400 b711 b1467
 T       t1467   o611 b1467 b1430  
3678  B       b1468   t1467  B       b1468   t1467
3679  B       b1469   t1466  T       t1468   o2 b1468
3680  T       t1469   o541 b542 b1469  B       b1469   t1468
3681  H       h1469   v t1469  T       t1469   o628 b1398 b4 b1469
3682  S       s1469   t597 h h1469 h992 h1443 h1444 h1452 h1453  B       b1470   t1469
3683  G       s1469   t1411  H       h1470   y t1333
3684  B       b1470   s1469  NCzf_itt_eq!eq  eq      eq Czf_itt_eq
3685  T       t1470   o611 b1470 b1430  O       o1470   eq
3686  B       b1471   t1470  T       t1470   o1470 b1334 b570
3687  B       b1472   t1444  S       s1470   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470
3688  B       b1473   t1452  G       s1470   t1470
3689  T       t1473   o541 b1472 b1473  B       b1471   s1470
3690  H       h1473   z_1 t1473  T       t1471   o629 b1471 b1364
3691  S       s1473   t597 h h1469 h992 h1443 h1473 h1453  B       b1472   t1471
3692  G       s1473   t1411  T       t1472   o568 b1334 b570
3693  B       b1474   s1473  S       s1472   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470
3694  T       t1474   o611 b1474 b1430  G       s1472   t1472
3695    B       b1473   s1472
3696    T       t1473   o629 b1473 b1364
3697    B       b1474   t1473
3698    T       t1474   o628 b1474 b711 b1467
3699  B       b1475   t1474  B       b1475   t1474
3700  B       b1476   t1443  T       t1475   o2 b1475
3701  B       b1477   t1473  B       b1476   t1475
3702  T       t1477   o541 b1476 b1477  T       t1476   o628 b1472 b4 b1476
3703  H       h1477   z t1477  B       b1477   t1476
3704  S       s1477   t597 h h1469 h992 h1477 h1453  T       t1477   o b1477 b4
3705  G       s1477   t1411  B       b1478   t1477
3706  B       b1478   s1477  T       t1478   o b1470 b1478
 T       t1478   o611 b1478 b1430  
3707  B       b1479   t1478  B       b1479   t1478
3708  B       b1480   t1477  T       t1479   o627 b1366 b1479
3709  T       t1480   o541 b542 b1480  B       b1480   t1479
3710  H       h1480   v_1 t1480  P       p1480   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 14 ttca"
3711  S       s1480   t597 h h1469 h1480 h1453  O       o1480   ext_rule p1480
3712  G       s1480   t1411  T       t1480   o564 b1395 b1329
3713    H       h1480   v t1480
3714    S       s1480   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396 h1480
3715    G       s1480   t1397
3716  B       b1481   s1480  B       b1481   s1480
3717  T       t1481   o611 b1481 b1430  T       t1481   o629 b1481 b1364
3718  B       b1482   t1481  B       b1482   t1481
3719  H       h1482   v_1 t1398  T       t1482   o2 b1470
3720  S       s1482   t597 h h1469 h1482 h1453  B       b1483   t1482
3721  G       s1482   t1411  T       t1483   o628 b1482 b4 b1483
 B       b1483   s1482  
 T       t1483   o611 b1483 b1430  
3722  B       b1484   t1483  B       b1484   t1483
3723  H       h1484   v t1396  T       t1484   o b1484 b4
3724  S       s1484   t597 h h1484 h1482 h1453  B       b1485   t1484
3725  G       s1484   t1411  T       t1485   o627 b1470 b1485
 B       b1485   s1484  
 T       t1485   o611 b1485 b1430  
3726  B       b1486   t1485  B       b1486   t1485
3727  S       s1486   t597 h h1484 h1482  P       p1486   String "rwh unfold_bisect 15 thenT dT 15 ttca"
3728  G       s1486   t1411  O       o1486   ext_rule p1486
3729  B       b1487   s1486  NCzf_itt_sep    Czf_itt_sep     Czf_itt_sep NIL
3730  T       t1487   o611 b1487 b1430  NCzf_itt_sep!sep        sep     sep Czf_itt_sep
3731  B       b1488   t1487  O       o1487   sep
3732  S       s1488   t597 h h1484  T       t1487   o564 b1395 b1328
3733  G       s1488   t1411  B       b1487   t1487 x
3734  B       b1489   s1488  T       t1488   o1487 b1327 b1487
3735  T       t1489   o611 b1489 b1430  B       b1488   t1488
3736  B       b1490   t1489  T       t1489   o564 b1395 b1488
3737  T       t1490   o2 b1432  H       h1489   v t1489
3738  B       b1491   t1490  T       t1490   o564 b1395 b1327
3739  T       t1491   o610 b1490 b4 b1491  H       h1490   u t1490
3740    H       h1491   v_1 t1487
3741    S       s1491   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396 h1489 h1490 h1491
3742    G       s1491   t1397
3743    B       b1491   s1491
3744    T       t1491   o629 b1491 b1364
3745  B       b1492   t1491  B       b1492   t1491
3746  T       t1492   o2 b1492  S       s1492   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396 h1489
3747  B       b1493   t1492  G       s1492   t1397
3748  T       t1493   o610 b1488 b4 b1493  B       b1493   s1492
3749    T       t1493   o629 b1493 b1364
3750  B       b1494   t1493  B       b1494   t1493
3751  T       t1494   o2 b1494  T       t1494   o2 b1484
3752  B       b1495   t1494  B       b1495   t1494
3753  T       t1495   o610 b1486 b4 b1495  T       t1495   o628 b1494 b4 b1495
3754  B       b1496   t1495  B       b1496   t1495
3755  T       t1496   o2 b1496  T       t1496   o2 b1496
3756  B       b1497   t1496  B       b1497   t1496
3757  T       t1497   o610 b1484 b4 b1497  T       t1497   o628 b1492 b4 b1497
3758  B       b1498   t1497  B       b1498   t1497
3759  T       t1498   o2 b1498  T       t1498   o b1498 b4
3760  B       b1499   t1498  B       b1499   t1498
3761  T       t1499   o610 b1482 b4 b1499  T       t1499   o627 b1484 b1499
3762  B       b1500   t1499  B       b1500   t1499
3763  T       t1500   o2 b1500  P       p1500   String "withT << 'x >> (dT 4) ttca"
3764    O       o1500   ext_rule p1500
3765    T       t1500   o627 b1498 b4
3766  B       b1501   t1500  B       b1501   t1500
3767  T       t1501   o610 b1479 b4 b1501  T       t1501   o1500 b626 b1501 b4 b4
3768  B       b1502   t1501  B       b1502   t1501
3769  T       t1502   o2 b1502  T       t1502   o b1502 b4
3770  B       b1503   t1502  B       b1503   t1502
3771  T       t1503   o610 b1475 b4 b1503  T       t1503   o1486 b626 b1500 b1503 b4
3772  B       b1504   t1503  B       b1504   t1503
3773  T       t1504   o2 b1504  T       t1504   o b1504 b4
3774  B       b1505   t1504  B       b1505   t1504
3775  T       t1505   o610 b1471 b4 b1505  T       t1505   o1480 b626 b1486 b1505 b4
3776  B       b1506   t1505  B       b1506   t1505
3777  T       t1506   o2 b1506  P       p1506   String "assumT 9 ttca"
3778  B       b1507   t1506  O       o1506   ext_rule p1506
3779  T       t1507   o610 b1468 b4 b1507  B       b1507   t1332
3780  B       b1508   t1507  B       b1508   t1333
3781  T       t1508   o2 b1508  B       b1509   t1336
3782  B       b1509   t1508  T       t1509   o563 b1508 b1509
 T       t1509   o610 b1464 b4 b1509  
3783  B       b1510   t1509  B       b1510   t1509
3784  T       t1510   o2 b1510  T       t1510   o563 b1507 b1510
3785  B       b1511   t1510  B       b1511   t1510 b
3786  T       t1511   o610 b1460 b729 b1511  T       t1511   o561 b562 b1511
3787  B       b1512   t1511  B       b1512   t1511 a
3788  T       t1512   o2 b1512  T       t1512   o561 b562 b1512
3789  B       b1513   t1512  H       h1512   v t1512
3790  T       t1513   o610 b1458 b729 b1513  S       s1512   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512
3791    G       s1512   t1470
3792    B       b1513   s1512
3793    T       t1513   o629 b1513 b1364
3794  B       b1514   t1513  B       b1514   t1513
3795  T       t1514   o2 b1514  T       t1514   o2 b1477
3796  B       b1515   t1514  B       b1515   t1514
3797  T       t1515   o610 b1456 b4 b1515  T       t1515   o628 b1514 b4 b1515
3798  B       b1516   t1515  B       b1516   t1515
3799  T       t1516   o b1516 b4  T       t1516   o b1516 b4
3800  B       b1517   t1516  B       b1517   t1516
3801  T       t1517   o609 b1432 b1517  T       t1517   o627 b1477 b1517
3802  B       b1518   t1517  B       b1518   t1517
3803  P       p1518   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 12 ttca"  P       p1518   String "instHypT [<< 'a >>; << 'b >>] 17 ttca thenT dT 18 ttca thenT dT 18 ttca"
3804  O       o1518   ext_rule p1518  O       o1518   ext_rule p1518
3805  T       t1518   o549 b680 b1403  H       h1518   y_9 t1336
3806  H       h1518   v t1518  S       s1518   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518
3807  S       s1518   t597 h h1432 h1433 h1434 h1442 h992 h1443 h1444 h1452 h1453 h1454 h1455 h1518  G       s1518   t1470
 G       s1518   t1455  
3808  B       b1519   s1518  B       b1519   s1518
3809  T       t1519   o611 b1519 b1430  T       t1519   o629 b1519 b1364
3810  B       b1520   t1519  B       b1520   t1519
3811  T       t1520   o2 b1516  H       h1520   y_8 t1509
3812  B       b1521   t1520  S       s1520   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1520 h1518
3813  T       t1521   o610 b1520 b4 b1521  G       s1520   t1470
3814    B       b1521   s1520
3815    T       t1521   o629 b1521 b1364
3816  B       b1522   t1521  B       b1522   t1521
3817  T       t1522   o b1522 b4  S       s1522   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1520
3818  B       b1523   t1522  G       s1522   t1470
3819  T       t1523   o609 b1516 b1523  B       b1523   s1522
3820    T       t1523   o629 b1523 b1364
3821  B       b1524   t1523  B       b1524   t1523
3822  P       p1524   String "rwh unfold_bisect 13 thenT dT 13 ttca"  H       h1524   w_1 t1510
3823  O       o1524   ext_rule p1524  S       s1524   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1524 h1520
3824  NCzf_itt_sep    Czf_itt_sep     Czf_itt_sep NIL  G       s1524   t1470
3825  NCzf_itt_sep!sep        sep     sep Czf_itt_sep  B       b1525   s1524
3826  O       o1525   sep  T       t1525   o629 b1525 b1364
3827  T       t1525   o549 b680 b1402  B       b1526   t1525
3828  B       b1525   t1525 x  S       s1526   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1524
3829  T       t1526   o1525 b1401 b1525  G       s1526   t1470
3830  B       b1526   t1526  B       b1527   s1526
3831  T       t1527   o549 b680 b1526  T       t1527   o629 b1527 b1364
3832  H       h1527   v t1527  B       b1528   t1527
3833  T       t1528   o549 b680 b1401  H       h1528   w t1511
3834  H       h1528   u t1528  S       s1528   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1528 h1524
3835  H       h1529   v_1 t1525  G       s1528   t1470
3836  S       s1529   t597 h h1432 h1433 h1434 h1442 h992 h1443 h1444 h1452 h1453 h1454 h1455 h1527 h1528 h1529  B       b1529   s1528
3837  G       s1529   t1455  T       t1529   o629 b1529 b1364
 B       b1529   s1529  
 T       t1529   o611 b1529 b1430  
3838  B       b1530   t1529  B       b1530   t1529
3839  S       s1530   t597 h h1432 h1433 h1434 h1442 h992 h1443 h1444 h1452 h1453 h1454 h1455 h1527  S       s1530   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1528
3840  G       s1530   t1455  G       s1530   t1470
3841  B       b1531   s1530  B       b1531   s1530
3842  T       t1531   o611 b1531 b1430  T       t1531   o629 b1531 b1364
3843  B       b1532   t1531  B       b1532   t1531
3844  T       t1532   o2 b1522  T       t1532   o b567 b4
3845  B       b1533   t1532  B       b1533   t1532
3846  T       t1533   o610 b1532 b4 b1533  T       t1533   o882 b1533
3847  B       b1534   t1533  B       b1534   t1533
3848  T       t1534   o2 b1534  T       t1534   o881 b1534
3849  B       b1535   t1534  B       b1535   t1534
3850  T       t1535   o610 b1530 b4 b1535  T       t1535   o b1535 b1003
3851  B       b1536   t1535  B       b1536   t1535
3852  T       t1536   o b1536 b4  T       t1536   o628 b1514 b1224 b1515
3853  B       b1537   t1536  B       b1537   t1536
3854  T       t1537   o609 b1522 b1537  T       t1537   o2 b1537
3855  B       b1538   t1537  B       b1538   t1537
3856  P       p1538   String "withT << 'x >> (dT 4) ttca"  T       t1538   o628 b1532 b1536 b1538
 O       o1538   ext_rule p1538  
 T       t1538   o609 b1536 b4  
3857  B       b1539   t1538  B       b1539   t1538
3858  T       t1539   o1538 b608 b1539 b4 b4  T       t1539   o2 b1539
3859  B       b1540   t1539  B       b1540   t1539
3860  T       t1540   o b1540 b4  T       t1540   o628 b1530 b1003 b1540
3861  B       b1541   t1540  B       b1541   t1540
3862  T       t1541   o1524 b608 b1538 b1541 b4  T       t1541   o2 b1541
3863  B       b1542   t1541  B       b1542   t1541
3864  T       t1542   o b1542 b4  T       t1542   o628 b1528 b4 b1542
3865  B       b1543   t1542  B       b1543   t1542
3866  T       t1543   o1518 b608 b1524 b1543 b4  T       t1543   o2 b1543
3867  B       b1544   t1543  B       b1544   t1543
3868  T       t1544   o b1544 b4  T       t1544   o628 b1526 b4 b1544
3869  B       b1545   t1544  B       b1545   t1544
3870  T       t1545   o1421 b608 b1518 b1545 b4  T       t1545   o2 b1545
3871  B       b1546   t1545  B       b1546   t1545
3872  T       t1546   o606 b1546  T       t1546   o628 b1524 b4 b1546
3873  B       b1547   t1546  B       b1547   t1546
3874  P       p1549   Number 3136  T       t1547   o2 b1547
3875  P       p607    Number 3753  B       b1548   t1547
3876  O       o612    location p1549 p607  T       t1548   o628 b1522 b4 b1548
3877  T       t621    o1379 b1386 b1421 b1547 b4  B       b1549   t1548
3878  B       b621    t621  T       t1549   o2 b1549
3879  T       t622    o612 b621  B       b1550   t1549
3880  B       b622    t622  T       t1550   o628 b1520 b4 b1550
3881  P       p624    Number 3755  B       b1551   t1550
3882  P       p625    Number 3828  T       t1551   o b1551 b4
3883  O       o625    location p624 p625  B       b1552   t1551
3884    T       t1552   o627 b1516 b1552
3885    B       b1553   t1552
3886    P       p1553   String "instHypT [<< 'a >>; << 'b >>] 5 ttca thenT dT 19 ttca"
3887    O       o1553   ext_rule p1553
3888    S       s1553   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518
3889    G       s1553   t1369
3890    B       b1554   s1553
3891    T       t1554   o629 b1554 b1364
3892    B       b1555   t1554
3893    H       h1555   w_1 t1373
3894    S       s1555   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1555
3895    G       s1555   t1369
3896    B       b1556   s1555
3897    T       t1556   o629 b1556 b1364
3898    B       b1557   t1556
3899    S       s1557   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1555
3900    G       s1557   t1470
3901    B       b1558   s1557
3902    T       t1558   o629 b1558 b1364
3903    B       b1559   t1558
3904    H       h1559   w t1374
3905    S       s1559   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1559 h1555
3906    G       s1559   t1470
3907    B       b1560   s1559
3908    T       t1560   o629 b1560 b1364
3909    B       b1561   t1560
3910    S       s1561   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1559
3911    G       s1561   t1470
3912    B       b1562   s1561
3913    T       t1562   o629 b1562 b1364
3914    B       b1563   t1562
3915    T       t1563   o628 b1520 b1224 b1550
3916    B       b1564   t1563
3917    T       t1564   o2 b1564
3918    B       b1565   t1564
3919    T       t1565   o628 b1563 b1536 b1565
3920    B       b1566   t1565
3921    T       t1566   o2 b1566
3922    B       b1567   t1566
3923    T       t1567   o628 b1561 b1003 b1567
3924    B       b1568   t1567
3925    T       t1568   o2 b1568
3926    B       b1569   t1568
3927    T       t1569   o628 b1559 b4 b1569
3928    B       b1570   t1569
3929    T       t1570   o2 b1570
3930    B       b1571   t1570
3931    T       t1571   o751 b1557 b4 b1571
3932    B       b1572   t1571
3933    T       t1572   o2 b1572
3934    B       b1573   t1572
3935    T       t1573   o751 b1555 b4 b1573
3936    B       b1574   t1573
3937    H       h1574   y_8 t1372
3938    S       s1574   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1574
3939    G       s1574   t1470
3940    B       b1575   s1574
3941    T       t1575   o629 b1575 b1364
3942    B       b1576   t1575
3943    S       s1576   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1555 h1574
3944    G       s1576   t1470
3945    B       b1577   s1576
3946    T       t1577   o629 b1577 b1364
3947    B       b1578   t1577
3948    T       t1578   o628 b1578 b4 b1571
3949    B       b1579   t1578
3950    T       t1579   o2 b1579
3951    B       b1580   t1579
3952    T       t1580   o628 b1576 b4 b1580
3953    B       b1581   t1580
3954    T       t1581   o b1581 b4
3955    B       b1582   t1581
3956    T       t1582   o b1574 b1582
3957    B       b1583   t1582
3958    T       t1583   o627 b1551 b1583
3959    B       b1584   t1583
3960    P       p1584   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 15 ttca"
3961    O       o1584   ext_rule p1584
3962    T       t1584   o564 b565 b1329
3963    H       h1584   v_1 t1584
3964    S       s1584   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1584
3965    G       s1584   t1369
3966    B       b1585   s1584
3967    T       t1585   o629 b1585 b1364
3968    B       b1586   t1585
3969    T       t1586   o2 b1574
3970    B       b1587   t1586
3971    T       t1587   o628 b1586 b4 b1587
3972    B       b1588   t1587
3973    T       t1588   o b1588 b4
3974    B       b1589   t1588
3975    T       t1589   o627 b1574 b1589
3976    B       b1590   t1589
3977    P       p1590   String "rwh unfold_bisect 19 thenT dT 19 ttca"
3978    O       o1590   ext_rule p1590
3979    T       t1590   o627 b1588 b4
3980    B       b1591   t1590
3981    T       t1591   o1590 b626 b1591 b4 b4
3982    B       b1592   t1591
3983    T       t1592   o b1592 b4
3984    B       b1593   t1592
3985    T       t1593   o1584 b626 b1590 b1593 b4
3986    B       b1594   t1593
3987    P       p1594   String "dT 19 ttca"
3988    O       o1594   ext_rule p1594
3989    S       s1594   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518
3990    G       s1594   t1370
3991    B       b1595   s1594
3992    T       t1595   o629 b1595 b1364
3993    B       b1596   t1595
3994    S       s1596   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1574
3995    G       s1596   t1370
3996    B       b1597   s1596
3997    T       t1597   o629 b1597 b1364
3998    B       b1598   t1597
3999    T       t1598   o2 b1581
4000    B       b1599   t1598
4001    T