let v be LTL-formula; :: thesis: for N being strict LTLnode of v
for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of BOOL (Subformulae v) st w |= * N & not N is elementary holds
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )
let N be strict LTLnode of v; :: thesis: for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of BOOL (Subformulae v) st w |= * N & not N is elementary holds
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )
let w be Element of Inf_seq AtomicFamily ; :: thesis: for U being Choice_Function of BOOL (Subformulae v) st w |= * N & not N is elementary holds
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )
let U be Choice_Function of BOOL (Subformulae v); :: thesis: ( w |= * N & not N is elementary implies ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N ) )
assume A1:
( w |= * N & not N is elementary )
; :: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )
set SN = chosen_succ w,v,U,N;
set H = chosen_formula U,N;
set H2 = the_right_argument_of (chosen_formula U,N);
A2:
chosen_formula U,N in the LTLnew of N
by A1, Thchoice;
now per cases
( ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) or ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) or ( not ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) & not ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) ) )
;
suppose A3:
( ( not
chosen_formula U,
N is
Until &
w |= * (SuccNode1 (chosen_formula U,N),N) ) or (
chosen_formula U,
N is
Until &
w |/= the_right_argument_of (chosen_formula U,N) ) )
;
:: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )then B1:
chosen_succ w,
v,
U,
N = SuccNode1 (chosen_formula U,N),
N
by Defchosensucc;
then Bp1:
chosen_succ w,
v,
U,
N is_succ1_of N
by A2, Def208;
w |= * (chosen_succ w,v,U,N)
proof
now per cases
( ( not chosen_formula U,N is Until & w |= * (SuccNode1 (chosen_formula U,N),N) ) or ( chosen_formula U,N is Until & w |/= the_right_argument_of (chosen_formula U,N) ) )
by A3;
suppose C1:
(
chosen_formula U,
N is
Until &
w |/= the_right_argument_of (chosen_formula U,N) )
;
:: thesis: w |= * (chosen_succ w,v,U,N)set N2 =
SuccNode2 (chosen_formula U,N),
N;
D1:
(
w |= * (chosen_succ w,v,U,N) or
w |= * (SuccNode2 (chosen_formula U,N),N) )
by A1, A2, B1, C1, Lem204;
now assume E1:
not
w |= * (chosen_succ w,v,U,N)
;
:: thesis: contradictionE2:
( the
LTLold of
(SuccNode2 (chosen_formula U,N),N) = the
LTLold of
N \/ {(chosen_formula U,N)} & the
LTLnew of
(SuccNode2 (chosen_formula U,N),N) = (the LTLnew of N \ {(chosen_formula U,N)}) \/ ((LTLNew2 (chosen_formula U,N)) \ the LTLold of N) )
by A2, C1, Def207;
LTLNew2 (chosen_formula U,N) = {(the_right_argument_of (chosen_formula U,N))}
by C1, Def204;
then
the_right_argument_of (chosen_formula U,N) in LTLNew2 (chosen_formula U,N)
by TARSKI:def 1;
then
( not
the_right_argument_of (chosen_formula U,N) in the
LTLold of
N implies
the_right_argument_of (chosen_formula U,N) in (LTLNew2 (chosen_formula U,N)) \ the
LTLold of
N )
by XBOOLE_0:def 5;
then E3:
( not
the_right_argument_of (chosen_formula U,N) in the
LTLold of
N implies
the_right_argument_of (chosen_formula U,N) in the
LTLnew of
(SuccNode2 (chosen_formula U,N),N) )
by E2, XBOOLE_0:def 3;
(
the_right_argument_of (chosen_formula U,N) in the
LTLold of
N implies
the_right_argument_of (chosen_formula U,N) in the
LTLold of
(SuccNode2 (chosen_formula U,N),N) )
by E2, XBOOLE_0:def 3;
then
the_right_argument_of (chosen_formula U,N) in * (SuccNode2 (chosen_formula U,N),N)
by LemSUM01, E3;
hence
contradiction
by E1, D1, C1, MODELC_2:def 66;
:: thesis: verum end; hence
w |= * (chosen_succ w,v,U,N)
;
:: thesis: verum end;
hence
w |= * (chosen_succ w,v,U,N)
;
:: thesis: verum
end; hence
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
by Bp1, Def210;
:: thesis: verum end; suppose A4:
( not ( not
chosen_formula U,
N is
Until &
w |= * (SuccNode1 (chosen_formula U,N),N) ) & not (
chosen_formula U,
N is
Until &
w |/= the_right_argument_of (chosen_formula U,N) ) )
;
:: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )then B1:
chosen_succ w,
v,
U,
N = SuccNode2 (chosen_formula U,N),
N
by Defchosensucc;
set N1 =
SuccNode1 (chosen_formula U,N),
N;
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
proof
now per cases
( ( chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) ) or not w |= * (SuccNode1 (chosen_formula U,N),N) )
by A4;
suppose B3:
(
chosen_formula U,
N is
Until &
w |= the_right_argument_of (chosen_formula U,N) )
;
:: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )then Cp1:
chosen_succ w,
v,
U,
N is_succ2_of N
by A2, B1, Def209;
C1:
LTLNew2 (chosen_formula U,N) = {(the_right_argument_of (chosen_formula U,N))}
by B3, Def204;
set SNO = the
LTLold of
(chosen_succ w,v,U,N);
set SNN = the
LTLnew of
(chosen_succ w,v,U,N);
set SNX = the
LTLnext of
(chosen_succ w,v,U,N);
set NO = the
LTLold of
N;
set NN = the
LTLnew of
N;
set NX = the
LTLnext of
N;
C2:
( the
LTLold of
(chosen_succ w,v,U,N) = the
LTLold of
N \/ {(chosen_formula U,N)} & the
LTLnew of
(chosen_succ w,v,U,N) = (the LTLnew of N \ {(chosen_formula U,N)}) \/ ({(the_right_argument_of (chosen_formula U,N))} \ the LTLold of N) & the
LTLnext of
(chosen_succ w,v,U,N) = the
LTLnext of
N )
by A2, B1, B3, Def207, C1;
{(chosen_formula U,N)} c= the
LTLnew of
N
by A2, ZFMISC_1:37;
then C4:
the
LTLold of
(chosen_succ w,v,U,N) c= the
LTLold of
N \/ the
LTLnew of
N
by C2, XBOOLE_1:9;
( the
LTLnew of
N \ {(chosen_formula U,N)} c= the
LTLnew of
N &
{(the_right_argument_of (chosen_formula U,N))} \ the
LTLold of
N c= {(the_right_argument_of (chosen_formula U,N))} )
by XBOOLE_1:36;
then C5:
the
LTLnew of
(chosen_succ w,v,U,N) c= the
LTLnew of
N \/ {(the_right_argument_of (chosen_formula U,N))}
by C2, XBOOLE_1:13;
for
G being
LTL-formula st
G in * (chosen_succ w,v,U,N) holds
w |= G
proof
let G be
LTL-formula;
:: thesis: ( G in * (chosen_succ w,v,U,N) implies w |= G )
assume D1:
G in * (chosen_succ w,v,U,N)
;
:: thesis: w |= G
now per cases
( G in the LTLold of (chosen_succ w,v,U,N) or G in the LTLnew of (chosen_succ w,v,U,N) or G in 'X' (CastLTL the LTLnext of (chosen_succ w,v,U,N)) )
by D1, LemSUM01;
end;
hence
w |= G
;
:: thesis: verum
end; hence
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
by Cp1, Def210, MODELC_2:def 66;
:: thesis: verum end; suppose B4:
not
w |= * (SuccNode1 (chosen_formula U,N),N)
;
:: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )now per cases
( chosen_formula U,N is atomic or chosen_formula U,N is negative or chosen_formula U,N is conjunctive or chosen_formula U,N is next or chosen_formula U,N is disjunctive or chosen_formula U,N is Until or chosen_formula U,N is Release )
by MODELC_2:2;
suppose
(
chosen_formula U,
N is
atomic or
chosen_formula U,
N is
negative or
chosen_formula U,
N is
conjunctive or
chosen_formula U,
N is
next )
;
:: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )hence
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
by A1, A2, LemSUM04, LemSUM06, B4;
:: thesis: verum end; suppose C2:
(
chosen_formula U,
N is
disjunctive or
chosen_formula U,
N is
Until or
chosen_formula U,
N is
Release )
;
:: thesis: ( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )then
chosen_succ w,
v,
U,
N is_succ2_of N
by A2, B1, Def209;
hence
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
by Def210, A1, A2, B1, C2, Lem203, Lem204, Lem205, B4;
:: thesis: verum end; hence
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
;
:: thesis: verum
hence
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
;
:: thesis: verum
end; hence
(
w |= * (chosen_succ w,v,U,N) &
chosen_succ w,
v,
U,
N is_succ_of N )
;
:: thesis: verum end;
hence
( w |= * (chosen_succ w,v,U,N) & chosen_succ w,v,U,N is_succ_of N )
; :: thesis: verum