Certificate for #4982 ⟨a, b | aaaabba=aabb⟩

Back:⟨a, b | aaaabba=aabb⟩

Completion settings:

[1] aaaabba=aabb

Axiom: aaaabba=aabb.

Referenced by [3].

[2] aabb=c

Axiom: aabb=c.

Defines rule #5.

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

[3] aaaabba=c

Simplify [1] aaaabba=aabb.

Reduce RHS:

[2](aabb)
⇒ c

Referenced by [4].

[4] aaca=c

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

aa aabba aabb

Critical pair: aaca=c.

Defines rule #4.

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

[5] aacc=caca

Overlap of [4] aaca=c with [4] aaca=c:

aac a aaca

Critical pair: aacc=caca.

Defines rule #3.

Referenced by [6].

[6] cabb=caca

Overlap of [4] aaca=c with [2] aabb=c:

aac a aabb

Critical pair: aacc=cabb.

Reduce LHS:

[5](aacc)
⇒ caca

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[7] cbb=cca

Overlap of [4] aaca=c with [6] cabb=caca:

aa ca cabb

Critical pair: aacaca=cbb.

Reduce LHS:

[4](aaca)ca
⇒ cca

Flip LHS and RHS.

Defines rule #1.