CondSeparation proof outline

• Base case, ps = []: trivial, because LHS = RHS = []
• Induction step: ps = (ch',ws):ps'
  • Two cases
    • ch' == ch: the equation reduces to
      • {p1:pick ch (chip algs state1' ps')}
=== {p2:chip algs state2' (pick ch ps')}

        This follows from follows from the invariant, GoodAlg (algs ch) and the induction hypothesis (using Invariant ch state1' state2').

    • ch' /= ch: the equation reduces to
      • {pick ch (chip algs state1' ps')}
=== {chip algs state2 (pick ch ps')}

        This follows from the invariant and the induction hypothesis.