Type natnum []
  declare
  	constructors
  		null () -> natnum;
  		succ (natnum) -> natnum;
  	others
                  plus(natnum,natnum) -> natnum;
                  minus(natnum, natnum) -> natnum;
                  leq(natnum,natnum) -> bool;
  for all i,j in natnum;
  let
          plus(null(),j) = j;
          plus(succ(i),j) = succ(plus(i,j));
  
          leq(null(),j) = true;
          leq(succ(i), null()) = false;
          leq(succ(i), succ(j)) = leq(i,j);
  
          minus(i, null()) = i;
          minus(null() , succ(j)) = error;
          minus(succ(i), succ(j)) = minus(i,j);
  end
end natnum.