Nuprl - Proof: eval factorization pluck 1 1 1

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

1. a :

2. b :

3. f : {a..b

}

4. z : {a..b

}
5. 0<f(z)
6. X : {a..b

}

7. X = reduce_factorization(f; z)

{a..b

}(f)

{a..b

}(

i.trivial_factorization(z)(i)+reduce_factorization(f; z)(i))

By:

Analyze

Generated subgoal:

1   f
  =
  (i.trivial_factorization(z)(i)+reduce_factorization(f; z)(i))
   {a..b}
3 steps

About:

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