Issue a warrant for a function so `apply$` can use it in proofs

It is best to be somewhat familiar with the documentation of `apply$` before reading this topic.

Before using `defun$` that relies
on it:

(include-book "projects/apply/top" :dir :system)

Several lemmas in that book are necessary for

It is easy to confuse badges, which are issued by `defbadge`,
with warrants, which are issued by `defbadge` for an extended discussion.

General Form: (defwarrant fn)

where `defbadge`, which `logic` mode function that is
not already badged. But below we describe all the conditions checked by

Basic conditions include that `logic`-mode and
that its justification (i.e., the measure, well-founded relation, and domain
predicate used to admit `apply$`, `ev$`, or `apply$-userfn`.

**The ``Reachability'' Test** in `defbadge`.
Roughly speaking the test is whether

If the reachability test succeeds — colloquially, if

*(a)* If `natp` or be a
lexicographic combination of natural numbers as defined by the

*(b)* Every function called in the body of `defbadge` and
signal an error if that fails. If some subfunction doesn't already have a
warrant,

*(c)* It must be possible for each formal of

*(d)* Every

This completes the list of additional restrictions imposed by

If the reachability test fails — colloquially, if `sys-call` and other
functions requiring a trust tag. For a list of the blacklisted functions see
the value of

Note that the restrictions imposed on functions from which `ev$` which would possibly
raise termination issues.

Regardless of whether

If the requisite conditions are met, `defbadge` for a brief discussion of how
ilks are computed.

Furthermore, `warrant` for `apply$` on *aka* ``the warrant,'' is
among the hypotheses of the conjecture being proved. The warrant specifies
the values of both `badge-userfn` and `apply$-userfn` and
then `defwarrant` proves rewrite rules to make calls of

If a warrant is issued for `warrant` for details.

You might worry that theorems burdened by warrants are vacuously valid
because it might be impossible to satisfy all the warrant hypotheses. You
needn't worry about this. *There is a model of apply$ and all of its
scions that makes every warrant issued by defwarrant valid.*
The proof of this is sketched in ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore and fully fleshed out in the comment titled

`fn-equal` is a congruence
relation for each

- Fn-equal
- Equivalence relation on tame functions