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

|#

;           Function Pointer Constrains with a Witness GT
\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim}#|
/* greater than relation */
gt(int a, int b)
{
  if (a == b)
    return 0;
  else if (a > b)
    return 1;
  else return -1;
}

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

0x22de <gt>:    linkw fp,#0 
0x22e2 <gt+4>:  movel fp@(8),d1 
0x22e6 <gt+8>:  movel fp@(12),d0 
0x22ea <gt+12>: cmpl d1,d0 
0x22ec <gt+14>: bne 0x22f2 <gt+20> 
0x22ee <gt+16>: clrl d0 
0x22f0 <gt+18>: bra 0x22fc <gt+30> 
0x22f2 <gt+20>: cmpl d1,d0 
0x22f4 <gt+22>: bge 0x22fa <gt+28> 
0x22f6 <gt+24>: movel #1,d0 
0x22f8 <gt+26>: bra 0x22fc <gt+30> 
0x22fa <gt+28>: movel #-1,d0 
0x22fc <gt+30>: unlk fp 
0x22fe <gt+32>: rts 

The machine code:

0x22de <gt>:    0x4e56  0x0000  0x222e  0x0008  0x202e  0x000c  0xb081  0x6604 
0x22ee <gt+16>: 0x4280  0x600a  0xb081  0x6c04  0x7001  0x6002  0x70ff  0x4e5e 
0x22fe <gt+32>: 0x4e75 

'(78      86      0       0       34      46      0       8 
  32      46      0       12      176     129     102     4 
  66      128     96      10      176     129     108     4 
  112     1       96      2       112     255     78      94 
  78      117)
|#

; In Nqthm logic, gt-code defines the programs.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gt-code} \\  
\=\+{\sc{gt-code}}\index{gt-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}} \\ 
{\tt{96}}{\tt{ }}{\tt{10}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{112}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{112}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gt} \\  
\=\+{\rm{gt}}\,({\it{a\/}}, {\it{b\/}})\index{gt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\it{b\/}}, {\it{a\/}})\index{ilessp}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{-1}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gt-t} \\  
\=\+{\rm{gt-t}}\,({\it{a\/}}, {\it{b\/}})\index{gt-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\tt{9}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\it{b\/}}, {\it{a\/}})\index{ilessp}$\;\;${\bf then }{\tt{11}} \\ 
{\bf else }{\tt{10}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; preconditions on the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{gt-statep} \\  
\=\+{\rm{gt-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gt-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{34}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{gt-code}}\index{gt-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{16}})\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}))\-\-
\end{tabbing}

\begin{verbatim}; correctness.
\end{verbatim}
\noindent{\sc Event}:   Disable ilessp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  gt-s-sn \\ \index{gt-s-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{gt-t}}\,({\it{a\/}}, {\it{b\/}})\index{gt-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{gt-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{gt-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-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add})\- \\ 
$\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{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{4}})\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{gt}}\,({\it{a\/}}, {\it{b\/}})\index{gt}))\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\noindent{\sc Event}:   Disable gt.

\addvspace{18pt}

\begin{verbatim}; function constrain with gt as witness.
\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  p-disjointness \\ \index{p-disjointness}
({\rm{p-disjoint}}\,({\it{x\/}}, {\it{n\/}}, {\it{s\/}})\index{p-disjoint} $\wedge$ (({\it{j\/}} $+$ {\rm{index-n}}\,({\it{y\/}}, {\it{x\/}})\index{index-n}) $\leq$ {\it{n\/}})) $\rightarrow$ {\rm{p-disjoint}}\,({\it{y\/}}, {\it{j\/}}, {\it{s\/}})\index{p-disjoint}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it p-disjoint\/}.
                 
\begin{tabbing}{\sc Conservative Axiom}:  fn*-correctness \\ \index{fn*-correctness}
\=\+{\rm{fn*-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{fn*-statep} \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\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-sp}}\,({\it{s\/}})\index{read-sp}, {\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{p-disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{s\/}})\index{p-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{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*})\-$\;${\bf  endlet}\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it fn*-statep\/}, {\it fn*-t\/}, and {\it fn*\/}.

\begin{verbatim};          Proof of the Correctness of a MAX Function        
#|
The following C function max computes the maximum of integers a and b, 
according to the comparison function comp.  Here, we study the problem
of function pointer.

max(int a, int b, int (*comp)(int, int))
{
  if ((*comp)(a, b) < 0)
    return b;
  else return a;    
}

The MC68020 assembly code of the C function max on SUN-3 is given as 
follows.  This binary is generated by "gcc -O".

0x2320 <max>:           linkw fp,#0
0x2324 <max+4>:         moveml d2-d3,sp@-
0x2328 <max+8>:         movel fp@(8),d3
0x232c <max+12>:        movel fp@(12),d2
0x2330 <max+16>:        movel d2,sp@-
0x2332 <max+18>:        movel d3,sp@-
0x2334 <max+20>:        moveal fp@(16),a0
0x2338 <max+24>:        jsr a0@
0x233a <max+26>:        tstl d0
0x233c <max+28>:        bge 0x2342 <max+34>
0x233e <max+30>:        movel d2,d0
0x2340 <max+32>:        bra 0x2344 <max+36>
0x2342 <max+34>:        movel d3,d0
0x2344 <max+36>:        moveml fp@(-8),d2-d3
0x234a <max+42>:        unlk fp
0x234c <max+44>:        rts

The machine code of the above program is:

<max>:      0x4e56  0x0000  0x48e7  0x3000  0x262e  0x0008  0x242e  0x000c
<max+16>:   0x2f02  0x2f03  0x206e  0x0010  0x4e90  0x4a80  0x6c04  0x2002
<max+32>:   0x6002  0x2003  0x4cee  0x000c  0xfff8  0x4e5e  0x4e75

'(78      86      0       0       72      231     48      0
  38      46      0       8       36      46      0       12
  47      2       47      3       32      110     0       16
  78      144     74      128     108     4       32      2
  96      2       32      3       76      238     0       12
  255     248     78      94      78      117)
|#

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{max-code} \\  
\=\+{\sc{max-code}}\index{max-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{38}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{3}} \\ 
{\tt{32}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{16}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{144}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{76}} \\ 
{\tt{238}}{\tt{ }}{\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{verbatim}; imax is the Nqthm counterpart of the program (max-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{max-fn*} \\  
\=\+{\rm{max-fn*}}\,({\it{a\/}}, {\it{b\/}})\index{max-fn*} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\rm{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*})$\;\;${\bf then }{\it{b\/}} \\ 
{\bf else }{\it{a\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the computation time of the program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{max-t0}$\;\;$
{\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0} $=$ {\tt{8}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{max-t} \\  
\=\+{\rm{max-t}}\,({\it{a\/}}, {\it{b\/}})\index{max-t} \\ 
$=$$\;\;\;\;${\rm{splus}}\,(\=\+{\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0}, \\ 
{\rm{splus}}\,(\=\+{\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t}, \\ 
\=\+{\bf if }{\rm{negativep}}\,({\rm{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*})$\;\;${\bf then }{\tt{7}} \\ 
{\bf else }{\tt{6}}$\;${\bf  endif}\-)\-\index{splus})\-\index{splus}\-
\end{tabbing}

\begin{verbatim}; the assumptions of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{max-sp} \\  
\=\+{\rm{max-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-sp} \\ 
$=$$\;\;\;\;$(\=\+({\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{46}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{max-code}}\index{max-code})\index{mcode-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$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{40}})\index{ram-addrp})\-\-
\end{tabbing}
  
\begin{tabbing}{\sc Conservative Axiom}:  max-state \\ \index{max-state}
\=\+({\rm{max-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-statep} $\rightarrow$ {\rm{fn*-statep}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0})\index{stepn}, {\it{a\/}}, {\it{b\/}})\index{fn*-statep}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{max-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-statep} \\ 
$\rightarrow$$\;\;\;\;${\rm{p-disjoint}}\,(\=\+{\rm{add}}\,({\tt{32}}, {\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{4294967272}})\index{add}, \\ 
{\tt{40}}, \\ 
{\rm{stepn}}\,({\it{s\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0})\index{stepn})\-\index{p-disjoint})\- \\ 
$\wedge$$\;\;\;\;$({\rm{max-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-statep} $=$ ({\rm{max-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-sp} $\wedge$ {\rm{comp-loadp}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{comp-loadp}))\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it max-statep\/} and {\it comp-loadp\/}.

\begin{verbatim}; an intermediate state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{max-s0p} \\  
\=\+{\rm{max-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{16}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem})\- \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{26}}, {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{46}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{26}}, {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{max-code}}\index{max-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{40}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\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} $=$ {\it{a\/}}) \\ 
$\wedge$$\;\;\;\;$({\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} $=$ {\it{b\/}}))\-\-
\end{tabbing}

\begin{verbatim}; an intermediate state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{max-s1p} \\  
\=\+{\rm{max-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\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{26}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{46}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{26}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{max-code}}\index{max-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{40}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{3}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $=$ {\rm{iread-dn}}\,({\tt{32}}, {\tt{2}}, {\it{s\/}})\index{iread-dn}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{iread-dn} $=$ {\rm{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  max-disjointness \\ \index{max-disjointness}
\=\+({\rm{max-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-statep} $\wedge$ {\rm{max-disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{s\/}})\index{max-disjoint}) \\ 
$\rightarrow$$\;\;\;\;${\rm{p-disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0})\index{stepn})\index{p-disjoint}\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it max-disjoint\/}.

\begin{verbatim}; from the initial state to s0.  s --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  max-s-s0 \\ \index{max-s-s0}
{\rm{max-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-sp} $\rightarrow$ {\rm{max-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0})\index{stepn}, {\it{a\/}}, {\it{b\/}})\index{max-s0p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  max-s-s0-else \\ \index{max-s-s0-else}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{max-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-sp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\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{movem-saved}}\,({\it{s0\/}}, {\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})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}
                     
\begin{tabbing}{\sc Theorem}:  max-s-s0-rfile \\ \index{max-s-s0-rfile}
\=\+({\rm{max-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-sp} $\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\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-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}:  max-s-s0-mem \\ \index{max-s-s0-mem}
\=\+({\rm{max-sp}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-sp} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\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\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-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.  s0 --> s1.  This is basically a fact about the
; subroutine comp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  max-s0-s1 \\ \index{max-s0-s1}
({\rm{max-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s0p} $\wedge$ {\rm{fn*-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{fn*-statep}) $\rightarrow$ {\rm{max-s1p}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\index{stepn}, {\it{a\/}}, {\it{b\/}})\index{max-s1p}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  max-s0-s1-else \\ \index{max-s0-s1-else}
\=\+(\=\+{\rm{max-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{fn*-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{fn*-statep} \\ 
$\wedge$$\;\;\;\;${\rm{p-disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{40}}, {\it{s\/}})\index{p-disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\index{stepn})\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}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\index{stepn})\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}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\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})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  max-s0-s1-rfile \\ \index{max-s0-s1-rfile}
\=\+({\rm{max-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s0p} $\wedge$ {\rm{fn*-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{fn*-statep} $\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{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\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}:  max-s0-s1-mem \\ \index{max-s0-s1-mem}
\=\+({\rm{max-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s0p} $\wedge$ {\rm{fn*-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{fn*-statep} $\wedge$ {\rm{p-disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{s\/}})\index{p-disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{fn*-t}}\,({\it{a\/}}, {\it{b\/}})\index{fn*-t})\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 exit.  s1 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  max-s1-sn-1 \\ \index{max-s1-sn-1}
\=\+({\rm{max-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s1p} $\wedge$ {\rm{negativep}}\,({\rm{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\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{7}})\index{stepn})\index{iread-dn} $=$ {\it{b\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{7}})\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{7}})\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{7}})\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{tabbing}{\sc Theorem}:  max-s1-sn-rfile-1 \\ \index{max-s1-sn-rfile-1}
\=\+(\=\+{\rm{max-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s1p} \\ 
$\wedge$$\;\;\;\;${\rm{negativep}}\,({\rm{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*}) \\ 
$\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\/}}, {\tt{7}})\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}:  max-s1-sn-2 \\ \index{max-s1-sn-2}
\=\+({\rm{max-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s1p} $\wedge$ ($\neg$ {\rm{negativep}}\,({\rm{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*}))) \\ 
$\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} $=$ {\it{a\/}}) \\ 
$\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{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{tabbing}{\sc Theorem}:  max-s1-sn-rfile-2 \\ \index{max-s1-sn-rfile-2}
\=\+(\=\+{\rm{max-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-s1p} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{negativep}}\,({\rm{fn*}}\,({\it{a\/}}, {\it{b\/}})\index{fn*})) \\ 
$\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\/}}, {\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{verbatim}; the correctness of max.
\end{verbatim}
\noindent{\sc Event}:   Disable max-t0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  max-correctness \\ \index{max-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{max-t}}\,({\it{a\/}}, {\it{b\/}})\index{max-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{max-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-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-sp}}\,({\it{s\/}})\index{read-sp}, {\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{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{40}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{max-disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\it{s\/}})\index{max-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{max-fn*}}\,({\it{a\/}}, {\it{b\/}})\index{max-fn*}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  disjoint-la4 \\ \index{disjoint-la4}
\=\+(\=\+{\rm{disjoint}}\,({\it{a\/}}, {\it{m\/}}, {\it{b\/}}, {\it{n\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$(({\it{j\/}} $+$ {\rm{index-n}}\,({\it{a1\/}}, {\it{a\/}})\index{index-n}) $\leq$ {\it{m\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{l\/}} $+$ {\rm{index-n}}\,({\it{b1\/}}, {\it{b\/}})\index{index-n}) $\leq$ {\it{n\/}}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{disjoint}}\,({\it{a1\/}}, {\it{j\/}}, {\it{b1\/}}, {\it{l\/}})\index{disjoint}\-
\end{tabbing}

\begin{verbatim}; instantiation.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{max-gt-statep} \\  
\=\+{\rm{max-gt-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-gt-statep} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{comp\/}}{\bf $\;$ be$\;\;$}{\rm{read-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{read-mem}\- \\ 
{\bf in} \\ 
\=\+({\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{46}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{max-code}}\index{max-code})\index{mcode-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$$\;\;\;\;${\rm{evenp}}\,({\it{comp\/}})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\it{comp\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\rm{len}}\,({\sc{gt-code}}\index{gt-code})\index{len})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\it{comp\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{gt-code}}\index{gt-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{28}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{44}})\index{ram-addrp}\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{max-gt-t} \\  
\=\+{\rm{max-gt-t}}\,({\it{a\/}}, {\it{b\/}})\index{max-gt-t} \\ 
$=$$\;\;\;\;${\rm{splus}}\,(\=\+{\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0}, \\ 
{\rm{splus}}\,(\=\+{\rm{gt-t}}\,({\it{a\/}}, {\it{b\/}})\index{gt-t}, \\ 
\=\+{\bf if }{\rm{negativep}}\,({\rm{gt}}\,({\it{a\/}}, {\it{b\/}})\index{gt})$\;\;${\bf then }{\tt{7}} \\ 
{\bf else }{\tt{6}}$\;${\bf  endif}\-)\-\index{splus})\-\index{splus}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{max-gt} \\  
\=\+{\rm{max-gt}}\,({\it{a\/}}, {\it{b\/}})\index{max-gt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\rm{gt}}\,({\it{a\/}}, {\it{b\/}})\index{gt})$\;\;${\bf then }{\it{b\/}} \\ 
{\bf else }{\it{a\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  max-gt-statep-s0 \\ \index{max-gt-statep-s0}
\=\+{\bf let }\=\+{\it{s0\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{max-t0}}\,({\it{a\/}}, {\it{b\/}})\index{max-t0})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{max-gt-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-gt-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s0\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{mc-pc}}\,({\it{s0\/}})\index{mc-pc} \\ 
$=$$\;\;\;\;${\rm{read-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{read-mem})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-mem}}\,(\=\+{\rm{add}}\,({\tt{32}}, {\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\tt{4}})\index{add}, \\ 
{\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, \\ 
{\tt{4}})\-\index{iread-mem} \\ 
$=$$\;\;\;\;${\it{a\/}})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-mem}}\,(\=\+{\rm{add}}\,({\tt{32}}, {\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s0\/}})\index{mc-rfile})\index{read-rn}, {\tt{8}})\index{add}, \\ 
{\rm{mc-mem}}\,({\it{s0\/}})\index{mc-mem}, \\ 
{\tt{4}})\-\index{iread-mem} \\ 
$=$$\;\;\;\;${\it{b\/}})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  max-gt-correctness \\ \index{max-gt-correctness}
\=\+{\rm{max-gt-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{b\/}})\index{max-gt-statep} \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{max-gt-t}}\,({\it{a\/}}, {\it{b\/}})\index{max-gt-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\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-sp}}\,({\it{s\/}})\index{read-sp}, {\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{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{40}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{28}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{4}})\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{max-gt}}\,({\it{a\/}}, {\it{b\/}})\index{max-gt})\-$\;${\bf  endlet}\-\-
\end{tabbing}

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