Certificate for #12183 ⟨a, b | aaaa=ab, baab=b⟩

Back:⟨a, b | aaaa=ab, baab=b⟩

Completion settings:

[1] aaaa=ab

Axiom: aaaa=ab.

Defines rule #4.

Referenced by [3], [6].

[2] baab=b

Axiom: baab=b.

Referenced by [4], [5], [7], [8].

[3] aba=aab

Overlap of [1] aaaa=ab with [1] aaaa=ab:

a aaa aaaa

Critical pair: aab=aba.

Flip LHS and RHS.

Referenced by [4], [5].

[4] baaab=ba

Overlap of [2] baab=b with [3] aba=aab:

ba ab aba

Critical pair: baaab=ba.

Referenced by [7].

[5] aaabb=ab

Overlap of [3] aba=aab with [2] baab=b:

a ba baab

Critical pair: ab=aabab.

Reduce RHS:

[3]a(aba)b
⇒ aaabb

Flip LHS and RHS.

Referenced by [6].

[6] aab=abbb

Overlap of [1] aaaa=ab with [5] aaabb=ab:

a aaa aaabb

Critical pair: aab=abbb.

Defines rule #3.

Referenced by [7].

[7] ba=bbb

Simplify [4] baaab=ba.

Reduce LHS:

[6]ba(aab)
[2]⇒ (baab)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[8] bbbbbb=b

Overlap of [2] baab=b with [7] ba=bbb:

baab ba

Critical pair: bbbab=b.

Reduce LHS:

[7]bb(ba)b
⇒ bbbbbb

Defines rule #1.