include "RTLabs/test/search.RTLabs.ma".

   example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
   normalize  (* you can examine the result here *)
   @refl qed.