let v be LTL-formula; :: thesis: for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 holds
( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )
let N1, N2 be strict LTLnode over v; :: thesis: ( N2 is_succ_of N1 implies ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 ) )
assume A1: N2 is_succ_of N1 ; :: thesis: ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )
now :: thesis: ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )
per cases ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) by A1;
suppose N2 is_succ1_of N1 ; :: thesis: ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )
then consider H being LTL-formula such that
A2: ( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) ) ;
( the LTLold of N2 = the LTLold of N1 \/ {H} & the LTLnext of N2 = the LTLnext of N1 \/ (LTLNext H) ) by A2, Def4;
hence ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 ) by XBOOLE_1:7; :: thesis: verum
end;
suppose N2 is_succ2_of N1 ; :: thesis: ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 )
then consider H being LTL-formula such that
A3: H in the LTLnew of N1 and
( H is disjunctive or H is Until or H is Release ) and
A4: N2 = SuccNode2 (H,N1) ;
the LTLold of N2 = the LTLold of N1 \/ {H} by A3, A4, Def5;
hence ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 ) by A3, A4, Def5, XBOOLE_1:7; :: thesis: verum
end;
end;
end;
hence ( the LTLold of N1 c= the LTLold of N2 & the LTLnext of N1 c= the LTLnext of N2 ) ; :: thesis: verum