Certificate for #16233 ⟨a, b | aab=ba, abba=aa⟩

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], [5], [6].

[2] aaaaabb=aa

Axiom: abba=aa.

Reduce LHS:

[1]	ab(ba)
[1]	⇒ a(ba)ab
[1]	⇒ aaa(ba)b
	⇒ aaaaabb

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

[3] aaaaaaab=aaaab

Overlap of [1] ba=aab with [2] aaaaabb=aa:

b a aaaaabb

Critical pair: baa=aabaaaabb.

Reduce LHS:

[1]	(ba)a
[1]	⇒ aa(ba)
	⇒ aaaab

Reduce RHS:

[1]	aa(ba)aaabb
[1]	⇒ aaaa(ba)aabb
[1]	⇒ aaaaaa(ba)abb
[1]	⇒ aaaaaaaa(ba)bb
[2]	⇒ aaaaa(aaaaabb)b
	⇒ aaaaaaab

Flip LHS and RHS.

Referenced by [4], [5].

[4] aaaabb=aaaa

Overlap of [3] aaaaaaab=aaaab with [2] aaaaabb=aa:

aa aaaaab aaaaabb

Critical pair: aaaa=aaaabb.

Flip LHS and RHS.

Referenced by [5], [6].

[5] aaaaab=aab

Overlap of [1] ba=aab with [4] aaaabb=aaaa:

b a aaaabb

Critical pair: baaaa=aabaaabb.

Reduce LHS:

[1]	(ba)aaa
[1]	⇒ aa(ba)aa
[1]	⇒ aaaa(ba)a
[1]	⇒ aaaaaa(ba)
[3]	⇒ a(aaaaaaab)
	⇒ aaaaab

Reduce RHS:

[1]	aa(ba)aabb
[1]	⇒ aaaa(ba)abb
[1]	⇒ aaaaaa(ba)bb
[3]	⇒ a(aaaaaaab)bb
[2]	⇒ (aaaaabb)b
	⇒ aab

Referenced by [6], [7].

[6] aabb=aaaaa

Overlap of [4] aaaabb=aaaa with [1] ba=aab:

aaaab b ba

Critical pair: aaaabaab=aaaaa.

Reduce LHS:

[1]	aaaa(ba)ab
[5]	⇒ a(aaaaab)ab
[1]	⇒ aaa(ba)b
[5]	⇒ (aaaaab)b
	⇒ aabb

Referenced by [7], [8].

[7] aaaaa=aa

Overlap of [2] aaaaabb=aa with [5] aaaaab=aab:

aaaaabb aaaaab

Critical pair: aabb=aa.

Reduce LHS:

[6]	(aabb)
	⇒ aaaaa

Defines rule #1.

Referenced by [8].

[8] aabb=aa

Simplify [6] aabb=aaaaa.

Reduce RHS:

[7]	(aaaaa)
	⇒ aa

Defines rule #3.