(13steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
atomic
imp
prime
a
:
. atomic(
a
)
prime(
a
)
By:
UnivCD
THEN
(FwdThru
Thm*
a
:
. atomic(
a
)
(
a
~ 1) & (
b
:
.
b
|
a
(
b
~ 1)
(
b
~
a
))
(
[-1])
Generated subgoal:
1
1.
a
:
2. atomic(
a
)
3.
(
a
~ 1) & (
b
:
.
b
|
a
(
b
~ 1)
(
b
~
a
))
prime(
a
)
12
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(13steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
a:
. atomic(a) 
prime(a) a:. atomic(a) prime(a)a:. atomic(a) 
(a ~ 1) & (b:. b | a (b ~ 1) 
(b ~ a))
(a ~ 1) & (b:. b | a (b ~ 1) (b ~ a))
prime(a)
