Nuprl - Proof: eval factorization not one

(8steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

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

a:{2...}, b:

, f:({a..b

}

).

{a..b

}(f) = 1

(

i:{a..b

}.

f(i) = 0)

By:	Rewrite by Thm* a:{2...}, b:, f:({a..b}). Thm* {a..b}(f) = 1 (i:{a..b}. f(i) = 0) ...

Generated subgoals:

1 1. a : {2...}
2. b :
3. f : {a..b}
4. (i:{a..b}. f(i) = 0)
i:{a..b}. f(i) = 0
4 steps

2 1. a : {2...}
2. b :
3. f : {a..b}
4. i:{a..b}. f(i) = 0
(i:{a..b}. f(i) = 0)
3 steps

About:

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

(8steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc