| Who Cites hanoi seq deepen? |
|
hanoi_seq_deepen | Def (s(?) {to n} h {to n'})(x) == s(x) {to n} h {to n'} |
| | Thm* a,z: , n: , s:({a...z} {1...n} Peg), n': .
Thm* n n'
Thm* 
Thm* ( h:({n+1...n'} Peg). (s(?) {to n} h {to n'}) {a...z} {1...n'} Peg) |
|
hanoi_extend | Def (f {to n} f' {to n'})(i) == if i n f(i) else f'(i) fi |
| | Thm* n: , f:({1...n} Peg), n': .
Thm* n n'  ( f':({n+1...n'} Peg). (f {to n} f' {to n'}) {1...n'} Peg) |
|
le_int | Def i j ==  j< i |
| | Thm* i,j: . (i j)  |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j)  |
|
bnot | Def  b == if b false else true fi |
| | Thm* b: .  b  |