Certificate for #5920 ⟨a, b | abbaab=abbba⟩

Back:⟨a, b | abbaab=abbba⟩

Completion settings:

[1] abbaab=abbba

Axiom: abbaab=abbba.

Defines rule #4.

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

[2] abbbab=c

Axiom: abbbab=c.

Defines rule #6.

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

[3] cbbab=abbbc

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

abbb ab abbbab

Critical pair: abbbc=cbbab.

Flip LHS and RHS.

Defines rule #5.

[4] caab=cba

Overlap of [1] abbaab=abbba with [1] abbaab=abbba:

abba ab abbaab

Critical pair: abbaabbba=abbbabaab.

Reduce LHS:

[1](abbaab)bba
[2]⇒ (abbbab)ba
⇒ cba

Reduce RHS:

[2](abbbab)aab
⇒ caab

Flip LHS and RHS.

Defines rule #1.

[5] cbab=abbac

Overlap of [1] abbaab=abbba with [2] abbbab=c:

abba ab abbbab

Critical pair: abbac=abbbabbab.

Reduce RHS:

[2](abbbab)bab
⇒ cbab

Flip LHS and RHS.

Defines rule #2.

[6] cbaab=cbba

Overlap of [2] abbbab=c with [1] abbaab=abbba:

abbb ab abbaab

Critical pair: abbbabbba=cbaab.

Reduce LHS:

[2](abbbab)bba
⇒ cbba

Flip LHS and RHS.

Defines rule #3.