ajout branche allocation de registres

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 16 insertions, 0 deletions

diff --git a/backend/Delete_Preference_Edges_Degree.v b/backend/Delete_Preference_Edges_Degree.v
new file mode 100755
index 00000000..6b781f22
--- /dev/null
+++ b/backend/Delete_Preference_Edges_Degree.v
@@ -0,0 +1,16 @@
+Require Import FSets.
+Require Import InterfGraphMapImp.
+Require Import Delete_Preference_Edges_Adjacency.
+Require Import Edges.
+
+Import Edge Props RegFacts.
+
+(* The interference degree is left unchanged when r is frozen. Hence,
+   a vertex is of low-degree after freezing r iff it is before freezing r *)
+Lemma delete_preference_edges_low : forall x r g K p,
+has_low_degree g K x = has_low_degree (delete_preference_edges r g p) K x.
+
+Proof.
+intros x r g K p. unfold has_low_degree, interf_degree.
+rewrite <-(Equal_cardinal (interf_adj_delete_preference x r g p)). reflexivity.
+Qed.