Certificate for #20118 ⟨a, b | aab=b, baaa=bba⟩

Back:⟨a, b | aab=b, baaa=bba⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3], [4].

[2] baaa=bba

Axiom: baaa=bba.

Defines rule #3.

Referenced by [3], [4].

[3] bbab=bab

Overlap of [2] baaa=bba with [1] aab=b:

ba aa aab

Critical pair: bab=bbab.

Flip LHS and RHS.

Defines rule #4.

[4] bbb=bb

Overlap of [2] baaa=bba with [1] aab=b:

baa a aab

Critical pair: baab=bbaab.

Reduce LHS:

[1]b(aab)
⇒ bb

Reduce RHS:

[1]bb(aab)
⇒ bbb

Flip LHS and RHS.

Defines rule #2.