NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def
sexprCdr(
s
) == Case of
s
: Inj(
x
)
Inj(
x
) ; Cons(
s1
;
s2
)
s2
is mentioned by
Thm*
s
:Sexpr(
A
). Size(
s
)
1
Size(sexprCdr(
s
))<Size(
s
)
[sfa_doc_sexprcdrsize]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NuprlPrimitives
Sections
NuprlLIB
Doc
Inj(x) ; Cons(s1;s2) s2 Inj(x) ; Cons(s1;s2) s2
s:Sexpr(A). Size(s) 
1 
Size(sexprCdr(s))<Size(s)