isAlways

Determine if symbolic conditions are true for all values of variables

isAlways issues a warning when returning false for undecidable inputs. To suppress the warning, set the Unknown option to false by using isAlways(cond,Unknown="false"). For details, see Handle Output for Undecidable Conditions.

Syntax

tf = isAlways(cond)

tf = isAlways(cond,Unknown=option)

Description

tf = isAlways(cond) checks if the conditions in cond are always mathematically true and returns an array of logical values. isAlways checks if cond holds true for all possible values of the symbolic variables in cond including all assumptions on the variables. If an element in cond is always true, then the corresponding element in tf is a logical 1 (true). Otherwise, the corresponding element in tf is a logical 0 (false).

tf = isAlways(cond,Unknown=option) returns the output of undecidable conditions as specified by option.

Examples

Test Symbolic Conditions

Check if an inequality is true for all values of its variable.

syms x
tf = isAlways(abs(x) >= 0)

tf = logical
   1

isAlways returns logical 1 (true), indicating that the inequality abs(x) >= 0 is true for all values of x.

Check if an equation is true for all values of its variable.

tf = isAlways(sin(x)^2 + cos(x)^2 == 1)

tf = logical
   1

isAlways returns logical 1 (true), indicating that the equation sin(x)^2 + cos(x)^2 == 1 is true for all values of x.

Test If One of Several Conditions Holds True

Check if at least one of two conditions holds true. To check if at least one of several conditions is true, combine them using the logical operator or or its shortcut |.

syms x
tf = isAlways(sin(x)^2 + cos(x)^2 == 1 | x^2 > 0)

tf = logical
   1

Check if both conditions hold true. To check if several conditions are true, combine them using the logical operator and or its shortcut &.

tf = isAlways(sin(x)^2 + cos(x)^2 == 1 & abs(x) > 2*abs(x))

tf = logical
   0

For multiple conditions, you can also represent the conditions as a symbolic array.

cond = [sin(x)^2 + cos(x)^2 == 1; abs(x) > 2*abs(x)]

cond = 
$$\left(\begin{array}{c}{\cos \left(x\right)}^2+{\sin \left(x\right)}^2=1\\ 2\hspace{0.17em}\left|x\right|<\left|x\right|\end{array}\right)$$

tf = isAlways(cond)

tf = 2x1 logical array

   1
   0

Handle Output for Undecidable Conditions

When isAlways cannot determine if a condition is true, it returns logical 0 (false) and issues a warning by default.

syms x
tf = isAlways(2*x >= x)

Warning: Unable to prove 'x <= 2*x'.

tf = logical
   0

To change this default behavior, use the Unknown name-value argument. For example, specify Unknown as "false" to suppress the warning and make isAlways return logical 0 (false) if it cannot determine whether the condition is true.

tf = isAlways(2*x >= x,Unknown="false")

tf = logical
   0

Instead of "false", you can also specify Unknown as "error" to return an error, and as "true" to return logical 1 (true).

Test Conditions with Assumptions

Check an inequality under the assumption that x is negative. When isAlways tests an equation or inequality, it takes into account assumptions on variables in that equation or inequality.

syms x
assume(x < 0)
tf = isAlways(2*x < x)

tf = logical
   1

For further computations, clear the assumption on x by recreating it using syms.

syms x

Input Arguments

cond — Condition to check

symbolic condition | vector of symbolic conditions | matrix of symbolic conditions | multidimensional array of symbolic conditions

Condition to check, specified as a symbolic condition, or a vector, matrix, or multidimensional array of symbolic conditions.

option — Return option for undecidable condition

"falseWithWarning" (default) | "false" | "true" | "error"

Return option for an undecidable condition, specified as one of these values:

"falseWithWarning" (default)	On undecidable inputs, return logical 0 (false) and a warning that the condition cannot be proven.
"false"	On undecidable inputs, return logical 0 (false).
"true"	On undecidable inputs, return logical 1 (true).
"error"	On undecidable inputs, return an error.

Version History

Introduced in R2012a