Nuprl - mb_nat Citations of bool

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def

== Unit+Unit

is mentioned by

Thm* k:, P:(k).
Thm* ((i:k. P(i)) 0<search(k;P))
Thm* & (0<search(k;P) P(search(k;P)-1) & (j:k. j<search(k;P)-1 P(j))) [search_property]

Thm* k:, f,g:(k), p:(k).
Thm* sum(if p(i) f(i)+g(i) else f(i) fi | i < k)
Thm* =
Thm* sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k) [sum-ite]

In prior sections: bool 1 list 1 rel 1 sqequal 1

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb nat Sections MarkB generic Doc

Thm* k:, P:(k). Thm* ((i:k. P(i)) 0<search(k;P)) Thm* & (0<search(k;P) P(search(k;P)-1) & (j:k. j<search(k;P)-1 P(j)))	[search_property]
Thm* k:, f,g:(k), p:(k). Thm* sum(if p(i) f(i)+g(i) else f(i) fi \| i < k) Thm* = Thm* sum(f(i) \| i < k)+sum(if p(i) g(i) else 0 fi \| i < k)	[sum-ite]