2. g : {2..k
}
3. x : {2..k
}
4. y : {2..k
}
5. x
y
6. x
y<k
7. y<x
y
8.
x<y
h:({2..k}).
{2..k}(g) = {2..k}(h) & h(xx) = 0 & (
u:{2..k}. xx<u 
h(u) = g(u))}
}
}
y
y<k
y
x<y
h:({2..k}).
{2..k}(g) = {2..k}(h) & h(xx) = 0 & (u:{2..k}. xx<u h(u) = g(u))| By: |
|
| 1 |
{2..k}(g) = {2..k}(split_factor1(g; x))
& split_factor1(g; x)(xx) = 0
& (u:{2..k}. xx<u split_factor1(g; x)(u) = g(u)) | 1 step |
About:
 |  |  |  |  |  |
 |  |  |  |
 |