\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 Yuan Yu.  All Rights Reserved.

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

 NO WARRANTY

 Yuan Yu 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 Yuan Yu 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.

|#

;            Proof of the Correctness of a GCD Program
\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim}#|

The following C program computes the greatest common divisor of two
integers a and b. We, here, investigate the machine code of this
program generated by a widely used C compiler, and verify the
correctness of the code.

/* computes the greatest common divisor by Euclid's algorithm */
gcd(int a, int b)
{
  while (a != 0){
    if (b == 0) return (a);
    if (a > b)
      a = a % b;
    else b = b % a;
  };
  return (b);
}

Here is the MC68020 assembly code of the above GCD program.  The code is 
generated by "gcc -O".

0x22c6 <gcd>:           linkw a6,#0
0x22ca <gcd+4>:         moveml d2-d3,sp@-
0x22ce <gcd+8>:         movel a6@(8),d2
0x22d2 <gcd+12>:        movel a6@(12),d3
0x22d6 <gcd+16>:        tstl d2
0x22d8 <gcd+18>:        beq 0x22f6 <gcd+48>
0x22da <gcd+20>:        tstl d3
0x22dc <gcd+22>:        bne 0x22e2 <gcd+28>
0x22de <gcd+24>:        movel d2,d0
0x22e0 <gcd+26>:        bra 0x22f8 <gcd+50>
0x22e2 <gcd+28>:        cmpl d2,d3
0x22e4 <gcd+30>:        bge 0x22ee <gcd+40>
0x22e6 <gcd+32>:        divsll d3,d0,d2
0x22ea <gcd+36>:        movel d0,d2
0x22ec <gcd+38>:        bra 0x22d6 <gcd+16>
0x22ee <gcd+40>:        divsll d2,d0,d3
0x22f2 <gcd+44>:        movel d0,d3
0x22f4 <gcd+46>:        bra 0x22d6 <gcd+16>
0x22f6 <gcd+48>:        movel d3,d0
0x22f8 <gcd+50>:        moveml a6@(-8),d2-d3
0x22fe <gcd+56>:        unlk a6
0x2300 <gcd+58>:        rts

The machine code of the above program is:

<gcd>:       0x4e56  0x0000  0x48e7  0x3000  0x242e  0x0008  0x262e  0x000c
<gcd+16>:    0x4a82  0x671c  0x4a83  0x6604  0x2002  0x6016  0xb682  0x6c08
<gcd+32>:    0x4c43  0x2800  0x2400  0x60e8  0x4c42  0x3800  0x2600  0x60e0
<gcd+48>:    0x2003  0x4cee  0x000c  0xfff8  0x4e5e  0x4e75

'(78      86      0       0       72      231     48      0
  36      46      0       8       38      46      0       12
  74      130     103     28      74      131     102     4
  32      2       96      22      182     130     108     8
  76      67      40      0       36      0       96      232
  76      66      56      0       38      0       96      224
  32      3       76      238     0       12      255     248
  78      94      78      117)
|#

; now we start the correctness proof of this GCD program, defined by 
; (gcd-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd-code} \\  
\=\+{\sc{gcd-code}}\index{gcd-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{231}}{\tt{ }}{\tt{48}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{130}} \\ 
{\tt{103}}{\tt{ }}{\tt{28}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{131}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{22}}{\tt{ }}{\tt{182}}{\tt{ }}{\tt{130}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{67}} \\ 
{\tt{40}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{232}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{56}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{224}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{238}} \\ 
{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{248}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  gcd-load \\ \index{gcd-load}
\=\+{\rm{gcd-loadp}}\,({\it{s\/}})\index{gcd-loadp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{evenp}}\,({\sc{gcd-addr}}\index{gcd-addr})\index{evenp} \\ 
$\wedge$$\;\;\;\;$({\sc{gcd-addr}}\index{gcd-addr} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\sc{gcd-addr}}\index{gcd-addr}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\sc{gcd-addr}}\index{gcd-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\sc{gcd-addr}}\index{gcd-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{gcd-code}}\index{gcd-code})\index{mcode-addrp})\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it gcd-loadp\/} and {\it gcd-addr\/}.

\begin{tabbing}{\sc Theorem}:  stepn-gcd-loadp \\ \index{stepn-gcd-loadp}
{\rm{gcd-loadp}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{n\/}})\index{stepn})\index{gcd-loadp} $=$ {\rm{gcd-loadp}}\,({\it{s\/}})\index{gcd-loadp}
\end{tabbing}

\begin{verbatim}; the functional description of the program (gcd-code). 
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd} \\  
\=\+{\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{fix}}\,({\it{b\/}}) \\ 
{\bf elseif }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{a\/}} \\ 
{\bf elseif }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }{\rm{gcd}}\,({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}, {\it{b\/}})\index{gcd} \\ 
{\bf else }{\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}})\index{gcd}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the clock function.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd-t1} \\  
\=\+{\rm{gcd-t1}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{6}} \\ 
{\bf elseif }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{9}} \\ 
{\bf elseif }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }{\rm{splus}}\,({\tt{9}}, {\rm{gcd-t1}}\,({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}, {\it{b\/}})\index{gcd-t1})\index{splus} \\ 
{\bf else }{\rm{splus}}\,({\tt{9}}, {\rm{gcd-t1}}\,({\it{a\/}}, {\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}})\index{gcd-t1})\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gcd-t}$\;\;$
{\rm{gcd-t}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t} $=$ {\rm{splus}}\,({\tt{4}}, {\rm{gcd-t1}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t1})\index{splus}
\end{tabbing}

\begin{verbatim}; an induction hint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd-induct} \\  
\=\+{\rm{gcd-induct}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{a\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{b\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }{\rm{gcd-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}, {\it{b\/}})\index{gcd-induct} \\ 
{\bf else }{\rm{gcd-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\it{a\/}}, {\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}})\index{gcd-induct}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd-statep} \\  
\=\+{\rm{gcd-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{gcd-code}}\index{gcd-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{24}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}

\begin{verbatim}; an intermediate state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd-s0p} \\  
\=\+{\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{60}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{gcd-code}}\index{gcd-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{8}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{24}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}

\begin{verbatim}; s --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-s-s0 \\ \index{gcd-s-s0}
\=\+{\rm{gcd-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gcd-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\-)\-\-
\end{tabbing}		   

\begin{tabbing}{\sc Theorem}:  gcd-s-s0-rfile \\ \index{gcd-s-s0-rfile}
\=\+({\rm{gcd-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-statep} $\wedge$ {\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s-s0-mem \\ \index{gcd-s-s0-mem}
\=\+({\rm{gcd-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{l\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; s0 --> exit.
; base case: s0 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-s0-sn-base-1 \\ \index{gcd-s0-sn-base-1}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ ({\it{a\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{iread-dn} $=$ {\rm{fix}}\,({\it{b\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s0-sn-base-rfile-1 \\ \index{gcd-s0-sn-base-rfile-1}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ ({\it{a\/}} $\simeq {\tt{0}}$) $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,({\it{oplen\/}}, {\tt{0}}, {\it{rn\/}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s0-sn-base-2 \\ \index{gcd-s0-sn-base-2}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{iread-dn} $=$ {\rm{fix}}\,({\it{a\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s0-sn-base-rfile-2 \\ \index{gcd-s0-sn-base-rfile-2}
\=\+(\=\+{\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,({\it{oplen\/}}, {\tt{0}}, {\it{rn\/}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; induction case:  s0 --> s0.
\end{verbatim}
\noindent{\sc Event}:   Enable integerp.

\addvspace{18pt}

\noindent{\sc Event}:   Enable iremainder.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  gcd-s0-s0-1 \\ \index{gcd-s0-s0-1}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $<$ {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gcd-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}, {\it{b\/}})\index{gcd-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s0-s0-2 \\ \index{gcd-s0-s0-2}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not<$ {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gcd-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\it{a\/}}, {\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}})\index{gcd-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-mem}, {\it{l\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s0-s0-rfile-1 \\ \index{gcd-s0-s0-rfile-1}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $<$ {\it{a\/}}) $\wedge$ {\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s0-s0-rfile-2 \\ \index{gcd-s0-s0-rfile-2}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not<$ {\it{a\/}}) $\wedge$ {\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; put together.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-s0-sn \\ \index{gcd-s0-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd-t1}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{iread-dn} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-s0-sn-rfile \\ \index{gcd-s0-sn-rfile}
\=\+({\rm{gcd-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-s0p} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd-t1}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t1})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d4-7a2-5p}}\,({\it{rn\/}})\index{d4-7a2-5p}$\;\;${\bf then }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn} \\ 
{\bf else }{\rm{get-vlst}}\,({\it{oplen\/}}, {\tt{0}}, {\it{rn\/}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{)}}, {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{8}}, {\tt{2}})\index{movem-saved})\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; the correctness of gcd.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-correctness \\ \index{gcd-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd-t}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gcd-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{24}})\index{disjoint} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-)\- \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{iread-dn} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}))\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable gcd-t.

\addvspace{18pt}

\begin{verbatim}; to prove that (gcd a b) does compute the greatest common divisor, we need 
; to prove the following two theorems:
;     1. (gcd a b) divides a and (gcd a b) divides b. 
;        i.e. (gcd a b) is a common divisor of a and b.
;     2. any divisor of a and b is no greater than (gcd a b).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-remainder \\ \index{remainder-remainder}
(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\rightarrow$ ((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}))
\end{tabbing}

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

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

\begin{verbatim}; a simple timing analysis.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  lessp-times-lessp \\ \index{lessp-times-lessp}
(({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\it{a\/}} $<$ ({\it{b\/}} $*$ {\it{c\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-shrink-half \\ \index{remainder-shrink-half}
(({\it{b\/}} $\leq$ {\it{a\/}}) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ (({\it{a\/}} $\div$ {\tt{2}}) $\not<$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-t-shrink-1 \\ \index{gcd-t-shrink-1}
(({\it{b\/}} $\leq$ {\it{a\/}}) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ (({\rm{log}}\,({\tt{2}}, {\it{a\/}})\index{log} $-\;1$) $\not<$ {\rm{log}}\,({\tt{2}}, {\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})\index{log})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-t-shrink-2 \\ \index{gcd-t-shrink-2}
\=\+(({\it{b\/}} $\leq$ {\it{a\/}}) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{a\/}} $\not=$ {\tt{1}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\tt{9}} $*$ ({\it{x\/}} $+$ {\rm{log}}\,({\tt{2}}, {\it{a\/}})\index{log})) \\ 
$\not<$$\;\;\;\;$({\tt{9}} $+$ ({\tt{9}} $*$ ({\it{x\/}} $+$ {\rm{log}}\,({\tt{2}}, {\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})\index{log}))))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gcd-t2} \\  
\=\+{\rm{gcd-t2}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{6}} \\ 
{\bf elseif }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{9}} \\ 
{\bf elseif }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }{\tt{9}} $+$ {\rm{gcd-t2}}\,({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}, {\it{b\/}})\index{gcd-t2} \\ 
{\bf elseif }{\it{a\/}} $<$ {\it{b\/}}$\;\;${\bf then }{\tt{9}} $+$ {\rm{gcd-t2}}\,({\it{a\/}}, {\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}})\index{gcd-t2} \\ 
{\bf else }{\tt{18}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-t2-ub \\ \index{gcd-t2-ub}
{\rm{gcd-t2}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t2} $\leq$ ({\tt{18}} $+$ ({\tt{9}} $*$ ({\rm{log}}\,({\tt{2}}, {\it{a\/}})\index{log} $+$ {\rm{log}}\,({\tt{2}}, {\it{b\/}})\index{log})))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  gcd-t-ub \\ \index{gcd-t-ub}
{\rm{gcd-t}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t} $\leq$ ({\tt{22}} $+$ ({\tt{9}} $*$ ({\rm{log}}\,({\tt{2}}, {\it{a\/}})\index{log} $+$ {\rm{log}}\,({\tt{2}}, {\it{b\/}})\index{log})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-t-ubound \\ \index{gcd-t-ubound}
(({\it{a\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{31}})\index{exp}) $\wedge$ ({\it{b\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\tt{31}})\index{exp})) $\rightarrow$ ({\rm{gcd-t}}\,({\it{a\/}}, {\it{b\/}})\index{gcd-t} $\leq$ {\tt{580}})
\end{tabbing}


\noindent{\sc Event}:   Make the library {\tt{"gcd"}} and compile it.

\addvspace{18pt}





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