theorem :: MODELC_3:53

for n being 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)) )