(22steps total)
Remark
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
char
3
1.
a
:
2.
(
a
~ 1)
3.
b
:
.
b
|
a
(
b
~ 1)
(
b
~
a
)
reducible(
a
)
By:
(Analyze 0) THEN (Unfold `reducible` -1) THEN ExRepD
Generated subgoal:
1
4.
b
:
5.
c
:
6.
(
b
~ 1)
7.
(
c
~ 1)
8.
a
=
b
c
False
9
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(22steps total)
Remark
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
(a ~ 1)
b:. b | a 
(b ~ 1) 
(b ~ a)
reducible(a)
(a ~ 1)
b:. b | a (b ~ 1) (b ~ a)
reducible(a)
(b ~ 1)
(c ~ 1)
c
False
