/[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 3559 by xiny, Tue Apr 2 08:08:36 2002 UTC revision 3560 by xiny, Wed Apr 3 05:27:01 2002 UTC
# Line 1435  Line 1435 
1435  T       t553    o546 b552  T       t553    o546 b552
1436  B       b553    t553  B       b553    t553
1437  P       p553    Number 652  P       p553    Number 652
1438  P       p554    Number 958  P       p554    Number 1113
1439  O       o554    location p553 p554  O       o554    location p553 p554
1440  NSummary!rewrite        rewrite rewrite Summary  NSummary!rewrite        rewrite rewrite Summary
1441  P       p555    String unfold_subgroup  P       p555    String unfold_subgroup
# Line 1485  Line 1485 
1485  B       b567    t567  B       b567    t567
1486  T       t568    o564 b567 b559  T       t568    o564 b567 b559
1487  B       b568    t568  B       b568    t568
1488  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1489  NCzf_itt_eq!equal       equal   equal Czf_itt_eq  NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1490  O       o568    equal  O       o568    equiv
1491  NCzf_itt_group!op       op      op Czf_itt_group  NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
1492  O       o569    op  O       o569    eqG
1493  T       t569    o569 b549 b565 b567  T       t569    o569 b549
1494  B       b569    t569  B       b569    t569
1495  T       t570    o569 b550 b565 b567  NCzf_itt_group!op       op      op Czf_itt_group
1496    O       o570    op
1497    T       t570    o570 b549 b565 b567
1498  B       b570    t570  B       b570    t570
1499  T       t571    o568 b569 b570  T       t571    o570 b550 b565 b567
1500  B       b571    t571  B       b571    t571
1501  T       t572    o563 b568 b571  T       t572    o568 b559 b569 b570 b571
1502  B       b572    t572  B       b572    t572
1503  T       t573    o563 b566 b572  T       t573    o563 b568 b572
1504  B       b573    t573 b  B       b573    t573
1505  T       t574    o561 b562 b573  T       t574    o563 b566 b573
1506  B       b574    t574 a  B       b574    t574 b
1507  T       t575    o561 b562 b574  T       t575    o561 b562 b574
1508  B       b575    t575  B       b575    t575 a
1509  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL  T       t576    o561 b562 b575
 NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv  
 O       o575    equiv  
 NCzf_itt_group!eqG      eqG     eqG Czf_itt_group  
 O       o576    eqG  
 T       t576    o576 b549  
1510  B       b576    t576  B       b576    t576
1511  T       t577    o575 b559 b576 b565 b567  T       t577    o568 b559 b569 b565 b567
1512  B       b577    t577  B       b577    t577
1513  T       t578    o576 b550  T       t578    o569 b550
1514  B       b578    t578  B       b578    t578
1515  T       t579    o575 b560 b578 b565 b567  T       t579    o568 b560 b578 b565 b567
1516  B       b579    t579  B       b579    t579
1517  T       t580    o563 b577 b579  T       t580    o563 b577 b579
1518  B       b580    t580 b  B       b580    t580 b
# Line 1523  Line 1520 
1520  B       b581    t581 a  B       b581    t581 a
1521  T       t582    o561 b562 b581  T       t582    o561 b562 b581
1522  B       b582    t582  B       b582    t582
1523  T       t583    o556 b575 b582  T       t583    o563 b579 b577
1524  B       b583    t583  B       b583    t583
1525  T       t584    o556 b561 b583  T       t584    o563 b568 b583
1526  B       b584    t584  B       b584    t584
1527  T       t585    o556 b558 b584  T       t585    o563 b566 b584
1528  B       b585    t585  B       b585    t585 b
1529  T       t586    o556 b557 b585  T       t586    o561 b562 b585
1530  B       b586    t586  B       b586    t586 a
1531  NSummary!prim   prim    prim Summary  T       t587    o561 b562 b586
 O       o586    prim  
 T       t587    o586 b4  
1532  B       b587    t587  B       b587    t587
1533  T       t588    o555 b551 b586 b587 b4  T       t588    o556 b582 b587
1534  B       b588    t588  B       b588    t588
1535  T       t589    o554 b588  T       t589    o556 b576 b588
1536  B       b589    t589  B       b589    t589
1537  P       p589    Number 960  T       t590    o556 b561 b589
1538  P       p590    Number 1063  B       b590    t590
1539  O       o590    location p589 p590  T       t591    o556 b558 b590
1540  NSummary!dform  dform   dform Summary  B       b591    t591
1541  P       p591    String subgroup_df  T       t592    o556 b557 b591
 O       o591    dform p591  
 NSummary!except_mode_df except_mode_df  except_mode_df Summary  
 P       p592    String src  
 O       o592    except_mode_df p592  
 T       t592    o592  
1542  B       b592    t592  B       b592    t592
1543  T       t593    o b592 b4  NSummary!prim   prim    prim Summary
1544    O       o592    prim
1545    T       t593    o592 b4
1546  B       b593    t593  B       b593    t593
1547  NSummary!df_term        df_term df_term Summary  T       t594    o555 b551 b592 b593 b4
 O       o593    df_term  
 NPerv!string    string593       string Perv  
 P       p593    String subgroup(  
 O       o594    string593 p593  
 T       t594    o594  
1548  B       b594    t594  B       b594    t594
1549  Nslot   slot    slot NIL  T       t595    o554 b594
 O       o595    slot  
 T       t595    o595 b549  
1550  B       b595    t595  B       b595    t595
1551  P       p595    String "; "  P       p595    Number 1115
1552  O       o596    string593 p595  P       p596    Number 1218
1553  T       t596    o596  O       o596    location p595 p596
1554  B       b596    t596  NSummary!dform  dform   dform Summary
1555  T       t597    o595 b550  P       p597    String subgroup_df
1556  B       b597    t597  O       o597    dform p597
1557  P       p597    String )  NSummary!except_mode_df except_mode_df  except_mode_df Summary
1558  O       o597    string593 p597  P       p598    String src
1559  T       t598    o597  O       o598    except_mode_df p598
1560    T       t598    o598
1561  B       b598    t598  B       b598    t598
1562  T       t599    o b598 b4  T       t599    o b598 b4
1563  B       b599    t599  B       b599    t599
1564  T       t600    o b597 b599  NSummary!df_term        df_term df_term Summary
1565    O       o599    df_term
1566    NPerv!string    string599       string Perv
1567    P       p599    String subgroup(
1568    O       o600    string599 p599
1569    T       t600    o600
1570  B       b600    t600  B       b600    t600
1571  T       t601    o b596 b600  Nslot   slot    slot NIL
1572    O       o601    slot
1573    T       t601    o601 b549
1574  B       b601    t601  B       b601    t601
1575  T       t602    o b595 b601  P       p601    String "; "
1576    O       o602    string599 p601
1577    T       t602    o602
1578  B       b602    t602  B       b602    t602
1579  T       t603    o b594 b602  T       t603    o601 b550
1580  B       b603    t603  B       b603    t603
1581  T       t604    o593 b603  P       p603    String )
1582    O       o603    string599 p603
1583    T       t604    o603
1584  B       b604    t604  B       b604    t604
1585  T       t605    o591 b593 b551 b604  T       t605    o b604 b4
1586  B       b605    t605  B       b605    t605
1587  T       t606    o590 b605  T       t606    o b603 b605
1588  B       b606    t606  B       b606    t606
1589  P       p606    Number 1082  T       t607    o b602 b606
1590  P       p607    Number 1272  B       b607    t607
1591  O       o607    location p606 p607  T       t608    o b601 b607
1592  NSummary!rule   rule    rule Summary  B       b608    t608
1593  P       p608    String subgroup_type  T       t609    o b600 b608
 O       o608    rule p608  
 NSummary!context_param  context_param   context_param Summary  
 P       p609    String H  
 O       o609    context_param p609  
 T       t609    o609  
1594  B       b609    t609  B       b609    t609
1595  T       t610    o b609 b4  T       t610    o599 b609
1596  B       b610    t610  B       b610    t610
1597    T       t611    o597 b599 b551 b610
1598    B       b611    t611
1599    T       t612    o596 b611
1600    B       b612    t612
1601    P       p612    Number 1237
1602    P       p613    Number 1425
1603    O       o613    location p612 p613
1604    NSummary!rule   rule    rule Summary
1605    P       p614    String subgroup_wf
1606    O       o614    rule p614
1607    NSummary!context_param  context_param   context_param Summary
1608    P       p615    String H
1609    O       o615    context_param p615
1610    T       t615    o615
1611    B       b615    t615
1612    T       t616    o b615 b4
1613    B       b616    t616
1614  NSummary!meta_implies   meta_implies    meta_implies Summary  NSummary!meta_implies   meta_implies    meta_implies Summary
1615  O       o610    meta_implies  O       o616    meta_implies
1616  NSummary!meta_theorem   meta_theorem    meta_theorem Summary  NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1617  O       o611    meta_theorem  O       o617    meta_theorem
1618  NBase_trivial   Base_trivial    Base_trivial NIL  NBase_trivial   Base_trivial    Base_trivial NIL
1619  NBase_trivial!squash    squash  squash Base_trivial  NBase_trivial!squash    squash  squash Base_trivial
1620  O       o612    squash  O       o618    squash
1621  T       t612    o612  T       t618    o618
1622  B       b612    t612  B       b618    t618
1623  T       t613    o b612 b4  T       t619    o b618 b4
1624  C       h       H  C       h       H
1625  NItt_equal      Itt_equal       Itt_equal NIL  NItt_equal      Itt_equal       Itt_equal NIL
1626  NItt_equal!equal        equal613        equal Itt_equal  NItt_equal!equal        equal   equal Itt_equal
1627  O       o613    equal613  O       o619    equal
1628  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL  NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1629  NItt_record_label0!label        label   label Itt_record_label0  NItt_record_label0!label        label   label Itt_record_label0
1630  O       o614    label  O       o620    label
1631  T       t614    o614  T       t620    o620
1632  B       b614    t614  B       b620    t620
1633  T       t615    o613 b614 b549 b549  T       t621    o619 b620 b549 b549
1634  S       s       t613 h  S       s       t619 h
1635  G       s       t615  G       s       t621
1636  B       b615    s  B       b621    s
1637  T       t616    o611 b615  T       t622    o617 b621
 B       b616    t616  
 T       t617    o613 b614 b550 b550  
 S       s617    t613 h  
 G       s617    t617  
 B       b617    s617  
 T       t618    o611 b617  
 B       b618    t618  
 P       p618    Var ext  
 O       o618    var p618  
 T       t619    o618  
 B       b619    t619  
 T       t620    o b619 b4  
 NItt_equal!type type    type Itt_equal  
 O       o620    type  
 T       t621    o620 b551  
 S       s621    t620 h  
 G       s621    t621  
 B       b621    s621  
 T       t622    o611 b621  
1638  B       b622    t622  B       b622    t622
1639  T       t623    o610 b618 b622  T       t623    o619 b620 b550 b550
1640  B       b623    t623  S       s623    t619 h
1641  T       t624    o610 b616 b623  G       s623    t623
1642    B       b623    s623
1643    T       t624    o617 b623
1644  B       b624    t624  B       b624    t624
1645    P       p624    Var ext
1646    O       o624    var p624
1647    T       t625    o624
1648    B       b625    t625
1649    T       t626    o b625 b4
1650    NItt_equal!type type    type Itt_equal
1651    O       o626    type
1652    T       t627    o626 b551
1653    S       s627    t626 h
1654    G       s627    t627
1655    B       b627    s627
1656    T       t628    o617 b627
1657    B       b628    t628
1658    T       t629    o616 b624 b628
1659    B       b629    t629
1660    T       t630    o616 b622 b629
1661    B       b630    t630
1662  NSummary!interactive    interactive     interactive Summary  NSummary!interactive    interactive     interactive Summary
1663  O       o624    interactive  O       o630    interactive
1664  NSummary!ext_rule       ext_rule        ext_rule Summary  NSummary!ext_rule       ext_rule        ext_rule Summary
1665  P       p624    String "rwh unfold_subgroup 0 thenT autoT"  P       p630    String "rwh unfold_subgroup 0 ttca"
1666  O       o625    ext_rule p624  O       o631    ext_rule p630
1667  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  NSummary!status_incomplete      status_incomplete       status_incomplete Summary
1668  O       o626    status_incomplete  O       o632    status_incomplete
1669  T       t626    o626  T       t632    o632
1670  B       b626    t626  B       b632    t632
1671  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
1672  O       o627    ext_unjustified  O       o633    ext_unjustified
1673  NSummary!tactic_arg     tactic_arg      tactic_arg Summary  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
1674  P       p627    String main  P       p633    String main
1675  O       o628    tactic_arg p627  O       o634    tactic_arg p633
1676  NSummary!msequent       msequent        msequent Summary  NSummary!msequent       msequent        msequent Summary
1677  O       o629    msequent  O       o635    msequent
1678  T       t629    o b617 b4  T       t635    o b623 b4
 B       b629    t629  
 T       t630    o b615 b629  
 B       b630    t630  
 T       t631    o629 b621 b630  
 B       b631    t631  
 NSummary!parent_none    parent_none     parent_none Summary  
 O       o631    parent_none  
 T       t632    o631  
 B       b632    t632  
 T       t633    o628 b631 b4 b632  
 B       b633    t633  
 T       t634    o627 b633 b4  
 B       b634    t634  
 T       t635    o625 b626 b634 b4 b4  
1679  B       b635    t635  B       b635    t635
1680  T       t636    o624 b635  T       t636    o b621 b635
1681  B       b636    t636  B       b636    t636
1682  NSummary!resource_defs  resource_defs   resource_defs Summary  T       t637    o635 b627 b636
1683  P       p636    Number 1111  B       b637    t637
1684  P       p637    Number 1119  NSummary!parent_none    parent_none     parent_none Summary
1685  O       o637    resource_defs p636 p637 p300  O       o637    parent_none
1686  NOcaml!uid      uid     uid Ocaml  T       t638    o637
1687  P       p638    Number 1117  B       b638    t638
1688  O       o638    uid p638 p637  T       t639    o634 b637 b4 b638
 P       p639    String []  
 O       o639    uid p639  
 T       t639    o639  
1689  B       b639    t639  B       b639    t639
1690  T       t640    o638 b639  T       t640    o633 b639 b4
1691  B       b640    t640  B       b640    t640
1692  T       t641    o b640 b4  T       t641    o631 b632 b640 b4 b4
1693  B       b641    t641  B       b641    t641
1694  T       t642    o637 b641  T       t642    o630 b641
1695  B       b642    t642  B       b642    t642
1696  T       t643    o b642 b4  NSummary!resource_defs  resource_defs   resource_defs Summary
1697  B       b643    t643  P       p642    Number 1264
1698  T       t644    o608 b610 b624 b636 b643  P       p643    Number 1272
1699  B       b644    t644  O       o643    resource_defs p642 p643 p300
1700  T       t645    o607 b644  NOcaml!uid      uid     uid Ocaml
1701    P       p644    Number 1270
1702    O       o644    uid p644 p643
1703    P       p645    String []
1704    O       o645    uid p645
1705    T       t645    o645
1706  B       b645    t645  B       b645    t645
1707  P       p645    Number 1274  T       t646    o644 b645
1708  O       o645    location p645 p309  B       b646    t646
1709  P       p646    String subgroup_intro  T       t647    o b646 b4
1710  O       o646    rule p646  B       b647    t647
1711  S       s646    t620 h  T       t648    o643 b647
1712  G       s646    t557  B       b648    t648
1713  B       b646    s646  T       t649    o b648 b4
1714  T       t646    o611 b646  B       b649    t649
1715  B       b647    t646  T       t650    o614 b616 b630 b642 b649
1716  S       s647    t620 h  B       b650    t650
1717  G       s647    t558  T       t651    o613 b650
1718  B       b648    s647  B       b651    t651
1719  T       t648    o611 b648  P       p651    Number 1427
1720  B       b649    t648  P       p652    Number 2171
1721  S       s649    t620 h  O       o652    location p651 p652
1722  G       s649    t561  P       p653    String subgroup_intro
1723  B       b650    s649  O       o653    rule p653
1724  T       t650    o611 b650  S       s653    t626 h
1725  B       b651    t650  G       s653    t557
1726  H       h651    a t562  B       b653    s653
1727  H       h652    b t562  T       t653    o617 b653
1728  H       h653    x t566  B       b654    t653
1729  H       h654    y t568  S       s654    t626 h
1730  S       s654    t620 h h651 h652 h653 h654  G       s654    t558
1731  G       s654    t571  B       b655    s654
1732  B       b654    s654  T       t655    o617 b655
1733  T       t654    o611 b654  B       b656    t655
1734  B       b655    t654  S       s656    t626 h
1735  H       h655    x t577  G       s656    t561
1736  S       s655    t620 h h651 h652 h655  B       b657    s656
1737  G       s655    t579  T       t657    o617 b657
1738  B       b656    s655  B       b658    t657
1739  T       t656    o611 b656  H       h658    a t562
1740  B       b657    t656  H       h659    b t562
1741  S       s657    t620 h  H       h660    x t566
1742  G       s657    t551  H       h661    y t568
1743  B       b658    s657  S       s661    t626 h h658 h659 h660 h661
1744  T       t658    o611 b658  G       s661    t572
1745  B       b659    t658  B       b661    s661
1746  T       t659    o610 b657 b659  T       t661    o617 b661
 B       b660    t659  
 T       t660    o610 b655 b660  
 B       b661    t660  
 T       t661    o610 b651 b661  
1747  B       b662    t661  B       b662    t661
1748  T       t662    o610 b649 b662  H       h662    c t562
1749  B       b663    t662  H       h663    d t562
1750  T       t663    o610 b647 b663  P       p663    Var c
1751  B       b664    t663  O       o663    var p663
1752  T       t664    o610 b618 b664  T       t663    o663
1753  B       b665    t664  B       b663    t663
1754  T       t665    o610 b616 b665  P       p664    Var d
1755  B       b666    t665  O       o664    var p664
1756  T       t666    o b656 b4  T       t664    o664
1757  B       b667    t666  B       b664    t664
1758  T       t667    o b654 b667  T       t665    o568 b559 b569 b663 b664
1759  B       b668    t667  H       h665    u t665
1760  T       t668    o b650 b668  T       t666    o568 b560 b578 b663 b664
1761  B       b669    t668  S       s666    t626 h h662 h663 h665
1762  T       t669    o b648 b669  G       s666    t666
1763  B       b670    t669  B       b666    s666
1764  T       t670    o b646 b670  T       t667    o617 b666
1765  B       b671    t670  B       b667    t667
1766  T       t671    o b617 b671  H       h667    p t562
1767  B       b672    t671  H       h668    q t562
1768  T       t672    o b615 b672  P       p668    Var p
1769  B       b673    t672  O       o668    var p668
1770  T       t673    o629 b658 b673  T       t668    o668
1771  B       b674    t673  B       b668    t668
1772  T       t674    o628 b674 b4 b632  T       t669    o564 b668 b559
1773  B       b675    t674  H       h669    x t669
1774  T       t675    o627 b675 b4  P       p669    Var q
1775    O       o669    var p669
1776    T       t670    o669
1777    B       b670    t670
1778    T       t671    o564 b670 b559
1779    H       h671    y t671
1780    T       t672    o568 b560 b578 b668 b670
1781    H       h672    v t672
1782    T       t673    o568 b559 b569 b668 b670
1783    S       s673    t626 h h667 h668 h669 h671 h672
1784    G       s673    t673
1785    B       b673    s673
1786    T       t674    o617 b673
1787    B       b674    t674
1788    S       s674    t626 h
1789    G       s674    t551
1790    B       b675    s674
1791    T       t675    o617 b675
1792  B       b676    t675  B       b676    t675
1793  T       t676    o625 b626 b676 b4 b4  T       t676    o616 b674 b676
1794  B       b677    t676  B       b677    t676
1795  T       t677    o624 b677  T       t677    o616 b667 b677
1796  B       b678    t677  B       b678    t677
1797  P       p678    Number 1304  T       t678    o616 b662 b678
1798  P       p679    Number 1312  B       b679    t678
1799  O       o679    resource_defs p678 p679 p300  T       t679    o616 b658 b679
1800  P       p680    Number 1310  B       b680    t679
1801  O       o680    uid p680 p679  T       t680    o616 b656 b680
1802  T       t680    o680 b639  B       b681    t680
1803  B       b680    t680  T       t681    o616 b654 b681
1804  T       t681    o b680 b4  B       b682    t681
1805  B       b681    t681  T       t682    o616 b624 b682
1806  T       t682    o679 b681  B       b683    t682
1807  B       b682    t682  T       t683    o616 b622 b683
1808  T       t683    o b682 b4  B       b684    t683
1809  B       b683    t683  T       t684    o b673 b4
1810  T       t684    o646 b610 b666 b678 b683  B       b685    t684
1811  B       b684    t684  T       t685    o b666 b685
1812  T       t685    o645 b684  B       b686    t685
1813  B       b685    t685  T       t686    o b661 b686
1814  P       p685    Number 1844  B       b687    t686
1815  P       p686    Number 2083  T       t687    o b657 b687
1816  O       o686    location p685 p686  B       b688    t687
1817  P       p687    String subgroup_equiv  T       t688    o b655 b688
1818  O       o687    rule p687  B       b689    t688
1819  T       t687    o575 b559 b578  T       t689    o b653 b689
1820  S       s687    t620 h  B       b690    t689
1821  G       s687    t687  T       t690    o b623 b690
1822  B       b687    s687  B       b691    t690
1823  T       t688    o611 b687  T       t691    o b621 b691
1824  B       b688    t688  B       b692    t691
1825  T       t689    o610 b659 b688  T       t692    o635 b675 b692
1826  B       b689    t689  B       b693    t692
1827  T       t690    o610 b618 b689  T       t693    o634 b693 b4 b638
1828  B       b690    t690  B       b694    t693
1829  T       t691    o610 b616 b690  T       t694    o633 b694 b4
1830  B       b691    t691  B       b695    t694
1831  P       p691    String "assumT 3 thenT rwh unfold_subgroup 2 thenT autoT"  T       t695    o631 b632 b695 b4 b4
1832  O       o691    ext_rule p691  B       b696    t695
1833  T       t692    o b658 b4  T       t696    o630 b696
1834  B       b692    t692  B       b697    t696
1835  T       t693    o b617 b692  P       p697    Number 1457
1836  B       b693    t693  P       p698    Number 1465
1837  T       t694    o b615 b693  O       o698    resource_defs p697 p698 p300
1838  B       b694    t694  P       p699    Number 1463
1839  T       t695    o629 b687 b694  O       o699    uid p699 p698
1840  B       b695    t695  T       t699    o699 b645
1841  T       t696    o628 b695 b4 b632  B       b699    t699
1842  B       b696    t696  T       t700    o b699 b4
1843  H       h696    y t557  B       b700    t700
1844  H       h697    y_1 t558  T       t701    o698 b700
1845  H       h698    y_2 t561  B       b701    t701
1846  H       h699    y_3 t575  T       t702    o b701 b4
 H       h700    z_1 t582  
 H       h701    c t562  
 H       h702    x t568  
 P       p702    Var c  
 O       o702    var p702  
 T       t702    o702  
1847  B       b702    t702  B       b702    t702
1848  T       t703    o564 b702 b559  T       t703    o653 b616 b684 b697 b702
1849  H       h703    y t703  B       b703    t703
1850  T       t704    o575 b559 b578 b567 b702  T       t704    o652 b703
1851  H       h704    u t704  B       b704    t704
1852  T       t705    o575 b559 b578 b702 b567  P       p704    Number 2173
1853  S       s705    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704  P       p705    Number 2412
1854  G       s705    t705  O       o705    location p704 p705
1855  B       b705    s705  P       p706    String subgroup_equiv
1856  T       t706    o629 b705 b694  O       o706    rule p706
1857  B       b706    t706  T       t706    o568 b559 b578
1858  S       s706    t620 h h696 h697 h698 h699 h700  S       s706    t626 h
1859  G       s706    t687  G       s706    t706
1860  B       b707    s706  B       b706    s706
1861  T       t707    o629 b707 b694  T       t707    o617 b706
1862  B       b708    t707  B       b707    t707
1863  NSummary!arg_named      arg_named       arg_named Summary  T       t708    o616 b676 b707
1864  P       p708    String d_auto  B       b708    t708
1865  O       o708    arg_named p708  T       t709    o616 b624 b708
 NSummary!arg_bool       arg_bool        arg_bool Summary  
 P       p709    String true  
 O       o709    arg_bool p709  
 T       t709    o709  
1866  B       b709    t709  B       b709    t709
1867  T       t710    o708 b709  T       t710    o616 b622 b709
1868  B       b710    t710  B       b710    t710
1869  T       t711    o b710 b4  P       p710    String "assumT 3 thenT rwh unfold_subgroup 2 thenT autoT"
1870    O       o710    ext_rule p710
1871    T       t711    o b675 b4
1872  B       b711    t711  B       b711    t711
1873  H       h711    z t583  T       t712    o b623 b711
1874  S       s711    t620 h h696 h697 h698 h711  B       b712    t712
1875  G       s711    t687  T       t713    o b621 b712
1876  B       b712    s711  B       b713    t713
1877  T       t712    o629 b712 b694  T       t714    o635 b706 b713
1878  B       b713    t712  B       b714    t714
1879  H       h713    z_1 t584  T       t715    o634 b714 b4 b638
1880  S       s713    t620 h h696 h697 h713  B       b715    t715
1881  G       s713    t687  H       h715    y t557
1882  B       b714    s713  H       h716    y_1 t558
1883  T       t714    o629 b714 b694  H       h717    y_2 t561
1884  B       b715    t714  H       h718    y_3 t576
1885  H       h715    z t585  H       h719    y_4 t582
1886  S       s715    t620 h h696 h715  H       h720    z t587
1887  G       s715    t687  H       h721    x t568
1888  B       b716    s715  T       t721    o564 b663 b559
1889  T       t716    o629 b716 b694  H       h722    y t721
1890  B       b717    t716  T       t722    o568 b559 b578 b567 b663
1891  H       h717    v t586  H       h723    u t722
1892  S       s717    t620 h h717  T       t723    o568 b559 b578 b663 b567
1893  G       s717    t687  S       s723    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723
1894  B       b718    s717  G       s723    t723
1895  T       t718    o629 b718 b694  B       b723    s723
1896  B       b719    t718  T       t724    o635 b723 b713
1897  H       h719    v t551  B       b724    t724
1898  S       s719    t620 h h719  S       s724    t626 h h715 h716 h717 h718 h719 h720
1899  G       s719    t687  G       s724    t706
1900  B       b720    s719  B       b725    s724
1901  T       t720    o629 b720 b694  T       t725    o635 b725 b713
 B       b721    t720  
 T       t721    o2 b696  
 B       b722    t721  
 T       t722    o628 b721 b4 b722  
 B       b723    t722  
 T       t723    o2 b723  
 B       b724    t723  
 T       t724    o628 b719 b4 b724  
 B       b725    t724  
 T       t725    o2 b725  
1902  B       b726    t725  B       b726    t725
1903  T       t726    o628 b717 b4 b726  NSummary!arg_named      arg_named       arg_named Summary
1904  B       b727    t726  P       p726    String d_auto
1905  T       t727    o2 b727  O       o726    arg_named p726
1906  B       b728    t727  NSummary!arg_bool       arg_bool        arg_bool Summary
1907  T       t728    o628 b715 b4 b728  P       p727    String true
1908  B       b729    t728  O       o727    arg_bool p727
1909  T       t729    o2 b729  T       t727    o727
1910  B       b730    t729  B       b727    t727
1911  T       t730    o628 b713 b4 b730  T       t728    o726 b727
1912    B       b728    t728
1913    T       t729    o b728 b4
1914    B       b729    t729
1915    H       h729    z_1 t588
1916    S       s729    t626 h h715 h716 h717 h718 h729
1917    G       s729    t706
1918    B       b730    s729
1919    T       t730    o635 b730 b713
1920  B       b731    t730  B       b731    t730
1921  T       t731    o2 b731  H       h731    z t589
1922  B       b732    t731  S       s731    t626 h h715 h716 h717 h731
1923  T       t732    o628 b708 b711 b732  G       s731    t706
1924    B       b732    s731
1925    T       t732    o635 b732 b713
1926  B       b733    t732  B       b733    t732
1927  T       t733    o2 b733  H       h733    z_1 t590
1928  B       b734    t733  S       s733    t626 h h715 h716 h733
1929  T       t734    o628 b706 b4 b734  G       s733    t706
1930    B       b734    s733
1931    T       t734    o635 b734 b713
1932  B       b735    t734  B       b735    t734
1933  H       h735    d t562  H       h735    z t591
1934  H       h736    e t562  S       s735    t626 h h715 h735
1935  H       h737    f t562  G       s735    t706
1936  P       p737    Var d  B       b736    s735
1937  O       o737    var p737  T       t736    o635 b736 b713
1938  T       t737    o737  B       b737    t736
1939  B       b737    t737  H       h737    v t592
1940  T       t738    o564 b737 b559  S       s737    t626 h h737
1941  H       h738    x t738  G       s737    t706
1942  P       p738    Var e  B       b738    s737
1943  O       o738    var p738  T       t738    o635 b738 b713
1944  T       t739    o738  B       b739    t738
1945  B       b739    t739  H       h739    v t551
1946  T       t740    o564 b739 b559  S       s739    t626 h h739
1947  H       h740    y t740  G       s739    t706
1948  P       p740    Var f  B       b740    s739
1949  O       o740    var p740  T       t740    o635 b740 b713
1950  T       t741    o740  B       b741    t740
1951  B       b741    t741  T       t741    o2 b715
1952  T       t742    o564 b741 b559  B       b742    t741
1953  H       h742    z t742  T       t742    o634 b741 b4 b742
1954  T       t743    o575 b559 b578 b737 b739  B       b743    t742
1955  H       h743    u t743  T       t743    o2 b743
1956  T       t744    o575 b559 b578 b739 b741  B       b744    t743
1957  H       h744    v t744  T       t744    o634 b739 b4 b744
1958  T       t745    o575 b559 b578 b737 b741  B       b745    t744
1959  S       s745    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744  T       t745    o2 b745
1960  G       s745    t745  B       b746    t745
1961  B       b745    s745  T       t746    o634 b737 b4 b746
1962  T       t746    o629 b745 b694  B       b747    t746
1963  B       b746    t746  T       t747    o2 b747
1964  T       t747    o628 b746 b4 b734  B       b748    t747
1965  B       b747    t747  T       t748    o634 b735 b4 b748
1966  T       t748    o b747 b4  B       b749    t748
1967  B       b748    t748  T       t749    o2 b749
1968  T       t749    o b735 b748  B       b750    t749
1969  B       b749    t749  T       t750    o634 b733 b4 b750
1970  T       t750    o627 b696 b749  B       b751    t750
1971  B       b750    t750  T       t751    o2 b751
1972  P       p750    String "assertT << equiv{car{'g}; eqG{'g}; 'b; 'c} >> thenT autoT"  B       b752    t751
1973  O       o750    ext_rule p750  T       t752    o634 b731 b4 b752
1974  P       p751    String assertion  B       b753    t752
1975  O       o751    tactic_arg p751  T       t753    o2 b753
1976  T       t751    o575 b560 b578 b567 b702  B       b754    t753
1977  S       s751    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704  T       t754    o634 b726 b729 b754
1978  G       s751    t751  B       b755    t754
1979  B       b751    s751  T       t755    o2 b755
 T       t752    o629 b751 b694  
 B       b752    t752  
 T       t753    o2 b735  
 B       b753    t753  
 T       t754    o751 b752 b4 b753  
 B       b754    t754  
 H       h754    v t751  
 S       s754    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754  
 G       s754    t705  
 B       b755    s754  
 T       t755    o629 b755 b694  
1980  B       b756    t755  B       b756    t755
1981  T       t756    o628 b756 b4 b753  T       t756    o634 b724 b4 b756
1982  B       b757    t756  B       b757    t756
1983  T       t757    o b757 b4  H       h757    e t562
1984  B       b758    t757  H       h758    f t562
1985  T       t758    o b754 b758  T       t758    o564 b664 b559
1986  B       b759    t758  H       h759    x t758
1987  T       t759    o627 b735 b759  P       p759    Var e
1988  B       b760    t759  O       o759    var p759
1989  P       p760    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 11 thenT autoT"  T       t759    o759
1990  O       o760    ext_rule p760  B       b759    t759
1991  NCzf_itt_set!isset      isset   isset Czf_itt_set  T       t760    o564 b759 b559
1992  O       o761    isset  H       h760    y t760
1993  T       t761    o761 b559  P       p760    Var f
1994  H       h761    y_6 t761  O       o760    var p760
1995  T       t762    o761 b578  T       t761    o760
1996  H       h762    y_5 t762  B       b761    t761
1997  T       t763    o761 b567  T       t762    o564 b761 b559
1998  H       h763    y_7 t763  H       h762    z t762
1999  T       t764    o761 b702  T       t763    o568 b559 b578 b664 b759
2000  H       h764    z_2 t764  H       h763    u t763
2001  H       h765    y_4 t568  T       t764    o568 b559 b578 b759 b761
2002  H       h766    z_3 t703  H       h764    v t764
2003  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL  T       t765    o568 b559 b578 b664 b761
2004  NCzf_itt_pair!pair      pair    pair Czf_itt_pair  S       s765    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764
2005  O       o766    pair  G       s765    t765
2006  T       t766    o766 b567 b702  B       b765    s765
2007    T       t766    o635 b765 b713
2008  B       b766    t766  B       b766    t766
2009  T       t767    o564 b766 b578  T       t767    o634 b766 b4 b756
2010  H       h767    z t767  B       b767    t767
2011  T       t768    o564 b567 b560  T       t768    o b767 b4
2012  S       s768    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767  B       b768    t768
2013  G       s768    t768  T       t769    o b757 b768
 B       b768    s768  
 T       t769    o629 b768 b694  
2014  B       b769    t769  B       b769    t769
2015  B       b770    t768  T       t770    o633 b715 b769
2016  T       t770    o564 b702 b560  B       b770    t770
2017  B       b771    t770  P       p770    String "assertT << equiv{car{'g}; eqG{'g}; 'b; 'c} >> thenT autoT"
2018  T       t771    o556 b770 b771  O       o770    ext_rule p770
2019  S       s771    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767  P       p771    String assertion
2020    O       o771    tactic_arg p771
2021    T       t771    o568 b560 b578 b567 b663
2022    S       s771    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723
2023  G       s771    t771  G       s771    t771
2024  B       b772    s771  B       b771    s771
2025  T       t772    o629 b772 b694  T       t772    o635 b771 b713
2026  B       b773    t772  B       b772    t772
2027  T       t773    o761 b560  T       t773    o2 b757
2028  B       b774    t773  B       b773    t773
2029  B       b775    t762  T       t774    o771 b772 b4 b773
2030  B       b776    t763  B       b774    t774
2031  B       b777    t764  H       h774    v t771
2032  T       t777    o556 b776 b777  S       s774    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723 h774
2033    G       s774    t723
2034    B       b775    s774
2035    T       t775    o635 b775 b713
2036    B       b776    t775
2037    T       t776    o634 b776 b4 b773
2038    B       b777    t776
2039    T       t777    o b777 b4
2040  B       b778    t777  B       b778    t777
2041  T       t778    o556 b775 b778  T       t778    o b774 b778
2042  B       b779    t778  B       b779    t778
2043  T       t779    o556 b774 b779  T       t779    o633 b757 b779
2044  B       b780    t779  B       b780    t779
2045  B       b781    t771  P       p780    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 12 thenT autoT"
2046  T       t781    o556 b780 b781  O       o780    ext_rule p780
2047  S       s781    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767  NCzf_itt_set!isset      isset   isset Czf_itt_set
2048  G       s781    t781  O       o781    isset
2049  B       b782    s781  T       t781    o781 b559
2050  T       t782    o629 b782 b694  H       h781    y_7 t781
2051  B       b783    t782  T       t782    o781 b578
2052  B       b784    t781  H       h782    y_6 t782
2053  B       b785    t767  T       t783    o781 b567
2054  T       t785    o556 b784 b785  H       h783    y_8 t783
2055  S       s785    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767  T       t784    o781 b663
2056  G       s785    t785  H       h784    z_2 t784
2057  B       b786    s785  H       h785    y_5 t568
2058  T       t786    o629 b786 b694  H       h786    z_3 t721
2059  B       b787    t786  NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL
2060  H       h787    z_4 t777  NCzf_itt_pair!pair      pair    pair Czf_itt_pair
2061  S       s787    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h787 h765 h766 h767  O       o786    pair
2062  G       s787    t785  T       t786    o786 b567 b663
2063  B       b788    s787  B       b786    t786
2064  T       t788    o629 b788 b694  T       t787    o564 b786 b578
2065  B       b789    t788  H       h787    z_1 t787
2066  H       h789    z_2 t778  T       t788    o564 b567 b560
2067  S       s789    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h789 h765 h766 h767  S       s788    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787
2068  G       s789    t785  G       s788    t788
2069  B       b790    s789  B       b788    s788
2070  T       t790    o629 b790 b694  T       t789    o635 b788 b713
2071    B       b789    t789
2072    B       b790    t788
2073    T       t790    o564 b663 b560
2074  B       b791    t790  B       b791    t790
2075  B       b792    t761  T       t791    o556 b790 b791
2076  T       t792    o556 b792 b779  S       s791    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787
2077  H       h792    y_5 t792  G       s791    t791
2078  S       s792    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h792 h765 h766 h767  B       b792    s791
2079  G       s792    t785  T       t792    o635 b792 b713
2080  B       b793    s792  B       b793    t792
2081  T       t793    o629 b793 b694  T       t793    o781 b560
2082  B       b794    t793  B       b794    t793
2083  B       b795    t703  B       b795    t782
2084  T       t795    o556 b568 b795  B       b796    t783
2085  H       h795    z_2 t795  B       b797    t784
2086  S       s795    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h792 h795 h767  T       t797    o556 b796 b797
2087  G       s795    t785  B       b798    t797
2088  B       b796    s795  T       t798    o556 b795 b798
2089  T       t796    o629 b796 b694  B       b799    t798
2090  B       b797    t796  T       t799    o556 b794 b799
2091  B       b798    t792  B       b800    t799
2092  B       b799    t795  B       b801    t791
2093  T       t799    o556 b798 b799  T       t801    o556 b800 b801
2094  H       h799    y_4 t799  S       s801    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787
2095  S       s799    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h799 h767  G       s801    t801
2096  G       s799    t785  B       b802    s801
2097  B       b800    s799  T       t802    o635 b802 b713
2098  T       t800    o629 b800 b694  B       b803    t802
2099  B       b801    t800  B       b804    t801
2100  B       b802    t799  B       b805    t787
2101  T       t802    o556 b802 b785  T       t805    o556 b804 b805
2102  H       h802    u t802  S       s805    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787
2103  S       s802    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h802  G       s805    t805
2104  G       s802    t785  B       b806    s805
2105  B       b803    s802  T       t806    o635 b806 b713
 T       t803    o629 b803 b694  
 B       b804    t803  
 S       s804    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704  
 G       s804    t785  
 B       b805    s804  
 T       t805    o629 b805 b694  
 B       b806    t805  
 T       t806    o2 b754  
2106  B       b807    t806  B       b807    t806
2107  T       t807    o751 b806 b4 b807  H       h807    z_4 t797
2108  B       b808    t807  S       s807    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h807 h785 h786 h787
2109  T       t808    o2 b808  G       s807    t805
2110    B       b808    s807
2111    T       t808    o635 b808 b713
2112  B       b809    t808  B       b809    t808
2113  T       t809    o751 b804 b4 b809  H       h809    z_2 t798
2114  B       b810    t809  S       s809    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h809 h785 h786 h787
2115  T       t810    o2 b810  G       s809    t805
2116    B       b810    s809
2117    T       t810    o635 b810 b713
2118  B       b811    t810  B       b811    t810
2119  T       t811    o628 b801 b4 b811  B       b812    t781
2120  B       b812    t811  T       t812    o556 b812 b799
2121  T       t812    o2 b812  H       h812    y_6 t812
2122  B       b813    t812  S       s812    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h812 h785 h786 h787
2123  T       t813    o628 b797 b4 b813  G       s812    t805
2124    B       b813    s812
2125    T       t813    o635 b813 b713
2126  B       b814    t813  B       b814    t813
2127  T       t814    o2 b814  B       b815    t721
2128  B       b815    t814  T       t815    o556 b568 b815
2129  T       t815    o628 b794 b4 b815  H       h815    z_2 t815
2130  B       b816    t815  S       s815    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h812 h815 h787
2131  T       t816    o2 b816  G       s815    t805
2132    B       b816    s815
2133    T       t816    o635 b816 b713
2134  B       b817    t816  B       b817    t816
2135  T       t817    o628 b791 b4 b817  B       b818    t812
2136  B       b818    t817  B       b819    t815
2137  T       t818    o2 b818  T       t819    o556 b818 b819
2138  B       b819    t818  H       h819    y_5 t819
2139  T       t819    o628 b789 b4 b819  S       s819    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h819 h787
2140  B       b820    t819  G       s819    t805
2141  T       t820    o2 b820  B       b820    s819
2142    T       t820    o635 b820 b713
2143  B       b821    t820  B       b821    t820
2144  T       t821    o628 b787 b711 b821  B       b822    t819
2145  B       b822    t821  T       t822    o556 b822 b805
2146  T       t822    o2 b822  H       h822    u t822
2147  B       b823    t822  S       s822    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h822
2148  T       t823    o628 b783 b711 b823  G       s822    t805
2149    B       b823    s822
2150    T       t823    o635 b823 b713
2151  B       b824    t823  B       b824    t823
2152  T       t824    o2 b824  S       s824    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723
2153  B       b825    t824  G       s824    t805
2154  T       t825    o628 b773 b711 b825  B       b825    s824
2155    T       t825    o635 b825 b713
2156  B       b826    t825  B       b826    t825
2157  T       t826    o2 b826  T       t826    o2 b774
2158  B       b827    t826  B       b827    t826
2159  T       t827    o628 b769 b4 b827  T       t827    o771 b826 b4 b827
2160  B       b828    t827  B       b828    t827
2161  S       s828    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h761 h762 h763 h764 h765 h766 h767  T       t828    o2 b828
2162  G       s828    t770  B       b829    t828
2163  B       b829    s828  T       t829    o771 b824 b4 b829
 T       t829    o629 b829 b694  
2164  B       b830    t829  B       b830    t829
2165  T       t830    o628 b830 b4 b827  T       t830    o2 b830
2166  B       b831    t830  B       b831    t830
2167  T       t831    o b831 b4  T       t831    o634 b821 b4 b831
2168  B       b832    t831  B       b832    t831
2169  T       t832    o b828 b832  T       t832    o2 b832
2170  B       b833    t832  B       b833    t832
2171  T       t833    o627 b754 b833  T       t833    o634 b817 b4 b833
2172  B       b834    t833  B       b834    t833
2173  P       p834    String "withT << 'b >> (dT 4) ttca"  T       t834    o2 b834
 O       o834    ext_rule p834  
 T       t834    o627 b828 b4  
2174  B       b835    t834  B       b835    t834
2175  T       t835    o834 b626 b835 b4 b4  T       t835    o634 b814 b4 b835
2176  B       b836    t835  B       b836    t835
2177  P       p836    String "withT << 'c >> (dT 4) ttca"  T       t836    o2 b836
 O       o836    ext_rule p836  
 T       t836    o627 b831 b4  
2178  B       b837    t836  B       b837    t836
2179  T       t837    o836 b626 b837 b4 b4  T       t837    o634 b811 b4 b837
2180  B       b838    t837  B       b838    t837
2181  T       t838    o b838 b4  T       t838    o2 b838
2182  B       b839    t838  B       b839    t838
2183  T       t839    o b836 b839  T       t839    o634 b809 b4 b839
2184  B       b840    t839  B       b840    t839
2185  T       t840    o760 b626 b834 b840 b4  T       t840    o2 b840
2186  B       b841    t840  B       b841    t840
2187  P       p841    String "assertT << equiv{car{'g}; eqG{'g}; 'c; 'b} >> thenT autoT"  T       t841    o634 b807 b729 b841
2188  O       o841    ext_rule p841  B       b842    t841
2189  T       t841    o575 b560 b578 b702 b567  T       t842    o2 b842
 S       s841    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754  
 G       s841    t841  
 B       b842    s841  
 T       t842    o629 b842 b694  
2190  B       b843    t842  B       b843    t842
2191  T       t843    o2 b757  T       t843    o634 b803 b729 b843
2192  B       b844    t843  B       b844    t843
2193  T       t844    o751 b843 b4 b844  T       t844    o2 b844
2194  B       b845    t844  B       b845    t844
2195  H       h845    v_1 t841  T       t845    o634 b793 b729 b845
2196  S       s845    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754 h845  B       b846    t845
2197  G       s845    t705  T       t846    o2 b846
 B       b846    s845  
 T       t846    o629 b846 b694  
2198  B       b847    t846  B       b847    t846
2199  T       t847    o628 b847 b4 b844  T       t847    o634 b789 b4 b847
2200  B       b848    t847  B       b848    t847
2201  T       t848    o b848 b4  S       s848    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h781 h782 h783 h784 h785 h786 h787
2202  B       b849    t848  G       s848    t790
2203  T       t849    o b845 b849  B       b849    s848
2204    T       t849    o635 b849 b713
2205  B       b850    t849  B       b850    t849
2206  T       t850    o627 b757 b850  T       t850    o634 b850 b4 b847
2207  B       b851    t850  B       b851    t850
2208  P       p851    String "equivSymT ttca"  T       t851    o b851 b4
2209  O       o851    ext_rule p851  B       b852    t851
2210  S       s851    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754  T       t852    o b848 b852
 G       s851    t768  
 B       b852    s851  
 T       t852    o629 b852 b694  
2211  B       b853    t852  B       b853    t852
2212  T       t853    o2 b845  T       t853    o633 b774 b853
2213  B       b854    t853  B       b854    t853
2214  T       t854    o751 b853 b4 b854  P       p854    String "withT << 'b >> (dT 4) ttca"
2215    O       o854    ext_rule p854
2216    T       t854    o633 b848 b4
2217  B       b855    t854  B       b855    t854
2218  S       s855    t620 h h696 h697 h698 h699 h700 h652 h701 h702 h703 h704 h754  T       t855    o854 b632 b855 b4 b4
2219  G       s855    t770  B       b856    t855
2220  B       b856    s855  P       p856    String "withT << 'c >> (dT 4) ttca"
2221  T       t856    o629 b856 b694  O       o856    ext_rule p856
2222    T       t856    o633 b851 b4
2223  B       b857    t856  B       b857    t856
2224  T       t857    o751 b857 b4 b854  T       t857    o856 b632 b857 b4 b4
2225  B       b858    t857  B       b858    t857
2226  T       t858    o b858 b4  T       t858    o b858 b4
2227  B       b859    t858  B       b859    t858
2228  T       t859    o b855 b859  T       t859    o b856 b859
2229  B       b860    t859  B       b860    t859
2230  T       t860    o627 b845 b860  T       t860    o780 b632 b854 b860 b4
2231  B       b861    t860  B       b861    t860
2232  T       t861    o627 b855 b4  P       p861    String "assertT << equiv{car{'g}; eqG{'g}; 'c; 'b} >> thenT autoT"
2233  B       b862    t861  O       o861    ext_rule p861
2234  T       t862    o834 b626 b862 b4 b4  T       t861    o568 b560 b578 b663 b567
2235    S       s861    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723 h774
2236    G       s861    t861
2237    B       b862    s861
2238    T       t862    o635 b862 b713
2239  B       b863    t862  B       b863    t862
2240  T       t863    o627 b858 b4  T       t863    o2 b777
2241  B       b864    t863  B       b864    t863
2242  T       t864    o836 b626 b864 b4 b4  T       t864    o771 b863 b4 b864
2243  B       b865    t864  B       b865    t864
2244  T       t865    o b865 b4  H       h865    v_1 t861
2245  B       b866    t865  S       s865    t626 h h715 h716 h717 h718 h719 h720 h659 h662 h721 h722 h723 h774 h865
2246  T       t866    o b863 b866  G       s865    t723
2247    B       b866    s865
2248    T       t866    o635 b866 b713
2249  B       b867    t866  B       b867    t866
2250  T       t867    o851 b626 b861 b867 b4  T       t867    o634 b867 b4 b864
2251  B       b868    t867  B       b868    t867
2252  P       p868    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 13 thenT autoT"  T       t868    o b868 b4
 O       o868    ext_rule p868  
 T       t868    o627 b848 b4  
2253  B       b869    t868  B       b869    t868
2254  T       t869    o868 b626 b869 b4 b4  T       t869    o b865 b869
2255  B       b870    t869  B       b870    t869
2256  T       t870    o b870 b4  T       t870    o633 b777 b870
2257  B       b871    t870  B       b871    t870
2258  T       t871    o b868 b871  P       p871    String "equivSymT ttca thenT rwh unfold_equiv 13 ttca"
2259    O       o871    ext_rule p871
2260    T       t871    o633 b865 b4
2261  B       b872    t871  B       b872    t871
2262  T       t872    o841 b626 b851 b872 b4  T       t872    o871 b632 b872 b4 b4
2263  B       b873    t872  B       b873    t872
2264  T       t873    o b873 b4  P       p873    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 14 thenT autoT"
2265    O       o873    ext_rule p873
2266    T       t873    o633 b868 b4
2267  B       b874    t873  B       b874    t873
2268  T       t874    o b841 b874  T       t874    o873 b632 b874 b4 b4
2269  B       b875    t874  B       b875    t874
2270  T       t875    o750 b626 b760 b875 b4  T       t875    o b875 b4
2271  B       b876    t875  B       b876    t875
2272  P       p876    String "withT << 'd >> (dT 4) ttca thenT withT << 'e >> (dT 4) ttca thenT withT << 'f >> (dT 4) ttca"  T       t876    o b873 b876
2273  O       o876    ext_rule p876  B       b877    t876
2274  T       t876    o564 b737 b560  T       t877    o861 b632 b871 b877 b4
2275  H       h876    z_2 t876  B       b878    t877
2276  T       t877    o564 b739 b560  T       t878    o b878 b4
2277  H       h877    z_3 t877  B       b879    t878
2278  T       t878    o564 b741 b560  T       t879    o b861 b879
2279  H       h878    z_4 t878  B       b880    t879
2280  S       s878    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878  T       t880    o770 b632 b780 b880 b4
 G       s878    t745  
 B       b878    s878  
 T       t879    o629 b878 b694  
 B       b879    t879  
 S       s879    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877  
 G       s879    t745  
 B       b880    s879  
 T       t880    o629 b880 b694  
2281  B       b881    t880  B       b881    t880
2282  P       p881    String with  P       p881    String "withT << 'd >> (dT 4) ttca thenT withT << 'e >> (dT 4) ttca thenT withT << 'f >> (dT 4) ttca"
2283  O       o881    arg_named p881  O       o881    ext_rule p881
2284  NSummary!arg_term_list  arg_term_list   arg_term_list Summary  T       t881    o564 b664 b560
2285  O       o882    arg_term_list  H       h881    z_1 t881
2286  T       t882    o b741 b4  T       t882    o564 b759 b560
2287  B       b882    t882  H       h882    z_2 t882
2288  T       t883    o882 b882  T       t883    o564 b761 b560
2289  B       b883    t883  H       h883    z_3 t883
2290  T       t884    o881 b883  S       s883    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882 h883
2291    G       s883    t765
2292    B       b883    s883
2293    T       t884    o635 b883 b713
2294  B       b884    t884  B       b884    t884
2295  T       t885    o b884 b4  S       s884    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882
2296  B       b885    t885  G       s884    t765
2297  S       s885    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876  B       b885    s884
2298  G       s885    t745  T       t885    o635 b885 b713
2299  B       b886    s885  B       b886    t885
2300  T       t886    o629 b886 b694  P       p886    String with
2301  B       b887    t886  O       o886    arg_named p886
2302  T       t887    o b739 b4  NSummary!arg_term_list  arg_term_list   arg_term_list Summary
2303  B       b888    t887  O       o887    arg_term_list
2304  T       t888    o882 b888  T       t887    o b761 b4
2305  B       b889    t888  B       b887    t887
2306  T       t889    o881 b889  T       t888    o887 b887
2307  B       b890    t889  B       b888    t888
2308  T       t890    o b890 b4  T       t889    o886 b888
2309  B       b891    t890  B       b889    t889
2310  T       t891    o b737 b4  T       t890    o b889 b4
2311    B       b890    t890
2312    S       s890    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881
2313    G       s890    t765
2314    B       b891    s890
2315    T       t891    o635 b891 b713
2316  B       b892    t891  B       b892    t891
2317  T       t892    o882 b892  T       t892    o b759 b4
2318  B       b893    t892  B       b893    t892
2319  T       t893    o881 b893  T       t893    o887 b893
2320  B       b894    t893  B       b894    t893
2321  T       t894    o b894 b4  T       t894    o886 b894
2322  B       b895    t894  B       b895    t894
2323  T       t895    o628 b746 b895 b734  T       t895    o b895 b4
2324  B       b896    t895  B       b896    t895
2325  T       t896    o2 b896  T       t896    o b664 b4
2326  B       b897    t896  B       b897    t896
2327  T       t897    o628 b887 b891 b897  T       t897    o887 b897
2328  B       b898    t897  B       b898    t897
2329  T       t898    o2 b898  T       t898    o886 b898
2330  B       b899    t898  B       b899    t898
2331  T       t899    o628 b881 b885 b899  T       t899    o b899 b4
2332  B       b900    t899  B       b900    t899
2333  T       t900    o2 b900  T       t900    o634 b766 b900 b756
2334  B       b901    t900  B       b901    t900
2335  T       t901    o628 b879 b4 b901  T       t901    o2 b901
2336  B       b902    t901  B       b902    t901
2337  T       t902    o b902 b4  T       t902    o634 b892 b896 b902
2338  B       b903    t902  B       b903    t902
2339  T       t903    o627 b747 b903  T       t903    o2 b903
2340  B       b904    t903  B       b904    t903
2341  P       p904    String "assertT << equiv{car{'g}; eqG{'g}; 'd; 'f} >> thenT autoT"  T       t904    o634 b886 b890 b904
2342  O       o904    ext_rule p904  B       b905    t904
2343  T       t904    o575 b560 b578 b737 b741  T       t905    o2 b905
 S       s904    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878  
 G       s904    t904  
 B       b905    s904  
 T       t905    o629 b905 b694  
2344  B       b906    t905  B       b906    t905
2345  T       t906    o2 b902  T       t906    o634 b884 b4 b906
2346  B       b907    t906  B       b907    t906
2347  T       t907    o751 b906 b4 b907  T       t907    o b907 b4
2348  B       b908    t907  B       b908    t907
2349  H       h908    v_1 t904  T       t908    o633 b767 b908
2350  S       s908    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878 h908  B       b909    t908
2351  G       s908    t745  P       p909    String "assertT << equiv{car{'g}; eqG{'g}; 'd; 'f} >> thenT autoT"
2352  B       b909    s908  O       o909    ext_rule p909
2353  T       t909    o629 b909 b694  T       t909    o568 b560 b578 b664 b761
2354  B       b910    t909  S       s909    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882 h883
2355  T       t910    o628 b910 b4 b907  G       s909    t909
2356    B       b910    s909
2357    T       t910    o635 b910 b713
2358  B       b911    t910  B       b911    t910
2359  T       t911    o b911 b4  T       t911    o2 b907
2360  B       b912    t911  B       b912    t911
2361  T       t912    o b908 b912  T       t912    o771 b911 b4 b912
2362  B       b913    t912  B       b913    t912
2363  T       t913    o627 b902 b913  H       h913    v_1 t909
2364  B       b914    t913  S       s913    t626 h h715 h716 h717 h718 h719 h720 h663 h757 h758 h759 h760 h762 h763 h764 h881 h882 h883 h913
2365  P       p914    String "equivTransT << 'e >> ttca"  G       s913    t765
2366  O       o914    ext_rule p914  B       b914    s913
2367  T       t914    o575 b560 b578 b737 b739  T       t914    o635 b914 b713
2368  S       s914    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878  B       b915    t914
2369  G       s914    t914  T       t915    o634 b915 b4 b912
 B       b915    s914  
 T       t915    o629 b915 b694  
2370  B       b916    t915  B       b916    t915
2371  T       t916    o2 b908  T       t916    o b916 b4
2372  B       b917    t916  B       b917    t916
2373  T       t917    o751 b916 b4 b917  T       t917    o b913 b917
2374  B       b918    t917  B       b918    t917
2375  T       t918    o575 b560 b578 b739 b741  T       t918    o633 b907 b918
2376  S       s918    t620 h h696 h697 h698 h699 h700 h735 h736 h737 h738 h740 h742 h743 h744 h876 h877 h878  B       b919    t918
2377  G       s918    t918  P       p919    String "equivTransT << 'e >> ttca thenT rwh unfold_equiv 0 thenT rwh unfold_equiv 14 thenT rwh unfold_equiv 15 ttca"
2378  B       b919    s918  O       o919    ext_rule p919
2379  T       t919    o629 b919 b694  T       t919    o633 b913 b4
2380  B       b920    t919  B       b920    t919
2381  T       t920    o751 b920 b4 b917  T       t920    o919 b632 b920 b4 b4
2382  B       b921    t920  B       b921    t920
2383  T       t921    o b921 b4  P       p921    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 19 ttca"
2384    O       o921    ext_rule p921
2385    T       t921    o633 b916 b4
2386  B       b922    t921  B       b922    t921
2387  T       t922    o b918 b922  T       t922    o921 b632 b922 b4 b4
2388  B       b923    t922  B       b923    t922
2389  T       t923    o627 b908 b923  T       t923    o b923 b4
2390  B       b924    t923  B       b924    t923
2391  T       t924    o627 b918 b4  T       t924    o b921 b924
2392  B       b925    t924  B       b925    t924
2393  T       t925    o868 b626 b925 b4 b4  T       t925    o909 b632 b919 b925 b4
2394  B       b926    t925  B       b926    t925
2395  P       p926    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 14 thenT autoT"  T       t926    o b926 b4
 O       o926    ext_rule p926  
 T       t926    o627 b921 b4  
2396  B       b927    t926  B       b927    t926
2397  T       t927    o926 b626 b927 b4 b4  T       t927    o881 b632 b909 b927 b4
2398  B       b928    t927  B       b928    t927
2399  T       t928    o b928 b4  T       t928    o b928 b4
2400  B       b929    t928  B       b929    t928
2401  T       t929    o b926 b929  T       t929    o b881 b929
2402  B       b930    t929  B       b930    t929
2403  T       t930    o914 b626 b924 b930 b4  T       t930    o710 b632 b770 b930 b4
2404  B       b931    t930  B       b931    t930
2405  P       p931    String "rwh unfold_equiv 0 thenT rwh unfold_equiv 18 thenT autoT"  T       t931    o630 b931
 O       o931    ext_rule p931  
 T       t931    o627 b911 b4  
2406  B       b932    t931  B       b932    t931
2407  T       t932    o931 b626 b932 b4 b4  P       p932    Number 2203
2408  B       b933    t932  P       p933    Number 2211
2409  T       t933    o b933 b4  O       o933    resource_defs p932 p933 p300
2410  B       b934    t933  P       p934    Number 2209
2411  T       t934    o b931 b934  O       o934    uid p934 p933
2412  B       b935    t934  T       t934    o934 b645
2413  T       t935    o904 b626 b914 b935 b4  B       b934    t934
2414  B       b936    t935  T       t935    o b934 b4
2415  T       t936    o b936 b4  B       b935    t935
2416  B       b937    t936  T       t936    o933 b935
2417  T       t937    o876 b626 b904 b937 b4  B       b936    t936
2418  B       b938    t937  T       t937    o b936 b4
2419  T       t938    o b938 b4  B       b937    t937
2420  B       b939    t938  T       t938    o706 b616 b710 b932 b937
2421  T       t939    o b876 b939  B       b938    t938
2422  B       b940    t939  T       t939    o705 b938
2423  T       t940    o691 b626 b750 b940 b4  B       b939    t939
2424  B       b941    t940  P       p939    Number 2414
2425  T       t941    o624 b941  P       p940    Number 2666
2426  B       b942    t941  O       o940    location p939 p940
2427  P       p942    Number 1874  P       p941    String subgroup_id
2428  P       p943    Number 1882  O       o941    rule p941
2429  O       o943    resource_defs p942 p943 p300  NCzf_itt_group!id       id      id Czf_itt_group
2430  P       p944    Number 1880  O       o942    id
2431  O       o944    uid p944 p943  T       t942    o942 b549
2432  T       t944    o944 b639  B       b942    t942
2433  B       b944    t944  T       t943    o942 b550
2434  T       t945    o b944 b4  B       b943    t943
2435    T       t944    o568 b560 b578 b942 b943
2436    S       s944    t626 h
2437    G       s944    t944
2438    B       b944    s944
2439    T       t945    o617 b944
2440  B       b945    t945  B       b945    t945
2441  T       t946    o943 b945  T       t946    o616 b676 b945
2442  B       b946    t946  B       b946    t946
2443  T       t947    o b946 b4  T       t947    o616 b624 b946
2444  B       b947    t947  B       b947    t947
2445  T       t948    o687 b610 b691 b942 b947  T       t948    o616 b622 b947
2446  B       b948    t948  B       b948    t948
2447  T       t949    o686 b948  T       t949    o635 b944 b713
2448  B       b949    t949  B       b949    t949
2449  P       p949    Number 2085  T       t950    o634 b949 b4 b638
2450  P       p950    Number 2337  B       b950    t950
2451  O       o950    location p949 p950  S       s950    t626 h h715 h716 h717 h718 h719 h720
2452  P       p951    String subgroup_id  G       s950    t944
2453  O       o951    rule p951  B       b951    s950
2454  NCzf_itt_group!id       id      id Czf_itt_group  T       t951    o635 b951 b713
2455  O       o952    id  B       b952    t951
2456  T       t952    o952 b549  S       s952    t626 h h715 h716 h717 h718 h729
2457  B       b952    t952  G       s952    t944
2458  T       t953    o952 b550  B       b953    s952
2459  B       b953    t953  T       t953    o635 b953 b713
2460  T       t954    o575 b560 b578 b952 b953  B       b954    t953
2461  S       s954    t620 h  S       s954    t626 h h715 h716 h717 h731
2462  G       s954    t954  G       s954    t944
2463  B       b954    s954  B       b955    s954
2464  T       t955    o611 b954  T       t955    o635 b955 b713
2465  B       b955    t955  B       b956    t955
2466  T       t956    o610 b659 b955  S       s956    t626 h h715 h716 h733
2467  B       b956    t956  G       s956    t944
2468  T       t957    o610 b618 b956  B       b957    s956
2469  B       b957    t957  T       t957    o635 b957 b713
2470  T       t958    o610 b616 b957  B       b958    t957
2471  B       b958    t958  S       s958    t626 h h715 h735
2472  T       t959    o629 b954 b694  G       s958    t944
2473  B       b959    t959  B       b959    s958
2474  T       t960    o628 b959 b4 b632  T       t959    o635 b959 b713
2475  B       b960    t960  B       b960    t959
2476  S       s960    t620 h h696 h697 h698 h699 h700  S       s960    t626 h h737
2477  G       s960    t954  G       s960    t944
2478  B       b961    s960  B       b961    s960
2479  T       t961    o629 b961 b694  T       t961    o635 b961 b713
2480  B       b962    t961  B       b962    t961
2481  S       s962    t620 h h696 h697 h698 h711  S       s962    t626 h h739
2482  G       s962    t954  G       s962    t944
2483  B       b963    s962  B       b963    s962
2484  T       t963    o629 b963 b694  T       t963    o635 b963 b713
2485  B       b964    t963  B       b964    t963
2486  S       s964    t620 h h696 h697 h713  T       t964    o2 b950
2487  G       s964    t954  B       b965    t964
2488  B       b965    s964  T       t965    o634 b964 b4 b965
 T       t965    o629 b965 b694  
2489  B       b966    t965  B       b966    t965
2490  S       s966    t620 h h696 h715  T       t966    o2 b966
2491  G       s966    t954  B       b967    t966
2492  B       b967    s966  T       t967    o634 b962 b4 b967
 T       t967    o629 b967 b694  
2493  B       b968    t967  B       b968    t967
2494  S       s968    t620 h h717  T       t968    o2 b968
2495  G       s968    t954  B       b969    t968
2496  B       b969    s968  T       t969    o634 b960 b4 b969
 T       t969    o629 b969 b694  
2497  B       b970    t969  B       b970    t969
2498  S       s970    t620 h h719  T       t970    o2 b970
2499  G       s970    t954  B       b971    t970
2500  B       b971    s970  T       t971    o634 b958 b4 b971
 T       t971    o629 b971 b694  
2501  B       b972    t971  B       b972    t971
2502  T       t972    o2 b960  T       t972    o2 b972
2503  B       b973    t972  B       b973    t972
2504  T       t973    o628 b972 b4 b973  T       t973    o634 b956 b4 b973
2505  B       b974    t973  B       b974    t973
2506  T       t974    o2 b974  T       t974    o2 b974
2507  B       b975    t974  B       b975    t974
2508  T       t975    o628 b970 b4 b975  T       t975    o634 b954 b4 b975
2509  B       b976    t975  B       b976    t975
2510  T       t976    o2 b976  T       t976    o2 b976
2511  B       b977    t976  B       b977    t976
2512  T       t977    o628 b968 b4 b977  T       t977    o634 b952 b4 b977
2513  B       b978    t977  B       b978    t977
2514  T       t978    o2 b978  T       t978    o b978 b4
2515  B       b979    t978  B       b979    t978
2516  T       t979    o628 b966 b4 b979  T       t979    o633 b950 b979
2517  B       b980    t979  B       b980    t979
2518  T       t980    o2 b980  P       p980    String "instHypT [<< op{'g; id{'s}; id{'s}} >>; << id{'s} >>] 6 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca"
2519    O       o980    ext_rule p980
2520    T       t980    o570 b550 b942 b942
2521  B       b981    t980  B       b981    t980
2522  T       t981    o628 b964 b4 b981  T       t981    o568 b559 b569 b981 b942
2523  B       b982    t981  S       s981    t626 h h715 h716 h717 h718 h719 h720
2524  T       t982    o2 b982  G       s981    t981
2525    B       b982    s981
2526    T       t982    o635 b982 b713
2527  B       b983    t982  B       b983    t982
2528  T       t983    o628 b962 b4 b983  B       b984    t981
2529  B       b984    t983  T       t984    o568 b560 b578 b981 b942
 T       t984    o b984 b4  
2530  B       b985    t984  B       b985    t984
2531  T       t985    o627 b960 b985  T       t985    o563 b984 b985
2532  B       b986    t985  H       h985    w_1 t985
2533  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"  S       s985    t626 h h715 h716 h717 h718 h719 h720 h985
2534  O       o986    ext_rule p986  G       s985    t981
2535  T       t986    o569 b549 b952 b952  B       b986    s985
2536    T       t986    o635 b986 b713
2537  B       b987    t986  B       b987    t986
2538  T       t987    o575 b560 b578 b987 b952  S       s987    t626 h h715 h716 h717 h718 h719 h720 h985
2539  H       h987    y_4 t987  G       s987    t944
 S       s987    t620 h h696 h697 h698 h699 h700 h987  
 G       s987    t954  
2540  B       b988    s987  B       b988    s987
2541  T       t988    o629 b988 b694  T       t988    o635 b988 b713
2542  B       b989    t988  B       b989    t988
2543  T       t989    o575 b559 b576 b987 b952  T       t989    o568 b559 b569 b981 b567
2544  B       b990    t989  B       b990    t989
2545  B       b991    t987  T       t990    o568 b560 b578 b981 b567
2546    B       b991    t990
2547  T       t991    o563 b990 b991  T       t991    o563 b990 b991
2548  H       h991    w_1 t991  B       b992    t991 b
2549  S       s991    t620 h h696 h697 h698 h699 h700 h991 h987  T       t992    o561 b562 b992
2550  G       s991    t954  H       h992    w t992
2551  B       b992    s991  S       s992    t626 h h715 h716 h717 h718 h719 h720 h992 h985
2552  T       t992    o629 b992 b694  G       s992    t944
2553  B       b993    t992  B       b993    s992
2554  S       s993    t620 h h696 h697 h698 h699 h700 h991  T       t993    o635 b993 b713
2555  G       s993    t954  B       b994    t993
2556  B       b994    s993  P       p994    String thin
2557  T       t994    o629 b994 b694  O       o994    arg_named p994
2558  B       b995    t994  P       p995    String false
2559  T       t995    o575 b559 b576 b987 b567  O       o995    arg_bool p995
2560  B       b996    t995  T       t995    o995
2561  T       t996    o575 b560 b578 b987 b567  B       b995    t995
2562  B       b997    t996  T       t996    o994 b995
2563  T       t997    o563 b996 b997  B       b996    t996
2564  B       b998    t997 b  T       t997    o b996 b4
2565  T       t998    o561 b562 b998  B       b997    t997
2566  H       h998    w t998  S       s997    t626 h h715 h716 h717 h718 h719 h720 h992
2567  S       s998    t620 h h696 h697 h698 h699 h700 h998 h991  G       s997    t944
2568  G       s998    t954  B       b998    s997
2569  B       b999    s998  T       t998    o635 b998 b713
2570  T       t999    o629 b999 b694  B       b999    t998
2571    T       t999    o b942 b4
2572  B       b1000   t999  B       b1000   t999
2573  P       p1000   String thin  T       t1000   o887 b1000
2574  O       o1000   arg_named p1000  B       b1001   t1000
2575  P       p1001   String false  T       t1001   o886 b1001
2576  O       o1001   arg_bool p1001  B       b1002   t1001
2577  T       t1001   o1001  T       t1002   o b1002 b997
2578  B       b1001   t1001  B       b1003   t1002
2579  T       t1002   o1000 b1001  T       t1003   o b981 b4
2580  B       b1002   t1002  B       b1004   t1003
2581  T       t1003   o b1002 b4  T       t1004   o887 b1004
 B       b1003   t1003  
 S       s1003   t620 h h696 h697 h698 h699 h700 h998  
 G       s1003   t954  
 B       b1004   s1003  
 T       t1004   o629 b1004 b694  
2582  B       b1005   t1004  B       b1005   t1004
2583  T       t1005   o b952 b4  T       t1005   o886 b1005
2584  B       b1006   t1005  B       b1006   t1005
2585  T       t1006   o882 b1006  T       t1006   o b1006 b997
2586  B       b1007   t1006  B       b1007   t1006
2587  T       t1007   o881 b1007  T       t1007   o634 b952 b1007 b977
2588  B       b1008   t1007  B       b1008   t1007
2589  T       t1008   o b1008 b1003  T       t1008   o2 b1008
2590  B       b1009   t1008  B       b1009   t1008
2591  T       t1009   o b987 b4  T       t1009   o634 b999 b1003 b1009
2592  B       b1010   t1009  B       b1010   t1009
2593  T       t1010   o882 b1010  T       t1010   o2 b1010
2594  B       b1011   t1010  B       b1011   t1010
2595  T       t1011   o881 b1011  T       t1011   o634 b994 b997 b1011
2596  B       b1012   t1011  B       b1012   t1011
2597  T       t1012   o b1012 b1003  T       t1012   o2 b1012
2598  B       b1013   t1012  B       b1013   t1012
2599  T       t1013   o628 b962 b1013 b983  T       t1013   o634 b989 b4 b1013
2600  B       b1014   t1013  B       b1014   t1013
2601  T       t1014   o2 b1014  T       t1014   o2 b1014
2602  B       b1015   t1014  B       b1015   t1014
2603  T       t1015   o628 b1005 b1009 b1015  T       t1015   o771 b987 b4 b1015
2604  B       b1016   t1015  B       b1016   t1015
2605  T       t1016   o2 b1016  T       t1016   o2 b1016
2606  B       b1017   t1016  B       b1017   t1016
2607  T       t1017   o628 b1000 b1003 b1017  T       t1017   o771 b983 b4 b1017
2608  B       b1018   t1017  B       b1018   t1017
2609  T       t1018   o2 b1018  H       h1018   y_5 t984
2610  B       b1019   t1018  S       s1018   t626 h h715 h716 h717 h718 h719 h720 h1018
2611  T       t1019   o628 b995 b4 b1019  G       s1018   t944
2612    B       b1019   s1018
2613    T       t1019   o635 b1019 b713
2614  B       b1020   t1019  B       b1020   t1019
2615  T       t1020   o2 b1020  S       s1020   t626 h h715 h716 h717 h718 h719 h720 h985 h1018
2616  B       b1021   t1020  G       s1020   t944
2617  T       t1021   o628 b993 b4 b1021  B       b1021   s1020
2618    T       t1021   o635 b1021 b713
2619  B       b1022   t1021  B       b1022   t1021
2620  T       t1022   o2 b1022  T       t1022   o634 b1022 b4 b1015
2621  B       b1023   t1022  B       b1023   t1022
2622  T       t1023   o628 b989 b4 b1023  T       t1023   o2 b1023
2623  B       b1024   t1023  B       b1024   t1023
2624  T       t1024   o b1024 b4  T       t1024   o634 b1020 b4 b1024
2625  B       b1025   t1024  B       b1025   t1024
2626  T       t1025   o627 b984 b1025  T       t1025   o b1025 b4
2627  B       b1026   t1025  B       b1026   t1025
2628  P       p1026   String "instHypT [<< id{'s} >>; << id{'s} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca thenT dT 8 ttca"  T       t1026   o b1018 b1026
 O       o1026   ext_rule p1026  
 T       t1026   o569 b550 b952 b952  
2629  B       b1027   t1026  B       b1027   t1026
2630  T       t1027   o568 b987 b1027  T       t1027   o633 b978 b1027
2631  H       h1027   y_6 t1027  B       b1028   t1027
2632  S       s1027   t620 h h696 h697 h698 h699 h700 h987 h1027  P       p1028   String "instHypT [<< id{'s} >>; << id{'s} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca thenT dT 8 ttca"
2633  G       s1027   t954  O       o1028   ext_rule p1028
2634  B       b1028   s1027  T       t1028   o570 b549 b942 b942
 T       t1028   o629 b1028 b694  
2635  B       b1029   t1028  B       b1029   t1028
2636  T       t1029   o564 b952 b559  T       t1029   o568 b559 b569 b1029 b981
2637  B       b1030   t1029  H       h1029   y_6 t1029
2638  B       b1031   t1027  S       s1029   t626 h h715 h716 h717 h718 h719 h720 h1029
2639  T       t1031   o563 b1030 b1031  G       s1029   t981
2640  H       h1031   y_5 t1031  B       b1030   s1029
2641  S       s1031   t620 h h696 h697 h698 h699 h700 h987 h1031 h1027  T       t1030   o635 b1030 b713
2642  G       s1031   t954  B       b1031   t1030
2643  B       b1032   s1031  T       t1031   o564 b942 b559
2644  T       t1032   o629 b1032 b694  B       b1032   t1031
2645  B       b1033   t1032  B       b1033   t1029
2646  S       s1033   t620 h h696 h697 h698 h699 h700 h987 h1031  T       t1033   o563 b1032 b1033
2647  G       s1033   t954  H       h1033   y_5 t1033
2648    S       s1033   t626 h h715 h716 h717 h718 h719 h720 h1033 h1029
2649    G       s1033   t981
2650  B       b1034   s1033  B       b1034   s1033
2651  T       t1034   o629 b1034 b694  T       t1034   o635 b1034 b713
2652  B       b1035   t1034  B       b1035   t1034
2653  B       b1036   t1031  S       s1035   t626 h h715 h716 h717 h718 h719 h720 h1033
2654  T       t1036   o563 b1030 b1036  G       s1035   t981
2655  H       h1036   w_1 t1036  B       b1036   s1035
2656  S       s1036   t620 h h696 h697 h698 h699 h700 h987 h1036 h1031  T       t1036   o635 b1036 b713
2657  G       s1036   t954  B       b1037   t1036
2658  B       b1037   s1036  B       b1038   t1033
2659  T       t1037   o629 b1037 b694  T       t1038   o563 b1032 b1038
2660  B       b1038   t1037  H       h1038   w_1 t1038
2661  S       s1038   t620 h h696 h697 h698 h699 h700 h987 h1036  S       s1038   t626 h h715 h716 h717 h718 h719 h720 h1038 h1033
2662  G       s1038   t954  G       s1038   t981
2663  B       b1039   s1038  B       b1039   s1038
2664  T       t1039   o629 b1039 b694  T       t1039   o635 b1039 b713
2665  B       b1040   t1039  B       b1040   t1039
2666  T       t1040   o569 b549 b952 b567  S       s1040   t626 h h715 h716 h717 h718 h719 h720 h1038
2667  B       b1041   t1040  G       s1040   t981
2668  T       t1041   o569 b550 b952 b567  B       b1041   s1040
2669    T       t1041   o635 b1041 b713
2670  B       b1042   t1041  B       b1042   t1041
2671  T       t1042   o568 b1041 b1042  T       t1042   o570 b549 b942 b567
2672  B       b1043   t1042  B       b1043   t1042
2673  T       t1043   o563 b568 b1043  T       t1043   o570 b550 b942 b567
2674  B       b1044   t1043  B       b1044   t1043
2675  T       t1044   o563 b1030 b1044  T       t1044   o568 b559 b569 b1043 b1044
2676  B       b1045   t1044 b  B       b1045   t1044
2677  T       t1045   o561 b562 b1045  T       t1045   o563 b568 b1045
2678  H       h1045   w t1045  B       b1046   t1045
2679  S       s1045   t620 h h696 h697 h698 h699 h700 h987 h1045 h1036  T       t1046   o563 b1032 b1046
2680  G       s1045   t954  B       b1047   t1046 b
2681  B       b1046   s1045  T       t1047   o561 b562 b1047
2682  T       t1046   o629 b1046 b694  H       h1047   w t1047
2683  B       b1047   t1046  S       s1047   t626 h h715 h716 h717 h718 h719 h720 h1047 h1038
2684  S       s1047   t620 h h696 h697 h698 h699 h700 h987 h1045  G       s1047   t981
 G       s1047   t954  
2685  B       b1048   s1047  B       b1048   s1047
2686  T       t1048   o629 b1048 b694  T       t1048   o635 b1048 b713
2687  B       b1049   t1048  B       b1049   t1048
2688  T       t1049   o628 b989 b1009 b1023  S       s1049   t626 h h715 h716 h717 h718 h719 h720 h1047
2689  B       b1050   t1049  G       s1049   t981
2690  T       t1050   o2 b1050  B       b1050   s1049
2691    T       t1050   o635 b1050 b713
2692  B       b1051   t1050  B       b1051   t1050
2693  T       t1051   o628 b1049 b1009 b1051  T       t1051   o771 b983 b1003 b1017
2694  B       b1052   t1051  B       b1052   t1051
2695  T       t1052   o2 b1052  T       t1052   o2 b1052
2696  B       b1053   t1052  B       b1053   t1052
2697  T       t1053   o628 b1047 b1003 b1053  T       t1053   o634 b1051 b1003 b1053
2698  B       b1054   t1053  B       b1054   t1053
2699  T       t1054   o2 b1054  T       t1054   o2 b1054
2700  B       b1055   t1054  B       b1055   t1054
2701  T       t1055   o628 b1040 b4 b1055  T       t1055   o634 b1049 b997 b1055
2702  B       b1056   t1055  B       b1056   t1055
2703  T       t1056   o2 b1056  T       t1056   o2 b1056
2704  B       b1057   t1056  B       b1057   t1056
2705  T       t1057   o628 b1038 b4 b1057  T       t1057   o634 b1042 b4 b1057
2706  B       b1058   t1057  B       b1058   t1057
2707  T       t1058   o2 b1058  T       t1058   o2 b1058
2708  B       b1059   t1058  B       b1059   t1058
2709  T       t1059   o628 b1035 b4 b1059  T       t1059   o634 b1040 b4 b1059
2710  B       b1060   t1059  B       b1060   t1059
2711  T       t1060   o2 b1060  T       t1060   o2 b1060
2712  B       b1061   t1060  B       b1061   t1060
2713  T       t1061   o628 b1033 b4 b1061  T       t1061   o634 b1037 b4 b1061
2714  B       b1062   t1061  B       b1062   t1061
2715  T       t1062   o2 b1062  T       t1062   o2 b1062
2716  B       b1063   t1062  B       b1063   t1062
2717  T       t1063   o628 b1029 b4 b1063  T       t1063   o634 b1035 b4 b1063
2718  B       b1064   t1063  B       b1064   t1063
2719  T       t1064   o b1064 b4  T       t1064   o2 b1064
2720  B       b1065   t1064  B       b1065   t1064
2721  T       t1065   o627 b1024 b1065  T       t1065   o634 b1031 b4 b1065
2722  B       b1066   t1065  B       b1066   t1065
2723  P       p1066   String "setSubstT << equal{op{'s; id{'s}; id{'s}}; op{'g; id{'s}; id{'s}}} >> 7 thenT autoT"  T       t1066   o b1066 b4
2724  O       o1066   ext_rule p1066  B       b1067   t1066
2725  T       t1066   o575 b560 b578 b1027 b952  T       t1067   o633 b1018 b1067
 H       h1066   v t1066  
 S       s1066   t620 h h696 h697 h698 h699 h700 h987 h1027 h1066  
 G       s1066   t954  
 B       b1067   s1066  
 T       t1067   o629 b1067 b694  
2726  B       b1068   t1067  B       b1068   t1067
2727  T       t1068   o2 b1064  P       p1068   String "equivSubstT << equiv{car{'s}; eqG{'s}; op{'g; id{'s}; id{'s}}; op{'s; id{'s}; id{'s}}} >> 0 ttca thenT equivSymT ttca thenT rwh unfold_equiv 8 ttca"
2728    O       o1068   ext_rule p1068
2729    T       t1068   o633 b1066 b4
2730  B       b1069   t1068  B       b1069   t1068
2731  T       t1069   o628 b1068 b4 b1069  T       t1069   o1068 b632 b1069 b4 b4
2732  B       b1070   t1069  B       b1070   t1069
2733  P       p1070   String wf  T       t1070   o b1070 b4
2734  O       o1070   tactic_arg p1070  B       b1071   t1070
2735  T       t1070   o564 b952 b560  T       t1071   o1028 b632 b1068 b1071 b4
 S       s1070   t620 h h696 h697 h698 h699 h700 h987 h1027  
 G       s1070   t1070  
 B       b1071   s1070  
 T       t1071   o629 b1071 b694  
2736  B       b1072   t1071  B       b1072   t1071
2737  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq  P       p1072   String "dT 8 ttca"
2738  O       o1072   fun_prop  O       o1072   ext_rule p1072
2739  P       p1072   Var v  T       t1072   o633 b1025 b4
2740  O       o1073   var p1072  B       b1073   t1072
2741  T       t1073   o1073  T       t1073   o1072 b632 b1073 b4 b4
2742  B       b1073   t1073  B       b1074   t1073
2743  T       t1074   o575 b560 b578 b1073 b952  T       t1074   o b1074 b4
2744  B       b1074   t1074 v  B       b1075   t1074
2745  T       t1075   o1072 b1074  T       t1075   o b1072 b1075
2746  S       s1075   t620 h h696 h697 h698 h699 h700 h987 h1027  B       b1076   t1075
2747  G       s1075   t1075  T       t1076   o980 b632 b1028 b1076 b4
2748  B       b1075   s1075  B       b1077   t1076
2749  T       t1076   o629 b1075 b694  T       t1077   o b1077 b4
2750  B       b1076   t1076  B       b1078   t1077
2751  T       t1077   o1070 b1076 b711 b1069  T       t1078   o710 b632 b980 b1078 b4
2752  B       b1077   t1077  B       b1079   t1078
2753  T       t1078   o2 b1077  T       t1079   o630 b1079
2754  B       b1078   t1078  B       b1080   t1079
2755  T       t1079   o1070 b1072 b4 b1078  P       p1080   Number 2441
2756  B       b1079   t1079  P       p1081   Number 2449
2757  T       t1080   o b1079 b4  O       o1081   resource_defs p1080 p1081 p300
2758  B       b1080   t1080  P       p1082   Number 2447
2759  T       t1081   o b1070 b1080  O       o1082   uid p1082 p1081
2760  B       b1081   t1081  T       t1082   o1082 b645
 T       t1082   o627 b1064 b1081  
2761  B       b1082   t1082  B       b1082   t1082
2762  P       p1082   String "dT 9 ttca"  T       t1083   o b1082 b4
 O       o1082   ext_rule p1082  
 T       t1083   o627 b1070 b4  
2763  B       b1083   t1083  B       b1083   t1083
2764  T       t1084   o1082 b626 b1083 b4 b4  T       t1084   o1081 b1083
2765  B       b1084   t1084  B       b1084   t1084
2766  P       p1084   String "withT << id{'s} >> (dT 4) ttca"  T       t1085   o b1084 b4
 O       o1084   ext_rule p1084  
 T       t1085   o627 b1079 b4  
2767  B       b1085   t1085  B       b1085   t1085
2768  T       t1086   o1084 b626 b1085 b4 b4  T       t1086   o941 b616 b948 b1080 b1085
2769  B       b1086   t1086  B       b1086   t1086
2770  T       t1087   o b1086 b4  T       t1087   o940 b1086
2771  B       b1087   t1087  B       b1087   t1087
2772  T       t1088   o b1084 b1087  P       p1087   Number 2668
2773  B       b1088   t1088  P       p1088   Number 3024
2774  T       t1089   o1066 b626 b1082 b1088 b4  O       o1088   location p1087 p1088
2775  B       b1089   t1089  P       p1089   String subgroup_inv
2776  T       t1090   o b1089 b4  O       o1089   rule p1089
2777    T       t1089   o781 b565
2778    S       s1089   t619 h
2779    G       s1089   t1089
2780    B       b1089   s1089
2781    T       t1090   o617 b1089
2782  B       b1090   t1090  B       b1090   t1090
2783  T       t1091   o1026 b626 b1066 b1090 b4  S       s1090   t626 h
2784  B       b1091   t1091  G       s1090   t566
2785  T       t1092   o b1091 b4  B       b1091   s1090
2786  B       b1092   t1092  T       t1091   o617 b1091
2787  T       t1093   o986 b626 b1026 b1092 b4  B       b1092   t1091
 B       b1093   t1093  
 T       t1094   o b1093 b4  
 B       b1094   t1094  
 T       t1095   o691 b626 b986 b1094 b4  
 B       b1095   t1095  
 T       t1096   o624 b1095  
 B       b1096   t1096  
 P       p1096   Number 2112  
 P       p1097   Number 2120  
 O       o1097   resource_defs p1096 p1097 p300  
 P       p1098   Number 2118  
 O       o1098   uid p1098 p1097  
 T       t1098   o1098 b639  
 B       b1098   t1098  
 T       t1099   o b1098 b4  
 B       b1099   t1099  
 T       t1100   o1097 b1099  
 B       b1100   t1100  
 T       t1101   o b1100 b4  
 B       b1101   t1101  
 T       t1102   o951 b610 b958 b1096 b1101  
 B       b1102   t1102  
 T       t1103   o950 b1102  
 B       b1103   t1103  
 P       p1103   Number 2339  
 P       p1104   Number 2695  
 O       o1104   location p1103 p1104  
 P       p1105   String subgroup_inv  
 O       o1105   rule p1105  
 T       t1105   o761 b565  
 S       s1105   t613 h  
 G       s1105   t1105  
 B       b1105   s1105  
 T       t1106   o611 b1105  
 B       b1106   t1106  
 S       s1106   t620 h  
 G       s1106   t566  
 B       b1107   s1106  
 T       t1107   o611 b1107  
 B       b1108   t1107  
2788  NCzf_itt_group!inv      inv     inv Czf_itt_group  NCzf_itt_group!inv      inv     inv Czf_itt_group
2789  O       o1108   inv  O       o1092   inv
2790  T       t1108   o1108 b549 b565  T       t1092   o1092 b549 b565
2791    B       b1093   t1092
2792    T       t1093   o1092 b550 b565
2793    B       b1094   t1093
2794    T       t1094   o568 b560 b578 b1093 b1094
2795    S       s1094   t626 h
2796    G       s1094   t1094
2797    B       b1095   s1094
2798    T       t1095   o617 b1095
2799    B       b1096   t1095
2800    T       t1096   o616 b676 b1096
2801    B       b1097   t1096
2802    T       t1097   o616 b1092 b1097
2803    B       b1098   t1097
2804    T       t1098   o616 b1090 b1098
2805    B       b1099   t1098
2806    T       t1099   o616 b624 b1099
2807    B       b1100   t1099
2808    T       t1100   o616 b622 b1100
2809    B       b1101   t1100
2810    P       p1101   String "assumT 5 thenT rwh unfold_subgroup 2 thenT autoT"
2811    O       o1101   ext_rule p1101
2812    T       t1101   o b1091 b711
2813    B       b1102   t1101
2814    T       t1102   o b1089 b1102
2815    B       b1103   t1102
2816    T       t1103   o b623 b1103
2817    B       b1104   t1103
2818    T       t1104   o b621 b1104
2819    B       b1105   t1104
2820    T       t1105   o635 b1095 b1105
2821    B       b1106   t1105
2822    T       t1106   o634 b1106 b4 b638
2823    B       b1107   t1106
2824    T       t1107   o564 b565 b560
2825    S       s1107   t626 h h715 h716 h717 h718 h719 h720
2826    G       s1107   t1107
2827    B       b1108   s1107
2828    T       t1108   o635 b1108 b1105
2829  B       b1109   t1108  B       b1109   t1108
2830  T       t1109   o1108 b550 b565  S       s1109   t626 h h715 h716 h717 h718 h719 h720
2831  B       b1110   t1109  G       s1109   t1094
2832  T       t1110   o575 b560 b578 b1109 b1110  B       b1110   s1109
2833  S       s1110   t620 h  T       t1110   o635 b1110 b1105
2834  G       s1110   t1110  B       b1111   t1110
2835  B       b1111   s1110  S       s1111   t626 h h715 h716 h717 h718 h729
2836  T       t1111   o611 b1111  G       s1111   t1094
2837  B       b1112   t1111  B       b1112   s1111
2838  T       t1112   o610 b659 b1112  T       t1112   o635 b1112 b1105
2839  B       b1113   t1112  B       b1113   t1112
2840  T       t1113   o610 b1108 b1113  S       s1113   t626 h h715 h716 h717 h731
2841  B       b1114   t1113  G       s1113   t1094
2842  T       t1114   o610 b1106 b1114  B       b1114   s1113
2843    T       t1114   o635 b1114 b1105
2844  B       b1115   t1114  B       b1115   t1114
2845  T       t1115   o610 b618 b1115  S       s1115   t626 h h715 h716 h733
2846  B       b1116   t1115  G       s1115   t1094
2847  T       t1116   o610 b616 b1116  B       b1116   s1115
2848    T       t1116   o635 b1116 b1105
2849  B       b1117   t1116  B       b1117   t1116
2850  P       p1117   String "assumT 5 thenT rwh unfold_subgroup 2 thenT autoT"  S       s1117   t626 h h715 h735
2851  O       o1117   ext_rule p1117  G       s1117   t1094
2852  T       t1117   o b1107 b692  B       b1118   s1117
2853  B       b1118   t1117  T       t1118   o635 b1118 b1105
 T       t1118   o b1105 b1118  
2854  B       b1119   t1118  B       b1119   t1118
2855  T       t1119   o b617 b1119  S       s1119   t626 h h737
2856  B       b1120   t1119  G       s1119   t1094
2857  T       t1120   o b615 b1120  B       b1120   s1119
2858    T       t1120   o635 b1120 b1105
2859  B       b1121   t1120  B       b1121   t1120
2860  T       t1121   o629 b1111 b1121  S       s1121   t626 h h739
2861  B       b1122   t1121  G       s1121   t1094
2862  T       t1122   o628 b1122 b4 b632  B       b1122   s1121
2863    T       t1122   o635 b1122 b1105
2864  B       b1123   t1122  B       b1123   t1122
2865  T       t1123   o564 b565 b560  T       t1123   o2 b1107
2866  S       s1123   t620 h h696 h697 h698 h699 h700  B       b1124   t1123
2867  G       s1123   t1123  T       t1124   o634 b1123 b4 b1124
 B       b1124   s1123  
 T       t1124   o629 b1124 b1121  
2868  B       b1125   t1124  B       b1125   t1124
2869  S       s1125   t620 h h696 h697 h698 h699 h700  T       t1125   o2 b1125
2870  G       s1125   t1110  B       b1126   t1125
2871  B       b1126   s1125  T       t1126   o634 b1121 b4 b1126
 T       t1126   o629 b1126 b1121  
2872  B       b1127   t1126  B       b1127   t1126
2873  S       s1127   t620 h h696 h697 h698 h711  T       t1127   o2 b1127
2874  G       s1127   t1110  B       b1128   t1127
2875  B       b1128   s1127  T       t1128   o634 b1119 b4 b1128
 T       t1128   o629 b1128 b1121  
2876  B       b1129   t1128  B       b1129   t1128
2877  S       s1129   t620 h h696 h697 h713  T       t1129   o2 b1129
2878  G       s1129   t1110  B       b1130   t1129
2879  B       b1130   s1129  T       t1130   o634 b1117 b4 b1130
 T       t1130   o629 b1130 b1121  
2880  B       b1131   t1130  B       b1131   t1130
2881  S       s1131   t620 h h696 h715  T       t1131   o2 b1131
2882  G       s1131   t1110  B       b1132   t1131
2883  B       b1132   s1131  T       t1132   o634 b1115 b4 b1132
 T       t1132   o629 b1132 b1121  
2884  B       b1133   t1132  B       b1133   t1132
2885  S       s1133   t620 h h717  T       t1133   o2 b1133
2886  G       s1133   t1110  B       b1134   t1133
2887  B       b1134   s1133  T       t1134   o634 b1113 b4 b1134
 T       t1134   o629 b1134 b1121  
2888  B       b1135   t1134  B       b1135   t1134
2889  S       s1135   t620 h h719  T       t1135   o2 b1135
2890  G       s1135   t1110  B       b1136   t1135
2891  B       b1136   s1135  T       t1136   o634 b1111 b729 b1136
 T       t1136   o629 b1136 b1121  
2892  B       b1137   t1136  B       b1137   t1136
2893  T       t1137   o2 b1123  T       t1137   o2 b1137
2894  B       b1138   t1137  B       b1138   t1137
2895  T       t1138   o628 b1137 b4 b1138  T       t1138   o634 b1109 b4 b1138
2896  B       b1139   t1138  B       b1139   t1138
2897  T       t1139   o2 b1139  T       t1139   o564 b1093 b560
2898  B       b1140   t1139  S       s1139   t626 h h715 h716 h717 h718 h719 h720
2899  T       t1140   o628 b1135 b4 b1140  G       s1139   t1139
2900    B       b1140   s1139
2901    T       t1140   o635 b1140 b1105
2902  B       b1141   t1140  B       b1141   t1140
2903  T       t1141   o2 b1141  T       t1141   o634 b1141 b4 b1138
2904  B       b1142   t1141  B       b1142   t1141
2905  T       t1142   o628 b1133 b4 b1142  T       t1142   o570 b550 b565 b1093
2906  B       b1143   t1142  B       b1143   t1142
2907  T       t1143   o2 b1143  T       t1143   o568 b560 b578 b1143 b943
2908  B       b1144   t1143  S       s1143   t626 h h715 h716 h717 h718 h719 h720
2909  T       t1144   o628 b1131 b4 b1144  G       s1143   t1143
2910    B       b1144   s1143
2911    T       t1144   o635 b1144 b1105
2912  B       b1145   t1144  B       b1145   t1144
2913  T       t1145   o2 b1145  T       t1145   o634 b1145 b4 b1138
2914  B       b1146   t1145  B       b1146   t1145
2915  T       t1146   o628 b1129 b4 b1146  T       t1146   o b1146 b4
2916  B       b1147   t1146  B       b1147   t1146
2917  T       t1147   o2 b1147  T       t1147   o b1142 b1147
2918  B       b1148   t1147  B       b1148   t1147
2919  T       t1148   o628 b1127 b711 b1148  T       t1148   o b1139 b1148
2920  B       b1149   t1148  B       b1149   t1148
2921  T       t1149   o2 b1149  T       t1149   o633 b1107 b1149
2922  B       b1150   t1149  B       b1150   t1149
2923  T       t1150   o628 b1125 b4 b1150  P       p1150   String "withT << 'a >> (dT 4) ttca"
2924    O       o1150   ext_rule p1150
2925    T       t1150   o633 b1139 b4
2926  B       b1151   t1150  B       b1151   t1150
2927  T       t1151   o564 b1109 b560  T       t1151   o1150 b632 b1151 b4 b4
2928  S       s1151   t620 h h696 h697 h698 h699 h700  B       b1152   t1151
2929  G       s1151   t1151  P       p1152   String "withT << inv{'s; 'a} >> (dT 4) ttca"
2930  B       b1152   s1151  O       o1152   ext_rule p1152
2931  T       t1152   o629 b1152 b1121  T       t1152   o633 b1142 b4
2932  B       b1153   t1152  B       b1153   t1152
2933  T       t1153   o628 b1153 b4 b1150  T       t1153   o1152 b632 b1153 b4 b4
2934  B       b1154   t1153  B       b1154   t1153
2935  T       t1154   o569 b550 b565 b1109  P       p1154   String "instHypT [<< op{'s; 'a; inv{'s; 'a}} >>; << id{'s} >>] 6 thenT autoT thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca"
2936    O       o1154   ext_rule p1154
2937    T       t1154   o570 b549 b565 b1093
2938  B       b1155   t1154  B       b1155   t1154
2939  T       t1155   o575 b560 b578 b1155 b953  T       t1155   o568 b560 b578 b1155 b942
2940  S       s1155   t620 h h696 h697 h698 h699 h700  H       h1155   y_5 t1155
2941  G       s1155   t1155  S       s1155   t626 h h715 h716 h717 h718 h719 h720 h1155
2942    G       s1155   t1143
2943  B       b1156   s1155  B       b1156   s1155
2944  T       t1156   o629 b1156 b1121  T       t1156   o635 b1156 b1105
2945  B       b1157   t1156  B       b1157   t1156
2946  T       t1157   o628 b1157 b4 b1150  T       t1157   o568 b559 b569 b1155 b942
2947  B       b1158   t1157  B       b1158   t1157
2948  T       t1158   o b1158 b4  B       b1159   t1155
2949  B       b1159   t1158  T       t1159   o563 b1158 b1159
2950  T       t1159   o b1154 b1159  H       h1159   w_1 t1159
2951  B       b1160   t1159  S       s1159   t626 h h715 h716 h717 h718 h719 h720 h1159 h1155
2952  T       t1160   o b1151 b1160  G       s1159   t1143
2953    B       b1160   s1159
2954    T       t1160   o635 b1160 b1105
2955  B       b1161   t1160  B       b1161   t1160
2956  T       t1161   o627 b1123 b1161  S       s1161   t626 h h715 h716 h717 h718 h719 h720 h1159
2957  B       b1162   t1161  G       s1161   t1143
2958  P       p1162   String "withT << 'a >> (dT 4) ttca"  B       b1162   s1161
2959  O       o1162   ext_rule p1162  T       t1162   o635 b1162 b1105
 T       t1162   o627 b1151 b4  
2960  B       b1163   t1162  B       b1163   t1162
2961  T       t1163   o1162 b626 b1163 b4 b4  T       t1163   o568 b559 b569 b1155 b567
2962  B       b1164   t1163  B       b1164   t1163
2963  P       p1164   String "withT << inv{'s; 'a} >> (dT 4) ttca"  T       t1164   o568 b560 b578 b1155 b567
 O       o1164   ext_rule p1164  
 T       t1164   o627 b1154 b4  
2964  B       b1165   t1164  B       b1165   t1164
2965  T       t1165   o1164 b626 b1165 b4 b4  T       t1165   o563 b1164 b1165
2966  B       b1166   t1165  B       b1166   t1165 b
2967  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"  T       t1166   o561 b562 b1166
2968  O       o1166   ext_rule p1166  H       h1166   w t1166
2969  T       t1166   o569 b549 b565 b1109  S       s1166   t626 h h715 h716 h717 h718 h719 h720 h1166 h1159
2970  B       b1167   t1166  G       s1166   t1143
2971  T       t1167   o575 b560 b578 b1167 b952  B       b1167   s1166
2972  H       h1167   y_4 t1167  T       t1167   o635 b1167 b1105
2973  S       s1167   t620 h h696 h697 h698 h699 h700 h1167  B       b1168   t1167
2974  G       s1167   t1155  S       s1168   t626 h h715 h716 h717 h718 h719 h720 h1166
2975  B       b1168   s1167  G       s1168   t1143
2976  T       t1168   o629 b1168 b1121  B       b1169   s1168
2977  B       b1169   t1168  T       t1169   o635 b1169 b1105
 T       t1169   o575 b559 b576 b1167 b952  
2978  B       b1170   t1169  B       b1170   t1169
2979  B       b1171   t1167  T       t1170   o b1155 b4
2980  T       t1171   o563 b1170 b1171  B       b1171   t1170
2981  H       h1171   w_1 t1171  T       t1171   o887 b1171
2982  S       s1171   t620 h h696 h697 h698 h699 h700 h1171 h1167  B       b1172   t1171
2983  G       s1171   t1155  T       t1172   o886 b1172
 B       b1172   s1171  
 T       t1172   o629 b1172 b1121  
2984  B       b1173   t1172  B       b1173   t1172
2985  S       s1173   t620 h h696 h697 h698 h699 h700 h1171  T       t1173   o b1173 b997
2986  G       s1173   t1155  B       b1174   t1173
2987  B       b1174   s1173  T       t1174   o634 b1145 b1174 b1138
 T       t1174   o629 b1174 b1121  
2988  B       b1175   t1174  B       b1175   t1174
2989  T       t1175   o575 b559 b576 b1167 b567  T       t1175   o2 b1175
2990  B       b1176   t1175  B       b1176   t1175
2991  T       t1176   o575 b560 b578 b1167 b567  T       t1176   o634 b1170 b1003 b1176
2992  B       b1177   t1176  B       b1177   t1176
2993  T       t1177   o563 b1176 b1177  T       t1177   o2 b1177
2994  B       b1178   t1177 b  B       b1178   t1177
2995  T       t1178   o561 b562 b1178  T       t1178   o634 b1168 b997 b1178
2996  H       h1178   w t1178  B       b1179   t1178
2997  S       s1178   t620 h h696 h697 h698 h699 h700 h1178 h1171  T       t1179   o2 b1179
 G       s1178   t1155  
 B       b1179   s1178  
 T       t1179   o629 b1179 b1121  
2998  B       b1180   t1179  B       b1180   t1179
2999  S       s1180   t620 h h696 h697 h698 h699 h700 h1178  T       t1180   o634 b1163 b4 b1180
3000  G       s1180   t1155  B       b1181   t1180
3001  B       b1181   s1180  T       t1181   o2 b1181
 T       t1181   o629 b1181 b1121  
3002  B       b1182   t1181  B       b1182   t1181
3003  T       t1182   o b1167 b4  T       t1182   o634 b1161 b4 b1182
3004  B       b1183   t1182  B       b1183   t1182
3005  T       t1183   o882 b1183  T       t1183   o2 b1183
3006  B       b1184   t1183  B       b1184   t1183
3007  T       t1184   o881 b1184  T       t1184   o634 b1157 b4 b1184
3008  B       b1185   t1184  B       b1185   t1184
3009  T       t1185   o b1185 b1003  T       t1185   o b1185 b4
3010  B       b1186   t1185  B       b1186   t1185
3011  T       t1186   o628 b1157 b1186 b1150  T       t1186   o633 b1146 b1186
3012  B       b1187   t1186  B       b1187   t1186
3013  T       t1187   o2 b1187  P       p1187   String "instHypT [<< 'a >>; << inv{'s; 'a} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 9 ttca thenT dT 9 ttca"
3014  B       b1188   t1187  O       o1187   ext_rule p1187
3015  T       t1188   o628 b1182 b1009 b1188  T       t1187   o568 b559 b569 b1155 b1143
3016    H       h1187   y_7 t1187
3017    S       s1187   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187
3018    G       s1187   t1143
3019    B       b1188   s1187
3020    T       t1188   o635 b1188 b1105
3021  B       b1189   t1188  B       b1189   t1188
3022  T       t1189   o2 b1189  T       t1189   o564 b1093 b559
3023  B       b1190   t1189  B       b1190   t1189
3024  T       t1190   o628 b1180 b1003 b1190  B       b1191   t1187
3025  B       b1191   t1190  T       t1191   o563 b1190 b1191
3026  T       t1191   o2 b1191  H       h1191   y_6 t1191
3027  B       b1192   t1191  S       s1191   t626 h h715 h716 h717 h718 h719 h720 h1155 h1191 h1187
3028  T       t1192   o628 b1175 b4 b1192  G       s1191   t1143
3029    B       b1192   s1191
3030    T       t1192   o635 b1192 b1105
3031  B       b1193   t1192  B       b1193   t1192
3032  T       t1193   o2 b1193  S       s1193   t626 h h715 h716 h717 h718 h719 h720 h1155 h1191
3033  B       b1194   t1193  G       s1193   t1143
3034  T       t1194   o628 b1173 b4 b1194  B       b1194   s1193
3035    T       t1194   o635 b1194 b1105
3036  B       b1195   t1194  B       b1195   t1194
3037  T       t1195   o2 b1195  B       b1196   t1191
3038  B       b1196   t1195  T       t1196   o563 b566 b1196
3039  T       t1196   o628 b1169 b4 b1196  H       h1196   w_1 t1196
3040  B       b1197   t1196  S       s1196   t626 h h715 h716 h717 h718 h719 h720 h1155 h1196 h1191
3041  T       t1197   o b1197 b4  G       s1196   t1143
3042    B       b1197   s1196
3043    T       t1197   o635 b1197 b1105
3044  B       b1198   t1197  B       b1198   t1197
3045  T       t1198   o627 b1158 b1198  S       s1198   t626 h h715 h716 h717 h718 h719 h720 h1155 h1196
3046  B       b1199   t1198  G       s1198   t1143
3047  P       p1199   String "instHypT [<< 'a >>; << inv{'s; 'a} >>] 5 thenT rwh fold_isset 0 thenT autoT thenT dT 8 ttca thenT dT 8 ttca"  B       b1199   s1198
3048  O       o1199   ext_rule p1199  T       t1199   o635 b1199 b1105
3049  T       t1199   o568 b1167 b1155  B       b1200   t1199
3050  H       h1199   y_6 t1199  H       h1200   w t575
3051  S       s1199   t620 h h696 h697 h698 h699 h700 h1167 h1199  S       s1200   t626 h h715 h716 h717 h718 h719 h720 h1155 h1200 h1196
3052  G       s1199   t1155  G       s1200   t1143
3053  B       b1200   s1199  B       b1201   s1200
3054  T       t1200   o629 b1200 b1121  T       t1201   o635 b1201 b1105
 B       b1201   t1200  
 T       t1201   o564 b1109 b559  
3055  B       b1202   t1201  B       b1202   t1201
3056  B       b1203   t1199  S       s1202   t626 h h715 h716 h717 h718 h719 h720 h1155 h1200
3057  T       t1203   o563 b1202 b1203  G       s1202   t1143
3058  H       h1203   y_5 t1203  B       b1203   s1202
3059  S       s1203   t620 h h696 h697 h698 h699 h700 h1167 h1203 h1199  T       t1203   o635 b1203 b1105
3060  G       s1203   t1155  B       b1204   t1203
3061  B       b1204   s1203  T       t1204   o b1093 b4
 T       t1204   o629 b1204 b1121  
3062  B       b1205   t1204  B       b1205   t1204
3063  S       s1205   t620 h h696 h697 h698 h699 h700 h1167 h1203  T       t1205   o887 b1205
3064  G       s1205   t1155  B       b1206   t1205
3065  B       b1206   s1205  T       t1206   o886 b1206
 T       t1206   o629 b1206 b1121  
3066  B       b1207   t1206  B       b1207   t1206
3067  B       b1208   t1203  T       t1207   o b1207 b997
3068  T       t1208   o563 b566 b1208  B       b1208   t1207
3069  H       h1208   w_1 t1208  T       t1208   o b565 b4
3070  S       s1208   t620 h h696 h697 h698 h699 h700 h1167 h1208 h1203  B       b1209   t1208
3071  G       s1208   t1155  T       t1209   o887 b1209
 B       b1209   s1208  
 T       t1209   o629 b1209 b1121  
3072  B       b1210   t1209  B       b1210   t1209
3073  S       s1210   t620 h h696 h697 h698 h699 h700 h1167 h1208  T       t1210   o886 b1210
3074  G       s1210   t1155  B       b1211   t1210
3075  B       b1211   s1210  T       t1211   o b1211 b997
 T       t1211   o629 b1211 b1121  
3076  B       b1212   t1211  B       b1212   t1211
3077  H       h1212   w t574  T       t1212   o634 b1157 b1212 b1184
3078  S       s1212   t620 h h696 h697 h698 h699 h700 h1167 h1212 h1208  B       b1213   t1212
3079  G       s1212   t1155  T       t1213   o2 b1213
 B       b1213   s1212  
 T       t1213   o629 b1213 b1121  
3080  B       b1214   t1213  B       b1214   t1213
3081  S       s1214   t620 h h696 h697 h698 h699 h700 h1167 h1212  T       t1214   o634 b1204 b1208 b1214
3082  G       s1214   t1155  B       b1215   t1214
3083  B       b1215   s1214  T       t1215   o2 b1215
 T       t1215   o629 b1215 b1121  
3084  B       b1216   t1215  B       b1216   t1215
3085  T       t1216   o b1109 b4  T       t1216   o634 b1202 b997 b1216
3086  B       b1217   t1216  B       b1217   t1216
3087  T       t1217   o882 b1217  T       t1217   o2 b1217
3088  B       b1218   t1217  B       b1218   t1217
3089  T       t1218   o881 b1218  T       t1218   o634 b1200 b4 b1218
3090  B       b1219   t1218  B       b1219   t1218
3091  T       t1219   o b1219 b1003  T       t1219   o2 b1219
3092  B       b1220   t1219  B       b1220   t1219
3093  T       t1220   o b565 b4  T       t1220   o634 b1198 b4 b1220
3094  B       b1221   t1220  B       b1221   t1220
3095  T       t1221   o882 b1221  T       t1221   o2 b1221
3096  B       b1222   t1221  B       b1222   t1221
3097  T       t1222   o881 b1222  T       t1222   o634 b1195 b4 b1222
3098  B       b1223   t1222  B       b1223   t1222
3099  T       t1223   o b1223 b1003  T       t1223   o2 b1223
3100  B       b1224   t1223  B       b1224   t1223
3101  T       t1224   o628 b1169 b1224 b1196  T       t1224   o634 b1193 b4 b1224
3102  B       b1225   t1224  B       b1225   t1224
3103  T       t1225   o2 b1225  T       t1225   o2 b1225
3104  B       b1226   t1225  B       b1226   t1225
3105  T       t1226   o628 b1216 b1220 b1226  T       t1226   o634 b1189 b4 b1226
3106  B       b1227   t1226  B       b1227   t1226
3107  T       t1227   o2 b1227  T       t1227   o b1227 b4
3108  B       b1228   t1227  B       b1228   t1227
3109  T       t1228   o628 b1214 b1003 b1228  T       t1228   o633 b1185 b1228
3110  B       b1229   t1228  B       b1229   t1228
3111  T       t1229   o2 b1229  P       p1229   String "equivSubstT << equiv{car{'s}; eqG{'s}; op{'s; 'a; inv{'s; 'a}}; op{'g; 'a; inv{'s; 'a}}} >> 8 thenT autoT"
3112  B       b1230   t1229  O       o1229   ext_rule p1229
3113  T       t1230   o628 b1212 b4 b1230  T       t1229   o568 b560 b578 b1143 b942
3114    H       h1229   z_1 t1229
3115    S       s1229   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229
3116    G       s1229   t1143
3117    B       b1230   s1229
3118    T       t1230   o635 b1230 b1105
3119  B       b1231   t1230  B       b1231   t1230
3120  T       t1231   o2 b1231  T       t1231   o2 b1227
3121  B       b1232   t1231  B       b1232   t1231
3122  T       t1232   o628 b1210 b4 b1232  T       t1232   o634 b1231 b4 b1232
3123  B       b1233   t1232  B       b1233   t1232
3124  T       t1233   o2 b1233  NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv
3125  B       b1234   t1233  O       o1233   equiv_fun_prop
3126  T       t1234   o628 b1207 b4 b1234  P       p1233   Var z_1
3127  B       b1235   t1234  O       o1234   var p1233
3128  T       t1235   o2 b1235  T       t1234   o1234
3129  B       b1236   t1235  B       b1234   t1234
3130  T       t1236   o628 b1205 b4 b1236  T       t1235   o568 b560 b578 b1234 b942
3131  B       b1237   t1236  B       b1235   t1235 z_1
3132  T       t1237   o2 b1237  T       t1236   o1233 b559 b569 b1235
3133  B       b1238   t1237  S       s1236   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187
3134  T       t1238   o628 b1201 b4 b1238  G       s1236   t1236
3135  B       b1239   t1238  B       b1236   s1236
3136  T       t1239   o b1239 b4  T       t1237   o635 b1236 b1105
3137  B       b1240   t1239  B       b1237   t1237
3138  T       t1240   o627 b1197 b1240  T       t1238   o634 b1237 b4 b1232
3139  B       b1241   t1240  B       b1238   t1238
3140  P       p1241   String "setSubstT << equal{op{'s; 'a; inv{'s; 'a}}; op{'g; 'a; inv{'s; 'a}}} >> 7 thenT autoT"  T       t1239   o b1238 b4
3141    B       b1239   t1239
3142    T       t1240   o b1233 b1239
3143    B       b1240   t1240
3144    T       t1241   o633 b1227 b1240
3145    B       b1241   t1241
3146    P       p1241   String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'s}; id{'g}} >> 10 thenT autoT"
3147  O       o1241   ext_rule p1241  O       o1241   ext_rule p1241
3148  T       t1241   o575 b560 b578 b1155 b952  S       s1241   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229
3149  H       h1241   v t1241  G       s1241   t1107
 S       s1241   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241  
 G       s1241   t1155  
3150  B       b1242   s1241  B       b1242   s1241
3151  T       t1242   o629 b1242 b1121  T       t1242   o635 b1242 b1105
3152  B       b1243   t1242  B       b1243   t1242
3153  T       t1243   o2 b1239  T       t1243   o564 b1143 b560
3154  B       b1244   t1243  S       s1243   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229
3155  T       t1244   o628 b1243 b4 b1244  G       s1243   t1243
3156    B       b1244   s1243
3157    T       t1244   o635 b1244 b1105
3158  B       b1245   t1244  B       b1245   t1244
3159  S       s1245   t620 h h696 h697 h698 h699 h700 h1167 h1199  P       p1245   Var z_2
3160  G       s1245   t1070  O       o1245   var p1245
3161  B       b1246   s1245  T       t1245   o1245
3162  T       t1246   o629 b1246 b1121  B       b1246   t1245
3163  B       b1247   t1246  T       t1246   o568 b560 b578 b1143 b1246
3164  S       s1247   t620 h h696 h697 h698 h699 h700 h1167 h1199  B       b1247   t1246 z_2
3165  G       s1247   t1075  T       t1247   o1233 b560 b578 b1247
3166    S       s1247   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229
3167    G       s1247   t1247
3168  B       b1248   s1247  B       b1248   s1247
3169  T       t1248   o629 b1248 b1121  T       t1248   o635 b1248 b1105
3170  B       b1249   t1248  B       b1249   t1248
3171  T       t1249   o1070 b1249 b711 b1244  T       t1249   o2 b1233
3172  B       b1250   t1249  B       b1250   t1249
3173  T       t1250   o2 b1250  T       t1250   o634 b1249 b729 b1250
3174  B       b1251   t1250  B       b1251   t1250
3175  T       t1251   o1070 b1247 b4 b1251  T       t1251   o2 b1251
3176  B       b1252   t1251  B       b1252   t1251
3177  T       t1252   o b1252 b4  T       t1252   o634 b1245 b729 b1252
3178  B       b1253   t1252  B       b1253   t1252
3179  T       t1253   o b1245 b1253  T       t1253   o2 b1253
3180  B       b1254   t1253  B       b1254   t1253
3181  T       t1254   o627 b1239 b1254  T       t1254   o634 b1243 b4 b1254
3182  B       b1255   t1254  B       b1255   t1254
3183  P       p1255   String "equivSubstT << equiv{car{'g}; eqG{'g}; id{'s}; id{'g}} >> 9 thenT autoT"  S       s1255   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h1229
3184  O       o1255   ext_rule p1255  G       s1255   t1139
 S       s1255   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241  
 G       s1255   t1123  
3185  B       b1256   s1255  B       b1256   s1255
3186  T       t1256   o629 b1256 b1121  T       t1256   o635 b1256 b1105
3187  B       b1257   t1256  B       b1257   t1256
3188  T       t1257   o564 b1155 b560  T       t1257   o634 b1257 b4 b1254
3189  S       s1257   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241  B       b1258   t1257
3190  G       s1257   t1257  T       t1258   o b1258 b4
 B       b1258   s1257  
 T       t1258   o629 b1258 b1121  
3191  B       b1259   t1258  B       b1259   t1258
3192  NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv  T       t1259   o b1255 b1259
3193  O       o1259   equiv_fun_prop  B       b1260   t1259
3194  P       p1259   Var z  T       t1260   o633 b1233 b1260
3195  O       o1260   var p1259  B       b1261   t1260
3196  T       t1260   o1260  T       t1261   o633 b1255 b4
3197  B       b1260   t1260  B       b1262   t1261
3198  T       t1261   o575 b560 b578 b1155 b1260  T       t1262   o1150 b632 b1262 b4 b4
3199  B       b1261   t1261 z  B       b1263   t1262
3200  T       t1262   o1259 b560 b578 b1261  T       t1263   o633 b1258 b4
3201  S       s1262   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241  B       b1264   t1263
3202  G       s1262   t1262  T       t1264   o1152 b632 b1264 b4 b4
3203  B       b1262   s1262  B       b1265   t1264
3204  T       t1263   o629 b1262 b1121  T       t1265   o b1265 b4
3205  B       b1263   t1263  B       b1266   t1265
3206  T       t1264   o2 b1245  T       t1266   o b1263 b1266
3207  B       b1264   t1264  B       b1267   t1266
3208  T       t1265   o628 b1263 b711 b1264  T       t1267   o1241 b632 b1261 b1267 b4
3209  B       b1265   t1265  B       b1268   t1267
3210  T       t1266   o2 b1265  P       p1268   String "rwh unfold_equiv_fun_prop 0 thenT autoT"
3211  B       b1266   t1266  O       o1268   ext_rule p1268
3212  T       t1267   o628 b1259 b711 b1266  T       t1268   o568 b559 b569
3213  B       b1267   t1267  H       h1268   x t1268
3214  T       t1268   o2 b1267  H       h1269   x_1 t577
3215  B       b1268   t1268  T       t1269   o568 b560 b578 b565 b942
3216  T       t1269   o628 b1257 b4 b1268  H       h1270   x_2 t1269
3217  B       b1269   t1269  T       t1270   o568 b560 b578 b567 b942
3218  S       s1269   t620 h h696 h697 h698 h699 h700 h1167 h1199 h1241  S       s1270   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659 h1268 h1269 h1270
3219  G       s1269   t1151  G       s1270   t1270
3220  B       b1270   s1269  B       b1270   s1270
3221  T       t1270   o629 b1270 b1121  T       t1271   o635 b1270 b1105
3222  B       b1271   t1270  B       b1271   t1271
3223  T       t1271   o628 b1271 b4 b1268  B       b1272   t1269
3224  B       b1272   t1271  B       b1273   t1270
3225  T       t1272   o b1272 b4  T       t1273   o563 b1272 b1273
3226  B       b1273   t1272  S       s1273   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659 h1268 h1269
3227  T       t1273   o b1269 b1273  G       s1273   t1273
3228  B       b1274   t1273  B       b1274   s1273
3229  T       t1274   o627 b1245 b1274  T       t1274   o635 b1274 b1105
3230  B       b1275   t1274  B       b1275   t1274
3231  T       t1275   o627 b1269 b4  B       b1276   t1273
3232  B       b1276   t1275  T       t1276   o563 b577 b1276
3233  T       t1276   o1162 b626 b1276 b4 b4  S       s1276   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659 h1268
3234  B       b1277   t1276  G       s1276   t1276
3235  T       t1277   o627 b1272 b4  B       b1277   s1276
3236    T       t1277   o635 b1277 b1105
3237  B       b1278   t1277  B       b1278   t1277
3238  T       t1278   o1164 b626 b1278 b4 b4  B       b1279   t1268
3239  B       b1279   t1278  B       b1280   t1276
3240  T       t1279   o b1279 b4  T       t1280   o563 b1279 b1280
3241  B       b1280   t1279  S       s1280   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658 h659
3242  T       t1280   o b1277 b1280  G       s1280   t1280
3243  B       b1281   t1280  B       b1281   s1280
3244  T       t1281   o1255 b626 b1275 b1281 b4  T       t1281   o635 b1281 b1105
3245  B       b1282   t1281  B       b1282   t1281
3246  T       t1282   o627 b1252 b4  B       b1283   t1280 b
3247  B       b1283   t1282  T       t1283   o561 b562 b1283
3248  T       t1283   o1084 b626 b1283 b4 b4  S       s1283   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187 h658
3249  B       b1284   t1283  G       s1283   t1283
3250  T       t1284   o b1284 b4  B       b1284   s1283
3251    T       t1284   o635 b1284 b1105
3252  B       b1285   t1284  B       b1285   t1284
3253  T       t1285   o b1282 b1285  B       b1286   t1283 a
3254  B       b1286   t1285  T       t1286   o561 b562 b1286
3255  T       t1286   o1241 b626 b1255 b1286 b4  S       s1286   t626 h h715 h716 h717 h718 h719 h720 h1155 h1187
3256  B       b1287   t1286  G       s1286   t1286
3257  T       t1287   o b1287 b4  B       b1287   s1286
3258    T       t1287   o635 b1287 b1105
3259  B       b1288   t1287  B       b1288   t1287
3260  T       t1288   o1199 b626 b1241 b1288 b4  T       t1288   o2 b1238
3261  B       b1289   t1288  B       b1289   t1288
3262  T       t1289   o b1289 b4  T       t1289   o634 b1288 b729 b1289
3263  B       b1290   t1289  B       b1290   t1289
3264  T       t1290   o1166 b626 b1199 b1290 b4  T       t1290   o2 b1290
3265  B       b1291   t1290  B       b1291   t1290
3266  T       t1291   o b1291 b4  T       t1291   o634 b1285 b729 b1291
3267  B       b1292   t1291  B       b1292   t1291
3268  T       t1292   o b1166 b1292  T       t1292   o2 b1292
3269  B       b1293   t1292  B       b1293   t1292
3270  T       t1293   o b1164 b1293  T       t1293   o634 b1282 b729 b1293
3271  B       b1294   t1293  B       b1294   t1293
3272  T       t1294   o1117 b626 b1162 b1294 b4  T       t1294   o2 b1294
3273  B       b1295   t1294  B       b1295   t1294
3274  T       t1295   o624 b1295  T       t1295   o634 b1278 b729 b1295
3275  B       b1296   t1295  B       b1296   t1295
3276  P       p1296   Number 2375  T       t1296   o2 b1296
3277  O       o1296   resource_defs p254 p1296 p300  B       b1297   t1296
3278  P       p1297   Number 2373  T       t1297   o634 b1275 b729 b1297
3279  O       o1297   uid p1297 p1296  B       b1298   t1297
3280  T       t1297   o1297 b639  T       t1298   o2 b1298
3281  B       b1297   t1297  B       b1299   t1298
3282  T       t1298   o b1297 b4  T       t1299   o634 b1271 b4 b1299
3283  B       b1298   t1298  B       b1300   t1299
3284  T       t1299   o1296 b1298  T       t1300   o b1300 b4
3285  B       b1299   t1299  B       b1301   t1300
3286  T       t1300   o b1299 b4  T       t1301   o633 b1238 b1301
3287  B       b1300   t1300  B       b1302   t1301
3288  T       t1301   o1105 b610 b1117 b1296 b1300  P       p1302   String "instHypT [<< 'a >>; << 'b >>] 6 ttca thenT dT 15 ttca thenT equivTransT << 'a >> thenT autoT thenT rwh unfold_equiv 14 thenT rwh unfold_equiv 15 ttca thenT equivSymT ttca"
3289  B       b1301   t1301  O       o1302   ext_rule p1302
3290  T       t1302   o1104 b1301  T       t1302   o633 b1300 b4
3291  B       b1302   t1302  B       b1303   t1302
3292  P       p1302   Number 2800  T       t1303   o1302 b632 b1303 b4 b4
3293  P       p1303   Number 3536  B       b1304   t1303
3294  O       o1303   location p1302 p1303  T       t1304   o b1304 b4
3295  P       p1304   String subgroup_isect  B       b1305   t1304
3296  O       o1304   rule p1304  T       t1305   o1268 b632 b1302 b1305 b4
3297  NSummary!term_param     term_param      term_param Summary  B       b1306   t1305
3298  O       o1305   term_param  T       t1306   o b1306 b4
3299  P       p1305   Var h1  B       b1307   t1306
3300  O       o1306   var p1305  T       t1307   o b1268 b1307
3301  T       t1306   o1306  B       b1308   t1307
3302  B       b1306   t1306  T       t1308   o1229 b632 b1241 b1308 b4
3303  T       t1307   o1305 b1306  B       b1309   t1308
3304  B       b1307   t1307  T       t1309   o b1309 b4
3305  P       p1307   Var h2  B       b1310   t1309
3306  O       o1307   var p1307  T       t1310   o1187 b632 b1229 b1310 b4
3307  T       t1308   o1307  B       b1311   t1310
3308  B       b1308   t1308  T       t1311   o b1311 b4
3309  T       t1309   o1305 b1308  B       b1312   t1311
3310  B       b1309   t1309  T       t1312   o1154 b632 b1187 b1312 b4
3311  T       t1310   o b1309 b4  B       b1313   t1312
3312  B       b1310   t1310  T       t1313   o b1313 b4
3313  T       t1311   o b1307 b1310  B       b1314   t1313
3314  B       b1311   t1311  T       t1314   o b1154 b1314
3315  T       t1312   o b609 b1311  B       b1315   t1314
3316  B       b1312   t1312  T       t1315   o b1152 b1315
3317  T       t1313   o613 b614 b1306 b1306  B       b1316   t1315
3318  S       s1313   t613 h  T       t1316   o1101 b632 b1150 b1316 b4
3319  G       s1313   t1313  B       b1317   t1316
3320  B       b1313   s1313  T       t1317   o630 b1317
3321  T       t1314   o611 b1313  B       b1318   t1317
3322  B       b1314   t1314  P       p1318   Number 2696
3323  T       t1315   o613 b614 b1308 b1308  P       p1319   Number 2704
3324  S       s1315   t613 h  O       o1319   resource_defs p1318 p1319 p300
3325  G       s1315   t1315  P       p1320   Number 2702
3326  B       b1315   s1315  O       o1320   uid p1320 p1319
3327  T       t1316   o611 b1315  T       t1320   o1320 b645
3328  B       b1316   t1316  B       b1320   t1320
3329  P       p1316   Var h  T       t1321   o b1320 b4
 O       o1316   var p1316  
 T       t1317   o1316  
 B       b1317   t1317  
 T       t1318   o613 b614 b1317 b1317  
 S       s1318   t613 h  
 G       s1318   t1318  
 B       b1318   s1318  
 T       t1319   o611 b1318  
 B       b1319   t1319  
 T       t1320   o557 b1317  
 S       s1320   t620 h  
 G       s1320   t1320  
 B       b1320   s1320  
 T       t1321   o611 b1320  
3330  B       b1321   t1321  B       b1321   t1321
3331  T       t1322   o548 b1306 b550  T       t1322   o1319 b1321
3332  S       s1322   t620 h  B       b1322   t1322
3333  G       s1322   t1322  T       t1323   o b1322 b4
 B       b1322   s1322  
 T       t1323   o611 b1322  
3334  B       b1323   t1323  B       b1323   t1323
3335  T       t1324   o548 b1308 b550  T       t1324   o1089 b616 b1101 b1318 b1323
3336  S       s1324   t620 h  B       b1324   t1324
3337  G       s1324   t1324  T       t1325   o1088 b1324
 B       b1324   s1324  
 T       t1325   o611 b1324  
3338  B       b1325   t1325  B       b1325   t1325
3339  T       t1326   o559 b1317  O       o1325   location p p
3340  B       b1326   t1326  P       p1325   String subgroup_isect
3341  NCzf_itt_isect  Czf_itt_isect   Czf_itt_isect NIL  O       o1326   rule p1325
3342  NCzf_itt_isect!isect    isect   isect Czf_itt_isect  NSummary!term_param     term_param      term_param Summary
3343  O       o1326   isect  O       o1327   term_param
3344  T       t1327   o559 b1306  P       p1327   Var h1
3345  B       b1327   t1327  O       o1328   var p1327
3346  T       t1328   o559 b1308  T       t1328   o1328
3347  B       b1328   t1328  B       b1328   t1328
3348  T       t1329   o1326 b1327 b1328  T       t1329   o1327 b1328
3349  B       b1329   t1329  B       b1329   t1329
3350  T       t1330   o568 b1326 b1329  P       p1329   Var h2
3351  S       s1330   t620 h  O       o1329   var p1329
3352  G       s1330   t1330  T       t1330   o1329
3353  B       b1330   s1330  B       b1330   t1330
3354  T       t1331   o611 b1330  T       t1331   o1327 b1330
3355  B       b1331   t1331  B       b1331   t1331
3356  T       t1332   o564 b565 b1326  T       t1332   o b1331 b4
3357  H       h1332   x t1332  B       b1332   t1332
3358  T       t1333   o564 b567 b1326  T       t1333   o b1329 b1332
3359  H       h1333   x t1333  B       b1333   t1333
3360  T       t1334   o569 b1317 b565 b567  T       t1334   o b615 b1333
3361  B       b1334   t1334  B       b1334   t1334
3362  T       t1335   o569 b1306 b565 b567  T       t1335   o619 b620 b1328 b1328
3363  B       b1335   t1335  S       s1335   t619 h
3364  T       t1336   o568 b1334 b1335  G       s1335   t1335
3365  S       s1336   t620 h h651 h652 h1332 h1333  B       b1335   s1335
3366  G       s1336   t1336  T       t1336   o617 b1335
3367  B       b1336   s1336  B       b1336   t1336
3368  T       t1337   o611 b1336  T       t1337   o619 b620 b1330 b1330
3369  B       b1337   t1337  S       s1337   t619 h
3370  T       t1338   o576 b1317  G       s1337   t1337
3371    B       b1337   s1337
3372    T       t1338   o617 b1337
3373  B       b1338   t1338  B       b1338   t1338
3374  T       t1339   o575 b1326 b1338 b565 b567  P       p1338   Var h
3375  H       h1339   x t1339  O       o1338   var p1338
3376  T       t1340   o576 b1306  T       t1339   o1338
3377  B       b1340   t1340  B       b1339   t1339
3378  T       t1341   o575 b1327 b1340 b565 b567  T       t1340   o619 b620 b1339 b1339
3379  S       s1341   t620 h h651 h652 h1339  S       s1340   t619 h
3380  G       s1341   t1341  G       s1340   t1340
3381  B       b1341   s1341  B       b1340   s1340
3382  T       t1342   o611 b1341  T       t1341   o617 b1340
3383  B       b1342   t1342  B       b1341   t1341
3384  T       t1343   o548 b1317 b550  T       t1342   o557 b1339
3385  S       s1343   t620 h  S       s1342   t626 h
3386  G       s1343   t1343  G       s1342   t1342
3387  B       b1343   s1343  B       b1342   s1342
3388  T       t1344   o611 b1343  T       t1343   o617 b1342
3389  B       b1344   t1344  B       b1343   t1343
3390  T       t1345   o610 b1342 b1344  T       t1344   o548 b1328 b550
3391    S       s1344   t626 h
3392    G       s1344   t1344
3393    B       b1344   s1344
3394    T       t1345   o617 b1344
3395  B       b1345   t1345  B       b1345   t1345
3396  T       t1346   o610 b1337 b1345  T       t1346   o548 b1330 b550
3397  B       b1346   t1346  S       s1346   t626 h
3398  T       t1347   o610 b1331 b1346  G       s1346   t1346
3399    B       b1346   s1346
3400    T       t1347   o617 b1346
3401  B       b1347   t1347  B       b1347   t1347
3402  T       t1348   o610 b1325 b1347  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
3403    NCzf_itt_eq!equal       equal1347       equal Czf_itt_eq
3404    O       o1347   equal1347
3405    T       t1348   o559 b1339
3406  B       b1348   t1348  B       b1348   t1348
3407  T       t1349   o610 b1323 b1348  NCzf_itt_isect  Czf_itt_isect   Czf_itt_isect NIL
3408    NCzf_itt_isect!isect    isect   isect Czf_itt_isect
3409    O       o1348   isect
3410    T       t1349   o559 b1328
3411  B       b1349   t1349  B       b1349   t1349
3412  T       t1350   o610 b1321 b1349  T       t1350   o559 b1330
3413  B       b1350   t1350  B       b1350   t1350
3414  T       t1351   o610 b1319 b1350  T       t1351   o1348 b1349 b1350
3415  B       b1351   t1351  B       b1351   t1351
3416  T       t1352   o610 b1316 b1351  T       t1352   o1347 b1348 b1351
3417  B       b1352   t1352  S       s1352   t626 h
3418  T       t1353   o610 b1314 b1352  G       s1352   t1352
3419    B       b1352   s1352
3420    T       t1353   o617 b1352
3421  B       b1353   t1353  B       b1353   t1353
3422  T       t1354   o610 b618 b1353  T       t1354   o564 b565 b1348
3423  B       b1354   t1354  H       h1354   x t1354
3424  P       p1354   String "assumT 6 thenT assumT 7 thenT assumT 8 thenT rwh unfold_subgroup 2 thenT rwh unfold_subgroup 3 thenT autoT"  T       t1355   o564 b567 b1348
3425  O       o1354   ext_rule p1354  H       h1355   y t1355
3426  T       t1355   o b1341 b4  T       t1356   o569 b1339
 B       b1355   t1355  
 T       t1356   o b1336 b1355  
3427  B       b1356   t1356  B       b1356   t1356
3428  T       t1357   o b1330 b1356  T       t1357   o570 b1339 b565 b567
3429  B       b1357   t1357  B       b1357   t1357
3430  T       t1358   o b1324 b1357  T       t1358   o570 b1328 b565 b567
3431  B       b1358   t1358  B       b1358   t1358
3432  T       t1359   o b1322 b1358  T       t1359   o568 b1348 b1356 b1357 b1358
3433  B       b1359   t1359  S       s1359   t626 h h658 h659 h1354 h1355
3434  T       t1360   o b1320 b1359  G       s1359   t1359
3435    B       b1359   s1359
3436    T       t1360   o617 b1359
3437  B       b1360   t1360  B       b1360   t1360
3438  T       t1361   o b1318 b1360  T       t1361   o568 b1348 b1356 b663 b664
3439  B       b1361   t1361  H       h1361   u t1361
3440  T       t1362   o b1315 b1361  T       t1362   o569 b1328
3441  B       b1362   t1362  B       b1362   t1362
3442  T       t1363   o b1313 b1362  T       t1363   o568 b1349 b1362 b663 b664
3443  B       b1363   t1363  S       s1363   t626 h h662 h663 h1361
3444  T       t1364   o b617 b1363  G       s1363   t1363
3445    B       b1363   s1363
3446    T       t1364   o617 b1363
3447  B       b1364   t1364  B       b1364   t1364
3448  T       t1365   o629 b1343 b1364  T       t1365   o564 b759 b1348
3449  B       b1365   t1365  H       h1365   x1 t1365
3450  T       t1366   o628 b1365 b4 b632  T       t1366   o564 b761 b1348
3451  B       b1366   t1366  H       h1366   y1 t1366
3452  T       t1367   o557 b1306  T       t1367   o568 b1349 b1362 b759 b761
3453  H       h1367   y_4 t1367  H       h1367   v t1367
3454  H       h1368   y_5 t558  T       t1368   o568 b1348 b1356 b759 b761
3455  T       t1368   o558 b1327 b560  S       s1368   t626 h h757 h758 h1365 h1366 h1367
3456  H       h1369   y_6 t1368  G       s1368   t1368
3457  T       t1369   o564 b565 b1327  B       b1368   s1368
3458    T       t1369   o617 b1368
3459  B       b1369   t1369  B       b1369   t1369
3460  T       t1370   o564 b567 b1327  T       t1370   o548 b1339 b550
3461  B       b1370   t1370  S       s1370   t626 h
3462  T       t1371   o568 b1335 b570  G       s1370   t1370
3463    B       b1370   s1370
3464    T       t1371   o617 b1370
3465  B       b1371   t1371  B       b1371   t1371
3466  T       t1372   o563 b1370 b1371  T       t1372   o616 b1369 b1371
3467  B       b1372   t1372  B       b1372   t1372
3468  T       t1373   o563 b1369 b1372  T       t1373   o616 b1364 b1372
3469  B       b1373   t1373 b  B       b1373   t1373
3470  T       t1374   o561 b562 b1373  T       t1374   o616 b1360 b1373
3471  B       b1374   t1374 a  B       b1374   t1374
3472  T       t1375   o561 b562 b1374  T       t1375   o616 b1353 b1374
3473  H       h1375   y_7 t1375  B       b1375   t1375
3474  B       b1375   t1341  T       t1376   o616 b1347 b1375
3475  T       t1376   o563 b1375 b579  B       b1376   t1376
3476  B       b1376   t1376 b  T       t1377   o616 b1345 b1376
3477  T       t1377   o561 b562 b1376  B       b1377   t1377
3478  B       b1377   t1377 a  T       t1378   o616 b1343 b1377
3479  T       t1378   o561 b562 b1377  B       b1378   t1378
3480  H       h1378   z_2 t1378  T       t1379   o616 b1341 b1378
3481  T       t1379   o557 b1308  B       b1379   t1379
3482  H       h1379   y t1379  T       t1380   o616 b1338 b1379
3483  T       t1380   o558 b1328 b560  B       b1380   t1380
3484  H       h1380   y_2 t1380  T       t1381   o616 b1336 b1380
 T       t1381   o564 b565 b1328  
3485  B       b1381   t1381  B       b1381   t1381
3486  T       t1382   o564 b567 b1328  T       t1382   o616 b624 b1381
3487  B       b1382   t1382  B       b1382   t1382
3488  T       t1383   o569 b1308 b565 b567  P       p1382   String "assumT 6 thenT assumT 8 thenT rwh unfold_subgroup 2 thenT autoT"
3489    O       o1382   ext_rule p1382
3490    T       t1383   o b1368 b4
3491  B       b1383   t1383  B       b1383   t1383
3492  T       t1384   o568 b1383 b570  T       t1384   o b1363 b1383
3493  B       b1384   t1384  B       b1384   t1384
3494  T       t1385   o563 b1382 b1384  T       t1385   o b1359 b1384
3495  B       b1385   t1385  B       b1385   t1385
3496  T       t1386   o563 b1381 b1385  T       t1386   o b1352 b1385
3497  B       b1386   t1386 b  B       b1386   t1386
3498  T       t1387   o561 b562 b1386  T       t1387   o b1346 b1386
3499  B       b1387   t1387 a  B       b1387   t1387
3500  T       t1388   o561 b562 b1387  T       t1388   o b1344 b1387
3501  H       h1388   y_3 t1388  B       b1388   t1388
3502  T       t1389   o576 b1308  T       t1389   o b1342 b1388
3503  B       b1389   t1389  B       b1389   t1389
3504  T       t1390   o575 b1328 b1389 b565 b567  T       t1390   o b1340 b1389
3505  B       b1390   t1390  B       b1390   t1390
3506  T       t1391   o563 b1390 b579  T       t1391   o b1337 b1390
3507  B       b1391   t1391 b  B       b1391   t1391
3508  T       t1392   o561 b562 b1391  T       t1392   o b1335 b1391
3509  B       b1392   t1392 a  B       b1392   t1392
3510  T       t1393   o561 b562 b1392  T       t1393   o b623 b1392
3511  H       h1393   z_1 t1393  B       b1393   t1393
3512  H       h1394   v_2 t1330  T       t1394   o635 b1370 b1393
3513  H       h1395   x t562  B       b1394   t1394
3514  P       p1395   Var x  T       t1395   o634 b1394 b4 b638
 O       o1395   var p1395  
 T       t1395   o1395  
3515  B       b1395   t1395  B       b1395   t1395
3516  T       t1396   o564 b1395 b1326  T       t1396   o557 b1328
3517  H       h1396   y t1396  H       h1396   y t1396
3518  T       t1397   o564 b1395 b560  T       t1397   o558 b1349 b560
3519  S       s1397   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396  H       h1397   y_2 t1397
3520  G       s1397   t1397  T       t1398   o564 b565 b1349
 B       b1397   s1397  
 T       t1398   o629 b1397 b1364  
3521  B       b1398   t1398  B       b1398   t1398
3522  T       t1399   o558 b1326 b560  T       t1399   o564 b567 b1349
3523  S       s1399   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394  B       b1399   t1399
3524  G       s1399   t1399  T       t1400   o568 b1349 b1362 b1358 b571
 B       b1399   s1399  
 T       t1400   o629 b1399 b1364  
3525  B       b1400   t1400  B       b1400   t1400
3526  S       s1400   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394  T       t1401   o563 b1399 b1400
3527  G       s1400   t1343  B       b1401   t1401
3528  B       b1401   s1400  T       t1402   o563 b1398 b1401
3529  T       t1401   o629 b1401 b1364  B       b1402   t1402 b
3530  B       b1402   t1401  T       t1403   o561 b562 b1402
3531  B       b1403   t1375  B       b1403   t1403 a
3532  B       b1404   t1378  T       t1404   o561 b562 b1403
3533  T       t1404   o556 b1403 b1404  H       h1404   y_3 t1404
3534  H       h1404   z t1404  T       t1405   o568 b1349 b1362 b565 b567
3535  S       s1404   t620 h h1367 h1368 h1369 h1404 h1379 h697 h1380 h1388 h1393 h1394  B       b1405   t1405
3536  G       s1404   t1343  T       t1406   o563 b1405 b579
3537  B       b1405   s1404  B       b1406   t1406 b
3538  T       t1405   o629 b1405 b1364  T       t1407   o561 b562 b1406
3539  B       b1406   t1405  B       b1407   t1407 a
3540  B       b1407   t1368  T       t1408   o561 b562 b1407
3541  B       b1408   t1404  H       h1408   y_4 t1408
3542  T       t1408   o556 b1407 b1408  T       t1409   o563 b579 b1405
3543  H       h1408   z_2 t1408  B       b1409   t1409
3544  S       s1408   t620 h h1367 h1368 h1408 h1379 h697 h1380 h1388 h1393 h1394  T       t1410   o563 b1399 b1409
3545  G       s1408   t1343  B       b1410   t1410
3546  B       b1409   s1408  T       t1411   o563 b1398 b1410
3547  T       t1409   o629 b1409 b1364  B       b1411   t1411 b
3548  B       b1410   t1409  T       t1412   o561 b562 b1411
3549  B       b1411   t1408  B       b1412   t1412 a
3550  T       t1411   o556 b558 b1411  T       t1413   o561 b562 b1412
3551  H       h1411   z t1411  H       h1413   z t1413
3552  S       s1411   t620 h h1367 h1411 h1379 h697 h1380 h1388 h1393 h1394  H       h1414   v_1 t1352
3553  G       s1411   t1343  H       h1415   x t562
3554  B       b1412   s1411  P       p1415   Var x
3555  T       t1412   o629 b1412 b1364  O       o1415   var p1415
3556  B       b1413   t1412  T       t1415   o1415
3557  B       b1414   t1367  B       b1415   t1415
3558  B       b1415   t1411  T       t1416   o564 b1415 b1348
3559  T       t1415   o556 b1414 b1415  H       h1416   y t1416
3560  H       h1415   v t1415  T       t1417   o564 b1415 b560
3561  S       s1415   t620 h h1415 h1379 h697 h1380 h1388 h1393 h1394  S       s1417   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416
3562  G       s1415   t1343  G       s1417   t1417
3563  B       b1416   s1415  B       b1417   s1417
3564  T       t1416   o629 b1416 b1364  T       t1418   o635 b1417 b1393
3565  B       b1417   t1416  B       b1418   t1418
3566  B       b1418   t1388  T       t1419   o558 b1348 b560
3567  B       b1419   t1393  S       s1419   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414
3568  T       t1419   o556 b1418 b1419  G       s1419   t1419
3569  H       h1419   z t1419  B       b1419   s1419
3570  S       s1419   t620 h h1415 h1379 h697 h1380 h1419 h1394  T       t1420   o635 b1419 b1393
3571  G       s1419   t1343  B       b1420   t1420
3572  B       b1420   s1419  S       s1420   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414
3573  T       t1420   o629 b1420 b1364  G       s1420   t1370
3574  B       b1421   t1420  B       b1421   s1420
3575  B       b1422   t1380  T       t1421   o635 b1421 b1393
3576  B       b1423   t1419  B       b1422   t1421
3577  T       t1423   o556 b1422 b1423  B       b1423   t1408
3578  H       h1423   z_1 t1423  B       b1424   t1413
3579  S       s1423   t620 h h1415 h1379 h697 h1423 h1394  T       t1424   o556 b1423 b1424
3580  G       s1423   t1343  H       h1424   z_1 t1424
3581  B       b1424   s1423  S       s1424   t626 h h1396 h716 h1397 h1404 h1424 h1414
3582  T       t1424   o629 b1424 b1364  G       s1424   t1370
3583  B       b1425   t1424  B       b1425   s1424
3584  B       b1426   t1423  T       t1425   o635 b1425 b1393
3585  T       t1426   o556 b558 b1426  B       b1426   t1425
3586  H       h1426   z t1426  B       b1427   t1404
3587  S       s1426   t620 h h1415 h1379 h1426 h1394  B       b1428   t1424
3588  G       s1426   t1343  T       t1428   o556 b1427 b1428
3589  B       b1427   s1426  H       h1428   z t1428
3590  T       t1427   o629 b1427 b1364  S       s1428   t626 h h1396 h716 h1397 h1428 h1414
3591  B       b1428   t1427  G       s1428   t1370
3592  B       b1429   t1379  B       b1429   s1428
3593  B       b1430   t1426  T       t1429   o635 b1429 b1393
3594  T       t1430   o556 b1429 b1430  B       b1430   t1429
3595  H       h1430   v_1 t1430  B       b1431   t1397
3596  S       s1430   t620 h h1415 h1430 h1394  B       b1432   t1428
3597  G       s1430   t1343  T       t1432   o556 b1431 b1432
3598  B       b1431   s1430  H       h1432   z_1 t1432
3599  T       t1431   o629 b1431 b1364  S       s1432   t626 h h1396 h716 h1432 h1414
3600  B       b1432   t1431  G       s1432   t1370
 H       h1432   v_1 t1324  
 S       s1432   t620 h h1415 h1432 h1394  
 G       s1432   t1343  
3601  B       b1433   s1432  B       b1433   s1432
3602  T       t1433   o629 b1433 b1364  T       t1433   o635 b1433 b1393
3603  B       b1434   t1433  B       b1434   t1433
3604  H       h1434   v t1322  B       b1435   t1432
3605  S       s1434   t620 h h1434 h1432 h1394  T       t1435   o556 b558 b1435
3606  G       s1434   t1343  H       h1435   z t1435
3607  B       b1435   s1434  S       s1435   t626 h h1396 h1435 h1414
3608  T       t1435   o629 b1435 b1364  G       s1435   t1370
3609  B       b1436   t1435  B       b1436   s1435
3610  S       s1436   t620 h h1434 h1432  T       t1436   o635 b1436 b1393
3611  G       s1436   t1343  B       b1437   t1436
3612  B       b1437   s1436  B       b1438   t1396
3613  T       t1437   o629 b1437 b1364  B       b1439   t1435
3614  B       b1438   t1437  T       t1439   o556 b1438 b1439
3615  S       s1438   t620 h h1434  H       h1439   v t1439
3616  G       s1438   t1343  S       s1439   t626 h h1439 h1414
3617  B       b1439   s1438  G       s1439   t1370
3618  T       t1439   o629 b1439 b1364  B       b1440   s1439
3619  B       b1440   t1439  T       t1440   o635 b1440 b1393
 T       t1440   o2 b1366  
3620  B       b1441   t1440  B       b1441   t1440
3621  T       t1441   o628 b1440 b4 b1441  H       h1441   v t1344
3622  B       b1442   t1441  S       s1441   t626 h h1441 h1414
3623  T       t1442   o2 b1442  G       s1441   t1370
3624    B       b1442   s1441
3625    T       t1442   o635 b1442 b1393
3626  B       b1443   t1442  B       b1443   t1442
3627  T       t1443   o628 b1438 b4 b1443  S       s1443   t626 h h1441
3628  B       b1444   t1443  G       s1443   t1370
3629  T       t1444   o2 b1444  B       b1444   s1443
3630    T       t1444   o635 b1444 b1393
3631  B       b1445   t1444  B       b1445   t1444
3632  T       t1445   o628 b1436 b4 b1445  T       t1445   o2 b1395
3633  B       b1446   t1445  B       b1446   t1445
3634  T       t1446   o2 b1446  T       t1446   o634 b1445 b4 b1446
3635  B       b1447   t1446  B       b1447   t1446
3636  T       t1447   o628 b1434 b4 b1447  T       t1447   o2 b1447
3637  B       b1448   t1447  B       b1448   t1447
3638  T       t1448   o2 b1448  T       t1448   o634 b1443 b4 b1448
3639  B       b1449   t1448  B       b1449   t1448
3640  T       t1449   o628 b1432 b4 b1449  T       t1449   o2 b1449
3641  B       b1450   t1449  B       b1450   t1449
3642  T       t1450   o2 b1450  T       t1450   o634 b1441 b4 b1450
3643  B       b1451   t1450  B       b1451   t1450
3644  T       t1451   o628 b1428 b4 b1451  T       t1451   o2 b1451
3645  B       b1452   t1451  B       b1452   t1451
3646  T       t1452   o2 b1452  T       t1452   o634 b1437 b4 b1452
3647  B       b1453   t1452  B       b1453   t1452
3648  T       t1453   o628 b1425 b4 b1453  T       t1453   o2 b1453
3649  B       b1454   t1453  B       b1454   t1453
3650  T       t1454   o2 b1454  T       t1454   o634 b1434 b4 b1454
3651  B       b1455   t1454  B       b1455   t1454
3652  T       t1455   o628 b1421 b4 b1455  T       t1455   o2 b1455
3653  B       b1456   t1455  B       b1456   t1455
3654  T       t1456   o2 b1456  T       t1456   o634 b1430 b4 b1456
3655  B       b1457   t1456  B       b1457   t1456
3656  T       t1457   o628 b1417 b4 b1457  T       t1457   o2 b1457
3657  B       b1458   t1457  B       b1458   t1457
3658  T       t1458   o2 b1458  T       t1458   o634 b1426 b4 b1458
3659  B       b1459   t1458  B       b1459   t1458
3660  T       t1459   o628 b1413 b4 b1459  T       t1459   o2 b1459
3661  B       b1460   t1459  B       b1460   t1459
3662  T       t1460   o2 b1460  T       t1460   o634 b1422 b729 b1460
3663  B       b1461   t1460  B       b1461   t1460
3664  T       t1461   o628 b1410 b4 b1461  T       t1461   o2 b1461
3665  B       b1462   t1461  B       b1462   t1461
3666  T       t1462   o2 b1462  T       t1462   o634 b1420 b729 b1462
3667  B       b1463   t1462  B       b1463   t1462
3668  T       t1463   o628 b1406 b4 b1463  T       t1463   o2 b1463
3669  B       b1464   t1463  B       b1464   t1463
3670  T       t1464   o2 b1464  T       t1464   o634 b1418 b4 b1464
3671  B       b1465   t1464  B       b1465   t1464
3672  T       t1465   o628 b1402 b711 b1465  T       t1465   o568 b1348 b1356 b1357 b571
3673  B       b1466   t1465  S       s1465   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355
3674  T       t1466   o2 b1466  G       s1465   t1465
3675    B       b1466   s1465
3676    T       t1466   o635 b1466 b1393
3677  B       b1467   t1466  B       b1467   t1466
3678  T       t1467   o628 b1400 b711 b1467  T       t1467   o634 b1467 b4 b1462
3679  B       b1468   t1467  B       b1468   t1467
3680  T       t1468   o2 b1468  T       t1468   o564 b668 b1348
3681  B       b1469   t1468  H       h1468   x t1468
3682  T       t1469   o628 b1398 b4 b1469  T       t1469   o564 b670 b1348
3683  B       b1470   t1469  H       h1469   y t1469
3684  H       h1470   y t1333  T       t1470   o568 b1348 b1356 b668 b670
3685  NCzf_itt_eq!eq  eq      eq Czf_itt_eq  S       s1470   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h667 h668 h1468 h1469 h672
 O       o1470   eq  
 T       t1470   o1470 b1334 b570  
 S       s1470   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470  
3686  G       s1470   t1470  G       s1470   t1470
3687  B       b1471   s1470  B       b1470   s1470
3688  T       t1471   o629 b1471 b1364  T       t1471   o635 b1470 b1393
3689  B       b1472   t1471  B       b1471   t1471
3690  T       t1472   o568 b1334 b570  T       t1472   o634 b1471 b4 b1462
3691  S       s1472   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470  B       b1472   t1472
3692  G       s1472   t1472  T       t1473   o b1472 b4
3693  B       b1473   s1472  B       b1473   t1473
3694  T       t1473   o629 b1473 b1364  T       t1474   o b1468 b1473
3695  B       b1474   t1473  B       b1474   t1474
3696  T       t1474   o628 b1474 b711 b1467  T       t1475   o b1465 b1474
3697  B       b1475   t1474  B       b1475   t1475
3698  T       t1475   o2 b1475  T       t1476   o633 b1395 b1475
3699  B       b1476   t1475  B       b1476   t1476
3700  T       t1476   o628 b1472 b4 b1476  P       p1476   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 10 ttca"
3701  B       b1477   t1476  O       o1476   ext_rule p1476
3702  T       t1477   o b1477 b4  T       t1477   o564 b1415 b1351
3703  B       b1478   t1477  H       h1477   v t1477
3704  T       t1478   o b1470 b1478  S       s1477   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416 h1477
3705  B       b1479   t1478  G       s1477   t1417
3706  T       t1479   o627 b1366 b1479  B       b1477   s1477
3707  B       b1480   t1479  T       t1478   o635 b1477 b1393
3708  P       p1480   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 14 ttca"  B       b1478   t1478
3709  O       o1480   ext_rule p1480  T       t1479   o2 b1465
3710  T       t1480   o564 b1395 b1329  B       b1479   t1479
3711  H       h1480   v t1480  T       t1480   o634 b1478 b4 b1479
3712  S       s1480   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396 h1480  B       b1480   t1480
3713  G       s1480   t1397  T       t1481   o b1480 b4
3714  B       b1481   s1480  B       b1481   t1481
3715  T       t1481   o629 b1481 b1364  T       t1482   o633 b1465 b1481
3716  B       b1482   t1481  B       b1482   t1482
3717  T       t1482   o2 b1470  P       p1482   String "rwh unfold_bisect 11 thenT dT 11 ttca"
3718  B       b1483   t1482  O       o1482   ext_rule p1482
 T       t1483   o628 b1482 b4 b1483  
 B       b1484   t1483  
 T       t1484   o b1484 b4  
 B       b1485   t1484  
 T       t1485   o627 b1470 b1485  
 B       b1486   t1485  
 P       p1486   String "rwh unfold_bisect 15 thenT dT 15 ttca"  
 O       o1486   ext_rule p1486  
3719  NCzf_itt_sep    Czf_itt_sep     Czf_itt_sep NIL  NCzf_itt_sep    Czf_itt_sep     Czf_itt_sep NIL
3720  NCzf_itt_sep!sep        sep     sep Czf_itt_sep  NCzf_itt_sep!sep        sep     sep Czf_itt_sep
3721  O       o1487   sep  O       o1483   sep
3722  T       t1487   o564 b1395 b1328  T       t1483   o564 b1415 b1350
3723  B       b1487   t1487 x  B       b1483   t1483 x
3724  T       t1488   o1487 b1327 b1487  T       t1484   o1483 b1349 b1483
3725  B       b1488   t1488  B       b1484   t1484
3726  T       t1489   o564 b1395 b1488  T       t1485   o564 b1415 b1484
3727  H       h1489   v t1489  H       h1485   v t1485
3728  T       t1490   o564 b1395 b1327  T       t1486   o564 b1415 b1349
3729  H       h1490   u t1490  H       h1486   u t1486
3730  H       h1491   v_1 t1487  H       h1487   v_2 t1483
3731  S       s1491   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396 h1489 h1490 h1491  S       s1487   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416 h1485 h1486 h1487
3732  G       s1491   t1397  G       s1487   t1417
3733  B       b1491   s1491  B       b1487   s1487
3734  T       t1491   o629 b1491 b1364  T       t1487   o635 b1487 b1393
3735    B       b1488   t1487
3736    S       s1488   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h1415 h1416 h1485
3737    G       s1488   t1417
3738    B       b1489   s1488
3739    T       t1489   o635 b1489 b1393
3740    B       b1490   t1489
3741    T       t1490   o2 b1480
3742    B       b1491   t1490
3743    T       t1491   o634 b1490 b4 b1491
3744  B       b1492   t1491  B       b1492   t1491
3745  S       s1492   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h1395 h1396 h1489  T       t1492   o2 b1492
3746  G       s1492   t1397  B       b1493   t1492
3747  B       b1493   s1492  T       t1493   o634 b1488 b4 b1493
 T       t1493   o629 b1493 b1364  
3748  B       b1494   t1493  B       b1494   t1493
3749  T       t1494   o2 b1484  T       t1494   o b1494 b4
3750  B       b1495   t1494  B       b1495   t1494
3751  T       t1495   o628 b1494 b4 b1495  T       t1495   o633 b1480 b1495
3752  B       b1496   t1495  B       b1496   t1495
3753  T       t1496   o2 b1496  P       p1496   String "withT << 'x >> (dT 4) ttca"
3754    O       o1496   ext_rule p1496
3755    T       t1496   o633 b1494 b4
3756  B       b1497   t1496  B       b1497   t1496
3757  T       t1497   o628 b1492 b4 b1497  T       t1497   o1496 b632 b1497 b4 b4
3758  B       b1498   t1497  B       b1498   t1497
3759  T       t1498   o b1498 b4  T       t1498   o b1498 b4
3760  B       b1499   t1498  B       b1499   t1498
3761  T       t1499   o627 b1484 b1499  T       t1499   o1482 b632 b1496 b1499 b4
3762  B       b1500   t1499  B       b1500   t1499
3763  P       p1500   String "withT << 'x >> (dT 4) ttca"  T       t1500   o b1500 b4
 O       o1500   ext_rule p1500  
 T       t1500   o627 b1498 b4  
3764  B       b1501   t1500  B       b1501   t1500
3765  T       t1501   o1500 b626 b1501 b4 b4  T       t1501   o1476 b632 b1482 b1501 b4
3766  B       b1502   t1501  B       b1502   t1501
3767  T       t1502   o b1502 b4  P       p1502   String "assumT 9 thenT assumT 11 ttca"
3768  B       b1503   t1502  O       o1502   ext_rule p1502
3769  T       t1503   o1486 b626 b1500 b1503 b4  B       b1503   t1354
3770  B       b1504   t1503  B       b1504   t1355
3771  T       t1504   o b1504 b4  B       b1505   t1359
3772  B       b1505   t1504  T       t1505   o563 b1504 b1505
 T       t1505   o1480 b626 b1486 b1505 b4  
3773  B       b1506   t1505  B       b1506   t1505
3774  P       p1506   String "assumT 9 ttca"  T       t1506   o563 b1503 b1506
3775  O       o1506   ext_rule p1506  B       b1507   t1506 b
3776  B       b1507   t1332  T       t1507   o561 b562 b1507
3777  B       b1508   t1333  B       b1508   t1507 a
3778  B       b1509   t1336  T       t1508   o561 b562 b1508
3779  T       t1509   o563 b1508 b1509  H       h1508   v t1508
3780  B       b1510   t1509  B       b1509   t1365
3781  T       t1510   o563 b1507 b1510  B       b1510   t1366
3782  B       b1511   t1510 b  B       b1511   t1367
3783  T       t1511   o561 b562 b1511  B       b1512   t1368
3784  B       b1512   t1511 a  T       t1512   o563 b1511 b1512
3785  T       t1512   o561 b562 b1512  B       b1513   t1512
3786  H       h1512   v t1512  T       t1513   o563 b1510 b1513
 S       s1512   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512  
 G       s1512   t1470  
 B       b1513   s1512  
 T       t1513   o629 b1513 b1364  
3787  B       b1514   t1513  B       b1514   t1513
3788  T       t1514   o2 b1477  T       t1514   o563 b1509 b1514
3789  B       b1515   t1514  B       b1515   t1514 f
3790  T       t1515   o628 b1514 b4 b1515  T       t1515   o561 b562 b1515
3791  B       b1516   t1515  B       b1516   t1515 e
3792  T       t1516   o b1516 b4  T       t1516   o561 b562 b1516
3793  B       b1517   t1516  H       h1516   v_2 t1516
3794  T       t1517   o627 b1477 b1517  S       s1516   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516
3795    G       s1516   t1465
3796    B       b1517   s1516
3797    T       t1517   o635 b1517 b1393
3798  B       b1518   t1517  B       b1518   t1517
3799  P       p1518   String "instHypT [<< 'a >>; << 'b >>] 17 ttca thenT dT 18 ttca thenT dT 18 ttca"  S       s1518   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508
3800  O       o1518   ext_rule p1518  G       s1518   t1465
 H       h1518   y_9 t1336  
 S       s1518   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518  
 G       s1518   t1470  
3801  B       b1519   s1518  B       b1519   s1518
3802  T       t1519   o629 b1519 b1364  T       t1519   o635 b1519 b1393
3803  B       b1520   t1519  B       b1520   t1519
3804  H       h1520   y_8 t1509  T       t1520   o2 b1468
3805  S       s1520   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1520 h1518  B       b1521   t1520
3806  G       s1520   t1470  T       t1521   o634 b1520 b4 b1521
 B       b1521   s1520  
 T       t1521   o629 b1521 b1364  
3807  B       b1522   t1521  B       b1522   t1521
3808  S       s1522   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1520  T       t1522   o2 b1522
3809  G       s1522   t1470  B       b1523   t1522
3810  B       b1523   s1522  T       t1523   o634 b1518 b4 b1523
 T       t1523   o629 b1523 b1364  
3811  B       b1524   t1523  B       b1524   t1523
3812  H       h1524   w_1 t1510  T       t1524   o b1524 b4
3813  S       s1524   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1524 h1520  B       b1525   t1524
3814  G       s1524   t1470  T       t1525   o633 b1468 b1525
 B       b1525   s1524  
 T       t1525   o629 b1525 b1364  
3815  B       b1526   t1525  B       b1526   t1525
3816  S       s1526   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1524  P       p1526   String "instHypT [<< 'a >>; << 'b >>] 13 ttca thenT dT 15 ttca thenT dT 15 ttca"
3817  G       s1526   t1470  O       o1526   ext_rule p1526
3818    H       h1526   y_6 t1359
3819    S       s1526   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526
3820    G       s1526   t1465
3821  B       b1527   s1526  B       b1527   s1526
3822  T       t1527   o629 b1527 b1364  T       t1527   o635 b1527 b1393
3823  B       b1528   t1527  B       b1528   t1527
3824  H       h1528   w t1511  H       h1528   y_5 t1505
3825  S       s1528   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1528 h1524  S       s1528   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1528 h1526
3826  G       s1528   t1470  G       s1528   t1465
3827  B       b1529   s1528  B       b1529   s1528
3828  T       t1529   o629 b1529 b1364  T       t1529   o635 b1529 b1393
3829  B       b1530   t1529  B       b1530   t1529
3830  S       s1530   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1528  S       s1530   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1528
3831  G       s1530   t1470  G       s1530   t1465
3832  B       b1531   s1530  B       b1531   s1530
3833  T       t1531   o629 b1531 b1364  T       t1531   o635 b1531 b1393
3834  B       b1532   t1531  B       b1532   t1531
3835  T       t1532   o b567 b4  H       h1532   w_1 t1506
3836  B       b1533   t1532  S       s1532   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1532 h1528
3837  T       t1533   o882 b1533  G       s1532   t1465
3838    B       b1533   s1532
3839    T       t1533   o635 b1533 b1393
3840  B       b1534   t1533  B       b1534   t1533
3841  T       t1534   o881 b1534  S       s1534   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1532
3842  B       b1535   t1534  G       s1534   t1465
3843  T       t1535   o b1535 b1003  B       b1535   s1534
3844    T       t1535   o635 b1535 b1393
3845  B       b1536   t1535  B       b1536   t1535
3846  T       t1536   o628 b1514 b1224 b1515  H       h1536   w t1507
3847  B       b1537   t1536  S       s1536   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1536 h1532
3848  T       t1537   o2 b1537  G       s1536   t1465
3849    B       b1537   s1536
3850    T       t1537   o635 b1537 b1393
3851  B       b1538   t1537  B       b1538   t1537
3852  T       t1538   o628 b1532 b1536 b1538  S       s1538   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1536
3853  B       b1539   t1538  G       s1538   t1465
3854  T       t1539   o2 b1539  B       b1539   s1538
3855    T       t1539   o635 b1539 b1393
3856  B       b1540   t1539  B       b1540   t1539
3857  T       t1540   o628 b1530 b1003 b1540  T       t1540   o b567 b4
3858  B       b1541   t1540  B       b1541   t1540
3859  T       t1541   o2 b1541  T       t1541   o887 b1541
3860  B       b1542   t1541  B       b1542   t1541
3861  T       t1542   o628 b1528 b4 b1542  T       t1542   o886 b1542
3862  B       b1543   t1542  B       b1543   t1542
3863  T       t1543   o2 b1543  T       t1543   o b1543 b997
3864  B       b1544   t1543  B       b1544   t1543
3865  T       t1544   o628 b1526 b4 b1544  T       t1544   o634 b1518 b1212 b1523
3866  B       b1545   t1544  B       b1545   t1544
3867  T       t1545   o2 b1545  T       t1545   o2 b1545
3868  B       b1546   t1545  B       b1546   t1545
3869  T       t1546   o628 b1524 b4 b1546  T       t1546   o634 b1540 b1544 b1546
3870  B       b1547   t1546  B       b1547   t1546
3871  T       t1547   o2 b1547  T       t1547   o2 b1547
3872  B       b1548   t1547  B       b1548   t1547
3873  T       t1548   o628 b1522 b4 b1548  T       t1548   o634 b1538 b997 b1548
3874  B       b1549   t1548  B       b1549   t1548
3875  T       t1549   o2 b1549  T       t1549   o2 b1549
3876  B       b1550   t1549  B       b1550   t1549
3877  T       t1550   o628 b1520 b4 b1550  T       t1550   o634 b1536 b4 b1550
3878  B       b1551   t1550  B       b1551   t1550
3879  T       t1551   o b1551 b4  T       t1551   o2 b1551
3880  B       b1552   t1551  B       b1552   t1551
3881  T       t1552   o627 b1516 b1552  T       t1552   o634 b1534 b4 b1552
3882  B       b1553   t1552  B       b1553   t1552
3883  P       p1553   String "instHypT [<< 'a >>; << 'b >>] 5 ttca thenT dT 19 ttca"  T       t1553   o2 b1553
3884  O       o1553   ext_rule p1553  B       b1554   t1553
3885  S       s1553   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518  T       t1554   o634 b1532 b4 b1554
 G       s1553   t1369  
 B       b1554   s1553  
 T       t1554   o629 b1554 b1364  
3886  B       b1555   t1554  B       b1555   t1554
3887  H       h1555   w_1 t1373  T       t1555   o2 b1555
3888  S       s1555   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1555  B       b1556   t1555
3889  G       s1555   t1369  T       t1556   o634 b1530 b4 b1556
 B       b1556   s1555  
 T       t1556   o629 b1556 b1364  
3890  B       b1557   t1556  B       b1557   t1556
3891  S       s1557   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1555  T       t1557   o2 b1557
3892  G       s1557   t1470  B       b1558   t1557
3893  B       b1558   s1557  T       t1558   o634 b1528 b4 b1558
 T       t1558   o629 b1558 b1364  
3894  B       b1559   t1558  B       b1559   t1558
3895  H       h1559   w t1374  T       t1559   o b1559 b4
3896  S       s1559   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1559 h1555  B       b1560   t1559
3897  G       s1559   t1470  T       t1560   o633 b1524 b1560
 B       b1560   s1559  
 T       t1560   o629 b1560 b1364  
3898  B       b1561   t1560  B       b1561   t1560
3899  S       s1561   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1559  P       p1561   String "instHypT [<< 'a >>; << 'b >>] 5 ttca thenT dT 16 ttca"
3900  G       s1561   t1470  O       o1561   ext_rule p1561
3901    S       s1561   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526
3902    G       s1561   t1398
3903  B       b1562   s1561  B       b1562   s1561
3904  T       t1562   o629 b1562 b1364  T       t1562   o635 b1562 b1393
3905  B       b1563   t1562  B       b1563   t1562
3906  T       t1563   o628 b1520 b1224 b1550  H       h1563   w_1 t1402
3907  B       b1564   t1563  S       s1563   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1563
3908  T       t1564   o2 b1564  G       s1563   t1398
3909    B       b1564   s1563
3910    T       t1564   o635 b1564 b1393
3911  B       b1565   t1564  B       b1565   t1564
3912  T       t1565   o628 b1563 b1536 b1565  S       s1565   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1563
3913  B       b1566   t1565  G       s1565   t1465
3914  T       t1566   o2 b1566  B       b1566   s1565
3915    T       t1566   o635 b1566 b1393
3916  B       b1567   t1566  B       b1567   t1566
3917  T       t1567   o628 b1561 b1003 b1567  H       h1567   w t1403
3918  B       b1568   t1567  S       s1567   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1567 h1563
3919  T       t1568   o2 b1568  G       s1567   t1465
3920    B       b1568   s1567
3921    T       t1568   o635 b1568 b1393
3922  B       b1569   t1568  B       b1569   t1568
3923  T       t1569   o628 b1559 b4 b1569  S       s1569   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1567
3924  B       b1570   t1569  G       s1569   t1465
3925  T       t1570   o2 b1570  B       b1570   s1569
3926    T       t1570   o635 b1570 b1393
3927  B       b1571   t1570  B       b1571   t1570
3928  T       t1571   o751 b1557 b4 b1571  T       t1571   o634 b1528 b1212 b1558
3929  B       b1572   t1571  B       b1572   t1571
3930  T       t1572   o2 b1572  T       t1572   o2 b1572
3931  B       b1573   t1572  B       b1573   t1572
3932  T       t1573   o751 b1555 b4 b1573  T       t1573   o634 b1571 b1544 b1573
3933  B       b1574   t1573  B       b1574   t1573
3934  H       h1574   y_8 t1372  T       t1574   o2 b1574
3935  S       s1574   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1574  B       b1575   t1574
3936  G       s1574   t1470  T       t1575   o634 b1569 b997 b1575
 B       b1575   s1574  
 T       t1575   o629 b1575 b1364  
3937  B       b1576   t1575  B       b1576   t1575
3938  S       s1576   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1555 h1574  T       t1576   o2 b1576
3939  G       s1576   t1470  B       b1577   t1576
3940  B       b1577   s1576  T       t1577   o634 b1567 b4 b1577
 T       t1577   o629 b1577 b1364  
3941  B       b1578   t1577  B       b1578   t1577
3942  T       t1578   o628 b1578 b4 b1571  T       t1578   o2 b1578
3943  B       b1579   t1578  B       b1579   t1578
3944  T       t1579   o2 b1579  T       t1579   o771 b1565 b4 b1579
3945  B       b1580   t1579  B       b1580   t1579
3946  T       t1580   o628 b1576 b4 b1580  T       t1580   o2 b1580
3947  B       b1581   t1580  B       b1581   t1580
3948  T       t1581   o b1581 b4  T       t1581   o771 b1563 b4 b1581
3949  B       b1582   t1581  B       b1582   t1581
3950  T       t1582   o b1574 b1582  H       h1582   y_5 t1401
3951  B       b1583   t1582  S       s1582   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1582
3952  T       t1583   o627 b1551 b1583  G       s1582   t1465
3953    B       b1583   s1582
3954    T       t1583   o635 b1583 b1393
3955  B       b1584   t1583  B       b1584   t1583
3956  P       p1584   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 15 ttca"  S       s1584   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1563 h1582
3957  O       o1584   ext_rule p1584  G       s1584   t1465
 T       t1584   o564 b565 b1329  
 H       h1584   v_1 t1584  
 S       s1584   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1584  
 G       s1584   t1369  
3958  B       b1585   s1584  B       b1585   s1584
3959  T       t1585   o629 b1585 b1364  T       t1585   o635 b1585 b1393
3960  B       b1586   t1585  B       b1586   t1585
3961  T       t1586   o2 b1574  T       t1586   o634 b1586 b4 b1579
3962  B       b1587   t1586  B       b1587   t1586
3963  T       t1587   o628 b1586 b4 b1587  T       t1587   o2 b1587
3964  B       b1588   t1587  B       b1588   t1587
3965  T       t1588   o b1588 b4  T       t1588   o634 b1584 b4 b1588
3966  B       b1589   t1588  B       b1589   t1588
3967  T       t1589   o627 b1574 b1589  T       t1589   o b1589 b4
3968  B       b1590   t1589  B       b1590   t1589
3969  P       p1590   String "rwh unfold_bisect 19 thenT dT 19 ttca"  T       t1590   o b1582 b1590
 O       o1590   ext_rule p1590  
 T       t1590   o627 b1588 b4  
3970  B       b1591   t1590  B       b1591   t1590
3971  T       t1591   o1590 b626 b1591 b4 b4  T       t1591   o633 b1559 b1591
3972  B       b1592   t1591  B       b1592   t1591
3973  T       t1592   o b1592 b4  P       p1592   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 11 ttca thenT rwh unfold_bisect 16 ttca thenT dT 16 ttca"
3974    O       o1592   ext_rule p1592
3975    T       t1592   o633 b1582 b4
3976  B       b1593   t1592  B       b1593   t1592
3977  T       t1593   o1584 b626 b1590 b1593 b4  T       t1593   o1592 b632 b1593 b4 b4
3978  B       b1594   t1593  B       b1594   t1593
3979  P       p1594   String "dT 19 ttca"  P       p1594   String "dT 16 ttca"
3980  O       o1594   ext_rule p1594  O       o1594   ext_rule p1594
3981  S       s1594   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518  S       s1594   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526
3982  G       s1594   t1370  G       s1594   t1399
3983  B       b1595   s1594  B       b1595   s1594
3984  T       t1595   o629 b1595 b1364  T       t1595   o635 b1595 b1393
3985  B       b1596   t1595  B       b1596   t1595
3986  S       s1596   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1574  S       s1596   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1582
3987  G       s1596   t1370  G       s1596   t1399
3988  B       b1597   s1596  B       b1597   s1596
3989  T       t1597   o629 b1597 b1364  T       t1597   o635 b1597 b1393
3990  B       b1598   t1597  B       b1598   t1597
3991  T       t1598   o2 b1581  T       t1598   o2 b1589
3992  B       b1599   t1598  B       b1599   t1598
3993  T       t1599   o751 b1598 b4 b1599  T       t1599   o771 b1598 b4 b1599
3994  B       b1600   t1599  B       b1600   t1599
3995  T       t1600   o2 b1600  T       t1600   o2 b1600
3996  B       b1601   t1600  B       b1601   t1600
3997  T       t1601   o751 b1596 b4 b1601  T       t1601   o771 b1596 b4 b1601
3998  B       b1602   t1601  B       b1602   t1601
3999  H       h1602   y_10 t1371  H       h1602   y_7 t1400
4000  S       s1602   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1602  S       s1602   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602
4001  G       s1602   t1470  G       s1602   t1465
4002  B       b1603   s1602  B       b1603   s1602
4003  T       t1603   o629 b1603 b1364  T       t1603   o635 b1603 b1393
4004  B       b1604   t1603  B       b1604   t1603
4005  S       s1604   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1574 h1602  S       s1604   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1582 h1602
4006  G       s1604   t1470  G       s1604   t1465
4007  B       b1605   s1604  B       b1605   s1604
4008  T       t1605   o629 b1605 b1364  T       t1605   o635 b1605 b1393
4009  B       b1606   t1605  B       b1606   t1605
4010  T       t1606   o628 b1606 b4 b1599  T       t1606   o634 b1606 b4 b1599
4011  B       b1607   t1606  B       b1607   t1606
4012  T       t1607   o2 b1607  T       t1607   o2 b1607
4013  B       b1608   t1607  B       b1608   t1607
4014  T       t1608   o628 b1604 b4 b1608  T       t1608   o634 b1604 b4 b1608
4015  B       b1609   t1608  B       b1609   t1608
4016  T       t1609   o b1609 b4  T       t1609   o b1609 b4
4017  B       b1610   t1609  B       b1610   t1609
4018  T       t1610   o b1602 b1610  T       t1610   o b1602 b1610
4019  B       b1611   t1610  B       b1611   t1610
4020  T       t1611   o627 b1581 b1611  T       t1611   o633 b1589 b1611
4021  B       b1612   t1611  B       b1612   t1611
4022  P       p1612   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 16 ttca"  P       p1612   String "setSubstT << equal{car{'h}; .\"isect\"{car{'h1}; car{'h2}}} >> 12 ttca thenT rwh unfold_bisect 16 ttca thenT dT 16 ttca"
4023  O       o1612   ext_rule p1612  O       o1612   ext_rule p1612
4024  T       t1612   o564 b567 b1329  T       t1612   o633 b1602 b4
4025  H       h1612   v_1 t1612  B       b1613   t1612
4026  S       s1612   t620 h h1367 h1368 h1369 h1375 h1378 h1379 h697 h1380 h1388 h1393 h1394 h651 h652 h1332 h1470 h1512 h1518 h1612  T       t1613   o1612 b632 b1613 b4 b4
 G       s1612   t1370  
 B       b1613   s1612  
 T       t1613   o629 b1613 b1364  
4027  B       b1614   t1613  B       b1614   t1613
4028  T       t1614   o2 b1602  P       p1614   String "instHypT [<< op{'h1; 'a; 'b} >>; << op{'g; 'a; 'b} >>] 14 ttca thenT rwh fold_isset 0 ttca thenT rwh unfold_equiv 15 thenT dT 17 ttca thenT rwh fold_equiv 15 ttca"
4029    O       o1614   ext_rule p1614
4030    T       t1614   o564 b571 b1348
4031  B       b1615   t1614  B       b1615   t1614
4032  T       t1615   o628 b1614 b4 b1615  T       t1615   o568 b1348 b1356 b1358 b571
4033  B       b1616   t1615  B       b1616   t1615
4034  T       t1616   o b1616 b4  T       t1616   o563 b1400 b1616
4035  B       b1617   t1616  B       b1617   t1616
4036  T       t1617   o627 b1602 b1617  T       t1617   o563 b1615 b1617
4037  B       b1618   t1617  H       h1617   y_5 t1617
4038  T       t1618   o627 b1616 b4  S       s1617   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602 h1617
4039    G       s1617   t1465
4040    B       b1618   s1617
4041    T       t1618   o635 b1618 b1393
4042  B       b1619   t1618  B       b1619   t1618
4043  T       t1619   o1590 b626 b1619 b4 b4  T       t1619   o781 b1348
4044  B       b1620   t1619  B       b1620   t1619
4045  T       t1620   o b1620 b4  T       t1620   o781 b1356
4046  B       b1621   t1620  B       b1621   t1620
4047  T       t1621   o1612 b626 b1618 b1621 b4  T       t1621   o781 b1357
4048  B       b1622   t1621  B       b1622   t1621
4049  P       p1622   String "eqSetTransT << op{'h1; 'a; 'b} >> thenT rwh unfold_equal 18 thenT rwh unfold_equal 19 thenT autoT"  T       t1622   o781 b1358
 O       o1622   ext_rule p1622  
 T       t1622   o627 b1609 b4  
4050  B       b1623   t1622  B       b1623   t1622
4051  T       t1623   o1622 b626 b1623 b4 b4  T       t1623   o556 b1622 b1623
4052  B       b1624   t1623  B       b1624   t1623
4053  T       t1624   o b1624 b4  T       t1624   o556 b1621 b1624
4054  B       b1625   t1624  B       b1625   t1624
4055  T       t1625   o b1622 b1625  T       t1625   o556 b1620 b1625
4056  B       b1626   t1625  B       b1626   t1625
4057  T       t1626   o1594 b626 b1612 b1626 b4  T       t1626   o564 b1357 b1348
4058  B       b1627   t1626  B       b1627   t1626
4059  T       t1627   o b1627 b4  T       t1627   o564 b1358 b1348
4060  B       b1628   t1627  B       b1628   t1627
4061  T       t1628   o b1594 b1628  T       t1628   o556 b1627 b1628
4062  B       b1629   t1628  B       b1629   t1628
4063  T       t1629   o1553 b626 b1584 b1629 b4  T       t1629   o556 b1626 b1629
4064  B       b1630   t1629  B       b1630   t1629
4065  T       t1630   o b1630 b4  T       t1630   o786 b1357 b1358
4066  B       b1631   t1630  B       b1631   t1630
4067  T       t1631   o1518 b626 b1553 b1631 b4  T       t1631   o564 b1631 b1356
4068  B       b1632   t1631  B       b1632   t1631
4069  T       t1632   o b1632 b4  T       t1632   o556 b1630 b1632
4070  B       b1633   t1632  H       h1632   y_6 t1632
4071  T       t1633   o1506 b626 b1518 b1633 b4  S       s1632   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1632 h1602 h1617
4072    G       s1632   t1465
4073    B       b1633   s1632
4074    T       t1633   o635 b1633 b1393
4075  B       b1634   t1633  B       b1634   t1633
4076  T       t1634   o b1634 b4  B       b1635   t1617
4077  B       b1635   t1634  T       t1635   o563 b1628 b1635
4078  T       t1635   o b1506 b1635  H       h1635   w_1 t1635
4079  B       b1636   t1635  S       s1635   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1632 h1602 h1635 h1617
4080  T       t1636   o1354 b626 b1480 b1636 b4  G       s1635   t1465
4081    B       b1636   s1635
4082    T       t1636   o635 b1636 b1393
4083  B       b1637   t1636  B       b1637   t1636
4084  T       t1637   o624 b1637  S       s1637   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1632 h1602 h1635
4085  B       b1638   t1637  G       s1637   t1465
4086  T       t1638   o1304 b1312 b1354 b1638 b4  B       b1638   s1637
4087    T       t1638   o635 b1638 b1393
4088  B       b1639   t1638  B       b1639   t1638
4089  T       t1639   o1303 b1639  S       s1639   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602 h1635
4090  B       b1640   t1639  G       s1639   t1465
4091  P       p1640   Number 3538  B       b1640   s1639
4092  P       p1641   Number 3611  T       t1640   o635 b1640 b1393
4093  O       o1641   location p1640 p1641  B       b1641   t1640
4094  NOcaml!str_let  str_let str_let Ocaml  T       t1641   o568 b1349 b1362 b1358 b761
4095  O       o1642   str_let p1640 p1641  B       b1642   t1641
4096  NOcaml!patt_var patt_var        patt_var Ocaml  T       t1642   o568 b1348 b1356 b1358 b761
4097  P       p1642   Number 3542  B       b1643   t1642
4098  O       o1643   patt_var p1642 p1641  T       t1643   o563 b1642 b1643
4099  NOcaml!patt_done        patt_done       patt_done Ocaml  B       b1644   t1643
4100  O       o1644   patt_done p1640 p1641  T       t1644   o563 b1510 b1644
4101  T       t1644   o1644  B       b1645   t1644
4102  B       b1644   t1644 subgroupIsectT  T       t1645   o563 b1628 b1645
4103  T       t1645   o1643 b1644  B       b1646   t1645 f
4104  B       b1645   t1645  T       t1646   o561 b562 b1646
4105  NOcaml!fun      fun     fun Ocaml  H       h1646   w t1646
4106  O       o1645   fun p1642 p1641  S       s1646   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602 h1646 h1635
4107  NOcaml!patt_if  patt_if patt_if Ocaml  G       s1646   t1465
4108  O       o1646   patt_if p1642 p1641  B       b1647   s1646
4109  P       p1646   Number 3557  T       t1647   o635 b1647 b1393
4110  P       p1647   Number 3559  B       b1648   t1647
4111  O       o1647   patt_var p1646 p1647  S       s1648   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602 h1646
4112  NOcaml!patt_body        patt_body       patt_body Ocaml  G       s1648   t1465
4113  O       o1648   patt_body p1642 p1641  B       b1649   s1648
4114  P       p1648   Number 3560  T       t1649   o635 b1649 b1393
4115  P       p1649   Number 3562  B       b1650   t1649
4116  O       o1649   patt_var p1648 p1649  T       t1650   o b571 b4
4117  P       p1650   Number 3563  B       b1651   t1650
4118  P       p1651   Number 3564  T       t1651   o887 b1651
4119  O       o1651   patt_var p1650 p1651  B       b1652   t1651
4120  NOcaml!apply    apply   apply Ocaml  T       t1652   o886 b1652
4121  P       p1652   Number 3570  B       b1653   t1652
4122  O       o1652   apply p1652 p1641  T       t1653   o b1653 b997
4123  P       p1653   Number 3609  B       b1654   t1653
4124  O       o1653   apply p1652 p1653  T       t1654   o b1358 b4
4125  P       p1654   Number 3606  B       b1655   t1654
4126  O       o1654   apply p1652 p1654  T       t1655   o887 b1655
4127  P       p1655   Number 3603  B       b1656   t1655
4128  O       o1655   apply p1652 p1655  T       t1656   o886 b1656
4129  NOcaml!lid      lid     lid Ocaml  B       b1657   t1656
4130  P       p1656   Number 3584  T       t1657   o b1657 b997
4131  O       o1656   lid p1652 p1656  B       b1658   t1657
4132  O       o1657   lid p1304  T       t1658   o634 b1604 b1658 b1608
4133  T       t1657   o1657  B       b1659   t1658
4134  B       b1657   t1657  T       t1659   o2 b1659
4135  T       t1658   o1656 b1657  B       b1660   t1659
4136  B       b1658   t1658  T       t1660   o634 b1650 b1654 b1660
4137  P       p1658   Number 3586  B       b1661   t1660
4138  P       p1659   Number 3602  T       t1661   o2 b1661
4139  O       o1659   apply p1658 p1659  B       b1662   t1661
4140  P       p1660   Number 3600  T       t1662   o634 b1648 b997 b1662
4141  O       o1660   lid p1658 p1660  B       b1663   t1662
4142  P       p1661   String hyp_count_addr  T       t1663   o2 b1663
4143  O       o1661   lid p1661  B       b1664   t1663
4144  T       t1661   o1661  T       t1664   o634 b1641 b4 b1664
4145  B       b1661   t1661  B       b1665   t1664
4146  T       t1662   o1660 b1661  T       t1665   o2 b1665
4147  B       b1662   t1662  B       b1666   t1665
4148  P       p1662   Number 3601  T       t1666   o634 b1639 b4 b1666
4149  O       o1662   lid p1662 p1659  B       b1667   t1666
4150  P       p1663   Var p  T       t1667   o2 b1667
4151  O       o1663   var p1663  B       b1668   t1667
4152  T       t1663   o1663  T       t1668   o634 b1637 b4 b1668
4153  B       b1663   t1663  B       b1669   t1668
4154  T       t1664   o1662 b1663  T       t1669   o2 b1669
4155  B       b1664   t1664  B       b1670   t1669
4156  T       t1665   o1659 b1662 b1664  T       t1670   o634 b1634 b4 b1670
4157  B       b1665   t1665  B       b1671   t1670
4158  T       t1666   o1655 b1658 b1665  T       t1671   o2 b1671
4159  B       b1666   t1666  B       b1672   t1671
4160  P       p1666   Number 3604  T       t1672   o634 b1619 b4 b1672
4161  O       o1666   lid p1666 p1654  B       b1673   t1672
4162  P       p1667   Var t1  T       t1673   o b1673 b4
4163  O       o1667   var p1667  B       b1674   t1673
4164  T       t1667   o1667  T       t1674   o633 b1609 b1674
4165  B       b1667   t1667  B       b1675   t1674
4166  T       t1668   o1666 b1667  P       p1675   String "dT 17 ttca"
4167  B       b1668   t1668  O       o1675   ext_rule p1675
4168  T       t1669   o1654 b1666 b1668  S       s1675   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602
4169  B       b1669   t1669  G       s1675   t1614
4170  P       p1669   Number 3607  B       b1676   s1675
4171  O       o1669   lid p1669 p1653  T       t1676   o635 b1676 b1393
4172  P       p1670   Var t2  B       b1677   t1676
4173  O       o1670   var p1670  S       s1677   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602 h1617
4174  T       t1670   o1670  G       s1677   t1614
4175  B       b1670   t1670  B       b1678   s1677
4176  T       t1671   o1669 b1670  T       t1678   o635 b1678 b1393
4177  B       b1671   t1671  B       b1679   t1678
4178  T       t1672   o1653 b1669 b1671  T       t1679   o2 b1673
4179  B       b1672   t1672  B       b1680   t1679
4180  P       p1672   Number 3610  T       t1680   o771 b1679 b4 b1680
4181  O       o1672   lid p1672 p1641  B       b1681   t1680
4182  T       t1673   o1672 b1663  T       t1681   o2 b1681
4183  B       b1673   t1673  B       b1682   t1681
4184  T       t1674   o1652 b1672 b1673  T       t1682   o771 b1677 b4 b1682
4185  B       b1674   t1674  B       b1683   t1682
4186  T       t1675   o1648 b1674  H       h1683   y_8 t1616
4187  B       b1675   t1675 p  S       s1683   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602 h1683
4188  T       t1676   o1651 b1675  G       s1683   t1465
4189  B       b1676   t1676  B       b1684   s1683
4190  T       t1677   o1646 b1676  T       t1684   o635 b1684 b1393
4191  B       b1677   t1677  B       b1685   t1684
4192  T       t1678   o1645 b1677  S       s1685   t626 h h1396 h716 h1397 h1404 h1408 h1413 h1414 h658 h659 h1354 h1355 h1508 h1516 h1526 h1602 h1617 h1683
4193  B       b1678   t1678  G       s1685   t1465
4194  T       t1679   o1648 b1678  B       b1686   s1685
4195  B       b1679   t1679 t2  T       t1686   o635 b1686 b1393
4196  T       t1680   o1649 b1679  B       b1687   t1686
4197  B       b1680   t1680  T       t1687   o634 b1687 b4 b1680
4198  T       t1681   o1646 b1680  B       b1688   t1687
4199  B       b1681   t1681  T       t1688   o2 b1688
4200  T       t1682   o1645 b1681  B       b1689   t1688
4201  B       b1682   t1682  T       t1689   o634 b1685 b4 b1689