examples

1 files changed, 3 insertions, 5 deletions

diff --git a/app/Web.hs b/app/Web.hs
index 7f7c2ba..ba54f85 100644
--- a/app/Web.hs
+++ b/app/Web.hs
@@ -95,17 +95,15 @@ homeURI f = "/" <> toUrlPiece (safeLink api (Proxy :: Proxy HomeAPI) f :: Link)
 examples :: [(String, String)]
 examples =
   [ ("1+1=2", "one plus one equals two."),
-    ("Ax.Ax'.x+x'=x'+x", "addition is commutative."),
-    ("Ee.Ax.x+e=x", "there exists an additive identity."),
+    ("Ax.Ay.x+y=y+x", "addition is commutative."),
     ("Ex.Ay.x>y", "there exists a largest natural."),
+    ("Ee.Ax.(x+e=x & Ay.(x+y=x -> e=y))", "the additive identity exists and is unique."),
     ("Ax.Ey.2y=x", "every natural is even."),
     ("Ax.Ey.(2y=x | 2y+1=x)", "every natural is either even or odd."),
     ("Ax.Ay.Az.((x=y & y=z) -> x=z)", "equality is transitive."),
     ("Ax.Ay.(x<=y <-> y<=x)", "less-than-or-equal-to is symmetric."),
     ("Ax.Ay.((x<=y & y<=x) -> x=y)", "less-than-or-equal-to is antisymmetric."),
-    ("Ax.Ay.(x+1=y+1 -> x=y)", "the successor function is injective."),
-    ("Ax.x+1!=0", "there is no natural whose successor is zero."),
-    ("(Ax.x=x & Ex.x=0 & Ex.x=1)", "the Sphinx is not an acolyte of prenex normal form.")
+    ("Ax.Ay.(x+1=y+1 -> x=y)", "the successor function is injective.")
   ]
 
 styles :: HomeView -> (String, String, [Attribute])