- <sect1 id="tac_reduce">
- <title>reduce</title>
- <titleabbrev>reduce</titleabbrev>
- <para><userinput>reduce patt</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">reduce</emphasis> &pattern;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It replaces all the terms matched by <command>patt</command>
- with their βδιζ-normal form.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>None.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>