Certificate for #4683 ⟨a, b | aabbaaab=baa⟩

Completion settings:

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

[1] aabbaaab=baa

Axiom: aabbaaab=baa.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #7.

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

[3] cbba=d

Axiom: cbba=d.

Defines rule #4.

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

[4] aabbaaab=bc

Simplify [1] aabbaaab=baa.

Reduce RHS:

[2]	b(aa)
	⇒ bc

Referenced by [5].

[5] bc=dcb

Overlap of [4] aabbaaab=bc with [2] aa=c:

aabbaaab aa

Critical pair: cbbaaab=bc.

Reduce LHS:

[3]	(cbba)aab
[2]	⇒ d(aa)b
	⇒ dcb

Flip LHS and RHS.

Defines rule #1.

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

[6] ca=ac

Overlap of [2] aa=c with [2] aa=c:

a a aa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7].

[7] dcba=bac

Overlap of [5] bc=dcb with [6] ca=ac:

b c ca

Critical pair: bac=dcba.

Flip LHS and RHS.

Defines rule #5.

[8] da=cbdcb

Overlap of [3] cbba=d with [2] aa=c:

cbb a aa

Critical pair: cbbc=da.

Reduce LHS:

[5]	cb(bc)
	⇒ cbdcb

Flip LHS and RHS.

Defines rule #2.

[9] dcbbba=bd

Overlap of [5] bc=dcb with [3] cbba=d:

b c cbba

Critical pair: bd=dcbbba.

Flip LHS and RHS.

Defines rule #6.