Certificate for #19070 ⟨a, b | aab=b, bbabbb=a⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #3.

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

[2] bbabbb=a

Axiom: bbabbb=a.

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

[3] aaa=a

Overlap of [1] aab=b with [2] bbabbb=a:

aa b bbabbb

Critical pair: aaa=bbabbb.

Reduce RHS:

[2](bbabbb)
⇒ a

Defines rule #2.

[4] bbaba=bbb

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

bbab bb bbabbb

Critical pair: bbaba=aabbb.

Reduce RHS:

[1](aab)bb
⇒ bbb

Referenced by [6].

[5] bbabba=ababbb

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

bbabb b bbabbb

Critical pair: bbabba=ababbb.

Referenced by [7].

[6] ba=ab

Overlap of [2] bbabbb=a with [4] bbaba=bbb:

bbab bb bbaba

Critical pair: bbabbbb=aaba.

Reduce LHS:

[2](bbabbb)b
⇒ ab

Reduce RHS:

[1](aab)a
⇒ ba

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] bbbbb=aa

Overlap of [2] bbabbb=a with [6] ba=ab:

bbabb b ba

Critical pair: bbabbab=aa.

Reduce LHS:

[5](bbabba)b
[6]⇒ a(ba)bbbb
[1]⇒ (aab)bbbb
⇒ bbbbb

Defines rule #4.