Certificate for #2613 ⟨a, b | ababba=bbba

Completion settings:

[1] ababba=bbba

Axiom: ababba=bbba.

Referenced by [3].

[2] bbba=c

Axiom: bbba=c.

Defines rule #1.

Referenced by [3], [5].

[3] ababba=c

Simplify [1] ababba=bbba.

Reduce RHS:

[2](bbba)
c

Defines rule #2.

Referenced by [4], [5].

[4] ababbc=cbabba

Overlap of [3] ababba=c with [3] ababba=c:

ababb a ababba

Critical pair: ababbc=cbabba.

Defines rule #4.

[5] bbbc=cbabba

Overlap of [2] bbba=c with [3] ababba=c:

bbb a ababba

Critical pair: bbbc=cbabba.

Defines rule #3.