1\DOC UNWIND_ALL_BUT_CONV 2 3\TYPE {UNWIND_ALL_BUT_CONV : (string list -> conv)} 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_CONV l} when applied to the following term: 13{ 14 "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn" 15} 16returns a theorem of the form: 17{ 18 |- t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn = 19 t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn' 20} 21where {ti'} (for {1 <= i <= n}) is {ti} rewritten with the equations 22{eqni} ({1 <= i <= m}). These equations are those conjuncts with line name not 23in {l} (and which are equations). 24 25\FAILURE 26Never fails but may loop indefinitely. 27 28\EXAMPLE 29{ 30#UNWIND_ALL_BUT_CONV [`l2`] 31# "(!(x:num). l1 x = (l2 x) - 1) /\ 32# (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ 33# (!x. l2 x = 7)";; 34|- (!x. l1 x = (l2 x) - 1) /\ 35 (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\ 36 (!x. l2 x = 7) = 37 (!x. l1 x = (l2 x) - 1) /\ 38 (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\ 39 (!x. l2 x = 7) 40} 41\SEEALSO 42unwindLib.UNWIND_ONCE_CONV, unwindLib.UNWIND_CONV, unwindLib.UNWIND_AUTO_CONV, 43unwindLib.UNWIND_ALL_BUT_RIGHT_RULE, unwindLib.UNWIND_AUTO_RIGHT_RULE. 44 45\ENDDOC 46