let k be Nat; for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= k & k < len L holds
CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)
let L be FinSequence; for v being LTL-formula st L is_Finseq_for v & 1 <= k & k < len L holds
CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)
let v be LTL-formula; ( L is_Finseq_for v & 1 <= k & k < len L implies CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v) )
assume
( L is_Finseq_for v & 1 <= k & k < len L )
; CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)
then consider N, M being strict LTLnode over v such that
A1:
N = L . k
and
A2:
( M = L . (k + 1) & M is_succ_of N )
;
CastNode ((L . k),v) = N
by A1, Def16;
hence
CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)
by A2, Def16; verum