</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
with their βδιζ-normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_paramodulation.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_reflexivity.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">paramodulation <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> reflexivity</td></tr></table></div></body></html>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>None.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It replaces all the terms matched by <span><strong class="command">patt</strong></span>
with their βδιζ-normal form.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_paramodulation.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_reflexivity.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">paramodulation <pattern> </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> reflexivity</td></tr></table></div></body></html>