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
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of 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
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of 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
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )
let U be Choice_Function of BOOL (Subformulae v); :: thesis: ( w |= * N & not N is elementary implies ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) )
assume that
A1: w |= * N and
A2: not N is elementary ; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )
set H = chosen_formula U,N;
set SN = chosen_succ w,v,U,N;
set H2 = the_right_argument_of (chosen_formula U,N);
A3: chosen_formula U,N in the LTLnew of N by A2, Th58;

now

per cases ( ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) or ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) or ( not ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) & not ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) ) ) ;

suppose A4: ( ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) or ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) ) ; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

then A5: chosen_succ w,v,U,N = SuccNode1 (chosen_formula U,N),N by Def35;
A6: w |= * (chosen_succ w,v,U,N)

proof

now

per cases ( ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) or ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) ) by A4;

suppose ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) ; :: thesis: w |= * (chosen_succ w,v,U,N)

hence w |= * (chosen_succ w,v,U,N) by Def35; :: thesis: verum

end;

suppose A7: ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) ; :: thesis: w |= * (chosen_succ w,v,U,N)

set N2 = SuccNode2 (chosen_formula U,N),N;
A8: ( w |= * (chosen_succ w,v,U,N) or w |= * (SuccNode2 (chosen_formula U,N),N) ) by A1, A3, A5, A7, Lm19;

now

the LTLold of (SuccNode2 (chosen_formula U,N),N) = the LTLold of N \/ {(chosen_formula U,N)} by A3, Def5;
then A9: ( the_right_argument_of (chosen_formula U,N) in the LTLold of N implies the_right_argument_of (chosen_formula U,N) in the LTLold of (SuccNode2 (chosen_formula U,N),N) ) by XBOOLE_0:def 3;
LTLNew2 (chosen_formula U,N) = {(the_right_argument_of (chosen_formula U,N))} by A7, Def2;
then the_right_argument_of (chosen_formula U,N) in LTLNew2 (chosen_formula U,N) by TARSKI:def 1;
then A10: ( not the_right_argument_of (chosen_formula U,N) in the LTLold of N implies the_right_argument_of (chosen_formula U,N) in (LTLNew2 (chosen_formula U,N)) \ the LTLold of N ) by XBOOLE_0:def 5;
assume A11: not w |= * (chosen_succ w,v,U,N) ; :: thesis: contradiction
the LTLnew of (SuccNode2 (chosen_formula U,N),N) = (the LTLnew of N \ {(chosen_formula U,N)}) \/ ((LTLNew2 (chosen_formula U,N)) \ the LTLold of N) by A3, Def5;
then ( not the_right_argument_of (chosen_formula U,N) in the LTLold of N implies the_right_argument_of (chosen_formula U,N) in the LTLnew of (SuccNode2 (chosen_formula U,N),N) ) by A10, XBOOLE_0:def 3;
then the_right_argument_of (chosen_formula U,N) in * (SuccNode2 (chosen_formula U,N),N) by A9, Lm1;
hence contradiction by A7, A8, A11, MODELC_2:def 68; :: thesis: verum

end;

hence w |= * (chosen_succ w,v,U,N) ; :: thesis: verum

end;

end;

end;

hence w |= * (chosen_succ w,v,U,N) ; :: thesis: verum

end;

chosen_succ w,v,U,N is_succ1_of N by A3, A5, Def7;
hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) by A6, Def9; :: thesis: verum

end;

suppose A12: ( not ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) & not ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) ) ; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

set N1 = SuccNode1 (chosen_formula U,N),N;
A13: chosen_succ w,v,U,N = SuccNode2 (chosen_formula U,N),N by A12, Def35;
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

proof

now

per cases ( ( chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) ) or not w |= * (SuccNode1 (chosen_formula U,N),N) ) by A12;

suppose A14: ( chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) ) ; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

set NN = the LTLnew of N;
set NO = the LTLold of N;
set SNN = the LTLnew of (chosen_succ w,v,U,N);
LTLNew2 (chosen_formula U,N) = {(the_right_argument_of (chosen_formula U,N))} by A14, Def2;
then A15: the LTLnew of (chosen_succ w,v,U,N) = (the LTLnew of N \ {(chosen_formula U,N)}) \/ ({(the_right_argument_of (chosen_formula U,N))} \ the LTLold of N) by A3, A13, Def5;
the LTLnew of N \ {(chosen_formula U,N)} c= the LTLnew of N by XBOOLE_1:36;
then A16: the LTLnew of (chosen_succ w,v,U,N) c= the LTLnew of N \/ {(the_right_argument_of (chosen_formula U,N))} by A15, XBOOLE_1:13;
set NX = the LTLnext of N;
set SNX = the LTLnext of (chosen_succ w,v,U,N);
set SNO = the LTLold of (chosen_succ w,v,U,N);
( the LTLold of (chosen_succ w,v,U,N) = the LTLold of N \/ {(chosen_formula U,N)} & {(chosen_formula U,N)} c= the LTLnew of N ) by A3, A13, Def5, ZFMISC_1:37;
then A17: the LTLold of (chosen_succ w,v,U,N) c= the LTLold of N \/ the LTLnew of N by XBOOLE_1:9;
A18: the LTLnext of (chosen_succ w,v,U,N) = the LTLnext of N by A3, A13, Def5;
A19: for G being LTL-formula st G in * (chosen_succ w,v,U,N) holds
w |= G

proof

let G be LTL-formula; :: thesis: ( G in * (chosen_succ w,v,U,N) implies w |= G )
assume A20: G in * (chosen_succ w,v,U,N) ; :: thesis: w |= G

now

per cases ( G in the LTLold of (chosen_succ w,v,U,N) or G in the LTLnew of (chosen_succ w,v,U,N) or G in 'X' (CastLTL the LTLnext of (chosen_succ w,v,U,N)) ) by A20, Lm1;

suppose G in the LTLold of (chosen_succ w,v,U,N) ; :: thesis: w |= G

then G in * N by A17, XBOOLE_0:def 3;
hence w |= G by A1, MODELC_2:def 68; :: thesis: verum

end;

suppose G in the LTLnew of (chosen_succ w,v,U,N) ; :: thesis: w |= G

then ( G in the LTLnew of N or G in {(the_right_argument_of (chosen_formula U,N))} ) by A16, XBOOLE_0:def 3;
then ( G in * N or G = the_right_argument_of (chosen_formula U,N) ) by Lm1, TARSKI:def 1;
hence w |= G by A1, A14, MODELC_2:def 68; :: thesis: verum

end;

suppose G in 'X' (CastLTL the LTLnext of (chosen_succ w,v,U,N)) ; :: thesis: w |= G

then G in * N by A18, Lm1;
hence w |= G by A1, MODELC_2:def 68; :: thesis: verum

end;

end;

end;

hence w |= G ; :: thesis: verum

end;

chosen_succ w,v,U,N is_succ2_of N by A3, A13, A14, Def8;
hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) by A19, Def9, MODELC_2:def 68; :: thesis: verum

end;

suppose A21: not w |= * (SuccNode1 (chosen_formula U,N),N) ; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

now

per cases ( chosen_formula U,N is atomic or chosen_formula U,N is negative or chosen_formula U,N is conjunctive or chosen_formula U,N is next or chosen_formula U,N is disjunctive or chosen_formula U,N is Until or chosen_formula U,N is Release ) by MODELC_2:2;

suppose ( chosen_formula U,N is atomic or chosen_formula U,N is negative or chosen_formula U,N is conjunctive or chosen_formula U,N is next ) ; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) by A1, A3, A21, Lm16, Lm17; :: thesis: verum

end;

suppose A22: ( chosen_formula U,N is disjunctive or chosen_formula U,N is Until or chosen_formula U,N is Release ) ; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )

then chosen_succ w,v,U,N is_succ2_of N by A3, A13, Def8;
hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) by A1, A3, A13, A21, A22, Def9, Lm18, Lm19, Lm20; :: thesis: verum

end;

end;

end;

hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) ; :: thesis: verum

end;

end;

end;

hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) ; :: thesis: verum

end;

hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) ; :: thesis: verum

end;

end;

end;

hence ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) ; :: thesis: verum