\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{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim};         Proof of the Corectness of a Majority Voting Program
;
#|
The following C function MJRTY determines if there is a candidate who
has received a majority of votes cast in an election.

/* a majority voting algorithm invented by Boyer and Moore */
#define YES 1
#define NO  0

struct winner {
  int x;
  int y;
};

struct winner mjrty (int a[], int n)
{
  int cand, i, k;
  struct winner temp;
  
  k = 0;
  for (i = 0; i < n; i++)
    if (k == 0) {
      cand = a[i];
      k = 1;
    }
  else {
    if (cand == a[i])
      k++;
    else 
      k--;
  };
  temp.x = cand;
  if (k == 0) {
    temp.y = NO;
    return temp;
  };
  if (k > n/2) {
    temp.y = YES;
    return temp;
  };
  k = 0;
  for (i = 0; i < n; i++)
    if (a[i] == cand)
      k++;
  if (k > n/2)
    temp.y = YES;
  else temp.y = NO;
  return temp;
}

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

0x2310 <mjrty>:         linkw a6,#0
0x2314 <mjrty+4>:       moveml d2-d5,sp@-
0x2318 <mjrty+8>:       moveal a6@(8),a0
0x231c <mjrty+12>:      movel a6@(12),d2
0x2320 <mjrty+16>:      clrl d1
0x2322 <mjrty+18>:      clrl d0
0x2324 <mjrty+20>:      cmpl d0,d2
0x2326 <mjrty+22>:      ble 0x2346 <mjrty+54>
0x2328 <mjrty+24>:      tstl d1
0x232a <mjrty+26>:      bne 0x2334 <mjrty+36>
0x232c <mjrty+28>:      movel 0(a0)[d0.l*4],d3
0x2330 <mjrty+32>:      movel #1,d1
0x2332 <mjrty+34>:      bra 0x2340 <mjrty+48>
0x2334 <mjrty+36>:      cmpl 0(a0)[d0.l*4],d3
0x2338 <mjrty+40>:      bne 0x233e <mjrty+46>
0x233a <mjrty+42>:      addql #1,d1
0x233c <mjrty+44>:      bra 0x2340 <mjrty+48>
0x233e <mjrty+46>:      subl #1,d1
0x2340 <mjrty+48>:      addql #1,d0
0x2342 <mjrty+50>:      cmpl d0,d2
0x2344 <mjrty+52>:      bgt 0x2328 <mjrty+24>
0x2346 <mjrty+54>:      movel d3,d4
0x2348 <mjrty+56>:      tstl d1
0x234a <mjrty+58>:      beq 0x2382 <mjrty+114>
0x234c <mjrty+60>:      movel d2,d0
0x234e <mjrty+62>:      bge 0x2352 <mjrty+66>
0x2350 <mjrty+64>:      addql #1,d0
0x2352 <mjrty+66>:      asrl #1,d0
0x2354 <mjrty+68>:      cmpl d1,d0
0x2356 <mjrty+70>:      bge 0x235c <mjrty+76>
0x2358 <mjrty+72>:      movel #1,d5
0x235a <mjrty+74>:      bra 0x2384 <mjrty+116>
0x235c <mjrty+76>:      clrl d1
0x235e <mjrty+78>:      clrl d0
0x2360 <mjrty+80>:      cmpl d0,d2
0x2362 <mjrty+82>:      ble 0x2372 <mjrty+98>
0x2364 <mjrty+84>:      cmpl 0(a0)[d0.l*4],d3
0x2368 <mjrty+88>:      bne 0x236c <mjrty+92>
0x236a <mjrty+90>:      addql #1,d1
0x236c <mjrty+92>:      addql #1,d0
0x236e <mjrty+94>:      cmpl d0,d2
0x2370 <mjrty+96>:      bgt 0x2364 <mjrty+84>
0x2372 <mjrty+98>:      movel d2,d0
0x2374 <mjrty+100>:     bge 0x2378 <mjrty+104>
0x2376 <mjrty+102>:     addql #1,d0
0x2378 <mjrty+104>:     asrl #1,d0
0x237a <mjrty+106>:     cmpl d1,d0
0x237c <mjrty+108>:     bge 0x2382 <mjrty+114>
0x237e <mjrty+110>:     movel #1,d5
0x2380 <mjrty+112>:     bra 0x2384 <mjrty+116>
0x2382 <mjrty+114>:     clrl d5
0x2384 <mjrty+116>:     movel d4,d0
0x2386 <mjrty+118>:     movel d5,d1
0x2388 <mjrty+120>:     moveml a6@(-16),d2-d5
0x238e <mjrty+126>:     unlk a6
0x2390 <mjrty+128>:     rts

The machine code of the above program is:


<mjrty>:      0x4e56  0x0000  0x48e7  0x3c00  0x206e  0x0008  0x242e  0x000c
<mjrty+16>:   0x4281  0x4280  0xb480  0x6f1e  0x4a81  0x6608  0x2630  0x0c00
<mjrty+32>:   0x7201  0x600c  0xb6b0  0x0c00  0x6604  0x5281  0x6002  0x5381
<mjrty+48>:   0x5280  0xb480  0x6ee2  0x2803  0x4a81  0x6736  0x2002  0x6c02
<mjrty+64>:   0x5280  0xe280  0xb081  0x6c04  0x7a01  0x6028  0x4281  0x4280
<mjrty+80>:   0xb480  0x6f0e  0xb6b0  0x0c00  0x6602  0x5281  0x5280  0xb480
<mjrty+96>:   0x6ef2  0x2002  0x6c02  0x5280  0xe280  0xb081  0x6c04  0x7a01
<mjrty+112>:  0x6002  0x4285  0x2004  0x2205  0x4cee  0x003c  0xfff0  0x4e5e
<mjrty+128>:  0x4e75

In the Nqthm logic, it is like:

'(78      86      0       0       72      231     60      0
  32      110     0       8       36      46      0       12
  66      129     66      128     180     128     111     30
  74      129     102     8       38      48      12      0
  114     1       96      12      182     176     12      0
  102     4       82      129     96      2       83      129
  82      128     180     128     110     226     40      3
  74      129     103     54      32      2       108     2
  82      128     226     128     176     129     108     4
  122     1       96      40      66      129     66      128
  180     128     111     14      182     176     12      0
  102     2       82      129     82      128     180     128
  110     242     32      2       108     2       82      128
  226     128     176     129     108     4       122     1
  96      2       66      133     32      4       34      5
  76      238     0       60      255     240     78      94
  78      117)
|#

; in the logic, the above program is defined by (mjrty-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-code} \\  
\=\+{\sc{mjrty-code}}\index{mjrty-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{72}}{\tt{ }}{\tt{231}}{\tt{ }}{\tt{60}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{36}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{129}} \\ 
{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{180}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{111}}{\tt{ }}{\tt{30}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{38}}{\tt{ }}{\tt{48}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{114}}{\tt{ }}{\tt{1}} \\ 
{\tt{96}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{182}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{83}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}} \\ 
{\tt{180}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{226}}{\tt{ }}{\tt{40}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{103}}{\tt{ }}{\tt{54}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}} \\ 
{\tt{226}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{122}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{40}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{180}} \\ 
{\tt{128}}{\tt{ }}{\tt{111}}{\tt{ }}{\tt{14}}{\tt{ }}{\tt{182}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{102}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{180}}{\tt{ }}{\tt{128}} \\ 
{\tt{110}}{\tt{ }}{\tt{242}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{226}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{129}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{122}} \\ 
{\tt{1}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{2}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{133}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{5}}{\tt{ }}{\tt{76}}{\tt{ }}{\tt{238}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{60}}{\tt{ }}{\tt{255}}{\tt{ }}{\tt{240}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}} \\ 
{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{verbatim}; mjrty-cand is a function in the logic to simulate the candidate
; findhe above code.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-cand} \\  
\=\+{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, $1\;+$ {\it{i\/}}, {\tt{1}})\index{mjrty-cand} \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{mjrty-cand} \\ 
{\bf else }{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}} $-\;1$)\index{mjrty-cand}$\;${\bf  endif}\- \\ 
{\bf else }{\it{cand\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mjrty-k} \\  
\=\+{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}, $1\;+$ {\it{i\/}}, {\tt{1}})\index{mjrty-k} \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{mjrty-k} \\ 
{\bf else }{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}} $-\;1$)\index{mjrty-k}$\;${\bf  endif}\- \\ 
{\bf else }{\it{k\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; cand-cnt is a function in the logic to simulate the process of 
; counting the number of votes for the given candidate.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cand-cnt} \\  
\=\+{\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{cand-cnt} \\ 
{\bf else }{\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}})\index{cand-cnt}$\;${\bf  endif}\- \\ 
{\bf else }{\it{k\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; mjrty-p determines if the given candidate cand has received a majority
; voting.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-p} \\  
\=\+{\rm{mjrty-p}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-p} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }({\it{n\/}} $\div$ {\tt{2}}) $<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+({\it{n\/}} $\div$ {\tt{2}}) \\ 
$<$$\;\;\;\;${\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the computation time.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-cand-t} \\  
\=\+{\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf let }\=\+{\it{cand1\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
{\rm{splus}}\,({\tt{8}}, {\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand1\/}}, $1\;+$ {\it{i\/}}, {\tt{1}})\index{mjrty-cand-t})\index{splus}$\;${\bf  endlet}\- \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\rm{splus}}\,({\tt{9}}, {\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{mjrty-cand-t})\index{splus} \\ 
{\bf else }{\rm{splus}}\,({\tt{8}}, {\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}} $-\;1$)\index{mjrty-cand-t})\index{splus}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\tt{18}} \\ 
{\bf else }{\tt{17}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mjrty-sn-t} \\  
\=\+{\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-sn-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf let }\=\+{\it{cand1\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
{\rm{splus}}\,({\tt{8}}, {\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand1\/}}, $1\;+$ {\it{i\/}}, {\tt{1}})\index{mjrty-sn-t})\index{splus}$\;${\bf  endlet}\- \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\rm{splus}}\,({\tt{9}}, {\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{mjrty-sn-t})\index{splus} \\ 
{\bf else }{\rm{splus}}\,({\tt{8}}, {\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}} $-\;1$)\index{mjrty-sn-t})\index{splus}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{11}} \\ 
{\bf else }{\tt{17}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{cand-cnt-t} \\  
\=\+{\rm{cand-cnt-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\rm{splus}}\,({\tt{6}}, {\rm{cand-cnt-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{cand-cnt-t})\index{splus} \\ 
{\bf else }{\rm{splus}}\,({\tt{5}}, {\rm{cand-cnt-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}})\index{cand-cnt-t})\index{splus}$\;${\bf  endif}\- \\ 
{\bf elseif }({\it{n\/}} $\div$ {\tt{2}}) $<$ {\it{k\/}}$\;\;${\bf then }{\tt{14}} \\ 
{\bf else }{\tt{13}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mjrty-t} \\  
\=\+{\rm{mjrty-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-t} \\ 
$=$$\;\;\;\;$\=\+{\bf let }\=\+{\it{cand\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
{\rm{splus}}\,(\=\+{\tt{14}}, \\ 
\=\+{\bf if }\=\+({\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{1}})\index{mjrty-k} $\simeq {\tt{0}}$) \\ 
$\vee$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{1}})\index{mjrty-k})\- \\ 
{\bf then }{\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{1}})\index{mjrty-sn-t} \\ 
{\bf else }{\rm{splus}}\,(\=\+{\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{1}})\index{mjrty-cand-t}, \\ 
\=\+{\bf if }{\it{cand\/}} $=$ {\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{1}})\index{mjrty-cand} \\ 
{\bf then }{\rm{cand-cnt-t}}\,(\=\+{\it{a\/}}, \\ 
{\it{n\/}}, \\ 
{\it{lst\/}}, \\ 
{\rm{mjrty-cand}}\,(\=\+{\it{n\/}}, \\ 
{\it{lst\/}}, \\ 
{\it{cand\/}}, \\ 
{\tt{1}}, \\ 
{\tt{1}})\-\index{mjrty-cand}, \\ 
{\tt{1}}, \\ 
{\tt{1}})\-\index{cand-cnt-t} \\ 
{\bf else }{\rm{cand-cnt-t}}\,(\=\+{\it{a\/}}, \\ 
{\it{n\/}}, \\ 
{\it{lst\/}}, \\ 
{\rm{mjrty-cand}}\,(\=\+{\it{n\/}}, \\ 
{\it{lst\/}}, \\ 
{\it{cand\/}}, \\ 
{\tt{1}}, \\ 
{\tt{1}})\-\index{mjrty-cand}, \\ 
{\tt{1}}, \\ 
{\tt{0}})\-\index{cand-cnt-t}$\;${\bf  endif}\-)\-\index{splus}$\;${\bf  endif}\-)\-\index{splus}$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{verbatim}; induction hints.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-cand-induct} \\  
\=\+{\rm{mjrty-cand-induct}}\,({\it{s\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf let }\=\+{\it{cand1\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
{\rm{mjrty-cand-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\it{n\/}}, {\it{lst\/}}, {\it{cand1\/}}, $1\;+$ {\it{i\/}}, {\tt{1}})\index{mjrty-cand-induct}$\;${\bf  endlet}\- \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\rm{mjrty-cand-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{mjrty-cand-induct} \\ 
{\bf else }{\rm{mjrty-cand-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}} $-\;1$)\index{mjrty-cand-induct}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{cand-cnt-induct} \\  
\=\+{\rm{cand-cnt-induct}}\,({\it{s\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}} \\ 
{\bf then }\=\+{\bf if }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\rm{cand-cnt-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{cand-cnt-induct} \\ 
{\bf else }{\rm{cand-cnt-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}})\index{cand-cnt-induct}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the preconditions of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-statep} \\  
\=\+{\rm{mjrty-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-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{130}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{mjrty-code}}\index{mjrty-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{32}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{32}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-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{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\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{n\/}} $\not\simeq {\tt{0}}$))\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state s0.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-s0p} \\  
\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-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{50}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{130}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{50}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{mjrty-code}}\index{mjrty-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{32}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{32}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-rn}}\,({\tt{32}}, {\tt{8}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{3}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{0}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{1}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\leq$ {\it{i\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state s1.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{mjrty-s1p} \\  
\=\+{\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-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{94}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{130}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{94}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{mjrty-code}}\index{mjrty-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{32}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{16}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{32}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-rn}}\,({\tt{32}}, {\tt{8}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{2}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{4}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{3}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{0}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-rn}}\,({\tt{32}}, {\tt{1}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\leq$ {\it{i\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the initial segment.  From the initial state to s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-s-s0 \\ \index{mjrty-s-s0}
\=\+{\bf let }\=\+{\it{cand\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
\=\+{\rm{mjrty-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{1}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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{14}})\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{14}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{readm-rn}}\,({\tt{32}}, {\tt{'}}{\tt{(}}{\tt{2}}{\tt{ }}{\tt{3}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{5}}{\tt{)}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{readm-rn})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s-s0-rfile \\ \index{mjrty-s-s0-rfile}
\=\+({\rm{mjrty-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-statep} $\wedge$ {\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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}:  mjrty-s-s0-mem \\ \index{mjrty-s-s0-mem}
\=\+({\rm{mjrty-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-statep} $\wedge$ {\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{32}}, {\it{x\/}}, {\it{k\/}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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}; s0 --> exit.
; base case.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-s0-sn-base-1 \\ \index{mjrty-s0-sn-base-1}
\=\+({\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} $\wedge$ ({\it{i\/}} $\not<$ {\it{n\/}}) $\wedge$ ({\it{k\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\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{11}})\index{stepn})\index{iread-dn} $=$ {\it{cand\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\index{stepn})\index{iread-dn} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{11}})\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{11}})\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{11}})\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}:  mjrty-s0-sn-base-2 \\ \index{mjrty-s0-sn-base-2}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\it{k\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\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{17}})\index{stepn})\index{iread-dn} $=$ {\it{cand\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\index{stepn})\index{iread-dn} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\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{17}})\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{17}})\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}:  mjrty-s0-sn-rfile-base-1 \\ \index{mjrty-s0-sn-rfile-base-1}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\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{11}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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{ }}{\tt{4}}{\tt{ }}{\tt{5}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s0-sn-rfile-base-2 \\ \index{mjrty-s0-sn-rfile-base-2}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\it{k\/}}) \\ 
$\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{17}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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{ }}{\tt{4}}{\tt{ }}{\tt{5}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; induction case.             
\end{verbatim}\begin{tabbing}{\sc Theorem}:  add1-int-rangep \\ \index{add1-int-rangep}
({\it{x\/}} $<$ {\rm{nat-to-int}}\,({\it{y\/}}, {\it{n\/}})\index{nat-to-int}) $\rightarrow$ {\rm{int-rangep}}\,($1\;+$ {\it{x\/}}, {\it{n\/}})\index{int-rangep}
\end{tabbing}


\noindent{\sc Event}:   Enable iplus.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mjrty-s0-s0-1 \\ \index{mjrty-s0-s0-1}
\=\+{\bf let }\=\+{\it{cand1\/}}{\bf $\;$ be$\;\;$}{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}\- \\ 
{\bf in} \\ 
\=\+({\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{k\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand1\/}}, $1\;+$ {\it{i\/}}, {\tt{1}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} \\ 
$=$$\;\;\;\;${\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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})\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  add1-int-rangepxx \\ \index{add1-int-rangepxx}
(({\it{i\/}} $\leq$ {\it{r\/}}) $\wedge$ ({\it{r\/}} $<$ {\it{n\/}}) $\wedge$ {\rm{int-rangep}}\,({\it{n\/}}, {\tt{32}})\index{int-rangep}) $\rightarrow$ {\rm{int-rangep}}\,($1\;+$ {\it{i\/}}, {\tt{32}})\index{int-rangep}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s0-s0-2 \\ \index{mjrty-s0-s0-2}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{mjrty-s0p} \\ 
$\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{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\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{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{9}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\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}:  mjrty-s0-s0-3 \\ \index{mjrty-s0-s0-3}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $\not=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}} $-\;1$)\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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}:  mjrty-s0-s0-rfile-1 \\ \index{mjrty-s0-s0-rfile-1}
\=\+({\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{k\/}} $\simeq {\tt{0}}$) $\wedge$ {\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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}:  mjrty-s0-s0-rfile-2 \\ \index{mjrty-s0-s0-rfile-2}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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}:  mjrty-s0-s0-rfile-3 \\ \index{mjrty-s0-s0-rfile-3}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $\not=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\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}; the proof of s0 --> exit.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-s0-sn \\ \index{mjrty-s0-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-sn-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k} $\simeq {\tt{0}}$) \\ 
$\vee$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k}))\-)\- \\ 
$\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{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\it{sn\/}})\index{iread-dn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $\div$ {\tt{2}}) $<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k} \\ 
{\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\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{l\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s0-sn-rfile \\ \index{mjrty-s0-sn-rfile}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-sn-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k} $\simeq {\tt{0}}$) \\ 
$\vee$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k}))\- \\ 
$\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} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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{ }}{\tt{4}}{\tt{ }}{\tt{5}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; s0 --> s1.
; base case:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-s0-s1-base1 \\ \index{mjrty-s0-s1-base1}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s1p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{1}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\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{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\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}:  mjrty-s0-s1-base2 \\ \index{mjrty-s0-s1-base2}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $\not=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s1p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\tt{0}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\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{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\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}:  mjrty-s0-s1-rfile-base1 \\ \index{mjrty-s0-s1-rfile-base1}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{18}})\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}:  mjrty-s0-s1-rfile-base2 \\ \index{mjrty-s0-s1-rfile-base2}
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{k\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\it{k\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $\not=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{17}})\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}; the proof of s0 --> s1.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-s0-s1 \\ \index{mjrty-s0-s1}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k}) \\ 
$\wedge$$\;\;\;\;$({\it{cand0\/}} $=$ {\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand}) \\ 
$\wedge$$\;\;\;\;$({\it{k0\/}} $=$ \=\+{\bf if }{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s1p}}\,({\it{s1\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand0\/}}, {\tt{1}}, {\it{k0\/}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\it{s1\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s1\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\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{movem-saved}}\,({\it{s1\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s1\/}})\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}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s0-s1-rfile \\ \index{mjrty-s0-s1-rfile}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{mjrty-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s0p} \\ 
$\wedge$$\;\;\;\;$({\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-k}) \\ 
$\wedge$$\;\;\;\;${\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; s1 --> exit.
; base case.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-s1-sn-1 \\ \index{mjrty-s1-sn-1}
\=\+({\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} $\wedge$ ({\it{i\/}} $\not<$ {\it{n\/}}) $\wedge$ (({\it{n\/}} $\div$ {\tt{2}}) $<$ {\it{k\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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{14}})\index{stepn})\index{iread-dn} $=$ {\it{cand\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\index{stepn})\index{iread-dn} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{14}})\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{14}})\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{14}})\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}:  mjrty-s1-sn-rfile-1 \\ \index{mjrty-s1-sn-rfile-1}
\=\+(\=\+{\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\it{k\/}}) \\ 
$\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{14}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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{ }}{\tt{4}}{\tt{ }}{\tt{5}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s1-sn-2 \\ \index{mjrty-s1-sn-2}
\=\+({\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} $\wedge$ ({\it{i\/}} $\not<$ {\it{n\/}}) $\wedge$ (({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\it{k\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\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{13}})\index{stepn})\index{iread-dn} $=$ {\it{cand\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\index{stepn})\index{iread-dn} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{13}})\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{13}})\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{13}})\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}:  mjrty-s1-sn-rfile-2 \\ \index{mjrty-s1-sn-rfile-2}
\=\+(\=\+{\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\it{k\/}}) \\ 
$\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{13}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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{ }}{\tt{4}}{\tt{ }}{\tt{5}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{verbatim}; induction case.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-s1-s1-1 \\ \index{mjrty-s1-s1-1}
\=\+({\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s1p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, $1\;+$ {\it{k\/}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\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{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\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}:  mjrty-s1-s1-2 \\ \index{mjrty-s1-s1-2}
\=\+({\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} $\wedge$ ({\it{i\/}} $<$ {\it{n\/}}) $\wedge$ ({\it{cand\/}} $\not=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-s1p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, $1\;+$ {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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{movem-saved}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved} $=$ {\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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}:  mjrty-s1-s1-rfile-1 \\ \index{mjrty-s1-s1-rfile-1}
\=\+(\=\+{\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s1-s1-rfile-2 \\ \index{mjrty-s1-s1-rfile-2}
\=\+(\=\+{\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{cand\/}} $\not=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}) \\ 
$\wedge$$\;\;\;\;${\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-7a2-5p})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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}:  mjrty-s1-sn \\ \index{mjrty-s1-sn}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{cand-cnt-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} \\ 
$\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} $=$ {\it{cand\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\it{sn\/}})\index{iread-dn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $\div$ {\tt{2}}) $<$ {\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt} \\ 
{\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\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{l\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{l\/}})\index{read-mem}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-s1-sn-rfile \\ \index{mjrty-s1-sn-rfile}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{cand-cnt-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+({\rm{mjrty-s1p}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-s1p} $\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} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{d6-7a2-5p}}\,({\it{rn\/}})\index{d6-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{ }}{\tt{4}}{\tt{ }}{\tt{5}}{\tt{)}}, \\ 
{\rm{movem-saved}}\,({\it{s\/}}, {\tt{4}}, {\tt{16}}, {\tt{4}})\index{movem-saved})\-\index{get-vlst}$\;${\bf  endif}\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; the correctness of MJRTY.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-statep-info \\ \index{mjrty-statep-info}
{\rm{mjrty-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-statep} $\rightarrow$ ({\it{n\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-correctness \\ \index{mjrty-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{mjrty-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{mjrty-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-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} $\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}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{32}}, {\it{x\/}}, {\it{k\/}})\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{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iread-dn}}\,({\tt{32}}, {\tt{1}}, {\it{sn\/}})\index{iread-dn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{mjrty-p}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-p}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-)\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; in the logic, mjrty is expected to have these properties:
;    1.  mjrty-thm-1: if mjrty-p returns 1,  cand wins the majority.
;    2.  mjrty-thm-2: if mjrty-p returns 0,  no one wins the majority.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-cand-0 \\ \index{mjrty-cand-0}
{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{n\/}}, {\it{k\/}})\index{mjrty-cand} $=$ {\it{x\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-cand-1 \\ \index{mjrty-cand-1}
\=\+{\rm{mjrty-cand}}\,($1\;+$ {\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{n\/}}, {\it{k\/}})\index{mjrty-cand} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{get-nth}}\,({\it{n\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-k-0 \\ \index{mjrty-k-0}
{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{n\/}}, {\it{k\/}})\index{mjrty-k} $=$ {\it{k\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-k-1 \\ \index{mjrty-k-1}
\=\+{\rm{mjrty-k}}\,($1\;+$ {\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{n\/}}, {\it{k\/}})\index{mjrty-k} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\rm{get-nth}}\,({\it{n\/}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }$1\;+$ {\it{k\/}} \\ 
{\bf else }{\it{k\/}} $-\;1$$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cand-cnt-0 \\ \index{cand-cnt-0}
{\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{n\/}}, {\it{k\/}})\index{cand-cnt} $=$ {\it{k\/}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cand-cnt-1 \\ \index{cand-cnt-1}
\=\+{\rm{cand-cnt}}\,($1\;+$ {\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{n\/}}, {\it{k\/}})\index{cand-cnt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\rm{get-nth}}\,({\it{n\/}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }$1\;+$ {\it{k\/}} \\ 
{\bf else }{\it{k\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-k-lemma \\ \index{mjrty-k-lemma}
\=\+(({\it{i\/}} $\leq$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{mjrty-cand}}\,({\it{i\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{mjrty-cand}, {\it{i\/}}, {\rm{mjrty-k}}\,({\it{i\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{mjrty-k})\index{mjrty-k} \\ 
$=$$\;\;\;\;${\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{mjrty-k})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-cand-lemma \\ \index{mjrty-cand-lemma}
\=\+(({\it{i\/}} $\leq$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{mjrty-cand}}\,({\it{i\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{mjrty-cand}, {\it{i\/}}, {\rm{mjrty-k}}\,({\it{i\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{mjrty-k})\index{mjrty-cand} \\ 
$=$$\;\;\;\;${\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{mjrty-cand})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cand-cnt-lemma \\ \index{cand-cnt-lemma}
\=\+(({\it{i\/}} $\leq$ {\it{n\/}}) $\wedge$ ({\it{j\/}} $\leq$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{i\/}}, {\rm{cand-cnt}}\,({\it{i\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{cand-cnt})\index{cand-cnt} $=$ {\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{j\/}}, {\it{k\/}})\index{cand-cnt})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-cand-rec \\ \index{mjrty-cand-rec}
\=\+({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-cand}}\,($1\;+$ {\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand} \\ 
$=$$\;\;\;\;${\rm{mjrty-cand}}\,(\=\+$1\;+$ {\it{n\/}}, \\ 
{\it{lst\/}}, \\ 
{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand}, \\ 
{\it{n\/}}, \\ 
{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{mjrty-k})\-\index{mjrty-cand})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-k-rec \\ \index{mjrty-k-rec}
\=\+({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{mjrty-k}}\,($1\;+$ {\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{mjrty-k} \\ 
$=$$\;\;\;\;${\rm{mjrty-k}}\,(\=\+$1\;+$ {\it{n\/}}, \\ 
{\it{lst\/}}, \\ 
{\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand}, \\ 
{\it{n\/}}, \\ 
{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{mjrty-k})\-\index{mjrty-k})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cand-cnt-rec \\ \index{cand-cnt-rec}
\=\+({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{cand-cnt}}\,($1\;+$ {\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{cand-cnt} \\ 
$=$$\;\;\;\;${\rm{cand-cnt}}\,($1\;+$ {\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\it{n\/}}, {\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{cand-cnt})\index{cand-cnt})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable mjrty-cand-lemma.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mjrty-k-lemma.

\addvspace{18pt}

\noindent{\sc Event}:   Disable cand-cnt-lemma.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mjrty-lemma1 \\ \index{mjrty-lemma1}
{\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand}, {\tt{0}}, {\tt{0}})\index{cand-cnt} $\not<$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-k}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mjrty-lemma2-induct} \\  
\=\+{\rm{mjrty-lemma2-induct}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}})\index{mjrty-lemma2-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{mjrty-lemma2-induct}}\,({\it{n\/}} $-\;1$, {\it{lst\/}}, {\it{x\/}})\index{mjrty-lemma2-induct} \\ 
$\wedge$$\;\;\;\;${\rm{mjrty-lemma2-induct}}\,({\it{n\/}} $-\;1$, {\it{lst\/}}, {\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{mjrty-lemma2-induct}\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-lemma2 \\ \index{mjrty-lemma2}
\=\+(\=\+({\it{n\/}} $+$ {\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-k}) \\ 
$\not<$$\;\;\;\;$({\tt{2}} $*$ {\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand}, {\tt{0}}, {\tt{0}})\index{cand-cnt}))\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\it{x\/}} $\not=$ {\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand}) \\ 
$\rightarrow$$\;\;\;\;$({\it{n\/}} $\not<$ (\=\+{\rm{mjrty-k}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-k} \\ 
$+$$\;\;\;\;$({\tt{2}} $*$ {\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{cand-cnt}))\-))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable mjrty-cand-rec.

\addvspace{18pt}

\noindent{\sc Event}:   Disable mjrty-k-rec.

\addvspace{18pt}

\noindent{\sc Event}:   Disable cand-cnt-rec.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  mjrty-thm1 \\ \index{mjrty-thm1}
\=\+{\rm{mjrty-p}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-p} \\ 
$\rightarrow$$\;\;\;\;$(({\it{n\/}} $\div$ {\tt{2}}) $<$ {\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\rm{mjrty-cand}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-cand}, {\tt{0}}, {\tt{0}})\index{cand-cnt})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-thm2 \\ \index{mjrty-thm2}
($\neg$ {\rm{mjrty-p}}\,({\it{n\/}}, {\it{lst\/}}, {\tt{0}}, {\tt{0}}, {\tt{0}})\index{mjrty-p}) $\rightarrow$ (({\it{n\/}} $\div$ {\tt{2}}) $\not<$ {\rm{cand-cnt}}\,({\it{n\/}}, {\it{lst\/}}, {\it{x\/}}, {\tt{0}}, {\tt{0}})\index{cand-cnt})
\end{tabbing}

\begin{verbatim}; a simple time analysis.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  mjrty-t-crock \\ \index{mjrty-t-crock}
({\it{z\/}} $*$ (({\it{x\/}} $-\;1$) $-$ {\it{y\/}})) $=$ (({\it{z\/}} $*$ ({\it{x\/}} $-$ {\it{y\/}})) $-$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-cand-t-0 \\ \index{mjrty-cand-t-0}
\=\+(\=\+{\rm{mjrty-cand-t}}\,({\it{a\/}}, {\tt{0}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\tt{18}} \\ 
{\bf else }{\tt{17}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{mjrty-cand-t}}\,({\it{a\/}}, {\tt{1}}, {\it{lst\/}}, {\it{cand\/}}, {\tt{1}}, {\it{k\/}})\index{mjrty-cand-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\tt{18}} \\ 
{\bf else }{\tt{17}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-cand-t-1 \\ \index{mjrty-cand-t-1}
\=\+{\rm{mjrty-cand-t}}\,({\it{a\/}}, {\tt{1}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{26}} \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth} \\ 
{\bf then }\=\+{\bf if }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\tt{27}} \\ 
{\bf else }{\tt{26}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\tt{26}} \\ 
{\bf else }{\tt{25}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\tt{0}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\tt{18}} \\ 
{\bf else }{\tt{17}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-cand-t-ubound \\ \index{mjrty-cand-t-ubound}
({\tt{18}} $+$ ({\tt{9}} $*$ ({\it{n\/}} $-$ {\it{i\/}}))) $\not<$ {\rm{mjrty-cand-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-cand-t}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-sn-t-ubound \\ \index{mjrty-sn-t-ubound}
({\tt{17}} $+$ ({\tt{9}} $*$ ({\it{n\/}} $-$ {\it{i\/}}))) $\not<$ {\rm{mjrty-sn-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{mjrty-sn-t}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cand-cnt-t-0 \\ \index{cand-cnt-t-0}
\=\+(\=\+{\rm{cand-cnt-t}}\,({\it{a\/}}, {\tt{0}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\tt{0}} $<$ {\it{k\/}}$\;\;${\bf then }{\tt{14}} \\ 
{\bf else }{\tt{13}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cand-cnt-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{n\/}}, {\it{k\/}})\index{cand-cnt-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $\div$ {\tt{2}}) $<$ {\it{k\/}}$\;\;${\bf then }{\tt{14}} \\ 
{\bf else }{\tt{13}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cand-cnt-t-1 \\ \index{cand-cnt-t-1}
\=\+{\rm{cand-cnt-t}}\,({\it{a\/}}, {\tt{1}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\it{cand\/}} $=$ {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}$\;\;${\bf then }{\tt{20}} \\ 
{\bf elseif }{\tt{0}} $<$ {\it{k\/}}$\;\;${\bf then }{\tt{19}} \\ 
{\bf else }{\tt{18}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\tt{0}} $<$ {\it{k\/}}$\;\;${\bf then }{\tt{14}} \\ 
{\bf else }{\tt{13}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cand-cnt-t-ubound \\ \index{cand-cnt-t-ubound}
({\tt{14}} $+$ ({\tt{6}} $*$ ({\it{n\/}} $-$ {\it{i\/}}))) $\not<$ {\rm{cand-cnt-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{cand\/}}, {\it{i\/}}, {\it{k\/}})\index{cand-cnt-t}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  mjrty-t-ubound \\ \index{mjrty-t-ubound}
{\rm{mjrty-t}}\,({\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{mjrty-t} $\leq$ ({\tt{46}} $+$ ({\tt{15}} $*$ ({\it{n\/}} $-\;1$)))
\end{tabbing}

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