Formalizing a Fragment of Combinatorics on Words
(Web Support)

June 2017

This page provides Web support for Formalizing a Fragment of Combinatorics on Words, presented at Computability in Europe 2017. In particular, we present proofs for two results described in the paper.

Commutation Lemma.

```   x * y = y * x -> (exists z (Power(x,z) & Power(y,z))).
```
Periodicity Lemma.
```   (Period(x,u) & Period(y,u) & -Shorter(u,x * y)) => x * y = y * x.
```
The proofs presented here were found with the automated theorem proving program, Prover9. We include for each problem the relevant input and output files and also a separate file with the proof from the output file.

### General Files

The shorter version of the axioms was used to help narrow two of the searches.

### Commutation Lemma

```   prover9 -f p9header axioms.in Goal01.in
```

### Periodicity Lemma

The file Goal02.map describes how the proof is organized into 9 parts run as follows.
```   # run with the full axiom set

prover9 -f p9header axioms.in Lemma_1.in
prover9 -f p9header axioms.in Lemma_2.in
prover9 -f p9header axioms.in Lemma_3.in
prover9 -f p9header axioms.in Lemma_4.in
prover9 -f p9header axioms.in Reform_1a.in
prover9 -f p9header axioms.in Reform_2a.in
prover9 -f p9header axioms.in Case1.in

# run with the shortened axiom set (to help narrow the search)

prover9 -f p9header axioms.short Case2a.in
prover9 -f p9header axioms.short Case2.in
```
9 sets of files (input, output, proof):