Certificate for #5219 ⟨a, b | aabbaab=bbaa⟩

Back:⟨a, b | aabbaab=bbaa⟩

Completion settings:

[1] aabbaab=bbaa

Axiom: aabbaab=bbaa.

Referenced by [3].

[2] bbaa=c

Axiom: bbaa=c.

Defines rule #5.

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

[3] aabbaab=c

Simplify [1] aabbaab=bbaa.

Reduce RHS:

[2](bbaa)
⇒ c

Referenced by [4].

[4] aacb=c

Overlap of [3] aabbaab=c with [2] bbaa=c:

aa bbaab bbaa

Critical pair: aacb=c.

Defines rule #3.

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

[5] bbc=ccb

Overlap of [2] bbaa=c with [4] aacb=c:

bb aa aacb

Critical pair: bbc=ccb.

Defines rule #1.

[6] bbac=cacb

Overlap of [2] bbaa=c with [4] aacb=c:

bba a aacb

Critical pair: bbac=cacb.

Defines rule #4.

[7] aacc=cbaa

Overlap of [4] aacb=c with [2] bbaa=c:

aac b bbaa

Critical pair: aacc=cbaa.

Defines rule #2.