1. 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
16. a+z-ji
17. u : {a+z-j...z}
  f(u) = q

By:	Rewrite by u = a+z-(a+z-u)  {a...z} THEN BackThru: Hyp:14

None

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