ForAll(name: String, bound: Formula, target: Formula)
First-order forall operator. Specifies that for all states in bound substituted for name, the target formula is valid at inspected state.
Note that (forall x in A : B)
is semantically equivalent to (forall x : ((at x: A) -> B))
.
However, we allow the in
syntax because it is much more readable and can yield interesting
performance optimisations.
Warning: name must usually be a free name (not assigned yet).