1272343Sngie\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