Nuprl - Proof: can reduce composite factor

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A composite factor in a factorization can be reduced to power zero, leaving all larger factors' powers unchanged.

At: can reduce composite factor

k:{2...}, g:({2..k

}

), x,y:{2..k

}.

x

y<k

(

h:({2..k

}

).

(

{2..k

}(g) =

{2..k

}(h)

(& h(x

y) = 0

(& (

u:{2..k

}. x

y<u

h(u) = g(u)))

By:	Guarding (x:<type>. <prop>) Auto

Generated subgoal:

1 1. k : {2...}
2. g : {2..k}
  x,y:{2..k}.
  xy<k

  (h:({2..k}).
  ({2..k}(g) = {2..k}(h)
  (& h(xy) = 0
  (& (u:{2..k}. xy<u  h(u) = g(u)))
11 steps

About:

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

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