include "RTL/RTL_semantics.ma".
include "joint/Traces.ma".
include "common/StatusSimulation.ma".

axiom RTL_separate_to_unique_ok :
∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
∀p_in : rtl_program.
∀init_in.make_initial_state
  (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in →
∃init_out.
  make_initial_state
   (mk_prog_params RTL_semantics_unique p_in stacksizes) =
    OK ? init_out ∧
∃[1] R.
  status_simulation_with_init
    (joint_status RTL_semantics_separate_overflow p_in stacksizes)
    (joint_status RTL_semantics_unique p_in stacksizes)
    R init_in init_out.