{ x12 = k24 - x6,
  x16 = k27 - x15,
  x20 = k26 - x19,
  x23 = k25 - x24 }