Library LibDefaultSimp
Variants on standard tactics
Tactics for inversion
Putting it all together
Library Binders
Process variables
some utils
Library HOASSyntax
Operations on process variables
Basic lemmas about monadic operations
Library Semantics
agents
LTS
Basic LTS properties
Library Bisimulation
Early bisimulation
Bisimilarity
Open extension
Library Struct_congr
SC vs binders
Simulation proof
nu (P //Q) = (nu P) // Q
The simulation proof itself
Simulation up to SC
Library Howe
Basic properties
Symmetry of the transitive closure
Substitutivity
Library HoweSound
Sequential proof, input then output
Sequential proof, output then input
Simultaneous proof
Part common to all proofs
This page has been generated by
coqdoc