Theorem. Budget-preserving matched comparison [ftip-00GH]
✍️source

    Let two evaluation plans use the same declared stages except for a substitution whose cost is at most the replaced stage cost. If their common prefix cost is \(c_0\) and both suffix costs fit \(B-c_0\), then both cells in Definition [ftip-00GF] are admissible under budget \(B\).

    Proof. 

      Apply Lemma [ftip-00GG] to the common prefix and each suffix. The assumed inequalities give total cost at most \(B\) in each plan.