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;