(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.
f
: Prime
2.
b
:
3.
i
: {2..
b
}
4. 0<prime_mset_complete(
f
)(
i
)
prime(
i
)
By:
Decide: prime(
i
)
Generated subgoal:
1
5.
prime(
i
)
prime(
i
)
1
step
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)
