Nuprl - Proof: eval factorization one b

PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eval factorization one b

a:{2...}, b:

, f:({a..b

}

).

{a..b

}(f) = 1

(

i:{a..b

}. 0<f(i))

By:	Rewrite by Thm* Q:(TProp). (x:T. Q(x)) (x:T. Q(x)) ...a THEN SimilarTo: Thm* a:{2...}, b:, f:({a..b}). Thm* {a..b}(f) = 1 (i:{a..b}. f(i) = 0) ...

Generated subgoals:

None

About:

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

PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc