Certificate for #1601 ⟨a, b | aaa=bb, aab=b⟩

Back:⟨a, b | aaa=bb, aab=b⟩

Completion settings:

[1] aaa=bb

Axiom: aaa=bb.

Defines rule #4.

Referenced by [3], [4].

[2] aab=b

Axiom: aab=b.

Referenced by [4], [6].

[3] bba=abb

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

a aa aaa

Critical pair: abb=bba.

Flip LHS and RHS.

Referenced by [5].

[4] ab=bbb

Overlap of [1] aaa=bb with [2] aab=b:

a aa aab

Critical pair: ab=bbb.

Defines rule #2.

Referenced by [5], [6].

[5] bba=bbbb

Simplify [3] bba=abb.

Reduce RHS:

[4](ab)b
⇒ bbbb

Referenced by [7].

[6] bbbbb=b

Overlap of [2] aab=b with [4] ab=bbb:

a ab ab

Critical pair: abbb=b.

Reduce LHS:

[4](ab)bb
⇒ bbbbb

Defines rule #1.

Referenced by [7].

[7] ba=bbb

Overlap of [6] bbbbb=b with [5] bba=bbbb:

bbb bb bba

Critical pair: bbbbbbb=ba.

Reduce LHS:

[6](bbbbb)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #3.