Simplify 01W Preorder

Author: nickdrozd

src/Algebra/ZeroOneOmega.idr

@@ -10,23 +10,22 @@ data ZeroOneOmega = Rig0 | Rig1 | RigW
 
 export
 Preorder ZeroOneOmega where
-  Rig0 <= _ = True
+  Rig0 <=    _ = True
   Rig1 <= Rig1 = True
-  Rig1 <= RigW = True
-  RigW <= RigW = True
-  _ <= _ = False
+  _    <= RigW = True
+  _    <=    _ = False
   preorderRefl {x = Rig0} = Refl
   preorderRefl {x = Rig1} = Refl
   preorderRefl {x = RigW} = Refl
-  preorderTrans {x = Rig0} {y = y} {z = z} a b = Refl
-  preorderTrans {x = Rig1} {y = Rig0} {z = Rig0} Refl Refl impossible
-  preorderTrans {x = Rig1} {y = Rig1} {z = Rig0} _ Refl impossible
-  preorderTrans {x = Rig1} {y = RigW} {z = Rig0} _ Refl impossible
-  preorderTrans {x = Rig1} {y = y} {z = Rig1} a b = Refl
-  preorderTrans {x = Rig1} {y = y} {z = RigW} a b = Refl
-  preorderTrans {x = RigW} {y = Rig0} {z = _} Refl _ impossible
-  preorderTrans {x = RigW} {y = Rig1} {z = _} Refl _ impossible
-  preorderTrans {x = RigW} {y = RigW} {z = z} a b = b
+  preorderTrans {x = Rig0} _ _ = Refl
+  preorderTrans {x = Rig1} {y = Rig0} _ _ impossible
+  preorderTrans {x = Rig1} {y = Rig1} _ yz = yz
+  preorderTrans {x = Rig1} {y = RigW} {z = Rig0} _ _ impossible
+  preorderTrans {x = Rig1} {y = RigW} {z = Rig1} _ _ = Refl
+  preorderTrans {x = Rig1} {y = RigW} {z = RigW} _ _ = Refl
+  preorderTrans {x = RigW} {y = Rig0} _ _ impossible
+  preorderTrans {x = RigW} {y = Rig1} _ _ impossible
+  preorderTrans {x = RigW} {y = RigW} _ yz = yz
 
 public export
 Eq ZeroOneOmega where
@@ -45,17 +44,16 @@ export
 rigPlus : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
 rigPlus Rig0 a = a
 rigPlus a Rig0 = a
-rigPlus Rig1 a = RigW
-rigPlus a Rig1 = RigW
-rigPlus RigW RigW = RigW
+rigPlus _ _ = RigW
 
 export
 rigMult : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
 rigMult Rig0 _ = Rig0
 rigMult _ Rig0 = Rig0
 rigMult Rig1 a = a
 rigMult a Rig1 = a
-rigMult RigW RigW = RigW
+rigMult _ _ = RigW
+
 
 public export
 Semiring ZeroOneOmega where