Certificate for #5186 ⟨a, b | aab=ba, bbba=a⟩

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] aaaaaaaabbb=a

Axiom: bbba=a.

Reduce LHS:

[1]	bb(ba)
[1]	⇒ b(ba)ab
[1]	⇒ (ba)abab
[1]	⇒ aa(ba)bab
[1]	⇒ aaaab(ba)b
[1]	⇒ aaaa(ba)abb
[1]	⇒ aaaaaa(ba)bb
	⇒ aaaaaaaabbb

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

[3] aaaaaaaaab=aab

Overlap of [1] ba=aab with [2] aaaaaaaabbb=a:

b a aaaaaaaabbb

Critical pair: ba=aabaaaaaaabbb.

Reduce LHS:

[1]	(ba)
	⇒ aab

Reduce RHS:

[1]	aa(ba)aaaaaabbb
[1]	⇒ aaaa(ba)aaaaabbb
[1]	⇒ aaaaaa(ba)aaaabbb
[1]	⇒ aaaaaaaa(ba)aaabbb
[1]	⇒ aaaaaaaaaa(ba)aabbb
[1]	⇒ aaaaaaaaaaaa(ba)abbb
[1]	⇒ aaaaaaaaaaaaaa(ba)bbb
[2]	⇒ aaaaaaaa(aaaaaaaabbb)b
	⇒ aaaaaaaaab

Flip LHS and RHS.

Referenced by [4].

[4] aabbb=aa

Overlap of [2] aaaaaaaabbb=a with [1] ba=aab:

aaaaaaaabb b ba

Critical pair: aaaaaaaabbaab=aa.

Reduce LHS:

[1]	aaaaaaaab(ba)ab
[1]	⇒ aaaaaaaa(ba)abab
[3]	⇒ a(aaaaaaaaab)abab
[1]	⇒ aaa(ba)bab
[1]	⇒ aaaaab(ba)b
[1]	⇒ aaaaa(ba)abb
[1]	⇒ aaaaaaa(ba)bb
[3]	⇒ (aaaaaaaaab)bb
	⇒ aabbb

Referenced by [5], [6].

[5] aaaaaaaa=a

Overlap of [2] aaaaaaaabbb=a with [4] aabbb=aa:

aaaaaa aabbb aabbb

Critical pair: aaaaaaaa=a.

Defines rule #1.

Referenced by [6].

[6] abbb=a

Overlap of [5] aaaaaaaa=a with [4] aabbb=aa:

aaaaaa aa aabbb

Critical pair: aaaaaaaa=abbb.

Reduce LHS:

[5]	(aaaaaaaa)
	⇒ a

Flip LHS and RHS.

Defines rule #3.