Certificate for #4063 ⟨a, b | aabaaaaab=ba⟩

Back:⟨a, b | aabaaaaab=ba⟩

Completion settings:

[1] aabaaaaab=ba

Axiom: aabaaaaab=ba.

Referenced by [3].

[2] baaaaa=c

Axiom: baaaaa=c.

Referenced by [3], [4].

[3] ba=aacb

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

aa baaaaab baaaaa

Critical pair: aacb=ba.

Flip LHS and RHS.

Defines rule #3.

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

[4] aacaacaacaacaacb=c

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

baaaaa ba

Critical pair: aacbaaaa=c.

Reduce LHS:

[3]aac(ba)aaa
[3]⇒ aacaac(ba)aa
[3]⇒ aacaacaac(ba)a
[3]⇒ aacaacaacaac(ba)
⇒ aacaacaacaacaacb

Defines rule #2.

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

[5] aacaacbcaacaacaacaacb=bc

Overlap of [3] ba=aacb with [4] aacaacaacaacaacb=c:

b a aacaacaacaacaacb

Critical pair: bc=aacbacaacaacaacaacb.

Reduce RHS:

[3]aac(ba)caacaacaacaacb
⇒ aacaacbcaacaacaacaacb

Flip LHS and RHS.

Referenced by [10].

[6] aacc=ca

Overlap of [4] aacaacaacaacaacb=c with [3] ba=aacb:

aacaacaacaacaac b ba

Critical pair: aacaacaacaacaacaacb=ca.

Reduce LHS:

[4]aac(aacaacaacaacaacb)
⇒ aacc

Defines rule #1.

Referenced by [7], [10].

[7] aacaacbcc=bca

Overlap of [3] ba=aacb with [6] aacc=ca:

b a aacc

Critical pair: bca=aacbacc.

Reduce RHS:

[3]aac(ba)cc
⇒ aacaacbcc

Flip LHS and RHS.

Referenced by [8], [9].

[8] aacaacaacbca=ccc

Overlap of [4] aacaacaacaacaacb=c with [7] aacaacbcc=bca:

aacaacaac aacaacb aacaacbcc

Critical pair: aacaacaacbca=ccc.

Referenced by [9].

[9] aacbca=cccacaacaacaacaacb

Overlap of [8] aacaacaacbca=ccc with [4] aacaacaacaacaacb=c:

aacaacaacbc a aacaacaacaacaacb

Critical pair: aacaacaacbcc=cccacaacaacaacaacb.

Reduce LHS:

[7]aac(aacaacbcc)
⇒ aacbca

Referenced by [10].

[10] bc=caccacccaacaacaacb

Simplify [5] aacaacbcaacaacaacaacb=bc.

Reduce LHS:

[9]aac(aacbca)acaacaacaacb
[6]⇒ (aacc)ccacaacaacaacaacbacaacaacaacb
[3]⇒ caccacaacaacaacaac(ba)caacaacaacb
[4]⇒ caccac(aacaacaacaacaacb)caacaacaacb
⇒ caccacccaacaacaacb

Flip LHS and RHS.

Defines rule #4.