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

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.

Defines rule #3.

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

[2] aaab=b

Axiom: aaab=b.

Defines rule #1.

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

[3] baba=abab

Overlap of [1] bb=aba with [1] bb=aba:

b b bb

Critical pair: baba=abab.

Defines rule #4.

Referenced by [4], [6].

[4] baabab=abaabaa

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

ba ba baba

Critical pair: baabab=ababba.

Reduce RHS:

[1]	aba(bb)a
	⇒ abaabaa

Defines rule #6.

Referenced by [5], [6].

[5] baabaaba=abaabaab

Overlap of [4] baabab=abaabaa with [1] bb=aba:

baaba b bb

Critical pair: baabaaba=abaabaab.

Defines rule #7.

[6] abaabaaa=abaab

Overlap of [4] baabab=abaabaa with [3] baba=abab:

baa bab baba

Critical pair: baaabab=abaabaaa.

Reduce LHS:

[2]	b(aaab)ab
[1]	⇒ (bb)ab
	⇒ abaab

Flip LHS and RHS.

Referenced by [7].

[7] baabaaa=baab

Overlap of [2] aaab=b with [6] abaabaaa=abaab:

aa ab abaabaaa

Critical pair: aaabaab=baabaaa.

Reduce LHS:

[2]	(aaab)aab
	⇒ baab

Flip LHS and RHS.

Defines rule #5.

Referenced by [8].

[8] aabaaaa=aaba

Overlap of [1] bb=aba with [7] baabaaa=baab:

b b baabaaa

Critical pair: bbaab=abaaabaaa.

Reduce LHS:

[1]	(bb)aab
[2]	⇒ ab(aaab)
[1]	⇒ a(bb)
	⇒ aaba

Reduce RHS:

[2]	ab(aaab)aaa
[1]	⇒ a(bb)aaa
	⇒ aabaaaa

Flip LHS and RHS.

Referenced by [9].

[9] baaaa=ba

Overlap of [2] aaab=b with [8] aabaaaa=aaba:

a aab aabaaaa

Critical pair: aaaba=baaaa.

Reduce LHS:

[2]	(aaab)a
	⇒ ba

Flip LHS and RHS.

Defines rule #2.