= Solution
Define the ordered <merge algorithm> explicitly:
``
mergePos :: [Integer] -> [Integer] -> [Integer]
mergePos [] ys = ys
mergePos xs [] = xs
mergePos xs@(x:xt) ys@(y:yt)
| x <= y = x : mergePos xt ys
| otherwise = y : mergePos xs yt
ilv :: Seq a -> Seq a -> Seq a
ilv s t v = mergePos (map (2*) (s v))
(map (\j -> 2*j+1) (t v))
``
The first sequence occupies even positions and the second occupies odd positions. Within each transformed <list>, order is preserved; merging puts all positions for a queried token into increasing order. The two transformed lists have disjoint parities, so equality cannot occur between their heads on valid inputs. The length assumption ensures that these positions describe the intended interleaved sequence without a gap at its finite end.
Back to article page
