Certificate for #6428 ⟨a, b | aab=b, babbb=a⟩

Back:⟨a, b | aab=b, babbb=a⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

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

[2] babbb=a

Axiom: babbb=a.

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

[3] babba=bbb

Overlap of [2] babbb=a with [2] babbb=a:

babb b babbb

Critical pair: babba=aabbb.

Reduce RHS:

[1](aab)bb
⇒ bbb

Referenced by [4], [5].

[4] bba=abb

Overlap of [2] babbb=a with [3] babba=bbb:

babb b babba

Critical pair: babbbbb=aabba.

Reduce LHS:

[2](babbb)bb
⇒ abb

Reduce RHS:

[1](aab)ba
⇒ bba

Flip LHS and RHS.

Referenced by [6], [7].

[5] baba=bbbbbb

Overlap of [3] babba=bbb with [2] babbb=a:

bab ba babbb

Critical pair: baba=bbbbbb.

Referenced by [6].

[6] aa=bbbbbbbb

Overlap of [2] babbb=a with [4] bba=abb:

bab bb bba

Critical pair: bababb=aa.

Reduce LHS:

[5](baba)bb
⇒ bbbbbbbb

Flip LHS and RHS.

Defines rule #4.

Referenced by [9].

[7] ba=abbbbb

Overlap of [4] bba=abb with [2] babbb=a:

b ba babbb

Critical pair: ba=abbbbb.

Defines rule #3.

Referenced by [8].

[8] abbbbbbbb=a

Overlap of [2] babbb=a with [7] ba=abbbbb:

babbb ba

Critical pair: abbbbbbbb=a.

Defines rule #2.

[9] bbbbbbbbb=b

Overlap of [1] aab=b with [6] aa=bbbbbbbb:

aab aa

Critical pair: bbbbbbbbb=b.

Defines rule #1.