{ x5 = k16 - x1,
  x6 = x3 + x1 }