Certificate for #12264 ⟨a, b | aaab=ab, bbab=a⟩

Completion settings:

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

[1] aaab=ab

Axiom: aaab=ab.

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

[2] bbab=a

Axiom: bbab=a.

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

[3] abab=bbaa

Overlap of [2] bbab=a with [2] bbab=a:

bba b bbab

Critical pair: bbaa=abab.

Flip LHS and RHS.

Referenced by [4], [5].

[4] aab=bbbbaa

Overlap of [2] bbab=a with [3] abab=bbaa:

bb ab abab

Critical pair: bbbbaa=aab.

Flip LHS and RHS.

Referenced by [7], [9].

[5] abbbaa=a

Overlap of [3] abab=bbaa with [3] abab=bbaa:

ab ab abab

Critical pair: abbbaa=bbaaab.

Reduce RHS:

[1]	bb(aaab)
[2]	⇒ (bbab)
	⇒ a

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

[6] aaa=a

Overlap of [1] aaab=ab with [5] abbbaa=a:

aa ab abbbaa

Critical pair: aaa=abbbaa.

Reduce RHS:

[5]	(abbbaa)
	⇒ a

Defines rule #3.

Referenced by [9].

[7] aba=bbbbaa

Overlap of [5] abbbaa=a with [1] aaab=ab:

abbb aa aaab

Critical pair: abbbab=aab.

Reduce LHS:

[2]	ab(bbab)
	⇒ aba

Reduce RHS:

[4]	(aab)
	⇒ bbbbaa

Referenced by [8], [9].

[8] bbbbbbaa=aa

Overlap of [2] bbab=a with [7] aba=bbbbaa:

bb ab aba

Critical pair: bbbbbbaa=aa.

Referenced by [9].

[9] ab=bbbba

Overlap of [5] abbbaa=a with [4] aab=bbbbaa:

abbb aa aab

Critical pair: abbbbbbbaa=ab.

Reduce LHS:

[8]	ab(bbbbbbaa)
[7]	⇒ (aba)a
[6]	⇒ bbbb(aaa)
	⇒ bbbba

Flip LHS and RHS.

Defines rule #2.

Referenced by [10].

[10] bbbbbba=a

Overlap of [2] bbab=a with [9] ab=bbbba:

bb ab ab

Critical pair: bbbbbba=a.

Defines rule #1.