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