Certificate for #16458 ⟨a, b | aba=bb, abba=bb⟩

Completion settings:

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

[1] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #2.

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

[2] aabaa=aba

Axiom: abba=bb.

Reduce LHS:

[1]	a(bb)a
	⇒ aabaa

Reduce RHS:

[1]	(bb)
	⇒ aba

Defines rule #1.

Referenced by [4].

[3] abab=baba

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

b b bb

Critical pair: baba=abab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] babaab=babaa

Overlap of [3] abab=baba with [3] abab=baba:

ab ab abab

Critical pair: abbaba=babaab.

Reduce LHS:

[1]	a(bb)aba
[2]	⇒ (aabaa)ba
[3]	⇒ (abab)a
	⇒ babaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [5], [6].

[5] babaaab=babaaa

Overlap of [3] abab=baba with [4] babaab=babaa:

a bab babaab

Critical pair: ababaa=babaaab.

Reduce LHS:

[3]	(abab)aa
	⇒ babaaa

Flip LHS and RHS.

Defines rule #6.

Referenced by [6].

[6] babaaaa=babaa

Overlap of [4] babaab=babaa with [1] bb=aba:

babaa b bb

Critical pair: babaaaba=babaab.

Reduce LHS:

[5]	(babaaab)a
	⇒ babaaaa

Reduce RHS:

[4]	(babaab)
	⇒ babaa

Defines rule #3.