def get_concat_level_bits(i, n, mul):
  """Create a string combining the bits of the current mul.

  Combine the bits of the multiplication of the current variable (at mul) by the
  i-th index of the previous variable.

  Args:
    i: An integer, the index of the previous variable.
    n: An integer, the number of bits in the bitvectors.
    mul: An integer, the index of the nested mul we're at.

  Returns:
    The resulting concat string.
  """
  concats = []
  if i > 0:
    concats.append(f"(concat m_{mul}_{i}_{i} #b{'0' * i})")
  else:
    concats.append(f"m_{mul}_0_0")
  if i < (n - 1):
    for j in range(i + 1, n):
      rhs = concats[j - i - 1]
      concat = ["(concat", f"m_{mul}_{i}_{j}", rhs + ")"]
      concats.append(" ".join(concat))
  return concats[-1]