let R be Relation; ( R is subcommutative implies for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )
assume A1:
R is subcommutative
; for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R
let a, b, c be object ; ( R reduces a,b & [a,c] in R implies b,c are_convergent_wrt R )
given p being RedSequence of R such that A2:
p . 1 = a
and
A3:
p . (len p) = b
; REWRITE1:def 3 ( not [a,c] in R or b,c are_convergent_wrt R )
defpred S1[ Nat] means ( $1 in dom p implies ex d being object st
( ( [(p . $1),d] in R or p . $1 = d ) & R reduces c,d ) );
assume A4:
[a,c] in R
; b,c are_convergent_wrt R
now for i being Nat st ( i in dom p implies S1[i] ) & i + 1 in dom p holds
S1[i + 1]let i be
Nat;
( ( i in dom p implies S1[i] ) & i + 1 in dom p implies S1[b1 + 1] )assume that A5:
(
i in dom p implies
S1[
i] )
and A6:
i + 1
in dom p
;
S1[b1 + 1]per cases
( i = 0 or i > 0 )
;
suppose A8:
i > 0
;
S1[b1 + 1]A9:
i < len p
by A6, Lm2;
then consider d being
object such that A10:
(
[(p . i),d] in R or
p . i = d )
and A11:
R reduces c,
d
by A5, A8, Lm3;
i in dom p
by A8, A9, Lm3;
then A12:
[(p . i),(p . (i + 1))] in R
by A6, Def2;
A13:
now ( [(p . i),d] in R implies ex e being object st
( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e ) )assume
[(p . i),d] in R
;
ex e being object st
( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )then
p . (i + 1),
d are_convergent<=1_wrt R
by A1, A12;
then consider e being
object such that A14:
(
[(p . (i + 1)),e] in R or
p . (i + 1) = e )
and A15:
(
[d,e] in R or
d = e )
;
take e =
e;
( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )thus
(
[(p . (i + 1)),e] in R or
p . (i + 1) = e )
by A14;
R reduces c,e
R reduces d,
e
by A15, Th12, Th15;
hence
R reduces c,
e
by A11, Th16;
verum end; hence
S1[
i + 1]
by A10, A13;
verum end; end; end;
then A16:
for k being Nat st S1[k] holds
S1[k + 1]
;
A17:
len p in dom p
by FINSEQ_5:6;
A18:
S1[ 0 ]
by Lm1;
for i being Nat holds S1[i]
from NAT_1:sch 2(A18, A16);
then consider d being object such that
A19:
( ( [b,d] in R or b = d ) & R reduces c,d )
by A3, A17;
take
d
; REWRITE1:def 7 ( R reduces b,d & R reduces c,d )
thus
( R reduces b,d & R reduces c,d )
by A19, Th12, Th15; verum