files.txt

*** preliminary shared modules ***
edone:			small extension of the [done] tactic
bounded:		fixpoint operator for bounded recursion
preliminaries:		miscellaneous basic lemmas missing from the standard libraries
finmap_plus:		additions to the mathcomp-finmap library
set_tac:		a simple tactic for reasoning about finite sets
bij:			computationally relevant bijections between sets
finite_quotient:	abstraction layer for mathcomp quotients
equiv:			lemmas about equivalence closure

*** JAR19 submission (general purpose graph library)
digraph:  	     	directed graphs, paths
sgraph:			simple graphs, trees and forests
helly:			Helly property for trees
treewidth:		tree decompositions, treewidth
minor:			minors, links with treewidth
menger:			Menger's theorem and corollaries
separators:		separators, proof of TW2 = K4-free via Menger's theorem
checkpoint:		checkpoints

*** JAR19 submission (2p-algebra related part)
ptt:	  		2p-algebras, initial algebra of terms
skeleton:		skeletons of multigraphs
mgraph2_tw2:		subalgebra of treewidth at most two multigraphs
cp_minor:		links between checkpoints and minors, for extraction
extraction_def: 	definition of the extraction function in the connected case
extraction_iso: 	correctness of the extraction function (connected case)
extraction_top: 	extension to the general case, TW2 = K4-free as a corollary

        mgraph      ptt   checkpoint  separators
        mgraph2    /            cp_minors
           skeleton             /
    mgraph2_tw2   extraction_def
       	         extraction_iso
   	  extraction_top

*** CPP20 submission
structures:		setoids, bisetoids, monoids
pttdom: 		2pdom-algebras, initial algebra of terms, tests
mgraph: 		labelled multigraphs
mgraph2: 		pointed multigraphs, 2pdom algebra of such graphs
rewriting: 		definition of the rewriting system
reduction: 		rewriting system powerful enough to reach normal forms
open_confluence: 	open graphs, open local confluence proof
transfer: 		transfer lemmas between the open and packed representations of 2p-graphs
completeness: 		wrapping up everything into a completeness proof

              structures                            
	     mgraph  pttdom
	        mgraph2
               rewriting
        reduction    open_confluence
                        transfer
	     completeness