Reference manual / Z-related commands / Tactic application commands / mu tac

The mu tac built-in tactic applies a proof rule to definite description (\mu) expressions. The definite description expressions must be in antecedent or consequent predicates.

\vdash? \exists1 s @ true, p(\mu s @ e)    | \exists1 s @ true \vdash? \exists s @ p[e/(\mu s @ e)]
\vdash? p(\mu s @ e)

| p(\mu s @ e) \vdash? \exists1 s @ true    | \exists1 s @ true, \exists s @ p[e/(\mu s @ e)] \vdash?
| p(\mu s @ e) \vdash?

The proof rule is not applicable if there are any names in the schema s that refer to declarations that are in p but not in s.

Tactic example

"apply tactic" e2 e3 "mu tac"

This example applies the mu tac built-in tactic to definite description expressions e2 and e3.

IT 28-Dec-2005