Certificate for #20085 ⟨a, b | aab=b, abaa=bab⟩

Back:⟨a, b | aab=b, abaa=bab⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

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

[2] bab=abaa

Axiom: abaa=bab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[3] bbaa=baa

Overlap of [2] bab=abaa with [2] bab=abaa:

ba b bab

Critical pair: baabaa=abaaab.

Reduce LHS:

[1]b(aab)aa
⇒ bbaa

Reduce RHS:

[1]aba(aab)
[2]⇒ a(bab)
[1]⇒ (aab)aa
⇒ baa

Defines rule #3.

Referenced by [4], [5].

[4] abaaaa=abaa

Overlap of [2] bab=abaa with [3] bbaa=baa:

ba b bbaa

Critical pair: babaa=abaabaa.

Reduce LHS:

[2](bab)aa
⇒ abaaaa

Reduce RHS:

[1]ab(aab)aa
[3]⇒ a(bbaa)
⇒ abaa

Referenced by [6].

[5] bbb=bb

Overlap of [3] bbaa=baa with [1] aab=b:

bb aa aab

Critical pair: bbb=baab.

Reduce RHS:

[1]b(aab)
⇒ bb

Defines rule #5.

[6] baaaa=baa

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

a ab abaaaa

Critical pair: aabaa=baaaa.

Reduce LHS:

[1](aab)aa
⇒ baa

Flip LHS and RHS.

Defines rule #1.