(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* just an axiom stub *)
include "ERTL/ERTLToERTLptr.ma".
include "ERTL/ERTL_semantics.ma".
include "ERTLptr/ERTLptr_semantics.ma".
include "joint/Traces.ma".
include "common/StatusSimulation.ma".

axiom ertl_to_ertlptr_ok:
∀prog.∀stack_sizes.
let trans_prog ≝ ertl_to_ertlptr prog in
   ∃[1]R.
   status_simulation
    (joint_status ERTL_semantics prog stack_sizes)
    (joint_status ERTLptr_semantics trans_prog stack_sizes) R ∧
  ∀init_in.make_initial_state
    (mk_prog_params ERTL_semantics prog stack_sizes) = OK … init_in →
  ∃init_out.
    make_initial_state
     (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) =
      OK ? init_out ∧
   R init_in init_out.