A slightly more powerful done tactic
Preliminaries
Bigops over Setoids
Simple Experimental Tactic for finite sets
Bijections between Types
Directed Graphs
- Unpackaged Paths
- Packaged paths
- Packaged Irredundant Paths
- Basic Constructions on digraphs
- Interior of irredundant paths
- Isomorphisms
- Unindexed paths
- Neighborhoods
Simple Graphs
- Disjoint Union
- Homomorphisms
- Isomorphism of simple graphs
- Unpackaged Simple Paths
- Connectedness
- Forests and Trees
- Complete graphs
- Complete bipartite graphs
- Adding Edges
- Neighboring sets
- Edge Sets
- Edge Deletion
- Neighborhood lemmas for simple graphs
Graph Connectivty
- Connectors, Separators, and Separations
- Menger's Theorem
- Independent Path Corollaries
- Hall's Marriage Theorem
- König's Theorem
- k-connectivity
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
Minors
- Links with Treewidth
- Excluded-Minor Characterization of Forests
Tree Decompositions for K4-free graphs
Checkpoints
- Link Graph
- CP Closure Operator
- Intervals and bags
- Neighouring Checkpoints
- Partitioning with intervals, bags and checkpoints
- Checkpoint Order
Combined Minor and Checkpoint Properties
- Collapsing Bags
- K4-freenes of Intervals
- Parallel Split Lemma
Merging Vertices
- Edge Contraction in 3-connected graphs
- Isomorphims for vertex merging
Setoids and Label Structures
- label structures (Definition 4.1)
- Structure Inference
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)
Directed Labeled Multigraphs
- Basic Operations
- Operations that require structures on labels
- Homomorphisms
- Isomorphisms
- isomorphisms about local and global operations
- Subgraphs and Induced Subgraphs
- Merging Subgraphs
- Walks
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
Rewrite System for 2p-graphs (additive presentation)
Reducibility for the rewrite system
- Preliminary isomorphisms (on arbitrary graphs)
- preservation of steps under algebraic operations
- reduction lemma
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
Local Confluence of Rewrite System for 2p (open variant)
- Open Step relation
- Open Local Confluence
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
Completeness of the 2pdom axioms
2p algebras, tests, initial algebra of terms
- 2p algebras (2pdom algebras with top)
- basic derivable laws
Skeletons
- Interval and Bag Graphs
Subalgebra of Tree-Width 2 Graphs
Term Extraction for 2p-graphs in TW2
- Extraction function for connected graphs
- Correctness of the Extraction Function
- Extraction from Disconnected Graphs
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.
Clique Number, Stable Set Number and Chromatic Number
- Clique number
- Stable Set Number
- chromatic number
Perfection
- Lovasz Replication Lemma
Weak Perfect Graph Theorem
- First Proof - via replication
- Second Proof - using matrix rank argument
- Minimally Imperfect Graphs