let H, v be LTL-formula; :: thesis: 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; :: thesis: ( H in the LTLnew of N & ( H is atomic or H is negative ) implies * N = * (SuccNode1 H,N) )
set N1 = SuccNode1 H,N;
assume A1:
( H in the LTLnew of N & ( H is atomic or H is negative ) )
; :: thesis: * N = * (SuccNode1 H,N)
A3:
( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release )
by A1, MODELC_2:78;
then A4:
LTLNew1 H = {}
by Def203;
A5:
LTLNext H = {}
by A3, Def205;
set N1O = the LTLold of (SuccNode1 H,N);
set N1N = the LTLnew of (SuccNode1 H,N);
set N1X = the LTLnext of (SuccNode1 H,N);
set NO = the LTLold of N;
set NN = the LTLnew of N;
set NX = the LTLnext of N;
A6:
( the LTLold of (SuccNode1 H,N) = the LTLold of N \/ {H} & the LTLnew of (SuccNode1 H,N) = (the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of (SuccNode1 H,N) = the LTLnext of N \/ (LTLNext H) )
by A1, Def206;
the LTLold of (SuccNode1 H,N) \/ the LTLnew of (SuccNode1 H,N) = the LTLold of N \/ the LTLnew of N
proof
B1:
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 ;
:: thesis: ( 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 C1:
a in the
LTLold of
(SuccNode1 H,N) \/ the
LTLnew of
(SuccNode1 H,N)
;
:: thesis: 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 A6, XBOOLE_0:def 3;
then C2:
( 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 A6, A4, XBOOLE_0:def 5;
hence
a in the
LTLold of
N \/ the
LTLnew of
N
by C1, C2, XBOOLE_0:def 3;
:: thesis: verum
end;
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 ;
:: thesis: ( 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 C1:
a in the
LTLold of
N \/ the
LTLnew of
N
;
:: thesis: a in the LTLold of (SuccNode1 H,N) \/ the LTLnew of (SuccNode1 H,N)
C2:
(
a in the
LTLold of
N implies
a in the
LTLold of
(SuccNode1 H,N) )
by A6, XBOOLE_0:def 3;
( 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
( 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;
hence
a in the
LTLold of
(SuccNode1 H,N) \/ the
LTLnew of
(SuccNode1 H,N)
by A6, A4, C1, C2, XBOOLE_0:def 3;
:: thesis: verum
end;
hence
the
LTLold of
(SuccNode1 H,N) \/ the
LTLnew of
(SuccNode1 H,N) = the
LTLold of
N \/ the
LTLnew of
N
by B1, TARSKI:2;
:: thesis: verum
end;
hence
* N = * (SuccNode1 H,N)
by A6, A5; :: thesis: verum