m,n:
. nnsub(m;n)+1 = if m
n then 0+1 else nnsub(m+1;n) fi Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. equal
Thm* (
m:hnum. (n:hnum. (suc(sub(m,n))
Thm* (
m:hnum. (n:hnum. ,cond(le(m,n),suc(0),sub(suc(m),n)))))| Theorem | Name |
| m,n:. nnsub(m;n)+1 = if mn then 0+1 else nnsub(m+1;n) fi | [sub_left_suc] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. equal
Thm* ( m:hnum. (n:hnum. (suc(sub(m,n))
Thm* ( m:hnum. (n:hnum. ,cond(le(m,n),suc(0),sub(suc(m),n))))) | [hsub_left_suc] |