Certificate for #22322 ⟨a, b | aaa=1, bbabbb=ab⟩

Back:⟨a, b | aaa=1, bbabbb=ab⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

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

[2] bbabbb=ab

Axiom: bbabbb=ab.

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

[3] bbabbab=aab

Overlap of [2] bbabbb=ab with [2] bbabbb=ab:

bbabb b bbabbb

Critical pair: bbabbab=abbabbb.

Reduce RHS:

[2]a(bbabbb)
⇒ aab

Referenced by [4], [5].

[4] bbaab=aabbb

Overlap of [3] bbabbab=aab with [2] bbabbb=ab:

bba bbab bbabbb

Critical pair: bbaab=aabbb.

Defines rule #3.

[5] aabbab=bbb

Overlap of [3] bbabbab=aab with [3] bbabbab=aab:

bba bbab bbabbab

Critical pair: bbaaab=aabbab.

Reduce LHS:

[1]bb(aaa)b
⇒ bbb

Flip LHS and RHS.

Referenced by [6], [7].

[6] bbab=abbb

Overlap of [1] aaa=1 with [5] aabbab=bbb:

a aa aabbab

Critical pair: abbb=bbab.

Flip LHS and RHS.

Defines rule #2.

[7] bbbbb=b

Overlap of [5] aabbab=bbb with [2] bbabbb=ab:

aa bbab bbabbb

Critical pair: aaab=bbbbb.

Reduce LHS:

[1](aaa)b
⇒ b

Flip LHS and RHS.

Defines rule #4.