:: Reduction Relations
:: by Grzegorz Bancerek
::
:: Received November 14, 1995
:: Copyright (c) 1995-2026 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 NUMBERS, FINSEQ_1, ORDINAL4, XBOOLE_0, SUBSET_1, ARYTM_3,
RELAT_1, XXREAL_0, CARD_1, NAT_1, FUNCT_1, FINSEQ_5, ARYTM_1, TARSKI,
WELLORD1, PBOOLE, RELAT_2, FUNCOP_1, EQREL_1, REWRITE1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
NAT_1, FUNCT_1, RELAT_1, RELAT_2, WELLORD1, EQREL_1, FINSEQ_1, FUNCOP_1,
PBOOLE, FINSEQ_5;
constructors SETFAM_1, WELLORD1, XXREAL_0, XREAL_0, NAT_1, EQREL_1, PBOOLE,
FINSEQ_5, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, NAT_1, XXREAL_0,
XREAL_0, FINSEQ_1, CARD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_1, RELAT_2, WELLORD1;
equalities RELAT_1;
expansions TARSKI, RELAT_2, WELLORD1;
theorems TARSKI, NAT_1, WELLORD1, RELAT_1, RELAT_2, FUNCT_1, FUNCOP_1,
FINSEQ_1, FINSEQ_5, EQREL_1, WELLORD2, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, ORDINAL1, CARD_1, PARTFUN1, XTUPLE_0;
schemes NAT_1, RELAT_1, EQREL_1, TREES_2;
begin :: Forgetting concatenation and reduction sequence
definition
let p,q be FinSequence;
func p$^q -> FinSequence means :Def1:
it = p^q if p = {} or q = {} otherwise
ex i being Nat, r being FinSequence st len p = i+1 & r = p|Seg i &
it = r^q;
existence
proof
thus p = {} or q = {} implies ex r being FinSequence st r = p^q;
assume that
A1: p <> {} and
q <> {};
len p >= 0+1 by A1,NAT_1:13;
then consider i being Nat such that
A2: len p = 1+i by NAT_1:10;
reconsider i as Nat;
reconsider r = p|Seg i as FinSequence by FINSEQ_1:15;
take r^q, i, r;
thus thesis by A2;
end;
uniqueness;
consistency;
end;
Lm1: now
let p be FinSequence, x be Nat;
assume x in dom p;
then
A1: x in Seg len p by FINSEQ_1:def 3;
hence x <= len p & x >= 0+1 by FINSEQ_1:1;
thus x > 0 by A1,FINSEQ_1:1;
end;
Lm2: now
let p be FinSequence, x be Nat;
assume x+1 in dom p;
then x+1 <= len p by Lm1;
hence x < len p by NAT_1:13;
end;
Lm3: now
let p be FinSequence, x be Nat;
assume that
A1: x <= len p or x < len p and
A2: x >= 1 or x > 0;
x >= 0+1 by A2,NAT_1:13;
then x in Seg len p by A1,FINSEQ_1:1;
hence x in dom p by FINSEQ_1:def 3;
end;
Lm4: now
let p be FinSequence, x be Nat;
assume x < len p;
then x+1 <= len p by NAT_1:13;
hence x+1 in dom p by Lm3;
end;
reserve p,q,r for FinSequence,
x,y for object;
theorem
{}$^p = p & p$^{} = p
proof
{}^p = p & p^{} = p by FINSEQ_1:34;
hence thesis by Def1;
end;
theorem Th2:
q <> {} implies (p^<*x*>)$^q = p^q
proof
len <*x*> = 1 by FINSEQ_1:40;
then
A1: len (p^<*x*>) = len p + 1 by FINSEQ_1:22;
assume q <> {};
then consider i being Nat, r being FinSequence such that
A2: len (p^<*x*>) = i+1 and
A3: r = (p^<*x*>)|Seg i and
A4: (p^<*x*>)$^q = r^q by Def1;
i <= i+1 by NAT_1:11;
then
A5: len r = i by A2,A3,FINSEQ_1:17;
ex s being FinSequence st p^<*x*> = r^s by A3,FINSEQ_1:80;
then consider t being FinSequence such that
A6: p^t = r by A2,A1,A5,FINSEQ_1:47;
len r + 0 = len p + len t by A6,FINSEQ_1:22;
then t = {} by A2,A1,A5;
hence thesis by A4,A6,FINSEQ_1:34;
end;
theorem
(p^<*x*>)$^(<*y*>^q) = p^<*y*>^q
proof
p^<*y*>^q = p^(<*y*>^q) by FINSEQ_1:32;
hence thesis by Th2;
end;
theorem
q <> {} implies <*x*>$^q = q
proof
{}^<*x*> = <*x*> & {}^q = q by FINSEQ_1:34;
hence thesis by Th2;
end;
theorem
p <> {} implies ex x,q st p = <*x*>^q & len p = len q+1
proof
defpred P[Nat] means for p st p <> {} & len p = $1 ex x,q st p =
<*x*>^q & len p = len q+1;
assume
A1: p <> {};
now
let i be Nat;
assume
A2: for p st p <> {} & len p = i ex x,q st p = <*x*>^q & len p = len q +1;
let p;
assume that
A3: p <> {} and
A4: len p = i+1;
consider q be FinSequence,y being object such that
A5: p = q^<*y*> by A3,FINSEQ_1:46;
A6: len p = len q+len <*y*> by A5,FINSEQ_1:22;
A7: len <*y*> = 1 by FINSEQ_1:39;
per cases;
suppose
A8: q = {};
then p = <*y*> by A5,FINSEQ_1:34
.= <*y*>^{} by FINSEQ_1:34;
hence ex x,q st p = <*x*>^q & len p = len q+1 by A7,A6,A8;
end;
suppose
q <> {};
then consider x,r such that
A9: q = <*x*>^r and
A10: len q = len r+1 by A2,A4,A7,A6;
A11: len (r^<*y*>) = len r+1 by A7,FINSEQ_1:22;
p = <*x*>^(r^<*y*>) by A5,A9,FINSEQ_1:32;
hence ex x,q st p = <*x*>^q & len p = len q+1 by A7,A6,A10,A11;
end;
end;
then
A12: for i be Nat st P[i] holds P[i+1];
A13: P[ 0 ];
for i being Nat holds P[i] from NAT_1:sch 2(A13,A12);
hence thesis by A1;
end;
scheme
PathCatenation {P[set,set], p,q() -> FinSequence}:
for i being Nat st i in dom (p()$^q()) & i+1 in dom (p()$^q())
for x,y being set st x = (p( )$^q()).i & y = (p()$^q()).(i+1) holds P[x,y]
provided
A1: for i being Nat st i in dom p() & i+1 in dom p() holds P[
p().i, p().(i+1)] and
A2: for i being Nat st i in dom q() & i+1 in dom q() holds P[
q().i, q().(i+1)] and
A3: len p() > 0 & len q() > 0 & p().len p() = q().1;
p() <> {} by A3;
then consider r being FinSequence, a being object such that
A4: p() = r^<*a*> by FINSEQ_1:46;
q() <> {} by A3;
then
A5: p()$^q() = r^q() by A4,Th2;
0+1 <= len q() by A3,NAT_1:13;
then
A6: 1 in Seg len q() by FINSEQ_1:1;
A7: Seg len q() = dom q() by FINSEQ_1:def 3;
let i be Nat;
assume that
A8: i in dom (p()$^q()) and
A9: i+1 in dom (p()$^q());
A10: i >= 0+1 by A8,Lm1;
let x,y be set;
A11: i+1 >= 1 by NAT_1:11;
A12: len p() = len r + len <*a*> by A4,FINSEQ_1:22
.= len r + 1 by FINSEQ_1:40;
assume that
A13: x = (p()$^q()).i and
A14: y = (p()$^q()).(i+1);
per cases;
suppose
A15: i < len p();
then i in dom p() & i+1 in dom p() by A10,Lm3,Lm4;
then
A16: P[p().i, p().(i+1)] by A1;
A17: now
assume i+1 <= len r;
then i+1 in Seg len r by A11,FINSEQ_1:1;
then i+1 in dom r by FINSEQ_1:def 3;
hence y = r.(i+1) & r.(i+1) = p().(i+1) by A14,A4,A5,FINSEQ_1:def 7;
end;
A18: i <= len r by A12,A15,NAT_1:13;
then i in Seg len r by A10,FINSEQ_1:1;
then i in dom r by FINSEQ_1:def 3;
then
A19: x = r.i & r.i = p().i by A13,A4,A5,FINSEQ_1:def 7;
i = len r or i < len r by A18,XXREAL_0:1;
hence thesis by A3,A6,A7,A14,A5,A12,A16,A19,A17,FINSEQ_1:def 7,NAT_1:13;
end;
suppose
i >= len p();
then consider k being Nat such that
A20: i = len p()+k by NAT_1:10;
reconsider k as Nat;
A21: i = len r+(1+k) by A12,A20;
len (p()$^q()) = len r + len q() by A5,FINSEQ_1:22;
then
A22: k+1 < len q() by A9,A21,Lm2,XREAL_1:7;
then
A23: k+1+1 in dom q() by Lm4;
A24: k+1 in dom q() by A22,Lm3;
then
A25: x = q().(k+1) by A13,A5,A21,FINSEQ_1:def 7;
len r+(1+k)+1 = len r+(k+1+1);
then y = q().(k+1+1) by A14,A5,A12,A20,A23,FINSEQ_1:def 7;
hence thesis by A2,A24,A23,A25;
end;
end;
definition
let R be Relation;
mode RedSequence of R -> FinSequence means :Def2:
len it > 0 & for i being Nat st
i in dom it & i+1 in dom it holds [it.i, it.(i+1)] in R;
existence
proof
take p = <*{}*>;
thus len p > 0;
let i be Nat;
assume that
A1: i in dom p and
A2: i+1 in dom p;
A3: dom p = {1} by FINSEQ_1:2,38;
then i = 1 by A1,TARSKI:def 1;
hence thesis by A3,A2,TARSKI:def 1;
end;
end;
registration
let R be Relation;
cluster -> non empty for RedSequence of R;
coherence by Def2,CARD_1:27;
end;
theorem Th6:
for R being Relation, a being object holds <*a*> is RedSequence of R
proof
let R be Relation, a be object;
set p = <*a*>;
thus len p > 0;
let i be Nat;
assume that
A1: i in dom p and
A2: i+1 in dom p;
A3: dom p = {1} by FINSEQ_1:2,38;
then i = 1 by A1,TARSKI:def 1;
hence thesis by A3,A2,TARSKI:def 1;
end;
theorem Th7:
for R being Relation, a,b being object st
[a,b] in R holds <*a,b*> is RedSequence of R
proof
let R be Relation, a,b be object;
assume
A1: [a,b] in R;
set p = <*a,b*>;
thus len p > 0;
let i be Nat;
assume that
A2: i in dom p and
A3: i+1 in dom p;
len p = 1+1 by FINSEQ_1:44;
then i+1 <= 1+1 by A3,Lm1;
then
A4: i <= 1 by XREAL_1:6;
i >= 1 by A2,Lm1;
then p.1 = a & i = 1 by A4,XXREAL_0:1;
hence thesis by A1;
end;
theorem Th8:
for R being Relation, p,q being RedSequence of R st p.len p = q.1
holds p$^q is RedSequence of R
proof
let R be Relation, p,q be RedSequence of R;
defpred P[set,set] means [$1,$2] in R;
set r = p$^q;
consider p1 being FinSequence, x being object such that
A1: p = p1^<*x*> by FINSEQ_1:46;
assume p.len p = q.1;
then
A2: len p > 0 & len q > 0 & p.len p = q.1;
r = p1^q by A1,Th2;
hence len r > 0;
A3: for i being Nat st i in dom q & i+1 in dom q holds P[q.i, q.(
i+1)] by Def2;
A4: for i being Nat st i in dom p & i+1 in dom p holds P[p.i, p.(
i+1)] by Def2;
for i being Nat st i in dom (p$^q) & i+1 in dom (p$^q) for x,
y being set st x = (p$^q).i & y = (p$^q).(i+1) holds P[x,y] from PathCatenation
(A4,A3,A2);
hence thesis;
end;
theorem Th9:
for R being Relation, p being RedSequence of R holds
Rev p is RedSequence of R~
proof
let R be Relation, p be RedSequence of R;
len p > 0;
hence len Rev p > 0 by FINSEQ_5:def 3;
let i be Nat;
assume that
A1: i in dom Rev p and
A2: i+1 in dom Rev p;
A3: len Rev p = len p by FINSEQ_5:def 3;
then
A4: dom Rev p = Seg len p by FINSEQ_1:def 3;
i+1 <= len p by A3,A2,Lm1;
then reconsider k = len p-(i+1)+1 as Nat by FINSEQ_5:1;
A5: dom p = Seg len p by FINSEQ_1:def 3;
then
A6: k in dom p by A4,A2,FINSEQ_5:2;
k = len p-i;
then k+1 in dom p by A4,A5,A1,FINSEQ_5:2;
then
A7: [p.k, p.(k+1)] in R by A6,Def2;
(Rev p).i = p.(len p-i+1) & (Rev p).(i+1) = p.(len p-(i+1)+1) by A1,A2,
FINSEQ_5:def 3;
hence thesis by A7,RELAT_1:def 7;
end;
theorem Th10:
for R,Q being Relation st R c= Q for p being RedSequence of R
holds p is RedSequence of Q
proof
let R,Q be Relation such that
A1: R c= Q;
let p be RedSequence of R;
thus len p > 0;
let i be Nat;
assume i in dom p & i+1 in dom p;
then [p.i, p.(i+1)] in R by Def2;
hence thesis by A1;
end;
begin :: Reducibility, convertibility, and normal forms
definition
let R be Relation;
let a,b be object;
pred R reduces a,b means
ex p being RedSequence of R st p.1 = a & p. len p = b;
end;
definition
let R be Relation;
let a,b be object;
pred a,b are_convertible_wrt R means
R \/ R~ reduces a,b;
end;
theorem Th11:
for R being Relation, a,b being object holds R reduces a,b iff
ex p being FinSequence st len p > 0 & p.1 = a & p.len p = b &
for i being Nat st i in dom p & i+1 in dom p holds [p.i, p.(i+1)] in R
proof
let R be Relation, a,b be object;
thus R reduces a,b implies ex p being FinSequence st len p > 0 & p.1 = a & p
.len p = b & for i being Nat st i in dom p & i+1 in dom p holds [p.i
, p.(i+1)] in R
proof
given p being RedSequence of R such that
A1: p.1 = a & p.len p = b;
take p;
thus thesis by A1,Def2;
end;
given p being FinSequence such that
A2: len p > 0 and
A3: p.1 = a & p.len p = b and
A4: for i being Nat st i in dom p & i+1 in dom p holds [p.i,
p.(i+1)] in R;
reconsider p as RedSequence of R by A2,A4,Def2;
take p;
thus thesis by A3;
end;
theorem Th12:
for R being Relation, a being object holds R reduces a,a
proof
let R be Relation;
let a be object;
reconsider p = <*a*> as RedSequence of R by Th6;
take p;
len p = 1 by FINSEQ_1:40;
hence thesis;
end;
theorem Th13:
for a,b being object st {} reduces a,b holds a = b
proof
let a,b be object;
given p being RedSequence of {} such that
A1: p.1 = a & p.len p = b;
A2: now
assume len p > 1;
then 1 in dom p & 1+1 in dom p by Lm3,Lm4;
hence contradiction by Def2;
end;
len p >= 0+1 by NAT_1:13;
hence thesis by A1,A2,XXREAL_0:1;
end;
theorem Th14:
for R being Relation, a,b being object st
R reduces a,b & not a in field R holds a = b
proof
let R be Relation, a,b be object;
given p being RedSequence of R such that
A1: p.1 = a and
A2: p.len p = b;
assume
A3: not a in field R;
A4: now
assume len p > 1;
then 1 in dom p & 1+1 in dom p by Lm3,Lm4;
then [p.1, p.(1+1)] in R by Def2;
hence contradiction by A1,A3,RELAT_1:15;
end;
len p >= 0+1 by NAT_1:13;
hence thesis by A1,A2,A4,XXREAL_0:1;
end;
theorem Th15:
for R being Relation, a,b being object st [a,b] in R holds R reduces a,b
proof
let R be Relation, a,b be object;
assume [a,b] in R;
then reconsider p = <*a,b*> as RedSequence of R by Th7;
take p;
len p = 2 by FINSEQ_1:44;
hence thesis;
end;
theorem Th16:
for R being Relation, a,b,c being object st
R reduces a,b & R reduces b,c holds R reduces a,c
proof
let R be Relation, a,b,c be object;
given p being RedSequence of R such that
A1: p.1 = a and
A2: p.len p = b;
given q being RedSequence of R such that
A3: q.1 = b and
A4: q.len q = c;
reconsider r = p$^q as RedSequence of R by A2,A3,Th8;
take r;
consider p1 being FinSequence, x being object such that
A5: p = p1^<*x*> by FINSEQ_1:46;
0+1 <= len q by NAT_1:13;
then len q in Seg len q by FINSEQ_1:1;
then
A6: len q in dom q by FINSEQ_1:def 3;
A7: r = p1^q by A5,Th2;
p1 = {} or len p1 >= 0+1 by NAT_1:13;
then r = q & p = <*x*> or 1 in Seg len p1 by A5,A7,FINSEQ_1:1,34;
then 1 in dom p1 or len p = 1 & r = q by FINSEQ_1:40,def 3;
then r.1 = p1.1 & p1.1 = a or r.1 = b & b = a by A1,A2,A3,A5,A7,
FINSEQ_1:def 7;
hence r.1 = a;
len r = len p1+len q by A7,FINSEQ_1:22;
hence thesis by A4,A7,A6,FINSEQ_1:def 7;
end;
theorem Th17:
for R being Relation, p being RedSequence of R,
i,j being Nat st i in dom p & j in dom p & i <= j holds
R reduces p.i,p.j
proof
let R be Relation, p be RedSequence of R, i,j be Nat;
defpred Q[Nat] means i+$1 in dom p implies R reduces p.i,p.(i+$1);
assume that
A1: i in dom p and
A2: j in dom p and
A3: i <= j;
consider k being Nat such that
A4: j = i+k by A3,NAT_1:10;
now
A5: i >= 1 by A1,Lm1;
let j be Nat such that
A6: i+j in dom p implies R reduces p.i,p.(i+j) and
A7: i+(j+1) in dom p;
A8: i+(j+1) = i+j+1;
then
A9: i+j < len p by A7,Lm2;
then i+j in dom p by A5,Lm3;
then [p.(i+j),p.(i+(j+1))] in R by A7,A8,Def2;
then R reduces p.(i+j), p.(i+(j+1)) by Th15;
hence R reduces p.i,p.(i+(j+1)) by A6,A5,A9,Lm3,Th16;
end;
then
A10: for k being Nat st Q[k] holds Q[k+1];
A11: Q[ 0 ] by Th12;
A12: for j being Nat holds Q[j] from NAT_1:sch 2(A11,A10);
thus thesis by A2,A12,A4;
end;
theorem Th18:
for R being Relation, a,b being object st R reduces a,b & a <> b
holds a in field R & b in field R
proof
let R be Relation, a,b be object;
given p being RedSequence of R such that
A1: a = p.1 and
A2: b = p.len p;
A3: len p >= 0+1 by NAT_1:13;
assume a <> b;
then len p > 1 by A1,A2,A3,XXREAL_0:1;
then
A4: 1+1 in dom p by Lm4;
1 in dom p by A3,Lm3;
then
A5: [a,p.2] in R by A1,A4,Def2;
hence a in field R by RELAT_1:15;
defpred P[Nat] means $1 in dom p implies p.$1 in field R;
A6: len p in dom p by FINSEQ_5:6;
now
let i be Nat such that
i in dom p implies p.i in field R and
A7: i+1 in dom p;
A8: i < len p by A7,Lm2;
per cases;
suppose
i = 0;
hence p.(i+1) in field R by A1,A5,RELAT_1:15;
end;
suppose
i > 0;
then i in dom p by A8,Lm3;
then [p.i,p.(i+1)] in R by A7,Def2;
hence p.(i+1) in field R by RELAT_1:15;
end;
end;
then
A9: for k being Nat st P[k] holds P[k+1];
A10: P[ 0 ] by Lm1;
for i being Nat holds P[i] from NAT_1:sch 2(A10,A9);
hence thesis by A2,A6;
end;
theorem
for R being Relation, a,b being object st
R reduces a,b holds a in field R iff b in field R by Th18;
theorem Th20:
for R being Relation, a,b being object holds
R reduces a,b iff a = b or [a,b] in R[*]
proof
let R be Relation, a,b be object;
hereby
assume
A1: R reduces a,b;
then consider p being RedSequence of R such that
A2: a = p.1 & b = p.len p;
A3: now
let i be Nat;
assume i >= 1 & i < len p;
then i in dom p & i+1 in dom p by Lm3,Lm4;
hence [p.i,p.(i+1)] in R by Def2;
end;
assume a <> b;
then
A4: a in field R & b in field R by A1,Th18;
len p >= 0+1 by NAT_1:13;
hence [a,b] in R[*] by A2,A4,A3,FINSEQ_1:def 17;
end;
assume that
A5: a = b or [a,b] in R[*] and
A6: not R reduces a,b;
consider p being FinSequence such that
A7: len p >= 1 and
A8: p.1 = a & p.(len p) = b and
A9: for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R by A5,A6
,Th12,FINSEQ_1:def 17;
p is RedSequence of R
proof
thus len p > 0 by A7;
let i be Nat;
assume that
A10: i in dom p and
A11: i+1 in dom p;
i >= 1 by A10,Lm1;
hence thesis by A9,A11,Lm2;
end;
hence contradiction by A6,A8;
end;
theorem Th21:
for R being Relation, a,b being object
holds R reduces a,b iff R[*] reduces a,b
proof
let R be Relation, a,b be object;
R reduces a,b iff a = b or [a,b] in R[*] by Th20;
hence R reduces a,b implies R[*] reduces a,b by Th12,Th15;
given p being RedSequence of R[*] such that
A1: a = p.1 and
A2: b = p.len p;
defpred P[Nat] means $1 in dom p implies R reduces a,p.$1;
now
let i be Nat such that
A3: i in dom p implies R reduces a,p.i and
A4: i+1 in dom p;
A5: i < len p by A4,Lm2;
per cases;
suppose
i = 0;
hence R reduces a,p.(i+1) by A1,Th12;
end;
suppose
A6: i > 0;
then i in dom p by A5,Lm3;
then [p.i,p.(i+1)] in R[*] by A4,Def2;
then R reduces p.i, p.(i+1) by Th20;
hence R reduces a,p.(i+1) by A3,A5,A6,Lm3,Th16;
end;
end;
then
A7: for k being Nat st P[k] holds P[k+1];
A8: len p in dom p by FINSEQ_5:6;
A9: P[ 0 ] by Lm1;
for i being Nat holds P[i] from NAT_1:sch 2(A9,A7);
hence thesis by A2,A8;
end;
theorem Th22:
for R,Q being Relation st R c= Q for a,b being object st
R reduces a,b holds Q reduces a,b
proof
let R,Q be Relation such that
A1: R c= Q;
let a,b be object;
given p being RedSequence of R such that
A2: p.1 = a & p.len p = b;
p is RedSequence of Q by A1,Th10;
hence ex p being RedSequence of Q st p.1 = a & p.len p = b by A2;
end;
theorem
for R being Relation, X being set, a,b being object holds
R reduces a,b iff R \/ id X reduces a,b
proof
let R be Relation, X be set, a,b be object;
thus R reduces a,b implies R \/ id X reduces a,b by Th22,XBOOLE_1:7;
given p being RedSequence of R \/ id X such that
A1: p.1 = a and
A2: p.len p = b;
defpred P[Nat] means $1 in dom p implies R reduces a,p.$1;
now
let i be Nat;
assume
A3: i in dom p implies R reduces a,p.i;
assume
A4: i+1 in dom p;
per cases;
suppose
A5: i in dom p;
then [p.i, p.(i+1)] in R \/ id X by A4,Def2;
then [p.i, p.(i+1)] in R or [p.i, p.(i+1)] in id X by XBOOLE_0:def 3;
then R reduces p.i, p.(i+1) or p.i = p.(i+1) by Th15,RELAT_1:def 10;
hence R reduces a, p.(i+1) by A3,A5,Th16;
end;
suppose
not i in dom p;
then i < 0+1 or i > len p & i+1 <= len p by A4,Lm1,Lm3;
then i = 0 by NAT_1:13;
hence R reduces a, p.(i+1) by A1,Th12;
end;
end;
then
A6: for k be Nat st P[k] holds P[k+1];
A7: len p in dom p by Lm3;
A8: P[ 0 ] by Lm1;
for i being Nat holds P[i] from NAT_1:sch 2(A8,A6);
hence thesis by A2,A7;
end;
theorem Th24:
for R being Relation, a,b being object st R reduces a,b
holds R~ reduces b,a
proof
let R be Relation, a,b be object;
given p being RedSequence of R such that
A1: p.1 = a and
A2: p.len p = b;
reconsider q = Rev p as RedSequence of R~ by Th9;
take q;
1 in dom q by FINSEQ_5:6;
hence q.1 = p.(len p-1+1) by FINSEQ_5:def 3
.= b by A2;
len q in dom q & len q = len p by FINSEQ_5:6,def 3;
hence q.(len q) = p.(len p-len p+1) by FINSEQ_5:def 3
.= a by A1;
end;
Lm5: for R being Relation, a,b being object
st a,b are_convertible_wrt R holds b,a are_convertible_wrt R
proof
let R be Relation;
let a,b be object;
assume R \/ R~ reduces a,b;
then (R \/ R~)~ reduces b,a by Th24;
then R~ \/ R~~ reduces b,a by RELAT_1:23;
hence R \/ R~ reduces b,a;
end;
theorem Th25:
for R being Relation, a,b being object st R reduces a,b holds
a,b are_convertible_wrt R & b,a are_convertible_wrt R
proof
let R be Relation, a,b be object;
given p being RedSequence of R such that
A1: p.1 = a & p.len p = b;
p is RedSequence of R \/ R~
proof
thus len p > 0;
let i be Nat;
assume i in dom p & i+1 in dom p;
then [p.i, p.(i+1)] in R by Def2;
hence thesis by XBOOLE_0:def 3;
end;
then R \/ R~ reduces a,b by A1;
hence a,b are_convertible_wrt R;
hence thesis by Lm5;
end;
theorem Th26:
for R being Relation, a being object holds a,a are_convertible_wrt R
by Th12;
theorem Th27:
for a,b being object st a,b are_convertible_wrt {} holds a = b by Th13;
theorem
for R being Relation, a,b being object st a,b are_convertible_wrt R &
not a in field R holds a = b
proof
let R be Relation;
let a,b be object;
A1: field R = field (R~) & field (R \/ R~) = (field R) \/ field (R~) by
RELAT_1:18,21;
assume R \/ R~ reduces a,b;
hence thesis by A1,Th14;
end;
theorem Th29:
for R being Relation, a,b being object st
[a,b] in R holds a,b are_convertible_wrt R
proof
let R be Relation, a,b be object;
assume [a,b] in R;
then R reduces a,b by Th15;
hence thesis by Th25;
end;
theorem Th30:
for R being Relation, a,b,c being object st
a,b are_convertible_wrt R & b,c are_convertible_wrt R holds
a,c are_convertible_wrt R by Th16;
theorem
for R being Relation, a,b being object st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R by Lm5;
theorem Th32:
for R being Relation, a,b being object st a,b are_convertible_wrt R
& a <> b holds a in field R & b in field R
proof
let R be Relation, a,b be object;
A1: field (R \/ R~) = (field R) \/ field (R~) by RELAT_1:18
.= (field R) \/ field R by RELAT_1:21
.= field R;
assume R \/ R~ reduces a,b;
hence thesis by A1,Th18;
end;
definition
let R be Relation;
let a be object;
pred a is_a_normal_form_wrt R means
not ex b being object st [a,b] in R;
end;
theorem Th33:
for R being Relation, a,b being object st a is_a_normal_form_wrt R
& R reduces a,b holds a = b
proof
let R be Relation;
let a,b be object;
assume
A1: not ex b being object st [a,b] in R;
assume R reduces a,b;
then consider p being FinSequence such that
A2: len p > 0 and
A3: p.1 = a and
A4: p.len p = b and
A5: for i being Nat st i in dom p & i+1 in dom p holds [p.i,
p.(i+1)] in R by Th11;
A6: now
assume len p > 1;
then 1 in dom p & 1+1 in dom p by Lm3,Lm4;
then [a, p.(1+1)] in R by A3,A5;
hence contradiction by A1;
end;
len p >= 0+1 by A2,NAT_1:13;
hence thesis by A3,A4,A6,XXREAL_0:1;
end;
theorem Th34:
for R being Relation, a being object st not a in field R holds
a is_a_normal_form_wrt R by RELAT_1:15;
definition
let R be Relation;
let a,b be object;
pred b is_a_normal_form_of a,R means
b is_a_normal_form_wrt R & R reduces a,b;
pred a,b are_convergent_wrt R means :Def7:
ex c being object st R reduces a,c & R reduces b,c;
pred a,b are_divergent_wrt R means
ex c being object st R reduces c,a & R reduces c,b;
pred a,b are_convergent<=1_wrt R means
ex c being object st ([a,c] in R or a = c) & ([b,c] in R or b = c);
pred a,b are_divergent<=1_wrt R means
ex c being object st ([c,a] in R or a = c) & ([c,b] in R or b = c);
end;
theorem Th35:
for R being Relation, a being object st not a in field R holds
a is_a_normal_form_of a,R by Th12,Th34;
theorem Th36:
for R being Relation, a,b being object st R reduces a,b holds
a,b are_convergent_wrt R & a,b are_divergent_wrt R &
b,a are_convergent_wrt R & b,a are_divergent_wrt R
proof
let R be Relation, a,b be object;
R reduces a,a & R reduces b,b by Th12;
hence thesis;
end;
theorem Th37:
for R being Relation, a,b being object st a,b are_convergent_wrt R
or a,b are_divergent_wrt R holds a,b are_convertible_wrt R
proof
let R be Relation, a,b be object;
assume
A1: a,b are_convergent_wrt R or a,b are_divergent_wrt R;
per cases by A1;
suppose
a,b are_convergent_wrt R;
then consider c being object such that
A2: R reduces a,c & R reduces b,c;
a,c are_convertible_wrt R & c,b are_convertible_wrt R by A2,Th25;
hence thesis by Th30;
end;
suppose
a,b are_divergent_wrt R;
then consider c being object such that
A3: R reduces c,a & R reduces c,b;
c,b are_convertible_wrt R & a,c are_convertible_wrt R by A3,Th25;
hence thesis by Th30;
end;
end;
theorem Th38:
for R being Relation, a being object holds a,a are_convergent_wrt R
& a,a are_divergent_wrt R by Th12;
theorem Th39:
for a,b being object st a,b are_convergent_wrt {} or
a,b are_divergent_wrt {} holds a = b
proof
let a,b be object;
A1: now
assume a,b are_convergent_wrt {};
then consider c being object such that
A2: {} reduces a,c and
A3: {} reduces b,c;
a = c by A2,Th13;
hence thesis by A3,Th13;
end;
A4: now
assume a,b are_divergent_wrt {};
then consider c being object such that
A5: {} reduces c,a and
A6: {} reduces c,b;
a = c by A5,Th13;
hence thesis by A6,Th13;
end;
assume a,b are_convergent_wrt {} or a,b are_divergent_wrt {};
hence thesis by A1,A4;
end;
theorem
for R being Relation, a,b being object st a,b are_convergent_wrt R holds
b,a are_convergent_wrt R;
theorem
for R being Relation, a,b being object st a,b are_divergent_wrt R holds
b,a are_divergent_wrt R;
theorem Th42:
for R being Relation, a,b,c being object st
R reduces a,b & b,c are_convergent_wrt R or
a,b are_convergent_wrt R & R reduces c,b holds a,c are_convergent_wrt R
proof
let R be Relation, a,b,c be object;
assume
A1: R reduces a,b & b,c are_convergent_wrt R or a,b are_convergent_wrt R
& R reduces c,b;
per cases by A1;
suppose
A2: R reduces a,b & b,c are_convergent_wrt R;
then consider d being object such that
A3: R reduces b,d and
A4: R reduces c,d;
R reduces a,d by A2,A3,Th16;
hence thesis by A4;
end;
suppose
A5: a,b are_convergent_wrt R & R reduces c,b;
then consider d being object such that
A6: R reduces a,d and
A7: R reduces b,d;
R reduces c,d by A5,A7,Th16;
hence thesis by A6;
end;
end;
theorem
for R being Relation, a,b,c being object st R reduces b,a & b,c
are_divergent_wrt R or a,b are_divergent_wrt R & R reduces b,c holds a,c
are_divergent_wrt R
proof
let R be Relation, a,b,c be object;
assume
A1: R reduces b,a & b,c are_divergent_wrt R or a,b are_divergent_wrt R &
R reduces b,c;
per cases by A1;
suppose
A2: R reduces b,a & b,c are_divergent_wrt R;
then consider d being object such that
A3: R reduces d,b and
A4: R reduces d,c;
R reduces d,a by A2,A3,Th16;
hence thesis by A4;
end;
suppose
A5: a,b are_divergent_wrt R & R reduces b,c;
then consider d being object such that
A6: R reduces d,a and
A7: R reduces d,b;
R reduces d,c by A5,A7,Th16;
hence thesis by A6;
end;
end;
theorem Th44:
for R being Relation, a,b being object st
a,b are_convergent<=1_wrt R holds a,b are_convergent_wrt R
proof
let R be Relation, a,b be object;
given c being object such that
A1: ([a,c] in R or a = c) & ([b,c] in R or b = c);
take c;
thus thesis by A1,Th12,Th15;
end;
theorem Th45:
for R being Relation, a,b being object st
a,b are_divergent<=1_wrt R holds a,b are_divergent_wrt R
proof
let R be Relation, a,b be object;
given c being object such that
A1: ([c,a] in R or a = c) & ([c,b] in R or b = c);
take c;
thus thesis by A1,Th12,Th15;
end;
definition
let R be Relation;
let a be object;
pred a has_a_normal_form_wrt R means
ex b being object st b is_a_normal_form_of a,R;
end;
theorem Th46:
for R being Relation, a being object st not a in field R holds
a has_a_normal_form_wrt R by Th35;
definition
let R be Relation, a be object;
assume that
A1: a has_a_normal_form_wrt R and
A2: for b,c being object st
b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c;
func nf(a,R) -> set means :Def12:
it is_a_normal_form_of a,R;
existence
proof
consider x such that
A3: x is_a_normal_form_of a,R by A1;
x is set by TARSKI:1;
hence thesis by A3;
end;
uniqueness by A2;
end;
begin :: Terminating reductions
definition
let R be Relation;
attr R is co-well_founded means
R~ is well_founded;
attr R is weakly-normalizing means :Def14:
for a being object st a in field R holds a has_a_normal_form_wrt R;
attr R is strongly-normalizing means :: terminating, Noetherian
for f being ManySortedSet of NAT
ex i being Nat st not [f.i,f.(i+1)] in R;
end;
definition
let R be Relation;
redefine attr R is co-well_founded means :: redefines co-well_founded (REWRITE1, definition)
: Def16:
for Y being set st Y c= field R & Y <> {}
ex a being object st a in Y & for b being object st b in Y & a <> b
holds not [a,b] in R;
compatibility
proof
A1: field R = field (R~) by RELAT_1:21;
hereby
assume R is co-well_founded;
then
A2: R~ is well_founded;
let Y be set;
assume Y c= field R & Y <> {};
then consider a being object such that
A3: a in Y and
A4: (R~)-Seg(a) misses Y by A1,A2;
take a;
thus a in Y by A3;
let b be object;
assume b in Y;
then not b in (R~)-Seg(a) by A4,XBOOLE_0:3;
then a = b or not [b,a] in R~ by WELLORD1:1;
hence a <> b implies not [a,b] in R by RELAT_1:def 7;
end;
hereby
assume
A5: for Y being set st Y c= field R & Y <> {} ex a being object st a
in Y & for b being object st b in Y & a <> b holds not [a,b] in R;
R~ is well_founded
proof
let Y be set;
assume Y c= field (R~) & Y <> {};
then consider a being object such that
A6: a in Y and
A7: for b being object st b in Y & a <> b holds not [a,b] in R by A1,A5;
take a;
thus a in Y by A6;
now
assume (R~)-Seg(a) /\ Y is non empty;
then reconsider A = (R~)-Seg(a) /\ Y as non empty set;
set x = the Element of A;
A8: x in (R~)-Seg(a) by XBOOLE_0:def 4;
then x in Y & x <> a by WELLORD1:1,XBOOLE_0:def 4;
then
A9: not [a,x] in R by A7;
[x,a] in R~ by A8,WELLORD1:1;
hence contradiction by A9,RELAT_1:def 7;
end;
hence thesis by XBOOLE_0:def 7;
end;
hence R is co-well_founded;
end;
end;
end;
scheme
coNoetherianInduction{R() -> Relation, P[object]}:
for a being object st a in field R() holds P[a]
provided
A1: R() is co-well_founded and
A2: for a being object
st for b being object st [a,b] in R() & a <> b holds P[b]
holds P[a]
proof
given a being object such that
A3: a in field R() and
A4: not P[a];
reconsider X = field R() as non empty set by A3;
reconsider a as Element of X by A3;
set Y = {x where x is Element of X: not P[x]};
A5: a in Y by A4;
Y c= field R()
proof
let y be object;
assume y in Y;
then ex x being Element of X st y = x & not P[x];
hence thesis;
end;
then consider a being object such that
A6: a in Y and
A7: for b being object st b in Y & a <> b holds not [a,b] in R()
by A1,A5;
A8: now
let b be object;
assume that
A9: [a,b] in R() & a <> b and
A10: not P[b];
( not b in Y)& b in X by A7,A9,RELAT_1:15;
hence contradiction by A10;
end;
ex x being Element of X st a = x & not P[x] by A6;
hence thesis by A2,A8;
end;
registration
cluster strongly-normalizing -> irreflexive co-well_founded for Relation;
coherence
proof
defpred Q[object] means not contradiction;
let R be Relation such that
A1: for f being ManySortedSet of NAT ex i being Nat st not
[f.i,f.(i+1)] in R;
thus R is irreflexive
proof
given x being object such that
x in field R and
A2: [x,x] in R;
dom (NAT --> x) = NAT by FUNCOP_1:13;
then reconsider f = NAT --> x as ManySortedSet of NAT by PARTFUN1:def 2
,RELAT_1:def 18;
consider i being Nat such that
A3: not [f.i, f.(i+1)] in R by A1;
i in NAT by ORDINAL1:def 12;
then f.i = x by FUNCOP_1:7;
hence contradiction by A2,A3,FUNCOP_1:7;
end;
defpred P[object,object] means [$1,$2] in R;
let Y be set;
assume that
Y c= field R and
A4: Y <> {} and
A5: for a being object st a in Y
ex b being object st b in Y & a <> b & [a,b ] in R;
reconsider Y as non empty set by A4;
now
let x be set;
assume x in Y;
then ex b being object st b in Y & x <> b & [x,b] in R by A5;
hence ex y being object st y in Y & [x,y] in R;
end;
then
A6: for x be object st x in Y & Q[x]
ex y be object st y in Y & P[x,y] & Q[y ];
set y = the Element of Y;
A7: y in Y & Q[y];
consider f being Function such that
A8: dom f = NAT & rng f c= Y & f.0 = y and
A9: for k being Nat holds P[f.k,f.(k+1)] & Q[f.k] from
TREES_2:sch 5(A7,A6);
f is ManySortedSet of NAT by A8,PARTFUN1:def 2,RELAT_1:def 18;
hence thesis by A1,A9;
end;
cluster co-well_founded irreflexive -> strongly-normalizing for Relation;
coherence
proof
let R be Relation such that
A10: for Y being set st Y c= field R & Y <> {}
ex a being object st a in
Y & for b being object st b in Y & a <> b holds not [a,b] in R;
assume
A11: for x being object st x in field R holds not [x,x] in R;
let f be ManySortedSet of NAT;
assume
A12: for i being Nat holds [f.i, f.(i+1)] in R;
A13: rng f c= field R
proof
let y be object;
assume y in rng f;
then consider x being object such that
A14: x in dom f and
A15: y = f.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A14,PARTFUN1:def 2;
[y, f.(x+1)] in R by A12,A15;
hence thesis by RELAT_1:15;
end;
A16: dom f = NAT by PARTFUN1:def 2;
then f.0 in rng f by FUNCT_1:def 3;
then consider a being object such that
A17: a in rng f and
A18: for b being object st b in rng f & a <> b holds not [a,b] in R
by A10,A13;
consider x being object such that
A19: x in dom f and
A20: a = f.x by A17,FUNCT_1:def 3;
reconsider x as Element of NAT by A19,PARTFUN1:def 2;
A21: f.(x+1) in rng f by A16,FUNCT_1:def 3;
A22: [a,f.(x+1)] in R by A12,A20;
then a <> f.(x+1) by A11,A13,A17;
hence contradiction by A18,A22,A21;
end;
end;
registration
cluster empty -> weakly-normalizing strongly-normalizing for Relation;
coherence by RELAT_1:40;
end;
theorem
for Q being co-well_founded Relation, R being Relation st R c= Q holds
R is co-well_founded
proof
let Q be co-well_founded Relation, R be Relation;
assume
A1: R c= Q;
let Y be set;
assume that
A2: Y c= field R and
A3: Y <> {};
field R c= field Q by A1,RELAT_1:16;
then Y c= field Q by A2;
then consider a being object such that
A4: a in Y and
A5: for b being object st b in Y & a <> b holds not [a,b] in Q by A3,Def16;
take a;
thus a in Y by A4;
let b be object;
assume b in Y & a <> b;
hence thesis by A1,A5;
end;
registration
cluster strongly-normalizing -> weakly-normalizing for Relation;
coherence
proof
let R be Relation such that
A1: R is strongly-normalizing;
let a be object;
assume
A2: a in field R;
then reconsider X = field R as non empty set;
set Y = {x where x is Element of X: R reduces a,x};
A3: Y c= field R
proof
let y be object;
assume y in Y;
then ex x being Element of X st y = x & R reduces a,x;
hence thesis;
end;
R reduces a,a by Th12;
then a in Y by A2;
then consider x being object such that
A4: x in Y and
A5: for b being object st b in Y & x <> b holds not [x,b] in R by A1,A3,Def16;
take x;
A6: ex y being Element of X st x = y & R reduces a,y by A4;
hereby
R is_irreflexive_in field R by A1,RELAT_2:def 10;
then
A7: not [x,x] in R by A3,A4;
given b being object such that
A8: [x,b] in R;
R reduces x,b by A8,Th15;
then
A9: R reduces a,b by A6,Th16;
b in X by A8,RELAT_1:15;
then b in Y by A9;
hence contradiction by A5,A8,A7;
end;
thus thesis by A6;
end;
end;
begin :: Church-Rosser property
definition
let R,Q be Relation;
pred R commutes-weakly_with Q means
for a,b,c being object st [a,b] in R & [a,c] in Q
ex d being object st Q reduces b,d & R reduces c,d;
symmetry
proof
let R,Q be Relation such that
A1: for a,b,c being object st [a,b] in R & [a,c] in Q
ex d being object st Q reduces b,d & R reduces c,d;
let a,b,c be object;
assume [a,b] in Q & [a,c] in R;
then ex d being object st Q reduces c,d & R reduces b,d by A1;
hence thesis;
end;
pred R commutes_with Q means :Def18:
for a,b,c being object st R reduces a,b &
Q reduces a,c ex d being object st Q reduces b,d & R reduces c,d;
symmetry
proof
let R,Q be Relation such that
A2: for a,b,c being object st R reduces a,b & Q reduces a,c
ex d being object st Q reduces b,d & R reduces c,d;
let a,b,c be object;
assume Q reduces a,b & R reduces a,c;
then ex d being object st Q reduces c,d & R reduces b,d by A2;
hence thesis;
end;
end;
theorem
for R,Q being Relation st R commutes_with Q holds R commutes-weakly_with Q
proof
let R,Q be Relation;
assume
A1: for a,b,c being object st R reduces a,b & Q reduces a,c
ex d being object st Q reduces b,d & R reduces c,d;
let a,b,c be object;
assume [a,b] in R & [a,c] in Q;
then R reduces a,b & Q reduces a,c by Th15;
hence thesis by A1;
end;
definition
let R be Relation;
attr R is with_UN_property means :Def19:
for a,b being object st
a is_a_normal_form_wrt R & b is_a_normal_form_wrt R &
a,b are_convertible_wrt R holds a = b;
attr R is with_NF_property means
for a,b being object st a is_a_normal_form_wrt R &
a,b are_convertible_wrt R holds R reduces b,a;
attr R is subcommutative means
for a,b,c being object st [a,b] in R & [a,c] in R holds
b,c are_convergent<=1_wrt R;
attr R is confluent means :Def22:
for a,b being object st a,b are_divergent_wrt R
holds a,b are_convergent_wrt R;
attr R is with_Church-Rosser_property means :Def23:
for a,b being object st a,b are_convertible_wrt R
holds a,b are_convergent_wrt R;
attr R is locally-confluent means
for a,b,c being object st [a,b] in R & [a,c] in R
holds b,c are_convergent_wrt R;
end;
theorem Th49:
for R being Relation st R is subcommutative for a,b,c being object
st R reduces a,b & [a,c] in R holds b,c are_convergent_wrt R
proof
let R be Relation;
assume
A1: R is subcommutative;
let a,b,c be object;
given p being RedSequence of R such that
A2: p.1 = a and
A3: p.len p = b;
defpred P[Nat] means $1 in dom p implies ex d being object st ([p.$1
,d] in R or p.$1 = d) & R reduces c,d;
assume
A4: [a,c] in R;
now
let i be Nat such that
A5: i in dom p implies P[i] and
A6: i+1 in dom p;
per cases;
suppose
A7: i = 0;
R reduces c,c by Th12;
hence P[i+1] by A2,A4,A7;
end;
suppose
A8: i > 0;
A9: i < len p by A6,Lm2;
then consider d being object such that
A10: [p.i,d] in R or p.i = d and
A11: R reduces c,d by A5,A8,Lm3;
i in dom p by A8,A9,Lm3;
then
A12: [p.i,p.(i+1)] in R by A6,Def2;
A13: now
assume [p.i,d] in R;
then p.(i+1),d are_convergent<=1_wrt R by A1,A12;
then consider e being object such that
A14: [p.(i+1),e] in R or p.(i+1) = e and
A15: [d,e] in R or d = e;
take e;
thus [p.(i+1),e] in R or p.(i+1) = e by A14;
R reduces d,e by A15,Th12,Th15;
hence R reduces c,e by A11,Th16;
end;
now
assume p.i = d;
then R reduces d, p.(i+1) by A12,Th15;
hence R reduces c, p.(i+1) by A11,Th16;
end;
hence P[i+1] by A10,A13;
end;
end;
then
A16: for k be Nat st P[k] holds P[k+1];
A17: len p in dom p by FINSEQ_5:6;
A18: P[ 0 ] by Lm1;
for i being Nat holds P[i] from NAT_1:sch 2(A18,A16);
then consider d being object such that
A19: ( [b,d] in R or b = d)& R reduces c,d by A3,A17;
take d;
thus thesis by A19,Th12,Th15;
end;
theorem
for R being Relation holds R is confluent iff R commutes_with R
proof
let R be Relation;
hereby
assume
A1: R is confluent;
thus R commutes_with R
proof
let a,b,c be object;
assume R reduces a,b & R reduces a,c;
then b,c are_divergent_wrt R;
then b,c are_convergent_wrt R by A1;
hence thesis;
end;
end;
assume
A2: for a,b,c being object st R reduces a,b & R reduces a,c
ex d being object st R reduces b,d & R reduces c,d;
let a,b be object;
assume ex c being object st R reduces c,a & R reduces c,b;
hence ex d being object st R reduces a,d & R reduces b,d by A2;
end;
theorem Th51:
for R being Relation holds R is confluent iff
for a,b,c being object st
R reduces a,b & [a,c] in R holds b,c are_convergent_wrt R
proof
let R be Relation;
hereby
assume
A1: R is confluent;
let a,b,c be object;
assume that
A2: R reduces a,b and
A3: [a,c] in R;
R reduces a,c by A3,Th15;
then b,c are_divergent_wrt R by A2;
hence b,c are_convergent_wrt R by A1;
end;
assume
A4: for a,b,c being object st R reduces a,b & [a,c] in R holds b,c
are_convergent_wrt R;
let b,c be object;
given a being object such that
A5: R reduces a,b and
A6: R reduces a,c;
consider p being RedSequence of R such that
A7: p.1 = a and
A8: p.len p = b by A5;
consider q being RedSequence of R such that
A9: q.1 = a and
A10: q.len q = c by A6;
defpred P[Nat,Nat] means p.$1, q.$2 are_convergent_wrt
R;
defpred Q[Nat] means $1 in dom p implies
for j being Nat st j in dom q holds P[$1,j];
A11: for i being Nat st Q[i] holds Q[i+1]
proof
let i be Nat such that
i in dom p implies for j being Nat st j in dom q holds P[i,
j] and
A12: i+1 in dom p;
defpred R[Nat] means $1 in dom q implies P[i+1,$1];
A13: for j being Nat st R[j] holds R[j+1]
proof
1 in dom p by FINSEQ_5:6;
then
A14: R reduces a,p.(i+1) by A7,A12,Th17,NAT_1:11;
let j be Nat such that
A15: j in dom q implies P[i+1,j] and
A16: j+1 in dom q;
per cases;
suppose
j = 0;
hence thesis by A9,A14,Th36;
end;
suppose
A17: j > 0;
A18: j < len q by A16,Lm2;
then consider d being object such that
A19: R reduces p.(i+1),d and
A20: R reduces q.j,d by A15,A17,Def7,Lm3;
j in dom q by A17,A18,Lm3;
then [q.j, q.(j+1)] in R by A16,Def2;
then d,q.(j+1) are_convergent_wrt R by A4,A20;
hence thesis by A19,Th42;
end;
end;
A21: R[ 0 ] by Lm1;
thus for j being Nat holds R[j] from NAT_1:sch 2(A21,A13 );
end;
A22: len p in dom p & len q in dom q by FINSEQ_5:6;
A23: Q[ 0 ] by Lm1;
for i being Nat holds Q[i] from NAT_1:sch 2(A23,A11);
hence thesis by A8,A10,A22;
end;
theorem
for R being Relation holds
R is locally-confluent iff R commutes-weakly_with R
proof
let R be Relation;
hereby
assume
A1: R is locally-confluent;
thus R commutes-weakly_with R
proof
let a,b,c be object;
assume [a,b] in R & [a,c] in R;
then b,c are_convergent_wrt R by A1;
hence thesis;
end;
end;
assume
A2: for a,b,c being object st [a,b] in R & [a,c] in R
ex d being object st R reduces b,d & R reduces c,d;
let a,b,c be object;
assume [a,b] in R & [a,c] in R;
hence ex d being object st R reduces b,d & R reduces c,d by A2;
end;
registration
cluster with_Church-Rosser_property -> confluent for Relation;
coherence
proof
let R be Relation;
assume
A1: for a,b being object st a,b are_convertible_wrt R holds a,b
are_convergent_wrt R;
let a,b be object;
assume a,b are_divergent_wrt R;
then a,b are_convertible_wrt R by Th37;
hence thesis by A1;
end;
cluster confluent -> locally-confluent with_Church-Rosser_property for
Relation;
coherence
proof
let R be Relation;
assume
A2: for a,b being object st a,b are_divergent_wrt R holds a,b
are_convergent_wrt R;
hereby
let a,b,c be object;
assume [a,b] in R & [a,c] in R;
then R reduces a,b & R reduces a,c by Th15;
then b,c are_divergent_wrt R;
hence b,c are_convergent_wrt R by A2;
end;
let a,b be object;
given p being RedSequence of R \/ R~ such that
A3: p.1 = a and
A4: p.len p = b;
defpred P[Nat] means $1 in dom p implies a,p.$1
are_convergent_wrt R;
now
let i be Nat;
assume that
A5: i in dom p implies a,p.i are_convergent_wrt R and
A6: i+1 in dom p;
per cases;
suppose
A7: i in dom p;
then consider c being object such that
A8: R reduces a,c and
A9: R reduces p.i,c by A5;
[p.i, p.(i+1)] in R \/ R~ by A6,A7,Def2;
then [p.i, p.(i+1)] in R or [p.i, p.(i+1)] in R~ by XBOOLE_0:def 3;
then [p.i, p.(i+1)] in R or [p.(i+1), p.i] in R by RELAT_1:def 7;
then R reduces p.i, p.(i+1) or R reduces p.(i+1), p.i by Th15;
then c,p.(i+1) are_divergent_wrt R or R reduces p.(i+1),c by A9,Th16;
then c,p.(i+1) are_convergent_wrt R or a,p.(i+1) are_convergent_wrt R
by A2,A8;
hence a, p.(i+1) are_convergent_wrt R by A8,Th42;
end;
suppose
not i in dom p;
then i < 0+1 or i > len p & i+1 <= len p by A6,Lm1,Lm3;
then i = 0 by NAT_1:13;
hence a, p.(i+1) are_convergent_wrt R by A3,Th38;
end;
end;
then
A10: for k being Nat st P[k] holds P[k+1];
A11: len p in dom p by FINSEQ_5:6;
A12: P[ 0 ] by Lm1;
for i being Nat holds P[i] from NAT_1:sch 2(A12,A10);
hence thesis by A4,A11;
end;
cluster subcommutative -> confluent for Relation;
coherence
proof
let R be Relation;
assume R is subcommutative;
then for a,b,c being object st R reduces a,b & [a,c] in R holds b,c
are_convergent_wrt R by Th49;
hence thesis by Th51;
end;
cluster with_Church-Rosser_property -> with_NF_property for Relation;
coherence
proof
let R be Relation;
assume
A13: R is with_Church-Rosser_property;
let b,a be object;
assume
A14: b is_a_normal_form_wrt R;
assume b,a are_convertible_wrt R;
then b,a are_convergent_wrt R by A13;
then ex c being object st R reduces b,c & R reduces a,c;
hence thesis by A14,Th33;
end;
cluster with_NF_property -> with_UN_property for Relation;
coherence
by Th33;
cluster with_UN_property weakly-normalizing -> with_Church-Rosser_property
for Relation;
coherence
proof
let R be Relation such that
A15: for a,b being object st a is_a_normal_form_wrt R & b
is_a_normal_form_wrt R & a,b are_convertible_wrt R holds a = b and
A16: for a being object st a in field R holds a has_a_normal_form_wrt R;
let a,b be object;
assume
A17: R \/ R~ reduces a,b;
A18: field (R \/ R~) = (field R) \/ field (R~) by RELAT_1:18
.= (field R) \/ field R by RELAT_1:21
.= field R;
per cases;
suppose
a = b;
hence thesis by Th38;
end;
suppose
A19: a <> b;
then b in field R by A17,A18,Th18;
then b has_a_normal_form_wrt R by A16;
then consider b9 being object such that
A20: b9 is_a_normal_form_of b,R;
a in field R by A17,A18,A19,Th18;
then a has_a_normal_form_wrt R by A16;
then consider a9 being object such that
A21: a9 is_a_normal_form_of a,R;
A22: a9 is_a_normal_form_wrt R by A21;
A23: a,b are_convertible_wrt R by A17;
A24: R reduces a,a9 by A21;
then a9,a are_convertible_wrt R by Th25;
then
A25: a9,b are_convertible_wrt R by A23,Th30;
A26: b9 is_a_normal_form_wrt R by A20;
A27: R reduces b,b9 by A20;
then b,b9 are_convertible_wrt R by Th25;
then a9 = b9 by A15,A22,A26,A25,Th30;
hence thesis by A24,A27;
end;
end;
end;
registration
cluster empty -> subcommutative for Relation;
coherence;
end;
theorem Th53:
for R being with_UN_property Relation for a,b,c being object st
b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds b = c
proof
let R be with_UN_property Relation;
let a,b,c be object such that
A1: b is_a_normal_form_wrt R and
A2: R reduces a,b and
A3: c is_a_normal_form_wrt R and
A4: R reduces a,c;
b,c are_divergent_wrt R by A2,A4;
then b,c are_convertible_wrt R by Th37;
hence thesis by A1,A3,Def19;
end;
theorem Th54:
for R being with_UN_property weakly-normalizing Relation
for a being object holds nf(a,R) is_a_normal_form_of a,R
proof
let R be with_UN_property weakly-normalizing Relation;
let a be object;
a in field R or not a in field R;
then
A1: a has_a_normal_form_wrt R by Def14,Th46;
for b,c being object st b is_a_normal_form_of a,R & c is_a_normal_form_of a
,R holds b = c by Th53;
hence thesis by A1,Def12;
end;
theorem Th55:
for R being with_UN_property weakly-normalizing Relation
for a,b being object st a,b are_convertible_wrt R holds
nf(a,R) = nf(b,R)
proof
let R be with_UN_property weakly-normalizing Relation;
let a,b be object;
A1: nf(b,R) is_a_normal_form_of b,R by Th54;
then
A2: nf(b,R) is_a_normal_form_wrt R;
R reduces b,nf(b,R) by A1;
then
A3: b,nf(b,R) are_convertible_wrt R by Th25;
A4: nf(a,R) is_a_normal_form_of a,R by Th54;
then R reduces a,nf(a,R);
then
A5: nf(a,R),a are_convertible_wrt R by Th25;
assume a,b are_convertible_wrt R;
then nf(a,R),b are_convertible_wrt R by A5,Th30;
then
A6: nf(a,R),nf(b,R) are_convertible_wrt R by A3,Th30;
nf(a,R) is_a_normal_form_wrt R by A4;
hence thesis by A2,A6,Def19;
end;
registration
cluster strongly-normalizing locally-confluent -> confluent for Relation;
coherence
proof
let R be Relation;
assume
A1: R is strongly-normalizing;
defpred P[object] means
for b,c being object st R reduces $1,b & R reduces $1,c
holds b,c are_convergent_wrt R;
assume
A2: for a,b,c being object st [a,b] in R & [a,c] in R holds b,c
are_convergent_wrt R;
A3: for a being object st
for b being object st [a,b] in R & a <> b holds P[b] holds P[a]
proof
let a be object;
assume
A4: for b being object st [a,b] in R & a <> b holds P[b];
let b,c be object;
assume that
A5: R reduces a,b and
A6: R reduces a,c;
consider p being RedSequence of R such that
A7: a = p.1 and
A8: b = p.len p by A5;
A9: len p >= 0+1 by NAT_1:13;
consider q being RedSequence of R such that
A10: a = q.1 and
A11: c = q.len q by A6;
A12: len q >= 0+1 by NAT_1:13;
per cases;
suppose
len p = 1;
hence thesis by A6,A7,A8,Th36;
end;
suppose
len q = 1;
hence thesis by A5,A10,A11,Th36;
end;
suppose
A13: len p <> 1 & len q <> 1;
then len q > 1 by A12,XXREAL_0:1;
then
A14: 1+1 <= len q by NAT_1:13;
then
A15: 1+1 in dom q by Lm3;
len q in dom q by FINSEQ_5:6;
then
A16: R reduces q.2,c by A11,A14,A15,Th17;
len p > 1 by A9,A13,XXREAL_0:1;
then
A17: 1+1 <= len p by NAT_1:13;
then
A18: 1+1 in dom p by Lm3;
len p in dom p by FINSEQ_5:6;
then
A19: R reduces p.2,b by A8,A17,A18,Th17;
1 in dom p by A9,Lm3;
then
A20: [a,p.2] in R by A7,A18,Def2;
then
A21: a in field R by RELAT_1:15;
1 in dom q by A12,Lm3;
then
A22: [a,q.2] in R by A10,A15,Def2;
then p.2,q.2 are_convergent_wrt R by A2,A20;
then consider d being object such that
A23: R reduces p.2,d and
A24: R reduces q.2,d;
A25: R is_irreflexive_in field R by A1,RELAT_2:def 10;
then
A26: a <> q.2 by A22,A21;
a <> p.2 by A20,A21,A25;
then b,d are_convergent_wrt R by A4,A20,A23,A19;
then consider e being object such that
A27: R reduces b,e and
A28: R reduces d,e;
R reduces q.2,e by A24,A28,Th16;
then e,c are_convergent_wrt R by A4,A22,A26,A16;
hence thesis by A27,Th42;
end;
end;
A29: R is co-well_founded by A1;
A30: for a being object st a in field R holds P[a] from coNoetherianInduction
(A29,A3);
given a0,b0 being object such that
A31: a0,b0 are_divergent_wrt R and
A32: not a0,b0 are_convergent_wrt R;
consider c0 being object such that
A33: R reduces c0,a0 & R reduces c0,b0 by A31;
a0 <> c0 or b0 <> c0 by A32,Th38;
then c0 in field R by A33,Th18;
hence thesis by A32,A33,A30;
end;
end;
definition
let R be Relation;
attr R is complete means
R is confluent strongly-normalizing;
end;
registration
cluster complete -> confluent strongly-normalizing for Relation;
coherence;
cluster confluent strongly-normalizing -> complete for Relation;
coherence;
end;
registration
cluster complete for non empty Relation;
existence
proof
reconsider R = {[0,1]} as non empty Relation;
take R;
A1: field R = {0,1} by RELAT_1:17;
thus R is confluent
proof
let a,b be object;
given c being object such that
A2: R reduces c,a and
A3: R reduces c,b;
per cases;
suppose
a = b;
hence thesis by Th38;
end;
suppose
a <> b;
then a <> c or b <> c;
then
A4: c in field R by A2,A3,Th18;
then a in {0,1} by A1,A2,Th18;
then
A5: a = 0 or a = 1 by TARSKI:def 2;
b in {0,1} by A1,A3,A4,Th18;
then
A6: b = 0 or b = 1 by TARSKI:def 2;
[0,1] in R by TARSKI:def 1;
then
A7: R reduces 0,1 by Th15;
R reduces 1,1 by Th12;
hence thesis by A5,A6,A7;
end;
end;
A8: R is co-well_founded
proof
let Y be set;
assume that
A9: Y c= field R and
A10: Y <> {};
reconsider Y9 = Y as non empty set by A10;
set y = the Element of Y9;
per cases;
suppose
A11: 1 in Y;
take 1;
thus 1 in Y by A11;
let b be object;
assume that
b in Y and
1 <> b;
[0,1] <> [1,b] by XTUPLE_0:1;
hence thesis by TARSKI:def 1;
end;
suppose
A12: not 1 in Y & y in Y;
take 0;
thus 0 in Y by A1,A9,A12,TARSKI:def 2;
let b be object;
assume b in Y;
hence thesis by A1,A9,A12,TARSKI:def 2;
end;
end;
R is irreflexive
proof
let x be object;
assume that
x in field R and
A13: [x,x] in R;
A14: [x,x] = [0,1] by A13,TARSKI:def 1;
then x = 0 by XTUPLE_0:1;
hence contradiction by A14,XTUPLE_0:1;
end;
hence thesis by A8;
end;
end;
theorem
for R,Q being with_Church-Rosser_property Relation st
R commutes_with Q holds R \/ Q is with_Church-Rosser_property
proof
let R,Q be with_Church-Rosser_property Relation;
assume
A1: R commutes_with Q;
R \/ Q is confluent
proof
let a,b be object;
given c being object such that
A2: R \/ Q reduces c,a and
A3: R \/ Q reduces c,b;
consider p being RedSequence of R \/ Q such that
A4: c = p.1 and
A5: a = p.len p by A2;
defpred Z[Nat] means $1 in dom p implies p.$1,b
are_convergent_wrt R \/ Q;
now
let i be Nat such that
A6: i in dom p implies p.i,b are_convergent_wrt R \/ Q and
A7: i+1 in dom p;
per cases;
suppose
i = 0;
hence p.(i+1),b are_convergent_wrt R \/ Q by A3,A4,Th36;
end;
suppose
A8: i > 0;
A9: i < len p by A7,Lm2;
then consider d being object such that
A10: R \/ Q reduces p.i,d and
A11: R \/ Q reduces b,d by A6,A8,Lm3;
consider q being RedSequence of R \/ Q such that
A12: p.i = q.1 and
A13: d = q.len q by A10;
defpred P[Nat] means $1 in dom q implies
ex e being object st
R \/ Q reduces p.(i+1),e & (R reduces q.$1,e or Q reduces q.$1,e);
i in dom p by A8,A9,Lm3;
then [p.i,p.(i+1)] in R \/ Q by A7,Def2;
then
A14: [p.i,p.(i+1)] in R or [p.i,p.(i+1)] in Q by XBOOLE_0:def 3;
now
let j be Nat such that
A15: j in dom q implies ex e being object st R \/ Q reduces p.(i+1)
,e & (R reduces q.j,e or Q reduces q.j,e) and
A16: j+1 in dom q;
A17: j < len q by A16,Lm2;
per cases;
suppose
A18: j = 0;
A19: R \/ Q reduces p.(i+1),p.(i+1) by Th12;
R reduces q.(j+1),p.(i+1) or Q reduces q.(j+1),p.(i+1) by A12,A14
,A18,Th15;
hence
ex e being object st R \/ Q reduces p.(i+1),e & (R reduces q.(j+
1),e or Q reduces q.(j+1),e) by A19;
end;
suppose
A20: j > 0;
then consider e being object such that
A21: R \/ Q reduces p.(i+1),e and
A22: R reduces q.j,e or Q reduces q.j,e by A15,A17,Lm3;
A23: now
assume R reduces q.j,q.(j+1) & Q reduces q.j,e;
then consider x being object such that
A24: Q reduces q.(j+1),x and
A25: R reduces e,x by A1;
take x;
R \/ Q reduces e,x by A25,Th22,XBOOLE_1:7;
hence R \/ Q reduces p.(i+1),x & (R reduces q.(j+1),x or Q
reduces q.(j+1),x) by A21,A24,Th16;
end;
A26: now
assume Q reduces q.j,q.(j+1) & Q reduces q.j,e;
then e,q.(j+1) are_divergent_wrt Q;
then e,q.(j+1) are_convergent_wrt Q by Def22;
then consider x being object such that
A27: Q reduces e,x and
A28: Q reduces q.(j+1),x;
take x;
R \/ Q reduces e,x by A27,Th22,XBOOLE_1:7;
hence R \/ Q reduces p.(i+1),x & (R reduces q.(j+1),x or Q
reduces q.(j+1),x) by A21,A28,Th16;
end;
A29: now
assume R reduces q.j,q.(j+1) & R reduces q.j,e;
then e,q.(j+1) are_divergent_wrt R;
then e,q.(j+1) are_convergent_wrt R by Def22;
then consider x being object such that
A30: R reduces e,x and
A31: R reduces q.(j+1),x;
take x;
R \/ Q reduces e,x by A30,Th22,XBOOLE_1:7;
hence R \/ Q reduces p.(i+1),x & (R reduces q.(j+1),x or Q
reduces q.(j+1),x) by A21,A31,Th16;
end;
A32: now
assume Q reduces q.j,q.(j+1) & R reduces q.j,e;
then consider x being object such that
A33: R reduces q.(j+1),x and
A34: Q reduces e,x by A1,Def18;
take x;
R \/ Q reduces e,x by A34,Th22,XBOOLE_1:7;
hence R \/ Q reduces p.(i+1),x & (R reduces q.(j+1),x or Q
reduces q.(j+1),x) by A21,A33,Th16;
end;
j in dom q by A17,A20,Lm3;
then [q.j,q.(j+1)] in R \/ Q by A16,Def2;
then [q.j,q.(j+1)] in R or [q.j,q.(j+1)] in Q by XBOOLE_0:def 3;
hence
ex e being object st R \/ Q reduces p.(i+1),e & (R reduces q.(j+
1),e or Q reduces q.(j+1),e) by A22,A29,A26,A23,A32,Th15;
end;
end;
then
A35: for k being Nat st P[k] holds P[k+1];
A36: P[ 0 ] by Lm1;
A37: for j being Nat holds P[j] from NAT_1:sch 2(A36,A35);
thus p.(i+1),b are_convergent_wrt R \/ Q
proof
len q in dom q by FINSEQ_5:6;
then consider e being object such that
A38: R \/ Q reduces p.(i+1),e and
A39: R reduces d,e or Q reduces d,e by A13,A37;
take e;
R \/ Q reduces d,e by A39,Th22,XBOOLE_1:7;
hence thesis by A11,A38,Th16;
end;
end;
end;
then
A40: for k being Nat st Z[k] holds Z[k+1];
A41: len p in dom p by FINSEQ_5:6;
A42: Z[ 0 ] by Lm1;
for i being Nat holds Z[i] from NAT_1:sch 2(A42,A40);
hence thesis by A5,A41;
end;
hence thesis;
end;
theorem
for R being Relation holds R is confluent iff R[*] is locally-confluent
proof
let R be Relation;
hereby
assume
A1: R is confluent;
thus R[*] is locally-confluent
proof
let a,b,c be object;
assume [a,b] in R[*] & [a,c] in R[*];
then R reduces a,b & R reduces a,c by Th20;
then b,c are_divergent_wrt R;
then b,c are_convergent_wrt R by A1;
then consider d being object such that
A2: R reduces b,d & R reduces c,d;
take d;
thus thesis by A2,Th21;
end;
end;
assume
A3: for a,b,c being object st [a,b] in R[*] & [a,c] in R[*] holds b,c
are_convergent_wrt R[*];
let a,b be object;
given c being object such that
A4: R reduces c,a and
A5: R reduces c,b;
A6: [c,b] in R[*] or c = b by A5,Th20;
[c,a] in R[*] or c = a by A4,Th20;
then a,b are_convergent_wrt R[*] or R[*] reduces a,b or R[*] reduces b,a by
A3,A6,Th15,Th38;
then a,b are_convergent_wrt R[*] by Th36;
then consider d being object such that
A7: R[*] reduces a,d & R[*] reduces b,d;
take d;
thus thesis by A7,Th21;
end;
theorem
for R being Relation holds R is confluent iff R[*] is subcommutative
proof
let R be Relation;
hereby
assume
A1: R is confluent;
thus R[*] is subcommutative
proof
let a,b,c be object;
assume [a,b] in R[*] & [a,c] in R[*];
then R reduces a,b & R reduces a,c by Th20;
then b,c are_divergent_wrt R;
then b,c are_convergent_wrt R by A1;
then consider d being object such that
A2: R reduces b,d & R reduces c,d;
take d;
thus thesis by A2,Th20;
end;
end;
assume
A3: for a,b,c being object st [a,b] in R[*] & [a,c] in R[*] holds b,c
are_convergent<=1_wrt R[*];
let a,b be object;
given c being object such that
A4: R reduces c,a and
A5: R reduces c,b;
A6: [c,b] in R[*] or c = b by A5,Th20;
[c,a] in R[*] or c = a by A4,Th20;
then a,b are_convergent<=1_wrt R[*] by A3,A6;
then a,b are_convergent_wrt R[*] by Th44;
then consider d being object such that
A7: R[*] reduces a,d & R[*] reduces b,d;
take d;
thus thesis by A7,Th21;
end;
begin :: Completion method
definition
let R,Q be Relation;
pred R,Q are_equivalent means
for a,b being object holds
a,b are_convertible_wrt R iff a,b are_convertible_wrt Q;
symmetry;
end;
definition
let R be Relation;
let a,b be object;
pred a,b are_critical_wrt R means
a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R;
end;
theorem Th59:
for R being Relation, a,b being object st a,b are_critical_wrt R
holds a,b are_convertible_wrt R by Th37,Th45;
theorem
for R being Relation st not ex a,b being object st a,b are_critical_wrt R
holds R is locally-confluent
proof
let R be Relation such that
A1: not ex a,b being object st a,b are_critical_wrt R;
let a,b,c be object;
assume [a,b] in R & [a,c] in R;
then
A2: b,c are_divergent<=1_wrt R;
not b,c are_critical_wrt R by A1;
hence thesis by A2;
end;
theorem
for R,Q being Relation st for a,b being object st [a,b] in Q holds
a,b are_critical_wrt R holds R, R \/ Q are_equivalent
proof
let R,Q be Relation;
assume
A1: for a,b being object st [a,b] in Q holds a,b are_critical_wrt R;
let a,b be object;
A2: R c= R \/ Q by XBOOLE_1:7;
A3: R~ c= (R \/ Q)~
proof
let x,y be object;
assume [x,y] in R~;
then [y,x] in R by RELAT_1:def 7;
hence thesis by A2,RELAT_1:def 7;
end;
thus a,b are_convertible_wrt R implies
a,b are_convertible_wrt R \/ Q by A2,A3,Th22,XBOOLE_1:13;
given p being RedSequence of (R \/ Q) \/ (R \/ Q)~ such that
A4: a = p.1 and
A5: b = p.len p;
defpred Z[Nat] means $1 in dom p implies a,p.$1
are_convertible_wrt R;
now
let i be Nat such that
A6: i in dom p implies a,p.i are_convertible_wrt R and
A7: i+1 in dom p;
A8: i < len p by A7,Lm2;
per cases;
suppose
i = 0;
hence a,p.(i+1) are_convertible_wrt R by A4,Th26;
end;
suppose
A9: i > 0;
then i in dom p by A8,Lm3;
then [p.i,p.(i+1)] in (R \/ Q) \/ (R \/ Q)~ by A7,Def2;
then [p.i,p.(i+1)] in R \/ Q or [p.i,p.(i+1)] in (R \/ Q)~ by
XBOOLE_0:def 3;
then [p.i,p.(i+1)] in R \/ Q or [p.(i+1),p.i] in R \/ Q by RELAT_1:def 7;
then
[p.i,p.(i+1)] in R or [p.i,p.(i+1)] in Q or [p.(i+1),p.i] in R or [
p.(i+1),p.i] in Q by XBOOLE_0:def 3;
then p.i,p.(i+1) are_convertible_wrt R or p.(i+1),p.i
are_convertible_wrt R by A1,Th29,Th59;
then p.i,p.(i+1) are_convertible_wrt R by Lm5;
hence a,p.(i+1) are_convertible_wrt R by A6,A8,A9,Lm3,Th30;
end;
end;
then
A10: for k being Nat st Z[k] holds Z[k+1];
A11: len p in dom p by FINSEQ_5:6;
A12: Z[ 0 ] by Lm1;
for i being Nat holds Z[i] from NAT_1:sch 2(A12,A10);
hence thesis by A5,A11;
end;
theorem Th62:
for R being Relation ex Q being complete Relation st
field Q c= field R & for a,b being object holds
a,b are_convertible_wrt R iff a,b are_convergent_wrt Q
proof
let R be Relation;
per cases;
suppose
A1: R = {};
take E = {};
thus field E c= field R;
let a,b be object;
a,b are_convertible_wrt R iff a = b by A1,Th26,Th27;
hence thesis by Th38,Th39;
end;
suppose
R <> {};
then reconsider R9 = R as non empty Relation;
set xx = the Element of R9;
consider x1,x2 being object such that
A2: xx = [x1,x2] by RELAT_1:def 1;
defpred P[object,object] means $1,$2 are_convertible_wrt R;
A3: for x,y being object st P[x,y] holds P[y,x] by Lm5;
A4: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] by Th30;
A5: for x being object st x in field R holds P[x,x] by Th26;
consider Q being Equivalence_Relation of field R such that
A6: for x,y being object
holds [x,y] in Q iff x in field R & y in field R & P[x,y]
from EQREL_1:sch 1(A5,A3,A4);
A7: ( for X being set st X in Class Q holds X <> {})& for X,Y being set
st X in Class Q & Y in Class Q & X <> Y holds X misses Y by EQREL_1:def 4;
x1 in field R by A2,RELAT_1:15;
then Class(Q,x1) in Class Q by EQREL_1:def 3;
then consider X being set such that
A8: for A being set st A in Class Q ex x st X /\ A = {x} by A7,WELLORD2:18;
defpred Z[object,object] means
$1 <> $2 & $1,$2 are_convertible_wrt R & $2 in X;
consider P being Relation such that
A9: for x,y being object
holds [x,y] in P iff x in field R & y in field R & Z[x,y]
from RELAT_1:sch 1;
A10: P is locally-confluent
proof
let a,b,c be object;
assume that
A11: [a,b] in P and
A12: [a,c] in P;
A13: a in field R by A9,A11;
then Class(Q,a) in Class Q by EQREL_1:def 3;
then consider x such that
A14: X /\ Class(Q,a) = {x} by A8;
c in field R & a,c are_convertible_wrt R by A9,A12;
then [a,c] in Q by A6,A13;
then [c,a] in Q by EQREL_1:6;
then
A15: c in Class(Q,a) by EQREL_1:19;
c in X by A9,A12;
then c in {x} by A15,A14,XBOOLE_0:def 4;
then
A16: c = x by TARSKI:def 1;
b in field R & a,b are_convertible_wrt R by A9,A11;
then [a,b] in Q by A6,A13;
then [b,a] in Q by EQREL_1:6;
then
A17: b in Class(Q,a) by EQREL_1:19;
take b;
b in X by A9,A11;
then b in {x} by A17,A14,XBOOLE_0:def 4;
then b = x by TARSKI:def 1;
hence thesis by A16,Th12;
end;
A18: for x,y st P reduces x,y holds x,y are_convertible_wrt R
proof
let x,y;
given p being RedSequence of P such that
A19: x = p.1 and
A20: y = p.len p;
defpred Z[Nat] means $1 in dom p implies x,p.$1
are_convertible_wrt R;
now
let i be Nat such that
A21: i in dom p implies x,p.i are_convertible_wrt R and
A22: i+1 in dom p;
A23: i < len p by A22,Lm2;
per cases;
suppose
i = 0;
hence x,p.(i+1) are_convertible_wrt R by A19,Th26;
end;
suppose
A24: i > 0;
then i in dom p by A23,Lm3;
then [p.i,p.(i+1)] in P by A22,Def2;
then p.i,p.(i+1) are_convertible_wrt R by A9;
hence x,p.(i+1) are_convertible_wrt R by A21,A23,A24,Lm3,Th30;
end;
end;
then
A25: for k being Nat st Z[k] holds Z[k+1];
A26: len p in dom p by FINSEQ_5:6;
A27: Z[ 0 ] by Lm1;
for i being Nat holds Z[i] from NAT_1:sch 2(A27,A25);
hence thesis by A20,A26;
end;
P is strongly-normalizing
proof
let f be ManySortedSet of NAT;
per cases;
suppose
not [f.0,f.(0+1)] in P;
hence thesis;
end;
suppose
A28: [f.0,f.(0+1)] in P;
take j = 0+1;
A29: f.j in X by A9,A28;
assume
A30: [f.j,f.(j+1)] in P;
then
A31: f.j in field R by A9;
then Class(Q,f.j) in Class Q by EQREL_1:def 3;
then consider x such that
A32: X /\ Class(Q,f.j) = {x} by A8;
f.(j+1) in field R & f.j,f.(j+1) are_convertible_wrt R by A9,A30;
then [f.j,f.(j+1)] in Q by A6,A31;
then [f.(j+1),f.j] in Q by EQREL_1:6;
then
A33: f.(j+1) in Class(Q,f.j) by EQREL_1:19;
f.j in Class(Q,f.j) by A31,EQREL_1:20;
then f.j in X /\ Class(Q,f.j) by A29,XBOOLE_0:def 4;
then
A34: f.j = x by A32,TARSKI:def 1;
f.(j+1) in X by A9,A30;
then f.(j+1) in X /\ Class(Q,f.j) by A33,XBOOLE_0:def 4;
then f.(j+1) = x by A32,TARSKI:def 1;
hence contradiction by A9,A30,A34;
end;
end;
then reconsider P as strongly-normalizing locally-confluent Relation by A10
;
take P;
thus field P c= field R
proof
let x be object;
assume x in field P;
then x in dom P or x in rng P by XBOOLE_0:def 3;
then (ex y being object st [x,y] in P) or
ex y being object st [y,x] in P by XTUPLE_0:def 12,def 13;
hence thesis by A9;
end;
let a,b be object;
thus thesis
proof
per cases;
suppose
a = b;
hence thesis by Th26,Th38;
end;
suppose
A35: a <> b;
hereby
assume
A36: a,b are_convertible_wrt R;
then
A37: b in field R by A35,Th32;
then Class(Q,b) in Class Q by EQREL_1:def 3;
then consider x such that
A38: X /\ Class(Q,b) = {x} by A8;
A39: a in field R by A35,A36,Th32;
then
A40: [a,b] in Q by A6,A36,A37;
thus a,b are_convergent_wrt P
proof
take x;
A41: x in {x} by TARSKI:def 1;
then
A42: x in X by A38,XBOOLE_0:def 4;
A43: x in Class(Q,b) by A38,A41,XBOOLE_0:def 4;
then [x,b] in Q by EQREL_1:19;
then [b,x] in Q by EQREL_1:6;
then b,x are_convertible_wrt R by A6;
then
A44: b = x or [b,x] in P by A9,A37,A38,A41,A42;
a in Class(Q,b) by A40,EQREL_1:19;
then [a,x] in Q by A43,EQREL_1:22;
then a,x are_convertible_wrt R by A6;
then a = x or [a,x] in P by A9,A39,A38,A41,A42;
hence thesis by A44,Th12,Th15;
end;
end;
given c being object such that
A45: P reduces a,c & P reduces b,c;
a,c are_convertible_wrt R & c,b are_convertible_wrt R by A18,A45,Lm5;
hence thesis by Th30;
end;
end;
end;
end;
definition
let R be Relation;
mode Completion of R -> complete Relation means :Def28:
for a,b being object
holds a,b are_convertible_wrt R iff a,b are_convergent_wrt it;
existence
proof
ex Q being complete Relation st field Q c= field R &
for a,b being object
holds a,b are_convertible_wrt R iff a,b are_convergent_wrt Q by Th62;
hence thesis;
end;
end;
theorem
for R being Relation, C being Completion of R holds R,C are_equivalent
proof
let R be Relation, C be Completion of R, a,b be object;
a,b are_convertible_wrt R iff a,b are_convergent_wrt C by Def28;
hence thesis by Def23,Th37;
end;
theorem
for R being Relation, Q being complete Relation st R,Q are_equivalent
holds Q is Completion of R
proof
let R be Relation, Q be complete Relation such that
A1: for a,b being object holds a,b are_convertible_wrt R iff a,b
are_convertible_wrt Q;
let a,b be object;
a,b are_convertible_wrt R iff a,b are_convertible_wrt Q by A1;
hence thesis by Def23,Th37;
end;
theorem
for R being Relation, C being Completion of R, a,b being object holds
a,b are_convertible_wrt R iff nf(a,C) = nf(b,C)
proof
let R be Relation, C be Completion of R, a,b be object;
nf(a,C) is_a_normal_form_of a,C by Th54;
then
A1: C reduces a,nf(a,C);
a,b are_convergent_wrt C implies a,b are_convertible_wrt C by Th37;
hence a,b are_convertible_wrt R implies nf(a,C) = nf(b,C) by Def28,Th55;
nf(b,C) is_a_normal_form_of b,C by Th54;
then
A2: C reduces b,nf(b,C);
a,b are_convertible_wrt R iff a,b are_convergent_wrt C by Def28;
hence thesis by A1,A2;
end;
:: added, SK 17.11.2024
theorem
for p,q being FinSequence st p <> {} & q <> {}
holds len(p$^q) + 1 = len p + len q
proof
let p,q be FinSequence;
assume p <> {} & q <> {};
then consider i being Nat, r being FinSequence such that
A1: len p = i + 1 & r = p|Seg i & p$^q = r^q by Def1;
A2: i <= len p by A1, NAT_1:11;
thus len(p$^q) + 1 = len r + len q + 1 by A1, FINSEQ_1:22
.= i + len q + 1 by A1, A2, FINSEQ_1:17
.= len p + len q by A1;
end;