Certificate for #21741 ⟨a, b | aaa=1, abbabbb=b⟩

Back:⟨a, b | aaa=1, abbabbb=b⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [3], [8].

[2] abbabbb=b

Axiom: abbabbb=b.

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

[3] bbabbb=aab

Overlap of [1] aaa=1 with [2] abbabbb=b:

aa a abbabbb

Critical pair: aab=bbabbb.

Flip LHS and RHS.

Defines rule #3.

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

[4] abbabbaab=aab

Overlap of [2] abbabbb=b with [3] bbabbb=aab:

abbabb b bbabbb

Critical pair: abbabbaab=bbabbb.

Reduce RHS:

[3](bbabbb)
⇒ aab

Referenced by [8].

[5] bbabaab=aababbb

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

bbab bb bbabbb

Critical pair: bbabaab=aababbb.

Defines rule #5.

[6] bbabbaab=ab

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

bbabb b bbabbb

Critical pair: bbabbaab=aabbabbb.

Reduce RHS:

[2]a(abbabbb)
⇒ ab

Referenced by [7], [8].

[7] babbaab=abbabab

Overlap of [2] abbabbb=b with [6] bbabbaab=ab:

abbab bb bbabbaab

Critical pair: abbabab=babbaab.

Flip LHS and RHS.

Defines rule #4.

[8] bbabbab=b

Overlap of [3] bbabbb=aab with [6] bbabbaab=ab:

bbabb b bbabbaab

Critical pair: bbabbab=aabbabbaab.

Reduce RHS:

[4]a(abbabbaab)
[1]⇒ (aaa)b
⇒ b

Referenced by [9].

[9] babbab=abbabb

Overlap of [2] abbabbb=b with [8] bbabbab=b:

abbab bb bbabbab

Critical pair: abbabb=babbab.

Flip LHS and RHS.

Defines rule #2.