Certificate for #15514 ⟨a, b | aaa=bb, aabaa=b⟩

Back:⟨a, b | aaa=bb, aabaa=b⟩

Completion settings:

[1] bb=aaa

Axiom: aaa=bb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [6].

[2] aabaa=b

Axiom: aabaa=b.

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

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

[4] aabab=babaa

Overlap of [2] aabaa=b with [2] aabaa=b:

aaba a aabaa

Critical pair: aabab=babaa.

Referenced by [6].

[5] ab=baaaaa

Overlap of [3] aaab=baaa with [2] aabaa=b:

a aab aabaa

Critical pair: ab=baaaaa.

Defines rule #3.

Referenced by [6], [7].

[6] aaaaaaaaaaaaaaa=aaa

Overlap of [2] aabaa=b with [5] ab=baaaaa:

aaba a ab

Critical pair: aababaaaaa=bb.

Reduce LHS:

[4](aabab)aaaaa
[5]⇒ b(ab)aaaaaaa
[1]⇒ (bb)aaaaaaaaaaaa
⇒ aaaaaaaaaaaaaaa

Reduce RHS:

[1](bb)
⇒ aaa

Defines rule #1.

[7] baaaaaaaaaaaa=b

Overlap of [2] aabaa=b with [5] ab=baaaaa:

a abaa ab

Critical pair: abaaaaaaa=b.

Reduce LHS:

[5](ab)aaaaaaa
⇒ baaaaaaaaaaaa

Defines rule #2.