nat : type.				%name nat X.
z : nat.
s : nat -> nat.

nt : nat -> type.			%name nt N.
nt_z : nt z.
nt_s : nt (s X) <- nt X.

plus : nat -> nat -> nat -> type.	%name plus P.
p_z : plus z Y Y.
p_s : plus (s X) Y (s Z)
       <- plus X Y Z.

acker : nat -> nat -> nat -> type.
%mode acker +X +Y -Z.

a_1   : acker z Y (s Y).
a_2   : acker (s X) z Z 
	 <- acker X (s z) Z.
a_3   : acker (s X) (s Y) Z
	 <- acker (s X) Y Z'
	 <- acker X Z' Z.

%worlds () (acker _ _ _).
%compile acker.

arg1 = (s (s (s z))).
arg2 = (s (s (s (s (s z))))).

% query 1 1  (acker arg1 arg2 Z).

% fquery (acker arg1 arg2 Z).