chip :: Algs → ChipState → [Packet] → [Packet] type Algs = Channel → Alg type ChipState = (Memory,Regs) type Regs = FM RegFile assert Separation = ∀ algs . ∀ ch . ∀ state . ∀ ps . {pick ch (chip algs state ps)} === {chip algs state (pick ch ps)}