PrintForm
Definitions
Lemmas
hol
arithmetic
3
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
add
clauses
n
,
m
:
. 0+
m
=
m
&
m
+0 =
m
&
m
+1+
n
=
m
+
n
+1
&
m
+
n
+1 =
m
+
n
+1
By:
RewriteOfThm Thm: hadd_clauses (SimpsetC [`hol_to_nuprl`;`bequal`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
arithmetic
3
Sections
HOLlib
Doc
n,m:
. 0+m = m 
& m+0 = m & m+1+n = m+n+1 & m+n+1 = m+n+1 n,m:. 0+m = m & m+0 = m & m+1+n = m+n+1 & m+n+1 = m+n+1 
