1\DOC PRUNE_RIGHT_RULE
2
3\TYPE {PRUNE_RIGHT_RULE : (thm -> thm)}
4
5\SYNOPSIS
6Prunes all hidden variables.
7
8\LIBRARY unwind
9
10\DESCRIBE
11{PRUNE_RIGHT_RULE} behaves as follows:
12{
13    A |- !z1 ... zr.
14          t = ?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp
15   ---------------------------------------------------------------------
16                   A |- !z1 ... zr. t = t1 /\ ... /\ tp
17}
18where each {eqni} has the form {"!y1 ... ym. li x1 ... xn = b"} and
19{li} does not appear free in any of the other conjuncts or in {b}. The rule
20works if one or more of the {eqni}'s are not present, that is if {li} is not
21free in any of the conjuncts, but does not work if {li} appears free in more
22than one of the conjuncts. {p} may be zero, that is, all the conjuncts may be
23{eqni}'s. In this case the result will be simply {T} (true). Also, for each
24{eqni}, {m} and {n} may be zero.
25
26\FAILURE
27Fails if the argument theorem is not of the specified form or if any of the
28{li}'s are free in more than one of the conjuncts or if the equation for any
29{li} is recursive.
30
31\EXAMPLE
32{
33#PRUNE_RIGHT_RULE
34# (ASSUME
35#   "!(in:num->bool) (out:num->bool).
36#     DEV (in,out) =
37#      ?(l1:num->bool) l2.
38#       (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");;
39. |- !in out. DEV(in,out) = (!x. out x = ~in x)
40}
41\SEEALSO
42unwindLib.PRUNE_SOME_RIGHT_RULE, unwindLib.PRUNE_ONCE_CONV,
43unwindLib.PRUNE_ONE_CONV, unwindLib.PRUNE_SOME_CONV, unwindLib.PRUNE_CONV.
44
45\ENDDOC
46