Formal proof of the equivalence between a denotational semantics and an operational semantics on traces model of CSP by Isabelle/HOL 2014

The syntax is compatible with CSP-Prover.

(C) 2020 Hisabumi Hatsugai