Certificate for #15158 ⟨a, b | aab=ba, ababab=1⟩

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] aaaaaaabbb=1

Axiom: ababab=1.

Reduce LHS:

[1]	a(ba)bab
[1]	⇒ aaab(ba)b
[1]	⇒ aaa(ba)abb
[1]	⇒ aaaaa(ba)bb
	⇒ aaaaaaabbb

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

[3] aaaaaaab=b

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

b a aaaaaaabbb

Critical pair: b=aabaaaaaabbb.

Reduce RHS:

[1]	aa(ba)aaaaabbb
[1]	⇒ aaaa(ba)aaaabbb
[1]	⇒ aaaaaa(ba)aaabbb
[1]	⇒ aaaaaaaa(ba)aabbb
[1]	⇒ aaaaaaaaaa(ba)abbb
[1]	⇒ aaaaaaaaaaaa(ba)bbb
[2]	⇒ aaaaaaa(aaaaaaabbb)b
	⇒ aaaaaaab

Flip LHS and RHS.

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

[4] abbb=a

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

aaaaaaabb b ba

Critical pair: aaaaaaabbaab=a.

Reduce LHS:

[3]	(aaaaaaab)baab
[1]	⇒ b(ba)ab
[1]	⇒ (ba)abab
[1]	⇒ aa(ba)bab
[1]	⇒ aaaab(ba)b
[1]	⇒ aaaa(ba)abb
[1]	⇒ aaaaaa(ba)bb
[3]	⇒ a(aaaaaaab)bb
	⇒ abbb

Referenced by [6].

[5] bbb=1

Overlap of [2] aaaaaaabbb=1 with [3] aaaaaaab=b:

aaaaaaabbb aaaaaaab

Critical pair: bbb=1.

Defines rule #3.

Referenced by [6].

[6] aaaaaaa=1

Overlap of [3] aaaaaaab=b with [4] abbb=a:

aaaaaa ab abbb

Critical pair: aaaaaaa=bbb.

Reduce RHS:

[5]	(bbb)
	⇒ 1

Defines rule #1.