Certificate for #4571 ⟨a, b | aaabbbaa=bba⟩

Back:⟨a, b | aaabbbaa=bba⟩

Completion settings:

[1] aaabbbaa=bba

Axiom: aaabbbaa=bba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #4.

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

[3] aaabbbaa=c

Simplify [1] aaabbbaa=bba.

Reduce RHS:

[2](bba)
⇒ c

Referenced by [4].

[4] aaabca=c

Overlap of [3] aaabbbaa=c with [2] bba=c:

aaab bbaa bba

Critical pair: aaabca=c.

Defines rule #2.

Referenced by [5], [6].

[5] bbc=caabca

Overlap of [2] bba=c with [4] aaabca=c:

bb a aaabca

Critical pair: bbc=caabca.

Defines rule #3.

[6] aaabcc=caabca

Overlap of [4] aaabca=c with [4] aaabca=c:

aaabc a aaabca

Critical pair: aaabcc=caabca.

Defines rule #1.