15 lines
520 B
Plaintext
15 lines
520 B
Plaintext
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)
|