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

isAlways(cond)

isAlways(cond,Name,Value)

Description

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).

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

Examples

Test Conditions

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

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

ans =
  logical
   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 =
  logical
   1

isAlways returns logical 1 (true) indicating that the equation 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 =
  logical
   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 =
  logical
   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: Unable to prove 'x <= 2*x'.
ans =
  logical
   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 =
  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 this 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)
isAlways(2*x < x)

ans =
  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.

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 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 condition

falseWithWarning (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.
false	On undecidable inputs, return logical 0 (false).
true	On undecidable inputs, return logical 1 (true).
error	On undecidable inputs, return an error.