User:IssaRice/Logical inductor construction

Lemma 5.1.1 (Fixed Point Lemma)

The following is used in the Fixed Point Lemma (5.1.1):

Writing the $n$ -strategy as

T_{n}=\sum _{j=1}^{k}\xi _{j}\phi _{j}-\sum _{j=1}^{k}\xi _{j}\phi _{j}^{*n}

we have

\mathbb {V} (T_{n}(\mathbb {P} _{\leq n-1},\mathbb {V} ))=\sum _{j=1}^{k}\xi _{j}(\mathbb {P} _{\leq n-1},\mathbb {V} )\cdot \mathbb {V} (\phi _{j})-\sum _{j=1}^{k}\xi _{j}(\mathbb {P} _{\leq n-1},\mathbb {V} )\cdot \phi _{j}^{*n}(\mathbb {P} _{\leq n-1},\mathbb {V} )

But $\phi _{j}^{*n}(\mathbb {P} _{\leq n-1},\mathbb {V} )=\mathbb {V} (\phi _{j})$ so the two sums cancel to obtain $0$ .