Certificate for #19812 ⟨a, b | aaa=a, abab=bba⟩

Completion settings:

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

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3].

[2] bba=abab

Axiom: abab=bba.

Flip LHS and RHS.

Defines rule #2.

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

[3] ababaa=abab

Overlap of [2] bba=abab with [1] aaa=a:

bb a aaa

Critical pair: bba=ababaa.

Reduce LHS:

[2]	(bba)
	⇒ abab

Flip LHS and RHS.

Defines rule #3.

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

[4] abaabaababa=abaababb

Overlap of [2] bba=abab with [3] ababaa=abab:

bb a ababaa

Critical pair: bbabab=ababbabaa.

Reduce LHS:

[2]	(bba)bab
[2]	⇒ aba(bba)b
	⇒ abaababb

Reduce RHS:

[2]	aba(bba)baa
[2]	⇒ abaaba(bba)a
	⇒ abaabaababa

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] abaababababa=abaababbb

Overlap of [3] ababaa=abab with [4] abaabaababa=abaababb:

ab abaa abaabaababa

Critical pair: ababaababb=ababbaababa.

Reduce LHS:

[3]	(ababaa)babb
[2]	⇒ aba(bba)bb
	⇒ abaababbb

Reduce RHS:

[2]	aba(bba)ababa
	⇒ abaababababa

Flip LHS and RHS.

Defines rule #5.

Referenced by [6].

[6] abaabaabaabaabab=abaababbbb

Overlap of [3] ababaa=abab with [5] abaababababa=abaababbb:

ab abaa abaababababa

Critical pair: ababaababbb=ababbabababa.

Reduce LHS:

[3]	(ababaa)babbb
[2]	⇒ aba(bba)bbb
	⇒ abaababbbb

Reduce RHS:

[2]	aba(bba)bababa
[2]	⇒ abaaba(bba)baba
[2]	⇒ abaabaaba(bba)ba
[2]	⇒ abaabaabaaba(bba)
	⇒ abaabaabaabaabab

Flip LHS and RHS.

Defines rule #6.