Alternating paths algorithm

Algorithmic problem: The graph [math]\displaystyle{ G }[/math] is biparite.
Type of algorithm: loop
Auxillary data:

Abstract view

Invariant: Before and after each iteration, [math]\displaystyle{ M }[/math] is a matching. 
Variant: [math]\displaystyle{ |M| }[/math] increases by [math]\displaystyle{ 1 }[/math].
Break condition: There is no more augmenting alternating path.

Induction basis

Abstract view: [math]\displaystyle{ M }[/math] is initialized to be some matching, for example,  [math]\displaystyle{ M:=\empty1 }[/math].
Implementation: Obvious.
Proof: Nothing to show.

Induction step

Abstract view: If there is an augmenting alternating path, use it to increase [math]\displaystyle{ M }[/math]; otherwise, terminate the algorithm and return [math]\displaystyle{ M }[/math].
Implementation:

1. Call the algorithm Find augmenting alternating path.
2. If this call fails, terminate the algorithm and return [math]\displaystyle{ M }[/math].
3. Otherwise, let [math]\displaystyle{ E' }[/math] denote the set of all edges on the path delivered by that call.
4. Let [math]\displaystyle{ M }[/math] be the symmetric difference of [math]\displaystyle{ M }[/math] and <math<???</math>

Correctness:

Complexity

Statement:

Proof: