include "ERTLptr/liveness.ma". inductive decision: Type[0] ≝ | decision_spill: nat → decision | decision_colour: Register → decision. (* prop_colouring is the non interferece prop_colouring 2 and 3 together say that spilled_no is the number of spilled registers *) (* Wilmer: the generation of the destruct principle diverges; Ctr-C make the file pass *) record coloured_graph (after: valuation register_lattice): Type[1] ≝ { colouring: vertex → decision ; spilled_no: nat ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2 ; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *) ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no }. definition coloured_graph_computer ≝ ∀globals. joint_internal_function ERTLptr globals → ∀valuation. coloured_graph valuation.