Certificate for #13029 ⟨a, b | abb=aba, baaa=b⟩

Back:⟨a, b | abb=aba, baaa=b⟩

Completion settings:

[1] aba=abb

Axiom: abb=aba.

Flip LHS and RHS.

Defines rule #2.

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

[2] baaa=b

Axiom: baaa=b.

Defines rule #3.

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

[3] abbba=abbbb

Overlap of [1] aba=abb with [1] aba=abb:

ab a aba

Critical pair: ababb=abbba.

Reduce LHS:

[1](aba)bb
⇒ abbbb

Flip LHS and RHS.

Referenced by [7].

[4] abbaa=ab

Overlap of [1] aba=abb with [2] baaa=b:

a ba baaa

Critical pair: ab=abbaa.

Flip LHS and RHS.

Referenced by [7].

[5] bba=bbb

Overlap of [2] baaa=b with [1] aba=abb:

baa a aba

Critical pair: baaabb=bba.

Reduce LHS:

[2](baaa)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #1.

Referenced by [6], [7].

[6] bbbbb=bb

Overlap of [5] bba=bbb with [2] baaa=b:

b ba baaa

Critical pair: bb=bbbaa.

Reduce RHS:

[5]b(bba)a
[5]⇒ bb(bba)
⇒ bbbbb

Flip LHS and RHS.

Defines rule #4.

[7] abbbb=ab

Simplify [4] abbaa=ab.

Reduce LHS:

[5]a(bba)a
[3]⇒ (abbba)
⇒ abbbb

Defines rule #5.