let H, v be LTL-formula; for N being strict LTLnode over 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 over 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 object 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
object ;
( 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 object 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
object ;
( 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