include "RTL/RTLToERTL.ma".
include "RTL/RTL_semantics.ma".
include "ERTL/ERTL_semantics.ma".
include "joint/Traces.ma".
include "common/StatusSimulation.ma".

axiom RTLToERTL_ok :
∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
∀p_in : rtl_program.
let p_out ≝ rtl_to_ertl p_in in
  ∀init_in.make_initial_state
    (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
∃init_out.
  make_initial_state
   (mk_prog_params ERTL_semantics p_out stacksizes) =
    OK ? init_out ∧
∃[1] R.
  status_simulation_with_init
    (joint_status RTL_semantics_unique p_in stacksizes)
    (joint_status ERTL_semantics p_out stacksizes)
    R init_in init_out.