Certificate for #5266 ⟨a, b | aba=ab, bbaa=a⟩

Back:⟨a, b | aba=ab, bbaa=a⟩

Completion settings:

[1] aba=ab

Axiom: aba=ab.

Defines rule #2.

Referenced by [3].

[2] bbaa=a

Axiom: bbaa=a.

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

[3] abba=abb

Overlap of [1] aba=ab with [1] aba=ab:

ab a aba

Critical pair: abab=abba.

Reduce LHS:

[1](aba)b
⇒ abb

Flip LHS and RHS.

Referenced by [4], [5].

[4] abb=aa

Overlap of [3] abba=abb with [2] bbaa=a:

a bba bbaa

Critical pair: aa=abba.

Reduce RHS:

[3](abba)
⇒ abb

Flip LHS and RHS.

Referenced by [5], [8].

[5] aaa=aa

Overlap of [3] abba=abb with [4] abb=aa:

abba abb

Critical pair: aaa=abb.

Reduce RHS:

[4](abb)
⇒ aa

Referenced by [6].

[6] aa=a

Overlap of [2] bbaa=a with [5] aaa=aa:

bb aa aaa

Critical pair: bbaa=aa.

Reduce LHS:

[2](bbaa)
⇒ a

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [8].

[7] bba=a

Overlap of [2] bbaa=a with [6] aa=a:

bb aa aa

Critical pair: bba=a.

Defines rule #4.

[8] abb=a

Simplify [4] abb=aa.

Reduce RHS:

[6](aa)
⇒ a

Defines rule #3.