(6steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eval trivial factorization 1 1 1

1. a : 
2. b : 
3. j : {a..b}
4. trivial_factorization(j)(j) = 1
  ( i:{a..j}. i0)j1( i:{j+1..b}. i0) = j


By: Compute i0 * 1 THEN Rewrite by Thm*  x:x1 = x


Generated subgoal:

1   ( i:{a..j}. 1)j( i:{j+1..b}. 1) = j
2 steps

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

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