include "Cminor/test/search.Cminor.ma".


   example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
   normalize  (* you can examine the result here *)
   @refl qed.


include "Cminor/toRTLabs.ma".
include "RTLabs/semantics.ma".

example execRTL: finishes_with (repr 3) ?
(bind ? (snapshot state) (cminor_to_rtlabs myprog)
  (λmyprog'. exec_up_to RTLabs_fullexec myprog' 1000 [ ])).
normalize  (* you can examine the result here *)
@refl
qed.