Certificate for #25188 ⟨a, b | aa=a, ababa=bab⟩

Completion settings:

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

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [6].

[2] ababa=bab

Axiom: ababa=bab.

Referenced by [4].

[3] ba=c

Axiom: ba=c.

Defines rule #4.

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

[4] ababa=cb

Simplify [2] ababa=bab.

Reduce RHS:

[3]	(ba)b
	⇒ cb

Referenced by [5].

[5] acc=cb

Overlap of [4] ababa=cb with [3] ba=c:

a baba ba

Critical pair: acba=cb.

Reduce LHS:

[3]	ac(ba)
	⇒ acc

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

[6] ca=c

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

b a aa

Critical pair: ba=ca.

Reduce LHS:

[3]	(ba)
	⇒ c

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[7] bcb=ccc

Overlap of [3] ba=c with [5] acc=cb:

b a acc

Critical pair: bcb=ccc.

Referenced by [9].

[8] cb=cc

Overlap of [5] acc=cb with [6] ca=c:

ac c ca

Critical pair: acc=cba.

Reduce LHS:

[5]	(acc)
	⇒ cb

Reduce RHS:

[3]	c(ba)
	⇒ cc

Defines rule #3.

Referenced by [9], [10].

[9] bcc=ccc

Simplify [7] bcb=ccc.

Reduce LHS:

[8]	b(cb)
	⇒ bcc

Defines rule #6.

[10] acc=cc

Simplify [5] acc=cb.

Reduce RHS:

[8]	(cb)
	⇒ cc

Defines rule #5.