diff --git a/index.html b/index.html
index c326915..b7ae8f3 100644
--- a/index.html
+++ b/index.html
@@ -596,6 +596,67 @@
             |- by (3) {}}
         s. 0 1 |- elim (M-Surround 1 "$s") {}}
     </hol-string-proof>
+    <hol-string id="index.html/string-arithmetic" deps="index.html/myconfig">
+      -------- nat-z
+      (Nat Z)
+      
+      n. (Nat n)
+      -------- nat-s
+      (Nat (S n))
+
+      n1.
+      -------- nat-plus-z
+      (Eval (Plus n1 Z) n1) 
+
+      n1. n2. res.
+      (Eval (Plus n1 n2) res)
+      --------- nat-plus-s
+      (Eval (Plus n1 (S n2)) (S res))
+
+      ------- string-zero
+      (Parse "0" Z)
+
+      ------- string-one
+      (Parse "1" (S Z))
+
+      -------- string-two
+      (Parse "2" (S (S Z)))
+
+      -------- string-three
+      (Parse "3" (S (S (S Z))))
+
+      s1. s2. n2.
+      (Parse s2 n2)
+      --------- string-prod
+      (Parse "$s1 * $s2" (Prod s1 n2))
+
+      s1.
+      ---------- eval-prod-Z
+      (Eval (Prod s1 Z) "")
+
+      s1. s1n. n.
+      (Eval (Prod s1 n) s1n)
+      ----------- eval-prod-S
+      (Eval (Prod s1 (S n)) "$s1$s1n")
+
+      s. ast. res.
+      (Parse s ast)
+      (Eval ast res)
+      --------------- program-eval
+      (PEval s res)
+
+    </hol-string>
+    <hol-string-proof id="index.html/sexp-nat-toy" deps="index.html/myconfig index.html/string-arithmetic">
+      ----------- mexp-lexp
+      (Eval (Plus (S Z) (S (S Z))) (S (S (S Z))))
+      |- ?
+    </hol-string-proof> 
+    <hol-string-proof id="index.html/string-prod-toy" deps="index.html/myconfig index.html/string-arithmetic">
+      ------------- foo-3
+      (PEval "foo * 3" "foo foo foo")
+      |- ?
+
+    </hol-string-proof>
   <script type="module" src="./src/testcomponent.tsx"></script>
   </body>
 </html>