include "ASM/I8051.ma".
include "common/Registers.ma".
include "utilities/adt/set_adt.ma".

definition vertex ≝ nat. (* XXX: int in o'caml *)

(*
axiom Register_ordered: ordered Register.
axiom register_ordered: ordered register.
axiom vertex_ordered: ordered vertex.
*)

axiom register_table: Type[0].
  
axiom rt_empty : register_table.

axiom rt_insert: vertex → set Register → register_table → register_table.
  
axiom rt_forward : vertex → register_table → set Register.
axiom rt_backward: Register → register_table → vertex.
  
axiom rt_add: Register → vertex → register_table → register_table.
axiom rt_remove: vertex → register_table → register_table.

axiom rt_fold: ∀a: Type[0]. (vertex → set Register → a → a) →
   register_table → a → a.

axiom rt_coalesce: vertex → vertex → register_table → register_table.
axiom rt_restrict: (vertex → bool) → register_table → register_table.