Certificate for #628 ⟨a, b | bb=aa, abab=1⟩

Back:⟨a, b | bb=aa, abab=1⟩

Completion settings:

[1] bb=aa

Axiom: bb=aa.

Defines rule #3.

Referenced by [3], [4], [6].

[2] abab=1

Axiom: abab=1.

Referenced by [4], [6].

[3] aab=baa

Overlap of [1] bb=aa with [1] bb=aa:

b b bb

Critical pair: baa=aab.

Flip LHS and RHS.

Referenced by [5], [6].

[4] abaaa=b

Overlap of [2] abab=1 with [1] bb=aa:

aba b bb

Critical pair: abaaa=b.

Referenced by [5].

[5] ab=baaaaa

Overlap of [3] aab=baa with [4] abaaa=b:

a ab abaaa

Critical pair: ab=baaaaa.

Defines rule #2.

Referenced by [6].

[6] aaaaaaaa=1

Overlap of [2] abab=1 with [5] ab=baaaaa:

abab ab

Critical pair: baaaaaab=1.

Reduce LHS:

[3]baaaa(aab)
[3]⇒ baa(aab)aa
[3]⇒ b(aab)aaaa
[1]⇒ (bb)aaaaaa
⇒ aaaaaaaa

Defines rule #1.