Maximum matching by Edmonds

Abstract view

Definition:

1. A path [math]\displaystyle{ p }[/math] in an undirected graph [math]\displaystyle{ G=(V,E) }[/math] is called alternating with respect to some matching [math]\displaystyle{ M }[/math] if, for any wo subsequent edges on [math]\displaystyle{ p }[/math], exactly one of them belongs to [math]\displaystyle{ M }[/math].
2. A path [math]\displaystyle{ p }[/math] in an undirected graph [math]\displaystyle{ G=(V,E) }[/math] is called augmenting with respect to some matching [math]\displaystyle{ M }[/math] if [math]\displaystyle{ p }[/math] is

Invariant: The current selection [math]\displaystyle{ M }[/math] of edges is a matching.

Variant: Either the cardinality of [math]\displaystyle{ M }[/math] increases, or the number of nodes of [math]\displaystyle{ G }[/math] decreases.

Break condition: There is no more augmenting path.

Induction basis

Abstract view: Start with some matching, for example, the empty matching.

Proof: Obvious.