let n be Nat; :: thesis: for L being FinSequence
for F, v being LTL-formula st L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) holds
ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
let L be FinSequence; :: thesis: for F, v being LTL-formula st L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) holds
ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
let F, v be LTL-formula; :: thesis: ( L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) implies ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) ) )
assume A1: ( L is_Finseq_for v & F in the LTLnew of (CastNode ((L . 1),v)) & 1 < n & n <= len L & not F in the LTLnew of (CastNode ((L . n),v)) ) ; :: thesis: ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) )
defpred S₁[ Nat] means for F1 being LTL-formula
for n1 being Nat
for L1 being FinSequence st len L1 <= $1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) holds
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) );
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let F1 be LTL-formula; :: thesis: for n1 being Nat
for L1 being FinSequence st len L1 <= k + 1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) holds
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )
let n1 be Nat; :: thesis: for L1 being FinSequence st len L1 <= k + 1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) holds
ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )
let L1 be FinSequence; :: thesis: ( len L1 <= k + 1 & L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) implies ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )
assume A4: len L1 <= k + 1 ; :: thesis: ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )

now :: thesis: ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )

per cases ( len L1 <= k or len L1 = k + 1 ) by A4, NAT_1:8;

suppose len L1 <= k ; :: thesis: ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )

hence ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) ) by A3; :: thesis: verum

end;

suppose A5: len L1 = k + 1 ; :: thesis: ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )

( L1 is_Finseq_for v & F1 in the LTLnew of (CastNode ((L1 . 1),v)) & 1 < n1 & n1 <= len L1 & not F1 in the LTLnew of (CastNode ((L1 . n1),v)) implies ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) )

proof

assume that
A6: L1 is_Finseq_for v and
A7: F1 in the LTLnew of (CastNode ((L1 . 1),v)) and
A8: 1 < n1 and
A9: n1 <= len L1 and
A10: not F1 in the LTLnew of (CastNode ((L1 . n1),v)) ; :: thesis: ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )

now :: thesis: ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )

per cases ( n1 <= k or n1 = k + 1 ) by A5, A9, NAT_1:8;

suppose A11: n1 <= k ; :: thesis: ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )

set L2 = L1 | (Seg k);
reconsider L2 = L1 | (Seg k) as FinSequence by FINSEQ_1:15;
A12: k + 0 <= k + 1 by XREAL_1:7;
then A13: dom L2 = Seg k by A5, FINSEQ_1:17;
then n1 in dom L2 by A8, A11, FINSEQ_1:1;
then A14: L2 . n1 = L1 . n1 by FUNCT_1:47;
1 < k by A8, A11, XXREAL_0:2;
then 1 in dom L2 by A13, FINSEQ_1:1;
then A15: F1 in the LTLnew of (CastNode ((L2 . 1),v)) by A7, FUNCT_1:47;
( len L2 = k & L2 is_Finseq_for v ) by A5, A6, A12, Th26, FINSEQ_1:17;
then consider m being Nat such that
A16: 1 <= m and
A17: m < n1 and
A18: ( F1 in the LTLnew of (CastNode ((L2 . m),v)) & not F1 in the LTLnew of (CastNode ((L2 . (m + 1)),v)) ) by A3, A8, A10, A11, A15, A14;
m + 1 <= n1 by A17, NAT_1:13;
then A19: m + 1 <= k by A11, XXREAL_0:2;
1 <= m + 1 by A16, NAT_1:13;
then m + 1 in dom L2 by A13, A19, FINSEQ_1:1;
then A20: L2 . (m + 1) = L1 . (m + 1) by FUNCT_1:47;
m <= k by A11, A17, XXREAL_0:2;
then m in dom L2 by A13, A16, FINSEQ_1:1;
then L2 . m = L1 . m by FUNCT_1:47;
hence ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) by A16, A17, A18, A20; :: thesis: verum

end;

suppose A21: n1 = k + 1 ; :: thesis: ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )

then A22: 1 <= k by A8, NAT_1:13;
A23: k + 0 < k + 1 by XREAL_1:8;

now :: thesis: ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )

per cases ( F1 in the LTLnew of (CastNode ((L1 . k),v)) or not F1 in the LTLnew of (CastNode ((L1 . k),v)) ) ;

suppose F1 in the LTLnew of (CastNode ((L1 . k),v)) ; :: thesis: ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )

hence ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) by A10, A21, A23, A22; :: thesis: verum

end;

suppose A24: not F1 in the LTLnew of (CastNode ((L1 . k),v)) ; :: thesis: ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) )

A25: 1 < k

proof

set b = 1 - k;
set a = k - 1;
A26: ( (k - 1) + (1 - k) = 0 & 1 - 1 <= k - 1 ) by A22, XREAL_1:9;

now :: thesis: not k <= 1

assume k <= 1 ; :: thesis: contradiction
then 1 - 1 <= 1 - k by XREAL_1:10;
then k - 1 = 0 by A26;
hence contradiction by A7, A24; :: thesis: verum

end;

hence 1 < k ; :: thesis: verum

end;

set L2 = L1 | (Seg k);
reconsider L2 = L1 | (Seg k) as FinSequence by FINSEQ_1:15;
A27: k + 0 <= k + 1 by XREAL_1:7;
then A28: dom L2 = Seg k by A5, FINSEQ_1:17;
then k in dom L2 by A22, FINSEQ_1:1;
then A29: not F1 in the LTLnew of (CastNode ((L2 . k),v)) by A24, FUNCT_1:47;
1 in dom L2 by A22, A28, FINSEQ_1:1;
then A30: F1 in the LTLnew of (CastNode ((L2 . 1),v)) by A7, FUNCT_1:47;
( len L2 = k & L2 is_Finseq_for v ) by A5, A6, A27, Th26, FINSEQ_1:17;
then consider m being Nat such that
A31: 1 <= m and
A32: m < k and
A33: F1 in the LTLnew of (CastNode ((L2 . m),v)) and
A34: not F1 in the LTLnew of (CastNode ((L2 . (m + 1)),v)) by A3, A30, A29, A25;
m in dom L2 by A28, A31, A32, FINSEQ_1:1;
then A35: F1 in the LTLnew of (CastNode ((L1 . m),v)) by A33, FUNCT_1:47;
( 1 <= m + 1 & m + 1 <= k ) by A31, A32, NAT_1:13;
then m + 1 in dom L2 by A28, FINSEQ_1:1;
then A36: L2 . (m + 1) = L1 . (m + 1) by FUNCT_1:47;
m < n1 by A21, A23, A32, XXREAL_0:2;
hence ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) by A31, A34, A35, A36; :: thesis: verum

end;

end;

end;

hence ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) ; :: thesis: verum

end;

end;

end;

hence ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) ; :: thesis: verum

end;

hence ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) ) ; :: thesis: verum

end;

end;

end;

hence ( not L1 is_Finseq_for v or not F1 in the LTLnew of (CastNode ((L1 . 1),v)) or not 1 < n1 or not n1 <= len L1 or F1 in the LTLnew of (CastNode ((L1 . n1),v)) or ex m being Nat st
( 1 <= m & m < n1 & F1 in the LTLnew of (CastNode ((L1 . m),v)) & not F1 in the LTLnew of (CastNode ((L1 . (m + 1)),v)) ) ) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A37: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A37, A2);
hence ex m being Nat st
( 1 <= m & m < n & F in the LTLnew of (CastNode ((L . m),v)) & not F in the LTLnew of (CastNode ((L . (m + 1)),v)) ) by A1; :: thesis: verum