(28steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Given a sequence of pegs, perhaps with repititions, that starts with one and ends with another, there is a maximal prefix sequence every entry of which is the start peg, and there is a maximal suffix sequence every entry of which is the ending peg.

At: hanoi pegseq analemma

  p,q:Peg.
  p  q
  
  (a:, z:{a...}, f:({a...z}Peg).
  (f(a) = p & f(z) = 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)))
By: p:Peg, a:, z:{a...}, f:({a...z}Peg).
f(a) = p & f(z)  p  (x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p)
Asserted

Generated subgoals:

1   p:Peg, a:, z:{a...}, f:({a...z}Peg).
  f(a) = p & f(z)  p  (x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p)
14 steps
2 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
  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)
13 steps

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

(28steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc