Proof of `Saturating and Perfect Matchings, Decided in the Same Time` (3rd statement)
groundedproofs/Lax117284Proofs/Bipartite/MachineTotal.lean · lax-117284
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
On every word whose length and entries fit the word length, the total program — the linear well-formedness check, the symmetrization of the adjacency lists into left rows, one search of Kuhn's algorithm per left vertex, and the comparison of the count with — decides the saturating question within instructions, .