It is then easy to verify that the conclusion of the partial derivation on the left-hand side of each rule has the value 3 C 4x C 2y C z, while the conclusion of the right-hand side has the value 2 C 2x C 2y C z.
each step decreases the value of a derivation tree under our assignment by the amount 1 C 2x.