Make equivalence work with repeated_receive #29
Description
Currently, equivalence is not configured to perform rewriting under repeated_receive. The reason is that repeated_receive is not compatible with bisimilarity, but only quasi-compatible. However, by resolving input-output-hk/equivalence-reasoner#60, rewriting under repeated_receive becomes possible.
We shall configure the equivalence reasoner such that it performs rewriting also under repeated_receive. For that, we shall add the following quasi-compatibility rule, with the compatibility attribute assigned to it, to the synchronous_transition_system locale:
lemma repeated_receive_quasi_compatibility_rule [compatibility]:
shows "A ▹⇧∞ x. 𝒫 x ∼ A ▹⇧∞ x. canonical (∼)⇧♯ 𝒫 x"