module chap6
imports prop-laws prop-eval2 signatures/-

rules

  SwapArgs : Or(e1,e2) -> Or(e2,e1)

  SwapBoth : Or(e1,e2)  -> Or(e2,e1)
  SwapBoth : And(e1,e2) -> And(e2,e1)

  ExMid: And(Not(x),x) -> False()
  ExMid: And(x,Not(x)) -> False()

strategies

  better-dnf =
    innermost(DefI <+ DefE <+ ExMid <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO); eval-down