Certificate for #4536 ⟨a, b | aaabbaaa=aab⟩

Completion settings:

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

[1] aaabbaaa=aab

Axiom: aaabbaaa=aab.

Referenced by [3].

[2] bbaaa=c

Axiom: bbaaa=c.

Defines rule #10.

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

[3] aab=aaac

Overlap of [1] aaabbaaa=aab with [2] bbaaa=c:

aaa bbaaa bbaaa

Critical pair: aaac=aab.

Flip LHS and RHS.

Defines rule #8.

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

[4] cb=cac

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

bba aa aab

Critical pair: bbaaaac=cb.

Reduce LHS:

[2]	(bbaaa)ac
	⇒ cac

Flip LHS and RHS.

Defines rule #7.

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

[5] cab=caac

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

bbaa a aab

Critical pair: bbaaaaac=cab.

Reduce LHS:

[2]	(bbaaa)aac
	⇒ caac

Flip LHS and RHS.

Defines rule #9.

Referenced by [8].

[6] aaacacaaa=aac

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

aa b bbaaa

Critical pair: aac=aaacbaaa.

Reduce RHS:

[4]	aaa(cb)aaa
	⇒ aaacacaaa

Flip LHS and RHS.

Defines rule #3.

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

[7] cacacaaa=cc

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

c b bbaaa

Critical pair: cc=cacbaaa.

Reduce RHS:

[4]	ca(cb)aaa
	⇒ cacacaaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [11].

[8] caacacaaa=cac

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

ca b bbaaa

Critical pair: cac=caacbaaa.

Reduce RHS:

[4]	caa(cb)aaa
	⇒ caacacaaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [12].

[9] bbaac=ccacaaa

Overlap of [2] bbaaa=c with [6] aaacacaaa=aac:

bb aaa aaacacaaa

Critical pair: bbaac=ccacaaa.

Defines rule #11.

[10] aaccacaaa=aaacacaac

Overlap of [6] aaacacaaa=aac with [6] aaacacaaa=aac:

aaacac aaa aaacacaaa

Critical pair: aaacacaac=aaccacaaa.

Flip LHS and RHS.

Defines rule #4.

[11] cccacaaa=cacacaac

Overlap of [7] cacacaaa=cc with [6] aaacacaaa=aac:

cacac aaa aaacacaaa

Critical pair: cacacaac=cccacaaa.

Flip LHS and RHS.

Defines rule #2.

[12] caccacaaa=caacacaac

Overlap of [8] caacacaaa=cac with [6] aaacacaaa=aac:

caacac aaa aaacacaaa

Critical pair: caacacaac=caccacaaa.

Flip LHS and RHS.

Defines rule #6.