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 conjunctive or H is next ) holds
( w |= * N iff w |= * (SuccNode1 (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 conjunctive or H is next ) holds
( w |= * N iff w |= * (SuccNode1 (H,N)) )
let w be Element of Inf_seq AtomicFamily; :: thesis: ( H in the LTLnew of N & ( H is conjunctive or H is next ) implies ( w |= * N iff w |= * (SuccNode1 (H,N)) ) )
assume that
A1: H in the LTLnew of N and
A2: ( H is conjunctive or H is next ) ; :: thesis: ( w |= * N iff w |= * (SuccNode1 (H,N)) )
set NX = the LTLnext of N;
set NN = the LTLnew of N;
set NO = the LTLold of N;
set SN = SuccNode1 (H,N);
set SNO = the LTLold of (SuccNode1 (H,N));
set SNN = the LTLnew of (SuccNode1 (H,N));
set SNX = the LTLnext of (SuccNode1 (H,N));
set XSNX = 'X' (CastLTL the LTLnext of (SuccNode1 (H,N)));
set XNX = 'X' (CastLTL the LTLnext of N);
A3: H in * N by A1, Lm1;
A4: ( w |= * N implies w |= * (SuccNode1 (H,N)) )

proof

assume A5: w |= * N ; :: thesis: w |= * (SuccNode1 (H,N))
then A6: w |= H by A3;
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 A7: F in * (SuccNode1 (H,N)) ; :: thesis: w |= F

now :: thesis: w |= F

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 A7, Lm1;

suppose F in the LTLold of (SuccNode1 (H,N)) ; :: thesis: w |= F

then A8: F in the LTLold of N \/ {H} by A1, Def4;

now :: thesis: w |= F

per cases ( F in the LTLold of N or F in {H} ) by A8, XBOOLE_0:def 3;

suppose F in the LTLold of N ; :: thesis: w |= F

then F in * N by Lm1;
hence w |= F by A5; :: thesis: verum

end;

suppose F in {H} ; :: thesis: w |= F

then F in * N by A3, TARSKI:def 1;
hence w |= F by A5; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

suppose F in the LTLnew of (SuccNode1 (H,N)) ; :: thesis: w |= F

then A9: F in ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) by A1, Def4;

now :: thesis: w |= F

per cases ( F in the LTLnew of N or F in LTLNew1 H ) by A9, Lm2;

suppose F in the LTLnew of N ; :: thesis: w |= F

then F in ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N)) by Lm1;
hence w |= F by A5; :: thesis: verum

end;

suppose A10: F in LTLNew1 H ; :: thesis: w |= F

now :: thesis: w |= F

per cases ( H is conjunctive or H is next ) by A2;

suppose A11: H is conjunctive ; :: thesis: w |= F

then F in {(the_left_argument_of H),(the_right_argument_of H)} by A10, Def1;
then A12: ( F = the_left_argument_of H or F = the_right_argument_of H ) by TARSKI:def 2;
H = (the_left_argument_of H) '&' (the_right_argument_of H) by A11, MODELC_2:6;
hence w |= F by A6, A12, MODELC_2:65; :: thesis: verum

end;

suppose H is next ; :: thesis: w |= F

hence w |= F by A10, Def1; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

suppose A13: F in 'X' (CastLTL the LTLnext of (SuccNode1 (H,N))) ; :: thesis: w |= F

set SN1 = CastLTL the LTLnext of (SuccNode1 (H,N));
consider G being LTL-formula such that
A14: F = G and
A15: ex G1 being LTL-formula st
( G1 in CastLTL the LTLnext of (SuccNode1 (H,N)) & G = 'X' G1 ) by A13;
consider G1 being LTL-formula such that
A16: G1 in CastLTL the LTLnext of (SuccNode1 (H,N)) and
A17: G = 'X' G1 by A15;
A18: CastLTL the LTLnext of (SuccNode1 (H,N)) = the LTLnext of N \/ (LTLNext H) by A1, Def4;

now :: thesis: w |= F

per cases ( G1 in the LTLnext of N or G1 in LTLNext H ) by A18, A16, XBOOLE_0:def 3;

suppose G1 in the LTLnext of N ; :: thesis: w |= F

then F in 'X' (CastLTL the LTLnext of N) by A14, A17;
then F in ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N)) by Lm1;
hence w |= F by A5; :: thesis: verum

end;

suppose A19: G1 in LTLNext H ; :: thesis: w |= F

now :: thesis: w |= F

per cases ( H is next or H is conjunctive ) by A2;

suppose A20: H is next ; :: thesis: w |= F

then G1 in {(the_argument_of H)} by A19, Def3;
then G1 = the_argument_of H by TARSKI:def 1;
hence w |= F by A6, A14, A17, A20, MODELC_2:5; :: thesis: verum

end;

suppose H is conjunctive ; :: thesis: w |= F

hence w |= F by A19, Def3; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

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

end;

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

proof

assume A21: w |= * (SuccNode1 (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 A22: F in * N ; :: thesis: w |= F

now :: thesis: w |= F

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 A22, Lm1;

suppose F in the LTLold of N ; :: thesis: w |= F

then F in the LTLold of N \/ {H} by XBOOLE_0:def 3;
then F in the LTLold of (SuccNode1 (H,N)) by A1, Def4;
then F in * (SuccNode1 (H,N)) by Lm1;
hence w |= F by A21; :: thesis: verum

end;

suppose A23: F in the LTLnew of N ; :: thesis: w |= F

now :: thesis: w |= F

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

suppose F = H ; :: thesis: w |= F

then F in {H} by TARSKI:def 1;
then F in the LTLold of N \/ {H} by XBOOLE_0:def 3;
then F in the LTLold of (SuccNode1 (H,N)) by A1, Def4;
then F in * (SuccNode1 (H,N)) by Lm1;
hence w |= F by A21; :: thesis: verum

end;

suppose not F = H ; :: thesis: w |= F

then not F in {H} by TARSKI:def 1;
then F in the LTLnew of N \ {H} by A23, XBOOLE_0:def 5;
then F in ( the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) by XBOOLE_0:def 3;
then F in the LTLnew of (SuccNode1 (H,N)) by A1, Def4;
then F in * (SuccNode1 (H,N)) by Lm1;
hence w |= F by A21; :: thesis: verum

end;

end;

end;

hence w |= F ; :: thesis: verum

end;

suppose A24: F in 'X' (CastLTL the LTLnext of N) ; :: thesis: w |= F

set SN11 = the LTLnext of N \/ (LTLNext H);
the LTLnext of (SuccNode1 (H,N)) = the LTLnext of N \/ (LTLNext H) by A1, Def4;
then reconsider SN11 = the LTLnext of N \/ (LTLNext H) as Subset of (Subformulae v) ;
set SN1 = CastLTL SN11;
set N1 = CastLTL the LTLnext of N;
consider G being LTL-formula such that
A25: F = G and
A26: ex G1 being LTL-formula st
( G1 in CastLTL the LTLnext of N & G = 'X' G1 ) by A24;
consider G1 being LTL-formula such that
A27: G1 in CastLTL the LTLnext of N and
A28: G = 'X' G1 by A26;
G1 in SN11 by A27, XBOOLE_0:def 3;
then F in 'X' (CastLTL SN11) by A25, A28;
then F in 'X' (CastLTL the LTLnext of (SuccNode1 (H,N))) by A1, Def4;
then F in * (SuccNode1 (H,N)) by Lm1;
hence w |= F by A21; :: 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)) ) by A4; :: thesis: verum