(7steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not
nat
occ
natfuns
1
1
1
1. (
) ~
2.
f
:
3. Inj(
;
;
f
)
4. Surj(
;
;
f
)
False
By:
Witness-1:
i
.
f
(
i
,
i
)+1
Generated subgoal:
1
5.
a
:
.
f
(
a
) = (
i
.
f
(
i
,
i
)+1)
False
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
) ~
; ; f)
; ; f)
False) ~
; ; f)
; ; f)
False
i.f(i,i)+1
a:. f(a) = (i.f(i,i)+1)
False
