Certificate for #3263 ⟨a, b, c | bb=ac, aaab=1⟩

Back:⟨a, b, c | bb=ac, aaab=1⟩

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Referenced by [3], [4].

[2] aaab=1

Axiom: aaab=1.

Referenced by [4], [6].

[3] bac=acb

Overlap of [1] bb=ac with [1] bb=ac:

b b bb

Critical pair: bac=acb.

Referenced by [5].

[4] b=aaaac

Overlap of [2] aaab=1 with [1] bb=ac:

aaa b bb

Critical pair: aaaac=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] acaaaac=aaaacac

Simplify [3] bac=acb.

Reduce LHS:

[4](b)ac
⇒ aaaacac

Reduce RHS:

[4]ac(b)
⇒ acaaaac

Flip LHS and RHS.

Defines rule #1.

[6] aaaaaaac=1

Overlap of [2] aaab=1 with [4] b=aaaac:

aaa b b

Critical pair: aaaaaaac=1.

Defines rule #2.