Certificate for #7039 ⟨a, b | bb=aa, aaaba=b⟩

Back:⟨a, b | bb=aa, aaaba=b⟩

Completion settings:

[1] aa=bb

Axiom: bb=aa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [2], [3], [5], [6].

[2] bbaba=b

Axiom: aaaba=b.

Reduce LHS:

[1](aa)aba
⇒ bbaba

Referenced by [4].

[3] bba=abb

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

a a aa

Critical pair: abb=bba.

Flip LHS and RHS.

Referenced by [4], [5].

[4] ababb=b

Simplify [2] bbaba=b.

Reduce LHS:

[3](bba)ba
[3]⇒ ab(bba)
⇒ ababb

Referenced by [5], [6].

[5] ba=abbbbb

Overlap of [4] ababb=b with [3] bba=abb:

aba bb bba

Critical pair: abaabb=ba.

Reduce LHS:

[1]ab(aa)bb
⇒ abbbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] bbbbbbbbb=b

Overlap of [4] ababb=b with [5] ba=abbbbb:

a babb ba

Critical pair: aabbbbbbb=b.

Reduce LHS:

[1](aa)bbbbbbb
⇒ bbbbbbbbb

Defines rule #1.