Certificate for #5332 ⟨a, b | abaabba=baab⟩

Back:⟨a, b | abaabba=baab⟩

Completion settings:

[1] abaabba=baab

Axiom: abaabba=baab.

Referenced by [3].

[2] baab=c

Axiom: baab=c.

Defines rule #3.

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

[3] abaabba=c

Simplify [1] abaabba=baab.

Reduce RHS:

[2](baab)
⇒ c

Referenced by [4].

[4] acba=c

Overlap of [3] abaabba=c with [2] baab=c:

a baabba baab

Critical pair: acba=c.

Defines rule #2.

Referenced by [5], [7].

[5] ccba=acbc

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

acb a acba

Critical pair: acbc=ccba.

Flip LHS and RHS.

Defines rule #5.

[6] caab=baac

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

baa b baab

Critical pair: baac=caab.

Flip LHS and RHS.

Defines rule #4.

[7] cab=acc

Overlap of [4] acba=c with [2] baab=c:

ac ba baab

Critical pair: acc=cab.

Flip LHS and RHS.

Defines rule #1.