Certificate for #8085 ⟨a, b | aaa=1, babb=abb⟩

Back:⟨a, b | aaa=1, babb=abb⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [4].

[2] babb=abb

Axiom: babb=abb.

Defines rule #3.

Referenced by [3], [4].

[3] baabb=aabb

Overlap of [2] babb=abb with [2] babb=abb:

bab b babb

Critical pair: bababb=abbabb.

Reduce LHS:

[2]ba(babb)
⇒ baabb

Reduce RHS:

[2]ab(babb)
[2]⇒ a(babb)
⇒ aabb

Defines rule #4.

Referenced by [4].

[4] bbb=bb

Overlap of [2] babb=abb with [3] baabb=aabb:

bab b baabb

Critical pair: babaabb=abbaabb.

Reduce LHS:

[3]ba(baabb)
[1]⇒ b(aaa)bb
⇒ bbb

Reduce RHS:

[3]ab(baabb)
[3]⇒ a(baabb)
[1]⇒ (aaa)bb
⇒ bb

Defines rule #2.