1 files changed, 0 insertions, 73 deletions
diff --git a/backend/Remove_Vertex_Adjacency.v b/backend/Remove_Vertex_Adjacency.v
deleted file mode 100755
index 668063d..0000000
--- a/backend/Remove_Vertex_Adjacency.v
+++ /dev/null
@@ -1,73 +0,0 @@
-Require Import FSets.
-Require Import InterfGraphMapImp.
-Require Import Interference_adjacency.
-Require Import Edges.
-Require Import MyRegisters.
-
-Import RegFacts Props.
-
-Module Register := Regs.
-
-(* For any vertex x different from r, the neighborhood of x in
-    (remove_vertex r g) is its one in g, minus r *)
-Lemma remove_interf_adj : forall x r g,
-~Register.eq x r ->
-VertexSet.Equal (interference_adj x (remove_vertex r g)) 
-                          (VertexSet.remove r (interference_adj x g)).
-
-Proof.
-intros.
-split; intros.
-apply VertexSet.remove_2. intro.
-rewrite <-H1 in H0. rewrite in_interf in H0.
-generalize (proj1 (In_graph_edge_in_ext _ _ H0)). change_rewrite. intro.
-rewrite In_remove_vertex in H2. destruct H2. elim (H3 (Register.eq_refl _)).
-rewrite in_interf in H0. rewrite In_remove_edge in H0. destruct H0.
-rewrite in_interf. assumption.
-
-rewrite in_interf. rewrite In_remove_edge.
-split.
-rewrite <-in_interf. apply (VertexSet.remove_3 H0).
-intro. destruct H1; change_rewrite.
-elim (VertexSet.remove_1 H1 H0).
-elim H. auto.
-Qed.
-
-(* If x is different from r and does not belong to the interference neighborhood
-   of r in g, then the interference neighborhood of x in (remove_vertex r g)
-   is equal to the interference neighborhood of x in g *)
-Lemma interf_adj_remove : forall x r g,
-~VertexSet.In x (interference_adj r g) ->
-~Register.eq x r ->
-VertexSet.Equal (interference_adj x g) (interference_adj x (remove_vertex r g)).
-
-Proof.
-intros x r g H H0.
-rewrite remove_interf_adj. rewrite remove_equal. apply VertexSet.eq_refl.
-intro. elim H. apply interf_adj_comm. assumption.
-auto.
-Qed.
-
-(* The interference neighborhood of x in (remove_vertex r g)
-    is a subset of the interference neighborhood of x in g *)
-Lemma sub_remove_interf : forall x r g,
-~Register.eq x r ->
-VertexSet.Subset (interference_adj x (remove_vertex r g))
-                            (interference_adj x g).
-
-Proof.
-intros x r g H. rewrite remove_interf_adj.
-unfold VertexSet.Subset. intros y H0.
-apply (VertexSet.remove_3 H0).
-assumption.
-Qed.
-
-(* If x is a neighbor of r in g, then x belongs to (remove_vertex r g) *)
-Lemma in_interf_adj_in_remove : forall x r g,
-VertexSet.In x (interference_adj r g) -> In_graph x (remove_vertex r g).
-
-Proof.
-intros x r g H. rewrite In_remove_vertex. split.
-rewrite in_interf in H. apply (proj1 (In_graph_edge_in_ext _ _ H)).
-intro H0. rewrite H0 in H. elim (not_in_interf_self _ _ H).
-Qed.