:- module(_,_).

% Example application of comparing non-ground terms
% (use of ==/2, \==/2, @>/2, ...)
% subterm_ng(Sub,Term): Sub is a strict subterm of Term
% (does not instantiate variables)

subterm_ng(Sub,Term) :- % a) A term is a subterm of another 
    Sub == Term.        %    if they are identical.
subterm_ng(Sub,Term) :- % b) The arguments are also subterms:
    nonvar(Term),       %    Check Term not a free variable
    functor(Term,_F,N), %    N is number of arguments of Term
    n_to_one(N, J),     %    J is a natural between N and 1
    arg(J,Term,Arg),    %    Arg is the J-th argument of Term
    subterm_ng(Sub,Arg).%    Sub are the subterms of Arg

n_to_one(N, N) :- N > 0.
n_to_one(N, X) :- N > 1, N1 is N-1, n_to_one(N1, X).

% Compare to subterm version with =/2 instead of ==/2 (below)

% Try (asking also for other solutions):
% ?- subterm_ng( f(a), g(b,f(a)) ).
% ?- subterm(    f(a), g(b,f(a)) ).
% ?- subterm_ng( f(b), g(b,f(a)) ).
% ?- subterm(    f(b), g(b,f(a)) ).
% ?- subterm_ng( g(b,f(a)), g(b,f(a)) ).
% ?- subterm(    g(b,f(a)), g(b,f(a)) ).
% ?- subterm_ng( X, g(b,f(a)) ).
% ?- subterm(    X, g(b,f(a)) ).
% ?- subterm_ng( f(X), g(b,f(a)) ).
% ?- subterm(    f(X), g(b,f(a)) ).
% ?- subterm_ng( f(a), g(b,f(X)) ).
% ?- subterm(    f(a), g(b,f(X)) ).
% ?- subterm_ng( f(X), g(b,f(X)) ).
% ?- subterm(    f(X), g(b,f(X)) ).
% ?- subterm_ng( X, g(X,f(a)) ).
% ?- subterm(    X, g(X,f(a)) ).

% Version using =/2:
subterm(Term,Term).  % a) A term is always a subterm of itself
subterm(Sub,Term):-  % b) The arguments are also subterms:
    nonvar(Term),    %    Check Term not a free variable
    functor(Term,_F,N),%  N is the number of arguments of Term
    n_to_one(N, J),  %    J is a natural between N and 1
    arg(J,Term,Arg), %    Arg is the J-th argument of Term
    subterm(Sub,Arg).%    Sub are the subterms of Arg