include "ERTL/ERTL.ma". include "ERTL/liveness.ma". definition vertex ≝ register ⊎ Register. inductive decision: Type[0] ≝ | decision_spill: nat → decision | decision_colour: Register → decision. definition is_member ≝ λvertex. λregister_lattice. let 〈l, r〉 ≝ register_lattice in match vertex with [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l | inr v ⇒ set_member ? eq_Register v r ]. record coloured_graph (v: valuation): Type[1] ≝ { colouring: vertex → decision; prop_colouring: ∀l. ∀v1, v2: vertex. is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2 }. axiom build: ∀valuation. coloured_graph valuation.