Certificate for #25237 ⟨a, b | aa=a, babab=abb⟩

Back:⟨a, b | aa=a, babab=abb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] babab=abb

Axiom: babab=abb.

Defines rule #4.

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

[3] abbab=babb

Overlap of [2] babab=abb with [2] babab=abb:

ba bab babab

Critical pair: baabb=abbab.

Reduce LHS:

[1]b(aa)bb
⇒ babb

Flip LHS and RHS.

Defines rule #5.

Referenced by [4], [5].

[4] ababb=babb

Overlap of [1] aa=a with [3] abbab=babb:

a a abbab

Critical pair: ababb=abbab.

Reduce RHS:

[3](abbab)
⇒ babb

Defines rule #6.

Referenced by [5], [6].

[5] bbabb=babb

Overlap of [3] abbab=babb with [2] babab=abb:

ab bab babab

Critical pair: ababb=babbab.

Reduce LHS:

[4](ababb)
⇒ babb

Reduce RHS:

[3]b(abbab)
⇒ bbabb

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] abbb=babb

Overlap of [2] babab=abb with [4] ababb=babb:

b abab ababb

Critical pair: bbabb=abbb.

Reduce LHS:

[5](bbabb)
⇒ babb

Flip LHS and RHS.

Defines rule #2.