The verify(expr1, expr2, relation) and verify(expr1, expr2, relation(ver)) calling sequences return true if it can be determined that the relations expr1 and expr2 are equivalent, either by testing for equality or by using verify/ver.

Two equations or inequations are considered to satisfy a relation if the left-hand side minus the right-hand side of the first argument is related to either plus or minus the same construction for the second argument.

Two similar inequalities are considered to satisfy a relation if the left-hand side minus the right-hand side of the first argument is related to the left-hand side minus the right-hand side of the second argument.

The verification relation is symmetric and a verification relation(ver) is symmetric if and only if the verification ver is symmetric.

If either expr1 or expr2 is not of type relation, then false is returned.  If expr1 and expr2 are not both of type =, <, <=, or <>,  then false is returned.

$\mathrm{verify}\left(x^2-1=1\&comma;x^2=2\&comma;'\mathrm{relation}'\right)$

$\mathrm{true}$

$\mathrm{verify}\left(x^2=1\&comma;\left(x-1\right)\left(x+1\right)=0\&comma;'\mathrm{relation}'\right)$

$\mathrm{false}$

$\mathrm{verify}\left(x^2=1\&comma;\left(x-1\right)\left(x+1\right)=0\&comma;'\mathrm{relation}'\left('\mathrm{expand}'\right)\right)$

$\mathrm{true}$