Certificate for #13198 ⟨a, b | abb=aab, bab=aa⟩

Completion settings:

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

[1] aab=abb

Axiom: abb=aab.

Flip LHS and RHS.

Referenced by [3].

[2] aa=bab

Axiom: bab=aa.

Flip LHS and RHS.

Defines rule #3.

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

[3] babb=abb

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

aab aa

Critical pair: babb=abb.

Defines rule #2.

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

[4] baba=abab

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

a a aa

Critical pair: abab=baba.

Flip LHS and RHS.

Defines rule #6.

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

[5] abbbb=abbb

Overlap of [3] babb=abb with [3] babb=abb:

bab b babb

Critical pair: bababb=abbabb.

Reduce LHS:

[4]	(baba)bb
[3]	⇒ a(babb)b
[2]	⇒ (aa)bbb
[3]	⇒ (babb)bb
	⇒ abbbb

Reduce RHS:

[3]	ab(babb)
[3]	⇒ a(babb)
[2]	⇒ (aa)bb
[3]	⇒ (babb)b
	⇒ abbb

Defines rule #1.

Referenced by [7].

[6] abbba=abbab

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

ba ba baba

Critical pair: baabab=ababba.

Reduce LHS:

[2]	b(aa)bab
[3]	⇒ b(babb)ab
[3]	⇒ (babb)ab
	⇒ abbab

Reduce RHS:

[3]	a(babb)a
[2]	⇒ (aa)bba
[3]	⇒ (babb)ba
	⇒ abbba

Flip LHS and RHS.

Referenced by [7], [8].

[7] abbab=abbb

Overlap of [5] abbbb=abbb with [4] baba=abab:

abbb b baba

Critical pair: abbbabab=abbbaba.

Reduce LHS:

[6]	(abbba)bab
[3]	⇒ ab(babb)ab
[3]	⇒ a(babb)ab
[2]	⇒ (aa)bbab
[3]	⇒ (babb)bab
[6]	⇒ (abbba)b
[3]	⇒ ab(babb)
[3]	⇒ a(babb)
[2]	⇒ (aa)bb
[3]	⇒ (babb)b
	⇒ abbb

Reduce RHS:

[6]	(abbba)ba
[3]	⇒ ab(babb)a
[3]	⇒ a(babb)a
[2]	⇒ (aa)bba
[3]	⇒ (babb)ba
[6]	⇒ (abbba)
	⇒ abbab

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

[8] abbba=abbb

Simplify [6] abbba=abbab.

Reduce RHS:

[7]	(abbab)
	⇒ abbb

Defines rule #5.