1\DOC PRUNE_ONE_CONV
2
3\TYPE {PRUNE_ONE_CONV : (string -> conv)}
4
5\SYNOPSIS
6Prunes a specified hidden variable.
7
8\LIBRARY unwind
9
10\DESCRIBE
11{PRUNE_ONE_CONV `lj`} when applied to the term:
12{
13   "?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp"
14}
15returns a theorem of the form:
16{
17   |- (?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) =
18      (?l1 ... l(j-1) l(j+1) ... lr. t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp)
19}
20where {eq} has the form {"!y1 ... ym. lj x1 ... xn = b"} and {lj}
21does not appear free in the {ti}'s or in {b}. The conversion works if {eq} is
22not present, that is if {lj} is not free in any of the conjuncts, but does not
23work if {lj} appears free in more than one of the conjuncts. Each of {m}, {n}
24and {p} may be zero.
25
26If there is more than one line with the specified name (but with different
27types), the one that appears outermost in the existential quantifications is
28pruned.
29
30\FAILURE
31Fails if the argument term is not of the specified form or if {lj} is free in
32more than one of the conjuncts or if the equation for {lj} is recursive. The
33function also fails if the specified line is not one of the existentially
34quantified lines.
35
36\EXAMPLE
37{
38#PRUNE_ONE_CONV `l2` "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
39|- (?l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (?l1. !x. l1 x = F)
40
41#PRUNE_ONE_CONV `l1` "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
42evaluation failed     PRUNE_ONE_CONV
43}
44\SEEALSO
45unwindLib.PRUNE_ONCE_CONV, unwindLib.PRUNE_SOME_CONV, unwindLib.PRUNE_CONV,
46unwindLib.PRUNE_SOME_RIGHT_RULE, unwindLib.PRUNE_RIGHT_RULE.
47
48\ENDDOC
49