:: deftheorem defines is_Finseq_for MODELC_3:def 19 :
for v being LTL-formula
for L being FinSequence holds
( L is_Finseq_for v iff for k being Nat st 1 <= k & k < len L holds
ex N, M being strict LTLnode over v st
( N = L . k & M = L . (k + 1) & M is_succ_of N ) );