To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Exercise 1

Try to define a next function over 'I_n that correspond to the successor function over the natural plus the special case that n -1 is mapped to zero

Exercise 2

Show that injectivity is decidable for a function f : aT -> rT with aT a finite

Exercise 3

Build a function that maps an element of an ordinal to another element of the same ordinal with a p subtracted from it.

Exercise 4

Try to formalize the following problem

Given a parking where the boolean indicates if the slot is occupied or not

Number of cars at line i

Number of cars at column j

Show that if 0 < n there is always two lines, or two columns, or a column and a line that have the same numbers of cars

Exercise 5

Prove the following state by induction and by following Gauss proof.

Exercise 6

Exercise 7

Exercise 8

Prove the following state by induction and by using a similar trick as for Gauss noticing that n ^ 3 = n * (n ^ 2)

Exercise 9

Prove the following statement using only big operator theorems. big_cat_nat, big_nat_cond, big_mkcondl, big1

Exercise 10

building a monoid law