module prop-dnf6
imports libstrategolib prop-laws

rules
  dnft6 : Not(x)     -> Not (<dnf6>x)
  dnft6 : And(x, y)  -> And (<dnf6>x, <dnf6>y)
  dnft6 : Or(x, y)   -> Or  (<dnf6>x, <dnf6>y)
  dnft6 : Impl(x, y) -> Impl(<dnf6>x, <dnf6>y)
  dnft6 : Eq(x, y)   -> Eq  (<dnf6>x, <dnf6>y)
strategies
  dnf6    = try(dnft6); dnfred6
  dnfred6 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf6)