λ> test
>>> insert x t = T B [ins 1 E]
E 1 E
>>> insert x t = T B [ins 2 (T B E 1 E)]
  [ins 2 E]
  [balance B E 1 (T R E 2 E)]
     => (T B E 1 (T R E 2 E))
E 1 (T R E 2 E)
>>> insert x t = T B [ins 3 (T B E 1 (T R E 2 E))]
  [ins 3 (T R E 2 E)]
    [ins 3 E]
    [balance R E 2 (T R E 3 E)]
       => (T R E 2 (T R E 3 E))
  [balance B E 1 (T R E 2 (T R E 3 E))]
     => (T R (T B E 1 E) 2 (T B E 3 E))
(T B E 1 E) 2 (T B E 3 E)
>>> insert x t = T B [ins 4 (T B (T B E 1 E) 2 (T B E 3 E))]
  [ins 4 (T B E 3 E)]
    [ins 4 E]
    [balance B E 3 (T R E 4 E)]
       => (T B E 3 (T R E 4 E))
  [balance B (T B E 1 E) 2 (T B E 3 (T R E 4 E))]
     => (T B (T B E 1 E) 2 (T B E 3 (T R E 4 E)))
(T B E 1 E) 2 (T B E 3 (T R E 4 E))
>>> insert x t = T B [ins 5 (T B (T B E 1 E) 2 (T B E 3 (T R E 4 E)))]
  [ins 5 (T B E 3 (T R E 4 E))]
    [ins 5 (T R E 4 E)]
      [ins 5 E]
      [balance R E 4 (T R E 5 E)]
         => (T R E 4 (T R E 5 E))
    [balance B E 3 (T R E 4 (T R E 5 E))]
       => (T R (T B E 3 E) 4 (T B E 5 E))
  [balance B (T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 E))]
     => (T B (T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 E)))
(T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 E))
>>> insert x t = T B [ins 6 (T B (T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 E)))]
  [ins 6 (T R (T B E 3 E) 4 (T B E 5 E))]
    [ins 6 (T B E 5 E)]
      [ins 6 E]
      [balance B E 5 (T R E 6 E)]
         => (T B E 5 (T R E 6 E))
    [balance R (T B E 3 E) 4 (T B E 5 (T R E 6 E))]
       => (T R (T B E 3 E) 4 (T B E 5 (T R E 6 E)))
  [balance B (T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 (T R E 6 E)))]
     => (T B (T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 (T R E 6 E))))
(T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 (T R E 6 E)))
>>> insert x t = T B [ins 7 (T B (T B E 1 E) 2 (T R (T B E 3 E) 4 (T B E 5 (T R E 6 E))))]
  [ins 7 (T R (T B E 3 E) 4 (T B E 5 (T R E 6 E)))]
    [ins 7 (T B E 5 (T R E 6 E))]
      [ins 7 (T R E 6 E)]
        [ins 7 E]
        [balance R E 6 (T R E 7 E)]
           => (T R E 6 (T R E 7 E))
      [balance B E 5 (T R E 6 (T R E 7 E))]
         => (T R (T B E 5 E) 6 (T B E 7 E))
    [balance R (T B E 3 E) 4 (T R (T B E 5 E) 6 (T B E 7 E))]
       => (T R (T B E 3 E) 4 (T R (T B E 5 E) 6 (T B E 7 E)))
  [balance B (T B E 1 E) 2 (T R (T B E 3 E) 4 (T R (T B E 5 E) 6 (T B E 7 E)))]
     => (T R (T B (T B E 1 E) 2 (T B E 3 E)) 4 (T B (T B E 5 E) 6 (T B E 7 E)))
(T B (T B E 1 E) 2 (T B E 3 E)) 4 (T B (T B E 5 E) 6 (T B E 7 E))
>>> final = T B (T B (T B E 1 E) 2 (T B E 3 E)) 4 (T B (T B E 5 E) 6 (T B E 7 E))
λ>