(16steps total)
PrintForm
Definitions
Lemmas
mb
event
system
7
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rdist-property
1
1
2
1
1
1.
R
: Id
2.
in
: |
R
|
IdLnk
3.
out
: |
R
|
IdLnk
4.
i
: |
R
|
5.
j
: |
R
|
6. ring(
R
;
in
;
out
)
7. (
k
.
x
.n(
x
)^
k
+1(
i
) =
j
)
8.
n
:
.
x
.n(
x
)^
n
+1(
i
) =
j
9.
x
.n(
x
)^mu(
k
.
x
.n(
x
)^
k
+1(
i
) =
j
)+1(
i
) =
j
9.
& (
i@0
:
.
i@0
<mu(
k
.
x
.n(
x
)^
k
+1(
i
) =
j
)
x
.n(
x
)^
i@0
+1(
i
) =
j
)
10. mu(
k
.
x
.n(
x
)^
k
+1(
i
) =
j
)
mu(
k
.
x
.n(
x
)^
k
+1(
i
) =
j
) ~ (d(
i
;
j
)-1)
By:
Unfold `rdist` 0 THEN GenConclAtAddr [1]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(16steps total)
PrintForm
Definitions
Lemmas
mb
event
system
7
Sections
EventSystems
Doc