Complete the formalization of the asynchronous semantics

[jeltsch]

Currently, the asynchronous transition system is defined, but beyond it’s definition nothing is said about it. We shall add the following:

• An interpretation of the transition_system and the weak_transition_system locale for the asynchronous transition system
• An appropriate interpretation of the mutation_system and the weak_mutation_system locale for the asynchronous transition system
• Proofs of all compatibilities and quasi-compatibilities of process family constructors and derived operations (like repeated_receive) with asynchronous strong and asynchronous weak bisimilarity
• Appropriate fact registrations for the equivalence reasoner
• A proof that asynchronous bisimilarity includes synchronous bisimilarity, if that’s the case
• A proof that asynchronous weak bisimilarity includes synchronous weak bisimilarity
• Proofs that loops and repeated loops are asynchronously (or synchronously, if that’s the case) bisimilar to 𝟬