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

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

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

revision 3556 by xiny, Mon Mar 11 10:35:54 2002 UTC revision 3557 by xiny, Tue Apr 2 08:18:40 2002 UTC
# Line 651  Line 651 
651  B       b241    t241  B       b241    t241
652  T       t242    o b7 b241  T       t242    o b7 b241
653  B       b242    t242  B       b242    t242
 T       t243    o b5 b242  
 B       b243    t243  
654  NSummary!resource       resource        resource Summary  NSummary!resource       resource        resource Summary
655  P       p243    String auto  P       p243    String auto
656  O       o243    resource p243  O       o243    resource p243
# Line 1040  Line 1038 
1038  B       b385    t385  B       b385    t385
1039  T       t386    o b258 b385  T       t386    o b258 b385
1040  B       b386    t386  B       b386    t386
 T       t387    o2 b5 b243 b386  
 B       b387    t387  
 T       t388    o1 b387  
 B       b388    t388  
1041  P       p388    Number 22  P       p388    Number 22
1042  P       p389    Number 43  P       p389    Number 43
1043  O       o389    location p388 p389  O       o389    location p388 p389
# Line 1083  Line 1077 
1077  B       b400    t400  B       b400    t400
1078  T       t401    o b400 b4  T       t401    o b400 b4
1079  B       b401    t401  B       b401    t401
1080  T       t402    o b401 b4  T       t1      o b401 b242
1081  B       b402    t402  B       b1      t1
1082  T       t403    o b399 b402  T       t2      o b399 b1
1083  B       b403    t403  B       b2      t2
1084  T       t404    o b397 b403  T       t3      o b397 b2
1085  B       b404    t404  B       b3      t3
1086  T       t405    o b395 b404  T       t249    o b395 b3
1087  B       b405    t405  B       b249    t249
1088  T       t406    o b393 b405  T       t281    o b393 b249
1089  B       b406    t406  B       b281    t281
1090  T       t407    o b391 b406  T       t286    o b391 b281
1091  B       b407    t407  B       b286    t286
1092  T       t408    o2 b391 b407 b386  T       t287    o b5 b286
1093  B       b408    t408  B       b287    t287
1094  T       t409    o389 b408  T       t350    o2 b5 b287 b386
1095  B       b409    t409  B       b533    t350
1096    T       t533    o1 b533
1097    B       b594    t533
1098    T       t594    o2 b391 b4 b386
1099    B       b599    t594
1100    T       t599    o389 b599
1101    B       b633    t599
1102  P       p409    Number 44  P       p409    Number 44
1103  P       p410    Number 68  P       p410    Number 68
1104  O       o410    location p409 p410  O       o410    location p409 p410
# Line 1620  Line 1620 
1620  O       o646    lid p601  O       o646    lid p601
1621  T       t646    o646  T       t646    o646
1622  B       b646    t646  B       b646    t646
 NSummary!prec   prec    prec Summary  
 P       p678    String prec_power  
 O       o678    prec p678  
 T       t678    o678  
 B       b678    t678  
1623  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
1624  P       p681    String power_df  P       p681    String power_df
1625  O       o681    dform p681  O       o681    dform p681
# Line 1633  Line 1628 
1628  O       o682    except_mode_df p682  O       o682    except_mode_df p682
1629  T       t682    o682  T       t682    o682
1630  B       b682    t682  B       b682    t682
 NSummary!prec_df        prec_df prec_df Summary  
 O       o683    prec_df p678  
 T       t683    o683  
 B       b683    t683  
1631  NSummary!parens_df      parens_df       parens_df Summary  NSummary!parens_df      parens_df       parens_df Summary
1632  O       o684    parens_df  O       o684    parens_df
1633  T       t684    o684  T       t684    o684
1634  B       b684    t684  B       b684    t684
1635  T       t685    o b684 b4  T       t685    o b684 b4
1636  B       b685    t685  B       b685    t685
 T       t686    o b683 b685  
 B       b686    t686  
 T       t687    o b682 b686  
 B       b687    t687  
1637  NSummary!df_term        df_term df_term Summary  NSummary!df_term        df_term df_term Summary
1638  O       o687    df_term  O       o687    df_term
1639  NPerv!string    string687       string Perv  NPerv!string    string687       string Perv
# Line 1686  Line 1673 
1673  B       b700    t700  B       b700    t700
1674  T       t701    o687 b700  T       t701    o687 b700
1675  B       b701    t701  B       b701    t701
 T       t702    o681 b687 b590 b701  
 B       b702    t702  
1676  T       t705    o b682 b4  T       t705    o b682 b4
1677  B       b705    t705  B       b705    t705
1678  T       t707    o689 b596  T       t707    o689 b596
# Line 1751  Line 1736 
1736  NCzf_itt_set!isset      isset   isset Czf_itt_set  NCzf_itt_set!isset      isset   isset Czf_itt_set
1737  O       o730    isset  O       o730    isset
1738  T       t731    o730 b588  T       t731    o730 b588
 S       s731    t726 h  
 G       s731    t731  
 B       b731    s731  
1739  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1740  NCzf_itt_member!mem     mem     mem Czf_itt_member  NCzf_itt_member!mem     mem     mem Czf_itt_member
1741  O       o732    mem  O       o732    mem
# Line 1773  Line 1755 
1755  B       b736    s736  B       b736    s736
1756  T       t737    o719 b736  T       t737    o719 b736
1757  B       b737    t737  B       b737    t737
 T       t738    o718 b735 b737  
 B       b738    t738  
1758  NSummary!interactive    interactive     interactive Summary  NSummary!interactive    interactive     interactive Summary
1759  O       o742    interactive  O       o742    interactive
1760  NSummary!ext_rule       ext_rule        ext_rule Summary  NSummary!ext_rule       ext_rule        ext_rule Summary
# Line 1793  Line 1773 
1773  O       o747    msequent  O       o747    msequent
1774  T       t747    o b734 b4  T       t747    o b734 b4
1775  B       b747    t747  B       b747    t747
 T       t748    o b731 b747  
 B       b748    t748  
 T       t749    o b729 b748  
 B       b749    t749  
 T       t750    o b727 b749  
 B       b750    t750  
 T       t751    o b723 b750  
 B       b751    t751  
 T       t752    o747 b736 b751  
 B       b752    t752  
1776  NSummary!parent_none    parent_none     parent_none Summary  NSummary!parent_none    parent_none     parent_none Summary
1777  O       o752    parent_none  O       o752    parent_none
1778  T       t753    o752  T       t753    o752
1779  B       b753    t753  B       b753    t753
 T       t754    o746 b752 b4 b753  
 B       b754    t754  
1780  H       h754    m t621  H       h754    m t621
1781  NItt_int_base!lt        lt      lt Itt_int_base  NItt_int_base!lt        lt      lt Itt_int_base
1782  O       o754    lt  O       o754    lt
# Line 1841  Line 1809 
1809  S       s766    t726 h h754 h757 h760  S       s766    t726 h h754 h757 h760
1810  G       s766    t766  G       s766    t766
1811  B       b766    s766  B       b766    s766
 T       t767    o747 b766 b751  
 B       b767    t767  
1812  T       t768    o586 b587 b588 b755  T       t768    o586 b587 b588 b755
1813  B       b768    t768  B       b768    t768
1814  T       t769    o730 b768  T       t769    o730 b768
1815  S       s769    t726 h h754 h757 h760  S       s769    t726 h h754 h757 h760
1816  G       s769    t769  G       s769    t769
1817  B       b769    s769  B       b769    s769
 T       t770    o747 b769 b751  
 B       b770    t770  
1818  H       h770    n t621  H       h770    n t621
1819  S       s770    t726 h h770 h754 h757 h760  S       s770    t726 h h770 h754 h757 h760
1820  G       s770    t769  G       s770    t769
1821  B       b771    s770  B       b771    s770
 T       t771    o747 b771 b751  
 B       b772    t771  
1822  S       s772    t726 h h770  S       s772    t726 h h770
1823  G       s772    t736  G       s772    t736
1824  B       b773    s772  B       b773    s772
 T       t773    o747 b773 b751  
 B       b774    t773  
1825  P       p774    String assertion  P       p774    String assertion
1826  O       o774    tactic_arg p774  O       o774    tactic_arg p774
1827  NItt_logic      Itt_logic       Itt_logic NIL  NItt_logic      Itt_logic       Itt_logic NIL
# Line 1872  Line 1832 
1832  S       s775    t726 h  S       s775    t726 h
1833  G       s775    t775  G       s775    t775
1834  B       b776    s775  B       b776    s775
 T       t776    o747 b776 b751  
 B       b777    t776  
1835  NSummary!arg_named      arg_named       arg_named Summary  NSummary!arg_named      arg_named       arg_named Summary
1836  P       p777    String d_auto  P       p777    String d_auto
1837  O       o777    arg_named p777  O       o777    arg_named p777
# Line 1886  Line 1844 
1844  B       b779    t779  B       b779    t779
1845  T       t780    o b779 b4  T       t780    o b779 b4
1846  B       b780    t780  B       b780    t780
 T       t781    o2 b754  
 B       b781    t781  
 T       t782    o774 b777 b780 b781  
 B       b782    t782  
 T       t783    o2 b782  
 B       b783    t783  
 T       t784    o746 b774 b4 b783  
 B       b784    t784  
 T       t785    o2 b784  
 B       b785    t785  
 T       t786    o746 b772 b4 b785  
 B       b786    t786  
 T       t787    o2 b786  
 B       b787    t787  
 T       t788    o746 b770 b4 b787  
 B       b788    t788  
 T       t789    o2 b788  
 B       b789    t789  
 T       t790    o746 b767 b4 b789  
 B       b790    t790  
1847  T       t791    o754 b756 b755  T       t791    o754 b756 b755
1848  H       h791    v t791  H       h791    v t791
1849  T       t792    o730 b763  T       t792    o730 b763
# Line 1913  Line 1851 
1851  S       s792    t726 h h754 h791 h792  S       s792    t726 h h754 h791 h792
1852  G       s792    t766  G       s792    t766
1853  B       b792    s792  B       b792    s792
 T       t793    o747 b792 b751  
 B       b793    t793  
1854  S       s793    t726 h h754 h791 h792  S       s793    t726 h h754 h791 h792
1855  G       s793    t769  G       s793    t769
1856  B       b794    s793  B       b794    s793
 T       t794    o747 b794 b751  
 B       b795    t794  
1857  S       s795    t726 h h770 h754 h791 h792  S       s795    t726 h h770 h754 h791 h792
1858  G       s795    t769  G       s795    t769
1859  B       b796    s795  B       b796    s795
 T       t796    o747 b796 b751  
 B       b797    t796  
 T       t797    o746 b797 b4 b785  
 B       b798    t797  
 T       t798    o2 b798  
 B       b799    t798  
 T       t799    o746 b795 b4 b799  
 B       b800    t799  
 T       t800    o2 b800  
 B       b801    t800  
 T       t801    o746 b793 b4 b801  
 B       b802    t801  
 T       t802    o b802 b4  
 B       b803    t802  
 T       t803    o b790 b803  
 B       b804    t803  
 T       t804    o745 b754 b804  
 B       b805    t804  
1860  P       p805    String "rwh reduce_ind_down 0 ttca"  P       p805    String "rwh reduce_ind_down 0 ttca"
1861  O       o805    ext_rule p805  O       o805    ext_rule p805
 T       t805    o745 b790 b4  
 B       b806    t805  
 T       t806    o805 b744 b806 b4 b4  
 B       b807    t806  
1862  P       p807    String "rwh reduce_ind_up 0 ttca"  P       p807    String "rwh reduce_ind_up 0 ttca"
1863  O       o807    ext_rule p807  O       o807    ext_rule p807
 T       t807    o745 b802 b4  
 B       b808    t807  
 T       t808    o807 b744 b808 b4 b4  
 B       b809    t808  
 T       t809    o b809 b4  
 B       b810    t809  
 T       t810    o b807 b810  
 B       b811    t810  
 T       t811    o743 b744 b805 b811 b4  
 B       b812    t811  
 T       t812    o742 b812  
 B       b813    t812  
1864  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
1865  P       p816    String []  P       p816    String []
1866  O       o816    uid p816  O       o816    uid p816
# Line 1976  Line 1876 
1876  B       b825    t825  B       b825    t825
1877  T       t826    o718 b735 b825  T       t826    o718 b735 b825
1878  B       b826    t826  B       b826    t826
 T       t831    o747 b824 b751  
 B       b831    t831  
 T       t832    o746 b831 b4 b753  
 B       b832    t832  
1879  T       t833    o732 b759 b733  T       t833    o732 b759 b733
1880  H       h833    z_1 t833  H       h833    z_1 t833
1881  T       t834    o732 b765 b733  T       t834    o732 b765 b733
1882  S       s834    t726 h h754 h757 h833  S       s834    t726 h h754 h757 h833
1883  G       s834    t834  G       s834    t834
1884  B       b834    s834  B       b834    s834
 T       t835    o747 b834 b751  
 B       b835    t835  
1885  T       t836    o732 b768 b733  T       t836    o732 b768 b733
1886  S       s836    t726 h h754 h757 h833  S       s836    t726 h h754 h757 h833
1887  G       s836    t836  G       s836    t836
1888  B       b836    s836  B       b836    s836
 T       t837    o747 b836 b751  
 B       b837    t837  
1889  S       s837    t726 h h770 h754 h757 h833  S       s837    t726 h h770 h754 h757 h833
1890  G       s837    t836  G       s837    t836
1891  B       b838    s837  B       b838    s837
 T       t838    o747 b838 b751  
 B       b839    t838  
1892  S       s839    t726 h h770  S       s839    t726 h h770
1893  G       s839    t824  G       s839    t824
1894  B       b840    s839  B       b840    s839
 T       t840    o747 b840 b751  
 B       b841    t840  
1895  B       b842    t824 n  B       b842    t824 n
1896  T       t842    o775 b621 b842  T       t842    o775 b621 b842
1897  S       s842    t726 h  S       s842    t726 h
1898  G       s842    t842  G       s842    t842
1899  B       b843    s842  B       b843    s842
 T       t843    o747 b843 b751  
 B       b844    t843  
 T       t844    o2 b832  
 B       b845    t844  
 T       t845    o774 b844 b780 b845  
 B       b846    t845  
 T       t846    o2 b846  
 B       b847    t846  
 T       t847    o746 b841 b4 b847  
 B       b848    t847  
 T       t848    o2 b848  
 B       b849    t848  
 T       t849    o746 b839 b4 b849  
 B       b850    t849  
 T       t850    o2 b850  
 B       b851    t850  
 T       t851    o746 b837 b4 b851  
 B       b852    t851  
 T       t852    o2 b852  
 B       b853    t852  
 T       t853    o746 b835 b4 b853  
 B       b854    t853  
1900  T       t854    o732 b763 b733  T       t854    o732 b763 b733
1901  H       h854    z_1 t854  H       h854    z_1 t854
1902  S       s854    t726 h h754 h791 h854  S       s854    t726 h h754 h791 h854
1903  G       s854    t834  G       s854    t834
1904  B       b855    s854  B       b855    s854
 T       t855    o747 b855 b751  
 B       b856    t855  
1905  S       s856    t726 h h754 h791 h854  S       s856    t726 h h754 h791 h854
1906  G       s856    t836  G       s856    t836
1907  B       b857    s856  B       b857    s856
 T       t857    o747 b857 b751  
 B       b858    t857  
1908  S       s858    t726 h h770 h754 h791 h854  S       s858    t726 h h770 h754 h791 h854
1909  G       s858    t836  G       s858    t836
1910  B       b859    s858  B       b859    s858
 T       t859    o747 b859 b751  
 B       b860    t859  
 T       t860    o746 b860 b4 b849  
 B       b861    t860  
 T       t861    o2 b861  
 B       b862    t861  
 T       t862    o746 b858 b4 b862  
 B       b863    t862  
 T       t863    o2 b863  
 B       b864    t863  
 T       t864    o746 b856 b4 b864  
 B       b865    t864  
 T       t865    o b865 b4  
 B       b866    t865  
 T       t866    o b854 b866  
 B       b867    t866  
 T       t867    o745 b832 b867  
 B       b868    t867  
 T       t868    o745 b854 b4  
 B       b869    t868  
 T       t869    o805 b744 b869 b4 b4  
 B       b870    t869  
 T       t870    o745 b865 b4  
 B       b871    t870  
 T       t871    o807 b744 b871 b4 b4  
 B       b872    t871  
 T       t872    o b872 b4  
 B       b873    t872  
 T       t873    o b870 b873  
 B       b874    t873  
 T       t874    o743 b744 b868 b874 b4  
 B       b875    t874  
 T       t875    o742 b875  
 B       b876    t875  
1911  P       p6      String power_fun  P       p6      String power_fun
1912  O       o8      rule p6  O       o8      rule p6
1913  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL  NCzf_itt_eq     Czf_itt_eq      Czf_itt_eq NIL
# Line 2124  Line 1952 
1952  B       b295    t295  B       b295    t295
1953  T       t296    o b245 b295  T       t296    o b245 b295
1954  B       b296    t296  B       b296    t296
 T       t298    o b729 b296  
 B       b298    t298  
 T       t299    o b727 b298  
 B       b299    t299  
 T       t300    o b723 b299  
 B       b300    t300  
 T       t303    o747 b268 b300  
 B       b303    t303  
 T       t304    o746 b303 b4 b753  
 B       b304    t304  
1955  P       p307    String wf  P       p307    String wf
1956  O       o307    tactic_arg p307  O       o307    tactic_arg p307
1957  H       h307    s1 t259  H       h307    s1 t259
# Line 2150  Line 1968 
1968  S       s887    t721 h  S       s887    t721 h
1969  G       s887    t887  G       s887    t887
1970  B       b887    s887  B       b887    s887
 T       t888    o719 b887  
 B       b888    t888  
1971  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1972  NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv  NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1973  O       o888    equiv  O       o888    equiv
# Line 2159  Line 1975 
1975  S       s889    t726 h  S       s889    t726 h
1976  G       s889    t889  G       s889    t889
1977  B       b889    s889  B       b889    s889
 T       t890    o719 b889  
 B       b890    t890  
1978  T       t891    o730 b622  T       t891    o730 b622
1979  S       s891    t726 h  S       s891    t726 h
1980  G       s891    t891  G       s891    t891
# Line 2183  Line 1997 
1997  S       s899    t726 h  S       s899    t726 h
1998  G       s899    t899  G       s899    t899
1999  B       b899    s899  B       b899    s899
 T       t900    o719 b899  
 B       b900    t900  
 T       t901    o718 b894 b900  
 B       b901    t901  
 P       p907    String "genAssumT [5] thenT dT 0 ttca thenT dT 2 ttca"  
 O       o907    ext_rule p907  
2000  T       t908    o b893 b4  T       t908    o b893 b4
2001  B       b908    t908  B       b908    t908
2002  T       t909    o b891 b908  T       t909    o b891 b908
# Line 2311  Line 2119 
2119  B       b961    t960  B       b961    t960
2120  T       t961    o746 b957 b4 b961  T       t961    o746 b957 b4 b961
2121  B       b962    t961  B       b962    t961
 T       t962    o b962 b4  
 B       b963    t962  
 T       t963    o b951 b963  
 B       b964    t963  
 T       t964    o b940 b964  
 B       b965    t964  
 T       t965    o745 b916 b965  
 B       b966    t965  
2122  P       p966    String "decideT << 'm = -1 in int >> ttca"  P       p966    String "decideT << 'm = -1 in int >> ttca"
2123  O       o966    ext_rule p966  O       o966    ext_rule p966
2124  NItt_int_base!minus     minus   minus Itt_int_base  NItt_int_base!minus     minus   minus Itt_int_base
# Line 2356  Line 2156 
2156  B       b978    t977  B       b978    t977
2157  P       p978    String "hypSubstT 5 0 ttca thenT rwh reduceC 0 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"  P       p978    String "hypSubstT 5 0 ttca thenT rwh reduceC 0 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
2158  O       o978    ext_rule p978  O       o978    ext_rule p978
 T       t978    o745 b971 b4  
 B       b979    t978  
 T       t979    o978 b744 b979 b4 b4  
 B       b980    t979  
2159  P       p980    String "rwh unfold_power 0 thenT rwh reduce_ind_down 0 ttca"  P       p980    String "rwh unfold_power 0 thenT rwh reduce_ind_down 0 ttca"
2160  O       o980    ext_rule p980  O       o980    ext_rule p980
2161  T       t980    o603 b587 b896 b918  T       t980    o603 b587 b896 b918
# Line 2420  Line 2216 
2216  B       b1006   t1005  B       b1006   t1005
2217  P       p1006   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; inv{'g; 'x}; power{'g; 'x; (('m +@ 1) +@ 1)}}; inv{'g; 'x}}; op{'g; inv{'g; 'x}; op{'g; power{'g; 'x; (('m +@ 1) +@ 1)}; inv{'g; 'x}}}} >>  0 ttca"  P       p1006   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; inv{'g; 'x}; power{'g; 'x; (('m +@ 1) +@ 1)}}; inv{'g; 'x}}; op{'g; inv{'g; 'x}; op{'g; power{'g; 'x; (('m +@ 1) +@ 1)}; inv{'g; 'x}}}} >>  0 ttca"
2218  O       o1006   ext_rule p1006  O       o1006   ext_rule p1006
 T       t1006   o745 b1000 b4  
 B       b1007   t1006  
 T       t1007   o1006 b744 b1007 b4 b4  
 B       b1008   t1007  
2219  P       p1008   String "splitIntT << 'm >> << minus{1} >> thenT autoT"  P       p1008   String "splitIntT << 'm >> << minus{1} >> thenT autoT"
2220  O       o1008   ext_rule p1008  O       o1008   ext_rule p1008
2221  T       t1008   o754 b755 b967  T       t1008   o754 b755 b967
# Line 2672  Line 2464 
2464  B       b1102   t1101  B       b1102   t1101
2465  T       t1102   o b1102 b4  T       t1102   o b1102 b4
2466  B       b1103   t1102  B       b1103   t1102
 T       t1103   o b1008 b1103  
 B       b1104   t1103  
 T       t1104   o980 b744 b1006 b1104 b4  
 B       b1105   t1104  
 T       t1105   o b1105 b4  
 B       b1106   t1105  
 T       t1106   o b980 b1106  
 B       b1107   t1106  
 T       t1107   o966 b744 b978 b1107 b4  
 B       b1108   t1107  
2467  P       p1108   String "rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"  P       p1108   String "rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
2468  O       o1108   ext_rule p1108  O       o1108   ext_rule p1108
2469  T       t1108   o603 b587 b622 b610  T       t1108   o603 b587 b622 b610
# Line 2946  Line 2728 
2728  B       b1221   t1220  B       b1221   t1220
2729  P       p1221   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; id{'g}}; 'x} >> 0 ttca"  P       p1221   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; id{'g}}; 'x} >> 0 ttca"
2730  O       o1221   ext_rule p1221  O       o1221   ext_rule p1221
 T       t1221   o745 b1219 b4  
 B       b1222   t1221  
 T       t1222   o1221 b744 b1222 b4 b4  
 B       b1223   t1222  
 T       t1223   o b1223 b4  
 B       b1224   t1223  
 T       t1224   o1108 b744 b1221 b1224 b4  
 B       b1225   t1224  
2731  P       p1225   String "decideT << 'm = 1 in int >> ttca"  P       p1225   String "decideT << 'm = 1 in int >> ttca"
2732  O       o1225   ext_rule p1225  O       o1225   ext_rule p1225
2733  T       t1225   o721 b621 b755 b606  T       t1225   o721 b621 b755 b606
# Line 3417  Line 3191 
3191  B       b1419   t1418  B       b1419   t1418
3192  T       t1419   o b1419 b4  T       t1419   o b1419 b4
3193  B       b1420   t1419  B       b1420   t1419
 T       t1420   o745 b1383 b1420  
 B       b1421   t1420  
3194  T       t1421   o603 b587 b622 b622  T       t1421   o603 b587 b622 b622
3195  B       b1422   t1421  B       b1422   t1421
3196  T       t1422   o603 b587 b1422 b896  T       t1422   o603 b587 b1422 b896
# Line 3453  Line 3225 
3225  B       b1434   t1433  B       b1434   t1433
3226  T       t1434   o b1427 b1434  T       t1434   o b1427 b1434
3227  B       b1435   t1434  B       b1435   t1434
 T       t1435   o745 b1419 b1435  
 B       b1436   t1435  
3228  P       p1436   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; 'x}; inv{'g; 'x}}; op{'g; 'x; op{'g; 'x; inv{'g; 'x}}}} >> 0 ttca"  P       p1436   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; 'x}; inv{'g; 'x}}; op{'g; 'x; op{'g; 'x; inv{'g; 'x}}}} >> 0 ttca"
3229  O       o1436   ext_rule p1436  O       o1436   ext_rule p1436
3230  T       t1436   o603 b587 b622 b896  T       t1436   o603 b587 b622 b896
# Line 3473  Line 3243 
3243  B       b1442   t1441  B       b1442   t1441
3244  T       t1442   o b1442 b4  T       t1442   o b1442 b4
3245  B       b1443   t1442  B       b1443   t1442
 T       t1443   o745 b1427 b1443  
 B       b1444   t1443  
3246  P       p1444   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; inv{'g; 'x}}; id{'g}} >> 0 ttca"  P       p1444   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; inv{'g; 'x}}; id{'g}} >> 0 ttca"
3247  O       o1444   ext_rule p1444  O       o1444   ext_rule p1444
 T       t1444   o745 b1442 b4  
 B       b1445   t1444  
 T       t1445   o1444 b744 b1445 b4 b4  
 B       b1446   t1445  
 T       t1446   o b1446 b4  
 B       b1447   t1446  
 T       t1447   o1436 b744 b1444 b1447 b4  
 B       b1448   t1447  
3248  P       p1448   String "autoT thenT rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 9 ttca"  P       p1448   String "autoT thenT rwh unfold_equiv_fun_set 0 thenT autoT thenT rwh unfold_equiv 9 ttca"
3249  O       o1448   ext_rule p1448  O       o1448   ext_rule p1448
 T       t1448   o745 b1433 b4  
 B       b1449   t1448  
 T       t1449   o1448 b744 b1449 b4 b4  
 B       b1450   t1449  
 T       t1450   o b1450 b4  
 B       b1451   t1450  
 T       t1451   o b1448 b1451  
 B       b1452   t1451  
 T       t1452   o1221 b744 b1436 b1452 b4  
 B       b1453   t1452  
 T       t1453   o b1453 b4  
 B       b1454   t1453  
 T       t1454   o1385 b744 b1421 b1454 b4  
 B       b1455   t1454  
 T       t1455   o b1455 b4  
 B       b1456   t1455  
 T       t1456   o1236 b744 b1385 b1456 b4  
 B       b1457   t1456  
3250  P       p1457   String "rwh unfold_power 0 thenT rwh reduce_ind_up 0 ttca"  P       p1457   String "rwh unfold_power 0 thenT rwh reduce_ind_up 0 ttca"
3251  O       o1457   ext_rule p1457  O       o1457   ext_rule p1457
3252  B       b1458   t988  B       b1458   t988
# Line 3890  Line 3632 
3632  B       b1619   t1618  B       b1619   t1618
3633  P       p1619   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; power{'g; 'x; 'm}}; inv{'g; 'x}}; op{'g; 'x; op{'g; power{'g; 'x; 'm}; inv{'g; 'x}}}} >> 0 ttca"  P       p1619   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; power{'g; 'x; 'm}}; inv{'g; 'x}}; op{'g; 'x; op{'g; power{'g; 'x; 'm}; inv{'g; 'x}}}} >> 0 ttca"
3634  O       o1619   ext_rule p1619  O       o1619   ext_rule p1619
 T       t1619   o745 b1617 b4  
 B       b1620   t1619  
 T       t1620   o1619 b744 b1620 b4 b4  
 B       b1621   t1620  
 T       t1621   o b1621 b4  
 B       b1622   t1621  
 T       t1622   o1474 b744 b1619 b1622 b4  
 B       b1623   t1622  
3635  P       p1623   String "assertT << (0 +@ 0) < ('m +@ 1) >> thenT autoT"  P       p1623   String "assertT << (0 +@ 0) < ('m +@ 1) >> thenT autoT"
3636  O       o1623   ext_rule p1623  O       o1623   ext_rule p1623
3637  T       t1623   o605 b756 b756  T       t1623   o605 b756 b756
# Line 4006  Line 3740 
3740  B       b1667   t1666  B       b1667   t1666
3741  T       t1667   o b1667 b4  T       t1667   o b1667 b4
3742  B       b1668   t1667  B       b1668   t1667
 T       t1668   o b1623 b1668  
 B       b1669   t1668  
 T       t1669   o1457 b744 b1474 b1669 b4  
 B       b1670   t1669  
 T       t1670   o b1670 b4  
 B       b1671   t1670  
 T       t1671   o b1457 b1671  
 B       b1672   t1671  
 T       t1672   o1225 b744 b1236 b1672 b4  
 B       b1673   t1672  
 T       t1673   o b1673 b4  
 B       b1674   t1673  
 T       t1674   o b1225 b1674  
 B       b1675   t1674  
 T       t1675   o b1108 b1675  
 B       b1676   t1675  
 T       t1676   o907 b744 b966 b1676 b4  
 B       b1677   t1676  
 T       t1677   o742 b1677  
 B       b1678   t1677  
3743  O       o1685   location p p  O       o1685   location p p
3744  P       p1685   String power_property2  P       p1685   String power_property2
3745  O       o1686   rule p1685  O       o1686   rule p1685
# Line 4035  Line 3749 
3749  S       s1687   t726 h  S       s1687   t726 h
3750  G       s1687   t1687  G       s1687   t1687
3751  B       b1687   s1687  B       b1687   s1687
 T       t1688   o719 b1687  
 B       b1688   t1688  
 T       t1689   o718 b894 b1688  
 B       b1689   t1689  
3752  T       t1696   o747 b1687 b914  T       t1696   o747 b1687 b914
3753  B       b1696   t1696  B       b1696   t1696
3754  T       t1697   o746 b1696 b4 b753  T       t1697   o746 b1696 b4 b753
# Line 4127  Line 3837 
3837  B       b1732   t1731  B       b1732   t1731
3838  T       t1732   o746 b1728 b4 b1732  T       t1732   o746 b1728 b4 b1732
3839  B       b1733   t1732  B       b1733   t1732
 T       t1733   o b1733 b4  
 B       b1734   t1733  
 T       t1734   o b1725 b1734  
 B       b1735   t1734  
 T       t1735   o b1717 b1735  
 B       b1736   t1735  
 T       t1736   o745 b1697 b1736  
 B       b1737   t1736  
3840  S       s1737   t726 h h754 h757 h1699 h968  S       s1737   t726 h h754 h757 h1699 h968
3841  G       s1737   t1701  G       s1737   t1701
3842  B       b1738   s1737  B       b1738   s1737
# Line 4423  Line 4125 
4125  B       b1860   t1859  B       b1860   t1859
4126  P       p1860   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 'x}; id{'g}}; inv{'g; 'x}} >> 0 ttca"  P       p1860   String "equivSubstT << equiv{car{'g}; 'R; op{'g; inv{'g; 'x}; id{'g}}; inv{'g; 'x}} >> 0 ttca"
4127  O       o1860   ext_rule p1860  O       o1860   ext_rule p1860
 T       t1860   o745 b1858 b4  
 B       b1861   t1860  
 T       t1861   o1860 b744 b1861 b4 b4  
 B       b1862   t1861  
 T       t1862   o b1862 b4  
 B       b1863   t1862  
 T       t1863   o1747 b744 b1860 b1863 b4  
 B       b1864   t1863  
4128  T       t1864   o603 b587 b983 b622  T       t1864   o603 b587 b983 b622
4129  B       b1865   t1864  B       b1865   t1864
4130  T       t1865   o888 b733 b886 b1865 b981  T       t1865   o888 b733 b886 b1865 b981
# Line 4470  Line 4164 
4164  B       b1880   t1879  B       b1880   t1879
4165  P       p1880   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; inv{'g; 'x}; power{'g; 'x; ('m +@ 1)}}; 'x}; op{'g; inv{'g; 'x}; op{'g; power{'g; 'x; ('m +@ 1)}; 'x}}} >> 0 ttca"  P       p1880   String "equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; inv{'g; 'x}; power{'g; 'x; ('m +@ 1)}}; 'x}; op{'g; inv{'g; 'x}; op{'g; power{'g; 'x; ('m +@ 1)}; 'x}}} >> 0 ttca"
4166  O       o1880   ext_rule p1880  O       o1880   ext_rule p1880
 T       t1880   o745 b1874 b4  
 B       b1881   t1880  
 T       t1881   o1880 b744 b1881 b4 b4  
 B       b1882   t1881  
4167  P       p1882   String "splitIntT << 'm >> << minus{1} >> ttca"  P       p1882   String "splitIntT << 'm >> << minus{1} >> ttca"
4168  O       o1882   ext_rule p1882  O       o1882   ext_rule p1882
4169  S       s1882   t726 h h754 h757 h1699 h972 h1008  S       s1882   t726 h h754 h757 h1699 h972 h1008
# Line 4629  Line 4319 
4319  B       b1951   t1950  B       b1951   t1950
4320  T       t1951   o b1951 b4  T       t1951   o b1951 b4
4321  B       b1952   t1951  B       b1952   t1951
 T       t1952   o b1882 b1952  
 B       b1953   t1952  
 T       t1953   o980 b744 b1880 b1953 b4  
 B       b1954   t1953  
 T       t1954   o b1954 b4  
 B       b1955   t1954  
 T       t1955   o b1864 b1955  
 B       b1956   t1955  
 T       t1956   o966 b744 b1747 b1956 b4  
 B       b1957   t1956  
 T       t1957   o745 b1725 b4  
 B       b1958   t1957  
 T       t1958   o1108 b744 b1958 b4 b4  
 B       b1959   t1958  
4322  S       s1959   t726 h h754 h791 h1726 h1225  S       s1959   t726 h h754 h791 h1726 h1225
4323  G       s1959   t1701  G       s1959   t1701
4324  B       b1960   s1959  B       b1960   s1959
# Line 5005  Line 4681 
4681  B       b2106   t2105  B       b2106   t2105
4682  T       t2106   o746 b2085 b4 b2106  T       t2106   o746 b2085 b4 b2106
4683  B       b2107   t2106  B       b2107   t2106
 T       t2107   o b2107 b4  
 B       b2108   t2107  
 T       t2108   o745 b2081 b2108  
 B       b2109   t2108  
4684  P       p2109   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; op{'g; 'x; id{'g}}}; op{'g; op{'g; 'x; 'x}; id{'g}}} >> 0 ttca thenT equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; 'x}; id{'g}}; op{'g; 'x; 'x}} >> 0 ttca"  P       p2109   String "equivSubstT << equiv{car{'g}; 'R; op{'g; 'x; op{'g; 'x; id{'g}}}; op{'g; op{'g; 'x; 'x}; id{'g}}} >> 0 ttca thenT equivSubstT << equiv{car{'g}; 'R; op{'g; op{'g; 'x; 'x}; id{'g}}; op{'g; 'x; 'x}} >> 0 ttca"
4685  O       o2109   ext_rule p2109  O       o2109   ext_rule p2109
 T       t2109   o745 b2107 b4  
 B       b2110   t2109  
 T       t2110   o2109 b744 b2110 b4 b4  
 B       b2111   t2110  
 T       t2111   o b2111 b4  
 B       b2112   t2111  
 T       t2112   o2083 b744 b2109 b2112 b4  
 B       b2113   t2112  
 T       t2113   o b2113 b4  
 B       b2114   t2113  
 T       t2114   o1236 b744 b2083 b2114 b4  
 B       b2115   t2114  
4686  T       t2115   o603 b587 b1460 b622  T       t2115   o603 b587 b1460 b622
4687  B       b2116   t2115  B       b2116   t2115
4688  T       t2116   o888 b733 b886 b2116 b1458  T       t2116   o888 b733 b886 b2116 b1458
# Line 5073  Line 4733 
4733  B       b2135   t2134  B       b2135   t2134
4734  T       t2135   o b2135 b4  T       t2135   o b2135 b4
4735  B       b2136   t2135  B       b2136   t2135
 T       t2136   o745 b2124 b2136  
 B       b2137   t2136  
4736  P       p2137   String "rwh unfold_sub 4 thenT rwh add_normalizeC 4 thenT rwh reduceC 4 thenT rwh unfold_sub 0 thenT rwh add_normalizeC 0 thenT rwh reduceC 0 ttca"  P       p2137   String "rwh unfold_sub 4 thenT rwh add_normalizeC 4 thenT rwh reduceC 4 thenT rwh unfold_sub 0 thenT rwh add_normalizeC 0 thenT rwh reduceC 0 ttca"
4737  O       o2137   ext_rule p2137  O       o2137   ext_rule p2137
 T       t2137   o745 b2135 b4  
 B       b2138   t2137  
 T       t2138   o2137 b744 b2138 b4 b4  
 B       b2139   t2138  
 T       t2139   o b2139 b4  
 B       b2140   t2139  
 T       t2140   o2130 b744 b2137 b2140 b4  
 B       b2141   t2140  
4738  S       s2141   t721 h h754 h791 h1726 h1230  S       s2141   t721 h h754 h791 h1726 h1230
4739  G       s2141   t1624  G       s2141   t1624
4740  B       b2142   s2141  B       b2142   s2141
# Line 5161  Line 4811 
4811  B       b2174   t2173  B       b2174   t2173
4812  T       t2174   o b2174 b4  T       t2174   o b2174 b4
4813  B       b2175   t2174  B       b2175   t2174
 T       t2175   o b2141 b2175  
 B       b2176   t2175  
 T       t2176   o1457 b744 b2130 b2176 b4  
 B       b2177   t2176  
 T       t2177   o b2177 b4  
 B       b2178   t2177  
 T       t2178   o b2115 b2178  
 B       b2179   t2178  
 T       t2179   o1225 b744 b1969 b2179 b4  
 B       b2180   t2179  
 T       t2180   o b2180 b4  
 B       b2181   t2180  
 T       t2181   o b1959 b2181  
 B       b2182   t2181  
 T       t2182   o b1957 b2182  
 B       b2183   t2182  
 T       t2183   o907 b744 b1737 b2183 b4  
 B       b2184   t2183  
 T       t2184   o742 b2184  
 B       b2185   t2184  
 P       p2192   String power_simplify  
 O       o2192   rule p2192  
4814  T       t2193   o721 b621 b755 b755  T       t2193   o721 b621 b755 b755
 S       s2193   t726 h  
 G       s2193   t2193  
 B       b2193   s2193  
4815  T       t2195   o603 b587 b923 b898  T       t2195   o603 b587 b923 b898
4816  B       b2195   t2195  B       b2195   t2195
4817  T       t2196   o605 b755 b589  T       t2196   o605 b755 b589
4818  B       b2196   t2196  B       b2196   t2196
4819  T       t2197   o586 b587 b622 b2196  T       t2197   o586 b587 b622 b2196
4820  B       b2197   t2197  B       b2197   t2197
 T       t2198   o888 b733 b886 b2195 b2197  
 S       s2198   t726 h  
 G       s2198   t2198  
 B       b2198   s2198  
 T       t2199   o719 b2198  
 B       b2199   t2199  
 T       t2200   o718 b894 b2199  
 B       b2200   t2200  
 T       t2208   o b2193 b910  
 B       b2208   t2208  
 T       t2209   o b889 b2208  
 B       b2209   t2209  
 T       t2210   o b727 b2209  
 B       b2210   t2210  
 T       t2211   o b723 b2210  
 B       b2211   t2211  
 T       t2212   o b887 b2211  
 B       b2212   t2212  
 T       t2213   o747 b2198 b2212  
 B       b2213   t2213  
 T       t2214   o746 b2213 b4 b753  
 B       b2214   t2214  
4821  T       t2224   o730 b596  T       t2224   o730 b596
 S       s2224   t726 h  
 G       s2224   t2224  
 B       b2224   s2224  
4822  T       t2226   o732 b596 b733  T       t2226   o732 b596 b733
4823  S       s2226   t726 h  S       s2226   t726 h
4824  G       s2226   t2226  G       s2226   t2226
4825  B       b2226   s2226  B       b2226   s2226
4826  T       t2227   o719 b2226  T       t2227   o719 b2226
4827  B       b2227   t2227  B       b2227   t2227
 T       t2234   o b2226 b4  
 B       b2234   t2234  
 T       t2235   o b2224 b2234  
 B       b2235   t2235  
4828  NCzf_itt_subset Czf_itt_subset  Czf_itt_subset NIL  NCzf_itt_subset Czf_itt_subset  Czf_itt_subset NIL
4829  NCzf_itt_subset!subset  subset  subset Czf_itt_subset  NCzf_itt_subset!subset  subset  subset Czf_itt_subset
4830  O       o2250   subset  O       o2250   subset
# Line 5248  Line 4844 
4844  S       s322    t721 h h307 h308 h319  S       s322    t721 h h307 h308 h319
4845  G       s322    t322  G       s322    t322
4846  B       b322    s322  B       b322    s322
 T       t330    o747 b322 b300  
 B       b330    t330  
4847  T       t331    o586 b587 b320 b589  T       t331    o586 b587 b320 b589
4848  B       b331    t331  B       b331    t331
4849  T       t334    o730 b331  T       t334    o730 b331
4850  S       s334    t721 h h307 h308 h319  S       s334    t721 h h307 h308 h319
4851  G       s334    t334  G       s334    t334
4852  B       b334    s334  B       b334    s334
 T       t339    o747 b334 b300  
 B       b339    t339  
4853  T       t340    o12 b2273  T       t340    o12 b2273
4854  B       b340    t340  B       b340    t340
4855  T       t345    o586 b587 b340 b589  T       t345    o586 b587 b340 b589
# Line 5266  Line 4858 
4858  S       s346    t726 h h307 h308 h319  S       s346    t726 h h307 h308 h319
4859  G       s346    t346  G       s346    t346
4860  B       b346    s346  B       b346    s346
 T       t348    o747 b346 b300  
 B       b348    t348  
4861  NItt_logic!implies      implies implies Itt_logic  NItt_logic!implies      implies implies Itt_logic
4862  O       o348    implies  O       o348    implies
4863  B       b350    t319  B       b350    t319
# Line 5276  Line 4866 
4866  S       s357    t726 h h307 h308  S       s357    t726 h h307 h308
4867  G       s357    t357  G       s357    t357
4868  B       b361    s357  B       b361    s357
 T       t361    o747 b361 b300  
 B       b362    t361  
4869  B       b365    t259  B       b365    t259
4870  B       b369    t357 s2  B       b369    t357 s2
4871  T       t369    o775 b365 b369  T       t369    o775 b365 b369
4872  S       s369    t726 h h307  S       s369    t726 h h307
4873  G       s369    t369  G       s369    t369
4874  B       b370    s369  B       b370    s369
 T       t370    o747 b370 b300  
 B       b389    t370  
4875  B       b410    t369 s1  B       b410    t369 s1
4876  T       t410    o775 b365 b410  T       t410    o775 b365 b410
4877  S       s410    t726 h  S       s410    t726 h
4878  G       s410    t410  G       s410    t410
4879  B       b423    s410  B       b423    s410
 T       t423    o747 b423 b300  
 B       b424    t423  
 T       t424    o2 b304  
 B       b425    t424  
 T       t425    o746 b424 b780 b425  
 B       b434    t425  
 T       t434    o2 b434  
 B       b435    t434  
 T       t435    o746 b389 b780 b435  
 B       b443    t435  
 T       t443    o2 b443  
 B       b444    t443  
 T       t444    o746 b362 b780 b444  
 B       b452    t444  
 T       t452    o2 b452  
 B       b453    t452  
 T       t453    o746 b348 b780 b453  
 B       b461    t453  
 T       t461    o2 b461  
 B       b462    t461  
 T       t462    o307 b339 b780 b462  
 B       b470    t462  
 T       t470    o2 b470  
 B       b471    t470  
 T       t471    o307 b330 b4 b471  
 B       b479    t471  
4880  T       t479    o730 b340  T       t479    o730 b340
4881  S       s479    t721 h h307 h308 h319  S       s479    t721 h h307 h308 h319
4882  G       s479    t479  G       s479    t479
4883  B       b480    s479  B       b480    s479
 T       t480    o747 b480 b300  
 B       b488    t480  
4884  T       t488    o730 b345  T       t488    o730 b345
4885  S       s488    t721 h h307 h308 h319  S       s488    t721 h h307 h308 h319
4886  G       s488    t488  G       s488    t488
4887  B       b489    s488  B       b489    s488
 T       t489    o747 b489 b300  
 B       b497    t489  
 T       t497    o307 b497 b780 b462  
 B       b498    t497  
 T       t498    o2 b498  
 B       b504    t498  
 T       t504    o307 b488 b4 b504  
 B       b505    t504  
4888  NCzf_itt_eq!eq  eq      eq Czf_itt_eq  NCzf_itt_eq!eq  eq      eq Czf_itt_eq
4889  O       o507    eq  O       o507    eq
4890  T       t511    o507 b331 b345  T       t511    o507 b331 b345
4891  S       s511    t726 h h307 h308 h319  S       s511    t726 h h307 h308 h319
4892  G       s511    t511  G       s511    t511
4893  B       b511    s511  B       b511    s511
 T       t512    o747 b511 b300  
 B       b512    t512  
 T       t518    o746 b512 b4 b462  
 B       b518    t518  
 T       t519    o b518 b4  
 B       b519    t519  
 T       t525    o b505 b519  
 B       b525    t525  
 T       t526    o b479 b525  
 B       b526    t526  
 T       t532    o745 b304 b526  
 B       b532    t532  
4894  P       p534    String "funSetT 2 ttca"  P       p534    String "funSetT 2 ttca"
4895  O       o535    ext_rule p534  O       o535    ext_rule p534
 T       t540    o745 b479 b4  
 B       b540    t540  
 T       t541    o535 b744 b540 b4 b4  
 B       b541    t541  
4896  P       p542    String "funSetT 3 ttca"  P       p542    String "funSetT 3 ttca"
4897  O       o543    ext_rule p542  O       o543    ext_rule p542
 T       t548    o745 b505 b4  
 B       b548    t548  
 T       t549    o543 b744 b548 b4 b4  
 B       b549    t549  
4898  P       p550    String "assertT << isset{'f['s1]} >> ttca"  P       p550    String "assertT << isset{'f['s1]} >> ttca"
4899  O       o551    ext_rule p550  O       o551    ext_rule p550
4900  S       s551    t726 h h307 h308 h319  S       s551    t726 h h307 h308 h319
4901  G       s551    t322  G       s551    t322
4902  B       b556    s551  B       b556    s551
 T       t556    o747 b556 b300  
 B       b557    t556  
 T       t557    o2 b518  
 B       b563    t557  
 T       t563    o774 b557 b4 b563  
 B       b564    t563  
4903  H       h564    v t322  H       h564    v t322
4904  S       s564    t726 h h307 h308 h319 h564  S       s564    t726 h h307 h308 h319 h564
4905  G       s564    t511  G       s564    t511
4906  B       b570    s564  B       b570    s564
 T       t570    o747 b570 b300  
 B       b571    t570  
 T       t571    o746 b571 b4 b563  
 B       b577    t571  
 T       t577    o b577 b4  
 B       b578    t577  
 T       t578    o b564 b578  
 B       b584    t578  
 T       t584    o745 b518 b584  
 B       b585    t584  
 T       t585    o745 b564 b4  
 B       b586    t585  
 T       t586    o535 b744 b586 b4 b4  
 B       b593    t586  
4907  P       p596    String "assertT << isset{'f['s2]} >> ttca"  P       p596    String "assertT << isset{'f['s2]} >> ttca"
4908  O       o597    ext_rule p596  O       o597    ext_rule p596
4909  S       s597    t726 h h307 h308 h319 h564  S       s597    t726 h h307 h308 h319 h564
4910  G       s597    t479  G       s597    t479
4911  B       b600    s597  B       b600    s597
 T       t600    o747 b600 b300  
 B       b601    t600  
 T       t601    o2 b577  
 B       b602    t601  
 T       t602    o774 b601 b4 b602  
 B       b603    t602  
4912  H       h603    v_1 t479  H       h603    v_1 t479
4913  S       s603    t726 h h307 h308 h319 h564 h603  S       s603    t726 h h307 h308 h319 h564 h603
4914  G       s603    t511  G       s603    t511
4915  B       b605    s603  B       b605    s603
 T       t605    o747 b605 b300  
 B       b618    t605  
 T       t618    o746 b618 b4 b602  
 B       b619    t618  
 T       t619    o b619 b4  
 B       b620    t619  
 T       t620    o b603 b620  
 B       b627    t620  
 T       t627    o745 b577 b627  
 B       b628    t627  
 T       t628    o745 b603 b4  
 B       b629    t628  
 T       t629    o543 b744 b629 b4 b4  
 B       b632    t629  
4916  P       p636    String "genAssumT [3] thenT autoT thenT dT 7 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"  P       p636    String "genAssumT [3] thenT autoT thenT dT 7 ttca thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
4917  O       o641    ext_rule p636  O       o641    ext_rule p636
4918  H       h641    v_2 t757  H       h641    v_2 t757
# Line 5456  Line 4946 
4946  S       s743    t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s743    t726 h h307 h308 h319 h564 h603 h754 h641 h656
4947  G       s743    t743  G       s743    t743
4948  B       b743    s743  B       b743    s743
 T       t745    o747 b743 b300  
 B       b745    t745  
4949  T       t746    o586 b587 b320 b755  T       t746    o586 b587 b320 b755
4950  B       b746    t746  B       b746    t746
4951  T       t772    o586 b587 b340 b755  T       t772    o586 b587 b340 b755
# Line 5466  Line 4954 
4954  S       s796    t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s796    t726 h h307 h308 h319 h564 h603 h754 h641 h656
4955  G       s796    t795  G       s796    t795
4956  B       b814    s796  B       b814    s796
 T       t814    o747 b814 b300  
 B       b815    t814  
4957  S       s815    t726 h h307 h308 h319 h564 h603 h770 h754 h641 h656  S       s815    t726 h h307 h308 h319 h564 h603 h770 h754 h641 h656
4958  G       s815    t795  G       s815    t795
4959  B       b823    s815  B       b823    s815
 T       t823    o747 b823 b300  
 B       b833    t823  
4960  S       s833    t726 h h307 h308 h319 h564 h603 h770  S       s833    t726 h h307 h308 h319 h564 h603 h770
4961  G       s833    t511  G       s833    t511
4962  B       b877    s833  B       b877    s833
 T       t877    o747 b877 b300  
 B       b884    t877  
4963  B       b885    t511 n  B       b885    t511 n
4964  T       t885    o775 b621 b885  T       t885    o775 b621 b885
4965  S       s885    t726 h h307 h308 h319 h564 h603  S       s885    t726 h h307 h308 h319 h564 h603
4966  G       s885    t885  G       s885    t885
4967  B       b921    s885  B       b921    s885
 T       t927    o747 b921 b300  
 B       b1038   t927  
 T       t1038   o2 b619  
 B       b1040   t1038  
 T       t1112   o774 b1038 b780 b1040  
 B       b1679   t1112  
 T       t1679   o2 b1679  
 B       b1699   t1679  
 T       t1704   o746 b884 b4 b1699  
 B       b2186   t1704  
 T       t2186   o2 b2186  
 B       b2217   t2186  
 T       t2217   o746 b833 b4 b2217  
 B       b2243   t2217  
 T       t2243   o2 b2243  
 B       b2261   t2243  
 T       t2261   o746 b815 b4 b2261  
 B       b2268   t2261  
 T       t2268   o2 b2268  
 B       b2269   t2268  
 T       t2269   o746 b745 b4 b2269  
 B       b2292   t2269  
4968  H       h2292   v_2 t791  H       h2292   v_2 t791
4969  T       t2292   o507 b662 b715  T       t2292   o507 b662 b715
4970  H       h2293   z t2292  H       h2293   z t2292
4971  S       s2293   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293  S       s2293   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
4972  G       s2293   t743  G       s2293   t743
4973  B       b2299   s2293  B       b2299   s2293
 T       t2299   o747 b2299 b300  
 B       b2312   t2299  
4974  S       s2312   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293  S       s2312   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
4975  G       s2312   t795  G       s2312   t795
4976  B       b2313   s2312  B       b2313   s2312
 T       t2313   o747 b2313 b300  
 B       b2328   t2313  
4977  S       s2328   t726 h h307 h308 h319 h564 h603 h770 h754 h2292 h2293  S       s2328   t726 h h307 h308 h319 h564 h603 h770 h754 h2292 h2293
4978  G       s2328   t795  G       s2328   t795
4979  B       b2381   s2328  B       b2381   s2328
 T       t2382   o747 b2381 b300  
 B       b2382   t2382  
 T       t2383   o746 b2382 b4 b2217  
 B       b2383   t2383  
 T       t2384   o2 b2383  
 B       b2384   t2384  
 T       t2385   o746 b2328 b4 b2384  
 B       b2385   t2385  
 T       t2386   o2 b2385  
 B       b2386   t2386  
 T       t2387   o746 b2312 b4 b2386  
 B       b2387   t2387  
 T       t2388   o b2387 b4  
 B       b2388   t2388  
 T       t2389   o b2292 b2388  
 B       b2389   t2389  
 T       t2390   o745 b619 b2389  
 B       b2390   t2390  
4980  B       b2391   t661  B       b2391   t661
4981  B       b2392   t704  B       b2392   t704
4982  T       t2392   o507 b2391 b2392  T       t2392   o507 b2391 b2392
4983  S       s2392   t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s2392   t726 h h307 h308 h319 h564 h603 h754 h641 h656
4984  G       s2392   t2392  G       s2392   t2392
4985  B       b2393   s2392  B       b2393   s2392
 T       t2393   o747 b2393 b300  
 B       b2394   t2393  
 T       t2394   o2 b2292  
 B       b2395   t2394  
 T       t2395   o746 b2394 b4 b2395  
 B       b2396   t2395  
 T       t2396   o b2396 b4  
 B       b2397   t2396  
 T       t2397   o745 b2292 b2397  
 B       b2398   t2397  
4986  P       p2398   String "setSubstT << equal{power{'g; 'f['s1]; ('m +@ 1)}; power{'g; 'f['s2]; ('m +@ 1)}} >> 0 thenT autoT"  P       p2398   String "setSubstT << equal{power{'g; 'f['s1]; ('m +@ 1)}; power{'g; 'f['s2]; ('m +@ 1)}} >> 0 thenT autoT"
4987  O       o2398   ext_rule p2398  O       o2398   ext_rule p2398
4988  T       t2398   o603 b587 b659 b655  T       t2398   o603 b587 b659 b655
# Line 5563  Line 4991 
4991  S       s2399   t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s2399   t726 h h307 h308 h319 h564 h603 h754 h641 h656
4992  G       s2399   t2399  G       s2399   t2399
4993  B       b2400   s2399  B       b2400   s2399
 T       t2400   o747 b2400 b300  
 B       b2401   t2400  
 T       t2401   o2 b2396  
 B       b2402   t2401  
 T       t2402   o746 b2401 b4 b2402  
 B       b2403   t2402  
 T       t2403   o b2403 b4  
 B       b2404   t2403  
 T       t2404   o745 b2396 b2404  
 B       b2405   t2404  
4994  P       p2405   String "setSubstT << equal{inv{'g; 'f['s1]}; inv{'g; 'f['s2]}} >> 0 thenT autoT"  P       p2405   String "setSubstT << equal{inv{'g; 'f['s1]}; inv{'g; 'f['s2]}} >> 0 thenT autoT"
4995  O       o2405   ext_rule p2405  O       o2405   ext_rule p2405
4996  P       p2406   String eq  P       p2406   String eq
# Line 5581  Line 4999 
4999  S       s2406   t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s2406   t726 h h307 h308 h319 h564 h603 h754 h641 h656
5000  G       s2406   t2406  G       s2406   t2406
5001  B       b2406   s2406  B       b2406   s2406
 T       t2407   o747 b2406 b300  
 B       b2407   t2407  
5002  T       t2408   o309 b659 b681  T       t2408   o309 b659 b681
5003  S       s2408   t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s2408   t726 h h307 h308 h319 h564 h603 h754 h641 h656
5004  G       s2408   t2408  G       s2408   t2408
5005  B       b2408   s2408  B       b2408   s2408
 T       t2409   o747 b2408 b300  
 B       b2409   t2409  
 T       t2410   o2 b2403  
 B       b2410   t2410  
 T       t2411   o2406 b2409 b780 b2410  
 B       b2411   t2411  
 T       t2412   o2 b2411  
 B       b2412   t2412  
 T       t2413   o2406 b2407 b4 b2412  
 B       b2413   t2413  
 T       t2414   o b2413 b4  
 B       b2414   t2414  
 T       t2415   o745 b2403 b2414  
 B       b2415   t2415  
5006  P       p2415   String "setSubstT << equal{'f['s1]; 'f['s2]} >> 0 thenT autoT"  P       p2415   String "setSubstT << equal{'f['s1]; 'f['s2]} >> 0 thenT autoT"
5007  O       o2415   ext_rule p2415  O       o2415   ext_rule p2415
5008  T       t2416   o507 b320 b340  T       t2416   o507 b320 b340
5009  S       s2416   t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s2416   t726 h h307 h308 h319 h564 h603 h754 h641 h656
5010  G       s2416   t2416  G       s2416   t2416
5011  B       b2416   s2416  B       b2416   s2416
 T       t2417   o747 b2416 b300  
 B       b2417   t2417  
5012  T       t2418   o309 b320 b340  T       t2418   o309 b320 b340
5013  S       s2418   t726 h h307 h308 h319 h564 h603 h754 h641 h656  S       s2418   t726 h h307 h308 h319 h564 h603 h754 h641 h656
5014  G       s2418   t2418  G       s2418   t2418
5015  B       b2418   s2418  B       b2418   s2418
 T       t2419   o747 b2418 b300  
 B       b2419   t2419  
 T       t2420   o2 b2413  
 B       b2420   t2420  
 T       t2421   o2406 b2419 b780 b2420  
 B       b2421   t2421  
 T       t2422   o2 b2421  
 B       b2422   t2422  
 T       t2423   o2406 b2417 b4 b2422  
 B       b2423   t2423  
 T       t2424   o b2423 b4  
 B       b2424   t2424  
 T       t2425   o745 b2413 b2424  
 B       b2425   t2425  
5016  P       p2425   String "assumT 4 thenT rwh unfold_fun_set 10 thenT instHypT [<< 's1 >>; << 's2 >>] 10 thenT autoT thenT dT 11 ttca thenT rwh unfold_equal 11 ttca"  P       p2425   String "assumT 4 thenT rwh unfold_fun_set 10 thenT instHypT [<< 's1 >>; << 's2 >>] 10 thenT autoT thenT dT 11 ttca thenT rwh unfold_equal 11 ttca"
5017  O       o2425   ext_rule p2425  O       o2425   ext_rule p2425
 T       t2426   o745 b2423 b4  
 B       b2426   t2426  
 T       t2427   o2425 b744 b2426 b4 b4  
 B       b2427   t2427  
 T       t2428   o b2427 b4  
 B       b2428   t2428  
 T       t2429   o2415 b744 b2425 b2428 b4  
 B       b2429   t2429  
 T       t2430   o b2429 b4  
 B       b2430   t2430  
 T       t2431   o2405 b744 b2415 b2430 b4  
 B       b2431   t2431  
 T       t2432   o b2431 b4  
 B       b2432   t2432  
 T       t2433   o2398 b744 b2405 b2432 b4  
 B       b2433   t2433  
 T       t2434   o b2433 b4  
 B       b2434   t2434  
 T       t2435   o805 b744 b2398 b2434 b4  
 B       b2435   t2435  
5018  B       b2436   t677  B       b2436   t677
5019  B       b2437   t716  B       b2437   t716
5020  T       t2437   o507 b2436 b2437  T       t2437   o507 b2436 b2437
5021  S       s2437   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293  S       s2437   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
5022  G       s2437   t2437  G       s2437   t2437
5023  B       b2438   s2437  B       b2438   s2437
 T       t2438   o747 b2438 b300  
 B       b2439   t2438  
 T       t2439   o2 b2387  
 B       b2440   t2439  
 T       t2440   o746 b2439 b4 b2440  
 B       b2441   t2440  
 T       t2441   o b2441 b4  
 B       b2442   t2441  
 T       t2442   o745 b2387 b2442  
 B       b2443   t2442  
5024  P       p2443   String "setSubstT << equal{power{'g; 'f['s1]; ('m -@ 1)}; power{'g; 'f['s2]; ('m -@ 1)}} >> 0 thenT autoT"  P       p2443   String "setSubstT << equal{power{'g; 'f['s1]; ('m -@ 1)}; power{'g; 'f['s2]; ('m -@ 1)}} >> 0 thenT autoT"
5025  O       o2443   ext_rule p2443  O       o2443   ext_rule p2443
5026  T       t2443   o603 b587 b320 b715  T       t2443   o603 b587 b320 b715
# Line 5673  Line 5029 
5029  S       s2444   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293  S       s2444   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
5030  G       s2444   t2444  G       s2444   t2444
5031  B       b2445   s2444  B       b2445   s2444
 T       t2445   o747 b2445 b300  
 B       b2446   t2445  
 T       t2446   o2 b2441  
 B       b2447   t2446  
 T       t2447   o746 b2446 b4 b2447  
 B       b2448   t2447  
 T       t2448   o b2448 b4  
 B       b2449   t2448  
 T       t2449   o745 b2441 b2449  
 B       b2450   t2449  
5032  P       p2450   String "setSubstT << equal{'f['s1]; 'f['s2]} >> 0 ttca"  P       p2450   String "setSubstT << equal{'f['s1]; 'f['s2]} >> 0 ttca"
5033  O       o2450   ext_rule p2450  O       o2450   ext_rule p2450
5034  S       s2450   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293  S       s2450   t726 h h307 h308 h319 h564 h603 h754 h2292 h2293
5035  G       s2450   t2418  G       s2450   t2418
5036  B       b2451   s2450  B       b2451   s2450
 T       t2451   o747 b2451 b300  
 B       b2452   t2451  
 T       t2452   o2 b2448  
 B       b2453   t2452  
 T       t2453   o2406 b2452 b4 b2453  
 B       b2454   t2453  
 T       t2454   o b2454 b4  
 B       b2455   t2454  
 T       t2455   o745 b2448 b2455  
 B       b2456   t2455  
5037  P       p2456   String "assumT 4 thenT rwh unfold_fun_set 10 thenT instHypT [<< 's1 >>; << 's2 >>] 10 ttca thenT dT 11 ttca"  P       p2456   String "assumT 4 thenT rwh unfold_fun_set 10 thenT instHypT [<< 's1 >>; << 's2 >>] 10 ttca thenT dT 11 ttca"
5038  O       o2456   ext_rule p2456  O       o2456   ext_rule p2456
 T       t2456   o745 b2454 b4  
 B       b2457   t2456  
 T       t2457   o2456 b744 b2457 b4 b4  
 B       b2458   t2457  
 T       t2458   o b2458 b4  
 B       b2459   t2458  
 T       t2459   o2450 b744 b2456 b2459 b4  
 B       b2460   t2459  
 T       t2460   o b2460 b4  
 B       b2461   t2460  
 T       t2461   o2443 b744 b2450 b2461 b4  
 B       b2462   t2461  
 T       t2462   o b2462 b4  
 B       b2463   t2462  
 T       t2463   o807 b744 b2443 b2463 b4  
 B       b2464   t2463  
 T       t2464   o b2464 b4  
 B       b2465   t2464  
 T       t2465   o b2435 b2465  
 B       b2466   t2465  
 T       t2466   o641 b744 b2390 b2466 b4  
 B       b2467   t2466  
 T       t2467   o b2467 b4  
 B       b2468   t2467  
 T       t2468   o b632 b2468  
 B       b2469   t2468  
 T       t2469   o597 b744 b628 b2469 b4  
 B       b2470   t2469  
 T       t2470   o b2470 b4  
 B       b2471   t2470  
 T       t2471   o b593 b2471  
 B       b2472   t2471  
 T       t2472   o551 b744 b585 b2472 b4  
 B       b2473   t2472  
 T       t2473   o b2473 b4  
 B       b2474   t2473  
 T       t2474   o b549 b2474  
 B       b2475   t2474  
 T       t2475   o b541 b2475  
 B       b2476   t2475  
 T       t2476   o290 b744 b532 b2476 b4  
 B       b2477   t2476  
 T       t2477   o742 b2477  
 B       b2478   t2477  
5039  P       p2487   String power_equiv_fun  P       p2487   String power_equiv_fun
5040  O       o2487   rule p2487  O       o2487   rule p2487
5041  NCzf_itt_equiv!equiv_fun_set    equiv_fun_set   equiv_fun_set Czf_itt_equiv  NCzf_itt_equiv!equiv_fun_set    equiv_fun_set   equiv_fun_set Czf_itt_equiv
# Line 5752  Line 5044 
5044  S       s2488   t726 h  S       s2488   t726 h
5045  G       s2488   t2488  G       s2488   t2488
5046  B       b2488   s2488  B       b2488   s2488
 T       t2489   o719 b2488  
 B       b2489   t2489  
5047  T       t2490   o2488 b733 b886 b267  T       t2490   o2488 b733 b886 b267
5048  S       s2490   t726 h  S       s2490   t726 h
5049  G       s2490   t2490  G       s2490   t2490
5050  B       b2490   s2490  B       b2490   s2490
 T       t2491   o719 b2490  
 B       b2491   t2491  
 T       t2492   o718 b2489 b2491  
 B       b2492   t2492  
 T       t2493   o718 b890 b2492  
 B       b2493   t2493  
 P       p2497   String "assumT 6 thenT rwh unfold_equiv_fun_set 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca thenT rwh unfold_equiv_fun_set 2 thenT instHypT [<< 'a >>; << 'b >>] 2 ttca thenT dT 7 ttca thenT dT 7 ttca"  
 O       o2497   ext_rule p2497  
5051  T       t2498   o b2488 b4  T       t2498   o b2488 b4
5052  B       b2498   t2498  B       b2498   t2498
5053  T       t2499   o b889 b2498  T       t2499   o b889 b2498
# Line 5981  Line 5263 
5263  B       b2590   t2589  B       b2590   t2589
5264  T       t2590   o746 b2522 b4 b2590  T       t2590   o746 b2522 b4 b2590
5265  B       b2591   t2590  B       b2591   t2590
 T       t2591   o b2591 b4  
 B       b2592   t2591  
 T       t2592   o745 b2505 b2592  
 B       b2593   t2592  
5266  P       p2593   String "genAssumT [4] thenT dT 0 ttca thenT dT 8 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"  P       p2593   String "genAssumT [4] thenT dT 0 ttca thenT dT 8 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
5267  O       o2593   ext_rule p2593  O       o2593   ext_rule p2593
5268  H       h2593   v_1 t757  H       h2593   v_1 t757
# Line 6191  Line 5469 
5469  B       b2679   t2678  B       b2679   t2678
5470  P       p2679   String "equivSubstT << equiv{car{'g}; 'R; 'f['a]; 'f['b]} >> 0 thenT autoT thenT rwh unfold_equiv 7 ttca"  P       p2679   String "equivSubstT << equiv{car{'g}; 'R; 'f['a]; 'f['b]} >> 0 thenT autoT thenT rwh unfold_equiv 7 ttca"
5471  O       o2679   ext_rule p2679  O       o2679   ext_rule p2679
 T       t2679   o745 b2667 b4  
 B       b2680   t2679  
 T       t2680   o2679 b744 b2680 b4 b4  
 B       b2681   t2680  
5472  P       p2681   String "autoT thenT rwh unfold_equiv 7 ttca"  P       p2681   String "autoT thenT rwh unfold_equiv 7 ttca"
5473  O       o2681   ext_rule p2681  O       o2681   ext_rule p2681
5474  T       t2681   o745 b2670 b4  T       t2681   o745 b2670 b4
5475  B       b2682   t2681  B       b2682   t2681
5476  T       t2682   o2681 b744 b2682 b4 b4  T       t2682   o2681 b744 b2682 b4 b4
5477  B       b2683   t2682  B       b2683   t2682
 T       t2683   o745 b2675 b4  
 B       b2684   t2683  
 T       t2684   o2681 b744 b2684 b4 b4  
 B       b2685   t2684  
 T       t2685   o b2685 b4  
 B       b2686   t2685  
 T       t2686   o b2683 b2686  
 B       b2687   t2686  
 T       t2687   o b2681 b2687  
 B       b2688   t2687  
 T       t2688   o2663 b744 b2679 b2688 b4  
 B       b2689   t2688  
 T       t2689   o745 b2660 b4  
 B       b2690   t2689  
 T       t2690   o2681 b744 b2690 b4 b4  
 B       b2691   t2690  
 T       t2691   o b2691 b4  
 B       b2692   t2691  
 T       t2692   o b2689 b2692  
 B       b2693   t2692  
 T       t2693   o2650 b744 b2663 b2693 b4  
 B       b2694   t2693  
 T       t2694   o b2694 b4  
 B       b2695   t2694  
 T       t2695   o805 b744 b2650 b2695 b4  
 B       b2696   t2695  
5478  B       b2697   t2599  B       b2697   t2599
5479  B       b2698   t2604  B       b2698   t2604
5480  T       t2698   o888 b733 b886 b2697 b2698  T       t2698   o888 b733 b886 b2697 b2698
# Line 6275  Line 5523 
5523  B       b2716   t2715  B       b2716   t2715
5524  T       t2716   o745 b2702 b2716  T       t2716   o745 b2702 b2716
5525  B       b2717   t2716  B       b2717   t2716
 T       t2717   o745 b2709 b4  
 B       b2718   t2717  
 T       t2718   o2679 b744 b2718 b4 b4  
 B       b2719   t2718  
 T       t2719   o745 b2714 b4  
 B       b2720   t2719  
 T       t2720   o2681 b744 b2720 b4 b4  
 B       b2721   t2720  
 T       t2721   o b2721 b4  
 B       b2722   t2721  
 T       t2722   o b2719 b2722  
 B       b2723   t2722  
 T       t2723   o2704 b744 b2717 b2723 b4  
 B       b2724   t2723  
 T       t2724   o b2724 b4  
 B       b2725   t2724  
 T       t2725   o807 b744 b2704 b2725 b4  
 B       b2726   t2725  
 T       t2726   o b2726 b4  
 B       b2727   t2726  
 T       t2727   o b2696 b2727  
 B       b2728   t2727  
 T       t2728   o2593 b744 b2642 b2728 b4  
 B       b2729   t2728  
 T       t2729   o b2729 b4  
 B       b2730   t2729  
 T       t2730   o2497 b744 b2593 b2730 b4  
 B       b2731   t2730  
 T       t2731   o742 b2731  
 B       b2732   t2731  
5526  P       p2739   String power_equiv_fun1  P       p2739   String power_equiv_fun1
5527  O       o2739   rule p2739  O       o2739   rule p2739
5528  B       b2740   t590 z  B       b2740   t590 z
 T       t2740   o2488 b733 b886 b2740  
 S       s2740   t726 h  
 G       s2740   t2740  
 B       b2741   s2740  
 T       t2741   o719 b2741  
 B       b2742   t2741  
 T       t2742   o718 b890 b2742  
 B       b2743   t2742  
5529  P       p2747   String autoT  P       p2747   String autoT
5530  O       o2747   ext_rule p2747  O       o2747   ext_rule p2747
 T       t2747   o b889 b4  
 B       b2748   t2747  
 T       t2748   o b729 b2748  
 B       b2749   t2748  
 T       t2749   o b727 b2749  
 B       b2750   t2749  
 T       t2750   o b723 b2750  
 B       b2751   t2750  
 T       t2751   o b887 b2751  
 B       b2752   t2751  
 T       t2752   o747 b2741 b2752  
 B       b2753   t2752  
 T       t2753   o746 b2753 b4 b753  
 B       b2754   t2753  
 T       t2754   o745 b2754 b4  
 B       b2755   t2754  
 T       t2755   o2747 b744 b2755 b4 b4  
 B       b2756   t2755  
 T       t2756   o742 b2756  
 B       b2757   t2756  
 P       p2784   String "genAssumT [5; 6] thenT dT 0 ttca thenT dT 0 ttca"  
 O       o2784   ext_rule p2784  
 S       s2784   t726 h h754 h770  
 G       s2784   t2198  
 B       b2784   s2784  
 T       t2784   o747 b2784 b2212  
 B       b2785   t2784  
 B       b2786   t2198 n  
 T       t2786   o775 b621 b2786  
 S       s2786   t726 h h754  
 G       s2786   t2786  
 B       b2787   s2786  
 T       t2787   o747 b2787 b2212  
 B       b2788   t2787  
 B       b2789   t2786 m  
 T       t2789   o775 b621 b2789  
 S       s2789   t726 h  
 G       s2789   t2789  
 B       b2790   s2789  
 T       t2790   o747 b2790 b2212  
 B       b2791   t2790  
 T       t2791   o2 b2214  
 B       b2792   t2791  
 T       t2792   o774 b2791 b4 b2792  
 B       b2793   t2792  
 T       t2793   o2 b2793  
 B       b2794   t2793  
 T       t2794   o746 b2788 b4 b2794  
 B       b2795   t2794  
 T       t2795   o2 b2795  
 B       b2796   t2795  
 T       t2796   o746 b2785 b4 b2796  
 B       b2797   t2796  
 T       t2797   o b2797 b4  
 B       b2798   t2797  
 T       t2798   o745 b2214 b2798  
 B       b2799   t2798  
5531  P       p2799   String "dT 3 thenT rwh reduceC 0 ttca"  P       p2799   String "dT 3 thenT rwh reduceC 0 ttca"
5532  O       o2799   ext_rule p2799  O       o2799   ext_rule p2799
5533  H       h2799   m_1 t621  H       h2799   m_1 t621
# Line 6394  Line 5547 
5547  B       b2805   t2805  B       b2805   t2805
5548  T       t2806   o586 b587 b622 b2805  T       t2806   o586 b587 b622 b2805
5549  B       b2806   t2806  B       b2806   t2806
 T       t2807   o888 b733 b886 b2804 b2806  
 H       h2807   z t2807  
5550  T       t2808   o586 b587 b622 b2800  T       t2808   o586 b587 b622 b2800
5551  B       b2808   t2808  B       b2808   t2808
5552  T       t2809   o603 b587 b923 b2808  T       t2809   o603 b587 b923 b2808
# Line 6404  Line 5555 
5555  B       b2810   t2810  B       b2810   t2810
5556  T       t2811   o586 b587 b622 b2810  T       t2811   o586 b587 b622 b2810
5557  B       b2811   t2811  B       b2811   t2811
 T       t2812   o888 b733 b886 b2809 b2811  
 S       s2812   t726 h h754 h2799 h2801 h2807  
 G       s2812   t2812  
 B       b2812   s2812  
 T       t2813   o747 b2812 b2212  
 B       b2813   t2813  
 S       s2813   t726 h h754 h770 h2799 h2801 h2807  
 G       s2813   t2812  
 B       b2814   s2813  
 T       t2814   o747 b2814 b2212  
 B       b2815   t2814  
 T       t2815   o2 b2797  
 B       b2816   t2815  
 T       t2816   o746 b2815 b4 b2816  
 B       b2817   t2816  
 T       t2817   o2 b2817  
 B       b2818   t2817  
 T       t2818   o746 b2813 b4 b2818  
 B       b2819   t2818  
5558  T       t2819   o603 b587 b923 b944  T       t2819   o603 b587 b923 b944
5559  B       b2820   t2819  B       b2820   t2819
 T       t2820   o888 b733 b886 b2820 b923  
 S       s2820   t726 h h754  
 G       s2820   t2820  
 B       b2821   s2820  
 T       t2821   o747 b2821 b2212  
 B       b2822   t2821  
5560  T       t2822   o605 b755 b756  T       t2822   o605 b755 b756
5561  B       b2823   t2822  B       b2823   t2822
5562  T       t2823   o586 b587 b622 b2823  T       t2823   o586 b587 b622 b2823
5563  B       b2824   t2823  B       b2824   t2823
 T       t2824   o888 b733 b886 b2820 b2824  
 S       s2824   t726 h h754  
 G       s2824   t2824  
 B       b2825   s2824  
 T       t2825   o747 b2825 b2212  
 B       b2826   t2825  
 S       s2826   t726 h h754 h770  
 G       s2826   t2824  
 B       b2827   s2826  
 T       t2827   o747 b2827 b2212  
 B       b2828   t2827  
 T       t2828   o746 b2828 b4 b2816  
 B       b2829   t2828  
 T       t2829   o2 b2829  
 B       b2830   t2829  
 T       t2830   o746 b2826 b4 b2830  
 B       b2831   t2830  
 T       t2831   o2 b2831  
 B       b2832   t2831  
 T       t2832   o746 b2822 b4 b2832  
 B       b2833   t2832  
5564  T       t2833   o754 b756 b2800  T       t2833   o754 b756 b2800
5565  H       h2833   v t2833  H       h2833   v t2833
5566  T       t2834   o610 b2800 b606  T       t2834   o610 b2800 b606
# Line 6468  Line 5573 
5573  B       b2837   t2837  B       b2837   t2837
5574  T       t2838   o586 b587 b622 b2837  T       t2838   o586 b587 b622 b2837
5575  B       b2838   t2838  B       b2838   t2838
 T       t2839   o888 b733 b886 b2836 b2838  
 H       h2839   z t2839  
 S       s2839   t726 h h754 h2799 h2833 h2839  
 G       s2839   t2812  
 B       b2839   s2839  
 T       t2840   o747 b2839 b2212  
 B       b2840   t2840  
 S       s2840   t726 h h754 h770 h2799 h2833 h2839  
 G       s2840   t2812  
 B       b2841   s2840  
 T       t2841   o747 b2841 b2212  
 B       b2842   t2841  
 T       t2842   o746 b2842 b4 b2816  
 B       b2843   t2842  
 T       t2843   o2 b2843  
 B       b2844   t2843  
 T       t2844   o746 b2840 b4 b2844  
 B       b2845   t2844  
 T       t2845   o b2845 b4  
 B       b2846   t2845  
 T       t2846   o b2833 b2846  
 B       b2847   t2846  
 T       t2847   o b2819 b2847  
 B       b2848   t2847  
 T       t2848   o745 b2797 b2848  
 B       b2849   t2848  
 P       p2849   String "equivSubstT << equiv{car{'g}; 'R; power{'g; 'x; ('m_1 +@ 1)}; op{'g; power{'g; 'x; 'm_1}; 'x}} >> 5 ttca"  
 O       o2849   ext_rule p2849  
5576  T       t2849   o603 b587 b2808 b622  T       t2849   o603 b587 b2808 b622
5577  B       b2850   t2849  B       b2850   t2849
 T       t2850   o888 b733 b886 b2803 b2850  
 S       s2850   t726 h h754 h2799 h2801 h2807  
 G       s2850   t2850  
 B       b2851   s2850  
 T       t2851   o747 b2851 b2212  
 B       b2852   t2851  
 T       t2852   o2 b2819  
 B       b2853   t2852  
 T       t2853   o746 b2852 b4 b2853  
 B       b2854   t2853  
5578  T       t2854   o603 b587 b923 b2850  T       t2854   o603 b587 b923 b2850
5579  B       b2855   t2854  B       b2855   t2854
 T       t2855   o888 b733 b886 b2855 b2806  
 H       h2855   z_1 t2855  
 S       s2855   t726 h h754 h2799 h2801 h2807 h2855  
 G       s2855   t2812  
 B       b2856   s2855  
 T       t2856   o747 b2856 b2212  
 B       b2857   t2856  
 T       t2857   o746 b2857 b4 b2853  
 B       b2858   t2857  
 T       t2858   o b2858 b4  
 B       b2859   t2858  
 T       t2859   o b2854 b2859  
 B       b2860   t2859  
 T       t2860   o745 b2819 b2860  
 B       b2861   t2860  
 P       p2861   String "equivSym1T ttca"  
 O       o2861   ext_rule p2861  
 T       t2861   o745 b2854 b4  
 B       b2862   t2861  
 T       t2862   o2861 b744 b2862 b4 b4  
 B       b2863   t2862  
 P       p2863   String "equivSubstT << equiv{car{'g}; 'R; power{'g; 'x; ('m +@ 'm_1 +@ 1)}; op{'g; power{'g; 'x; ('m +@ 'm_1)}; 'x}} >> 6 ttca"  
 O       o2863   ext_rule p2863  
5580  T       t2863   o603 b587 b2811 b622  T       t2863   o603 b587 b2811 b622
5581  B       b2864   t2863  B       b2864   t2863
 T       t2864   o888 b733 b886 b2806 b2864  
 S       s2864   t726 h h754 h2799 h2801 h2807 h2855  
 G       s2864   t2864  
 B       b2865   s2864  
 T       t2865   o747 b2865 b2212  
 B       b2866   t2865  
 T       t2866   o2 b2858  
 B       b2867   t2866  
 T       t2867   o746 b2866 b4 b2867  
 B       b2868   t2867  
 T       t2868   o888 b733 b886 b2855 b2864  
 H       h2868   z_2 t2868  
 S       s2868   t726 h h754 h2799 h2801 h2807 h2855 h2868  
 G       s2868   t2812  
 B       b2869   s2868  
 T       t2869   o747 b2869 b2212  
 B       b2870   t2869  
 T       t2870   o746 b2870 b4 b2867  
 B       b2871   t2870  
 T       t2871   o b2871 b4  
 B       b2872   t2871  
 T       t2872   o b2868 b2872  
 B       b2873   t2872  
 T       t2873   o745 b2858 b2873  
 B       b2874   t2873  
 P       p2874   String "rwh add_AssocC 0 ttca thenT equivSym1T ttca"  
 O       o2874   ext_rule p2874  
 T       t2874   o745 b2868 b4  
 B       b2875   t2874  
 T       t2875   o2874 b744 b2875 b4 b4  
 B       b2876   t2875  
 P       p2876   String "equivSubstT << equiv{car{'g}; 'R; op{'g; power{'g; 'x; 'm}; op{'g; power{'g; 'x; 'm_1}; 'x}}; op{'g; op{'g; power{'g; 'x; 'm}; power{'g; 'x; 'm_1}}; 'x}} >> 7 ttca"  
 O       o2876   ext_rule p2876  
5582  T       t2876   o603 b587 b2809 b622  T       t2876   o603 b587 b2809 b622
5583  B       b2877   t2876  B       b2877   t2876
 T       t2877   o888 b733 b886 b2877 b2864  
 H       h2877   z_3 t2877  
 S       s2877   t726 h h754 h2799 h2801 h2807 h2855 h2868 h2877  
 G       s2877   t2812  
 B       b2878   s2877  
 T       t2878   o747 b2878 b2212  
 B       b2879   t2878  
 T       t2879   o2 b2871  
 B       b2880   t2879  
 T       t2880   o746 b2879 b4 b2880  
 B       b2881   t2880  
 T       t2881   o b2881 b4  
 B       b2882   t2881  
 T       t2882   o745 b2871 b2882  
 B       b2883   t2882  
5584  P       p2883   String "groupCancelRightT 8 ttca"  P       p2883   String "groupCancelRightT 8 ttca"
5585  O       o2883   ext_rule p2883  O       o2883   ext_rule p2883
 T       t2883   o745 b2881 b4  
 B       b2884   t2883  
 T       t2884   o2883 b744 b2884 b4 b4  
 B       b2885   t2884  
 T       t2885   o b2885 b4  
 B       b2886   t2885  
 T       t2886   o2876 b744 b2883 b2886 b4  
 B       b2887   t2886  
 T       t2887   o b2887 b4  
 B       b2888   t2887  
 T       t2888   o b2876 b2888  
 B       b2889   t2888  
 T       t2889   o2863 b744 b2874 b2889 b4  
 B       b2890   t2889  
 T       t2890   o b2890 b4  
 B       b2891   t2890  
 T       t2891   o b2863 b2891  
 B       b2892   t2891  
 T       t2892   o2849 b744 b2861 b2892 b4  
 B       b2893   t2892  
5586  P       p2893   String "rwh unfold_power 0 thenT rwh reduceC 0 thenT rwh fold_power 0 ttca"  P       p2893   String "rwh unfold_power 0 thenT rwh reduceC 0 thenT rwh fold_power 0 ttca"
5587  O       o2893   ext_rule p2893  O       o2893   ext_rule p2893
 T       t2893   o745 b2833 b4  
 B       b2894   t2893  
 T       t2894   o2893 b744 b2894 b4 b4  
 B       b2895   t2894  
 P       p2895   String "equivSubstT << equiv{car{'g}; 'R; power{'g; 'x; ('m_1 -@ 1)}; op{'g; power{'g; 'x; (('m_1 -@ 1) +@ 1)}; inv{'g; 'x}}} >> 5 ttca"  
 O       o2895   ext_rule p2895  
5588  T       t2895   o605 b2834 b606  T       t2895   o605 b2834 b606
5589  B       b2896   t2895  B       b2896   t2895
5590  T       t2896   o586 b587 b622 b2896  T       t2896   o586 b587 b622 b2896
# Line 6623  Line 5593 
5593  B       b2898   t2897  B       b2898   t2897
5594  T       t2898   o603 b587 b923 b2898  T       t2898   o603 b587 b923 b2898
5595  B       b2899   t2898  B       b2899   t2898
 T       t2899   o888 b733 b886 b2899 b2838  
 H       h2899   z_1 t2899  
 S       s2899   t726 h h754 h2799 h2833 h2839 h2899  
 G       s2899   t2812  
 B       b2900   s2899  
 T       t2900   o747 b2900 b2212  
 B       b2901   t2900  
 T       t2901   o2 b2845  
 B       b2902   t2901  
 T       t2902   o746 b2901 b4 b2902  
 B       b2903   t2902  
 T       t2903   o b2903 b4  
 B       b2904   t2903  
 T       t2904   o745 b2845 b2904  
 B       b2905   t2904  
 P       p2905   String "equivSubstT << equiv{car{'g}; 'R; power{'g; 'x; ('m +@ 'm_1 -@ 1)}; op{'g; power{'g; 'x; (('m +@ 'm_1 -@ 1) +@ 1)}; inv{'g; 'x}}} >> 6 ttca"  
 O       o2905   ext_rule p2905  
5596  T       t2905   o605 b2837 b606  T       t2905   o605 b2837 b606
5597  B       b2906   t2905  B       b2906   t2905
5598  T       t2906   o586 b587 b622 b2906  T       t2906   o586 b587 b622 b2906
5599  B       b2907   t2906  B       b2907   t2906
5600  T       t2907   o603 b587 b2907 b896  T       t2907   o603 b587 b2907 b896
5601  B       b2908   t2907  B       b2908   t2907
 T       t2908   o888 b733 b886 b2899 b2908  
 H       h2908   z_2 t2908  
 S       s2908   t726 h h754 h2799 h2833 h2839 h2899 h2908  
 G       s2908   t2812  
 B       b2909   s2908  
 T       t2909   o747 b2909 b2212  
 B       b2910   t2909  
 T       t2910   o2 b2903  
 B       b2911   t2910  
 T       t2911   o746 b2910 b4 b2911  
 B       b2912   t2911  
 T       t2912   o b2912 b4  
 B       b2913   t2912  
 T       t2913   o745 b2903 b2913  
 B       b2914   t2913  
 P       p2914   String "equivSubstT << equiv{car{'g}; 'R; op{'g; power{'g; 'x; 'm}; op{'g; power{'g; 'x; (('m_1 -@ 1) +@ 1)}; inv{'g; 'x}}}; op{'g; op{'g; power{'g; 'x; 'm}; power{'g; 'x; (('m_1 -@ 1) +@ 1)}}; inv{'g; 'x}}} >> 7 ttca"  
 O       o2914   ext_rule p2914  
5602  T       t2914   o603 b587 b923 b2897  T       t2914   o603 b587 b923 b2897
5603  B       b2915   t2914  B       b2915   t2914
5604  T       t2915   o603 b587 b2915 b896  T       t2915   o603 b587 b2915 b896
5605  B       b2916   t2915  B       b2916   t2915
 T       t2916   o888 b733 b886 b2916 b2908  
 H       h2916   z_3 t2916  
 S       s2916   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2916  
 G       s2916   t2812  
 B       b2917   s2916  
 T       t2917   o747 b2917 b2212  
 B       b2918   t2917  
 T       t2918   o2 b2912  
 B       b2919   t2918  
 T       t2919   o746 b2918 b4 b2919  
 B       b2920   t2919  
 T       t2920   o b2920 b4  
 B       b2921   t2920  
 T       t2921   o745 b2912 b2921  
 B       b2922   t2921  
5606  P       p2922   String "rwh unfold_sub 8 thenT rwh add_normalizeC 8 thenT rwh reduceC 8 ttca"  P       p2922   String "rwh unfold_sub 8 thenT rwh add_normalizeC 8 thenT rwh reduceC 8 ttca"
5607  O       o2922   ext_rule p2922  O       o2922   ext_rule p2922
5608  T       t2922   o603 b587 b2809 b896  T       t2922   o603 b587 b2809 b896
5609  B       b2923   t2922  B       b2923   t2922
5610  T       t2923   o603 b587 b2811 b896  T       t2923   o603 b587 b2811 b896
5611  B       b2924   t2923  B       b2924   t2923
 T       t2924   o888 b733 b886 b2923 b2924  
 H       h2924   z_3 t2924  
 S       s2924   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2924  
 G       s2924   t2812  
 B       b2925   s2924  
 T       t2925   o747 b2925 b2212  
 B       b2926   t2925  
5612  T       t2926   o605 b1483 b2800  T       t2926   o605 b1483 b2800
5613  B       b2927   t2926  B       b2927   t2926
5614  T       t2927   o586 b587 b622 b2927  T       t2927   o586 b587 b622 b2927
5615  B       b2928   t2927  B       b2928   t2927
5616  T       t2928   o603 b587 b2928 b896  T       t2928   o603 b587 b2928 b896
5617  B       b2929   t2928  B       b2929   t2928
 T       t2929   o888 b733 b886 b2923 b2929  
 H       h2929   z_3 t2929  
 S       s2929   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2929  
 G       s2929   t2812  
 B       b2930   s2929  
 T       t2930   o747 b2930 b2212  
 B       b2931   t2930  
5618  T       t2931   o605 b1489 b2800  T       t2931   o605 b1489 b2800
5619  B       b2932   t2931  B       b2932   t2931
5620  T       t2932   o586 b587 b622 b2932  T       t2932   o586 b587 b622 b2932
5621  B       b2933   t2932  B       b2933   t2932
5622  T       t2933   o603 b587 b2933 b896  T       t2933   o603 b587 b2933 b896
5623  B       b2934   t2933  B       b2934   t2933
 T       t2934   o888 b733 b886 b2923 b2934  
 H       h2934   z_3 t2934  
 S       s2934   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2934  
 G       s2934   t2812  
 B       b2935   s2934  
 T       t2935   o747 b2935 b2212  
 B       b2936   t2935  
5624  T       t2936   o605 b756 b2800  T       t2936   o605 b756 b2800
5625  B       b2937   t2936  B       b2937   t2936
5626  T       t2937   o586 b587 b622 b2937  T       t2937   o586 b587 b622 b2937
# Line 6729  Line 5629 
5629  B       b2939   t2938  B       b2939   t2938
5630  T       t2939   o603 b587 b2939 b896  T       t2939   o603 b587 b2939 b896
5631  B       b2940   t2939  B       b2940   t2939
 T       t2940   o888 b733 b886 b2940 b2934  
 H       h2940   z_3 t2940  
 S       s2940   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2940  
 G       s2940   t2812  
 B       b2941   s2940  
 T       t2941   o747 b2941 b2212  
 B       b2942   t2941  
5632  T       t2942   o605 b1495 b2800  T       t2942   o605 b1495 b2800
5633  B       b2943   t2942  B       b2943   t2942
5634  T       t2943   o586 b587 b622 b2943  T       t2943   o586 b587 b622 b2943
5635  B       b2944   t2943  B       b2944   t2943
5636  T       t2944   o603 b587 b2944 b896  T       t2944   o603 b587 b2944 b896
5637  B       b2945   t2944  B       b2945   t2944
 T       t2945   o888 b733 b886 b2940 b2945  
 H       h2945   z_3 t2945  
 S       s2945   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2945  
 G       s2945   t2812  
 B       b2946   s2945  
 T       t2946   o747 b2946 b2212  
 B       b2947   t2946  
5638  T       t2947   o605 b1048 b2800  T       t2947   o605 b1048 b2800
5639  B       b2948   t2947  B       b2948   t2947
5640  T       t2948   o586 b587 b622 b2948  T       t2948   o586 b587 b622 b2948
# Line 6757  Line 5643 
5643  B       b2950   t2949  B       b2950   t2949
5644  T       t2950   o603 b587 b2950 b896  T       t2950   o603 b587 b2950 b896
5645  B       b2951   t2950  B       b2951   t2950
 T       t2951   o888 b733 b886 b2951 b2945  
 H       h2951   z_3 t2951  
 S       s2951   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2951  
 G       s2951   t2812  
 B       b2952   s2951  
 T       t2952   o747 b2952 b2212  
 B       b2953   t2952  
5646  T       t2953   o605 b1057 b2810  T       t2953   o605 b1057 b2810
5647  B       b2954   t2953  B       b2954   t2953
5648  T       t2954   o586 b587 b622 b2954  T       t2954   o586 b587 b622 b2954
5649  B       b2955   t2954  B       b2955   t2954
5650  T       t2955   o603 b587 b2955 b896  T       t2955   o603 b587 b2955 b896
5651  B       b2956   t2955  B       b2956   t2955
 T       t2956   o888 b733 b886 b2951 b2956  
 H       h2956   z_3 t2956  
 S       s2956   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2956  
 G       s2956   t2812  
 B       b2957   s2956  
 T       t2957   o747 b2957 b2212  
 B       b2958   t2957  
5652  T       t2958   o605 b1057 b2800  T       t2958   o605 b1057 b2800
5653  B       b2959   t2958  B       b2959   t2958
5654  T       t2959   o586 b587 b622 b2959  T       t2959   o586 b587 b622 b2959
# Line 6785  Line 5657 
5657  B       b2961   t2960  B       b2961   t2960
5658  T       t2961   o603 b587 b2961 b896  T       t2961   o603 b587 b2961 b896
5659  B       b2962   t2961  B       b2962   t2961
 T       t2962   o888 b733 b886 b2962 b2956  
 H       h2962   z_3 t2962  
 S       s2962   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2962  
 G       s2962   t2812  
 B       b2963   s2962  
 T       t2963   o747 b2963 b2212  
 B       b2964   t2963  
5660  T       t2964   o605 b606 b2810  T       t2964   o605 b606 b2810
5661  B       b2965   t2964  B       b2965   t2964
5662  T       t2965   o605 b967 b2965  T       t2965   o605 b967 b2965
# Line 6800  Line 5665 
5665  B       b2967   t2966  B       b2967   t2966
5666  T       t2967   o603 b587 b2967 b896  T       t2967   o603 b587 b2967 b896
5667  B       b2968   t2967  B       b2968   t2967
 T       t2968   o888 b733 b886 b2962 b2968  
 H       h2968   z_3 t2968  
 S       s2968   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2968  
 G       s2968   t2812  
 B       b2969   s2968  
 T       t2969   o747 b2969 b2212  
 B       b2970   t2969  
5668  T       t2970   o605 b606 b2800  T       t2970   o605 b606 b2800
5669  B       b2971   t2970  B       b2971   t2970
5670  T       t2971   o605 b967 b2971  T       t2971   o605 b967 b2971
# Line 6817  Line 5675 
5675  B       b2974   t2973  B       b2974   t2973
5676  T       t2974   o603 b587 b2974 b896  T       t2974   o603 b587 b2974 b896
5677  B       b2975   t2974  B       b2975   t2974
 T       t2975   o888 b733 b886 b2975 b2968  
 H       h2975   z_3 t2975  
 S       s2975   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2975  
 G       s2975   t2812  
 B       b2976   s2975  
 T       t2976   o747 b2976 b2212  
 B       b2977   t2976  
5678  T       t2977   o605 b755 b2971  T       t2977   o605 b755 b2971
5679  B       b2978   t2977  B       b2978   t2977
5680  T       t2978   o605 b967 b2978  T       t2978   o605 b967 b2978
# Line 6832  Line 5683 
5683  B       b2980   t2979  B       b2980   t2979
5684  T       t2980   o603 b587 b2980 b896  T       t2980   o603 b587 b2980 b896
5685  B       b2981   t2980  B       b2981   t2980
 T       t2981   o888 b733 b886 b2975 b2981  
 H       h2981   z_3 t2981  
 S       s2981   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2981  
 G       s2981   t2812  
 B       b2982   s2981  
 T       t2982   o747 b2982 b2212  
 B       b2983   t2982  
5686  T       t2983   o605 b755 b2972  T       t2983   o605 b755 b2972
5687  B       b2984   t2983  B       b2984   t2983
5688  T       t2984   o586 b587 b622 b2984  T       t2984   o586 b587 b622 b2984
5689  B       b2985   t2984  B       b2985   t2984
5690  T       t2985   o603 b587 b2985 b896  T       t2985   o603 b587 b2985 b896
5691  B       b2986   t2985  B       b2986   t2985
 T       t2986   o888 b733 b886 b2975 b2986  
 H       h2986   z_3 t2986  
 S       s2986   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2986  
 G       s2986   t2812  
 B       b2987   s2986  
 T       t2987   o747 b2987 b2212  
 B       b2988   t2987  
5692  T       t2988   o605 b967 b2802  T       t2988   o605 b967 b2802
5693  B       b2989   t2988  B       b2989   t2988
5694  T       t2989   o605 b755 b2989  T       t2989   o605 b755 b2989
# Line 6860  Line 5697 
5697  B       b2991   t2990  B       b2991   t2990
5698  T       t2991   o603 b587 b2991 b896  T       t2991   o603 b587 b2991 b896
5699  B       b2992   t2991  B       b2992   t2991
 T       t2992   o888 b733 b886 b2975 b2992  
 H       h2992   z_3 t2992  
 S       s2992   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2992  
 G       s2992   t2812  
 B       b2993   s2992  
 T       t2993   o747 b2993 b2212  
 B       b2994   t2993  
5700  T       t2994   o605 b2800 b1057  T       t2994   o605 b2800 b1057
5701  B       b2995   t2994  B       b2995   t2994
5702  T       t2995   o605 b755 b2995  T       t2995   o605 b755 b2995
# Line 6875  Line 5705 
5705  B       b2997   t2996  B       b2997   t2996
5706  T       t2997   o603 b587 b2997 b896  T       t2997   o603 b587 b2997 b896
5707  B       b2998   t2997  B       b2998   t2997
 T       t2998   o888 b733 b886 b2975 b2998  
 H       h2998   z_3 t2998  
 S       s2998   t726 h h754 h2799 h2833 h2839 h2899 h2908 h2998  
 G       s2998   t2812  
 B       b2999   s2998  
 T       t2999   o747 b2999 b2212  
 B       b3000   t2999  
5708  T       t3000   o586 b587 b622 b2989  T       t3000   o586 b587 b622 b2989
5709  B       b3001   t3000  B       b3001   t3000
5710  T       t3001   o603 b587 b923 b3001  T       t3001   o603 b587 b923 b3001
5711  B       b3002   t3001  B       b3002   t3001
5712  T       t3002   o603 b587 b3002 b896  T       t3002   o603 b587 b3002 b896
5713  B       b3003   t3002  B       b3003   t3002
 T       t3003   o888 b733 b886 b3003 b2998  
 H       h3003   z_3 t3003  
 S       s3003   t726 h h754 h2799 h2833 h2839 h2899 h2908 h3003  
 G       s3003   t2812  
 B       b3004   s3003  
 T       t3004   o747 b3004 b2212  
 B       b3005   t3004  
5714  T       t3005   o586 b587 b622 b2995  T       t3005   o586 b587 b622 b2995
5715  B       b3006   t3005  B       b3006   t3005
5716  T       t3006   o603 b587 b923 b3006  T       t3006   o603 b587 b923 b3006
5717  B       b3007   t3006  B       b3007   t3006
5718  T       t3007   o603 b587 b3007 b896  T       t3007   o603 b587 b3007 b896
5719  B       b3008   t3007  B       b3008   t3007
 T       t3008   o888 b733 b886 b3008 b2998  
 H       h3008   z_3 t3008  
 S       s3008   t726 h h754 h2799 h2833 h2839 h2899 h2908 h3008  
 G       s3008   t2812  
 B       b3009   s3008  
 T       t3009   o747 b3009 b2212  
 B       b3010   t3009  
5720  T       t3010   o605 b2800 b967  T       t3010   o605 b2800 b967
5721  B       b3011   t3010  B       b3011   t3010
5722  T       t3011   o605 b3011 b606  T       t3011   o605 b3011 b606
# Line 6918  Line 5727 
5727  B       b3014   t3013  B       b3014   t3013
5728  T       t3014   o603 b587 b3014 b896  T       t3014   o603 b587 b3014 b896
5729  B       b3015   t3014  B       b3015   t3014
 T       t3015   o888 b733 b886 b3008 b3015  
 H       h3015   z_3 t3015  
 S       s3015   t726 h h754 h2799 h2833 h2839 h2899 h2908 h3015  
 G       s3015   t2812  
 B       b3016   s3015  
 T       t3016   o747 b3016 b2212  
 B       b3017   t3016  
5730  T       t3017   o605 b755 b3011  T       t3017   o605 b755 b3011
5731  B       b3018   t3017  B       b3018   t3017
5732  T       t3018   o605 b3018 b606  T       t3018   o605 b3018 b606
# Line 6933  Line 5735 
5735  B       b3020   t3019  B       b3020   t3019
5736  T       t3020   o603 b587 b3020 b896  T       t3020   o603 b587 b3020 b896
5737  B       b3021   t3020  B       b3021   t3020
 T       t3021   o888 b733 b886 b3008 b3021  
 H       h3021   z_3 t3021  
 S       s3021   t726 h h754 h2799 h2833 h2839 h2899 h2908 h3021  
 G       s3021   t2812  
 B       b3022   s3021  
 T       t3022   o747 b3022 b2212  
 B       b3023   t3022  
5738  T       t3023   o586 b587 b622 b3012  T       t3023   o586 b587 b622 b3012
5739  B       b3024   t3023  B       b3024   t3023
5740  T       t3024   o603 b587 b923 b3024  T       t3024   o603 b587 b923 b3024
5741  B       b3025   t3024  B       b3025   t3024
5742  T       t3025   o603 b587 b3025 b896  T       t3025   o603 b587 b3025 b896
5743  B       b3026   t3025  B       b3026   t3025
 T       t3026   o888 b733 b886 b3026 b3021  
 H       h3026   z_3 t3026  
 S       s3026   t726 h h754 h2799 h2833 h2839 h2899 h2908 h3026  
 G       s3026   t2812  
 B       b3027   s3026  
 T       t3027   o747 b3027 b2212  
 B       b3028   t3027  
 T       t3028   o2 b2920  
 B       b3029   t3028  
 T       t3029   o746 b3028 b4 b3029  
 B       b3030   t3029  
 T       t3030   o2 b3030  
 B       b3031   t3030  
 T       t3031   o746 b3023 b4 b3031  
 B       b3032   t3031  
 T       t3032   o2 b3032  
 B       b3033   t3032  
 T       t3033   o746 b3017 b4 b3033  
 B       b3034   t3033  
 T       t3034   o2 b3034  
 B       b3035   t3034  
 T       t3035   o746 b3010 b4 b3035  
 B       b3036   t3035  
 T       t3036   o2 b3036  
 B       b3037   t3036  
 T       t3037   o746 b3005 b4 b3037  
 B       b3038   t3037  
 T       t3038   o2 b3038  
 B       b3039   t3038  
 T       t3039   o746 b3000 b4 b3039  
 B       b3040   t3039  
 T       t3040   o2 b3040  
 B       b3041   t3040  
 T       t3041   o746 b2994 b4 b3041  
 B       b3042   t3041  
 T       t3042   o2 b3042  
 B       b3043   t3042  
 T       t3043   o746 b2988 b4 b3043  
 B       b3044   t3043  
 T       t3044   o2 b3044  
 B       b3045   t3044  
 T       t3045   o746 b2983 b4 b3045  
 B       b3046   t3045  
 T       t3046   o2 b3046  
 B       b3047   t3046  
 T       t3047   o746 b2977 b4 b3047  
 B       b3048   t3047  
 T       t3048   o2 b3048  
 B       b3049   t3048  
 T       t3049   o746 b2970 b4 b3049  
 B       b3050   t3049  
 T       t3050   o2 b3050  
 B       b3051   t3050  
 T       t3051   o746 b2964 b4 b3051  
 B       b3052   t3051  
 T       t3052   o2 b3052  
 B       b3053   t3052  
 T       t3053   o746 b2958 b4 b3053  
 B       b3054   t3053  
 T       t3054   o2 b3054  
 B       b3055   t3054  
 T       t3055   o746 b2953 b4 b3055  
 B       b3056   t3055  
 T       t3056   o2 b3056  
 B       b3057   t3056  
 T       t3057   o746 b2947 b4 b3057  
 B       b3058   t3057  
 T       t3058   o2 b3058  
 B       b3059   t3058  
 T       t3059   o746 b2942 b4 b3059  
 B       b3060   t3059  
 T       t3060   o2 b3060  
 B       b3061   t3060  
 T       t3061   o746 b2936 b4 b3061  
 B       b3062   t3061  
 T       t3062   o2 b3062  
 B       b3063   t3062  
 T       t3063   o746 b2931 b4 b3063  
 B       b3064   t3063  
 T       t3064   o2 b3064  
 B       b3065   t3064  
 T       t3065   o746 b2926 b4 b3065  
 B       b3066   t3065  
 T       t3066   o b3066 b4  
 B       b3067   t3066  
 T       t3067   o745 b2920 b3067  
 B       b3068   t3067  
 T       t3068   o745 b3066 b4  
 B       b3069   t3068  
 T       t3069   o2883 b744 b3069 b4 b4  
 B       b3070   t3069  
 T       t3070   o b3070 b4  
 B       b3071   t3070  
 T       t3071   o2922 b744 b3068 b3071 b4  
 B       b3072   t3071  
 T       t3072   o b3072 b4  
 B       b3073   t3072  
 T       t3073   o2914 b744 b2922 b3073 b4  
 B       b3074   t3073  
 T       t3074   o b3074 b4  
 B       b3075   t3074  
 T       t3075   o2905 b744 b2914 b3075 b4  
 B       b3076   t3075  
 T       t3076   o b3076 b4  
 B       b3077   t3076  
 T       t3077   o2895 b744 b2905 b3077 b4  
 B       b3078   t3077  
 T       t3078   o b3078 b4  
 B       b3079   t3078  
 T       t3079   o b2895 b3079  
 B       b3080   t3079  
 T       t3080   o b2893 b3080  
 B       b3081   t3080  
 T       t3081   o2799 b744 b2849 b3081 b4  
 B       b3082   t3081  
 T       t3082   o b3082 b4  
 B       b3083   t3082  
 T       t3083   o2784 b744 b2799 b3083 b4  
 B       b3084   t3083  
 T       t3084   o742 b3084  
 B       b3085   t3084  
5744  P       p2314   Var s  P       p2314   Var s
5745  O       o2314   var p2314  O       o2314   var p2314
5746  T       t2314   o2314  T       t2314   o2314
5747  B       b2314   t2314  B       b2314   t2314
5748  T       t362    o18 b587 b2314 b596  T       t635    o18 b2314 b587 b596
5749  B       b595    t362  B       b636    t635
5750  T       t595    o16 b595  T       t636    o16 b636
5751  B       b597    t595  B       b653    t636
5752  T       t597    o6 b597  T       t653    o6 b653
5753  B       b598    t597  B       b669    t653
5754  P       p599    Number 629  P       p599    Number 629
5755  P       p600    Number 790  P       p600    Number 790
5756  O       o600    location p599 p600  O       o600    location p599 p600
5757  T       t617    o600 b616  T       t617    o600 b616
5758  B       b617    t617  B       b617    t617
5759  P       p617    Number 792  P       p617    Number 792
 P       p618    Number 1030  
 O       o618    location p617 p618  
5760  P       p620    String unfold_cyc_subg  P       p620    String unfold_cyc_subg
5761  O       o623    rewrite p620  O       o623    rewrite p620
5762  NItt_logic!and  and     and Itt_logic  NItt_logic!and  and     and Itt_logic
# Line 7114  Line 5786 
5786  B       b2191   t2190 a  B       b2191   t2190 a
5787  T       t2191   o775 b365 b2191  T       t2191   o775 b365 b2191
5788  B       b2192   t2191  B       b2192   t2191
5789  T       t2192   o644 b1682 b2192  NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
5790  B       b2215   t2192  O       o671    eqG
5791  T       t2215   o644 b1680 b2215  T       t706    o671 b2314
5792  B       b2216   t2215  B       b706    t706
5793  T       t2216   o644 b656 b2216  T       t710    o888 b1681 b706 b596 b2507
5794  B       b2218   t2216  B       b710    t710
5795  T       t625    o623 b595 b2218 b615 b4  T       t711    o671 b587
5796  B       b625    t625  B       b711    t711
5797  T       t626    o618 b625  T       t712    o888 b733 b711 b596 b2507
5798  B       b626    t626  B       b712    t712
5799  P       p626    Number 1032  T       t730    o348 b710 b712
5800  P       p627    Number 1095  B       b730    t730 b
5801  O       o627    location p626 p627  T       t732    o775 b365 b730
5802  O       o628    str_let p626 p627  B       b732    t732 a
5803  P       p628    Number 1036  T       t739    o775 b365 b732
5804  P       p629    Number 1046  B       b739    t739
5805  O       o629    patt_var p628 p629  T       t740    o644 b2192 b739
5806  O       o630    patt_done p626 p627  B       b740    t740
5807  T       t630    o630  T       t741    o644 b1682 b740
5808  B       b630    t630 fold_power  B       b741    t741
5809  T       t631    o629 b630  P       p828    Number 1146
5810  B       b631    t631  O       o14     location p617 p828
 P       p631    Number 1049  
 O       o631    apply p631 p627  
 P       p632    Number 1082  
 O       o632    apply p631 p632  
 P       p633    Number 1058  
 O       o633    lid p631 p633  
 T       t633    o633 b634  
 B       b635    t633  
 P       p635    Number 1059  
 O       o635    apply p635 p632  
 O       o636    proj p635 p632  
 O       o637    uid p635 p632  
 T       t637    o637 b638  
 B       b637    t637  
 O       o639    lid p635 p632  
 T       t639    o639 b640  
 B       b639    t639  
 T       t641    o636 b637 b639  
 B       b641    t641  
 P       p8      String "MP-Caml3.02 term:\\132\\149\\166\\190\\000\\000\\000\\\\\\000\\000\\000!\\000\\000\\000`\\000\\000\\000[\\160\\160\\160$\\000\\000\\000\\000\\160%power\\1607Czf_itt_cyclic_subgroup@@\\160\\160@\\160\\160\\160\\004\\n\\160#var@\\160\\148!g@@\\160\\160@\\160\\160\\160\\004\\020\\004\\n\\160\\148!z@@\\160\\160@\\160\\160\\004\\018\\160\\148!n@@@"  
 O       o20     string p635 p632 p8  
 T       t365    o20  
 B       b642    t365  
 T       t642    o635 b641 b642  
 B       b643    t642  
 T       t643    o632 b635 b643  
 B       b644    t643  
 P       p644    Number 1083  
 O       o645    lid p644 p627  
 T       t645    o645 b646  
 B       b645    t645  
 T       t644    o631 b644 b645  
 B       b647    t644  
 T       t647    o628 b631 b647  
 B       b648    t647  
 T       t648    o b648 b4  
 B       b649    t648  
 T       t649    o628 b649  
 B       b650    t649  
 T       t650    o424 b650  
 B       b651    t650  
 T       t651    o627 b651  
 B       b652    t651  
 P       p652    Number 1096  
 P       p653    Number 1168  
 O       o653    location p652 p653  
 O       o654    str_let p652 p653  
 P       p654    Number 1100  
 P       p655    Number 1113  
 O       o655    patt_var p654 p655  
 O       o656    patt_done p652 p653  
 T       t657    o656  
 B       b657    t657 fold_cyc_subg  
 T       t658    o655 b657  
 B       b658    t658  
 P       p2221   Number 1116  
 O       o658    apply p2221 p653  
 P       p658    Number 1152  
 O       o659    apply p2221 p658  
 P       p659    Number 1125  
 O       o660    lid p2221 p659  
 T       t660    o660 b634  
 B       b660    t660  
 P       p660    Number 1126  
 O       o661    apply p660 p658  
 O       o662    proj p660 p658  
 O       o663    uid p660 p658  
 T       t663    o663 b638  
 B       b663    t663  
 O       o664    lid p660 p658  
 T       t664    o664 b640  
 B       b664    t664  
 T       t665    o662 b663 b664  
 B       b665    t665  
 P       p656    String "MP-Caml3.02 term:\\132\\149\\166\\190\\000\\000\\000\\\\\\000\\000\\000 \\000\\000\\000^\\000\\000\\000Y\\160\\160\\160$\\000\\000\\000\\000\\160(cyc_subg\\1607Czf_itt_cyclic_subgroup@@\\160\\160@\\160\\160\\160\\004\\n\\160#var@\\160\\148!g@@\\160\\160@\\160\\160\\004\\n\\160\\148!s@@\\160\\160@\\160\\160\\004\\017\\160\\148!a@@@"  
 O       o657    string p660 p658 p656  
 T       t666    o657  
 B       b666    t666  
 T       t667    o661 b665 b666  
 B       b667    t667  
 T       t668    o659 b660 b667  
 B       b668    t668  
 P       p2315   Number 1153  
 O       o668    lid p2315 p653  
5811  O       o670    lid p620  O       o670    lid p620
5812  T       t670    o670  T       t670    o670
5813  B       b670    t670  B       b670    t670
5814  T       t671    o668 b670  T       t2256   o b682 b685
5815  B       b671    t671  B       b2256   t2256
5816  T       t672    o658 b668 b671  T       t2257   o681 b2256 b590 b701
5817  B       b672    t672  B       b2257   t2257
 T       t673    o654 b658 b672  
 B       b673    t673  
 T       t674    o b673 b4  
 B       b674    t674  
 T       t675    o654 b674  
 B       b675    t675  
 T       t676    o424 b675  
 B       b676    t676  
 T       t679    o653 b676  
 B       b679    t679  
 P       p679    Number 1170  
 P       p680    Number 1185  
 O       o680    location p679 p680  
 T       t703    o680 b678  
 B       b703    t703  
 P       p683    Number 1187  
 P       p684    Number 1333  
 O       o685    location p683 p684  
 T       t713    o685 b702  
 B       b713    t713  
 P       p713    Number 1335  
 P       p714    Number 1464  
 O       o714    location p713 p714  
5818  P       p712    String cyc_subg_df  P       p712    String cyc_subg_df
5819  O       o712    dform p712  O       o712    dform p712
5820  P       p2236   String cyclic_subgroup(  P       p2236   String cyclic_subgroup(
# Line 7258  Line 5823 
5823  B       b2242   t2242  B       b2242   t2242
5824  T       t2351   o689 b2314  T       t2351   o689 b2314
5825  B       b2351   t2351  B       b2351   t2351
5826  T       t2352   o b2351 b709  T       t2263   o b689 b709
5827  B       b2352   t2352  B       b2263   t2263
5828  T       t2353   o b690 b2352  T       t2264   o b690 b2263
5829  B       b2353   t2353  B       b2264   t2264
5830  T       t2354   o b689 b2353  T       t2272   o b2351 b2264
5831  B       b2354   t2354  B       b2272   t2272
5832  T       t2244   o b2242 b2354  T       t2275   o b2242 b2272
5833  B       b2244   t2244  B       b2275   t2275
5834  T       t2245   o687 b2244  T       t2276   o687 b2275
5835  B       b2245   t2245  B       b2276   t2276
5836  T       t2246   o712 b705 b595 b2245  T       t2277   o712 b705 b636 b2276
5837  B       b2246   t2246  B       b2277   t2277
 T       t714    o714 b2246  
 B       b714    t714  
 P       p715    Number 1509  
 P       p718    Number 1828  
 O       o723    location p715 p718  
5838  S       s723    t721 h  S       s723    t721 h
5839  G       s723    t729  G       s723    t729
5840  B       b726    s723  B       b726    s723
# Line 7285  Line 5845 
5845  B       b818    s817  B       b818    s817
5846  T       t818    o719 b818  T       t818    o719 b818
5847  B       b819    t818  B       b819    t818
5848  T       t819    o718 b819 b738  T       t2284   o718 b817 b737
5849  B       b878    t819  B       b2284   t2284
5850  T       t878    o718 b817 b878  T       t2285   o718 b819 b2284
5851  B       b879    t878  B       b2285   t2285
5852  T       t879    o718 b728 b879  T       t2293   o718 b724 b2285
5853  B       b880    t879  B       b2293   t2293
5854  T       t880    o718 b724 b880  T       t2296   o b726 b4
5855  B       b881    t880  B       b2296   t2296
5856  P       p881    Number 1534  T       t2297   o b818 b2296
5857  P       p2247   Number 1542  B       b2297   t2297
5858  O       o881    resource_defs p881 p2247 p294  T       t2298   o b723 b2297
5859  P       p882    Number 1540  B       b2298   t2298
5860  O       o882    uid p882 p2247  T       t2300   o747 b736 b2298
5861  T       t882    o882 b816  B       b2300   t2300
5862  B       b882    t882  T       t2301   o746 b2300 b4 b753
5863  T       t883    o b882 b4  B       b2301   t2301
5864  B       b883    t883  T       t2306   o747 b766 b2298
5865  T       t884    o881 b883  B       b2306   t2306
5866  B       b2221   t884  T       t2310   o747 b769 b2298
5867  T       t2221   o b2221 b4  B       b2310   t2310
5868  B       b2222   t2221  T       t2311   o747 b771 b2298
5869  T       t2222   o716 b718 b881 b813 b2222  B       b2311   t2311
5870  B       b2223   t2222  T       t2312   o747 b773 b2298
5871  T       t2223   o723 b2223  B       b2315   t2312
5872  B       b2228   t2223  T       t2315   o747 b776 b2298
5873  P       p2228   Number 1909  B       b2316   t2315
5874  P       p2229   Number 2235  T       t2316   o2 b2301
5875  O       o2229   location p2228 p2229  B       b2317   t2316
5876    T       t2317   o774 b2316 b780 b2317
5877    B       b2318   t2317
5878    T       t2318   o2 b2318
5879    B       b2319   t2318
5880    T       t2324   o746 b2315 b4 b2319
5881    B       b2329   t2324
5882    T       t2329   o2 b2329
5883    B       b2331   t2329
5884    T       t2331   o746 b2311 b4 b2331
5885    B       b2332   t2331
5886    T       t2332   o2 b2332
5887    B       b2338   t2332
5888    T       t2338   o746 b2310 b4 b2338
5889    B       b2339   t2338
5890    T       t2339   o2 b2339
5891    B       b2340   t2339
5892    T       t2340   o746 b2306 b4 b2340
5893    B       b2341   t2340
5894    T       t2341   o747 b792 b2298
5895    B       b2342   t2341
5896    T       t2342   o747 b794 b2298
5897    B       b2343   t2342
5898    T       t2343   o747 b796 b2298
5899    B       b2347   t2343
5900    T       t2347   o746 b2347 b4 b2331
5901    B       b2349   t2347
5902    T       t2349   o2 b2349
5903    B       b2350   t2349
5904    T       t2350   o746 b2343 b4 b2350
5905    B       b2355   t2350
5906    T       t2355   o2 b2355
5907    B       b2356   t2355
5908    T       t2356   o746 b2342 b4 b2356
5909    B       b2357   t2356
5910    T       t2357   o b2357 b4
5911    B       b2358   t2357
5912    T       t2362   o b2341 b2358
5913    B       b2362   t2362
5914    T       t2363   o745 b2301 b2362
5915    B       b2363   t2363
5916    T       t2364   o745 b2341 b4
5917    B       b2364   t2364
5918    T       t2365   o805 b744 b2364 b4 b4
5919    B       b2365   t2365
5920    T       t2366   o745 b2357 b4
5921    B       b2366   t2366
5922    T       t2367   o807 b744 b2366 b4 b4
5923    B       b2367   t2367
5924    T       t2369   o b2367 b4
5925    B       b2370   t2369
5926    T       t2370   o b2365 b2370
5927    B       b2371   t2370
5928    T       t2371   o743 b744 b2363 b2371 b4
5929    B       b2372   t2371
5930    T       t2372   o742 b2372
5931    B       b2373   t2372
5932  T       t2229   o718 b819 b826  T       t2229   o718 b819 b826
5933  B       b2229   t2229  B       b2229   t2229
5934  T       t2230   o718 b817 b2229  T       t2230   o718 b817 b2229
# Line 7321  Line 5937 
5937  B       b2232   t2231  B       b2232   t2231
5938  T       t2232   o718 b724 b2232  T       t2232   o718 b724 b2232
5939  B       b2233   t2232  B       b2233   t2232
5940  P       p2234   Number 1934  T       t2480   o b818 b747
5941  P       p2235   Number 1942  B       b2480   t2480
5942  O       o2235   resource_defs p2234 p2235 p294  T       t2486   o b726 b2480
5943  P       p2237   Number 1940  B       b2486   t2486
5944  O       o2237   uid p2237 p2235  T       t2487   o b727 b2486
5945  T       t2237   o2237 b816  B       b2487   t2487
5946  B       b2237   t2237  T       t2494   o b723 b2487
5947  T       t2238   o b2237 b4  B       b2494   t2494
5948  B       b2238   t2238  T       t2495   o747 b824 b2494
5949  T       t2239   o2235 b2238  B       b2495   t2495
5950  B       b2239   t2239  T       t2496   o746 b2495 b4 b753
5951  T       t2240   o b2239 b4  B       b2496   t2496
5952  B       b2240   t2240  T       t2497   o747 b834 b2494
5953  T       t2241   o824 b718 b2233 b876 b2240  B       b2497   t2497
5954  B       b2241   t2241  T       t2515   o747 b836 b2494
5955  T       t2248   o2229 b2241  B       b2515   t2515
5956  B       b2248   t2248  T       t2516   o747 b838 b2494
5957  P       p2249   Number 2237  B       b2517   t2516
5958  P       p2253   Number 2584  T       t2517   o747 b840 b2494
5959  O       o2253   location p2249 p2253  B       b2733   t2517
5960    T       t2733   o747 b843 b2494
5961    B       b2744   t2733
5962    T       t2744   o2 b2496
5963    B       b2745   t2744
5964    T       t2745   o774 b2744 b780 b2745
5965    B       b2746   t2745
5966    T       t2746   o2 b2746
5967    B       b2747   t2746
5968    T       t2758   o746 b2733 b4 b2747
5969    B       b2758   t2758
5970    T       t2760   o2 b2758
5971    B       b2761   t2760
5972    T       t2761   o746 b2517 b4 b2761
5973    B       b2762   t2761
5974    T       t2762   o2 b2762
5975    B       b2763   t2762
5976    T       t2763   o746 b2515 b4 b2763
5977    B       b2764   t2763
5978    T       t2764   o2 b2764
5979    B       b2765   t2764
5980    T       t2765   o746 b2497 b4 b2765
5981    B       b2766   t2765
5982    T       t2766   o747 b855 b2494
5983    B       b2767   t2766
5984    T       t2767   o747 b857 b2494
5985    B       b2768   t2767
5986    T       t2785   o747 b859 b2494
5987    B       b2801   t2785
5988    T       t2826   o746 b2801 b4 b2761
5989    B       b3086   t2826
5990    T       t3086   o2 b3086
5991    B       b3093   t3086
5992    T       t3093   o746 b2768 b4 b3093
5993    B       b3094   t3093
5994    T       t3094   o2 b3094
5995    B       b3095   t3094
5996    T       t3095   o746 b2767 b4 b3095
5997    B       b3102   t3095
5998    T       t3102   o b3102 b4
5999    B       b3120   t3102
6000    T       t3120   o b2766 b3120
6001    B       b3121   t3120
6002    T       t3121   o745 b2496 b3121
6003    B       b3129   t3121
6004    T       t3129   o745 b2766 b4
6005    B       b3130   t3129
6006    T       t3130   o805 b744 b3130 b4 b4
6007    B       b3149   t3130
6008    T       t3149   o745 b3102 b4
6009    B       b3165   t3149
6010    T       t3165   o807 b744 b3165 b4 b4
6011    B       b3179   t3165
6012    T       t3179   o b3179 b4
6013    B       b3185   t3179
6014    T       t3186   o b3149 b3185
6015    B       b3187   t3186
6016    T       t3187   o743 b744 b3129 b3187 b4
6017    B       b3189   t3187
6018    T       t3189   o742 b3189
6019    B       b3191   t3189
6020  T       t2253   o718 b817 b273  T       t2253   o718 b817 b273
6021  B       b2253   t2253  B       b2253   t2253
6022  T       t2254   o718 b728 b2253  T       t2254   o718 b728 b2253
6023  B       b2254   t2254  B       b2254   t2254
6024  T       t2258   o718 b724 b2254  T       t2258   o718 b724 b2254
6025  B       b2258   t2258  B       b2258   t2258
6026  P       p2296   Number 2262  T       t3203   o b726 b296
6027  P       p2258   Number 2270  B       b3204   t3203
6028  O       o2258   resource_defs p2296 p2258 p294  T       t3204   o b727 b3204
6029  P       p2259   Number 2268  B       b3205   t3204
6030  O       o2259   uid p2259 p2258  T       t3205   o b723 b3205
6031  T       t2259   o2259 b816  B       b3206   t3205
6032  B       b2259   t2259  T       t3206   o747 b268 b3206
6033  T       t2260   o b2259 b4  B       b3207   t3206
6034  B       b2260   t2260  T       t3207   o746 b3207 b4 b753
6035  T       t2265   o2258 b2260  B       b3208   t3207
6036  B       b2265   t2265  T       t3208   o747 b322 b3206
6037  T       t2266   o b2265 b4  B       b3209   t3208
6038  B       b2266   t2266  T       t3209   o747 b334 b3206
6039  T       t2267   o8 b718 b2258 b2478 b2266  B       b3210   t3209
6040  B       b2267   t2267  T       t3210   o747 b346 b3206
6041  T       t2271   o2253 b2267  B       b3211   t3210
6042  B       b2271   t2271  T       t3215   o747 b361 b3206
6043  P       p2271   Number 2586  B       b3216   t3215
6044  P       p2273   Number 3011  T       t3216   o747 b370 b3206
6045  O       o2273   location p2271 p2273  B       b3217   t3216
6046  T       t2274   o718 b817 b2493  T       t3217   o747 b423 b3206
6047  B       b2274   t2274  B       b3218   t3217
6048  T       t2278   o718 b728 b2274  T       t3218   o2 b3208
6049  B       b2278   t2278  B       b3219   t3218
6050  T       t2279   o718 b724 b2278  T       t3219   o746 b3218 b780 b3219
6051  B       b2279   t2279  B       b3220   t3219
6052  T       t2280   o718 b888 b2279  T       t3222   o2 b3220
6053  B       b2280   t2280  B       b3222   t3222
6054  P       p2280   Number 2617  T       t3223   o746 b3217 b780 b3222
6055  P       p2281   Number 2625  B       b3223   t3223
6056  O       o2281   resource_defs p2280 p2281 p294  T       t3224   o2 b3223
6057  P       p2282   Number 2623  B       b3224   t3224
6058  O       o2282   uid p2282 p2281  T       t3225   o746 b3216 b780 b3224
6059  T       t2282   o2282 b816  B       b3225   t3225
6060  B       b2282   t2282  T       t3226   o2 b3225
6061  T       t2283   o b2282 b4  B       b3226   t3226
6062  B       b2283   t2283  T       t3227   o746 b3211 b780 b3226
6063  T       t2286   o2281 b2283  B       b3227   t3227
6064  B       b2286   t2286  T       t3230   o2 b3227
6065  T       t2287   o b2286 b4  B       b3233   t3230
6066  B       b2287   t2287  T       t3233   o307 b3210 b780 b3233
6067  T       t2288   o2487 b718 b2280 b2732 b2287  B       b3234   t3233
6068  B       b2288   t2288  T       t3234   o2 b3234
6069  T       t2289   o2273 b2288  B       b3235   t3234
6070  B       b2289   t2289  T       t3235   o307 b3209 b4 b3235
6071  P       p2289   Number 3013  B       b3236   t3235
6072  P       p2290   Number 3365  T       t3236   o747 b480 b3206
6073  O       o2290   location p2289 p2290  B       b3237   t3236
6074  T       t2290   o718 b817 b2743  T       t3237   o747 b489 b3206
6075  B       b2290   t2290  B       b3238   t3237
6076  T       t2291   o718 b728 b2290  T       t3238   o307 b3238 b780 b3233
6077  B       b2291   t2291  B       b3239   t3238
6078  T       t2294   o718 b724 b2291  T       t3239   o2 b3239
6079  B       b2294   t2294  B       b3240   t3239
6080  T       t2295   o718 b888 b2294  T       t3240   o307 b3237 b4 b3240
6081  B       b2295   t2295  B       b3241   t3240
6082  P       p2295   Number 3045  T       t3241   o747 b511 b3206
6083  P       p2301   Number 3053  B       b3242   t3241
6084  O       o2301   resource_defs p2295 p2301 p294  T       t3250   o746 b3242 b4 b3233
6085  P       p2302   Number 3051  B       b3251   t3250
6086  O       o2302   uid p2302 p2301  T       t3251   o b3251 b4
6087  T       t2302   o2302 b816  B       b3252   t3251
6088  B       b2302   t2302  T       t3252   o b3241 b3252
6089  T       t2303   o b2302 b4  B       b3253   t3252
6090  B       b2303   t2303  T       t3253   o b3236 b3253
6091  T       t2304   o2301 b2303  B       b3254   t3253
6092  B       b2304   t2304  T       t3254   o745 b3208 b3254
6093  T       t2305   o b2304 b4  B       b3255   t3254
6094  B       b2305   t2305  T       t3255   o745 b3236 b4
6095  T       t2325   o2739 b718 b2295 b2757 b2305  B       b3257   t3255
6096  B       b2325   t2325  T       t3257   o535 b744 b3257 b4 b4
6097  T       t2326   o2290 b2325  B       b3258   t3257
6098  B       b2326   t2326  T       t3258   o745 b3241 b4
6099  P       p2326   Number 3404  B       b3259   t3258
6100  P       p2327   Number 3884  T       t3259   o543 b744 b3259 b4 b4
6101  O       o2327   location p2326 p2327  B       b3260   t3259
6102    T       t3260   o747 b556 b3206
6103    B       b3261   t3260
6104    T       t3261   o2 b3251
6105    B       b3262   t3261
6106    T       t3262   o774 b3261 b4 b3262
6107    B       b3268   t3262
6108    T       t3268   o747 b570 b3206
6109    B       b3269   t3268
6110    T       t3269   o746 b3269 b4 b3262
6111    B       b3270   t3269
6112    T       t3270   o b3270 b4
6113    B       b3271   t3270
6114    T       t3271   o b3268 b3271
6115    B       b3272   t3271
6116    T       t3272   o745 b3251 b3272
6117    B       b3273   t3272
6118    T       t3273   o745 b3268 b4
6119    B       b3274   t3273
6120    T       t3274   o535 b744 b3274 b4 b4
6121    B       b3275   t3274
6122    T       t3275   o747 b600 b3206
6123    B       b3276   t3275
6124    T       t3276   o2 b3270
6125    B       b3277   t3276
6126    T       t3277   o774 b3276 b4 b3277
6127    B       b3278   t3277
6128    T       t3278   o747 b605 b3206
6129    B       b3279   t3278
6130    T       t3279   o746 b3279 b4 b3277
6131    B       b3280   t3279
6132    T       t3280   o b3280 b4
6133    B       b3281   t3280
6134    T       t3281   o b3278 b3281
6135    B       b3282   t3281
6136    T       t3282   o745 b3270 b3282
6137    B       b3283   t3282
6138    T       t3283   o745 b3278 b4
6139    B       b3293   t3283
6140    T       t3295   o543 b744 b3293 b4 b4
6141    B       b3296   t3295
6142    T       t3297   o747 b743 b3206
6143    B       b3298   t3297
6144    T       t3299   o747 b814 b3206
6145    B       b3318   t3299
6146    T       t3318   o747 b823 b3206
6147    B       b3319   t3318
6148    T       t3319   o747 b877 b3206
6149    B       b3320   t3319
6150    T       t3320   o747 b921 b3206
6151    B       b3323   t3320
6152    T       t3323   o2 b3280
6153    B       b3324   t3323
6154    T       t3324   o774 b3323 b780 b3324
6155    B       b3325   t3324
6156    T       t3325   o2 b3325
6157    B       b3327   t3325
6158    T       t3327   o746 b3320 b4 b3327
6159    B       b3329   t3327
6160    T       t3329   o2 b3329
6161    B       b3331   t3329
6162    T       t3331   o746 b3319 b4 b3331
6163    B       b3335   t3331
6164    T       t3407   o2 b3335
6165    B       b3407   t3407
6166    T       t3408   o746 b3318 b4 b3407
6167    B       b3408   t3408
6168    T       t3409   o2 b3408
6169    B       b3409   t3409
6170    T       t3410   o746 b3298 b4 b3409
6171    B       b3410   t3410
6172    T       t3411   o747 b2299 b3206
6173    B       b3411   t3411
6174    T       t3412   o747 b2313 b3206
6175    B       b3412   t3412
6176    T       t3413   o747 b2381 b3206
6177    B       b3413   t3413
6178    T       t3414   o746 b3413 b4 b3331
6179    B       b3414   t3414
6180    T       t3415   o2 b3414
6181    B       b3415   t3415
6182    T       t3416   o746 b3412 b4 b3415
6183    B       b3416   t3416
6184    T       t3417   o2 b3416
6185    B       b3417   t3417
6186    T       t3418   o746 b3411 b4 b3417
6187    B       b3418   t3418
6188    T       t3419   o b3418 b4
6189    B       b3419   t3419
6190    T       t3420   o b3410 b3419
6191    B       b3420   t3420
6192    T       t3421   o745 b3280 b3420
6193    B       b3421   t3421
6194    T       t3422   o747 b2393 b3206
6195    B       b3422   t3422
6196    T       t3423   o2 b3410
6197    B       b3423   t3423
6198    T       t3424   o746 b3422 b4 b3423
6199    B       b3424   t3424
6200    T       t3425   o b3424 b4
6201    B       b3425   t3425
6202    T       t3426   o745 b3410 b3425
6203    B       b3426   t3426
6204    T       t3427   o747 b2400 b3206
6205    B       b3427   t3427
6206    T       t3428   o2 b3424
6207    B       b3428   t3428
6208    T       t3429   o746 b3427 b4 b3428
6209    B       b3429   t3429
6210    T       t3430   o b3429 b4
6211    B       b3430   t3430
6212    T       t3431   o745 b3424 b3430
6213    B       b3431   t3431
6214    T       t3432   o747 b2406 b3206
6215    B       b3432   t3432
6216    T       t3433   o747 b2408 b3206
6217    B       b3433   t3433
6218    T       t3434   o2 b3429
6219    B       b3434   t3434
6220    T       t3435   o2406 b3433 b780 b3434
6221    B       b3435   t3435
6222    T       t3436   o2 b3435
6223    B       b3436   t3436
6224    T       t3437   o2406 b3432 b4 b3436
6225    B       b3437   t3437
6226    T       t3438   o b3437 b4
6227    B       b3438   t3438
6228    T       t3439   o745 b3429 b3438
6229    B       b3439   t3439
6230    T       t3440   o747 b2416 b3206
6231    B       b3440   t3440
6232    T       t3441   o747 b2418 b3206
6233    B       b3441   t3441
6234    T       t3442   o2 b3437
6235    B       b3442   t3442
6236    T       t3443   o2406 b3441 b780 b3442
6237    B       b3443   t3443
6238    T       t3444   o2 b3443
6239    B       b3444   t3444
6240    T       t3445   o2406 b3440 b4 b3444
6241    B       b3445   t3445
6242    T       t3446   o b3445 b4
6243    B       b3446   t3446
6244    T       t3447   o745 b3437 b3446
6245    B       b3447   t3447
6246    T       t3448   o745 b3445 b4
6247    B       b3448   t3448
6248    T       t3449   o2425 b744 b3448 b4 b4
6249    B       b3449   t3449
6250    T       t3450   o b3449 b4
6251    B       b3450   t3450
6252    T       t3451   o2415 b744 b3447 b3450 b4
6253    B       b3451   t3451
6254    T       t3452   o b3451 b4
6255    B       b3452   t3452
6256    T       t3453   o2405 b744 b3439 b3452 b4
6257    B       b3453   t3453
6258    T       t3454   o b3453 b4
6259    B       b3454   t3454
6260    T       t3455   o2398 b744 b3431 b3454 b4
6261    B       b3455   t3455
6262    T       t3456   o b3455 b4
6263    B       b3456   t3456
6264    T       t3457   o805 b744 b3426 b3456 b4
6265    B       b3457   t3457
6266    T       t3458   o747 b2438 b3206
6267    B       b3458   t3458
6268    T       t3459   o2 b3418
6269    B       b3459   t3459
6270    T       t3460   o746 b3458 b4 b3459
6271    B       b3460   t3460
6272    T       t3461   o b3460 b4
6273    B       b3461   t3461
6274    T       t3462   o745 b3418 b3461
6275    B       b3462   t3462
6276    T       t3463   o747 b2445 b3206
6277    B       b3463   t3463
6278    T       t3464   o2 b3460
6279    B       b3464   t3464
6280    T       t3465   o746 b3463 b4 b3464
6281    B       b3465   t3465
6282    T       t3466   o b3465 b4
6283    B       b3466   t3466
6284    T       t3467   o745 b3460 b3466
6285    B       b3467   t3467
6286    T       t3468   o747 b2451 b3206
6287    B       b3468   t3468
6288    T       t3469   o2 b3465
6289    B       b3469   t3469
6290    T       t3470   o2406 b3468 b4 b3469
6291    B       b3470   t3470
6292    T       t3471   o b3470 b4
6293    B       b3471   t3471
6294    T       t3472   o745 b3465 b3471
6295    B       b3472   t3472
6296    T       t3473   o745 b3470 b4
6297    B       b3473   t3473
6298    T       t3474   o2456 b744 b3473 b4 b4
6299    B       b3474   t3474
6300    T       t3475   o b3474 b4
6301    B       b3475   t3475
6302    T       t3476   o2450 b744 b3472 b3475 b4
6303    B       b3476   t3476
6304    T       t3477   o b3476 b4
6305    B       b3477   t3477
6306    T       t3478   o2443 b744 b3467 b3477 b4
6307    B       b3478   t3478
6308    T       t3479   o b3478 b4
6309    B       b3479   t3479
6310    T       t3480   o807 b744 b3462 b3479 b4
6311    B       b3480   t3480
6312    T       t3481   o b3480 b4
6313    B       b3481   t3481
6314    T       t3482   o b3457 b3481
6315    B       b3482   t3482
6316    T       t3483   o641 b744 b3421 b3482 b4
6317    B       b3483   t3483
6318    T       t3484   o b3483 b4
6319    B       b3484   t3484
6320    T       t3485   o b3296 b3484
6321    B       b3485   t3485
6322    T       t3486   o597 b744 b3283 b3485 b4
6323    B       b3486   t3486
6324    T       t3487   o b3486 b4
6325    B       b3487   t3487
6326    T       t3488   o b3275 b3487
6327    B       b3488   t3488
6328    T       t3489   o551 b744 b3273 b3488 b4
6329    B       b3489   t3489
6330    T       t3490   o b3489 b4
6331    B       b3490   t3490
6332    T       t3491   o b3260 b3490
6333    B       b3491   t3491
6334    T       t3492   o b3258 b3491
6335    B       b3492   t3492
6336    T       t3493   o290 b744 b3255 b3492 b4
6337    B       b3493   t3493
6338    T       t3494   o742 b3493
6339    B       b3494   t3494
6340    T       t3501   o2488 b733 b711 b244
6341    S       s3501   t726 h
6342    G       s3501   t3501
6343    B       b3501   s3501
6344    T       t3502   o719 b3501
6345    B       b3502   t3502
6346    T       t3503   o2488 b733 b711 b267
6347    S       s3503   t726 h
6348    G       s3503   t3503
6349    B       b3503   s3503
6350    T       t3504   o719 b3503
6351    B       b3504   t3504
6352    T       t3505   o718 b3502 b3504
6353    B       b3505   t3505
6354    T       t3506   o718 b817 b3505
6355    B       b3506   t3506
6356    T       t3507   o718 b728 b3506
6357    B       b3507   t3507
6358    T       t3508   o718 b724 b3507
6359    B       b3508   t3508
6360    P       p3508   String "assumT 4 thenT rwh unfold_equiv_fun_set 0 thenT dT 0 thenT dT 0 thenT dT 0 ttca thenT dT 0 ttca thenT rwh unfold_equiv_fun_set 2 thenT instHypT [<< 'a >>; << 'b >>] 2 ttca thenT dT 7 ttca thenT dT 7 ttca"
6361    O       o3508   ext_rule p3508
6362    T       t3509   o b3501 b4
6363    B       b3509   t3509
6364    T       t3510   o b726 b3509
6365    B       b3510   t3510
6366    T       t3511   o b727 b3510
6367    B       b3511   t3511
6368    T       t3512   o b723 b3511
6369    B       b3512   t3512
6370    T       t3513   o747 b3503 b3512
6371    B       b3513   t3513
6372    T       t3514   o746 b3513 b4 b753
6373    B       b3514   t3514
6374    T       t3515   o888 b733 b711
6375    B       b3515   t3515
6376    T       t3516   o888 b733 b711 b2509 b2510
6377    B       b3516   t3516
6378    T       t3517   o348 b712 b3516
6379    B       b3517   t3517
6380    T       t3518   o348 b3515 b3517
6381    B       b3518   t3518 b
6382    T       t3519   o775 b365 b3518
6383    B       b3519   t3519 a
6384    T       t3520   o775 b365 b3519
6385    H       h3520   v t3520
6386    H       h3521   x t3515
6387    H       h3522   x_1 t712
6388    H       h3523   y_1 t3516
6389    T       t3523   o888 b733 b711 b2519 b2520
6390    S       s3523   t726 h h3520 h2515 h2516 h3521 h3522 h3523
6391    G       s3523   t3523
6392    B       b3523   s3523
6393    T       t3524   o747 b3523 b3512
6394    B       b3524   t3524
6395    H       h3524   y t3517
6396    S       s3524   t726 h h3520 h2515 h2516 h3521 h3522 h3524 h3523
6397    G       s3524   t3523
6398    B       b3525   s3524
6399    T       t3525   o747 b3525 b3512
6400    B       b3526   t3525
6401    S       s3526   t726 h h3520 h2515 h2516 h3521 h3522 h3524
6402    G       s3526   t3523
6403    B       b3527   s3526
6404    T       t3527   o747 b3527 b3512
6405    B       b3528   t3527
6406    H       h3528   w_1 t3518
6407    S       s3528   t726 h h3520 h2515 h2516 h3521 h3522 h3528 h3524
6408    G       s3528   t3523
6409    B       b3529   s3528
6410    T       t3529   o747 b3529 b3512
6411    B       b3530   t3529
6412    S       s3530   t726 h h3520 h2515 h2516 h3521 h3522 h3528
6413    G       s3530   t3523
6414    B       b3531   s3530
6415    T       t3531   o747 b3531 b3512
6416    B       b3532   t3531
6417    H       h3532   w t3519
6418    S       s3532   t726 h h3520 h2515 h2516 h3521 h3522 h3532 h3528
6419    G       s3532   t3523
6420    B       b3533   s3532
6421    T       t3533   o747 b3533 b3512
6422    B       b3534   t3533
6423    S       s3534   t726 h h3520 h2515 h2516 h3521 h3522 h3532
6424    G       s3534   t3523
6425    B       b3535   s3534
6426    T       t3535   o747 b3535 b3512
6427    B       b3536   t3535
6428    S       s3536   t726 h h3520 h2515 h2516 h3521 h3522
6429    G       s3536   t3523
6430    B       b3537   s3536
6431    T       t3537   o747 b3537 b3512
6432    B       b3538   t3537
6433    H       h3538   v t3501
6434    S       s3538   t726 h h3538 h2515 h2516 h3521 h3522
6435    G       s3538   t3523
6436    B       b3539   s3538
6437    T       t3539   o747 b3539 b3512
6438    B       b3540   t3539
6439    B       b3541   t3523
6440    T       t3541   o348 b712 b3541
6441    S       s3541   t726 h h3538 h2515 h2516 h3521
6442    G       s3541   t3541
6443    B       b3542   s3541
6444    T       t3542   o747 b3542 b3512
6445    B       b3543   t3542
6446    B       b3544   t3541
6447    T       t3544   o348 b3515 b3544
6448    S       s3544   t726 h h3538 h2515 h2516
6449    G       s3544   t3544
6450    B       b3545   s3544
6451    T       t3545   o747 b3545 b3512
6452    B       b3546   t3545
6453    B       b3547   t3544 b
6454    T       t3547   o775 b365 b3547
6455    S       s3547   t726 h h3538 h2515
6456    G       s3547   t3547
6457    B       b3548   s3547
6458    T       t3548   o747 b3548 b3512
6459    B       b3549   t3548
6460    B       b3550   t3547 a
6461    T       t3550   o775 b365 b3550
6462    S       s3550   t726 h h3538
6463    G       s3550   t3550
6464    B       b3551   s3550
6465    T       t3551   o747 b3551 b3512
6466    B       b3552   t3551
6467    S       s3552   t726 h h3538
6468    G       s3552   t3503
6469    B       b3553   s3552
6470    T       t3553   o747 b3553 b3512
6471    B       b3554   t3553
6472    T       t3554   o2 b3514
6473    B       b3555   t3554
6474    T       t3555   o746 b3554 b4 b3555
6475    B       b3556   t3555
6476    T       t3556   o2 b3556
6477    B       b3557   t3556
6478    T       t3557   o746 b3552 b4 b3557
6479    B       b3558   t3557
6480    T       t3558   o2 b3558
6481    B       b3559   t3558
6482    T       t3559   o746 b3549 b4 b3559
6483    B       b3560   t3559
6484    T       t3560   o2 b3560
6485    B       b3561   t3560
6486    T       t3561   o746 b3546 b4 b3561
6487    B       b3562   t3561
6488    T       t3562   o2 b3562
6489    B       b3563   t3562
6490    T       t3563   o746 b3543 b4 b3563
6491    B       b3564   t3563
6492    T       t3564   o2 b3564
6493    B       b3565   t3564
6494    T       t3565   o746 b3540 b4 b3565
6495    B       b3566   t3565
6496    T       t3566   o2 b3566
6497    B       b3567   t3566
6498    T       t3567   o746 b3538 b2547 b3567
6499    B       b3568   t3567
6500    T       t3568   o2 b3568
6501    B       b3569   t3568
6502    T       t3569   o746 b3536 b2541 b3569
6503    B       b3570   t3569
6504    T       t3570   o2 b3570
6505    B       b3571   t3570
6506    T       t3571   o746 b3534 b2535 b3571
6507    B       b3572   t3571
6508    T       t3572   o2 b3572
6509    B       b3573   t3572
6510    T       t3573   o746 b3532 b4 b3573
6511    B       b3574   t3573
6512    T       t3574   o2 b3574
6513    B       b3575   t3574
6514    T       t3575   o746 b3530 b4 b3575
6515    B       b3576   t3575
6516    T       t3576   o2 b3576
6517    B       b3577   t3576
6518    T       t3577   o746 b3528 b4 b3577
6519    B       b3578   t3577
6520    T       t3578   o2 b3578
6521    B       b3579   t3578
6522    T       t3579   o746 b3526 b4 b3579
6523    B       b3580   t3579
6524    T       t3580   o2 b3580
6525    B       b3581   t3580
6526    T       t3581   o746 b3524 b4 b3581
6527    B       b3582   t3581
6528    T       t3582   o b3582 b4
6529    B       b3583   t3582
6530    T       t3583   o745 b3514 b3583
6531    B       b3584   t3583
6532    P       p3584   String "genAssumT [3] thenT dT 0 ttca thenT dT 8 thenT rwh unfold_power 0 thenT rwh reduceC 0 ttca"
6533    O       o3584   ext_rule p3584
6534    T       t3584   o888 b733 b711 b2594 b2595
6535    H       h3584   z t3584
6536    T       t3585   o888 b733 b711 b2600 b2605
6537    S       s3585   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6538    G       s3585   t3585
6539    B       b3585   s3585
6540    T       t3586   o747 b3585 b3512
6541    B       b3586   t3586
6542    T       t3587   o888 b733 b711 b2608 b2609
6543    S       s3587   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6544    G       s3587   t3587
6545    B       b3587   s3587
6546    T       t3588   o747 b3587 b3512
6547    B       b3588   t3588
6548    S       s3588   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h770 h754 h2593 h3584
6549    G       s3588   t3587
6550    B       b3589   s3588
6551    T       t3589   o747 b3589 b3512
6552    B       b3590   t3589
6553    S       s3590   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h770
6554    G       s3590   t3523
6555    B       b3591   s3590
6556    T       t3591   o747 b3591 b3512
6557    B       b3592   t3591
6558    B       b3593   t3523 n
6559    T       t3593   o775 b621 b3593
6560    S       s3593   t726 h h3520 h2515 h2516 h3521 h3522 h3523
6561    G       s3593   t3593
6562    B       b3594   s3593
6563    T       t3594   o747 b3594 b3512
6564    B       b3595   t3594
6565    T       t3595   o2 b3582
6566    B       b3596   t3595
6567    T       t3596   o774 b3595 b4 b3596
6568    B       b3597   t3596
6569    T       t3597   o2 b3597
6570    B       b3598   t3597
6571    T       t3598   o746 b3592 b4 b3598
6572    B       b3599   t3598
6573    T       t3599   o2 b3599
6574    B       b3600   t3599
6575    T       t3600   o746 b3590 b4 b3600
6576    B       b3601   t3600
6577    T       t3601   o2 b3601
6578    B       b3602   t3601
6579    T       t3602   o746 b3588 b4 b3602
6580    B       b3603   t3602
6581    T       t3603   o2 b3603
6582    B       b3604   t3603
6583    T       t3604   o746 b3586 b4 b3604
6584    B       b3605   t3604
6585    T       t3605   o888 b733 b711 b2598 b2603
6586    H       h3605   z t3605
6587    S       s3605   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2628 h3605
6588    G       s3605   t3585
6589    B       b3606   s3605
6590    T       t3606   o747 b3606 b3512
6591    B       b3607   t3606
6592    S       s3607   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2628 h3605
6593    G       s3607   t3587
6594    B       b3608   s3607
6595    T       t3608   o747 b3608 b3512
6596    B       b3609   t3608
6597    S       s3609   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h770 h754 h2628 h3605
6598    G       s3609   t3587
6599    B       b3610   s3609
6600    T       t3610   o747 b3610 b3512
6601    B       b3611   t3610
6602    T       t3611   o746 b3611 b4 b3600
6603    B       b3612   t3611
6604    T       t3612   o2 b3612
6605    B       b3613   t3612
6606    T       t3613   o746 b3609 b4 b3613
6607    B       b3614   t3613
6608    T       t3614   o2 b3614
6609    B       b3615   t3614
6610    T       t3615   o746 b3607 b4 b3615
6611    B       b3616   t3615
6612    T       t3616   o b3616 b4
6613    B       b3617   t3616
6614    T       t3617   o b3605 b3617
6615    B       b3618   t3617
6616    T       t3618   o745 b3582 b3618
6617    B       b3619   t3618
6618    T       t3619   o888 b733 b711 b2643 b2644
6619    S       s3619   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6620    G       s3619   t3619
6621    B       b3620   s3619
6622    T       t3620   o747 b3620 b3512
6623    B       b3621   t3620
6624    T       t3621   o2 b3605
6625    B       b3622   t3621
6626    T       t3622   o746 b3621 b4 b3622
6627    B       b3623   t3622
6628    T       t3623   o b3623 b4
6629    B       b3624   t3623
6630    T       t3624   o745 b3605 b3624
6631    B       b3625   t3624
6632    P       p3625   String "equivSubstT << equiv{car{'g}; eqG{'g}; power{'g; 'f['a]; ('m +@ 1)}; power{'g; 'f['b]; ('m +@ 1)}} >> 0 ttca"
6633    O       o3625   ext_rule p3625
6634    T       t3625   o888 b733 b711 b2651 b2644
6635    S       s3625   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6636    G       s3625   t3625
6637    B       b3626   s3625
6638    T       t3626   o747 b3626 b3512
6639    B       b3627   t3626
6640    T       t3627   o2 b3623
6641    B       b3628   t3627
6642    T       t3628   o746 b3627 b4 b3628
6643    B       b3629   t3628
6644    T       t3629   o888 b733 b711 b2656 b2644
6645    B       b3630   t3629 z
6646    T       t3630   o1427 b733 b711 b3630
6647    S       s3630   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6648    G       s3630   t3630
6649    B       b3631   s3630
6650    T       t3631   o747 b3631 b3512
6651    B       b3632   t3631
6652    T       t3632   o746 b3632 b4 b3628
6653    B       b3633   t3632
6654    T       t3633   o b3633 b4
6655    B       b3634   t3633
6656    T       t3634   o b3629 b3634
6657    B       b3635   t3634
6658    T       t3635   o745 b3623 b3635
6659    B       b3636   t3635
6660    P       p3636   String "equivSubstT << equiv{car{'g}; eqG{'g}; inv{'g; 'f['a]}; inv{'g; 'f['b]}} >> 0 ttca"
6661    O       o3636   ext_rule p3636
6662    T       t3636   o888 b733 b711 b2596 b2601
6663    S       s3636   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6664    G       s3636   t3636
6665    B       b3637   s3636
6666    T       t3637   o747 b3637 b3512
6667    B       b3638   t3637
6668    T       t3638   o2 b3629
6669    B       b3639   t3638
6670    T       t3639   o746 b3638 b4 b3639
6671    B       b3640   t3639
6672    T       t3640   o888 b733 b711 b2644 b2644
6673    S       s3640   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6674    G       s3640   t3640
6675    B       b3641   s3640
6676    T       t3641   o747 b3641 b3512
6677    B       b3642   t3641
6678    T       t3642   o746 b3642 b4 b3639
6679    B       b3643   t3642
6680    T       t3643   o888 b733 b711 b2671 b2644
6681    B       b3644   t3643 z
6682    T       t3644   o1427 b733 b711 b3644
6683    S       s3644   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2593 h3584
6684    G       s3644   t3644
6685    B       b3645   s3644
6686    T       t3645   o747 b3645 b3512
6687    B       b3646   t3645
6688    T       t3646   o746 b3646 b4 b3639
6689    B       b3647   t3646
6690    T       t3647   o b3647 b4
6691    B       b3648   t3647
6692    T       t3648   o b3643 b3648
6693    B       b3649   t3648
6694    T       t3649   o b3640 b3649
6695    B       b3650   t3649
6696    T       t3650   o745 b3629 b3650
6697    B       b3651   t3650
6698    P       p3651   String "equivSubstT << equiv{car{'g}; eqG{'g}; 'f['a]; 'f['b]} >> 0 thenT autoT thenT rwh unfold_equiv 7 ttca"
6699    O       o3651   ext_rule p3651
6700    T       t3651   o745 b3640 b4
6701    B       b3652   t3651
6702    T       t3652   o3651 b744 b3652 b4 b4
6703    B       b3653   t3652
6704    T       t3653   o745 b3643 b4
6705    B       b3654   t3653
6706    T       t3654   o2681 b744 b3654 b4 b4
6707    B       b3655   t3654
6708    T       t3655   o745 b3647 b4
6709    B       b3656   t3655
6710    T       t3656   o2681 b744 b3656 b4 b4
6711    B       b3657   t3656
6712    T       t3657   o b3657 b4
6713    B       b3658   t3657
6714    T       t3658   o b3655 b3658
6715    B       b3659   t3658
6716    T       t3659   o b3653 b3659
6717    B       b3660   t3659
6718    T       t3660   o3636 b744 b3651 b3660 b4
6719    B       b3661   t3660
6720    T       t3661   o745 b3633 b4
6721    B       b3662   t3661
6722    T       t3662   o2681 b744 b3662 b4 b4
6723    B       b3663   t3662
6724    T       t3663   o b3663 b4
6725    B       b3664   t3663
6726    T       t3664   o b3661 b3664
6727    B       b3665   t3664
6728    T       t3665   o3625 b744 b3636 b3665 b4
6729    B       b3666   t3665
6730    T       t3666   o b3666 b4
6731    B       b3667   t3666
6732    T       t3667   o805 b744 b3625 b3667 b4
6733    B       b3668   t3667
6734    T       t3668   o888 b733 b711 b2697 b2698
6735    S       s3668   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2628 h3605
6736    G       s3668   t3668
6737    B       b3669   s3668
6738    T       t3669   o747 b3669 b3512
6739    B       b3670   t3669
6740    T       t3670   o2 b3616
6741    B       b3671   t3670
6742    T       t3671   o746 b3670 b4 b3671
6743    B       b3672   t3671
6744    T       t3672   o b3672 b4
6745    B       b3673   t3672
6746    T       t3673   o745 b3616 b3673
6747    B       b3674   t3673
6748    P       p3674   String "equivSubstT << equiv{car{'g}; eqG{'g}; power{'g; 'f['a]; ('m -@ 1)}; power{'g; 'f['b]; ('m -@ 1)}} >> 0 ttca"
6749    O       o3674   ext_rule p3674
6750    T       t3674   o888 b733 b711 b2705 b2698
6751    S       s3674   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2628 h3605
6752    G       s3674   t3674
6753    B       b3675   s3674
6754    T       t3675   o747 b3675 b3512
6755    B       b3676   t3675
6756    T       t3676   o2 b3672
6757    B       b3677   t3676
6758    T       t3677   o746 b3676 b4 b3677
6759    B       b3678   t3677
6760    T       t3678   o888 b733 b711 b2710 b2698
6761    B       b3679   t3678 z
6762    T       t3679   o1427 b733 b711 b3679
6763    S       s3679   t726 h h3520 h2515 h2516 h3521 h3522 h3523 h754 h2628 h3605
6764    G       s3679   t3679
6765    B       b3680   s3679
6766    T       t3680   o747 b3680 b3512
6767    B       b3681   t3680
6768    T       t3681   o746 b3681 b4 b3677
6769    B       b3682   t3681
6770    T       t3682   o b3682 b4
6771    B       b3683   t3682
6772    T       t3683   o b3678 b3683
6773    B       b3684   t3683
6774    T       t3684   o745 b3672 b3684
6775    B       b3685   t3684
6776    T       t3685   o745 b3678 b4
6777    B       b3686   t3685
6778    T       t3686   o3651 b744 b3686 b4 b4
6779    B       b3687   t3686
6780    T       t3687   o745 b3682 b4
6781    B       b3688   t3687
6782    T       t3688   o2681 b744 b3688 b4 b4
6783    B       b3689   t3688
6784    T       t3689   o b3689 b4
6785    B       b3690   t3689
6786    T       t3690   o b3687 b3690
6787    B       b3691   t3690
6788    T       t3691   o3674 b744 b3685 b3691 b4
6789    B       b3692   t3691
6790    T       t3692   o b3692 b4
6791    B       b3693   t3692
6792    T       t3693   o807 b744 b3674 b3693 b4
6793    B       b3694   t3693
6794    T       t3694   o b3694 b4
6795    B       b3695   t3694
6796    T       t3695   o b3668 b3695
6797    B       b3696   t3695
6798    T       t3696   o3584 b744 b3619 b3696 b4
6799    B       b3697   t3696
6800    T       t3697   o b3697 b4
6801    B       b3698   t3697
6802    T       t3698   o730 b733
6803    B       b3699   t3698
6804    B       b3700   t887
6805    T       t3700   o730 b2509
6806    B       b3701   t3700
6807    T       t3701   o730 b2510
6808    B       b3702   t3701
6809    T       t3702   o644 b3701 b3702
6810    B       b3703   t3702
6811    T       t3703   o644 b3700 b3703
6812    B       b3704   t3703
6813    T       t3704   o644 b3699 b3704
6814    B       b3705   t3704
6815    T       t3705   o732 b2509 b733
6816    B       b3706   t3705
6817    T       t3706   o732 b2510 b733
6818    B       b3707   t3706
6819    T       t3707   o644 b3706 b3707
6820    B       b3708   t3707
6821    T       t3708   o644 b3705 b3708
6822    B       b3709   t3708
6823    NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL
6824    NCzf_itt_pair!pair      pair    pair Czf_itt_pair
6825    O       o3709   pair
6826    T       t3709   o3709 b2509 b2510
6827    B       b3710   t3709
6828    T       t3710   o732 b3710 b886
6829    B       b3711   t3710
6830    T       t3711   o644 b3709 b3711
6831    H       h3711   y_1 t3711
6832    B       b3712   t604 z
6833    T       t3712   o2488 b733 b886 b3712
6834    S       s3712   t726 h h2514 h2515 h2516 h2517 h2518 h3711 h754 h2593 h2595
6835    G       s3712   t3712
6836    B       b3713   s3712
6837    T       t3713   o747 b3713 b2503
6838    B       b3714   t3713
6839    S       s3714   t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
6840    G       s3714   t3712
6841    B       b3715   s3714
6842    T       t3715   o747 b3715 b2503
6843    B       b3716   t3715
6844    T       t3716   o888 b733 b886 b604 b2601
6845    B       b3717   t3716 z
6846    T       t3717   o1427 b733 b886 b3717
6847    S       s3717   t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
6848    G       s3717   t3717
6849    B       b3718   s3717
6850    T       t3718   o747 b3718 b2503
6851    B       b3719   t3718
6852    T       t3719   o2 b2667
6853    B       b3720   t3719
6854    T       t3720   o746 b3719 b780 b3720
6855    B       b3721   t3720
6856    T       t3721   o2 b3721
6857    B       b3722   t3721
6858    T       t3722   o746 b3716 b4 b3722
6859    B       b3723   t3722
6860    T       t3723   o2 b3723
6861    B       b3724   t3723
6862    T       t3724   o746 b3714 b4 b3724
6863    B       b3725   t3724
6864    T       t3725   o b3725 b4
6865    B       b3726   t3725
6866    T       t3726   o745 b2667 b3726
6867    B       b3727   t3726
6868    NSummary!ext_goal       ext_goal        ext_goal Summary
6869    O       o3727   ext_goal
6870    T       t3727   o3727 b3725
6871    B       b3728   t3727
6872    T       t3728   o b3728 b4
6873    B       b3729   t3728
6874    T       t3729   o2679 b744 b3727 b3729 b4
6875    B       b3730   t3729
6876    B       b3731   t2670 z
6877    T       t3731   o2488 b733 b886 b3731
6878    S       s3731   t726 h h2514 h2515 h2516 h2517 h2518 h3711 h754 h2593 h2595
6879    G       s3731   t3731
6880    B       b3732   s3731
6881    T       t3732   o747 b3732 b2503
6882    B       b3733   t3732
6883    S       s3733   t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
6884    G       s3733   t3731
6885    B       b3734   s3733
6886    T       t3734   o747 b3734 b2503
6887    B       b3735   t3734
6888    T       t3735   o746 b2674 b780 b2666
6889    B       b3736   t3735
6890    T       t3736   o2 b3736
6891    B       b3737   t3736
6892    T       t3737   o746 b3735 b4 b3737
6893    B       b3738   t3737
6894    T       t3738   o2 b3738
6895    B       b3739   t3738
6896    T       t3739   o746 b3733 b4 b3739
6897    B       b3740   t3739
6898    T       t3740   o b3740 b4
6899    B       b3741   t3740
6900    T       t3741   o745 b2675 b3741
6901    B       b3742   t3741
6902    T       t3742   o3727 b3740
6903    B       b3743   t3742
6904    T       t3743   o b3743 b4
6905    B       b3744   t3743
6906    T       t3744   o2681 b744 b3742 b3744 b4
6907    B       b3745   t3744
6908    T       t3745   o b3745 b4
6909    B       b3746   t3745
6910    T       t3746   o b2683 b3746
6911    B       b3747   t3746
6912    T       t3747   o b3730 b3747
6913    B       b3748   t3747
6914    T       t3748   o2663 b744 b2679 b3748 b4
6915    B       b3749   t3748
6916    B       b3750   t2655 z
6917    T       t3750   o2488 b733 b886 b3750
6918    S       s3750   t726 h h2514 h2515 h2516 h2517 h2518 h3711 h754 h2593 h2595
6919    G       s3750   t3750
6920    B       b3751   s3750
6921    T       t3751   o747 b3751 b2503
6922    B       b3752   t3751
6923    S       s3752   t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2593 h2595
6924    G       s3752   t3750
6925    B       b3753   s3752
6926    T       t3753   o747 b3753 b2503
6927    B       b3754   t3753
6928    T       t3754   o746 b2659 b780 b2654
6929    B       b3755   t3754
6930    T       t3755   o2 b3755
6931    B       b3756   t3755
6932    T       t3756   o746 b3754 b4 b3756
6933    B       b3757   t3756
6934    T       t3757   o2 b3757
6935    B       b3758   t3757
6936    T       t3758   o746 b3752 b4 b3758
6937    B       b3759   t3758
6938    T       t3759   o b3759 b4
6939    B       b3760   t3759
6940    T       t3760   o745 b2660 b3760
6941    B       b3761   t3760
6942    T       t3761   o3727 b3759
6943    B       b3762   t3761
6944    T       t3762   o b3762 b4
6945    B       b3763   t3762
6946    T       t3763   o2681 b744 b3761 b3763 b4
6947    B       b3764   t3763
6948    T       t3764   o b3764 b4
6949    B       b3765   t3764
6950    T       t3765   o b3749 b3765
6951    B       b3766   t3765
6952    T       t3766   o2650 b744 b2663 b3766 b4
6953    B       b3767   t3766
6954    T       t3767   o b3767 b4
6955    B       b3768   t3767
6956    T       t3768   o805 b744 b2650 b3768 b4
6957    B       b3769   t3768
6958    T       t3769   o603 b587 b588 b2603
6959    B       b3770   t3769 z
6960    T       t3770   o2488 b733 b886 b3770
6961    S       s3770   t726 h h2514 h2515 h2516 h2517 h2518 h3711 h754 h2628 h2629
6962    G       s3770   t3770
6963    B       b3771   s3770
6964    T       t3771   o747 b3771 b2503
6965    B       b3772   t3771
6966    S       s3772   t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
6967    G       s3772   t3770
6968    B       b3773   s3772
6969    T       t3773   o747 b3773 b2503
6970    B       b3774   t3773
6971    B       b3775   t3769
6972    T       t3775   o888 b733 b886 b3775 b2698
6973    B       b3776   t3775 z
6974    T       t3776   o1427 b733 b886 b3776
6975    S       s3776   t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
6976    G       s3776   t3776
6977    B       b3777   s3776
6978    T       t3777   o747 b3777 b2503
6979    B       b3778   t3777
6980    T       t3778   o2 b2709
6981    B       b3779   t3778
6982    T       t3779   o746 b3778 b780 b3779
6983    B       b3780   t3779
6984    T       t3780   o2 b3780
6985    B       b3781   t3780
6986    T       t3781   o746 b3774 b4 b3781
6987    B       b3782   t3781
6988    T       t3782   o2 b3782
6989    B       b3783   t3782
6990    T       t3783   o746 b3772 b4 b3783
6991    B       b3784   t3783
6992    T       t3784   o b3784 b4
6993    B       b3785   t3784
6994    T       t3785   o745 b2709 b3785
6995    B       b3786   t3785
6996    T       t3786   o3727 b3784
6997    B       b3787   t3786
6998    T       t3787   o b3787 b4
6999    B       b3788   t3787
7000    T       t3788   o2679 b744 b3786 b3788 b4
7001    B       b3789   t3788
7002    B       b3790   t2709 z
7003    T       t3790   o2488 b733 b886 b3790
7004    S       s3790   t726 h h2514 h2515 h2516 h2517 h2518 h3711 h754 h2628 h2629
7005    G       s3790   t3790
7006    B       b3791   s3790
7007    T       t3791   o747 b3791 b2503
7008    B       b3792   t3791
7009    S       s3792   t726 h h2514 h2515 h2516 h2517 h2518 h2519 h754 h2628 h2629
7010    G       s3792   t3790
7011    B       b3793   s3792
7012    T       t3793   o747 b3793 b2503
7013    B       b3794   t3793
7014    T       t3794   o746 b2713 b780 b2708
7015    B       b3795   t3794
7016    T       t3795   o2 b3795
7017    B       b3796   t3795
7018    T       t3796   o746 b3794 b4 b3796
7019    B       b3797   t3796
7020    T       t3797   o2 b3797
7021    B       b3798   t3797
7022    T       t3798   o746 b3792 b4 b3798
7023    B       b3799   t3798
7024    T       t3799   o b3799 b4
7025    B       b3800   t3799
7026    T       t3800   o745 b2714 b3800
7027    B       b3801   t3800
7028    T       t3801   o3727 b3799
7029    B       b3802   t3801
7030    T       t3802   o b3802 b4
7031    B       b3803   t3802
7032    T       t3803   o2681 b744 b3801 b3803 b4
7033    B       b3804   t3803
7034    T       t3804   o b3804 b4
7035    B       b3805   t3804
7036    T       t3805   o b3789 b3805
7037    B       b3806   t3805
7038    T       t3806   o2704 b744 b2717 b3806 b4
7039    B       b3807   t3806
7040    T       t3807   o b3807 b4
7041    B       b3808   t3807
7042    T       t3808   o807 b744 b2704 b3808 b4
7043    B       b3809   t3808
7044    T       t3809   o b3809 b4
7045    B       b3810   t3809
7046    T       t3810   o b3769 b3810
7047    B       b3811   t3810
7048    T       t3811   o2593 b744 b2642 b3811 b4
7049    B       b3812   t3811
7050    T       t3812   o b3812 b4
7051    B       b3813   t3812
7052    T       t3813   o3508 b744 b3584 b3698 b3813
7053    B       b3814   t3813
7054    T       t3814   o742 b3814
7055    B       b3815   t3814
7056    T       t3822   o2488 b733 b711 b2740
7057    S       s3822   t726 h
7058    G       s3822   t3822
7059    B       b3822   s3822
7060    T       t3823   o719 b3822
7061    B       b3823   t3823
7062    T       t3824   o718 b817 b3823
7063    B       b3824   t3824
7064    T       t3825   o718 b728 b3824
7065    B       b3825   t3825
7066    T       t3826   o718 b724 b3825
7067    B       b3826   t3826
7068    T       t3827   o b727 b2296
7069    B       b3827   t3827
7070    T       t3828   o b723 b3827
7071    B       b3828   t3828
7072    T       t3829   o747 b3822 b3828
7073    B       b3829   t3829
7074    T       t3830   o746 b3829 b4 b753
7075    B       b3830   t3830
7076    T       t3831   o745 b3830 b4
7077    B       b3831   t3831
7078    T       t3832   o2747 b744 b3831 b4 b4
7079    B       b3832   t3832
7080    T       t3833   o742 b3832
7081    B       b3833   t3833
7082  S       s2327   t721 h  S       s2327   t721 h
7083  G       s2327   t891  G       s2327   t891
7084  B       b2327   s2327  B       b2327   s2327
7085  T       t2327   o719 b2327  T       t2327   o719 b2327
7086  B       b2330   t2327  B       b2330   t2327
7087  T       t2330   o718 b2330 b901  T       t3840   o888 b733 b711 b897 b898
7088  B       b2333   t2330  S       s3840   t726 h
7089  T       t2333   o718 b817 b2333  G       s3840   t3840
7090  B       b2334   t2333  B       b3840   s3840
7091  T       t2334   o718 b890 b2334  T       t3841   o719 b3840
7092  B       b2344   t2334  B       b3841   t3841
7093  T       t2344   o718 b728 b2344  T       t3842   o718 b894 b3841
7094  B       b2345   t2344  B       b3842   t3842
7095  T       t2345   o718 b724 b2345  T       t3843   o718 b2330 b3842
7096  B       b2346   t2345  B       b3843   t3843
7097  T       t2346   o718 b888 b2346  T       t3844   o718 b817 b3843
7098  B       b2348   t2346  B       b3844   t3844
7099  P       p2348   Number 3435  T       t3845   o718 b728 b3844
7100  P       p2349   Number 3443  B       b3845   t3845
7101  O       o2349   resource_defs p2348 p2349 p294  T       t3846   o718 b724 b3845
7102  P       p2350   Number 3441  B       b3846   t3846
7103  O       o2350   uid p2350 p2349  P       p3846   String "genAssumT [3] thenT autoT thenT dT 2 ttca"
7104  T       t2358   o2350 b816  O       o3846   ext_rule p3846
7105  B       b2379   t2358  T       t3847   o b2327 b908
7106  T       t2379   o b2379 b4  B       b3847   t3847
7107  B       b2518   t2379  T       t3848   o b726 b3847
7108  T       t2518   o2349 b2518  B       b3848   t3848
7109  B       b2734   t2518  T       t3849   o b727 b3848
7110  T       t2734   o b2734 b4  B       b3849   t3849
7111  B       b2735   t2734  T       t3850   o b723 b3849
7112  T       t2735   o885 b718 b2348 b1678 b2735  B       b3850   t3850
7113  B       b2736   t2735  T       t3851   o747 b3840 b3850
7114  T       t2736   o2327 b2736  B       b3851   t3851
7115  B       b2737   t2736  T       t3852   o746 b3851 b4 b753
7116  P       p2737   Number 3916  B       b3852   t3852
7117  P       p2738   Number 4387  T       t3853   o888 b733 b711 b919 b920
7118  O       o2738   location p2737 p2738  H       h3853   z t3853
7119  T       t2738   o718 b2330 b1689  T       t3854   o888 b733 b711 b922 b923
7120  B       b2738   t2738  S       s3854   t726 h h754 h757 h3853
7121  T       t2739   o718 b817 b2738  G       s3854   t3854
7122  B       b2739   t2739  B       b3854   s3854
7123  T       t2774   o718 b890 b2739  T       t3855   o747 b3854 b3850
7124  B       b3122   t2774  B       b3855   t3855
7125  T       t3122   o718 b728 b3122  S       s3855   t726 h h770 h754 h757 h3853
7126  B       b3131   t3122  G       s3855   t3854
7127  T       t3131   o718 b724 b3131  B       b3856   s3855
7128  B       b3147   t3131  T       t3856   o747 b3856 b3850
7129  T       t3147   o718 b888 b3147  B       b3857   t3856
7130  B       b3148   t3147  S       s3857   t726 h h770
7131  P       p3148   Number 3947  G       s3857   t3840
7132  P       p3149   Number 3955  B       b3858   s3857
7133  O       o3149   resource_defs p3148 p3149 p294  T       t3858   o747 b3858 b3850
7134  P       p3150   Number 3953  B       b3859   t3858
7135  O       o3150   uid p3150 p3149  B       b3860   t3840 n
7136  T       t3150   o3150 b816  T       t3860   o775 b621 b3860
7137  B       b3150   t3150  S       s3860   t726 h
7138  T       t3151   o b3150 b4  G       s3860   t3860
7139  B       b3151   t3151  B       b3861   s3860
7140  T       t3152   o3149 b3151  T       t3861   o747 b3861 b3850
7141  B       b3152   t3152  B       b3862   t3861
7142  T       t3153   o b3152 b4  T       t3862   o2 b3852
7143  B       b3153   t3153  B       b3863   t3862
7144  T       t3154   o1686 b718 b3148 b2185 b3153  T       t3863   o774 b3862 b780 b3863
7145  B       b3154   t3154  B       b3864   t3863
7146  T       t3155   o2738 b3154  T       t3864   o2 b3864
7147  B       b3155   t3155  B       b3865   t3864
7148  P       p3155   Number 4410  T       t3865   o746 b3859 b4 b3865
7149  P       p3156   Number 4940  B       b3866   t3865
7150  O       o3156   location p3155 p3156  T       t3866   o2 b3866
7151    B       b3867   t3866
7152    T       t3867   o746 b3857 b4 b3867
7153    B       b3868   t3867
7154    T       t3868   o2 b3868
7155    B       b3869   t3868
7156    T       t3869   o746 b3855 b4 b3869
7157    B       b3870   t3869
7158    T       t3870   o888 b733 b711 b943 b944
7159    S       s3870   t726 h
7160    G       s3870   t3870
7161    B       b3871   s3870
7162    T       t3871   o747 b3871 b3850
7163    B       b3872   t3871
7164    S       s3872   t726 h h770
7165    G       s3872   t3870
7166    B       b3873   s3872
7167    T       t3873   o747 b3873 b3850
7168    B       b3874   t3873
7169    T       t3874   o746 b3874 b4 b3867
7170    B       b3875   t3874
7171    T       t3875   o2 b3875
7172    B       b3876   t3875
7173    T       t3876   o746 b3872 b4 b3876
7174    B       b3877   t3876
7175    T       t3877   o888 b733 b711 b954 b955
7176    H       h3877   z t3877
7177    S       s3877   t726 h h754 h791 h3877
7178    G       s3877   t3854
7179    B       b3878   s3877
7180    T       t3878   o747 b3878 b3850
7181    B       b3879   t3878
7182    S       s3879   t726 h h770 h754 h791 h3877
7183    G       s3879   t3854
7184    B       b3880   s3879
7185    T       t3880   o747 b3880 b3850
7186    B       b3881   t3880
7187    T       t3881   o746 b3881 b4 b3867
7188    B       b3882   t3881
7189    T       t3882   o2 b3882
7190    B       b3883   t3882
7191    T       t3883   o746 b3879 b4 b3883
7192    B       b3884   t3883
7193    T       t3884   o b3884 b4
7194    B       b3885   t3884
7195    T       t3885   o b3877 b3885
7196    B       b3886   t3885
7197    T       t3886   o b3870 b3886
7198    B       b3887   t3886
7199    T       t3887   o745 b3852 b3887
7200    B       b3888   t3887
7201    S       s3888   t726 h h754 h757 h3853 h968
7202    G       s3888   t3854
7203    B       b3889   s3888
7204    T       t3889   o747 b3889 b3850
7205    B       b3890   t3889
7206    T       t3890   o2 b3870
7207    B       b3891   t3890
7208    T       t3891   o746 b3890 b4 b3891
7209    B       b3892   t3891
7210    S       s3892   t726 h h754 h757 h3853 h972
7211    G       s3892   t3854
7212    B       b3893   s3892
7213    T       t3893   o747 b3893 b3850
7214    B       b3894   t3893
7215    T       t3894   o746 b3894 b4 b3891
7216    B       b3895   t3894
7217    T       t3895   o b3895 b4
7218    B       b3896   t3895
7219    T       t3896   o b3892 b3896
7220    B       b3897   t3896
7221    T       t3897   o745 b3870 b3897
7222    B       b3898   t3897
7223    T       t3898   o745 b3892 b4
7224    B       b3899   t3898
7225    T       t3899   o978 b744 b3899 b4 b4
7226    B       b3900   t3899
7227    T       t3900   o888 b733 b711 b982 b983
7228    S       s3900   t726 h h754 h757 h3853 h972
7229    G       s3900   t3900
7230    B       b3901   s3900
7231    T       t3901   o747 b3901 b3850
7232    B       b3902   t3901
7233    T       t3902   o888 b733 b711 b991 b994
7234    S       s3902   t726 h h754 h757 h3853 h972
7235    G       s3902   t3902
7236    B       b3903   s3902
7237    T       t3903   o747 b3903 b3850
7238    B       b3904   t3903
7239    T       t3904   o2 b3895
7240    B       b3905   t3904
7241    T       t3905   o746 b3904 b4 b3905
7242    B       b3906   t3905
7243    T       t3906   o2 b3906
7244    B       b3907   t3906
7245    T       t3907   o746 b3902 b4 b3907
7246    B       b3908   t3907
7247    S       s3908   t726 h h754 h757 h3853 h972
7248    G       s3908   t1000
7249    B       b3909   s3908
7250    T       t3909   o747 b3909 b3850
7251    B       b3910   t3909
7252    T       t3910   o774 b3910 b4 b3907
7253    B       b3911   t3910
7254    T       t3911   o b3911 b4
7255    B       b3912   t3911
7256    T       t3912   o b3908 b3912
7257    B       b3913   t3912
7258    T       t3913   o745 b3895 b3913
7259    B       b3914   t3913
7260    P       p3914   String "equivSubstT << equiv{car{'g}; eqG{'g}; op{'g; op{'g; inv{'g; 'x}; power{'g; 'x; (('m +@ 1) +@ 1)}}; inv{'g; 'x}}; op{'g; inv{'g; 'x}; op{'g; power{'g; 'x; (('m +@ 1) +@ 1)}; inv{'g; 'x}}}} >>  0 ttca"
7261    O       o3914   ext_rule p3914
7262    T       t3914   o745 b3908 b4
7263    B       b3915   t3914
7264    T       t3915   o3914 b744 b3915 b4 b4
7265    B       b3916   t3915
7266    S       s3916   t721 h h754 h757 h3853 h972 h1008
7267    G       s3916   t1000
7268    B       b3917   s3916
7269    T       t3917   o747 b3917 b3850
7270    B       b3918   t3917
7271    S       s3918   t721 h h754 h757 h3853 h972 h1008
7272    G       s3918   t1011
7273    B       b3919   s3918
7274    T       t3919   o747 b3919 b3850
7275    B       b3920   t3919
7276    S       s3920   t726 h h754 h757 h3853 h972 h1008
7277    G       s3920   t1000
7278    B       b3921   s3920
7279    T       t3921   o747 b3921 b3850
7280    B       b3922   t3921
7281    T       t3922   o2 b3911
7282    B       b3923   t3922
7283    T       t3923   o746 b3922 b4 b3923
7284    B       b3924   t3923
7285    T       t3924   o2 b3924
7286    B       b3925   t3924
7287    T       t3925   o746 b3920 b4 b3925
7288    B       b3926   t3925
7289    T       t3926   o2 b3926
7290    B       b3927   t3926
7291    T       t3927   o746 b3918 b4 b3927
7292    B       b3928   t3927
7293    S       s3928   t721 h h754 h757 h3853 h972 h1021
7294    G       s3928   t1000
7295    B       b3929   s3928
7296    T       t3929   o747 b3929 b3850
7297    B       b3930   t3929
7298    S       s3930   t721 h h754 h757 h3853 h972 h1021
7299    G       s3930   t1011
7300    B       b3931   s3930
7301    T       t3931   o747 b3931 b3850
7302    B       b3932   t3931
7303    S       s3932   t726 h h754 h757 h3853 h972 h1021
7304    G       s3932   t1000
7305    B       b3933   s3932
7306    T       t3933   o747 b3933 b3850
7307    B       b3934   t3933
7308    T       t3934   o746 b3934 b4 b3923
7309    B       b3935   t3934
7310    T       t3935   o2 b3935
7311    B       b3936   t3935
7312    T       t3936   o746 b3932 b4 b3936
7313    B       b3937   t3936
7314    T       t3937   o2 b3937
7315    B       b3938   t3937
7316    T       t3938   o746 b3930 b4 b3938
7317    B       b3939   t3938
7318    T       t3939   o b3939 b4
7319    B       b3940   t3939
7320    T       t3940   o b3928 b3940
7321    B       b3941   t3940
7322    T       t3941   o745 b3911 b3941
7323    B       b3942   t3941
7324    T       t3942   o745 b3928 b4
7325    B       b3943   t3942
7326    T       t3943   o1035 b744 b3943 b4 b4
7327    B       b3944   t3943
7328    S       s3944   t721 h h754 h757 h3853 h972 h1040
7329    G       s3944   t1041
7330    B       b3945   s3944
7331    T       t3945   o747 b3945 b3850
7332    B       b3946   t3945
7333    S       s3946   t721 h h754 h757 h3853 h972 h1045
7334    G       s3946   t1041
7335    B       b3947   s3946
7336    T       t3947   o747 b3947 b3850
7337    B       b3948   t3947
7338    S       s3948   t721 h h754 h757 h3853 h972 h1051
7339    G       s3948   t1041
7340    B       b3949   s3948
7341    T       t3949   o747 b3949 b3850
7342    B       b3950   t3949
7343    S       s3950   t721 h h754 h757 h3853 h972 h1055
7344    G       s3950   t1041
7345    B       b3951   s3950
7346    T       t3951   o747 b3951 b3850
7347    B       b3952   t3951
7348    S       s3952   t721 h h754 h757 h3853 h972 h1060
7349    G       s3952   t1041
7350    B       b3953   s3952
7351    T       t3953   o747 b3953 b3850
7352    B       b3954   t3953
7353    S       s3954   t721 h h754 h757 h3853 h972 h1064
7354    G       s3954   t1041
7355    B       b3955   s3954
7356    T       t3955   o747 b3955 b3850
7357    B       b3956   t3955
7358    S       s3956   t721 h h754 h757 h3853 h972 h1067
7359    G       s3956   t1041
7360    B       b3957   s3956
7361    T       t3957   o747 b3957 b3850
7362    B       b3958   t3957
7363    S       s3958   t721 h h754 h757 h3853 h972 h1021
7364    G       s3958   t1041
7365    B       b3959   s3958
7366    T       t3959   o747 b3959 b3850
7367    B       b3960   t3959
7368    T       t3960   o2 b3939
7369    B       b3961   t3960
7370    T       t3961   o774 b3960 b4 b3961
7371    B       b3962   t3961
7372    T       t3962   o2 b3962
7373    B       b3963   t3962
7374    T