Certificate for #6543 ⟨a, b | aaa=a, abab=ba⟩

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] abab=ba

Axiom: abab=ba.

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

[3] aaba=ba

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

aa a abab

Critical pair: aaba=abab.

Reduce RHS:

[2]	(abab)
	⇒ ba

Defines rule #2.

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

[4] abba=baab

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

ab ab abab

Critical pair: abba=baab.

Referenced by [6], [7].

[5] bab=aba

Overlap of [3] aaba=ba with [2] abab=ba:

a aba abab

Critical pair: aba=bab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7].

[6] bba=abaab

Overlap of [3] aaba=ba with [3] aaba=ba:

aab a aaba

Critical pair: aabba=baaba.

Reduce LHS:

[4]	a(abba)
	⇒ abaab

Reduce RHS:

[3]	b(aaba)
	⇒ bba

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

[7] baabb=baa

Overlap of [5] bab=aba with [6] bba=abaab:

ba b bba

Critical pair: baabaab=ababa.

Reduce LHS:

[3]	b(aaba)ab
[6]	⇒ (bba)ab
[3]	⇒ ab(aaba)b
[4]	⇒ (abba)b
	⇒ baabb

Reduce RHS:

[2]	(abab)a
	⇒ baa

Defines rule #5.