Certificate for #5215 ⟨a, b | aab=bb, bbaa=b⟩

Back:⟨a, b | aab=bb, bbaa=b⟩

Completion settings:

[1] bb=aab

Axiom: aab=bb.

Flip LHS and RHS.

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

[2] aabaa=b

Axiom: bbaa=b.

Reduce LHS:

[1](bb)aa
⇒ aabaa

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

[3] aaaab=b

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

aab aa aabaa

Critical pair: aabb=bbaa.

Reduce LHS:

[1]aa(bb)
⇒ aaaab

Reduce RHS:

[1](bb)aa
[2]⇒ (aabaa)
⇒ b

Referenced by [4].

[4] aab=baa

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

aa aab aabaa

Critical pair: aab=baa.

Defines rule #2.

Referenced by [5], [6].

[5] baaaa=b

Overlap of [2] aabaa=b with [4] aab=baa:

aabaa aab

Critical pair: baaaa=b.

Defines rule #1.

[6] bb=baa

Simplify [1] bb=aab.

Reduce RHS:

[4](aab)
⇒ baa

Defines rule #3.