logo

Context: proveit.logic.boolean.quantification.universal

Universal quantification is a general expression about everything (Forall: $\forall$).
The Forall Expression derives from proveit._generic_.operation_over_instances.OperationOverInstances. As such, it has instance variables (instanceVars) with an instance expression (instanceExpr) and may be restricted to a domain and have zero or more conditions. For example $\forall_{x, y \in S~|~Q(x),~R(x, y)} P(x, y)$ means that $P(x, y)$ is TRUE for all occurrences of $x$ and $y$ in domain $S$ given that the conditions $Q(x)$ and $R(x, y)$ are satisfied. The conditions may be any Expressions involving the instance variables.

In [1]:
import proveit
%context