Certificate for #13218 ⟨a, b | abb=aba, bbb=aa⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] abb=aba

Axiom: abb=aba.

Defines rule #1.

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

[2] bbb=aa

Axiom: bbb=aa.

Defines rule #3.

Referenced by [3], [4].

[3] baa=aab

Overlap of [2] bbb=aa with [2] bbb=aa:

b bb bbb

Critical pair: baa=aab.

Defines rule #2.

Referenced by [5], [7].

[4] abab=aaa

Overlap of [1] abb=aba with [2] bbb=aa:

a bb bbb

Critical pair: aaa=abab.

Flip LHS and RHS.

Defines rule #5.

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

[5] aaaab=aaaa

Overlap of [3] baa=aab with [1] abb=aba:

ba a abb

Critical pair: baaba=aabbb.

Reduce LHS:

[3]	(baa)ba
[1]	⇒ a(abb)a
[3]	⇒ aa(baa)
	⇒ aaaab

Reduce RHS:

[1]	a(abb)b
[4]	⇒ a(abab)
	⇒ aaaa

Referenced by [7].

[6] aaab=aaaa

Overlap of [4] abab=aaa with [1] abb=aba:

ab ab abb

Critical pair: ababa=aaab.

Reduce LHS:

[4]	(abab)a
	⇒ aaaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

[7] aaaaa=aaaa

Overlap of [4] abab=aaa with [4] abab=aaa:

ab ab abab

Critical pair: abaaa=aaaab.

Reduce LHS:

[3]	a(baa)a
[6]	⇒ (aaab)a
	⇒ aaaaa

Reduce RHS:

[5]	(aaaab)
	⇒ aaaa

Defines rule #6.