6 

     7 notation (latex output)

     8   fun_rel ("_ ===> _" [51, 51] 50)

     9 

    67 text {* TBD *}

    68 

    69 text {* Why providing a statement to prove is necessary is some cases *}

    70 

    71 subsection {* Regularization *}

    72 

    73 text {*

    74 Transformation of the theorem statement:

    75 \begin{itemize}

    76 \item Quantifiers and abstractions involving raw types replaced by bounded ones.

    77 \item Equalities involving raw types replaced by bounded ones.

    78 \end{itemize}

    79 

    80 The procedure.

    81 

    82 Example of non-regularizable theorem ($0 = 1$).

    83 

    84 New regularization lemmas:

    85 \begin{lemma}

    86 If @{term R2} is an equivalence relation, then:

    87 \begin{eqnarray}

    88 @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\

    89 @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}

    90 \end{eqnarray}

    91 \end{lemma}

    92 

    93 *}

    94 

    95 subsection {* Injection *}

    96 

    97 subsection {* Cleaning *}

    98 

    99 text {* Preservation of quantifiers, abstractions, relations, quotient-constants

   100   (definitions) and user given constant preservation lemmas *}

   101 

   102 section {* Examples *}

   103