From 6b3075d90d945d5e7e8fd4d28284ffd99dbeb82e Mon Sep 17 00:00:00 2001
From: Shinya Sato <shinnya.sato@gmail.com>
Date: Fri, 24 Sep 2021 16:42:54 +0900
Subject: v0.4.1

---
 sample/AckSZ-3_5.in | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 sample/AckSZ-3_5.in

(limited to 'sample/AckSZ-3_5.in')

diff --git a/sample/AckSZ-3_5.in b/sample/AckSZ-3_5.in
new file mode 100644
index 0000000..0d0ebe4
--- /dev/null
+++ b/sample/AckSZ-3_5.in
@@ -0,0 +1,18 @@
+// Ackermann function on unary natural numbers
+// fun ack(0,y) = y+1
+//   | ack(x,0) = ack(x-1,1)        
+//   | ack(x,y) = ack(x-1,ack(x,y-1));
+//
+ack(r,y)>< Z => r~S(y);
+ack(r,y)>< S(x) => ack_Sx(r, x)~y;
+ack_Sx(r,x)>< Z => ack(r, S(Z))~x;
+ack_Sx(r,x)>< S(y) => dup(x1,x2)~x, ack(r,cnt)~x1, ack_Sx(cnt,x2)~y;
+
+
+dup(a1,a2)>< Z => a1~Z, a2~Z;
+dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), dup(w1,w2)~x;
+
+// Ack 3 5
+ack(r, S(S(S(S(S(Z))))))~S(S(S(Z)));
+prnat r;
+exit;
-- 
cgit v1.2.3