Certificate for #6708 ⟨a, b | aab=b, babb=ba⟩

Back:⟨a, b | aab=b, babb=ba⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

Referenced by [3], [5].

[2] babb=ba

Axiom: babb=ba.

Defines rule #5.

Referenced by [3], [4].

[3] baa=bbb

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

bab b babb

Critical pair: babba=baabb.

Reduce LHS:

[2](babb)a
⇒ baa

Reduce RHS:

[1]b(aab)b
⇒ bbb

Defines rule #1.

Referenced by [4], [5].

[4] bbba=ba

Overlap of [2] babb=ba with [3] baa=bbb:

bab b baa

Critical pair: babbbb=baaa.

Reduce LHS:

[2](babb)bb
[2]⇒ (babb)
⇒ ba

Reduce RHS:

[3](baa)a
⇒ bbba

Flip LHS and RHS.

Defines rule #4.

[5] bbbb=bb

Overlap of [3] baa=bbb with [1] aab=b:

b aa aab

Critical pair: bb=bbbb.

Flip LHS and RHS.

Defines rule #3.