PartialRefDefault.tex

% The following substitutions are from the file:
%   /home/augusto/Desktop/PVS/pvs-tex.sub
\def\munderscoretimestwofn#1#2{{#1 \times #2}}% How to print function m_times with arity (2)
\def\fmunderscoretimestwofn#1#2{{#1 \times #2}}% How to print function fm_times with arity (2)
\def\sigmaunderscoretimestwofn#1#2{{#1 \times #2}}% How to print function sigma_times with arity (2)
\def\generatedunderscoresubsetunderscorealgebraonefn#1{{{\cal A}(#1)}}% How to print function generated_subset_algebra with arity (1)
\def\generatedunderscoresigmaunderscorealgebraonefn#1{{{\cal S}(#1)}}% How to print function generated_sigma_algebra with arity (1)
\def\aeunderscoredecreasingotheronefn#1{{\pvsid{decreasing?}(#1)~\mbox{\it a.e.}}}% How to print function ae_decreasing? with arity (1)
\def\aeunderscoreincreasingotheronefn#1{{\pvsid{increasing?}(#1)~\mbox{\it a.e.}}}% How to print function ae_increasing? with arity (1)
\def\aeunderscoreconvergenceothertwofn#1#2{{#1 \longrightarrow #2~\mbox{\it a.e.}}}% How to print function ae_convergence? with arity (2)
\def\aeunderscoreeqothertwofn#1#2{{#1 = #2~\mbox{\it a.e.}}}% How to print function ae_eq? with arity (2)
\def\aeunderscoreleothertwofn#1#2{{#1 \leq #2~\mbox{\it a.e.}}}% How to print function ae_le? with arity (2)
\def\aeunderscoreposotheronefn#1{{#1> 0~\mbox{\it a.e.}}}% How to print function ae_pos? with arity (1)
\def\aeunderscorenonnegotheronefn#1{{#1 \geq 0~\mbox{\it a.e.}}}% How to print function ae_nonneg? with arity (1)
\def\aeunderscorezerootheronefn#1{{#1 = 0~\mbox{\it a.e.}}}% How to print function ae_0? with arity (1)
\def\xunderscorelttwofn#1#2{{#1 < #2}}% How to print function x_lt with arity (2)
\def\xunderscoreletwofn#1#2{{#1 \leq #2}}% How to print function x_le with arity (2)
\def\xunderscoreeqtwofn#1#2{{#1 = #2}}% How to print function x_eq with arity (2)
\def\xunderscoretimestwofn#1#2{{#1 \times #2}}% How to print function x_times with arity (2)
\def\xunderscoreaddtwofn#1#2{{#1 + #2}}% How to print function x_add with arity (2)
\def\xunderscorelimitonefn#1{{\pvsid{limit}(#1)}}% How to print function x_limit with arity (1)
\def\xunderscoresumonefn#1{{\sum #1}}% How to print function x_sum with arity (1)
\def\xunderscoresigmathreefn#1#2#3{{\sum_{#1}^{#2} #3}}% How to print function x_sigma with arity (3)
\def\xunderscoresuponefn#1{{\pvsid{sup}(#1)}}% How to print function x_sup with arity (1)
\def\xunderscoreinfonefn#1{{\pvsid{inf}(#1)}}% How to print function x_inf with arity (1)
\def\pointwiseunderscoreconvergesunderscoredowntoothertwofn#1#2{{#1 \searrow #2}}% How to print function pointwise_converges_downto? with arity (2)
\def\pointwiseunderscoreconvergesunderscoreuptoothertwofn#1#2{{#1 \nearrow #2}}% How to print function pointwise_converges_upto? with arity (2)
\def\pointwiseunderscoreconvergenceothertwofn#1#2{{#1 \longrightarrow #2}}% How to print function pointwise_convergence? with arity (2)
\def\convergesunderscoredowntoothertwofn#1#2{{#1 \searrow #2}}% How to print function converges_downto? with arity (2)
\def\convergesunderscoreuptoothertwofn#1#2{{#1 \nearrow #2}}% How to print function converges_upto? with arity (2)
\def\convergenceothertwofn#1#2{{#1 \longrightarrow #2}}% How to print function convergence? with arity (2)
\def\convergencetwofn#1#2{{#1 \longrightarrow #2}}% How to print function convergence with arity (2)
\def\crossunderscoreproducttwofn#1#2{{#1 \times #2}}% How to print function cross_product with arity (2)
\def\conjugateonefn#1{{\overline{#1}}}% How to print function conjugate with arity (1)
\def\cunderscoredivtwofn#1#2{{#1/#2}}% How to print function c_div with arity (2)
\def\cunderscoremultwofn#1#2{{#1\times#2}}% How to print function c_mul with arity (2)
\def\cunderscoresubtwofn#1#2{{#1-#2}}% How to print function c_sub with arity (2)
\def\cunderscorenegonefn#1{{-#1}}% How to print function c_neg with arity (1)
\def\cunderscoreaddtwofn#1#2{{#1+#2}}% How to print function c_add with arity (2)
\def\Imonefn#1{{\Im(#1)}}% How to print function Im with arity (1)
\def\Reonefn#1{{\Re(#1)}}% How to print function Re with arity (1)
\def\Etwofn#1#2{{\mathbb{E}(#1~|~#2)}}% How to print function E with arity (2)
\def\Eonefn#1{{\mathbb{E}(#1)}}% How to print function E with arity (1)
\def\Ptwofn#1#2{{\mathbb{P}(#1~|~#2)}}% How to print function P with arity (2)
\def\Ponefn#1{{\mathbb{P}(#1)}}% How to print function P with arity (1)
\def\xtwofn#1#2{{#1\times#2}}% How to print function x with arity (2)
\def\asttwofn#1#2{{#1\ast#2}}% How to print function ast with arity (2)
\def\minusonefn#1{{{#1}^{-}}}% How to print function minus with arity (1)
\def\plusonefn#1{{{#1}^{+}}}% How to print function plus with arity (1)
\def\astonefn#1{{{#1}^{\ast}}}% How to print function ast with arity (1)
\def\dottwofn#1#2{{#1\bullet#2}}% How to print function dot with arity (2)
\def\integralthreefn#1#2#3{{\int_{#1}^{#2} #3}}% How to print function integral with arity (3)
\def\integraltwofn#1#2{{\int_{#1} #2}}% How to print function integral with arity (2)
\def\integralonefn#1{{\int#1}}% How to print function integral with arity (1)
\def\normonefn#1{{\left||{#1}\right||}}% How to print function norm with arity (1)
\def\phionefn#1{{\pvssubscript{\phi}{#1}}}% How to print function phi with arity (1)
\def\infunderscoreclosedonefn#1{{\left(-\infty,~#1\right]}}% How to print function inf_closed with arity (1)
\def\closedunderscoreinfonefn#1{{\left[#1,~\infty\right)}}% How to print function closed_inf with arity (1)
\def\infunderscoreopenonefn#1{(-\infty,~#1)}% How to print function inf_open with arity (1)
\def\openunderscoreinfonefn#1{(#1,~\infty)}% How to print function open_inf with arity (1)
\def\closedtwofn#1#2{{\left[#1,~#2\right]}}% How to print function closed with arity (2)
\def\opentwofn#1#2{(#1,~#2)}% How to print function open with arity (2)
\def\sigmathreefn#1#2#3{{\sum_{#1}^{#2} #3}}% How to print function sigma with arity (3)
\def\sigmatwofn#1#2{{\sum_{#1} {#2}}}% How to print function sigma with arity (2)
\def\ceilingonefn#1{{\lceil{#1}\rceil}}% How to print function ceiling with arity (1)
\def\flooronefn#1{{\lfloor{#1}\rfloor}}% How to print function floor with arity (1)
\def\absonefn#1{{\left|{#1}\right|}}% How to print function abs with arity (1)
\def\roottwofn#1#2{{\sqrt[#2]{#1}}}% How to print function root with arity (2)
\def\sqrtonefn#1{{\sqrt{#1}}}% How to print function sqrt with arity (1)
\def\sqonefn#1{{\pvssuperscript{#1}{2}}}% How to print function sq with arity (1)
\def\expttwofn#1#2{{\pvssuperscript{#1}{#2}}}% How to print function expt with arity (2)
\def\opcarettwofn#1#2{{\pvssuperscript{#1}{#2}}}% How to print function ^ with arity (2)
\def\indexedunderscoresetsotherIIntersectiononefn#1{{\bigcap #1}}% How to print function indexed_sets.IIntersection with arity (1)
\def\indexedunderscoresetsotherIUniononefn#1{{\bigcup #1}}% How to print function indexed_sets.IUnion with arity (1)
\def\setsotherIntersectiononefn#1{{\bigcap #1}}% How to print function sets.Intersection with arity (1)
\def\setsotherUniononefn#1{{\bigcup #1}}% How to print function sets.Union with arity (1)
\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{{\frac{#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)
\begin{alltt}
\pvsid{PartialRefDefault}\({\pvsbracketl}\)\pvsid{Conf}: \pvskey{TYPE}, \pvsid{FM}: \pvskey{TYPE}, \pvsid{\{||\}}: \({\pvsbracketl}\)\pvsid{FM} \(\rightarrow\) \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\)\({\pvsbracketr}\), \pvsid{Asset}: \pvskey{TYPE}, \pvsid{AssetName}: \pvskey{TYPE},
                   \pvsid{CK}: \pvskey{TYPE},
                   \pvsid{(}\pvskey{IMPORTING} \pvsid{maps}\({\pvsbracketl}\)\pvsid{AssetName}, \pvsid{Asset}\({\pvsbracketr}\)\pvsid{)} \pvsid{[||]}: \({\pvsbracketl}\)\pvsid{CK} \(\rightarrow\)
                                                                  \({\pvsbracketl}\)\pvsid{mapping} \(\rightarrow\)
                                                                    \({\pvsbracketl}\)\pvsid{Conf} \(\rightarrow\)
                                                                      \pvsid{finite\_sets}
                                                                      \({\pvsbracketl}\)\pvsid{Asset}\({\pvsbracketr}\).\pvsid{finite\_set}\({\pvsbracketr}\)\({\pvsbracketr}\)\({\pvsbracketr}\)\({\pvsbracketr}\): \pvskey{THEORY}
 \pvskey{BEGIN}

  \(c\), \(c\sb{2}\): \pvskey{VAR} \pvsid{Conf}\vspace*{\pvsdeclspacing}

  \(s\), \(t\), \(u\): \pvskey{VAR} \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\)\vspace*{\pvsdeclspacing}

  \pvsid{fm}, \pvsid{fm1}, \pvsid{fm2}: \pvskey{VAR} \pvsid{FM}\vspace*{\pvsdeclspacing}

  \pvsid{ck}, \pvsid{ck2}: \pvskey{VAR} \pvsid{CK}\vspace*{\pvsdeclspacing}

  \(a\), \(a\sb{1}\), \(a\sb{2}\): \pvskey{VAR} \pvsid{Asset}\vspace*{\pvsdeclspacing}

  \pvsid{an}: \pvskey{VAR} \pvsid{AssetName}\vspace*{\pvsdeclspacing}

  \pvsid{anSet}: \pvskey{VAR} \pvsid{set}\({\pvsbracketl}\)\pvsid{AssetName}\({\pvsbracketr}\)\vspace*{\pvsdeclspacing}

  \pvsid{pair}: \pvskey{VAR} \({\pvsbracketl}\)\pvsid{Asset}\({\pvsbracketr}\)\vspace*{\pvsdeclspacing}

  \pvskey{IMPORTING} \pvsid{PartialRefBasics}\({\pvsbracketl}\)\pvsid{Conf}, \pvsid{FM}, \pvsid{\{||\}}, \pvsid{Asset}, \pvsid{AssetName}, \pvsid{CK}, \pvsid{[||]}\({\pvsbracketr}\)

  \pvsid{am}, \pvsid{am1}, \pvsid{am2}, \pvsid{pairs}: \pvskey{VAR} \pvsid{AM}\vspace*{\pvsdeclspacing}

  \pvsid{pl}, \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl3}, \pvsid{pl4}: \pvskey{VAR} \pvsid{PL}\vspace*{\pvsdeclspacing}

  \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)}: \pvsid{bool} \pvskey{=}
      \(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)}}\) \(\wedge\)
       \(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl2}\pvsid{)}\pvsid{)}}\) \(\wedge\)
        \pvsid{(}\pvskey{forall} \(c\): \(s\)\pvsid{(}\(c\)\pvsid{)} \(\Rightarrow\) \pvsid{(}\pvsid{prod}\pvsid{(}\pvsid{pl1}, \(c\)\pvsid{)} \pvsid{|-} \pvsid{prod}\pvsid{(}\pvsid{pl2}, \(c\)\pvsid{)}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{strongPartRefReflexive}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl}, \(s\):
      \(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl}\pvsid{)}\pvsid{)}}\) \(\Rightarrow\) \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl}, \pvsid{pl}, \(s\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{strongPartRefTransitive}: \pvskey{THEOREM}
    \pvsid{(}\pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl3}, \(s\), \(t\):
        \pvsid{(}\pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl3}, \(t\)\pvsid{)}\pvsid{)} \(\Rightarrow\)
         \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}, \(\setsotherintersectiontwofn{s}{t}\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{newprop}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \(s\), \pvsid{pl2}:
      \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{forall} \(t\):
           \(\setsothersubsetothertwofn{t}{s}\) \(\Rightarrow\) \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(t\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{fmCompStrongDef}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{(}\pvsid{pl}, \pvsid{fm2}, \(s\)\pvsid{)}:
      \pvsid{(}\pvsid{fmPartialRefinement}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl}\pvsid{)}, \pvsid{fm2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{wfPL}\pvsid{(}\pvsid{pl2}\pvsid{)} \(\Rightarrow\)
         \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl}, \pvsid{pl2}, \(s\)\pvsid{)}\pvsid{)}
        \pvskey{WHERE} \pvsid{fm1} \pvskey{=} \(F\)\pvsid{(}\pvsid{pl}\pvsid{)},
              \pvsid{pl2} \pvskey{=} \pvsid{(\#}\(F\) \pvskey{:=} \pvsid{fm2}, \(A\) \pvskey{:=} \(A\)\pvsid{(}\pvsid{pl}\pvsid{)}, \(K\) \pvskey{:=} \(K\)\pvsid{(}\pvsid{pl}\pvsid{)}\pvsid{\#)}\vspace*{\pvsdeclspacing}

  \pvsid{fmRefStrongDef}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{(}\pvsid{pl}, \pvsid{fm2}, \(s\)\pvsid{)}:
      \pvsid{(}\(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl}\pvsid{)}\pvsid{)}}\) \(\wedge\) \pvsid{(}\(F\)\pvsid{(}\pvsid{pl}\pvsid{)} \(\models\) \pvsid{fm2}\pvsid{)} \(\wedge\) \pvsid{wfPL}\pvsid{(}\pvsid{pl2}\pvsid{)} \(\Rightarrow\)
         \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl}, \pvsid{pl2}, \(s\)\pvsid{)}\pvsid{)}
        \pvskey{WHERE} \pvsid{fm1} \pvskey{=} \(F\)\pvsid{(}\pvsid{pl}\pvsid{)},
              \pvsid{pl2} \pvskey{=} \pvsid{(\#}\(F\) \pvskey{:=} \pvsid{fm2}, \(A\) \pvskey{:=} \(A\)\pvsid{(}\pvsid{pl}\pvsid{)}, \(K\) \pvskey{:=} \(K\)\pvsid{(}\pvsid{pl}\pvsid{)}\pvsid{\#)}\vspace*{\pvsdeclspacing}

  \pvsid{ckWeakerEqStrongDef}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{(}\pvsid{pl}, \pvsid{ck2}, \(s\)\pvsid{)}:
      \pvsid{(}\(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl}\pvsid{)}\pvsid{)}}\) \(\wedge\) \pvsid{ckWeakerEq}\pvsid{(}\pvsid{ck1}, \pvsid{ck2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{wfPL}\pvsid{(}\pvsid{pl2}\pvsid{)} \(\Rightarrow\)
         \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl}, \pvsid{pl2}, \(s\)\pvsid{)}\pvsid{)}
        \pvskey{WHERE} \pvsid{ck1} \pvskey{=} \(K\)\pvsid{(}\pvsid{pl}\pvsid{)},
              \pvsid{pl2} \pvskey{=} \pvsid{(\#}\(F\) \pvskey{:=} \(F\)\pvsid{(}\pvsid{pl}\pvsid{)}, \(A\) \pvskey{:=} \(A\)\pvsid{(}\pvsid{pl}\pvsid{)}, \(K\) \pvskey{:=} \pvsid{ck2}\pvsid{\#)}\vspace*{\pvsdeclspacing}

  \pvsid{partCaseStrongerPLRef}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \(s\):
      \(s\) \(=\) \pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\Leftrightarrow\)
          \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{partRefRel}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}: \pvsid{PL}, \(s\): \{\pvsid{confs}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\) | \(\setsothersubsetothertwofn{\pvsid{confs}}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)}}\)\}\pvsid{)}:
        \pvsid{bool} \pvskey{=}
      \pvskey{forall} \(c\):
        \(s\)\pvsid{(}\(c\)\pvsid{)} \(\Rightarrow\)
         \pvsid{(}\pvskey{exists} \(c\sb{2}\):
             \pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl2}\pvsid{)}\pvsid{)}\pvsid{(}\(c\sb{2}\)\pvsid{)} \(\wedge\)
              \pvsid{(}\pvsid{prod}\pvsid{(}\pvsid{pl1}, \(c\)\pvsid{)} \pvsid{|-} \pvsid{prod}\pvsid{(}\pvsid{pl2}, \(c\sb{2}\)\pvsid{)}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{partRefFun}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}: \pvsid{PL}, \(s\): \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\), \(f\): \({\pvsbracketl}\)\pvsid{(}\(s\)\pvsid{)} \(\rightarrow\) \pvsid{(}\pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl2}\pvsid{)}\pvsid{)}\pvsid{)}\({\pvsbracketr}\)\pvsid{)}: \pvsid{bool} \pvskey{=}
      \pvskey{forall} \pvsid{(}\(c\): \pvsid{domain}\pvsid{(}\(f\)\pvsid{)}\pvsid{)}:
        \pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl2}\pvsid{)}\pvsid{)}\pvsid{(}\(f\)\pvsid{(}\(c\)\pvsid{)}\pvsid{)} \(\wedge\)
         \pvsid{(}\pvsid{prod}\pvsid{(}\pvsid{pl1}, \(c\)\pvsid{)} \pvsid{|-} \pvsid{prod}\pvsid{(}\pvsid{pl2}, \(f\)\pvsid{(}\(c\)\pvsid{)}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{totalImpliesPartial}: \pvskey{LEMMA}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{(}\(s\): \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\) | \(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)}}\)\pvsid{)}:
      \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}\pvsid{)} \(\Rightarrow\)
       \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{partialImpliesTotal}: \pvskey{LEMMA}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \(s\):
      \pvsid{(}\(s\) \(=\) \pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)} \(\wedge\) \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)}\pvsid{)} \(\Rightarrow\)
       \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{commutableDiagram}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl3}, \pvsid{pl4}, \pvsid{(}\(s\): \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\) | \(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)}}\)\pvsid{)}:
      \pvsid{(}\pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}\pvsid{)} \(\wedge\) \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl3}, \pvsid{pl4}, \(s\)\pvsid{)}\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{exists} \pvsid{pl2}:
           \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\wedge\)
            \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl4}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{commutableDiagram2}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl4}, \(s\):
      \pvsid{(}\pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl4}\pvsid{)}\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{exists} \pvsid{pl3}:
           \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}\pvsid{)} \(\wedge\)
            \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl3}, \pvsid{pl4}, \(s\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{commutableDiagramAlt}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl4}, \pvsid{(}\(s\): \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\) | \(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)}}\)\pvsid{)}:
      \pvsid{(}\pvskey{exists} \pvsid{pl2}: \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl4}\pvsid{)}\pvsid{)}
       \(\Leftrightarrow\)
       \pvsid{(}\pvskey{exists} \pvsid{pl3}:
           \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}\pvsid{)} \(\wedge\)
            \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl3}, \pvsid{pl4}, \(s\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{partPlusTotalStrongerImpliesPart}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl3}, \(s\):
      \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl3}\pvsid{)} \(\Rightarrow\)
       \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}, \(s\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{totalStrongerPlusPartImpliesPart}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl3}, \pvsid{(}\(s\): \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\) | \(\setsothersubsetothertwofn{s}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)}}\)\pvsid{)}:
      \pvsid{strongerPLrefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}\pvsid{)} \(\wedge\) \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl3}, \(s\)\pvsid{)} \(\Rightarrow\)
       \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}, \(s\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{partPlusTotalImpliesPartRel}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl3}, \(s\):
      \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{plRefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl3}\pvsid{)} \(\Rightarrow\)
       \pvsid{partRefRel}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}, \(s\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{totalPlusPartImpliesPartRef}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl3}, \(s\):
      \pvsid{plRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}\pvsid{)} \(\wedge\) \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl3}, \(s\)\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{exists} \pvsid{(}\(t\): \pvsid{set}\({\pvsbracketl}\)\pvsid{Conf}\({\pvsbracketr}\) | \(\setsothersubsetothertwofn{t}{\pvsid{\{||\}}\pvsid{(}F\pvsid{(}\pvsid{pl1}\pvsid{)}\pvsid{)}}\)\pvsid{)}:
           \pvsid{partRefRel}\pvsid{(}\pvsid{pl1}, \pvsid{pl3}, \(t\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{partRefExistsFunId}: \pvskey{LEMMA}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \(s\):
      \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{exists} \pvsid{(}\(f\): \({\pvsbracketl}\)\pvsid{(}\(s\)\pvsid{)} \(\rightarrow\) \pvsid{(}\(s\)\pvsid{)}\({\pvsbracketr}\)\pvsid{)}:
           \pvsid{(}\pvskey{forall} \(c\):
               \(s\)\pvsid{(}\(c\)\pvsid{)} \(\Rightarrow\)
                \pvsid{(}\pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl2}\pvsid{)}\pvsid{)}\pvsid{(}\(f\)\pvsid{(}\(c\)\pvsid{)}\pvsid{)}\pvsid{)} \(\wedge\)
                 \pvsid{(}\pvsid{prod}\pvsid{(}\pvsid{pl1}, \(c\)\pvsid{)} \pvsid{|-} \pvsid{prod}\pvsid{(}\pvsid{pl2}, \(f\)\pvsid{(}\(c\)\pvsid{)}\pvsid{)}\pvsid{)}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{partPlusTotalImpliesPartFun}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{pl1}, \pvsid{pl2}, \pvsid{pl3}, \(s\):
      \pvsid{strongPartialRefinement}\pvsid{(}\pvsid{pl1}, \pvsid{pl2}, \(s\)\pvsid{)} \(\wedge\) \pvsid{plRefinement}\pvsid{(}\pvsid{pl2}, \pvsid{pl3}\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{exists} \pvsid{(}\(f\): \({\pvsbracketl}\)\pvsid{(}\(s\)\pvsid{)} \(\rightarrow\) \pvsid{(}\pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl3}\pvsid{)}\pvsid{)}\pvsid{)}\({\pvsbracketr}\)\pvsid{)}:
           \pvsid{(}\pvskey{forall} \(c\):
               \(s\)\pvsid{(}\(c\)\pvsid{)} \(\Rightarrow\)
                \pvsid{(}\pvsid{\{||\}}\pvsid{(}\(F\)\pvsid{(}\pvsid{pl3}\pvsid{)}\pvsid{)}\pvsid{(}\(f\)\pvsid{(}\(c\)\pvsid{)}\pvsid{)} \(\wedge\)
                   \pvsid{(}\pvsid{prod}\pvsid{(}\pvsid{pl1}, \(c\)\pvsid{)} \pvsid{|-} \pvsid{prod}\pvsid{(}\pvsid{pl3}, \(f\)\pvsid{(}\(c\)\pvsid{)}\pvsid{)}\pvsid{)}\pvsid{)}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

 \pvskey{END} \pvsid{PartialRefDefault}\end{alltt}