Certificate for #19507 ⟨a, b | aab=b, aaaaa=bb⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Referenced by [3], [5].

[2] aaaaa=bb

Axiom: aaaaa=bb.

Defines rule #4.

Referenced by [3], [4].

[3] ab=bbb

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

aaa aa aab

Critical pair: aaab=bbb.

Reduce LHS:

[1]a(aab)
⇒ ab

Defines rule #2.

Referenced by [4], [5].

[4] bba=bbbb

Overlap of [2] aaaaa=bb with [2] aaaaa=bb:

a aaaa aaaaa

Critical pair: abb=bba.

Reduce LHS:

[3](ab)b
⇒ bbbb

Flip LHS and RHS.

Referenced by [6].

[5] bbbbb=b

Overlap of [1] aab=b with [3] ab=bbb:

a ab ab

Critical pair: abbb=b.

Reduce LHS:

[3](ab)bb
⇒ bbbbb

Defines rule #1.

Referenced by [6].

[6] ba=bbb

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

bbb bb bba

Critical pair: bbbbbbb=ba.

Reduce LHS:

[5](bbbbb)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #3.