rm old select/selectl/selectf/selectfs

1 files changed, 0 insertions, 75 deletions

diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 78a2bb31..ada02585 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -660,81 +660,6 @@ Proof.
 - InvEval. apply eval_orlimm; auto.
 - (*orn*) InvEval. TrivialExists; simpl; congruence.
 - (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence.
-  - (* selectl *)
-    destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists.
-    predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists.
-    predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; [ | TrivialExists].
-    inv H.
-    inv H0.
-    inv H6.
-    inv H3.
-    inv H2.
-    inv H7.
-    inv H4.
-    inv H3.
-    inv H6.
-    inv H4.
-    inv H3.
-    inv H14.
-    inv H13.
-    inv H6.
-    inv H4.
-    inv H13.
-    inv H14.
-    inv H9.
-    inv H11.
-    inv H13.
-    inv H3.
-    inv H6.
-    inv H7.
-    inv H3.
-    inv H14.
-    inv H17.
-    simpl in *.
-    inv H8.
-    inv H5.
-    inv H10.
-    inv H12.
-    inv H15.
-    inv H16.
-    inv H11.
-    inv H13.
-    unfold same_expr_pure in PURE.
-    destruct y0; try congruence.
-    destruct y1; try congruence.
-    destruct (ident_eq i i0); try congruence; clear PURE.
-    rewrite <- e0 in *; clear e0.
-    inv H6.
-    inv H7.
-    rename v10 into vtest.
-    replace v11 with vtest in * by congruence.
-    TrivialExists.
-    simpl.
-    f_equal.
-    rewrite eval_selectl_to2.
-    unfold eval_selectl2.
-    destruct vtest; simpl; trivial.
-    rewrite Val.andl_commut.
-    destruct v4; simpl; trivial.
-    rewrite Val.andl_commut.
-    rewrite Val.orl_commut.
-    destruct v9; simpl; trivial.
-    rewrite int64_eq_commut.
-    destruct (Int64.eq Int64.zero i1); simpl.
-    
-    + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
-      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
-      rewrite Int64.and_mone.
-      rewrite Int64.and_zero.
-      rewrite Int64.or_commut.
-      rewrite Int64.or_zero.
-      reflexivity.
-   + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
-      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
-      rewrite Int64.and_mone.
-      rewrite Int64.and_zero.
-      rewrite Int64.or_zero.
-      reflexivity.
 
   - (*insfl first case*)
     destruct (is_bitfieldl _ _) eqn:Risbitfield.