(46steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
num
iso
3
1.
x
:
2. is_num_rep(
x
)
x'
:
.
x
= rep_num(
x'
)
By:
Unab [`his_num_rep`] THEN Simp THEN StrongAuto
Generated subgoal:
1
2.
P
:(
).
P
(zero_rep) & (
n
:
.
P
(
n
)
P
(suc_rep(
n
)))
P
(
x
)
x'
:
.
x
= rep_num(
x'
)
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(46steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
x':. x = rep_num(x') 
x':. x = rep_num(x') 
P:(
). P(zero_rep) & (n:. P(n) 
P(suc_rep(n))) P(x)
x':. x = rep_num(x') 
