Certificate for #9172 ⟨a, b | aa=a, babb=aba⟩

Back:⟨a, b | aa=a, babb=aba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] babb=aba

Axiom: babb=aba.

Defines rule #2.

Referenced by [3], [7].

[3] bababa=aba

Overlap of [2] babb=aba with [2] babb=aba:

bab b babb

Critical pair: bababa=abaabb.

Reduce RHS:

[1]ab(aa)bb
[2]⇒ a(babb)
[1]⇒ (aa)ba
⇒ aba

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

[4] ababa=baba

Overlap of [3] bababa=aba with [3] bababa=aba:

ba baba bababa

Critical pair: baaba=ababa.

Reduce LHS:

[1]b(aa)ba
⇒ baba

Flip LHS and RHS.

Defines rule #3.

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

[5] abbaba=aba

Overlap of [4] ababa=baba with [4] ababa=baba:

ab aba ababa

Critical pair: abbaba=bababa.

Reduce RHS:

[3](bababa)
⇒ aba

Referenced by [6].

[6] abbbaba=baba

Overlap of [5] abbaba=aba with [4] ababa=baba:

abb aba ababa

Critical pair: abbbaba=ababa.

Reduce RHS:

[4](ababa)
⇒ baba

Referenced by [7].

[7] bbaba=aba

Overlap of [2] babb=aba with [6] abbbaba=baba:

b abb abbbaba

Critical pair: bbaba=abababa.

Reduce RHS:

[4](ababa)ba
[3]⇒ (bababa)
⇒ aba

Defines rule #4.