theorem
for
v being
LTL-formula for
N being
strict LTLnode over
v for
w being
Element of
Inf_seq AtomicFamily for
U being
Choice_Function of
(BOOL (Subformulae v)) st not
N is
elementary &
chosen_formula (
U,
N) is
Until &
w |= the_right_argument_of (chosen_formula (U,N)) holds
( (
the_right_argument_of (chosen_formula (U,N)) in the
LTLnew of
(chosen_succ (w,v,U,N)) or
the_right_argument_of (chosen_formula (U,N)) in the
LTLold of
N ) &
chosen_formula (
U,
N)
in the
LTLold of
(chosen_succ (w,v,U,N)) )