Certificate for #12285 ⟨a, b | aaab=ba, baab=b⟩

Completion settings:

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

[1] ba=aaab

Axiom: aaab=ba.

Flip LHS and RHS.

Defines rule #2.

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

[2] aaaaaabb=b

Axiom: baab=b.

Reduce LHS:

[1]	(ba)ab
[1]	⇒ aaa(ba)b
	⇒ aaaaaabb

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

[3] bb=aaaaaab

Overlap of [1] ba=aaab with [2] aaaaaabb=b:

b a aaaaaabb

Critical pair: bb=aaabaaaaabb.

Reduce RHS:

[1]	aaa(ba)aaaabb
[1]	⇒ aaaaaa(ba)aaabb
[1]	⇒ aaaaaaaaa(ba)aabb
[1]	⇒ aaaaaaaaaaaa(ba)abb
[1]	⇒ aaaaaaaaaaaaaaa(ba)bb
[2]	⇒ aaaaaaaaaaaa(aaaaaabb)b
[2]	⇒ aaaaaa(aaaaaabb)
	⇒ aaaaaab

Referenced by [5], [6].

[4] aaaaaaaaab=aaab

Overlap of [2] aaaaaabb=b with [1] ba=aaab:

aaaaaab b ba

Critical pair: aaaaaabaaab=ba.

Reduce LHS:

[1]	aaaaaa(ba)aab
[1]	⇒ aaaaaaaaa(ba)ab
[1]	⇒ aaaaaaaaaaaa(ba)b
[2]	⇒ aaaaaaaaa(aaaaaabb)
	⇒ aaaaaaaaab

Reduce RHS:

[1]	(ba)
	⇒ aaab

Referenced by [5].

[5] aaaaaab=b

Overlap of [2] aaaaaabb=b with [3] bb=aaaaaab:

aaaaaa bb bb

Critical pair: aaaaaaaaaaaab=b.

Reduce LHS:

[4]	aaa(aaaaaaaaab)
	⇒ aaaaaab

Defines rule #1.

Referenced by [6].

[6] bb=b

Simplify [3] bb=aaaaaab.

Reduce RHS:

[5]	(aaaaaab)
	⇒ b

Defines rule #3.