Certificate for #1001 ⟨a, b | abbbbba=ab

Completion settings:

[1] abbbbba=ab

Axiom: abbbbba=ab.

Referenced by [3].

[2] abbbbb=c

Axiom: abbbbb=c.

Referenced by [3], [4].

[3] ab=ca

Overlap of [1] abbbbba=ab with [2] abbbbb=c:

abbbbba abbbbb

Critical pair: ca=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] ccccca=c

Overlap of [2] abbbbb=c with [3] ab=ca:

abbbbb ab

Critical pair: cabbbb=c.

Reduce LHS:

[3]c(ab)bbb
[3]cc(ab)bb
[3]ccc(ab)b
[3]cccc(ab)
ccccca

Defines rule #3.

Referenced by [5].

[5] cb=cc

Overlap of [4] ccccca=c with [3] ab=ca:

ccccc a ab

Critical pair: cccccca=cb.

Reduce LHS:

[4]c(ccccca)
cc

Flip LHS and RHS.

Defines rule #1.