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

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 #5.

Referenced by [2], [3], [4], [7].

[2] abab=aaa

Axiom: abab=bb.

Reduce RHS:

[1]	(bb)
	⇒ aaa

Defines rule #6.

Referenced by [4], [5].

[3] aaab=baaa

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

b b bb

Critical pair: baaa=aaab.

Flip LHS and RHS.

Defines rule #4.

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

[4] abaaaa=baaa

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

aba b bb

Critical pair: abaaaa=aaab.

Reduce RHS:

[3]	(aaab)
	⇒ baaa

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

[5] babaaa=aaaaa

Overlap of [3] aaab=baaa with [2] abab=aaa:

aa ab abab

Critical pair: aaaaa=baaaab.

Reduce RHS:

[3]	ba(aaab)
	⇒ babaaa

Flip LHS and RHS.

Referenced by [7].

[6] aabaaa=baaaaaaa

Overlap of [3] aaab=baaa with [4] abaaaa=baaa:

aa ab abaaaa

Critical pair: aabaaa=baaaaaaa.

Referenced by [7], [8].

[7] aaaaaaaaaaa=aaaaa

Overlap of [4] abaaaa=baaa with [3] aaab=baaa:

abaa aa aaab

Critical pair: abaabaaa=baaaab.

Reduce LHS:

[6]	ab(aabaaa)
[1]	⇒ a(bb)aaaaaaa
	⇒ aaaaaaaaaaa

Reduce RHS:

[3]	ba(aaab)
[5]	⇒ (babaaa)
	⇒ aaaaa

Defines rule #1.

[8] abaaa=baaaaaaaa

Overlap of [6] aabaaa=baaaaaaa with [4] abaaaa=baaa:

a abaaa abaaaa

Critical pair: abaaa=baaaaaaaa.

Defines rule #3.

Referenced by [9].

[9] baaaaaaaaa=baaa

Overlap of [4] abaaaa=baaa with [8] abaaa=baaaaaaaa:

abaaaa abaaa

Critical pair: baaaaaaaaa=baaa.

Defines rule #2.