Certificate for #12906 ⟨a, b | aab=aaa, bbab=a⟩

Completion settings:

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

[1] aab=aaa

Axiom: aab=aaa.

Defines rule #1.

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

[2] bbab=a

Axiom: bbab=a.

Defines rule #3.

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

[3] bbaa=abab

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

bba b bbab

Critical pair: bbaa=abab.

Defines rule #2.

Referenced by [5], [6].

[4] aaaaaa=aaa

Overlap of [1] aab=aaa with [2] bbab=a:

aa b bbab

Critical pair: aaa=aaabab.

Reduce RHS:

[1]	a(aab)ab
[1]	⇒ aaa(aab)
	⇒ aaaaaa

Flip LHS and RHS.

Defines rule #6.

[5] ababb=ababa

Overlap of [3] bbaa=abab with [1] aab=aaa:

bb aa aab

Critical pair: bbaaa=ababb.

Reduce LHS:

[3]	(bbaa)a
	⇒ ababa

Flip LHS and RHS.

Referenced by [7], [8], [10].

[6] ababab=ababaa

Overlap of [3] bbaa=abab with [1] aab=aaa:

bba a aab

Critical pair: bbaaaa=ababab.

Reduce LHS:

[3]	(bbaa)aa
	⇒ ababaa

Flip LHS and RHS.

Referenced by [8].

[7] ababaaa=abaa

Overlap of [5] ababb=ababa with [2] bbab=a:

aba bb bbab

Critical pair: abaa=ababaab.

Reduce RHS:

[1]	abab(aab)
	⇒ ababaaa

Flip LHS and RHS.

Referenced by [8], [9].

[8] ababa=abaaa

Overlap of [5] ababb=ababa with [2] bbab=a:

abab b bbab

Critical pair: ababa=abababab.

Reduce RHS:

[6]	(ababab)ab
[7]	⇒ (ababaaa)b
[1]	⇒ ab(aab)
	⇒ abaaa

Defines rule #4.

Referenced by [9], [10].

[9] abaaaaa=abaa

Simplify [7] ababaaa=abaa.

Reduce LHS:

[8]	(ababa)aa
	⇒ abaaaaa

Defines rule #7.

[10] ababb=abaaa

Simplify [5] ababb=ababa.

Reduce RHS:

[8]	(ababa)
	⇒ abaaa

Defines rule #5.