mu tac

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

$\vdash$ ? $\exists$ ₁ s

true, p( $\mu$ s

e) | $\exists$ ₁ s

true $\vdash$ ? $\exists$ s

p[e/( $\mu$ s

e)]

$\vdash$ ? p( $\mu$ s

| p( $\mu$ s

e) $\vdash$ ? $\exists$ ₁ s

true | $\exists$ ₁ 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" e₂ e₃ "mu tac"

This example applies the mu tac built-in tactic to definite description expressions e₂ and e₃.

IT 28-Dec-2005