1\DOC UNWIND_AUTO_RIGHT_RULE
2
3\TYPE {UNWIND_AUTO_RIGHT_RULE : (thm -> thm)}
4
5\SYNOPSIS
6Automatic unwinding of equations defining wire values in a standard device
7specification.
8
9\LIBRARY unwind
10
11\DESCRIBE
12{UNWIND_AUTO_RIGHT_RULE} behaves as follows:
13{
14    A |- !z1 ... zr. t = ?l1 ... lm. t1  /\ ... /\ tn
15   ----------------------------------------------------
16    A |- !z1 ... zr. t = ?l1 ... lm. t1' /\ ... /\ tn'
17}
18where {tj'} is {tj} rewritten with equations selected from the
19{ti}'s.
20
21The function decides which equations to use for rewriting by performing a loop
22analysis on the graph representing the dependencies of the lines. By this means
23the term can be unwound as much as possible without the risk of looping. The
24user is left to deal with the recursive equations.
25
26\FAILURE
27Fails if there is more than one equation for any line variable, or if the
28argument theorem is not of the required form, though either or both of {m} and
29{r} may be zero.
30
31\EXAMPLE
32{
33#UNWIND_AUTO_RIGHT_RULE
34# (ASSUME
35#   "!f. IMP(f) =
36#     ?l2 l1.
37#      (!(x:num). l1 x = (l2 x) - 1) /\
38#      (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
39#      (!x. l2 x = 7)");;
40. |- !f.
41      IMP f =
42      (?l2 l1.
43        (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7))
44}
45\SEEALSO
46unwindLib.UNWIND_ALL_BUT_RIGHT_RULE, unwindLib.UNWIND_AUTO_CONV,
47unwindLib.UNWIND_ALL_BUT_CONV, unwindLib.UNWIND_ONCE_CONV,
48unwindLib.UNWIND_CONV.
49
50\ENDDOC
51