WhoCites
Definitions
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites prime
mset
complete?
prime_mset_complete
Def prime_mset_complete(
f
)(
x
) == if is_prime(
x
)
f
(
x
) else 0 fi
Thm*
f
:(Prime
). prime_mset_complete(
f
)
prime_decider
Def
is_prime(
x
) == prime_decider_exists{1:l}(
x
)
Thm*
x
:
. is_prime(
x
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
FTA
Sections
DiscrMathExt
Doc
f(x) else 0 fi
f:(Prime
). prime_mset_complete(f) 
x:
. is_prime(x) 
f(x) else 0 fif:(Prime). prime_mset_complete(f) x:. is_prime(x) 
