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
CastNode ((L . (k + 1)),v) is_succ_of CastNode ((L . k),v)
let L be FinSequence; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum