| Who Cites ndiff? |
|
ndiff | Def a -- b == imax(a-b;0) |
| | Thm* a,b:. (a -- b) |
|
imax | Def imax(a;b) == if ab b else a fi |
| | Thm* a,b:. imax(a;b) |
|
le_int | Def ij == j<i |
| | Thm* i,j:. (ij) |
|
lt_int | Def i<j == if i<j true ; false fi |
| | Thm* i,j:. (i<j) |
|
bnot | Def b == if b false else true fi |
| | Thm* b:. b |