Certificate for #20052 ⟨a, b | aab=b, aaaa=baa⟩

Back:⟨a, b | aab=b, aaaa=baa⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

Referenced by [3], [5].

[2] aaaa=baa

Axiom: aaaa=baa.

Defines rule #4.

Referenced by [3], [4].

[3] bb=b

Overlap of [2] aaaa=baa with [1] aab=b:

aa aa aab

Critical pair: aab=baab.

Reduce LHS:

[1](aab)
⇒ b

Reduce RHS:

[1]b(aab)
⇒ bb

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[4] baaa=abaa

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

a aaa aaaa

Critical pair: abaa=baaa.

Flip LHS and RHS.

Defines rule #5.

Referenced by [5].

[5] bab=ab

Overlap of [4] baaa=abaa with [1] aab=b:

ba aa aab

Critical pair: bab=abaab.

Reduce RHS:

[1]ab(aab)
[3]⇒ a(bb)
⇒ ab

Defines rule #3.