Certificate for #3774 ⟨a, b | abababbaba=a⟩

Back:⟨a, b | abababbaba=a⟩

Completion settings:

[1] abababbaba=a

Axiom: abababbaba=a.

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

[2] ababbaba=abababba

Overlap of [1] abababbaba=a with [1] abababbaba=a:

abababb aba abababbaba

Critical pair: abababba=ababbaba.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abbaba=ababba

Overlap of [2] ababbaba=abababba with [1] abababbaba=a:

ababb aba abababbaba

Critical pair: ababba=abababbababbaba.

Reduce RHS:

[1](abababbaba)bbaba
⇒ abbaba

Flip LHS and RHS.

Defines rule #1.

[4] ababababba=a

Overlap of [1] abababbaba=a with [2] ababbaba=abababba:

ab ababbaba ababbaba

Critical pair: ababababba=a.

Defines rule #2.