k:{2...}, g:({2..k
}
), x,y:{2..k}.
Thm* x
y<k
Thm*
Thm* (
h:({2..k}).
Thm* (
{2..k}(g) = {2..k}(h)
Thm* (& h(x
y) = 0
Thm* (& (
u:{2..k}. xy<u h(u) = g(u)))i:{2...}, j:{1...}. j<ijk:{2...}, g:({2..k}), x,y:{2..k}.
Thm* x
y<k
Thm*
Thm* x<y
Thm*
Thm*
{2..k}(g) = {2..k}(split_factor2(g; x; y))
Thm* & split_factor2(g; x; y)(x
y) = 0
Thm* & (
u:{2..k}. xy<u split_factor2(g; x; y)(u) = g(u))k:{2...}, g:({2..k}), x:{2..k}.
Thm* x
x<k
Thm*
Thm*
{2..k}(g) = {2..k}(split_factor1(g; x))
Thm* & split_factor1(g; x)(x
x) = 0
Thm* & (
u:{2..k}. xx<u split_factor1(g; x)(u) = g(u))