Nuprl - mb_nat Citations of decidable

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Dec(P) == P

is mentioned by

Thm* k,n:, R:(nnProp). (i,j:n. Dec(i R j)) (i,j:n. Dec(i R^k j)) [decidable__rel_exp]

Thm* m:, P:(mProp).
Thm* (i:m. Dec(P(i)))
Thm*
Thm* (n,k:, f:(nm), g:(km).
Thm* (increasing(f;n)
Thm* (& increasing(g;k)
Thm* (& (i:n. P(f(i)))
Thm* (& (j:k. P(g(j)))
Thm* (& (i:m. (j:n. i = f(j)) (j:k. i = g(j)))) [increasing_split]

In prior sections: core int 1 bool 1 int 2 rel 1 mb basic

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,n:, R:(nnProp). (i,j:n. Dec(i R j)) (i,j:n. Dec(i R^k j))	[decidable__rel_exp]
Thm* m:, P:(mProp). Thm* (i:m. Dec(P(i))) Thm* Thm* (n,k:, f:(nm), g:(km). Thm* (increasing(f;n) Thm* (& increasing(g;k) Thm* (& (i:n. P(f(i))) Thm* (& (j:k. P(g(j))) Thm* (& (i:m. (j:n. i = f(j)) (j:k. i = g(j))))	[increasing_split]