module prop-dnf7
imports libstrategolib prop-laws

rules
  proptr7(s) : Not(x)     -> Not (<s>x)
  proptr7(s) : And(x, y)  -> And (<s>x, <s>y)
  proptr7(s) : Or(x, y)   -> Or  (<s>x, <s>y)
  proptr7(s) : Impl(x, y) -> Impl(<s>x, <s>y)
  proptr7(s) : Eq(x, y)   -> Eq  (<s>x, <s>y)
strategies
  dnf7    = try(proptr7(dnf7)); dnfred7
  dnfred7 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf7)
  cnf7    = try(proptr7(cnf7)); cnfred7
  cnfred7 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf7)