Certificate for #5120 ⟨a, b | aab=aa, bbab=a⟩

Back:⟨a, b | aab=aa, bbab=a⟩

Completion settings:

[1] aab=aa

Axiom: aab=aa.

Defines rule #1.

Referenced by [4], [5].

[2] bbab=a

Axiom: bbab=a.

Defines rule #3.

Referenced by [3], [6].

[3] bbaa=abab

Overlap of [2] bbab=a with [2] bbab=a:

bba b bbab

Critical pair: bbaa=abab.

Defines rule #2.

Referenced by [4], [5].

[4] ababb=abab

Overlap of [3] bbaa=abab with [1] aab=aa:

bb aa aab

Critical pair: bbaa=ababb.

Reduce LHS:

[3](bbaa)
⇒ abab

Flip LHS and RHS.

Defines rule #5.

Referenced by [6].

[5] ababab=ababa

Overlap of [3] bbaa=abab with [1] aab=aa:

bba a aab

Critical pair: bbaaa=ababab.

Reduce LHS:

[3](bbaa)a
⇒ ababa

Flip LHS and RHS.

Referenced by [6].

[6] ababa=abaa

Overlap of [4] ababb=abab with [2] bbab=a:

aba bb bbab

Critical pair: abaa=ababab.

Reduce RHS:

[5](ababab)
⇒ ababa

Flip LHS and RHS.

Defines rule #4.