(4steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
mset
c
is
prime
f
1
1
1
1.
f
: Prime
2.
b
:
3.
i
: {2..
b
}
4. 0<prime_mset_complete(
f
)(
i
)
5.
prime(
i
)
prime(
i
)
By:
HypsImpossibleBy
Inst:
Thm*
f
:(Prime
),
x
:
.
prime(
x
)
prime_mset_complete(
f
)(
x
) = 0
Using:[
f
|
i
]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
}
prime(i)
prime(i)
f:(Prime
prime_mset_complete(f)(x) = 0
