(31steps 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:
bi-tree-diameter
T
:(Id
),
to
,
from
:(|
T
|
(IdLnk List)).
bi-tree(
T
;
to
;
from
)
(
n
:
.
p
:Edge(
T
) List. lpath(
p
)
||
p
||
n
)
By:
Auto
Generated subgoal:
1
1.
T
: Id
2.
to
: |
T
|
(IdLnk List)
3.
from
: |
T
|
(IdLnk List)
4. bi-tree(
T
;
to
;
from
)
n
:
.
p
:Edge(
T
) List. lpath(
p
)
||
p
||
n
30
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(31steps total)
PrintForm
Definitions
Lemmas
mb
event
system
7
Sections
EventSystems
Doc