let R be Relation; :: thesis: ex Q being complete Relation st
( field Q c= field R & ( for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )

per cases ( R = {} or R <> {} ) ;

suppose A1: R = {} ; :: thesis: ex Q being complete Relation st
( field Q c= field R & ( for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )

take E = {} ; :: thesis: ( field E c= field R & ( for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt E ) ) )
thus field E c= field R ; :: thesis: for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt E )
let a, b be object ; :: thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt E )
( a,b are_convertible_wrt R iff a = b ) by A1, Th26, Th27;
hence ( a,b are_convertible_wrt R iff a,b are_convergent_wrt E ) by Th38, Th39; :: thesis: verum

end;

suppose R <> {} ; :: thesis: ex Q being complete Relation st
( field Q c= field R & ( for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q ) ) )

then reconsider R9 = R as non empty Relation ;
set xx = the Element of R9;
consider x1, x2 being object such that
A2: the Element of R9 = [x1,x2] by RELAT_1:def 1;
defpred S₁[ object , object ] means $1,$2 are_convertible_wrt R;
A3: for x, y being object st S₁[x,y] holds
S₁[y,x] by Lm5;
A4: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by Th30;
A5: for x being object st x in field R holds
S₁[x,x] by Th26;
consider Q being Equivalence_Relation of (field R) such that
A6: for x, y being object holds
( [x,y] in Q iff ( x in field R & y in field R & S₁[x,y] ) ) from EQREL_1:sch 1(A5, A3, A4);
A7: ( ( for X being set st X in Class Q holds
X <> {} ) & ( for X, Y being set st X in Class Q & Y in Class Q & X <> Y holds
X misses Y ) ) by EQREL_1:def 4;
x1 in field R by A2, RELAT_1:15;
then Class (Q,x1) in Class Q by EQREL_1:def 3;
then consider X being set such that
A8: for A being set st A in Class Q holds
ex x being object st X /\ A = {x} by A7, WELLORD2:18;
defpred S₂[ object , object ] means ( $1 <> $2 & $1,$2 are_convertible_wrt R & $2 in X );
consider P being Relation such that
A9: for x, y being object holds
( [x,y] in P iff ( x in field R & y in field R & S₂[x,y] ) ) from RELAT_1:sch 1();
A10: P is locally-confluent

proof

let a, b, c be object ; :: according to REWRITE1:def 24 :: thesis: ( [a,b] in P & [a,c] in P implies b,c are_convergent_wrt P )
assume that
A11: [a,b] in P and
A12: [a,c] in P ; :: thesis: b,c are_convergent_wrt P
A13: a in field R by A9, A11;
then Class (Q,a) in Class Q by EQREL_1:def 3;
then consider x being object such that
A14: X /\ (Class (Q,a)) = {x} by A8;
( c in field R & a,c are_convertible_wrt R ) by A9, A12;
then [a,c] in Q by A6, A13;
then [c,a] in Q by EQREL_1:6;
then A15: c in Class (Q,a) by EQREL_1:19;
c in X by A9, A12;
then c in {x} by A15, A14, XBOOLE_0:def 4;
then A16: c = x by TARSKI:def 1;
( b in field R & a,b are_convertible_wrt R ) by A9, A11;
then [a,b] in Q by A6, A13;
then [b,a] in Q by EQREL_1:6;
then A17: b in Class (Q,a) by EQREL_1:19;
take b ; :: according to REWRITE1:def 7 :: thesis: ( P reduces b,b & P reduces c,b )
b in X by A9, A11;
then b in {x} by A17, A14, XBOOLE_0:def 4;
then b = x by TARSKI:def 1;
hence ( P reduces b,b & P reduces c,b ) by A16, Th12; :: thesis: verum

end;

A18: for x, y being object st P reduces x,y holds
x,y are_convertible_wrt R

proof

let x, y be object ; :: thesis: ( P reduces x,y implies x,y are_convertible_wrt R )
given p being RedSequence of P such that A19: x = p . 1 and
A20: y = p . (len p) ; :: according to REWRITE1:def 3 :: thesis: x,y are_convertible_wrt R
defpred S₃[ Nat] means ( $1 in dom p implies x,p . $1 are_convertible_wrt R );

now :: thesis: for i being Nat st ( i in dom p implies x,p . i are_convertible_wrt R ) & i + 1 in dom p holds
x,p . (i + 1) are_convertible_wrt R

let i be Nat; :: thesis: ( ( i in dom p implies x,p . i are_convertible_wrt R ) & i + 1 in dom p implies x,p . (b₁ + 1) are_convertible_wrt R )
assume that
A21: ( i in dom p implies x,p . i are_convertible_wrt R ) and
A22: i + 1 in dom p ; :: thesis: x,p . (b₁ + 1) are_convertible_wrt R
A23: i < len p by A22, Lm2;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: x,p . (b₁ + 1) are_convertible_wrt R

hence x,p . (i + 1) are_convertible_wrt R by A19, Th26; :: thesis: verum

end;

suppose A24: i > 0 ; :: thesis: x,p . (b₁ + 1) are_convertible_wrt R

then i in dom p by A23, Lm3;
then [(p . i),(p . (i + 1))] in P by A22, Def2;
then p . i,p . (i + 1) are_convertible_wrt R by A9;
hence x,p . (i + 1) are_convertible_wrt R by A21, A23, A24, Lm3, Th30; :: thesis: verum

end;

end;

end;

then A25: for k being Nat st S₃[k] holds
S₃[k + 1] ;
A26: len p in dom p by FINSEQ_5:6;
A27: S₃[ 0 ] by Lm1;
for i being Nat holds S₃[i] from NAT_1:sch 2(A27, A25);
hence x,y are_convertible_wrt R by A20, A26; :: thesis: verum

end;

P is strongly-normalizing

proof

let f be ManySortedSet of NAT ; :: according to REWRITE1:def 15 :: thesis: not for i being Nat holds [(f . i),(f . (i + 1))] in P

per cases ( not [(f . 0),(f . (0 + 1))] in P or [(f . 0),(f . (0 + 1))] in P ) ;

suppose not [(f . 0),(f . (0 + 1))] in P ; :: thesis: not for i being Nat holds [(f . i),(f . (i + 1))] in P

hence not for i being Nat holds [(f . i),(f . (i + 1))] in P ; :: thesis: verum

end;

suppose A28: [(f . 0),(f . (0 + 1))] in P ; :: thesis: not for i being Nat holds [(f . i),(f . (i + 1))] in P

take j = 0 + 1; :: thesis: not [(f . j),(f . (j + 1))] in P
A29: f . j in X by A9, A28;
assume A30: [(f . j),(f . (j + 1))] in P ; :: thesis: contradiction
then A31: f . j in field R by A9;
then Class (Q,(f . j)) in Class Q by EQREL_1:def 3;
then consider x being object such that
A32: X /\ (Class (Q,(f . j))) = {x} by A8;
( f . (j + 1) in field R & f . j,f . (j + 1) are_convertible_wrt R ) by A9, A30;
then [(f . j),(f . (j + 1))] in Q by A6, A31;
then [(f . (j + 1)),(f . j)] in Q by EQREL_1:6;
then A33: f . (j + 1) in Class (Q,(f . j)) by EQREL_1:19;
f . j in Class (Q,(f . j)) by A31, EQREL_1:20;
then f . j in X /\ (Class (Q,(f . j))) by A29, XBOOLE_0:def 4;
then A34: f . j = x by A32, TARSKI:def 1;
f . (j + 1) in X by A9, A30;
then f . (j + 1) in X /\ (Class (Q,(f . j))) by A33, XBOOLE_0:def 4;
then f . (j + 1) = x by A32, TARSKI:def 1;
hence contradiction by A9, A30, A34; :: thesis: verum

end;

end;

end;

then reconsider P = P as strongly-normalizing locally-confluent Relation by A10;
take P ; :: thesis: ( field P c= field R & ( for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt P ) ) )
thus field P c= field R :: thesis: for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in field P or x in field R )
assume x in field P ; :: thesis: x in field R
then ( x in dom P or x in rng P ) by XBOOLE_0:def 3;
then ( ex y being object st [x,y] in P or ex y being object st [y,x] in P ) by XTUPLE_0:def 12, XTUPLE_0:def 13;
hence x in field R by A9; :: thesis: verum

end;

let a, b be object ; :: thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )
thus ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P ) :: thesis: verum

proof

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )

hence ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P ) by Th26, Th38; :: thesis: verum

end;

suppose A35: a <> b ; :: thesis: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )

hereby :: thesis: ( a,b are_convergent_wrt P implies a,b are_convertible_wrt R )

assume A36: a,b are_convertible_wrt R ; :: thesis: a,b are_convergent_wrt P
then A37: b in field R by A35, Th32;
then Class (Q,b) in Class Q by EQREL_1:def 3;
then consider x being object such that
A38: X /\ (Class (Q,b)) = {x} by A8;
A39: a in field R by A35, A36, Th32;
then A40: [a,b] in Q by A6, A36, A37;
thus a,b are_convergent_wrt P :: thesis: verum

proof

take x ; :: according to REWRITE1:def 7 :: thesis: ( P reduces a,x & P reduces b,x )
A41: x in {x} by TARSKI:def 1;
then A42: x in X by A38, XBOOLE_0:def 4;
A43: x in Class (Q,b) by A38, A41, XBOOLE_0:def 4;
then [x,b] in Q by EQREL_1:19;
then [b,x] in Q by EQREL_1:6;
then b,x are_convertible_wrt R by A6;
then A44: ( b = x or [b,x] in P ) by A9, A37, A38, A41, A42;
a in Class (Q,b) by A40, EQREL_1:19;
then [a,x] in Q by A43, EQREL_1:22;
then a,x are_convertible_wrt R by A6;
then ( a = x or [a,x] in P ) by A9, A39, A38, A41, A42;
hence ( P reduces a,x & P reduces b,x ) by A44, Th12, Th15; :: thesis: verum

end;

end;

given c being object such that A45: ( P reduces a,c & P reduces b,c ) ; :: according to REWRITE1:def 7 :: thesis: a,b are_convertible_wrt R
( a,c are_convertible_wrt R & c,b are_convertible_wrt R ) by A18, A45, Lm5;
hence a,b are_convertible_wrt R by Th30; :: thesis: verum

end;

end;

end;

end;

end;