Certificate for #15658 ⟨a, b | aab=ab, bbaaa=b⟩

Back:⟨a, b | aab=ab, bbaaa=b⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Defines rule #2.

Referenced by [3], [4].

[2] bbaaa=b

Axiom: bbaaa=b.

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

[3] bbab=bb

Overlap of [2] bbaaa=b with [1] aab=ab:

bba aa aab

Critical pair: bbaab=bb.

Reduce LHS:

[1]bb(aab)
⇒ bbab

Referenced by [5].

[4] bab=bb

Overlap of [2] bbaaa=b with [1] aab=ab:

bbaa a aab

Critical pair: bbaaab=bab.

Reduce LHS:

[2](bbaaa)b
⇒ bb

Flip LHS and RHS.

Referenced by [5], [8].

[5] bbb=bb

Overlap of [4] bab=bb with [4] bab=bb:

ba b bab

Critical pair: babb=bbab.

Reduce LHS:

[4](bab)b
⇒ bbb

Reduce RHS:

[3](bbab)
⇒ bb

Referenced by [6].

[6] bb=b

Overlap of [5] bbb=bb with [2] bbaaa=b:

b bb bbaaa

Critical pair: bb=bbaaa.

Reduce RHS:

[2](bbaaa)
⇒ b

Defines rule #1.

Referenced by [7], [8].

[7] baaa=b

Overlap of [2] bbaaa=b with [6] bb=b:

bbaaa bb

Critical pair: baaa=b.

Defines rule #4.

[8] bab=b

Simplify [4] bab=bb.

Reduce RHS:

[6](bb)
⇒ b

Defines rule #3.