Nuprl - Proof: hanoi extend wf

(2steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc

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

n:

, f:({1...n}

Peg), n':

.

n

n'

(

f':({n+1...n'}

Peg). (f {to n}

f' {to n'})

{1...n'}

Peg)

By:	Def of <fun> {to <nat>} <fun> {to <nat>} THEN UnivCD THEN Analyze

Generated subgoal:

1 1. n :
2. f : {1...n}Peg
3. n' :
4. nn'
5. f' : {n+1...n'}Peg
6. i : {1...n'}
if in f(i) else f'(i) fi Peg
1 step

About:

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

(2steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc