**Good rules**: each rule checked (linear), G1, sites under nodes, every
control of redex and reactum owned by the component, ports linked as
`portOf` says. 

**A good agent of the component**: checked, one region, no sites, no
inner names, outer names exactly the ports, every control owned, ports
linked as `portOf` says. 

**Disjoint control sets** (Birkedal et al. 2006, Def 1, ⊥): no control is
owned by both. 

**UNBRIDGED** (built from `ppar`, `merge`, `close`). The composite agent:
one region, the names `hide` closed. 

**NEW** (no counterpart in TR-580 or Milner's book: a product of two
reaction rules; needed to make one rule out of an emitting and a
receiving half-rule) and **UNBRIDGED** (uses `ppar`).
The synchronisation of two half-rules: the wide redex `R₁ ∥ R₂`,
the reactum `R₁′ ∥ R₂′`, and `η₁ ++ (η₂ shifted by m₁)`. 

**NEW** (a construction on rule lists; no counterpart in the sources).
Synchronised composition `P ∥ Q` with the ports `keep` kept (all others
closed). Theorems about it are about the rule list it produces. 

**One composite step, on the components**: `P` moves alone (tag kept),
`Q` moves alone, or they synchronise on a shared port (`p!m` against
`p?m`, either way round), tag τ. The idle side's data is unchanged. 

**(D1) Decomposition** (OPEN; the bigraph content of option A; prior-art
§6 "D1", APPARENTLY NEW for BRS, template Baldan et al. 2008 Lemma 3.3).
For components with DISJOINT control sets (needed so that a rule of `P`
cannot match a node of `Q`: every redex node then lies in one side),
good rules (linear, G1, sites under nodes, own controls only, fixed port
linking `portOf`) and good agents `a₁`, `a₂`, the tagged library reactions of the composite agent
`⟦a₁ ∥ a₂⟧` under the composite rules are exactly the `CompStep`s, up
to ≏: every composite reaction is ≏ to `⟦a₁′ ∥ a₂′⟧` for a component
step `a₁ → a₁′`, `a₂ → a₂′` of that shape, and every such pair of
component steps gives a composite reaction ≏ to `⟦a₁′ ∥ a₂′⟧`. 

**The redex has no edge.** Under `portsFixed` every port is on an outer
name, so an edge of a redex is IDLE; the library matches an idle redex
edge to any idle edge of the agent, and the composite agent has idle
edges the component does not (an idle edge of the other side; a hidden
port no node is on). 

**Every outer name of the redex is on a port of a redex node.** An
outer name of the redex that is on no port (an idle name) is matched by
the library to ANY link of the agent, so the fixed port linking does not
constrain it: in the composite it can meet a link of the other side. 

**Good redexes** of a component: no edge, no idle outer name. 

**(D1′) Decomposition, restated** (OPEN). As `D1Statement`, with good
redexes (`RedexOk`), `faceOk` agents, and `faceOk` successors in the
second half. 

**A rule of one side in the composite agent** (OPEN). For a rule `r` of
`P` (any tag): the reactions of `⟦a₁ ∥ a₂⟧` by `r` are, up to ≏, the
`⟦a₁′ ∥ a₂⟧` for the reactions `a₁ → a₁′` of `⟦a₁⟧` by `r`; and
likewise for a rule of `Q` (the second pair). The splitting half needs
disjoint controls (the redex's nodes are `P`'s), `sitesUnderNodes` (the
parameter is `P`'s), `RedexOk` (no idle edge or name to meet `Q`). 

**The synchronisation rule in the composite agent** (OPEN; the rule
level of D1, for redexes WITH SITES). For a rule `r₁` of `P` and a rule
`r₂` of `Q` (any tags): the reactions of `⟦a₁ ∥ a₂⟧` by
`RuleD.par r₁ r₂` are, up to ≏, the `⟦a₁′ ∥ a₂′⟧` for the pairs of
reactions `a₁ → a₁′` by `r₁` and `a₂ → a₂′` by `r₂`. First half:
SPLITTING (an occurrence of the wide redex restricts to each side;
the parameter `d` splits as `d₁ ∥ d₂` along `η₁ ++ (η₂ + m₁)`). Second
half: JOINING.