Certificate for #2064 ⟨a, b | aab=b, abba=a⟩

Back:⟨a, b | aab=b, abba=a⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

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

[2] abba=a

Axiom: abba=a.

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

[3] aa=bba

Overlap of [1] aab=b with [2] abba=a:

a ab abba

Critical pair: aa=bba.

Defines rule #4.

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

[4] bbab=abbb

Overlap of [2] abba=a with [1] aab=b:

abb a aab

Critical pair: abbb=aab.

Reduce RHS:

[3](aa)b
⇒ bbab

Flip LHS and RHS.

Referenced by [5].

[5] abbb=b

Overlap of [1] aab=b with [3] aa=bba:

aab aa

Critical pair: bbab=b.

Reduce LHS:

[4](bbab)
⇒ abbb

Referenced by [7], [8].

[6] bbbba=a

Overlap of [3] aa=bba with [3] aa=bba:

a a aa

Critical pair: abba=bbaa.

Reduce LHS:

[2](abba)
⇒ a

Reduce RHS:

[3]bb(aa)
⇒ bbbba

Flip LHS and RHS.

Defines rule #3.

[7] ab=bbb

Overlap of [1] aab=b with [5] abbb=b:

a ab abbb

Critical pair: ab=bbb.

Defines rule #2.

Referenced by [8].

[8] bbbbb=b

Overlap of [5] abbb=b with [7] ab=bbb:

abbb ab

Critical pair: bbbbb=b.

Defines rule #1.