Certificate for #5086 ⟨a, b | aaa=bb, abbb=a⟩

Back:⟨a, b | aaa=bb, abbb=a⟩

Completion settings:

[1] aaa=bb

Axiom: aaa=bb.

Defines rule #2.

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

[2] abbb=a

Axiom: abbb=a.

Defines rule #3.

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

[3] bba=abb

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

a aa aaa

Critical pair: abb=bba.

Flip LHS and RHS.

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

[4] bbbbb=bb

Overlap of [1] aaa=bb with [2] abbb=a:

aa a abbb

Critical pair: aaa=bbbbb.

Reduce LHS:

[1](aaa)
⇒ bb

Flip LHS and RHS.

Defines rule #4.

[5] aba=aab

Overlap of [2] abbb=a with [3] bba=abb:

abb b bba

Critical pair: abbabb=aba.

Reduce LHS:

[3]a(bba)bb
[2]⇒ a(abbb)b
⇒ aab

Flip LHS and RHS.

Referenced by [6].

[6] babb=a

Overlap of [1] aaa=bb with [5] aba=aab:

aa a aba

Critical pair: aaaab=bbba.

Reduce LHS:

[1](aaa)ab
[3]⇒ (bba)b
[2]⇒ (abbb)
⇒ a

Reduce RHS:

[3]b(bba)
⇒ babb

Flip LHS and RHS.

Referenced by [7].

[7] ba=ab

Overlap of [3] bba=abb with [6] babb=a:

b ba babb

Critical pair: ba=abbbb.

Reduce RHS:

[2](abbb)b
⇒ ab

Defines rule #1.