Nuprl - Proof: split factor2 char 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: split factor2 char 1 1

1. k : {2...}
2. g : {2..k

}

3. x : {2..k

}
4. y : {2..k

}
5. x

y<k
6. x<y
7. x<x

y
8. y<x

y
9. h : {2..k

}

10. h = split_factor2(g; x; y)
11. h(x

y) = 0
12. h(x) = g(x)+g(x

y)
13. h(y) = g(y)+g(x

y)
14.

u:{2..k

}.

u = x

u = y

u = x

y

h(u) = g(u)

{2..x

}(g)

x

g(x)

{x+1..y

}(g)

y

g(y)

{y+1..x

y

}(g)

{2..x

}(g)

x

g(x)

{x+1..y

}(g)

y

g(y)

(x

y)

g(x

y)

{x

y+1..k

}(g)

=

{2..x

}(h)

x

h(x)

{x+1..y

}(h)

y

h(y)

{y+1..x

y

}(h)

{2..x

}(h)

x

h(x)

{x+1..y

}(h)

y

h(y)

(x

y)

h(x

y)

{x

y+1..k

}(h)

By:	{Factor out the sections falling between x, y, and xy, which agree by Hyp:14 } SideProof

Generated subgoal:

1 xg(x)yg(y)(xy)g(xy) = xh(x)yh(y)(xy)h(xy)
3 steps

About:

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

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