Certificate for #12319 ⟨a, b | aaab=bb, bbaa=b⟩

Back:⟨a, b | aaab=bb, bbaa=b⟩

Completion settings:

[1] aaab=bb

Axiom: aaab=bb.

Defines rule #4.

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

[2] bbaa=b

Axiom: bbaa=b.

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

[3] bab=bbbb

Overlap of [2] bbaa=b with [1] aaab=bb:

bb aa aaab

Critical pair: bbbb=bab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] baab=bbbbbb

Overlap of [2] bbaa=b with [1] aaab=bb:

bba a aaab

Critical pair: bbabb=baab.

Reduce LHS:

[3]b(bab)b
⇒ bbbbbb

Flip LHS and RHS.

Referenced by [5], [6].

[5] bbbbbbb=bb

Overlap of [1] aaab=bb with [4] baab=bbbbbb:

aaa b baab

Critical pair: aaabbbbbb=bbaab.

Reduce LHS:

[1](aaab)bbbbb
⇒ bbbbbbb

Reduce RHS:

[2](bbaa)b
⇒ bb

Referenced by [6].

[6] bbbbbb=b

Overlap of [4] baab=bbbbbb with [2] bbaa=b:

baa b bbaa

Critical pair: baab=bbbbbbbaa.

Reduce LHS:

[4](baab)
⇒ bbbbbb

Reduce RHS:

[5](bbbbbbb)aa
[2]⇒ (bbaa)
⇒ b

Defines rule #1.

Referenced by [7].

[7] baa=bbbbb

Overlap of [6] bbbbbb=b with [2] bbaa=b:

bbbb bb bbaa

Critical pair: bbbbb=baa.

Flip LHS and RHS.

Defines rule #3.