Certificate for #1651 ⟨a, b | aab=bb, baa=b⟩

Back:⟨a, b | aab=bb, baa=b⟩

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[2] baa=b

Axiom: baa=b.

Defines rule #1.

Referenced by [3].

[3] aaaab=aab

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

b b bb

Critical pair: baab=aabb.

Reduce LHS:

[2](baa)b
[1]⇒ (bb)
⇒ aab

Reduce RHS:

[1]aa(bb)
⇒ aaaab

Flip LHS and RHS.

Defines rule #2.