let H, v be LTL-formula; :: thesis: for N being strict LTLnode of 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 of 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

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

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

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

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

proof

let F be LTL-formula; :: thesis: ( F in * (SuccNode1 H,N) implies w |= F )
assume F in * (SuccNode1 H,N) ; :: thesis: w |= F
then ( F in * N or F = the_left_argument_of H ) by A7;
hence w |= F by A16, A17, MODELC_2:def 68; :: thesis: verum

end;

hence ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) by MODELC_2:def 68; :: 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

proof

let F be LTL-formula; :: thesis: ( F in * (SuccNode2 H,N) implies w |= F )
assume F in * (SuccNode2 H,N) ; :: thesis: w |= F
then ( F in * N or F = the_right_argument_of H ) by A12;
hence w |= F by A16, A18, MODELC_2:def 68; :: thesis: verum

end;

hence ( w |= * (SuccNode1 H,N) or w |= * (SuccNode2 H,N) ) by MODELC_2:def 68; :: 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

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

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

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, MODELC_2:def 68; :: thesis: verum

end;

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

hence w |= F by A25, MODELC_2:def 68; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

hence w |= * N by MODELC_2:def 68; :: thesis: verum

end;

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