Overall proof structure
The proof of Separation is obtained by combining
two the proofs of two main properties: CondSeparation and
AllGoodAlgs.
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
This factoring of the proof as some advantages...