Solution (source code)

= Solution

Only the first two trees need inspection:
``
cons :: a -> List a -> List a
cons x (List ((w,t):(v,u):ts))
  | w == v = List ((2*w+1, Node x t u):ts)
cons x (List ts) = List ((1, Leaf x):ts)
``
When the first sizes agree, place `x` above those two <perfect binary trees>. Its <preorder traversal> is `x` followed by the old two traversals. No further size-$w$ tree can occur, so all remaining sizes are at least $2w+1$; equality creates at most the allowed initial duplicate. When the first sizes differ, adjoining a singleton is valid, including the case that the old first tree is also a singleton. These are exactly the two possible greedy representations after increasing the length by one. Each case creates a bounded number of constructors and inspects no tree interior, giving \b[worst-case $O(1)$ <time complexity>]. Existing trees are shared.