255   \end{tabular}

   255   \end{tabular}

   256   \end{center}

   256   \end{center}

   257 

   257 

   258   \noindent

   258   \noindent

   259   The first two clauses replace the head of the right-list

   259   The first two clauses replace the head of the right-list

   261   these clauses make sense in case where @{text r} is the empty

   261   these clauses make sense in case where @{text r} is the empty

   262   list, one has to know that the tail function, @{term tl}, is defined

   262   list, one has to know that the tail function, @{term tl}, is defined

   263   such that @{term "tl [] == []"} holds. The third clause 

   263   such that @{term "tl [] == []"} holds. The third clause 

   264   implements the move of the read-write unit to the left: we need

   264   implements the move of the read-write unit to the left: we need

   265   to test if the left-list is empty; if yes, then we just add a 

   265   to test if the left-list is empty; if yes, then we just add a