Certificate for #6411 ⟨a, b | aab=b, abbba=b⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #3.

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

[2] abbba=b

Axiom: abbba=b.

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

[3] bbba=ab

Overlap of [1] aab=b with [2] abbba=b:

a ab abbba

Critical pair: ab=bbba.

Flip LHS and RHS.

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

[4] bab=abbbb

Overlap of [2] abbba=b with [1] aab=b:

abbb a aab

Critical pair: abbbb=bab.

Flip LHS and RHS.

Referenced by [5], [6].

[5] bbbbbbbbbb=bb

Overlap of [2] abbba=b with [4] bab=abbbb:

abb ba bab

Critical pair: abbabbbb=bb.

Reduce LHS:

[4]	ab(bab)bbb
[4]	⇒ a(bab)bbbbbb
[1]	⇒ (aab)bbbbbbbbb
	⇒ bbbbbbbbbb

Referenced by [6], [7].

[6] bba=abbbbbb

Overlap of [5] bbbbbbbbbb=bb with [3] bbba=ab:

bbbbbbb bbb bbba

Critical pair: bbbbbbbab=bba.

Reduce LHS:

[3]	bbbb(bbba)b
[3]	⇒ b(bbba)bb
[4]	⇒ (bab)bb
	⇒ abbbbbb

Flip LHS and RHS.

Referenced by [7].

[7] abbbbbbbbb=ab

Overlap of [5] bbbbbbbbbb=bb with [6] bba=abbbbbb:

bbbbbbbbb b bba

Critical pair: bbbbbbbbbabbbbbb=bbba.

Reduce LHS:

[3]	bbbbbb(bbba)bbbbbb
[3]	⇒ bbb(bbba)bbbbbbb
[3]	⇒ (bbba)bbbbbbbb
	⇒ abbbbbbbbb

Reduce RHS:

[3]	(bbba)
	⇒ ab

Referenced by [8], [9].

[8] bbbbbbbbb=b

Overlap of [1] aab=b with [7] abbbbbbbbb=ab:

a ab abbbbbbbbb

Critical pair: aab=bbbbbbbbb.

Reduce LHS:

[1]	(aab)
	⇒ b

Flip LHS and RHS.

Defines rule #1.

[9] aba=bbb

Overlap of [7] abbbbbbbbb=ab with [3] bbba=ab:

abbbbbb bbb bbba

Critical pair: abbbbbbab=aba.

Reduce LHS:

[3]	abbb(bbba)b
[2]	⇒ (abbba)bb
	⇒ bbb

Flip LHS and RHS.

Referenced by [10].

[10] ba=abbb

Overlap of [1] aab=b with [9] aba=bbb:

a ab aba

Critical pair: abbb=ba.

Flip LHS and RHS.

Defines rule #2.