PRUNE_ONCE_CONV : conv
STRUCTURE
unwindLib
SYNOPSIS
Prunes one hidden variable.
LIBRARY
unwind
DESCRIPTION
PRUNE_ONCE_CONV "?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp" returns a theorem of the form: 
   |- (?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) =
      (t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp)
where eq has the form "!y1 ... ym. l x1 ... xn = b" and l does not appear free in the ti’s or in b. The conversion works if eq is not present, that is if l is not free in any of the conjuncts, but does not work if l appears free in more than one of the conjuncts. Each of m, n and p may be zero.
FAILURE
Fails if the argument term is not of the specified form or if l is free in more than one of the conjuncts or if the equation for l is recursive.
EXAMPLE
#PRUNE_ONCE_CONV "?l2. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
|- (?l2. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (!x. l1 x = F)
SEEALSO
PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE, PRUNE_RIGHT_RULE
HOL  Trindemossen-1