The definition of the conditioning modality requires an extra condition. In
particular, the forcing relation for

	(s, D, (F, μ)) ⊨ x ← X ~ π | P

is defined by

	X*μ « π and (s, D, F, μ) ⊨ own(X) and for all Borel measure μ’
	extending μ, for all (X, π)-disintegration (μ’ₓ) w.r.t μ’, π({x | μ’ₓ(Ω)
	= 0}) = 0 and for almost-all x,  μ’ₓ(Ω) > 0 implies ((s, x), D, F,
	μ’ₓ|F) ⊨ P.

The condition

	π({x | μ’ₓ(Ω) = 0}) = 0

is new. Consequently, Theorem 4.11 needs to be restated as follows:

Let f : A → [0,∞) be a Borel measurable function f · π ≫ π. Then the following
bi-entailment is valid:

	X ~ f · π ⊣⊢ x ← X ~ π | L(f(x)).

The proof rule HCondScore therefore needs a side condition:

	π({x ∈ A|(f · p)(x, B) = 0}) = 0.

for the Bayesian conditioning rule

	{x ← X ∼ π | Y ∼ p(x)} score(f(Y)) {x ← X ∼ π | Y ∼ (f · p)(x)}

to hold. The example Collider is therefore not sound via the existing proof
rules; other examples are unaffected.

Acknowledgement: We thank Janine Lohse for pointing this out.