let H be LTL-formula; :: thesis: for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula
for U being Choice_Function of BOOL (Subformulae v) st w |= v holds
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)
let w be Element of Inf_seq AtomicFamily ; :: thesis: for v being neg-inner-most LTL-formula
for U being Choice_Function of BOOL (Subformulae v) st w |= v holds
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)
let v be neg-inner-most LTL-formula; :: thesis: for U being Choice_Function of BOOL (Subformulae v) st w |= v holds
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)
let U be Choice_Function of BOOL (Subformulae v); :: thesis: ( w |= v implies 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) )
assume A0: w |= v ; :: thesis: 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)
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

let j be Nat; :: thesis: ( 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) )
set LN = LTLNodes v;
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;
A000: 'X' (CastNode ((chosen_run w,v,U) . j),v) in LTLNodes v by defLTLNodes;
A1: Shift w,j |= * ('X' (CastNode ((chosen_run w,v,U) . j),v)) by A0, thBA05;

now

per cases ( not 'X' (CastNode ((chosen_run w,v,U) . j),v) is elementary or 'X' (CastNode ((chosen_run w,v,U) . j),v) is elementary ) ;

suppose B1: not 'X' (CastNode ((chosen_run w,v,U) . j),v) is elementary ; :: thesis: ( 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) )

C0: 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 = CastNode ((chosen_run w,v,U) . (j + 1)),v

proof

(chosen_run w,v,U) . (j + 1) = chosen_next (Shift w,j),v,U,(CastNode ((chosen_run w,v,U) . j),v) by Defchosenrun
.= 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 Defchosennext, A1, B1 ;
hence 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 = CastNode ((chosen_run w,v,U) . (j + 1)),v by defCastNode01; :: thesis: verum

end;

set n1 = (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1;
C3: 1 <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 by NAT_1:11;
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;
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
C4: len L = (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 and
C5: for k being Nat st k in dom L holds
L . k = H₁(k) ;
C601: Seg ((chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1) = dom L by C4, FINSEQ_1:def 3;
C6: 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: ( 1 <= k & k <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 implies L . k = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat (k - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v )
assume ( 1 <= k & k <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 ) ; :: thesis: L . k = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat (k - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v
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 C5, C601;
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: verum

end;

C800: L . 1 = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat (1 - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by C3, C6
.= CastNode (((choice_succ_func (Shift w,j),v,U) |** 0 ) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by MODELC_2:def 1
.= CastNode ((id (LTLNodes v)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by FUNCT_7:86
.= CastNode ('X' (CastNode ((chosen_run w,v,U) . j),v)),v by A000, FUNCT_1:35
.= 'X' (CastNode ((chosen_run w,v,U) . j),v) by defCastNode01 ;
C801: ( 1 <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 & (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 ) by NAT_1:11;
C8: L . (len L) = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat (((chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1) - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by C6, C801, C4
.= 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 MODELC_2:def 1 ;
C8p: 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: ( 1 <= k & k < len L implies ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) )
assume D1: ( 1 <= k & k < len L ) ; :: thesis: ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 )
set k1 = k - 1;
set kp = k + 1;
D200: ( 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 D1, C4, NAT_1:13;
reconsider k1 = k - 1 as Nat by D1, NAT_1:21;
D2: k - 1 < ((chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1) - 1 by D1, C4, XREAL_1:16;
set M1 = CastNode (((choice_succ_func (Shift w,j),v,U) |** (k1 + 1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v;
set N1 = CastNode (((choice_succ_func (Shift w,j),v,U) |** k1) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v;
D3: 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 D2, DefUsuccEndnum, A1, B1;
D4: L . k = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat k1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by D1, C4, C6
.= 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 ;
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 D200, C6
.= 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 ;
hence ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) by D3, D4; :: thesis: verum

end;

then C9: L is_Finseq_for v by DefFinseq;
C10: 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 is elementary by DefUsuccEndnum, A1, B1;
( 1 <= len L & 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 is_next_of CastNode ((chosen_run w,v,U) . j),v ) by A0, thBA05, C0, C4, NAT_1:11;
then C12: len L > 1 by C800, B1, C10, C8, XXREAL_0:1;
( 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) & H is Until & Shift w,j |= the_right_argument_of H implies 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) )

proof

set H2 = the_right_argument_of H;
assume D1: ( 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) & H is Until & Shift w,j |= the_right_argument_of H ) ; :: thesis: 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)
D3: the LTLold of (CastNode (L . 1),v) = {} v by defCastNode01, C800;
D4: the LTLold of (CastNode (L . (len L)),v) = 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 defCastNode01, C8;
consider m being Nat such that
D501: ( 1 <= m & m < (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 & not H in the LTLold of (CastNode (L . m),v) & H in the LTLold of (CastNode (L . (m + 1)),v) ) by C9, D3, C4, C12, D4, D1, ThSucc03;
consider N1, N2 being strict LTLnode of v such that
D5p: ( N1 = L . m & N2 = L . (m + 1) & N2 is_succ_of N1 ) by C8p, D501, C4;
D5p1: ( N1 = CastNode (L . m),v & N2 = CastNode (L . (m + 1)),v ) by D5p, defCastNode01;
set mm1 = m - 1;
reconsider mm1 = m - 1 as Nat by D501, NAT_1:21;
D601: m - 1 < ((chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1) - 1 by D501, XREAL_1:16;
set Nm1 = ((choice_succ_func (Shift w,j),v,U) |** mm1) . ('X' (CastNode ((chosen_run w,v,U) . j),v));
D6: ((choice_succ_func (Shift w,j),v,U) |** mm1) . ('X' (CastNode ((chosen_run w,v,U) . j),v)) in LTLNodes v by A000, FUNCT_2:7;
D7: N1 = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat mm1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by C6, D501, D5p
.= CastNode (((choice_succ_func (Shift w,j),v,U) |** mm1) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by MODELC_2:def 1 ;
then D7p: ( Shift w,j |= * N1 & not N1 is elementary ) by D601, DefUsuccEndnum, A1, B1;
set m1 = m + 1;
D801: ( 1 <= m + 1 & m + 1 <= (chosen_succ_end_num (Shift w,j),v,U,('X' (CastNode ((chosen_run w,v,U) . j),v))) + 1 ) by D501, NAT_1:13;
D8: N2 = CastNode (((choice_succ_func (Shift w,j),v,U) |** (CastNat ((m + 1) - 1))) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by C6, D801, D5p
.= CastNode (((choice_succ_func (Shift w,j),v,U) |** (mm1 + 1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by MODELC_2:def 1
.= CastNode (((choice_succ_func (Shift w,j),v,U) * ((choice_succ_func (Shift w,j),v,U) |** mm1)) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v by FUNCT_7:73
.= CastNode ((choice_succ_func (Shift w,j),v,U) . (((choice_succ_func (Shift w,j),v,U) |** mm1) . ('X' (CastNode ((chosen_run w,v,U) . j),v)))),v by A000, FUNCT_2:21
.= CastNode (chosen_succ (Shift w,j),v,U,(CastNode (((choice_succ_func (Shift w,j),v,U) |** mm1) . ('X' (CastNode ((chosen_run w,v,U) . j),v))),v)),v by D6, Defchoicesuccfunc
.= chosen_succ (Shift w,j),v,U,N1 by defCastNode01, D7 ;
D10: N2 is_succ_of N1,H by D501, D5p, D5p1, ThSucc04;
D11: chosen_formula U,N1 = H

proof

set M0 = the LTLnew of N1;
set M1 = the LTLold of N1;
set M2 = the LTLold of N2;
E1: ( not H in the LTLold of N1 & H in the LTLold of N2 ) by D501, D5p, defCastNode01;
set G = chosen_formula U,N1;
E401: chosen_formula U,N1 in the LTLnew of N1 by D7p, Thchoice;
E5: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

proof

now

per cases ( ( 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) ) or ( 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) ) ) ) ;

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: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

then chosen_succ (Shift w,j),v,U,N1 = SuccNode1 (chosen_formula U,N1),N1 by Defchosensucc;
hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)} by D8, E401, Def206; :: thesis: verum

end;

suppose EA1: ( 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: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

then EB1: N2 = SuccNode2 (chosen_formula U,N1),N1 by Defchosensucc, D8;
set S1 = SuccNode1 (chosen_formula U,N1),N1;
set G2 = the_right_argument_of (chosen_formula U,N1);

now

per cases ( ( chosen_formula U,N1 is Until & Shift w,j |= the_right_argument_of (chosen_formula U,N1) ) or not Shift w,j |= * (SuccNode1 (chosen_formula U,N1),N1) ) by EA1;

suppose ( chosen_formula U,N1 is Until & Shift w,j |= the_right_argument_of (chosen_formula U,N1) ) ; :: thesis: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)} by E401, EB1, Def207; :: thesis: verum

end;

suppose EB4: not Shift w,j |= * (SuccNode1 (chosen_formula U,N1),N1) ; :: thesis: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

now

per cases ( chosen_formula U,N1 is atomic or chosen_formula U,N1 is negative or chosen_formula U,N1 is conjunctive or chosen_formula U,N1 is next or chosen_formula U,N1 is disjunctive or chosen_formula U,N1 is Until or chosen_formula U,N1 is Release ) by MODELC_2:2;

suppose ( chosen_formula U,N1 is atomic or chosen_formula U,N1 is negative or chosen_formula U,N1 is conjunctive or chosen_formula U,N1 is next ) ; :: thesis: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)} by D7p, E401, LemSUM04, LemSUM06, EB4; :: thesis: verum

end;

suppose ( chosen_formula U,N1 is disjunctive or chosen_formula U,N1 is Until or chosen_formula U,N1 is Release ) ; :: thesis: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)}

hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula U,N1)} by E401, EB1, Def207; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

now

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

end;

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

end;

D12: N2 = SuccNode2 H,N1 by D11, D1, Defchosensucc, D8;
D13: ( H in the LTLnew of N1 & H is Until ) by D1, D10, DefSucc01;
LTLNew2 H = {(the_right_argument_of H)} by D1, Def204;
then D13p: the LTLnew of N2 = (the LTLnew of N1 \ {H}) \/ ({(the_right_argument_of H)} \ the LTLold of N1) by D12, D13, Def207;
D14: CastNode (L . (len L)),v = 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 C8, defCastNode01;
the LTLnew 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 C10, Defelementary;
then the LTLnew of (CastNode (L . (m + 1)),v) c= the LTLold of (CastNode (L . (len L)),v) by D14, C9, D801, C4, ThSucc10;
then D16: the LTLnew of N2 c= 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 D5p, D14, defCastNode01;
the LTLold of (CastNode (L . m),v) c= the LTLold of (CastNode (L . (len L)),v) by D501, C4, C9, ThSucc07;
then D17: the LTLold of N1 c= 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 D5p, D14, defCastNode01;

now

per cases ( the_right_argument_of H in the LTLold of N1 or not the_right_argument_of H in the LTLold of N1 ) ;

suppose the_right_argument_of H in the LTLold of N1 ; :: thesis: 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)

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 D17; :: thesis: verum

end;

suppose D18: not the_right_argument_of H in the LTLold of N1 ; :: thesis: 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)

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 D18, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by D13p, 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 D16; :: thesis: verum

end;

end;

end;

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) ; :: thesis: verum

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) ) by C0; :: thesis: verum

end;

suppose B2: 'X' (CastNode ((chosen_run w,v,U) . j),v) is elementary ; :: thesis: ( 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) )

C1: the LTLnew of ('X' (CastNode ((chosen_run w,v,U) . j),v)) = the LTLnew of (FinalNode v) by B2, Defelementary;
chosen_next (Shift w,j),v,U,(CastNode ((chosen_run w,v,U) . j),v) = 'X' (CastNode ((chosen_run w,v,U) . j),v) by C1, A1, Defchosennext;
then CastNode ((chosen_run w,v,U) . (j + 1)),v = CastNode ('X' (CastNode ((chosen_run w,v,U) . j),v)),v by Defchosenrun
.= 'X' (CastNode ((chosen_run w,v,U) . j),v) by defCastNode01 ;
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: verum

end;

end;

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: verum

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: verum