let v be LTL-formula; :: thesis: 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; :: 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