let H, v be LTL-formula; :: thesis: for N being strict LTLnode over v
for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is disjunctive holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
let N be strict LTLnode over v; :: thesis: for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is disjunctive holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
let w be Element of Inf_seq AtomicFamily; :: thesis: ( H in the LTLnew of N & H is disjunctive implies ( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ) )
assume that
A1: H in the LTLnew of N and
A2: H is disjunctive ; :: thesis: ( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
set NN = the LTLnew of N;
set NO = the LTLold of N;
set SN2 = SuccNode2 (H,N);
set NX = the LTLnext of N;
set SN1 = SuccNode1 (H,N);
A3: H in * N by A1, Lm1;
set SN1X = the LTLnext of (SuccNode1 (H,N));
LTLNext H = {} by A2, Def3;
then A4: the LTLnext of (SuccNode1 (H,N)) = the LTLnext of N \/ {} by A1, Def4
.= the LTLnext of N ;
set H1 = the_left_argument_of H;
set XSN1X = 'X' (CastLTL the LTLnext of (SuccNode1 (H,N)));
set SN1N = the LTLnew of (SuccNode1 (H,N));
set SN1O = the LTLold of (SuccNode1 (H,N));
A5: the LTLold of (SuccNode1 (H,N)) = the LTLold of N \/ {H} by A1, Def4;
LTLNew1 H = {(the_left_argument_of H)} by A2, Def1;
then A6: the LTLnew of (SuccNode1 (H,N)) = ( the LTLnew of N \ {H}) \/ ({(the_left_argument_of H)} \ the LTLold of N) by A1, Def4;
A7: for F being LTL-formula holds
( not F in * (SuccNode1 (H,N)) or F in * N or F = the_left_argument_of H )

proof

let F be LTL-formula; :: thesis: ( not F in * (SuccNode1 (H,N)) or F in * N or F = the_left_argument_of H )
assume A8: F in * (SuccNode1 (H,N)) ; :: thesis: ( F in * N or F = the_left_argument_of H )

now :: thesis: ( F in * N or F = the_left_argument_of H )

per cases ( F in the LTLold of (SuccNode1 (H,N)) or F in the LTLnew of (SuccNode1 (H,N)) or F in 'X' (CastLTL the LTLnext of (SuccNode1 (H,N))) ) by A8, Lm1;

suppose F in the LTLold of (SuccNode1 (H,N)) ; :: thesis: ( F in * N or F = the_left_argument_of H )

then ( F in the LTLold of N or F in {H} ) by A5, XBOOLE_0:def 3;
hence ( F in * N or F = the_left_argument_of H ) by A3, Lm1, TARSKI:def 1; :: thesis: verum

end;

suppose F in the LTLnew of (SuccNode1 (H,N)) ; :: thesis: ( F in * N or F = the_left_argument_of H )

then ( F in the LTLnew of N \ {H} or F in {(the_left_argument_of H)} \ the LTLold of N ) by A6, XBOOLE_0:def 3;
then ( F in the LTLnew of N or F in {(the_left_argument_of H)} ) by XBOOLE_0:def 5;
hence ( F in * N or F = the_left_argument_of H ) by Lm1, TARSKI:def 1; :: thesis: verum

end;

suppose F in 'X' (CastLTL the LTLnext of (SuccNode1 (H,N))) ; :: thesis: ( F in * N or F = the_left_argument_of H )

hence ( F in * N or F = the_left_argument_of H ) by A4, Lm1; :: thesis: verum

end;

end;

end;

hence ( F in * N or F = the_left_argument_of H ) ; :: thesis: verum

end;

set XNX = 'X' (CastLTL the LTLnext of N);
set SN2X = the LTLnext of (SuccNode2 (H,N));
set XSN2X = 'X' (CastLTL the LTLnext of (SuccNode2 (H,N)));
set SN2O = the LTLold of (SuccNode2 (H,N));
A9: the LTLold of (SuccNode2 (H,N)) = the LTLold of N \/ {H} by A1, Def5;
set H2 = the_right_argument_of H;
set SN2N = the LTLnew of (SuccNode2 (H,N));
LTLNew2 H = {(the_right_argument_of H)} by A2, Def2;
then A10: the LTLnew of (SuccNode2 (H,N)) = ( the LTLnew of N \ {H}) \/ ({(the_right_argument_of H)} \ the LTLold of N) by A1, Def5;
A11: the LTLnext of (SuccNode2 (H,N)) = the LTLnext of N by A1, Def5;
A12: for F being LTL-formula holds
( not F in * (SuccNode2 (H,N)) or F in * N or F = the_right_argument_of H )

proof

let F be LTL-formula; :: thesis: ( not F in * (SuccNode2 (H,N)) or F in * N or F = the_right_argument_of H )
assume A13: F in * (SuccNode2 (H,N)) ; :: thesis: ( F in * N or F = the_right_argument_of H )

now :: thesis: ( F in * N or F = the_right_argument_of H )

per cases ( F in the LTLold of (SuccNode2 (H,N)) or F in the LTLnew of (SuccNode2 (H,N)) or F in 'X' (CastLTL the LTLnext of (SuccNode2 (H,N))) ) by A13, Lm1;

suppose F in the LTLold of (SuccNode2 (H,N)) ; :: thesis: ( F in * N or F = the_right_argument_of H )

then ( F in the LTLold of N or F in {H} ) by A9, XBOOLE_0:def 3;
hence ( F in * N or F = the_right_argument_of H ) by A3, Lm1, TARSKI:def 1; :: thesis: verum

end;

suppose F in the LTLnew of (SuccNode2 (H,N)) ; :: thesis: ( F in * N or F = the_right_argument_of H )

then ( F in the LTLnew of N \ {H} or F in {(the_right_argument_of H)} \ the LTLold of N ) by A10, XBOOLE_0:def 3;
then ( F in the LTLnew of N or F in {(the_right_argument_of H)} ) by XBOOLE_0:def 5;
hence ( F in * N or F = the_right_argument_of H ) by Lm1, TARSKI:def 1; :: thesis: verum

end;

suppose F in 'X' (CastLTL the LTLnext of (SuccNode2 (H,N))) ; :: thesis: ( F in * N or F = the_right_argument_of H )

hence ( F in * N or F = the_right_argument_of H ) by A11, Lm1; :: thesis: verum

end;

end;

end;

hence ( F in * N or F = the_right_argument_of H ) ; :: thesis: verum

end;

H = (the_left_argument_of H) 'or' (the_right_argument_of H) by A2, MODELC_2:7;
then A14: ( w |= H iff ( w |= the_left_argument_of H or w |= the_right_argument_of H ) ) by MODELC_2:66;
A15: ( not w |= * N or w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) )

proof

assume A16: w |= * N ; :: thesis: ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) )

now :: thesis: ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) )

per cases ( w |= the_left_argument_of H or w |= the_right_argument_of H ) by A3, A14, A16;

suppose A17: w |= the_left_argument_of H ; :: thesis: ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) )

for F being LTL-formula st F in * (SuccNode1 (H,N)) holds
w |= F by A7, A16, A17;
hence ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis: verum

end;

suppose A18: w |= the_right_argument_of H ; :: thesis: ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) )

for F being LTL-formula st F in * (SuccNode2 (H,N)) holds
w |= F by A12, A16, A18;
hence ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis: verum

end;

end;

end;

hence ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis: verum

end;

A19: for F being LTL-formula st F in * N holds
( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

proof

let F be LTL-formula; :: thesis: ( F in * N implies ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) )
assume A20: F in * N ; :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

now :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

per cases ( F in the LTLold of N or F in the LTLnew of N or F in 'X' (CastLTL the LTLnext of N) ) by A20, Lm1;

suppose F in the LTLold of N ; :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

then ( F in the LTLold of (SuccNode1 (H,N)) & F in the LTLold of (SuccNode2 (H,N)) ) by A5, A9, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by Lm1; :: thesis: verum

end;

suppose A21: F in the LTLnew of N ; :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

now :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

per cases ( F = H or not F = H ) ;

suppose F = H ; :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

then F in {H} by TARSKI:def 1;
then ( F in the LTLold of (SuccNode1 (H,N)) & F in the LTLold of (SuccNode2 (H,N)) ) by A5, A9, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by Lm1; :: thesis: verum

end;

suppose not F = H ; :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

then not F in {H} by TARSKI:def 1;
then F in the LTLnew of N \ {H} by A21, XBOOLE_0:def 5;
then ( F in the LTLnew of (SuccNode1 (H,N)) & F in the LTLnew of (SuccNode2 (H,N)) ) by A6, A10, XBOOLE_0:def 3;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by Lm1; :: thesis: verum

end;

end;

end;

hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) ; :: thesis: verum

end;

suppose A22: F in 'X' (CastLTL the LTLnext of N) ; :: thesis: ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )

then F in 'X' (CastLTL the LTLnext of (SuccNode2 (H,N))) by A1, Def5;
hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) by A4, A22, Lm1; :: thesis: verum

end;

end;

end;

hence ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) ; :: thesis: verum

end;

( ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) implies w |= * N )

proof

assume A23: ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ; :: thesis: w |= * N
for F being LTL-formula st F in * N holds
w |= F

proof

let F be LTL-formula; :: thesis: ( F in * N implies w |= F )
assume A24: F in * N ; :: thesis: w |= F
then A25: F in * (SuccNode2 (H,N)) by A19;
A26: F in * (SuccNode1 (H,N)) by A19, A24;

now :: thesis: w |= F

per cases ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) by A23;

suppose w |= * (SuccNode1 (H,N)) ; :: thesis: w |= F

hence w |= F by A26; :: thesis: verum

end;

suppose w |= * (SuccNode2 (H,N)) ; :: thesis: w |= F

hence w |= F by A25; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

hence w |= * N ; :: thesis: verum

end;

hence ( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ) by A15; :: thesis: verum