Certificate for #18757 ⟨a, b | aaa=a, bbabbb=b⟩

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

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

[2] bbabbb=b

Axiom: bbabbb=b.

Referenced by [3], [4].

[3] bbabb=babbb

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

bbab bb bbabbb

Critical pair: bbabb=babbb.

Referenced by [4], [5].

[4] babbbb=b

Overlap of [2] bbabbb=b with [3] bbabb=babbb:

bbabbb bbabb

Critical pair: babbbb=b.

Defines rule #3.

Referenced by [5], [6].

[5] bbababbb=bab

Overlap of [3] bbabb=babbb with [3] bbabb=babbb:

bba bb bbabb

Critical pair: bbababbb=babbbabb.

Reduce RHS:

[3]bab(bbabb)
[3]⇒ ba(bbabb)b
[4]⇒ ba(babbbb)
⇒ bab

Referenced by [6].

[6] bbab=babb

Overlap of [5] bbababbb=bab with [4] babbbb=b:

bba babbb babbbb

Critical pair: bbab=babb.

Defines rule #2.