| Who Cites hanoi peg perm? |
|
hanoi_peg_perm | Def permute(p to r ; q to s)(u) == if u= p r ; u= q s else otherPeg(r; s) fi |
| | Thm* p,r,q,s:Peg. p q  r s  permute(p to r ; q to s) Peg Peg |
|
hanoi_otherpeg | Def otherPeg(x; y) == 6-(x+y) |
| | Thm* x,y:Peg. x y  otherPeg(x; y) Peg |
|
eq_hanoi_PEG | Def p= q == if p=q true ; false fi |
| | Thm* p,q:Peg. (p= q)  |