-- The cycle double cover theorem: every finite bridgeless multigraph has a
-- list of cycles holding every edge exactly twice, as the cycles of its even
-- double cover.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.GraphTheory.DoubleCover.Theorem
import EvenDoubleCover
import CycleCover

-- The cycle double cover theorem: the even double cover splits into cycles.
theorem cycleDoubleCover (V E leftEnd rightEnd : Set)
  requires graph : Graph(V, E, leftEnd, rightEnd)
  requires finiteVertices : Finite(V)
  requires finiteEdges : Finite(E)
  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)
  shows ∃ H, ∃ I, CycleDoubleCover(V, E, leftEnd, rightEnd, H, I)
proof
  obtain ⟨H, I, cover⟩ := Bridgeless.even_double_cover
    with graph, finiteVertices, finiteEdges, bridgeless
  exact EvenDoubleCover.to_cycles with graph, finiteVertices, cover