GraphCountingStarter

Applying the finite handshaking theorem

Open in Workbench View on GitHub

1-- Applying the finite handshaking theorem.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module GraphCountingStarter7import Grace.Cumulus.GraphTheory.Counting89theorem degree_sum_is_twice_edges (V E enumeration : Set, n : Nat)10  requires graph : SimpleGraph(V, E)11  requires vertices : BijectiveBetween(enumeration, n, V)12  shows GraphCount.degreeSum(E, enumeration, n, n) =13    2 * GraphCount.edgeCount(E, enumeration, n)14proof15  exact SimpleGraph.handshaking with assumption, graph, vertices1617theorem degree_counts_neighbors (V E enumeration x : Set, n : Nat)18  requires vertices : ∀ i ∈ n, enumeration[i] ∈ V19  shows GraphCount.degree(E, enumeration, x, n) =20    countMembers(neighbors(V, E, x), enumeration, n)21proof22  exact GraphCount.degree.neighbors with assumption, vertices23