let H be LTL-formula; :: thesis:
let w be Element of Inf_seq AtomicFamily ; :: thesis:
let v be neg-inner-most LTL-formula; :: thesis:
let U be Choice_Function of BOOL (Subformulae v); :: thesis:
assume A1: w |= v ; :: thesis:
for j being Nat st H in the LTLold of (CastNode ((chosen_run w,v,U) . (j + 1)),v) & H is Until & Shift w,j |= the_right_argument_of H holds
the_right_argument_of H in the LTLold of (CastNode ((chosen_run w,v,U) . (j + 1)),v)

proof

set LN = LTLNodes v;
let j be Nat; :: thesis:
set s = CastNode ((chosen_run w,v,U) . j),v;
set s1 = CastNode ((chosen_run w,v,U) . (j + 1)),v;
set w0 = Shift w,j;
set N = 'X' (CastNode ((chosen_run w,v,U) . j),v);
set f = choice_succ_func (Shift w,j),v,U;
set n = chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v));
set nextnode = CastNode (((choice_succ_func (Shift w,j),v,U) |** (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v)))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v;
A2: Shift w,j |= * ('X' (CastNode ((chosen_run w,v,U) . j),v)) by A1, Th73;
A3: 'X' (CastNode ((chosen_run w,v,U) . j),v) in LTLNodes v by Def30;

now

per cases ;

suppose A4: not 'X' (CastNode ((chosen_run w,v,U) . j),v) is elementary ; :: thesis:

deffunc H₁( set ) -> strict LTLnode of v = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat ((CastNat $1) - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v;
set n1 = (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1;
ex L being FinSequence st
( len L = (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 & ( for k being Nat st k in dom L holds
L . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider L being FinSequence such that
A5: len L = (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 and
A6: for k being Nat st k in dom L holds
L . k = H₁(k) ;
A7: Seg ((chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1) = dom L by A5, FINSEQ_1:def 3;
A8: for k being Nat st 1 <= k & k <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 holds
L . k = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat (k - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v

proof

let k be Nat; :: thesis:
assume ( 1 <= k & k <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 ) ; :: thesis:
then k in Seg ((chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1) by FINSEQ_1:3;
then L . k = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat ((CastNat k) - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by A6, A7;
hence L . k = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat (k - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by MODELC_2:def 1; :: thesis:

end;

A9: for k being Nat st 1 <= k & k < len L holds
ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 )

proof

let k be Nat; :: thesis:
assume that
A10: 1 <= k and
A11: k < len L ; :: thesis:
set k1 = k - 1;
reconsider k1 = k - 1 as Nat by A10, NAT_1:21;
set M1 = CastNode (((choice_succ_func (Shift w,j),v,U) |** (k1 + 1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v;
set kp = k + 1;
( 1 <= k + 1 & k + 1 <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 ) by A5, A10, A11, NAT_1:13;
then A12: L . (k + 1) = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat ((k + 1) - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by A8
.= CastNode (((choice_succ_func (Shift w,j),v,U) |** (k1 + 1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by MODELC_2:def 1 ;
set N1 = CastNode (((choice_succ_func (Shift w,j),v,U) |** k1) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v;
k - 1 < ((chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1) - 1 by A5, A11, XREAL_1:16;
then A13: CastNode (((choice_succ_func (Shift w,j),v,U) |** (k1 + 1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v is_succ_of CastNode (((choice_succ_func (Shift w,j),v,U) |** k1) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by A2, A4, Def48;
L . k = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat k1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by A5, A8, A10, A11
.= CastNode (((choice_succ_func (Shift w,j),v,U) |** k1) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by MODELC_2:def 1 ;
hence ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) by A13, A12; :: thesis:

end;

proof

proof

set G = chosen_formula U,N1;
set M2 = the LTLold of N2;
set M1 = the LTLold of N1;
set M0 = the LTLnew of N1;
A36: chosen_formula U,N1 in the LTLnew of N1 by A34, Th58;
A37: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

proof

now

per cases ;

suppose ( ( not chosen_formula U,N1 is Until & Shift w,j |= * (SuccNode1 (chosen_formula U,N1),N1) ) or ( chosen_formula U,N1 is Until & Shift w,j |/= the_right_argument_of (chosen_formula U,N1) ) ) ; :: thesis:

then chosen_succ (Shift w,j),v,U,N1 = SuccNode1 (chosen_formula U,N1),N1 by Def35;
hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)} by A32, A36, Def4; :: thesis:

end;

suppose A38: ( not ( not chosen_formula U,N1 is Until & Shift w,j |= * (SuccNode1 (chosen_formula U,N1),N1) ) & not ( chosen_formula U,N1 is Until & Shift w,j |/= the_right_argument_of (chosen_formula U,N1) ) ) ; :: thesis:

set G2 = the_right_argument_of (chosen_formula U,N1);
set S1 = SuccNode1 (chosen_formula U,N1),N1;
N2 = SuccNode2 (chosen_formula U,N1),N1 by A32, A38, Def35;
hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)} by A36, Def5; :: thesis:

end;

hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)} ; :: thesis:

end;

A41: ( not H in the LTLold of N1 & H in the LTLold of N2 ) by A25, A27, A28, Def16;

now

assume H <> chosen_formula U,N1 ; :: thesis:
then not H in {(chosen_formula U,N1)} by TARSKI:def 1;
hence contradiction by A41, A37, XBOOLE_0:def 3; :: thesis:

end;

hence chosen_formula U,N1 = H ; :: thesis:

end;

now

per cases ;

suppose the_right_argument_of H in the LTLold of N1 ; :: thesis:

hence the_right_argument_of H in the LTLold of (CastNode (((choice_succ_func (Shift w,j),v,U) |** (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v)))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v) by A46; :: thesis:

end;

suppose A48: not the_right_argument_of H in the LTLold of N1 ; :: thesis:

the_right_argument_of H in {(the_right_argument_of H)} by TARSKI:def 1;
then the_right_argument_of H in {(the_right_argument_of H)} \ the LTLold of N1 by A48, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by A47, XBOOLE_0:def 3;
hence the_right_argument_of H in the LTLold of (CastNode (((choice_succ_func (Shift w,j),v,U) |** (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v)))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v) by A45; :: thesis:

end;

(chosen_run w,v,U) . (j + 1) = chosen_next (Shift w,j),v,U,(CastNode ((chosen_run w,v,U) . j),v) by Def50
.= CastNode (((choice_succ_func (Shift w,j),v,U) |** (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v)))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by A2, A4, Def49 ;
hence ( H in the LTLold of (CastNode ((chosen_run w,v,U) . (j + 1)),v) & H is Until & Shift w,j |= the_right_argument_of H implies the_right_argument_of H in the LTLold of (CastNode ((chosen_run w,v,U) . (j + 1)),v) ) by A19, Def16; :: thesis:

end;

suppose 'X' (CastNode ((chosen_run w,v,U) . j),v) is elementary ; :: thesis:

end;

hence ( H in the LTLold of (CastNode ((chosen_run w,v,U) . (j + 1)),v) & H is Until & Shift w,j |= the_right_argument_of H implies the_right_argument_of H in the LTLold of (CastNode ((chosen_run w,v,U) . (j + 1)),v) ) ; :: thesis:

end;

hence for i being Nat st H in the LTLold of (CastNode ((chosen_run w,v,U) . (i + 1)),v) & H is Until & Shift w,i |= the_right_argument_of H holds
the_right_argument_of H in the LTLold of (CastNode ((chosen_run w,v,U) . (i + 1)),v) ; :: thesis: