p:Peg, a:
, z:{a...}, f:({a...z}
Peg).
1. f(a) = p & f(z)
p 
(
x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1) p)
2. p : Peg
3. q : Peg
4. p
q
5. a :
6. z : {a...}
7. f : {a...z}
Peg
8. f(a) = p
9. f(z) = q
10. i : {a...z-1}
11.
u:{a...i}. f(u) = p
12. f(i+1)
p
13. j : {a...z-1}
14.
u:{a...j}. f(a+z-u) = q
15. f(a+z-(j+1))
q
x:{a...z-1}, y:{x+1...z}.
(u:{a...x}. f(u) = p) & f(x+1) p & f(y-1) q & (u:{y...z}. f(u) = q)
a+z-j
i Asserted
