Certificate for #1790 ⟨a, b, c | aab=cc, cbb=1⟩

Back:⟨a, b, c | aab=cc, cbb=1⟩

Completion settings:

[1] cc=aab

Axiom: aab=cc.

Flip LHS and RHS.

Referenced by [3], [4].

[2] cbb=1

Axiom: cbb=1.

Referenced by [4], [5].

[3] aabc=caab

Overlap of [1] cc=aab with [1] cc=aab:

c c cc

Critical pair: caab=aabc.

Flip LHS and RHS.

Referenced by [6].

[4] c=aabbb

Overlap of [1] cc=aab with [2] cbb=1:

c c cbb

Critical pair: c=aabbb.

Defines rule #3.

Referenced by [5], [6].

[5] aabbbbb=1

Overlap of [2] cbb=1 with [4] c=aabbb:

cbb c

Critical pair: aabbbbb=1.

Defines rule #1.

[6] aabbbaab=aabaabbb

Simplify [3] aabc=caab.

Reduce LHS:

[4]aab(c)
⇒ aabaabbb

Reduce RHS:

[4](c)aab
⇒ aabbbaab

Flip LHS and RHS.

Defines rule #2.