Certificate for #13210 ⟨a, b | abb=aba, bab=aa⟩

Completion settings:

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

[1] aba=abb

Axiom: abb=aba.

Flip LHS and RHS.

Defines rule #4.

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

[2] aa=bab

Axiom: bab=aa.

Flip LHS and RHS.

Defines rule #3.

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

[3] abbb=babb

Overlap of [2] aa=bab with [2] aa=bab:

a a aa

Critical pair: abab=baba.

Reduce LHS:

[1]	(aba)b
	⇒ abbb

Reduce RHS:

[1]	b(aba)
	⇒ babb

Defines rule #2.

Referenced by [5], [6].

[4] abbab=abba

Overlap of [1] aba=abb with [2] aa=bab:

ab a aa

Critical pair: abbab=abba.

Referenced by [5].

[5] abba=bbbabb

Overlap of [1] aba=abb with [3] abbb=babb:

ab a abbb

Critical pair: abbabb=abbbbb.

Reduce LHS:

[4]	(abbab)b
[4]	⇒ (abbab)
	⇒ abba

Reduce RHS:

[3]	(abbb)bb
[3]	⇒ b(abbb)b
[3]	⇒ bb(abbb)
	⇒ bbbabb

Referenced by [7].

[6] bbbabb=bbabb

Overlap of [2] aa=bab with [3] abbb=babb:

a a abbb

Critical pair: ababb=babbbb.

Reduce LHS:

[1]	(aba)bb
[3]	⇒ (abbb)b
[3]	⇒ b(abbb)
	⇒ bbabb

Reduce RHS:

[3]	b(abbb)b
[3]	⇒ bb(abbb)
	⇒ bbbabb

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] abba=bbabb

Simplify [5] abba=bbbabb.

Reduce RHS:

[6]	(bbbabb)
	⇒ bbabb

Defines rule #5.