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

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

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

revision 3404 by xiny, Sun Sep 23 07:25:28 2001 UTC revision 3405 by xiny, Sun Sep 23 07:33:50 2001 UTC
# Line 1478  Line 1478 
1478  T       t576    o570 b575  T       t576    o570 b575
1479  B       b576    t576  B       b576    t576
1480  P       p576    Number 664  P       p576    Number 664
1481  P       p577    Number 713  P       p577    Number 712
1482  O       o577    location p576 p577  O       o577    location p576 p577
1483  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
1484  P       p578    String car_df  P       p578    String car_df
# Line 1505  Line 1505 
1505  B       b584    t584  B       b584    t584
1506  T       t585    o577 b584  T       t585    o577 b584
1507  B       b585    t585  B       b585    t585
1508  P       p585    Number 715  P       p585    Number 714
1509  P       p586    Number 762  P       p586    Number 760
1510  O       o586    location p585 p586  O       o586    location p585 p586
1511  P       p587    String id_df  P       p587    String id_df
1512  O       o587    dform p587  O       o587    dform p587
# Line 1522  Line 1522 
1522  B       b591    t591  B       b591    t591
1523  T       t592    o586 b591  T       t592    o586 b591
1524  B       b592    t592  B       b592    t592
1525  P       p592    Number 765  P       p592    Number 762
1526  P       p593    Number 866  P       p593    Number 862
1527  O       o593    location p592 p593  O       o593    location p592 p593
1528  P       p594    String op_df  P       p594    String op_df
1529  O       o594    dform p594  O       o594    dform p594
# Line 1558  Line 1558 
1558  B       b605    t605  B       b605    t605
1559  T       t606    o593 b605  T       t606    o593 b605
1560  B       b606    t606  B       b606    t606
1561  P       p606    Number 868  P       p606    Number 864
1562  P       p607    Number 946  P       p607    Number 941
1563  O       o607    location p606 p607  O       o607    location p606 p607
1564  P       p608    String inv_df  P       p608    String inv_df
1565  O       o608    dform p608  O       o608    dform p608
# Line 1579  Line 1579 
1579  B       b613    t613  B       b613    t613
1580  T       t614    o607 b613  T       t614    o607 b613
1581  B       b614    t614  B       b614    t614
1582  P       p614    Number 961  P       p614    Number 956
1583  P       p615    Number 1037  P       p615    Number 1032
1584  O       o615    location p614 p615  O       o615    location p614 p615
1585  NSummary!rule   rule    rule Summary  NSummary!rule   rule    rule Summary
1586  P       p616    String car_wf  P       p616    String car_wf
# Line 1614  Line 1614 
1614  T       t623    o622  T       t623    o622
1615  B       b623    t623  B       b623    t623
1616  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
1617  P       p623    Number 983  P       p623    Number 978
1618  P       p624    Number 990  P       p624    Number 985
1619  O       o624    resource_defs p623 p624 p264  O       o624    resource_defs p623 p624 p264
1620  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
1621  P       p625    Number 988  P       p625    Number 983
1622  O       o625    uid p625 p624  O       o625    uid p625 p624
1623  P       p626    String []  P       p626    String []
1624  O       o626    uid p626  O       o626    uid p626
# Line 1636  Line 1636 
1636  B       b631    t631  B       b631    t631
1637  T       t632    o615 b631  T       t632    o615 b631
1638  B       b632    t632  B       b632    t632
1639  P       p632    Number 1039  P       p632    Number 1034
1640  P       p633    Number 1214  P       p633    Number 1209
1641  O       o633    location p632 p633  O       o633    location p632 p633
1642  P       p634    String op_wf1  P       p634    String op_wf1
1643  O       o634    rule p634  O       o634    rule p634
# Line 1671  Line 1671 
1671  B       b644    t644  B       b644    t644
1672  T       t645    o635 b639 b644  T       t645    o635 b639 b644
1673  B       b645    t645  B       b645    t645
1674  P       p645    Number 1061  P       p645    Number 1056
1675  P       p646    Number 1068  P       p646    Number 1063
1676  O       o646    resource_defs p645 p646 p264  O       o646    resource_defs p645 p646 p264
1677  P       p647    Number 1066  P       p647    Number 1061
1678  O       o647    uid p647 p646  O       o647    uid p647 p646
1679  T       t647    o647 b626  T       t647    o647 b626
1680  B       b647    t647  B       b647    t647
# Line 1688  Line 1688 
1688  B       b651    t651  B       b651    t651
1689  T       t652    o633 b651  T       t652    o633 b651
1690  B       b652    t652  B       b652    t652
1691  P       p652    Number 1216  P       p652    Number 1211
1692  P       p653    Number 1486  P       p653    Number 1481
1693  O       o653    location p652 p653  O       o653    location p652 p653
1694  P       p654    String op_wf2  P       p654    String op_wf2
1695  O       o654    rule p654  O       o654    rule p654
# Line 1722  Line 1722 
1722  B       b663    t663  B       b663    t663
1723  T       t664    o635 b639 b663  T       t664    o635 b639 b663
1724  B       b664    t664  B       b664    t664
1725  P       p664    Number 1238  P       p664    Number 1233
1726  P       p665    Number 1245  P       p665    Number 1240
1727  O       o665    resource_defs p664 p665 p264  O       o665    resource_defs p664 p665 p264
1728  P       p666    Number 1243  P       p666    Number 1238
1729  O       o666    uid p666 p665  O       o666    uid p666 p665
1730  T       t666    o666 b626  T       t666    o666 b626
1731  B       b666    t666  B       b666    t666
# Line 1739  Line 1739 
1739  B       b670    t670  B       b670    t670
1740  T       t671    o653 b670  T       t671    o653 b670
1741  B       b671    t671  B       b671    t671
1742  P       p671    Number 1488  P       p671    Number 1483
1743  P       p672    Number 1766  P       p672    Number 1760
1744  O       o672    location p671 p672  O       o672    location p671 p672
1745  P       p673    String op_eq1  P       p673    String op_eq1
1746  O       o673    rule p673  O       o673    rule p673
# Line 1781  Line 1781 
1781  B       b685    t685  B       b685    t685
1782  T       t686    o635 b639 b685  T       t686    o635 b639 b685
1783  B       b686    t686  B       b686    t686
1784  P       p686    Number 1510  P       p686    Number 1505
1785  P       p687    Number 1517  P       p687    Number 1512
1786  O       o687    resource_defs p686 p687 p264  O       o687    resource_defs p686 p687 p264
1787  P       p688    Number 1515  P       p688    Number 1510
1788  O       o688    uid p688 p687  O       o688    uid p688 p687
1789  T       t688    o688 b626  T       t688    o688 b626
1790  B       b688    t688  B       b688    t688
# Line 1798  Line 1798 
1798  B       b692    t692  B       b692    t692
1799  T       t693    o672 b692  T       t693    o672 b692
1800  B       b693    t693  B       b693    t693
1801  P       p693    Number 1768  P       p693    Number 1762
1802  P       p694    Number 2046  P       p694    Number 2039
1803  O       o694    location p693 p694  O       o694    location p693 p694
1804  P       p695    String op_eq2  P       p695    String op_eq2
1805  O       o695    rule p695  O       o695    rule p695
# Line 1821  Line 1821 
1821  B       b701    t701  B       b701    t701
1822  T       t702    o635 b639 b701  T       t702    o635 b639 b701
1823  B       b702    t702  B       b702    t702
1824  P       p702    Number 1790  P       p702    Number 1784
1825  P       p703    Number 1797  P       p703    Number 1791
1826  O       o703    resource_defs p702 p703 p264  O       o703    resource_defs p702 p703 p264
1827  P       p704    Number 1795  P       p704    Number 1789
1828  O       o704    uid p704 p703  O       o704    uid p704 p703
1829  T       t704    o704 b626  T       t704    o704 b626
1830  B       b704    t704  B       b704    t704
# Line 1838  Line 1838 
1838  B       b708    t708  B       b708    t708
1839  T       t709    o694 b708  T       t709    o694 b708
1840  B       b709    t709  B       b709    t709
1841  P       p709    Number 2048  P       p709    Number 2041
1842  P       p710    Number 2181  O       o709    location p709 p334
1843  O       o710    location p709 p710  P       p710    String op_fun1
1844  P       p711    String op_fun1  O       o710    rule p710
1845  O       o711    rule p711  T       t710    o620 b573
1846  T       t711    o620 b573  S       s710    t637 h
1847  S       s711    t637 h  G       s710    t710
1848  G       s711    t711  B       b710    s710
1849  B       b711    s711  T       t711    o618 b710
1850  T       t712    o618 b711  B       b711    t711
 B       b712    t712  
1851  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq  NCzf_itt_eq!fun_set     fun_set fun_set Czf_itt_eq
1852  O       o712    fun_set  O       o711    fun_set
1853  P       p712    Var z  P       p711    Var z
1854  O       o713    var p712  O       o712    var p711
1855  T       t713    o713  T       t712    o712
1856  B       b713    t713  B       b712    t712
1857  T       t714    o559 b713 b573  T       t713    o559 b712 b573
1858  B       b714    t714 z  B       b713    t713 z
1859  T       t715    o712 b714  T       t714    o711 b713
1860  S       s715    t620 h  S       s714    t620 h
1861  G       s715    t715  G       s714    t714
1862  B       b715    s715  B       b714    s714
1863  T       t716    o618 b715  T       t715    o618 b714
1864    B       b715    t715
1865    T       t716    o635 b711 b715
1866  B       b716    t716  B       b716    t716
1867  T       t717    o635 b712 b716  P       p716    Number 2064
 B       b717    t717  
1868  P       p717    Number 2071  P       p717    Number 2071
1869  P       p718    Number 2078  O       o717    resource_defs p716 p717 p264
1870  O       o718    resource_defs p717 p718 p264  P       p718    Number 2069
1871  P       p719    Number 2076  O       o718    uid p718 p717
1872  O       o719    uid p719 p718  T       t718    o718 b626
1873  T       t719    o719 b626  B       b718    t718
1874    T       t719    o b718 b4
1875  B       b719    t719  B       b719    t719
1876  T       t720    o b719 b4  T       t720    o717 b719
1877  B       b720    t720  B       b720    t720
1878  T       t721    o718 b720  T       t721    o b720 b4
1879  B       b721    t721  B       b721    t721
1880  T       t722    o b721 b4  T       t722    o710 b618 b716 b623 b721
1881  B       b722    t722  B       b722    t722
1882  T       t723    o711 b618 b717 b623 b722  T       t723    o709 b722
1883  B       b723    t723  B       b723    t723
1884  T       t724    o710 b723  P       p723    Number 2176
1885  B       b724    t724  P       p724    Number 2309
1886  P       p724    Number 2183  O       o724    location p723 p724
1887  P       p725    Number 2316  P       p725    String op_fun2
1888  O       o725    location p724 p725  O       o725    rule p725
1889  P       p726    String op_fun2  T       t725    o559 b573 b712
1890  O       o726    rule p726  B       b725    t725 z
1891  T       t726    o559 b573 b713  T       t726    o711 b725
1892  B       b726    t726 z  S       s726    t620 h
1893  T       t727    o712 b726  G       s726    t726
1894  S       s727    t620 h  B       b726    s726
1895  G       s727    t727  T       t727    o618 b726
1896  B       b727    s727  B       b727    t727
1897  T       t728    o618 b727  T       t728    o635 b711 b727
1898  B       b728    t728  B       b728    t728
1899  T       t729    o635 b712 b728  P       p728    Number 2199
 B       b729    t729  
1900  P       p729    Number 2206  P       p729    Number 2206
1901  P       p730    Number 2213  O       o729    resource_defs p728 p729 p264
1902  O       o730    resource_defs p729 p730 p264  P       p730    Number 2204
1903  P       p731    Number 2211  O       o730    uid p730 p729
1904  O       o731    uid p731 p730  T       t730    o730 b626
1905  T       t731    o731 b626  B       b730    t730
1906    T       t731    o b730 b4
1907  B       b731    t731  B       b731    t731
1908  T       t732    o b731 b4  T       t732    o729 b731
1909  B       b732    t732  B       b732    t732
1910  T       t733    o730 b732  T       t733    o b732 b4
1911  B       b733    t733  B       b733    t733
1912  T       t734    o b733 b4  T       t734    o725 b618 b728 b623 b733
1913  B       b734    t734  B       b734    t734
1914  T       t735    o726 b618 b729 b623 b734  T       t735    o724 b734
1915  B       b735    t735  B       b735    t735
1916  T       t736    o725 b735  P       p735    Number 2499
1917  B       b736    t736  P       p736    Number 2892
1918  P       p736    Number 2506  O       o736    location p735 p736
1919  P       p737    Number 2899  P       p737    String op_assoc1
1920  O       o737    location p736 p737  O       o737    rule p737
1921  P       p738    String op_assoc1  T       t737    o655 b674 b554
1922  O       o738    rule p738  S       s737    t620 h
1923  T       t738    o655 b674 b554  G       s737    t737
1924  S       s738    t620 h  B       b737    s737
1925  G       s738    t738  T       t738    o618 b737
1926  B       b738    s738  B       b738    t738
 T       t739    o618 b738  
 B       b739    t739  
1927  NCzf_itt_eq!equal       equal   equal Czf_itt_eq  NCzf_itt_eq!equal       equal   equal Czf_itt_eq
1928  O       o739    equal  O       o738    equal
1929  T       t740    o559 b562 b674  T       t739    o559 b562 b674
1930    B       b739    t739
1931    T       t740    o559 b560 b696
1932  B       b740    t740  B       b740    t740
1933  T       t741    o559 b560 b696  T       t741    o738 b739 b740
1934  B       b741    t741  S       s741    t620 h
1935  T       t742    o739 b740 b741  G       s741    t741
1936  S       s742    t620 h  B       b741    s741
1937  G       s742    t742  T       t742    o618 b741
1938  B       b742    s742  B       b742    t742
1939  T       t743    o618 b742  T       t743    o635 b738 b742
1940  B       b743    t743  B       b743    t743
1941  T       t744    o635 b739 b743  T       t744    o635 b658 b743
1942  B       b744    t744  B       b744    t744
1943  T       t745    o635 b658 b744  T       t745    o635 b656 b744
1944  B       b745    t745  B       b745    t745
1945  T       t746    o635 b656 b745  T       t746    o635 b676 b745
1946  B       b746    t746  B       b746    t746
1947  T       t747    o635 b676 b746  T       t747    o635 b641 b746
1948  B       b747    t747  B       b747    t747
1949  T       t748    o635 b641 b747  T       t748    o635 b639 b747
1950  B       b748    t748  B       b748    t748
1951  T       t749    o635 b639 b748  P       p748    Number 2524
 B       b749    t749  
1952  P       p749    Number 2531  P       p749    Number 2531
1953  P       p750    Number 2538  O       o749    resource_defs p748 p749 p264
1954  O       o750    resource_defs p749 p750 p264  P       p750    Number 2529
1955  P       p751    Number 2536  O       o750    uid p750 p749
1956  O       o751    uid p751 p750  T       t750    o750 b626
1957  T       t751    o751 b626  B       b750    t750
1958    T       t751    o b750 b4
1959  B       b751    t751  B       b751    t751
1960  T       t752    o b751 b4  T       t752    o749 b751
1961  B       b752    t752  B       b752    t752
1962  T       t753    o750 b752  T       t753    o b752 b4
1963  B       b753    t753  B       b753    t753
1964  T       t754    o b753 b4  T       t754    o737 b618 b748 b623 b753
1965  B       b754    t754  B       b754    t754
1966  T       t755    o738 b618 b749 b623 b754  T       t755    o736 b754
1967  B       b755    t755  B       b755    t755
1968  T       t756    o737 b755  P       p755    Number 2965
1969  B       b756    t756  P       p756    Number 3358
1970  P       p756    Number 2972  O       o756    location p755 p756
1971  P       p757    Number 3365  P       p757    String op_assoc2
1972  O       o757    location p756 p757  O       o757    rule p757
1973  P       p758    String op_assoc2  T       t757    o738 b740 b739
1974  O       o758    rule p758  S       s757    t620 h
1975  T       t758    o739 b741 b740  G       s757    t757
1976  S       s758    t620 h  B       b757    s757
1977  G       s758    t758  T       t758    o618 b757
1978  B       b758    s758  B       b758    t758
1979  T       t759    o618 b758  T       t759    o635 b738 b758
1980  B       b759    t759  B       b759    t759
1981  T       t760    o635 b739 b759  T       t760    o635 b658 b759
1982  B       b760    t760  B       b760    t760
1983  T       t761    o635 b658 b760  T       t761    o635 b656 b760
1984  B       b761    t761  B       b761    t761
1985  T       t762    o635 b656 b761  T       t762    o635 b676 b761
1986  B       b762    t762  B       b762    t762
1987  T       t763    o635 b676 b762  T       t763    o635 b641 b762
1988  B       b763    t763  B       b763    t763
1989  T       t764    o635 b641 b763  T       t764    o635 b639 b763
1990  B       b764    t764  B       b764    t764
1991  T       t765    o635 b639 b764  P       p764    Number 2990
 B       b765    t765  
1992  P       p765    Number 2997  P       p765    Number 2997
1993  P       p766    Number 3004  O       o765    resource_defs p764 p765 p264
1994  O       o766    resource_defs p765 p766 p264  P       p766    Number 2995
1995  P       p767    Number 3002  O       o766    uid p766 p765
1996  O       o767    uid p767 p766  T       t766    o766 b626
1997  T       t767    o767 b626  B       b766    t766
1998    T       t767    o b766 b4
1999  B       b767    t767  B       b767    t767
2000  T       t768    o b767 b4  T       t768    o765 b767
2001  B       b768    t768  B       b768    t768
2002  T       t769    o766 b768  T       t769    o b768 b4
2003  B       b769    t769  B       b769    t769
2004  T       t770    o b769 b4  T       t770    o757 b618 b764 b623 b769
2005  B       b770    t770  B       b770    t770
2006  T       t771    o758 b618 b765 b623 b770  T       t771    o756 b770
2007  B       b771    t771  B       b771    t771
2008  T       t772    o757 b771  P       p771    Number 3431
2009  B       b772    t772  P       p772    Number 3507
2010  P       p772    Number 3438  O       o772    location p771 p772
2011  P       p773    Number 3514  P       p773    String id_wf1
2012  O       o773    location p772 p773  O       o773    rule p773
2013  P       p774    String id_wf1  T       t773    o620 b567
2014  O       o774    rule p774  S       s773    t620 h
2015  T       t774    o620 b567  G       s773    t773
2016  S       s774    t620 h  B       b773    s773
2017  G       s774    t774  T       t774    o618 b773
2018  B       b774    s774  B       b774    t774
2019  T       t775    o618 b774  P       p774    Number 3453
2020  B       b775    t775  P       p775    Number 3461
2021  P       p775    Number 3460  O       o775    resource_defs p774 p775 p264
2022  P       p776    Number 3468  P       p776    Number 3459
2023  O       o776    resource_defs p775 p776 p264  O       o776    uid p776 p775
2024  P       p777    Number 3466  T       t776    o776 b626
2025  O       o777    uid p777 p776  B       b776    t776
2026  T       t777    o777 b626  T       t777    o b776 b4
2027  B       b777    t777  B       b777    t777
2028  T       t778    o b777 b4  T       t778    o775 b777
2029  B       b778    t778  B       b778    t778
2030  T       t779    o776 b778  T       t779    o b778 b4
2031  B       b779    t779  B       b779    t779
2032  T       t780    o b779 b4  T       t780    o773 b618 b774 b623 b779
2033  B       b780    t780  B       b780    t780
2034  T       t781    o774 b618 b775 b623 b780  T       t781    o772 b780
2035  B       b781    t781  B       b781    t781
2036  T       t782    o773 b781  P       p781    Number 3509
2037  B       b782    t782  P       p782    Number 3587
2038  P       p782    Number 3517  O       o782    location p781 p782
2039  P       p783    Number 3595  P       p783    String id_wf2
2040  O       o783    location p782 p783  O       o783    rule p783
2041  P       p784    String id_wf2  T       t783    o655 b567 b554
2042  O       o784    rule p784  S       s783    t620 h
2043  T       t784    o655 b567 b554  G       s783    t783
2044  S       s784    t620 h  B       b783    s783
2045  G       s784    t784  T       t784    o618 b783
2046  B       b784    s784  B       b784    t784
2047  T       t785    o618 b784  P       p784    Number 3531
2048  B       b785    t785  P       p785    Number 3538
2049  P       p785    Number 3539  O       o785    resource_defs p784 p785 p264
2050  P       p786    Number 3546  P       p786    Number 3536
2051  O       o786    resource_defs p785 p786 p264  O       o786    uid p786 p785
2052  P       p787    Number 3544  T       t786    o786 b626
2053  O       o787    uid p787 p786  B       b786    t786
2054  T       t787    o787 b626  T       t787    o b786 b4
2055  B       b787    t787  B       b787    t787
2056  T       t788    o b787 b4  T       t788    o785 b787
2057  B       b788    t788  B       b788    t788
2058  T       t789    o786 b788  T       t789    o b788 b4
2059  B       b789    t789  B       b789    t789
2060  T       t790    o b789 b4  T       t790    o783 b618 b784 b623 b789
2061  B       b790    t790  B       b790    t790
2062  T       t791    o784 b618 b785 b623 b790  T       t791    o782 b790
2063  B       b791    t791  B       b791    t791
2064  T       t792    o783 b791  P       p791    Number 3675
2065  B       b792    t792  P       p792    Number 3851
2066  P       p792    Number 3684  O       o792    location p791 p792
2067  P       p793    Number 3860  P       p793    String id_eq1
2068  O       o793    location p792 p793  O       o793    rule p793
2069  P       p794    String id_eq1  T       t793    o655 b573 b554
2070  O       o794    rule p794  S       s793    t620 h
2071  T       t794    o655 b573 b554  G       s793    t793
2072  S       s794    t620 h  B       b793    s793
2073  G       s794    t794  T       t794    o618 b793
2074  B       b794    s794  B       b794    t794
2075  T       t795    o618 b794  T       t795    o559 b567 b573
2076  B       b795    t795  B       b795    t795
2077  T       t796    o559 b567 b573  T       t796    o738 b795 b573
2078  B       b796    t796  S       s796    t620 h
2079  T       t797    o739 b796 b573  G       s796    t796
2080  S       s797    t620 h  B       b796    s796
2081  G       s797    t797  T       t797    o618 b796
2082  B       b797    s797  B       b797    t797
2083  T       t798    o618 b797  T       t798    o635 b794 b797
2084  B       b798    t798  B       b798    t798
2085  T       t799    o635 b795 b798  T       t799    o635 b711 b798
2086  B       b799    t799  B       b799    t799
2087  T       t800    o635 b712 b799  P       p799    Number 3697
2088  B       b800    t800  P       p800    Number 3704
2089  P       p800    Number 3706  O       o800    resource_defs p799 p800 p264
2090  P       p801    Number 3713  P       p801    Number 3702
2091  O       o801    resource_defs p800 p801 p264  O       o801    uid p801 p800
2092  P       p802    Number 3711  T       t801    o801 b626
2093  O       o802    uid p802 p801  B       b801    t801
2094  T       t802    o802 b626  T       t802    o b801 b4
2095  B       b802    t802  B       b802    t802
2096  T       t803    o b802 b4  T       t803    o800 b802
2097  B       b803    t803  B       b803    t803
2098  T       t804    o801 b803  T       t804    o b803 b4
2099  B       b804    t804  B       b804    t804
2100  T       t805    o b804 b4  T       t805    o793 b618 b799 b623 b804
2101  B       b805    t805  B       b805    t805
2102  T       t806    o794 b618 b800 b623 b805  T       t806    o792 b805
2103  B       b806    t806  B       b806    t806
2104  T       t807    o793 b806  P       p806    Number 3853
2105  B       b807    t807  P       p807    Number 4029
2106  P       p807    Number 3862  O       o807    location p806 p807
2107  P       p808    Number 4038  P       p808    String id_eq2
2108  O       o808    location p807 p808  O       o808    rule p808
2109  P       p809    String id_eq2  T       t808    o559 b573 b567
2110  O       o809    rule p809  B       b808    t808
2111  T       t809    o559 b573 b567  T       t809    o738 b808 b573
2112  B       b809    t809  S       s809    t620 h
2113  T       t810    o739 b809 b573  G       s809    t809
2114  S       s810    t620 h  B       b809    s809
2115  G       s810    t810  T       t810    o618 b809
2116  B       b810    s810  B       b810    t810
2117  T       t811    o618 b810  T       t811    o635 b794 b810
2118  B       b811    t811  B       b811    t811
2119  T       t812    o635 b795 b811  T       t812    o635 b711 b811
2120  B       b812    t812  B       b812    t812
2121  T       t813    o635 b712 b812  P       p812    Number 3875
2122  B       b813    t813  P       p813    Number 3882
2123  P       p813    Number 3884  O       o813    resource_defs p812 p813 p264
2124  P       p814    Number 3891  P       p814    Number 3880
2125  O       o814    resource_defs p813 p814 p264  O       o814    uid p814 p813
2126  P       p815    Number 3889  T       t814    o814 b626
2127  O       o815    uid p815 p814  B       b814    t814
2128  T       t815    o815 b626  T       t815    o b814 b4
2129  B       b815    t815  B       b815    t815
2130  T       t816    o b815 b4  T       t816    o813 b815
2131  B       b816    t816  B       b816    t816
2132  T       t817    o814 b816  T       t817    o b816 b4
2133  B       b817    t817  B       b817    t817
2134  T       t818    o b817 b4  T       t818    o808 b618 b812 b623 b817
2135  B       b818    t818  B       b818    t818
2136  T       t819    o809 b618 b813 b623 b818  T       t819    o807 b818
2137  B       b819    t819  B       b819    t819
2138  T       t820    o808 b819  P       p819    Number 4031
2139  B       b820    t820  P       p820    Number 4088
2140  P       p820    Number 4040  O       o820    location p819 p820
 P       p821    Number 4097  
 O       o821    location p820 p821  
2141  NOcaml!str_let  str_let str_let Ocaml  NOcaml!str_let  str_let str_let Ocaml
2142  O       o822    str_let p820 p821  O       o821    str_let p819 p820
2143  NOcaml!patt_var patt_var        patt_var Ocaml  NOcaml!patt_var patt_var        patt_var Ocaml
2144  P       p822    Number 4044  P       p821    Number 4035
2145  O       o823    patt_var p822 p821  O       o822    patt_var p821 p820
2146  NOcaml!patt_done        patt_done       patt_done Ocaml  NOcaml!patt_done        patt_done       patt_done Ocaml
2147  O       o824    patt_done p820 p821  O       o823    patt_done p819 p820
2148  T       t824    o824  T       t823    o823
2149  B       b824    t824 id_elim2T  B       b823    t823 id_elim2T
2150  T       t825    o823 b824  T       t824    o822 b823
2151  B       b825    t825  B       b824    t824
2152  NOcaml!fun      fun     fun Ocaml  NOcaml!fun      fun     fun Ocaml
2153  O       o825    fun p822 p821  O       o824    fun p821 p820
2154  NOcaml!patt_if  patt_if patt_if Ocaml  NOcaml!patt_if  patt_if patt_if Ocaml
2155  O       o826    patt_if p822 p821  O       o825    patt_if p821 p820
2156  P       p826    Number 4054  P       p825    Number 4045
2157  P       p827    Number 4055  P       p826    Number 4046
2158  O       o827    patt_var p826 p827  O       o826    patt_var p825 p826
2159  NOcaml!patt_body        patt_body       patt_body Ocaml  NOcaml!patt_body        patt_body       patt_body Ocaml
2160  O       o828    patt_body p822 p821  O       o827    patt_body p821 p820
2161  NOcaml!apply    apply   apply Ocaml  NOcaml!apply    apply   apply Ocaml
2162  P       p828    Number 4061  P       p827    Number 4052
2163  O       o829    apply p828 p821  O       o828    apply p827 p820
2164  P       p829    Number 4095  P       p828    Number 4086
2165  O       o830    apply p828 p829  O       o829    apply p827 p828
2166  NOcaml!lid      lid     lid Ocaml  NOcaml!lid      lid     lid Ocaml
2167  P       p830    Number 4067  P       p829    Number 4058
2168  O       o831    lid p828 p830  O       o830    lid p827 p829
2169  O       o832    lid p794  O       o831    lid p793
2170  T       t832    o832  T       t831    o831
2171    B       b831    t831
2172    T       t832    o830 b831
2173  B       b832    t832  B       b832    t832
2174  T       t833    o831 b832  P       p832    Number 4060
2175  B       b833    t833  P       p833    Number 4085
2176  P       p833    Number 4069  O       o833    apply p832 p833
 P       p834    Number 4094  
 O       o834    apply p833 p834  
2177  NOcaml!proj     proj    proj Ocaml  NOcaml!proj     proj    proj Ocaml
2178  P       p835    Number 4092  P       p834    Number 4083
2179  O       o835    proj p833 p835  O       o834    proj p832 p834
2180  O       o836    uid p833 p835  O       o835    uid p832 p834
2181  O       o837    uid p509  O       o836    uid p509
2182  T       t837    o837  T       t836    o836
2183    B       b836    t836
2184    T       t837    o835 b836
2185  B       b837    t837  B       b837    t837
2186  T       t838    o836 b837  P       p837    Number 4069
2187    O       o837    lid p837 p834
2188    P       p838    String hyp_count_addr
2189    O       o838    lid p838
2190    T       t838    o838
2191  B       b838    t838  B       b838    t838
2192  P       p838    Number 4078  T       t839    o837 b838
 O       o838    lid p838 p835  
 P       p839    String hyp_count_addr  
 O       o839    lid p839  
 T       t839    o839  
2193  B       b839    t839  B       b839    t839
2194  T       t840    o838 b839  T       t840    o834 b837 b839
2195  B       b840    t840  B       b840    t840
2196  T       t841    o835 b838 b840  P       p840    Number 4084
2197    O       o840    lid p840 p833
2198    P       p841    Var p
2199    O       o841    var p841
2200    T       t841    o841
2201  B       b841    t841  B       b841    t841
2202  P       p841    Number 4093  T       t842    o840 b841
 O       o841    lid p841 p834  
 P       p842    Var p  
 O       o842    var p842  
 T       t842    o842  
2203  B       b842    t842  B       b842    t842
2204  T       t843    o841 b842  T       t843    o833 b840 b842
2205  B       b843    t843  B       b843    t843
2206  T       t844    o834 b841 b843  T       t844    o829 b832 b843
2207  B       b844    t844  B       b844    t844
2208  T       t845    o830 b833 b844  P       p844    Number 4087
2209    O       o844    lid p844 p820
2210    T       t845    o844 b841
2211  B       b845    t845  B       b845    t845
2212  P       p845    Number 4096  T       t846    o828 b844 b845
 O       o845    lid p845 p821  
 T       t846    o845 b842  
2213  B       b846    t846  B       b846    t846
2214  T       t847    o829 b845 b846  T       t847    o827 b846
2215  B       b847    t847  B       b847    t847 p
2216  T       t848    o828 b847  T       t848    o826 b847
2217  B       b848    t848 p  B       b848    t848
2218  T       t849    o827 b848  T       t849    o825 b848
2219  B       b849    t849  B       b849    t849
2220  T       t850    o826 b849  T       t850    o824 b849
2221  B       b850    t850  B       b850    t850
2222  T       t851    o825 b850  T       t851    o821 b824 b850
2223  B       b851    t851  B       b851    t851
2224  T       t852    o822 b825 b851  T       t852    o b851 b4
2225  B       b852    t852  B       b852    t852
2226  T       t853    o b852 b4  T       t853    o821 b852
2227  B       b853    t853  B       b853    t853
2228  T       t854    o822 b853  T       t854    o392 b853
2229  B       b854    t854  B       b854    t854
2230  T       t855    o392 b854  T       t855    o820 b854
2231  B       b855    t855  B       b855    t855
2232  T       t856    o821 b855  P       p855    Number 4090
2233  B       b856    t856  P       p856    Number 4263
2234  P       p856    Number 4099  O       o856    location p855 p856
2235  P       p857    Number 4272  P       p857    String inv_wf1
2236  O       o857    location p856 p857  O       o857    rule p857
2237  P       p858    String inv_wf1  T       t857    o572 b560
2238  O       o858    rule p858  B       b857    t857
2239  T       t858    o572 b560  T       t858    o620 b857
2240  B       b858    t858  S       s858    t620 h
2241  T       t859    o620 b858  G       s858    t858
2242  S       s859    t620 h  B       b858    s858
2243  G       s859    t859  T       t859    o618 b858
2244  B       b859    s859  B       b859    t859
2245  T       t860    o618 b859  T       t860    o635 b656 b859
2246  B       b860    t860  B       b860    t860
2247  T       t861    o635 b656 b860  T       t861    o635 b639 b860
2248  B       b861    t861  B       b861    t861
2249  T       t862    o635 b639 b861  P       p861    Number 4113
2250  B       b862    t862  P       p862    Number 4120
2251  P       p862    Number 4122  O       o862    resource_defs p861 p862 p264
2252  P       p863    Number 4129  P       p863    Number 4118
2253  O       o863    resource_defs p862 p863 p264  O       o863    uid p863 p862
2254  P       p864    Number 4127  T       t863    o863 b626
2255  O       o864    uid p864 p863  B       b863    t863
2256  T       t864    o864 b626  T       t864    o b863 b4
2257  B       b864    t864  B       b864    t864
2258  T       t865    o b864 b4  T       t865    o862 b864
2259  B       b865    t865  B       b865    t865
2260  T       t866    o863 b865  T       t866    o b865 b4
2261  B       b866    t866  B       b866    t866
2262  T       t867    o b866 b4  T       t867    o857 b618 b861 b623 b866
2263  B       b867    t867  B       b867    t867
2264  T       t868    o858 b618 b862 b623 b867  T       t868    o856 b867
2265  B       b868    t868  B       b868    t868
2266  T       t869    o857 b868  P       p868    Number 4265
2267  B       b869    t869  P       p869    Number 4441
2268  P       p869    Number 4274  O       o869    location p868 p869
2269  P       p870    Number 4450  P       p870    String inv_wf2
2270  O       o870    location p869 p870  O       o870    rule p870
2271  P       p871    String inv_wf2  T       t870    o655 b857 b554
2272  O       o871    rule p871  S       s870    t620 h
2273  T       t871    o655 b858 b554  G       s870    t870
2274  S       s871    t620 h  B       b870    s870
2275  G       s871    t871  T       t871    o618 b870
2276  B       b871    s871  B       b871    t871
2277  T       t872    o618 b871  T       t872    o635 b656 b871
2278  B       b872    t872  B       b872    t872
2279  T       t873    o635 b656 b872  T       t873    o635 b639 b872
2280  B       b873    t873  B       b873    t873
2281  T       t874    o635 b639 b873  P       p873    Number 4288
2282  B       b874    t874  P       p874    Number 4295
2283  P       p874    Number 4297  O       o874    resource_defs p873 p874 p264
2284  P       p875    Number 4304  P       p875    Number 4293
2285  O       o875    resource_defs p874 p875 p264  O       o875    uid p875 p874
2286  P       p876    Number 4302  T       t875    o875 b626
2287  O       o876    uid p876 p875  B       b875    t875
2288  T       t876    o876 b626  T       t876    o b875 b4
2289  B       b876    t876  B       b876    t876
2290  T       t877    o b876 b4  T       t877    o874 b876
2291  B       b877    t877  B       b877    t877
2292  T       t878    o875 b877  T       t878    o b877 b4
2293  B       b878    t878  B       b878    t878
2294  T       t879    o b878 b4  T       t879    o870 b618 b873 b623 b878
2295  B       b879    t879  B       b879    t879
2296  T       t880    o871 b618 b874 b623 b879  T       t880    o869 b879
2297  B       b880    t880  B       b880    t880
2298  T       t881    o870 b880  P       p880    Number 4443
2299  B       b881    t881  P       p881    Number 4530
2300  P       p881    Number 4452  O       o881    location p880 p881
2301  P       p882    Number 4539  P       p882    String inv_fun1
2302  O       o882    location p881 p882  O       o882    rule p882
2303  P       p883    String inv_fun1  T       t882    o572 b712
2304  O       o883    rule p883  B       b882    t882 z
2305  T       t883    o572 b713  T       t883    o711 b882
2306  B       b883    t883 z  S       s883    t620 h
2307  T       t884    o712 b883  G       s883    t883
2308  S       s884    t620 h  B       b883    s883
2309  G       s884    t884  T       t884    o618 b883
2310  B       b884    s884  B       b884    t884
2311  T       t885    o618 b884  P       p884    Number 4467
2312  B       b885    t885  P       p885    Number 4474
2313  P       p885    Number 4476  O       o885    resource_defs p884 p885 p264
2314  P       p886    Number 4483  P       p886    Number 4472
2315  O       o886    resource_defs p885 p886 p264  O       o886    uid p886 p885
2316  P       p887    Number 4481  T       t886    o886 b626
2317  O       o887    uid p887 p886  B       b886    t886
2318  T       t887    o887 b626  T       t887    o b886 b4
2319  B       b887    t887  B       b887    t887
2320  T       t888    o b887 b4  T       t888    o885 b887
2321  B       b888    t888  B       b888    t888
2322  T       t889    o886 b888  T       t889    o b888 b4
2323  B       b889    t889  B       b889    t889
2324  T       t890    o b889 b4  T       t890    o882 b618 b884 b623 b889
2325  B       b890    t890  B       b890    t890
2326  T       t891    o883 b618 b885 b623 b890  T       t891    o881 b890
2327  B       b891    t891  B       b891    t891
2328  T       t892    o882 b891  P       p891    Number 4532
2329  B       b892    t892  P       p892    Number 4718
2330  P       p892    Number 4541  O       o892    location p891 p892
2331  P       p893    Number 4727  P       p893    String inv_id1
2332  O       o893    location p892 p893  O       o893    rule p893
2333  P       p894    String inv_id1  T       t893    o559 b857 b560
2334  O       o894    rule p894  B       b893    t893
2335  T       t894    o559 b858 b560  T       t894    o738 b893 b567
2336  B       b894    t894  S       s894    t620 h
2337  T       t895    o739 b894 b567  G       s894    t894
2338  S       s895    t620 h  B       b894    s894
2339  G       s895    t895  T       t895    o618 b894
2340  B       b895    s895  B       b895    t895
2341  T       t896    o618 b895  T       t896    o635 b656 b895
2342  B       b896    t896  B       b896    t896
2343  T       t897    o635 b656 b896  T       t897    o635 b639 b896
2344  B       b897    t897  B       b897    t897
2345  T       t898    o635 b639 b897  P       p897    Number 4555
2346  B       b898    t898  P       p898    Number 4562
2347  P       p898    Number 4564  O       o898    resource_defs p897 p898 p264
2348  P       p899    Number 4571  P       p899    Number 4560
2349  O       o899    resource_defs p898 p899 p264  O       o899    uid p899 p898
2350  P       p900    Number 4569  T       t899    o899 b626
2351  O       o900    uid p900 p899  B       b899    t899
2352  T       t900    o900 b626  T       t900    o b899 b4
2353  B       b900    t900  B       b900    t900
2354  T       t901    o b900 b4  T       t901    o898 b900
2355  B       b901    t901  B       b901    t901
2356  T       t902    o899 b901  T       t902    o b901 b4
2357  B       b902    t902  B       b902    t902
2358  T       t903    o b902 b4  T       t903    o893 b618 b897 b623 b902
2359  B       b903    t903  B       b903    t903
2360  T       t904    o894 b618 b898 b623 b903  T       t904    o892 b903
2361  B       b904    t904  B       b904    t904
2362  T       t905    o893 b904  P       p904    Number 4720
2363  B       b905    t905  P       p905    Number 4906
2364  P       p905    Number 4729  O       o905    location p904 p905
2365  P       p906    Number 4915  P       p906    String inv_id2
2366  O       o906    location p905 p906  O       o906    rule p906
2367  P       p907    String inv_id2  T       t906    o559 b560 b857
2368  O       o907    rule p907  B       b906    t906
2369  T       t907    o559 b560 b858  T       t907    o738 b906 b567
2370  B       b907    t907  S       s907    t620 h
2371  T       t908    o739 b907 b567  G       s907    t907
2372  S       s908    t620 h  B       b907    s907
2373  G       s908    t908  T       t908    o618 b907
2374  B       b908    s908  B       b908    t908
2375  T       t909    o618 b908  T       t909    o635 b656 b908
2376  B       b909    t909  B       b909    t909
2377  T       t910    o635 b656 b909  T       t910    o635 b639 b909
2378  B       b910    t910  B       b910    t910
2379  T       t911    o635 b639 b910  P       p910    Number 4743
2380  B       b911    t911  P       p911    Number 4750
2381  P       p911    Number 4752  O       o911    resource_defs p910 p911 p264
2382  P       p912    Number 4759  P       p912    Number 4748
2383  O       o912    resource_defs p911 p912 p264  O       o912    uid p912 p911
2384  P       p913    Number 4757  T       t912    o912 b626
2385  O       o913    uid p913 p912  B       b912    t912
2386  T       t913    o913 b626  T       t913    o b912 b4
2387  B       b913    t913  B       b913    t913
2388  T       t914    o b913 b4  T       t914    o911 b913
2389  B       b914    t914  B       b914    t914
2390  T       t915    o912 b914  T       t915    o b914 b4
2391  B       b915    t915  B       b915    t915
2392  T       t916    o b915 b4  T       t916    o906 b618 b910 b623 b915
2393  B       b916    t916  B       b916    t916
2394  T       t917    o907 b618 b911 b623 b916  T       t917    o905 b916
2395  B       b917    t917  B       b917    t917
2396  T       t918    o906 b917  P       p917    Number 5367
2397  B       b918    t918  P       p918    Number 5793
2398  P       p918    Number 5376  O       o918    location p917 p918
2399  P       p919    Number 5802  P       p919    String cancel1
2400  O       o919    location p918 p919  O       o919    rule p919
 P       p920    String cancel1  
 O       o920    rule p920  
2401  NSummary!term_param     term_param      term_param Summary  NSummary!term_param     term_param      term_param Summary
2402  O       o921    term_param  O       o920    term_param
2403  T       t921    o921 b560  T       t920    o920 b560
2404    B       b920    t920
2405    T       t921    o b920 b4
2406  B       b921    t921  B       b921    t921
2407  T       t922    o b921 b4  T       t922    o b617 b921
2408  B       b922    t922  B       b922    t922
2409  T       t923    o b617 b922  T       t923    o738 b562 b695
2410  B       b923    t923  S       s923    t620 h
2411  T       t924    o739 b562 b695  G       s923    t923
2412  S       s924    t620 h  B       b923    s923
2413  G       s924    t924  T       t924    o618 b923
2414  B       b924    s924  B       b924    t924
2415  T       t925    o618 b924  T       t925    o738 b561 b674
2416  B       b925    t925  S       s925    t620 h
2417  T       t926    o739 b561 b674  G       s925    t925
2418  S       s926    t620 h  B       b925    s925
2419  G       s926    t926  T       t926    o618 b925
2420  B       b926    s926  B       b926    t926
2421  T       t927    o618 b926  T       t927    o635 b924 b926
2422  B       b927    t927  B       b927    t927
2423  T       t928    o635 b925 b927  T       t928    o635 b738 b927
2424  B       b928    t928  B       b928    t928
2425  T       t929    o635 b739 b928  T       t929    o635 b658 b928
2426  B       b929    t929  B       b929    t929
2427  T       t930    o635 b658 b929  T       t930    o635 b656 b929
2428  B       b930    t930  B       b930    t930
2429  T       t931    o635 b656 b930  T       t931    o635 b676 b930
2430  B       b931    t931  B       b931    t931
2431  T       t932    o635 b676 b931  T       t932    o635 b641 b931
2432  B       b932    t932  B       b932    t932
2433  T       t933    o635 b641 b932  T       t933    o635 b639 b932
2434  B       b933    t933  B       b933    t933
 T       t934    o635 b639 b933  
 B       b934    t934  
2435  NSummary!interactive    interactive     interactive Summary  NSummary!interactive    interactive     interactive Summary
2436  O       o934    interactive  O       o933    interactive
2437  NSummary!ext_rule       ext_rule        ext_rule Summary  NSummary!ext_rule       ext_rule        ext_rule Summary
2438  P       p934    String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"  P       p933    String "assumT 7 thenT assertT << equal{op{inv{'s1}; op{'s1; 's2}}; op{inv{'s1}; op{'s1; 's3}}} >> thenWT autoT"
2439  O       o935    ext_rule p934  O       o934    ext_rule p933
2440  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  NSummary!status_incomplete      status_incomplete       status_incomplete Summary
2441  O       o936    status_incomplete  O       o935    status_incomplete
2442  T       t936    o936  T       t935    o935
2443  B       b936    t936  B       b935    t935
2444  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
2445  O       o937    ext_unjustified  O       o936    ext_unjustified
2446  NSummary!tactic_arg     tactic_arg      tactic_arg Summary  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
2447  P       p937    String main  P       p936    String main
2448  O       o938    tactic_arg p937  O       o937    tactic_arg p936
2449  NSummary!msequent       msequent        msequent Summary  NSummary!msequent       msequent        msequent Summary
2450  O       o939    msequent  O       o938    msequent
2451  T       t939    o b924 b4  T       t938    o b923 b4
2452    B       b938    t938
2453    T       t939    o b737 b938
2454  B       b939    t939  B       b939    t939
2455  T       t940    o b738 b939  T       t940    o b657 b939
2456  B       b940    t940  B       b940    t940
2457  T       t941    o b657 b940  T       t941    o b655 b940
2458  B       b941    t941  B       b941    t941
2459  T       t942    o b655 b941  T       t942    o b675 b941
2460  B       b942    t942  B       b942    t942
2461  T       t943    o b675 b942  T       t943    o b640 b942
2462  B       b943    t943  B       b943    t943
2463  T       t944    o b640 b943  T       t944    o b638 b943
2464  B       b944    t944  B       b944    t944
2465  T       t945    o b638 b944  T       t945    o938 b925 b944
2466  B       b945    t945  B       b945    t945
 T       t946    o939 b926 b945  
 B       b946    t946  
2467  NSummary!parent_none    parent_none     parent_none Summary  NSummary!parent_none    parent_none     parent_none Summary
2468  O       o946    parent_none  O       o945    parent_none
2469  T       t947    o946  T       t946    o945
2470    B       b946    t946
2471    T       t947    o937 b945 b4 b946
2472  B       b947    t947  B       b947    t947
2473  T       t948    o938 b946 b4 b947  P       p947    String assertion
2474    O       o947    tactic_arg p947
2475    H       h947    v t923
2476    T       t948    o559 b857 b562
2477  B       b948    t948  B       b948    t948
2478  P       p948    String assertion  T       t949    o559 b857 b695
 O       o948    tactic_arg p948  
 H       h948    v t924  
 T       t949    o559 b858 b562  
2479  B       b949    t949  B       b949    t949
2480  T       t950    o559 b858 b695  T       t950    o738 b948 b949
2481  B       b950    t950  S       s950    t620 h h947
2482  T       t951    o739 b949 b950  G       s950    t950
2483  S       s951    t620 h h948  B       b950    s950
2484  G       s951    t951  T       t951    o938 b950 b944
2485  B       b951    s951  B       b951    t951
2486  T       t952    o939 b951 b945  S       s951    t620 h h947
2487  B       b952    t952  G       s951    t925
2488  S       s952    t620 h h948  B       b952    s951
2489  G       s952    t926  T       t952    o938 b952 b944
2490  B       b953    s952  B       b953    t952
2491  T       t953    o939 b953 b945  T       t953    o2 b947
2492  B       b954    t953  B       b954    t953
2493  T       t954    o2 b948  T       t954    o937 b953 b4 b954
2494  B       b955    t954  B       b955    t954
2495  T       t955    o938 b954 b4 b955  T       t955    o2 b955
2496  B       b956    t955  B       b956    t955
2497  T       t956    o2 b956  T       t956    o947 b951 b4 b956
2498  B       b957    t956  B       b957    t956
2499  T       t957    o948 b952 b4 b957  H       h957    v_1 t950
2500  B       b958    t957  S       s957    t620 h h947 h957
2501  H       h958    v_1 t951  G       s957    t925
2502  S       s958    t620 h h948 h958  B       b958    s957
2503  G       s958    t926  T       t958    o938 b958 b944
2504  B       b959    s958  B       b959    t958
2505  T       t959    o939 b959 b945  T       t959    o937 b959 b4 b956
2506  B       b960    t959  B       b960    t959
2507  T       t960    o938 b960 b4 b957  T       t960    o b960 b4
2508  B       b961    t960  B       b961    t960
2509  T       t961    o b961 b4  T       t961    o b957 b961
2510  B       b962    t961  B       b962    t961
2511  T       t962    o b958 b962  T       t962    o936 b947 b962
2512  B       b963    t962  B       b963    t962
2513  T       t963    o937 b948 b963  P       p963    String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"
2514    O       o963    ext_rule p963
2515    T       t963    o936 b957 b4
2516  B       b964    t963  B       b964    t963
2517  P       p964    String "rwh unfold_equal 0 thenT rwh unfold_equal 2 thenT autoT"  T       t964    o963 b935 b964 b4 b4
 O       o964    ext_rule p964  
 T       t964    o937 b958 b4  
2518  B       b965    t964  B       b965    t964
2519  T       t965    o964 b936 b965 b4 b4  P       p965    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"
2520  B       b966    t965  O       o965    ext_rule p965
2521  P       p966    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3 thenWT autoT"  P       p966    String eq
2522  O       o966    ext_rule p966  O       o966    tactic_arg p966
2523  P       p967    String eq  T       t966    o559 b893 b561
2524  O       o967    tactic_arg p967  B       b966    t966
2525  T       t967    o559 b894 b561  T       t967    o738 b948 b966
2526  B       b967    t967  S       s967    t620 h h947 h957
2527  T       t968    o739 b949 b967  G       s967    t967
2528  S       s968    t620 h h948 h958  B       b967    s967
2529  G       s968    t968  T       t968    o938 b967 b944
2530  B       b968    s968  B       b968    t968
2531  T       t969    o939 b968 b945  T       t969    o2 b960
2532  B       b969    t969  B       b969    t969
2533  T       t970    o2 b961  T       t970    o966 b968 b4 b969
2534  B       b970    t970  B       b970    t970
2535  T       t971    o967 b969 b4 b970  T       t971    o738 b966 b949
2536  B       b971    t971  H       h971    v_2 t971
2537  T       t972    o739 b967 b950  S       s971    t620 h h947 h957 h971
2538  H       h972    v_2 t972  G       s971    t925
2539  S       s972    t620 h h948 h958 h972  B       b971    s971
2540  G       s972    t926  T       t972    o938 b971 b944
2541  B       b972    s972  B       b972    t972
2542  T       t973    o939 b972 b945  T       t973    o937 b972 b4 b969
2543  B       b973    t973  B       b973    t973
2544  T       t974    o938 b973 b4 b970  P       p973    String wf
2545  B       b974    t974  O       o973    tactic_arg p973
2546  P       p974    String wf  B       b974    t949 v_2
2547  O       o974    tactic_arg p974  T       t974    o711 b974
2548  B       b975    t950 v_2  S       s974    t620 h h947 h957
2549  T       t975    o712 b975  G       s974    t974
2550  S       s975    t620 h h948 h958  B       b975    s974
2551  G       s975    t975  T       t975    o938 b975 b944
2552  B       b976    s975  B       b976    t975
 T       t976    o939 b976 b945  
 B       b977    t976  
2553  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq
2554  O       o977    fun_prop  O       o976    fun_prop
2555  P       p977    Var v_2  P       p976    Var v_2
2556  O       o978    var p977  O       o977    var p976
2557  T       t978    o978  T       t977    o977
2558  B       b978    t978  B       b977    t977
2559  T       t979    o739 b978 b950  T       t978    o738 b977 b949
2560  B       b979    t979 v_2  B       b978    t978 v_2
2561  T       t980    o977 b979  T       t979    o976 b978
2562  S       s980    t620 h h948 h958  S       s979    t620 h h947 h957
2563  G       s980    t980  G       s979    t979
2564  B       b980    s980  B       b979    s979
2565  T       t981    o939 b980 b945  T       t980    o938 b979 b944
2566  B       b981    t981  B       b980    t980
2567  NSummary!arg_named      arg_named       arg_named Summary  NSummary!arg_named      arg_named       arg_named Summary
2568  P       p981    String d_auto  P       p980    String d_auto
2569  O       o981    arg_named p981  O       o980    arg_named p980
2570  NSummary!arg_bool       arg_bool        arg_bool Summary  NSummary!arg_bool       arg_bool        arg_bool Summary
2571  P       p982    String true  P       p981    String true
2572  O       o982    arg_bool p982  O       o981    arg_bool p981
2573  T       t982    o982  T       t981    o981
2574    B       b981    t981
2575    T       t982    o980 b981
2576  B       b982    t982  B       b982    t982
2577  T       t983    o981 b982  T       t983    o b982 b4
2578  B       b983    t983  B       b983    t983
2579  T       t984    o b983 b4  T       t984    o973 b980 b983 b969
2580  B       b984    t984  B       b984    t984
2581  T       t985    o974 b981 b984 b970  T       t985    o2 b984
2582  B       b985    t985  B       b985    t985
2583  T       t986    o2 b985  T       t986    o973 b976 b4 b985
2584  B       b986    t986  B       b986    t986
2585  T       t987    o974 b977 b4 b986  T       t987    o b986 b4
2586  B       b987    t987  B       b987    t987
2587  T       t988    o b987 b4  T       t988    o b973 b987
2588  B       b988    t988  B       b988    t988
2589  T       t989    o b974 b988  T       t989    o b970 b988
2590  B       b989    t989  B       b989    t989
2591  T       t990    o b971 b989  T       t990    o936 b960 b989
2592  B       b990    t990  B       b990    t990
2593  T       t991    o937 b961 b990  P       p990    String autoT
2594    O       o990    ext_rule p990
2595    T       t991    o936 b970 b4
2596  B       b991    t991  B       b991    t991
2597  P       p991    String autoT  T       t992    o990 b935 b991 b4 b4
 O       o991    ext_rule p991  
 T       t992    o937 b971 b4  
2598  B       b992    t992  B       b992    t992
2599  T       t993    o991 b936 b992 b4 b4  P       p992    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"
2600    O       o992    ext_rule p992
2601    T       t993    o559 b893 b674
2602  B       b993    t993  B       b993    t993
2603  P       p993    String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4 thenWT autoT"  T       t994    o738 b949 b993
2604  O       o993    ext_rule p993  S       s994    t620 h h947 h957 h971
2605  T       t994    o559 b894 b674  G       s994    t994
2606  B       b994    t994  B       b994    s994
2607  T       t995    o739 b950 b994  T       t995    o938 b994 b944
2608  S       s995    t620 h h948 h958 h972  B       b995    t995
2609  G       s995    t995  T       t996    o2 b973
 B       b995    s995  
 T       t996    o939 b995 b945  
2610  B       b996    t996  B       b996    t996
2611  T       t997    o2 b974  T       t997    o966 b995 b4 b996
2612  B       b997    t997  B       b997    t997
2613  T       t998    o967 b996 b4 b997  T       t998    o738 b966 b993
2614  B       b998    t998  H       h998    v_3 t998
2615  T       t999    o739 b967 b994  S       s998    t620 h h947 h957 h971 h998
2616  H       h999    v_3 t999  G       s998    t925
2617  S       s999    t620 h h948 h958 h972 h999  B       b998    s998
2618  G       s999    t926  T       t999    o938 b998 b944
2619  B       b999    s999  B       b999    t999
2620  T       t1000   o939 b999 b945  T       t1000   o937 b999 b4 b996
2621  B       b1000   t1000  B       b1000   t1000
2622  T       t1001   o938 b1000 b4 b997  B       b1001   t966 v_3
2623  B       b1001   t1001  T       t1001   o711 b1001
2624  B       b1002   t967 v_3  S       s1001   t620 h h947 h957 h971
2625  T       t1002   o712 b1002  G       s1001   t1001
2626  S       s1002   t620 h h948 h958 h972  B       b1002   s1001
2627  G       s1002   t1002  T       t1002   o938 b1002 b944
2628  B       b1003   s1002  B       b1003   t1002
2629  T       t1003   o939 b1003 b945  P       p1003   Var v_3
2630    O       o1003   var p1003
2631    T       t1003   o1003
2632  B       b1004   t1003  B       b1004   t1003
2633  P       p1004   Var v_3  T       t1004   o738 b966 b1004
2634  O       o1004   var p1004  B       b1005   t1004 v_3
2635  T       t1004   o1004  T       t1005   o976 b1005
2636  B       b1005   t1004  S       s1005   t620 h h947 h957 h971
2637  T       t1005   o739 b967 b1005  G       s1005   t1005
2638  B       b1006   t1005 v_3  B       b1006   s1005
2639  T       t1006   o977 b1006  T       t1006   o938 b1006 b944
2640  S       s1006   t620 h h948 h958 h972  B       b1007   t1006
2641  G       s1006   t1006  T       t1007   o973 b1007 b983 b996
 B       b1007   s1006  
 T       t1007   o939 b1007 b945  
2642  B       b1008   t1007  B       b1008   t1007
2643  T       t1008   o974 b1008 b984 b997  T       t1008   o2 b1008
2644  B       b1009   t1008  B       b1009   t1008
2645  T       t1009   o2 b1009  T       t1009   o973 b1003 b4 b1009
2646  B       b1010   t1009  B       b1010   t1009
2647  T       t1010   o974 b1004 b4 b1010  T       t1010   o b1010 b4
2648  B       b1011   t1010  B       b1011   t1010
2649  T       t1011   o b1011 b4  T       t1011   o b1000 b1011
2650  B       b1012   t1011  B       b1012   t1011
2651  T       t1012   o b1001 b1012  T       t1012   o b997 b1012
2652  B       b1013   t1012  B       b1013   t1012
2653  T       t1013   o b998 b1013  T       t1013   o936 b973 b1013
2654  B       b1014   t1013  B       b1014   t1013
2655  T       t1014   o937 b974 b1014  T       t1014   o936 b997 b4
2656  B       b1015   t1014  B       b1015   t1014
2657  T       t1015   o937 b998 b4  T       t1015   o990 b935 b1015 b4 b4
2658  B       b1016   t1015  B       b1016   t1015
2659  T       t1016   o991 b936 b1016 b4 b4  P       p1016   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"
2660    O       o1016   ext_rule p1016
2661    T       t1016   o559 b567 b561
2662  B       b1017   t1016  B       b1017   t1016
2663  P       p1017   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 5 thenAT autoT"  T       t1017   o559 b567 b674
 O       o1017   ext_rule p1017  
 T       t1017   o559 b567 b561  
2664  B       b1018   t1017  B       b1018   t1017
2665  T       t1018   o559 b567 b674  T       t1018   o738 b1017 b1018
2666  B       b1019   t1018  H       h1018   v_4 t1018
2667  T       t1019   o739 b1018 b1019  S       s1018   t620 h h947 h957 h971 h998 h1018
2668  H       h1019   v_4 t1019  G       s1018   t925
2669  S       s1019   t620 h h948 h958 h972 h999 h1019  B       b1019   s1018
2670  G       s1019   t926  T       t1019   o938 b1019 b944
2671  B       b1020   s1019  B       b1020   t1019
2672  T       t1020   o939 b1020 b945  T       t1020   o2 b1000
2673  B       b1021   t1020  B       b1021   t1020
2674  T       t1021   o2 b1001  T       t1021   o937 b1020 b4 b1021
2675  B       b1022   t1021  B       b1022   t1021
2676  T       t1022   o938 b1021 b4 b1022  T       t1022   o b1022 b4
2677  B       b1023   t1022  B       b1023   t1022
2678  T       t1023   o b1023 b4  T       t1023   o936 b1000 b1023
2679  B       b1024   t1023  B       b1024   t1023
2680  T       t1024   o937 b1001 b1024  P       p1024   String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"
2681  B       b1025   t1024  O       o1024   ext_rule p1024
2682  P       p1025   String "setSubstT << equal{op{id; 's2}; 's2} >> 6 thenAT autoT"  T       t1024   o738 b561 b1018
2683  O       o1025   ext_rule p1025  H       h1024   v_5 t1024
2684  T       t1025   o739 b561 b1019  S       s1024   t620 h h947 h957 h971 h998 h1018 h1024
2685  H       h1025   v_5 t1025  G       s1024   t925
2686  S       s1025   t620 h h948 h958 h972 h999 h1019 h1025  B       b1025   s1024
2687  G       s1025   t926  T       t1025   o938 b1025 b944
2688  B       b1026   s1025  B       b1026   t1025
2689  T       t1026   o939 b1026 b945  T       t1026   o2 b1022
2690  B       b1027   t1026  B       b1027   t1026
2691  T       t1027   o2 b1023  T       t1027   o937 b1026 b4 b1027
2692  B       b1028   t1027  B       b1028   t1027
2693  T       t1028   o938 b1027 b4 b1028  B       b1029   t1017 v_5
2694  B       b1029   t1028  T       t1029   o711 b1029
2695  B       b1030   t1018 v_5  S       s1029   t620 h h947 h957 h971 h998 h1018
2696  T       t1030   o712 b1030  G       s1029   t1029
2697  S       s1030   t620 h h948 h958 h972 h999 h1019  B       b1030   s1029
2698  G       s1030   t1030  T       t1030   o938 b1030 b944
2699  B       b1031   s1030  B       b1031   t1030
2700  T       t1031   o939 b1031 b945  P       p1031   Var v_5
2701    O       o1031   var p1031
2702    T       t1031   o1031
2703  B       b1032   t1031  B       b1032   t1031
2704  P       p1032   Var v_5  T       t1032   o738 b1032 b1018
2705  O       o1032   var p1032  B       b1033   t1032 v_5
2706  T       t1032   o1032  T       t1033   o976 b1033
2707  B       b1033   t1032  S       s1033   t620 h h947 h957 h971 h998 h1018
2708  T       t1033   o739 b1033 b1019  G       s1033   t1033
2709  B       b1034   t1033 v_5  B       b1034   s1033
2710  T       t1034   o977 b1034  T       t1034   o938 b1034 b944
2711  S       s1034   t620 h h948 h958 h972 h999 h1019  B       b1035   t1034
2712  G       s1034   t1034  T       t1035   o973 b1035 b983 b1027
 B       b1035   s1034  
 T       t1035   o939 b1035 b945  
2713  B       b1036   t1035  B       b1036   t1035
2714  T       t1036   o974 b1036 b984 b1028  T       t1036   o2 b1036
2715  B       b1037   t1036  B       b1037   t1036
2716  T       t1037   o2 b1037  T       t1037   o973 b1031 b4 b1037
2717  B       b1038   t1037  B       b1038   t1037
2718  T       t1038   o974 b1032 b4 b1038  T       t1038   o b1038 b4
2719  B       b1039   t1038  B       b1039   t1038
2720  T       t1039   o b1039 b4  T       t1039   o b1028 b1039
2721  B       b1040   t1039  B       b1040   t1039
2722  T       t1040   o b1029 b1040  T       t1040   o936 b1022 b1040
2723  B       b1041   t1040  B       b1041   t1040
2724  T       t1041   o937 b1023 b1041  P       p1041   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"
2725  B       b1042   t1041  O       o1041   ext_rule p1041
2726  P       p1042   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenAT autoT"  H       h1041   v_6 t925
2727  O       o1042   ext_rule p1042  S       s1041   t620 h h947 h957 h971 h998 h1018 h1024 h1041
2728  H       h1042   v_6 t926  G       s1041   t925
2729  S       s1042   t620 h h948 h958 h972 h999 h1019 h1025 h1042  B       b1042   s1041
2730  G       s1042   t926  T       t1042   o938 b1042 b944
2731  B       b1043   s1042  B       b1043   t1042
2732  T       t1043   o939 b1043 b945  T       t1043   o2 b1028
2733  B       b1044   t1043  B       b1044   t1043
2734  T       t1044   o2 b1029  T       t1044   o937 b1043 b4 b1044
2735  B       b1045   t1044  B       b1045   t1044
2736  T       t1045   o938 b1044 b4 b1045  T       t1045   o b1045 b4
2737  B       b1046   t1045  B       b1046   t1045
2738  T       t1046   o b1046 b4  T       t1046   o936 b1028 b1046
2739  B       b1047   t1046  B       b1047   t1046
2740  T       t1047   o937 b1029 b1047  P       p1047   String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"
2741    O       o1047   ext_rule p1047
2742    T       t1047   o936 b1045 b4
2743  B       b1048   t1047  B       b1048   t1047
2744  P       p1048   String "rwh unfold_equal 0 thenT rwh unfold_equal 8 thenT autoT"  T       t1048   o1047 b935 b1048 b4 b4
 O       o1048   ext_rule p1048  
 T       t1048   o937 b1046 b4  
2745  B       b1049   t1048  B       b1049   t1048
2746  T       t1049   o1048 b936 b1049 b4 b4  T       t1049   o b1049 b4
2747  B       b1050   t1049  B       b1050   t1049
2748  T       t1050   o b1050 b4  P       p1050   String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"
2749  B       b1051   t1050  O       o1050   ext_rule p1050
2750  P       p1051   String "rwh unfold_fun_set 0 thenT autoT thenT rwh unfold_equal 0 thenT autoT"  B       b1051   t1016 v_6
2751  O       o1051   ext_rule p1051  T       t1051   o711 b1051
2752  B       b1052   t1017 v_6  S       s1051   t620 h h947 h957 h971 h998 h1018 h1024
2753  T       t1052   o712 b1052  G       s1051   t1051
2754  S       s1052   t620 h h948 h958 h972 h999 h1019 h1025  B       b1052   s1051
2755  G       s1052   t1052  T       t1052   o938 b1052 b944
2756  B       b1053   s1052  B       b1053   t1052
2757  T       t1053   o939 b1053 b945  P       p1053   Var v_6
2758    O       o1053   var p1053
2759    T       t1053   o1053
2760  B       b1054   t1053  B       b1054   t1053
2761  P       p1054   Var v_6  T       t1054   o738 b1017 b1054
2762  O       o1054   var p1054  B       b1055   t1054 v_6
2763  T       t1054   o1054  T       t1055   o976 b1055
2764  B       b1055   t1054  S       s1055   t620 h h947 h957 h971 h998 h1018 h1024
2765  T       t1055   o739 b1018 b1055  G       s1055   t1055
2766  B       b1056   t1055 v_6  B       b1056   s1055
2767  T       t1056   o977 b1056  T       t1056   o938 b1056 b944
2768  S       s1056   t620 h h948 h958 h972 h999 h1019 h1025  B       b1057   t1056
2769  G       s1056   t1056  T       t1057   o973 b1057 b983 b1044
 B       b1057   s1056  
 T       t1057   o939 b1057 b945  
2770  B       b1058   t1057  B       b1058   t1057
2771  T       t1058   o974 b1058 b984 b1045  T       t1058   o2 b1058
2772  B       b1059   t1058  B       b1059   t1058
2773  T       t1059   o2 b1059  T       t1059   o973 b1053 b4 b1059
2774  B       b1060   t1059  B       b1060   t1059
2775  T       t1060   o974 b1054 b4 b1060  T       t1060   o936 b1060 b4
2776  B       b1061   t1060  B       b1061   t1060
2777  T       t1061   o937 b1061 b4  T       t1061   o1050 b935 b1061 b4 b4
2778  B       b1062   t1061  B       b1062   t1061
2779  T       t1062   o1051 b936 b1062 b4 b4  T       t1062   o b1062 b4
2780  B       b1063   t1062  B       b1063   t1062
2781  T       t1063   o b1063 b4  T       t1063   o1041 b935 b1047 b1050 b1063
2782  B       b1064   t1063  B       b1064   t1063
2783  T       t1064   o1042 b936 b1048 b1051 b1064  T       t1064   o936 b1038 b4
2784  B       b1065   t1064  B       b1065   t1064
2785  T       t1065   o937 b1039 b4  T       t1065   o1050 b935 b1065 b4 b4
2786  B       b1066   t1065  B       b1066   t1065
2787  T       t1066   o1051 b936 b1066 b4 b4  T       t1066   o b1066 b4
2788  B       b1067   t1066  B       b1067   t1066
2789  T       t1067   o b1067 b4  T       t1067   o b1064 b1067
2790  B       b1068   t1067  B       b1068   t1067
2791  T       t1068   o b1065 b1068  T       t1068   o1024 b935 b1041 b1068 b4
2792  B       b1069   t1068  B       b1069   t1068
2793  T       t1069   o1025 b936 b1042 b1069 b4  T       t1069   o b1069 b4
2794  B       b1070   t1069  B       b1070   t1069
2795  T       t1070   o b1070 b4  T       t1070   o1016 b935 b1024 b1070 b4
2796  B       b1071   t1070  B       b1071   t1070
2797  T       t1071   o1017 b936 b1025 b1071 b4  P       p1071   String "rwh unfold_fun_set 0 thenT autoT"
2798    O       o1071   ext_rule p1071
2799    T       t1071   o936 b1010 b4
2800  B       b1072   t1071  B       b1072   t1071
2801  P       p1072   String "rwh unfold_fun_set 0 thenT autoT"  T       t1072   o1071 b935 b1072 b4 b4
 O       o1072   ext_rule p1072  
 T       t1072   o937 b1011 b4  
2802  B       b1073   t1072  B       b1073   t1072
2803  T       t1073   o1072 b936 b1073 b4 b4  T       t1073   o b1073 b4
2804  B       b1074   t1073  B       b1074   t1073
2805  T       t1074   o b1074 b4  T       t1074   o b1071 b1074
2806  B       b1075   t1074  B       b1075   t1074
2807  T       t1075   o b1072 b1075  T       t1075   o b1016 b1075
2808  B       b1076   t1075  B       b1076   t1075
2809  T       t1076   o b1017 b1076  T       t1076   o992 b935 b1014 b1076 b4
2810  B       b1077   t1076  B       b1077   t1076
2811  T       t1077   o993 b936 b1015 b1077 b4  T       t1077   o936 b986 b4
2812  B       b1078   t1077  B       b1078   t1077
2813  T       t1078   o937 b987 b4  T       t1078   o1071 b935 b1078 b4 b4
2814  B       b1079   t1078  B       b1079   t1078
2815  T       t1079   o1072 b936 b1079 b4 b4  T       t1079   o b1079 b4
2816  B       b1080   t1079  B       b1080   t1079
2817  T       t1080   o b1080 b4  T       t1080   o b1077 b1080
2818  B       b1081   t1080  B       b1081   t1080
2819  T       t1081   o b1078 b1081  T       t1081   o b992 b1081
2820  B       b1082   t1081  B       b1082   t1081
2821  T       t1082   o b993 b1082  T       t1082   o965 b935 b990 b1082 b4
2822  B       b1083   t1082  B       b1083   t1082
2823  T       t1083   o966 b936 b991 b1083 b4  T       t1083   o b1083 b4
2824  B       b1084   t1083  B       b1084   t1083
2825  T       t1084   o b1084 b4  T       t1084   o b965 b1084
2826  B       b1085   t1084  B       b1085   t1084
 T       t1085   o b966 b1085  
 B       b1086   t1085  
2827  NSummary!ext_goal       ext_goal        ext_goal Summary  NSummary!ext_goal       ext_goal        ext_goal Summary
2828  O       o1086   ext_goal  O       o1085   ext_goal
2829  S       s1086   t620 h  S       s1085   t620 h
2830  G       s1086   t951  G       s1085   t950
2831  B       b1087   s1086  B       b1086   s1085
2832  T       t1087   o939 b1087 b945  T       t1086   o938 b1086 b944
2833    B       b1087   t1086
2834    T       t1087   o947 b1087 b4 b954
2835  B       b1088   t1087  B       b1088   t1087
2836  T       t1088   o948 b1088 b4 b955  T       t1088   o1085 b1088
2837  B       b1089   t1088  B       b1089   t1088
2838  T       t1089   o1086 b1089  T       t1089   o b1089 b4
2839  B       b1090   t1089  B       b1090   t1089
2840  T       t1090   o b1090 b4  T       t1090   o963 b935 b1089 b1090 b4
2841  B       b1091   t1090  B       b1091   t1090
2842  T       t1091   o964 b936 b1090 b1091 b4  P       p1091   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"
2843  B       b1092   t1091  O       o1091   ext_rule p1091
2844  P       p1092   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 3"  H       h1091   v t950
2845  O       o1092   ext_rule p1092  S       s1091   t620 h h1091
2846  H       h1092   v t951  G       s1091   t925
2847  S       s1092   t620 h h1092  B       b1092   s1091
2848  G       s1092   t926  T       t1092   o938 b1092 b944
2849  B       b1093   s1092  B       b1093   t1092
2850  T       t1093   o939 b1093 b945  T       t1093   o937 b1093 b4 b954
2851  B       b1094   t1093  B       b1094   t1093
2852  T       t1094   o938 b1094 b4 b955  T       t1094   o1085 b1094
2853  B       b1095   t1094  B       b1095   t1094
2854  T       t1095   o1086 b1095  P       p1095   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"
2855  B       b1096   t1095  O       o1095   ext_rule p1095
2856  P       p1096   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 4"  P       p1096   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"
2857  O       o1096   ext_rule p1096  O       o1096   ext_rule p1096
2858  P       p1097   String "setSubstT << equal{op{id; 's3}; 's3} >> 7 thenT autoT"  T       t1096   o b1095 b4
2859  O       o1097   ext_rule p1097  B       b1096   t1096
2860  T       t1097   o b1096 b4  H       h1096   x t923
2861  B       b1097   t1097  H       h1097   v_1 t971
2862  H       h1097   x t924  H       h1098   v_2 t998
2863  H       h1098   v_1 t972  H       h1099   v_3 t1018
2864  H       h1099   v_2 t999  H       h1100   v_4 t1024
2865  H       h1100   v_3 t1019  B       b1100   t1016 v_5
2866  H       h1101   v_4 t1025  T       t1100   o711 b1100
2867  B       b1101   t1017 v_5  S       s1100   t620 h h1096 h1091 h1097 h1098 h1099 h1100
2868  T       t1101   o712 b1101  G       s1100   t1100
2869  S       s1101   t620 h h1097 h1092 h1098 h1099 h1100 h1101  B       b1101   s1100
2870  G       s1101   t1101  T       t1101   o b737 b4
2871  B       b1102   s1101  B       b1102   t1101
2872  T       t1102   o b738 b4  T       t1102   o b657 b1102
2873  B       b1103   t1102  B       b1103   t1102
2874  T       t1103   o b657 b1103  T       t1103   o b655 b1103
2875  B       b1104   t1103  B       b1104   t1103
2876  T       t1104   o b655 b1104  T       t1104   o b675 b1104
2877  B       b1105   t1104  B       b1105   t1104
2878  T       t1105   o b675 b1105  T       t1105   o b640 b1105
2879  B       b1106   t1105  B       b1106   t1105
2880  T       t1106   o b640 b1106  T       t1106   o b638 b1106
2881  B       b1107   t1106  B       b1107   t1106
2882  T       t1107   o b638 b1107  T       t1107   o938 b1101 b1107
2883  B       b1108   t1107  B       b1108   t1107
2884  T       t1108   o939 b1102 b1108  T       t1108   o738 b1017 b1032
2885  B       b1109   t1108  B       b1109   t1108 v_5
2886  T       t1109   o739 b1018 b1033  T       t1109   o976 b1109
2887  B       b1110   t1109 v_5  S       s1109   t620 h h1096 h1091 h1097 h1098 h1099 h1100
2888  T       t1110   o977 b1110  G       s1109   t1109
2889  S       s1110   t620 h h1097 h1092 h1098 h1099 h1100 h1101  B       b1110   s1109
2890  G       s1110   t1110  T       t1110   o938 b1110 b1107
2891  B       b1111   s1110  B       b1111   t1110
2892  T       t1111   o939 b1111 b1108  S       s1111   t620 h h1096 h1091 h1097 h1098 h1099 h1100
2893  B       b1112   t1111  G       s1111   t925
2894  S       s1112   t620 h h1097 h1092 h1098 h1099 h1100 h1101  B       b1112   s1111
2895  G       s1112   t926  T       t1112   o938 b1112 b1107
2896  B       b1113   s1112  B       b1113   t1112
2897  T       t1113   o939 b1113 b1108  S       s1113   t620 h h1096 h1091 h1097 h1098 h1099
2898  B       b1114   t1113  G       s1113   t925
2899  S       s1114   t620 h h1097 h1092 h1098 h1099 h1100  B       b1114   s1113
2900  G       s1114   t926  T       t1114   o938 b1114 b1107
2901  B       b1115   s1114  B       b1115   t1114
2902  T       t1115   o939 b1115 b1108  S       s1115   t620 h h1096 h1091 h1097 h1098
2903  B       b1116   t1115  G       s1115   t925
2904  S       s1116   t620 h h1097 h1092 h1098 h1099  B       b1116   s1115
2905  G       s1116   t926  T       t1116   o938 b1116 b1107
2906  B       b1117   s1116  B       b1117   t1116
2907  T       t1117   o939 b1117 b1108  S       s1117   t620 h h1096 h1091 h1097
2908  B       b1118   t1117  G       s1117   t925
2909  S       s1118   t620 h h1097 h1092 h1098  B       b1118   s1117
2910  G       s1118   t926  T       t1118   o938 b1118 b1107
2911  B       b1119   s1118  B       b1119   t1118
2912  T       t1119   o939 b1119 b1108  S       s1119   t620 h h1096 h1091
2913  B       b1120   t1119  G       s1119   t925
2914  S       s1120   t620 h h1097 h1092  B       b1120   s1119
2915  G       s1120   t926  T       t1120   o938 b1120 b1107
2916  B       b1121   s1120  B       b1121   t1120
2917  T       t1121   o939 b1121 b1108  S       s1121   t620 h h1096
2918  B       b1122   t1121  G       s1121   t925
2919  S       s1122   t620 h h1097  B       b1122   s1121
2920  G       s1122   t926  T       t1122   o938 b1122 b1107
2921  B       b1123   s1122  B       b1123   t1122
2922  T       t1123   o939 b1123 b1108  T       t1123   o937 b1123 b4 b946
2923  B       b1124   t1123  B       b1124   t1123
2924  T       t1124   o938 b1124 b4 b947  T       t1124   o2 b1124
2925  B       b1125   t1124  B       b1125   t1124
2926  T       t1125   o2 b1125  T       t1125   o937 b1121 b4 b1125
2927  B       b1126   t1125  B       b1126   t1125
2928  T       t1126   o938 b1122 b4 b1126  T       t1126   o2 b1126
2929  B       b1127   t1126  B       b1127   t1126
2930  T       t1127   o2 b1127  T       t1127   o937 b1119 b4 b1127
2931  B       b1128   t1127  B       b1128   t1127
2932  T       t1128   o938 b1120 b4 b1128  T       t1128   o2 b1128
2933  B       b1129   t1128  B       b1129   t1128
2934  T       t1129   o2 b1129  T       t1129   o937 b1117 b4 b1129
2935  B       b1130   t1129  B       b1130   t1129
2936  T       t1130   o938 b1118 b4 b1130  T       t1130   o2 b1130
2937  B       b1131   t1130  B       b1131   t1130
2938  T       t1131   o2 b1131  T       t1131   o937 b1115 b4 b1131
2939  B       b1132   t1131  B       b1132   t1131
2940  T       t1132   o938 b1116 b4 b1132  T       t1132   o2 b1132
2941  B       b1133   t1132  B       b1133   t1132
2942  T       t1133   o2 b1133  T       t1133   o937 b1113 b4 b1133
2943  B       b1134   t1133  B       b1134   t1133
2944  T       t1134   o938 b1114 b4 b1134  T       t1134   o2 b1134
2945  B       b1135   t1134  B       b1135   t1134
2946  T       t1135   o2 b1135  T       t1135   o973 b1111 b983 b1135
2947  B       b1136   t1135  B       b1136   t1135
2948  T       t1136   o974 b1112 b984 b1136  T       t1136   o2 b1136
2949  B       b1137   t1136  B       b1137   t1136
2950  T       t1137   o2 b1137  T       t1137   o973 b1108 b4 b1137
2951  B       b1138   t1137  B       b1138   t1137
2952  T       t1138   o974 b1109 b4 b1138  T       t1138   o936 b1138 b4
2953  B       b1139   t1138  B       b1139   t1138
2954  T       t1139   o937 b1139 b4  T       t1139   o1050 b935 b1139 b4 b4
2955  B       b1140   t1139  B       b1140   t1139
2956  T       t1140   o1051 b936 b1140 b4 b4  T       t1140   o b1140 b4
2957  B       b1141   t1140  B       b1141   t1140
2958  T       t1141   o b1141 b4  T       t1141   o1096 b935 b1095 b1096 b1141
2959  B       b1142   t1141  B       b1142   t1141
2960  T       t1142   o1097 b936 b1096 b1097 b1142  T       t1142   o b1142 b4
2961  B       b1143   t1142  B       b1143   t1142
2962  T       t1143   o b1143 b4  B       b1144   t1017 v_4
2963  B       b1144   t1143  T       t1144   o711 b1144
2964  B       b1145   t1018 v_4  S       s1144   t620 h h1096 h1091 h1097 h1098 h1099
2965  T       t1145   o712 b1145  G       s1144   t1144
2966  S       s1145   t620 h h1097 h1092 h1098 h1099 h1100  B       b1145   s1144
2967  G       s1145   t1145  T       t1145   o938 b1145 b1107
2968  B       b1146   s1145  B       b1146   t1145
2969  T       t1146   o939 b1146 b1108  P       p1146   Var v_4
2970    O       o1146   var p1146
2971    T       t1146   o1146
2972  B       b1147   t1146  B       b1147   t1146
2973  P       p1147   Var v_4  T       t1147   o738 b1147 b1018
2974  O       o1147   var p1147  B       b1148   t1147 v_4
2975  T       t1147   o1147  T       t1148   o976 b1148
2976  B       b1148   t1147  S       s1148   t620 h h1096 h1091 h1097 h1098 h1099
2977  T       t1148   o739 b1148 b1019  G       s1148   t1148
2978  B       b1149   t1148 v_4  B       b1149   s1148
2979  T       t1149   o977 b1149  T       t1149   o938 b1149 b1107
2980  S       s1149   t620 h h1097 h1092 h1098 h1099 h1100  B       b1150   t1149
2981  G       s1149   t1149  T       t1150   o973 b1150 b983 b1133
 B       b1150   s1149  
 T       t1150   o939 b1150 b1108  
2982  B       b1151   t1150  B       b1151   t1150
2983  T       t1151   o974 b1151 b984 b1134  T       t1151   o2 b1151
2984  B       b1152   t1151  B       b1152   t1151
2985  T       t1152   o2 b1152  T       t1152   o973 b1146 b4 b1152
2986  B       b1153   t1152  B       b1153   t1152
2987  T       t1153   o974 b1147 b4 b1153  T       t1153   o936 b1153 b4
2988  B       b1154   t1153  B       b1154   t1153
2989  T       t1154   o937 b1154 b4  T       t1154   o1050 b935 b1154 b4 b4
2990  B       b1155   t1154  B       b1155   t1154
2991  T       t1155   o1051 b936 b1155 b4 b4  T       t1155   o b1155 b4
2992  B       b1156   t1155  B       b1156   t1155
2993  T       t1156   o b1156 b4  T       t1156   o1024 b935 b1095 b1143 b1156
2994  B       b1157   t1156  B       b1157   t1156
2995  T       t1157   o1025 b936 b1096 b1144 b1157  T       t1157   o b1157 b4
2996  B       b1158   t1157  B       b1158   t1157
2997  T       t1158   o b1158 b4  T       t1158   o1016 b935 b1095 b1158 b4
2998  B       b1159   t1158  B       b1159   t1158
2999  T       t1159   o1017 b936 b1096 b1159 b4  T       t1159   o b1159 b4
3000  B       b1160   t1159  B       b1160   t1159
3001  T       t1160   o b1160 b4  S       s1160   t620 h h1096 h1091 h1097
3002  B       b1161   t1160  G       s1160   t994
3003  S       s1161   t620 h h1097 h1092 h1098  B       b1161   s1160
3004  G       s1161   t995  T       t1161   o938 b1161 b1107
3005  B       b1162   s1161  B       b1162   t1161
3006  T       t1162   o939 b1162 b1108  T       t1162   o966 b1162 b4 b1129
3007  B       b1163   t1162  B       b1163   t1162
3008  T       t1163   o967 b1163 b4 b1130  T       t1163   o936 b1163 b4
3009  B       b1164   t1163  B       b1164   t1163
3010  T       t1164   o937 b1164 b4  T       t1164   o990 b935 b1164 b4 b4
3011  B       b1165   t1164  B       b1165   t1164
3012  T       t1165   o991 b936 b1165 b4 b4  P       p1165   String "rwh unfold_fun_prop 0 thenT autoT"
3013  B       b1166   t1165  O       o1165   ext_rule p1165
3014  P       p1166   String "rwh unfold_fun_prop 0 thenT autoT"  T       t1165   o738 b966 b977
3015  O       o1166   ext_rule p1166  B       b1166   t1165 v_2
3016  T       t1166   o739 b967 b978  T       t1166   o976 b1166
3017  B       b1167   t1166 v_2  S       s1166   t620 h h1096 h1091 h1097
3018  T       t1167   o977 b1167  G       s1166   t1166
3019  S       s1167   t620 h h1097 h1092 h1098  B       b1167   s1166
3020  G       s1167   t1167  T       t1167   o938 b1167 b1107
3021  B       b1168   s1167  B       b1168   t1167
3022  T       t1168   o939 b1168 b1108  T       t1168   o973 b1168 b4 b1129
3023  B       b1169   t1168  B       b1169   t1168
 T       t1169   o974 b1169 b4 b1130  
 B       b1170   t1169  
3024  NCzf_itt_set!set        set     set Czf_itt_set  NCzf_itt_set!set        set     set Czf_itt_set
3025  O       o1170   set  O       o1169   set
3026    T       t1169   o1169
3027    H       h1169   s1_1 t1169
3028    H       h1170   s2_1 t1169
3029    P       p1170   Var s1_1
3030    O       o1170   var p1170
3031  T       t1170   o1170  T       t1170   o1170
3032  H       h1170   s1_1 t1170  B       b1170   t1170
3033  H       h1171   s2_1 t1170  P       p1171   Var s2_1
 P       p1171   Var s1_1  
3034  O       o1171   var p1171  O       o1171   var p1171
3035  T       t1171   o1171  T       t1171   o1171
3036  B       b1171   t1171  B       b1171   t1171
3037  P       p1172   Var s2_1  T       t1172   o738 b1170 b1171
3038  O       o1172   var p1172  H       h1172   x_1 t1172
3039  T       t1172   o1172  T       t1173   o738 b966 b1170
3040  B       b1172   t1172  H       h1173   x_2 t1173
3041  T       t1173   o739 b1171 b1172  T       t1174   o676 b966 b1171
3042  H       h1173   x_1 t1173  S       s1174   t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3043  T       t1174   o739 b967 b1171  G       s1174   t1174
3044  H       h1174   x_2 t1174  B       b1174   s1174
3045  T       t1175   o676 b967 b1172  T       t1175   o938 b1174 b1107
3046  S       s1175   t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174  B       b1175   t1175
3047  G       s1175   t1175  T       t1176   o738 b966 b1171
3048  B       b1175   s1175  S       s1176   t620 h h1096 h1091 h1097 h1169 h1170 h1172 h1173
3049  T       t1176   o939 b1175 b1108  G       s1176   t1176
3050  B       b1176   t1176  B       b1176   s1176
3051  T       t1177   o739 b967 b1172  T       t1177   o938 b1176 b1107
3052  S       s1177   t620 h h1097 h1092 h1098 h1170 h1171 h1173 h1174  B       b1177   t1177
 G       s1177   t1177  
 B       b1177   s1177  
 T       t1178   o939 b1177 b1108  
 B       b1178   t1178  
3053  NItt_logic      Itt_logic       Itt_logic NIL  NItt_logic      Itt_logic       Itt_logic NIL
3054  NItt_logic!implies      implies implies Itt_logic  NItt_logic!implies      implies implies Itt_logic
3055  O       o1178   implies  O       o1177   implies
3056  B       b1179   t1174  B       b1178   t1173
3057  B       b1180   t1177  B       b1179   t1176
3058  T       t1180   o1178 b1179 b1180  T       t1179   o1177 b1178 b1179
3059  S       s1180   t620 h h1097 h1092 h1098 h1170 h1171 h1173  S       s1179   t620 h h1096 h1091 h1097 h1169 h1170 h1172
3060  G       s1180   t1180  G       s1179   t1179
3061  B       b1181   s1180  B       b1180   s1179
3062  T       t1181   o939 b1181 b1108  T       t1180   o938 b1180 b1107
3063  B       b1182   t1181  B       b1181   t1180
3064  B       b1183   t1173  B       b1182   t1172
3065  B       b1184   t1180  B       b1183   t1179
3066  T       t1184   o1178 b1183 b1184  T       t1183   o1177 b1182 b1183
3067  S       s1184   t620 h h1097 h1092 h1098 h1170 h1171  S       s1183   t620 h h1096 h1091 h1097 h1169 h1170
3068  G       s1184   t1184  G       s1183   t1183
3069  B       b1185   s1184  B       b1184   s1183
3070  T       t1185   o939 b1185 b1108  T       t1184   o938 b1184 b1107
3071  B       b1186   t1185  B       b1185   t1184
3072  NItt_logic!all  all     all Itt_logic  NItt_logic!all  all     all Itt_logic
3073  O       o1186   all  O       o1185   all
3074  B       b1187   t1170  B       b1186   t1169
3075  B       b1188   t1184 s2_1  B       b1187   t1183 s2_1
3076  T       t1188   o1186 b1187 b1188  T       t1187   o1185 b1186 b1187
3077  S       s1188   t620 h h1097 h1092 h1098 h1170  S       s1187   t620 h h1096 h1091 h1097 h1169
3078  G       s1188   t1188  G       s1187   t1187
3079  B       b1189   s1188  B       b1188   s1187
3080  T       t1189   o939 b1189 b1108  T       t1188   o938 b1188 b1107
3081  B       b1190   t1189  B       b1189   t1188
3082  B       b1191   t1188 s1_1  B       b1190   t1187 s1_1
3083  T       t1191   o1186 b1187 b1191  T       t1190   o1185 b1186 b1190
3084  S       s1191   t620 h h1097 h1092 h1098  S       s1190   t620 h h1096 h1091 h1097
3085  G       s1191   t1191  G       s1190   t1190
3086  B       b1192   s1191  B       b1191   s1190
3087  T       t1192   o939 b1192 b1108  T       t1191   o938 b1191 b1107
3088    B       b1192   t1191
3089    T       t1192   o2 b1169
3090  B       b1193   t1192  B       b1193   t1192
3091  T       t1193   o2 b1170  T       t1193   o973 b1192 b983 b1193
3092  B       b1194   t1193  B       b1194   t1193
3093  T       t1194   o974 b1193 b984 b1194  T       t1194   o2 b1194
3094  B       b1195   t1194  B       b1195   t1194
3095  T       t1195   o2 b1195  T       t1195   o937 b1189 b983 b1195
3096  B       b1196   t1195  B       b1196   t1195
3097  T       t1196   o938 b1190 b984 b1196  T       t1196   o2 b1196
3098  B       b1197   t1196  B       b1197   t1196
3099  T       t1197   o2 b1197  T       t1197   o937 b1185 b983 b1197
3100  B       b1198   t1197  B       b1198   t1197
3101  T       t1198   o938 b1186 b984 b1198  T       t1198   o2 b1198
3102  B       b1199   t1198  B       b1199   t1198
3103  T       t1199   o2 b1199  T       t1199   o937 b1181 b983 b1199
3104  B       b1200   t1199  B       b1200   t1199
3105  T       t1200   o938 b1182 b984 b1200  T       t1200   o2 b1200
3106  B       b1201   t1200  B       b1201   t1200
3107  T       t1201   o2 b1201  T       t1201   o937 b1177 b983 b1201
3108  B       b1202   t1201  B       b1202   t1201
3109  T       t1202   o938 b1178 b984 b1202  T       t1202   o2 b1202
3110  B       b1203   t1202  B       b1203   t1202
3111  T       t1203   o2 b1203  T       t1203   o937 b1175 b4 b1203
3112  B       b1204   t1203  B       b1204   t1203
3113  T       t1204   o938 b1176 b4 b1204  T       t1204   o b1204 b4
3114  B       b1205   t1204  B       b1205   t1204
3115  T       t1205   o b1205 b4  T       t1205   o936 b1169 b1205
3116  B       b1206   t1205  B       b1206   t1205
3117  T       t1206   o937 b1170 b1206  P       p1206   String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"
3118    O       o1206   ext_rule p1206
3119    T       t1206   o936 b1204 b4
3120  B       b1207   t1206  B       b1207   t1206
3121  P       p1207   String "rwh unfold_equal 7 thenT rwh unfold_equal 8 thenT eqSetTransT << 's1_1 >> thenT autoT"  T       t1207   o1206 b935 b1207 b4 b4
 O       o1207   ext_rule p1207  
 T       t1207   o937 b1205 b4  
3122  B       b1208   t1207  B       b1208   t1207
3123  T       t1208   o1207 b936 b1208 b4 b4  T       t1208   o b1208 b4
3124  B       b1209   t1208  B       b1209   t1208
3125  T       t1209   o b1209 b4  T       t1209   o1165 b935 b1206 b1209 b4
3126  B       b1210   t1209  B       b1210   t1209
3127  T       t1210   o1166 b936 b1207 b1210 b4  T       t1210   o b1210 b4
3128  B       b1211   t1210  B       b1211   t1210
3129  T       t1211   o b1211 b4  T       t1211   o b1165 b1211
3130  B       b1212   t1211  B       b1212   t1211
3131  T       t1212   o b1166 b1212  T       t1212   o1095 b935 b1095 b1160 b1212
3132  B       b1213   t1212  B       b1213   t1212
3133  T       t1213   o1096 b936 b1096 b1161 b1213  T       t1213   o b1213 b4
3134  B       b1214   t1213  B       b1214   t1213
3135  T       t1214   o b1214 b4  S       s1214   t620 h h1096 h1091
3136  B       b1215   t1214  G       s1214   t967
3137  S       s1215   t620 h h1097 h1092  B       b1215   s1214
3138  G       s1215   t968  T       t1215   o938 b1215 b1107
3139  B       b1216   s1215  B       b1216   t1215
3140  T       t1216   o939 b1216 b1108  T       t1216   o966 b1216 b4 b1127
3141  B       b1217   t1216  B       b1217   t1216
3142  T       t1217   o967 b1217 b4 b1128  T       t1217   o936 b1217 b4
3143  B       b1218   t1217  B       b1218   t1217
3144  T       t1218   o937 b1218 b4  T       t1218   o990 b935 b1218 b4 b4
3145  B       b1219   t1218  B       b1219   t1218
3146  T       t1219   o991 b936 b1219 b4 b4  P       p1219   Var v_1
3147    O       o1219   var p1219
3148    T       t1219   o1219
3149  B       b1220   t1219  B       b1220   t1219
3150  P       p1220   Var v_1  T       t1220   o738 b1220 b949
3151  O       o1220   var p1220  B       b1221   t1220 v_1
3152  T       t1220   o1220  T       t1221   o976 b1221
3153  B       b1221   t1220  S       s1221   t620 h h1096 h1091
3154  T       t1221   o739 b1221 b950  G       s1221   t1221
3155  B       b1222   t1221 v_1  B       b1222   s1221
3156  T       t1222   o977 b1222  T       t1222   o938 b1222 b1107
3157  S       s1222   t620 h h1097 h1092  B       b1223   t1222
3158  G       s1222   t1222  T       t1223   o973 b1223 b4 b1127
 B       b1223   s1222  
 T       t1223   o939 b1223 b1108  
3159  B       b1224   t1223  B       b1224   t1223
3160  T       t1224   o974 b1224 b4 b1128  H       h1224   s2 t1169
3161  B       b1225   t1224  T       t1224   o738 b1170 b561
3162  H       h1225   s2 t1170  H       h1225   x_1 t1224
3163  T       t1225   o739 b1171 b561  T       t1225   o738 b1170 b949
3164  H       h1226   x_1 t1225  H       h1226   x_2 t1225
3165  T       t1226   o739 b1171 b950  T       t1226   o676 b561 b949
3166  H       h1227   x_2 t1226  S       s1226   t620 h h1096 h1091 h1169 h1224 h1225 h1226
3167  T       t1227   o676 b561 b950  G       s1226   t1226
3168  S       s1227   t620 h h1097 h1092 h1170 h1225 h1226 h1227  B       b1226   s1226
3169  G       s1227   t1227  T       t1227   o938 b1226 b1107
3170  B       b1227   s1227  B       b1227   t1227
3171  T       t1228   o939 b1227 b1108  T       t1228   o738 b561 b949
3172  B       b1228   t1228  S       s1228   t620 h h1096 h1091 h1169 h1224 h1225 h1226
3173  T       t1229   o739 b561 b950  G       s1228   t1228
3174  S       s1229   t620 h h1097 h1092 h1170 h1225 h1226 h1227  B       b1228   s1228
3175  G       s1229   t1229  T       t1229   o938 b1228 b1107
3176  B       b1229   s1229  B       b1229   t1229
3177  T       t1230   o939 b1229 b1108  B       b1230   t1225
3178  B       b1230   t1230  B       b1231   t1228
3179  B       b1231   t1226  T       t1231   o1177 b1230 b1231
3180  B       b1232   t1229  S       s1231   t620 h h1096 h1091 h1169 h1224 h1225
3181  T       t1232   o1178 b1231 b1232  G       s1231   t1231
3182  S       s1232   t620 h h1097 h1092 h1170 h1225 h1226  B       b1232   s1231
3183  G       s1232   t1232  T       t1232   o938 b1232 b1107
3184  B       b1233   s1232  B       b1233   t1232
3185  T       t1233   o939 b1233 b1108  B       b1234   t1224
3186  B       b1234   t1233  B       b1235   t1231
3187  B       b1235   t1225  T       t1235   o1177 b1234 b1235
3188  B       b1236   t1232  S       s1235   t620 h h1096 h1091 h1169 h1224
3189  T       t1236   o1178 b1235 b1236  G       s1235   t1235
3190  S       s1236   t620 h h1097 h1092 h1170 h1225  B       b1236   s1235
3191  G       s1236   t1236  T       t1236   o938 b1236 b1107
3192  B       b1237   s1236  B       b1237   t1236
3193  T       t1237   o939 b1237 b1108  B       b1238   t1235 s2
3194  B       b1238   t1237  T       t1238   o1185 b1186 b1238
3195  B       b1239   t1236 s2  S       s1238   t620 h h1096 h1091 h1169
3196  T       t1239   o1186 b1187 b1239  G       s1238   t1238
3197  S       s1239   t620 h h1097 h1092 h1170  B       b1239   s1238
3198  G       s1239   t1239  T       t1239   o938 b1239 b1107
3199  B       b1240   s1239  B       b1240   t1239
3200  T       t1240   o939 b1240 b1108  B       b1241   t1238 s1_1
3201  B       b1241   t1240  T       t1241   o1185 b1186 b1241
3202  B       b1242   t1239 s1_1  S       s1241   t620 h h1096 h1091
3203  T       t1242   o1186 b1187 b1242  G       s1241   t1241
3204  S       s1242   t620 h h1097 h1092  B       b1242   s1241
3205  G       s1242   t1242  T       t1242   o938 b1242 b1107
3206  B       b1243   s1242  B       b1243   t1242
3207  T       t1243   o939 b1243 b1108  T       t1243   o2 b1224
3208  B       b1244   t1243  B       b1244   t1243
3209  T       t1244   o2 b1225  T       t1244   o973 b1243 b983 b1244
3210  B       b1245   t1244  B       b1245   t1244
3211  T       t1245   o974 b1244 b984 b1245  T       t1245   o2 b1245
3212  B       b1246   t1245  B       b1246   t1245
3213  T       t1246   o2 b1246  T       t1246   o937 b1240 b983 b1246
3214  B       b1247   t1246  B       b1247   t1246
3215  T       t1247   o938 b1241 b984 b1247  T       t1247   o2 b1247
3216  B       b1248   t1247  B       b1248   t1247
3217  T       t1248   o2 b1248  T       t1248   o937 b1237 b983 b1248
3218  B       b1249   t1248  B       b1249   t1248
3219  T       t1249   o938 b1238 b984 b1249  T       t1249   o2 b1249
3220  B       b1250   t1249  B       b1250   t1249
3221  T       t1250   o2 b1250  T       t1250   o937 b1233 b983 b1250
3222  B       b1251   t1250  B       b1251   t1250
3223  T       t1251   o938 b1234 b984 b1251  T       t1251   o2 b1251
3224  B       b1252   t1251  B       b1252   t1251
3225  T       t1252   o2 b1252  T       t1252   o937 b1229 b983 b1252
3226  B       b1253   t1252  B       b1253   t1252
3227  T       t1253   o938 b1230 b984 b1253  T       t1253   o2 b1253
3228  B       b1254   t1253  B       b1254   t1253
3229  T       t1254   o2 b1254  T       t1254   o937 b1227 b4 b1254
3230  B       b1255   t1254  B       b1255   t1254
3231  T       t1255   o938 b1228 b4 b1255  T       t1255   o b1255 b4
3232  B       b1256   t1255  B       b1256   t1255
3233  T       t1256   o b1256 b4  T       t1256   o936 b1224 b1256
3234  B       b1257   t1256  B       b1257   t1256
3235  T       t1257   o937 b1225 b1257  P       p1257   String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"
3236    O       o1257   ext_rule p1257
3237    T       t1257   o936 b1255 b4
3238  B       b1258   t1257  B       b1258   t1257
3239  P       p1258   String "rwh unfold_equal 6 thenT rwh unfold_equal 7 thenT eqSetTransT << 's1_1 >> thenT autoT thenT eqSetSymT thenT autoT"  T       t1258   o1257 b935 b1258 b4 b4
 O       o1258   ext_rule p1258  
 T       t1258   o937 b1256 b4  
3240  B       b1259   t1258  B       b1259   t1258
3241  T       t1259   o1258 b936 b1259 b4 b4  T       t1259   o b1259 b4
3242  B       b1260   t1259  B       b1260   t1259
3243  T       t1260   o b1260 b4  T       t1260   o1165 b935 b1257 b1260 b4
3244  B       b1261   t1260  B       b1261   t1260
3245  T       t1261   o1166 b936 b1258 b1261 b4  T       t1261   o b1261 b4
3246  B       b1262   t1261  B       b1262   t1261
3247  T       t1262   o b1262 b4  T       t1262   o b1219 b1262
3248  B       b1263   t1262  B       b1263   t1262
3249  T       t1263   o b1220 b1263  T       t1263   o1091 b935 b1095 b1214 b1263
3250  B       b1264   t1263  B       b1264   t1263
3251  T       t1264   o1092 b936 b1096 b1215 b1264  P       p1264   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"
3252  B       b1265   t1264  O       o1264   ext_rule p1264
3253  P       p1265   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's2}}; op{op{inv{'s1}; 's1}; 's2}} >> 5 thenT autoT"  H       h1264   y_1 t642
3254  O       o1265   ext_rule p1265  T       t1264   o620 b695
3255  H       h1265   y_1 t642  H       h1265   z_1 t1264
3256  T       t1265   o620 b695  T       t1265   o676 b562 b695
3257  H       h1266   z_1 t1265  H       h1266   z t1265
3258  T       t1266   o676 b562 b695  T       t1266   o676 b948 b949
3259  H       h1267   z t1266  H       h1267   v t1266
3260  T       t1267   o676 b949 b950  T       t1267   o676 b561 b674
3261  H       h1268   v t1267  S       s1267   t620 h h1264 h1265 h1266 h1267
3262  T       t1268   o676 b561 b674  G       s1267   t1267
3263  S       s1268   t620 h h1265 h1266 h1267 h1268  B       b1267   s1267
3264  G       s1268   t1268  T       t1268   o938 b1267 b1107
3265  B       b1268   s1268  B       b1268   t1268
3266  T       t1269   o939 b1268 b1108  S       s1268   t620 h h1264 h1265 h1266 h1267
3267  B       b1269   t1269  G       s1268   t925
3268  S       s1269   t620 h h1265 h1266 h1267 h1268  B       b1269   s1268
3269  G       s1269   t926  T       t1269   o938 b1269 b1107
3270  B       b1270   s1269  B       b1270   t1269
 T       t1270   o939 b1270 b1108  
 B       b1271   t1270  
3271  NItt_logic!and  and     and Itt_logic  NItt_logic!and  and     and Itt_logic
3272  O       o1271   and  O       o1270   and
3273  B       b1272   t642  B       b1271   t642
3274  B       b1273   t1265  B       b1272   t1264
3275  T       t1273   o1271 b1272 b1273  T       t1272   o1270 b1271 b1272
3276  H       h1273   y t1273  H       h1272   y t1272
3277  S       s1273   t620 h h1273 h1267 h1268  S       s1272   t620 h h1272 h1266 h1267
3278  G       s1273   t926  G       s1272   t925
3279  B       b1274   s1273  B       b1273   s1272
3280  T       t1274   o939 b1274 b1108  T       t1273   o938 b1273 b1107
3281  B       b1275   t1274  B       b1274   t1273
3282  B       b1276   t1273  B       b1275   t1272
3283  B       b1277   t1266  B       b1276   t1265
3284  T       t1277   o1271 b1276 b1277  T       t1276   o1270 b1275 b1276
3285  H       h1277   x t1277  H       h1276   x t1276
3286  S       s1277   t620 h h1277 h1268  S       s1276   t620 h h1276 h1267
3287  G       s1277   t926  G       s1276   t925
3288  B       b1278   s1277  B       b1277   s1276
3289  T       t1278   o939 b1278 b1108  T       t1277   o938 b1277 b1107
3290  B       b1279   t1278  B       b1278   t1277
3291  S       s1279   t620 h h1277  S       s1278   t620 h h1276
3292  G       s1279   t926  G       s1278   t925
3293  B       b1280   s1279  B       b1279   s1278
3294  T       t1280   o939 b1280 b1108  T       t1279   o938 b1279 b1107
3295    B       b1280   t1279
3296    T       t1280   o937 b1280 b4 b1125
3297  B       b1281   t1280  B       b1281   t1280
3298  T       t1281   o938 b1281 b4 b1126  T       t1281   o2 b1281
3299  B       b1282   t1281  B       b1282   t1281
3300  T       t1282   o2 b1282  T       t1282   o937 b1278 b4 b1282
3301  B       b1283   t1282  B       b1283   t1282
3302  T       t1283   o938 b1279 b4 b1283  T       t1283   o2 b1283
3303  B       b1284   t1283  B       b1284   t1283
3304  T       t1284   o2 b1284  T       t1284   o937 b1274 b4 b1284
3305  B       b1285   t1284  B       b1285   t1284
3306  T       t1285   o938 b1275 b4 b1285  T       t1285   o2 b1285
3307  B       b1286   t1285  B       b1286   t1285
3308  T       t1286   o2 b1286  T       t1286   o937 b1270 b983 b1286
3309  B       b1287   t1286  B       b1287   t1286
3310  T       t1287   o938 b1271 b984 b1287  T       t1287   o2 b1287
3311  B       b1288   t1287  B       b1288   t1287
3312  T       t1288   o2 b1288  T       t1288   o937 b1268 b4 b1288
3313  B       b1289   t1288  B       b1289   t1288
3314  T       t1289   o938 b1269 b4 b1289  T       t1289   o676 b966 b949
3315  B       b1290   t1289  H       h1289   v_1 t1289
3316  T       t1290   o676 b967 b950  S       s1289   t620 h h1264 h1265 h1266 h1267 h1289
3317  H       h1290   v_1 t1290  G       s1289   t1267
3318  S       s1290   t620 h h1265 h1266 h1267 h1268 h1290  B       b1290   s1289
3319  G       s1290   t1268  T       t1290   o938 b1290 b1107
3320  B       b1291   s1290  B       b1291   t1290
3321  T       t1291   o939 b1291 b1108  T       t1291   o2 b1289
3322  B       b1292   t1291  B       b1292   t1291
3323  T       t1292   o2 b1290  T       t1292   o937 b1291 b4 b1292
3324  B       b1293   t1292  B       b1293   t1292
3325  T       t1293   o938 b1292 b4 b1293  B       b1294   t949 v_1
3326  B       b1294   t1293  T       t1294   o711 b1294
3327  B       b1295   t950 v_1  S       s1294   t620 h h1264 h1265 h1266 h1267
3328  T       t1295   o712 b1295  G       s1294   t1294
3329  S       s1295   t620 h h1265 h1266 h1267 h1268  B       b1295   s1294
3330  G       s1295   t1295  T       t1295   o938 b1295 b1107
3331  B       b1296   s1295  B       b1296   t1295
3332  T       t1296   o939 b1296 b1108  T       t1296   o676 b1220 b949
3333  B       b1297   t1296  B       b1297   t1296 v_1
3334  T       t1297   o676 b1221 b950  T       t1297   o976 b1297
3335  B       b1298   t1297 v_1  S       s1297   t620 h h1264 h1265 h1266 h1267
3336  T       t1298   o977 b1298  G       s1297   t1297
3337  S       s1298   t620 h h1265 h1266 h1267 h1268  B       b1298   s1297
3338  G       s1298   t1298  T       t1298   o938 b1298 b1107
3339  B       b1299   s1298  B       b1299   t1298
3340  T       t1299   o939 b1299 b1108  T       t1299   o973 b1299 b983 b1292
3341  B       b1300   t1299  B       b1300   t1299
3342  T       t1300   o974 b1300 b984 b1293  T       t1300   o2 b1300
3343  B       b1301   t1300  B       b1301   t1300
3344  T       t1301   o2 b1301  T       t1301   o973 b1296 b4 b1301
3345  B       b1302   t1301  B       b1302   t1301
3346  T       t1302   o974 b1297 b4 b1302  T       t1302   o b1302 b4
3347  B       b1303   t1302  B       b1303   t1302
3348  T       t1303   o b1303 b4  T       t1303   o b1293 b1303
3349  B       b1304   t1303  B       b1304   t1303
3350  T       t1304   o b1294 b1304  T       t1304   o936 b1289 b1304
3351  B       b1305   t1304  B       b1305   t1304
3352  T       t1305   o937 b1290 b1305  P       p1305   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"
3353  B       b1306   t1305  O       o1305   ext_rule p1305
3354  P       p1306   String "setSubstT << equal{op{inv{'s1}; op{'s1; 's3}}; op{op{inv{'s1}; 's1}; 's3}} >> 6 thenT autoT"  T       t1305   o676 b966 b993
3355  O       o1306   ext_rule p1306  H       h1305   v_2 t1305
3356  T       t1306   o676 b967 b994  S       s1305   t620 h h1264 h1265 h1266 h1267 h1289 h1305
3357  H       h1306   v_2 t1306  G       s1305   t1267
3358  S       s1306   t620 h h1265 h1266 h1267 h1268 h1290 h1306  B       b1306   s1305
3359  G       s1306   t1268  T       t1306   o938 b1306 b1107
3360  B       b1307   s1306  B       b1307   t1306
3361  T       t1307   o939 b1307 b1108  T       t1307   o2 b1293
3362  B       b1308   t1307  B       b1308   t1307
3363  T       t1308   o2 b1294  T       t1308   o937 b1307 b4 b1308
3364  B       b1309   t1308  B       b1309   t1308
3365  T       t1309   o938 b1308 b4 b1309  B       b1310   t966 v_2
3366  B       b1310   t1309  T       t1310   o711 b1310
3367  B       b1311   t967 v_2  S       s1310   t620 h h1264 h1265 h1266 h1267 h1289
3368  T       t1311   o712 b1311  G       s1310   t1310
3369  S       s1311   t620 h h1265 h1266 h1267 h1268 h1290  B       b1311   s1310
3370  G       s1311   t1311  T       t1311   o938 b1311 b1107
3371  B       b1312   s1311  B       b1312   t1311
3372  T       t1312   o939 b1312 b1108  T       t1312   o676 b966 b977
3373  B       b1313   t1312  B       b1313   t1312 v_2
3374  T       t1313   o676 b967 b978  T       t1313   o976 b1313
3375  B       b1314   t1313 v_2  S       s1313   t620 h h1264 h1265 h1266 h1267 h1289
3376  T       t1314   o977 b1314  G       s1313   t1313
3377  S       s1314   t620 h h1265 h1266 h1267 h1268 h1290  B       b1314   s1313
3378  G       s1314   t1314  T       t1314   o938 b1314 b1107
3379  B       b1315   s1314  B       b1315   t1314
3380  T       t1315   o939 b1315 b1108  T       t1315   o973 b1315 b983 b1308
3381  B       b1316   t1315  B       b1316   t1315
3382  T       t1316   o974 b1316 b984 b1309  T       t1316   o2 b1316
3383  B       b1317   t1316  B       b1317   t1316
3384  T       t1317   o2 b1317  T       t1317   o973 b1312 b4 b1317
3385  B       b1318   t1317  B       b1318   t1317
3386  T       t1318   o974 b1313 b4 b1318  T       t1318   o b1318 b4
3387  B       b1319   t1318  B       b1319   t1318
3388  T       t1319   o b1319 b4  T       t1319   o b1309 b1319
3389  B       b1320   t1319  B       b1320   t1319
3390  T       t1320   o b1310 b1320  T       t1320   o936 b1293 b1320
3391  B       b1321   t1320  B       b1321   t1320
3392  T       t1321   o937 b1294 b1321  P       p1321   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"
3393  B       b1322   t1321  O       o1321   ext_rule p1321
3394  P       p1322   String "setSubstT << equal{op{inv{'s1}; 's1}; id} >> 7 thenT autoT"  T       t1321   o676 b1017 b1018
3395  O       o1322   ext_rule p1322  H       h1321   v_3 t1321
3396  T       t1322   o676 b1018 b1019  S       s1321   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3397  H       h1322   v_3 t1322  G       s1321   t1267
3398  S       s1322   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322  B       b1322   s1321
3399  G       s1322   t1268  T       t1322   o938 b1322 b1107
3400  B       b1323   s1322  B       b1323   t1322
3401  T       t1323   o939 b1323 b1108  T       t1323   o2 b1309
3402  B       b1324   t1323  B       b1324   t1323
3403  T       t1324   o2 b1310  T       t1324   o937 b1323 b4 b1324
3404  B       b1325   t1324  B       b1325   t1324
3405  T       t1325   o938 b1324 b4 b1325  T       t1325   o b1325 b4
3406  B       b1326   t1325  B       b1326   t1325
3407  T       t1326   o b1326 b4  T       t1326   o936 b1309 b1326
3408  B       b1327   t1326  B       b1327   t1326
3409  T       t1327   o937 b1310 b1327  P       p1327   String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"
3410  B       b1328   t1327  O       o1327   ext_rule p1327
3411  P       p1328   String "setSubstT << equal{op{id; 's2}; 's2} >> 8 thenT autoT"  T       t1327   o676 b561 b1018
3412  O       o1328   ext_rule p1328  H       h1327   v_4 t1327
3413  T       t1328   o676 b561 b1019  S       s1327   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1327
3414  H       h1328   v_4 t1328  G       s1327   t1267
3415  S       s1328   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1328  B       b1328   s1327
3416  G       s1328   t1268  T       t1328   o938 b1328 b1107
3417  B       b1329   s1328  B       b1329   t1328
3418  T       t1329   o939 b1329 b1108  T       t1329   o2 b1325
3419  B       b1330   t1329  B       b1330   t1329
3420  T       t1330   o2 b1326  T       t1330   o937 b1329 b4 b1330
3421  B       b1331   t1330  B       b1331   t1330
3422  T       t1331   o938 b1330 b4 b1331  S       s1331   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3423  B       b1332   t1331  G       s1331   t1144
3424  S       s1332   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322  B       b1332   s1331
3425  G       s1332   t1145  T       t1332   o938 b1332 b1107
3426  B       b1333   s1332  B       b1333   t1332
3427  T       t1333   o939 b1333 b1108  T       t1333   o676 b1147 b1018
3428  B       b1334   t1333  B       b1334   t1333 v_4
3429  T       t1334   o676 b1148 b1019  T       t1334   o976 b1334
3430  B       b1335   t1334 v_4  S       s1334   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3431  T       t1335   o977 b1335  G       s1334   t1334
3432  S       s1335   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322  B       b1335   s1334
3433  G       s1335   t1335  T       t1335   o938 b1335 b1107
3434  B       b1336   s1335  B       b1336   t1335
3435  T       t1336   o939 b1336 b1108  T       t1336   o973 b1336 b983 b1330
3436  B       b1337   t1336  B       b1337   t1336
3437  T       t1337   o974 b1337 b984 b1331  T       t1337   o2 b1337
3438  B       b1338   t1337  B       b1338   t1337
3439  T       t1338   o2 b1338  T       t1338   o973 b1333 b4 b1338
3440  B       b1339   t1338  B       b1339   t1338
3441  T       t1339   o974 b1334 b4 b1339  T       t1339   o b1339 b4
3442  B       b1340   t1339  B       b1340   t1339
3443  T       t1340   o b1340 b4  T       t1340   o b1331 b1340
3444  B       b1341   t1340  B       b1341   t1340
3445  T       t1341   o b1332 b1341  T       t1341   o936 b1325 b1341
3446  B       b1342   t1341  B       b1342   t1341
3447  T       t1342   o937 b1326 b1342  P       p1342   String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"
3448    O       o1342   ext_rule p1342
3449    T       t1342   o936 b1331 b4
3450  B       b1343   t1342  B       b1343   t1342
3451  P       p1343   String "setSubstT << equal{op{id; 's3}; 's3} >> 9 thenT autoT"  T       t1343   o1342 b935 b1343 b4 b4
 O       o1343   ext_rule p1343  
 T       t1343   o937 b1332 b4  
3452  B       b1344   t1343  B       b1344   t1343
3453  T       t1344   o1343 b936 b1344 b4 b4  H       h1344   s1 t1169
3454  B       b1345   t1344  T       t1344   o738 b560 b561
3455  H       h1345   s1 t1170  H       h1345   x t1344
3456  T       t1345   o739 b560 b561  T       t1345   o738 b1018 b1018
3457  H       h1346   x t1345  S       s1345   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344 h1224 h1345
3458  T       t1346   o739 b1019 b1019  G       s1345   t1345
3459  S       s1346   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345 h1225 h1346  B       b1345   s1345
3460  G       s1346   t1346  T       t1346   o938 b1345 b1107
3461  B       b1346   s1346  B       b1346   t1346
3462  T       t1347   o939 b1346 b1108  B       b1347   t1344
 B       b1347   t1347  
3463  B       b1348   t1345  B       b1348   t1345
3464  B       b1349   t1346  T       t1348   o1177 b1347 b1348
3465  T       t1349   o1178 b1348 b1349  S       s1348   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344 h1224
3466  S       s1349   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345 h1225  G       s1348   t1348
3467  G       s1349   t1349  B       b1349   s1348
3468  B       b1350   s1349  T       t1349   o938 b1349 b1107
3469  T       t1350   o939 b1350 b1108  B       b1350   t1349
3470  B       b1351   t1350  B       b1351   t1348 s2
3471  B       b1352   t1349 s2  T       t1351   o1185 b1186 b1351
3472  T       t1352   o1186 b1187 b1352  S       s1351   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321 h1344
3473  S       s1352   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322 h1345  G       s1351   t1351
3474  G       s1352   t1352  B       b1352   s1351
3475  B       b1353   s1352  T       t1352   o938 b1352 b1107
3476  T       t1353   o939 b1353 b1108  B       b1353   t1352
3477  B       b1354   t1353  B       b1354   t1351 s1
3478  B       b1355   t1352 s1  T       t1354   o1185 b1186 b1354
3479  T       t1355   o1186 b1187 b1355  S       s1354   t620 h h1264 h1265 h1266 h1267 h1289 h1305 h1321
3480  S       s1355   t620 h h1265 h1266 h1267 h1268 h1290 h1306 h1322  G       s1354   t1354
3481  G       s1355   t1355  B       b1355   s1354
3482  B       b1356   s1355  T       t1355   o938 b1355 b1107
3483  T       t1356   o939 b1356 b1108  B       b1356   t1355
3484    T       t1356   o2 b1339
3485  B       b1357   t1356  B       b1357   t1356
3486  T       t1357   o2 b1340  T       t1357   o973 b1356 b983 b1357
3487  B       b1358   t1357  B       b1358   t1357
3488  T       t1358   o974 b1357 b984 b1358  T       t1358   o2 b1358
3489  B       b1359   t1358  B       b1359   t1358
3490  T       t1359   o2 b1359  T       t1359   o937 b1353 b983 b1359
3491  B       b1360   t1359  B       b1360   t1359
3492  T       t1360   o938 b1354 b984 b1360  T       t1360   o2 b1360
3493  B       b1361   t1360  B       b1361   t1360
3494  T       t1361   o2 b1361  T       t1361   o937 b1350 b983 b1361
3495  B       b1362   t1361  B       b1362   t1361
3496  T       t1362   o938 b1351 b984 b1362  T       t1362   o2 b1362
3497  B       b1363   t1362  B       b1363   t1362
3498  T       t1363   o2 b1363  T       t1363   o937 b1346 b4 b1363
3499  B       b1364   t1363  B       b1364   t1363
3500  T       t1364   o938 b1347 b4 b1364  T       t1364   o b1364 b4
3501  B       b1365   t1364  B       b1365   t1364
3502  T       t1365   o b1365 b4  T       t1365   o936 b1339 b1365
3503  B       b1366   t1365  B       b1366   t1365
3504  T       t1366   o937 b1340 b1366  T       t1366   o1085 b1364
3505  B       b1367   t1366  B       b1367   t1366
3506  T       t1367   o1086 b1365  T       t1367   o b1367 b4
3507  B       b1368   t1367  B       b1368   t1367
3508  T       t1368   o b1368 b4  T       t1368   o1071 b935 b1366 b1368 b4
3509  B       b1369   t1368  B       b1369   t1368
3510  T       t1369   o1072 b936 b1367 b1369 b4  T       t1369   o b1369 b4
3511  B       b1370   t1369  B       b1370   t1369
3512  T       t1370   o b1370 b4  T       t1370   o b1344 b1370
3513  B       b1371   t1370  B       b1371   t1370
3514  T       t1371   o b1345 b1371  T       t1371   o1327 b935 b1342 b1371 b4
3515  B       b1372   t1371  B       b1372   t1371
3516  T       t1372   o1328 b936 b1343 b1372 b4  T       t1372   o b1372 b4
3517  B       b1373   t1372  B       b1373   t1372
3518  T       t1373   o b1373 b4  T       t1373   o1321 b935 b1327 b1373 b4
3519  B       b1374   t1373  B       b1374   t1373
3520  T       t1374   o1322 b936 b1328 b1374 b4  T       t1374   o936 b1318 b4
3521  B       b1375   t1374  B       b1375   t1374
3522  T       t1375   o937 b1319 b4  T       t1375   o1071 b935 b1375 b4 b4
3523  B       b1376   t1375  B       b1376   t1375
3524  T       t1376   o1072 b936 b1376 b4 b4  T       t1376   o b1376 b4
3525  B       b1377   t1376  B       b1377   t1376
3526  T       t1377   o b1377 b4  T       t1377   o b1374 b1377
3527  B       b1378   t1377  B       b1378   t1377
3528  T       t1378   o b1375 b1378  P       p1378   String "eqSetSymT thenT autoT"
3529  B       b1379   t1378  O       o1378   ext_rule p1378
3530  P       p1379   String "eqSetSymT thenT autoT"  T       t1378   o676 b949 b993
3531  O       o1379   ext_rule p1379  S       s1378   t620 h h1264 h1265 h1266 h1267 h1289
3532  T       t1379   o676 b950 b994  G       s1378   t1378
3533  S       s1379   t620 h h1265 h1266 h1267 h1268 h1290  B       b1379   s1378
3534  G       s1379   t1379  T       t1379   o938 b1379 b1107
3535  B       b1380   s1379  B       b1380   t1379
3536  T       t1380   o939 b1380 b1108  S       s1380   t620 h h1264 h1265 h1266 h1267 h1289
3537  B       b1381   t1380  G       s1380   t994
3538  S       s1381   t620 h h1265 h1266 h1267 h1268 h1290  B       b1381   s1380
3539  G       s1381   t995  T       t1381   o938 b1381 b1107
3540  B       b1382   s1381  B       b1382   t1381
3541  T       t1382   o939 b1382 b1108  T       t1382   o966 b1382 b983 b1308
3542  B       b1383   t1382  B       b1383   t1382
3543  T       t1383   o967 b1383 b984 b1309  T       t1383   o2 b1383
3544  B       b1384   t1383  B       b1384   t1383
3545  T       t1384   o2 b1384  T       t1384   o966 b1380 b4 b1384
3546  B       b1385   t1384  B       b1385   t1384
3547  T       t1385   o967 b1381 b4 b1385  T       t1385   o676 b993 b949
3548  B       b1386   t1385  S       s1385   t620 h h1264 h1265 h1266 h1267 h1289
3549  T       t1386   o676 b994 b950  G       s1385   t1385
3550  S       s1386   t620 h h1265 h1266 h1267 h1268 h1290  B       b1386   s1385
3551  G       s1386   t1386  T       t1386   o938 b1386 b1107
3552  B       b1387   s1386  B       b1387   t1386
3553  T       t1387   o939 b1387 b1108  T       t1387   o2 b1385
3554  B       b1388   t1387  B       b1388   t1387
3555  T       t1388   o2 b1386  T       t1388   o966 b1387 b4 b1388
3556  B       b1389   t1388  B       b1389   t1388
3557  T       t1389   o967 b1388 b4 b1389  T       t1389   o b1389 b4
3558  B       b1390   t1389  B       b1390   t1389
3559  T       t1390   o b1390 b4  T       t1390   o936 b1385 b1390
3560  B       b1391   t1390  B       b1391   t1390
3561  T       t1391   o937 b1386 b1391  T       t1391   o1085 b1389
3562  B       b1392   t1391  B       b1392   t1391
3563  T       t1392   o1086 b1390  T       t1392   o b1392 b4
3564  B       b1393   t1392  B       b1393   t1392
3565  T       t1393   o b1393 b4  T       t1393   o1378 b935 b1391 b1393 b4
3566  B       b1394   t1393  B       b1394   t1393
3567  T       t1394   o1379 b936 b1392 b1394 b4  T       t1394   o b1394 b4
3568  B       b1395   t1394  B       b1395   t1394
3569  T       t1395   o b1395 b4  T       t1395   o1305 b935 b1321 b1378 b1395
3570  B       b1396   t1395  B       b1396   t1395
3571  T       t1396   o1306 b936 b1322 b1379 b1396  T       t1396   o936 b1302 b4
3572  B       b1397   t1396  B       b1397   t1396
3573  T       t1397   o937 b1303 b4  T       t1397   o1071 b935 b1397 b4 b4
3574  B       b1398   t1397  B       b1398   t1397
3575  T       t1398   o1072 b936 b1398 b4 b4  T       t1398   o b1398 b4
3576  B       b1399   t1398  B       b1399   t1398
3577  T       t1399   o b1399 b4  T       t1399   o b1396 b1399
3578  B       b1400   t1399  B       b1400   t1399
3579  T       t1400   o b1397 b1400  T       t1400   o676 b948 b966
3580  B       b1401   t1400  S       s1400   t620 h h1264 h1265 h1266 h1267
3581  T       t1401   o676 b949 b967  G       s1400   t1400
3582  S       s1401   t620 h h1265 h1266 h1267 h1268  B       b1401   s1400
3583  G       s1401   t1401  T       t1401   o938 b1401 b1107
3584  B       b1402   s1401  B       b1402   t1401
3585  T       t1402   o939 b1402 b1108  S       s1402   t620 h h1264 h1265 h1266 h1267
3586  B       b1403   t1402  G       s1402   t967
3587  S       s1403   t620 h h1265 h1266 h1267 h1268  B       b1403   s1402
3588  G       s1403   t968  T       t1403   o938 b1403 b1107
3589  B       b1404   s1403  B       b1404   t1403
3590  T       t1404   o939 b1404 b1108  T       t1404   o966 b1404 b983 b1292
3591  B       b1405   t1404  B       b1405   t1404
3592  T       t1405   o967 b1405 b984 b1293  T       t1405   o2 b1405
3593  B       b1406   t1405  B       b1406   t1405
3594  T       t1406   o2 b1406  T       t1406   o966 b1402 b4 b1406
3595  B       b1407   t1406  B       b1407   t1406
3596  T       t1407   o967 b1403 b4 b1407  T       t1407   o676 b966 b948
3597  B       b1408   t1407  S       s1407   t620 h h1264 h1265 h1266 h1267
3598  T       t1408   o676 b967 b949  G       s1407   t1407
3599  S       s1408   t620 h h1265 h1266 h1267 h1268  B       b1408   s1407
3600  G       s1408   t1408  T       t1408   o938 b1408 b1107
3601  B       b1409   s1408  B       b1409   t1408
3602  T       t1409   o939 b1409 b1108  T       t1409   o2 b1407
3603  B       b1410   t1409  B       b1410   t1409
3604  T       t1410   o2 b1408  T       t1410   o966 b1409 b4 b1410
3605  B       b1411   t1410  B       b1411   t1410
3606  T       t1411   o967 b1410 b4 b1411  T       t1411   o b1411 b4
3607  B       b1412   t1411  B       b1412   t1411
3608  T       t1412   o b1412 b4  T       t1412   o936 b1407 b1412
3609  B       b1413   t1412  B       b1413   t1412
3610  T       t1413   o937 b1408 b1413  T       t1413   o1085 b1411
3611  B       b1414   t1413  B       b1414   t1413
3612  T       t1414   o1086 b1412  T       t1414   o b1414 b4
3613  B       b1415   t1414  B       b1415   t1414
3614  T       t1415   o b1415 b4  T       t1415   o1378 b935 b1413 b1415 b4
3615  B       b1416   t1415  B       b1416   t1415
3616  T       t1416   o1379 b936 b1414 b1416 b4  T       t1416   o b1416 b4
3617  B       b1417   t1416  B       b1417   t1416
3618  T       t1417   o b1417 b4  T       t1417   o1264 b935 b1305 b1400 b1417
3619  B       b1418   t1417  B       b1418   t1417
3620  T       t1418   o1265 b936 b1306 b1401 b1418  T       t1418   o b1418 b4
3621  B       b1419   t1418  B       b1419   t1418
3622  T       t1419   o b1419 b4  T       t1419   o b1264 b1419
3623  B       b1420   t1419  B       b1420   t1419
3624  T       t1420   o b1265 b1420  T       t1420   o b1091 b1420
3625  B       b1421   t1420  B       b1421   t1420
3626  T       t1421   o b1092 b1421  T       t1421   o934 b935 b963 b1085 b1421
3627  B       b1422   t1421  B       b1422   t1421
3628  T       t1422   o935 b936 b964 b1086 b1422  T       t1422   o933 b1422
3629  B       b1423   t1422  B       b1423   t1422
3630  T       t1423   o934 b1423  P       p1423   Number 5390
3631  B       b1424   t1423  P       p1424   Number 5398
3632  P       p1424   Number 5399  O       o1424   resource_defs p1423 p1424 p264
3633  P       p1425   Number 5407  P       p1425   Number 5396
3634  O       o1425   resource_defs p1424 p1425 p264  O       o1425   uid p1425 p1424
3635  P       p1426   Number 5405  T       t1425   o1425 b626
3636  O       o1426   uid p1426 p1425  B       b1425   t1425
3637  T       t1426   o1426 b626  T       t1426   o b1425 b4
3638  B       b1426   t1426  B       b1426   t1426
3639  T       t1427   o b1426 b4  T       t1427   o1424 b1426
3640  B       b1427   t1427  B       b1427   t1427
3641  T       t1428   o1425 b1427  T       t1428   o b1427 b4
3642  B       b1428   t1428  B       b1428   t1428
3643  T       t1429   o b1428 b4  T       t1429   o919 b922 b933 b1423 b1428
3644  B       b1429   t1429  B       b1429   t1429
3645  T       t1430   o920 b923 b934 b1424 b1429  T       t1430   o918 b1429
3646  B       b1430   t1430  B       b1430   t1430
3647  T       t1431   o919 b1430  P       p1430   Number 5838
3648  B       b1431   t1431  P       p1431   Number 6264
3649  P       p1431   Number 5847  O       o1431   location p1430 p1431
3650  P       p1432   Number 6273  P       p1432   String cancel2
3651  O       o1432   location p1431 p1432  O       o1432   rule p1432
3652  P       p1433   String cancel2  T       t1432   o920 b674
3653  O       o1433   rule p1433  B       b1432   t1432
3654  T       t1433   o921 b674  T       t1433   o b1432 b4
3655  B       b1433   t1433  B       b1433   t1433
3656  T       t1434   o b1433 b4  T       t1434   o b617 b1433
3657  B       b1434   t1434  B       b1434   t1434
3658  T       t1435   o b617 b1434  T       t1435   o738 b695 b696
3659  B       b1435   t1435  S       s1435   t620 h
3660  T       t1436   o739 b695 b696  G       s1435   t1435
3661    B       b1435   s1435
3662    T       t1436   o618 b1435
3663    B       b1436   t1436
3664  S       s1436   t620 h  S       s1436   t620 h
3665  G       s1436   t1436  G       s1436   t1344
3666  B       b1436   s1436  B       b1437   s1436
3667  T       t1437   o618 b1436  T       t1437   o618 b1437
3668  B       b1437   t1437  B       b1438   t1437
3669  S       s1437   t620 h  T       t1438   o635 b1436 b1438
 G       s1437   t1345  
 B       b1438   s1437  
 T       t1438   o618 b1438  
3670  B       b1439   t1438  B       b1439   t1438
3671  T       t1439   o635 b1437 b1439  T       t1439   o635 b738 b1439
3672  B       b1440   t1439  B       b1440   t1439
3673  T       t1440   o635 b739 b1440  T       t1440   o635 b658 b1440
3674  B       b1441   t1440  B       b1441   t1440
3675  T       t1441   o635 b658 b1441  T       t1441   o635 b656 b1441
3676  B       b1442   t1441  B       b1442   t1441
3677  T       t1442   o635 b656 b1442  T       t1442   o635 b676 b1442
3678  B       b1443   t1442  B       b1443   t1442
3679  T       t1443   o635 b676 b1443  T       t1443   o635 b641 b1443
3680  B       b1444   t1443  B       b1444   t1443
3681  T       t1444   o635 b641 b1444  T       t1444   o635 b639 b1444
3682  B       b1445   t1444  B       b1445   t1444
3683  T       t1445   o635 b639 b1445  P       p1445   String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"
3684    O       o1445   ext_rule p1445
3685    T       t1445   o b1435 b4
3686  B       b1446   t1445  B       b1446   t1445
3687  P       p1446   String "assumT 7 thenT assertT << equal{op{op{'s1; 's3}; inv{'s3}}; op{op{'s2; 's3}; inv{'s3}}} >> thenT autoT"  T       t1446   o b737 b1446
 O       o1446   ext_rule p1446  
 T       t1446   o b1436 b4  
3688  B       b1447   t1446  B       b1447   t1446
3689  T       t1447   o b738 b1447  T       t1447   o b657 b1447
3690  B       b1448   t1447  B       b1448   t1447
3691  T       t1448   o b657 b1448  T       t1448   o b655 b1448
3692  B       b1449   t1448  B       b1449   t1448
3693  T       t1449   o b655 b1449  T       t1449   o b675 b1449
3694  B       b1450   t1449  B       b1450   t1449
3695  T       t1450   o b675 b1450  T       t1450   o b640 b1450
3696  B       b1451   t1450  B       b1451   t1450
3697  T       t1451   o b640 b1451  T       t1451   o b638 b1451
3698  B       b1452   t1451  B       b1452   t1451
3699  T       t1452   o b638 b1452  T       t1452   o938 b1437 b1452
3700  B       b1453   t1452  B       b1453   t1452
3701  T       t1453   o939 b1438 b1453  T       t1453   o937 b1453 b4 b946
3702  B       b1454   t1453  B       b1454   t1453
3703  T       t1454   o938 b1454 b4 b947  H       h1454   v t1435
3704    T       t1454   o572 b674
3705  B       b1455   t1454  B       b1455   t1454
3706  H       h1455   v t1436  T       t1455   o559 b695 b1455
 T       t1455   o572 b674  
3707  B       b1456   t1455  B       b1456   t1455
3708  T       t1456   o559 b695 b1456  T       t1456   o559 b696 b1455
3709  B       b1457   t1456  B       b1457   t1456
3710  T       t1457   o559 b696 b1456  T       t1457   o738 b1456 b1457
3711  B       b1458   t1457  S       s1457   t620 h h1454
3712  T       t1458   o739 b1457 b1458  G       s1457   t1457
3713  S       s1458   t620 h h1455  B       b1458   s1457
3714  G       s1458   t1458  T       t1458   o938 b1458 b1452
3715  B       b1459   s1458  B       b1459   t1458
3716  T       t1459   o939 b1459 b1453  S       s1459   t620 h h1454
3717  B       b1460   t1459  G       s1459   t1344
3718  S       s1460   t620 h h1455  B       b1460   s1459
3719  G       s1460   t1345  T       t1460   o938 b1460 b1452
3720  B       b1461   s1460  B       b1461   t1460
3721  T       t1461   o939 b1461 b1453  T       t1461   o2 b1454
3722  B       b1462   t1461  B       b1462   t1461
3723  T       t1462   o2 b1455  T       t1462   o937 b1461 b4 b1462
3724  B       b1463   t1462  B       b1463   t1462
3725  T       t1463   o938 b1462 b4 b1463  T       t1463   o2 b1463
3726  B       b1464   t1463  B       b1464   t1463
3727  T       t1464   o2 b1464  T       t1464   o947 b1459 b4 b1464
3728  B       b1465   t1464  B       b1465   t1464
3729  T       t1465   o948 b1460 b4 b1465  H       h1465   v_1 t1457
3730  B       b1466   t1465  S       s1465   t620 h h1454 h1465
3731  H       h1466   v_1 t1458  G       s1465   t1344
3732  S       s1466   t620 h h1455 h1466  B       b1466   s1465
3733  G       s1466   t1345  T       t1466   o938 b1466 b1452
3734  B       b1467   s1466  B       b1467   t1466
3735  T       t1467   o939 b1467 b1453  T       t1467   o937 b1467 b4 b1464
3736  B       b1468   t1467  B       b1468   t1467
3737  T       t1468   o938 b1468 b4 b1465  T       t1468   o b1468 b4
3738  B       b1469   t1468  B       b1469   t1468
3739  T       t1469   o b1469 b4  T       t1469   o b1465 b1469
3740  B       b1470   t1469  B       b1470   t1469
3741  T       t1470   o b1466 b1470  T       t1470   o936 b1454 b1470
3742  B       b1471   t1470  B       b1471   t1470
3743  T       t1471   o937 b1455 b1471  T       t1471   o936 b1465 b4
3744  B       b1472   t1471  B       b1472   t1471
3745  T       t1472   o937 b1466 b4  T       t1472   o963 b935 b1472 b4 b4
3746  B       b1473   t1472  B       b1473   t1472
3747  T       t1473   o964 b936 b1473 b4 b4  P       p1473   String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"
3748    O       o1473   ext_rule p1473
3749    T       t1473   o559 b674 b1455
3750  B       b1474   t1473  B       b1474   t1473
3751  P       p1474   String "setSubstT << equal{op{op{'s1; 's3}; inv{'s3}}; op{'s1; op{'s3; inv{'s3}}}} >> 3 thenT autoT"  T       t1474   o559 b560 b1474
 O       o1474   ext_rule p1474  
 T       t1474   o559 b674 b1456  
3752  B       b1475   t1474  B       b1475   t1474
3753  T       t1475   o559 b560 b1475  T       t1475   o738 b1475 b1457
3754  B       b1476   t1475  H       h1475   v_2 t1475
3755  T       t1476   o739 b1476 b1458  S       s1475   t620 h h1454 h1465 h1475
3756  H       h1476   v_2 t1476  G       s1475   t1344
3757  S       s1476   t620 h h1455 h1466 h1476  B       b1476   s1475
3758  G       s1476   t1345  T       t1476   o938 b1476 b1452
3759  B       b1477   s1476  B       b1477   t1476
3760  T       t1477   o939 b1477 b1453  T       t1477   o2 b1468
3761  B       b1478   t1477  B       b1478   t1477
3762  T       t1478   o2 b1469  T       t1478   o937 b1477 b4 b1478
3763  B       b1479   t1478  B       b1479   t1478
3764  T       t1479   o938 b1478 b4 b1479  B       b1480   t1456 v_2
3765  B       b1480   t1479  T       t1480   o711 b1480
3766  B       b1481   t1457 v_2  S       s1480   t620 h h1454 h1465
3767  T       t1481   o712 b1481  G       s1480   t1480
3768  S       s1481   t620 h h1455 h1466  B       b1481   s1480
3769  G       s1481   t1481  T       t1481   o938 b1481 b1452
3770  B       b1482   s1481  B       b1482   t1481
3771  T       t1482   o939 b1482 b1453  T       t1482   o738 b977 b1457
3772  B       b1483   t1482  B       b1483   t1482 v_2
3773  T       t1483   o739 b978 b1458  T       t1483   o976 b1483
3774  B       b1484   t1483 v_2  S       s1483   t620 h h1454 h1465
3775  T       t1484   o977 b1484  G       s1483   t1483
3776  S       s1484   t620 h h1455 h1466  B       b1484   s1483
3777  G       s1484   t1484  T       t1484   o938 b1484 b1452
3778  B       b1485   s1484  B       b1485   t1484
3779  T       t1485   o939 b1485 b1453  T       t1485   o973 b1485 b983 b1478
3780  B       b1486   t1485  B       b1486   t1485
3781  T       t1486   o974 b1486 b984 b1479  T       t1486   o2 b1486
3782  B       b1487   t1486  B       b1487   t1486
3783  T       t1487   o2 b1487  T       t1487   o973 b1482 b4 b1487
3784  B       b1488   t1487  B       b1488   t1487
3785  T       t1488   o974 b1483 b4 b1488  T       t1488   o b1488 b4
3786  B       b1489   t1488  B       b1489   t1488
3787  T       t1489   o b1489 b4  T       t1489   o b1479 b1489
3788  B       b1490   t1489  B       b1490   t1489
3789  T       t1490   o b1480 b1490  T       t1490   o936 b1468 b1490
3790  B       b1491   t1490  B       b1491   t1490
3791  T       t1491   o937 b1469 b1491  P       p1491   String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"
3792    O       o1491   ext_rule p1491
3793    T       t1491   o559 b561 b1474
3794  B       b1492   t1491  B       b1492   t1491
3795  P       p1492   String "setSubstT << equal{op{op{'s2; 's3}; inv{'s3}}; op{'s2; op{'s3; inv{'s3}}}} >> 4 thenT autoT"  T       t1492   o738 b1475 b1492
3796  O       o1492   ext_rule p1492  H       h1492   v_3 t1492
3797  T       t1492   o559 b561 b1475  S       s1492   t620 h h1454 h1465 h1475 h1492
3798  B       b1493   t1492  G       s1492   t1344
3799  T       t1493   o739 b1476 b1493  B       b1493   s1492
3800  H       h1493   v_3 t1493  T       t1493   o938 b1493 b1452
3801  S       s1493   t620 h h1455 h1466 h1476 h1493  B       b1494   t1493
3802  G       s1493   t1345  T       t1494   o2 b1479
 B       b1494   s1493  
 T       t1494   o939 b1494 b1453  
3803  B       b1495   t1494  B       b1495   t1494
3804  T       t1495   o2 b1480  T       t1495   o937 b1494 b4 b1495
3805  B       b1496   t1495  B       b1496   t1495
3806  T       t1496   o938 b1495 b4 b1496  B       b1497   t1474 v_3
3807  B       b1497   t1496  T       t1497   o711 b1497
3808  B       b1498   t1475 v_3  S       s1497   t620 h h1454 h1465 h1475
3809  T       t1498   o712 b1498  G       s1497   t1497
3810  S       s1498   t620 h h1455 h1466 h1476  B       b1498   s1497
3811  G       s1498   t1498  T       t1498   o938 b1498 b1452
3812  B       b1499   s1498  B       b1499   t1498
3813  T       t1499   o939 b1499 b1453  T       t1499   o738 b1475 b1004
3814  B       b1500   t1499  B       b1500   t1499 v_3
3815  T       t1500   o739 b1476 b1005  T       t1500   o976 b1500
3816  B       b1501   t1500 v_3  S       s1500   t620 h h1454 h1465 h1475
3817  T       t1501   o977 b1501  G       s1500   t1500
3818  S       s1501   t620 h h1455 h1466 h1476  B       b1501   s1500
3819  G       s1501   t1501  T       t1501   o938 b1501 b1452
3820  B       b1502   s1501  B       b1502   t1501
3821  T       t1502   o939 b1502 b1453  T       t1502   o973 b1502 b983 b1495
3822  B       b1503   t1502  B       b1503   t1502
3823  T       t1503   o974 b1503 b984 b1496  T       t1503   o2 b1503
3824  B       b1504   t1503  B       b1504   t1503
3825  T       t1504   o2 b1504  T       t1504   o973 b1499 b4 b1504
3826  B       b1505   t1504  B       b1505   t1504
3827  T       t1505   o974 b1500 b4 b1505  T       t1505   o b1505 b4
3828  B       b1506   t1505  B       b1506   t1505
3829  T       t1506   o b1506 b4  T       t1506   o b1496 b1506
3830  B       b1507   t1506  B       b1507   t1506
3831  T       t1507   o b1497 b1507  T       t1507   o936 b1479 b1507
3832  B       b1508   t1507  B       b1508   t1507
3833  T       t1508   o937 b1480 b1508  P       p1508   String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"
3834    O       o1508   ext_rule p1508
3835    T       t1508   o559 b560 b567
3836  B       b1509   t1508  B       b1509   t1508
3837  P       p1509   String "setSubstT << equal{op{'s3; inv{'s3}}; id} >> 5 thenT autoT"  T       t1509   o559 b561 b567
 O       o1509   ext_rule p1509  
 T       t1509   o559 b560 b567  
3838  B       b1510   t1509  B       b1510   t1509
3839  T       t1510   o559 b561 b567  T       t1510   o738 b1509 b1510
3840  B       b1511   t1510  H       h1510   v_4 t1510
3841  T       t1511   o739 b1510 b1511  S       s1510   t620 h h1454 h1465 h1475 h1492 h1510
3842  H       h1511   v_4 t1511  G       s1510   t1344
3843  S       s1511   t620 h h1455 h1466 h1476 h1493 h1511  B       b1511   s1510
3844  G       s1511   t1345  T       t1511   o938 b1511 b1452
3845  B       b1512   s1511  B       b1512   t1511
3846  T       t1512   o939 b1512 b1453  T       t1512   o2 b1496
3847  B       b1513   t1512  B       b1513   t1512
3848  T       t1513   o2 b1497  T       t1513   o937 b1512 b4 b1513
3849  B       b1514   t1513  B       b1514   t1513
3850  T       t1514   o938 b1513 b4 b1514  T       t1514   o b1514 b4
3851  B       b1515   t1514  B       b1515   t1514
3852  T       t1515   o b1515 b4  T       t1515   o936 b1496 b1515
3853  B       b1516   t1515  B       b1516   t1515
3854  T       t1516   o937 b1497 b1516  P       p1516   String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"
3855  B       b1517   t1516  O       o1516   ext_rule p1516
3856  P       p1517   String "setSubstT << equal{op{'s1; id}; 's1} >> 6 thenT autoT"  T       t1516   o738 b560 b1510
3857  O       o1517   ext_rule p1517  H       h1516   v_5 t1516
3858  T       t1517   o739 b560 b1511  S       s1516   t620 h h1454 h1465 h1475 h1492 h1510 h1516
3859  H       h1517   v_5 t1517  G       s1516   t1344
3860  S       s1517   t620 h h1455 h1466 h1476 h1493 h1511 h1517  B       b1517   s1516
3861  G       s1517   t1345  T       t1517   o938 b1517 b1452
3862  B       b1518   s1517  B       b1518   t1517
3863  T       t1518   o939 b1518 b1453  T       t1518   o2 b1514
3864  B       b1519   t1518  B       b1519   t1518
3865  T       t1519   o2 b1515  T       t1519   o937 b1518 b4 b1519
3866  B       b1520   t1519  B       b1520   t1519
3867  T       t1520   o938 b1519 b4 b1520  B       b1521   t1509 v_5
3868  B       b1521   t1520  T       t1521   o711 b1521
3869  B       b1522   t1510 v_5  S       s1521   t620 h h1454 h1465 h1475 h1492 h1510
3870  T       t1522   o712 b1522  G       s1521   t1521
3871  S       s1522   t620 h h1455 h1466 h1476 h1493 h1511  B       b1522   s1521
3872  G       s1522   t1522  T       t1522   o938 b1522 b1452
3873  B       b1523   s1522  B       b1523   t1522
3874  T       t1523   o939 b1523 b1453  T       t1523   o738 b1032 b1510
3875  B       b1524   t1523  B       b1524   t1523 v_5
3876  T       t1524   o739 b1033 b1511  T       t1524   o976 b1524
3877  B       b1525   t1524 v_5  S       s1524   t620 h h1454 h1465 h1475 h1492 h1510
3878  T       t1525   o977 b1525  G       s1524   t1524
3879  S       s1525   t620 h h1455 h1466 h1476 h1493 h1511  B       b1525   s1524
3880  G       s1525   t1525  T       t1525   o938 b1525 b1452
3881  B       b1526   s1525  B       b1526   t1525
3882  T       t1526   o939 b1526 b1453  T       t1526   o973 b1526 b983 b1519
3883  B       b1527   t1526  B       b1527   t1526
3884  T       t1527   o974 b1527 b984 b1520  T       t1527   o2 b1527
3885  B       b1528   t1527  B       b1528   t1527
3886  T       t1528   o2 b1528  T       t1528   o973 b1523 b4 b1528
3887  B       b1529   t1528  B       b1529   t1528
3888  T       t1529   o974 b1524 b4 b1529  T       t1529   o b1529 b4
3889  B       b1530   t1529  B       b1530   t1529
3890  T       t1530   o b1530 b4  T       t1530   o b1520 b1530
3891  B       b1531   t1530  B       b1531   t1530
3892  T       t1531   o b1521 b1531  T       t1531   o936 b1514 b1531
3893  B       b1532   t1531  B       b1532   t1531
3894  T       t1532   o937 b1515 b1532  P       p1532   String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"
3895    O       o1532   ext_rule p1532
3896    T       t1532   o936 b1520 b4
3897  B       b1533   t1532  B       b1533   t1532
3898  P       p1533   String "setSubstT << equal{op{'s2; id}; 's2} >> 7 thenT autoT"  T       t1533   o1532 b935 b1533 b4 b4
 O       o1533   ext_rule p1533  
 T       t1533   o937 b1521 b4  
3899  B       b1534   t1533  B       b1534   t1533
3900  T       t1534   o1533 b936 b1534 b4 b4  T       t1534   o936 b1529 b4
3901  B       b1535   t1534  B       b1535   t1534
3902  T       t1535   o937 b1530 b4  T       t1535   o1050 b935 b1535 b4 b4
3903  B       b1536   t1535  B       b1536   t1535
3904  T       t1536   o1051 b936 b1536 b4 b4  T       t1536   o b1536 b4
3905  B       b1537   t1536  B       b1537   t1536
3906  T       t1537   o b1537 b4  T       t1537   o b1534 b1537
3907  B       b1538   t1537  B       b1538   t1537
3908  T       t1538   o b1535 b1538  T       t1538   o1516 b935 b1532 b1538 b4
3909  B       b1539   t1538  B       b1539   t1538
3910  T       t1539   o1517 b936 b1533 b1539 b4  T       t1539   o b1539 b4
3911  B       b1540   t1539  B       b1540   t1539
3912  T       t1540   o b1540 b4  T       t1540   o1508 b935 b1516 b1540 b4
3913  B       b1541   t1540  B       b1541   t1540
3914  T       t1541   o1509 b936 b1517 b1541 b4  T       t1541   o936 b1505 b4
3915  B       b1542   t1541  B       b1542   t1541
3916  T       t1542   o937 b1506 b4  T       t1542   o1050 b935 b1542 b4 b4
3917  B       b1543   t1542  B       b1543   t1542
3918  T       t1543   o1051 b936 b1543 b4 b4  T       t1543   o b1543 b4
3919  B       b1544   t1543  B       b1544   t1543
3920  T       t1544   o b1544 b4  T       t1544   o b1541 b1544
3921  B       b1545   t1544  B       b1545   t1544
3922  T       t1545   o b1542 b1545  T       t1545   o1491 b935 b1508 b1545 b4
3923  B       b1546   t1545  B       b1546   t1545
3924  T       t1546   o1492 b936 b1509 b1546 b4  T       t1546   o936 b1488 b4
3925  B       b1547   t1546  B       b1547   t1546
3926  T       t1547   o937 b1489 b4  T       t1547   o1050 b935 b1547 b4 b4
3927  B       b1548   t1547  B       b1548   t1547
3928  T       t1548   o1051 b936 b1548 b4 b4  T       t1548   o b1548 b4
3929  B       b1549   t1548  B       b1549   t1548
3930  T       t1549   o b1549 b4  T       t1549   o b1546 b1549
3931  B       b1550   t1549  B       b1550   t1549
3932  T       t1550   o b1547 b1550  T       t1550   o1473 b935 b1491 b1550 b4
3933  B       b1551   t1550  B       b1551   t1550
3934  T       t1551   o1474 b936 b1492 b1551 b4  T       t1551   o b1551 b4
3935  B       b1552   t1551  B       b1552   t1551
3936  T       t1552   o b1552 b4  T       t1552   o b1473 b1552
3937  B       b1553   t1552  B       b1553   t1552
3938  T       t1553   o b1474 b1553  S       s1553   t620 h
3939  B       b1554   t1553  G       s1553   t1457
3940  S       s1554   t620 h  B       b1554   s1553
3941  G       s1554   t1458  T       t1554   o938 b1554 b1452
3942  B       b1555   s1554  B       b1555   t1554
3943  T       t1555   o939 b1555 b1453  T       t1555   o947 b1555 b4 b1462
3944  B       b1556   t1555  B       b1556   t1555
3945  T       t1556   o948 b1556 b4 b1463  T       t1556   o1085 b1556
3946  B       b1557   t1556  B       b1557   t1556
3947  T       t1557   o1086 b1557  T       t1557   o b1557 b4
3948  B       b1558   t1557  B       b1558   t1557
3949  T       t1558   o b1558 b4  T       t1558   o963 b935 b1557 b1558 b4
3950  B       b1559   t1558  B       b1559   t1558
3951  T       t1559   o964 b936 b1558 b1559 b4  H       h1559   v t1457
3952  B       b1560   t1559  S       s1559   t620 h h1559
3953  H       h1560   v t1458  G       s1559   t1344
3954  S       s1560   t620 h h1560  B       b1560   s1559
3955  G       s1560   t1345  T       t1560   o938 b1560 b1452
3956  B       b1561   s1560  B       b1561   t1560
3957  T       t1561   o939 b1561 b1453  T       t1561   o937 b1561 b4 b1462
3958  B       b1562   t1561  B       b1562   t1561
3959  T       t1562   o938 b1562 b4 b1463  T       t1562   o1085 b1562
3960  B       b1563   t1562  B       b1563   t1562
3961  T       t1563   o1086 b1563  T       t1563   o b1563 b4
3962  B       b1564   t1563  B       b1564   t1563
3963  T       t1564   o b1564 b4  T       t1564   o1532 b935 b1563 b1564 b4
3964  B       b1565   t1564  B       b1565   t1564
3965  T       t1565   o1533 b936 b1564 b1565 b4  T       t1565   o b1565 b4
3966  B       b1566   t1565  B       b1566   t1565
3967  T       t1566   o b1566 b4  H       h1566   x t1435
3968  B       b1567   t1566  H       h1567   v_1 t1475
3969  H       h1567   x t1436  H       h1568   v_2 t1492
3970  H       h1568   v_1 t1476  H       h1569   v_3 t1510
3971  H       h1569   v_2 t1493  B       b1569   t1509 v_4
3972  H       h1570   v_3 t1511  T       t1569   o711 b1569
3973  B       b1570   t1510 v_4  S       s1569   t620 h h1566 h1559 h1567 h1568 h1569
3974  T       t1570   o712 b1570  G       s1569   t1569
3975  S       s1570   t620 h h1567 h1560 h1568 h1569 h1570  B       b1570   s1569
3976  G       s1570   t1570  T       t1570   o938 b1570 b1107
3977  B       b1571   s1570  B       b1571   t1570
3978  T       t1571   o939 b1571 b1108  T       t1571   o738 b1147 b1510
3979  B       b1572   t1571  B       b1572   t1571 v_4
3980  T       t1572   o739 b1148 b1511  T       t1572   o976 b1572
3981  B       b1573   t1572 v_4  S       s1572   t620 h h1566 h1559 h1567 h1568 h1569
3982  T       t1573   o977 b1573  G       s1572   t1572
3983  S       s1573   t620 h h1567 h1560 h1568 h1569 h1570  B       b1573   s1572
3984  G       s1573   t1573  T       t1573   o938 b1573 b1107
3985  B       b1574   s1573  B       b1574   t1573
3986  T       t1574   o939 b1574 b1108  S       s1574   t620 h h1566 h1559 h1567 h1568 h1569
3987  B       b1575   t1574  G       s1574   t1344
3988  S       s1575   t620 h h1567 h1560 h1568 h1569 h1570  B       b1575   s1574
3989  G       s1575   t1345  T       t1575   o938 b1575 b1107
3990  B       b1576   s1575  B       b1576   t1575
3991  T       t1576   o939 b1576 b1108  S       s1576   t620 h h1566 h1559 h1567 h1568
3992  B       b1577   t1576  G       s1576   t1344
3993  S       s1577   t620 h h1567 h1560 h1568 h1569  B       b1577   s1576
3994  G       s1577   t1345  T       t1577   o938 b1577 b1107
3995  B       b1578   s1577  B       b1578   t1577
3996  T       t1578   o939 b1578 b1108  S       s1578   t620 h h1566 h1559 h1567
3997  B       b1579   t1578  G       s1578   t1344
3998  S       s1579   t620 h h1567 h1560 h1568  B       b1579   s1578
3999  G       s1579   t1345  T       t1579   o938 b1579 b1107
4000  B       b1580   s1579  B       b1580   t1579
4001  T       t1580   o939 b1580 b1108  S       s1580   t620 h h1566 h1559
4002  B       b1581   t1580  G       s1580   t1344
4003  S       s1581   t620 h h1567 h1560  B       b1581   s1580
4004  G       s1581   t1345  T       t1581   o938 b1581 b1107
4005  B       b1582   s1581  B       b1582   t1581
4006  T       t1582   o939 b1582 b1108  S       s1582   t620 h h1566
4007  B       b1583   t1582  G       s1582   t1344
4008  S       s1583   t620 h h1567  B       b1583   s1582
4009  G       s1583   t1345  T       t1583   o938 b1583 b1107
4010  B       b1584   s1583  B       b1584   t1583
4011  T       t1584   o939 b1584 b1108  T       t1584   o937 b1584 b4 b946
4012  B       b1585   t1584  B       b1585   t1584
4013  T       t1585   o938 b1585 b4 b947  T       t1585   o2 b1585
4014  B       b1586   t1585  B       b1586   t1585
4015  T       t1586   o2 b1586  T       t1586   o937 b1582 b4 b1586
4016  B       b1587   t1586  B       b1587   t1586
4017  T       t1587   o938 b1583 b4 b1587  T       t1587   o2 b1587
4018  B       b1588   t1587  B       b1588   t1587
4019  T       t1588   o2 b1588  T       t1588   o937 b1580 b4 b1588
4020  B       b1589   t1588  B       b1589   t1588
4021  T       t1589   o938 b1581 b4 b1589  T       t1589   o2 b1589
4022  B       b1590   t1589  B       b1590   t1589
4023  T       t1590   o2 b1590  T       t1590   o937 b1578 b4 b1590
4024  B       b1591   t1590  B       b1591   t1590
4025  T       t1591   o938 b1579 b4 b1591  T       t1591   o2 b1591
4026  B       b1592   t1591  B       b1592   t1591
4027  T       t1592   o2 b1592  T       t1592   o937 b1576 b4 b1592
4028  B       b1593   t1592  B       b1593   t1592
4029  T       t1593   o938 b1577 b4 b1593  T       t1593   o2 b1593
4030  B       b1594   t1593  B       b1594   t1593
4031  T       t1594   o2 b1594  T       t1594   o973 b1574 b983 b1594
4032  B       b1595   t1594  B       b1595   t1594
4033  T       t1595   o974 b1575 b984 b1595  T       t1595   o2 b1595
4034  B       b1596   t1595  B       b1596   t1595
4035  T       t1596   o2 b1596  T       t1596   o973 b1571 b4 b1596
4036  B       b1597   t1596  B       b1597   t1596
4037  T       t1597   o974 b1572 b4 b1597  T       t1597   o936 b1597 b4
4038  B       b1598   t1597  B       b1598   t1597
4039  T       t1598   o937 b1598 b4  T       t1598   o1050 b935 b1598 b4 b4
4040  B       b1599   t1598  B       b1599   t1598
4041  T       t1599   o1051 b936 b1599 b4 b4  T       t1599   o b1599 b4
4042  B       b1600   t1599  B       b1600   t1599
4043  T       t1600   o b1600 b4  T       t1600   o1516 b935 b1563 b1566 b1600
4044  B       b1601   t1600  B       b1601   t1600
4045  T       t1601   o1517 b936 b1564 b1567 b1601  T       t1601   o b1601 b4
4046  B       b1602   t1601  B       b1602   t1601
4047  T       t1602   o b1602 b4  T       t1602   o1508 b935 b1563 b1602 b4
4048  B       b1603   t1602  B       b1603   t1602
4049  T       t1603   o1509 b936 b1564 b1603 b4  T       t1603   o b1603 b4
4050  B       b1604   t1603  B       b1604   t1603
4051  T       t1604   o b1604 b4  P       p1604   String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"
4052  B       b1605   t1604  O       o1604   ext_rule p1604
4053  P       p1605   String "rwh unfold_fun_set 0 thenT rwh unfold_equal 0 thenT autoT"  B       b1605   t1474 v_2
4054  O       o1605   ext_rule p1605  T       t1605   o711 b1605
4055  B       b1606   t1475 v_2  S       s1605   t620 h h1566 h1559 h1567
4056  T       t1606   o712 b1606  G       s1605   t1605
4057  S       s1606   t620 h h1567 h1560 h1568  B       b1606   s1605
4058  G       s1606   t1606  T       t1606   o938 b1606 b1107
4059  B       b1607   s1606  B       b1607   t1606
4060  T       t1607   o939 b1607 b1108  T       t1607   o738 b1475 b977
4061  B       b1608   t1607  B       b1608   t1607 v_2
4062  T       t1608   o739 b1476 b978  T       t1608   o976 b1608
4063  B       b1609   t1608 v_2  S       s1608   t620 h h1566 h1559 h1567
4064  T       t1609   o977 b1609  G       s1608   t1608
4065  S       s1609   t620 h h1567 h1560 h1568  B       b1609   s1608
4066  G       s1609   t1609  T       t1609   o938 b1609 b1107
4067  B       b1610   s1609  B       b1610   t1609
4068  T       t1610   o939 b1610 b1108  T       t1610   o973 b1610 b983 b1590
4069  B       b1611   t1610  B       b1611   t1610
4070  T       t1611   o974 b1611 b984 b1591  T       t1611   o2 b1611
4071  B       b1612   t1611  B       b1612   t1611
4072  T       t1612   o2 b1612  T       t1612   o973 b1607 b4 b1612
4073  B       b1613   t1612  B       b1613   t1612
4074  T       t1613   o974 b1608 b4 b1613  T       t1613   o936 b1613 b4
4075  B       b1614   t1613  B       b1614   t1613
4076  T       t1614   o937 b1614 b4  T       t1614   o1604 b935 b1614 b4 b4
4077  B       b1615   t1614  B       b1615   t1614
4078  T       t1615   o1605 b936 b1615 b4 b4  T       t1615   o b1615 b4
4079  B       b1616   t1615  B       b1616   t1615
4080  T       t1616   o b1616 b4  T       t1616   o1491 b935 b1563 b1604 b1616
4081  B       b1617   t1616  B       b1617   t1616
4082  T       t1617   o1492 b936 b1564 b1605 b1617  T       t1617   o b1617 b4
4083  B       b1618   t1617  B       b1618   t1617
4084  T       t1618   o b1618 b4  B       b1619   t1456 v_1
4085  B       b1619   t1618  T       t1619   o711 b1619
4086  B       b1620   t1457 v_1  S       s1619   t620 h h1566 h1559
4087  T       t1620   o712 b1620  G       s1619   t1619
4088  S       s1620   t620 h h1567 h1560  B       b1620   s1619
4089  G       s1620   t1620  T       t1620   o938 b1620 b1107
4090  B       b1621   s1620  B       b1621   t1620
4091  T       t1621   o939 b1621 b1108  T       t1621   o738 b1220 b1457
4092  B       b1622   t1621  B       b1622   t1621 v_1
4093  T       t1622   o739 b1221 b1458  T       t1622   o976 b1622
4094  B       b1623   t1622 v_1  S       s1622   t620 h h1566 h1559
4095  T       t1623   o977 b1623  G       s1622   t1622
4096  S       s1623   t620 h h1567 h1560  B       b1623   s1622
4097  G       s1623   t1623  T       t1623   o938 b1623 b1107
4098  B       b1624   s1623  B       b1624   t1623
4099  T       t1624   o939 b1624 b1108  T       t1624   o973 b1624 b983 b1588
4100  B       b1625   t1624  B       b1625   t1624
4101  T       t1625   o974 b1625 b984 b1589  T       t1625   o2 b1625
4102  B       b1626   t1625  B       b1626   t1625
4103  T       t1626   o2 b1626  T       t1626   o973 b1621 b4 b1626
4104  B       b1627   t1626  B       b1627   t1626
4105  T       t1627   o974 b1622 b4 b1627  T       t1627   o936 b1627 b4
4106  B       b1628   t1627  B       b1628   t1627
4107  T       t1628   o937 b1628 b4  T       t1628   o1604 b935 b1628 b4 b4
4108  B       b1629   t1628  B       b1629   t1628
4109  T       t1629   o1605 b936 b1629 b4 b4  T       t1629   o b1629 b4
4110  B       b1630   t1629  B       b1630   t1629
4111  T       t1630   o b1630 b4  T       t1630   o1473 b935 b1563 b1618 b1630
4112  B       b1631   t1630  B       b1631   t1630
4113  T       t1631   o1474 b936 b1564 b1619 b1631  T       t1631   o b1631 b4
4114  B       b1632   t1631  B       b1632   t1631
4115  T       t1632   o b1632 b4  T       t1632   o b1559 b1632
4116  B       b1633   t1632  B       b1633   t1632
4117  T       t1633   o b1560 b1633  T       t1633   o1445 b935 b1471 b1553 b1633
4118  B       b1634   t1633  B       b1634   t1633
4119  T       t1634   o1446 b936 b1472 b1554 b1634  T       t1634   o933 b1634
4120  B       b1635   t1634  B       b1635   t1634
4121  T       t1635   o934 b1635  P       p1635   Number 5861
4122  B       b1636   t1635  P       p1636   Number 5869
4123  P       p1636   Number 5870  O       o1636   resource_defs p1635 p1636 p264
4124  P       p1637   Number 5878  P       p1637   Number 5867
4125  O       o1637   resource_defs p1636 p1637 p264  O       o1637   uid p1637 p1636
4126  P       p1638   Number 5876  T       t1637   o1637 b626
4127  O       o1638   uid p1638 p1637  B       b1637   t1637
4128  T       t1638   o1638 b626  T       t1638   o b1637 b4
4129  B       b1638   t1638  B       b1638   t1638
4130  T       t1639   o b1638 b4  T       t1639   o1636 b1638
4131  B       b1639   t1639  B       b1639   t1639
4132  T       t1640   o1637 b1639  T       t1640   o b1639 b4
4133  B       b1640   t1640  B       b1640   t1640
4134  T       t1641   o b1640 b4  T       t1641   o1432 b1434 b1445 b1635 b1640
4135  B       b1641   t1641  B       b1641   t1641
4136  T       t1642   o1433 b1435 b1446 b1636 b1641  T       t1642   o1431 b1641
4137  B       b1642   t1642  B       b1642   t1642
4138  T       t1643   o1432 b1642  P       p1642   Number 6266
4139  B       b1643   t1643  P       p1643   Number 6335
4140  P       p1643   Number 6275  O       o1643   location p1642 p1643
4141  P       p1644   Number 6344  O       o1644   str_let p1642 p1643
4142  O       o1644   location p1643 p1644  P       p1644   Number 6270
4143  O       o1645   str_let p1643 p1644  O       o1645   patt_var p1644 p1643
4144  P       p1645   Number 6279  O       o1646   patt_done p1642 p1643
4145  O       o1646   patt_var p1645 p1644  T       t1646   o1646
4146  O       o1647   patt_done p1643 p1644  B       b1646   t1646 groupCancelLeftT
4147  T       t1647   o1647  T       t1647   o1645 b1646
4148  B       b1647   t1647 groupCancelLeftT  B       b1647   t1647
4149  T       t1648   o1646 b1647  O       o1647   fun p1644 p1643
4150  B       b1648   t1648  O       o1648   patt_if p1644 p1643
4151  O       o1648   fun p1645 p1644  P       p1648   Number 6287
4152  O       o1649   patt_if p1645 p1644  P       p1649   Number 6288
4153  P       p1649   Number 6296  O       o1649   patt_var p1648 p1649
4154  P       p1650   Number 6297  O       o1650   patt_body p1644 p1643
4155  O       o1650   patt_var p1649 p1650  P       p1650   Number 6289
4156  O       o1651   patt_body p1645 p1644  P       p1651   Number 6290
4157  P       p1651   Number 6298  O       o1651   patt_var p1650 p1651
4158  P       p1652   Number 6299  P       p1652   Number 6296
4159  O       o1652   patt_var p1651 p1652  O       o1652   apply p1652 p1643
4160  P       p1653   Number 6305  P       p1653   Number 6333
4161  O       o1653   apply p1653 p1644  O       o1653   apply p1652 p1653
4162  P       p1654   Number 6342  P       p1654   Number 6331
4163  O       o1654   apply p1653 p1654  O       o1654   apply p1652 p1654
4164  P       p1655   Number 6340  P       p1655   Number 6303
4165  O       o1655   apply p1653 p1655  O       o1655   lid p1652 p1655
4166  P       p1656   Number 6312  O       o1656   lid p919
4167  O       o1656   lid p1653 p1656  T       t1656   o1656
4168  O       o1657   lid p920  B       b1656   t1656
4169  T       t1657   o1657  T       t1657   o1655 b1656
4170  B       b1657   t1657  B       b1657   t1657
4171  T       t1658   o1656 b1657  P       p1657   Number 6305
4172  B       b1658   t1658  P       p1658   Number 6330
4173  P       p1658   Number 6314  O       o1658   apply p1657 p1658
4174  P       p1659   Number 6339  P       p1659   Number 6328
4175  O       o1659   apply p1658 p1659  O       o1659   proj p1657 p1659
4176  P       p1660   Number 6337  O       o1660   uid p1657 p1659
4177  O       o1660   proj p1658 p1660  T       t1660   o1660 b836
4178  O       o1661   uid p1658 p1660  B       b1660   t1660
4179  T       t1661   o1661 b837  P       p1660   Number 6314
4180    O       o1661   lid p1660 p1659
4181    T       t1661   o1661 b838
4182  B       b1661   t1661  B       b1661   t1661
4183  P       p1661   Number 6323  T       t1662   o1659 b1660 b1661
 O       o1662   lid p1661 p1660  
 T       t1662   o1662 b839  
4184  B       b1662   t1662  B       b1662   t1662
4185  T       t1663   o1660 b1661 b1662  P       p1662   Number 6329
4186    O       o1662   lid p1662 p1658
4187    T       t1663   o1662 b841
4188  B       b1663   t1663  B       b1663   t1663
4189  P       p1663   Number 6338  T       t1664   o1658 b1662 b1663
 O       o1663   lid p1663 p1659  
 T       t1664   o1663 b842  
4190  B       b1664   t1664  B       b1664   t1664
4191  T       t1665   o1659 b1663 b1664  T       t1665   o1654 b1657 b1664
4192  B       b1665   t1665  B       b1665   t1665
4193  T       t1666   o1655 b1658 b1665  P       p1665   Number 6332
4194    O       o1665   lid p1665 p1653
4195    P       p1666   Var t
4196    O       o1666   var p1666
4197    T       t1666   o1666
4198  B       b1666   t1666  B       b1666   t1666
4199  P       p1666   Number 6341  T       t1667   o1665 b1666
 O       o1666   lid p1666 p1654  
 P       p1667   Var t  
 O       o1667   var p1667  
 T       t1667   o1667  
4200  B       b1667   t1667  B       b1667   t1667
4201  T       t1668   o1666 b1667  T       t1668   o1653 b1665 b1667
4202  B       b1668   t1668  B       b1668   t1668
4203  T       t1669   o1654 b1666 b1668  P       p1668   Number 6334
4204    O       o1668   lid p1668 p1643
4205    T       t1669   o1668 b841
4206  B       b1669   t1669  B       b1669   t1669
4207  P       p1669   Number 6343  T       t1670   o1652 b1668 b1669
 O       o1669   lid p1669 p1644  
 T       t1670   o1669 b842  
4208  B       b1670   t1670  B       b1670   t1670
4209  T       t1671   o1653 b1669 b1670  T       t1671   o1650 b1670
4210  B       b1671   t1671  B       b1671   t1671 p
4211  T       t1672   o1651 b1671  T       t1672   o1651 b1671
4212  B       b1672   t1672 p  B       b1672   t1672
4213  T       t1673   o1652 b1672  T       t1673   o1648 b1672
4214  B       b1673   t1673  B       b1673   t1673
4215  T       t1674   o1649 b1673  T       t1674   o1647 b1673
4216  B       b1674   t1674  B       b1674   t1674
4217  T       t1675   o1648 b1674  T       t1675   o1650 b1674
4218  B       b1675   t1675  B       b1675   t1675 t
4219  T       t1676   o1651 b1675  T       t1676   o1649 b1675
4220  B       b1676   t1676 t  B       b1676   t1676
4221  T       t1677   o1650 b1676  T       t1677   o1648 b1676
4222  B       b1677   t1677  B       b1677   t1677
4223  T       t1678   o1649 b1677  T       t1678   o1647 b1677
4224  B       b1678   t1678  B       b1678   t1678
4225  T       t1679   o1648 b1678  T       t1679   o1644 b1647 b1678
4226  B       b1679   t1679  B       b1679   t1679
4227  T       t1680   o1645 b1648 b1679  T       t1680   o b1679 b4
4228  B       b1680   t1680  B       b1680   t1680
4229  T       t1681   o b1680 b4  T       t1681   o1644 b1680
4230  B       b1681   t1681  B       b1681   t1681
4231  T       t1682   o1645 b1681  T       t1682   o392 b1681
4232  B       b1682   t1682  B       b1682   t1682
4233  T       t1683   o392 b1682  T       t1683   o1643 b1682
4234  B       b1683   t1683  B       b1683   t1683
4235  T       t1684   o1644 b1683  P       p1683   Number 6337
4236  B       b1684   t1684  P       p1684   Number 6407
4237  P       p1684   Number 6346  O       o1684   location p1683 p1684
4238  P       p1685   Number 6416  O       o1685   str_let p1683 p1684
4239  O       o1685   location p1684 p1685  P       p1685   Number 6341
4240  O       o1686   str_let p1684 p1685  O       o1686   patt_var p1685 p1684
4241  P       p1686   Number 6350  O       o1687   patt_done p1683 p1684
4242  O       o1687   patt_var p1686 p1685  T       t1687   o1687
4243  O       o1688   patt_done p1684 p1685  B       b1687   t1687 groupCancelRightT
4244  T       t1688   o1688  T       t1688   o1686 b1687
4245  B       b1688   t1688 groupCancelRightT  B       b1688   t1688
4246  T       t1689   o1687 b1688  O       o1688   fun p1685 p1684
4247  B       b1689   t1689  O       o1689   patt_if p1685 p1684
4248  O       o1689   fun p1686 p1685  P       p1689   Number 6359
4249  O       o1690   patt_if p1686 p1685  P       p1690   Number 6360
4250  P       p1690   Number 6368  O       o1690   patt_var p1689 p1690
4251  P       p1691   Number 6369  O       o1691   patt_body p1685 p1684
4252  O       o1691   patt_var p1690 p1691  P       p1691   Number 6361
4253  O       o1692   patt_body p1686 p1685  P       p1692   Number 6362
4254  P       p1692   Number 6370  O       o1692   patt_var p1691 p1692
4255  P       p1693   Number 6371  P       p1693   Number 6368
4256  O       o1693   patt_var p1692 p1693  O       o1693   apply p1693 p1684
4257  P       p1694   Number 6377  P       p1694   Number 6405
4258  O       o1694   apply p1694 p1685  O       o1694   apply p1693 p1694
4259  P       p1695   Number 6414  P       p1695   Number 6403
4260  O       o1695   apply p1694 p1695  O       o1695   apply p1693 p1695
4261  P       p1696   Number 6412  P       p1696   Number 6375
4262  O       o1696   apply p1694 p1696  O       o1696   lid p1693 p1696
4263  P       p1697   Number 6384  O       o1697   lid p1432
4264  O       o1697   lid p1694 p1697  T       t1697   o1697
4265  O       o1698   lid p1433  B       b1697   t1697
4266  T       t1698   o1698  T       t1698   o1696 b1697
4267  B       b1698   t1698  B       b1698   t1698
4268  T       t1699   o1697 b1698  P       p1698   Number 6377
4269  B       b1699   t1699  P       p1699   Number 6402
4270  P       p1699   Number 6386  O       o1699   apply p1698 p1699
4271  P       p1700   Number 6411  P       p1700   Number 6400
4272  O       o1700   apply p1699 p1700  O       o1700   proj p1698 p1700
4273  P       p1701   Number 6409  O       o1701   uid p1698 p1700
4274  O       o1701   proj p1699 p1701  T       t1701   o1701 b836
4275  O       o1702   uid p1699 p1701  B       b1701   t1701
4276  T       t1702   o1702 b837  P       p1701   Number 6386
4277    O       o1702   lid p1701 p1700
4278    T       t1702   o1702 b838
4279  B       b1702   t1702  B       b1702   t1702
4280  P       p1702   Number 6395  T       t1703   o1700 b1701 b1702
 O       o1703   lid p1702 p1701  
 T       t1703   o1703 b839  
4281  B       b1703   t1703  B       b1703   t1703
4282  T       t1704   o1701 b1702 b1703  P       p1703   Number 6401
4283    O       o1703   lid p1703 p1699
4284    T       t1704   o1703 b841
4285  B       b1704   t1704  B       b1704   t1704
4286  P       p1704   Number 6410  T       t1705   o1699 b1703 b1704
 O       o1704   lid p1704 p1700  
 T       t1705   o1704 b842  
4287  B       b1705   t1705  B       b1705   t1705
4288  T       t1706   o1700 b1704 b1705  T       t1706   o1695 b1698 b1705
4289  B       b1706   t1706  B       b1706   t1706
4290  T       t1707   o1696 b1699 b1706  P       p1706   Number 6404
4291    O       o1706   lid p1706 p1694
4292    T       t1707   o1706 b1666
4293  B       b1707   t1707  B       b1707   t1707
4294  P       p1707   Number 6413  T       t1708   o1694 b1706 b1707
 O       o1707   lid p1707 p1695  
 T       t1708   o1707 b1667  
4295  B       b1708   t1708  B       b1708   t1708
4296  T       t1709   o1695 b1707 b1708  P       p1708   Number 6406
4297    O       o1708   lid p1708 p1684
4298    T       t1709   o1708 b841
4299  B       b1709   t1709  B       b1709   t1709
4300  P       p1709   Number 6415  T       t1710   o1693 b1708 b1709
 O       o1709   lid p1709 p1685  
 T       t1710   o1709 b842  
4301  B       b1710   t1710  B       b1710   t1710
4302  T       t1711   o1694 b1709 b1710  T       t1711   o1691 b1710
4303  B       b1711   t1711  B       b1711   t1711 p
4304  T       t1712   o1692 b1711  T       t1712   o1692 b1711
4305  B       b1712   t1712 p  B       b1712   t1712
4306  T       t1713   o1693 b1712  T       t1713   o1689 b1712
4307  B       b1713   t1713  B       b1713   t1713
4308  T       t1714   o1690 b1713  T       t1714   o1688 b1713
4309  B       b1714   t1714  B       b1714   t1714
4310  T       t1715   o1689 b1714  T       t1715   o1691 b1714
4311  B       b1715   t1715  B       b1715   t1715 t
4312  T       t1716   o1692 b1715  T       t1716   o1690 b1715
4313  B       b1716   t1716 t  B       b1716   t1716
4314  T       t1717   o1691 b1716  T       t1717   o1689 b1716
4315  B       b1717   t1717  B       b1717   t1717
4316  T       t1718   o1690 b1717  T       t1718   o1688 b1717
4317  B       b1718   t1718  B       b1718   t1718
4318  T       t1719   o1689 b1718  T       t1719   o1685 b1688 b1718
4319  B       b1719   t1719  B       b1719   t1719
4320  T       t1720   o1686 b1689 b1719  T       t1720   o b1719 b4
4321  B       b1720   t1720  B       b1720   t1720
4322  T       t1721   o b1720 b4  T       t1721   o1685 b1720
4323  B       b1721   t1721  B       b1721   t1721
4324  T       t1722   o1686 b1721  T       t1722   o392 b1721
4325  B       b1722   t1722  B       b1722   t1722
4326  T       t1723   o392 b1722  T       t1723   o1684 b1722
4327  B       b1723   t1723  B       b1723   t1723
4328  T       t1724   o1685 b1723  P       p1723   Number 6425
4329  B       b1724   t1724  P       p1724   Number 6666
4330  P       p1724   Number 6434  O       o1724   location p1723 p1724
4331  P       p1725   Number 6675  P       p1725   String unique_id1
4332  O       o1725   location p1724 p1725  O       o1725   rule p1725
4333  P       p1726   String unique_id1  P       p1726   Var e2
4334  O       o1726   rule p1726  O       o1726   var p1726
4335  P       p1727   Var e2  T       t1726   o1726
4336  O       o1727   var p1727  B       b1726   t1726
4337  T       t1727   o1727  T       t1727   o620 b1726
4338  B       b1727   t1727  S       s1727   t637 h
4339  T       t1728   o620 b1727  G       s1727   t1727
4340  S       s1728   t637 h  B       b1727   s1727
4341  G       s1728   t1728  T       t1728   o618 b1727
4342  B       b1728   s1728  B       b1728   t1728
4343  T       t1729   o618 b1728  T       t1729   o655 b1726 b554
4344  B       b1729   t1729  S       s1729   t620 h
4345  T       t1730   o655 b1727 b554  G       s1729   t1729
4346  S       s1730   t620 h  B       b1729   s1729
4347  G       s1730   t1730  T       t1730   o618 b1729
4348  B       b1730   s1730  B       b1730   t1730
 T       t1731   o618 b1730  
 B       b1731   t1731  
4349  NCzf_itt_dall   Czf_itt_dall    Czf_itt_dall NIL  NCzf_itt_dall   Czf_itt_dall    Czf_itt_dall NIL
4350  NCzf_itt_dall!dall      dall    dall Czf_itt_dall  NCzf_itt_dall!dall      dall    dall Czf_itt_dall
4351  O       o1731   dall  O       o1730   dall
4352  T       t1732   o559 b1727 b573  T       t1731   o559 b1726 b573
4353    B       b1731   t1731
4354    T       t1732   o676 b1731 b573
4355  B       b1732   t1732  B       b1732   t1732
4356  T       t1733   o676 b1732 b573  T       t1733   o559 b573 b1726
4357  B       b1733   t1733  B       b1733   t1733
4358  T       t1734   o559 b573 b1727  T       t1734   o676 b1733 b573
4359  B       b1734   t1734  B       b1734   t1734
4360  T       t1735   o676 b1734 b573  T       t1735   o1270 b1732 b1734
4361  B       b1735   t1735  B       b1735   t1735 s
4362  T       t1736   o1271 b1733 b1735  T       t1736   o1730 b554 b1735
4363  B       b1736   t1736 s  H       h1736   x t1736
4364  T       t1737   o1731 b554 b1736  T       t1737   o676 b1726 b567
4365  H       h1737   x t1737  S       s1737   t620 h h1736
4366  T       t1738   o676 b1727 b567  G       s1737   t1737
4367  S       s1738   t620 h h1737  B       b1737   s1737
4368  G       s1738   t1738  T       t1738   o618 b1737
4369  B       b1738   s1738  B       b1738   t1738
4370  T       t1739   o618 b1738  T       t1739   o635 b1730 b1738
4371  B       b1739   t1739  B       b1739   t1739
4372  T       t1740   o635 b1731 b1739  T       t1740   o635 b1728 b1739
4373  B       b1740   t1740  B       b1740   t1740
4374  T       t1741   o635 b1729 b1740  P       p1740   String "withT << id >> (dT 2) thenT autoT"
4375    O       o1740   ext_rule p1740
4376    T       t1741   o b1729 b4
4377  B       b1741   t1741  B       b1741   t1741
4378  P       p1741   String "withT << id >> (dT 2) thenT autoT"  T       t1742   o b1727 b1741
 O       o1741   ext_rule p1741  
 T       t1742   o b1730 b4  
4379  B       b1742   t1742  B       b1742   t1742
4380  T       t1743   o b1728 b1742  T       t1743   o938 b1737 b1742
4381  B       b1743   t1743  B       b1743   t1743
4382  T       t1744   o939 b1738 b1743  T       t1744   o937 b1743 b4 b946
4383  B       b1744   t1744  B       b1744   t1744
4384  T       t1745   o938 b1744 b4 b947  T       t1745   o559 b1726 b567
4385  B       b1745   t1745  B       b1745   t1745
4386  T       t1746   o559 b1727 b567  T       t1746   o676 b1745 b567
4387  B       b1746   t1746  H       h1746   y t1746
4388  T       t1747   o676 b1746 b567  T       t1747   o559 b567 b1726
4389  H       h1747   y t1747  B       b1747   t1747
4390  T       t1748   o559 b567 b1727  T       t1748   o676 b1747 b567
4391  B       b1748   t1748  H       h1748   z t1748
4392  T       t1749   o676 b1748 b567  S       s1748   t620 h h1736 h1746 h1748
4393  H       h1749   z t1749  G       s1748   t1737
4394  S       s1749   t620 h h1737 h1747 h1749  B       b1748   s1748
4395  G       s1749   t1738  T       t1749   o938 b1748 b1742
4396  B       b1749   s1749  B       b1749   t1749
4397  T       t1750   o939 b1749 b1743  B       b1750   t1746
4398  B       b1750   t1750  B       b1751   t1748
4399  B       b1751   t1747  T       t1751   o1270 b1750 b1751
4400  B       b1752   t1749  H       h1751   w t1751
4401  T       t1752   o1271 b1751 b1752  S       s1751   t620 h h1736 h1751
4402  H       h1752   w t1752  G       s1751   t1737
4403  S       s1752   t620 h h1737 h1752  B       b1752   s1751
4404  G       s1752   t1738  T       t1752   o938 b1752 b1742
4405  B       b1753   s1752  B       b1753   t1752
4406  T       t1753   o939 b1753 b1743  P       p1753   String with
4407  B       b1754   t1753  O       o1753   arg_named p1753
 P       p1754   String with  
 O       o1754   arg_named p1754  
4408  NSummary!arg_term_list  arg_term_list   arg_term_list Summary  NSummary!arg_term_list  arg_term_list   arg_term_list Summary
4409  O       o1755   arg_term_list  O       o1754   arg_term_list
4410  T       t1755   o b567 b4  T       t1754   o b567 b4
4411    B       b1754   t1754
4412    T       t1755   o1754 b1754
4413  B       b1755   t1755  B       b1755   t1755
4414  T       t1756   o1755 b1755  T       t1756   o1753 b1755
4415  B       b1756   t1756  B       b1756   t1756
4416  T       t1757   o1754 b1756  T       t1757   o b1756 b4
4417  B       b1757   t1757  B       b1757   t1757
4418  T       t1758   o b1757 b4  T       t1758   o937 b1743 b1757 b946
4419  B       b1758   t1758  B       b1758   t1758
4420  T       t1759   o938 b1744 b1758 b947  T       t1759   o2 b1758
4421  B       b1759   t1759  B       b1759   t1759
4422  T       t1760   o2 b1759  T       t1760   o937 b1753 b4 b1759
4423  B       b1760   t1760  B       b1760   t1760
4424  T       t1761   o938 b1754 b4 b1760  T       t1761   o2 b1760
4425  B       b1761   t1761  B       b1761   t1761
4426  T       t1762   o2 b1761  T       t1762   o937 b1749 b4 b1761
4427  B       b1762   t1762  B       b1762   t1762
4428  T       t1763   o938 b1750 b4 b1762  T       t1763   o b1762 b4
4429  B       b1763   t1763  B       b1763   t1763
4430  T       t1764   o b1763 b4  T       t1764   o936 b1744 b1763
4431  B       b1764   t1764  B       b1764   t1764
4432  T       t1765   o937 b1745 b1764  P       p1764   String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"
4433    O       o1764   ext_rule p1764
4434    T       t1765   o936 b1762 b4
4435  B       b1765   t1765  B       b1765   t1765
4436  P       p1765   String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenT autoT"  T       t1766   o1764 b935 b1765 b4 b4
 O       o1765   ext_rule p1765  
 T       t1766   o937 b1763 b4  
4437  B       b1766   t1766  B       b1766   t1766
4438  T       t1767   o1765 b936 b1766 b4 b4  T       t1767   o b1766 b4
4439  B       b1767   t1767  B       b1767   t1767
4440  T       t1768   o b1767 b4  S       s1767   t620 h
4441  B       b1768   t1768  G       s1767   t1727
4442  S       s1768   t620 h  B       b1768   s1767
4443  G       s1768   t1728  T       t1768   o b1768 b1741
4444  B       b1769   s1768  B       b1769   t1768
4445  T       t1769   o b1769 b1742  T       t1769   o938 b1748 b1769
4446  B       b1770   t1769  B       b1770   t1769
4447  T       t1770   o939 b1749 b1770  T       t1770   o938 b1752 b1769
4448  B       b1771   t1770  B       b1771   t1770
4449  T       t1771   o939 b1753 b1770  T       t1771   o938 b1737 b1769
4450  B       b1772   t1771  B       b1772   t1771
4451  T       t1772   o939 b1738 b1770  T       t1772   o937 b1772 b1757 b946
4452  B       b1773   t1772  B       b1773   t1772
4453  T       t1773   o938 b1773 b1758 b947  T       t1773   o2 b1773
4454  B       b1774   t1773  B       b1774   t1773
4455  T       t1774   o2 b1774  T       t1774   o937 b1771 b4 b1774
4456  B       b1775   t1774  B       b1775   t1774
4457  T       t1775   o938 b1772 b4 b1775  T       t1775   o2 b1775
4458  B       b1776   t1775  B       b1776   t1775
4459  T       t1776   o2 b1776  T       t1776   o937 b1770 b4 b1776
4460  B       b1777   t1776  B       b1777   t1776
4461  T       t1777   o938 b1771 b4 b1777  T       t1777   o936 b1777 b4
4462  B       b1778   t1777  B       b1778   t1777
4463  T       t1778   o937 b1778 b4  T       t1778   o1764 b935 b1778 b4 b4
4464  B       b1779   t1778  B       b1779   t1778
4465  T       t1779   o1765 b936 b1779 b4 b4  P       p1779   String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"
4466  B       b1780   t1779  O       o1779   ext_rule p1779
4467  P       p1780   String "setSubstT << equal{op{'e2; id}; 'e2} >> 3 thenAT autoT"  H       h1779   v t1737
4468  O       o1780   ext_rule p1780  S       s1779   t620 h h1736 h1746 h1748 h1779
4469  H       h1780   v t1738  G       s1779   t1737
4470  S       s1780   t620 h h1737 h1747 h1749 h1780  B       b1780   s1779
4471  G       s1780   t1738  T       t1780   o938 b1780 b1769
4472  B       b1781   s1780  B       b1781   t1780
4473  T       t1781   o939 b1781 b1770  T       t1781   o2 b1777
4474  B       b1782   t1781  B       b1782   t1781
4475  T       t1782   o2 b1778  T       t1782   o937 b1781 b4 b1782
4476  B       b1783   t1782  B       b1783   t1782
4477  T       t1783   o938 b1782 b4 b1783  T       t1783   o b1783 b4
4478  B       b1784   t1783  B       b1784   t1783
4479  T       t1784   o b1784 b4  T       t1784   o936 b1777 b1784
4480  B       b1785   t1784  B       b1785   t1784
4481  T       t1785   o937 b1778 b1785  T       t1785   o1085 b1783
4482  B       b1786   t1785  B       b1786   t1785
4483  T       t1786   o1086 b1784  T       t1786   o b1786 b4
4484  B       b1787   t1786  B       b1787   t1786
4485  T       t1787   o b1787 b4  T       t1787   o1779 b935 b1785 b1787 b4
4486  B       b1788   t1787  B       b1788   t1787
4487  T       t1788   o1780 b936 b1786 b1788 b4  P       p1788   String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"
4488  B       b1789   t1788  O       o1788   ext_rule p1788
4489  P       p1789   String "setSubstT << equal{op{'e2; 'e}; 'e2} >> 3 thenAT autoT"  P       p1789   Var e
4490  O       o1789   ext_rule p1789  O       o1789   var p1789
4491  P       p1790   Var e  T       t1789   o1789
4492  O       o1790   var p1790  B       b1789   t1789
4493  T       t1790   o1790  T       t1790   o620 b1789
4494  B       b1790   t1790  S       s1790   t637 h h1736 h1746 h1748
4495  T       t1791   o620 b1790  G       s1790   t1790
4496  S       s1791   t637 h h1737 h1747 h1749  B       b1790   s1790
4497  G       s1791   t1791  T       t1791   o938 b1790 b1769
4498  B       b1791   s1791  B       b1791   t1791
4499  T       t1792   o939 b1791 b1770  T       t1792   o559 b1726 b1789
4500  B       b1792   t1792  B       b1792   t1792
4501  T       t1793   o559 b1727 b1790  T       t1793   o620 b1792
4502  B       b1793   t1793  S       s1793   t637 h h1736 h1746 h1748
4503  T       t1794   o620 b1793  G       s1793   t1793
4504  S       s1794   t637 h h1737 h1747 h1749  B       b1793   s1793
4505  G       s1794   t1794  T       t1794   o938 b1793 b1769
4506  B       b1794   s1794  B       b1794   t1794
4507  T       t1795   o939 b1794 b1770  T       t1795   o738 b1792 b1726
4508  B       b1795   t1795  S       s1795   t620 h h1736 h1746 h1748
4509  T       t1796   o739 b1793 b1727  G       s1795   t1795
4510  S       s1796   t620 h h1737 h1747 h1749  B       b1795   s1795
4511  G       s1796   t1796  T       t1796   o938 b1795 b1769
4512  B       b1796   s1796  B       b1796   t1796
4513  T       t1797   o939 b1796 b1770  T       t1797   o966 b1796 b983 b1782
4514  B       b1797   t1797  B       b1797   t1797
4515  T       t1798   o967 b1797 b984 b1783  T       t1798   o2 b1797
4516  B       b1798   t1798  B       b1798   t1798
4517  T       t1799   o2 b1798  T       t1799   o973 b1794 b983 b1798
4518  B       b1799   t1799  B       b1799   t1799
4519  T       t1800   o974 b1795 b984 b1799  T       t1800   o2 b1799
4520  B       b1800   t1800  B       b1800   t1800
4521  T       t1801   o2 b1800  T       t1801   o973 b1791 b4 b1800
4522  B       b1801   t1801  B       b1801   t1801
4523  T       t1802   o974 b1792 b4 b1801  T       t1802   o676 b1792 b1726
4524  B       b1802   t1802  S       s1802   t620 h h1736 h1746 h1748
4525  T       t1803   o676 b1793 b1727  G       s1802   t1802
4526  S       s1803   t620 h h1737 h1747 h1749  B       b1802   s1802
4527  G       s1803   t1803  T       t1803   o938 b1802 b1769
4528  B       b1803   s1803  B       b1803   t1803
4529  T       t1804   o939 b1803 b1770  T       t1804   o966 b1803 b4 b1798
4530  B       b1804   t1804  B       b1804   t1804
4531  T       t1805   o967 b1804 b4 b1799  H       h1804   v t1746
4532  B       b1805   t1805  S       s1804   t620 h h1736 h1746 h1748 h1804
4533  H       h1805   v t1747  G       s1804   t1737
4534  S       s1805   t620 h h1737 h1747 h1749 h1805  B       b1805   s1804
4535  G       s1805   t1738  T       t1805   o938 b1805 b1769
4536  B       b1806   s1805  B       b1806   t1805
4537  T       t1806   o939 b1806 b1770  T       t1806   o937 b1806 b4 b1782
4538  B       b1807   t1806  B       b1807   t1806
4539  T       t1807   o938 b1807 b4 b1783  B       b1808   t1745 v
4540  B       b1808   t1807  T       t1808   o711 b1808
4541  B       b1809   t1746 v  S       s1808   t620 h h1736 h1746 h1748
4542  T       t1809   o712 b1809  G       s1808   t1808
4543  S       s1809   t620 h h1737 h1747 h1749  B       b1809   s1808
4544  G       s1809   t1809  T       t1809   o938 b1809 b1769
4545  B       b1810   s1809  B       b1810   t1809
4546  T       t1810   o939 b1810 b1770  B       b1811   t1746 v
4547  B       b1811   t1810  T       t1811   o976 b1811
4548  B       b1812   t1747 v  S       s1811   t620 h h1736 h1746 h1748
4549  T       t1812   o977 b1812  G       s1811   t1811
4550  S       s1812   t620 h h1737 h1747 h1749  B       b1812   s1811
4551  G       s1812   t1812