n then 0 else m-n fi n then 0 else m-n fi is mentioned by
 m,n,x: . nnsub(m;n) = x   m = n+x   m n & x0 | [sub_right_eq] |
| m,n,x:. m = nnsub(n;x) m+x = n m0 & nx | [sub_left_eq] |
| m,n,x:. x<nnsub(m;n) n+x<m | [sub_right_greater] |
| m,n,x:. nnsub(n;x)<m n<m+x & 0<m | [sub_left_greater] |
| m,n,x:. xnnsub(m;n) n+xm x0 | [sub_right_greater_eq] |
| m,n,x:. nnsub(n;x)m nm+x | [sub_left_greater_eq] |
| m,n,x:. nnsub(m;n)<x m<n+x & 0<x | [sub_right_less] |
| m,n,x:. m<nnsub(n;x) m+x<n | [sub_left_less] |
| m,n,x:. nnsub(m;n)x mn+x | [sub_right_less_eq] |
| m,n,x:. mnnsub(n;x) m+xn m0 | [sub_left_less_eq] |
| m,n:. nnsub(m;n)+1 = if mn then 0+1 else nnsub(m+1;n) fi | [sub_left_suc] |
| m,n,x:. nnsub(nnsub(m;n);x) = nnsub(m;n+x) | [sub_right_sub] |
| m,n,x:. nnsub(m;nnsub(n;x)) = if nx then m else nnsub(m+x;n) fi | [sub_left_sub] |
| m,n,x:. nnsub(m;n)+x = if mn then x else nnsub(m+x;n) fi | [sub_right_add] |
| m,n,x:. m+nnsub(n;x) = if nx then m else nnsub(m+n;x) fi | [sub_left_add] |
In prior sections: hol arithmetic 1 hol arithmetic 4
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html