Certificate for #14498 ⟨a, b | aaab=b, abbaa=b⟩

Completion settings:

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

[1] aaab=b

Axiom: aaab=b.

Defines rule #4.

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

[2] abbaa=b

Axiom: abbaa=b.

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

[3] bbaa=aab

Overlap of [1] aaab=b with [2] abbaa=b:

aa ab abbaa

Critical pair: aab=bbaa.

Flip LHS and RHS.

Referenced by [7], [9].

[4] bab=abbb

Overlap of [2] abbaa=b with [1] aaab=b:

abb aa aaab

Critical pair: abbb=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] baab=aabbbbb

Overlap of [2] abbaa=b with [1] aaab=b:

abba a aaab

Critical pair: abbab=baab.

Reduce LHS:

[4]	ab(bab)
[4]	⇒ a(bab)bb
	⇒ aabbbbb

Flip LHS and RHS.

Referenced by [6], [7].

[6] bbbbbbbbb=bb

Overlap of [2] abbaa=b with [5] baab=aabbbbb:

ab baa baab

Critical pair: abaabbbbb=bb.

Reduce LHS:

[5]	a(baab)bbbb
[1]	⇒ (aaab)bbbbbbbb
	⇒ bbbbbbbbb

Referenced by [7].

[7] aabbbbbbbb=aab

Overlap of [6] bbbbbbbbb=bb with [3] bbaa=aab:

bbbbbbb bb bbaa

Critical pair: bbbbbbbaab=bbaa.

Reduce LHS:

[3]	bbbbb(bbaa)b
[3]	⇒ bbb(bbaa)bb
[3]	⇒ b(bbaa)bbb
[5]	⇒ (baab)bbb
	⇒ aabbbbbbbb

Reduce RHS:

[3]	(bbaa)
	⇒ aab

Referenced by [8].

[8] bbbbbbbb=b

Overlap of [1] aaab=b with [7] aabbbbbbbb=aab:

a aab aabbbbbbbb

Critical pair: aaab=bbbbbbbb.

Reduce LHS:

[1]	(aaab)
	⇒ b

Flip LHS and RHS.

Defines rule #1.

Referenced by [9].

[9] baa=aabbbb

Overlap of [8] bbbbbbbb=b with [3] bbaa=aab:

bbbbbb bb bbaa

Critical pair: bbbbbbaab=baa.

Reduce LHS:

[3]	bbbb(bbaa)b
[3]	⇒ bb(bbaa)bb
[3]	⇒ (bbaa)bbb
	⇒ aabbbb

Flip LHS and RHS.

Defines rule #3.