let n be Nat; 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; 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); ( 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 H1( Nat) -> strict LTLnode over v = CastNode ((q . $1),v);
assume that
A1:
H is Until
and
A2:
( H in the LTLold of H1(1) & ( for i being Nat holds H1(i + 1) is_next_of H1(i) ) )
; ( 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, Lm31; verum