mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
n
:
. ||upto(
n
)|| ~
n
[length_upto]
cites the following:
Thm*
as
,
bs
:
T
List. ||
as
@
bs
|| = ||
as
||+||
bs
||
[length_append]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
1
Sections
EventSystems
Doc
n:
. ||upto(n)|| ~ nas,bs:T List. ||as @ bs|| = ||as||+||bs|| 
n:. ||upto(n)|| ~ nas,bs:T List. ||as @ bs|| = ||as||+||bs||