Certificate for #15996 ⟨a, b | aaa=ab, aabb=bb⟩

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

Completion settings:

[1] ab=aaa

Axiom: aaa=ab.

Flip LHS and RHS.

Defines rule #3.

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

[2] bb=aaaaaa

Axiom: aabb=bb.

Reduce LHS:

[1]a(ab)b
[1]⇒ aaa(ab)
⇒ aaaaaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [4].

[3] aaaaaaa=aaaaa

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

a b bb

Critical pair: aaaaaaa=aaab.

Reduce RHS:

[1]aa(ab)
⇒ aaaaa

Defines rule #1.

Referenced by [4], [5].

[4] baaaaaa=aaaaaa

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

b b bb

Critical pair: baaaaaa=aaaaaab.

Reduce RHS:

[1]aaaaa(ab)
[3]⇒ (aaaaaaa)a
⇒ aaaaaa

Referenced by [5].

[5] baaaaa=aaaaa

Overlap of [4] baaaaaa=aaaaaa with [3] aaaaaaa=aaaaa:

b aaaaaa aaaaaaa

Critical pair: baaaaa=aaaaaaa.

Reduce RHS:

[3](aaaaaaa)
⇒ aaaaa

Defines rule #2.