Nuprl - Proof: eval factorization pluck 1

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

1. a :

2. b :

3. f : {a..b

}

4. z : {a..b

}
5. 0<f(z)

{a..b

}(f) = z

{a..b

}(reduce_factorization(f; z))

By:	Let (X = reduce_factorization(f; z)) THEN Rewrite by Thm* a,b:, j:{a..b}. {a..b}(trivial_factorization(j)) = j Using:[j:= z] THEN Rewrite by Hyp:7

Generated subgoal:

1 6. X : {a..b}
7. X = reduce_factorization(f; z)
  {a..b}(f)
  =
  {a..b}(trivial_factorization(z)){a..b}(reduce_factorization(f; z))
5 steps

About:

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