(25steps 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-rprev
1
1
2
2
1.
R
: Id
2.
in
: |
R
|
IdLnk
3.
out
: |
R
|
IdLnk
4.
i
: |
R
|
5.
j
: |
R
|
6. ring(
R
;
in
;
out
)
7.
i
= p(
j
)
8.
x
.n(
x
)^d(
i
;
j
)(
i
) =
j
9.
k
:
.
k
<d(
i
;
j
)
x
.n(
x
)^
k
(
i
) =
j
10.
x
.n(
x
)^d(
i
;p(
j
))(
i
) = p(
j
)
11.
k
:
.
k
<d(
i
;p(
j
))
x
.n(
x
)^
k
(
i
) = p(
j
)
12. n(p(
j
)) =
j
13.
x
.n(
x
)^d(
i
;p(
j
))+1(
i
) =
j
d(
i
;p(
j
)) = d(
i
;
j
)-1
By:
Assert (d(
i
;
j
)
d(
i
;p(
j
))+1)
Generated subgoals:
1
d(
i
;
j
)
d(
i
;p(
j
))+1
2
steps
2
14. d(
i
;
j
)
d(
i
;p(
j
))+1
d(
i
;p(
j
)) = d(
i
;
j
)-1
15
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(25steps total)
PrintForm
Definitions
Lemmas
mb
event
system
7
Sections
EventSystems
Doc