Type
f' {to n'})(i) == if i
n
f(i) else f'(i) fi
n:
, f:({1...n}
Peg), n':.
Thm* n
n' 
(f':({n+1...n'}Peg). (f {to n} f' {to n'}) {1...n'}Peg)
| ik & kj }i,j:. {i...j} Type == {i:| 0i } TypeB == 
B<Ai,j:. (ij) Prop| Some definitions of interest. | |
| hanoi_PEG | |
| Type | |
| hanoi_extend | f' {to n'})(i) == if in f(i) else f'(i) fi |
| n:, f:({1...n}Peg), n':.
Thm* n n' (f':({n+1...n'}Peg). (f {to n} f' {to n'}) {1...n'}Peg) | |
| int_iseg | | ik & kj } |
| i,j:. {i...j} Type | |
| nat | == {i:| 0i } |
| Type | |
| le | B == B<A |
| i,j:. (ij) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |