Certificate for #16295 ⟨a, b | aab=bb, abab=ba⟩

Completion settings:

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

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

Defines rule #3.

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

[2] abab=ba

Axiom: abab=ba.

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

[3] baab=aaaab

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

b b bb

Critical pair: baab=aabb.

Reduce RHS:

[1]	aa(bb)
	⇒ aaaab

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

[4] abaaab=bab

Overlap of [2] abab=ba with [1] bb=aab:

aba b bb

Critical pair: abaaab=bab.

Referenced by [7].

[5] aaaba=aaaab

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

ab ab abab

Critical pair: abba=baab.

Reduce LHS:

[1]	a(bb)a
	⇒ aaaba

Reduce RHS:

[3]	(baab)
	⇒ aaaab

Referenced by [6], [8].

[6] baba=aaaaaaab

Overlap of [3] baab=aaaab with [2] abab=ba:

ba ab abab

Critical pair: baba=aaaabab.

Reduce RHS:

[5]	a(aaaba)b
[1]	⇒ aaaaa(bb)
	⇒ aaaaaaab

Referenced by [8].

[7] baa=aba

Overlap of [4] abaaab=bab with [4] abaaab=bab:

abaa ab abaaab

Critical pair: abaabab=babaaab.

Reduce LHS:

[2]	aba(abab)
[2]	⇒ (abab)a
	⇒ baa

Reduce RHS:

[4]	b(abaaab)
[1]	⇒ (bb)ab
[2]	⇒ a(abab)
	⇒ aba

Referenced by [8], [9].

[8] aaaaaaab=aaaab

Overlap of [1] bb=aab with [7] baa=aba:

b b baa

Critical pair: baba=aabaa.

Reduce LHS:

[6]	(baba)
	⇒ aaaaaaab

Reduce RHS:

[7]	aa(baa)
[5]	⇒ (aaaba)
	⇒ aaaab

Defines rule #1.

[9] ba=aaaab

Overlap of [3] baab=aaaab with [7] baa=aba:

baab baa

Critical pair: abab=aaaab.

Reduce LHS:

[2]	(abab)
	⇒ ba

Defines rule #2.