1\DOC UNWIND_CONV 2 3\TYPE {UNWIND_CONV : ((term -> bool) -> conv)} 4 5\SYNOPSIS 6Unwinds device behaviour using selected line equations until no change. 7 8\LIBRARY unwind 9 10\DESCRIBE 11{UNWIND_CONV p "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn"} returns a 12theorem of the form: 13{ 14 |- t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn = 15 t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn' 16} 17where {ti'} (for {1 <= i <= n}) is {ti} rewritten with the equations 18{eqni} ({1 <= i <= m}). These equations are the conjuncts for which the 19predicate {p} is true. The {ti} terms are the conjuncts for which {p} is false. 20The rewriting is repeated until no changes take place. 21 22\FAILURE 23Never fails but may loop indefinitely. 24 25\EXAMPLE 26{ 27#UNWIND_CONV (\tm. mem (line_name tm) [`l1`;`l2`]) 28# "(!(x:num). l1 x = (l2 x) - 1) /\ 29# (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\ 30# (!x. l2 x = 7)";; 31|- (!x. 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) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7) 35} 36\SEEALSO 37unwindLib.UNWIND_ONCE_CONV, unwindLib.UNWIND_ALL_BUT_CONV, 38unwindLib.UNWIND_AUTO_CONV, unwindLib.UNWIND_ALL_BUT_RIGHT_RULE, 39unwindLib.UNWIND_AUTO_RIGHT_RULE. 40 41\ENDDOC 42