Certificate for #4797 ⟨a, b | abaababa=bba⟩

Back:⟨a, b | abaababa=bba⟩

Completion settings:

[1] abaababa=bba

Axiom: abaababa=bba.

Referenced by [3].

[2] ba=c

Axiom: ba=c.

Defines rule #1.

Referenced by [3], [4].

[3] abaababa=bc

Simplify [1] abaababa=bba.

Reduce RHS:

[2]b(ba)
⇒ bc

Referenced by [4].

[4] bc=acacc

Overlap of [3] abaababa=bc with [2] ba=c:

a baababa ba

Critical pair: acababa=bc.

Reduce LHS:

[2]aca(ba)ba
[2]⇒ acac(ba)
⇒ acacc

Flip LHS and RHS.

Defines rule #2.