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
( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of 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
( 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 :: thesis: ( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N )

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 :: thesis: w |= * (chosen_succ (w,v,U,N))

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 :: thesis: w |= * (chosen_succ (w,v,U,N))

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; :: 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;
hence ( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N ) by A6; :: 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 :: thesis: ( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N )

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:31;
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 :: thesis: w |= G

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; :: 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; :: 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; :: 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;
hence ( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N ) by A19; :: 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 :: thesis: ( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N )

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;
hence ( w |= * (chosen_succ (w,v,U,N)) & chosen_succ (w,v,U,N) is_succ_of N ) by A1, A3, A13, A21, A22, 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