:: 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";