let n be Nat; :: thesis: for H, v being LTL-formula
for q being sequence of (LTLStates v) st H is Until & H in the LTLold of (CastNode (q . 1),v) & ( for i being Nat holds CastNode (q . (i + 1)),v is_next_of CastNode (q . i),v ) & ( for i being Nat st 1 <= i & i < n holds
not the_right_argument_of H in the LTLold of (CastNode (q . i),v) ) holds
for i being Nat st 1 <= i & i < n holds
( the_left_argument_of H in the LTLold of (CastNode (q . i),v) & H in the LTLold of (CastNode (q . i),v) )
let H, v be LTL-formula; :: thesis: for q being sequence of (LTLStates v) st H is Until & H in the LTLold of (CastNode (q . 1),v) & ( for i being Nat holds CastNode (q . (i + 1)),v is_next_of CastNode (q . i),v ) & ( for i being Nat st 1 <= i & i < n holds
not the_right_argument_of H in the LTLold of (CastNode (q . i),v) ) holds
for i being Nat st 1 <= i & i < n holds
( the_left_argument_of H in the LTLold of (CastNode (q . i),v) & H in the LTLold of (CastNode (q . i),v) )
let q be sequence of (LTLStates v); :: thesis: ( H is Until & H in the LTLold of (CastNode (q . 1),v) & ( for i being Nat holds CastNode (q . (i + 1)),v is_next_of CastNode (q . i),v ) & ( for i being Nat st 1 <= i & i < n holds
not the_right_argument_of H in the LTLold of (CastNode (q . i),v) ) implies for i being Nat st 1 <= i & i < n holds
( the_left_argument_of H in the LTLold of (CastNode (q . i),v) & H in the LTLold of (CastNode (q . i),v) ) )
deffunc H₁( Nat) -> strict LTLnode of v = CastNode (q . $1),v;
assume that
A1: H is Until and
A2: ( H in the LTLold of H₁(1) & ( for i being Nat holds H₁(i + 1) is_next_of H₁(i) ) ) ; :: thesis: ( ex i being Nat st
( 1 <= i & i < n & the_right_argument_of H in the LTLold of (CastNode (q . i),v) ) or for i being Nat st 1 <= i & i < n holds
( the_left_argument_of H in the LTLold of (CastNode (q . i),v) & H in the LTLold of (CastNode (q . i),v) ) )
set G = the_right_argument_of H;
set F = the_left_argument_of H;
H = (the_left_argument_of H) 'U' (the_right_argument_of H) by A1, MODELC_2:8;
hence ( ex i being Nat st
( 1 <= i & i < n & the_right_argument_of H in the LTLold of (CastNode (q . i),v) ) or for i being Nat st 1 <= i & i < n holds
( the_left_argument_of H in the LTLold of (CastNode (q . i),v) & H in the LTLold of (CastNode (q . i),v) ) ) by A2, Lm32; :: thesis: verum