let n, m be Nat; :: thesis: for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= n & n <= len L holds
( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) & the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) )
let L be FinSequence; :: thesis: for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= n & n <= len L holds
( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) & the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) )
let v be LTL-formula; :: thesis: ( L is_Finseq_for v & 1 <= m & m <= n & n <= len L implies ( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) & the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) ) )
assume A1: ( L is_Finseq_for v & 1 <= m & m <= n & n <= len L ) ; :: thesis: ( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) & the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) )
defpred S₁[ Nat] means for n1, m1 being Nat
for L1 being FinSequence st len L1 <= $1 & L1 is_Finseq_for v & 1 <= m1 & m1 <= n1 & n1 <= len L1 holds
( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),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 n1, m1 be Nat; :: thesis: for L1 being FinSequence st len L1 <= k + 1 & L1 is_Finseq_for v & 1 <= m1 & m1 <= n1 & n1 <= len L1 holds
( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) )
let L1 be FinSequence; :: thesis: ( len L1 <= k + 1 & L1 is_Finseq_for v & 1 <= m1 & m1 <= n1 & n1 <= len L1 implies ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) )
assume A4: len L1 <= k + 1 ; :: thesis: ( not L1 is_Finseq_for v or not 1 <= m1 or not m1 <= n1 or not n1 <= len L1 or ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) )

now :: thesis: ( not L1 is_Finseq_for v or not 1 <= m1 or not m1 <= n1 or not n1 <= len L1 or ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),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 1 <= m1 or not m1 <= n1 or not n1 <= len L1 or ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) )

hence ( not L1 is_Finseq_for v or not 1 <= m1 or not m1 <= n1 or not n1 <= len L1 or ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) ) by A3; :: thesis: verum

end;

suppose A5: len L1 = k + 1 ; :: thesis: ( not L1 is_Finseq_for v or not 1 <= m1 or not m1 <= n1 or not n1 <= len L1 or ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) )

( L1 is_Finseq_for v & 1 <= m1 & m1 <= n1 & n1 <= len L1 implies ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) )

proof

assume that
A6: L1 is_Finseq_for v and
A7: 1 <= m1 and
A8: m1 <= n1 and
A9: n1 <= len L1 ; :: thesis: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) )
A10: 1 <= n1 by A7, A8, XXREAL_0:2;

now :: thesis: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) )

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

suppose A11: n1 <= k ; :: thesis: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),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 A10, A11, FINSEQ_1:1;
then A14: L2 . n1 = L1 . n1 by FUNCT_1:47;
m1 <= k by A8, A11, XXREAL_0:2;
then m1 in dom L2 by A7, A13, FINSEQ_1:1;
then A15: L2 . m1 = L1 . m1 by FUNCT_1:47;
( len L2 = k & L2 is_Finseq_for v ) by A5, A6, A12, Th26, FINSEQ_1:17;
hence ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) by A3, A7, A8, A11, A15, A14; :: thesis: verum

end;

suppose A16: n1 = k + 1 ; :: thesis: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) )

now :: thesis: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) )

per cases ( m1 < n1 or m1 = n1 ) by A8, XXREAL_0:1;

suppose A17: m1 < n1 ; :: thesis: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) )

set L2 = L1 | (Seg k);
reconsider L2 = L1 | (Seg k) as FinSequence by FINSEQ_1:15;
A18: m1 <= k by A16, A17, NAT_1:13;
A19: k + 0 <= k + 1 by XREAL_1:7;
then A20: dom L2 = Seg k by A5, FINSEQ_1:17;
then m1 in dom L2 by A7, A18, FINSEQ_1:1;
then A21: L2 . m1 = L1 . m1 by FUNCT_1:47;
A22: 1 <= k by A7, A18, XXREAL_0:2;
then k in dom L2 by A20, FINSEQ_1:1;
then A23: L2 . k = L1 . k by FUNCT_1:47;
( len L2 = k & L2 is_Finseq_for v ) by A5, A6, A19, Th26, FINSEQ_1:17;
then A24: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . k),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . k),v)) ) by A3, A7, A18, A21, A23;
k < len L1 by A5, NAT_1:13;
then consider N1, N2 being strict LTLnode over v such that
A25: ( N1 = L1 . k & N2 = L1 . (k + 1) ) and
A26: N2 is_succ_of N1 by A6, A22;
A27: ( N1 = CastNode (N1,v) & N2 = CastNode (N2,v) ) by Def16;
( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 ) by A26, Th25;
hence ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) by A16, A24, A25, A27; :: thesis: verum

end;

suppose m1 = n1 ; :: thesis: ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) )

hence ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) ; :: thesis: verum

end;

end;

end;

hence ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) ; :: thesis: verum

end;

end;

end;

hence ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) ; :: thesis: verum

end;

hence ( not L1 is_Finseq_for v or not 1 <= m1 or not m1 <= n1 or not n1 <= len L1 or ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) ) ; :: thesis: verum

end;

end;

end;

hence ( not L1 is_Finseq_for v or not 1 <= m1 or not m1 <= n1 or not n1 <= len L1 or ( the LTLold of (CastNode ((L1 . m1),v)) c= the LTLold of (CastNode ((L1 . n1),v)) & the LTLnext of (CastNode ((L1 . m1),v)) c= the LTLnext of (CastNode ((L1 . n1),v)) ) ) ; :: thesis: verum

end;

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

end;

A28: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A28, A2);
hence ( the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . n),v)) & the LTLnext of (CastNode ((L . m),v)) c= the LTLnext of (CastNode ((L . n),v)) ) by A1; :: thesis: verum