Certificate for #12288 ⟨a, b | aaab=ba, babb=a⟩

Completion settings:

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

[1] aaab=ba

Axiom: aaab=ba.

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

[2] babb=a

Axiom: babb=a.

Referenced by [3], [4], [6], [8], [14], [15].

[3] baba=aabb

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

bab b babb

Critical pair: baba=aabb.

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

[4] baabb=aaaa

Overlap of [1] aaab=ba with [2] babb=a:

aaa b babb

Critical pair: aaaa=baabb.

Flip LHS and RHS.

Referenced by [7], [9], [10], [15], [16].

[5] baaba=aabab

Overlap of [1] aaab=ba with [3] baba=aabb:

aaa b baba

Critical pair: aaaaabb=baaba.

Reduce LHS:

[1]	aa(aaab)b
	⇒ aabab

Flip LHS and RHS.

Referenced by [7].

[6] aabbaab=aa

Overlap of [3] baba=aabb with [1] aaab=ba:

bab a aaab

Critical pair: babba=aabbaab.

Reduce LHS:

[2]	(babb)a
	⇒ aa

Flip LHS and RHS.

Referenced by [10], [11].

[7] baab=aabb

Overlap of [4] baabb=aaaa with [4] baabb=aaaa:

baab b baabb

Critical pair: baabaaaa=aaaaaabb.

Reduce LHS:

[5]	(baaba)aaa
[3]	⇒ aa(baba)aa
[1]	⇒ a(aaab)baa
[3]	⇒ a(baba)a
[1]	⇒ (aaab)ba
[3]	⇒ (baba)
	⇒ aabb

Reduce RHS:

[1]	aaa(aaab)b
[1]	⇒ (aaab)ab
	⇒ baab

Flip LHS and RHS.

Referenced by [8], [9], [10], [11], [17].

[8] aaba=ba

Overlap of [2] babb=a with [7] baab=aabb:

bab b baab

Critical pair: babaabb=aaab.

Reduce LHS:

[3]	(baba)abb
[2]	⇒ aab(babb)
	⇒ aaba

Reduce RHS:

[1]	(aaab)
	⇒ ba

Referenced by [11], [12], [13], [16].

[9] aabbb=aaaa

Overlap of [4] baabb=aaaa with [7] baab=aabb:

baabb baab

Critical pair: aabbb=aaaa.

Referenced by [11], [16], [17].

[10] baa=aab

Overlap of [4] baabb=aaaa with [7] baab=aabb:

baab b baab

Critical pair: baabaabb=aaaaaab.

Reduce LHS:

[7]	(baab)aabb
[6]	⇒ (aabbaab)b
	⇒ aab

Reduce RHS:

[1]	aaa(aaab)
[1]	⇒ (aaab)a
	⇒ baa

Flip LHS and RHS.

Referenced by [11], [12], [13], [15], [16].

[11] aaaa=aa

Overlap of [7] baab=aabb with [7] baab=aabb:

baa b baab

Critical pair: baaaabb=aabbaab.

Reduce LHS:

[10]	(baa)aabb
[8]	⇒ (aaba)abb
[10]	⇒ (baa)bb
[9]	⇒ (aabbb)
	⇒ aaaa

Reduce RHS:

[6]	(aabbaab)
	⇒ aa

Referenced by [15].

[12] aabba=bab

Overlap of [3] baba=aabb with [10] baa=aab:

ba ba baa

Critical pair: baaab=aabba.

Reduce LHS:

[10]	(baa)ab
[8]	⇒ (aaba)b
	⇒ bab

Flip LHS and RHS.

Referenced by [15], [17].

[13] bba=bab

Overlap of [10] baa=aab with [1] aaab=ba:

b aa aaab

Critical pair: bba=aabab.

Reduce RHS:

[8]	(aaba)b
	⇒ bab

Referenced by [14], [15], [16], [17].

[14] aba=aab

Overlap of [2] babb=a with [13] bba=bab:

bab b bba

Critical pair: babbab=aba.

Reduce LHS:

[2]	(babb)ab
	⇒ aab

Flip LHS and RHS.

Referenced by [17].

[15] aaa=a

Overlap of [4] baabb=aaaa with [13] bba=bab:

baa bb bba

Critical pair: baabab=aaaaa.

Reduce LHS:

[10]	(baa)bab
[12]	⇒ (aabba)b
[2]	⇒ (babb)
	⇒ a

Reduce RHS:

[11]	(aaaa)a
	⇒ aaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [16], [17].

[16] ba=ab

Overlap of [4] baabb=aaaa with [13] bba=bab:

baab b bba

Critical pair: baabbab=aaaaba.

Reduce LHS:

[10]	(baa)bbab
[9]	⇒ (aabbb)ab
[15]	⇒ (aaa)aab
[15]	⇒ (aaa)b
	⇒ ab

Reduce RHS:

[15]	(aaa)aba
[8]	⇒ (aaba)
	⇒ ba

Flip LHS and RHS.

Defines rule #1.

Referenced by [17].

[17] abbb=a

Overlap of [7] baab=aabb with [13] bba=bab:

baa b bba

Critical pair: baabab=aabbba.

Reduce LHS:

[16]	(ba)abab
[14]	⇒ (aba)bab
[12]	⇒ (aabba)b
[16]	⇒ (ba)bb
	⇒ abbb

Reduce RHS:

[9]	(aabbb)a
[15]	⇒ (aaa)aa
[15]	⇒ (aaa)
	⇒ a

Defines rule #3.