Grace/Cumulus/GraphTheory/DoubleCover/Theorem.g17

Open in Workbench Download source

Imports

EvenDoubleCover · CycleCover

Declarations

• cycleDoubleCover theorem derivation

Source

1-- The cycle double cover theorem: every finite bridgeless multigraph has a2-- list of cycles holding every edge exactly twice, as the cycles of its even3-- double cover.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.GraphTheory.DoubleCover.Theorem10import EvenDoubleCover11import CycleCover1213-- The cycle double cover theorem: the even double cover splits into cycles.14theorem cycleDoubleCover (V E leftEnd rightEnd : Set)15  requires graph : Graph(V, E, leftEnd, rightEnd)16  requires finiteVertices : Finite(V)17  requires finiteEdges : Finite(E)18  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)19  shows ∃ H, ∃ I, CycleDoubleCover(V, E, leftEnd, rightEnd, H, I)20proof21  obtain ⟨H, I, cover⟩ := Bridgeless.even_double_cover22    with graph, finiteVertices, finiteEdges, bridgeless23  exact EvenDoubleCover.to_cycles with graph, finiteVertices, cover24