{ x6 = k20 - x2,
  x7 = x3 }