Certificate for #2021 ⟨a, b | abaaaaab=ba⟩

Back:⟨a, b | abaaaaab=ba⟩

Completion settings:

[1] abaaaaab=ba

Axiom: abaaaaab=ba.

Referenced by [3].

[2] baaaaa=c

Axiom: baaaaa=c.

Referenced by [3], [4].

[3] ba=acb

Overlap of [1] abaaaaab=ba with [2] baaaaa=c:

a baaaaab baaaaa

Critical pair: acb=ba.

Flip LHS and RHS.

Defines rule #2.

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

[4] acacacacacb=c

Overlap of [2] baaaaa=c with [3] ba=acb:

baaaaa ba

Critical pair: acbaaaa=c.

Reduce LHS:

[3]ac(ba)aaa
[3]⇒ acac(ba)aa
[3]⇒ acacac(ba)a
[3]⇒ acacacac(ba)
⇒ acacacacacb

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

[5] acbcacacacacb=bc

Overlap of [3] ba=acb with [4] acacacacacb=c:

b a acacacacacb

Critical pair: bc=acbcacacacacb.

Flip LHS and RHS.

Referenced by [7].

[6] ca=acc

Overlap of [4] acacacacacb=c with [3] ba=acb:

acacacacac b ba

Critical pair: acacacacacacb=ca.

Reduce LHS:

[4]ac(acacacacacb)
⇒ acc

Flip LHS and RHS.

Defines rule #3.

Referenced by [7], [8].

[7] aaaaacccccccccccccccccccccccccccccccbcccccccccccccccccccccccccccccccb=bc

Simplify [5] acbcacacacacb=bc.

Reduce LHS:

[6]acb(ca)cacacacb
[3]⇒ ac(ba)cccacacacb
[6]⇒ a(ca)cbcccacacacb
[6]⇒ aacccbcc(ca)cacacb
[6]⇒ aacccbc(ca)cccacacb
[6]⇒ aacccb(ca)cccccacacb
[3]⇒ aaccc(ba)cccccccacacb
[6]⇒ aacc(ca)cbcccccccacacb
[6]⇒ aac(ca)cccbcccccccacacb
[6]⇒ aa(ca)cccccbcccccccacacb
[6]⇒ aaacccccccbcccccc(ca)cacb
[6]⇒ aaacccccccbccccc(ca)cccacb
[6]⇒ aaacccccccbcccc(ca)cccccacb
[6]⇒ aaacccccccbccc(ca)cccccccacb
[6]⇒ aaacccccccbcc(ca)cccccccccacb
[6]⇒ aaacccccccbc(ca)cccccccccccacb
[6]⇒ aaacccccccb(ca)cccccccccccccacb
[3]⇒ aaaccccccc(ba)cccccccccccccccacb
[6]⇒ aaacccccc(ca)cbcccccccccccccccacb
[6]⇒ aaaccccc(ca)cccbcccccccccccccccacb
[6]⇒ aaacccc(ca)cccccbcccccccccccccccacb
[6]⇒ aaaccc(ca)cccccccbcccccccccccccccacb
[6]⇒ aaacc(ca)cccccccccbcccccccccccccccacb
[6]⇒ aaac(ca)cccccccccccbcccccccccccccccacb
[6]⇒ aaa(ca)cccccccccccccbcccccccccccccccacb
[6]⇒ aaaacccccccccccccccbcccccccccccccc(ca)cb
[6]⇒ aaaacccccccccccccccbccccccccccccc(ca)cccb
[6]⇒ aaaacccccccccccccccbcccccccccccc(ca)cccccb
[6]⇒ aaaacccccccccccccccbccccccccccc(ca)cccccccb
[6]⇒ aaaacccccccccccccccbcccccccccc(ca)cccccccccb
[6]⇒ aaaacccccccccccccccbccccccccc(ca)cccccccccccb
[6]⇒ aaaacccccccccccccccbcccccccc(ca)cccccccccccccb
[6]⇒ aaaacccccccccccccccbccccccc(ca)cccccccccccccccb
[6]⇒ aaaacccccccccccccccbcccccc(ca)cccccccccccccccccb
[6]⇒ aaaacccccccccccccccbccccc(ca)cccccccccccccccccccb
[6]⇒ aaaacccccccccccccccbcccc(ca)cccccccccccccccccccccb
[6]⇒ aaaacccccccccccccccbccc(ca)cccccccccccccccccccccccb
[6]⇒ aaaacccccccccccccccbcc(ca)cccccccccccccccccccccccccb
[6]⇒ aaaacccccccccccccccbc(ca)cccccccccccccccccccccccccccb
[6]⇒ aaaacccccccccccccccb(ca)cccccccccccccccccccccccccccccb
[3]⇒ aaaaccccccccccccccc(ba)cccccccccccccccccccccccccccccccb
[6]⇒ aaaacccccccccccccc(ca)cbcccccccccccccccccccccccccccccccb
[6]⇒ aaaaccccccccccccc(ca)cccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaacccccccccccc(ca)cccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaaccccccccccc(ca)cccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaacccccccccc(ca)cccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaaccccccccc(ca)cccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaacccccccc(ca)cccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaaccccccc(ca)cccccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaacccccc(ca)cccccccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaaccccc(ca)cccccccccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaacccc(ca)cccccccccccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaaccc(ca)cccccccccccccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaacc(ca)cccccccccccccccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaac(ca)cccccccccccccccccccccccccccbcccccccccccccccccccccccccccccccb
[6]⇒ aaaa(ca)cccccccccccccccccccccccccccccbcccccccccccccccccccccccccccccccb
⇒ aaaaacccccccccccccccccccccccccccccccbcccccccccccccccccccccccccccccccb

Referenced by [9].

[8] aaaaacccccccccccccccccccccccccccccccb=c

Overlap of [4] acacacacacb=c with [6] ca=acc:

a cacacacacb ca

Critical pair: aacccacacacb=c.

Reduce LHS:

[6]aacc(ca)cacacb
[6]⇒ aac(ca)cccacacb
[6]⇒ aa(ca)cccccacacb
[6]⇒ aaacccccc(ca)cacb
[6]⇒ aaaccccc(ca)cccacb
[6]⇒ aaacccc(ca)cccccacb
[6]⇒ aaaccc(ca)cccccccacb
[6]⇒ aaacc(ca)cccccccccacb
[6]⇒ aaac(ca)cccccccccccacb
[6]⇒ aaa(ca)cccccccccccccacb
[6]⇒ aaaacccccccccccccc(ca)cb
[6]⇒ aaaaccccccccccccc(ca)cccb
[6]⇒ aaaacccccccccccc(ca)cccccb
[6]⇒ aaaaccccccccccc(ca)cccccccb
[6]⇒ aaaacccccccccc(ca)cccccccccb
[6]⇒ aaaaccccccccc(ca)cccccccccccb
[6]⇒ aaaacccccccc(ca)cccccccccccccb
[6]⇒ aaaaccccccc(ca)cccccccccccccccb
[6]⇒ aaaacccccc(ca)cccccccccccccccccb
[6]⇒ aaaaccccc(ca)cccccccccccccccccccb
[6]⇒ aaaacccc(ca)cccccccccccccccccccccb
[6]⇒ aaaaccc(ca)cccccccccccccccccccccccb
[6]⇒ aaaacc(ca)cccccccccccccccccccccccccb
[6]⇒ aaaac(ca)cccccccccccccccccccccccccccb
[6]⇒ aaaa(ca)cccccccccccccccccccccccccccccb
⇒ aaaaacccccccccccccccccccccccccccccccb

Defines rule #4.

Referenced by [9].

[9] ccccccccccccccccccccccccccccccccb=bc

Overlap of [7] aaaaacccccccccccccccccccccccccccccccbcccccccccccccccccccccccccccccccb=bc with [8] aaaaacccccccccccccccccccccccccccccccb=c:

aaaaacccccccccccccccccccccccccccccccbcccccccccccccccccccccccccccccccb aaaaacccccccccccccccccccccccccccccccb

Critical pair: ccccccccccccccccccccccccccccccccb=bc.

Defines rule #1.