Formulation of the Channel Separation property

These two circuits produce the same output, provided

• the algorithm for the observed channel is good
• the initial states of two chips are related in an appropriate way
  ∀ algs ch state1 state2 ps .
  GoodAlg (algs ch) ==>
  Invariant state1 state2 ch ==>
  {pick ch (chip algs state1 ps)}
  ===
  {chip algs state2 (pick ch ps)}