Certificate for #11343 ⟨a, b | aabaa=b, bbbbb=1⟩

Back:⟨a, b | aabaa=b, bbbbb=1⟩

Completion settings:

[1] aabaa=b

Axiom: aabaa=b.

Referenced by [3], [5].

[2] bbbbb=1

Axiom: bbbbb=1.

Defines rule #3.

Referenced by [4], [6].

[3] bbaa=aabb

Overlap of [1] aabaa=b with [1] aabaa=b:

aab aa aabaa

Critical pair: aabb=bbaa.

Flip LHS and RHS.

Referenced by [4], [5].

[4] baa=aab

Overlap of [2] bbbbb=1 with [3] bbaa=aabb:

bbbb b bbaa

Critical pair: bbbbaabb=baa.

Reduce LHS:

[3]bb(bbaa)bb
[3]⇒ (bbaa)bbbb
[2]⇒ aa(bbbbb)b
⇒ aab

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] aaaabb=bb

Overlap of [4] baa=aab with [1] aabaa=b:

b aa aabaa

Critical pair: bb=aabbaa.

Reduce RHS:

[3]aa(bbaa)
⇒ aaaabb

Flip LHS and RHS.

Referenced by [6].

[6] aaaa=1

Overlap of [5] aaaabb=bb with [2] bbbbb=1:

aaaa bb bbbbb

Critical pair: aaaa=bbbbb.

Reduce RHS:

[2](bbbbb)
⇒ 1

Defines rule #2.