
% The following substitutions are from the file:
%   /usr/local/pvs-2.4/pvs-tex.sub
\def\setsotherremovetwofn#1#2{{(#2 \setminus \{#1\})}}% How to print function sets.remove with arity (2)
\def\setsotheraddtwofn#1#2{{(#2 \cup \{#1\})}}% How to print function sets.add with arity (2)
\def\setsotherdifferencetwofn#1#2{{(#1 \setminus #2)}}% How to print function sets.difference with arity (2)
\def\setsothercomplementonefn#1{{\overline{#1}}}% How to print function sets.complement with arity (1)
\def\setsotherintersectiontwofn#1#2{{(#1 \cap #2)}}% How to print function sets.intersection with arity (2)
\def\setsotheruniontwofn#1#2{{(#1 \cup #2)}}% How to print function sets.union with arity (2)
\def\setsotherstrictunderscoresubsetothertwofn#1#2{{(#1 \subset #2)}}% How to print function sets.strict_subset? with arity (2)
\def\setsothersubsetothertwofn#1#2{{(#1 \subseteq #2)}}% How to print function sets.subset? with arity (2)
\def\setsothermembertwofn#1#2{{(#1 \in #2)}}% How to print function sets.member with arity (2)
\def\opohtwofn#1#2{{#1\circ#2}}% How to print function O with arity (2)
\def\opdividetwofn#1#2{{#1/#2}}% How to print function / with arity (2)
\def\optimestwofn#1#2{{#1\times#2}}% How to print function * with arity (2)
\def\opdifferenceonefn#1{{-#1}}% How to print function - with arity (1)
\def\opdifferencetwofn#1#2{{#1-#2}}% How to print function - with arity (2)
\def\opplustwofn#1#2{{#1+#2}}% How to print function + with arity (2)
Verbose proof for {\tt STABLE}.


{\tt STABLE:}

\vspace*{0.1in}\hspace*{0.2in}
\begin{tabular}{|cl}
\strut\\\hline
$\{\mbox{\rm 1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\(\forall\) (\(i\): \pvsid{nat}, \(n\): \pvsid{nat}): \pvsid{st}(\(i\), \(v\)) \(\geq\) \(n\) \(\supset\) \pvsid{st}(\(\opplustwofn{i}{1}\), \(v\)) \(\geq\) \(n\)\end{alltt}}\end{minipage}\\
\end{tabular}

\vspace{0.1in}

Skolemizing,

{\tt STABLE:}

\vspace*{0.1in}\hspace*{0.2in}
\begin{tabular}{|cl}
\strut\\\hline
$\{\mbox{\rm 1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(i'\), \(v\)) \(\geq\) \(n'\) \(\supset\) \pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\
\end{tabular}

\vspace{0.1in}

Applying disjunctive simplification to flatten sequent,

{\tt STABLE:}

\vspace*{0.1in}\hspace*{0.2in}
\begin{tabular}{|cl}
$\{\mbox{\rm -1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(i'\), \(v\)) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\\hline
$\{\mbox{\rm 1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\
\end{tabular}

\vspace{0.1in}

Using \(n\sb{0}\) to name and replace \pvsid{st}(\(i'\), \(v\)),

{\tt STABLE:}

\vspace*{0.1in}\hspace*{0.2in}
\begin{tabular}{|cl}
$\{\mbox{\rm -1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(i'\), \(v\)) \(=\) \(n\sb{0}\)\end{alltt}}\end{minipage}\\$\{\mbox{\rm -2}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\(n\sb{0}\) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\\hline
$\{\mbox{\rm 1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\
\end{tabular}

\vspace{0.1in}

Forward chaining on NEXT,

 we get 2 subgoals:

{\tt STABLE.1:}

\vspace*{0.1in}\hspace*{0.2in}
\begin{tabular}{|cl}
$\{\mbox{\rm -1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)) \(=\) \(n\sb{0}\)\end{alltt}}\end{minipage}\\$\{\mbox{\rm -2}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(i'\), \(v\)) \(=\) \(n\sb{0}\)\end{alltt}}\end{minipage}\\$\{\mbox{\rm -3}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\(n\sb{0}\) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\\hline
$\{\mbox{\rm 1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\
\end{tabular}

\vspace{0.1in}

Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of {\tt STABLE.1}.

{\tt STABLE.2:}

\vspace*{0.1in}\hspace*{0.2in}
\begin{tabular}{|cl}
$\{\mbox{\rm -1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)) \(>\) \(n\sb{0}\)\end{alltt}}\end{minipage}\\$\{\mbox{\rm -2}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\(S\)(\pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)))\end{alltt}}\end{minipage}\\$\{\mbox{\rm -3}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(i'\), \(v\)) \(=\) \(n\sb{0}\)\end{alltt}}\end{minipage}\\$\{\mbox{\rm -4}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\(n\sb{0}\) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\\hline
$\{\mbox{\rm 1}\}$ &\begin{minipage}[t]{5.5in}{\begin{alltt}\pvsid{st}(\(\opplustwofn{i'}{1}\), \(v\)) \(\geq\) \(n'\)\end{alltt}}\end{minipage}\\
\end{tabular}

\vspace{0.1in}

Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of {\tt STABLE.2}.


Q.E.D.

