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