( ( balance
  =   a x b y c zd
    .       !arg
          : ( B
            .   ( ( R
                  .   ((R.?a,?x,?b),?y,?c)
                    | (?a,?x,(R.?b,?y,?c))
                  )
                , ?zd
                )
              | ( ?a
                , ?x
                , ( R
                  .   ((R.?b,?y,?c),?zd)
                    | (?b,?y,(R.?c,?zd))
                  )
                )
            )
        & (R.(B.!a,!x,!b),!y,(B.!c,!zd))
      | !arg
  )
& ( ins
  =   C X tree a m z
    .     !arg:(?X.?tree)
        & !tree:(?C.?a,?m,?z)
        & (   !X:<!m
            & balance$(!C.ins$(!X.!a),!m,!z)
          |   !X:>!m
            & balance$(!C.!a,!m,ins$(!X.!z))
          | !tree
          )
      | (R.,!X,)
  )
& ( insert
  =   X tree
    .   !arg:(?X.?tree)
      & ins$(!X.!tree):(?.?X)
      & (B.!X)
  )
& ( insertMany
  =   L R tree
    .     !arg:(%?L_%?R.?tree)
        & insertMany$(!L.!tree):?tree
        & insertMany$(!R.!tree)
      | insert$!arg
  )
);