K4free/TW2 graphs, free algebras, Coq proofs
This page is a web appendix to the following three papers:

K4free Graphs as a Free Algebra,
.pdf.
E. Cosme Llopez, D. Pous, in Proc. MFCS'17.

TreewidthTwo Graphs as a Free Algebra,
.pdf.
C. Doczkal, D. Pous, in Proc. MFCS'18.

A Formal Proof of the MinorExclusion Property for TreewidthTwo Graphs,
.pdf.
C. Doczkal, G. Combette, D. Pous, in Proc. ITP'18.
It is a wellknown 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 seriesparallel.

In the first paper above, we turn those graphs into a free
algebra, answering positively a question by Courcelle and
Engelfriet, in the case of treewidth two.
First we propose a syntax for denoting them: in addition to
parallel composition and series composition, it suffices to
consider the neutral elements of those operations and a unary
transpose operation. Then we give a finite equational
presentation (2palgebra) and we prove it complete: two terms from
the syntax are congruent if and only if they denote the same
graph.
Our proof is based on an precise analysis of the structure of
K4free graphs; it actually requires us to (re)prove that those
have treewidth at most two.

In the second paper, we give a simpler proof of the main result
from the first paper, not using minors at all: we use a confluent
rewriting system to extract terms from TW2 graphs. This approach
is more flexible and allows us to handle variants of 2palgebras:
2pdomalgebras for connected graphs and 1free 2palgebras for
graphs with distinct input and output and without selfloops.

In the third paper we give a formal and constructive proof in
Coq/Ssreflect that the graphs of treewidth two are exactly those
that do not admit K4 as a minor. This result is no longer required
to formally prove that those graphs form a free algebra, thanks to
the proof from the second paper; it should however be useful to
formalise the characterisation of
allegories we obtained with Valeria Vignudelli.
Coq/ssreflect proof of TW2=K4free
Independence of the 2palgebra 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 countermodels 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 countermodels, we found that there are 11
2palgebras with three elements and 236 with four elements (up to
isomorphism).