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 & chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) holds
( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,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 & chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) holds
( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,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 & chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) holds
( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,N) )
let U be Choice_Function of BOOL (Subformulae v); :: thesis: ( w |= * N & not N is elementary & chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) implies ( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,N) ) )
assume A1:
( w |= * N & not N is elementary )
; :: thesis: ( not chosen_formula U,N is Until or not w |= the_right_argument_of (chosen_formula U,N) or ( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,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);
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;
A2:
chosen_formula U,N in the LTLnew of N
by A1, Thchoice;
( chosen_formula U,N is Until & w |= the_right_argument_of (chosen_formula U,N) implies ( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,N) ) )
proof
assume B1:
(
chosen_formula U,
N is
Until &
w |= the_right_argument_of (chosen_formula U,N) )
;
:: thesis: ( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,N) )
then B2:
chosen_succ w,
v,
U,
N = SuccNode2 (chosen_formula U,N),
N
by Defchosensucc;
B3:
LTLNew2 (chosen_formula U,N) = {(the_right_argument_of (chosen_formula U,N))}
by B1, Def204;
B4:
( 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, B2, Def207, B3;
B5:
chosen_formula U,
N in {(chosen_formula U,N)}
by TARSKI:def 1;
now per cases
( the_right_argument_of (chosen_formula U,N) in the LTLold of N or not the_right_argument_of (chosen_formula U,N) in the LTLold of N )
;
suppose B6:
not
the_right_argument_of (chosen_formula U,N) in the
LTLold of
N
;
:: thesis: ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N )
the_right_argument_of (chosen_formula U,N) in {(the_right_argument_of (chosen_formula U,N))}
by TARSKI:def 1;
then
the_right_argument_of (chosen_formula U,N) in {(the_right_argument_of (chosen_formula U,N))} \ the
LTLold of
N
by B6, XBOOLE_0:def 5;
hence
(
the_right_argument_of (chosen_formula U,N) in the
LTLnew of
(chosen_succ w,v,U,N) or
the_right_argument_of (chosen_formula U,N) in the
LTLold of
N )
by B4, XBOOLE_0:def 3;
:: thesis: verum end;
hence
( (
the_right_argument_of (chosen_formula U,N) in the
LTLnew of
(chosen_succ w,v,U,N) or
the_right_argument_of (chosen_formula U,N) in the
LTLold of
N ) &
chosen_formula U,
N in the
LTLold of
(chosen_succ w,v,U,N) )
by B5, B4, XBOOLE_0:def 3;
:: thesis: verum
end;
hence
( not chosen_formula U,N is Until or not w |= the_right_argument_of (chosen_formula U,N) or ( ( the_right_argument_of (chosen_formula U,N) in the LTLnew of (chosen_succ w,v,U,N) or the_right_argument_of (chosen_formula U,N) in the LTLold of N ) & chosen_formula U,N in the LTLold of (chosen_succ w,v,U,N) ) )
; :: thesis: verum