(2steps total)
PrintForm
Definitions
mb
event
system
7
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rnext-one-one
1
1.
R
: Id
2.
in
: |
R
|
IdLnk
3.
out
: |
R
|
IdLnk
4.
i
:|
R
|.
4.
R
(source(
in
(
i
))) &
R
(destination(
out
(
i
)))
4.
& source(
out
(
i
)) =
i
4. &
& destination(
in
(
i
)) =
i
4. &
&
in
(destination(
out
(
i
))) =
out
(
i
)
4. &
&
out
(source(
in
(
i
))) =
in
(
i
)
5.
i
,
j
:|
R
|.
k
:
.
x
.destination(
out
(
x
))^
k
(
i
) =
j
6. |
R
|
7.
i
: |
R
|
8.
j
: |
R
|
9. destination(
out
(
i
)) = destination(
out
(
j
))
10.
R
(source(
in
(
i
)))
11.
R
(destination(
out
(
i
)))
12. source(
out
(
i
)) =
i
13. destination(
in
(
i
)) =
i
14.
in
(destination(
out
(
i
))) =
out
(
i
)
15.
out
(source(
in
(
i
))) =
in
(
i
)
16.
R
(source(
in
(
j
)))
17.
R
(destination(
out
(
j
)))
18. source(
out
(
j
)) =
j
19. destination(
in
(
j
)) =
j
20.
in
(destination(
out
(
j
))) =
out
(
j
)
21.
out
(source(
in
(
j
))) =
in
(
j
)
22.
in
(destination(
out
(
i
))) =
in
(destination(
out
(
j
)))
23.
out
(
i
) =
out
(
j
)
24. source(
out
(
i
)) = source(
out
(
j
))
25.
i
=
j
i
=
j
By:
StrongHypSubst -1 0 THEN DVar `
j
' THEN Unfold `rset` 0 THEN Analyze
THEN
HypSubst -1 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
event
system
7
Sections
EventSystems
Doc