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