Nuprl - Proof: hanoi pegseq analemma 1 1

(28steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi pegseq analemma 1 1

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)

By:	k:, a:, z:{a...}. z-ak (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   k:, a:, z:{a...}.
  z-ak

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

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

About:

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

(28steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc