Certificate for #3768 ⟨a, b | abababaaab=b⟩

Back:⟨a, b | abababaaab=b⟩

Completion settings:

[1] abababaaab=b

Axiom: abababaaab=b.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Referenced by [3], [4].

[3] b=cccaac

Overlap of [1] abababaaab=b with [2] ab=c:

abababaaab ab

Critical pair: cababaaab=b.

Reduce LHS:

[2]c(ab)abaaab
[2]⇒ cc(ab)aaab
[2]⇒ cccaa(ab)
⇒ cccaac

Flip LHS and RHS.

Defines rule #4.

Referenced by [4].

[4] acccaac=c

Overlap of [2] ab=c with [3] b=cccaac:

a b b

Critical pair: acccaac=c.

Defines rule #3.

Referenced by [5], [6].

[5] acccac=cccaac

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

accca ac acccaac

Critical pair: acccac=cccaac.

Defines rule #2.

Referenced by [6].

[6] acccc=cccac

Overlap of [5] acccac=cccaac with [4] acccaac=c:

accc ac acccaac

Critical pair: acccc=cccaacccaac.

Reduce RHS:

[4]ccca(acccaac)
⇒ cccac

Defines rule #1.