Note: for this proof, the denotational semnatics of the rewrite rules is that of equality
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.
DS |- eq mk(next(S:Sys)) = data(next(S:Sys)), list(S:Sys)
See proof2 for a proof of the above property.