Certificate for #12194 ⟨a, b | aaaa=ab, bbbb=a⟩

Back:⟨a, b | aaaa=ab, bbbb=a⟩

Completion settings:

[1] aaaa=ab

Axiom: aaaa=ab.

Referenced by [3].

[2] a=bbbb

Axiom: bbbb=a.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] aaaa=bbbbb

Simplify [1] aaaa=ab.

Reduce RHS:

[2](a)b
⇒ bbbbb

Referenced by [4].

[4] bbbbbbbbbbbbbbbb=bbbbb

Overlap of [3] aaaa=bbbbb with [2] a=bbbb:

aaaa a

Critical pair: bbbbaaa=bbbbb.

Reduce LHS:

[2]bbbb(a)aa
[2]⇒ bbbbbbbb(a)a
[2]⇒ bbbbbbbbbbbb(a)
⇒ bbbbbbbbbbbbbbbb

Defines rule #1.