17.2.4. Correctness
The correctness of the algorithm in the previous subsection is easily established using Lemmas 17.2 and 17.3:
Rule 1 is correct because a maximum induced forest of \(G\) is the union of maximum induced forests of its connected components.
Rule 2 is correct by Lemma 17.2.
Rule 3 is correct because \(V \supseteq F\) and \(G = G[V]\) is acyclic either because \(V = F\) and \(G[F]\) is acyclic or every vertex in \(G\) has degree at most \(1\), so \(G\) cannot contain any cycles.
For any vertex \(v \notin F\) and any element \(F^* \in \mathcal{M}_G(F)\), either \(v \in F^*\) or \(v \notin F^*\). In the former case, \(F^* \in \mathcal{M}_G(F \cup \{v\})\) and the first recursive call of Rule 4 or 7 finds an element in \(\mathcal{M}_G(F \cup \{v\})\) of the same size as \(F^*\). In the latter case, \(F^* \in \mathcal{M}_{G-v}(F)\) and the second recursive call of Rule 4 or 7 finds an element in \(\mathcal{M}_{G-v}(F)\) of the same size as \(F^*\). Thus, Rules 4 and 7 are correct.
Rule 5 only picks an active vertex \(t\) and thus has no influence on the correctness of the algorithm.
Now consider an application of Rule 6 or 8. Then \(F\) is an independent set, \(t\) is the active vertex in \(F\), and \(v \in N(t)\). By Lemma 17.3, there exists an element \(F^* \in \mathcal{M}_G(F)\) such that either \(v \in F^*\) or \(|F^* \cap \tilde N_t(v)| \ge 2\). If \(|\tilde N_t(v)| \le 1\) or \(\tilde N_t(v) = \{w_1, w_2\}\) and \(G[F \cup \{w_1, w_2\}]\) contains a cycle, then there is no element \(F^* \in \mathcal{M}_G(F)\) such that \(|F^* \cap \tilde N_t(v)| \ge 2\). Thus, there must exist an element \(F^* \in \mathcal{M}_G(F)\) with \(v \in F^*\). This element is in \(\mathcal{M}_G(F \cup \{v\})\) and the recursive call in Rule 6 or the first recursive call in Rule 8 finds a set in \(\mathcal{M}_G(F \cup \{v\})\) of the same size as \(F^*\). This shows that Rule~6 is correct and that Rule 8 is correct in the case when \(G[F \cup \{w_1, w_2\}]\) contains a cycle.
If \(G[F \cup \{w_1, w_2\}]\) does not contain a cycle, then any set \(F^* \in \mathcal{M}_G(F)\) such that \(|F^* \cap \tilde N_t(v)| \ge 2\) contains both \(w_1\) and \(w_2\). Thus, we only need to consider sets \(F^*\) such that either \(v \in F^*\) or \(v \notin F^*\) and \(w_1, w_2 \in F^*\). In the former case, \(F^* \in \mathcal{M}_G(F \cup \{v\})\) and the first recursive call in Rule 8 finds an element of \(\mathcal{M}_G(F \cup \{v\})\) of the same size as \(F^*\). In the latter case, \(F^* \in \mathcal{M}_{G - v}(F \cup \{w_1, w_2\})\) and the second recursive call in Rule 8 finds an element of \(\mathcal{M}_{G-v}(F \cup \{w_1, w_2\})\) of the same size as \(F^*\). Thus, Rule 8 is correct.

This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.