Verification of DS

Note: for this proof, the denotational semnatics of the rewrite rules is that of equality

• If channel contains bit then all bits after bit are equal to bit

   crl B':Bit => bit(S:Sys) if C1:Channel, < B:Bit,D:Data >, C2:Channel, < B':Bit,D':Data >, C3:Channel := channel(S:Sys) /\ B:Bit = bit(S:Sys) 

  See proof1 for a proof of the above property.

  ---

• All encrypted data sent are decoded and stored in the list structure in the same order they were sent

   DS |- eq mk(next(S:Sys)) = data(next(S:Sys)), list(S:Sys) 

  See proof2 for a proof of the above property.