Certificate for #8883 ⟨a, b | aa=a, abbab=ba⟩

Back:⟨a, b | aa=a, abbab=ba⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [5].

[2] abbab=ba

Axiom: abbab=ba.

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

[3] aba=ba

Overlap of [1] aa=a with [2] abbab=ba:

a a abbab

Critical pair: aba=abbab.

Reduce RHS:

[2](abbab)
⇒ ba

Defines rule #2.

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

[4] abbba=bbab

Overlap of [2] abbab=ba with [2] abbab=ba:

abb ab abbab

Critical pair: abbba=babab.

Reduce RHS:

[3]b(aba)b
⇒ bbab

Referenced by [5].

[5] bbab=ba

Overlap of [2] abbab=ba with [3] aba=ba:

abb ab aba

Critical pair: abbba=baa.

Reduce LHS:

[4](abbba)
⇒ bbab

Reduce RHS:

[1]b(aa)
⇒ ba

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

[6] bbba=ba

Overlap of [5] bbab=ba with [2] abbab=ba:

bb ab abbab

Critical pair: bbba=babab.

Reduce RHS:

[3]b(aba)b
[5]⇒ (bbab)
⇒ ba

Referenced by [7].

[7] bba=bab

Overlap of [6] bbba=ba with [5] bbab=ba:

b bba bbab

Critical pair: bba=bab.

Defines rule #3.

Referenced by [8].

[8] babb=ba

Overlap of [5] bbab=ba with [7] bba=bab:

bbab bba

Critical pair: babb=ba.

Defines rule #4.