Nuprl - Proof: eval reduce factorization less 1 1

(4steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Search Doc

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eval reduce factorization less 1 1

1. a :

2. b :

3. f : {a..b

}

4. j : {a..b

}
5. 2

j
6. 0<f(j)

{a..b

}(reduce_factorization(f; j))<j

{a..b

}(reduce_factorization(f; j))

By:	BackThru: Thm* i:{2...}, j:{1...}. j<ij ...

Generated subgoal:

1 {a..b}(reduce_factorization(f; j)) {1...}
1 step

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(4steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Search Doc