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