let k be Nat; :: thesis: for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= k & k <= len L holds
len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1
let L be FinSequence; :: thesis: for v being LTL-formula st L is_Finseq_for v & 1 <= k & k <= len L holds
len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1
let v be LTL-formula; :: thesis: ( L is_Finseq_for v & 1 <= k & k <= len L implies len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 )
defpred S₁[ Nat] means for L being FinSequence
for j being Nat st len L <= $1 & L is_Finseq_for v & 1 <= j & j <= len L holds
len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
A3: for L being FinSequence
for k being Nat st len L = n + 1 & L is_Finseq_for v & 1 <= k & k <= len L holds
len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1

proof

let L be FinSequence; :: thesis: for k being Nat st len L = n + 1 & L is_Finseq_for v & 1 <= k & k <= len L holds
len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1
let k be Nat; :: thesis: ( len L = n + 1 & L is_Finseq_for v & 1 <= k & k <= len L implies len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 )
assume A4: len L = n + 1 ; :: thesis: ( not L is_Finseq_for v or not 1 <= k or not k <= len L or len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 )
( L is_Finseq_for v & 1 <= k & k <= len L implies len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 )

proof

set L1 = L | (Seg n);
assume that
A5: L is_Finseq_for v and
A6: 1 <= k and
A7: k <= len L ; :: thesis: len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1
reconsider L1 = L | (Seg n) as FinSequence by FINSEQ_1:15;
A8: n < len L by A4, NAT_1:13;
then A9: len L1 = n by FINSEQ_1:17;
A10: dom L1 = Seg n by A8, FINSEQ_1:17;
A11: for m being Nat st 1 <= m & m <= n holds
L1 . m = L . m by A10, FINSEQ_1:1, FUNCT_1:47;
A12: ( not n = 0 implies 0 < 0 + n ) ;

now :: thesis: len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1

per cases ( k <= n or ( k = n + 1 & n >= 1 ) or ( k = n + 1 & n = 0 ) ) by A4, A7, A12, NAT_1:8, NAT_1:19;

suppose A13: k <= n ; :: thesis: len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1

then 1 <= n by A6, XXREAL_0:2;
then A14: L1 . 1 = L . 1 by A11;
L1 . k = L . k by A6, A11, A13;
hence len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 by A2, A5, A6, A8, A9, A13, A14, Th26; :: thesis: verum

end;

suppose A15: ( k = n + 1 & n >= 1 ) ; :: thesis: len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1

then len (CastNode ((L . k),v)) <= (len (CastNode ((L . n),v))) - 1 by A5, A8, Th21, Th35;
then A16: (len (CastNode ((L . k),v))) + 1 <= ((len (CastNode ((L . n),v))) - 1) + 1 by XREAL_1:6;
( L1 . n = L . n & L1 . 1 = L . 1 ) by A11, A15;
then len (CastNode ((L . n),v)) <= ((len (CastNode ((L . 1),v))) - n) + 1 by A2, A5, A8, A9, A15, Th26;
then (len (CastNode ((L . k),v))) + 1 <= ((len (CastNode ((L . 1),v))) - n) + 1 by A16, XXREAL_0:2;
hence len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 by A15, XREAL_1:6; :: thesis: verum

end;

suppose ( k = n + 1 & n = 0 ) ; :: thesis: len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1

hence len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 ; :: thesis: verum

end;

end;

end;

hence len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 ; :: thesis: verum

end;

hence ( not L is_Finseq_for v or not 1 <= k or not k <= len L or len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 ) ; :: thesis: verum

end;

S₁[n + 1]

proof

let L be FinSequence; :: thesis: for j being Nat st len L <= n + 1 & L is_Finseq_for v & 1 <= j & j <= len L holds
len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1
let j be Nat; :: thesis: ( len L <= n + 1 & L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 )
assume A17: len L <= n + 1 ; :: thesis: ( not L is_Finseq_for v or not 1 <= j or not j <= len L or len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 )
( L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 )

proof

now :: thesis: ( L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 )

per cases ( len L <= n or len L = n + 1 ) by A17, NAT_1:8;

suppose len L <= n ; :: thesis: ( L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 )

hence ( L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 ) by A2; :: thesis: verum

end;

suppose len L = n + 1 ; :: thesis: ( L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 )

hence ( L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 ) by A3; :: thesis: verum

end;

end;

end;

hence ( L is_Finseq_for v & 1 <= j & j <= len L implies len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 ) ; :: thesis: verum

end;

hence ( not L is_Finseq_for v or not 1 <= j or not j <= len L or len (CastNode ((L . j),v)) <= ((len (CastNode ((L . 1),v))) - j) + 1 ) ; :: thesis: verum

end;

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

end;

A18: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A18, A1);
hence ( L is_Finseq_for v & 1 <= k & k <= len L implies len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1 ) ; :: thesis: verum