\DOC PRUNE_RIGHT_RULE

\TYPE {PRUNE_RIGHT_RULE : (thm -> thm)}

\SYNOPSIS
Prunes all hidden variables.

\LIBRARY unwind

\DESCRIBE
{PRUNE_RIGHT_RULE} behaves as follows:
{
    A |- !z1 ... zr.
          t = ?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp
   ---------------------------------------------------------------------
                   A |- !z1 ... zr. t = t1 /\ ... /\ tp
}
where each {eqni} has the form {"!y1 ... ym. li x1 ... xn = b"} and
{li} does not appear free in any of the other conjuncts or in {b}. The rule
works if one or more of the {eqni}'s are not present, that is if {li} is not
free in any of the conjuncts, but does not work if {li} appears free in more
than one of the conjuncts. {p} may be zero, that is, all the conjuncts may be
{eqni}'s. In this case the result will be simply {T} (true). Also, for each
{eqni}, {m} and {n} may be zero.

\FAILURE
Fails if the argument theorem is not of the specified form or if any of the
{li}'s are free in more than one of the conjuncts or if the equation for any
{li} is recursive.

\EXAMPLE
{
#PRUNE_RIGHT_RULE
# (ASSUME
#   "!(in:num->bool) (out:num->bool).
#     DEV (in,out) =
#      ?(l1:num->bool) l2.
#       (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");;
. |- !in out. DEV(in,out) = (!x. out x = ~in x)
}
\SEEALSO
unwindLib.PRUNE_SOME_RIGHT_RULE, unwindLib.PRUNE_ONCE_CONV,
unwindLib.PRUNE_ONE_CONV, unwindLib.PRUNE_SOME_CONV, unwindLib.PRUNE_CONV.

\ENDDOC