Nuprl - Proof: hanoi pegseq analemma 1 1 2

(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 2

1. p : Peg
2.

k:

, a:

, z:{a...}.
2. z-a

k
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)

By:	Auto THEN BackThru: Hyp:2 Using:[z-a]

Generated subgoals:

None

About:

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

(28steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc