\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 Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

 Computational Logic, Inc. 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 Computational Logic, Inc. 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.
|#

; Matt Wilding

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"extras"}} using the compiled version.

\addvspace{18pt}

\begin{verbatim};; Proof of Matijasevich's lemma constructed by MW week of 5-10-91.  Inspired by
;; proof in Concrete Mathematics by Graham, Knuth, and Patashnik and notes from 
;; Dijkstra's Capita Selecta Spring '90 course.

;;;; Some additional facts needed in the proof that appear useful 
;;;; enough to add to libraries (and a few facts to prove them)

\end{verbatim}\begin{tabbing}{\sc Theorem}:  irem-igcd-arg1 \\ \index{irem-igcd-arg1}
({\rm{irem}}\,({\rm{igcd}}\,({\it{a\/}}, {\it{b\/}})\index{igcd}, {\it{c\/}})\index{irem} $=$ {\tt{0}}) $=$ (({\rm{irem}}\,({\it{a\/}}, {\it{c\/}})\index{irem} $=$ {\tt{0}}) $\wedge$ ({\rm{irem}}\,({\it{b\/}}, {\it{c\/}})\index{irem} $=$ {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  irem-x-x \\ \index{irem-x-x}
{\rm{irem}}\,({\it{x\/}}, {\it{x\/}})\index{irem} $=$ {\tt{0}}
\end{tabbing}

\begin{verbatim};; The nonsensical induction hint is a silly trick to get the prover 
;; to throw an equality away after using it
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-times-easy-proof-helper-helper \\ \index{gcd-times-easy-proof-helper-helpe!r}
\=\+(({\it{a\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{b\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{c\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$((({\it{c\/}} $*$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd}) $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-times-easy-proof-helper \\ \index{gcd-times-easy-proof-helper}
(({\it{c\/}} $*$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-times-easy-proof \\ \index{gcd-times-easy-proof}
({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\tt{1}}) $\rightarrow$ ({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd})
\end{tabbing}
        
\begin{verbatim};; Would the more general case of rewriting gcd-times regardless 
;; of the value of gcd with one of the times arguments be superior?
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-times-easy \\ \index{gcd-times-easy}
\=\+({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\tt{1}}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd}) $\wedge$ ({\rm{gcd}}\,({\it{a\/}}, {\it{c\/}} $*$ {\it{b\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd}))\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  lessp-gcd3 \\ \index{lessp-gcd3}
\=\+(({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $<$ {\it{a\/}}) $=$ ((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$))) \\ 
$\wedge$$\;\;\;\;$(({\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd} $<$ {\it{a\/}}) $=$ ((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$)))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-gcd-0-proof \\ \index{equal-remainder-gcd-0-proof}
(({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) $=$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{verbatim};; not used in proof (though equal-remainder-gcd-0-proof is)
\end{verbatim}\begin{tabbing}{\sc Theorem}:  equal-remainder-gcd-0 \\ \index{equal-remainder-gcd-0}
\=\+((({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) $=$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}})) \\ 
$\wedge$$\;\;\;\;$((({\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) $=$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-x-y-x \\ \index{equal-remainder-x-y-x}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\it{x\/}}) \\ 
$=$$\;\;\;\;$(\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})) \\ 
$\vee$$\;\;\;\;$({\it{x\/}} $=$ {\tt{0}}) \\ 
$\vee$$\;\;\;\;$(({\rm{fix}}\,({\it{y\/}}) $=$ {\tt{0}}) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$)))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-a-gcd-exp-a \\ \index{gcd-a-gcd-exp-a}
\=\+{\rm{gcd}}\,({\it{a\/}}, {\rm{exp}}\,({\it{a\/}}, {\it{b\/}})\index{exp})\index{gcd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{fix}}\,({\it{a\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-gcd-times-1-help1 \\ \index{equal-gcd-times-1-help1}
(({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\tt{1}}) $\wedge$ ({\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd} $=$ {\tt{1}})) $\rightarrow$ ({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd} $=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-gcd-gcd-0-hack \\ \index{remainder-gcd-gcd-0-hack}
({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-gcd-times \\ \index{lessp-gcd-times}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\vee$ (({\it{b\/}} $*$ {\it{c\/}}) $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd} $\not<$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-hack \\ \index{lessp-1-hack}
({\tt{1}} $<$ {\it{x\/}}) $=$ (({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-gcd-times-1-help2 \\ \index{equal-gcd-times-1-help2}
({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd} $=$ {\tt{1}}) $\rightarrow$ ({\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd} $=$ {\tt{1}})
\end{tabbing}
             
\begin{tabbing}{\sc Theorem}:  equal-gcd-times-1 \\ \index{equal-gcd-times-1}
({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $*$ {\it{c\/}})\index{gcd} $=$ {\tt{1}}) $=$ (({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\tt{1}}) $\wedge$ ({\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd} $=$ {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-exp-1 \\ \index{gcd-exp-1}
\=\+(({\rm{gcd}}\,({\it{a\/}}, {\rm{exp}}\,({\it{b\/}}, {\it{c\/}})\index{exp})\index{gcd} $=$ {\tt{1}}) $=$ (({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\tt{1}}) $\vee$ ({\it{c\/}} $\simeq {\tt{0}}$))) \\ 
$\wedge$$\;\;\;\;$(({\rm{gcd}}\,({\rm{exp}}\,({\it{b\/}}, {\it{c\/}})\index{exp}, {\it{a\/}})\index{gcd} $=$ {\tt{1}}) $=$ (({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\tt{1}}) $\vee$ ({\it{c\/}} $\simeq {\tt{0}}$)))\-
\end{tabbing}

\begin{verbatim};; mistake in other version of this lemma limits applicability and
;; makes this version needed
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-remainder-times-fact1-proof2 \\ \index{gcd-remainder-times-fact1-proof!2}
({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\tt{1}}) $\rightarrow$ (((({\it{c\/}} $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) $=$ (({\it{c\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  times-quotient-better \\ \index{times-quotient-better}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+(({\it{x\/}} $\div$ {\it{y\/}}) $*$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\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}:  equal-remainder-exp-0 \\ \index{equal-remainder-exp-0}
((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ (({\rm{exp}}\,({\it{a\/}}, {\it{b\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  remainder-2-hack \\ \index{remainder-2-hack}
\=\+({\tt{2}} ${}${\bf{mod}}${}$ {\it{x\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} $=$ {\tt{1}}) $\vee$ ({\it{x\/}} $=$ {\tt{2}})$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{2}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times-hack2 \\ \index{remainder-times-hack2}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $\not=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} ${}${\bf{mod}}${}$ ({\it{b\/}} $*$ {\it{c\/}})) $\not=$ {\tt{0}}) $\wedge$ (({\it{a\/}} ${}${\bf{mod}}${}$ ({\it{c\/}} $*$ {\it{b\/}})) $\not=$ {\tt{0}}))\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  gcd-a-add1-a \\ \index{gcd-a-add1-a}
{\rm{gcd}}\,({\it{a\/}}, $1\;+$ {\it{a\/}})\index{gcd} $=$ {\tt{1}}
\end{tabbing}

\begin{verbatim};; These facts should perhaps be generalized into a meta lemma that 
;; factors first
\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-times-times-hack \\ \index{remainder-times-times-hack}
(({\it{b\/}} $*$ ({\it{a\/}} $*$ {\it{c\/}})) ${}${\bf{mod}}${}$ ({\it{a\/}} $*$ {\it{x\/}})) $=$ ({\it{a\/}} $*$ (({\it{b\/}} $*$ {\it{c\/}}) ${}${\bf{mod}}${}$ {\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-times-hack \\ \index{remainder-plus-times-hack}
\=\+((({\it{a\/}} $*$ {\it{x\/}}) $+$ ({\it{b\/}} $*$ ({\it{c\/}} $*$ ({\it{a\/}} $*$ {\it{y\/}})))) ${}${\bf{mod}}${}$ ({\it{a\/}} $*$ {\it{z\/}})) \\ 
$=$$\;\;\;\;$({\it{a\/}} $*$ (({\it{x\/}} $+$ ({\it{b\/}} $*$ ({\it{c\/}} $*$ {\it{y\/}}))) ${}${\bf{mod}}${}$ {\it{z\/}}))\-
\end{tabbing}


\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Now, on to the proof
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fib} \\  
\=\+{\rm{fib}}\,({\it{x\/}})\index{fib} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{fib}}\,(({\it{x\/}} $-\;1$) $-\;1$)\index{fib} $+$ {\rm{fib}}\,({\it{x\/}} $-\;1$)\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib-plus \\ \index{fib-plus}
\=\+{\rm{fib}}\,({\it{j\/}} $+$ {\it{k\/}})\index{fib} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{fib}}\,({\it{k\/}})\index{fib} \\ 
{\bf else }({\rm{fib}}\,($1\;+$ {\it{k\/}})\index{fib} $*$ {\rm{fib}}\,({\it{j\/}})\index{fib}) $+$ ({\rm{fib}}\,({\it{j\/}} $-\;1$)\index{fib} $*$ {\rm{fib}}\,({\it{k\/}})\index{fib})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-fib-next-fib \\ \index{gcd-fib-next-fib}
{\rm{gcd}}\,({\rm{fib}}\,({\it{n\/}})\index{fib}, {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib})\index{gcd} $=$ {\tt{1}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-fib \\ \index{gcd-fib}
{\rm{gcd}}\,({\rm{fib}}\,({\it{a\/}})\index{fib}, {\rm{fib}}\,({\it{b\/}})\index{fib})\index{gcd} $=$ {\rm{fib}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd})\index{fib}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  equal-fib-constant \\ \index{equal-fib-constant}
\=\+(({\rm{fib}}\,({\it{a\/}})\index{fib} $=$ {\tt{0}}) $=$ ({\it{a\/}} $\simeq {\tt{0}}$)) \\ 
$\wedge$$\;\;\;\;$(({\rm{fib}}\,({\it{a\/}})\index{fib} $=$ {\tt{1}}) $=$ (({\it{a\/}} $=$ {\tt{1}}) $\vee$ ({\it{a\/}} $=$ {\tt{2}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib-small \\ \index{fib-small}
\=\+({\it{a\/}} $<$ {\tt{3}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fib}}\,({\it{a\/}})\index{fib} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{double-fib-induction} \\  
\=\+{\rm{double-fib-induction}}\,({\it{a\/}}, {\it{b\/}})\index{double-fib-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{a\/}} $<$ {\tt{3}}) $\vee$ ({\it{b\/}} $<$ {\tt{3}})$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{double-fib-induction}}\,({\it{a\/}} $-\;1$, {\it{b\/}} $-\;1$)\index{double-fib-induction} \\ 
$\wedge$$\;\;\;\;${\rm{double-fib-induction}}\,(({\it{a\/}} $-\;1$) $-\;1$, ({\it{b\/}} $-\;1$) $-\;1$)\index{double-fib-induction}\-$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  lessp-fib-fib \\ \index{lessp-fib-fib}
({\rm{fib}}\,({\it{a\/}})\index{fib} $<$ {\rm{fib}}\,({\it{b\/}})\index{fib}) $=$ (({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ($\neg$ (({\it{a\/}} $=$ {\tt{1}}) $\wedge$ ({\it{b\/}} $=$ {\tt{2}}))))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-fib-fib-0 \\ \index{remainder-fib-fib-0}
(({\rm{fib}}\,({\it{a\/}})\index{fib} ${}${\bf{mod}}${}$ {\rm{fib}}\,({\it{b\/}})\index{fib}) $=$ {\tt{0}}) $=$ ((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\tt{0}}) $\vee$ ({\it{b\/}} $=$ {\tt{2}}))
\end{tabbing}

\begin{verbatim};; fib-times-open and fib-add1-times-open apply fib-plus to 
;; particular terms in a way that will be useful in the proof 
;; of fib-times-special
\end{verbatim}\begin{tabbing}{\sc Theorem}:  fib-times-open \\ \index{fib-times-open}
\=\+({\tt{0}} $<$ {\it{k\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fib}}\,({\it{k\/}} $*$ {\it{n\/}})\index{fib} \\ 
$=$$\;\;\;\;$(\=\+({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ (({\it{k\/}} $-\;1$) $*$ {\it{n\/}}))\index{fib}) \\ 
$+$$\;\;\;\;$({\rm{fib}}\,({\it{n\/}} $-\;1$)\index{fib} $*$ {\rm{fib}}\,(({\it{k\/}} $-\;1$) $*$ {\it{n\/}})\index{fib}))\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable fib-times-open.

\addvspace{18pt}
                
\begin{tabbing}{\sc Theorem}:  fib-add1-times-open \\ \index{fib-add1-times-open}
\=\+({\tt{0}} $<$ {\it{k\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fib}}\,($1\;+$ ({\it{k\/}} $*$ {\it{n\/}}))\index{fib} \\ 
$=$$\;\;\;\;$(\=\+({\rm{fib}}\,($1\;+$ (({\it{k\/}} $-\;1$) $*$ {\it{n\/}}))\index{fib} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}) \\ 
$+$$\;\;\;\;$({\rm{fib}}\,(({\it{k\/}} $-\;1$) $*$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib}))\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable fib-add1-times-open.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  fib-times-special-step \\ \index{fib-times-special-step}
\=\+({\tt{1}} $<$ {\it{k\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{k\/}} $*$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{exp}}\,({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}, {\it{k\/}} $-\;1$)\index{exp})) ${}${\bf{mod}}${}$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib})) \\ 
$=$$\;\;\;\;$(\=\+(\=\+({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{exp}}\,({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}, {\it{k\/}} $-\;1$)\index{exp}) \\ 
$+$$\;\;\;\;$(\=\+{\rm{fib}}\,({\it{n\/}} $-\;1$)\index{fib} \\ 
$*$$\;\;\;\;$(\=\+({\it{k\/}} $-\;1$) \\ 
$*$$\;\;\;\;$(\=\+{\rm{fib}}\,({\it{n\/}})\index{fib} \\ 
$*$$\;\;\;\;${\rm{exp}}\,({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}, ({\it{k\/}} $-\;1$) $-\;1$)\index{exp})\-)\-)\-)\- \\ 
${}${\bf{mod}}${}$$\;\;\;\;$({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib}))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib-remainder-hack \\ \index{fib-remainder-hack}
({\rm{fib}}\,({\it{x\/}} $*$ {\it{y\/}})\index{fib} ${}${\bf{mod}}${}$ {\rm{fib}}\,({\it{x\/}})\index{fib}) $=$ {\tt{0}}
\end{tabbing}

\begin{verbatim};; We wish the rewriter to use a modulo arithmetic equality to rewrite
;; a term.  Fortunately, we can can construct REMAINDER-FIB-BACKCHAIN
;; to do it the way we wish since the terms are of a specialized form
\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-backchain-proof1 \\ \index{remainder-backchain-proof1}
(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) $\rightarrow$ ((({\it{a\/}} $*$ {\it{d\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ (({\it{b\/}} $*$ {\it{d\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-backchain-proof2 \\ \index{remainder-backchain-proof2}
\=\+((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) $\wedge$ (({\it{d\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{e\/}} ${}${\bf{mod}}${}$ {\it{c\/}}))) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $+$ {\it{d\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ (({\it{b\/}} $+$ {\it{e\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-fib-backchain \\ \index{remainder-fib-backchain}
\=\+(\=\+(({\rm{fib}}\,({\it{x\/}})\index{fib} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\rm{exp}}\,({\it{p\/}}, {\it{q\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$(({\rm{fib}}\,({\it{y\/}})\index{fib} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ (({\it{r\/}} $*$ {\it{s\/}}) ${}${\bf{mod}}${}$ {\it{c\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{a\/}} $*$ {\rm{fib}}\,({\it{x\/}})\index{fib}) $+$ ({\it{b\/}} $*$ {\rm{fib}}\,({\it{y\/}})\index{fib})) ${}${\bf{mod}}${}$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$((({\it{a\/}} $*$ {\rm{exp}}\,({\it{p\/}}, {\it{q\/}})\index{exp}) $+$ ({\it{b\/}} $*$ ({\it{r\/}} $*$ {\it{s\/}}))) ${}${\bf{mod}}${}$ {\it{c\/}}))\-\-
\end{tabbing}

\begin{verbatim};; This is the guts of the proof
\end{verbatim}\begin{tabbing}{\sc Theorem}:  fib-times-special \\ \index{fib-times-special}
\=\+({\tt{1}} $<$ {\it{k\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{fib}}\,({\it{k\/}} $*$ {\it{n\/}})\index{fib} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\rm{fib}}\,({\it{n\/}})\index{fib}, {\tt{2}})\index{exp}) \\ 
$=$$\;\;\;\;$(\=\+({\it{k\/}} $*$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{exp}}\,({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}, {\it{k\/}} $-\;1$)\index{exp})) \\ 
${}${\bf{mod}}${}$$\;\;\;\;${\rm{exp}}\,({\rm{fib}}\,({\it{n\/}})\index{fib}, {\tt{2}})\index{exp})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{fib}}\,($1\;+$ ({\it{k\/}} $*$ {\it{n\/}}))\index{fib} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\rm{fib}}\,({\it{n\/}})\index{fib}, {\tt{2}})\index{exp}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}, {\it{k\/}})\index{exp} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\rm{fib}}\,({\it{n\/}})\index{fib}, {\tt{2}})\index{exp}))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib-remainder-times-special \\ \index{fib-remainder-times-special}
\=\+({\rm{fib}}\,({\it{n\/}} $*$ {\it{k\/}})\index{fib} ${}${\bf{mod}}${}$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib})) \\ 
$=$$\;\;\;\;$(({\it{k\/}} $*$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{exp}}\,({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}, {\it{k\/}} $-\;1$)\index{exp})) ${}${\bf{mod}}${}$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times-times-hack2 \\ \index{remainder-times-times-hack2}
(({\it{k\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ ({\it{n\/}} $*$ {\it{p\/}})) $=$ ({\it{n\/}} $*$ ({\it{k\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  matijasevich-lemma-helper \\ \index{matijasevich-lemma-helper}
\=\+(({\tt{2}} $<$ {\it{n\/}}) $\wedge$ (({\it{m\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\rm{fib}}\,({\it{m\/}})\index{fib} ${}${\bf{mod}}${}$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib})) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$(({\it{m\/}} ${}${\bf{mod}}${}$ ({\it{n\/}} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib})) $=$ {\tt{0}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  matijasevich-lemma \\ \index{matijasevich-lemma}
\=\+({\tt{2}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\rm{fib}}\,({\it{m\/}})\index{fib} ${}${\bf{mod}}${}$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib})) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$(({\it{m\/}} ${}${\bf{mod}}${}$ ({\it{n\/}} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib})) $=$ {\tt{0}}))\-\-
\end{tabbing}

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