Certificate for #12959 ⟨a, b | aba=aab, bbab=b

Completion settings:

[1] aab=aba

Axiom: aba=aab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] bbab=b

Axiom: bbab=b.

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

[3] ababab=aba

Overlap of [1] aab=aba with [2] bbab=b:

aa b bbab

Critical pair: aab=ababab.

Reduce LHS:

[1](aab)
aba

Flip LHS and RHS.

Referenced by [4].

[4] babab=ba

Overlap of [2] bbab=b with [3] ababab=aba:

bb ab ababab

Critical pair: bbaba=babab.

Reduce LHS:

[2](bbab)a
ba

Flip LHS and RHS.

Referenced by [5].

[5] bab=bba

Overlap of [2] bbab=b with [4] babab=ba:

b bab babab

Critical pair: bba=bab.

Flip LHS and RHS.

Defines rule #1.

Referenced by [6].

[6] bbba=b

Overlap of [2] bbab=b with [5] bab=bba:

b bab bab

Critical pair: bbba=b.

Defines rule #3.