Certificate for #6935 ⟨a, b | bb=aa, aaabab=1⟩

Back:⟨a, b | bb=aa, aaabab=1⟩

Completion settings:

[1] bb=aa

Axiom: bb=aa.

Defines rule #3.

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

[2] aaabab=1

Axiom: aaabab=1.

Referenced by [4].

[3] aab=baa

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

b b bb

Critical pair: baa=aab.

Flip LHS and RHS.

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

[4] ababaa=1

Simplify [2] aaabab=1.

Reduce LHS:

[3]a(aab)ab
[3]⇒ aba(aab)
⇒ ababaa

Referenced by [5], [7].

[5] abaaaaa=b

Overlap of [4] ababaa=1 with [3] aab=baa:

abab aa aab

Critical pair: ababbaa=b.

Reduce LHS:

[1]aba(bb)aa
⇒ abaaaaa

Referenced by [6].

[6] ab=baaaaaaa

Overlap of [3] aab=baa with [5] abaaaaa=b:

a ab abaaaaa

Critical pair: ab=baaaaaaa.

Defines rule #2.

Referenced by [7].

[7] aaaaaaaaaaaa=1

Overlap of [4] ababaa=1 with [6] ab=baaaaaaa:

ababaa ab

Critical pair: baaaaaaaabaa=1.

Reduce LHS:

[3]baaaaaa(aab)aa
[3]⇒ baaaa(aab)aaaa
[3]⇒ baa(aab)aaaaaa
[3]⇒ b(aab)aaaaaaaa
[1]⇒ (bb)aaaaaaaaaa
⇒ aaaaaaaaaaaa

Defines rule #1.