<?xml version="1.0"?>
<div><span class="kw">theorem </span><span class="lab"><font color="Green" title="E97">Th16</font></span>: <a NAME="T16"><span class="comment"><font color="firebrick">:: FOMODEL4:16</font></span><br/></a><div class="add"> for <font color="Olive" title="b1">S</font> being   <a href="fomodel1.html#NM2" title="FOMODEL1:NM.2">Language</a><br/>  for <font color="Olive" title="b2">psi</font> being   <a href="fomodel2.html#V4" title="FOMODEL2:attr.4">wff</a>  <a href="fomodel1.html#NM3" title="FOMODEL1:NM.3">string</a> of <font color="Olive" title="b1">S</font><br/>  for <font color="Olive" title="b3">D1</font> being   <a href="numbers.html#K5" title="NUMBERS:func.5">0</a>  <a href="fomodel4.html#V13" title="FOMODEL4:attr.13">-ranked</a>  1 <a href="fomodel4.html#V13" title="FOMODEL4:attr.13">-ranked</a>  <a href="fomodel4.html#NM2" title="FOMODEL4:NM.2">RuleSet</a> of <font color="Olive" title="b1">S</font><br/>  for <font color="Olive" title="b4">X</font> being  <font color="Olive">b<sub>3</sub></font> <a href="fomodel4.html#V11" title="FOMODEL4:attr.11">-expanded</a>   <a href="hidden.html#M2" title="HIDDEN:mode.2">set</a>   st  <a href="fomodel4.html#K25" title="FOMODEL4:func.25">R#1</a> <font color="Olive" title="b1">S</font> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a> <font color="Olive" title="b3">D1</font> &amp;  <a href="fomodel4.html#K31" title="FOMODEL4:func.31">R#4</a> <font color="Olive" title="b1">S</font> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a> <font color="Olive" title="b3">D1</font> &amp;  <a href="fomodel4.html#K33" title="FOMODEL4:func.33">R#6</a> <font color="Olive" title="b1">S</font> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a> <font color="Olive" title="b3">D1</font> &amp;  <a href="fomodel4.html#K34" title="FOMODEL4:func.34">R#7</a> <font color="Olive" title="b1">S</font> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a> <font color="Olive" title="b3">D1</font> &amp;  <a href="fomodel4.html#K35" title="FOMODEL4:func.35">R#8</a> <font color="Olive" title="b1">S</font> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a> <font color="Olive" title="b3">D1</font> &amp; <font color="Olive" title="b4">X</font> is <font color="Olive" title="b1">S</font> <a href="fomodel2.html#V6" title="FOMODEL2:attr.6">-mincover</a>  &amp; <font color="Olive" title="b4">X</font> is <font color="Olive" title="b1">S</font> <a href="fomodel4.html#V14" title="FOMODEL4:attr.14">-witnessed</a>  holds <br/>( <span class="p1">(<span class="default"><font color="Olive" title="b3">D1</font> <a href="fomodel4.html#K41" title="FOMODEL4:func.41">Henkin</a> <font color="Olive" title="b4">X</font></span>)</span> <a href="fomodel2.html#K25" title="FOMODEL2:func.25">-TruthEval</a> <font color="Olive" title="b2">psi</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 1 iff <font color="Olive" title="b2">psi</font> <a href="tarski.html#R2" title="TARSKI:pred.2">in</a> <font color="Olive" title="b4">X</font> )</div></div>
