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