let v be LTL-formula; :: thesis: for N being strict LTLnode of 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 of v; :: thesis: 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 ; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum