diff --git a/test/manual-suite.spt b/test/manual-suite.spt
index 1e4f1d9..59b35da 100644
--- a/test/manual-suite.spt
+++ b/test/manual-suite.spt
@@ -1,7 +1,7 @@
 /** md
 Title: The Remaining Tests
 
-## Programmable Rewriting strategies
+## Programmable Rewriting Strategies
 
 The manual then begins to discuss "programmable rewriting strategies" in
 [Section 5.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/05-rewriting-strategies.html#programmable-rewriting-strategies)
@@ -54,12 +54,13 @@ test sec5_1_2_test1_cnf_ex [[
                        Or(Not(Atom("r")), Atom("q"))),
                    Atom("p"))
 
-test sec5_1_2_test1_both_ex [[
+test sec5_1_2_test1_both [[
   (r -> p & q) & p
-]] run dcnf to (Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p"))),
-                And(And(Or(Not(Atom("r")), Atom("p")),
-                        Or(Not(Atom("r")), Atom("q"))),
-                    Atom("p")))
+]] run dcnf to Atom("x")
+//(Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p"))),
+//                And(And(Or(Not(Atom("r")), Atom("p")),
+//                        Or(Not(Atom("r")), Atom("q"))),
+//                    Atom("p")))
 
 test sec5_3_1_test1_dnf_ex [[
   (r -> p & q) & p
@@ -70,3 +71,23 @@ test sec5_3_1_test1_cnf_ex [[
 ]] run cnf4 to And(And(Or(Not(Atom("r")), Atom("p")),
                        Or(Not(Atom("r")), Atom("q"))),
                    Atom("p"))
+
+test sec5_3_2_eval_up_ex [[
+  (1 -> p & q) & p
+]] run eval-up to And(And(Atom("p"),Atom("q")),Atom("p"))
+
+test sec5_3_2_eval_down_ex [[
+  (1 -> p & q) & p
+]] run eval-down to And(And(Atom("p"),Atom("q")),Atom("p"))
+
+test sec5_3_2_desugar_ex [[
+  (1 -> p & q) & p
+]] run desugar to And(Or(Not(True()),And(Atom("p"),Atom("q"))),Atom("p"))
+
+test sec5_3_2_impl_nf_ex [[
+  (1 -> p & q) & p
+]] run impl-nf to Impl(Impl(Impl(True(),Impl(Impl(Atom("p"),
+                                                  Impl(Atom("q"),False())),
+                                             False())),
+                            Impl(Atom("p"),False())),
+                       False())
diff --git a/trans/prop-desugar.str b/trans/prop-desugar.str
new file mode 100644
index 0000000..45f70a7
--- /dev/null
+++ b/trans/prop-desugar.str
@@ -0,0 +1,22 @@
+module prop-desugar
+imports libstrategolib signatures/-
+
+rules
+
+  DefN  : Not(x)     -> Impl(x, False())
+  DefI  : Impl(x, y) -> Or(Not(x), y)
+  DefE  : Eq(x, y)   -> And(Impl(x, y), Impl(y, x))
+  DefO1 : Or(x, y)   -> Impl(Not(x), y)
+  DefO2 : Or(x, y)   -> Not(And(Not(x), Not(y)))
+  DefA1 : And(x, y)  -> Not(Or(Not(x), Not(y)))
+  DefA2 : And(x, y)  -> Not(Impl(x, Not(y)))
+
+  IDefI : Or(Not(x), y) -> Impl(x, y)
+
+  IDefE : And(Impl(x, y), Impl(y, x)) -> Eq(x, y)
+
+strategies
+
+  desugar = topdown(try(DefI <+ DefE))
+
+  impl-nf = topdown(repeat(DefN <+ DefA2 <+ DefO1 <+ DefE))
diff --git a/trans/prop-dnf-rules.str b/trans/prop-dnf-rules.str
index 9bfab66..dcf6a86 100644
--- a/trans/prop-dnf-rules.str
+++ b/trans/prop-dnf-rules.str
@@ -67,7 +67,7 @@ So, we can just take our `test3` expression above and make it a part of
 an SPT test suite, which we will call `test/manual-suite.spt`:
 ```SPT
 {! ../test/manual-suite.spt extract:
-  start: '\*\*/'
+  start: '\*\*[/]'
 terminate: '(.*run dnf)' !}
 ```
 
@@ -86,7 +86,7 @@ what the transformation actually produced. So we add just a bit to
 `test/manual-suite.spt`:
 ```SPT
 {! ../test/manual-suite.spt extract:
-  start: '\*\*/'
+  start: '\*\*[/]'
 terminate: '(.*run dnf.*)$' !}
 ```
 
diff --git a/trans/prop-eval2.str b/trans/prop-eval2.str
new file mode 100644
index 0000000..9861aff
--- /dev/null
+++ b/trans/prop-eval2.str
@@ -0,0 +1,27 @@
+module prop-eval2
+imports libstrategolib signatures/-
+rules
+
+  Eval : Not(True())      -> False()
+  Eval : Not(False())     -> True()
+  Eval : And(True(), x)   -> x
+  Eval : And(x, True())   -> x
+  Eval : And(False(), x)  -> False()
+  Eval : And(x, False())  -> False()
+  Eval : Or(True(), x)    -> True()
+  Eval : Or(x, True())    -> True()
+  Eval : Or(False(), x)   -> x
+  Eval : Or(x, False())   -> x
+  Eval : Impl(True(), x)  -> x
+  Eval : Impl(x, True())  -> True()
+  Eval : Impl(False(), x) -> True()
+  Eval : Impl(x, False()) -> Not(x)
+  Eval : Eq(False(), x)   -> Not(x)
+  Eval : Eq(x, False())   -> Not(x)
+  Eval : Eq(True(), x)    -> x
+  Eval : Eq(x, True())    -> x
+
+strategies
+
+  eval-up = bottomup(repeat(Eval))
+  eval-down = downup(repeat(Eval))
diff --git a/trans/prop-laws.str b/trans/prop-laws.str
index 1f8987e..570f8ba 100644
--- a/trans/prop-laws.str
+++ b/trans/prop-laws.str
@@ -19,4 +19,4 @@ rules
 strategies
 
   dnf4 = innermost(DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO)
-  cnf4 = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO)
\ No newline at end of file
+  cnf4 = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO)
diff --git a/trans/spoofax_propositional_language.str b/trans/spoofax_propositional_language.str
index f80a4f4..1017ff8 100644
--- a/trans/spoofax_propositional_language.str
+++ b/trans/spoofax_propositional_language.str
@@ -11,6 +11,8 @@ imports
   prop-dnf3
   prop-cnf3
   prop-laws
+  prop-eval2
+  prop-desugar
 
 rules // Debugging