Certificate for #20103 ⟨a, b | aab=b, abba=bbb⟩

Back:⟨a, b | aab=b, abba=bbb⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #4.

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

[2] abba=bbb

Axiom: abba=bbb.

Referenced by [3], [4].

[3] bba=abbb

Overlap of [1] aab=b with [2] abba=bbb:

a ab abba

Critical pair: abbb=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] babbbb=abbb

Overlap of [2] abba=bbb with [1] aab=b:

abb a aab

Critical pair: abbb=bbbab.

Reduce RHS:

[3]b(bba)b
⇒ babbbb

Flip LHS and RHS.

Referenced by [5], [6].

[5] babbb=abbbbbbb

Overlap of [3] bba=abbb with [4] babbbb=abbb:

b ba babbbb

Critical pair: babbb=abbbbbbb.

Defines rule #2.

Referenced by [6].

[6] abbbbbbbb=abbb

Overlap of [4] babbbb=abbb with [5] babbb=abbbbbbb:

babbbb babbb

Critical pair: abbbbbbbb=abbb.

Referenced by [7].

[7] bbbbbbbb=bbb

Overlap of [1] aab=b with [6] abbbbbbbb=abbb:

a ab abbbbbbbb

Critical pair: aabbb=bbbbbbbb.

Reduce LHS:

[1](aab)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #1.