\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.

|#

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

\addvspace{18pt}

\begin{verbatim}#|

The following C program computes the greatest common divisor of 
three nonnegative integers a, b and c. We investigate the machine 
code of this program generated by a widely used C compiler gcc, 
and verify the correctness of the code.  The aim here is to see 
how to handle subroutine calls.

gcd3(a, b, c)
long int a, b, c;
{
  gcd(gcd(a, b), c);
}

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

0x2324 <gcd3>:          linkw a6,#0
0x2328 <gcd3+4>:        movel a2,sp@-
0x232a <gcd3+6>:        movel a6@(16),sp@-
0x232e <gcd3+10>:       movel a6@(12),sp@-
0x2332 <gcd3+14>:       movel a6@(8),sp@-
0x2336 <gcd3+18>:       lea @#0x2350 <gcd>,a2
0x233c <gcd3+24>:       jsr a2@
0x233e <gcd3+26>:       addqw #8,sp
0x2340 <gcd3+28>:       movel d0,sp@-
0x2342 <gcd3+30>:       jsr a2@
0x2344 <gcd3+32>:       moveal a6@(-4),a2
0x2348 <gcd3+36>:       unlk a6
0x234a <gcd3+38>:       rts

The machine code of the above program is:

<gcd3>:       0x4e56  0x0000  0x2f0a  0x2f2e  0x0010  0x2f2e  0x000c  0x2f2e
<gcd3+16>:    0x0008  0x45f9  0x0000  0x2350  0x4e92  0x504f  0x2f00  0x4e92
<gcd3+32>:    0x246e  0xfffc  0x4e5e  0x4e75

'(78      86      0       0       47      10      47      46
  0       16      47      46      0       12      47      46
  0       8       69      249     0       0       35      80
  78      146     80      79      47      0       78      146
  36      110     255     252     78      94      78      117)
|#

; now we start to verify this GCD3 program,  defined by (gcd3-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd3-code} \\  
\=\+{\sc{gcd3-code}}\index{gcd3-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{69}} \\ 
{\tt{249}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{146}}{\tt{ }}{\tt{80}}{\tt{ }}{\tt{79}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{146}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{255}} \\ 
{\tt{252}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

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

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

\begin{tabbing}{\sc Definition}:\index{gcd3}$\;\;$
{\rm{gcd3}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3} $=$ {\rm{gcd}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{c\/}})\index{gcd}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gcd3-t0}$\;\;$
{\rm{gcd3-t0}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t0} $=$ {\tt{7}}
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{gcd3-t2}$\;\;$
{\rm{gcd3-t2}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t2} $=$ {\tt{3}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gcd3-t3}$\;\;$
{\rm{gcd3-t3}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t3} $=$ {\rm{gcd-t}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{c\/}})\index{gcd-t}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gcd3-t4}$\;\;$
{\rm{gcd3-t4}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t4} $=$ {\tt{3}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gcd3-t} \\  
\=\+{\rm{gcd3-t}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t} \\ 
$=$$\;\;\;\;${\rm{splus}}\,(\=\+{\rm{gcd3-t0}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t0}, \\ 
{\rm{splus}}\,(\=\+{\rm{gcd3-t1}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t1}, \\ 
{\rm{splus}}\,({\rm{gcd3-t2}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t2}, {\rm{splus}}\,({\rm{gcd3-t3}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t3}, {\rm{gcd3-t4}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t4})\index{splus})\index{splus})\-\index{splus})\-\index{splus}\-
\end{tabbing}

\begin{verbatim}; the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd3-statep} \\  
\=\+{\rm{gcd3-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{gcd3-loadp}}\,({\it{s\/}})\index{gcd3-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{gcd3-addr}}\index{gcd3-addr}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{36}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{52}})\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{c\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{12}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{a\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{c\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the state after the execution of the first JSR instruction, but before
; the execution of the subroutine GCD.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd3-s0p} \\  
\=\+{\rm{gcd3-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{gcd3-loadp}}\,({\it{s\/}})\index{gcd3-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{gcd-addr}}\index{gcd-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an} $=$ {\sc{gcd-addr}}\index{gcd-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr} $=$ {\rm{add}}\,({\tt{32}}, {\sc{gcd3-addr}}\index{gcd3-addr}, {\tt{26}})\index{add}) \\ 
$\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{52}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{20}})\index{add})\index{equal*} \\ 
$\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{c\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{12}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{a\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{c\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the state right after return from the first call to subroutine GCD.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd3-s1p} \\  
\=\+{\rm{gcd3-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{gcd3-loadp}}\,({\it{s\/}})\index{gcd3-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an} $=$ {\sc{gcd-addr}}\index{gcd-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{gcd3-addr}}\index{gcd3-addr}, {\tt{26}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{52}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{16}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{iread-dn} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) \\ 
$\wedge$$\;\;\;\;$({\it{c\/}} $=$ {\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$$\;\;\;\;$({\tt{0}} $<$ {\it{a\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{c\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the state after the execution of the second JSR, but before the 
; execution of the subroutine GCD.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd3-s2p} \\  
\=\+{\rm{gcd3-s2p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s2p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{gcd3-loadp}}\,({\it{s\/}})\index{gcd3-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{gcd-addr}}\index{gcd-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr} $=$ {\rm{add}}\,({\tt{32}}, {\sc{gcd3-addr}}\index{gcd3-addr}, {\tt{32}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{52}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{16}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\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{c\/}} $=$ {\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$$\;\;\;\;$({\tt{0}} $<$ {\it{a\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{c\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the state returned from the second call to the subroutine GCD.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gcd3-s3p} \\  
\=\+{\rm{gcd3-s3p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s3p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{gcd3-loadp}}\,({\it{s\/}})\index{gcd3-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{gcd3-addr}}\index{gcd3-addr}, {\tt{32}})\index{add}) \\ 
$\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{44}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{12}})\index{add})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{c\/}})\index{gcd} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{a\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{c\/}}))\-\-
\end{tabbing}

\begin{verbatim}; from the initial state to s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd3-s-s0 \\ \index{gcd3-s-s0}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t0}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd3-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gcd3-s0p}}\,({\it{s0\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s0\/}})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s0\/}})\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}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\it{s0\/}})\index{rn-saved} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{read-an}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd3-s-s0-rfile \\ \index{gcd3-s-s0-rfile}
\=\+({\rm{gcd3-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-statep} $\wedge$ {\rm{d2-7a3-5p}}\,({\it{rn\/}})\index{d2-7a3-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t0}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t0})\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}:  gcd3-s-s0-mem \\ \index{gcd3-s-s0-mem}
\=\+({\rm{gcd3-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{36}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{52}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t0}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t0})\index{stepn})\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})\-\-
\end{tabbing}

\begin{verbatim}; from s0 to s1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd3-s0-s1 \\ \index{gcd3-s0-s1}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t1}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t1})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd3-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gcd3-s1p}}\,({\it{s1\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s1\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s1\/}})\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{linked-a6}}\,({\it{s1\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\it{s1\/}})\index{rn-saved} $=$ {\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd3-s0-s1-rfile \\ \index{gcd3-s0-s1-rfile}
\=\+({\rm{gcd3-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-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{gcd3-t1}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t1})\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}:  gcd3-s0-s1-mem \\ \index{gcd3-s0-s1-mem}
\=\+({\rm{gcd3-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s0p} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{52}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t1}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t1})\index{stepn})\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})\-\-
\end{tabbing}

\begin{verbatim}; from s1 to s2. 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd3-s1-s2 \\ \index{gcd3-s1-s2}
\=\+{\bf let }\=\+{\it{s2\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t2}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t2})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd3-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s1p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gcd3-s2p}}\,({\it{s2\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s2p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s2\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s2\/}})\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{linked-a6}}\,({\it{s2\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\it{s2\/}})\index{rn-saved} $=$ {\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd3-s1-s2-rfile \\ \index{gcd3-s1-s2-rfile}
\=\+({\rm{gcd3-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s1p} $\wedge$ {\rm{d2-7a3-5p}}\,({\it{rn\/}})\index{d2-7a3-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t2}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t2})\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}:  gcd3-s1-s2-mem \\ \index{gcd3-s1-s2-mem}
\=\+({\rm{gcd3-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s1p} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{52}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t2}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t2})\index{stepn})\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})\-\-
\end{tabbing}

\begin{verbatim}; from s2 to s3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-nonzero \\ \index{gcd-nonzero}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $\not=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd3-s2-s3 \\ \index{gcd3-s2-s3}
\=\+{\bf let }\=\+{\it{s3\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t3}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t3})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd3-s2p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s2p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{gcd3-s3p}}\,({\it{s3\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s3p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s3\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s3\/}})\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{linked-a6}}\,({\it{s3\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{rn-saved}}\,({\it{s3\/}})\index{rn-saved} $=$ {\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd3-s2-s3-rfile \\ \index{gcd3-s2-s3-rfile}
\=\+({\rm{gcd3-s2p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s2p} $\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{gcd3-t3}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t3})\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}:  gcd3-s2-s3-mem \\ \index{gcd3-s2-s3-mem}
\=\+({\rm{gcd3-s2p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s2p} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{52}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t3}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t3})\index{stepn})\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})\-\-
\end{tabbing}

\begin{verbatim}; from s3 to exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd3-s3-sn \\ \index{gcd3-s3-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t4}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t4})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd3-s3p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s3p} \\ 
$\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}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{c\/}})\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})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd3-s3-sn-rfile \\ \index{gcd3-s3-sn-rfile}
\=\+({\rm{gcd3-s3p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s3p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}}) $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t4}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t4})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{rn\/}} $=$ {\tt{10}}$\;\;${\bf then }{\rm{head}}\,({\rm{rn-saved}}\,({\it{s\/}})\index{rn-saved}, {\it{oplen\/}})\index{head} \\ 
{\bf else }{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd3-s3-sn-mem \\ \index{gcd3-s3-sn-mem}
\=\+({\rm{gcd3-s3p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-s3p} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{52}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t4}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t4})\index{stepn})\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})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable gcd3-t0.

\addvspace{18pt}

\noindent{\sc Event}:   Disable gcd3-t1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable gcd3-t2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable gcd3-t3.

\addvspace{18pt}

\noindent{\sc Event}:   Disable gcd3-t4.

\addvspace{18pt}

\begin{verbatim}; the correctness of the program GCD3.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd3-correctness \\ \index{gcd3-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gcd3-t}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gcd3-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{gcd3-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-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{4}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{oplen\/}} $\leq$ {\tt{32}}) $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p}) \\ 
$\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{36}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{52}})\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}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{c\/}})\index{gcd}))\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; in the logic, the function gcd3 does computes the greatest common divisor
; of its three arguments.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-trans \\ \index{remainder-trans}
((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  cd-divides-gcd \\ \index{cd-divides-gcd}
((({\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} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}})
\end{tabbing}

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


\noindent{\sc Event}:   Disable remainder-trans.

\addvspace{18pt}

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