let F, v be LTL-formula; :: thesis: for N1, N2 being strict LTLnode over v st N2 is_succ_of N1 & F in the LTLnew of N1 & not F in the LTLnew of N2 holds
N2 is_succ_of N1,F
let N1, N2 be strict LTLnode over v; :: thesis: ( N2 is_succ_of N1 & F in the LTLnew of N1 & not F in the LTLnew of N2 implies N2 is_succ_of N1,F )
assume that
A1: N2 is_succ_of N1 and
A2: F in the LTLnew of N1 and
A3: not F in the LTLnew of N2 ; :: thesis: N2 is_succ_of N1,F

now :: thesis: N2 is_succ_of N1,F

per cases ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) by A1;

suppose N2 is_succ1_of N1 ; :: thesis: N2 is_succ_of N1,F

then consider H being LTL-formula such that
A4: ( H in the LTLnew of N1 & N2 = SuccNode1 (H,N1) ) ;
the LTLnew of N2 = ( the LTLnew of N1 \ {H}) \/ ((LTLNew1 H) \ the LTLold of N1) by A4, Def4;
then not F in the LTLnew of N1 \ {H} by A3, XBOOLE_0:def 3;
then ( not F in the LTLnew of N1 or F in {H} ) by XBOOLE_0:def 5;
then F = H by A2, TARSKI:def 1;
hence N2 is_succ_of N1,F by A4; :: thesis: verum

end;

suppose N2 is_succ2_of N1 ; :: thesis: N2 is_succ_of N1,F

then consider H being LTL-formula such that
A5: H in the LTLnew of N1 and
A6: ( H is disjunctive or H is Until or H is Release ) and
A7: N2 = SuccNode2 (H,N1) ;
the LTLnew of N2 = ( the LTLnew of N1 \ {H}) \/ ((LTLNew2 H) \ the LTLold of N1) by A5, A7, Def5;
then not F in the LTLnew of N1 \ {H} by A3, XBOOLE_0:def 3;
then ( not F in the LTLnew of N1 or F in {H} ) by XBOOLE_0:def 5;
then F = H by A2, TARSKI:def 1;
hence N2 is_succ_of N1,F by A5, A6, A7; :: thesis: verum

end;

end;

end;

hence N2 is_succ_of N1,F ; :: thesis: verum