Certificate for #20168 ⟨a, b | aab=b, bbbb=aaa⟩

Back:⟨a, b | aab=b, bbbb=aaa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Referenced by [3], [5].

[2] aaa=bbbb

Axiom: bbbb=aaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[3] ab=bbbbb

Overlap of [2] aaa=bbbb with [1] aab=b:

a aa aab

Critical pair: ab=bbbbb.

Defines rule #2.

Referenced by [4], [5].

[4] bbbba=bbbbbbbb

Overlap of [2] aaa=bbbb with [2] aaa=bbbb:

a aa aaa

Critical pair: abbbb=bbbba.

Reduce LHS:

[3](ab)bbb
⇒ bbbbbbbb

Flip LHS and RHS.

Referenced by [6].

[5] bbbbbbbbb=b

Overlap of [1] aab=b with [3] ab=bbbbb:

a ab ab

Critical pair: abbbbb=b.

Reduce LHS:

[3](ab)bbbb
⇒ bbbbbbbbb

Defines rule #1.

Referenced by [6].

[6] ba=bbbbb

Overlap of [5] bbbbbbbbb=b with [4] bbbba=bbbbbbbb:

bbbbb bbbb bbbba

Critical pair: bbbbbbbbbbbbb=ba.

Reduce LHS:

[5](bbbbbbbbb)bbbb
⇒ bbbbb

Flip LHS and RHS.

Defines rule #3.