isAlways

Check whether equation or inequality holds for all values of its variables

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

Syntax

Description

example

isAlways(cond) checks if the condition cond is valid for all possible values of the symbolic variables in cond. When verifying cond, the isAlways function considers all assumptions on the variables in cond. If the condition holds, isAlways returns logical 1 (true). Otherwise it returns logical 0 (false).

example

isAlways(cond,Name,Value) uses additional options specified by one or more Name,Value pair arguments.

Examples

Test a Condition

Check if this inequality is valid for all values of x.

syms x
isAlways(abs(x) >= 0)
ans =
     1

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

Check if this equation is valid for all values of x.

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

isAlways returns logical 1 (true) indicating that the inequality is valid for all values of x.

Test if One of Several Conditions Is Valid

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

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

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

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

Handle Output for Undecidable Conditions

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

syms x
isAlways(2*x >= x)
Warning: Cannot prove 'x <= 2*x'.
ans =
     0

To change this default behavior, use Unknown. For example, specify Unknown as false to suppress the warning and make isAlways return logical 0 (false) if it cannot determine the validity of the condition.

isAlways(2*x >= x,'Unknown','false')
ans =
     0

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

Test a Condition with Assumptions

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

syms x
assume(x < 0)
isAlways(2*x < x)
ans =
     1

For further computations, clear the assumption on x.

syms x clear

Input Arguments

expand all

cond — Condition to checksymbolic 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.

Name-Value Pair Arguments

Specify optional comma-separated pairs of Name,Value arguments. Name is the argument name and Value is the corresponding value. Name must appear inside single quotes (' '). You can specify several name and value pair arguments in any order as Name1,Value1,...,NameN,ValueN.

Example: isAlways(cond,'Unknown',true) makes isAlways return logical 1 (true) when the specified condition cannot be decided.

'Unknown' — Return value for undecidable conditionfalseWithWarning (default) | false | true | error

Return value for an undecidable condition, specified as the comma-separated pair of 'Unknown' and one of these values.

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

Was this topic helpful?