3. Bigraphs
Milner's pure bigraphs (Milner 2009; Jensen and Milner, TR-580, 2004) in
Lean: the algebra of composition and tensor up to support equivalence,
reaction, the congruence theorem for bisimilarity, and the encoding of CCS.
Symbols are those of the Notation chapter. Every other result is in
Bigraph/: the remaining spm laws (Laws.lean), the derived operators
(Derived.lean), binding and the scope rule (Binding.lean, Scope.lean),
and the place-graph layout check and certificate checker
(Layout.lean, Problems/Check.lean).