Certificate for #10846 ⟨a, b | aaba=baa, bbbb=1⟩

Back:⟨a, b | aaba=baa, bbbb=1⟩

Completion settings:

[1] baa=aaba

Axiom: aaba=baa.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[2] bbbb=1

Axiom: bbbb=1.

Defines rule #3.

Referenced by [3].

[3] aababababa=aa

Overlap of [2] bbbb=1 with [1] baa=aaba:

bbb b baa

Critical pair: bbbaaba=aa.

Reduce LHS:

[1]bb(baa)ba
[1]⇒ b(baa)baba
[1]⇒ (baa)bababa
⇒ aababababa

Defines rule #4.

Referenced by [4].

[4] aaaaaaaaaaaaaaaaaa=aaa

Overlap of [3] aababababa=aa with [1] baa=aaba:

aabababa ba baa

Critical pair: aabababaaaba=aaa.

Reduce LHS:

[1]aababa(baa)aba
[1]⇒ aaba(baa)abaaba
[1]⇒ aa(baa)abaabaaba
[1]⇒ aaaa(baa)baabaaba
[1]⇒ aaaaaaba(baa)baaba
[1]⇒ aaaaaa(baa)ababaaba
[1]⇒ aaaaaaaa(baa)babaaba
[1]⇒ aaaaaaaaaababa(baa)ba
[1]⇒ aaaaaaaaaaba(baa)ababa
[1]⇒ aaaaaaaaaa(baa)abaababa
[1]⇒ aaaaaaaaaaaa(baa)baababa
[1]⇒ aaaaaaaaaaaaaaba(baa)baba
[1]⇒ aaaaaaaaaaaaaa(baa)abababa
[1]⇒ aaaaaaaaaaaaaaaa(baa)bababa
[3]⇒ aaaaaaaaaaaaaaaa(aababababa)
⇒ aaaaaaaaaaaaaaaaaa

Defines rule #1.