Certificate for #12559 ⟨a, b | abba=aa, baab=b⟩

Back:⟨a, b | abba=aa, baab=b⟩

Completion settings:

[1] abba=aa

Axiom: abba=aa.

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

[2] baab=b

Axiom: baab=b.

Defines rule #5.

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

[3] abb=aaab

Overlap of [1] abba=aa with [2] baab=b:

ab ba baab

Critical pair: abb=aaab.

Defines rule #7.

Referenced by [6], [7].

[4] bba=baaa

Overlap of [2] baab=b with [1] abba=aa:

ba ab abba

Critical pair: baaa=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [7], [10].

[5] baaaab=bb

Overlap of [4] bba=baaa with [2] baab=b:

b ba baab

Critical pair: bb=baaaab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [10].

[6] aaaba=aa

Overlap of [1] abba=aa with [3] abb=aaab:

abba abb

Critical pair: aaaba=aa.

Referenced by [7], [8].

[7] abaaa=aa

Overlap of [3] abb=aaab with [4] bba=baaa:

a bb bba

Critical pair: abaaa=aaaba.

Reduce RHS:

[6](aaaba)
⇒ aa

Defines rule #1.

Referenced by [8].

[8] aaba=abaa

Overlap of [7] abaaa=aa with [6] aaaba=aa:

ab aaa aaaba

Critical pair: abaa=aaba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[9] babaa=ba

Overlap of [2] baab=b with [8] aaba=abaa:

b aab aaba

Critical pair: babaa=ba.

Defines rule #4.

[10] bbb=baaaaaab

Overlap of [4] bba=baaa with [5] baaaab=bb:

b ba baaaab

Critical pair: bbb=baaaaaab.

Defines rule #8.