v0.12.2

8 files changed, 619 insertions, 0 deletions

diff --git a/sample/unary_numbers/GCM2023/AckSZ-3_10-reuse.in b/sample/unary_numbers/GCM2023/AckSZ-3_10-reuse.in
new file mode 100644
index 0000000..6c82def
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/AckSZ-3_10-reuse.in
@@ -0,0 +1,13 @@
+// Ackermann function on unary natural numbers
+
+ack(r,y)>< Z    => r~(*R)S(y);
+ack(r,y)>< S(x) => (*L)ack_Sx(r, x)~y;
+ack_Sx(r,x)>< Z    => (*L)ack(r, S((*R)Z))~x;
+ack_Sx(r,x)>< S(y) => (*R)Dup(x1,x2)~x, (*L)ack(r,cnt)~x1, ack_Sx(cnt,x2)~y;
+
+// ack 3 10
+//          1 2 3 4 5 6 7 8 9 0
+ack(result, S(S(S(S(S(S(S(S(S(S(Z)))))))))))~S(S(S(Z)));
+
+prnat result;
+exit;
diff --git a/sample/unary_numbers/GCM2023/AckSZ-3_10.in b/sample/unary_numbers/GCM2023/AckSZ-3_10.in
new file mode 100644
index 0000000..6dec0ab
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/AckSZ-3_10.in
@@ -0,0 +1,13 @@
+// Ackermann function on unary natural numbers
+
+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;
+
+// ack 3 10
+//          1 2 3 4 5 6 7 8 9 0
+ack(result, S(S(S(S(S(S(S(S(S(S(Z)))))))))))~S(S(S(Z)));
+
+prnat result;
+exit;
diff --git a/sample/unary_numbers/GCM2023/FibSZ_31-reuse.in b/sample/unary_numbers/GCM2023/FibSZ_31-reuse.in
new file mode 100644
index 0000000..3163182
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/FibSZ_31-reuse.in
@@ -0,0 +1,19 @@
+// Fibonacci number on unary natural numbers
+fib(r)><Z => r~(*R)Z;
+fib(r)><S(x) => (*L)fibS(r)~x;
+fibS(r)><Z => r~(*L)S((*R)Z);
+fibS(r)><S(x) => (*R)Dup(x1,x2)~x, (*L)add(r,r2)~r1, fib(r2)~x2, fibS(r1)~x1;
+
+
+//------ ADD ------
+add(r,x)><Z => r~x;
+add(r,x)><S(y) => r~(*R)S(w), (*L)add(w,x)~y;
+
+
+// Execution
+// Fib 31
+//     1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
+fib(r)~S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)))))))))))))))))))))))))))))));
+prnat r;
+free r;
+
diff --git a/sample/unary_numbers/GCM2023/FibSZ_31.in b/sample/unary_numbers/GCM2023/FibSZ_31.in
new file mode 100644
index 0000000..6bb2297
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/FibSZ_31.in
@@ -0,0 +1,19 @@
+// Fibonacci number on unary natural numbers
+fib(r)><Z => r~Z;
+fib(r)><S(x) => fibS(r)~x;
+fibS(r)><Z => r~S(Z);
+fibS(r)><S(x) => Dup(x1,x2)~x, add(r,r2)~r1, fib(r2)~x2, fibS(r1)~x1;
+
+
+//------ ADD ------
+add(r,x)><Z => r~x;
+add(r,x)><S(y) => r~S(w), add(w,x)~y;
+
+
+// Execution
+// Fib 31
+//     1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
+fib(r)~S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)))))))))))))))))))))))))))))));
+prnat r;
+free r;
+
diff --git a/sample/unary_numbers/GCM2023/hanoi19-reuse.in b/sample/unary_numbers/GCM2023/hanoi19-reuse.in
new file mode 100644
index 0000000..af34c47
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/hanoi19-reuse.in
@@ -0,0 +1,52 @@
+// Tower of Hanoi Puzzle
+
+// Rules
+hanoi(return, source, target, aux) >< Z => 
+          // Erase the source, target and aux
+          source ~ (*L)Eraser,
+          target ~ (*R)Eraser,
+          aux ~ Eraser,
+
+          // result
+          return~[];
+
+hanoi(return, source, target, aux) >< S(n) => 
+          // Duplicate the source, target and aux
+	  source ~ Dup(src1, Dup(src2, src3)),
+          target ~ Dup(tgt1, Dup(tgt2, tgt3)),
+          aux ~ Dup(aux1, aux2),
+
+	  
+          // recursive applications
+	  n ~ Dup(nn1, Dup(nn2, nn3)),
+          (*L)hanoi(ret1, src1, aux1, tgt1)~nn1,
+          (*R)hanoi(ret2, aux2, tgt2, src2)~nn2,
+
+          // result
+	  append(return, ((nn3,src3,tgt3)):ret2)~ret1;
+
+
+// ---------------------------------------
+// append
+// ---------------------------------------
+append(r,a) >< [] => r~a;
+append(r,a) >< x:xs => r~(*R)(x:w), (*L)append(w,a)~xs;
+
+
+// ---------------------------------------
+// len
+// ---------------------------------------
+len(ret) >< [] => ret~(*L)Z;
+len(ret) >< x:xs => (*L)len_(ret, (*R)S(Z))~xs, Eraser~x;
+len_(ret, n) >< [] => ret~n;
+len_(ret, n) >< x:xs => (*L)len_(ret, (*R)S(n))~xs, Eraser~x;
+
+
+
+// Net
+hanoi(result, A, C, B) ~
+//1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9
+  S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z))))))))))))))))))),
+
+len(r)~result;
+prnat r;
diff --git a/sample/unary_numbers/GCM2023/hanoi19.in b/sample/unary_numbers/GCM2023/hanoi19.in
new file mode 100644
index 0000000..66bc4ab
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/hanoi19.in
@@ -0,0 +1,52 @@
+// Tower of Hanoi Puzzle
+
+// Rules
+hanoi(return, source, target, aux) >< Z => 
+          // Erase the source, target and aux
+          source ~ Eraser,
+          target ~ Eraser,
+          aux ~ Eraser,
+
+          // result
+          return~[];
+
+hanoi(return, source, target, aux) >< S(n) => 
+          // Duplicate the source, target and aux
+	  source ~ Dup(src1, Dup(src2, src3)),
+          target ~ Dup(tgt1, Dup(tgt2, tgt3)),
+          aux ~ Dup(aux1, aux2),
+
+	  
+          // recursive applications
+	  n ~ Dup(nn1, Dup(nn2, nn3)),
+          hanoi(ret1, src1, aux1, tgt1)~nn1,
+          hanoi(ret2, aux2, tgt2, src2)~nn2,
+
+          // result
+	  append(return, ((nn3,src3,tgt3)):ret2)~ret1;
+
+
+// ---------------------------------------
+// append
+// ---------------------------------------
+append(r,a) >< [] => r~a;
+append(r,a) >< x:xs => r~x:w, append(w,a)~xs;
+
+
+// ---------------------------------------
+// len
+// ---------------------------------------
+len(ret) >< [] => ret~Z;
+len(ret) >< x:xs => len_(ret, S(Z))~xs, Eraser~x;
+len_(ret, n) >< [] => ret~n;
+len_(ret, n) >< x:xs => len_(ret, S(n))~xs, Eraser~x;
+
+
+
+// Net
+hanoi(result, A, C, B) ~
+//1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9
+  S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z))))))))))))))))))),
+
+len(r)~result;
+prnat r;
diff --git a/sample/unary_numbers/GCM2023/nqueenSZ_10-reuse.in b/sample/unary_numbers/GCM2023/nqueenSZ_10-reuse.in
new file mode 100644
index 0000000..c37d7dc
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/nqueenSZ_10-reuse.in
@@ -0,0 +1,225 @@
+// N-Queen on unary natural numbers
+//
+// The original is written as a Lisp program in the following file:
+// https://www.istc.kobe-u.ac.jp/activity/mage/m27/27_Lisp.pdf
+
+
+// ---------------------------------------
+// eq
+// equality between unary natural numbers numbers
+// r << eq(m, n)
+// ---------------------------------------
+eq(r,m) >< Z => (*L)eqZ(r)~m;
+eq(r,m) >< S(x) => (*L)eqS(r,x)~m;
+
+eqZ(r) >< Z => r~(*R)True;
+eqZ(r) >< S(x) => r~(*L)False, (*R)Eraser~x;
+
+eqS(r,x) >< Z => r~(*L)False, (*R)Eraser~x;
+eqS(r,x) >< S(y) => (*L)eq(r,y)~x;
+
+
+
+// ---------------------------------------
+// r, m1, n1 << eq_stream(m,n)
+// ---------------------------------------
+eq_stream(r,m1,n1, m) >< Z => (*L)eqZ_stream(r,m1,n1)~m;
+eq_stream(r,m1,n1, m) >< S(n) => n1~(*R)S(w), (*L)eqS_stream(r,m1,w, n)~m;
+
+eqZ_stream(r,m1,n1) >< Z => r~(*L)True, m1~(*R)Z, n1~Z;
+eqZ_stream(r,m1,n1) >< S(m) => r~(*L)False, m1~(*R)S(m), n1~Z;
+
+
+eqS_stream(r,m1,n1, n) >< Z => r~(*L)False, m1~(*R)Z, n1~n;
+eqS_stream(r,m1,n1, n) >< S(m) => m1~(*R)S(w), (*L)eq_stream(r,w , n1, m)~n;
+
+
+
+
+
+// ---------------------------------------
+// member
+//   r, m1, list1 << member(m, list)
+// ---------------------------------------
+// fun member x [] = false
+//  | member x (y::ys) = if x=y then true else (member x ys);
+
+member(r, m1, list1, m) >< [] =>
+        r~(*L)False, m1~m,  list1~(*R)[];
+
+member(r, m1, list1, m) >< n:ys  =>
+	  eq_result, m2, n2 << eq_stream(m,n),
+	  list1~(*R)(n2:cnt), 
+	  (*L)member1(r, m1, cnt, m2, ys) ~ eq_result;
+
+
+member1(r, m1, list1, m2, ys) >< True =>
+	   r~(*R)True, m1~m2, list1~ys;
+
+member1(r, m1, list1, m2, ys) >< False =>
+	   (*L)member(r, m1, list1, m2) ~ys;
+	   
+
+
+
+// ---------------------------------------
+// len_list (stream version)
+//   len, done << len_list(list)
+// ---------------------------------------
+ 
+len_list(len, done) >< [] =>
+        len~(*L)Z, done~(*R)[];
+len_list(len, done) >< x:xs => 
+        done~(*R)(x:cnt), 
+        (*L)len_list_(len, cnt, S(Z))~xs;
+
+len_list_(len, done, ct) >< [] =>
+        len~ct, done~(*R)[];
+len_list_(len, done, ct) >< x:xs => 
+        done~(*R)(x:cnt), 
+        (*L)len_list_(len, cnt, S(ct)) ~ xs; 
+
+
+// ---------------------------------------
+// len (non-stream version)
+//   ret << len(list)
+// ---------------------------------------
+len(ret) >< [] => ret~(*L)Z;
+len(ret) >< x:xs => (*L)len_(ret, (*R)S(Z))~xs, Eraser~x;
+len_(ret, n) >< [] => ret~n;
+len_(ret, n) >< x:xs => (*L)len_(ret, (*R)S(n))~xs, Eraser~x;
+
+
+// ---------------------------------------
+// append (list1++list2)
+//   ret << append(list2, list1) 
+// ---------------------------------------
+append(r,a) >< [] => r~a;
+append(r,a) >< x:xs => r~(*R)(x:w), (*L)append(w,a)~xs;
+
+
+
+
+/** 
+ * threat (stream version)
+ * check for (0,q) and (k, qpos[col=k]) where k=1...
+ * http://www.nct9.ne.jp/m_hiroi/func/haskell06.html
+     0 1 2    --> 
+    +-------------
+   1| . . . . . .
+   2| . . . -3. .  5 - 3 = 2
+   3| . . -2. . .  5 - 2 = 3
+   4| . -1. . . .  5 - 1 = 4
+   5| Q . . . . .  Q position is 5  
+   6| . +1. . . .  5 + 1 = 6
+   7| . . +2. . .  5 + 2 = 7
+   8| . . . +3. .  5 + 2 = 8
+    +-------------
+ *   r, board_done << threat(k,m, board)
+ *   return
+ *        r: True if threat conditions are satisfied
+ *     done: the same to `board'
+ */
+// fun threat k m [] = false
+//   | threat k m (x::xs) =
+//    if (k = x-m) orelse (k = x+m) then true
+//    else (threat (k+1) m xs);
+
+
+
+// r << diff(m,n)
+diff(r,m) >< Z => r~m;
+diff(r,m) >< S(n) => (*L)diff_S(r,n)~m;
+diff_S(r, n) >< Z => r~(*L)S(n);
+diff_S(r, n) >< S(m) => (*L)diff(r,m)~n;
+
+
+
+threat(r, done, k, q) >< [] =>
+	  r~(*L)False, done~(*R)[], Eraser~k, Eraser~q;
+
+threat(r, done, k, q) >< x:xs =>
+	  x1,x2 << Dup(x),
+	  q1,q2 << Dup(q),
+	  diff_xq << diff(x1,q1),
+	  k1,k2 << Dup(k),
+	  eq_ret << eq(k1, diff_xq),
+	  (*L)threat1(r, done, k2, q2 , (*R)(x2:xs))~eq_ret;
+	  
+threat1(r, done, k, q, xxs) >< True =>
+	   r~(*R)True, done~xxs, (*L)Eraser~k, Eraser~q;
+	   
+threat1(r, done, k, q, xxs) >< False =>
+	   (*R)(x1:xs1) ~ xxs,
+	   done~x1:cnt, (*L)threat(r, cnt, S(k), q)~xs1;
+	   
+
+// fun queen1 b n 0 = []
+//   | queen1 b n m =
+//     if (member m b) orelse (threat 1 m b) then (queen1 b n (m-1))
+//     else if (length b) = (n-1) then (m::b)::(queen1 b n (m-1))
+//         else (queen1 (m::b) n n) @ (queen1 b n (m-1));
+// fun queen n = queen1 n [] n;
+
+queen(ret, n) >< () =>
+	   n1, n2 << (*R)Dup(n),
+	   (*L)queen_(ret, [], n1)~n2;
+
+
+queen_(r, b, n) >< Z =>
+	  r~(*L)[], (*R)Eraser~b, Eraser~n;
+	  
+queen_(r, b, n) >< S(m) =>
+	  mem_ret, done_m, done_b << member((*R)S(m), b),
+	  (*L)queen__chk_m_in_b(r, done_b, n, done_m)~mem_ret;	  
+
+
+dec(r)><Z => r~(*R)Z;
+dec(r)><S(n) => r~n;
+
+queen__chk_m_in_b(r, b, n, m) >< True =>
+     m1 << (*R)dec(m),
+     (*L)queen_(r, b, n)~m1;
+
+queen__chk_m_in_b(r, b, n, m) >< False =>
+     m1,m2 << (*R)Dup(m),
+     th_ret, done_b << threat(S(Z), m1, b), 
+     (*L)queen__chk_threat(r, done_b, n, m2)~th_ret;
+
+
+
+queen__chk_threat(r, b, n, m) >< True =>
+	m_dec << (*R)dec(m),
+        (*L)queen_(r, b, n)~m_dec;
+	
+queen__chk_threat(r, b, n, m) >< False =>
+        len_ret, done_b << (*R)len_list(b), 
+	n1,nn << Dup(n),
+	n_dec << dec(nn),
+	eq_ret << eq(len_ret, n_dec),
+	(*L)queen__chk_lastelem(r, done_b, n1, m) ~ eq_ret;
+
+
+
+queen__chk_lastelem(r,b,n, m) >< True =>
+        b1, b2 << (*R)Dup(b),
+	m1, mm << Dup(m),
+	m_dec << dec(mm),
+        r~(m1:b1):cnt, (*L)queen_(cnt, b2, n)~m_dec;
+
+queen__chk_lastelem(r,b,n, m) >< False =>
+        b1, b2 << (*R)Dup(b),
+        r << (*L)append(cnt2, cnt1),
+	n1, Dup(n2,n3) << Dup(n),
+	m1, mm << Dup(m),
+	m_dec << dec(mm),	
+        queen_(cnt1, m1:b1, n1)~n2, queen_(cnt2, b2, n3)~m_dec;
+
+
+
+// ----------------------------------------------------------
+// main
+// ----------------------------------------------------------
+n~S(S(S(S(S(S(S(S(S(S(Z)))))))))), // 10
+queen(ret,n)~(), len(count)~ret;
+prnat count;
\ No newline at end of file
diff --git a/sample/unary_numbers/GCM2023/nqueenSZ_10.in b/sample/unary_numbers/GCM2023/nqueenSZ_10.in
new file mode 100644
index 0000000..2038886
--- /dev/null
+++ b/sample/unary_numbers/GCM2023/nqueenSZ_10.in
@@ -0,0 +1,226 @@
+// N-Queen on unary natural numbers
+//
+// The original is written as a Lisp program in the following file:
+// https://www.istc.kobe-u.ac.jp/activity/mage/m27/27_Lisp.pdf
+
+
+// ---------------------------------------
+// eq
+// equality between unary natural numbers numbers
+// r << eq(m, n)
+// ---------------------------------------
+eq(r,m) >< Z => eqZ(r)~m;
+eq(r,m) >< S(x) => eqS(r,x)~m;
+
+eqZ(r) >< Z => r~True;
+eqZ(r) >< S(x) => r~False, Eraser~x;
+
+eqS(r,x) >< Z => r~False, Eraser~x;
+eqS(r,x) >< S(y) => eq(r,y)~x;
+
+
+
+// ---------------------------------------
+// r, m1, n1 << eq_stream(m,n)
+// ---------------------------------------
+eq_stream(r,m1,n1, m) >< Z => eqZ_stream(r,m1,n1)~m;
+eq_stream(r,m1,n1, m) >< S(n) => n1~S(w), eqS_stream(r,m1,w, n)~m;
+
+eqZ_stream(r,m1,n1) >< Z => r~True, m1~Z, n1~Z;
+eqZ_stream(r,m1,n1) >< S(m) => r~False, m1~S(m), n1~Z;
+
+
+eqS_stream(r,m1,n1, n) >< Z => r~False, m1~Z, n1~n;
+eqS_stream(r,m1,n1, n) >< S(m) => m1~S(w), eq_stream(r,w , n1, m)~n;
+
+
+
+
+
+// ---------------------------------------
+// member
+//   r, m1, list1 << member(m, list)
+// ---------------------------------------
+// fun member x [] = false
+//  | member x (y::ys) = if x=y then true else (member x ys);
+
+member(r, m1, list1, m) >< [] =>
+        r~False, m1~m,  list1~[];
+
+member(r, m1, list1, m) >< n:ys  =>
+	  eq_result, m2, n2 << eq_stream(m,n),
+	  list1~n2:cnt, 
+	  member1(r, m1, cnt, m2, ys) ~ eq_result;
+
+
+member1(r, m1, list1, m2, ys) >< True =>
+	   r~True, m1~m2, list1~ys;
+
+member1(r, m1, list1, m2, ys) >< False =>
+	   member(r, m1, list1, m2) ~ys;
+	   
+
+
+
+
+// ---------------------------------------
+// len_list (stream version)
+//   len, done << len_list(list)
+// ---------------------------------------
+ 
+len_list(len, done) >< [] =>
+        len~Z, done~[];
+len_list(len, done) >< x:xs => 
+        done~x:cnt, 
+        len_list_(len, cnt, S(Z))~xs;
+
+len_list_(len, done, ct) >< [] =>
+        len~ct, done~[];
+len_list_(len, done, ct) >< x:xs => 
+        done~x:cnt, 
+        len_list_(len, cnt, S(ct)) ~ xs; 
+
+
+// ---------------------------------------
+// len (non-stream version)
+//   ret << len(list)
+// ---------------------------------------
+len(ret) >< [] => ret~Z;
+len(ret) >< x:xs => len_(ret, S(Z))~xs, Eraser~x;
+len_(ret, n) >< [] => ret~n;
+len_(ret, n) >< x:xs => len_(ret, S(n))~xs, Eraser~x;
+
+
+// ---------------------------------------
+// append (list1++list2)
+//   ret << append(list2, list1) 
+// ---------------------------------------
+append(r,a) >< [] => r~a;
+append(r,a) >< x:xs => r~x:w, append(w,a)~xs;
+
+
+
+
+/** 
+ * threat (stream version)
+ * check for (0,q) and (k, qpos[col=k]) where k=1...
+ * http://www.nct9.ne.jp/m_hiroi/func/haskell06.html
+     0 1 2    --> 
+    +-------------
+   1| . . . . . .
+   2| . . . -3. .  5 - 3 = 2
+   3| . . -2. . .  5 - 2 = 3
+   4| . -1. . . .  5 - 1 = 4
+   5| Q . . . . .  Q position is 5  
+   6| . +1. . . .  5 + 1 = 6
+   7| . . +2. . .  5 + 2 = 7
+   8| . . . +3. .  5 + 2 = 8
+    +-------------
+ *   r, board_done << threat(k,m, board)
+ *   return
+ *        r: True if threat conditions are satisfied
+ *     done: the same to `board'
+ */
+// fun threat k m [] = false
+//   | threat k m (x::xs) =
+//    if (k = x-m) orelse (k = x+m) then true
+//    else (threat (k+1) m xs);
+
+
+
+// r << diff(m,n)
+diff(r,m) >< Z => r~m;
+diff(r,m) >< S(n) => diff_S(r,n)~m;
+diff_S(r, n) >< Z => r~S(n);
+diff_S(r, n) >< S(m) => diff(r,m)~n;
+
+
+
+threat(r, done, k, q) >< [] =>
+	  r~False, done~[], Eraser~k, Eraser~q;
+
+threat(r, done, k, q) >< x:xs =>
+	  x1,x2 << Dup(x),
+	  q1,q2 << Dup(q),
+	  diff_xq << diff(x1,q1),
+	  k1,k2 << Dup(k),
+	  eq_ret << eq(k1, diff_xq),
+	  threat1(r, done, k2, q2 , x2:xs)~eq_ret;
+	  
+threat1(r, done, k, q, xxs) >< True =>
+	   r~True, done~xxs, Eraser~k, Eraser~q;
+	   
+threat1(r, done, k, q, xxs) >< False =>
+	   x1:xs1 ~ xxs,
+	   done~x1:cnt, threat(r, cnt, S(k), q)~xs1;
+	   
+
+// fun queen1 b n 0 = []
+//   | queen1 b n m =
+//     if (member m b) orelse (threat 1 m b) then (queen1 b n (m-1))
+//     else if (length b) = (n-1) then (m::b)::(queen1 b n (m-1))
+//         else (queen1 (m::b) n n) @ (queen1 b n (m-1));
+// fun queen n = queen1 n [] n;
+
+queen(ret, n) >< () =>
+	   n1, n2 << Dup(n),
+	   queen_(ret, [], n1)~n2;
+
+
+queen_(r, b, n) >< Z =>
+	  r~[], Eraser~b, Eraser~n;
+	  
+queen_(r, b, n) >< S(m) =>
+	  mem_ret, done_m, done_b << member(S(m), b),
+	  queen__chk_m_in_b(r, done_b, n, done_m)~mem_ret;	  
+
+
+dec(r)><Z => r~Z;
+dec(r)><S(n) => r~n;
+
+queen__chk_m_in_b(r, b, n, m) >< True =>
+     m1 << dec(m),
+     queen_(r, b, n)~m1;
+
+queen__chk_m_in_b(r, b, n, m) >< False =>
+     m1,m2 << Dup(m),
+     th_ret, done_b << threat(S(Z), m1, b), 
+     queen__chk_threat(r, done_b, n, m2)~th_ret;
+
+
+
+queen__chk_threat(r, b, n, m) >< True =>
+	m_dec << dec(m),
+        queen_(r, b, n)~m_dec;
+	
+queen__chk_threat(r, b, n, m) >< False =>
+        len_ret, done_b << len_list(b), 
+	n1,nn << Dup(n),
+	n_dec << dec(nn),
+	eq_ret << eq(len_ret, n_dec),
+	queen__chk_lastelem(r, done_b, n1, m) ~ eq_ret;
+
+
+
+queen__chk_lastelem(r,b,n, m) >< True =>
+        b1, b2 << Dup(b),
+	m1, mm << Dup(m),
+	m_dec << dec(mm),
+        r~(m1:b1):cnt, queen_(cnt, b2, n)~m_dec;
+
+queen__chk_lastelem(r,b,n, m) >< False =>
+        b1, b2 << Dup(b),
+        r << append(cnt2, cnt1),
+	n1, Dup(n2,n3) << Dup(n),
+	m1, mm << Dup(m),
+	m_dec << dec(mm),	
+        queen_(cnt1, m1:b1, n1)~n2, queen_(cnt2, b2, n3)~m_dec;
+
+
+
+// ----------------------------------------------------------
+// main
+// ----------------------------------------------------------
+n~S(S(S(S(S(S(S(S(S(S(Z)))))))))), // 10
+queen(ret,n)~(), len(count)~ret;
+prnat count;
\ No newline at end of file