Certificate for #14518 ⟨a, b | aaab=b, babba=b⟩

Back:⟨a, b | aaab=b, babba=b⟩

Completion settings:

[1] aaab=b

Axiom: aaab=b.

Defines rule #3.

Referenced by [4].

[2] babba=b

Axiom: babba=b.

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

[3] bbba=babb

Overlap of [2] babba=b with [2] babba=b:

bab ba babba

Critical pair: babb=bbba.

Flip LHS and RHS.

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

[4] bab=bbbb

Overlap of [3] bbba=babb with [1] aaab=b:

bbb a aaab

Critical pair: bbbb=babbaab.

Reduce RHS:

[2](babba)ab
⇒ bab

Flip LHS and RHS.

Referenced by [5], [6].

[5] bbbbbbb=b

Overlap of [2] babba=b with [4] bab=bbbb:

babba bab

Critical pair: bbbbba=b.

Reduce LHS:

[3]bb(bbba)
[3]⇒ (bbba)bb
[4]⇒ (bab)bbb
⇒ bbbbbbb

Defines rule #1.

Referenced by [6].

[6] ba=bbb

Overlap of [5] bbbbbbb=b with [3] bbba=babb:

bbbb bbb bbba

Critical pair: bbbbbabb=ba.

Reduce LHS:

[3]bb(bbba)bb
[3]⇒ (bbba)bbbb
[4]⇒ (bab)bbbbb
[5]⇒ (bbbbbbb)bb
⇒ bbb

Flip LHS and RHS.

Defines rule #2.