Certificate for #15897 ⟨a, b | aba=ab, bbbaa=a⟩

Back:⟨a, b | aba=ab, bbbaa=a⟩

Completion settings:

[1] aba=ab

Axiom: aba=ab.

Defines rule #2.

Referenced by [3], [4].

[2] bbbaa=a

Axiom: bbbaa=a.

Referenced by [5], [7], [8].

[3] abba=abb

Overlap of [1] aba=ab with [1] aba=ab:

ab a aba

Critical pair: abab=abba.

Reduce LHS:

[1](aba)b
⇒ abb

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] abbba=abbb

Overlap of [1] aba=ab with [3] abba=abb:

ab a abba

Critical pair: ababb=abbba.

Reduce LHS:

[1](aba)bb
⇒ abbb

Flip LHS and RHS.

Referenced by [5], [6].

[5] abbb=aa

Overlap of [4] abbba=abbb with [2] bbbaa=a:

a bbba bbbaa

Critical pair: aa=abbba.

Reduce RHS:

[4](abbba)
⇒ abbb

Flip LHS and RHS.

Referenced by [6], [9].

[6] aaa=aa

Overlap of [4] abbba=abbb with [5] abbb=aa:

abbba abbb

Critical pair: aaa=abbb.

Reduce RHS:

[5](abbb)
⇒ aa

Referenced by [7].

[7] aa=a

Overlap of [2] bbbaa=a with [6] aaa=aa:

bbb aa aaa

Critical pair: bbbaa=aa.

Reduce LHS:

[2](bbbaa)
⇒ a

Flip LHS and RHS.

Defines rule #1.

Referenced by [8], [9].

[8] bbba=a

Overlap of [2] bbbaa=a with [7] aa=a:

bbb aa aa

Critical pair: bbba=a.

Defines rule #5.

[9] abbb=a

Simplify [5] abbb=aa.

Reduce RHS:

[7](aa)
⇒ a

Defines rule #4.