Certificate for #16441 ⟨a, b | aba=bb, aaab=ab⟩

Back:⟨a, b | aba=bb, aaab=ab⟩

Completion settings:

[1] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #2.

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

[2] aaab=ab

Axiom: aaab=ab.

Defines rule #1.

Referenced by [6].

[3] baba=abab

Overlap of [1] bb=aba with [1] bb=aba:

b b bb

Critical pair: baba=abab.

Defines rule #3.

Referenced by [4], [6].

[4] baabab=abaabaa

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

ba ba baba

Critical pair: baabab=ababba.

Reduce RHS:

[1]aba(bb)a
⇒ abaabaa

Defines rule #5.

Referenced by [5], [6].

[5] baabaaba=abaabaab

Overlap of [4] baabab=abaabaa with [1] bb=aba:

baaba b bb

Critical pair: baabaaba=abaabaab.

Defines rule #6.

[6] abaabaaa=abaaba

Overlap of [4] baabab=abaabaa with [3] baba=abab:

baa bab baba

Critical pair: baaabab=abaabaaa.

Reduce LHS:

[2]b(aaab)ab
[3]⇒ (baba)b
[1]⇒ aba(bb)
⇒ abaaba

Flip LHS and RHS.

Defines rule #4.