Certificate for #1592 ⟨a, b | aaa=ab, baa=a⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(b) = 0; deg(a) = 1

[1] aaa=ab

Axiom: aaa=ab.

Referenced by [3], [4].

[2] baa=a

Axiom: baa=a.

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

[3] aba=aab

Overlap of [1] aaa=ab with [1] aaa=ab:

a aa aaa

Critical pair: aab=aba.

Flip LHS and RHS.

Referenced by [5], [6].

[4] aa=bab

Overlap of [2] baa=a with [1] aaa=ab:

b aa aaa

Critical pair: bab=aa.

Flip LHS and RHS.

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

[5] bab=abb

Overlap of [2] baa=a with [4] aa=bab:

ba a aa

Critical pair: babab=aa.

Reduce LHS:

[3]	b(aba)b
[2]	⇒ (baa)bb
	⇒ abb

Reduce RHS:

[4]	(aa)
	⇒ bab

Flip LHS and RHS.

Referenced by [6], [7].

[6] abbb=a

Overlap of [5] bab=abb with [2] baa=a:

ba b baa

Critical pair: baa=abbaa.

Reduce LHS:

[2]	(baa)
	⇒ a

Reduce RHS:

[2]	ab(baa)
[3]	⇒ (aba)
[4]	⇒ (aa)b
[5]	⇒ (bab)b
	⇒ abbb

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] ba=ab

Overlap of [5] bab=abb with [6] abbb=a:

b ab abbb

Critical pair: ba=abbbb.

Reduce RHS:

[6]	(abbb)b
	⇒ ab

Defines rule #2.

Referenced by [8].

[8] aa=abb

Simplify [4] aa=bab.

Reduce RHS:

[7]	(ba)b
	⇒ abb

Defines rule #3.