Certificate for #5358 ⟨a, b | abababa=aabb⟩

Back:⟨a, b | abababa=aabb⟩

Completion settings:

[1] abababa=aabb

Axiom: abababa=aabb.

Referenced by [3].

[2] aabb=c

Axiom: aabb=c.

Defines rule #2.

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

[3] abababa=c

Simplify [1] abababa=aabb.

Reduce RHS:

[2](aabb)
⇒ c

Defines rule #7.

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

[4] abc=cba

Overlap of [3] abababa=c with [3] abababa=c:

ab ababa abababa

Critical pair: abc=cba.

Defines rule #1.

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

[5] cbababa=cabb

Overlap of [3] abababa=c with [2] aabb=c:

ababab a aabb

Critical pair: abababc=cabb.

Reduce LHS:

[4]abab(abc)
[4]⇒ ab(abc)ba
[4]⇒ (abc)baba
⇒ cbababa

Defines rule #5.

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

[6] cabbba=cbc

Overlap of [3] abababa=c with [4] abc=cba:

ababab a abc

Critical pair: abababcba=cbc.

Reduce LHS:

[4]abab(abc)ba
[4]⇒ ab(abc)baba
[4]⇒ (abc)bababa
[5]⇒ (cbababa)ba
⇒ cabbba

Defines rule #4.

Referenced by [7].

[7] cabbbc=cbcabb

Overlap of [6] cabbba=cbc with [3] abababa=c:

cabbb a abababa

Critical pair: cabbbc=cbcbababa.

Reduce RHS:

[5]cb(cbababa)
⇒ cbcabb

Defines rule #3.

[8] cabbabb=cbcbaba

Overlap of [5] cbababa=cabb with [2] aabb=c:

cbabab a aabb

Critical pair: cbababc=cabbabb.

Reduce LHS:

[4]cbab(abc)
[4]⇒ cb(abc)ba
⇒ cbcbaba

Flip LHS and RHS.

Defines rule #6.