Certificate for #2723 ⟨a, b | abbba=abbab⟩

Back:⟨a, b | abbba=abbab⟩

Completion settings:

[1] abbab=abbba

Axiom: abbba=abbab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [4], [5], [6], [9], [11], [13].

[2] abbbabb=c

Axiom: abbbabb=c.

Defines rule #14.

Referenced by [3], [4], [5], [6], [9], [10], [13], [16], [21].

[3] cbabb=abbbc

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

abbb abb abbbabb

Critical pair: abbbc=cbabb.

Flip LHS and RHS.

Referenced by [8].

[4] abbbabab=ca

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

abb ab abbab

Critical pair: abbabbba=abbbabab.

Reduce LHS:

[1](abbab)bba
[2]⇒ (abbbabb)a
⇒ ca

Flip LHS and RHS.

Defines rule #17.

Referenced by [13], [14], [15], [18].

[5] cabb=abbc

Overlap of [1] abbab=abbba with [2] abbbabb=c:

abb ab abbbabb

Critical pair: abbc=abbbabbabb.

Reduce RHS:

[2](abbbabb)abb
⇒ cabb

Flip LHS and RHS.

Referenced by [7].

[6] cab=cba

Overlap of [2] abbbabb=c with [1] abbab=abbba:

abbb abb abbab

Critical pair: abbbabbba=cab.

Reduce LHS:

[2](abbbabb)ba
⇒ cba

Flip LHS and RHS.

Defines rule #1.

Referenced by [7], [11], [12], [13], [14], [15], [16], [17], [18], [21], [22].

[7] cbab=abbc

Simplify [5] cabb=abbc.

Reduce LHS:

[6](cab)b
⇒ cbab

Defines rule #3.

Referenced by [8], [11], [12], [14], [15].

[8] abbcb=abbbc

Simplify [3] cbabb=abbbc.

Reduce LHS:

[7](cbab)b
⇒ abbcb

Defines rule #7.

Referenced by [9], [10], [11], [14], [15], [16], [17], [18], [19], [21].

[9] abbbabcb=cc

Overlap of [1] abbab=abbba with [8] abbcb=abbbc:

abb ab abbcb

Critical pair: abbabbbc=abbbabcb.

Reduce LHS:

[1](abbab)bbc
[2]⇒ (abbbabb)c
⇒ cc

Flip LHS and RHS.

Defines rule #18.

Referenced by [16], [18], [21].

[10] ccb=cbc

Overlap of [2] abbbabb=c with [8] abbcb=abbbc:

abbb abb abbcb

Critical pair: abbbabbbc=ccb.

Reduce LHS:

[2](abbbabb)bc
⇒ cbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [12], [16], [20], [21], [22].

[11] abbbcba=abbbabc

Overlap of [8] abbcb=abbbc with [7] cbab=abbc:

abb cb cbab

Critical pair: abbabbc=abbbcab.

Reduce LHS:

[1](abbab)bc
⇒ abbbabc

Reduce RHS:

[6]abbb(cab)
⇒ abbbcba

Flip LHS and RHS.

Defines rule #15.

Referenced by [16], [17], [18].

[12] cbcba=abbcc

Overlap of [10] ccb=cbc with [7] cbab=abbc:

c cb cbab

Critical pair: cabbc=cbcab.

Reduce LHS:

[6](cab)bc
[7]⇒ (cbab)c
⇒ abbcc

Reduce RHS:

[6]cb(cab)
⇒ cbcba

Flip LHS and RHS.

Defines rule #10.

[13] cbaab=abbca

Overlap of [1] abbab=abbba with [4] abbbabab=ca:

abb ab abbbabab

Critical pair: abbca=abbbabbabab.

Reduce RHS:

[2](abbbabb)abab
[6]⇒ (cab)ab
⇒ cbaab

Flip LHS and RHS.

Defines rule #8.

Referenced by [16], [17], [18].

[14] cbacb=abbcc

Overlap of [4] abbbabab=ca with [8] abbcb=abbbc:

abbbab ab abbcb

Critical pair: abbbababbbc=cabcb.

Reduce LHS:

[4](abbbabab)bbc
[6]⇒ (cab)bc
[7]⇒ (cbab)c
⇒ abbcc

Reduce RHS:

[6](cab)cb
⇒ cbacb

Flip LHS and RHS.

Defines rule #9.

Referenced by [21].

[15] abbbcaab=abbbabca

Overlap of [4] abbbabab=ca with [4] abbbabab=ca:

abbbab ab abbbabab

Critical pair: abbbabca=cabbabab.

Reduce RHS:

[6](cab)babab
[7]⇒ (cbab)abab
[6]⇒ abb(cab)ab
[8]⇒ (abbcb)aab
⇒ abbbcaab

Flip LHS and RHS.

Defines rule #19.

[16] cbca=cbac

Overlap of [13] cbaab=abbca with [2] abbbabb=c:

cba ab abbbabb

Critical pair: cbac=abbcabbabb.

Reduce RHS:

[6]abb(cab)babb
[8]⇒ (abbcb)ababb
[6]⇒ abbb(cab)abb
[11]⇒ (abbbcba)abb
[6]⇒ abbbab(cab)b
[9]⇒ (abbbabcb)ab
[6]⇒ c(cab)
[10]⇒ (ccb)a
⇒ cbca

Flip LHS and RHS.

Defines rule #4.

Referenced by [19], [20].

[17] abbbcacb=abbbabcc

Overlap of [13] cbaab=abbca with [8] abbcb=abbbc:

cba ab abbcb

Critical pair: cbaabbbc=abbcabcb.

Reduce LHS:

[13](cbaab)bbc
[6]⇒ abb(cab)bc
[8]⇒ (abbcb)abc
[6]⇒ abbb(cab)c
[11]⇒ (abbbcba)c
⇒ abbbabcc

Reduce RHS:

[6]abb(cab)cb
[8]⇒ (abbcb)acb
⇒ abbbcacb

Flip LHS and RHS.

Defines rule #20.

Referenced by [21].

[18] ccaab=cbaca

Overlap of [13] cbaab=abbca with [4] abbbabab=ca:

cba ab abbbabab

Critical pair: cbaca=abbcabbabab.

Reduce RHS:

[6]abb(cab)babab
[8]⇒ (abbcb)ababab
[6]⇒ abbb(cab)abab
[11]⇒ (abbbcba)abab
[6]⇒ abbbab(cab)ab
[9]⇒ (abbbabcb)aab
⇒ ccaab

Flip LHS and RHS.

Defines rule #12.

Referenced by [21].

[19] abbbcca=abbbcac

Overlap of [8] abbcb=abbbc with [16] cbca=cbac:

abb cb cbca

Critical pair: abbcbac=abbbcca.

Reduce LHS:

[8](abbcb)ac
⇒ abbbcac

Flip LHS and RHS.

Defines rule #16.

Referenced by [21].

[20] cbcca=cbacc

Overlap of [10] ccb=cbc with [16] cbca=cbac:

c cb cbca

Critical pair: ccbac=cbcca.

Reduce LHS:

[10](ccb)ac
[16]⇒ (cbca)c
⇒ cbacc

Flip LHS and RHS.

Defines rule #11.

Referenced by [22].

[21] ccca=ccac

Overlap of [18] ccaab=cbaca with [2] abbbabb=c:

cca ab abbbabb

Critical pair: ccac=cbacabbabb.

Reduce RHS:

[6]cba(cab)babb
[14]⇒ (cbacb)ababb
[6]⇒ abbc(cab)abb
[10]⇒ abb(ccb)aabb
[8]⇒ (abbcb)caabb
[19]⇒ (abbbcca)abb
[6]⇒ abbbca(cab)b
[17]⇒ (abbbcacb)ab
[6]⇒ abbbabc(cab)
[10]⇒ abbbab(ccb)a
[9]⇒ (abbbabcb)ca
⇒ ccca

Flip LHS and RHS.

Defines rule #5.

Referenced by [22].

[22] ccacb=cbacc

Overlap of [21] ccca=ccac with [6] cab=cba:

cc ca cab

Critical pair: cccba=ccacb.

Reduce LHS:

[10]c(ccb)a
[10]⇒ (ccb)ca
[20]⇒ (cbcca)
⇒ cbacc

Flip LHS and RHS.

Defines rule #13.