Certificate for #12897 ⟨a, b | aab=aaa, baaa=b⟩

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

Completion settings:

[1] aaa=aab

Axiom: aab=aaa.

Flip LHS and RHS.

Defines rule #2.

Referenced by [2], [3].

[2] baab=b

Axiom: baaa=b.

Reduce LHS:

[1]b(aaa)
⇒ baab

Referenced by [4], [5].

[3] aaba=aabb

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

a aa aaa

Critical pair: aaab=aaba.

Reduce LHS:

[1](aaa)b
⇒ aabb

Flip LHS and RHS.

Referenced by [4].

[4] ba=bb

Overlap of [2] baab=b with [3] aaba=aabb:

b aab aaba

Critical pair: baabb=ba.

Reduce LHS:

[2](baab)b
⇒ bb

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] bbbb=b

Overlap of [2] baab=b with [4] ba=bb:

baab ba

Critical pair: bbab=b.

Reduce LHS:

[4]b(ba)b
⇒ bbbb

Defines rule #3.