[proofplan] The search is finite, so it must either discover an exposed vertex of $Y$ or exhaust all unmatched edges leaving the currently reached part of $X$. The key invariant is that $S$ consists precisely of vertices of $X$ reached by alternating paths of the correct parity, while $T$ consists of vertices of $Y$ reached by such paths after an unmatched edge. If an exposed vertex of $Y$ is reached, the invariant gives an augmenting path. If the search fails, the exhaustion condition forces every possible augmenting path from an exposed vertex of $X$ to remain inside the explored sets until its last vertex, contradicting that all reached vertices of $Y$ are matched. [/proofplan] [step:Record the alternating paths maintained by the search] For each vertex added during the search, record a predecessor as follows. If $y\in Y$ is added because $xy\in E\setminus M$ with $x\in S$, set the predecessor of $y$ to be $x$. If $y$ is matched by $x'y\in M$ and $x'$ is added to $S$, set the predecessor of $x'$ to be $y$. Vertices of $X_0$ have no predecessor. We prove the invariant: every $x\in S$ is reached from some vertex of $X_0$ by an $M$-alternating path whose first edge, if present, lies in $E\setminus M$ and whose final edge, if present, lies in $M$; every $y\in T$ is reached from some vertex of $X_0$ by an $M$-alternating path whose first and final edges lie in $E\setminus M$. Initially this holds because each $x\in X_0$ is reached by the path of length $0$. Suppose the invariant holds before an operation. If $y$ is added using $xy\in E\setminus M$, then an alternating path to $x$ followed by the unmatched edge $xy$ gives an alternating path to $y$ with final edge in $E\setminus M$. If $y$ is matched and $x'$ is added using $x'y\in M$, then appending the matched edge $yx'$ to the path to $y$ gives an alternating path to $x'$ with final edge in $M$. Thus the invariant is preserved. [guided] We want to make precise what the search has actually proved about each reached vertex. Define a recorded predecessor relation during the search. When a vertex $y\in Y$ is first added because there is an edge $xy\in E\setminus M$ with $x\in S$, record $x$ as the predecessor of $y$. If $y$ is not exposed, then matching means there is a unique vertex $x'\in X$ with $x'y\in M$; when $x'$ is added, record $y$ as the predecessor of $x'$. The vertices in $X_0$ are roots and have no predecessor. The invariant is the following parity statement. Every vertex $x\in S$ has a recorded path from some root $x_0\in X_0$ to $x$ whose edges alternate between $E\setminus M$ and $M$, starting with an unmatched edge when the path has positive length and ending with a matched edge when the path has positive length. Every vertex $y\in T$ has a recorded path from some root $x_0\in X_0$ to $y$ whose edges alternate between $E\setminus M$ and $M$, starting and ending with an unmatched edge. At the beginning, $S=X_0$ and $T=\varnothing$. For $x\in X_0$, the path of length $0$ is allowed, so the assertion for $S$ holds, and there is nothing to prove for $T$. Now assume the invariant holds immediately before one operation of the search. If the search adds $y\in Y$ using an edge $xy\in E\setminus M$ with $x\in S$, then by the invariant there is an alternating path from some $x_0\in X_0$ to $x$ of the correct parity. Appending the edge $xy$ preserves alternation, because the path to $x$ either has length $0$ or ends with a matched edge, while $xy$ is unmatched. Therefore $y$ has the required alternating path ending in an unmatched edge. If $y$ is matched, let $x'\in X$ be the unique vertex satisfying $x'y\in M$. The search adds $x'$ to $S$. The path to $y$ just constructed ends with an unmatched edge, so appending the matched edge $yx'$ again preserves alternation. The resulting path reaches $x'$ and ends with a matched edge. This proves that the invariant is preserved at every operation of the search. [/guided] [/step] [step:Show that reaching an exposed vertex of $Y$ gives an augmenting path] Assume the search stops with success after adding an $M$-exposed vertex $y\in Y$. By the invariant, there is an alternating path \begin{align*} P=(v_0,v_1,\dots,v_k) \end{align*} from some $v_0\in X_0$ to $v_k=y$, whose first and final edges lie in $E\setminus M$. Since $v_0\in X_0$, the vertex $v_0$ is $M$-exposed by definition of $X_0$. Since $y$ is reached in the success case, $v_k=y$ is also $M$-exposed. Thus $P$ is an alternating path whose endpoints are $M$-exposed and whose edges alternate between unmatched and matched edges. Therefore $P$ is an $M$-augmenting path. [/step] [step:Use failure to rule out every augmenting path from $X$] Assume the search stops with failure. Let $S\subset X$ and $T\subset Y$ be the final reached sets. Failure means that no edge $xy\in E\setminus M$ exists with $x\in S$ and $y\in Y\setminus T$. Also, every vertex of $T$ is matched by $M$; otherwise the search would have stopped with success when that vertex was added. Moreover, if $y\in T$ and $x'y\in M$, then $x'\in S$ by the rule of the search. Suppose, for contradiction, that there is an $M$-augmenting path \begin{align*} P=(v_0,v_1,\dots,v_k) \end{align*} with $v_0\in X$ exposed. Since $G$ is bipartite and $P$ starts in $X$ and ends at an exposed vertex of $Y$, the vertices with even index lie in $X$, the vertices with odd index lie in $Y$, and $k$ is odd. Since $v_0$ is exposed in $X$, we have $v_0\in X_0\subset S$. We prove by induction along the path that every even-indexed vertex $v_{2j}$ lies in $S$ and every odd-indexed vertex $v_{2j+1}$ lies in $T$. The base case is $v_0\in S$. If $v_{2j}\in S$, then the next edge $v_{2j}v_{2j+1}$ is in $E\setminus M$, because an augmenting path starting at an exposed vertex alternates beginning with an unmatched edge. Since failure leaves no unmatched edge from $S$ to $Y\setminus T$, it follows that $v_{2j+1}\in T$. If $2j+1<k$, then $v_{2j+1}$ is not the terminal exposed vertex, so the next edge $v_{2j+1}v_{2j+2}$ is the unique edge of $M$ incident to $v_{2j+1}$. By the search rule, its matched partner $v_{2j+2}$ lies in $S$. Applying this induction up to the last index gives $v_k\in T$. But $v_k$ is the terminal vertex of an augmenting path, hence is $M$-exposed, while every vertex in $T$ is matched in the failure case. This contradiction proves that no such augmenting path exists. [/step] [step:Conclude the two alternatives are exhaustive and exclusive] Because $G$ is finite and each operation adds at least one new vertex to $S\cup T$, the search terminates after finitely many operations. At termination it either has reached an $M$-exposed vertex of $Y$ or it has not. In the first case, the reached path is augmenting by the preceding step. In the second case, the search has failed and no augmenting path can start at an exposed vertex of $X$. These alternatives cannot both occur, since failure explicitly means that no exposed vertex of $Y$ was reached. Hence exactly one of the two stated alternatives occurs. [/step]