(**************************************************************************)
(*       ___                                                              *)
(*      ||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                  *)
(*                                                                        *)
(**************************************************************************)

include "ASM/Interpret2.ma".
include "ASM/Policy.ma".
include "common/StatusSimulation.ma".

axiom assembly_ok :
∀p_in : pseudo_assembly_program.
∀sigma_pol.
jump_expansion' p_in = Some ? sigma_pol →
let sigma ≝ λx.\fst sigma_pol x in
let policy ≝ λx.\snd sigma_pol x in
let p_out ≝ pi1 ?? (assembly p_in sigma policy) in
let init_in ≝ initialise_status … p_in in
let init_out ≝ initialise_status … (cm p_out) in
∃[1]R.
  status_simulation_with_init
    (ASM_status p_in sigma policy)
    (OC_abstract_status p_out)
    R init_in init_out.