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

(*include "ASM/BitVectorTrie.ma".*)
include "common/Identifiers.ma".
(*include "ASM/I8051.ma".*)
include "common/Order.ma".

definition register ≝ identifier RegisterTag.

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

definition register_env ≝ identifier_map RegisterTag.

(*
axiom register_ord: register → register → order.
*)