trivial

The built-in function trivial accepts one sentence expression value, and if the sentence is trivially true, returns the same sentence value except verified.

Syntax

trivial([sentence argument expression])

Behavior

The argument must be an expression evaluating to a sentence expression value with no unbound objects or predicates. If the argument sentence is not trivially true, then an error is raised. Otherwise, the output is a verified sentence value storing the same sentence as the argument.

Note

Anything that can be proven using the trivial built-in command can be proven without it. trivial is usually used to save the programmer the time of having to prove simple statements that are obviously true. Due to the limited scope of what is defined as trivially true, there are other sentences that are just as obvious but must be proven manually.

Examples

If in is a relation, the following expression:

trivial(<: *X*Y(X in Y -> ~~X in Y)>)

Returns the following verified sentence value:

*X*Y(X in Y -> ~~X in Y)