set include BOOL off . fmod Hanoi is protecting BOOL * (sort Bool to REC-Bool) . sorts Disk List Move Tower . op 0 : -> Disk . op 1 : -> Disk . op 10 : -> Disk . op 11 : -> Disk . op 12 : -> Disk . op 13 : -> Disk . op 14 : -> Disk . op 15 : -> Disk . op 16 : -> Disk . op 2 : -> Disk . op 3 : -> Disk . op 4 : -> Disk . op 5 : -> Disk . op 6 : -> Disk . op 7 : -> Disk . op 8 : -> Disk . op 9 : -> Disk . op a : -> Tower . op b : -> Tower . op c : -> Tower . op conc : List List -> List . op dec : Disk -> Disk . op l : Move List -> List . op move : Disk Tower Tower -> Move . op nil : -> List . op other : Tower Tower -> Tower . op solve : Tower Tower Disk -> List . eq conc(L:List,nil) = L:List . eq conc(nil,L:List) = L:List . eq conc(l(H:Move,T:List),L:List) = l(H:Move,conc(T:List,L:List)) . eq dec(1) = 0 . eq dec(10) = 9 . eq dec(11) = 10 . eq dec(12) = 11 . eq dec(13) = 12 . eq dec(14) = 13 . eq dec(15) = 14 . eq dec(16) = 15 . eq dec(2) = 1 . eq dec(3) = 2 . eq dec(4) = 3 . eq dec(5) = 4 . eq dec(6) = 5 . eq dec(7) = 6 . eq dec(8) = 7 . eq dec(9) = 8 . eq other(a,b) = c . eq other(a,c) = b . eq other(b,a) = c . eq other(b,c) = a . eq other(c,a) = b . eq other(c,b) = a . eq solve(ORG:Tower,DEST:Tower,0) = nil . ceq solve(ORG:Tower,DEST:Tower,D:Disk) = conc(solve(ORG:Tower,other(ORG:Tower,DEST:Tower),dec(D:Disk)),l(move(D:Disk,ORG:Tower,DEST:Tower),solve(other( ORG:Tower,DEST:Tower),DEST:Tower,dec(D:Disk)))) if D:Disk =/= 0 = true . endfm reduce solve(a, b, 4) .