Certificate for #25698 ⟨a, b | aa=a, baba=abab⟩

Completion settings:

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

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [6], [7].

[2] baba=abab

Axiom: baba=abab.

Referenced by [4].

[3] aba=c

Axiom: aba=c.

Defines rule #6.

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

[4] baba=cb

Simplify [2] baba=abab.

Reduce RHS:

[3]	(aba)b
	⇒ cb

Referenced by [5].

[5] bc=cb

Overlap of [4] baba=cb with [3] aba=c:

b aba aba

Critical pair: bc=cb.

Referenced by [8], [9].

[6] ac=c

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

a a aba

Critical pair: ac=aba.

Reduce RHS:

[3]	(aba)
	⇒ c

Defines rule #2.

Referenced by [8].

[7] ca=c

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

ab a aa

Critical pair: aba=ca.

Reduce LHS:

[3]	(aba)
	⇒ c

Flip LHS and RHS.

Defines rule #3.

[8] cb=cc

Overlap of [3] aba=c with [6] ac=c:

ab a ac

Critical pair: abc=cc.

Reduce LHS:

[5]	a(bc)
[6]	⇒ (ac)b
	⇒ cb

Defines rule #4.

Referenced by [9].

[9] bc=cc

Simplify [5] bc=cb.

Reduce RHS:

[8]	(cb)
	⇒ cc

Defines rule #5.