include "ERTLptr/ERTLptrToLTL.ma".
include "ERTLptr/ERTLptr_semantics.ma".
include "LTL/LTL_semantics.ma".
include "joint/Traces.ma".
include "common/StatusSimulation.ma".
include "common/AssocList.ma".

(* Inefficient, replace with Trie lookup *)
definition lookup_stack_cost ≝
 λp.λid : ident.
  assoc_list_lookup ? ℕ id (eq_identifier …) p.

axiom ERTLptrToLTL_ok :
∀fix_comp : fixpoint_computer.
∀colour : coloured_graph_computer.
∀p_in : ertlptr_program.
let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in
(* what should we do with n? *)
let stacksizes ≝ lookup_stack_cost m in
∃[1] R.
  status_simulation
    (joint_status ERTLptr_semantics p_in stacksizes)
    (joint_status LTL_semantics p_out stacksizes)
    R ∧
  ∀init_in.make_initial_state
    (mk_prog_params ERTLptr_semantics p_in stacksizes) = OK … init_in →
  ∃init_out.
    make_initial_state
     (mk_prog_params LTL_semantics p_out stacksizes) =
      OK ? init_out ∧
   R init_in init_out.