FeatureModelSemantics.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{FeatureModelSemantics}: \pvskey{THEORY}
 \pvskey{BEGIN}

  \pvskey{IMPORTING} \pvsid{FormulaTheory}

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

  \pvsid{exp}: \pvskey{VAR} \pvsid{Formula\_}\vspace*{\pvsdeclspacing}

  \pvsid{exps}: \pvskey{VAR} \pvsid{set}\({\pvsbracketl}\)\pvsid{Formula\_}\({\pvsbracketr}\)\vspace*{\pvsdeclspacing}

  \(c\): \pvskey{VAR} \pvsid{Configuration}\vspace*{\pvsdeclspacing}

  \(Q\): \pvskey{VAR} \pvsid{Name}\vspace*{\pvsdeclspacing}

  \pvsid{wfFM}\pvsid{(}\pvsid{fm}: \pvsid{FM}\pvsid{)}: \pvsid{bool} \pvskey{=} \pvsid{wfTree}\pvsid{(}\pvsid{fm}\pvsid{)} \(\wedge\) \pvsid{wfFormulae}\pvsid{(}\pvsid{fm}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{WFM}: \pvskey{TYPE} = \pvsid{(}\pvsid{wfFM}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{getFeatures}\pvsid{(}\pvsid{fm}: \pvsid{FM}\pvsid{)}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Name}\({\pvsbracketr}\) \pvskey{=} \pvsid{features}\pvsid{(}\pvsid{fm}\pvsid{)};\vspace*{\pvsdeclspacing}

  \pvsid{genFE}\pvsid{(}\(f\): \pvsid{Name}\pvsid{)}: \pvsid{Formula\_} \pvskey{=} \pvsid{NAME\_FORMULA}\pvsid{(}\(f\)\pvsid{)};\vspace*{\pvsdeclspacing}

  \pvsid{satImpConsts}\pvsid{(}\pvsid{fm}: \pvsid{FM}, \(c\): \pvsid{Configuration}\pvsid{)}: \pvsid{bool} \pvskey{=}
      \pvskey{forall} \pvsid{(}\(n\): \pvsid{Name}\pvsid{)}: \(c\)\pvsid{(}\(n\)\pvsid{)} \(\Rightarrow\) \pvsid{features}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\(n\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{satExpConsts}\pvsid{(}\pvsid{fm}: \pvsid{FM}, \(c\): \pvsid{Configuration}\pvsid{)}: \pvsid{bool} \pvskey{=}
      \pvskey{forall} \pvsid{(}\(f\): \pvsid{Formula\_}\pvsid{)}: \pvsid{formulae}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\(f\)\pvsid{)} \(\Rightarrow\) \pvsid{satisfies}\pvsid{(}\(f\), \(c\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{semantics}\pvsid{(}\pvsid{fm}: \pvsid{FM}\pvsid{)}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Configuration}\({\pvsbracketr}\) \pvskey{=}
      \{\(c\): \pvsid{Configuration} |
          \pvsid{satImpConsts}\pvsid{(}\pvsid{fm}, \(c\)\pvsid{)} \(\wedge\) \pvsid{satExpConsts}\pvsid{(}\pvsid{fm}, \(c\)\pvsid{)}\}\vspace*{\pvsdeclspacing}

  \pvsid{refines}\pvsid{(}\pvsid{abs}, \pvsid{con}: \pvsid{WFM}\pvsid{)}: \pvsid{bool} \pvskey{=}
      \(\setsothersubsetothertwofn{\pvsid{semantics}\pvsid{(}\pvsid{abs}\pvsid{)}}{\pvsid{semantics}\pvsid{(}\pvsid{con}\pvsid{)}}\)\vspace*{\pvsdeclspacing}

  \pvsid{refines2}\pvsid{(}\pvsid{abs}, \pvsid{con}: \pvsid{WFM}\pvsid{)}: \pvsid{bool} \pvskey{=}
      \pvskey{forall} \pvsid{(}\(c\sb{1}\): \pvsid{Configuration}\pvsid{)}:
        \pvsid{semantics}\pvsid{(}\pvsid{abs}\pvsid{)}\pvsid{(}\(c\sb{1}\)\pvsid{)} \(\Rightarrow\)
         \pvsid{(}\pvskey{exists} \pvsid{(}\(c\sb{2}\): \pvsid{Configuration}\pvsid{)}: \pvsid{semantics}\pvsid{(}\pvsid{con}\pvsid{)}\pvsid{(}\(c\sb{2}\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{addMandatoryFM}\pvsid{(}\pvsid{fm}: \pvsid{FM}, \(n\sb{1}\), \(n\sb{2}\): \pvsid{Name}\pvsid{)}: \pvsid{FM} \pvskey{=}
      \pvsid{fm}
        \pvskey{WITH} \({\pvsbracketl}\)\pvsid{features} \pvskey{:=} \(\setsotheraddtwofn{n\sb{2}}{\pvsid{features}\pvsid{(}\pvsid{fm}\pvsid{)}}\),
               \pvsid{formulae}
                 \pvskey{:=} \(\setsotheraddtwofn{\pvsid{IMPLIES\_FORMULA}\pvsid{(}\pvsid{NAME\_FORMULA}\pvsid{(}n\sb{2}\pvsid{)}, \pvsid{NAME\_FORMULA}\pvsid{(}n\sb{1}\pvsid{)}\pvsid{)}}{\setsotheraddtwofn{\pvsid{IMPLIES\_FORMULA}\pvsid{(}\pvsid{NAME\_FORMULA}\pvsid{(}n\sb{1}\pvsid{)}, \pvsid{NAME\_FORMULA}\pvsid{(}n\sb{2}\pvsid{)}\pvsid{)}}{\pvsid{formulae}\pvsid{(}\pvsid{fm}\pvsid{)}}}\)\({\pvsbracketr}\)\vspace*{\pvsdeclspacing}

  \pvsid{addOptionalFM}\pvsid{(}\pvsid{fm}: \pvsid{FM}, \(n\sb{1}\), \(n\sb{2}\): \pvsid{Name}\pvsid{)}: \pvsid{FM} \pvskey{=}
      \pvsid{fm}
        \pvskey{WITH} \({\pvsbracketl}\)\pvsid{features} \pvskey{:=} \(\setsotheraddtwofn{n\sb{2}}{\pvsid{features}\pvsid{(}\pvsid{fm}\pvsid{)}}\),
               \pvsid{formulae}
                 \pvskey{:=} \(\setsotheraddtwofn{\pvsid{IMPLIES\_FORMULA}\pvsid{(}\pvsid{NAME\_FORMULA}\pvsid{(}n\sb{2}\pvsid{)}, \pvsid{NAME\_FORMULA}\pvsid{(}n\sb{1}\pvsid{)}\pvsid{)}}{\pvsid{formulae}\pvsid{(}\pvsid{fm}\pvsid{)}}\)\({\pvsbracketr}\)\vspace*{\pvsdeclspacing}

  \pvsid{addMandatory}\pvsid{(}\pvsid{abs}: \pvsid{WFM}, \pvsid{con}: \pvsid{FM}, \(n\sb{1}\), \(n\sb{2}\): \pvsid{Name}\pvsid{)}: \pvsid{bool} \pvskey{=}
      \pvsid{features}\pvsid{(}\pvsid{con}\pvsid{)} \(=\) \(\setsotheraddtwofn{n\sb{2}}{\pvsid{features}\pvsid{(}\pvsid{abs}\pvsid{)}}\) \(\wedge\)
       \pvsid{formulae}\pvsid{(}\pvsid{con}\pvsid{)} \(=\)
        \(\setsotheraddtwofn{\pvsid{IMPLIES\_FORMULA}\pvsid{(}\pvsid{NAME\_FORMULA}\pvsid{(}n\sb{2}\pvsid{)}, \pvsid{NAME\_FORMULA}\pvsid{(}n\sb{1}\pvsid{)}\pvsid{)}}{\setsotheraddtwofn{\pvsid{IMPLIES\_FORMULA}\pvsid{(}\pvsid{NAME\_FORMULA}\pvsid{(}n\sb{1}\pvsid{)}, \pvsid{NAME\_FORMULA}\pvsid{(}n\sb{2}\pvsid{)}\pvsid{)}}{\pvsid{formulae}\pvsid{(}\pvsid{abs}\pvsid{)}}}\)
        \(\wedge\) \pvsid{features}\pvsid{(}\pvsid{abs}\pvsid{)}\pvsid{(}\(n\sb{1}\)\pvsid{)} \(\wedge\) \pvsid{(}\(\neg\) \pvsid{features}\pvsid{(}\pvsid{abs}\pvsid{)}\pvsid{(}\(n\sb{2}\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{addOptional}\pvsid{(}\pvsid{abs}: \pvsid{WFM}, \pvsid{con}: \pvsid{FM}, \(n\sb{1}\), \(n\sb{2}\): \pvsid{Name}\pvsid{)}: \pvsid{bool} \pvskey{=}
      \pvsid{features}\pvsid{(}\pvsid{con}\pvsid{)} \(=\) \(\setsotheraddtwofn{n\sb{2}}{\pvsid{features}\pvsid{(}\pvsid{abs}\pvsid{)}}\) \(\wedge\)
       \pvsid{features}\pvsid{(}\pvsid{abs}\pvsid{)}\pvsid{(}\(n\sb{1}\)\pvsid{)} \(\wedge\)
        \pvsid{formulae}\pvsid{(}\pvsid{con}\pvsid{)} \(=\)
         \(\setsotheraddtwofn{\pvsid{IMPLIES\_FORMULA}\pvsid{(}\pvsid{NAME\_FORMULA}\pvsid{(}n\sb{2}\pvsid{)}, \pvsid{NAME\_FORMULA}\pvsid{(}n\sb{1}\pvsid{)}\pvsid{)}}{\pvsid{formulae}\pvsid{(}\pvsid{abs}\pvsid{)}}\)
         \(\wedge\) \pvsid{(}\(\neg\) \pvsid{features}\pvsid{(}\pvsid{abs}\pvsid{)}\pvsid{(}\(n\sb{2}\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{wtFormRefinement}: \pvskey{LEMMA}
    \pvskey{forall} \pvsid{(}\pvsid{abs}, \pvsid{con}: \pvsid{FM}\pvsid{)}:
      \pvsid{(}\pvskey{forall} \pvsid{(}\pvsid{name}: \pvsid{Name}\pvsid{)}: \pvsid{features}\pvsid{(}\pvsid{abs}\pvsid{)}\pvsid{(}\pvsid{name}\pvsid{)} \(\Rightarrow\) \pvsid{features}\pvsid{(}\pvsid{con}\pvsid{)}\pvsid{(}\pvsid{name}\pvsid{)}\pvsid{)} \(\wedge\)
       \pvsid{wfTree}\pvsid{(}\pvsid{abs}\pvsid{)} \(\wedge\) \pvsid{wfTree}\pvsid{(}\pvsid{con}\pvsid{)}
       \(\Rightarrow\) \pvsid{(}\pvskey{forall} \pvsid{(}\(f\): \pvsid{Formula\_}\pvsid{)}: \pvsid{wt}\pvsid{(}\pvsid{abs}, \(f\)\pvsid{)} \(\Rightarrow\) \pvsid{wt}\pvsid{(}\pvsid{con}, \(f\)\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{notMember}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{(}\pvsid{fm}: \pvsid{WFM}, \pvsid{opt}: \pvsid{Name}\pvsid{)}:
      \pvsid{(}\(\neg\) \pvsid{(}\pvsid{features}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\pvsid{opt}\pvsid{)}\pvsid{)}\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{forall} \pvsid{(}\(c\): \pvsid{Configuration}\pvsid{)}:
           \pvsid{semantics}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\(c\)\pvsid{)} \(\Rightarrow\) \(\neg\) \(c\)\pvsid{(}\pvsid{opt}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{teste2}: \pvskey{LEMMA}
    \pvskey{forall} \pvsid{(}\(F\), \(G\): \pvsid{Name}\pvsid{)}:
      \pvsid{(}\pvskey{forall} \pvsid{(}\(c\): \pvsid{Configuration}, \(f\): \pvsid{Formula\_}\pvsid{)}:
          \(\neg\) \(\pvsid{(}\setsothermembertwofn{G}{\pvsid{names}\pvsid{(}f\pvsid{)}}\pvsid{)}\) \(\Rightarrow\)
           \pvsid{(}\pvsid{satisfies}\pvsid{(}\(f\), \pvskey{IF} \pvsid{(}\(c\)\pvsid{(}\(G\)\pvsid{)}\pvsid{)} \pvskey{THEN} \(\setsotheraddtwofn{F}{\setsotherremovetwofn{G}{c}}\) \pvskey{ELSE} \(c\) \pvskey{ENDIF}\pvsid{)} \(\Leftrightarrow\)
              \pvsid{satisfies}\pvsid{(}\pvsid{rename}\pvsid{(}\(f\), \(F\), \(G\)\pvsid{)},
                         \pvskey{IF} \pvsid{(}\(c\)\pvsid{(}\(F\)\pvsid{)}\pvsid{)}
                           \pvskey{THEN} \(\setsotheraddtwofn{G}{\setsotherremovetwofn{F}{c}}\)
                         \pvskey{ELSE} \(c\)
                         \pvskey{ENDIF}\pvsid{)}\pvsid{)}\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{renameFormulae}\pvsid{(}\pvsid{forms}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Formula\_}\({\pvsbracketr}\), \(F\), \(G\): \pvsid{Name}\pvsid{)}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Formula\_}\({\pvsbracketr}\) \pvskey{=}
      \{\(f\): \pvsid{Formula\_} |
          \pvskey{exists} \pvsid{(}\(f\sb{1}\): \pvsid{Formula\_}\pvsid{)}:
            \pvsid{forms}\pvsid{(}\(f\sb{1}\)\pvsid{)} \(\wedge\) \(f\) \(=\) \pvsid{rename}\pvsid{(}\(f\sb{1}\), \(F\), \(G\)\pvsid{)}\}\vspace*{\pvsdeclspacing}

  \pvsid{renameFM}\pvsid{(}\pvsid{fm}: \pvsid{FM}, \(F\), \(G\): \pvsid{Name}\pvsid{)}: \pvsid{FM} \pvskey{=}
      \pvsid{(\#}\pvsid{features} \pvskey{:=} \(\setsotheraddtwofn{G}{\setsotherremovetwofn{F}{\pvsid{features}\pvsid{(}\pvsid{fm}\pvsid{)}}}\),
        \pvsid{formulae} \pvskey{:=} \pvsid{renameFormulae}\pvsid{(}\pvsid{formulae}\pvsid{(}\pvsid{fm}\pvsid{)}, \(F\), \(G\)\pvsid{)}\pvsid{\#)}\vspace*{\pvsdeclspacing}

  \pvsid{wtFormRename2}: \pvskey{LEMMA}
    \pvskey{forall} \pvsid{(}\pvsid{fm1}: \pvsid{WFM}, \(F\), \(G\): \pvsid{Name}\pvsid{)}:
      \pvsid{(}\pvsid{(}\pvsid{wfTree}\pvsid{(}\pvsid{fm1}\pvsid{)} \(\wedge\) \pvsid{wfTree}\pvsid{(}\pvsid{fm2}\pvsid{)}\pvsid{)} \(\Rightarrow\)
         \pvsid{(}\pvskey{forall} \pvsid{(}\(f\): \pvsid{Formula\_}\pvsid{)}: \pvsid{wt}\pvsid{(}\pvsid{fm1}, \(f\)\pvsid{)} \(\Rightarrow\) \pvsid{wt}\pvsid{(}\pvsid{fm2}, \pvsid{rename}\pvsid{(}\(f\), \(F\), \(G\)\pvsid{)}\pvsid{)}\pvsid{)}\pvsid{)}
        \pvskey{WHERE} \pvsid{fm2} \pvskey{=} \pvsid{renameFM}\pvsid{(}\pvsid{fm1}, \(F\), \(G\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{renameFeature\_WF}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{(}\pvsid{fm1}: \pvsid{WFM}, \(F\), \(G\): \pvsid{Name}\pvsid{)}:
      \pvsid{wfFM}\pvsid{(}\pvsid{fm2}\pvsid{)} \pvskey{WHERE} \pvsid{fm2} \pvskey{=} \pvsid{renameFM}\pvsid{(}\pvsid{fm1}, \(F\), \(G\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{satFormula3}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{(}\pvsid{fm1}: \pvsid{WFM}, \(F\), \(G\): \pvsid{Name}\pvsid{)}:
      \pvsid{(}\(\neg\) \pvsid{features}\pvsid{(}\pvsid{fm1}\pvsid{)}\pvsid{(}\(G\)\pvsid{)}\pvsid{)} \(\Rightarrow\)
       \pvsid{(}\pvskey{forall} \pvsid{(}\(c\): \pvsid{Configuration}, \(f\): \pvsid{Formula\_}\pvsid{)}:
           \pvsid{semantics}\pvsid{(}\pvsid{fm1}\pvsid{)}\pvsid{(}\(c\)\pvsid{)} \(\wedge\) \pvsid{(}\(\neg\) \(\pvsid{(}\setsothermembertwofn{G}{\pvsid{names}\pvsid{(}f\pvsid{)}}\pvsid{)}\)\pvsid{)} \(\Rightarrow\)
            \pvsid{(}\pvsid{satisfies}\pvsid{(}\(f\), \(c\)\pvsid{)} \(\Rightarrow\)
               \pvsid{satisfies}\pvsid{(}\pvsid{rename}\pvsid{(}\(f\), \(F\), \(G\)\pvsid{)},
                          \pvskey{IF} \pvsid{(}\(c\)\pvsid{(}\(F\)\pvsid{)}\pvsid{)} \pvskey{THEN} \(\setsotheraddtwofn{G}{\setsotherremovetwofn{F}{c}}\) \pvskey{ELSE} \(c\) \pvskey{ENDIF}\pvsid{)}\pvsid{)}\pvsid{)}
         \pvskey{WHERE} \pvsid{fm2} \pvskey{=} \pvsid{renameFM}\pvsid{(}\pvsid{fm1}, \(F\), \(G\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \pvsid{renameFeature3}: \pvskey{THEOREM}
    \pvskey{forall} \pvsid{(}\pvsid{fm1}: \pvsid{WFM}, \(F\), \(G\): \pvsid{Name}\pvsid{)}:
      \pvsid{(}\(\neg\) \pvsid{features}\pvsid{(}\pvsid{fm1}\pvsid{)}\pvsid{(}\(G\)\pvsid{)}\pvsid{)} \(\Rightarrow\)
       \pvsid{refines2}\pvsid{(}\pvsid{fm1}, \pvsid{fm2}\pvsid{)} \pvskey{WHERE} \pvsid{fm2} \pvskey{=} \pvsid{renameFM}\pvsid{(}\pvsid{fm1}, \(F\), \(G\)\pvsid{)}\vspace*{\pvsdeclspacing}

  \(\Diamond\)\pvsid{(}\pvsid{fm}, \pvsid{exp}\pvsid{)}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Configuration}\({\pvsbracketr}\) \pvskey{=}
      \{\(c\) | \pvsid{semantics}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\(c\)\pvsid{)} \(\wedge\) \pvsid{satisfies}\pvsid{(}\pvsid{exp}, \(c\)\pvsid{)}\}\vspace*{\pvsdeclspacing}

  \(\Diamond\)\pvsid{(}\pvsid{exp}, \pvsid{fm}\pvsid{)}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Configuration}\({\pvsbracketr}\) \pvskey{=}
      \{\(c\) | \pvsid{semantics}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\(c\)\pvsid{)} \(\wedge\) \(\neg\) \pvsid{satisfies}\pvsid{(}\pvsid{exp}, \(c\)\pvsid{)}\}\vspace*{\pvsdeclspacing}

  \(\Diamond\)\pvsid{(}\pvsid{exps}, \pvsid{fm}\pvsid{)}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Configuration}\({\pvsbracketr}\) \pvskey{=}
      \{\(c\) |
          \pvsid{semantics}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\(c\)\pvsid{)} \(\wedge\)
           \pvsid{(}\pvskey{forall} \pvsid{exp}: \pvsid{exps}\pvsid{(}\pvsid{exp}\pvsid{)} \(\Rightarrow\) \(\neg\) \pvsid{satisfies}\pvsid{(}\pvsid{exp}, \(c\)\pvsid{)}\pvsid{)}\}\vspace*{\pvsdeclspacing}

  \pvsid{filterFormulae}\pvsid{(}\pvsid{fm}, \(Q\)\pvsid{)}: \pvsid{set}\({\pvsbracketl}\)\pvsid{Formula\_}\({\pvsbracketr}\) \pvskey{=}
      \{\pvsid{form}: \pvsid{Formula\_} |
          \pvsid{formulae}\pvsid{(}\pvsid{fm}\pvsid{)}\pvsid{(}\pvsid{form}\pvsid{)} \(\wedge\) \(\neg\) \(\setsothermembertwofn{Q}{\pvsid{names}\pvsid{(}\pvsid{form}\pvsid{)}}\)\}\vspace*{\pvsdeclspacing}

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