Certificate for #2049 ⟨a, b | ababaaab=aa⟩

Back:⟨a, b | ababaaab=aa⟩

Completion settings:

[1] ababaaab=aa

Axiom: ababaaab=aa.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

Referenced by [3].

[3] ccaac=aa

Overlap of [1] ababaaab=aa with [2] ab=c:

ababaaab ab

Critical pair: cabaaab=aa.

Reduce LHS:

[2]c(ab)aaab
[2]⇒ ccaa(ab)
⇒ ccaac

Defines rule #2.

Referenced by [4], [5].

[4] aacaac=ccaaaa

Overlap of [3] ccaac=aa with [3] ccaac=aa:

ccaa c ccaac

Critical pair: ccaaaa=aacaac.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] aaaac=ccccaaaa

Overlap of [3] ccaac=aa with [4] aacaac=ccaaaa:

cc aac aacaac

Critical pair: ccccaaaa=aaaac.

Flip LHS and RHS.

Defines rule #3.