let v be LTL-formula; 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 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; for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of BOOL (Subformulae v) st 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 ; for U being Choice_Function of BOOL (Subformulae v) st 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); ( 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) ) )
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;
assume
not N is elementary
; ( 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) ) )
then A1:
chosen_formula U,N in the LTLnew of N
by Th58;
( 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 that A2:
chosen_formula U,
N is
Until
and A3:
w |= the_right_argument_of (chosen_formula U,N)
;
( ( 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) )
A4:
chosen_succ w,
v,
U,
N = SuccNode2 (chosen_formula U,N),
N
by A2, A3, Def35;
LTLNew2 (chosen_formula U,N) = {(the_right_argument_of (chosen_formula U,N))}
by A2, Def2;
then A5:
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)
by A1, A4, Def5;
A6:
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 A7:
not
the_right_argument_of (chosen_formula U,N) in the
LTLold of
N
;
( 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 A7, 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 A5, XBOOLE_0:def 3;
verum end;
A8:
chosen_formula U,
N in {(chosen_formula U,N)}
by TARSKI:def 1;
the
LTLold of
(chosen_succ w,v,U,N) = the
LTLold of
N \/ {(chosen_formula U,N)}
by A1, A4, Def5;
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 A8, A6, XBOOLE_0:def 3;
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) ) )
; verum