Certificate for #5902 ⟨a, b | ababba=bbaab⟩

Back:⟨a, b | ababba=bbaab⟩

Completion settings:

[1] ababba=bbaab

Axiom: ababba=bbaab.

Referenced by [3].

[2] bbaab=c

Axiom: bbaab=c.

Defines rule #4.

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

[3] ababba=c

Simplify [1] ababba=bbaab.

Reduce RHS:

[2](bbaab)
⇒ c

Defines rule #5.

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

[4] bbaac=cbaab

Overlap of [2] bbaab=c with [2] bbaab=c:

bbaa b bbaab

Critical pair: bbaac=cbaab.

Defines rule #3.

[5] ababbc=cbabba

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

ababb a ababba

Critical pair: ababbc=cbabba.

Defines rule #6.

[6] abac=cab

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

aba bba bbaab

Critical pair: abac=cab.

Defines rule #1.

[7] bbac=cabba

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

bba ab ababba

Critical pair: bbac=cabba.

Defines rule #2.