PVS‎ > ‎exercises‎ > ‎

### {1, 2, 3}

 GoalLearn how to create a new theory from scratch;Get familiar with the "sets as predicates" important concept for typed higher order logics such as PVS;Learn from looking at PVS prelude (Meta-x view-prelude-file);Learn how to map your proof idea into a PVS proof scenario.Step by step Start PVS (if necessary) under your ~login/pvs/intro/ context;Create a new theory named s123 using Meta-x new-pvs-file PVS command;Erase unuseful comments, and type requested definitions and lemmas, so as to obtain:s123: THEORY   BEGIN     s12?(n: nat): bool       = n = 1  OR  n = 2  ;     s123?(n: nat): bool       = n = 1  OR  n = 2  OR  n = 3 ;     s12_subset_of_s123: LEMMA       subset?(s12?, s123?)     s12_differs_from_s123: LEMMA       s12? /= s123?     s312?: [nat -> bool]       = (LAMBDA (n: nat): n = 3  OR  n = 1  OR n = 2)     s312_equals_s123: LEMMA       s312? = s123?   END s123Try to type check the theory, using Meta-x tc PVS command; does it correctly type check?Try proving each lemma using Meta-x prove PVS command while the cursor is within the lemma.Hint: proof of the first lemma requires using EXPAND command on each function you see, in order to apply the definition of the function, FLATTEN, SKOLEM and PROP commands;  proof of the second lemma requires EXPAND (sometimes with the :IF-SIMPLIFIES T option), CASE (to use a lemma on the fly), and ASSERT.Don't look at solution