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

set LN = LTLNodes v;
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 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 :: 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)) )

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 A4: 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)) )

deffunc H₁( set ) -> strict LTLnode over 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: ( 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:1;
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: verum

end;

A9: for k being Nat st 1 <= k & k < len L holds
ex N1, M1 being strict LTLnode over 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 over v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) )
assume that
A10: 1 <= k and
A11: k < len L ; :: thesis: ex N1, M1 being strict LTLnode over v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 )
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:14;
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 over v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) by A13, A12; :: thesis: verum

end;

then A14: L is_Finseq_for 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;
then A15: 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 A8
.= 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:84
.= CastNode (('X' (CastNode (((chosen_run (w,v,U)) . j),v))),v) by A3, FUNCT_1:18
.= 'X' (CastNode (((chosen_run (w,v,U)) . j),v)) by Def16 ;
1 <= (chosen_succ_end_num ((Shift (w,j)),v,U,('X' (CastNode (((chosen_run (w,v,U)) . j),v))))) + 1 by NAT_1:11;
then A16: 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 A5, A8
.= 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 ;
A17: 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 A2, A4, Def48;
1 <= len L by A5, NAT_1:11;
then A18: len L > 1 by A4, A15, A16, A17, XXREAL_0:1;
A19: ( 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 that
A20: 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)) and
A21: H is Until and
A22: 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))
( the LTLold of (CastNode ((L . 1),v)) = {} v & 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 A15, A16, Def16;
then consider m being Nat such that
A23: 1 <= m and
A24: m < (chosen_succ_end_num ((Shift (w,j)),v,U,('X' (CastNode (((chosen_run (w,v,U)) . j),v))))) + 1 and
A25: ( not H in the LTLold of (CastNode ((L . m),v)) & H in the LTLold of (CastNode ((L . (m + 1)),v)) ) by A5, A14, A18, A20, Th27;
set mm1 = m - 1;
reconsider mm1 = m - 1 as Nat by A23, NAT_1:21;
set Nm1 = ((choice_succ_func ((Shift (w,j)),v,U)) |** mm1) . ('X' (CastNode (((chosen_run (w,v,U)) . j),v)));
set m1 = m + 1;
A26: ((choice_succ_func ((Shift (w,j)),v,U)) |** mm1) . ('X' (CastNode (((chosen_run (w,v,U)) . j),v))) in LTLNodes v by A3, FUNCT_2:5;
consider N1, N2 being strict LTLnode over v such that
A27: N1 = L . m and
A28: N2 = L . (m + 1) and
A29: N2 is_succ_of N1 by A5, A9, A23, A24;
A30: N1 = CastNode ((((choice_succ_func ((Shift (w,j)),v,U)) |** (CastNat mm1)) . ('X' (CastNode (((chosen_run (w,v,U)) . j),v)))),v) by A8, A23, A24, A27
.= 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 ;
A31: ( 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 A23, A24, NAT_1:13;
then A32: 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 A8, A28
.= 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:71
.= 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 A3, FUNCT_2:15
.= 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 A26, Def36
.= chosen_succ ((Shift (w,j)),v,U,N1) by A30, Def16 ;
m - 1 < ((chosen_succ_end_num ((Shift (w,j)),v,U,('X' (CastNode (((chosen_run (w,v,U)) . j),v))))) + 1) - 1 by A24, XREAL_1:14;
then A33: not N1 is elementary by A2, A4, A30, Def48;
chosen_formula (U,N1) = H

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;
A34: chosen_formula (U,N1) in the LTLnew of N1 by A33, Th58;
A35: the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula (U,N1))}

proof

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

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 Def35;
hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula (U,N1))} by A32, A34, Def4; :: thesis: verum

end;

suppose A36: ( 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))}

N2 = SuccNode2 ((chosen_formula (U,N1)),N1) by A32, A36, Def35;
hence the LTLold of N2 = the LTLold of N1 \/ {(chosen_formula (U,N1))} by A34, Def5; :: thesis: verum

end;

end;

end;

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

end;

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

now :: thesis: not H <> chosen_formula (U,N1)

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

end;

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

end;

then A38: N2 = SuccNode2 (H,N1) by A21, A22, A32, Def35;
A39: 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 A16, Def16;
( N1 = CastNode ((L . m),v) & N2 = CastNode ((L . (m + 1)),v) ) by A27, A28, Def16;
then N2 is_succ_of N1,H by A25, A29, Th28;
then A40: H in the LTLnew of N1 ;
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 A17;
then the LTLnew of (CastNode ((L . (m + 1)),v)) c= the LTLold of (CastNode ((L . (len L)),v)) by A5, A14, A31, A39, Th34;
then A41: 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 A28, A39, Def16;
the LTLold of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v)) by A5, A14, A23, A24, Th31;
then A42: 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 A27, A39, Def16;
LTLNew2 H = {(the_right_argument_of H)} by A21, Def2;
then A43: the LTLnew of N2 = ( the LTLnew of N1 \ {H}) \/ ({(the_right_argument_of H)} \ the LTLold of N1) by A38, A40, Def5;

now :: 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))

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

end;

suppose A44: 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 A44, XBOOLE_0:def 5;
then the_right_argument_of H in the LTLnew of N2 by A43, 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 A41; :: 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;

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

end;

suppose '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)) )

then the LTLnew of ('X' (CastNode (((chosen_run (w,v,U)) . j),v))) = the LTLnew of (FinalNode v) ;
then 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 A2, Def49;
then CastNode (((chosen_run (w,v,U)) . (j + 1)),v) = CastNode (('X' (CastNode (((chosen_run (w,v,U)) . j),v))),v) by Def50
.= 'X' (CastNode (((chosen_run (w,v,U)) . j),v)) by Def16 ;
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