Copyright (c) 1995 Association of Mizar Users
environ
vocabulary FINSEQ_1, BOOLE, RELAT_1, FUNCT_1, FINSEQ_5, ARYTM_1, WELLORD1,
PBOOLE, RELAT_2, FUNCOP_1, BHSP_3, ISOCAT_1, EQREL_1, REWRITE1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
FUNCT_1, RELAT_1, RELAT_2, WELLORD1, EQREL_1, FUNCOP_1, FINSEQ_1, PBOOLE,
FINSEQ_5, LANG1;
constructors NAT_1, WELLORD1, EQREL_1, FUNCOP_1, PBOOLE, FINSEQ_5, LANG1,
XREAL_0, MEMBERED, PARTFUN1, TOLER_1, RELAT_1, RELAT_2, RELSET_1;
clusters SUBSET_1, RELAT_1, FINSEQ_1, XREAL_0, FUNCOP_1, ARYTM_3, MEMBERED,
NUMBERS, ORDINAL2, EQREL_1, TOLER_1, PARTFUN1, RELSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_1, RELAT_2, WELLORD1;
theorems TARSKI, AXIOMS, ZFMISC_1, REAL_1, NAT_1, WELLORD1, RELAT_1, RELAT_2,
FUNCT_1, FUNCOP_1, PBOOLE, FINSEQ_1, TOLER_1, TREES_1, FINSEQ_5, LANG1,
EQREL_1, WELLORD2, XBOOLE_0, XBOOLE_1, XCMPLX_1;
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 p <> {} & q <> {};
then len p <> 0 & len p >= 0 by FINSEQ_1:25,NAT_1:18;
then len p >= 0+1 by NAT_1:38;
then consider i being Nat such that
A1: len p = 1+i by NAT_1:28;
reconsider r = p|Seg i as FinSequence by FINSEQ_1:19;
take r^q, i, r;
thus thesis by A1;
end;
uniqueness by XCMPLX_1:2;
consistency;
end;
Lm1:
now let p be FinSequence, x be Nat;
assume x in dom p;
then x in Seg len p by FINSEQ_1:def 3;
hence x <= len p & x >= 0+1 by FINSEQ_1:3;
hence x > 0 by NAT_1:38;
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:38;
end;
Lm3:
now let p be FinSequence, x be Nat;
assume (x <= len p or x < len p) & (x >= 1 or x > 0);
then x <= len p & x >= 0+1 by NAT_1:38;
then x in Seg len p by FINSEQ_1:3;
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 & x+1 >= 1 by NAT_1:29,38;
hence x+1 in dom p by Lm3;
end;
reserve p,q,r for FinSequence, x,y for set;
theorem
{}$^p = p & p$^{} = p
proof {}^p = p & p^{} = p by FINSEQ_1:47;
hence thesis by Def1;
end;
theorem Th2:
q <> {} implies (p^<*x*>)$^q = p^q
proof assume
A1: q <> {};
<*x*> <> {} by TREES_1:4;
then p^<*x*> <> {} by FINSEQ_1:48;
then consider i being Nat, r being FinSequence such that
A2: len (p^<*x*>) = i+1 & r = (p^<*x*>)|Seg i & (p^<*x*>)$^q = r^q by A1,Def1;
consider s being FinSequence such that
A3: p^<*x*> = r^s by A2,TREES_1:3;
len <*x*> = 1 by FINSEQ_1:57;
then len (p^<*x*>) = len p + 1 by FINSEQ_1:35;
then A4: len p = i & i <= i+1 by A2,NAT_1:29,XCMPLX_1:2;
then A5: len r = i by A2,FINSEQ_1:21;
then consider t being FinSequence such that
A6: p^t = r by A3,A4,FINSEQ_1:64;
len r + 0 = len p + len t by A6,FINSEQ_1:35;
then len t = 0 by A4,A5,XCMPLX_1:2;
then t = {} by FINSEQ_1:25;
hence thesis by A2,A6,FINSEQ_1:47;
end;
theorem
(p^<*x*>)$^(<*y*>^q) = p^<*y*>^q
proof <*y*> <> {} by TREES_1:4;
then <*y*>^q <> {} & p^<*y*>^q = p^(<*y*>^q) by FINSEQ_1:45,48;
hence thesis by Th2;
end;
theorem
q <> {} implies <*x*>$^q = q
proof {}^<*x*> = <*x*> & {}^q = q by FINSEQ_1:47;
hence thesis by Th2;
end;
theorem
p <> {} implies ex x,q st p = <*x*>^q & len p = len q+1
proof assume
A1: p <> {};
defpred P[Nat] means
for p st p <> {} & len p = $1 ex x,q st p = <*x*>^q & len p = len q+1;
A2: P[0] by FINSEQ_1:25;
A3: for i be Nat st P[i] holds P[i+1]
proof
now let i be Nat; assume
A4: for p st p <> {} & len p = i ex x,q st p = <*x*>^q & len p = len q+1;
let p; assume
A5: p <> {} & len p = i+1;
then consider q,y such that
A6: p = q^<*y*> by FINSEQ_1:63;
A7: len <*y*> = 1 & len p = len q+len <*y*> by A6,FINSEQ_1:35,56;
then A8: len q = i by A5,XCMPLX_1:2;
per cases; suppose
A9: q = {};
then p = <*y*> by A6,FINSEQ_1:47 .= <*y*>^{} by FINSEQ_1:47;
hence ex x,q st p = <*x*>^q & len p = len q+1 by A7,A9;
suppose q <> {}; then consider x,r such that
A10: q = <*x*>^r & len q = len r+1 by A4,A8;
p = <*x*>^(r^<*y*>) & len (r^<*y*>) = len r+1 & len <*x*> = 1
by A6,A7,A10,FINSEQ_1:35,45,56;
hence ex x,q st p = <*x*>^q & len p = len q+1 by A7,A10;
end;
hence thesis;
end;
for i being Nat holds P[i] from Ind(A2,A3);
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
proof let i be Nat; assume
A4: i in dom (p()$^q()) & i+1 in dom (p()$^q());
then A5: i >= 0+1 by Lm1;
A6: i+1 >= 1 by NAT_1:29;
0+1 <= len q() by A3,NAT_1:38;
then A7: 1 in Seg len q() & Seg len q() = dom q() by FINSEQ_1:3,def 3;
let x,y be set; assume
A8: x = (p()$^q()).i & y = (p()$^q()).(i+1);
A9: p() <> {} & q() <> {} by A3,FINSEQ_1:25;
then consider r being FinSequence, a being set such that
A10: p() = r^<*a*> by FINSEQ_1:63;
A11: p()$^q() = r^q() by A9,A10,Th2;
A12: len p() = len r + len <*a*> by A10,FINSEQ_1:35 .= len r + 1 by FINSEQ_1:
57;
per cases;
suppose
A13: i < len p();
then i in dom p() & i+1 in dom p() by A5,Lm3,Lm4;
then A14: P[p().i, p().(i+1)] by A1;
A15: i <= len r by A12,A13,NAT_1:38;
then i in Seg len r by A5,FINSEQ_1:3;
then i in dom r by FINSEQ_1:def 3;
then A16: x = r.i & r.i = p().i by A8,A10,A11,FINSEQ_1:def 7;
A17: now assume i+1 <= len r;
then i+1 in Seg len r by A6,FINSEQ_1:3;
then i+1 in dom r by FINSEQ_1:def 3;
hence y = r.(i+1) & r.(i+1) = p().(i+1) by A8,A10,A11,FINSEQ_1:def 7;
end;
i = len r or i < len r by A15,REAL_1:def 5;
hence thesis by A3,A7,A8,A11,A12,A14,A16,A17,FINSEQ_1:def 7,NAT_1:38;
suppose i >= len p();
then consider k being Nat such that
A18: i = len p()+k by NAT_1:28;
A19: len (p()$^q()) = len r + len q() & i = len r+(1+k) &
i < len (p()$^q()) & len r+(1+k)+1 = len r+(k+1+1)
by A4,A11,A12,A18,Lm2,FINSEQ_1:35,XCMPLX_1:1;
then k+1 < len q() & k+1 >= 1 by NAT_1:29,REAL_1:55;
then A20: k+1 in dom q() & k+1+1 in dom q() & k+1<>0 by Lm3,Lm4;
then x = q().(k+1) & y = q().(k+1+1) & k+1 > 0
by A8,A11,A19,FINSEQ_1:def 7,NAT_1:19;
hence thesis by A2,A20;
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 consider x being set;
take p = <*x*>;
A1: dom p = {1} & len p = 1 by FINSEQ_1:4,55,57;
hence len p > 0;
let i be Nat; assume i in dom p & i+1 in dom p;
then i = 1 & i+1 = 1 by A1,TARSKI:def 1;
hence thesis;
end;
end;
definition
let R be Relation;
cluster -> non empty RedSequence of R;
coherence
proof let p be RedSequence of R; len p > 0 by Def2;
hence thesis by FINSEQ_1:25;
end;
end;
canceled;
theorem Th7:
for R being Relation, a being set holds <*a*> is RedSequence of R
proof let R be Relation, a be set; set p = <*a*>;
A1: dom p = {1} & len p = 1 by FINSEQ_1:4,55,57;
hence len p > 0;
let i be Nat; assume i in dom p & i+1 in dom p;
then i = 1 & i+1 = 1 by A1,TARSKI:def 1;
hence thesis;
end;
theorem Th8:
for R being Relation, a,b being set st [a,b] in R holds
<*a,b*> is RedSequence of R
proof let R be Relation, a,b be set; assume
A1: [a,b] in R; set p = <*a,b*>;
A2: len p = 1+1 & dom p = Seg len p by FINSEQ_1:61,def 3;
hence len p > 0;
A3: p.1 = a & p.len p = b by A2,FINSEQ_1:61;
let i be Nat; assume i in dom p & i+1 in dom p;
then i >= 1 & i+1 <= 1+1 by A2,Lm1;
then i <= 1 & i >= 1 by REAL_1:53;
then i = 1 by AXIOMS:21;
hence thesis by A1,A3,FINSEQ_1:61;
end;
theorem Th9:
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;
A1: for i being Nat st i in dom p & i+1 in dom p holds P[p.i, p.(i+1)]
by Def2;
A2: for i being Nat st i in dom q & i+1 in dom q holds P[q.i, q.(i+1)]
by Def2;
assume p.len p = q.1;
then A3: len p > 0 & len q > 0 & p.len p = q.1 by Def2;
set r = p$^q;
consider p1 being FinSequence, x being set such that
A4: p = p1^<*x*> by FINSEQ_1:63;
r = p1^q by A4,Th2;
then len r = len p1+len q by FINSEQ_1:35;
then len r > len p1+0 & len p1+0 >= 0 by A3,NAT_1:18,REAL_1:67;
hence len r > 0;
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(A1,A2,A3);
hence thesis;
end;
theorem Th10:
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;
A1: len p > 0 &
for i being Nat st i in dom p & i+1 in dom p holds [p.i, p.(i+1)] in R
by Def2;
A2: len Rev p = len p by FINSEQ_5:def 3;
thus len Rev p > 0 by A1,FINSEQ_5:def 3;
A3: dom Rev p = Seg len p & dom p = Seg len p by A2,FINSEQ_1:def 3;
let i be Nat; assume
A4: i in dom Rev p & i+1 in dom Rev p;
then A5: (Rev p).i = p.(len p-i+1) & (Rev p).(i+1) = p.(len p-(i+1)+1)
by FINSEQ_5:def 3;
i <= len p & i+1 <= len p by A2,A4,Lm1;
then reconsider k = len p-(i+1)+1 as Nat by FINSEQ_5:1;
A6: k = len p-i-1+1 by XCMPLX_1:36 .= len p-i by XCMPLX_1:27;
then k+1 in dom p & k in dom p by A3,A4,FINSEQ_5:2;
then [p.k, p.(k+1)] in R by Def2;
hence thesis by A5,A6,RELAT_1:def 7;
end;
theorem Th11:
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 by Def2;
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 [p.i, p.(i+1)] in Q by A1;
end;
begin :: Reducibility, convertibility, and normal forms
definition
let R be Relation;
let a,b be set;
pred R reduces a,b means:
Def3:
ex p being RedSequence of R st p.1 = a & p.len p = b;
end;
definition
let R be Relation;
let a,b be set;
pred a,b are_convertible_wrt R means:
Def4:
R \/ R~ reduces a,b;
end;
theorem Th12:
for R being Relation, a,b being set 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 set;
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 & 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;
reconsider p as RedSequence of R by A2,Def2;
take p; thus thesis by A2;
end;
theorem Th13:
for R being Relation, a being set holds R reduces a,a
proof let R be Relation; let a be set;
reconsider p = <*a*> as RedSequence of R by Th7;
take p;
len p = 1 by FINSEQ_1:57;
hence p.1 = a & p.len p = a by FINSEQ_1:57;
end;
theorem Th14:
for a,b being set st {} reduces a,b holds a = b
proof let a,b be set; given p being RedSequence of {} such that
A1: p.1 = a & p.len p = b;
A2: len p > 0 &
for i being Nat st i in dom p & i+1 in dom p holds [p.i, p.(i+1)] in {}
by Def2;
now assume len p > 1;
then 1 in dom p & 1+1 in dom p by Lm3,Lm4;
hence contradiction by Def2;
end;
then len p <= 1 & len p >= 0+1 by A2,NAT_1:38;
hence thesis by A1,AXIOMS:21;
end;
theorem Th15:
for R being Relation, a,b being set st R reduces a,b & not a in field R
holds a = b
proof let R be Relation, a,b be set;
given p being RedSequence of R such that
A1: p.1 = a & p.len p = b;
A2: len p > 0 &
for i being Nat st i in dom p & i+1 in dom p holds [p.i, p.(i+1)] in R
by Def2;
assume
A3: not a in field R;
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:30;
end;
then len p <= 1 & len p >= 0+1 by A2,NAT_1:38;
hence thesis by A1,AXIOMS:21;
end;
theorem Th16:
for R being Relation, a,b being set st [a,b] in R holds R reduces a,b
proof let R be Relation, a,b be set; assume
[a,b] in R;
then reconsider p = <*a,b*> as RedSequence of R by Th8;
take p; len p = 2 by FINSEQ_1:61;
hence p.1 = a & p.len p = b by FINSEQ_1:61;
end;
theorem Th17:
for R being Relation, a,b,c being set st R reduces a,b & R reduces b,c
holds R reduces a,c
proof let R be Relation, a,b,c be set;
given p being RedSequence of R such that
A1: p.1 = a & p.len p = b;
given q being RedSequence of R such that
A2: q.1 = b & q.len q = c;
A3: len p > 0 & len q > 0 by Def2;
reconsider r = p$^q as RedSequence of R by A1,A2,Th9;
take r;
consider p1 being FinSequence, x being set such that
A4: p = p1^<*x*> by FINSEQ_1:63;
A5: r = p1^q by A4,Th2;
then A6: len r = len p1+len q by FINSEQ_1:35;
len p1 = 0 or len p1 > 0 by NAT_1:19;
then p1 = {} or len p1 >= 0+1 by FINSEQ_1:25,NAT_1:38;
then r = q & p = <*x*> or 1 in Seg len p1 by A4,A5,FINSEQ_1:3,47;
then 1 in dom p1 or len p = 1 & r = q by FINSEQ_1:57,def 3;
then r.1 = p1.1 & p1.1 = a or r.1 = b & b = a by A1,A2,A4,A5,FINSEQ_1:def 7
;
hence r.1 = a;
0+1 <= len q by A3,NAT_1:38;
then len q in Seg len q by FINSEQ_1:3;
then len q in dom q by FINSEQ_1:def 3;
hence r.len r = c by A2,A5,A6,FINSEQ_1:def 7;
end;
theorem Th18:
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
A1: i in dom p & j in dom p & i <= j;
A2: Q[0] by Th13;
A3: for k being Nat st Q[k] holds Q[k+1]
proof
now let j be Nat such that
A4: i+j in dom p implies R reduces p.i,p.(i+j) and
A5: i+(j+1) in dom p;
A6: i+(j+1) = i+j+1 by XCMPLX_1:1;
i <= i+j & i >= 1 by A1,Lm1,NAT_1:29;
then A7: i+j >= 1 & i+j < len p by A5,A6,Lm2,AXIOMS:22;
then i+j in dom p by Lm3;
then [p.(i+j),p.(i+(j+1))] in R by A5,A6,Def2;
then R reduces p.i,p.(i+j) & R reduces p.(i+j), p.(i+(j+1)) by A4,A7,Lm3,
Th16;
hence R reduces p.i,p.(i+(j+1)) by Th17;
end;
hence thesis;
end;
A8: for j being Nat holds Q[j] from Ind(A2,A3);
ex k being Nat st j = i+k by A1,NAT_1:28;
hence R reduces p.i,p.j by A1,A8;
end;
theorem Th19:
for R being Relation, a,b being set st R reduces a,b & a <> b
holds a in field R & b in field R
proof let R be Relation, a,b be set;
given p being RedSequence of R such that
A1: a = p.1 & b = p.len p;
assume
A2: a <> b;
len p > 0 by Def2;
then len p <> 1 & len p >= 0+1 by A1,A2,NAT_1:38;
then len p > 1 by REAL_1:def 5;
then 1 in dom p & 1+1 in dom p by Lm3,Lm4;
then A3: [a,p.2] in R by A1,Def2;
hence
a in field R by RELAT_1:30;
defpred P[Nat] means $1 in dom p implies p.$1 in field R;
A4: P[0] by Lm1;
A5: for k being Nat st P[k] holds P[k+1]
proof
now let i be Nat such that
i in dom p implies p.i in field R and
A6: i+1 in dom p;
A7: i < len p by A6,Lm2;
per cases by NAT_1:19; suppose i = 0; hence p.(i+1) in field R by A1,A3,
RELAT_1:30;
suppose i > 0;
then i in dom p by A7,Lm3;
then [p.i,p.(i+1)] in R by A6,Def2;
hence p.(i+1) in field R by RELAT_1:30;
end;
hence thesis;
end;
A8: for i being Nat holds P[i] from Ind(A4,A5);
len p in dom p by FINSEQ_5:6;
hence thesis by A1,A8;
end;
theorem Th20:
for R being Relation, a,b being set st R reduces a,b holds
a in field R iff b in field R
proof let R be Relation, a,b be set; assume
A1: R reduces a,b;
per cases; suppose a = b; hence thesis;
suppose a <> b;
thus thesis by A1,Th19;
end;
theorem Th21:
for R being Relation, a,b being set holds
R reduces a,b iff a = b or [a,b] in R*
proof let R be Relation, a,b be set;
hereby assume
A1: R reduces a,b;
then consider p being RedSequence of R such that
A2: a = p.1 & b = p.len p by Def3;
assume a <> b;
then A3: a in field R & b in field R by A1,Th19;
len p > 0 by Def2;
then A4: len p >= 0+1 by NAT_1:38;
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;
hence [a,b] in R* by A2,A3,A4,LANG1:def 13;
end;
assume
A5: (a = b or [a,b] in R*) & not R reduces a,b;
then consider p being FinSequence such that
A6: len p >= 1 & p.1 = a & p.(len p) = b and
A7: for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R
by Th13,LANG1:def 13;
p is RedSequence of R
proof 0+1 = 1; hence len p > 0 by A6,NAT_1:38;
let i be Nat; assume i in dom p & i+1 in dom p;
then i >= 1 & i < len p by Lm1,Lm2;
hence thesis by A7;
end;
hence contradiction by A5,A6,Def3;
end;
theorem Th22:
for R being Relation, a,b being set holds
R reduces a,b iff R* reduces a,b
proof let R be Relation, a,b be set;
R reduces a,b iff a = b or [a,b] in R* by Th21;
hence R reduces a,b implies R* reduces a,b by Th13,Th16;
given p being RedSequence of R* such that
A1: a = p.1 & b = p.len p;
defpred P[Nat] means $1 in dom p implies R reduces a,p.$1;
A2: P[0] by Lm1;
A3: for k being Nat st P[k] holds P[k+1]
proof
now let i be Nat such that
A4: i in dom p implies R reduces a,p.i and
A5: i+1 in dom p;
A6: i < len p by A5,Lm2;
per cases by NAT_1:19;
suppose i = 0; hence R reduces a,p.(i+1) by A1,Th13;
suppose A7: i > 0;
then i in dom p by A6,Lm3;
then [p.i,p.(i+1)] in R* by A5,Def2;
then R reduces a,p.i & R reduces p.i, p.(i+1) by A4,A6,A7,Lm3,Th21;
hence R reduces a,p.(i+1) by Th17;
end;
hence thesis;
end;
A8: for i being Nat holds P[i] from Ind(A2,A3);
len p in dom p by FINSEQ_5:6;
hence thesis by A1,A8;
end;
theorem Th23:
for R,Q being Relation st R c= Q for a,b being set 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 set; given p being RedSequence of R such that
A2: p.1 = a & p.len p = b;
p is RedSequence of Q by A1,Th11;
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 set holds
R reduces a,b iff R \/ id X reduces a,b
proof let R be Relation, X be set, a,b be set;
R c= R \/ id X by XBOOLE_1:7;
hence R reduces a,b implies R \/ id X reduces a,b by Th23;
given p being RedSequence of R \/ id X such that
A1: p.1 = a & p.len p = b;
len p > 0 by Def2;
then A2: len p in dom p by Lm3;
defpred P[Nat] means $1 in dom p implies R reduces a,p.$1;
A3: P[0] by Lm1;
A4: for k be Nat st P[k] holds P[k+1]
proof
now let i be Nat; assume
A5: i in dom p implies R reduces a,p.i; assume
A6: i+1 in dom p;
per cases;
suppose A7: i in dom p;
then [p.i, p.(i+1)] in R \/ id X & R reduces a,p.i by A5,A6,Def2;
then [p.i, p.(i+1)] in R or [p.i, p.(i+1)] in id X by XBOOLE_0:def 2;
then R reduces p.i, p.(i+1) or p.i = p.(i+1) by Th16,RELAT_1:def 10;
hence R reduces a, p.(i+1) by A5,A7,Th17;
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 & i >= 0 by NAT_1:18,38;
then i = 0;
hence R reduces a, p.(i+1) by A1,Th13;
end;
hence thesis;
end;
for i being Nat holds P[i] from Ind(A3,A4);
hence R reduces a,b by A1,A2;
end;
theorem Th25:
for R being Relation, a,b being set st R reduces a,b
holds R~ reduces b,a
proof let R be Relation, a,b be set; given p being RedSequence of R such that
A1: p.1 = a & p.len p = b;
reconsider q = Rev p as RedSequence of R~ by Th10;
take q;
A2: 1 in dom q & len q in dom q & len q = len p by FINSEQ_5:6,def 3;
hence q.1 = p.(len p-1+1) by FINSEQ_5:def 3 .= b by A1,XCMPLX_1:27;
thus q.(len q) = p.(len p-len p+1) by A2,FINSEQ_5:def 3
.= p.(0+1) by XCMPLX_1:14 .= a by A1;
end;
Lm5:for R being Relation, a,b being set st a,b are_convertible_wrt R
holds b,a are_convertible_wrt R
proof let R be Relation; let a,b be set; assume
R \/ R~ reduces a,b;
then (R \/ R~)~ reduces b,a by Th25;
then R~ \/ R~~ reduces b,a by RELAT_1:40;
hence R \/ R~ reduces b,a;
end;
theorem Th26:
for R being Relation, a,b being set 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 set;
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 by Def2;
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 2;
end;
then R \/ R~ reduces a,b by A1,Def3;
hence a,b are_convertible_wrt R by Def4;
hence thesis by Lm5;
end;
theorem Th27:
for R being Relation, a being set holds a,a are_convertible_wrt R
proof let R be Relation, a be set;
R reduces a,a by Th13;
hence thesis by Th26;
end;
theorem Th28:
for a,b being set st a,b are_convertible_wrt {} holds a = b
proof let a,b be set; assume
a,b are_convertible_wrt {};
then {} \/ ({} qua Relation)~ reduces a,b &
{} = ({} qua Relation)~ by Def4;
hence a = b by Th14;
end;
theorem
for R being Relation, a,b being set st a,b are_convertible_wrt R &
not a in field R holds a = b
proof let R be Relation; let a,b be set; assume
A1: R \/ R~ reduces a,b;
field R = field (R~) & (field R) \/ field R = field R &
field (R \/ R~) = (field R) \/ field (R~) by RELAT_1:33,38;
hence thesis by A1,Th15;
end;
theorem Th30:
for R being Relation, a,b being set st [a,b] in R
holds a,b are_convertible_wrt R
proof let R be Relation, a,b be set; assume [a,b] in R;
then R reduces a,b by Th16;
hence thesis by Th26;
end;
theorem Th31:
for R being Relation, a,b,c being set st
a,b are_convertible_wrt R & b,c are_convertible_wrt R
holds a,c are_convertible_wrt R
proof let R be Relation, a,b,c be set; assume
R \/ R~ reduces a,b & R \/ R~ reduces b,c;
hence R \/ R~ reduces a,c by Th17;
end;
theorem
for R being Relation, a,b being set st a,b are_convertible_wrt R
holds b,a are_convertible_wrt R by Lm5;
theorem Th33:
for R being Relation, a,b being set 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 set; assume
A1: R \/ R~ reduces a,b;
field (R \/ R~) = (field R) \/ field (R~) by RELAT_1:33
.= (field R) \/ field R by RELAT_1:38
.= field R;
hence thesis by A1,Th19;
end;
definition
let R be Relation;
let a be set;
pred a is_a_normal_form_wrt R means
not ex b being set st [a,b] in R;
end;
theorem Th34:
for R being Relation, a,b being set st
a is_a_normal_form_wrt R & R reduces a,b holds a = b
proof let R be Relation; let a,b be set; assume
A1: not ex b being set st [a,b] in R; assume R reduces a,b;
then consider p being FinSequence such that
A2: 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 by Th12
;
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 A2;
hence contradiction by A1;
end;
then len p <= 1 & len p >= 0+1 by A2,NAT_1:38;
hence thesis by A2,AXIOMS:21;
end;
theorem Th35:
for R being Relation, a being set st not a in field R
holds a is_a_normal_form_wrt R
proof let R be Relation, a be set such that
A1: not a in field R;
assume
ex b being set st [a,b] in R;
hence contradiction by A1,RELAT_1:30;
end;
definition
let R be Relation;
let a,b be set;
pred b is_a_normal_form_of a,R means:
Def6:
b is_a_normal_form_wrt R & R reduces a,b;
pred a,b are_convergent_wrt R means:
Def7:
ex c being set st R reduces a,c & R reduces b,c;
pred a,b are_divergent_wrt R means:
Def8:
ex c being set st R reduces c,a & R reduces c,b;
pred a,b are_convergent<=1_wrt R means:
Def9:
ex c being set st ([a,c] in R or a = c) & ([b,c] in R or b = c);
pred a,b are_divergent<=1_wrt R means:
Def10:
ex c being set st ([c,a] in R or a = c) & ([c,b] in R or b = c);
end;
theorem Th36:
for R being Relation, a being set st not a in field R
holds a is_a_normal_form_of a,R
proof let R be Relation, a be set; assume
not a in field R;
hence a is_a_normal_form_wrt R & R reduces a,a by Th13,Th35;
end;
theorem Th37:
for R being Relation, a,b being set 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 set;
R reduces a,a & R reduces b,b by Th13;
hence thesis by Def7,Def8;
end;
theorem Th38:
for R being Relation, a,b being set 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 set; 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 set such that
A2: R reduces a,c & R reduces b,c by Def7;
A3: a,c are_convertible_wrt R & b,c are_convertible_wrt R by A2,Th26;
c,b are_convertible_wrt R by A2,Th26;
hence thesis by A3,Th31;
suppose a,b are_divergent_wrt R;
then consider c being set such that
A4: R reduces c,a & R reduces c,b by Def8;
A5: c,a are_convertible_wrt R & c,b are_convertible_wrt R by A4,Th26;
a,c are_convertible_wrt R by A4,Th26;
hence thesis by A5,Th31;
end;
theorem Th39:
for R being Relation, a being set holds
a,a are_convergent_wrt R & a,a are_divergent_wrt R
proof let R be Relation, a be set;
R reduces a,a by Th13;
hence (ex b being set st R reduces a,b & R reduces a,b) &
ex b being set st R reduces b,a & R reduces b,a;
end;
theorem Th40:
for a,b being set st a,b are_convergent_wrt {} or a,b are_divergent_wrt {}
holds a = b
proof let a,b be set; assume
A1: a,b are_convergent_wrt {} or a,b are_divergent_wrt {};
A2: now assume a,b are_convergent_wrt {};
then consider c being set such that
A3: {} reduces a,c & {} reduces b,c by Def7;
a = c & b = c by A3,Th14;
hence thesis;
end;
now assume a,b are_divergent_wrt {};
then consider c being set such that
A4: {} reduces c,a & {} reduces c,b by Def8;
a = c & b = c by A4,Th14;
hence thesis;
end;
hence thesis by A1,A2;
end;
theorem
for R being Relation, a,b being set st a,b are_convergent_wrt R
holds b,a are_convergent_wrt R
proof let R be Relation, a,b be set;
assume ex c being set st R reduces a,c & R reduces b,c;
hence ex c being set st R reduces b,c & R reduces a,c;
end;
theorem
for R being Relation, a,b being set st a,b are_divergent_wrt R
holds b,a are_divergent_wrt R
proof let R be Relation, a,b be set;
assume ex c being set st R reduces c,a & R reduces c,b;
hence ex c being set st R reduces c,b & R reduces c,a;
end;
theorem Th43:
for R being Relation, a,b,c being set 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 set; 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 set such that
A3: R reduces b,d & R reduces c,d by Def7;
R reduces a,d by A2,A3,Th17;
hence thesis by A3,Def7;
suppose
A4: a,b are_convergent_wrt R & R reduces c,b;
then consider d being set such that
A5: R reduces a,d & R reduces b,d by Def7;
R reduces c,d by A4,A5,Th17;
hence thesis by A5,Def7;
end;
theorem
for R being Relation, a,b,c being set 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 set; 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 set such that
A3: R reduces d,b & R reduces d,c by Def8;
R reduces d,a by A2,A3,Th17;
hence thesis by A3,Def8;
suppose
A4: a,b are_divergent_wrt R & R reduces b,c;
then consider d being set such that
A5: R reduces d,a & R reduces d,b by Def8;
R reduces d,c by A4,A5,Th17;
hence thesis by A5,Def8;
end;
theorem Th45:
for R being Relation, a,b being set st a,b are_convergent<=1_wrt R
holds a,b are_convergent_wrt R
proof let R be Relation, a,b be set;
given c being set such that
A1: ([a,c] in R or a = c) & ([b,c] in R or b = c);
take c; thus R reduces a,c & R reduces b,c by A1,Th13,Th16;
end;
theorem Th46:
for R being Relation, a,b being set st a,b are_divergent<=1_wrt R
holds a,b are_divergent_wrt R
proof let R be Relation, a,b be set;
given c being set such that
A1: ([c,a] in R or a = c) & ([c,b] in R or b = c);
take c; thus R reduces c,a & R reduces c,b by A1,Th13,Th16;
end;
definition
let R be Relation;
let a be set;
pred a has_a_normal_form_wrt R means:
Def11:
ex b being set st b is_a_normal_form_of a,R;
end;
theorem Th47:
for R being Relation, a being set st not a in field R
holds a has_a_normal_form_wrt R
proof let R be Relation, a be set; assume
not a in field R;
then a is_a_normal_form_of a,R by Th36;
hence ex b being set st b is_a_normal_form_of a,R;
end;
definition
let R be Relation, a be set;
assume that
A1: a has_a_normal_form_wrt R and
A2: for b,c being set st b is_a_normal_form_of a,R &
c is_a_normal_form_of a,R holds b = c;
func nf(a,R) means:
Def12:
it is_a_normal_form_of a,R;
existence by A1,Def11;
uniqueness by A2;
end;
begin :: Terminating reductions
definition
let R be Relation;
attr R is co-well_founded means:
Def13:
R~ is well_founded;
attr R is weakly-normalizing means:
Def14:
for a being set 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:
Def16:
for Y being set st Y c= field R & Y <> {}
ex a being set st a in Y &
for b being set st b in Y & a <> b holds not [a,b] in R;
compatibility
proof
A1: field R = field (R~) by RELAT_1:38;
hereby assume R is co-well_founded;
then A2: R~ is well_founded by Def13;
let Y be set; assume Y c= field R & Y <> {};
then consider a being set such that
A3: a in Y & (R~)-Seg(a) misses Y by A1,A2,WELLORD1:def 2;
take a; thus a in Y by A3;
let b be set; assume b in Y;
then not b in (R~)-Seg(a) by A3,XBOOLE_0:3;
then a = b or not [b,a] in R~ by WELLORD1:def 1;
hence a <> b implies not [a,b] in R by RELAT_1:def 7;
end;
hereby assume
A4: for Y being set st Y c= field R & Y <> {}
ex a being set st a in Y &
for b being set 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 set such that
A5: a in Y & for b being set st b in Y & a <> b holds not [a,b] in
R by A1,A4;
take a; thus a in Y by A5;
now assume (R~)-Seg(a) /\ Y is non empty;
then reconsider A = (R~)-Seg(a) /\ Y as non empty set;
consider x being Element of A;
A6: x in (R~)-Seg(a) & x in Y by XBOOLE_0:def 3;
then x <> a & [x,a] in R~ by WELLORD1:def 1;
then not [a,x] in R & [a,x] in R by A5,A6,RELAT_1:def 7;
hence contradiction;
end;
hence (R~)-Seg(a) misses Y by XBOOLE_0:def 7;
end;
hence R is co-well_founded by Def13;
end;
end;
end;
scheme coNoetherianInduction{R() -> Relation, P[set]}:
for a being set st a in field R() holds P[a]
provided
A1: R() is co-well_founded
and
A2: for a being set st for b being set st [a,b] in R() & a <> b holds P[b]
holds P[a]
proof given a being set such that
A3: a in field R() & 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]};
A4: a in Y by A3;
Y c= field R()
proof let y be set; assume y in Y;
then ex x being Element of X st y = x & not P[x];
hence thesis;
end;
then consider a being set such that
A5: a in Y and
A6: for b being set st b in Y & a <> b holds not [a,b] in R() by A1,A4,Def16;
consider x being Element of X such that
A7: a = x & not P[x] by A5;
now let b be set; assume
A8: [a,b] in R() & a <> b & not P[b];
then not b in Y & b in X by A6,RELAT_1:30;
hence contradiction by A8;
end;
hence thesis by A2,A7;
end;
definition
cluster strongly-normalizing -> irreflexive co-well_founded Relation;
coherence
proof 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 set such that
A2: x in field R & [x,x] in R;
dom (NAT --> x) = NAT by FUNCOP_1:19;
then reconsider f = NAT --> x as ManySortedSet of NAT by PBOOLE:def 3;
consider i being Nat such that
A3: not [f.i, f.(i+1)] in R by A1;
f.i = x & f.(i+1) = x by FUNCOP_1:13;
hence contradiction by A2,A3;
end;
let Y be set; assume that
A4: Y c= field R & Y <> {} and
A5: for a being set st a in Y
ex b being set st b in Y & a <> b & [a,b] in R;
reconsider Y as non empty set by A4;
consider y being Element of Y;
defpred P[set,set] means [$1,$2] in R;
defpred Q[set] means not contradiction;
A6: y in Y & Q[y];
now let x be set; assume x in Y;
then ex b being set st b in Y & x <> b & [x,b] in R by A5;
hence ex y being set st y in Y & [x,y] in R;
end; then
A7: for x be set st x in Y & Q[x] ex y be set st y in Y & P[x,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 InfiniteChain(A6,A7);
f is ManySortedSet of NAT by A8,PBOOLE:def 3;
hence thesis by A1,A9;
end;
cluster co-well_founded irreflexive -> strongly-normalizing Relation;
coherence
proof let R be Relation such that
A10: for Y being set st Y c= field R & Y <> {}
ex a being set st a in Y &
for b being set st b in Y & a <> b holds not [a,b] in R;
assume
A11: for x being set 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: dom f = NAT by PBOOLE:def 3;
A14: rng f c= field R
proof let y be set; assume y in rng f;
then consider x being set such that
A15: x in dom f & y = f.x by FUNCT_1:def 5;
reconsider x as Nat by A15,PBOOLE:def 3;
[y, f.(x+1)] in R by A12,A15;
hence thesis by RELAT_1:30;
end;
f.0 in rng f by A13,FUNCT_1:def 5;
then consider a being set such that
A16: a in rng f & for b being set st b in rng f & a <> b holds not [a,b] in R
by A10,A14;
consider x being set such that
A17: x in dom f & a = f.x by A16,FUNCT_1:def 5;
reconsider x as Nat by A17,PBOOLE:def 3;
A18: [a,f.(x+1)] in R & not [a,a] in R by A11,A12,A14,A16,A17;
then a <> f.(x+1) & f.(x+1) in rng f by A13,FUNCT_1:def 5;
hence contradiction by A16,A18;
end;
end;
definition
cluster empty -> weakly-normalizing strongly-normalizing Relation;
coherence
proof let R be Relation; assume
A1: R is empty;
thus R is weakly-normalizing
proof let x be set; thus thesis by A1,TOLER_1:1; end;
thus R is strongly-normalizing
proof let f be ManySortedSet of NAT; take 0; thus thesis by A1; end;
end;
end;
definition
cluster empty Relation; existence proof take {}; thus thesis; end;
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;
then A2: field R c= field Q by RELAT_1:31;
let Y be set; assume
A3: Y c= field R & Y <> {};
then Y c= field Q by A2,XBOOLE_1:1;
then consider a being set such that
A4: a in Y and
A5: for b being set 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 set; assume b in Y & a <> b;
hence thesis by A1,A5;
end;
definition
cluster strongly-normalizing -> weakly-normalizing Relation;
coherence
proof let R be Relation such that
A1: R is strongly-normalizing;
let a be set; 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 set; 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 & a in X by A2,Th13;
then A4: a in Y & R is strongly-normalizing Relation by A1;
then consider x being set such that
A5: x in Y &
for b being set st b in Y & x <> b holds not [x,b] in R by A3,Def16;
take x;
A6: ex y being Element of X st x = y & R reduces a,y by A5;
hereby given b being set such that
A7: [x,b] in R;
x in field R & R is_irreflexive_in field R & R reduces x,b
by A3,A4,A5,A7,Th16,RELAT_2:def 10;
then not [x,x] in R & R reduces a,b & b in X
by A6,A7,Th17,RELAT_1:30,RELAT_2:def 2;
then x <> b & b in Y by A7;
hence contradiction by A5,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 set st [a,b] in R & [a,c] in Q
ex d being set st Q reduces b,d & R reduces c,d;
symmetry
proof let R,Q be Relation such that
A1: for a,b,c being set st [a,b] in R & [a,c] in Q
ex d being set st Q reduces b,d & R reduces c,d;
let a,b,c be set; assume [a,b] in Q & [a,c] in R;
then ex d being set st Q reduces c,d & R reduces b,d by A1;
hence ex d being set st R reduces b,d & Q reduces c,d;
end;
pred R commutes_with Q means:
Def18:
for a,b,c being set st R reduces a,b & Q reduces a,c
ex d being set st Q reduces b,d & R reduces c,d;
symmetry
proof let R,Q be Relation such that
A2: for a,b,c being set st R reduces a,b & Q reduces a,c
ex d being set st Q reduces b,d & R reduces c,d;
let a,b,c be set; assume Q reduces a,b & R reduces a,c;
then ex d being set st Q reduces c,d & R reduces b,d by A2;
hence ex d being set st R reduces b,d & Q reduces c,d;
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 set st R reduces a,b & Q reduces a,c
ex d being set st Q reduces b,d & R reduces c,d;
let a,b,c be set; assume [a,b] in R & [a,c] in Q;
then R reduces a,b & Q reduces a,c by Th16;
hence thesis by A1;
end;
definition
let R be Relation;
attr R is with_UN_property means:
Def19:
for a,b being set 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 set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R
holds R reduces b,a;
attr R is subcommutative means:
Def21:
for a,b,c being set st [a,b] in R & [a,c] in R
holds b,c are_convergent<=1_wrt R;
synonym R has_diamond_property;
attr R is confluent means:
Def22:
for a,b being set 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 set st a,b are_convertible_wrt R
holds a,b are_convergent_wrt R;
synonym R has_Church-Rosser_property;
attr R is locally-confluent means:
Def24:
for a,b,c being set st [a,b] in R & [a,c] in R
holds b,c are_convergent_wrt R;
synonym R has_weak-Church-Rosser_property;
end;
theorem Th50:
for R being Relation st R is subcommutative for a,b,c being set 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 set; given p being RedSequence of R such that
A2: p.1 = a & p.len p = b;
A3: len p in dom p by FINSEQ_5:6;
assume
A4: [a,c] in R;
defpred P[Nat] means $1 in dom p implies
ex d being set st ([p.$1,d] in R or p.$1 = d) & R reduces c,d;
A5: P[0] by Lm1;
now let i be Nat such that
A6: i in dom p implies P[i] and
A7: i+1 in dom p;
per cases by NAT_1:19; suppose i = 0;
then p.(i+1) = a & R reduces c,c by A2,Th13;
hence P[i+1] by A4;
suppose i > 0;
then A8: i >= 0+1 & i < len p by A7,Lm2,NAT_1:38;
then A9: i in dom p by Lm3;
consider d being set such that
A10: ([p.i,d] in R or p.i = d) & R reduces c,d by A6,A8,Lm3;
A11: [p.i,p.(i+1)] in R by A7,A9,Def2;
A12: now assume [p.i,d] in R;
then p.(i+1),d are_convergent<=1_wrt R by A1,A11,Def21;
then consider e being set such that
A13: ([p.(i+1),e] in R or p.(i+1) = e) & ([d,e] in R or d = e) by Def9;
take e; thus [p.(i+1),e] in R or p.(i+1) = e by A13;
R reduces d,e by A13,Th13,Th16;
hence R reduces c,e by A10,Th17;
end;
now assume p.i = d;
then R reduces d, p.(i+1) by A11,Th16;
hence R reduces c, p.(i+1) by A10,Th17;
end;
hence P[i+1] by A10,A12;
end; then
A14: for k be Nat st P[k] holds P[k+1];
for i being Nat holds P[i] from Ind(A5,A14);
then consider d being set such that
A15: ([b,d] in R or b = d) & R reduces c,d by A2,A3;
take d; thus thesis by A15,Th13,Th16;
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 set; assume R reduces a,b & R reduces a,c;
then b,c are_divergent_wrt R by Def8;
then b,c are_convergent_wrt R by A1,Def22;
hence ex d being set st R reduces b,d & R reduces c,d by Def7;
end;
end;
assume
A2: for a,b,c being set st R reduces a,b & R reduces a,c
ex d being set st R reduces b,d & R reduces c,d;
let a,b be set; assume
ex c being set st R reduces c,a & R reduces c,b;
hence ex d being set st R reduces a,d & R reduces b,d by A2;
end;
theorem Th52:
for R being Relation holds
R is confluent iff for a,b,c being set 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 set; assume
A2: R reduces a,b & [a,c] in R; then R reduces a,c by Th16;
then b,c are_divergent_wrt R by A2,Def8;
hence b,c are_convergent_wrt R by A1,Def22;
end;
assume
A3: for a,b,c being set st R reduces a,b & [a,c] in R
holds b,c are_convergent_wrt R;
let b,c be set; given a being set such that
A4: R reduces a,b & R reduces a,c;
consider p being RedSequence of R such that
A5: p.1 = a & p.len p = b by A4,Def3;
A6: len p in dom p by FINSEQ_5:6;
consider q being RedSequence of R such that
A7: q.1 = a & q.len q = c by A4,Def3;
A8: len q in dom q & len q > 0 by Def2,FINSEQ_5:6;
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];
A9: Q[0] by Lm1;
A10: 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
A11: i+1 in dom p;
defpred R[Nat] means $1 in dom q implies P[i+1,$1];
A12: R[0] by Lm1;
A13: for j being Nat st R[j] holds R[j+1]
proof let j be Nat such that
A14: j in dom q implies P[i+1,j] and
A15: j+1 in dom q;
1 in dom p & i+1 >= 1 by FINSEQ_5:6,NAT_1:29;
then A16: R reduces a,p.(i+1) by A5,A11,Th18;
per cases by NAT_1:19; suppose j = 0;
hence P[i+1,j+1] by A7,A16,Th37;
suppose j > 0;
then A17: j >= 0+1 & j < len q by A15,Lm2,NAT_1:38;
then A18: j in dom q by Lm3;
consider d being set such that
A19: R reduces p.(i+1),d & R reduces q.j,d by A14,A17,Def7,Lm3;
[q.j, q.(j+1)] in R by A15,A18,Def2;
then d,q.(j+1) are_convergent_wrt R by A3,A19;
hence P[i+1,j+1] by A19,Th43;
end;
thus for j being Nat holds R[j] from Ind(A12,A13);
end;
for i being Nat holds Q[i] from Ind(A9,A10);
hence thesis by A5,A6,A7,A8;
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 set; assume [a,b] in R & [a,c] in R;
then b,c are_convergent_wrt R by A1,Def24;
hence ex d being set st R reduces b,d & R reduces c,d by Def7;
end;
end;
assume
A2: for a,b,c being set st [a,b] in R & [a,c] in R
ex d being set st R reduces b,d & R reduces c,d;
let a,b,c be set; assume
[a,b] in R & [a,c] in R;
hence ex d being set st R reduces b,d & R reduces c,d by A2;
end;
definition
cluster with_Church-Rosser_property -> confluent Relation;
coherence
proof let R be Relation; assume
A1: for a,b being set st a,b are_convertible_wrt R
holds a,b are_convergent_wrt R;
let a,b be set; assume a,b are_divergent_wrt R;
then a,b are_convertible_wrt R by Th38;
hence a,b are_convergent_wrt R by A1;
end;
cluster confluent -> locally-confluent with_Church-Rosser_property Relation;
coherence
proof let R be Relation; assume
A2: for a,b being set st a,b are_divergent_wrt R
holds a,b are_convergent_wrt R;
hereby let a,b,c be set; assume
[a,b] in R & [a,c] in R;
then R reduces a,b & R reduces a,c by Th16;
then b,c are_divergent_wrt R by Def8;
hence b,c are_convergent_wrt R by A2;
end;
let a,b be set; given p being RedSequence of R \/ R~ such that
A3: p.1 = a & p.len p = b;
A4: len p in dom p by FINSEQ_5:6;
defpred P[Nat] means $1 in dom p implies a,p.$1 are_convergent_wrt R;
A5: P[0] by Lm1;
now let i be Nat; assume that
A6: i in dom p implies a,p.i are_convergent_wrt R and
A7: i+1 in dom p;
per cases;
suppose A8: i in dom p;
then a,p.i are_convergent_wrt R & [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 2;
then [p.i, p.(i+1)] in R or [p.(i+1), p.i] in R by RELAT_1:def 7;
then A9: R reduces p.i, p.(i+1) or R reduces p.(i+1), p.i by Th16;
consider c being set such that
A10: R reduces a,c & R reduces p.i,c by A6,A8,Def7;
c,p.(i+1) are_divergent_wrt R or R reduces p.(i+1),c
by A9,A10,Def8,Th17;
then c,p.(i+1) are_convergent_wrt R or a,p.(i+1) are_convergent_wrt R
by A2,A10,Def7;
hence a, p.(i+1) are_convergent_wrt R by A10,Th43;
suppose not i in dom p;
then i < 0+1 or i > len p & i+1 <= len p by A7,Lm1,Lm3;
then i <= 0 & i >= 0 by NAT_1:18,38;
then i = 0;
hence a, p.(i+1) are_convergent_wrt R by A3,Th39;
end;
then A11: for k being Nat st P[k] holds P[k+1];
for i being Nat holds P[i] from Ind(A5,A11);
hence thesis by A3,A4;
end;
cluster subcommutative -> confluent Relation;
coherence
proof let R be Relation; assume
R is subcommutative;
then for a,b,c being set st R reduces a,b & [a,c] in R
holds b,c are_convergent_wrt R by Th50;
hence thesis by Th52;
end;
cluster with_Church-Rosser_property -> with_NF_property Relation;
coherence
proof let R be Relation; assume
A12: R is with_Church-Rosser_property;
let b,a be set; assume
A13: b is_a_normal_form_wrt R;
assume b,a are_convertible_wrt R;
then b,a are_convergent_wrt R by A12,Def23;
then consider c being set such that
A14: R reduces b,c & R reduces a,c by Def7;
thus thesis by A13,A14,Th34;
end;
cluster with_NF_property -> with_UN_property Relation;
coherence
proof let R be Relation such that
A15: for a,b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R
holds R reduces b,a;
let a,b be set such that
A16: a is_a_normal_form_wrt R & b is_a_normal_form_wrt R and
A17: a,b are_convertible_wrt R;
R reduces b,a by A15,A16,A17;
hence a = b by A16,Th34;
end;
cluster with_UN_property weakly-normalizing -> with_Church-Rosser_property
Relation;
coherence
proof let R be Relation such that
A18: for a,b being set 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
A19: for a being set st a in field R holds a has_a_normal_form_wrt R;
let a,b be set; assume
A20: R \/ R~ reduces a,b;
A21: field (R \/ R~) = (field R) \/ field (R~) by RELAT_1:33
.= (field R) \/ field R by RELAT_1:38
.= field R;
per cases; suppose a = b; hence thesis by Th39;
suppose
a <> b;
then a in field R & b in field R by A20,A21,Th19;
then A22: a has_a_normal_form_wrt R & b has_a_normal_form_wrt R by A19;
then consider a' being set such that
A23: a' is_a_normal_form_of a,R by Def11;
consider b' being set such that
A24: b' is_a_normal_form_of b,R by A22,Def11;
A25: a' is_a_normal_form_wrt R & b' is_a_normal_form_wrt R by A23,A24,Def6;
A26: R reduces a,a' & R reduces b,b' by A23,A24,Def6;
then a',a are_convertible_wrt R & a,b are_convertible_wrt R
by A20,Def4,Th26;
then b,b' are_convertible_wrt R & a',b are_convertible_wrt R
by A26,Th26,Th31;
then a',b' are_convertible_wrt R by Th31;
then a' = b' by A18,A25;
hence thesis by A26,Def7;
end;
end;
definition
cluster empty -> subcommutative Relation;
coherence
proof let R be Relation; assume
A1: R is empty;
let x be set; thus thesis by A1;
end;
end;
definition
cluster empty Relation; existence proof take {}; thus thesis; end;
end;
theorem Th54:
for R being with_UN_property Relation
for a,b,c being set 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 set such that
A1: b is_a_normal_form_wrt R & R reduces a,b and
A2: c is_a_normal_form_wrt R & R reduces a,c;
b,c are_divergent_wrt R by A1,A2,Def8;
then b,c are_convertible_wrt R by Th38;
hence thesis by A1,A2,Def19;
end;
theorem Th55:
for R being with_UN_property weakly-normalizing Relation
for a being set holds nf(a,R) is_a_normal_form_of a,R
proof let R be with_UN_property weakly-normalizing Relation;
let a be set;
a in field R or not a in field R;
then a has_a_normal_form_wrt R &
for b,c being set st b is_a_normal_form_of a,R &
c is_a_normal_form_of a,R holds b = c by Def14,Th47,Th54;
hence thesis by Def12;
end;
theorem Th56:
for R being with_UN_property weakly-normalizing Relation
for a,b being set 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 set;
A1: nf(a,R) is_a_normal_form_of a,R & nf(b,R) is_a_normal_form_of b,R
by Th55;
then A2: nf(a,R) is_a_normal_form_wrt R & nf(b,R) is_a_normal_form_wrt R by
Def6;
R reduces a,nf(a,R) & R reduces b,nf(b,R) by A1,Def6;
then A3: nf(a,R),a are_convertible_wrt R & b,nf(b,R) are_convertible_wrt R
by Th26;
assume a,b are_convertible_wrt R;
then nf(a,R),b are_convertible_wrt R by A3,Th31;
then nf(a,R),nf(b,R) are_convertible_wrt R by A3,Th31;
hence thesis by A2,Def19;
end;
definition
cluster strongly-normalizing locally-confluent -> confluent Relation;
coherence
proof let R be Relation; assume
R is strongly-normalizing;
then A1: R is strongly-normalizing Relation;
then A2: R is co-well_founded;
assume
A3: for a,b,c being set st [a,b] in R & [a,c] in R
holds b,c are_convergent_wrt R;
given a0,b0 being set such that
A4: a0,b0 are_divergent_wrt R & not a0,b0 are_convergent_wrt R;
consider c0 being set such that
A5: R reduces c0,a0 & R reduces c0,b0 by A4,Def8;
a0 <> c0 or b0 <> c0 by A4,Th39;
then A6: c0 in field R by A5,Th19;
defpred P[set] means
for b,c being set st R reduces $1,b & R reduces $1,c
holds b,c are_convergent_wrt R;
A7: for a being set st for b being set st [a,b] in R & a <> b holds P[b]
holds P[a]
proof let a be set; assume
A8: for b being set st [a,b] in R & a <> b holds P[b];
let b,c be set; assume
A9: R reduces a,b & R reduces a,c;
then consider p being RedSequence of R such that
A10: a = p.1 & b = p.len p by Def3;
consider q being RedSequence of R such that
A11: a = q.1 & c = q.len q by A9,Def3;
len p > 0 & len q > 0 by Def2;
then A12: len p >= 0+1 & len q >= 0+1 by NAT_1:38;
per cases;
suppose len p = 1; hence b,c are_convergent_wrt R by A9,A10,Th37;
suppose len q = 1; hence b,c are_convergent_wrt R by A9,A11,Th37;
suppose len p <> 1 & len q <> 1;
then len p > 1 & len q > 1 by A12,REAL_1:def 5;
then A13: 1 <= 2 & 1+1 <= len p & 1+1 <= len q by NAT_1:38;
then A14: 1 in dom p & 1+1 in dom p & 1 in dom q & 1+1 in
dom q by A12,Lm3;
then A15: [a,p.2] in R & [a,q.2] in R by A10,A11,Def2;
then a in field R & R is_irreflexive_in field R
by A1,RELAT_1:30,RELAT_2:def 10;
then A16: a <> p.2 & a <> q.2 by A15,RELAT_2:def 2;
p.2,q.2 are_convergent_wrt R by A3,A15;
then consider d being set such that
A17: R reduces p.2,d & R reduces q.2,d by Def7;
len p in dom p by FINSEQ_5:6;
then R reduces p.2,b by A10,A13,A14,Th18;
then b,d are_convergent_wrt R by A8,A15,A16,A17;
then consider e being set such that
A18: R reduces b,e & R reduces d,e by Def7;
len q in dom q by FINSEQ_5:6;
then R reduces q.2,e & R reduces q.2,c by A11,A13,A14,A17,A18,Th17,
Th18
;
then e,c are_convergent_wrt R by A8,A15,A16;
hence b,c are_convergent_wrt R by A18,Th43;
end;
for a being set st a in field R holds P[a]
from coNoetherianInduction(A2,A7);
hence thesis by A4,A5,A6;
end;
end;
definition let R be Relation;
attr R is complete means R is confluent strongly-normalizing;
end;
definition
cluster complete -> confluent strongly-normalizing Relation;
coherence
proof let R be Relation; assume
R is confluent strongly-normalizing;
hence thesis;
end;
cluster confluent strongly-normalizing -> complete Relation;
coherence
proof let R be Relation; assume
R is confluent strongly-normalizing;
hence R is confluent strongly-normalizing;
end;
end;
definition
cluster empty Relation; existence proof take {}; thus thesis; end;
end;
definition
cluster complete (non empty Relation);
existence
proof reconsider R = {[0,1]} as non empty Relation by RELAT_1:4;
take R;
A1: field R = {0,1} by RELAT_1:32;
thus R is confluent
proof let a,b be set; given c being set such that
A2: R reduces c,a & R reduces c,b;
per cases; suppose a = b; hence thesis by Th39;
suppose a <> b;
then a <> c or b <> c;
then c in field R by A2,Th19;
then a in {0,1} & b in {0,1} & [0,1] in R by A1,A2,Th20,TARSKI:def 1;
then (a = 0 or a = 1) & (b = 0 or b = 1) & R reduces 0,1 & R reduces 1,1
by Th13,Th16,TARSKI:def 2;
hence a,b are_convergent_wrt R by Def7;
end;
A3: R is irreflexive
proof let x be set; assume x in field R & [x,x] in R;
then [x,x] = [0,1] by TARSKI:def 1;
then x = 0 & x = 1 by ZFMISC_1:33;
hence contradiction;
end;
R is co-well_founded
proof let Y be set; assume
A4: Y c= field R & Y <> {}; then reconsider Y' = Y as non empty set;
consider y being Element of Y';
per cases; suppose
A5: 1 in Y;
take 1; thus 1 in Y by A5;
let b be set; assume b in Y & 1 <> b;
[0,1] <> [1,b] by ZFMISC_1:33;
hence not [1,b] in R by TARSKI:def 1;
suppose
A6: not 1 in Y & y in Y;
take 0; thus 0 in Y by A1,A4,A6,TARSKI:def 2;
let b be set; assume b in Y;
hence thesis by A1,A4,A6,TARSKI:def 2;
end;
then R is irreflexive co-well_founded Relation by A3;
hence R is strongly-normalizing;
end;
end;
theorem
for R,Q being with_Church-Rosser_property Relation st
R commutes_with Q holds R \/ Q has_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 set; given c being set such that
A2: R \/ Q reduces c,a & R \/ Q reduces c,b;
A3: R c= R \/ Q & Q c= R \/ Q by XBOOLE_1:7;
consider p being RedSequence of R \/ Q such that
A4: c = p.1 & a = p.len p by A2,Def3;
defpred Z[Nat] means $1 in dom p implies p.$1,b are_convergent_wrt R \/ Q;
A5: Z[0] by Lm1;
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 by NAT_1:19;
suppose i = 0; hence p.(i+1),b are_convergent_wrt R \/ Q by A2,A4,Th37;
suppose i > 0; then A8: i >= 0+1 & i < len p by A7,Lm2,NAT_1:38;
then A9: i in dom p by Lm3;
consider d being set such that
A10: R \/ Q reduces p.i,d & R \/ Q reduces b,d by A6,A8,Def7,Lm3;
consider q being RedSequence of R \/ Q such that
A11: p.i = q.1 & d = q.len q by A10,Def3;
[p.i,p.(i+1)] in R \/ Q by A7,A9,Def2;
then A12: [p.i,p.(i+1)] in R or [p.i,p.(i+1)] in Q by XBOOLE_0:def 2;
defpred P[Nat] means $1 in dom q implies
ex e being set st R \/ Q reduces p.(i+1),e &
(R reduces q.$1,e or Q reduces q.$1,e);
A13: P[0] by Lm1;
now let j be Nat such that
A14: j in dom q implies
ex e being set st R \/ Q reduces p.(i+1),e &
(R reduces q.j,e or Q reduces q.j,e) and
A15: j+1 in dom q;
A16: j < len q by A15,Lm2;
per cases by NAT_1:19;
suppose j = 0;
then R \/ Q reduces p.(i+1),p.(i+1) &
(R reduces q.(j+1),p.(i+1) or
Q reduces q.(j+1),p.(i+1)) by A11,A12,Th13,Th16;
hence ex e being set st R \/ Q reduces p.(i+1),e &
(R reduces q.(j+1),e or Q reduces q.(j+1),e);
suppose A17: j > 0;
then j in dom q by A16,Lm3;
then [q.j,q.(j+1)] in R \/ Q by A15,Def2;
then A18: [q.j,q.(j+1)] in R or [q.j,q.(j+1)] in Q by XBOOLE_0:def 2
;
consider e being set such that
A19: R \/ Q reduces p.(i+1),e &
(R reduces q.j,e or Q reduces q.j,e) by A14,A16,A17,Lm3;
A20: now assume R reduces q.j,q.(j+1) & R reduces q.j,e;
then e,q.(j+1) are_divergent_wrt R by Def8;
then e,q.(j+1) are_convergent_wrt R by Def22;
then consider x being set such that
A21: R reduces e,x & R reduces q.(j+1),x by Def7;
take x; R \/ Q reduces e,x by A3,A21,Th23;
hence R \/ Q reduces p.(i+1),x &
(R reduces q.(j+1),x or Q reduces q.(j+1),x) by A19,A21,Th17;
end;
A22: now assume Q reduces q.j,q.(j+1) & Q reduces q.j,e;
then e,q.(j+1) are_divergent_wrt Q by Def8;
then e,q.(j+1) are_convergent_wrt Q by Def22;
then consider x being set such that
A23: Q reduces e,x & Q reduces q.(j+1),x by Def7;
take x; R \/ Q reduces e,x by A3,A23,Th23;
hence R \/ Q reduces p.(i+1),x &
(R reduces q.(j+1),x or Q reduces q.(j+1),x) by A19,A23,Th17;
end;
A24: now assume R reduces q.j,q.(j+1) & Q reduces q.j,e;
then consider x being set such that
A25: Q reduces q.(j+1),x & R reduces e,x by A1,Def18;
take x; R \/ Q reduces e,x by A3,A25,Th23;
hence R \/ Q reduces p.(i+1),x &
(R reduces q.(j+1),x or Q reduces q.(j+1),x) by A19,A25,Th17;
end;
now assume Q reduces q.j,q.(j+1) & R reduces q.j,e;
then consider x being set such that
A26: R reduces q.(j+1),x & Q reduces e,x by A1,Def18;
take x; R \/ Q reduces e,x by A3,A26,Th23;
hence R \/ Q reduces p.(i+1),x &
(R reduces q.(j+1),x or Q reduces q.(j+1),x) by A19,A26,Th17;
end;
hence ex e being set st R \/ Q reduces p.(i+1),e &
(R reduces q.(j+1),e or Q reduces q.(j+1),e)
by A18,A19,A20,A22,A24,Th16;
end; then
A27: for k being Nat st P[k] holds P[k+1];
A28: for j being Nat holds P[j] from Ind(A13,A27);
thus p.(i+1),b are_convergent_wrt R \/ Q
proof len q in dom q by FINSEQ_5:6;
then consider e being set such that
A29: R \/ Q reduces p.(i+1),e & (R reduces d,e or Q reduces d,e)
by A11,A28;
take e;
R \/ Q reduces d,e by A3,A29,Th23;
hence thesis by A10,A29,Th17;
end;
end; then
A30: for k being Nat st Z[k] holds Z[k+1];
A31: for i being Nat holds Z[i] from Ind(A5,A30);
len p in dom p by FINSEQ_5:6;
hence a,b are_convergent_wrt R \/ Q by A4,A31;
end;
then R \/ Q is confluent Relation;
hence R \/ Q has_Church-Rosser_property;
end;
theorem
for R being Relation holds
R is confluent iff R* has_weak-Church-Rosser_property
proof let R be Relation;
hereby assume A1: R is confluent;
thus R* has_weak-Church-Rosser_property
proof let a,b,c be set; assume [a,b] in R* & [a,c] in R*;
then R reduces a,b & R reduces a,c by Th21;
then b,c are_divergent_wrt R by Def8;
then b,c are_convergent_wrt R by A1,Def22;
then consider d being set such that
A2: R reduces b,d & R reduces c,d by Def7;
take d; thus R* reduces b,d & R* reduces c,d by A2,Th22;
end;
end;
assume
A3: for a,b,c being set st [a,b] in R* & [a,c] in R*
holds b,c are_convergent_wrt R*;
let a,b be set; given c being set such that
A4: R reduces c,a & R reduces c,b;
([c,a] in R* or c = a) & ([c,b] in R* or c = b) by A4,Th21;
then a,b are_convergent_wrt R* or R* reduces a,b or R* reduces b,a
by A3,Th16,Th39;
then a,b are_convergent_wrt R* by Th37;
then consider d being set such that
A5: R* reduces a,d & R* reduces b,d by Def7;
take d; thus thesis by A5,Th22;
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 set; assume [a,b] in R* & [a,c] in R*;
then R reduces a,b & R reduces a,c by Th21;
then b,c are_divergent_wrt R by Def8;
then b,c are_convergent_wrt R by A1,Def22;
then consider d being set such that
A2: R reduces b,d & R reduces c,d by Def7;
take d; thus thesis by A2,Th21;
end;
end;
assume
A3: for a,b,c being set st [a,b] in R* & [a,c] in R*
holds b,c are_convergent<=1_wrt R*;
let a,b be set; given c being set such that
A4: R reduces c,a & R reduces c,b;
([c,a] in R* or c = a) & ([c,b] in R* or c = b) by A4,Th21;
then a,b are_convergent<=1_wrt R* by A3,Def9;
then a,b are_convergent_wrt R* by Th45;
then consider d being set such that
A5: R* reduces a,d & R* reduces b,d by Def7;
take d; thus thesis by A5,Th22;
end;
begin :: Completion method
definition
let R,Q be Relation;
pred R,Q are_equivalent means
for a,b being set 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 set;
pred a,b are_critical_wrt R means:
Def27:
a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R;
end;
theorem Th60:
for R being Relation, a,b being set st a,b are_critical_wrt R
holds a,b are_convertible_wrt R
proof let R be Relation, a,b be set; assume
a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R;
then a,b are_divergent_wrt R by Th46;
hence thesis by Th38;
end;
theorem
for R being Relation st not ex a,b being set 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 set st a,b are_critical_wrt R;
let a,b,c be set; assume
[a,b] in R & [a,c] in R;
then b,c are_divergent<=1_wrt R & not b,c are_critical_wrt R by A1,Def10;
hence thesis by Def27;
end;
theorem
for R,Q being Relation st
for a,b being set 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 set st [a,b] in Q holds a,b are_critical_wrt R;
A2: R c= R \/ Q by XBOOLE_1:7;
R~ c= (R \/ Q)~
proof let x,y be set; assume [x,y] in R~;
then [y,x] in R by RELAT_1:def 7;
hence thesis by A2,RELAT_1:def 7;
end;
then A3: R \/ R~ c= (R \/ Q) \/ (R \/ Q)~ by A2,XBOOLE_1:13;
let a,b be set;
hereby assume a,b are_convertible_wrt R;
then R \/ R~ reduces a,b by Def4;
then (R \/ Q) \/ (R \/ Q)~ reduces a,b by A3,Th23;
hence a,b are_convertible_wrt R \/ Q by Def4;
end;
given p being RedSequence of (R \/ Q) \/ (R \/ Q)~ such that
A4: a = p.1 & b = p.len p;
defpred Z[Nat] means $1 in dom p implies a,p.$1 are_convertible_wrt R;
A5: Z[0] by Lm1;
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 by NAT_1:19; suppose i = 0;
hence a,p.(i+1) are_convertible_wrt R by A4,Th27;
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 2;
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 2;
then [p.i,p.(i+1)] in R or p.i,p.(i+1) are_critical_wrt R or
[p.(i+1),p.i] in R or p.(i+1),p.i are_critical_wrt R by A1;
then p.i,p.(i+1) are_convertible_wrt R or p.(i+1),p.i
are_convertible_wrt R
by Th30,Th60;
then a,p.i are_convertible_wrt R & p.i,p.(i+1) are_convertible_wrt R
by A6,A8,A9,Lm3,Lm5;
hence a,p.(i+1) are_convertible_wrt R by Th31;
end; then
A10: for k being Nat st Z[k] holds Z[k+1];
A11: for i being Nat holds Z[i] from Ind(A5,A10);
len p in dom p by FINSEQ_5:6;
hence a,b are_convertible_wrt R by A4,A11;
end;
theorem Th63:
for R being Relation ex Q being complete Relation st
field Q c= field R &
for a,b being set holds
a,b are_convertible_wrt R iff a,b are_convergent_wrt Q
proof let R be Relation;
per cases; suppose
A1: R = {}; consider E being empty Relation;
take E; thus field E c= field R by TOLER_1:1,XBOOLE_1:2;
let a,b be set;
a,b are_convertible_wrt R iff a = b by A1,Th27,Th28;
hence thesis by Th39,Th40;
suppose
R <> {}; then reconsider R' = R as non empty Relation;
consider xx being Element of R';
consider x1,x2 being set such that
A2: xx = [x1,x2] by RELAT_1:def 1;
defpred P[set,set] means $1,$2 are_convertible_wrt R;
A3: for x st x in field R holds P[x,x] by Th27;
A4: for x,y being set st P[x,y] holds P[y,x] by Lm5;
A5: for x,y,z being set st P[x,y] & P[y,z] holds P[x,z] by Th31;
consider Q being Equivalence_Relation of field R such that
A6: for x,y holds [x,y] in Q iff x in field R & y in field R &
P[x,y] from Ex_Eq_Rel(A3,A4,A5);
A7: x1 in field R by A2,RELAT_1:30;
A8: Class Q is a_partition of field R by EQREL_1:42;
then A9: for X being set st X in Class Q holds X <> {} by A7,EQREL_1:def 6;
A10: for X,Y being set st X in Class Q & Y in
Class Q & X <> Y holds X misses Y by A7,A8,EQREL_1:def 6;
Class(Q,x1) in Class Q by A7,EQREL_1:def 5;
then consider X being set such that
A11: for A being set st A in
Class Q ex x st X /\ A = {x} by A9,A10,WELLORD2:27;
defpred Z[set,set] means $1 <> $2 &
$1,$2 are_convertible_wrt R & $2 in X;
consider P being Relation such that
A12: for x,y holds [x,y] in P iff x in field R & y in field R & Z[x,y]
from Rel_Existence;
A13: 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
A14: x = p.1 & y = p.len p;
defpred Z[Nat] means $1 in dom p implies x,p.$1 are_convertible_wrt R;
A15: Z[0] by Lm1;
now let i be Nat such that
A16: i in dom p implies x,p.i are_convertible_wrt R and
A17: i+1 in dom p;
A18: i < len p by A17,Lm2;
per cases by NAT_1:19; suppose i = 0;
hence x,p.(i+1) are_convertible_wrt R by A14,Th27;
suppose A19: i > 0;
then i in dom p by A18,Lm3;
then [p.i,p.(i+1)] in P by A17,Def2;
then p.i,p.(i+1) are_convertible_wrt R & x,p.i are_convertible_wrt R
by A12,A16,A18,A19,Lm3;
hence x,p.(i+1) are_convertible_wrt R by Th31;
end; then
A20: for k being Nat st Z[k] holds Z[k+1];
A21: for i being Nat holds Z[i] from Ind(A15,A20);
len p in dom p by FINSEQ_5:6;
hence thesis by A14,A21;
end;
A22: P is strongly-normalizing
proof let f be ManySortedSet of NAT;
consider i being Nat;
per cases; suppose not [f.i,f.(i+1)] in P; hence thesis;
suppose
A23: [f.i,f.(i+1)] in P;
take j = i+1; assume A24: [f.j,f.(j+1)] in P;
then A25: f.j in field R & f.(j+1) in field R & f.(j+1) <> f.j &
f.j,f.(j+1) are_convertible_wrt R & f.j in X & f.(j+1) in X by A12,A23
;
then [f.j,f.(j+1)] in Q by A6;
then [f.(j+1),f.j] in Q by EQREL_1:12;
then f.j in Class(Q,f.j) & f.(j+1) in
Class(Q,f.j) by A25,EQREL_1:27,28;
then A26: f.j in X /\ Class(Q,f.j) & f.(j+1) in X /\ Class(Q,f.j) &
Class(Q,f.j) in Class Q by A25,EQREL_1:def 5,XBOOLE_0:def 3;
then consider x such that
A27: X /\ Class(Q,f.j) = {x} by A11;
f.j = x & f.(j+1) = x by A26,A27,TARSKI:def 1;
hence contradiction by A12,A24;
end;
P is locally-confluent
proof let a,b,c be set; assume
A28: [a,b] in P & [a,c] in P;
take b;
A29: a in field R & b in field R & c in field R &
a,b are_convertible_wrt R & a,c are_convertible_wrt R &
b in X & c in X by A12,A28;
then [a,b] in Q & [a,c] in Q by A6;
then [b,a] in Q & [c,a] in Q by EQREL_1:12;
then A30: b in Class(Q,a) & c in Class(Q,a) by EQREL_1:27;
Class(Q,a) in Class Q by A29,EQREL_1:def 5;
then consider x such that
A31: X /\ Class(Q,a) = {x} by A11;
b in {x} & c in {x} by A29,A30,A31,XBOOLE_0:def 3;
then b = x & c = x by TARSKI:def 1;
hence thesis by Th13;
end;
then reconsider P as strongly-normalizing locally-confluent Relation by A22
;
take P;
thus field P c= field R
proof let x; assume x in field P;
then x in dom P \/ rng P by RELAT_1:def 6;
then x in dom P or x in rng P by XBOOLE_0:def 2;
then (ex y st [x,y] in P) or (ex y st [y,x] in
P) by RELAT_1:def 4,def 5;
hence thesis by A12;
end;
let a,b be set;
thus thesis
proof per cases; suppose a = b;
hence a,b are_convertible_wrt R iff a,b are_convergent_wrt P by Th27,Th39
;
suppose
A32: a <> b;
hereby assume
A33: a,b are_convertible_wrt R;
then A34: a in field R & b in field R by A32,Th33;
then A35: [a,b] in Q & Class(Q,b) in Class Q & b in Class(Q,b)
by A6,A33,EQREL_1:28,def 5;
then consider x such that
A36: X /\ Class(Q,b) = {x} by A11;
thus a,b are_convergent_wrt P
proof take x;
x in {x} by TARSKI:def 1;
then A37: x in X & x in Class(Q,b) by A36,XBOOLE_0:def 3;
then [x,b] in Q & a in Class(Q,b) by A35,EQREL_1:27;
then [b,x] in Q & [a,x] in Q by A37,EQREL_1:12,30;
then x in field R & b,x are_convertible_wrt R & a,x
are_convertible_wrt R
by A6;
then (a = x or [a,x] in P) & (b = x or [b,x] in P) by A12,A34,A37;
hence P reduces a,x & P reduces b,x by Th13,Th16;
end;
end;
given c being set such that
A38: P reduces a,c & P reduces b,c;
b,c are_convertible_wrt R by A13,A38;
then a,c are_convertible_wrt R & c,b are_convertible_wrt R by A13,A38,
Lm5;
hence a,b are_convertible_wrt R by Th31;
end;
end;
definition
let R be Relation;
mode Completion of R -> complete Relation means:
Def28:
for a,b being set 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 set holds
a,b are_convertible_wrt R iff a,b are_convergent_wrt Q by Th63;
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 set;
a,b are_convertible_wrt R iff a,b are_convergent_wrt C by Def28;
hence a,b are_convertible_wrt R iff a,b are_convertible_wrt C
by Def23,Th38;
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 set holds
a,b are_convertible_wrt R iff a,b are_convertible_wrt Q;
let a,b be set;
a,b are_convertible_wrt R iff a,b are_convertible_wrt Q by A1;
hence a,b are_convertible_wrt R iff a,b are_convergent_wrt Q by Def23,Th38;
end;
theorem
for R being Relation, C being Completion of R, a,b being set 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 set;
A1: a,b are_convertible_wrt R iff a,b are_convergent_wrt C by Def28;
a,b are_convergent_wrt C implies a,b are_convertible_wrt C by Th38;
hence a,b are_convertible_wrt R implies nf(a,C) = nf(b,C) by Def28,Th56;
nf(a,C) is_a_normal_form_of a,C & nf(b,C) is_a_normal_form_of b,C
by Th55;
then C reduces a,nf(a,C) & C reduces b,nf(b,C) by Def6;
hence thesis by A1,Def7;
end;