Corollary: Finite event ancestry

For a finite sequence of localized internal devices with envelopes $b_1,\dots ,b_m$, start from $S_m=Y$ and put

The complete pullback of $\mathfrak{A}(Y)$ lies in $\mathfrak{A}(S_0)$. Replacing excluded devices does not change the terminal snapshot when the initial restriction and the included complete device actions agree.

Proof. Apply Lemma lem:devicesupport at each backward step. Then apply Theorem thm:comparison.