Certificate for #16060 ⟨a, b | aaa=bb, abab=aa⟩

Completion settings:

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

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4], [8].

[2] abab=aa

Axiom: abab=aa.

Defines rule #5.

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

[3] aaab=baaa

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

b b bb

Critical pair: baaa=aaab.

Flip LHS and RHS.

Referenced by [5], [6].

[4] aab=abaaaa

Overlap of [2] abab=aa with [1] bb=aaa:

aba b bb

Critical pair: abaaaa=aab.

Flip LHS and RHS.

Referenced by [6], [7].

[5] abaa=baaa

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

ab ab abab

Critical pair: abaa=aaab.

Reduce RHS:

[3]	(aaab)
	⇒ baaa

Defines rule #2.

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

[6] baaaaaa=baaa

Simplify [3] aaab=baaa.

Reduce LHS:

[4]	a(aab)
[5]	⇒ a(abaa)aa
[5]	⇒ (abaa)aaa
	⇒ baaaaaa

Referenced by [8].

[7] aab=baaaaa

Simplify [4] aab=abaaaa.

Reduce RHS:

[5]	(abaa)aa
	⇒ baaaaa

Defines rule #3.

Referenced by [8].

[8] aaaaaa=aaa

Overlap of [7] aab=baaaaa with [2] abab=aa:

a ab abab

Critical pair: aaa=baaaaaab.

Reduce RHS:

[6]	(baaaaaa)b
[7]	⇒ ba(aab)
[5]	⇒ b(abaa)aaa
[6]	⇒ b(baaaaaa)
[1]	⇒ (bb)aaa
	⇒ aaaaaa

Flip LHS and RHS.

Defines rule #1.