(13steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iter prod zero iff factor zero 1 2

1. a : 
2. b:e:({a..b}).
2. ab  (( i:{a..b}. e(i)) = 0  (Or i:{a..b}. e(i) = 0))
3. b : 
4. e : {a..b}
  ( i:{a..b}. e(i)) = 0  (Or i:{a..b}. e(i) = 0)


By: Decide: ab


Generated subgoals:

1 5. ab
  ( i:{a..b}. e(i)) = 0  (Or i:{a..b}. e(i) = 0)

1 step
2 5. ab
  ( i:{a..b}. e(i)) = 0  (Or i:{a..b}. e(i) = 0)

2 steps

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

(13steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc