Certificate for #16012 ⟨a, b | aaa=ab, abbb=bb⟩

Back:⟨a, b | aaa=ab, abbb=bb⟩

Completion settings:

[1] ab=aaa

Axiom: aaa=ab.

Flip LHS and RHS.

Defines rule #3.

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

[2] bb=aaaaaaa

Axiom: abbb=bb.

Reduce LHS:

[1](ab)bb
[1]⇒ aa(ab)b
[1]⇒ aaaa(ab)
⇒ aaaaaaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[3] aaaaaaaa=aaaaa

Overlap of [1] ab=aaa with [2] bb=aaaaaaa:

a b bb

Critical pair: aaaaaaaa=aaab.

Reduce RHS:

[1]aa(ab)
⇒ aaaaa

Defines rule #1.

Referenced by [4], [5].

[4] baaaaaaa=aaaaaa

Overlap of [2] bb=aaaaaaa with [2] bb=aaaaaaa:

b b bb

Critical pair: baaaaaaa=aaaaaaab.

Reduce RHS:

[1]aaaaaa(ab)
[3]⇒ (aaaaaaaa)a
⇒ aaaaaa

Referenced by [5].

[5] baaaaa=aaaaaaa

Overlap of [4] baaaaaaa=aaaaaa with [3] aaaaaaaa=aaaaa:

b aaaaaaa aaaaaaaa

Critical pair: baaaaa=aaaaaaa.

Defines rule #2.