| Some definitions of interest. |
|
his_num_rep | Def is_num_rep
Def == m: .  P:  
Def == m: .  ((P(zero_rep)) ( n: . (P(n))  (P(suc_rep(n)))))  (P(m)) |
| | Thm* is_num_rep (hind  hbool) |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
hrep_num | Def rep_num == n: . ncompose(suc_rep;n;zero_rep) |
| | Thm* rep_num (hnum  hind) |
|
hzero_rep | Def zero_rep == @x: . ( y: . x = suc_rep(y) ) |
| | Thm* zero_rep hind |
|
hsuc_rep | Def suc_rep == x: . (@f:   . (one_one( ; ;f) & onto( ; ;f)))(x) |
| | Thm* suc_rep (hind  hind) |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
| | Thm* S |
|
ncompose | Def ncompose(f;n;x) == if n= 0 then x else f(ncompose(f;n-1;x)) fi (recursive) |
| | Thm* 'a:Type, n: , x:'a, f:('a 'a). ncompose(f;n;x) 'a |