% plus with meta level check (error if not an integer; beyond FOL)

plus_t(X,Y,Z) :- nonvar(X), nonvar(Y), Z is X+Y.

plus_t(X,Y,Z) :- nonvar(X), nonvar(Z), Y is Z-X.

plus_t(X,Y,Z) :- nonvar(Y), nonvar(Z), X is Z-Y.


% plus with type check (fails if not an integer; within FOL)
constant(X) :- atomic(X).

% ground(Term)
% Term is a ground term

ground_n(Term) :-
	nonvar(Term), constant(Term).

ground_n(Term) :-
	nonvar(Term),
	compound(Term),
	functor(Term,_,N),
	ground(N,Term).

ground(N,Term) :-
	N>0,
	arg(N,Term,Arg),
	ground(Arg),
	N1 is N-1,
	ground(N1,Term).

ground(0,_).


