1\DOC PRUNE_ONCE_CONV
2
3\TYPE {PRUNE_ONCE_CONV : conv}
4
5\SYNOPSIS
6Prunes one hidden variable.
7
8\LIBRARY unwind
9
10\DESCRIBE
11{PRUNE_ONCE_CONV "?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp"} returns a
12theorem of the form:
13{
14   |- (?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) =
15      (t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp)
16}
17where {eq} has the form {"!y1 ... ym. l x1 ... xn = b"} and {l} does
18not appear free in the {ti}'s or in {b}. The conversion works if {eq} is not
19present, that is if {l} is not free in any of the conjuncts, but does not work
20if {l} appears free in more than one of the conjuncts. Each of {m}, {n} and {p}
21may be zero.
22
23\FAILURE
24Fails if the argument term is not of the specified form or if {l} is free in
25more than one of the conjuncts or if the equation for {l} is recursive.
26
27\EXAMPLE
28{
29#PRUNE_ONCE_CONV "?l2. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
30|- (?l2. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (!x. l1 x = F)
31}
32\SEEALSO
33unwindLib.PRUNE_ONE_CONV, unwindLib.PRUNE_SOME_CONV, unwindLib.PRUNE_CONV,
34unwindLib.PRUNE_SOME_RIGHT_RULE, unwindLib.PRUNE_RIGHT_RULE.
35
36\ENDDOC
37