Certificate for #1662 ⟨a, b, c | aab=ba, bac=1⟩

Completion settings:

Auxiliary generators:
1. d = ab
2. e = ad
Reduction order:
- Right-to-left recursive path with deg(a) = deg(c) = 0, a < c; deg(e) = deg(d) = deg(b) = 1, e < d < b

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Referenced by [2], [5].

[2] aabc=1

Axiom: bac=1.

Reduce LHS:

[1]	(ba)c
	⇒ aabc

Referenced by [6].

[3] ab=d

Axiom: ab=d.

Defines rule #5.

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

[4] ad=e

Axiom: ad=e.

Defines rule #3.

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

[5] ba=e

Simplify [1] ba=aab.

Reduce RHS:

[3]	a(ab)
[4]	⇒ (ad)
	⇒ e

Defines rule #6.

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

[6] ec=1

Overlap of [2] aabc=1 with [3] ab=d:

a abc ab

Critical pair: adc=1.

Reduce LHS:

[4]	(ad)c
	⇒ ec

Defines rule #2.

[7] eb=bd

Overlap of [5] ba=e with [3] ab=d:

b a ab

Critical pair: bd=eb.

Flip LHS and RHS.

Defines rule #8.

[8] ed=be

Overlap of [5] ba=e with [4] ad=e:

b a ad

Critical pair: be=ed.

Flip LHS and RHS.

Defines rule #7.

[9] da=ae

Overlap of [3] ab=d with [5] ba=e:

a b ba

Critical pair: ae=da.

Flip LHS and RHS.

Defines rule #4.

Referenced by [10].

[10] ea=aae

Overlap of [4] ad=e with [9] da=ae:

a d da

Critical pair: aae=ea.

Flip LHS and RHS.

Defines rule #1.