Certificate for #5886 ⟨a, b | ababba=abaab⟩

Back:⟨a, b | ababba=abaab⟩

Completion settings:

[1] ababba=abaab

Axiom: ababba=abaab.

Referenced by [3].

[2] abaab=c

Axiom: abaab=c.

Defines rule #5.

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

[3] ababba=c

Simplify [1] ababba=abaab.

Reduce RHS:

[2](abaab)
⇒ c

Defines rule #6.

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

[4] caab=abac

Overlap of [2] abaab=c with [2] abaab=c:

aba ab abaab

Critical pair: abac=caab.

Flip LHS and RHS.

Defines rule #1.

[5] cbabba=ababbc

Overlap of [3] ababba=c with [3] ababba=c:

ababb a ababba

Critical pair: ababbc=cbabba.

Flip LHS and RHS.

Defines rule #4.

[6] cbaab=ababbc

Overlap of [3] ababba=c with [2] abaab=c:

ababb a abaab

Critical pair: ababbc=cbaab.

Flip LHS and RHS.

Defines rule #3.

[7] cabba=abac

Overlap of [2] abaab=c with [3] ababba=c:

aba ab ababba

Critical pair: abac=cabba.

Flip LHS and RHS.

Defines rule #2.