:: Abstract Reduction Systems and Idea of {K}nuth {B}endix Completion :: Algorithm :: by Grzegorz Bancerek :: :: Received March 31, 2014 :: Copyright (c) 2014-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies RELAT_1, XBOOLE_0, FUNCT_1, REWRITE1, TDGROUP, ABSRED_0, ZFMISC_1, FINSEQ_1, ARYTM_1, SUBSET_1, NUMBERS, STRUCT_0, NAT_1, ARYTM_3, CARD_1, XXREAL_0, ZFREFLE1, TARSKI, UNIALG_1, GROUP_1, MSUALG_6, FUNCT_2, INCPROJ, EQREL_1, MSUALG_1, PARTFUN1, UNIALG_2, FUNCT_4, PBOOLE, FUNCT_7, FINSEQ_2, FUNCOP_1, ORDINAL1, MESFUNC1; notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, RELSET_1, FUNCT_1, SUBSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, EQREL_1, ORDINAL1, BINOP_1, FINSEQ_1, FINSEQ_2, NAT_1, FINSEQ_4, FUNCT_7, MARGREL1, STRUCT_0, PBOOLE, UNIALG_1, PUA2MSS1, REWRITE1; constructors RELAT_1, RELSET_1, FUNCT_2, STRUCT_0, REWRITE1, XCMPLX_0, XXREAL_0, NAT_1, FINSEQ_5, ENUMSET1, BINOP_1, FINSEQ_1, FINSEQ_4, FUNCT_7, CARD_1, XXREAL_1, UNIALG_1, PUA2MSS1, REALSET1, MARGREL1, EQREL_1, NUMBERS, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, PARTFUN1; registrations SUBSET_1, XBOOLE_0, RELSET_1, ORDINAL1, NAT_1, REWRITE1, XXREAL_0, XCMPLX_0, STRUCT_0, AOFA_A00, FUNCT_2, FINSEQ_1, PARTFUN1, FUNCOP_1, FINSEQ_2, CARD_1, MARGREL1, UNIALG_1, PUA2MSS1, RELAT_1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Reduction and Convertibility definition struct(1-sorted) ARS(# carrier -> set, reduction -> Relation of the carrier #); end; registration let A be non empty set, r be Relation of A; cluster ARS(#A, r#) -> non empty; end; registration cluster non empty strict for ARS; end; definition let X be ARS; let x,y be Element of X; pred x ==> y means :: ABSRED_0:def 1 [x,y] in the reduction of X; end; notation let X be ARS; let x,y be Element of X; synonym y <== x for x ==> y; end; definition let X be ARS; let x,y be Element of X; pred x =01=> y means :: ABSRED_0:def 2 x = y or x ==> y; reflexivity; pred x =*=> y means :: ABSRED_0:def 3 the reduction of X reduces x,y; reflexivity; end; reserve X for ARS, a,b,c,u,v,w,x,y,z for Element of X; theorem :: ABSRED_0:1 a ==> b implies X is non empty; theorem :: ABSRED_0:2 x ==> y implies x =*=> y; theorem :: ABSRED_0:3 x =*=> y & y =*=> z implies x =*=> z; scheme :: ABSRED_0:sch 1 Star{X() -> ARS, P[object]}: for x,y being Element of X() st x =*=> y & P[x] holds P[y] provided for x,y being Element of X() st x ==> y & P[x] holds P[y]; scheme :: ABSRED_0:sch 2 Star1{X() -> ARS, P[object], a, b() -> Element of X()}: P[b()] provided a() =*=> b() and P[a()] and for x,y being Element of X() st x ==> y & P[x] holds P[y]; scheme :: ABSRED_0:sch 3 StarBack{X() -> ARS, P[object]}: for x,y being Element of X() st x =*=> y & P[y] holds P[x] provided for x,y being Element of X() st x ==> y & P[y] holds P[x]; scheme :: ABSRED_0:sch 4 StarBack1{X() -> ARS, P[object], a, b() -> Element of X()}: P[a()] provided a() =*=> b() and P[b()] and for x,y being Element of X() st x ==> y & P[y] holds P[x]; definition let X be ARS; let x,y be Element of X; pred x =+=> y means :: ABSRED_0:def 4 ex z being Element of X st x ==> z & z =*=> y; end; theorem :: ABSRED_0:4 x =+=> y iff ex z st x =*=> z & z ==> y; notation let X,x,y; synonym y <=01= x for x =01=> y; synonym y <=*= x for x =*=> y; synonym y <=+= x for x =+=> y; end; :: x ==> y implies x =+=> y; :: x =+=> y implies x =*=> y; :: x =+=> y & y =*=> z implies x =+=> z; :: x =*=> y & y =+=> z implies x =+=> z; definition let X,x,y; pred x <==> y means :: ABSRED_0:def 5 x ==> y or x <== y; symmetry; end; theorem :: ABSRED_0:5 x <==> y iff [x,y] in (the reduction of X)\/(the reduction of X)~; definition let X,x,y; pred x <=01=> y means :: ABSRED_0:def 6 x = y or x <==> y; reflexivity; symmetry; pred x <=*=> y means :: ABSRED_0:def 7 x,y are_convertible_wrt the reduction of X; reflexivity; symmetry; end; theorem :: ABSRED_0:6 x <==> y implies x <=*=> y; theorem :: ABSRED_0:7 x <=*=> y & y <=*=> z implies x <=*=> z; scheme :: ABSRED_0:sch 5 Star2{X() -> ARS, P[object]}: for x,y being Element of X() st x <=*=> y & P[x] holds P[y] provided for x,y being Element of X() st x <==> y & P[x] holds P[y]; scheme :: ABSRED_0:sch 6 Star2A{X() -> ARS, P[object], a, b() -> Element of X()}: P[b()] provided a() <=*=> b() and P[a()] and for x,y being Element of X() st x <==> y & P[x] holds P[y]; definition let X,x,y; pred x <=+=> y means :: ABSRED_0:def 8 ex z st x <==> z & z <=*=> y; symmetry; end; theorem :: ABSRED_0:8 x <=+=> y iff ex z st x <=*=> z & z <==> y; theorem :: ABSRED_0:9 x =01=> y implies x =*=> y; theorem :: ABSRED_0:10 x =+=> y implies x =*=> y; theorem :: ABSRED_0:11 x ==> y implies x =+=> y; theorem :: ABSRED_0:12 x ==> y & y ==> z implies x =*=> z; theorem :: ABSRED_0:13 x ==> y & y =01=> z implies x =*=> z; theorem :: ABSRED_0:14 x ==> y & y =*=> z implies x =*=> z; theorem :: ABSRED_0:15 x ==> y & y =+=> z implies x =*=> z; theorem :: ABSRED_0:16 x =01=> y & y ==> z implies x =*=> z; theorem :: ABSRED_0:17 x =01=> y & y =01=> z implies x =*=> z; theorem :: ABSRED_0:18 x =01=> y & y =*=> z implies x =*=> z; theorem :: ABSRED_0:19 x =01=> y & y =+=> z implies x =*=> z; theorem :: ABSRED_0:20 x =*=> y & y ==> z implies x =*=> z; theorem :: ABSRED_0:21 x =*=> y & y =01=> z implies x =*=> z; theorem :: ABSRED_0:22 x =*=> y & y =+=> z implies x =*=> z; theorem :: ABSRED_0:23 x =+=> y & y ==> z implies x =*=> z; theorem :: ABSRED_0:24 x =+=> y & y =01=> z implies x =*=> z; theorem :: ABSRED_0:25 x =+=> y & y =+=> z implies x =*=> z; theorem :: ABSRED_0:26 x ==> y & y ==> z implies x =+=> z; theorem :: ABSRED_0:27 x ==> y & y =01=> z implies x =+=> z; theorem :: ABSRED_0:28 x ==> y & y =+=> z implies x =+=> z; theorem :: ABSRED_0:29 x =01=> y & y ==> z implies x =+=> z; theorem :: ABSRED_0:30 x =01=> y & y =+=> z implies x =+=> z; theorem :: ABSRED_0:31 x =*=> y & y =+=> z implies x =+=> z; theorem :: ABSRED_0:32 x =+=> y & y ==> z implies x =+=> z; theorem :: ABSRED_0:33 x =+=> y & y =01=> z implies x =+=> z; theorem :: ABSRED_0:34 x =+=> y & y =*=> z implies x =+=> z; theorem :: ABSRED_0:35 x =+=> y & y =+=> z implies x =+=> z; theorem :: ABSRED_0:36 x <=01=> y implies x <=*=> y; theorem :: ABSRED_0:37 x <=+=> y implies x <=*=> y; theorem :: ABSRED_0:38 x <==> y implies x <=+=> y; theorem :: ABSRED_0:39 x <==> y & y <==> z implies x <=*=> z; theorem :: ABSRED_0:40 x <==> y & y <=01=> z implies x <=*=> z; theorem :: ABSRED_0:41 x <=01=> y & y <==> z implies x <=*=> z; theorem :: ABSRED_0:42 x <==> y & y <=*=> z implies x <=*=> z; theorem :: ABSRED_0:43 x <=*=> y & y <==> z implies x <=*=> z; theorem :: ABSRED_0:44 x <==> y & y <=+=> z implies x <=*=> z; theorem :: ABSRED_0:45 x <=+=> y & y <==> z implies x <=*=> z; theorem :: ABSRED_0:46 x <=01=> y & y <=01=> z implies x <=*=> z; theorem :: ABSRED_0:47 x <=01=> y & y <=*=> z implies x <=*=> z; theorem :: ABSRED_0:48 x <=*=> y & y <=01=> z implies x <=*=> z; theorem :: ABSRED_0:49 x <=01=> y & y <=+=> z implies x <=*=> z; theorem :: ABSRED_0:50 x <=+=> y & y <=01=> z implies x <=*=> z; theorem :: ABSRED_0:51 x <=*=> y & y <=+=> z implies x <=*=> z; theorem :: ABSRED_0:52 x <=+=> y & y <=+=> z implies x <=*=> z; theorem :: ABSRED_0:53 x <==> y & y <==> z implies x <=+=> z; theorem :: ABSRED_0:54 x <==> y & y <=01=> z implies x <=+=> z; theorem :: ABSRED_0:55 x <==> y & y <=+=> z implies x <=+=> z; theorem :: ABSRED_0:56 x <=01=> y & y <=+=> z implies x <=+=> z; theorem :: ABSRED_0:57 x <=*=> y & y <=+=> z implies x <=+=> z; theorem :: ABSRED_0:58 x <=+=> y & y <=+=> z implies x <=+=> z; theorem :: ABSRED_0:59 x <=01=> y implies x <== y or x = y or x ==> y; theorem :: ABSRED_0:60 x <== y or x = y or x ==> y implies x <=01=> y; theorem :: ABSRED_0:61 x <=01=> y implies x <=01= y or x ==> y; theorem :: ABSRED_0:62 x <=01= y or x ==> y implies x <=01=> y; theorem :: ABSRED_0:63 x <=01=> y implies x <=01= y or x =+=> y; theorem :: ABSRED_0:64 x <=01=> y implies x <=01= y or x <==> y; theorem :: ABSRED_0:65 x <=01= y or x <==> y implies x <=01=> y; theorem :: ABSRED_0:66 x <=*=> y & y ==> z implies x <=+=> z; theorem :: ABSRED_0:67 x <=+=> y & y ==> z implies x <=+=> z; theorem :: ABSRED_0:68 x <=01=> y implies x <=01= y or x ==> y; theorem :: ABSRED_0:69 x <=01=> y implies x <=01= y or x =+=> y; theorem :: ABSRED_0:70 x <=01= y or x ==> y implies x <=01=> y; theorem :: ABSRED_0:71 x <=01= y or x <==> y implies x <=01=> y; theorem :: ABSRED_0:72 x <=01=> y implies x <=01= y or x <==> y; theorem :: ABSRED_0:73 x <=+=> y & y ==> z implies x <=+=> z; theorem :: ABSRED_0:74 x <=*=> y & y ==> z implies x <=+=> z; theorem :: ABSRED_0:75 x <=01=> y & y ==> z implies x <=+=> z; theorem :: ABSRED_0:76 x <=+=> y & y =01=> z implies x <=+=> z; theorem :: ABSRED_0:77 x <==> y & y =01=> z implies x <=+=> z; theorem :: ABSRED_0:78 x ==> y & y ==> z & z ==> u implies x =+=> u; theorem :: ABSRED_0:79 x ==> y & y =01=> z & z ==> u implies x =+=> u; theorem :: ABSRED_0:80 x ==> y & y =*=> z & z ==> u implies x =+=> u; theorem :: ABSRED_0:81 x ==> y & y =+=> z & z ==> u implies x =+=> u; theorem :: ABSRED_0:82 x =*=> y implies x <=*=> y; theorem :: ABSRED_0:83 for z st for x,y st x ==> z & x ==> y holds y ==> z for x,y st x ==> z & x =*=> y holds y ==> z; theorem :: ABSRED_0:84 (for x,y st x ==> y holds y ==> x) implies for x,y st x <=*=> y holds x =*=> y; theorem :: ABSRED_0:85 x =*=> y implies x = y or x =+=> y; theorem :: ABSRED_0:86 (for x,y,z st x ==> y & y ==> z holds x ==> z) implies for x,y st x =+=> y holds x ==> y; begin :: Examples of ARS scheme :: ABSRED_0:sch 7 ARSex{A() -> non empty set, R[object,object]}: ex X being strict non empty ARS st the carrier of X = A() & for x,y being Element of X holds x ==> y iff R[x,y]; definition func ARS_01 -> strict ARS means :: ABSRED_0:def 9 the carrier of it = {0,1} & the reduction of it = [:{0},{0,1}:]; func ARS_02 -> strict ARS means :: ABSRED_0:def 10 the carrier of it = {0,1,2} & the reduction of it = [:{0},{0,1,2}:]; end; registration cluster ARS_01 -> non empty; cluster ARS_02 -> non empty; end; reserve i,j,k for Element of ARS_01; theorem :: ABSRED_0:87 for s being set holds s is Element of ARS_01 iff s = 0 or s = 1; theorem :: ABSRED_0:88 i ==> j iff i = 0; reserve l,m,n for Element of ARS_02; theorem :: ABSRED_0:89 for s being set holds s is Element of ARS_02 iff s = 0 or s = 1 or s = 2; theorem :: ABSRED_0:90 m ==> n iff m = 0; begin :: Normal Forms definition let X,x; attr x is normform means :: ABSRED_0:def 11 not ex y st x ==> y; end; theorem :: ABSRED_0:91 x is normform iff x is_a_normal_form_wrt the reduction of X; definition let X,x,y; pred x is_normform_of y means :: ABSRED_0:def 12 x is normform & y =*=> x; end; theorem :: ABSRED_0:92 x is_normform_of y iff x is_a_normal_form_of y, the reduction of X; definition let X,x; attr x is normalizable means :: ABSRED_0:def 13 ex y st y is_normform_of x; end; theorem :: ABSRED_0:93 x is normalizable iff x has_a_normal_form_wrt the reduction of X; definition let X; attr X is WN means :: ABSRED_0:def 14 for x holds x is normalizable; attr X is SN means :: ABSRED_0:def 15 for f being Function of NAT, the carrier of X ex i being Nat st not f.i ==> f.(i+1); attr X is UN* means :: ABSRED_0:def 16 for x,y,z st y is_normform_of x & z is_normform_of x holds y = z; attr X is UN means :: ABSRED_0:def 17 for x,y st x is normform & y is normform & x <=*=> y holds x = y; attr X is N.F. means :: ABSRED_0:def 18 for x,y st x is normform & x <=*=> y holds y =*=> x; end; theorem :: ABSRED_0:94 X is WN iff the reduction of X is weakly-normalizing; theorem :: ABSRED_0:95 X is SN implies the reduction of X is strongly-normalizing; theorem :: ABSRED_0:96 X is non empty & the reduction of X is strongly-normalizing implies X is SN; reserve A for set; theorem :: ABSRED_0:97 for X holds X is SN iff not ex A,z st z in A & for x st x in A ex y st y in A & x ==> y; scheme :: ABSRED_0:sch 8 notSN{X() -> ARS, P[object]}: X() is not SN provided ex x being Element of X() st P[x] and for x being Element of X() st P[x] ex y being Element of X() st P[y] & x ==> y; theorem :: ABSRED_0:98 X is UN iff the reduction of X is with_UN_property; theorem :: ABSRED_0:99 X is N.F. iff the reduction of X is with_NF_property; definition let X; let x such that ex y st y is_normform_of x and for y,z st y is_normform_of x & z is_normform_of x holds y = z; func nf x -> Element of X means :: ABSRED_0:def 19 it is_normform_of x; end; theorem :: ABSRED_0:100 (ex y st y is_normform_of x) & (for y,z st y is_normform_of x & z is_normform_of x holds y = z) implies nf x = nf(x, the reduction of X); theorem :: ABSRED_0:101 x is normform & x =*=> y implies x = y; theorem :: ABSRED_0:102 x is normform implies x is_normform_of x; theorem :: ABSRED_0:103 x is normform & y ==> x implies x is_normform_of y; theorem :: ABSRED_0:104 x is normform & y =01=> x implies x is_normform_of y; theorem :: ABSRED_0:105 x is normform & y =+=> x implies x is_normform_of y; theorem :: ABSRED_0:106 x is_normform_of y & y is_normform_of x implies x = y; theorem :: ABSRED_0:107 x is_normform_of y & z ==> y implies x is_normform_of z; theorem :: ABSRED_0:108 x is_normform_of y & z =*=> y implies x is_normform_of z; theorem :: ABSRED_0:109 x is_normform_of y & z =*=> x implies x is_normform_of z; registration let X; cluster normform -> normalizable for Element of X; end; theorem :: ABSRED_0:110 x is normalizable & y ==> x implies y is normalizable; theorem :: ABSRED_0:111 X is WN iff for x ex y st y is_normform_of x; theorem :: ABSRED_0:112 (for x holds x is normform) implies X is WN; registration cluster SN -> WN for ARS; end; theorem :: ABSRED_0:113 x <> y & (for a,b holds a ==> b iff a = x) implies y is normform & x is normalizable; theorem :: ABSRED_0:114 ex X st X is WN & X is not SN; registration cluster N.F. -> UN* for ARS; cluster N.F. -> UN for ARS; cluster UN -> UN* for ARS; end; theorem :: ABSRED_0:115 X is WN UN* & x is normform & x <=*=> y implies y =*=> x; registration cluster WN UN* -> N.F. for ARS; cluster WN UN* -> UN for ARS; end; theorem :: ABSRED_0:116 y is_normform_of x & z is_normform_of x & y <> z implies x =+=> y; theorem :: ABSRED_0:117 X is WN UN* implies nf x is_normform_of x; theorem :: ABSRED_0:118 X is WN UN* & y is_normform_of x implies y = nf x; theorem :: ABSRED_0:119 X is WN UN* implies nf x is normform; theorem :: ABSRED_0:120 X is WN UN* implies nf nf x = nf x; theorem :: ABSRED_0:121 X is WN UN* & x =*=> y implies nf x = nf y; theorem :: ABSRED_0:122 X is WN UN* & x <=*=> y implies nf x = nf y; theorem :: ABSRED_0:123 X is WN UN* & nf x = nf y implies x <=*=> y; begin :: Divergence and Convergence definition let X,x,y; pred x <<>> y means :: ABSRED_0:def 20 ex z st x <=*= z & z =*=> y; symmetry; reflexivity; pred x >><< y means :: ABSRED_0:def 21 ex z st x =*=> z & z <=*= y; symmetry; reflexivity; pred x <<01>> y means :: ABSRED_0:def 22 ex z st x <=01= z & z =01=> y; symmetry; reflexivity; pred x >>01<< y means :: ABSRED_0:def 23 ex z st x =01=> z & z <=01= y; symmetry; reflexivity; end; theorem :: ABSRED_0:124 x <<>> y iff x,y are_divergent_wrt the reduction of X; theorem :: ABSRED_0:125 x >><< y iff x,y are_convergent_wrt the reduction of X; theorem :: ABSRED_0:126 x <<01>> y iff x,y are_divergent<=1_wrt the reduction of X; theorem :: ABSRED_0:127 x >>01<< y iff x,y are_convergent<=1_wrt the reduction of X; definition let X; attr X is DIAMOND means :: ABSRED_0:def 24 x <<01>> y implies x >>01<< y; attr X is CONF means :: ABSRED_0:def 25 x <<>> y implies x >><< y; attr X is CR means :: ABSRED_0:def 26 x <=*=> y implies x >><< y; attr X is WCR means :: ABSRED_0:def 27 x <<01>> y implies x >><< y; end; definition let X; attr X is COMP means :: ABSRED_0:def 28 X is SN CONF; end; scheme :: ABSRED_0:sch 9 isCR{X() -> non empty ARS, F(Element of X()) -> Element of X()}: X() is CR provided for x being Element of X() holds x =*=> F(x) and for x,y being Element of X() st x <=*=> y holds F(x) = F(y); scheme :: ABSRED_0:sch 10 isCOMP{X() -> non empty ARS, F(Element of X()) -> Element of X()}: X() is COMP provided X() is SN and for x being Element of X() holds x =*=> F(x) and for x,y being Element of X() st x <=*=> y holds F(x) = F(y); theorem :: ABSRED_0:128 x <<01>> y implies x <<>> y; theorem :: ABSRED_0:129 x >>01<< y implies x >><< y; theorem :: ABSRED_0:130 x ==> y implies x <<01>> y; theorem :: ABSRED_0:131 x ==> y implies x >>01<< y; theorem :: ABSRED_0:132 x =01=> y implies x <<01>> y; theorem :: ABSRED_0:133 x =01=> y implies x >>01<< y; theorem :: ABSRED_0:134 x <==> y implies x <<01>> y; theorem :: ABSRED_0:135 x <==> y implies x >>01<< y; theorem :: ABSRED_0:136 x <=01=> y implies x <<01>> y; theorem :: ABSRED_0:137 x <=01=> y implies x >>01<< y; theorem :: ABSRED_0:138 x ==> y implies x >><< y; theorem :: ABSRED_0:139 x =*=> y implies x >><< y; theorem :: ABSRED_0:140 x =*=> y implies x <<>> y; theorem :: ABSRED_0:141 x =+=> y implies x >><< y; theorem :: ABSRED_0:142 x =+=> y implies x <<>> y; theorem :: ABSRED_0:143 x ==> y & x ==> z implies y <<01>> z; theorem :: ABSRED_0:144 x ==> y & z ==> y implies x >>01<< z; theorem :: ABSRED_0:145 x >><< z & z <== y implies x >><< y; theorem :: ABSRED_0:146 x >><< z & z <=01= y implies x >><< y; theorem :: ABSRED_0:147 x >><< z & z <=*= y implies x >><< y; theorem :: ABSRED_0:148 x <<>> y implies x <=*=> y; theorem :: ABSRED_0:149 x >><< y implies x <=*=> y; begin :: Church-Rosser Property theorem :: ABSRED_0:150 X is DIAMOND iff the reduction of X is subcommutative; theorem :: ABSRED_0:151 X is CONF iff the reduction of X is confluent; theorem :: ABSRED_0:152 X is CR iff the reduction of X is with_Church-Rosser_property; theorem :: ABSRED_0:153 X is WCR iff the reduction of X is locally-confluent; theorem :: ABSRED_0:154 for X being non empty ARS holds X is COMP iff the reduction of X is complete; theorem :: ABSRED_0:155 X is DIAMOND & x <=*= z & z =01=> y implies ex u st x =01=> u & u <=*= y; theorem :: ABSRED_0:156 X is DIAMOND & x <=01= y & y =*=> z implies ex u st x =*=> u & u <=01= z; registration cluster DIAMOND -> CONF for ARS; end; registration cluster DIAMOND -> CR for ARS; end; registration cluster CR -> WCR for ARS; end; registration cluster CR -> CONF for ARS; end; registration cluster CONF -> CR for ARS; end; theorem :: ABSRED_0:157 X is non CONF WN implies ex x,y,z st y is_normform_of x & z is_normform_of x & y <> z; registration ::$N Newman's lemma cluster SN WCR -> CR for ARS; end; registration cluster CR -> N.F. for ARS; end; registration cluster WN UN -> CR for ARS; end; registration cluster SN CR -> COMP for ARS; cluster COMP -> CR WCR N.F. UN UN* WN for ARS; end; theorem :: ABSRED_0:158 X is COMP implies for x,y st x <=*=> y holds nf x = nf y; registration cluster WN UN* -> CR for ARS; cluster SN UN* -> COMP for ARS; end; begin :: Term Rewriting Systems definition struct(ARS,UAStr) TRSStr (# carrier -> set, charact -> PFuncFinSequence of the carrier, reduction -> Relation of the carrier #); end; registration cluster non empty non-empty strict for TRSStr; end; definition let S be non empty UAStr; attr S is Group-like means :: ABSRED_0:def 29 Seg 3 c= dom the charact of S & for f being non empty homogeneous PartFunc of (the carrier of S)*, the carrier of S holds (f = (the charact of S).1 implies arity f = 0) & (f = (the charact of S).2 implies arity f = 1) & (f = (the charact of S).3 implies arity f = 2); end; theorem :: ABSRED_0:159 for X being non empty set for f1,f2,f3 being non empty homogeneous PartFunc of X*, X st arity f1 = 0 & arity f2 = 1 & arity f3 = 2 for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> c= the charact of S holds S is Group-like; theorem :: ABSRED_0:160 for X being non empty set for f1,f2,f3 being non empty quasi_total homogeneous PartFunc of X*, X for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> = the charact of S holds S is quasi_total partial; definition let S be non empty non-empty UAStr; let o be operation of S; let a be Element of dom o; redefine func o.a -> Element of S; end; registration let S be non empty non-empty UAStr; cluster -> non empty for operation of S; let o be operation of S; cluster -> Relation-like Function-like for Element of dom o; end; registration let S be partial non empty non-empty UAStr; cluster -> homogeneous for operation of S; end; registration let S be quasi_total non empty non-empty UAStr; cluster -> quasi_total for operation of S; end; theorem :: ABSRED_0:161 for S being non empty non-empty UAStr st S is Group-like holds 1 is OperSymbol of S & 2 is OperSymbol of S & 3 is OperSymbol of S; theorem :: ABSRED_0:162 for S being partial non empty non-empty UAStr st S is Group-like holds arity Den(In(1, dom the charact of S), S) = 0 & arity Den(In(2, dom the charact of S), S) = 1 & arity Den(In(3, dom the charact of S), S) = 2; definition let S be non empty non-empty TRSStr; attr S is invariant means :: ABSRED_0:def 30 for o being OperSymbol of S for a,b being Element of dom Den(o,S) for i being Nat st i in dom a for x,y being Element of S st x = a.i & b = a+*(i,y) & x ==> y holds Den(o,S).a ==> Den(o,S).b; end; definition let S be non empty non-empty TRSStr; attr S is compatible means :: ABSRED_0:def 31 for o being OperSymbol of S for a,b being Element of dom Den(o,S) st for i being Nat st i in dom a holds for x,y being Element of S st x = a.i & y = b.i holds x ==> y holds Den(o,S).a =*=> Den(o,S).b; end; theorem :: ABSRED_0:163 for n being natural number, X being non empty set, x being Element of X ex f being non empty homogeneous quasi_total PartFunc of X*, X st arity f = n & f = (n-tuples_on X) --> x; registration let X be non empty set; let O be PFuncFinSequence of X; let r be Relation of X; cluster TRSStr(#X, O, r#) -> non empty; end; registration let X be non empty set; let O be non empty non-empty PFuncFinSequence of X; let r be Relation of X; cluster TRSStr(#X, O, r#) -> non-empty; end; definition let X be non empty set; let x be Element of X; func TotalTRS(X,x) -> non empty non-empty strict TRSStr means :: ABSRED_0:def 32 the carrier of it = X & the charact of it = <*(0-tuples_on X)-->x, (1-tuples_on X)-->x, (2-tuples_on X)-->x*> & the reduction of it = nabla X; end; registration let X be non empty set; let x be Element of X; cluster TotalTRS(X,x) -> quasi_total partial Group-like invariant; end; registration cluster strict quasi_total partial Group-like invariant for non empty non-empty TRSStr; end; definition let S be Group-like quasi_total partial non empty non-empty TRSStr; func 1.S -> Element of S equals :: ABSRED_0:def 33 Den(In(1,dom the charact of S), S).{}; let a be Element of S; func a " -> Element of S equals :: ABSRED_0:def 34 Den(In(2,dom the charact of S), S).<*a*>; let b be Element of S; func a * b -> Element of S equals :: ABSRED_0:def 35 Den(In(3,dom the charact of S), S).<*a,b*>; end; reserve S for Group-like quasi_total partial invariant non empty non-empty TRSStr; reserve a,b,c for Element of S; theorem :: ABSRED_0:164 a ==> b implies a" ==> b"; theorem :: ABSRED_0:165 a ==> b implies a*c ==> b*c; theorem :: ABSRED_0:166 a ==> b implies c*a ==> c*b; begin :: An Execution of Knuth-Bendix Algorithm reserve S for Group-like quasi_total partial non empty non-empty TRSStr; reserve a,b,c for Element of S; definition let S; attr S is (R1) means :: ABSRED_0:def 36 1.S * a ==> a; attr S is (R2) means :: ABSRED_0:def 37 a" * a ==> 1.S; attr S is (R3) means :: ABSRED_0:def 38 (a * b) * c ==> a * (b * c); attr S is (R4) means :: ABSRED_0:def 39 a" * (a * b) ==> b; attr S is (R5) means :: ABSRED_0:def 40 (1.S)" * a ==> a; attr S is (R6) means :: ABSRED_0:def 41 (a")" * 1.S ==> a; attr S is (R7) means :: ABSRED_0:def 42 (a")" * b ==> a * b; attr S is (R8) means :: ABSRED_0:def 43 a * 1.S ==> a; attr S is (R9) means :: ABSRED_0:def 44 (a")" ==> a; attr S is (R10) means :: ABSRED_0:def 45 (1.S)" ==> 1.S; attr S is (R11) means :: ABSRED_0:def 46 a * (a") ==> 1.S; attr S is (R12) means :: ABSRED_0:def 47 a * (a" * b) ==> b; attr S is (R13) means :: ABSRED_0:def 48 a * (b * (a * b)") ==> 1.S; attr S is (R14) means :: ABSRED_0:def 49 a * (b * a)" ==> b"; attr S is (R15) means :: ABSRED_0:def 50 (a * b)" ==> b" * a"; end; reserve S for Group-like quasi_total partial invariant non empty non-empty TRSStr, a,b,c for Element of S; theorem :: ABSRED_0:167 S is (R1) (R2) (R3) implies a" * (a * b) <<>> b; theorem :: ABSRED_0:168 S is (R1) (R4) implies (1.S)" * a <<>> a; theorem :: ABSRED_0:169 S is (R2) (R4) implies (a")" * 1.S <<>> a; theorem :: ABSRED_0:170 S is (R1) (R3) (R6) implies (a")" * b <<>> a * b; theorem :: ABSRED_0:171 S is (R6) (R7) implies a * 1.S <<>> a; theorem :: ABSRED_0:172 S is (R6) (R8) implies (a")" <<>> a; theorem :: ABSRED_0:173 S is (R5) (R8) implies (1.S)" <<>> 1.S; theorem :: ABSRED_0:174 S is (R2) (R9) implies a * (a") <<>> 1.S; theorem :: ABSRED_0:175 S is (R1) (R3) (R11) implies a * (a" * b) <<>> b; theorem :: ABSRED_0:176 S is (R3) (R11) implies a * (b * (a * b)") <<>> 1.S; theorem :: ABSRED_0:177 S is (R4) (R8) (R13) implies a * (b * a)" <<>> b"; theorem :: ABSRED_0:178 S is (R4) (R14) implies (a * b)" <<>> b" * a"; theorem :: ABSRED_0:179 S is (R1) (R10) implies (1.S)" * a =*=> a; theorem :: ABSRED_0:180 S is (R8) (R9) implies (a")" * 1.S =*=> a; theorem :: ABSRED_0:181 S is (R9) implies (a")" * b =*=> a * b; theorem :: ABSRED_0:182 S is (R11) (R14) implies a * (b * (a * b)") =*=> 1.S; theorem :: ABSRED_0:183 S is (R12) (R15) implies a * (b * a)" =*=> b";