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