Certificate for #14993 ⟨a, b | aaa=bb, ababbb=1⟩

Back:⟨a, b | aaa=bb, ababbb=1⟩

Completion settings:

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #3.

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

[2] abaaaab=1

Axiom: ababbb=1.

Reduce LHS:

[1]aba(bb)b
⇒ abaaaab

Referenced by [4].

[3] aaab=baaa

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

b b bb

Critical pair: baaa=aaab.

Flip LHS and RHS.

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

[4] ababaaa=1

Simplify [2] abaaaab=1.

Reduce LHS:

[3]aba(aaab)
⇒ ababaaa

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

[5] ababaa=babaaa

Overlap of [4] ababaaa=1 with [4] ababaaa=1:

ababaa a ababaaa

Critical pair: ababaa=babaaa.

Referenced by [7].

[6] abaaaaaaa=b

Overlap of [4] ababaaa=1 with [3] aaab=baaa:

abab aaa aaab

Critical pair: ababbaaa=b.

Reduce LHS:

[1]aba(bb)aaa
⇒ abaaaaaaa

Referenced by [8].

[7] aab=baaaaaaaaaa

Overlap of [4] ababaaa=1 with [3] aaab=baaa:

ababaa a aaab

Critical pair: ababaabaaa=aab.

Reduce LHS:

[5](ababaa)baaa
[3]⇒ bab(aaab)aaa
[1]⇒ ba(bb)aaaaaa
⇒ baaaaaaaaaa

Flip LHS and RHS.

Referenced by [8].

[8] ab=baaaaaaaaaaaaaaaaa

Overlap of [7] aab=baaaaaaaaaa with [6] abaaaaaaa=b:

a ab abaaaaaaa

Critical pair: ab=baaaaaaaaaaaaaaaaa.

Defines rule #2.

Referenced by [9].

[9] aaaaaaaaaaaaaaaaaaaaaaaa=1

Overlap of [4] ababaaa=1 with [8] ab=baaaaaaaaaaaaaaaaa:

ababaaa ab

Critical pair: baaaaaaaaaaaaaaaaaabaaa=1.

Reduce LHS:

[3]baaaaaaaaaaaaaaa(aaab)aaa
[3]⇒ baaaaaaaaaaaa(aaab)aaaaaa
[3]⇒ baaaaaaaaa(aaab)aaaaaaaaa
[3]⇒ baaaaaa(aaab)aaaaaaaaaaaa
[3]⇒ baaa(aaab)aaaaaaaaaaaaaaa
[3]⇒ b(aaab)aaaaaaaaaaaaaaaaaa
[1]⇒ (bb)aaaaaaaaaaaaaaaaaaaaa
⇒ aaaaaaaaaaaaaaaaaaaaaaaa

Defines rule #1.