Certificate for #13067 ⟨a, b | baa=abb, aaab=b⟩

Back:⟨a, b | baa=abb, aaab=b⟩

Completion settings:

[1] baa=abb

Axiom: baa=abb.

Defines rule #1.

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

[2] aaab=b

Axiom: aaab=b.

Defines rule #2.

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

[3] abbab=bb

Overlap of [1] baa=abb with [2] aaab=b:

b aa aaab

Critical pair: bb=abbab.

Flip LHS and RHS.

Referenced by [5].

[4] ababbb=bab

Overlap of [1] baa=abb with [2] aaab=b:

ba a aaab

Critical pair: bab=abbaab.

Reduce RHS:

[1]ab(baa)b
⇒ ababbb

Flip LHS and RHS.

Referenced by [6].

[5] bbab=aabb

Overlap of [2] aaab=b with [3] abbab=bb:

aa ab abbab

Critical pair: aabb=bbab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7].

[6] babbb=aabab

Overlap of [2] aaab=b with [4] ababbb=bab:

aa ab ababbb

Critical pair: aabab=babbb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

[7] abbbbbb=aababab

Overlap of [6] babbb=aabab with [5] bbab=aabb:

bab bb bbab

Critical pair: babaabb=aababab.

Reduce LHS:

[1]ba(baa)bb
[1]⇒ (baa)bbbb
⇒ abbbbbb

Referenced by [8].

[8] bbbbbb=ababab

Overlap of [2] aaab=b with [7] abbbbbb=aababab:

aa ab abbbbbb

Critical pair: aaaababab=bbbbbb.

Reduce LHS:

[2]a(aaab)abab
⇒ ababab

Flip LHS and RHS.

Defines rule #5.

Referenced by [9].

[9] bababab=abababb

Overlap of [8] bbbbbb=ababab with [8] bbbbbb=ababab:

b bbbbb bbbbbb

Critical pair: bababab=abababb.

Defines rule #6.