(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
2
1.
a
:
2.
(
a
~ 1)
3.
b
:
.
b
|
a
(
b
~ 1)
(
b
~
a
)
a
= 0
By:
Witness3 2 THEN (Analyze 0)
Generated subgoal:
1
3. 2 |
a
(2 ~ 1)
(2 ~
a
)
4.
a
= 0
False
3
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)
a = 0
(a ~ 1)
b:. b | a (b ~ 1) (b ~ a)
a = 0 (2 ~ 1) (2 ~ a)
False
