1\DOC UNWIND_AUTO_CONV
2
3\TYPE {UNWIND_AUTO_CONV : conv}
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_CONV "?l1 ... lm. t1 /\ ... /\ tn"} returns a theorem of the form:
13{
14   |- (?l1 ... lm. t1 /\ ... /\ tn) = (?l1 ... lm. t1' /\ ... /\ tn')
15}
16where {tj'} is {tj} rewritten with equations selected from the
17{ti}'s.
18
19The function decides which equations to use for rewriting by performing a loop
20analysis on the graph representing the dependencies of the lines. By this means
21the term can be unwound as much as possible without the risk of looping. The
22user is left to deal with the recursive equations.
23
24\FAILURE
25Fails if there is more than one equation for any line variable.
26
27\EXAMPLE
28{
29#UNWIND_AUTO_CONV
30# "(!(x:num). l1 x = (l2 x) - 1) /\
31#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
32#  (!x. l2 x = 7)";;
33|- (!x. l1 x = (l2 x) - 1) /\
34   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
35   (!x. l2 x = 7) =
36   (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7)
37}
38\SEEALSO
39unwindLib.UNWIND_ONCE_CONV, unwindLib.UNWIND_CONV,
40unwindLib.UNWIND_ALL_BUT_CONV, unwindLib.UNWIND_ALL_BUT_RIGHT_RULE,
41unwindLib.UNWIND_AUTO_RIGHT_RULE.
42
43\ENDDOC
44