Certificate for #25678 ⟨a, b | aa=a, abba=abab⟩

Completion settings:

Auxiliary generators:
1. c = ab
Reduction order:
- Left-to-right shortlex with a < c < b

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [6], [7].

[2] abba=abab

Axiom: abba=abab.

Referenced by [4].

[3] ab=c

Axiom: ab=c.

Defines rule #3.

Referenced by [4], [5], [6], [8].

[4] abba=cc

Simplify [2] abba=abab.

Reduce RHS:

[3]	(ab)ab
[3]	⇒ c(ab)
	⇒ cc

Referenced by [5].

[5] cba=cc

Overlap of [4] abba=cc with [3] ab=c:

abba ab

Critical pair: cba=cc.

Defines rule #6.

Referenced by [7], [8], [9].

[6] ac=c

Overlap of [1] aa=a with [3] ab=c:

a a ab

Critical pair: ac=ab.

Reduce RHS:

[3]	(ab)
	⇒ c

Defines rule #2.

Referenced by [9].

[7] cca=cc

Overlap of [5] cba=cc with [1] aa=a:

cb a aa

Critical pair: cba=cca.

Reduce LHS:

[5]	(cba)
	⇒ cc

Flip LHS and RHS.

Defines rule #4.

[8] cbc=ccb

Overlap of [5] cba=cc with [3] ab=c:

cb a ab

Critical pair: cbc=ccb.

Referenced by [9], [10].

[9] ccb=ccc

Overlap of [5] cba=cc with [6] ac=c:

cb a ac

Critical pair: cbc=ccc.

Reduce LHS:

[8]	(cbc)
	⇒ ccb

Defines rule #5.

Referenced by [10].

[10] cbc=ccc

Simplify [8] cbc=ccb.

Reduce RHS:

[9]	(ccb)
	⇒ ccc

Defines rule #7.