Project Page Index Table of Contents
  • A slightly more powerful done tactic
  • Preliminaries
  • Simple Graphs
    • Disjoint Union
    • Homomorphisms
    • Paths through simple graphs
    • Irredundant Paths
    • Packaged paths
    • Connectedness
    • Forests and Trees
  • Tree Width and Minors
    • Tree Decompositions
    • Complete graphs
    • Minors
  • Checkpoints
    • Link Graph
    • CP Closure Operator
    • Intervals and bags
    • Neighouring Checkpoints
    • Partitioning with intervals, bags and checkpoints
    • Checkpoint Order
  • Combined Minor and Checkpoint Properties
    • K4 of link triangle
    • Collapsing Bags
    • K4-freenes of Intervals
    • Parallel Split Lemma
  • Directed Multigraphs
    • Disjoint Union
    • Homomorphisms
    • Quotient Graphs
    • Subgraphs and Induced Subgraphs
    • Isomorphim Properties
  • Skeletons
    • Adjacency
    • Interval and Bag Graphs
  • Terms to Treewidth Two
    • Renaming
    • Disjoint Union
    • Link Construction
  • Subalgebra of Tree-Width 2 Graphs
    • Closure Properties for operations
    • Terms and tree-width 2 property
  • Isomorphim Properties for Graph-Algebra
    • Parallel Composition
    • Sequential Composition
  • Term Extraction Function
    • Termination Metric
    • Subroutines
    • The Extraction Functional
    • Termination Argument
  • Isomorphim Theorem
    • Graph Minor Theorem for TW2
Generated by coqdoc and improved with CoqdocJS