Certificate for #14826 ⟨a, b | abba=a, babab=b⟩

Back:⟨a, b | abba=a, babab=b⟩

Completion settings:

[1] abba=a

Axiom: abba=a.

Defines rule #3.

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

[2] babab=b

Axiom: babab=b.

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

[3] abab=abb

Overlap of [1] abba=a with [2] babab=b:

ab ba babab

Critical pair: abb=abab.

Flip LHS and RHS.

Referenced by [5], [8].

[4] baba=bba

Overlap of [2] babab=b with [1] abba=a:

bab ab abba

Critical pair: baba=bba.

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

[5] abbb=ab

Overlap of [3] abab=abb with [3] abab=abb:

ab ab abab

Critical pair: ababb=abbab.

Reduce LHS:

[3](abab)b
⇒ abbb

Reduce RHS:

[1](abba)b
⇒ ab

Referenced by [6].

[6] bbab=bbb

Overlap of [2] babab=b with [5] abbb=ab:

bab ab abbb

Critical pair: babab=bbb.

Reduce LHS:

[4](baba)b
⇒ bbab

Referenced by [7], [8].

[7] bbb=b

Overlap of [2] babab=b with [4] baba=bba:

babab baba

Critical pair: bbab=b.

Reduce LHS:

[6](bbab)
⇒ bbb

Defines rule #2.

Referenced by [8].

[8] babb=b

Overlap of [4] baba=bba with [3] abab=abb:

b aba abab

Critical pair: babb=bbab.

Reduce RHS:

[6](bbab)
[7]⇒ (bbb)
⇒ b

Referenced by [9].

[9] bab=bb

Overlap of [2] babab=b with [8] babb=b:

ba bab babb

Critical pair: bab=bb.

Defines rule #1.