1\DOC PRUNE_SOME_RIGHT_RULE
2
3\TYPE {PRUNE_SOME_RIGHT_RULE : (string list -> thm -> thm)}
4
5\SYNOPSIS
6Prunes several hidden variables.
7
8\LIBRARY unwind
9
10\DESCRIBE
11{PRUNE_SOME_RIGHT_RULE [`li1`;...;`lik`]} behaves as follows:
12{
13    A |- !z1 ... zr.
14          t = ?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp
15   -----------------------------------------------------------------------
16           A |- !z1 ... zr. t = ?li(k+1) ... lir. t1 /\ ... /\ tp
17}
18where for {1 <= j <= k}, each {eqnij} has the form:
19{
20   "!y1 ... ym. lij x1 ... xn = b"
21}
22and {lij} does not appear free in any of the other conjuncts or in
23{b}. The {li}'s are related by the equation:
24{
25   {{li1,...,lik}} u {{li(k+1),...,lir}} = {{l1,...,lr}}
26}
27The rule works if one or more of the {eqnij}'s are not present, that
28is if {lij} is not free in any of the conjuncts, but does not work if {lij}
29appears free in more than one of the conjuncts. {p} may be zero, that is, all
30the conjuncts may be {eqnij}'s. In this case the conjunction will be
31transformed to {T} (true). Also, for each {eqnij}, {m} and {n} may be zero.
32
33If there is more than one line with a specified name (but with different
34types), the one that appears outermost in the existential quantifications is
35pruned. If such a line name is mentioned twice in the list, the two outermost
36occurrences of lines with that name will be pruned, and so on.
37
38\FAILURE
39Fails if the argument theorem is not of the specified form or if any of the
40{lij}'s are free in more than one of the conjuncts or if the equation for any
41{lij} is recursive. The function also fails if any of the specified lines are
42not one of the existentially quantified lines.
43
44\EXAMPLE
45{
46#PRUNE_SOME_RIGHT_RULE [`l1`;`l2`]
47# (ASSUME
48#   "!(in:num->bool) (out:num->bool).
49#     DEV (in,out) =
50#      ?(l1:num->bool) l2.
51#       (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");;
52. |- !in out. DEV(in,out) = (!x. out x = ~in x)
53}
54\SEEALSO
55unwindLib.PRUNE_RIGHT_RULE, unwindLib.PRUNE_ONCE_CONV,
56unwindLib.PRUNE_ONE_CONV, unwindLib.PRUNE_SOME_CONV, unwindLib.PRUNE_CONV.
57
58\ENDDOC
59