2. g : {2..k
}
3. x : {2..k
}
4. x
x<k
5. x<x
x
6. h : {2..k
}
7. h = split_factor1(g; x)
8. h(x
x) = 0
9. h(x) = g(x)+g(x
x)+g(xx)
10.
u:{2..k}. 
u = x 
u = xx h(u) = g(u)
{xx+1..k}(g) = {xx+1..k}(h)}
}
x<k
x
}
x) = 0
x)+g(xx)
u:{2..k}. u = x u = xx h(u) = g(u)
{xx+1..k}(g) = {xx+1..k}(h)| By: |
THEN New:u FunExtensionality THEN BackThru: Hyp:10 ... |
None
About:
 |  |  |  |  |  |  |  |  |  |