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