<deduction-rule> ::= when <hypothesis>+, yield <conclusion>+,
<hypothesis> ::= <formula> <conclusion> ::= <formula> when x <
y, y < z yield x < z when p /\ q yield p, q when \A e (e \in s1
<=> e \in s2) yield s1 = s2 A deduction rule can be applied to a
formula or rewrite rule if there is a substitution that matches
the first hypothesis of the deduction rule to the formula or
rewrite rule. The result of applying a deduction rule with one
hypothesis is the set of formulas obtained by applying the
substitution(s) that matched its hypothesis to each of its
conclusions. For example, applying the second example to 1 <
f(x) /\ f(x) < 2 yields two formulas, 1 < f(x) and f(x) < 2.
Likewise, applying the third example to x \in s <=> x \in (s \U
s) yields the formula s = s \U s. The result of applying a
deduction rule with more than one hypothesis is the set of
deduction rules obtained by deleting its first hypothesis (i.e.,
the one that was matched) and applying the substitution(s) that
matched this hypothesis to the