573 inductive cases of $\textit{rdistinct}$. |
573 inductive cases of $\textit{rdistinct}$. |
574 |
574 |
575 \end{proof} |
575 \end{proof} |
576 |
576 |
577 \noindent |
577 \noindent |
578 $\rdistinct{\_}{\_}$ will cancel out all regular expression terms |
578 $\textit{rdistinct}$ will cancel out all regular expression terms |
579 that are in the accumulator, therefore prepending a list $rs_a$ with an arbitrary |
579 that are in the accumulator, therefore prepending a list $rs_a$ with an arbitrary |
580 list $rs$ whose elements are all from the accumulator, and then call $\rdistinct{\_}{\_}$ |
580 list $rs$ whose elements are all from the accumulator, and then call $\textit{rdistinct}$ |
581 on the resulting list, the output will be as if we had called $\rdistinct{\_}{\_}$ |
581 on the resulting list, the output will be as if we had called $\textit{rdistinct}$ |
582 without the prepending of $rs$: |
582 without the prepending of $rs$: |
583 \begin{lemma}\label{rdistinctConcat} |
583 \begin{lemma}\label{rdistinctConcat} |
584 The elements appearing in the accumulator will always be removed. |
584 The elements appearing in the accumulator will always be removed. |
585 More precisely, |
585 More precisely, |
586 \begin{itemize} |
586 \begin{itemize} |
927 |
927 |
928 |
928 |
929 |
929 |
930 |
930 |
931 We are also |
931 We are also |
932 \subsubsection{$\rsimp$ is Idempotent} |
932 \subsection{$\rsimp$ is Idempotent} |
933 The idempotency of $\rsimp$ is very useful in |
933 The idempotency of $\rsimp$ is very useful in |
934 manipulating regular expression terms into desired |
934 manipulating regular expression terms into desired |
935 forms so that key steps allowing further rewriting to closed forms |
935 forms so that key steps allowing further rewriting to closed forms |
936 are possible. |
936 are possible. |
937 \begin{lemma}\label{rsimpIdem} |
937 \begin{lemma}\label{rsimpIdem} |
1040 %Rewriting steps not put in--too long and complicated------------------------------- |
1040 %Rewriting steps not put in--too long and complicated------------------------------- |
1041 \noindent |
1041 \noindent |
1042 We need more equalities like the above to enable a closed form, |
1042 We need more equalities like the above to enable a closed form, |
1043 but to proceed we need to introduce two rewrite relations, |
1043 but to proceed we need to introduce two rewrite relations, |
1044 to make things smoother. |
1044 to make things smoother. |
1045 \subsubsection{The rewrite relation $\hrewrite$ , $\scfrewrites$ , $\frewrite$ and $\grewrite$} |
1045 \subsection{The rewrite relation $\hrewrite$ , $\scfrewrites$ , $\frewrite$ and $\grewrite$} |
1046 Insired by the success we had in the correctness proof |
1046 Insired by the success we had in the correctness proof |
1047 in \ref{Bitcoded2}, where we invented |
1047 in \ref{Bitcoded2}, where we invented |
1048 a term rewriting system to capture the similarity between terms, |
1048 a term rewriting system to capture the similarity between terms, |
1049 we follow suit here defining simplification |
1049 we follow suit here defining simplification |
1050 steps as rewriting steps. This allows capturing |
1050 steps as rewriting steps. This allows capturing |