Certificate for #16240 ⟨a, b | aab=ba, abbb=bb⟩

Completion settings:

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

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #1.

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

[2] abbb=bb

Axiom: abbb=bb.

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

[3] bbb=bb

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

b a abbb

Critical pair: bbb=aabbbb.

Reduce RHS:

[2]	a(abbb)b
[2]	⇒ (abbb)
	⇒ bb

Defines rule #3.

Referenced by [5], [7].

[4] aaaaaaaabb=aaaabb

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

abb b ba

Critical pair: abbaab=bba.

Reduce LHS:

[1]	ab(ba)ab
[1]	⇒ a(ba)abab
[1]	⇒ aaa(ba)bab
[1]	⇒ aaaaab(ba)b
[1]	⇒ aaaaa(ba)abb
[1]	⇒ aaaaaaa(ba)bb
[2]	⇒ aaaaaaaa(abbb)
	⇒ aaaaaaaabb

Reduce RHS:

[1]	b(ba)
[1]	⇒ (ba)ab
[1]	⇒ aa(ba)b
	⇒ aaaabb

Referenced by [5].

[5] aaaabb=aaabb

Overlap of [3] bbb=bb with [1] ba=aab:

bb b ba

Critical pair: bbaab=bba.

Reduce LHS:

[1]	b(ba)ab
[1]	⇒ (ba)abab
[1]	⇒ aa(ba)bab
[1]	⇒ aaaab(ba)b
[1]	⇒ aaaa(ba)abb
[1]	⇒ aaaaaa(ba)bb
[4]	⇒ (aaaaaaaabb)b
[2]	⇒ aaa(abbb)
	⇒ aaabb

Reduce RHS:

[1]	b(ba)
[1]	⇒ (ba)ab
[1]	⇒ aa(ba)b
	⇒ aaaabb

Flip LHS and RHS.

Referenced by [6], [7].

[6] aaabb=aabb

Overlap of [5] aaaabb=aaabb with [2] abbb=bb:

aaa abb abbb

Critical pair: aaabb=aaabbb.

Reduce RHS:

[2]	aa(abbb)
	⇒ aabb

Referenced by [7].

[7] aabb=abb

Overlap of [5] aaaabb=aaabb with [3] bbb=bb:

aaaa bb bbb

Critical pair: aaaabb=aaabbb.

Reduce LHS:

[5]	(aaaabb)
[6]	⇒ (aaabb)
	⇒ aabb

Reduce RHS:

[6]	(aaabb)b
[2]	⇒ a(abbb)
	⇒ abb

Referenced by [8].

[8] abb=bb

Overlap of [7] aabb=abb with [2] abbb=bb:

a abb abbb

Critical pair: abb=abbb.

Reduce RHS:

[2]	(abbb)
	⇒ bb

Defines rule #2.