(6steps 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:
prime
imp
atomic
a
:
. prime(
a
)
atomic(
a
)
By:
Unfolds [`prime`;`atomic`] 0
Generated subgoal:
1
1.
a
:
2.
a
= 0
3.
(
a
~ 1)
4.
b
,
c
:
.
a
|
b
c
a
|
b
a
|
c
reducible(
a
)
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
a:
. prime(a) 
atomic(a) a:. prime(a) atomic(a)
a = 0
(a ~ 1)
b,c:. a | b
c a | b 
a | c
reducible(a)
