Certificate for #6403 ⟨a, b | aab=b, ababa=b⟩

Back:⟨a, b | aab=b, ababa=b⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3], [5], [6], [8].

[2] ababa=b

Axiom: ababa=b.

Referenced by [3], [4], [6], [9].

[3] baba=ab

Overlap of [1] aab=b with [2] ababa=b:

a ab ababa

Critical pair: ab=baba.

Flip LHS and RHS.

Referenced by [5].

[4] bba=abb

Overlap of [2] ababa=b with [2] ababa=b:

ab aba ababa

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[5] babb=abab

Overlap of [3] baba=ab with [1] aab=b:

bab a aab

Critical pair: babb=abab.

Referenced by [6], [7].

[6] bbb=b

Overlap of [5] babb=abab with [4] bba=abb:

ba bb bba

Critical pair: baabb=ababa.

Reduce LHS:

[1]b(aab)b
⇒ bbb

Reduce RHS:

[2](ababa)
⇒ b

Defines rule #5.

Referenced by [7].

[7] abab=ba

Overlap of [6] bbb=b with [4] bba=abb:

b bb bba

Critical pair: babb=ba.

Reduce LHS:

[5](babb)
⇒ abab

Referenced by [8], [9].

[8] bab=aba

Overlap of [1] aab=b with [7] abab=ba:

a ab abab

Critical pair: aba=bab.

Flip LHS and RHS.

Defines rule #3.

[9] baa=b

Overlap of [2] ababa=b with [7] abab=ba:

ababa abab

Critical pair: baa=b.

Defines rule #2.