Nuprl - Proof: reduce factorization bound

PrintForm Definitions FTA Sections DiscrMathExt Doc

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

a,b:

, f:({a..b

}

), j:{a..b

}.

0<f(j)

(

i:{a..b

}. reduce_factorization(f; j)(i)

f(i))

By:	Compute reduce_factorization(f; j)(i) * if i=j f(i)-1 else f(i) fi THEN SplitOnConclITE

Generated subgoals:

None

About:

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

PrintForm Definitions FTA Sections DiscrMathExt Doc