let R be Relation; :: thesis: 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 ) ) )

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

suppose A1: R = {} ; :: thesis: 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 ) ) )

take E = {} ; :: thesis: ( field E c= field R & ( for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt E ) ) )
thus field E c= field R by XBOOLE_1:2; :: thesis: for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt E )
let a, b be set ; :: 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, Th27, Th28;
hence ( a,b are_convertible_wrt R iff a,b are_convergent_wrt E ) by Th39, Th40; :: thesis: verum

end;

suppose R <> {} ; :: thesis: 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 ) ) )

then reconsider R9 = R as non empty Relation ;
consider xx being Element of R9;
consider x1, x2 being set such that
A2: xx = [x1,x2] by RELAT_1:def 1;
defpred S₁[ set , set ] means $1,$2 are_convertible_wrt R;
A3: for x, y being set st S₁[x,y] holds
S₁[y,x] by Lm5;
A4: for x, y, z being set st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by Th31;
A5: for x being set st x in field R holds
S₁[x,x] by Th27;
consider Q being Equivalence_Relation of (field R) such that
A6: for x, y being set 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 6;
x1 in field R by A2, RELAT_1:30;
then Class (Q,x1) in Class Q by EQREL_1:def 5;
then consider X being set such that
A8: for A being set st A in Class Q holds
ex x being set st X /\ A = {x} by A7, WELLORD2:27;
defpred S₂[ set , set ] means ( $1 <> $2 & $1,$2 are_convertible_wrt R & $2 in X );
consider P being Relation such that
A9: for x, y being set 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 set ; :: 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 5;
then consider x being set 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:12;
then A15: c in Class (Q,a) by EQREL_1:27;
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:12;
then A17: b in Class (Q,a) by EQREL_1:27;
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, Th13; :: thesis: verum

end;

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

proof

let x, y be set ; :: 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₃[ Element of NAT ] means ( $1 in dom p implies x,p . $1 are_convertible_wrt R );

now

let i be Element of 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, Th27; :: 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, Th31; :: thesis: verum

end;

end;

end;

then A25: for k being Element of 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 Element of NAT holds S₃[i] from NAT_1:sch 1(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 Element of 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 Element of NAT holds [(f . i),(f . (i + 1))] in P

hence not for i being Element of 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 Element of 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 5;
then consider x being set 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:12;
then A33: f . (j + 1) in Class (Q,(f . j)) by EQREL_1:27;
f . j in Class (Q,(f . j)) by A31, EQREL_1:28;
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 set 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 set holds
( a,b are_convertible_wrt R iff a,b are_convergent_wrt P )

proof

let x be set ; :: 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 set st [x,y] in P or ex y being set st [y,x] in P ) by RELAT_1:def 4, RELAT_1:def 5;
hence x in field R by A9; :: thesis: verum

end;

let a, b be set ; :: 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 Th27, Th39; :: 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, Th33;
then Class (Q,b) in Class Q by EQREL_1:def 5;
then consider x being set such that
A38: X /\ (Class (Q,b)) = {x} by A8;
A39: a in field R by A35, A36, Th33;
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:27;
then [b,x] in Q by EQREL_1:12;
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:27;
then [a,x] in Q by A43, EQREL_1:30;
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, Th13, Th16; :: thesis: verum

end;

end;

given c being set 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 Th31; :: thesis: verum

end;

end;

end;

end;

end;