include "Cminor/test/factorial.Cminor.ma".

example exec: finishes_with (repr 120) ? (exec_up_to Cminor_fullexec myprog 100 [EVint I32 (repr 5)]).
normalize  (* you can examine the result here *)
@refl qed.

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

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