Certificate for #14527 ⟨a, b | aaab=b, bbabb=a⟩

Back:⟨a, b | aaab=b, bbabb=a⟩

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Referenced by [3], [7], [8].

[2] bbabb=a

Axiom: bbabb=a.

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

[3] aaaa=a

Overlap of [1] aaab=b with [2] bbabb=a:

aaa b bbabb

Critical pair: aaaa=bbabb.

Reduce RHS:

[2](bbabb)
⇒ a

Referenced by [5].

[4] bbaa=aabb

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

bba bb bbabb

Critical pair: bbaa=aabb.

Referenced by [5].

[5] bba=abb

Overlap of [4] bbaa=aabb with [3] aaaa=a:

bb aa aaaa

Critical pair: bba=aabbaa.

Reduce RHS:

[4]aa(bbaa)
[3]⇒ (aaaa)bb
⇒ abb

Defines rule #3.

Referenced by [6].

[6] abbbb=a

Overlap of [2] bbabb=a with [5] bba=abb:

bbabb bba

Critical pair: abbbb=a.

Defines rule #2.

Referenced by [7].

[7] aaa=bbbb

Overlap of [1] aaab=b with [6] abbbb=a:

aa ab abbbb

Critical pair: aaa=bbbb.

Defines rule #4.

Referenced by [8].

[8] bbbbb=b

Overlap of [1] aaab=b with [7] aaa=bbbb:

aaab aaa

Critical pair: bbbbb=b.

Defines rule #1.