Nuprl - Proof: hanoi general exists lemma2PROG wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi general exists lemma2PROG wf

, a:

, z:{a...}, m:{a...z-1}, f,g:({1...n}

Peg),

s1:({a...m}

{1...n-1}

Peg), s2:({m+1...z}

{1...n-1}

Peg).

HanoiHelper(n; s1; f; s2; g)

({a...m}

{1...n}

Peg)

({m+1...z}

{1...n}

Peg)

By:	Def of HanoiHelper(<nat>; <seq>; <fn>; <seq>; <fn>)

Generated subgoals:

None

About:

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