Certificate for #8630 ⟨a, b | aa=a, babbab=a⟩

Completion settings:

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

[1] aa=a

Axiom: aa=a.

Defines rule #1.

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

[2] babbab=a

Axiom: babbab=a.

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

[3] baba=abab

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

bab bab babbab

Critical pair: baba=abab.

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

[4] babba=abbab

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

babba b babbab

Critical pair: babbaa=aabbab.

Reduce LHS:

[1]	babb(aa)
	⇒ babba

Reduce RHS:

[1]	(aa)bbab
	⇒ abbab

Referenced by [5], [6].

[5] abbabb=a

Overlap of [2] babbab=a with [3] baba=abab:

bab bab baba

Critical pair: bababab=aa.

Reduce LHS:

[3]	(baba)bab
[4]	⇒ a(babba)b
[1]	⇒ (aa)bbabb
	⇒ abbabb

Reduce RHS:

[1]	(aa)
	⇒ a

Referenced by [7].

[6] abbab=ababb

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

ba ba baba

Critical pair: baabab=ababba.

Reduce LHS:

[1]	b(aa)bab
[3]	⇒ (baba)b
	⇒ ababb

Reduce RHS:

[4]	a(babba)
[1]	⇒ (aa)bbab
	⇒ abbab

Flip LHS and RHS.

Referenced by [7].

[7] ababbb=a

Simplify [5] abbabb=a.

Reduce LHS:

[6]	(abbab)b
	⇒ ababbb

Referenced by [8], [9].

[8] ba=ab

Overlap of [3] baba=abab with [7] ababbb=a:

b aba ababbb

Critical pair: ba=ababbbb.

Reduce RHS:

[7]	(ababbb)b
	⇒ ab

Defines rule #2.

Referenced by [9].

[9] abbbb=a

Overlap of [7] ababbb=a with [8] ba=ab:

a babbb ba

Critical pair: aabbbb=a.

Reduce LHS:

[1]	(aa)bbbb
	⇒ abbbb

Defines rule #3.