equal
deleted
inserted
replaced
902 \section{Specifications of Certain Functions to be Used} |
902 \section{Specifications of Certain Functions to be Used} |
903 Here we give some functions' definitions, |
903 Here we give some functions' definitions, |
904 which we will use later. |
904 which we will use later. |
905 \begin{center} |
905 \begin{center} |
906 \begin{tabular}{ccc} |
906 \begin{tabular}{ccc} |
907 $\retrieve \; \ACHAR \, \textit{bs} \, c \; \Char(c) = \textit{bs} |
907 $\retrieve \; \ACHAR \, \textit{bs} \, c \; \Char(c) = \textit{bs}$ |
908 \end{tabular} |
908 \end{tabular} |
909 \end{center} |
909 \end{center} |
910 |
910 |
911 |
911 |
912 %---------------------------------------------------------------------------------------- |
912 %---------------------------------------------------------------------------------------- |
913 % SECTION correctness proof |
913 % SECTION correctness proof |
914 %---------------------------------------------------------------------------------------- |
914 %---------------------------------------------------------------------------------------- |
915 \section{Correctness of Bit-coded Algorithm (Without Simplification) |
915 \section{Correctness of Bit-coded Algorithm (Without Simplification)} |
916 We now give the proof the correctness of the algorithm with bit-codes. |
916 We now give the proof the correctness of the algorithm with bit-codes. |
917 |
917 |
918 Ausaf and Urban cleverly defined an auxiliary function called $\flex$, |
918 Ausaf and Urban cleverly defined an auxiliary function called $\flex$, |
919 defined as |
919 defined as |
920 \[ |
920 \[ |