Certificate for #16459 ⟨a, b | aba=bb, abbb=aa⟩

Back:⟨a, b | aba=bb, abbb=aa⟩

Completion settings:

[1] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2], [3], [6], [9].

[2] aabab=aa

Axiom: abbb=aa.

Reduce LHS:

[1]a(bb)b
⇒ aabab

Referenced by [4].

[3] abab=baba

Overlap of [1] bb=aba with [1] bb=aba:

b b bb

Critical pair: baba=abab.

Flip LHS and RHS.

Defines rule #5.

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

[4] babaa=aa

Simplify [2] aabab=aa.

Reduce LHS:

[3]a(abab)
[3]⇒ (abab)a
⇒ babaa

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

[5] baaba=aa

Overlap of [4] babaa=aa with [3] abab=baba:

baba a abab

Critical pair: babababa=aabab.

Reduce LHS:

[3]b(abab)aba
[4]⇒ b(babaa)ba
⇒ baaba

Reduce RHS:

[3]a(abab)
[3]⇒ (abab)a
[4]⇒ (babaa)
⇒ aa

Referenced by [6], [8].

[6] aab=aaaa

Overlap of [3] abab=baba with [3] abab=baba:

ab ab abab

Critical pair: abbaba=babaab.

Reduce LHS:

[1]a(bb)aba
[5]⇒ aa(baaba)
⇒ aaaa

Reduce RHS:

[4](babaa)b
⇒ aab

Flip LHS and RHS.

Defines rule #3.

Referenced by [7], [8].

[7] aaaaaaa=aa

Overlap of [6] aab=aaaa with [3] abab=baba:

a ab abab

Critical pair: ababa=aaaaab.

Reduce LHS:

[3](abab)a
[4]⇒ (babaa)
⇒ aa

Reduce RHS:

[6]aaa(aab)
⇒ aaaaaaa

Flip LHS and RHS.

Defines rule #1.

[8] baaaaa=aa

Simplify [5] baaba=aa.

Reduce LHS:

[6]b(aab)a
⇒ baaaaa

Referenced by [9].

[9] baa=aaaa

Overlap of [1] bb=aba with [8] baaaaa=aa:

b b baaaaa

Critical pair: baa=abaaaaaa.

Reduce RHS:

[8]a(baaaaa)a
⇒ aaaa

Defines rule #2.