Download VeriFun User Guide

Quantifications and Lemmas
A closed quantification all x1:sort1,...,xn:sortn TERM is true iff the
value of the term TERM‘, obtained from TERM by substituting values for
the universally quantified variables xi, is true no matter which values
are substituted for the variables.
The semantics of closed quantifications respect the interpretation of the
data structures and procedures and is formally defined by:
A closed quantification
all x1:sort1,...,xn:sortn TERM is true
↔
eval(TERM[x1/q1,...,xn/qn]) = true for all q1,...,qn∈Val ,
where TERM[x1/q1,...,xn/qn] is obtained from TERM by replacing the
variables xi in TERM with the values qi of sort sorti.
A lemma lemma LEM <= BODY is true iff BODY is true.
X
The purpose of eriFun is to verify the truth of a lemma by computing a
proof for it.
12