11.3.224 subsumes_term/2   ISO

Synopsis

subsumes_term(+General, +Specific)

True iff there is a substitution that makes General identical to Specific and that does not affect Specific. It does not bind any variables.

Arguments

General

any term.

Specific

any term.

Description

True iff there is a substitution that makes General identical to Specific and that does not affect Specific.

The predicate is determinate and either succeeds or fails. It never binds variables.

The predicate does not take any constraints, variable attributes, or blocked goals into account when determining whether a substitution exists. This can be seen in the last two examples.

Examples

| ?- subsumes_term(a, a).
yes

| ?- subsumes_term(f(X,Y), f(Z,Z)).
yes

| ?- subsumes_term(f(Z,Z), f(X,Y)).
no

| ?- subsumes_term(f(X,Y), f(Y,X)).
no

| ?- subsumes_term(g(X), g(f(X))).
no

| ?- subsumes_term(X, f(X)).
no

| ?- subsumes_term(X, Y), subsumes_term(Y, f(X)).
yes

| ?- when(nonvar(X), X=a), subsumes_term(X, b), X = a.
X = a ? 
yes

| ?- when(nonvar(X), X=a), subsumes_term(X, b), X = b.
no

Exceptions

None.

See Also

ref-lte-met-usu.