Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line. Use ALT-(right-arrow) to go to the cursor. You can save your edits inside your browser and load them back. Finally, you can download your working copy of the file, e.g., for sending it to teachers.

Exercise 1:

  • Write a recursive function taking a natural number to a boolean value. That value is true iff the number if even

Exercise 2:

  • State and prove the following boolean formulas: b1 && (~~ b2 || b3) = (b1 && ~~ b2) || (b1 && b3)

Exercise 3 :

Prove Peirce's law using only the rewrite command.

  • Hint: use Search to find relevant lemmas about ==> and ~~
  • Hint: use the lemma that says (a || b) && a = a

When you are done, click the Download link at the top of the page and send us your homework by email: Assia.Mahboubi@inria.fr