[proofplan]
We prove the check-name identity by set-theoretic induction on the rank of the ground-model set $x$. The recursive definition of $\check{x}$ ensures that evaluating $\check{x}$ by a filter containing $1_{\mathbb{P}}$ produces exactly the evaluations of the check names of the elements of $x$. The induction hypothesis identifies those evaluations with the original elements. Finally, the generic name evaluates to the set of evaluated check names of the conditions belonging to $G$, and the first identity turns this into $G$ itself.
[/proofplan]
[step:Evaluate check names by induction on rank]
We prove that $(\check{x})_G = x$ for every ground-model set $x$ by set-theoretic induction on $x$. Assume that for a fixed ground-model set $x$, the identity $(\check{y})_G = y$ holds for every $y \in x$.
By the definition of valuation applied to the name $\check{x}$,
\begin{align*}
(\check{x})_G = \{\sigma_G : \text{there exists } p \in G \text{ such that } (\sigma,p) \in \check{x}\}.
\end{align*}
By the recursive definition of the check name, the pairs in $\check{x}$ are exactly the pairs $(\check{y},1_{\mathbb{P}})$ with $y \in x$. Since $1_{\mathbb{P}} \in G$, this gives
\begin{align*}
(\check{x})_G = \{(\check{y})_G : y \in x\}.
\end{align*}
Using the induction hypothesis for each $y \in x$, we obtain
\begin{align*}
(\check{x})_G = \{y : y \in x\} = x.
\end{align*}
By set-theoretic induction, the identity holds for every ground-model set $x$.
[guided]
We want to show that evaluating the canonical name $\check{x}$ recovers the original ground-model set $x$. The proof follows the recursive definition of $\check{x}$, so the correct induction is set-theoretic induction on membership: assume that every element $y \in x$ has already been recovered, meaning $(\check{y})_G = y$.
Now apply the definition of valuation to the name $\check{x}$. By definition,
\begin{align*}
(\check{x})_G = \{\sigma_G : \text{there exists } p \in G \text{ such that } (\sigma,p) \in \check{x}\}.
\end{align*}
The recursive definition of the check name says that the only pairs in $\check{x}$ are
\begin{align*}
(\check{y},1_{\mathbb{P}}) \quad \text{with } y \in x.
\end{align*}
Therefore the possible first coordinates $\sigma$ are precisely the names $\check{y}$ for $y \in x$, and the associated condition is always $1_{\mathbb{P}}$. The hypothesis $1_{\mathbb{P}} \in G$ is used exactly here: it guarantees that every pair $(\check{y},1_{\mathbb{P}})$ contributes to the valuation. Hence
\begin{align*}
(\check{x})_G = \{(\check{y})_G : y \in x\}.
\end{align*}
By the induction hypothesis, each element on the right satisfies $(\check{y})_G = y$. Substituting this into the displayed set gives
\begin{align*}
(\check{x})_G = \{y : y \in x\} = x.
\end{align*}
This completes the induction step, and set-theoretic induction gives $(\check{x})_G = x$ for every ground-model set $x$.
[/guided]
[/step]
[step:Evaluate the generic name using the check-name calculation]
By the definition of valuation applied to $\dot{G}$,
\begin{align*}
(\dot{G})_G = \{\sigma_G : \text{there exists } p \in G \text{ such that } (\sigma,p) \in \dot{G}\}.
\end{align*}
By the definition of the generic name, the pairs in $\dot{G}$ are exactly $(\check{q},q)$ with $q \in \mathbb{P}$. Therefore a pair from $\dot{G}$ contributes to the valuation exactly when its second coordinate $q$ belongs to $G$, and so
\begin{align*}
(\dot{G})_G = \{(\check{q})_G : q \in G\}.
\end{align*}
Since every $q \in G$ is a ground-model set and the first part gives $(\check{q})_G = q$, we obtain
\begin{align*}
(\dot{G})_G = \{q : q \in G\} = G.
\end{align*}
This proves both claimed identities.
[/step]
