다시 짜봤습니다:


Nat

{

    succ(n: Nat) = "s" * ''n'.

    zero() = "z".

}


List

{

    nil() = ".".

    cons(head: Nat, tail: List) = "." * 'head' * 'tail'.

}


Plus(Nat, Nat, Nat).

/ Plus(n, zero(), n).

Plus(i, j, k) / Plus(i, succ(j), succ(k)).


F(List, Nat).

/ F(".sz.", "z").

/ F(".sz.sz.", "sz").

F(cons(x, cons(y, z)), n), Plus(x, y, a) / F(cons(a, cons(x, cons(y, z))), succ(n)).


Main(Nat, Nat).

F(cons(x, _), n) / Main(n, x).


＜＜ Main("ssz", x).

＞＞ x = succ(succ(zero())).