Certificate for #19271 ⟨a, b | aaa=a, ababb=ba⟩

Completion settings:

Reduction order:
- Right-to-left shortlex with a < b

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

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

[2] ababb=ba

Axiom: ababb=ba.

Referenced by [3], [4], [5], [6], [11], [13].

[3] aaba=ba

Overlap of [1] aaa=a with [2] ababb=ba:

aa a ababb

Critical pair: aaba=ababb.

Reduce RHS:

[2]	(ababb)
	⇒ ba

Defines rule #2.

Referenced by [4], [5], [8], [16], [18].

[4] babb=aba

Overlap of [3] aaba=ba with [2] ababb=ba:

a aba ababb

Critical pair: aba=babb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7], [11], [12], [13], [16], [18].

[5] aabba=bba

Overlap of [3] aaba=ba with [2] ababb=ba:

aab a ababb

Critical pair: aabba=bababb.

Reduce RHS:

[2]	b(ababb)
	⇒ bba

Defines rule #4.

Referenced by [8], [9], [14].

[6] abababa=baabb

Overlap of [2] ababb=ba with [4] babb=aba:

abab b babb

Critical pair: abababa=baabb.

Referenced by [10].

[7] abaabb=bababa

Overlap of [4] babb=aba with [4] babb=aba:

bab b babb

Critical pair: bababa=abaabb.

Flip LHS and RHS.

Referenced by [10], [15].

[8] aabbba=bbba

Overlap of [3] aaba=ba with [5] aabba=bba:

aab a aabba

Critical pair: aabbba=baabba.

Reduce RHS:

[5]	b(aabba)
	⇒ bbba

Defines rule #9.

Referenced by [10].

[9] aabbbba=bbbba

Overlap of [5] aabba=bba with [5] aabba=bba:

aabb a aabba

Critical pair: aabbbba=bbaabba.

Reduce RHS:

[5]	bb(aabba)
	⇒ bbbba

Referenced by [11], [14].

[10] bbaabb=abbbba

Overlap of [7] abaabb=bababa with [8] aabbba=bbba:

ab aabb aabbba

Critical pair: abbbba=babababa.

Reduce RHS:

[6]	b(abababa)
	⇒ bbaabb

Flip LHS and RHS.

Referenced by [11], [13], [14].

[11] bbbbba=ba

Overlap of [4] babb=aba with [10] bbaabb=abbbba:

ba bb bbaabb

Critical pair: baabbbba=abaaabb.

Reduce LHS:

[9]	b(aabbbba)
	⇒ bbbbba

Reduce RHS:

[1]	ab(aaa)bb
[2]	⇒ (ababb)
	⇒ ba

Defines rule #11.

Referenced by [12], [13].

[12] bbbbaba=aba

Overlap of [11] bbbbba=ba with [4] babb=aba:

bbbb ba babb

Critical pair: bbbbaba=babb.

Reduce RHS:

[4]	(babb)
	⇒ aba

Referenced by [16].

[13] baabb=bbbaa

Overlap of [11] bbbbba=ba with [10] bbaabb=abbbba:

bbb bba bbaabb

Critical pair: bbbabbbba=baabb.

Reduce LHS:

[4]	bb(babb)bba
[2]	⇒ bb(ababb)a
	⇒ bbbaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [14], [15].

[14] abbbba=bbbbaa

Overlap of [5] aabba=bba with [13] baabb=bbbaa:

aab ba baabb

Critical pair: aabbbbaa=bbaabb.

Reduce LHS:

[9]	(aabbbba)a
	⇒ bbbbaa

Reduce RHS:

[10]	(bbaabb)
	⇒ abbbba

Flip LHS and RHS.

Defines rule #10.

[15] bababa=abbbaa

Overlap of [7] abaabb=bababa with [13] baabb=bbbaa:

a baabb baabb

Critical pair: abbbaa=bababa.

Flip LHS and RHS.

Defines rule #6.

[16] bbbabaa=abba

Overlap of [12] bbbbaba=aba with [3] aaba=ba:

bbbbab a aaba

Critical pair: bbbbabba=abaaba.

Reduce LHS:

[4]	bbb(babb)a
	⇒ bbbabaa

Reduce RHS:

[3]	ab(aaba)
	⇒ abba

Referenced by [17], [18].

[17] bbbaba=abbaa

Overlap of [16] bbbabaa=abba with [1] aaa=a:

bbbab aa aaa

Critical pair: bbbaba=abbaa.

Defines rule #8.

[18] abbaba=bbabaa

Overlap of [16] bbbabaa=abba with [3] aaba=ba:

bbbab aa aaba

Critical pair: bbbabba=abbaba.

Reduce LHS:

[4]	bb(babb)a
	⇒ bbabaa

Flip LHS and RHS.

Defines rule #7.