module peano.

kind nat     type.
type z       nat.
type s       nat -> nat.

type numb    nat -> o.

numb z.
numb (s N) :- numb N.

type plus    nat -> nat -> nat -> o.

plus z N N.
plus (s N) M (s P) :- plus N M P.

type mult    nat -> nat -> nat -> o.

mult z N z.
mult (s N) M P :- mult N M Q, plus M Q P.

type fib     nat -> nat -> o.

fib z z.
fib (s z) (s z).
fib (s (s N)) F :-
  fib N F1,  fib (s N) F2,  plus F1 F2 F.

type sqfib   nat -> nat -> o.

sqfib N M :- fib N M, mult N N M.