Certificate for #2184 ⟨a, b | aaabbaa=aab⟩

Completion settings:

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

[1] aaabbaa=aab

Axiom: aaabbaa=aab.

Referenced by [3].

[2] bbaa=c

Axiom: bbaa=c.

Defines rule #10.

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

[3] aab=aaac

Overlap of [1] aaabbaa=aab with [2] bbaa=c:

aaa bbaa bbaa

Critical pair: aaac=aab.

Flip LHS and RHS.

Defines rule #8.

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

[4] cb=cac

Overlap of [2] bbaa=c with [3] aab=aaac:

bb aa aab

Critical pair: bbaaac=cb.

Reduce LHS:

[2]	(bbaa)ac
	⇒ cac

Flip LHS and RHS.

Defines rule #7.

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

[5] cab=caac

Overlap of [2] bbaa=c with [3] aab=aaac:

bba a aab

Critical pair: bbaaaac=cab.

Reduce LHS:

[2]	(bbaa)aac
	⇒ caac

Flip LHS and RHS.

Defines rule #9.

Referenced by [8].

[6] aaacacaa=aac

Overlap of [3] aab=aaac with [2] bbaa=c:

aa b bbaa

Critical pair: aac=aaacbaa.

Reduce RHS:

[4]	aaa(cb)aa
	⇒ aaacacaa

Flip LHS and RHS.

Defines rule #3.

Referenced by [9].

[7] cacacaa=cc

Overlap of [4] cb=cac with [2] bbaa=c:

c b bbaa

Critical pair: cc=cacbaa.

Reduce RHS:

[4]	ca(cb)aa
	⇒ cacacaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [10].

[8] caacacaa=cac

Overlap of [5] cab=caac with [2] bbaa=c:

ca b bbaa

Critical pair: cac=caacbaa.

Reduce RHS:

[4]	caa(cb)aa
	⇒ caacacaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [9], [10], [11].

[9] aaccacaa=aaacacac

Overlap of [6] aaacacaa=aac with [8] caacacaa=cac:

aaaca caa caacacaa

Critical pair: aaacacac=aaccacaa.

Flip LHS and RHS.

Defines rule #4.

[10] cccacaa=cacacac

Overlap of [7] cacacaa=cc with [8] caacacaa=cac:

caca caa caacacaa

Critical pair: cacacac=cccacaa.

Flip LHS and RHS.

Defines rule #2.

[11] caccacaa=caacacac

Overlap of [8] caacacaa=cac with [8] caacacaa=cac:

caaca caa caacacaa

Critical pair: caacacac=caccacaa.

Flip LHS and RHS.

Defines rule #6.