Certificate for #16263 ⟨a, b | aab=ba, bbab=ba⟩

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 #2.

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

[2] aaaabbb=aab

Axiom: bbab=ba.

Reduce LHS:

[1]	b(ba)b
[1]	⇒ (ba)abb
[1]	⇒ aa(ba)bb
	⇒ aaaabbb

Reduce RHS:

[1]	(ba)
	⇒ aab

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

[3] aaaaaabb=aaaabb

Overlap of [1] ba=aab with [2] aaaabbb=aab:

b a aaaabbb

Critical pair: baab=aabaaabbb.

Reduce LHS:

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

Reduce RHS:

[1]	aa(ba)aabbb
[1]	⇒ aaaa(ba)abbb
[1]	⇒ aaaaaa(ba)bbb
[2]	⇒ aaaa(aaaabbb)b
	⇒ aaaaaabb

Flip LHS and RHS.

Referenced by [4].

[4] aaaab=aab

Overlap of [2] aaaabbb=aab with [1] ba=aab:

aaaabb b ba

Critical pair: aaaabbaab=aaba.

Reduce LHS:

[1]	aaaab(ba)ab
[1]	⇒ aaaa(ba)abab
[1]	⇒ aaaaaa(ba)bab
[3]	⇒ aa(aaaaaabb)ab
[3]	⇒ (aaaaaabb)ab
[1]	⇒ aaaab(ba)b
[1]	⇒ aaaa(ba)abb
[1]	⇒ aaaaaa(ba)bb
[3]	⇒ aa(aaaaaabb)b
[3]	⇒ (aaaaaabb)b
[2]	⇒ (aaaabbb)
	⇒ aab

Reduce RHS:

[1]	aa(ba)
	⇒ aaaab

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] aabbb=aab

Overlap of [2] aaaabbb=aab with [4] aaaab=aab:

aaaabbb aaaab

Critical pair: aabbb=aab.

Defines rule #3.