equal
deleted
inserted
replaced
819 quotient type. The purpose of cleaning is to bring the theorem derived in the |
819 quotient type. The purpose of cleaning is to bring the theorem derived in the |
820 first two phases into the form the user has specified. Abstractly, our |
820 first two phases into the form the user has specified. Abstractly, our |
821 package establishes the following three proof steps: |
821 package establishes the following three proof steps: |
822 |
822 |
823 \begin{center} |
823 \begin{center} |
824 \begin{tabular}{r@ {\hspace{4mm}}l} |
824 \begin{tabular}{l@ {\hspace{4mm}}l} |
825 1.) & @{text "raw_thm \<longrightarrow> reg_thm"}\\ |
825 1.) Regularisation & @{text "raw_thm \<longrightarrow> reg_thm"}\\ |
826 2.) & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\ |
826 2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\ |
827 3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\ |
827 3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\ |
828 \end{tabular} |
828 \end{tabular} |
829 \end{center} |
829 \end{center} |
830 |
830 |
831 \noindent |
831 \noindent |
832 which means the raw theorem implies the quotient theorem. |
832 which means the raw theorem implies the quotient theorem. |