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
inside your browser and (edits are also saved when you close the window). Finally you can the file for offline editing.
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
Show that injectivity is decidable for a function f : aT -> rT with aT a finite
Build a function that maps an element of an ordinal to another element of the same ordinal with a p subtracted from it.
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
Prove the following state by induction and by following Gauss proof.
Prove the following state by induction and by using a similar trick as for Gauss noticing that n ^ 3 = n * (n ^ 2)
Prove the following statement using only big operator theorems. big_cat_nat, big_nat_cond, big_mkcondl, big1
building a monoid law