(* 4 type annotations, whcih occupy about 10 lines *)

structure HanoiTowers =
    struct
	assert sub <| {n:nat, i:nat | i < n } 'a array(n) * int(i) -> 'a
        and    update <| {n:nat, i:nat| i < n } 'a array(n) * int(i) * 'a -> unit

	fun{size:nat}
	    play(size) =
	    let
		val leftPost = array(size,0)
		and middlePost = array(size,0)
		and rightPost = array(size,0)

		fun initialize(arr) =
		    let
			fun aux(i) =
			    if (i = size) then ()
			    else (update(arr, i, i+1); aux(i+1))
                        where aux <| {i:nat | i <= size } int(i) -> unit
		    in
			aux(0)
		    end
                where initialize <| int array(size) -> unit

		val _ = initialize(leftPost)

		fun move(n, source, s, post, p, post', p') =
		    if (n = 1) then (update(post, p - 1, sub(source, s)))
		    else (move(n-1, source, s, post', p', post, p);
			  update(post, p - 1, sub(source, s + n - 1));
			  update(source, s + n - 1, 0);
			  move(n-1, post', p'-n+1, post, p - 1, source, s + n))
                where move <|
		{n:nat, s, p:nat, p':nat |
		 p <= size /\ p' <= size /\ s + p + p' = size + size /\ 0 < n /\
		 s + n <= size /\ n <= p /\ n <= p' }
		int(n) * int array(size) * int(s) *
		int array(size) * int(p) * int array(size) * int(p') -> unit
                
	    in
		move(size, leftPost, 0, rightPost, size, middlePost, size)
	    end
	where play <| {dummy | size > 0 } int(size) -> unit
    end