let v be 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 w |= * N & not N is elementary holds
( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )
let N be strict LTLnode over v; for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of (BOOL (Subformulae v)) st w |= * N & not N is elementary holds
( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )
let w be Element of Inf_seq AtomicFamily; for U being Choice_Function of (BOOL (Subformulae v)) st w |= * N & not N is elementary holds
( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )
let U be Choice_Function of (BOOL (Subformulae v)); ( w |= * N & not N is elementary implies ( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) ) )
assume
( w |= * N & not N is elementary )
; ( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )
then
chosen_succ (w,v,U,N) is_succ_of N
by Th59;
hence
( the LTLold of N c= the LTLold of (chosen_succ (w,v,U,N)) & the LTLnext of N c= the LTLnext of (chosen_succ (w,v,U,N)) )
by Th25; verum