Nuprl - Proof: eval reduce factorization less

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

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

a:

, b:

, f:({a..b

}

), j:{a..b

}.

2

j

0<f(j)

{a..b

}(reduce_factorization(f; j))<

{a..b

}(f)

By:

Auto

Generated subgoal:

1 1. a :
2. b :
3. f : {a..b}
4. j : {a..b}
5. 2j
6. 0<f(j)
{a..b}(reduce_factorization(f; j))<{a..b}(f)
3 steps

About:

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

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