Certificate for #8900 ⟨a, b | aa=a, babab=ab⟩

Back:⟨a, b | aa=a, babab=ab⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] babab=ab

Axiom: babab=ab.

Referenced by [3], [4].

[3] abab=bab

Overlap of [2] babab=ab with [2] babab=ab:

ba bab babab

Critical pair: baab=abab.

Reduce LHS:

[1]b(aa)b
⇒ bab

Flip LHS and RHS.

Defines rule #2.

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

[4] abbab=ab

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

ab ab abab

Critical pair: abbab=babab.

Reduce RHS:

[2](babab)
⇒ ab

Referenced by [5], [6].

[5] abbbab=bab

Overlap of [4] abbab=ab with [3] abab=bab:

abb ab abab

Critical pair: abbbab=abab.

Reduce RHS:

[3](abab)
⇒ bab

Referenced by [6].

[6] bbab=ab

Overlap of [3] abab=bab with [5] abbbab=bab:

ab ab abbbab

Critical pair: abbab=babbbab.

Reduce LHS:

[4](abbab)
⇒ ab

Reduce RHS:

[5]b(abbbab)
⇒ bbab

Flip LHS and RHS.

Defines rule #3.