Certificate for #13197 ⟨a, b | abb=aab, baa=bb⟩

Back:⟨a, b | abb=aab, baa=bb⟩

Completion settings:

[1] abb=aab

Axiom: abb=aab.

Referenced by [3].

[2] bb=baa

Axiom: baa=bb.

Flip LHS and RHS.

Defines rule #3.

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

[3] aab=abaa

Overlap of [1] abb=aab with [2] bb=baa:

a bb bb

Critical pair: abaa=aab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] babaa=baaaa

Overlap of [2] bb=baa with [2] bb=baa:

b b bb

Critical pair: bbaa=baab.

Reduce LHS:

[2](bb)aa
⇒ baaaa

Reduce RHS:

[3]b(aab)
⇒ babaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] baaaaaaaa=baaaaaa

Overlap of [2] bb=baa with [4] babaa=baaaa:

b b babaa

Critical pair: bbaaaa=baaabaa.

Reduce LHS:

[2](bb)aaaa
⇒ baaaaaa

Reduce RHS:

[3]ba(aab)aa
[3]⇒ b(aab)aaaa
[4]⇒ (babaa)aaaa
⇒ baaaaaaaa

Flip LHS and RHS.

Defines rule #1.