module Algebra.ZeroOneOmega import Algebra.Semiringimport Algebra.Preorder exportdata ZeroOneOmega = Rig0 | Rig1 | RigW Preorder ZeroOneOmega where  Rig0 <= _ = True  Rig1 <= Rig1 = True  Rig1 <= RigW = True  RigW <= 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 public exportEq ZeroOneOmega where  (==) Rig0 Rig0 = True  (==) Rig1 Rig1 = True  (==) RigW RigW = True  (==) _ _ = False exportShow ZeroOneOmega where  show Rig0 = "Rig0"  show Rig1 = "Rig1"  show RigW = "RigW" exportrigPlus : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmegarigPlus Rig0 a = arigPlus a Rig0 = arigPlus Rig1 a = RigWrigPlus a Rig1 = RigWrigPlus RigW RigW = RigW exportrigMult : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmegarigMult Rig0 _ = Rig0rigMult _ Rig0 = Rig0rigMult Rig1 a = arigMult a Rig1 = arigMult RigW RigW = RigW public exportSemiring ZeroOneOmega where  (|+|) = rigPlus  (|*|) = rigMult  plusNeutral = Rig0  timesNeutral = Rig1 ||| The top value of a latticeexportTop ZeroOneOmega where  top = RigW  topAbs {x = Rig0} = Refl  topAbs {x = Rig1} = Refl  topAbs {x = RigW} = Refl