1. a : 
2. b : 
3. j : {a..b}
  ( i:{a..j}. itrivial_factorization(j)(i))
  jtrivial_factorization(j)(j)( i:{j+1..b}. itrivial_factorization(j)(i))
  =
  j

By:	Inst: Thm*  x,y:. x = y  trivial_factorization(x)(y) = 1   Using:[j | j] THEN Rewrite by Hyp:-1 THEN Rewrite by Thm*  x,y:. x  y  trivial_factorization(x)(y) = 0

1

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

3 steps

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