Object Substitution

Objects accessible from the current scope can be substituted for an object bound by a universal quantifier using object substitution. Object substitution results in a new sentence expression value without the universal quantifier.

Syntax

[sentence expression]([object expression], [object expression], ...)

Object substitution begins with a parent expression evaluating to a sentence value. The sentence referenced by the sentence value must begin with a top level universal quantifier. In other words, the sentence must be of the form *X(P(X)) for some sentence P with one unbound object. Following the parent expression is ( and one or more expressions evaluating to object expression values. The ( is matched with a closing ).

For each object expression value, a top-level universal quantifier is peeled from the parent expression sentence, and the unbound variable is replaced with the object.

Object substitution can only be applied when the parent expression evaluates to a sentence value with no unbound variables or predicates. If the parent expression evaluates to a verified sentence value, then the object substitution evaluates to a verified sentence value. Otherwise, the object substitution evaluates to an unverified sentence value. In any case, the new sentence value has no bound variables or predicates.

Examples

If = and <= are relations, S and T are objects, subset_equal is a sentence variable storing the following sentence:

*X*Y(X <= Y & Y <= X -> X = Y)

Then the expression:

subset_equal(S, T)

Evaluates to the sentence value:

S <= T & T <= S -> S = T

If the sentence stored by subset_equal is verified, then this sentence value is also verified, otherwise it is unverified.