| Who Cites hanoi sol2 ala generalPROG? |
|
hanoi_sol2_ala_generalPROG | Def HanoiSTD(n disks; from: p; to: q; indexing from: a)
Def == if n= 0 <a, x,i. whatever>
Def == else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)
Def == else /m,s1.
Def == else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m
Def == else HanoiSTD(+1)
Def == else /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi
Def (recursive) |
| | Thm* n: , p,q:Peg.
Thm* p q
Thm* 
Thm* ( a: .
Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a)
Thm* ( z:{a...} ({a...z} {1...n} Peg)) |
|
hanoi_seq_join | Def (s1 @(m) s2)(x) == if x m s1(x) else s2(x) fi |
| | Thm* n: , m,a,z: , s1:({a...m} {1...n} Peg), s2:({m+1...z} {1...n} Peg).
Thm* (s1 @(m) s2) {a...z} {1...n} Peg |
|
hanoi_general_exists_lemma2PROG | Def HanoiHelper(n; s1; f; s2; g)
Def == <s1(?) {to n-1} f {to n},s2(?) {to n-1} g {to n}> |
| | Thm* n: , a: , z:{a...}, m:{a...z-1}, f,g:({1...n} Peg),
Thm* s1:({a...m} {1...n-1} Peg), s2:({m+1...z} {1...n-1} Peg).
Thm* HanoiHelper(n; s1; f; s2; g)
Thm* ({a...m} {1...n} Peg) ({m+1...z} {1...n} Peg) |
|
hanoi_otherpeg | Def otherPeg(x; y) == 6-(x+y) |
| | Thm* x,y:Peg. x y  otherPeg(x; y) Peg |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j)  |
|
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  |