Certificate for #1787 ⟨a, b, c | aab=cc, cab=1⟩

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

Completion settings:

[1] cc=aab

Axiom: aab=cc.

Flip LHS and RHS.

Referenced by [3], [4].

[2] cab=1

Axiom: cab=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=aabab

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

c c cab

Critical pair: c=aabab.

Defines rule #3.

Referenced by [5], [6].

[5] aababab=1

Overlap of [2] cab=1 with [4] c=aabab:

cab c

Critical pair: aababab=1.

Defines rule #1.

[6] aababaab=aabaabab

Simplify [3] aabc=caab.

Reduce LHS:

[4]aab(c)
⇒ aabaabab

Reduce RHS:

[4](c)aab
⇒ aababaab

Flip LHS and RHS.

Defines rule #2.