fmod CLEARBLOCK is
	sorts Block Tower State InVec .
	
	op table : -> Tower [ctor] .
	op __ : Block Tower -> Tower [ctor] .
	
	op putt : Block State -> State [ctor] .		*** put to table
	
	op ClearBlock : Block Tower State -> State [metadata "induce"] .
	op in : Block Tower State -> InVec [ctor] .
	
	*** solution
	*** ClearBlock(A, B T, S) = S if A == B
	*** ClearBlock(A, B T, S) = ClearBlock(A, T, putt(B, S))
	
	vars A B C : Block .
	var S : State .
	
	*** examples
	*** second example indicates that the block to be cleared need not
	*** be the bottom block
	eq ClearBlock(A, A table, S) = S .
	eq ClearBlock(A, A B table, S) = S .
	eq ClearBlock(A, B A table, S) = putt(B, S) .
	eq ClearBlock(A, C B A table, S) = putt(B, putt(C, S)) .
endfm