Certificate for #19053 ⟨a, b | aab=b, babbba=b⟩

Back:⟨a, b | aab=b, babbba=b⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3].

[2] babbba=b

Axiom: babbba=b.

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

[3] babbbb=bab

Overlap of [2] babbba=b with [1] aab=b:

babbb a aab

Critical pair: babbbb=bab.

Referenced by [5].

[4] bbbba=babbb

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

babb ba babbba

Critical pair: babbb=bbbba.

Flip LHS and RHS.

Referenced by [5], [6].

[5] bbbb=b

Overlap of [4] bbbba=babbb with [2] babbba=b:

bbb ba babbba

Critical pair: bbbb=babbbbbba.

Reduce RHS:

[3](babbbb)bba
[2]⇒ (babbba)
⇒ b

Defines rule #3.

Referenced by [6], [7].

[6] babbb=ba

Overlap of [4] bbbba=babbb with [5] bbbb=b:

bbbba bbbb

Critical pair: ba=babbb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

[7] baa=b

Overlap of [5] bbbb=b with [2] babbba=b:

bbb b babbba

Critical pair: bbbb=babbba.

Reduce LHS:

[5](bbbb)
⇒ b

Reduce RHS:

[6](babbb)a
⇒ baa

Flip LHS and RHS.

Defines rule #2.