Certificate for #4948 ⟨a, b | aaaabaa=aaab⟩

Back:⟨a, b | aaaabaa=aaab⟩

Completion settings:

[1] aaaabaa=aaab

Axiom: aaaabaa=aaab.

Referenced by [3].

[2] aaab=c

Axiom: aaab=c.

Defines rule #5.

Referenced by [3], [4], [6], [7].

[3] aaaabaa=c

Simplify [1] aaaabaa=aaab.

Reduce RHS:

[2](aaab)
⇒ c

Referenced by [4].

[4] acaa=c

Overlap of [3] aaaabaa=c with [2] aaab=c:

a aaabaa aaab

Critical pair: acaa=c.

Defines rule #1.

Referenced by [5], [6], [7], [8].

[5] ccaa=acac

Overlap of [4] acaa=c with [4] acaa=c:

aca a acaa

Critical pair: acac=ccaa.

Flip LHS and RHS.

Defines rule #2.

[6] cab=acc

Overlap of [4] acaa=c with [2] aaab=c:

ac aa aaab

Critical pair: acc=cab.

Flip LHS and RHS.

Defines rule #4.

[7] caab=acac

Overlap of [4] acaa=c with [2] aaab=c:

aca a aaab

Critical pair: acac=caab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [8].

[8] cb=aacac

Overlap of [4] acaa=c with [7] caab=acac:

a caa caab

Critical pair: aacac=cb.

Flip LHS and RHS.

Defines rule #3.