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.