unwindLib.UNWIND_AUTO_RIGHT

STRUCTURE

SYNOPSIS

Automatic unwinding of equations defining wire values in a standard device specification.

LIBRARY

unwind

DESCRIPTION

UNWIND_AUTO_RIGHT_RULE behaves as follows:

    A |- !z1 ... zr. t = ?l1 ... lm. t1  /\ ... /\ tn
   ----------------------------------------------------
    A |- !z1 ... zr. t = ?l1 ... lm. t1' /\ ... /\ tn'

where tj' is tj rewritten with equations selected from the ti’s.

The function decides which equations to use for rewriting by performing a loop analysis on the graph representing the dependencies of the lines. By this means the term can be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations.

FAILURE

Fails if there is more than one equation for any line variable, or if the argument theorem is not of the required form, though either or both of m and r may be zero.

EXAMPLE

#UNWIND_AUTO_RIGHT_RULE
# (ASSUME
#   "!f. IMP(f) =
#     ?l2 l1.
#      (!(x:num). l1 x = (l2 x) - 1) /\
#      (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#      (!x. l2 x = 7)");;
. |- !f.
      IMP f =
      (?l2 l1.
        (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7))

SEEALSO

UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_CONV, UNWIND_ONCE_CONV, UNWIND_CONV