EXISTS

existential quantifier
Major Section:  DEFUN-SK

The symbol exists (in the ACL2 package) represents existential quantification in the context of a defun-sk form. See defun-sk and see forall.

See quantifiers for an example illustrating how the use of recursion, rather than explicit quantification with defun-sk, may be preferable.