let m, n 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 that
A1: L is_Finseq_for v and
A2: ( 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) );
A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: 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 C1: 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

per cases ( len L1 <= k or len L1 = k + 1 ) by C1, 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 B1; :: thesis: verum

end;

suppose C3: 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
D1: L1 is_Finseq_for v and
D2: ( 1 <= m1 & m1 <= n1 & 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) )
D3: 1 <= n1 by D2, XXREAL_0:2;

now

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

suppose D5: 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:19;
E0: k + 0 <= k + 1 by XREAL_1:9;
then E1: ( len L2 = k & dom L2 = Seg k ) by C3, FINSEQ_1:21;
E3: L2 is_Finseq_for v by D1, E0, C3, ThSucc02;
( 1 <= m1 & m1 <= k ) by D5, D2, XXREAL_0:2;
then m1 in dom L2 by E1, FINSEQ_1:3;
then E4: L2 . m1 = L1 . m1 by FUNCT_1:70;
n1 in dom L2 by E1, D5, D3, FINSEQ_1:3;
then L2 . n1 = L1 . n1 by FUNCT_1:70;
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 E1, B1, D5, D2, E3, E4; :: thesis: verum

end;

suppose D6: 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

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

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) )

then D600: m1 <= k by D6, NAT_1:13;
then D601: 1 <= k by D2, XXREAL_0:2;
set L2 = L1 | (Seg k);
reconsider L2 = L1 | (Seg k) as FinSequence by FINSEQ_1:19;
E0: k + 0 <= k + 1 by XREAL_1:9;
then E1: ( len L2 = k & dom L2 = Seg k ) by C3, FINSEQ_1:21;
E3: L2 is_Finseq_for v by D1, E0, C3, ThSucc02;
m1 in dom L2 by E1, D2, D600, FINSEQ_1:3;
then E4: L2 . m1 = L1 . m1 by FUNCT_1:70;
k in dom L2 by E1, D601, FINSEQ_1:3;
then L2 . k = L1 . k by FUNCT_1:70;
then E6: ( 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 E1, B1, E3, D2, D600, E4;
k < len L1 by C3, NAT_1:13;
then consider N1, N2 being strict LTLnode of v such that
E7: ( N1 = L1 . k & N2 = L1 . (k + 1) & N2 is_succ_of N1 ) by D601, D1, DefFinseq;
E8: ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 ) by E7, ThSucc01;
( N1 = CastNode N1,v & N2 = CastNode N2,v ) by defCastNode01;
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 E8, D6, E7, E6, XBOOLE_1:1; :: 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;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
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, A2; :: thesis: verum