(35steps 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:
spanner-root-exists
1
2
2
1
1.
T
: Id
2.
to
: |
T
|
(IdLnk List)
3.
from
: |
T
|
(IdLnk List)
4.
f
: Edge(
T
)
5. bi-graph(
T
;
to
;
from
)
6.
i
,
j
:|
T
|.
6.
p
:Edge(
T
) List.
6.
lconnects(
p
;
i
;
j
) & (
q
:Edge(
T
) List. lconnects(
q
;
i
;
j
)
q
=
p
)
7.
L
: |
T
| List
8.
i
:|
T
|. (
i
L
)
9.
j
: |
T
|
10. bi-graph(
T
;
to
;
from
)
11. spanner(
f
;
T
;
to
;
from
)
12.
n
:
13.
p
:Edge(
T
) List. lpath(
p
)
||
p
||
n
14.
||to(
j
)|| = 0
15.
(
i
:|
T
|. spanner-root(
f
;
T
;
to
;
from
;
i
))
i
:|
T
|. spanner-root(
f
;
T
;
to
;
from
;
i
)
By:
Assert False THEN Unfold `spanner-root` -1
THEN
Assert (
i
:|
T
|. (
l
to(
i
).
f
(
l
)))
Generated subgoals:
1
15.
(
i
:|
T
|.
l
:Edge(
T
). (
l
to(
i
))
f
(
l
))
i
:|
T
|. (
l
to(
i
).
f
(
l
))
3
steps
2
15.
(
i
:|
T
|.
l
:Edge(
T
). (
l
to(
i
))
f
(
l
))
16.
i
:|
T
|. (
l
to(
i
).
f
(
l
))
False
22
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(35steps total)
PrintForm
Definitions
Lemmas
mb
event
system
7
Sections
EventSystems
Doc