let H, v be LTL-formula; for N being strict LTLnode of v st H in the LTLnew of N & ( H is atomic or H is negative ) holds
* N = * (SuccNode1 H,N)
let N be strict LTLnode of v; ( H in the LTLnew of N & ( H is atomic or H is negative ) implies * N = * (SuccNode1 H,N) )
set N1 = SuccNode1 H,N;
assume that
A1:
H in the LTLnew of N
and
A2:
( H is atomic or H is negative )
; * N = * (SuccNode1 H,N)
A3:
( not H is next & not H is Until )
by A2, MODELC_2:78;
set NX = the LTLnext of N;
set N1X = the LTLnext of (SuccNode1 H,N);
A4:
the LTLnext of (SuccNode1 H,N) = the LTLnext of N \/ (LTLNext H)
by A1, Def4;
set NN = the LTLnew of N;
set N1N = the LTLnew of (SuccNode1 H,N);
set NO = the LTLold of N;
set N1O = the LTLold of (SuccNode1 H,N);
A5:
the LTLold of (SuccNode1 H,N) = the LTLold of N \/ {H}
by A1, Def4;
A6:
not H is Release
by A2, MODELC_2:78;
A7:
( not H is conjunctive & not H is disjunctive )
by A2, MODELC_2:78;
then A8:
LTLNew1 H = {}
by A3, A6, Def1;
A9:
the LTLnew of (SuccNode1 H,N) = (the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N)
by A1, Def4;
A10:
for a being set st a in the LTLold of (SuccNode1 H,N) \/ the LTLnew of (SuccNode1 H,N) holds
a in the LTLold of N \/ the LTLnew of N
proof
let a be
set ;
( a in the LTLold of (SuccNode1 H,N) \/ the LTLnew of (SuccNode1 H,N) implies a in the LTLold of N \/ the LTLnew of N )
assume A11:
a in the
LTLold of
(SuccNode1 H,N) \/ the
LTLnew of
(SuccNode1 H,N)
;
a in the LTLold of N \/ the LTLnew of N
( not
a in the
LTLold of
(SuccNode1 H,N) or
a in the
LTLold of
N or
a in {H} )
by A5, XBOOLE_0:def 3;
then A12:
( not
a in the
LTLold of
(SuccNode1 H,N) or
a in the
LTLold of
N or
a in the
LTLnew of
N )
by A1, TARSKI:def 1;
(
a in the
LTLnew of
(SuccNode1 H,N) implies (
a in the
LTLnew of
N & not
a in {H} ) )
by A8, A9, XBOOLE_0:def 5;
hence
a in the
LTLold of
N \/ the
LTLnew of
N
by A11, A12, XBOOLE_0:def 3;
verum
end;
A13:
for a being set st a in the LTLold of N \/ the LTLnew of N holds
a in the LTLold of (SuccNode1 H,N) \/ the LTLnew of (SuccNode1 H,N)
proof
let a be
set ;
( a in the LTLold of N \/ the LTLnew of N implies a in the LTLold of (SuccNode1 H,N) \/ the LTLnew of (SuccNode1 H,N) )
assume A14:
a in the
LTLold of
N \/ the
LTLnew of
N
;
a in the LTLold of (SuccNode1 H,N) \/ the LTLnew of (SuccNode1 H,N)
( not
a in the
LTLnew of
N or ( not
a in {H} &
a in the
LTLnew of
N ) or (
a in {H} &
a in the
LTLnew of
N ) )
;
then A15:
( not
a in the
LTLnew of
N or
a in the
LTLnew of
N \ {H} or
a in the
LTLold of
N \/ {H} )
by XBOOLE_0:def 3, XBOOLE_0:def 5;
(
a in the
LTLold of
N implies
a in the
LTLold of
(SuccNode1 H,N) )
by A5, XBOOLE_0:def 3;
hence
a in the
LTLold of
(SuccNode1 H,N) \/ the
LTLnew of
(SuccNode1 H,N)
by A8, A5, A9, A14, A15, XBOOLE_0:def 3;
verum
end;
LTLNext H = {}
by A7, A3, A6, Def3;
hence
* N = * (SuccNode1 H,N)
by A4, A10, A13, TARSKI:2; verum