Certificate for #5300 ⟨a, b | aaa=aa, aba=bb⟩

Back:⟨a, b | aaa=aa, aba=bb⟩

Completion settings:

[1] aaa=aa

Axiom: aaa=aa.

Defines rule #1.

[2] bb=aba

Axiom: aba=bb.

Flip LHS and RHS.

Defines rule #2.

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

[3] abab=baba

Overlap of [2] bb=aba with [2] bb=aba:

b b bb

Critical pair: baba=abab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] babaab=aabaaba

Overlap of [3] abab=baba with [3] abab=baba:

ab ab abab

Critical pair: abbaba=babaab.

Reduce LHS:

[2]a(bb)aba
⇒ aabaaba

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] abaabaab=baabaaba

Overlap of [2] bb=aba with [4] babaab=aabaaba:

b b babaab

Critical pair: baabaaba=abaabaab.

Flip LHS and RHS.

Defines rule #5.