Certificate for #24675 ⟨a, b | aa=a, abbabb=ba⟩

Completion settings:

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

[1] aa=a

Axiom: aa=a.

Defines rule #3.

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

[2] abbabb=ba

Axiom: abbabb=ba.

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

[3] aba=ba

Overlap of [1] aa=a with [2] abbabb=ba:

a a abbabb

Critical pair: aba=abbabb.

Reduce RHS:

[2]	(abbabb)
	⇒ ba

Defines rule #4.

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

[4] abbba=babb

Overlap of [2] abbabb=ba with [2] abbabb=ba:

abb abb abbabb

Critical pair: abbba=baabb.

Reduce RHS:

[1]	b(aa)bb
	⇒ babb

Referenced by [7].

[5] abba=bba

Overlap of [3] aba=ba with [2] abbabb=ba:

ab a abbabb

Critical pair: abba=babbabb.

Reduce RHS:

[2]	b(abbabb)
	⇒ bba

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

[6] abbbba=ba

Overlap of [2] abbabb=ba with [5] abba=bba:

abb abb abba

Critical pair: abbbba=baa.

Reduce RHS:

[1]	b(aa)
	⇒ ba

Referenced by [9].

[7] bbba=babb

Overlap of [3] aba=ba with [5] abba=bba:

ab a abba

Critical pair: abbba=babba.

Reduce LHS:

[4]	(abbba)
	⇒ babb

Reduce RHS:

[5]	b(abba)
	⇒ bbba

Flip LHS and RHS.

Referenced by [8], [9].

[8] bba=babbbb

Overlap of [2] abbabb=ba with [7] bbba=babb:

abba bb bbba

Critical pair: abbababb=baba.

Reduce LHS:

[5]	(abba)babb
[3]	⇒ bb(aba)bb
[7]	⇒ (bbba)bb
	⇒ babbbb

Reduce RHS:

[3]	b(aba)
	⇒ bba

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[9] babbbbbb=ba

Simplify [6] abbbba=ba.

Reduce LHS:

[7]	ab(bbba)
[5]	⇒ (abba)bb
[8]	⇒ (bba)bb
	⇒ babbbbbb

Defines rule #1.