Goal of exercise
 Show the expressive power of PVS equality and higher order logic;
 Give a hint on how PVS kernel could be reduced by building quantification on equality;
 Learn more on importing theory instances.
Exercise
Define FORALL in terms of equality (=). The universal quantifier will be defined as a function of one argument of the form:
each(P: [T > bool]): bool = (P = ???)
Note that we cannot overload FORALL definition, and thus choose a different name, each, for lexical reasons: this is also clearer!
Then prove
each_forall: THEOREM (FORALL (P: [T > bool]): each(P) = (FORALL (x: T): P(x)))
each_each: COROLLARY each((LAMBDA (P: [T > bool]): each(P) = (FORALL (x: T): P(x))))
Step by step
 Create an each theory in a new ~login/pvs/forall/ directory (use Metax newpvsfile command to create this new theory) and define each function as specified above in the each theory. What are the parameters of each theory?
 Introduce and prove above each_forall theorem;
 Try to introduce each_each corollary in each theory: is it possible? How can you circumvent the difficulty?
 Finally prove each_each corollary.
DO NOT IMMEDIATELY LOOK AT solutions
