Certificate for #18748 ⟨a, b | aaa=a, bababb=a⟩

Completion settings:

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

[1] aaa=a

Axiom: aaa=a.

Defines rule #3.

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

[2] bababb=a

Axiom: bababb=a.

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

[3] aababb=bababa

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

babab b bababb

Critical pair: bababa=aababb.

Flip LHS and RHS.

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

[4] abababa=ababb

Overlap of [1] aaa=a with [3] aababb=bababa:

a aa aababb

Critical pair: abababa=ababb.

Referenced by [5].

[5] ababbba=aa

Overlap of [4] abababa=ababb with [4] abababa=ababb:

ab ababa abababa

Critical pair: abababb=ababbba.

Reduce LHS:

[2]	a(bababb)
	⇒ aa

Flip LHS and RHS.

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

[6] aba=baa

Overlap of [2] bababb=a with [5] ababbba=aa:

b ababb ababbba

Critical pair: baa=aba.

Flip LHS and RHS.

Defines rule #2.

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

[7] bbbbaa=a

Overlap of [3] aababb=bababa with [5] ababbba=aa:

a ababb ababbba

Critical pair: aaa=babababa.

Reduce LHS:

[1]	(aaa)
	⇒ a

Reduce RHS:

[6]	b(aba)baba
[6]	⇒ bba(aba)ba
[6]	⇒ bb(aba)aba
[1]	⇒ bbb(aaa)ba
[6]	⇒ bbb(aba)
	⇒ bbbbaa

Flip LHS and RHS.

Referenced by [8], [9].

[8] baabb=bbbaa

Overlap of [5] ababbba=aa with [3] aababb=bababa:

ababbb a aababb

Critical pair: ababbbbababa=aaababb.

Reduce LHS:

[6]	(aba)bbbbababa
[6]	⇒ baabbbb(aba)ba
[7]	⇒ baab(bbbbaa)ba
[6]	⇒ ba(aba)ba
[6]	⇒ b(aba)aba
[1]	⇒ bb(aaa)ba
[6]	⇒ bb(aba)
	⇒ bbbaa

Reduce RHS:

[1]	(aaa)babb
[6]	⇒ (aba)bb
	⇒ baabb

Flip LHS and RHS.

Referenced by [10].

[9] bbbba=aa

Overlap of [7] bbbbaa=a with [1] aaa=a:

bbbb aa aaa

Critical pair: bbbba=aa.

Defines rule #4.

Referenced by [10].

[10] abb=bba

Overlap of [5] ababbba=aa with [8] baabb=bbbaa:

ababb ba baabb

Critical pair: ababbbbbaa=aaabb.

Reduce LHS:

[6]	(aba)bbbbbaa
[8]	⇒ (baabb)bbbaa
[8]	⇒ bb(baabb)baa
[9]	⇒ b(bbbba)abaa
[1]	⇒ b(aaa)baa
[6]	⇒ b(aba)a
[1]	⇒ bb(aaa)
	⇒ bba

Reduce RHS:

[1]	(aaa)bb
	⇒ abb

Flip LHS and RHS.

Defines rule #1.