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 & p1 . 1 = n2 & p1 . (len p1) = n1 & ( 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 A2: ( len p2 >= 1 & p2 . 1 = n3 & p2 . (len p2) = n2 & ( 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 A2;
then consider q being FinSequence, x being set such that
A3: 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 ) ) )
len <*x*> = 1 by FINSEQ_1:57;
then A4: ( len p = (len q) + (len p1) & len p2 = (len q) + 1 & dom q = dom q & dom p2 = dom p2 & dom p1 = dom p1 ) by A3, FINSEQ_1:35;
then ( len p >= 1 + (len q) & 1 + (len q) >= 1 ) by A1, NAT_1:11, XREAL_1:9;
hence len p >= 1 by 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 q = {} ; :: thesis: p . 1 = n3

then ( p2 = <*x*> & p = p1 ) by A3, FINSEQ_1:47;
hence p . 1 = n3 by A1, A2, FINSEQ_1:57; :: thesis: verum

end;

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

then ( len q <> 0 & len q >= 0 ) by NAT_1:2;
then ( len q > 0 & 0 + 1 = 1 ) ;
then len q >= 1 by NAT_1:13;
then 1 in dom q by FINSEQ_3:27;
then ( p . 1 = q . 1 & q . 1 = p2 . 1 ) by A3, FINSEQ_1:def 7;
hence p . 1 = n3 by A2; :: 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 A1, A4, 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 A5: ( i >= 1 & i < len p ) ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )

now

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

suppose A6: 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 q & i < len p2 ) by A4, NAT_1:13;
then consider a, b being String of G such that
A7: ( p2 . i = a & p2 . (i + 1) = b & a ==> b ) by A2, A5;
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 )
( 1 in dom p1 & i in dom q ) by A1, A4, A5, A6, FINSEQ_3:27;
then ( p . (i + 1) = p1 . 1 & p2 . i = q . i & q . i = p . i ) by A3, A4, A6, FINSEQ_1:def 7;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A1, A2, A6, A7; :: 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 & i + 1 <= len p ) by A5, NAT_1:13;
then consider j being Nat such that
A8: i = (len p2) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A9: ( i = (len q) + (1 + j) & 1 + j >= 1 ) by A4, A8, NAT_1:11;
then A10: 1 + j < len p1 by A4, A5, XREAL_1:8;
then consider a, b being String of G such that
A11: ( p1 . (1 + j) = a & p1 . ((1 + j) + 1) = b & a ==> b ) by A1, A9;
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 )
A12: ( (1 + j) + 1 = 1 + (1 + j) & i + 1 = (len q) + ((1 + j) + 1) ) by A4, A8;
( 1 + j <= len p1 & (1 + j) + 1 <= len p1 & (1 + j) + 1 >= 1 ) by A10, NAT_1:11, NAT_1:13;
then ( 1 + j in dom p1 & (1 + j) + 1 in dom p1 ) by A9, FINSEQ_3:27;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A9, A11, A12, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A13: 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 a, b being String of G such that
A14: ( p2 . i = a & p2 . (i + 1) = b & a ==> b ) by A2, A5;
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 & i + 1 <= len q & 1 <= 1 + i & i + 1 = 1 + i ) by A4, A13, NAT_1:11, NAT_1:13, XREAL_1:8;
then ( i in dom q & i + 1 in dom q ) by A5, FINSEQ_3:27;
then ( p . i = q . i & q . i = p2 . i & p . (i + 1) = q . (i + 1) & q . (i + 1) = p2 . (i + 1) ) by A3, FINSEQ_1:def 7;
hence ( p . i = a & p . (i + 1) = b & a ==> b ) by A14; :: 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