Project Page Index Table of Contents
  • A slightly more powerful done tactic
  • Preliminaries
  • Bijections between Types
  • Setoids and Label Structures
    • setoids
    • label structures (Definition 4.1)
    • BigOps over the label monoid
  • 2p algebras, tests, initial algebra of terms
    • 2p algebras (2pdom algebras with top)
    • basic derivable laws
  • 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
  • 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
  • Rewrite System on Packaged Graphs
  • 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
  • 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
    • Main Result
Generated by coqdoc and improved with CoqdocJS