let v be LTL-formula; for N being strict LTLnode over 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 over 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 NO = the LTLold of N;
set NN = the LTLnew 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 ( 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 )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