Certificate for #20318 ⟨a, b | aba=b, bbbb=bab⟩

Back:⟨a, b | aba=b, bbbb=bab⟩

Completion settings:

[1] aba=b

Axiom: aba=b.

Defines rule #1.

Referenced by [3], [5], [6].

[2] bbbb=bab

Axiom: bbbb=bab.

Referenced by [4], [5], [7].

[3] bba=abb

Overlap of [1] aba=b with [1] aba=b:

ab a aba

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] babb=abbb

Overlap of [2] bbbb=bab with [2] bbbb=bab:

b bbb bbbb

Critical pair: bbab=babb.

Reduce LHS:

[3](bba)b
⇒ abbb

Flip LHS and RHS.

Referenced by [5].

[5] bab=abb

Overlap of [4] babb=abbb with [3] bba=abb:

bab b bba

Critical pair: bababb=abbbba.

Reduce LHS:

[1]b(aba)bb
[2]⇒ (bbbb)
⇒ bab

Reduce RHS:

[2]a(bbbb)a
[1]⇒ (aba)ba
[3]⇒ (bba)
⇒ abb

Defines rule #2.

Referenced by [6], [7].

[6] aabb=bb

Overlap of [1] aba=b with [5] bab=abb:

a ba bab

Critical pair: aabb=bb.

Defines rule #4.

[7] bbbb=abb

Simplify [2] bbbb=bab.

Reduce RHS:

[5](bab)
⇒ abb

Defines rule #5.