(* NB: this is essentially the same as Graphs! *)

include "basics/types.ma".

include "ASM/BitVectorTrie.ma".
include "common/Identifiers.ma".
include "ASM/I8051.ma".

axiom RegisterTag : String.

definition register ≝ identifier RegisterTag.

definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.

definition register_env ≝ identifier_map RegisterTag.

(* dpm: fix the Register/register mismatch *)
axiom Register_of_register: register → Register.
axiom register_of_Register: Register → register.