hol
arithmetic
4
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
a
,
c
:
. nnsub(
a
+
c
;
c
) =
a
[add_sub]
cites the following:
Thm*
all(
a
:hnum. all(
c
:hnum. equal(sub(add(
a
,
c
),
c
),
a
)))
[hadd_sub]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
arithmetic
4
Sections
HOLlib
Doc
a,c:
. nnsub(a+c;c) = a
a:hnum. all(c:hnum. equal(sub(add(a,c),c),a)))a,c:. nnsub(a+c;c) = aa:hnum. all(c:hnum. equal(sub(add(a,c),c),a)))