1. p : Peg
2. k : 
3. k1:. 
3. k1<k
3. 
3. (a:, z:{a...}.
3. (z-ak1
3. (
3. ((f:({a...z}Peg). 
3. ((f(a) = p & f(z)  p
3. ((
3. (((x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p)))
4. a : 
5. z : {a...}
6. z-ak
7. f : {a...z}Peg
8. f(a) = p
9. f(z)  p
10. a = z
11. f(a+1) = p
  x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p

1

12. x:{a+1...z-1}. (u:{a+1...x}. f(u) = p) & f(x+1)  p   x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p

4 steps

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