Certificate for #2623 ⟨a, b | abbaab=baba⟩

Completion settings:

Auxiliary generators:
1. c = ba
2. d = ab
Reduction order:
- Left-to-right recursive path with deg(b) = 0; deg(d) = deg(c) = 1, d < c; deg(a) = 2

[1] abbaab=baba

Axiom: abbaab=baba.

Referenced by [4].

[2] ba=c

Axiom: ba=c.

Defines rule #5.

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

[3] ab=d

Axiom: ab=d.

Defines rule #4.

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

[4] abbaab=cc

Simplify [1] abbaab=baba.

Reduce RHS:

[2]	(ba)ba
[2]	⇒ c(ba)
	⇒ cc

Referenced by [5].

[5] dcd=cc

Overlap of [4] abbaab=cc with [3] ab=d:

abbaab ab

Critical pair: dbaab=cc.

Reduce LHS:

[2]	d(ba)ab
[3]	⇒ dc(ab)
	⇒ dcd

Defines rule #2.

Referenced by [8], [9].

[6] cb=bd

Overlap of [2] ba=c with [3] ab=d:

b a ab

Critical pair: bd=cb.

Flip LHS and RHS.

Defines rule #1.

[7] da=ac

Overlap of [3] ab=d with [2] ba=c:

a b ba

Critical pair: ac=da.

Flip LHS and RHS.

Defines rule #6.

Referenced by [9].

[8] cccd=dccc

Overlap of [5] dcd=cc with [5] dcd=cc:

dc d dcd

Critical pair: dccc=cccd.

Flip LHS and RHS.

Defines rule #3.

[9] cca=dcac

Overlap of [5] dcd=cc with [7] da=ac:

dc d da

Critical pair: dcac=cca.

Flip LHS and RHS.

Defines rule #7.