K4-free/TW2 graphs, free algebras, Coq proofs

This page is a web appendix to the following three papers:

  1. K4-free Graphs as a Free Algebra, .pdf.
    E. Cosme Llopez, D. Pous, in Proc. MFCS'17.
  2. Treewidth-Two Graphs as a Free Algebra, .pdf.
    C. Doczkal, D. Pous, in Proc. MFCS'18.
  3. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs, .pdf.
    C. Doczkal, G. Combette, D. Pous, in Proc. ITP'18.

It is a well-known result that graphs of treewidth at most two (TW2) are the ones excluding the clique with four vertices (K4) as a minor, or equivalently, the graphs whose biconnected components are series-parallel.

Coq/ssreflect proof of TW2=K4-free

Independence of the 2p-algebra axioms

We prove the independence of the axioms by exhibiting finite (partial) models.
We automatically checked those models in the Coq proof assistant, see the proof script here or download it there.
These counter-models have at most four elements; the converse operation is always taken to be the identity, except for the independence of axioms A6 and A7.

When looking for those counter-models, we found that there are 11 2p-algebras with three elements and 236 with four elements (up to isomorphism).