\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|
 Copyright (C) 1994 by Ken Kunen.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Ken Kunen PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS
 IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT
 NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Ken Kunen BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}    \begin{verbatim}; load initial database

; This file was developed by Ken Kunen, kunen@cs.wisc.edu.  It checks
; the fundamental theorem of arithmetic.  Unlike the proof in the book
; A Compuational Logic and in the file basic.events, Kunen's proof does not
; need auxilliary functions, e.g., gcd.  Why should one be interested
; in this matter?

; In full first order logic, one can show that definitions are
; unnecessary, both in the ``use sense'' that they are ``eliminable''
; from theorems in which they occur and in the ``unnecessary'' sense
; that anything that can be proved with a definition (whose statement
; does not involve that definition) can be proved without the
; definition.

; However, NQTHM does not provide the full power of first order logic.
; It remains an open question, can any Nqthm theorem be proved without
; the definition of concepts not used in the theorem?  Kunen did the
; job for prime factorization.  Can someone else do the job for, say,
; Wilson's theorem?

; Foregoing comments by Robert S. Boyer

; file basic4 -- proof of prime-factorization uniqueness
; no definitions needed except those used to state the theorem,
; EXCEPT the identically 0 function kludge used to 
; force the correct induction.
; events in caps were just copied from basic.events
; no attemt to be elegant here, but it works
; time on decstation3100:  [ 22.7 1448.2 29.1 ]



;;;;;;;;;;;  basic defns -- needed to state the uniqueness of prime fact.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{divides}$\;\;$
{\rm{divides}}\,({\it{x\/}}, {\it{y\/}})\index{divides} $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $\simeq {\tt{0}}$)
\end{tabbing}

    \begin{tabbing}{\sc Definition}:\index{prime1} \\  
\=\+{\rm{prime1}}\,({\it{x\/}}, {\it{y\/}})\index{prime1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{y\/}} $=$ {\tt{1}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }($\neg$ {\rm{divides}}\,({\it{y\/}}, {\it{x\/}})\index{divides}) $\wedge$ {\rm{prime1}}\,({\it{x\/}}, {\it{y\/}} $-\;1$)\index{prime1}$\;${\bf  endif}\-\-
\end{tabbing}

    \begin{tabbing}{\sc Definition}:\index{prime} \\  
{\rm{prime}}\,({\it{x\/}})\index{prime} $=$ (({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}}) $\wedge$ {\rm{prime1}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{prime1})
\end{tabbing}


    \begin{tabbing}{\sc Definition}:\index{delete} \\  
\=\+{\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{car}}\,({\it{y\/}})$\;\;${\bf then }{\rm{cdr}}\,({\it{y\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{y\/}}), {\rm{delete}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{delete})$\;${\bf  endif}\- \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}


    \begin{tabbing}{\sc Definition}:\index{perm} \\  
\=\+{\rm{perm}}\,({\it{a\/}}, {\it{b\/}})\index{perm} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{b\/}} $\simeq\;${{\bf{nil}}}${}$ \\ 
{\bf elseif }{\rm{car}}\,({\it{a\/}}) $\in$ {\it{b\/}}$\;\;${\bf then }{\rm{perm}}\,({\rm{cdr}}\,({\it{a\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{a\/}}), {\it{b\/}})\index{delete})\index{perm} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

    \begin{tabbing}{\sc Definition}:\index{prime-list} \\  
\=\+{\rm{prime-list}}\,({\it{l\/}})\index{prime-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{prime}}\,({\rm{car}}\,({\it{l\/}}))\index{prime} $\wedge$ {\rm{prime-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{prime-list}$\;${\bf  endif}\-\-
\end{tabbing}

    \begin{tabbing}{\sc Definition}:\index{times-list} \\  
\=\+{\rm{times-list}}\,({\it{l\/}})\index{times-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{car}}\,({\it{l\/}}) $*$ {\rm{times-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{times-list}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; end defns
; THE GOAL
;    (PROVE-LEMMA PRIME-FACTORIZATION-UNIQUENESS NIL
;                (IMPLIES (AND (PRIME-LIST L1)
;                              (PRIME-LIST L2)
;                              (EQUAL (TIMES-LIST L1)
;                                     (TIMES-LIST L2)))
;                         (PERM L1 L2)))
; 


;;;;;;;;;;;;;;;;;;;;;;;;;
;;;   Basic facts about +, *, -
;;;;;;;;;;;;;;;;;;;;;;;;


    \end{verbatim}\begin{tabbing}{\sc Theorem}:  plus-right-id2 \\ \index{plus-right-id2}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $+$ {\it{y\/}}) $=$ {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
\=\+({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }$1\;+$ ({\it{x\/}} $+$ {\it{y\/}}) \\ 
{\bf else }$1\;+$ {\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  commutativity2-of-plus \\ \index{commutativity2-of-plus}
({\it{x\/}} $+$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $+$ ({\it{x\/}} $+$ {\it{z\/}}))
\end{tabbing} 
    \begin{tabbing}{\sc Theorem}:  commutativity-of-plus \\ \index{commutativity-of-plus}
({\it{x\/}} $+$ {\it{y\/}}) $=$ ({\it{y\/}} $+$ {\it{x\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  associativity-of-plus \\ \index{associativity-of-plus}
(({\it{x\/}} $+$ {\it{y\/}}) $+$ {\it{z\/}}) $=$ ({\it{x\/}} $+$ ({\it{y\/}} $+$ {\it{z\/}}))
\end{tabbing} 
    \begin{tabbing}{\sc Theorem}:  plus-equal-0 \\ \index{plus-equal-0}
(({\it{a\/}} $+$ {\it{b\/}}) $=$ {\tt{0}}) $=$ (({\it{a\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\simeq {\tt{0}}$))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-x-x \\ \index{difference-x-x}
({\it{x\/}} $-$ {\it{x\/}}) $=$ {\tt{0}}
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-plus \\ \index{difference-plus}
((({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})) $\wedge$ ((({\it{y\/}} $+$ {\it{x\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  plus-cancellation \\ \index{plus-cancellation}
(({\it{a\/}} $+$ {\it{b\/}}) $=$ ({\it{a\/}} $+$ {\it{c\/}})) $=$ ({\rm{fix}}\,({\it{b\/}}) $=$ {\rm{fix}}\,({\it{c\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-0 \\ \index{difference-0}
({\it{y\/}} $\not<$ {\it{x\/}}) $\rightarrow$ (({\it{x\/}} $-$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  equal-difference-0 \\ \index{equal-difference-0}
({\tt{0}} $=$ ({\it{x\/}} $-$ {\it{y\/}})) $=$ ({\it{y\/}} $\not<$ {\it{x\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-cancellation-0 \\ \index{difference-cancellation-0}
({\it{x\/}} $=$ ({\it{x\/}} $-$ {\it{y\/}})) $=$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$)))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-cancellation-1 \\ \index{difference-cancellation-1}
\=\+(({\it{x\/}} $-$ {\it{y\/}}) $=$ ({\it{z\/}} $-$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{y\/}} $\not<$ {\it{z\/}} \\ 
{\bf elseif }{\it{z\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{y\/}} $\not<$ {\it{x\/}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}}) $=$ {\rm{fix}}\,({\it{z\/}})$\;${\bf  endif}\-\-
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  times-zero2 \\ \index{times-zero2}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  distributivity-of-times-over-plus \\ \index{distributivity-of-times-over-pl!us}
({\it{x\/}} $*$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ (({\it{x\/}} $*$ {\it{y\/}}) $+$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  times-add1 \\ \index{times-add1}
\=\+({\it{x\/}} $*$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{x\/}} $+$ ({\it{x\/}} $*$ {\it{y\/}}) \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  commutativity-of-times \\ \index{commutativity-of-times}
({\it{x\/}} $*$ {\it{y\/}}) $=$ ({\it{y\/}} $*$ {\it{x\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  commutativity2-of-times \\ \index{commutativity2-of-times}
({\it{x\/}} $*$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ ({\it{y\/}} $*$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  associativity-of-times \\ \index{associativity-of-times}
(({\it{x\/}} $*$ {\it{y\/}}) $*$ {\it{z\/}}) $=$ ({\it{x\/}} $*$ ({\it{y\/}} $*$ {\it{z\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  equal-times-0 \\ \index{equal-times-0}
(({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}}) $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$))
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  equal-lessp \\ \index{equal-lessp}
\=\+(({\it{x\/}} $<$ {\it{y\/}}) $=$ {\it{z\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\bf{t}} $=$ {\it{z\/}} \\ 
{\bf else }{\bf{f}} $=$ {\it{z\/}}$\;${\bf  endif}\-\-
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-elim \\ \index{difference-elim}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\not<$ {\it{x\/}})) $\rightarrow$ (({\it{x\/}} $+$ ({\it{y\/}} $-$ {\it{x\/}})) $=$ {\it{y\/}})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  lessp-times-1 \\ \index{lessp-times-1}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{i\/}} $*$ {\it{j\/}}) $\not<$ {\it{j\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  lessp-times-2 \\ \index{lessp-times-2}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{j\/}} $*$ {\it{i\/}}) $\not<$ {\it{j\/}})
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  difference-plus1 \\ \index{difference-plus1}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-plus2 \\ \index{difference-plus2}
(({\it{y\/}} $+$ {\it{x\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  difference-plus-cancelation \\ \index{difference-plus-cancelation}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  times-difference \\ \index{times-difference}
({\it{x\/}} $*$ ({\it{c\/}} $-$ {\it{w\/}})) $=$ (({\it{c\/}} $*$ {\it{x\/}}) $-$ ({\it{w\/}} $*$ {\it{x\/}}))
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  difference-plus3 \\ \index{difference-plus3}
(({\it{b\/}} $+$ ({\it{a\/}} $+$ {\it{c\/}})) $-$ {\it{a\/}}) $=$ ({\it{b\/}} $+$ {\it{c\/}})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  difference-add1-cancellation \\ \index{difference-add1-cancellation}
(($1\;+$ ({\it{y\/}} $+$ {\it{z\/}})) $-$ {\it{z\/}}) $=$ ($1\;+$ {\it{y\/}})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  lessp-plus-cancelation \\ \index{lessp-plus-cancelation}
(({\it{x\/}} $+$ {\it{y\/}}) $<$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $<$ {\it{z\/}})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  lessp-times-cancellation \\ \index{lessp-times-cancellation}
(({\it{x\/}} $*$ {\it{z\/}}) $<$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  lessp-plus-cancellation3 \\ \index{lessp-plus-cancellation3}
({\it{y\/}} $<$ ({\it{x\/}} $+$ {\it{y\/}})) $=$ ({\it{x\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  times-id-iff-1 \\ \index{times-id-iff-1}
({\it{z\/}} $=$ ({\it{w\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{z\/}} $=$ {\tt{0}}) $\vee$ ({\it{w\/}} $=$ {\tt{1}})))
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  times-identity1 \\ \index{times-identity1}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{y\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}})) $\rightarrow$ ({\it{x\/}} $\not=$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  times-identity \\ \index{times-identity}
({\it{x\/}} $=$ ({\it{x\/}} $*$ {\it{y\/}})) $=$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})))
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  times-equal-1 \\ \index{times-equal-1}
\=\+(({\it{a\/}} $*$ {\it{b\/}}) $=$ {\tt{1}}) \\ 
$=$$\;\;\;\;$(\=\+({\it{a\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} $-\;1$) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{b\/}} $-\;1$) $=$ {\tt{0}}))\-\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  List facts -- pure lists only
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

    \end{verbatim}\begin{tabbing}{\sc Theorem}:  delete-non-member \\ \index{delete-non-member}
({\it{x\/}} $\not\in$ {\it{y\/}}) $\rightarrow$ ({\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete} $=$ {\it{y\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  member-delete \\ \index{member-delete}
({\it{x\/}} $\in$ {\rm{delete}}\,({\it{u\/}}, {\it{v\/}})\index{delete}) $\rightarrow$ ({\it{x\/}} $\in$ {\it{v\/}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  commutativity-of-delete \\ \index{commutativity-of-delete}
{\rm{delete}}\,({\it{x\/}}, {\rm{delete}}\,({\it{y\/}}, {\it{z\/}})\index{delete})\index{delete} $=$ {\rm{delete}}\,({\it{y\/}}, {\rm{delete}}\,({\it{x\/}}, {\it{z\/}})\index{delete})\index{delete}
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  lessp-count-delete \\ \index{lessp-count-delete}
({\it{n\/}} $\in$ {\it{l\/}}) $\rightarrow$ ({\rm{count}}\,({\rm{delete}}\,({\it{n\/}}, {\it{l\/}})\index{delete}) $<$ {\rm{count}}\,({\it{l\/}}))
\end{tabbing}

\begin{verbatim};;; ok to here -- save as basic4a


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;  Quotients, Remainders, Divisibility
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;   !!!!!!!  this one is really important
    \end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-quotient \\ \index{remainder-quotient}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $+$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}



    \begin{tabbing}{\sc Theorem}:  remainder-wrt-1 \\ \index{remainder-wrt-1}
({\it{y\/}} ${}${\bf{mod}}${}$ {\tt{1}}) $=$ {\tt{0}}
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  remainder-wrt-12 \\ \index{remainder-wrt-12}
({\it{x\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  lessp-remainder2 \\ \index{lessp-remainder2}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{y\/}}) $=$ ({\it{y\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  remainder-x-x \\ \index{remainder-x-x}
({\it{x\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  remainder-quotient-elim \\ \index{remainder-quotient-elim}
(({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $+$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))) $=$ {\it{x\/}})
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  lessp-quotient1 \\ \index{lessp-quotient1}
(({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{i\/}}) $=$ (({\it{i\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{j\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{j\/}} $\not=$ {\tt{1}})))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  lessp-remainder1 \\ \index{lessp-remainder1}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{x\/}}) $=$ (({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not<$ {\it{y\/}}))
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  divides-times \\ \index{divides-times}
(({\it{x\/}} $*$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  remainder-add1 \\ \index{remainder-add1}
(({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}})) $\rightarrow$ ((($1\;+$ ({\it{x\/}} $*$ {\it{y\/}})) ${}${\bf{mod}}${}$ {\it{y\/}}) $\not=$ {\tt{0}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  divides-plus-rewrite1 \\ \index{divides-plus-rewrite1}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  divides-plus-rewrite2 \\ \index{divides-plus-rewrite2}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $\not=$ {\tt{0}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $\not=$ {\tt{0}})
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  divides-plus-rewrite \\ \index{divides-plus-rewrite}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ (((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}))
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  divides-plus-rewrite-commuted \\ \index{divides-plus-rewrite-commuted}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ (((({\it{y\/}} $+$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}))
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  euclid \\ \index{euclid}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{y\/}} $-$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-)\-\-
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  remainder-0-crock \\ \index{remainder-0-crock}
({\tt{0}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}}
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  quotient-times1 \\ \index{quotient-times1}
\=\+(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}}) $\wedge$ {\rm{divides}}\,({\it{x\/}}, {\it{y\/}})\index{divides}) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $*$ ({\it{y\/}} $\div$ {\it{x\/}})) $=$ {\it{y\/}})\-
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  quotient-lessp \\ \index{quotient-lessp}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})) $\rightarrow$ (({\it{y\/}} $\div$ {\it{x\/}}) $\not=$ {\tt{0}})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  divides-times1 \\ \index{divides-times1}
({\it{a\/}} $=$ ({\it{z\/}} $*$ {\it{y\/}})) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  quotient-divides \\ \index{quotient-divides}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{x\/}} $*$ ({\it{y\/}} $\div$ {\it{x\/}})) $\not=$ {\it{y\/}})) $\rightarrow$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $\not=$ {\tt{0}})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  quotient-times \\ \index{quotient-times}
\=\+(({\it{y\/}} $*$ {\it{x\/}}) $\div$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
    \begin{tabbing}{\sc Theorem}:  distributivity-of-divides \\ \index{distributivity-of-divides}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ {\rm{divides}}\,({\it{a\/}}, {\it{w\/}})\index{divides}) $\rightarrow$ (({\it{c\/}} $*$ ({\it{w\/}} $\div$ {\it{a\/}})) $=$ (({\it{c\/}} $*$ {\it{w\/}}) $\div$ {\it{a\/}}))
\end{tabbing}




\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Times-list and Prime-list facts -- only stuff that
;;;  doesn't depend on meaning of "prime"
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

    \end{verbatim}\begin{tabbing}{\sc Theorem}:  times-list-append \\ \index{times-list-append}
{\rm{times-list}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{times-list} $=$ ({\rm{times-list}}\,({\it{x\/}})\index{times-list} $*$ {\rm{times-list}}\,({\it{y\/}})\index{times-list})
\end{tabbing}

    \begin{tabbing}{\sc Theorem}:  prime-list-append \\ \index{prime-list-append}
{\rm{prime-list}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{prime-list} $=$ ({\rm{prime-list}}\,({\it{x\/}})\index{prime-list} $\wedge$ {\rm{prime-list}}\,({\it{y\/}})\index{prime-list})
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  prime-list-delete \\ \index{prime-list-delete}
{\rm{prime-list}}\,({\it{l2\/}})\index{prime-list} $\rightarrow$ {\rm{prime-list}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l2\/}})\index{delete})\index{prime-list}
\end{tabbing}

\begin{verbatim};  ok to here -- save as "basic4b"


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Primes and their properties
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; as far as possible, try to express theorems in terms of 
; divisibility, rather than remainder=0 -- then, in later lemmas,
; we don't have to expand DIVIDES
; ????????? actually, that's not so clear -- divides is still
; expanded, even when it's disabled

\end{verbatim}\begin{tabbing}{\sc Theorem}:  primes-are-big \\ \index{primes-are-big}
{\rm{prime}}\,({\it{p\/}})\index{prime} $\rightarrow$ (({\tt{1}} $<$ {\it{p\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  little-step-aux1 \\ \index{little-step-aux1}
({\rm{prime1}}\,({\it{p\/}}, {\it{z\/}})\index{prime1} $\wedge$ ({\tt{1}} $<$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $\leq$ {\it{z\/}})) $\rightarrow$ ($\neg$ {\rm{divides}}\,({\it{y\/}}, {\it{p\/}})\index{divides})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  little-step-aux2 \\ \index{little-step-aux2}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\tt{1}} $<$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $<$ {\it{p\/}})) $\rightarrow$ ($\neg$ {\rm{divides}}\,({\it{y\/}}, {\it{p\/}})\index{divides})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  little-step-aux3 \\ \index{little-step-aux3}
(({\tt{1}} $<$ {\it{p\/}}) $\wedge$ ({\tt{1}} $<$ {\it{y\/}}) $\wedge$ {\rm{divides}}\,({\it{y\/}}, {\it{p\/}})\index{divides}) $\rightarrow$ ({\it{y\/}} $\leq$ {\it{p\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  little-step \\ \index{little-step}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\tt{1}} $<$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $\not=$ {\it{p\/}})) $\rightarrow$ ($\neg$ {\rm{divides}}\,({\it{y\/}}, {\it{p\/}})\index{divides})
\end{tabbing}
                        

\begin{tabbing}{\sc Theorem}:  exact-remainder-quotient \\ \index{exact-remainder-quotient}
(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{x\/}})\index{divides}) $\rightarrow$ (({\it{p\/}} $*$ ({\it{x\/}} $\div$ {\it{p\/}})) $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-product-aux1 \\ \index{divides-product-aux1}
{\rm{divides}}\,({\it{p\/}}, {\it{x\/}})\index{divides} $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $=$ ({\it{p\/}} $*$ (({\it{x\/}} $\div$ {\it{p\/}}) $*$ {\it{y\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-product-aux2 \\ \index{divides-product-aux2}
{\rm{divides}}\,({\it{p\/}}, {\it{p\/}} $*$ {\it{w\/}})\index{divides} $=$ {\bf{t}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-product \\ \index{divides-product}
{\rm{divides}}\,({\it{p\/}}, {\it{x\/}})\index{divides} $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, {\it{x\/}} $*$ {\it{y\/}})\index{divides}
\end{tabbing}


\begin{verbatim}; ok to here -- saved as basic4c

\end{verbatim}\begin{tabbing}{\sc Theorem}:  divides-sum \\ \index{divides-sum}
({\rm{divides}}\,({\it{p\/}}, {\it{u\/}} $+$ {\it{v\/}})\index{divides} $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{v\/}})\index{divides}) $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, {\it{u\/}})\index{divides}
\end{tabbing}
\begin{verbatim}; really just a restatement of DIVIDES-PLUS-REWRITE

\end{verbatim}\begin{tabbing}{\sc Theorem}:  divides-reduction-aux1 \\ \index{divides-reduction-aux1}
({\tt{1}} $<$ {\it{p\/}}) $\rightarrow$ ((({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $+$ ({\it{b\/}} $*$ ({\it{p\/}} $\div$ {\it{b\/}}))) $=$ {\it{p\/}})
\end{tabbing}
\begin{verbatim}; just a restatement of REMAINDER-QUOTIENT

; now, multiply on left by a:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divides-reduction-aux2 \\ \index{divides-reduction-aux2}
\=\+({\tt{1}} $<$ {\it{p\/}}) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $*$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) $+$ ({\it{a\/}} $*$ ({\it{b\/}} $*$ ({\it{p\/}} $\div$ {\it{b\/}})))) $=$ ({\it{a\/}} $*$ {\it{p\/}}))\-
\end{tabbing}

\begin{verbatim}; since p divides a*p: 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divides-reduction-aux3 \\ \index{divides-reduction-aux3}
({\tt{1}} $<$ {\it{p\/}}) $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, ({\it{a\/}} $*$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) $+$ ({\it{a\/}} $*$ ({\it{b\/}} $*$ ({\it{p\/}} $\div$ {\it{b\/}}))))\index{divides}
\end{tabbing}

\begin{verbatim}; now, if p divides a*b, it divides the second term
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divides-reduction-aux4 \\ \index{divides-reduction-aux4}
{\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides} $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ ({\it{b\/}} $*$ {\it{anything\/}}))\index{divides}
\end{tabbing}


\begin{verbatim}; hence:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divides-reduction \\ \index{divides-reduction}
(({\tt{1}} $<$ {\it{p\/}}) $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides}) $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}))\index{divides}
\end{tabbing} 
\begin{verbatim}; point of this lemma -- it reduces b to a smaller b', so induction can be used

; basis for induction:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux1 \\ \index{prime-divides-small-product-aux!1}
{\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\tt{1}})\index{divides} $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux2 \\ \index{prime-divides-small-product-aux!2}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\tt{1}} $<$ {\it{b\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{p\/}})) $\rightarrow$ ({\tt{0}} $<$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}))
\end{tabbing}
\begin{verbatim}; just a restatement of little-step

; ok to here -- save as "basic4d"


; goal -- prime-divides-small-product is of form:
; (prime p) --> phi(b,p,a)
; we want to prove a lemma saying (prime p) & not(phi(b,p,a)) -->
; remainder(p,b) < b  and not(phi(remainder(p,b),p,a))
; phi is: not( b<p  and 0<b  and divides(p, a*b) and not(divides(p, a)))
; we can't seem to prove the induction lemma all in one step

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux3 \\ \index{prime-divides-small-product-aux!3}
({\tt{0}} $<$ {\it{b\/}}) $\rightarrow$ (({\tt{1}} $<$ {\it{b\/}}) $\vee$ ({\tt{1}} $=$ {\it{b\/}}))
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux4 \\ \index{prime-divides-small-product-aux!4}
(({\tt{0}} $<$ {\it{b\/}}) $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) $\rightarrow$ ({\tt{1}} $<$ {\it{b\/}})
\end{tabbing}
\begin{verbatim}; ok
; i.e., the the induction lemma is trivial unless 1<b

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux5 \\ \index{prime-divides-small-product-aux!5}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\tt{1}} $<$ {\it{b\/}})) $\rightarrow$ (({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $<$ {\it{b\/}})
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux6 \\ \index{prime-divides-small-product-aux!6}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\tt{1}} $<$ {\it{b\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{p\/}})) $\rightarrow$ ({\tt{0}} $<$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}))
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux7 \\ \index{prime-divides-small-product-aux!7}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\tt{1}} $<$ {\it{b\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{p\/}})) $\rightarrow$ (({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $<$ {\it{p\/}})
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux8 \\ \index{prime-divides-small-product-aux!8}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}))\index{divides} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}))\-\-
\end{tabbing}
\begin{verbatim}; trivially rewrites to T, after 166.6 seconds !!!!!!!!

; the induction lemma -- same as above, but with 1 replaced by 0
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product-aux9 \\ \index{prime-divides-small-product-aux!9}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ ({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}))\index{divides} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}))\-\-
\end{tabbing}
\begin{verbatim}; rewrites trivially to T after 76.3 sec


; we still have to force nqthm to do the right induction

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{kludge} \\  
\=\+{\rm{kludge}}\,({\it{b\/}}, {\it{p\/}})\index{kludge} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{prime}}\,({\it{p\/}})\index{prime}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\tt{0}} $\not<$ {\it{b\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{kludge}}\,({\it{p\/}} ${}${\bf{mod}}${}$ {\it{b\/}}, {\it{p\/}})\index{kludge}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim}; always returns 0, but now we can use it in an induct hint

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-small-product \\ \index{prime-divides-small-product}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides} $\wedge$ ({\tt{0}} $<$ {\it{b\/}}) $\wedge$ ({\it{b\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}\-
\end{tabbing}
\begin{verbatim}; ok after 199.1 sec -- probably phrasing some of the auxilliary
; lemmas as rewrite rules would have helped speed things up

;;; ok to here -- save as basic4e

; now, try to replace (b < p) by (not (divides p b))
; idea -- if p divdes a*b, then p divides a*(b mod p) -- if  b mod p 
; isn't 0, then it's between 0 and p, so apply prime-divides-small-product

; first step -- prove a variant of divides-reduction, but replacing
; (remainder p b) by (remainder b p)
; i.e.  : divides p (a * b) --> divides p (a * remainder b p)
; say, 
; plan
; remainder b p + p * b/p  = fix( b)    (REMAINDER-QUOTENT)
;  a * remainder b p + a * ( p * b/p) = a * b


\end{verbatim}\begin{tabbing}{\sc Theorem}:  divides-reduction-var-aux1 \\ \index{divides-reduction-var-aux1}
\=\+({\it{b\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $*$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) $+$ ({\it{a\/}} $*$ ({\it{p\/}} $*$ ({\it{b\/}} $\div$ {\it{p\/}})))) $=$ ({\it{a\/}} $*$ {\it{b\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-reduction-var-aux2 \\ \index{divides-reduction-var-aux2}
{\rm{divides}}\,({\it{p\/}}, {\it{p\/}} $*$ {\it{anything\/}})\index{divides}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-reduction-var-aux3 \\ \index{divides-reduction-var-aux3}
({\it{a\/}} $*$ ({\it{p\/}} $*$ {\it{anything\/}})) $=$ ({\it{p\/}} $*$ ({\it{a\/}} $*$ {\it{anything\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-reduction-var-aux4 \\ \index{divides-reduction-var-aux4}
{\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ ({\it{p\/}} $*$ {\it{anything\/}}))\index{divides}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-reduction-var \\ \index{divides-reduction-var}
(({\it{b\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides}) $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\index{divides}
\end{tabbing}


\begin{verbatim}; ok to here -- save as basic4f

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-product-aux1 \\ \index{prime-divides-product-aux1}
(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) $\rightarrow$ (({\tt{0}} $<$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prime-divides-product-aux2 \\ \index{prime-divides-product-aux2}
{\rm{prime}}\,({\it{p\/}})\index{prime} $\rightarrow$ ((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $<$ {\it{p\/}}) $=$ {\bf{t}})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  prime-divides-product \\ \index{prime-divides-product}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}} $*$ {\it{b\/}})\index{divides} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{b\/}})\index{divides})) $\rightarrow$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}
\end{tabbing}
\begin{verbatim};;;;;;;;  THIS is the key lemma -- the rest should be just list-hacking

\end{verbatim}\begin{tabbing}{\sc Theorem}:  car-divides-times-list \\ \index{car-divides-times-list}
{\rm{listp}}\,({\it{l\/}}) $\rightarrow$ {\rm{divides}}\,({\rm{car}}\,({\it{l\/}}), {\rm{times-list}}\,({\it{l\/}})\index{times-list})\index{divides}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-equal \\ \index{divides-equal}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\it{q\/}})\index{divides}) $\rightarrow$ (({\it{p\/}} $=$ {\it{q\/}}) $=$ {\bf{t}})
\end{tabbing}

\begin{verbatim}; following should be trivial by times-divides-product
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-list-aux1 \\ \index{prime-divides-list-aux1}
\=\+(\=\+{\rm{prime-list}}\,({\it{l\/}})\index{prime-list} \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{l\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\it{l\/}})\index{times-list})\index{divides} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{times-list})\index{divides}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\rm{car}}\,({\it{l\/}}))\index{divides}\-
\end{tabbing}


\noindent{\sc Event}:   Disable prime-divides-small-product-aux1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable prime-divides-small-product-aux2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable prime-divides-small-product.

\addvspace{18pt}
\begin{verbatim}; these auxilliaries are getting in the way

\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-list-aux2 \\ \index{prime-divides-list-aux2}
\=\+(\=\+{\rm{prime-list}}\,({\it{l\/}})\index{prime-list} \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{l\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\it{l\/}})\index{times-list})\index{divides} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{times-list})\index{divides}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\it{l\/}}) $=$ {\it{p\/}})\-
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}
\noindent{\sc Event}:   Disable prime-divides-list-aux1.

\addvspace{18pt}

\begin{verbatim}; basis of induction
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-list-aux3 \\ \index{prime-divides-list-aux3}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{l\/}} $\simeq\;${{\bf{nil}}}${}$)) $\rightarrow$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\it{l\/}})\index{times-list})\index{divides})
\end{tabbing}
\begin{verbatim}; ok


; so it can see the trivial induction:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-list-aux4 \\ \index{prime-divides-list-aux4}
\=\+({\rm{prime-list}}\,({\it{l\/}})\index{prime-list} $\wedge$ {\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\it{l\/}})\index{times-list})\index{divides}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{listp}}\,({\it{l\/}}) $\wedge$ (({\rm{car}}\,({\it{l\/}}) $=$ {\it{p\/}}) $\vee$ {\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{times-list})\index{divides}))\-
\end{tabbing}
\begin{verbatim}; ok
\end{verbatim}
\noindent{\sc Event}:   Disable prime-divides-list-aux2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable prime-divides-list-aux3.

\addvspace{18pt}

\begin{verbatim}; now, by a simple induction on L:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-divides-list \\ \index{prime-divides-list}
({\rm{prime-list}}\,({\it{l\/}})\index{prime-list} $\wedge$ {\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{divides}}\,({\it{p\/}}, {\rm{times-list}}\,({\it{l\/}})\index{times-list})\index{divides}) $\rightarrow$ ({\it{p\/}} $\in$ {\it{l\/}})
\end{tabbing}
\begin{verbatim}; ok


;;; two lemmas from basic.events now follow trivially

    \end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-list-times-list \\ \index{prime-list-times-list}
\=\+({\rm{prime}}\,({\it{c\/}})\index{prime} $\wedge$ {\rm{prime-list}}\,({\it{l2\/}})\index{prime-list} $\wedge$ ({\it{c\/}} $\not\in$ {\it{l2\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{times-list}}\,({\it{l2\/}})\index{times-list} ${}${\bf{mod}}${}$ {\it{c\/}}) $\not=$ {\tt{0}})\-
\end{tabbing}


    \begin{tabbing}{\sc Theorem}:  prime-member \\ \index{prime-member}
\=\+((({\it{c\/}} $*$ {\rm{times-list}}\,({\it{l1\/}})\index{times-list}) $=$ {\rm{times-list}}\,({\it{l2\/}})\index{times-list}) $\wedge$ {\rm{prime}}\,({\it{c\/}})\index{prime} $\wedge$ {\rm{prime-list}}\,({\it{l2\/}})\index{prime-list}) \\ 
$\rightarrow$$\;\;\;\;$({\it{c\/}} $\in$ {\it{l2\/}})\-
\end{tabbing}

\begin{verbatim};;;;; some more lemmas about lists and producs

; this is the base case in PRIME-FACTORIZATION-UNIQUENESS
\end{verbatim}\begin{tabbing}{\sc Theorem}:  void-case \\ \index{void-case}
({\rm{prime-list}}\,({\it{l\/}})\index{prime-list} $\wedge$ ({\tt{1}} $=$ {\rm{times-list}}\,({\it{l\/}})\index{times-list})) $\rightarrow$ ({\it{l\/}} $\simeq\;${{\bf{nil}}}${}$)
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  product-delete \\ \index{product-delete}
({\it{x\/}} $\in$ {\it{l\/}}) $\rightarrow$ ({\rm{times-list}}\,({\it{l\/}})\index{times-list} $=$ ({\it{x\/}} $*$ {\rm{times-list}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{times-list}))
\end{tabbing}
\begin{verbatim}; ok


\end{verbatim}\begin{tabbing}{\sc Theorem}:  times-cancellation \\ \index{times-cancellation}
(({\tt{0}} $<$ {\it{p\/}}) $\wedge$ (({\it{p\/}} $*$ {\it{x\/}}) $=$ ({\it{p\/}} $*$ {\it{y\/}}))) $\rightarrow$ ({\rm{fix}}\,({\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  number-times-cancellation \\ \index{number-times-cancellation}
\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\tt{0}} $<$ {\it{p\/}}) $\wedge$ (({\it{p\/}} $*$ {\it{x\/}}) $=$ ({\it{p\/}} $*$ {\it{y\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $=$ {\it{y\/}}) $=$ {\bf{t}})\-
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  products-are-numbers \\ \index{products-are-numbers}
({\rm{times-list}}\,({\it{l\/}})\index{times-list} $\in\;${\bf{N}}${}$) $=$ {\bf{t}}
\end{tabbing}
\begin{verbatim}; ok

; changed
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divide-by-member-aux1 \\ \index{divide-by-member-aux1}
\=\+(({\it{p\/}} $\in$ {\it{l\/}}) $\wedge$ (({\it{p\/}} $*$ {\it{x\/}}) $=$ {\rm{times-list}}\,({\it{l\/}})\index{times-list})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{p\/}} $*$ {\rm{times-list}}\,({\rm{delete}}\,({\it{p\/}}, {\it{l\/}})\index{delete})\index{times-list}) $=$ ({\it{p\/}} $*$ {\it{x\/}}))\-
\end{tabbing}
\begin{verbatim}; ok

; next is just a kludge to force final rewrite
; with hypotheses stated in exact form required
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divide-by-member-aux2 \\ \index{divide-by-member-aux2}
\=\+(\=\+(({\it{p\/}} $*$ {\it{x\/}}) $=$ {\rm{times-list}}\,({\it{l\/}})\index{times-list}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{times-list}}\,({\it{l\/}})\index{times-list} $=$ ({\it{p\/}} $*$ {\rm{times-list}}\,({\rm{delete}}\,({\it{p\/}}, {\it{l\/}})\index{delete})\index{times-list})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{delete}}\,({\it{p\/}}, {\it{l\/}})\index{delete})\index{times-list} $=$ {\it{x\/}})\-
\end{tabbing}   

\begin{verbatim}; trivially, we should have now:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divide-by-member \\ \index{divide-by-member}
\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{p\/}} $\in$ {\it{l\/}}) $\wedge$ ({\tt{0}} $<$ {\it{p\/}}) $\wedge$ (({\it{p\/}} $*$ {\it{x\/}}) $=$ {\rm{times-list}}\,({\it{l\/}})\index{times-list})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{delete}}\,({\it{p\/}}, {\it{l\/}})\index{delete})\index{times-list} $=$ {\it{x\/}})\-
\end{tabbing}
\begin{verbatim}; ok

\end{verbatim}\begin{tabbing}{\sc Theorem}:  divide-by-prime-member-aux1 \\ \index{divide-by-prime-member-aux1}
({\rm{prime-list}}\,({\it{l\/}})\index{prime-list} $\wedge$ ({\it{p\/}} $\in$ {\it{l\/}})) $\rightarrow$ {\rm{prime}}\,({\it{p\/}})\index{prime}
\end{tabbing}

\begin{verbatim}; since primes are positive:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  divide-by-prime-member \\ \index{divide-by-prime-member}
\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{prime-list}}\,({\it{l\/}})\index{prime-list} $\wedge$ ({\it{p\/}} $\in$ {\it{l\/}}) $\wedge$ (({\it{p\/}} $*$ {\it{x\/}}) $=$ {\rm{times-list}}\,({\it{l\/}})\index{times-list})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{delete}}\,({\it{p\/}}, {\it{l\/}})\index{delete})\index{times-list} $=$ {\it{x\/}})\-
\end{tabbing}
\begin{verbatim}; ok

; should handle induction case in prime factorization uniqueness
\end{verbatim}\begin{tabbing}{\sc Theorem}:  reduct-product \\ \index{reduct-product}
\=\+(\=\+{\rm{prime-list}}\,({\it{l1\/}})\index{prime-list} \\ 
$\wedge$$\;\;\;\;${\rm{prime-list}}\,({\it{l2\/}})\index{prime-list} \\ 
$\wedge$$\;\;\;\;$({\rm{times-list}}\,({\it{l1\/}})\index{times-list} $=$ {\rm{times-list}}\,({\it{l2\/}})\index{times-list}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{l1\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{l1\/}}) $\in$ {\it{l2\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{delete}}\,({\rm{car}}\,({\it{l1\/}}), {\it{l2\/}})\index{delete})\index{times-list} $=$ {\rm{times-list}}\,({\rm{cdr}}\,({\it{l1\/}}))\index{times-list})\-
\end{tabbing}
\begin{verbatim}; ok






;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; On to the goal:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}
\noindent{\sc Event}:   Disable divides-equal.

\addvspace{18pt}

\noindent{\sc Event}:   Disable divide-by-prime-member-aux1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  prime-factorization-uniqueness-aux1 \\ \index{prime-factorization-uniqueness-!aux1}
({\rm{prime-list}}\,({\it{l\/}})\index{prime-list} $\wedge$ {\rm{listp}}\,({\it{l\/}})) $\rightarrow$ ({\tt{1}} $<$ {\rm{times-list}}\,({\it{l\/}})\index{times-list})
\end{tabbing}

\begin{verbatim}; a trivial variant:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-factorization-uniqueness-aux2 \\ \index{prime-factorization-uniqueness-!aux2}
({\rm{prime-list}}\,({\it{l\/}})\index{prime-list} $\wedge$ ({\tt{1}} $=$ {\rm{times-list}}\,({\it{l\/}})\index{times-list})) $\rightarrow$ ($\neg$ {\rm{listp}}\,({\it{l\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable product-delete.

\addvspace{18pt}

\begin{verbatim}; seems to require some hints in our present setting
    \end{verbatim}\begin{tabbing}{\sc Theorem}:  prime-factorization-uniqueness \\ \index{prime-factorization-uniqueness}
\=\+({\rm{prime-list}}\,({\it{l1\/}})\index{prime-list} $\wedge$ {\rm{prime-list}}\,({\it{l2\/}})\index{prime-list} $\wedge$ ({\rm{times-list}}\,({\it{l1\/}})\index{times-list} $=$ {\rm{times-list}}\,({\it{l2\/}})\index{times-list})) \\ 
$\rightarrow$$\;\;\;\;${\rm{perm}}\,({\it{l1\/}}, {\it{l2\/}})\index{perm}\-
\end{tabbing}









%\end{list}
\printindex
\end{document}
