Certificate for #19231 ⟨a, b | aba=b, bbbbbb=b

Completion settings:

[1] aba=b

Axiom: aba=b.

Referenced by [3], [5].

[2] bbbbbb=b

Axiom: bbbbbb=b.

Defines rule #3.

Referenced by [4], [6].

[3] bba=abb

Overlap of [1] aba=b with [1] aba=b:

ab a aba

Critical pair: abb=bba.

Flip LHS and RHS.

Referenced by [4], [5].

[4] ba=ab

Overlap of [2] bbbbbb=b with [3] bba=abb:

bbbb bb bba

Critical pair: bbbbabb=ba.

Reduce LHS:

[3]bb(bba)bb
[3](bba)bbbb
[2]a(bbbbbb)
ab

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] aabb=bb

Overlap of [4] ba=ab with [1] aba=b:

b a aba

Critical pair: bb=abba.

Reduce RHS:

[3]a(bba)
aabb

Flip LHS and RHS.

Referenced by [6].

[6] aab=b

Overlap of [5] aabb=bb with [2] bbbbbb=b:

aa bb bbbbbb

Critical pair: aab=bbbbbb.

Reduce RHS:

[2](bbbbbb)
b

Defines rule #2.