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