(2steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable
rel
star
1
1.
n
:
2.
R
:
n
n
Prop
3.
i
,
j
:
n
. Dec(
i
R
j
)
4.
i
:
n
5.
j
:
n
Dec(
i
(
R
^*)
j
)
By:
RWO
Thm*
n
:
,
R
:(
n
n
Prop),
x
,
y
:
n
. (
x
(
R
^*)
y
)
(
k
:
(
n
+1).
x
R
^
k
y
) 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
i,j:
Dec(i (R^*) j)
(
k:
