bexp2store True_ _ = return True

bexp2store False_ _ = return False

bexp2store (BVar x) _ = ($x)

bexp2store (Or bs) st = do

is <- mapM (\x -> bexp2store x st) bs

return (or is)

bexp2store (And bs) st = do

is <- mapM (\x -> bexp2store x st) bs

return (and is)

bexp2store (Not bs) st = do

i <- bexp2store bs st

return (not i)

bexp2store (e1 := e2) st

= return ( exp2store e1 st == exp2store e2 st)

bexp2store (e1 :<= e2) st

= return ( exp2store e1 st <= exp2store e2 st)