3 <para><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
6 <para><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
10 <link linkend="tac_assumption">
11 <emphasis role="bold">assumption</emphasis>
16 <para><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">width=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>]</para>
19 <para><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
23 <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
24 <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
28 <para><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
31 <para><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></para>
35 <link linkend="tac_contradiction">
36 <emphasis role="bold">contradiction</emphasis>
41 <para><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
45 <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
46 [<emphasis role="bold">(</emphasis>
47 <emphasis><link linkend="grammar.id">id</link></emphasis>…
48 <emphasis role="bold">)</emphasis>]
49 [<emphasis><link linkend="grammar.id">id</link></emphasis>]
50 [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
54 <para><link linkend="tac_demodulation"><emphasis role="bold">demodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
57 <para><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
60 <para><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
63 <para><link linkend="tac_elimType"><emphasis role="bold">elimType</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
66 <para><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
70 <link linkend="tac_exists">
71 <emphasis role="bold">exists</emphasis>
77 <link linkend="tac_fail">
78 <emphasis role="bold">fail</emphasis>
83 <para><link linkend="tac_fold"><emphasis role="bold">fold</emphasis></link> <emphasis><link linkend="grammar.reduction-kind">reduction-kind</link></emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
87 <link linkend="tac_fourier">
88 <emphasis role="bold">fourier</emphasis>
93 <para><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</para>
96 <para><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
100 <link linkend="tac_id">
101 <emphasis role="bold">id</emphasis>
106 <para><link linkend="tac_injection"><emphasis role="bold">injection</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
109 <para><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
112 <para><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
115 <para><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
119 <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
120 [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>]
121 <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
122 [<emphasis role="bold">to</emphasis>
123 <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
124 [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
126 [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
131 <link linkend="tac_left">
132 <emphasis role="bold">left</emphasis>
137 <para><link linkend="tac_letin"><emphasis role="bold">letin</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">≝</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
140 <para><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
143 <para><link linkend="tac_paramodulation"><emphasis role="bold">paramodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
146 <para><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
150 <link linkend="tac_reflexivity">
151 <emphasis role="bold">reflexivity</emphasis>
156 <para><link linkend="tac_replace"><emphasis role="bold">replace</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
159 <para><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
163 <link linkend="tac_right">
164 <emphasis role="bold">right</emphasis>
170 <link linkend="tac_ring">
171 <emphasis role="bold">ring</emphasis>
176 <para><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
180 <link linkend="tac_split">
181 <emphasis role="bold">split</emphasis>
187 <link linkend="tac_symmetry">
188 <emphasis role="bold">symmetry</emphasis>
193 <para><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
196 <para><link linkend="tac_unfold"><emphasis role="bold">unfold</emphasis></link> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
199 <para><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>