1 files changed, 6 insertions, 12 deletions
diff --git a/src/Rep/WordEquivalence.v b/src/Rep/WordEquivalence.v
index 6c625db60..4005adc2a 100644
--- a/src/Rep/WordEquivalence.v
+++ b/src/Rep/WordEquivalence.v
@@ -22,9 +22,9 @@ Module GFBits (M: Modulus).
     match len with
     | O => []
     | S len' =>
-      if(sz - wordSize > 0)
+      if(sz - wordSize >? 0)
       then Cons (split1 wordSize (sz - wordSize) x)
-                (words len' (split2 wordSize (sz - wordSize) x))
+                (splitWords len' (split2 wordSize (sz - wordSize) x))
       else zext x wordSize
     end.
 
@@ -34,22 +34,16 @@ Module GFBits (M: Modulus).
     | Cons x xs => combine x (combineAll xs)
     end.
 
+  wordEq a b := wordToN (combineAll a) = wordToN (combineAll b)
+
   Definition toZ (b: BinGF) := Z.of_N (wordToN (combineAll b)).
   Definition toGF (b: BinGF) := ZToGF ((toZ b) mod modulus)
 
   Definition fromZ (x: Z) := splitWords numWords (NToWord (Z.to_N x))
   Definition fromGF (x: GF) := fromZ (proj1_sig x).
 
-  Inductive BinEquiv (x: GF) (y: BinGF) :=
-  | EquivGF : forall x, BinEquiv x (fromGF x)
-  | EquivBin : forall y, BinEquiv (toGF y) y
-  | EquivPlus : forall x1 y1 x2 y2,
-    BinEquiv x1 y1 -> binEquiv x2 y2 -> BinEquiv (x1 + x2) (y1 ^+ y2)%word
-  | EquivMinus : forall x1 y1 x2 y2,
-    BinEquiv x1 y1 -> binEquiv x2 y2 -> BinEquiv (x1 - x2) (y1 ^- y2)%word
-  | EquivMult : forall x1 y1 x2 y2,
-    BinEquiv x1 y1 -> binEquiv x2 y2 -> BinEquiv (x1 * x2) (y1 ^* y2)%word.
-
+  toZ a + toZ b = toZ (a ^+ b)
+  
   Lemma equivalent_GF : BinEquiv x y <-> x = toGF y.
   Admitted.