Certificate for #19301 ⟨a, b | aaa=a, bbbbb=aa

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Referenced by [3].

[2] aa=bbbbb

Axiom: bbbbb=aa.

Flip LHS and RHS.

Defines rule #4.

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

[3] bbbbba=a

Overlap of [1] aaa=a with [2] aa=bbbbb:

aaa aa

Critical pair: bbbbba=a.

Defines rule #3.

Referenced by [4], [5].

[4] abbbbb=a

Overlap of [2] aa=bbbbb with [2] aa=bbbbb:

a a aa

Critical pair: abbbbb=bbbbba.

Reduce RHS:

[3](bbbbba)
a

Defines rule #2.

[5] bbbbbbbbbb=bbbbb

Overlap of [3] bbbbba=a with [2] aa=bbbbb:

bbbbb a aa

Critical pair: bbbbbbbbbb=aa.

Reduce RHS:

[2](aa)
bbbbb

Defines rule #1.