fmod HANOI is
	sorts Disc Peg State InVec .
	
	op 0 : -> Disc [ctor] .			*** smallest disc
	op s_ : Disc -> Disc [ctor] .	*** next bigger disc
	
	*** move disc from one peg to another in a current state
	op move : Disc Peg Peg State -> State [ctor] .
	
	*** move tower up to specified disc from start peg via aux peg to
	*** goal peg in a given state
	op Hanoi : Disc Peg Peg Peg State -> State [metadata "induce"] .
	op in : Disc Peg Peg Peg State -> InVec [ctor] .
	
	*** solution
	*** Hanoi(0, Src, Aux, Dst, S) = move(0, Src, Dst, S)
	*** Hanoi(s D, Src, Aux, Dst, S) = 
	***		Hanoi(D, Aux, Src, Dst, 
	***			move(s D, Src, Dst, 
	***				Hanoi(D, Src, Dst, Aux, S)))
	
	var S : State .
	vars Src Aux Dst : Peg .
	
	eq Hanoi(0, Src, Aux, Dst, S) = move(0, Src, Dst, S) .
	eq Hanoi(s 0, Src, Aux, Dst, S) = 
		move(0, Aux, Dst, move(s 0, Src, Dst, move(0, Src, Aux, S))) .
	eq Hanoi(s s 0, Src, Aux, Dst, S) = 
		move(0, Src, Dst, 
			move(s 0, Aux, Dst,
				move(0, Aux, Src,
					move(s s 0, Src, Dst, 
						move(0, Dst, Aux,
							move(s 0, Src, Aux,
								move(0, Src, Dst, S))))))) .
endfm