diff --git a/examples/arithmetic.modal b/examples/arithmetic.modal
index 374274f..776bc74 100644
--- a/examples/arithmetic.modal
+++ b/examples/arithmetic.modal
@@ -1,6 +1,6 @@
-<> (add (s ?x) (s ?y)) ((s add ?x (s ?y)))
-<> (add (s ?y) (0)) ((s ?y))
-<> (add (0) (s ?y)) ((s ?y))
+<> (add (s ?x) (s ?y)) (s (add ?x (s ?y)))
+<> (add (s ?x) (0)) (s ?x)
+<> (add (0) (s ?y)) (s ?y)
 <> (add (0) (0)) (0)
 
 <> (subtract (s ?x) (s ?y)) (subtract ?x ?y)
@@ -8,7 +8,7 @@
 <> (subtract (0) (s ?y)) (s ?y)
 <> (subtract (0) (0)) (0)
 
-<> (multiply (s ?x) (s ?y)) (add (s ?x) (multiply (s ?x) (subtract (s ?y) (s (0))))
+<> (multiply (s ?x) (s ?y)) (add (s ?x) (multiply (s ?x) (subtract (s ?y) (s (0)))))
 <> (multiply (s ?x) (s (0)) (s ?x)
 <> (multiply (s (0)) (s ?y) (s ?y)
 <> (multiply (s ?x) (0)) (0)
@@ -17,7 +17,8 @@
 <> (?x + ?y) (add ?x ?y)
 <> (?x - ?y) (subtract ?x ?y)
 <> (?x * ?y) (multiply ?x ?y)
-<> (factorial (s (0))) ((s (0)))
-<> (factorial (s ?x)) ((s ?x) * factorial ((s ?x) - (s (0))))
 
-(s (0)) * (s (s (0)))
\ No newline at end of file
+<> (factorial (s (0))) ((s (0)))
+<> (factorial (s ?x)) (((s ?x) * factorial ((s ?x) - (s (0)))))
+
+factorial (s (s (s (s (s (0))))))
diff --git a/examples/test.modal b/examples/test.modal
index 374274f..2b3e220 100644
--- a/examples/test.modal
+++ b/examples/test.modal
@@ -1,23 +1,5 @@
-<> (add (s ?x) (s ?y)) ((s add ?x (s ?y)))
-<> (add (s ?y) (0)) ((s ?y))
-<> (add (0) (s ?y)) ((s ?y))
-<> (add (0) (0)) (0)
+<> (?x dup) (?x ?x)
+<> (?x ?y swap) (?y ?x)
+<> ( ?x pop) ()
 
-<> (subtract (s ?x) (s ?y)) (subtract ?x ?y)
-<> (subtract (s ?x) (0)) (s ?x)
-<> (subtract (0) (s ?y)) (s ?y)
-<> (subtract (0) (0)) (0)
-
-<> (multiply (s ?x) (s ?y)) (add (s ?x) (multiply (s ?x) (subtract (s ?y) (s (0))))
-<> (multiply (s ?x) (s (0)) (s ?x)
-<> (multiply (s (0)) (s ?y) (s ?y)
-<> (multiply (s ?x) (0)) (0)
-<> (multiply (0) (s ?x)) (0)
-
-<> (?x + ?y) (add ?x ?y)
-<> (?x - ?y) (subtract ?x ?y)
-<> (?x * ?y) (multiply ?x ?y)
-<> (factorial (s (0))) ((s (0)))
-<> (factorial (s ?x)) ((s ?x) * factorial ((s ?x) - (s (0))))
-
-(s (0)) * (s (s (0)))
\ No newline at end of file
+(1 2 3) (4 5 6) swap pop dup