Certificate for #19539 ⟨a, b | aab=b, abaaa=bb⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

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

[2] abaaa=bb

Axiom: abaaa=bb.

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

[3] baaa=abb

Overlap of [1] aab=b with [2] abaaa=bb:

a ab abaaa

Critical pair: abb=baaa.

Flip LHS and RHS.

Defines rule #4.

[4] abab=bbb

Overlap of [2] abaaa=bb with [1] aab=b:

aba aa aab

Critical pair: abab=bbb.

Referenced by [6], [7].

[5] bbab=abb

Overlap of [2] abaaa=bb with [1] aab=b:

abaa a aab

Critical pair: abaab=bbab.

Reduce LHS:

[1]ab(aab)
⇒ abb

Flip LHS and RHS.

Referenced by [7].

[6] bab=abbb

Overlap of [1] aab=b with [4] abab=bbb:

a ab abab

Critical pair: abbb=bab.

Flip LHS and RHS.

Defines rule #2.

[7] bbbbb=bb

Overlap of [5] bbab=abb with [4] abab=bbb:

bb ab abab

Critical pair: bbbbb=abbab.

Reduce RHS:

[5]a(bbab)
[1]⇒ (aab)b
⇒ bb

Defines rule #1.