Certificate for #1780 ⟨a, b, c | aab=cc, bba=1⟩

Back:⟨a, b, c | aab=cc, bba=1⟩

Completion settings:

[1] cc=aab

Axiom: aab=cc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3].

[2] bba=1

Axiom: bba=1.

Defines rule #1.

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

[3] caab=aabc

Overlap of [1] cc=aab with [1] cc=aab:

c c cc

Critical pair: caab=aabc.

Referenced by [4], [5].

[4] caa=aabcba

Overlap of [3] caab=aabc with [2] bba=1:

caa b bba

Critical pair: caa=aabcba.

Defines rule #2.

Referenced by [5].

[5] aabcbab=aabc

Overlap of [3] caab=aabc with [4] caa=aabcba:

caab caa

Critical pair: aabcbab=aabc.

Referenced by [6].

[6] abcbab=abc

Overlap of [2] bba=1 with [5] aabcbab=aabc:

bb a aabcbab

Critical pair: bbaabc=abcbab.

Reduce LHS:

[2](bba)abc
⇒ abc

Flip LHS and RHS.

Referenced by [7].

[7] bcbab=bc

Overlap of [2] bba=1 with [6] abcbab=abc:

bb a abcbab

Critical pair: bbabc=bcbab.

Reduce LHS:

[2](bba)bc
⇒ bc

Flip LHS and RHS.

Defines rule #3.