include "basics/types.ma".
include "basics/list.ma".
include "common/Graphs.ma".
include "common/Registers.ma".

definition interference_graph ≝ graph label. 
axiom vertex: Type[0].
axiom vertex_set: Type[0].
axiom vertex_map: Type[0].

axiom ig_create: list register → interference_graph.
axiom ig_mki: interference_graph → (list register) × (list Register) →
  (list register) × (list Register) → interference_graph.
axiom ig_mkiph: interference_graph → list register → list Register →
  interference_graph.
axiom ig_mkppp: interference_graph → register → register → interference_graph.
axiom ig_mkpph: interference_graph → register → Register → interference_graph.
axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
axiom ig_remove: interference_graph → vertex → interference_graph.
axiom ig_freeze: interference_graph → vertex → interference_graph.
axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
axiom ig_droph: interference_graph → interference_graph.
axiom ig_lookup: interference_graph → register → vertex.
axiom ig_registers: interference_graph → vertex → list register.
axiom ig_degree: interference_graph → vertex → nat.
axiom ig_lowest: interference_graph → option (vertex × nat).
axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
  interference_graph → option vertex.
axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
axiom ig_ipp: interference_graph → vertex → list vertex.
axiom ig_iph: interference_graph → vertex → list Register.
axiom ig_ppp: interference_graph → vertex → list vertex.
axiom ig_pph: interference_graph → vertex → list Register.
definition ig_ppedge ≝ vertex × vertex.
axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
definition ig_phedge ≝ vertex × Register.
axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.