A slightly more powerful done tactic
Preliminaries
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
Simple Graphs
- Disjoint Union
- Homomorphisms
- Isomorphism of simple graphs
- Unpackaged Simple Paths
- Connectedness
- Forests and Trees
- Complete graphs
- Adding Edges
- Neighboring sets
Graph Connectivty
- Connectors, Separators, and Separations
- Menger's Theorem
- Independent Path Corollaries
- Hall's Marriage Theorem
- König's Theorem
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
Setoids and Label Structures
- setoids
- label structures (Definition 4.1)
- BigOps over the label monoid
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
- labeled directed multigraphs and their operations
- Basic Operations
- Disjoint Union and Quotients of graphs
- 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
- laws about low level operations (union/merge/add_vertex/add_vlabel/add_edge)
- 2p-graphs form a 2p-algebra
- additional laws required for the completeness proof
- Relabeling Graphs
2p algebras, tests, initial algebra of terms
- 2p algebras (2pdom algebras with top)
- basic derivable laws
Skeletons
- Strong skeletons
- Interval and Bag Graphs
- Disjoint Union of a connected component and the remainder of the graph
Subalgebra of Tree-Width 2 Graphs
Term Extraction Function
- Termination Metric
- Subroutines
- The Extraction Functional
- Termination Argument
Isomorphim Theorem
Extraction from Disconnected Graphs