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