Certificate for #16442 ⟨a, b | aba=bb, aaab=ba⟩

Completion settings:

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

[1] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Referenced by [3].

[2] ba=aaab

Axiom: aaab=ba.

Flip LHS and RHS.

Defines rule #2.

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

[3] bb=aaaab

Simplify [1] bb=aba.

Reduce RHS:

[2]	a(ba)
	⇒ aaaab

Defines rule #3.

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

[4] aaaaaaaaaaaaaaaab=aaaaaaaab

Overlap of [3] bb=aaaab with [3] bb=aaaab:

b b bb

Critical pair: baaaab=aaaabb.

Reduce LHS:

[2]	(ba)aaab
[2]	⇒ aaa(ba)aab
[2]	⇒ aaaaaa(ba)ab
[2]	⇒ aaaaaaaaa(ba)b
[3]	⇒ aaaaaaaaaaaa(bb)
	⇒ aaaaaaaaaaaaaaaab

Reduce RHS:

[3]	aaaa(bb)
	⇒ aaaaaaaab

Referenced by [6], [7].

[5] aaaaaaaaaaaaab=aaaaaaab

Overlap of [3] bb=aaaab with [2] ba=aaab:

b b ba

Critical pair: baaab=aaaaba.

Reduce LHS:

[2]	(ba)aab
[2]	⇒ aaa(ba)ab
[2]	⇒ aaaaaa(ba)b
[3]	⇒ aaaaaaaaa(bb)
	⇒ aaaaaaaaaaaaab

Reduce RHS:

[2]	aaaa(ba)
	⇒ aaaaaaab

Referenced by [6], [7], [8].

[6] aaaaaaaaaaab=aaaaaaaaab

Overlap of [5] aaaaaaaaaaaaab=aaaaaaab with [3] bb=aaaab:

aaaaaaaaaaaaa b bb

Critical pair: aaaaaaaaaaaaaaaaab=aaaaaaabb.

Reduce LHS:

[4]	a(aaaaaaaaaaaaaaaab)
	⇒ aaaaaaaaab

Reduce RHS:

[3]	aaaaaaa(bb)
	⇒ aaaaaaaaaaab

Flip LHS and RHS.

Referenced by [8].

[7] aaaaaaaaaab=aaaaaaaab

Overlap of [5] aaaaaaaaaaaaab=aaaaaaab with [2] ba=aaab:

aaaaaaaaaaaaa b ba

Critical pair: aaaaaaaaaaaaaaaab=aaaaaaaba.

Reduce LHS:

[4]	(aaaaaaaaaaaaaaaab)
	⇒ aaaaaaaab

Reduce RHS:

[2]	aaaaaaa(ba)
	⇒ aaaaaaaaaab

Flip LHS and RHS.

Referenced by [8].

[8] aaaaaaaaab=aaaaaaab

Overlap of [7] aaaaaaaaaab=aaaaaaaab with [2] ba=aaab:

aaaaaaaaaa b ba

Critical pair: aaaaaaaaaaaaab=aaaaaaaaba.

Reduce LHS:

[5]	(aaaaaaaaaaaaab)
	⇒ aaaaaaab

Reduce RHS:

[2]	aaaaaaaa(ba)
[6]	⇒ (aaaaaaaaaaab)
	⇒ aaaaaaaaab

Flip LHS and RHS.

Defines rule #1.