1\DOC UNWIND_ALL_BUT_RIGHT_RULE 2 3\TYPE {UNWIND_ALL_BUT_RIGHT_RULE : (string list -> thm -> thm)} 4 5\SYNOPSIS 6Unwinds all lines of a device (except those in the argument list) as much as 7possible. 8 9\LIBRARY unwind 10 11\DESCRIBE 12{UNWIND_ALL_BUT_RIGHT_RULE l} behaves as follows: 13{ 14 A |- !z1 ... zr. 15 t = 16 (?l1 ... lp. t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn) 17 --------------------------------------------------------------------- 18 A |- !z1 ... zr. 19 t = 20 (?l1 ... lp. t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn') 21} 22where {ti'} (for {1 <= i <= n}) is {ti} rewritten with the equations 23{eqni} ({1 <= i <= m}). These equations are those conjuncts with line name not 24in {l} (and which are equations). 25 26\FAILURE 27Fails if the argument theorem is not of the required form, though either or 28both of {p} and {r} may be zero. May loop indefinitely. 29 30\EXAMPLE 31{ 32#UNWIND_ALL_BUT_RIGHT_RULE [`l2`] 33# (ASSUME 34# "!f. IMP(f) = 35# ?l2 l1. 36# (!(x:num). l1 x = (l2 x) - 1) /\ 37# (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ 38# (!x. l2 x = 7)");; 39. |- !f. 40 IMP f = 41 (?l2 l1. 42 (!x. l1 x = (l2 x) - 1) /\ 43 (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\ 44 (!x. l2 x = 7)) 45} 46\SEEALSO 47unwindLib.UNWIND_AUTO_RIGHT_RULE, unwindLib.UNWIND_ALL_BUT_CONV, 48unwindLib.UNWIND_AUTO_CONV, unwindLib.UNWIND_ONCE_CONV, unwindLib.UNWIND_CONV. 49 50\ENDDOC 51