week4 tweaking

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/week4.mdwn b/week4.mdwn
index 5238b26..78e2d37 100644 (file)
--- a/week4.mdwn
+++ b/week4.mdwn
@@ -69,9 +69,9 @@ succ X
 ≡ (\n s z. s (n s z)) X 
 ~~> \s z. s (X s z)
 <~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-~~> \s z. s ([succ (\s z. s (X s z))] s z)
-~~> \s z. s ([\s z. s ([succ (\s z. s (X s z))] s z)] s z)
-~~> \s z. s (s (succ (\s z. s (X s z))))
+&equiv; (\n s z. s (n s z)) (\s z. s (X s z))
+~~> \s z. s ((\s z. s (X s z)) s z)
+~~> \s z. s (s (X s z))
 </code></pre>
 
 So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,