Certificate for #14648 ⟨a, b | aaba=b, babbb=b⟩

Completion settings:

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

[1] aaba=b

Axiom: aaba=b.

Referenced by [3], [4], [6], [8].

[2] babbb=b

Axiom: babbb=b.

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

[3] baba=aabb

Overlap of [1] aaba=b with [1] aaba=b:

aab a aaba

Critical pair: aabb=baba.

Flip LHS and RHS.

Referenced by [7].

[4] bbbb=aab

Overlap of [1] aaba=b with [2] babbb=b:

aa ba babbb

Critical pair: aab=bbbb.

Flip LHS and RHS.

Defines rule #3.

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

[5] baaab=bb

Overlap of [2] babbb=b with [4] bbbb=aab:

ba bbb bbbb

Critical pair: baaab=bb.

Referenced by [6].

[6] bba=bab

Overlap of [5] baaab=bb with [1] aaba=b:

ba aab aaba

Critical pair: bab=bba.

Flip LHS and RHS.

Referenced by [7], [8].

[7] ba=aaaab

Overlap of [2] babbb=b with [6] bba=bab:

bab bb bba

Critical pair: babbab=ba.

Reduce LHS:

[6]	ba(bba)b
[3]	⇒ (baba)bb
[4]	⇒ aa(bbbb)
	⇒ aaaab

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[8] aaaaaab=b

Overlap of [4] bbbb=aab with [6] bba=bab:

bb bb bba

Critical pair: bbbab=aaba.

Reduce LHS:

[6]	b(bba)b
[6]	⇒ (bba)bb
[7]	⇒ (ba)bbb
[4]	⇒ aaaa(bbbb)
	⇒ aaaaaab

Reduce RHS:

[1]	(aaba)
	⇒ b

Defines rule #1.