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) ) & ex i being Nat st
( i >= 1 & not ( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) holds
ex j being Nat st
( j >= 1 & the_right_argument_of H in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of 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) ) & ex i being Nat st
( i >= 1 & not ( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) implies ex j being Nat st
( j >= 1 & the_right_argument_of H in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) ) )
deffunc H₁( Nat) -> strict LTLnode over 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: ( for i being Nat st i >= 1 holds
( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) or ex j being Nat st
( j >= 1 & the_right_argument_of H in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of 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 ( for i being Nat st i >= 1 holds
( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) & not the_right_argument_of H in the LTLold of (CastNode ((q . i),v)) ) or ex j being Nat st
( j >= 1 & the_right_argument_of H in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( H in the LTLold of (CastNode ((q . i),v)) & the_left_argument_of H in the LTLold of (CastNode ((q . i),v)) ) ) ) ) by A2, Lm32; :: thesis: verum