From 1d86b1c178deb97f3d499f461a417a4fe6846cf8 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 20 Oct 2021 10:03:01 +0100
Subject: Start to prove termination of SAT

---
 src/hls/Abstr.v | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'src/hls/Abstr.v')

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index faa5955..dc883b2 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -790,14 +790,6 @@ Definition ind_preds_l t :=
     sat_predicate p1 c = true ->
     sat_predicate p2 c = false.
 
-Definition sat_predictable :
-  forall a b c n,
-  sat_pred_simple n (a ∧ b) = Some c ->
-  exists d e, sat_pred_simple n a = Some e /\ sat_pred_simple n a = Some d.
-Proof.
-  intros. unfold sat_pred_simple in H. destruct_match; try discriminate.
-  destruct_match. unfold sat_pred in *. simplify.
-
 Lemma pred_equivalence_Some :
   forall (ta tb: PTree.t pred_op) e pe pe',
     ta ! e = Some pe ->
-- 
cgit