PrintForm
Definitions
Lemmas
hol
arithmetic
4
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mult
exp
mono
x
,
q
,
n
,
m
:
.
n
exp(
q
+1;
x
) =
m
exp(
q
+1;
x
)
n
=
m
By:
RewriteOfThm Thm:
hmult
exp
mono
(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
4
Sections
HOLlib
Doc
x,q,n,m:
. n
exp(q+1;x) = mexp(q+1;x) 
n = m x,q,n,m:. nexp(q+1;x) = mexp(q+1;x) n = m
