let G be non empty DTConstrStr ; :: thesis: for n1, n2, n3 being String of G st n1 is_derivable_from n2 & n2 is_derivable_from n3 holds
n1 is_derivable_from n3
let n1, n2, n3 be String of G; :: thesis: ( n1 is_derivable_from n2 & n2 is_derivable_from n3 implies n1 is_derivable_from n3 )
given p1 being FinSequence such that A1: len p1 >= 1 and
A2: p1 . 1 = n2 and
A3: p1 . (len p1) = n1 and
A4: for i being Element of NAT st i >= 1 & i < len p1 holds
ex a, b being String of G st
( p1 . i = a & p1 . (i + 1) = b & a ==> b ) ; :: according to LANG1:def 5 :: thesis: ( not n2 is_derivable_from n3 or n1 is_derivable_from n3 )
given p2 being FinSequence such that A5: len p2 >= 1 and
A6: p2 . 1 = n3 and
A7: p2 . (len p2) = n2 and
A8: for i being Element of NAT st i >= 1 & i < len p2 holds
ex a, b being String of G st
( p2 . i = a & p2 . (i + 1) = b & a ==> b ) ; :: according to LANG1:def 5 :: thesis: n1 is_derivable_from n3
p2 <> {} by A5;
then consider q being FinSequence, x being set such that
A9: p2 = q ^ <*x*> by FINSEQ_1:63;
take p = q ^ p1; :: according to LANG1:def 5 :: thesis: ( len p >= 1 & p . 1 = n3 & p . (len p) = n1 & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
A10: 1 + (len q) >= 1 by NAT_1:11;
A11: len p = (len q) + (len p1) by FINSEQ_1:35;
then len p >= 1 + (len q) by A1, XREAL_1:9;
hence len p >= 1 by A10, XXREAL_0:2; :: thesis: ( p . 1 = n3 & p . (len p) = n1 & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )

now

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

suppose A12: q = {} ; :: thesis: p . 1 = n3

then A13: p = p1 by FINSEQ_1:47;
p2 = <*x*> by A9, A12, FINSEQ_1:47;
hence p . 1 = n3 by A2, A6, A7, A13, FINSEQ_1:57; :: thesis: verum

end;

suppose A14: q <> {} ; :: thesis: p . 1 = n3

A15: 0 + 1 = 1 ;
len q > 0 by A14, NAT_1:2;
then len q >= 1 by A15, NAT_1:13;
then A16: 1 in dom q by FINSEQ_3:27;
then p . 1 = q . 1 by FINSEQ_1:def 7;
hence p . 1 = n3 by A6, A9, A16, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence p . 1 = n3 ; :: thesis: ( p . (len p) = n1 & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
len p1 in dom p1 by A1, FINSEQ_3:27;
hence p . (len p) = n1 by A3, A11, FINSEQ_1:def 7; :: thesis: for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
let i be Element of NAT ; :: thesis: ( i >= 1 & i < len p implies ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) )
assume that
A17: i >= 1 and
A18: i < len p ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
len <*x*> = 1 by FINSEQ_1:57;
then A19: len p2 = (len q) + 1 by A9, FINSEQ_1:35;

now

per cases ( i + 1 = len p2 or i + 1 > len p2 or i + 1 < len p2 ) by XXREAL_0:1;

suppose A20: i + 1 = len p2 ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )

A21: 1 in dom p1 by A1, FINSEQ_3:27;
i < len p2 by A20, NAT_1:13;
then consider a, b being String of G such that
A22: p2 . i = a and
A23: p2 . (i + 1) = b and
A24: a ==> b by A8, A17;
take a = a; :: thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = b; :: thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
A25: i in dom q by A19, A17, A20, FINSEQ_3:27;
then p2 . i = q . i by A9, FINSEQ_1:def 7;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A2, A7, A19, A20, A22, A23, A24, A21, A25, FINSEQ_1:def 7; :: thesis: verum

end;

suppose i + 1 > len p2 ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )

then i >= len p2 by NAT_1:13;
then consider j being Nat such that
A26: i = (len p2) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A27: i = (len q) + (1 + j) by A19, A26;
then A28: 1 + j < len p1 by A11, A18, XREAL_1:8;
then consider a, b being String of G such that
A29: p1 . (1 + j) = a and
A30: p1 . ((1 + j) + 1) = b and
A31: a ==> b by A4, NAT_1:11;
take a = a; :: thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = b; :: thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
A32: (1 + j) + 1 >= 1 by NAT_1:11;
1 + j >= 1 by NAT_1:11;
then A33: 1 + j in dom p1 by A28, FINSEQ_3:27;
(1 + j) + 1 <= len p1 by A28, NAT_1:13;
then A34: (1 + j) + 1 in dom p1 by A32, FINSEQ_3:27;
i + 1 = (len q) + ((1 + j) + 1) by A19, A26;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A27, A29, A30, A31, A33, A34, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A35: i + 1 < len p2 ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )

A36: 1 <= 1 + i by NAT_1:11;
i + 1 <= len q by A19, A35, NAT_1:13;
then A37: i + 1 in dom q by A36, FINSEQ_3:27;
then A38: p . (i + 1) = q . (i + 1) by FINSEQ_1:def 7;
i < len p2 by A35, NAT_1:13;
then consider a, b being String of G such that
A39: p2 . i = a and
A40: p2 . (i + 1) = b and
A41: a ==> b by A8, A17;
take a = a; :: thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = b; :: thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
i <= len q by A19, A35, XREAL_1:8;
then A42: i in dom q by A17, FINSEQ_3:27;
then p . i = q . i by FINSEQ_1:def 7;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A9, A39, A40, A41, A42, A37, A38, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ; :: thesis: verum