let H, v be LTL-formula; for N being strict LTLnode over v
for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is Release holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
let N be strict LTLnode over v; for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & H is Release holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
let w be Element of Inf_seq AtomicFamily; ( H in the LTLnew of N & H is Release 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 Release
; ( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (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 = {H}
by A2, Def3;
then A4:
the LTLnext of (SuccNode1 (H,N)) = the LTLnext of N \/ {H}
by A1, Def4;
set H2 = the_right_argument_of H;
set NN = the LTLnew of N;
set NO = the LTLold of N;
set SN2 = SuccNode2 (H,N);
set H1 = the_left_argument_of H;
set SN2N = the LTLnew of (SuccNode2 (H,N));
LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)}
by A2, Def2;
then A5:
the LTLnew of (SuccNode2 (H,N)) = ( the LTLnew of N \ {H}) \/ ({(the_left_argument_of H),(the_right_argument_of H)} \ the LTLold of N)
by A1, Def5;
set XNX = 'X' (CastLTL the LTLnext of N);
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));
A6:
the LTLold of (SuccNode1 (H,N)) = the LTLold of N \/ {H}
by A1, Def4;
LTLNew1 H = {(the_right_argument_of H)}
by A2, Def1;
then A7:
the LTLnew of (SuccNode1 (H,N)) = ( the LTLnew of N \ {H}) \/ ({(the_right_argument_of H)} \ the LTLold of N)
by A1, Def4;
A8:
for F being LTL-formula holds
( not F in * (SuccNode1 (H,N)) or F in * N or F = the_right_argument_of H or F = 'X' H )
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));
A15:
the LTLold of (SuccNode2 (H,N)) = the LTLold of N \/ {H}
by A1, Def5;
A16:
the LTLnext of (SuccNode2 (H,N)) = the LTLnext of N
by A1, Def5;
A17:
for F being LTL-formula holds
( not F in * (SuccNode2 (H,N)) or F in * N or F = the_left_argument_of H or F = the_right_argument_of H )
H = (the_left_argument_of H) 'R' (the_right_argument_of H)
by A2, MODELC_2:9;
then
( w |= H iff w |= ((the_left_argument_of H) '&' (the_right_argument_of H)) 'or' ((the_right_argument_of H) '&' ('X' H)) )
by MODELC_2:76;
then A19:
( w |= H iff ( w |= (the_left_argument_of H) '&' (the_right_argument_of H) or w |= (the_right_argument_of H) '&' ('X' H) ) )
by MODELC_2:66;
A20:
( not w |= * N or w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) )
A24:
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;
( F in * N implies ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) ) )
assume A25:
F in * N
;
( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )
now ( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )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 A25, Lm1;
suppose
F in 'X' (CastLTL the LTLnext of N)
;
( F in * (SuccNode1 (H,N)) & F in * (SuccNode2 (H,N)) )then consider G being
LTL-formula such that A27:
F = G
and A28:
ex
G1 being
LTL-formula st
(
G1 in CastLTL the
LTLnext of
N &
G = 'X' G1 )
;
consider G1 being
LTL-formula such that A29:
G1 in the
LTLnext of
N
and A30:
G = 'X' G1
by A28;
G1 in the
LTLnext of
(SuccNode1 (H,N))
by A4, A29, XBOOLE_0:def 3;
then A31:
F in 'X' (CastLTL the LTLnext of (SuccNode1 (H,N)))
by A27, A30;
F in 'X' (CastLTL the LTLnext of (SuccNode2 (H,N)))
by A16, A27, A29, A30;
hence
(
F in * (SuccNode1 (H,N)) &
F in * (SuccNode2 (H,N)) )
by A31, Lm1;
verum end; end; end;
hence
(
F in * (SuccNode1 (H,N)) &
F in * (SuccNode2 (H,N)) )
;
verum
end;
( ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) implies w |= * N )
hence
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) )
by A20; verum