Certificate for #1609 ⟨a, b | aaa=bb, bbb=b⟩

Back:⟨a, b | aaa=bb, bbb=b⟩

Completion settings:

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

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

[2] aaab=b

Axiom: bbb=b.

Reduce LHS:

[1](bb)b
⇒ aaab

Defines rule #3.

Referenced by [3], [4].

[3] baaa=b

Overlap of [1] bb=aaa with [1] bb=aaa:

b b bb

Critical pair: baaa=aaab.

Reduce RHS:

[2](aaab)
⇒ b

Defines rule #2.

[4] aaaaaa=aaa

Overlap of [2] aaab=b with [1] bb=aaa:

aaa b bb

Critical pair: aaaaaa=bb.

Reduce RHS:

[1](bb)
⇒ aaa

Defines rule #1.