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)}