Thm* m,n: . ndiv(m;n)  | [ndiv_wf] |
Thm* m,n: . nmod(m;n)  | [nmod_wf] |
Thm* n: . n>0  odd(n) =  odd(n-1) | [odd_pos] |
Thm* n: . odd(n)  | [odd_wf] |
Thm* n: . n>0  even(n) =  even(n-1) | [even_pos] |
Thm* n: . even(n)  | [even_wf] |
Thm* n: . n>0  fact(n) = n fact(n-1) | [fact_pos] |
Thm* fact(0) = 1 | [fact_zero] |
Thm* n: . fact(n)  | [fact_wf] |
Thm* m,n: . n>0  exp(m;n) = m exp(m;n-1) | [exp_pos] |
Thm* m: . exp(m;0) = 1 | [exp_zero] |
Thm* m,n: . exp(m;n)  | [exp_wf] |
Thm* m,n: . m n  | [multiply_wf_nat] |
Thm* m,n: . nnsub(m;n)  | [nnsub_wf] |
Thm* m,n: . m n  nnsub(n;m) = n-m | [nnsub_nuprl] |
Thm* m,n: . m+n  | [add_wf_nat] |
Def div == m: . n: . ndiv(m;n) | [hdiv] |
Def mod == m: . n: . nmod(m;n) | [hmod] |
Def odd == n: . odd(n) | [hodd] |
Def even == n: . even(n) | [heven] |
Def fact == n: . fact(n) | [hfact] |
Def ge == m: . n: . n m | [hge] |
Def le == m: . n: . m n | [hle] |
Def gt == m: . n: . n< m | [hgt] |
Def exp == m: . n: . exp(m;n) | [hexp] |
Def mult == m: . n: . m n | [hmult] |
Def sub == m: . n: . nnsub(m;n) | [hsub] |
Def add == m: . n: . m+n | [hadd] |