Certificate for #18754 ⟨a, b | aaa=a, bbaabb=a⟩

Back:⟨a, b | aaa=a, bbaabb=a⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

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

[2] bbaabb=a

Axiom: bbaabb=a.

Referenced by [3], [4].

[3] bba=abb

Overlap of [2] bbaabb=a with [2] bbaabb=a:

bbaa bb bbaabb

Critical pair: bbaaa=aaabb.

Reduce LHS:

[1]bb(aaa)
⇒ bba

Reduce RHS:

[1](aaa)bb
⇒ abb

Defines rule #2.

Referenced by [4], [5].

[4] aa=abbbb

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

bbaa bb bba

Critical pair: bbaaabb=aa.

Reduce LHS:

[3](bba)aabb
[3]⇒ a(bba)abb
[3]⇒ aa(bba)bb
[1]⇒ (aaa)bbbb
⇒ abbbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] abbbbbbbb=a

Overlap of [1] aaa=a with [4] aa=abbbb:

aaa aa

Critical pair: abbbba=a.

Reduce LHS:

[3]abb(bba)
[3]⇒ a(bba)bb
[4]⇒ (aa)bbbb
⇒ abbbbbbbb

Defines rule #1.