matita/matita/help/C/tac_thatisequivalentto.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>that is equivalent to</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><link rel="up" href="sec_declarative_tactics.html" title="Chapter 8. Declarative Tactics" /><link rel="prev" href="tac_let.html" title="letin" /><link rel="next" href="tac_thesisbecomes.html" title="the thesis becomes" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">that is equivalent to</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_let.html">Prev</a> </td><th width="60%" align="center">Chapter 8. Declarative Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_thesisbecomes.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_thatisequivalentto"></a>that is equivalent to</h2></div></div></div><p><strong class="userinput"><code>that is equivalent to t</code></strong></p><p>
   3       </p><div class="variablelist"><dl class="variablelist"><dt><span class="term">Synopsis:</span></dt><dd><p>
   4                <span class="bold"><strong>that is equivalent to</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.term">term</a></em></span>
   5            </p></dd><dt><span class="term">Pre-condition:</span></dt><dd><p>
   6                  The user must have applied one of the following tactics immediately before applying this tactic: <span class="bold"><strong>assume</strong></span>, <span class="bold"><strong>suppose</strong></span>, <span class="bold"><strong>we need to prove</strong></span>, <span class="bold"><strong>by just we proved</strong></span>,<span class="bold"><strong>the thesis becomes</strong></span>, <span class="bold"><strong>that is equivalent to</strong></span>.
   7              </p></dd><dt><span class="term">Action:</span></dt><dd><p>
   8                    If the tactic that was applied before this introduced a new hypothesis in the context, this tactic works on this hypothesis; otherwise, it works on the conclusion. Either way, if the term <span class="command"><strong>t</strong></span> is beta-equivalent to the term <span class="command"><strong>t1</strong></span> on which this tactic is working (i.e. they can be reduced to a common term), <span class="command"><strong>t1</strong></span> is changed with <span class="command"><strong>t</strong></span>.
   9
  10                        If the tactic that was applied before this tactic was <span class="bold"><strong>that is equivalent to</strong></span>, and that tactic was working on a term <span class="command"><strong>t1</strong></span>, this tactic keeps working on <span class="command"><strong>t1</strong></span>.
  11            </p></dd><dt><span class="term">New sequent to prove:</span></dt><dd><p>
  12                      If this tactic is working on the conclusion, a new sequent with the same hypotheses and the conclusion changed to <span class="command"><strong>t</strong></span> is opened. If this tactic is working on the last introduced hypotesis, a new sequent with the same conclusion is opened. The hypotheses of this sequent are the same, except for the one on which the tactic is working on, which is changed with <span class="command"><strong>t</strong></span>.
  13              </p></dd></dl></div><p>
  14      </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_let.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_declarative_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_thesisbecomes.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">letin </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> the thesis becomes</td></tr></table></div></body></html>