Certificate for #4050 ⟨a, b | aaabbbbaa=ab⟩

Completion settings:

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

[1] aaabbbbaa=ab

Axiom: aaabbbbaa=ab.

Referenced by [3].

[2] abbbb=c

Axiom: abbbb=c.

Referenced by [3], [4].

[3] ab=aacaa

Overlap of [1] aaabbbbaa=ab with [2] abbbb=c:

aa abbbbaa abbbb

Critical pair: aacaa=ab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] aacaaacaaacaaacaa=c

Overlap of [2] abbbb=c with [3] ab=aacaa:

abbbb ab

Critical pair: aacaabbb=c.

Reduce LHS:

[3]	aaca(ab)bb
[3]	⇒ aacaaaca(ab)b
[3]	⇒ aacaaacaaaca(ab)
	⇒ aacaaacaaacaaacaa

Defines rule #3.

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

[5] cb=cacaa

Overlap of [4] aacaaacaaacaaacaa=c with [3] ab=aacaa:

aacaaacaaacaaaca a ab

Critical pair: aacaaacaaacaaacaaacaa=cb.

Reduce LHS:

[4]	(aacaaacaaacaaacaa)acaa
	⇒ cacaa

Flip LHS and RHS.

Referenced by [8].

[6] cacaa=aacac

Overlap of [4] aacaaacaaacaaacaa=c with [4] aacaaacaaacaaacaa=c:

aaca aacaaacaaacaa aacaaacaaacaaacaa

Critical pair: aacac=cacaa.

Flip LHS and RHS.

Defines rule #1.

Referenced by [8].

[7] ccaaacaaacaaacaa=aacaaacaaacaaacc

Overlap of [4] aacaaacaaacaaacaa=c with [4] aacaaacaaacaaacaa=c:

aacaaacaaacaaac aa aacaaacaaacaaacaa

Critical pair: aacaaacaaacaaacc=ccaaacaaacaaacaa.

Flip LHS and RHS.

Defines rule #2.

[8] cb=aacac

Simplify [5] cb=cacaa.

Reduce RHS:

[6]	(cacaa)
	⇒ aacac

Defines rule #5.