Certificate for #12179 ⟨a, b | aaaa=ab, abbb=b⟩

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

Completion settings:

[1] ab=aaaa

Axiom: aaaa=ab.

Flip LHS and RHS.

Referenced by [2], [3].

[2] b=aaaaaaaaaa

Axiom: abbb=b.

Reduce LHS:

[1](ab)bb
[1]⇒ aaa(ab)b
[1]⇒ aaaaaa(ab)
⇒ aaaaaaaaaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaaaaaaaaa=aaaa

Overlap of [1] ab=aaaa with [2] b=aaaaaaaaaa:

a b b

Critical pair: aaaaaaaaaaa=aaaa.

Defines rule #1.