Certificate for #8636 ⟨a, b | aa=a, bbabbb=a⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #3.

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

[2] bbabbb=a

Axiom: bbabbb=a.

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

[3] bbaba=abbb

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

bbab bb bbabbb

Critical pair: bbaba=aabbb.

Reduce RHS:

[1](aa)bbb
⇒ abbb

Referenced by [5].

[4] bbabba=ababbb

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

bbabb b bbabbb

Critical pair: bbabba=ababbb.

Referenced by [6].

[5] aba=abbbbbb

Overlap of [2] bbabbb=a with [3] bbaba=abbb:

bbab bb bbaba

Critical pair: bbababbb=aaba.

Reduce LHS:

[3](bbaba)bbb
⇒ abbbbbb

Reduce RHS:

[1](aa)ba
⇒ aba

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[6] bbabba=abbbbbbbbb

Simplify [4] bbabba=ababbb.

Reduce RHS:

[5](aba)bbb
⇒ abbbbbbbbb

Referenced by [7].

[7] bba=abbbbbbbbbbbb

Overlap of [6] bbabba=abbbbbbbbb with [2] bbabbb=a:

bba bba bbabbb

Critical pair: bbaa=abbbbbbbbbbbb.

Reduce LHS:

[1]bb(aa)
⇒ bba

Defines rule #2.

Referenced by [8].

[8] abbbbbbbbbbbbbbb=a

Overlap of [2] bbabbb=a with [7] bba=abbbbbbbbbbbb:

bbabbb bba

Critical pair: abbbbbbbbbbbbbbb=a.

Defines rule #1.