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