Certificate for #4153 ⟨a, b | abb=aaa, bab=b⟩

Back:⟨a, b | abb=aaa, bab=b⟩

Completion settings:

[1] aaa=abb

Axiom: abb=aaa.

Flip LHS and RHS.

Defines rule #5.

Referenced by [3], [6].

[2] bab=b

Axiom: bab=b.

Defines rule #2.

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

[3] abba=aabb

Overlap of [1] aaa=abb with [1] aaa=abb:

a aa aaa

Critical pair: aabb=abba.

Flip LHS and RHS.

Referenced by [4], [5].

[4] baabb=bba

Overlap of [2] bab=b with [3] abba=aabb:

b ab abba

Critical pair: baabb=bba.

Referenced by [7].

[5] aabbb=abb

Overlap of [3] abba=aabb with [2] bab=b:

ab ba bab

Critical pair: abb=aabbb.

Flip LHS and RHS.

Referenced by [6].

[6] aabb=abbbbb

Overlap of [1] aaa=abb with [5] aabbb=abb:

a aa aabbb

Critical pair: aabb=abbbbb.

Defines rule #4.

Referenced by [7].

[7] bba=bbbbb

Simplify [4] baabb=bba.

Reduce LHS:

[6]b(aabb)
[2]⇒ (bab)bbbb
⇒ bbbbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[8] bbbbbb=bb

Overlap of [7] bba=bbbbb with [2] bab=b:

b ba bab

Critical pair: bb=bbbbbb.

Flip LHS and RHS.

Defines rule #1.