assert CondSeparation = ∀ algs ch state1 state2 ps . GoodAlg {algs ch} ==> Invariant state1 state2 ch ==> {pick ch (chip algs state1 ps)} === {chip algs state2 (pick ch ps)} assert AllGoodAlg = ∀ alg . GoodAlg alg assert SameState = ∀ state . ∀ ch . Invariant state state ch