Let \(a\) and \(b\) be detector events with \(a.\mathrm{getInit}.\mathrm{isSome}\) and \(b.\mathrm{getInit}.\mathrm{isSome}\) and \(a.\mathrm{getInit} = b.\mathrm{getInit}\). We proceed by case analysis on \(a\) and \(b\). If both are \(\mathrm{init}(e_a)\) and \(\mathrm{init}(e_b)\), then by simplification of \(\mathrm{getInit}\) and injectivity of \(\mathrm{some}\), we get \(e_a = e_b\) and hence \(a = b\). The cases where \(a\) is \(\mathrm{init}\) and \(b\) is \(\mathrm{meas}\) (or vice versa) are impossible since \(\mathrm{getInit}\) of a \(\mathrm{meas}\) event is \(\mathrm{none}\), contradicting \(\mathrm{isSome}\). The case where both are \(\mathrm{meas}\) is similarly impossible.

Let \(a\) and \(b\) be detector events with \(a.\mathrm{getMeas}.\mathrm{isSome}\) and \(b.\mathrm{getMeas}.\mathrm{isSome}\) and \(a.\mathrm{getMeas} = b.\mathrm{getMeas}\). By case analysis: if both are \(\mathrm{meas}(e_a)\) and \(\mathrm{meas}(e_b)\), simplification and injectivity of \(\mathrm{some}\) yields \(e_a = e_b\), hence \(a = b\). All other cases lead to contradictions with the \(\mathrm{isSome}\) hypotheses.

Unfolding the definitions of \(\mathrm{isSatisfied}\) and \(\mathrm{isViolated}\), this reduces to the fact that for any two elements \(a, b \in \mathbb {Z}/2\mathbb {Z}\), either \(a = b\) or \(a \neq b\), which holds by decidable equality.

Unfolding the definitions, we prove both directions. For the forward direction: assume \(\mathrm{observedParity} = \mathrm{expectedParity}\) and suppose for contradiction that \(\mathrm{observedParity} \neq \mathrm{expectedParity}\); this is a direct contradiction. For the backward direction: assume \(\neg (\mathrm{observedParity} \neq \mathrm{expectedParity})\) and suppose for contradiction that \(\mathrm{observedParity} \neq \mathrm{expectedParity}\); again a contradiction.

By simplification: the empty detector has no initialization events and no measurement events, so \(\mathrm{initParity} = 0\) and the sum over measurement events is \(0\). Thus \(\mathrm{observedParity} = 0 = \mathrm{expectedParity}\).

By simplification: the observed parity of the empty detector is \(0\), which equals the expected parity \(0\).

For the forward direction, if \(D_1 = D_2\) then both components are equal by reflexivity. For the backward direction, given equality of both components, we case-split on the structures and apply structural equality.

We use detector extensionality and verify both components. For events: \(\emptyset \mathbin {\triangle } D.\mathrm{events} = D.\mathrm{events}\) since \(\bot \mathbin {\triangle } x = x\). For expected parity: \(0 + D.\mathrm{expectedParity} = D.\mathrm{expectedParity}\).

By detector extensionality: \(D.\mathrm{events} \mathbin {\triangle } \emptyset = D.\mathrm{events}\) since \(x \mathbin {\triangle } \bot = x\), and \(D.\mathrm{expectedParity} + 0 = D.\mathrm{expectedParity}\).

By detector extensionality: \(D.\mathrm{events} \mathbin {\triangle } D.\mathrm{events} = \emptyset \) by the self-symmetric-difference property, and \(D.\mathrm{expectedParity} + D.\mathrm{expectedParity} = 0\) by the characteristic-\(2\) property.

Unfolding the definitions of \(\mathrm{isSatisfied}\), \(\mathrm{observedParity}\), and \(\mathrm{faultFreeOutcomes}\), the goal becomes exactly the consistency hypothesis.

By simplification of the definition of \(\mathrm{applyTimeFault}\) using the hypotheses \(e.\mathrm{measurement} = f.\mathrm{measurement}\), \(e.\mathrm{time} = f.\mathrm{time}\), and \(f.\mathrm{isFlipped} = \mathrm{true}\), the conditional evaluates to the flipped branch.

We unfold \(\mathrm{applyTimeFault}\) and split on the conditional. If the condition holds, we obtain \(m = f.\mathrm{measurement}\) and \(t = f.\mathrm{time}\), which contradicts the hypothesis that \(m \neq f.\mathrm{measurement}\) or \(t \neq f.\mathrm{time}\) (by case analysis on the disjunction). If the condition does not hold, the result follows by reflexivity.

Unfolding the definitions of \(\mathrm{isViolated}\), \(\mathrm{observedParity}\), and \(\mathrm{faultSyndrome}\), and using the hypotheses \(\mathrm{initParity} = 0\) and \(\mathrm{expectedParity} = 0\), the goal reduces to showing that the sum of measurement outcomes equals \(|D.\mathrm{measEvents} \cap \mathrm{faultedMeas}|\) in \(\mathbb {Z}/2\mathbb {Z}\), and that this quantity being nonzero is equivalent to it being \(1\).

For the sum equality, we split the sum over \(D.\mathrm{measEvents}\) into elements that are in \(\mathrm{faultedMeas}\) and those that are not. By hypothesis (1), the faulted elements each contribute \(1\), so their sum equals the cardinality of \(D.\mathrm{measEvents} \cap \mathrm{faultedMeas}\) (using the filter characterization). By hypothesis (2), the non-faulted elements each contribute \(0\), so their sum is \(0\). Adding these gives the desired equality.

For the equivalence between nonzero and equal to \(1\): in \(\mathbb {Z}/2\mathbb {Z}\), every element is either \(0\) or \(1\) (by exhaustive case analysis on \(\mathrm{Fin}\, 2\)). For the forward direction, if the value is nonzero then it must be \(1\). For the backward direction, if the value is \(1\) then \(1 \neq 0\) holds by computation.

Unfolding \(\mathrm{allSatisfied}\) and \(\mathrm{syndrome}\), the condition \(\mathrm{syndrome} = \emptyset \) is equivalent (via Finset.filter_eq_empty_iff) to the statement that no detector in the collection is violated. For the forward direction, if no detector is violated, then by the equivalence \(\mathrm{isSatisfied} \iff \neg \mathrm{isViolated}\) each detector is satisfied. For the backward direction, if each detector is satisfied, then by the same equivalence none is violated.

By simplification: filtering the empty set yields the empty set, so \(\mathrm{syndrome} = \emptyset \).