Certificate for #4858 ⟨a, b | abbaaaab=bab⟩

Back:⟨a, b | abbaaaab=bab⟩

Completion settings:

[1] abbaaaab=bab

Axiom: abbaaaab=bab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

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

[3] abbaaaab=bc

Simplify [1] abbaaaab=bab.

Reduce RHS:

[2]b(ab)
⇒ bc

Referenced by [4].

[4] cbaaac=bc

Overlap of [3] abbaaaab=bc with [2] ab=c:

abbaaaab ab

Critical pair: cbaaaab=bc.

Reduce LHS:

[2]cbaaa(ab)
⇒ cbaaac

Defines rule #2.

Referenced by [5], [7].

[5] bbc=cbaacc

Overlap of [4] cbaaac=bc with [4] cbaaac=bc:

cbaaa c cbaaac

Critical pair: cbaaabc=bcbaaac.

Reduce LHS:

[2]cbaa(ab)c
⇒ cbaacc

Reduce RHS:

[4]b(cbaaac)
⇒ bbc

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] acbaacc=cbc

Overlap of [2] ab=c with [5] bbc=cbaacc:

a b bbc

Critical pair: acbaacc=cbc.

Defines rule #3.

[7] cbaacbc=bcbaacc

Overlap of [5] bbc=cbaacc with [4] cbaaac=bc:

bb c cbaaac

Critical pair: bbbc=cbaaccbaaac.

Reduce LHS:

[5]b(bbc)
⇒ bcbaacc

Reduce RHS:

[4]cbaac(cbaaac)
⇒ cbaacbc

Flip LHS and RHS.

Defines rule #5.