Library GraphTheory.edone

• A slightly more powerful done tactic

Library GraphTheory.bounded

• • • A fixpoint operator for bounded recursion

Library GraphTheory.preliminaries

• Preliminaries
  • • Tactics
    • Notations
    • Generic Trivialities
    • Disjointness
    • Function Update
    • Sequences and Paths
    • Reflexive Transitive Closure
    • Set preimage
    • Set image
    • Replacement for partial functions
    • Partitions
• Preliminaries (used in Domination Theory)

Library GraphTheory.setoid_bigop

• Bigops over Setoids
  • setoids

Library GraphTheory.finmap_plus

Library GraphTheory.set_tac

• Simple Experimental Tactic for finite sets

Library GraphTheory.bij

• Bijections between Types

Library GraphTheory.finite_quotient

Library GraphTheory.equiv

Library GraphTheory.digraph

• Directed Graphs
  • Unpackaged Paths
  • Packaged paths
    • Splitting Paths
    • Between nodes (reflection lemmas)
  • Packaged Irredundant Paths
  • Basic Constructions on digraphs
    • Induced Subgraphs
    • Edge Deletion
  • Interior of irredundant paths
  • Isomorphisms
  • Unindexed paths
  • Neighborhoods

Library GraphTheory.sgraph

• Simple Graphs
  • Disjoint Union
  • Homomorphisms
  • Isomorphism of simple graphs
  • Unpackaged Simple Paths
    • Transporting paths to and from induced subgraphs
    • Path indexing and 3-way split
  • Connectedness
    • Of subsets
    • Connected components
    • Cliques
  • Forests and Trees
    • Forest Type (for tree decompositions)
  • Complete graphs
  • Adding Edges
  • Neighboring sets
  • Edge Sets
  • Edge Deletion
  • Neighborhood lemmas for simple graphs

Library GraphTheory.helly

Library GraphTheory.connectivity

• Graph Connectivty
  • Connectors, Separators, and Separations
  • Menger's Theorem
  • Independent Path Corollaries
    • Vertex version
    • Edge Version
  • Hall's Marriage Theorem
  • König's Theorem

Library GraphTheory.treewidth

• Tree Decompositions and treewidth
  • Renaming
  • Disjoint Union
  • Link Construction (without intermediate node)
  • Link Construction (with intermediate node)
  • Every clique is contained in some bag
  • Forests have treewidth 1

Library GraphTheory.minor

• Minors
  • Links with Treewidth
  • Excluded-Minor Characterization of Forests

Library GraphTheory.excluded

• Tree Decompositions for K4-free graphs

Library GraphTheory.checkpoint

• Checkpoints
  • Link Graph
  • CP Closure Operator
    • Checkpoint graph
  • Intervals and bags
    • Strict intervals
    • Intervals
    • Bags
  • Neighouring Checkpoints
    • Application to bags
  • Partitioning with intervals, bags and checkpoints
    • Disjointness statements
    • Covering statements
  • Checkpoint Order

Library GraphTheory.cp_minor

• Combined Minor and Checkpoint Properties
  • Collapsing Bags
  • K4-freenes of Intervals
  • Parallel Split Lemma

Library GraphTheory.structures

• Setoids and Label Structures
  • label structures (Definition 4.1)
  • Structure Inference

Library GraphTheory.pttdom

• 2pdom algebra, tests, initial algebra of terms
  • 2pdom algebra (the top-free fragment of 2p algebra)
  • basic derivable laws
  • tests
  • commutative monoid of tests
  • label structure of a 2pdom algebra (Definition 4.3)
  • other derivable laws used in the completeness proof
  • initial algebra of terms
  • normal terms and normalisation function (Section 7)

Library GraphTheory.mgraph

• Directed Labeled Multigraphs
  • Basic Operations
  • Operations that require structures on labels
  • Homomorphisms
  • Isomorphisms
  • isomorphisms about local and global operations
    • isomorphisms about unit_graph
    • isomorphisms about add_edge
    • isomorphisms about union
    • isomorphisms about merge
    • isomorphisms about union and merge (Lemma 4.11)
  • Subgraphs and Induced Subgraphs
    • isomorphisms about subgraphs
  • Merging Subgraphs
  • Walks

Library GraphTheory.mgraph2

• Two-pointed labelled multigraphs
  • Isomorphisms of 2p-graphs
  • 2pdom operations on graphs
  • 2p-graphs form a 2p-algebra
  • additional laws required for the completeness proof
  • Relabeling Graphs

Library GraphTheory.rewriting

• Rewrite System on Packaged Graphs

Library GraphTheory.reduction

• Reducibility for the rewrite system
  • Preliminary isomorphisms (on arbitrary graphs)
  • preservation of steps under algebraic operations
    • Lemma 6.3
    • Lemma 6.2
  • reduction lemma
    • graphs of terms and normal terms

Library GraphTheory.open_confluence

• Open Graphs
  • Open 2p-graphs labeled with elements of a 2pdom algebra
  • Strong Equivalence
  • Helper functions
  • Operatons on open graphs
  • Properties of the operations
  • Commutation Lemmas
  • Morphism Lemmas
  • Killing Lemmas
• Open Step relation
  • Open Local Confluence

Library GraphTheory.transfer

• Transfer of Open Local Confluence
  • Opening and packing of type-based graphs
  • Isomorphism and Commutation Properties
  • Commutation with open/pack
  • Isomorphisms on open graphs
  • Preservation of open steps under isomorphisms
  • Packaged steps to open steps
  • Open steps to packaged steps

Library GraphTheory.completeness

• Completeness
  • Main Result

Library GraphTheory.ptt

• 2p algebras, tests, initial algebra of terms
  • 2p algebras (2pdom algebras with top)
  • basic derivable laws

Library GraphTheory.skeleton

• Skeletons
  • Strong skeletons
  • Interval and Bag Graphs
  • Disjoint Union of a connected component and the remainder of the graph

Library GraphTheory.mgraph2_tw2

• Subalgebra of Tree-Width 2 Graphs

Library GraphTheory.extraction_def

• Term Extraction Function
  • Termination Metric
  • Subroutines
  • The Extraction Functional
  • Termination Argument

Library GraphTheory.extraction_iso

• Isomorphim Theorem

Library GraphTheory.extraction_top

• Extraction from Disconnected Graphs

Library GraphTheory.dom

• Domination Theory
  • Hereditary and superhereditary properties
  • Weighted Sets
  • Stable, Dominating and Irredundant Sets
  • Fundamental facts about Domination Theory
  • Weighted version of the Cockayne-Hedetniemi domination chain.
  • Classic (unweighted) parameters (use cardinality instead of weight)
  • Classic Cockayne-Hedetniemi domination chain.