Certificate for #14981 ⟨a, b | aaa=bb, aabaab=1⟩

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

Completion settings:

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #3.

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

[2] aabaab=1

Axiom: aabaab=1.

Referenced by [4], [6].

[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], [5], [6].

[4] baabaaa=a

Overlap of [3] aaab=baaa with [2] aabaab=1:

a aab aabaab

Critical pair: a=baaaaab.

Reduce RHS:

[3]baa(aaab)
⇒ baabaaa

Flip LHS and RHS.

Referenced by [5].

[5] ab=baaaaaaaa

Overlap of [4] baabaaa=a with [3] aaab=baaa:

baab aaa aaab

Critical pair: baabbaaa=ab.

Reduce LHS:

[1]baa(bb)aaa
⇒ baaaaaaaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] aaaaaaaaaaaaaaaaaaaaa=1

Overlap of [2] aabaab=1 with [5] ab=baaaaaaaa:

a abaab ab

Critical pair: abaaaaaaaaaab=1.

Reduce LHS:

[3]abaaaaaaa(aaab)
[3]⇒ abaaaa(aaab)aaa
[3]⇒ aba(aaab)aaaaaa
[5]⇒ (ab)abaaaaaaaaa
[3]⇒ baaaaaa(aaab)aaaaaaaaa
[3]⇒ baaa(aaab)aaaaaaaaaaaa
[3]⇒ b(aaab)aaaaaaaaaaaaaaa
[1]⇒ (bb)aaaaaaaaaaaaaaaaaa
⇒ aaaaaaaaaaaaaaaaaaaaa

Defines rule #1.