\chapter{ML Functions in the unwind Library}\input{entries-intro}\DOC{CONJ\_FORALL\_CONV}

\TYPE {\small\verb%CONJ_FORALL_CONV : conv%}\egroup

\SYNOPSIS
Moves universal quantifiers up through a tree of conjunctions.

\DESCRIBE
{\small\verb%CONJ_FORALL_CONV "(!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)"%} returns the
following theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) =
      !x1 ... xm. t1 /\ ... /\ tn
\end{verbatim}
}
\noindent where the original term can be an arbitrary tree of conjunctions. The
structure of the tree is retained in both sides of the equation.

\FAILURE
Never fails.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#CONJ_FORALL_CONV "((!(x:*) (y:*) (z:*). a) /\ (!(x:*) (y:*) (z:*). b)) /\
#                  (!(x:*) (y:*) (z:*). c)";;
|- ((!x y z. a) /\ (!x y z. b)) /\ (!x y z. c) = (!x y z. (a /\ b) /\ c)

#CONJ_FORALL_CONV "T";;
|- T = T

#CONJ_FORALL_CONV "((!(x:*) (y:*) (z:*). a) /\ (!(x:*) (w:*) (z:*). b)) /\
#                  (!(x:*) (y:*) (z:*). c)";;
|- ((!x y z. a) /\ (!x w z. b)) /\ (!x y z. c) =
   (!x. ((!y z. a) /\ (!w z. b)) /\ (!y z. c))
\end{verbatim}
}
\SEEALSO
FORALL_CONJ_CONV, CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV,
CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_RIGHT_RULE.

\ENDDOC
\DOC{CONJ\_FORALL\_ONCE\_CONV}

\TYPE {\small\verb%CONJ_FORALL_ONCE_CONV : conv%}\egroup

\SYNOPSIS
Moves a single universal quantifier up through a tree of conjunctions.

\DESCRIBE
{\small\verb%CONJ_FORALL_ONCE_CONV "(!x. t1) /\ ... /\ (!x. tn)"%} returns the theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (!x. t1) /\ ... /\ (!x. tn) = !x. t1 /\ ... /\ tn
\end{verbatim}
}
\noindent where the original term can be an arbitrary tree of conjunctions. The
structure of the tree is retained in both sides of the equation.

\FAILURE
Fails if the argument term is not of the required form. The term need not be a
conjunction, but if it is every conjunct must be universally quantified with
the same variable.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#CONJ_FORALL_ONCE_CONV "((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c)";;
|- ((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c) =
   (!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c))

#CONJ_FORALL_ONCE_CONV "!x. x \/ a";;
|- (!x. x \/ a) = (!x. x \/ a)

#CONJ_FORALL_ONCE_CONV "((!x. x \/ a) /\ (!y. y \/ b)) /\ (!x. x \/ c)";;
evaluation failed     CONJ_FORALL_ONCE_CONV
\end{verbatim}
}
\SEEALSO
FORALL_CONJ_ONCE_CONV, CONJ_FORALL_CONV, FORALL_CONJ_CONV,
CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_RIGHT_RULE.

\ENDDOC
\DOC{CONJ\_FORALL\_RIGHT\_RULE}

\TYPE {\small\verb%CONJ_FORALL_RIGHT_RULE : (thm -> thm)%}\egroup

\SYNOPSIS
Moves universal quantifiers up through a tree of conjunctions.

\DESCRIBE
{\par\samepage\setseps\small
\begin{verbatim}
    A |- !z1 ... zr.
          t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)
   -------------------------------------------------------------------
      A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn
\end{verbatim}
}

\FAILURE
Fails if the argument theorem is not of the required form, though either or
both of {\small\verb%r%} and {\small\verb%p%} may be zero.

\SEEALSO
FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_CONV, FORALL_CONJ_CONV,
CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV.

\ENDDOC
\DOC{DEPTH\_EXISTS\_CONV}

\TYPE {\small\verb%DEPTH_EXISTS_CONV : (conv -> conv)%}\egroup

\SYNOPSIS
Applies a conversion to the body of nested existential quantifications.

\DESCRIBE
{\small\verb%DEPTH_EXISTS_CONV conv "?x1 ... xn. body"%} applies {\small\verb%conv%} to {\small\verb%"body"%} and
returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?x1 ... xn. body) = (?x1 ... xn. body')
\end{verbatim}
}

\FAILURE
Fails if the application of {\small\verb%conv%} fails.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#DEPTH_EXISTS_CONV BETA_CONV "?x y z. (\w. x /\ y /\ z /\ w) T";;
|- (?x y z. (\w. x /\ y /\ z /\ w)T) = (?x y z. x /\ y /\ z /\ T)
\end{verbatim}
}
\SEEALSO
DEPTH_FORALL_CONV.

\ENDDOC
\DOC{DEPTH\_FORALL\_CONV}

\TYPE {\small\verb%DEPTH_FORALL_CONV : (conv -> conv)%}\egroup

\SYNOPSIS
Applies a conversion to the body of nested universal quantifications.

\DESCRIBE
{\small\verb%DEPTH_FORALL_CONV conv "!x1 ... xn. body"%} applies {\small\verb%conv%} to {\small\verb%"body"%} and
returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (!x1 ... xn. body) = (!x1 ... xn. body')
\end{verbatim}
}

\FAILURE
Fails if the application of {\small\verb%conv%} fails.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#DEPTH_FORALL_CONV BETA_CONV "!x y z. (\w. x /\ y /\ z /\ w) T";;
|- (!x y z. (\w. x /\ y /\ z /\ w)T) = (!x y z. x /\ y /\ z /\ T)
\end{verbatim}
}
\SEEALSO
DEPTH_EXISTS_CONV.

\ENDDOC
\DOC{EXISTS\_DEL1\_CONV}

\TYPE {\small\verb%EXISTS_DEL1_CONV : conv%}\egroup

\SYNOPSIS
Deletes one existential quantifier.

\DESCRIBE
{\small\verb%EXISTS_DEL1_CONV "?x. t"%} returns the theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?x. t) = t
\end{verbatim}
}
\noindent provided {\small\verb%x%} is not free in {\small\verb%t%}.

\FAILURE
Fails if the argument term is not an existential quantification or if {\small\verb%x%} is
free in {\small\verb%t%}.

\SEEALSO
EXISTS_DEL_CONV, PRUNE_ONCE_CONV.

\ENDDOC
\DOC{EXISTS\_DEL\_CONV}

\TYPE {\small\verb%EXISTS_DEL_CONV : conv%}\egroup

\SYNOPSIS
Deletes existential quantifiers.

\DESCRIBE
{\small\verb%EXISTS_DEL_CONV "?x1 ... xn. t"%} returns the theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?x1 ... xn. t) = t
\end{verbatim}
}
\noindent provided {\small\verb%x1,...,xn%} are not free in {\small\verb%t%}.

\FAILURE
Fails if any of the {\small\verb%x%}'s appear free in {\small\verb%t%}. The function does not perform a
partial deletion; for example, if {\small\verb%x1%} and {\small\verb%x2%} do not appear free in {\small\verb%t%} but
{\small\verb%x3%} does, the function will fail; it will not return:
{\par\samepage\setseps\small
\begin{verbatim}
   |- ?x1 ... xn. t = ?x3 ... xn. t
\end{verbatim}
}
\SEEALSO
EXISTS_DEL1_CONV, PRUNE_CONV.

\ENDDOC
\DOC{EXISTS\_EQN\_CONV}

\TYPE {\small\verb%EXISTS_EQN_CONV : conv%}\egroup

\SYNOPSIS
Proves the existence of a line that has a non-recursive equation.

\DESCRIBE
{\small\verb%EXISTS_EQN_CONV "?l. !y1 ... ym. l x1 ... xn = t"%} returns the theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?l. !y1 ... ym. l x1 ... xn = t) = T
\end{verbatim}
}
\noindent provided {\small\verb%l%} is not free in {\small\verb%t%}. Both {\small\verb%m%} and {\small\verb%n%} may be zero.

\FAILURE
Fails if the argument term is not of the specified form or if {\small\verb%l%} appears free
in {\small\verb%t%}.

\SEEALSO
PRUNE_ONCE_CONV.

\ENDDOC
\DOC{EXPAND\_ALL\_BUT\_CONV}

\TYPE {\small\verb%EXPAND_ALL_BUT_CONV : (string list -> thm list -> conv)%}\egroup

\SYNOPSIS
Unfolds, then unwinds all lines (except those specified) as much as possible,
then prunes the unwound lines.

\DESCRIBE
{\small\verb%EXPAND_ALL_BUT_CONV [`li(k+1)`;...;`lim`] thl%} when applied to the following
term:
{\par\samepage\setseps\small
\begin{verbatim}
   "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn"
\end{verbatim}
}
\noindent returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) =
        (?li(k+1) ... lim. t1' /\ ... /\ tn')
\end{verbatim}
}
\noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in
{\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions
of the theorems used for rewriting. If none of the rewrites are applicable to a
conjunct, it is unchanged. Those conjuncts that after rewriting are equations
for the lines {\small\verb%li1,...,lik%} (they are denoted by {\small\verb%ui1,...,uik%}) are used to
unwind and the lines {\small\verb%li1,...,lik%} are then pruned.

The {\small\verb%li%}'s are related by the equation:
{\par\samepage\setseps\small
\begin{verbatim}
   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}
\end{verbatim}
}

\FAILURE
The function may fail if the argument term is not of the specified form. It
will also fail if the unwound lines cannot be pruned. It is possible for the
function to attempt unwinding indefinitely (to loop).

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#EXPAND_ALL_BUT_CONV [`l1`]
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# "?l1 l2.
#   INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";;
. |- (?l1 l2.
       INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) =
     (?l1.
       (!t. out t = ~~l1 t) /\ (!t. l1 t = ~l1(t - 1) \/ ~~l1(t - 1)))
\end{verbatim}
}
\SEEALSO
EXPAND_AUTO_CONV, EXPAND_ALL_BUT_RIGHT_RULE, EXPAND_AUTO_RIGHT_RULE,
UNFOLD_CONV, UNWIND_ALL_BUT_CONV, PRUNE_SOME_CONV.

\ENDDOC
\DOC{EXPAND\_ALL\_BUT\_RIGHT\_RULE}

\TYPE {\small\verb%EXPAND_ALL_BUT_RIGHT_RULE : (string list -> thm list -> thm -> thm)%}\egroup

\SYNOPSIS
Unfolds, then unwinds all lines (except those specified) as much as possible,
then prunes the unwound lines.

\DESCRIBE
{\small\verb%EXPAND_ALL_BUT_RIGHT_RULE [`li(k+1)`;...;`lim`] thl%} behaves as follows:
{\par\samepage\setseps\small
\begin{verbatim}
    A |- !z1 ... zr.
          t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn
   -------------------------------------------------------------------
       B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn'
\end{verbatim}
}
\noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in
{\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions
of the theorems used for rewriting. If none of the rewrites are applicable to a
conjunct, it is unchanged. Those conjuncts that after rewriting are equations
for the lines {\small\verb%li1,...,lik%} (they are denoted by {\small\verb%ui1,...,uik%}) are used to
unwind and the lines {\small\verb%li1,...,lik%} are then pruned.

The {\small\verb%li%}'s are related by the equation:
{\par\samepage\setseps\small
\begin{verbatim}
   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}
\end{verbatim}
}

\FAILURE
The function may fail if the argument theorem is not of the specified form. It
will also fail if the unwound lines cannot be pruned. It is possible for the
function to attempt unwinding indefinitely (to loop).

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#EXPAND_ALL_BUT_RIGHT_RULE [`l1`]
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# (ASSUME
#   "!(in:num->bool) out.
#     DEV(in,out) =
#      ?l1 l2.
#       INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");;
.. |- !in out.
       DEV(in,out) =
       (?l1. (!t. out t = ~~l1 t) /\ (!t. l1 t = in t \/ ~~l1(t - 1)))
\end{verbatim}
}
\SEEALSO
EXPAND_AUTO_RIGHT_RULE, EXPAND_ALL_BUT_CONV, EXPAND_AUTO_CONV,
UNFOLD_RIGHT_RULE, UNWIND_ALL_BUT_RIGHT_RULE, PRUNE_SOME_RIGHT_RULE.

\ENDDOC
\DOC{EXPAND\_AUTO\_CONV}

\TYPE {\small\verb%EXPAND_AUTO_CONV : (thm list -> conv)%}\egroup

\SYNOPSIS
Unfolds, then unwinds as much as possible, then prunes the unwound lines.

\DESCRIBE
{\small\verb%EXPAND_AUTO_CONV thl%} when applied to the following term:
{\par\samepage\setseps\small
\begin{verbatim}
   "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn"
\end{verbatim}
}
\noindent returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) =
        (?li(k+1) ... lim. t1' /\ ... /\ tn')
\end{verbatim}
}
\noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in
{\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions
of the theorems used for rewriting. If none of the rewrites are applicable to a
conjunct, it is unchanged. After rewriting, the function decides which of the
resulting terms to use for unwinding, by performing a loop analysis on the
graph representing the dependencies of the lines.

Suppose the function decides to unwind {\small\verb%li1,...,lik%} using the terms
{\small\verb%ui1',...,uik'%} respectively. Then, after unwinding, the lines {\small\verb%li1,...,lik%}
are pruned (provided they have been eliminated from the right-hand sides of the
conjuncts that are equations, and from the whole of any other conjuncts)
resulting in the elimination of {\small\verb%ui1',...,uik'%}.

The {\small\verb%li%}'s are related by the equation:
{\par\samepage\setseps\small
\begin{verbatim}
   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}
\end{verbatim}
}
\noindent The loop analysis allows the term to be unwound as much as possible
without the risk of looping. The user is left to deal with the recursive
equations.

\FAILURE
The function may fail if the argument term is not of the specified form. It
also fails if there is more than one equation for any line variable.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#EXPAND_AUTO_CONV
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# "?l1 l2.
#   INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";;
. |- (?l1 l2.
       INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) =
     (?l1.
       (!t. out t = ~~l1 t) /\ (!t. l1 t = ~l1(t - 1) \/ ~~l1(t - 1)))
\end{verbatim}
}
\SEEALSO
EXPAND_ALL_BUT_CONV, EXPAND_AUTO_RIGHT_RULE, EXPAND_ALL_BUT_RIGHT_RULE,
UNFOLD_CONV, UNWIND_AUTO_CONV, PRUNE_SOME_CONV.

\ENDDOC
\DOC{EXPAND\_AUTO\_RIGHT\_RULE}

\TYPE {\small\verb%EXPAND_AUTO_RIGHT_RULE : (thm list -> thm -> thm)%}\egroup

\SYNOPSIS
Unfolds, then unwinds as much as possible, then prunes the unwound lines.

\DESCRIBE
{\small\verb%EXPAND_AUTO_RIGHT_RULE thl%} behaves as follows:
{\par\samepage\setseps\small
\begin{verbatim}
    A |- !z1 ... zr.
          t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn
   -------------------------------------------------------------------
      B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn'
\end{verbatim}
}
\noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in
{\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions
of the theorems used for rewriting. If none of the rewrites are applicable to a
conjunct, it is unchanged. After rewriting, the function decides which of the
resulting terms to use for unwinding, by performing a loop analysis on the
graph representing the dependencies of the lines.

Suppose the function decides to unwind {\small\verb%li1,...,lik%} using the terms
{\small\verb%ui1',...,uik'%} respectively. Then, after unwinding, the lines {\small\verb%li1,...,lik%}
are pruned (provided they have been eliminated from the right-hand sides of
the conjuncts that are equations, and from the whole of any other conjuncts)
resulting in the elimination of {\small\verb%ui1',...,uik'%}.

The {\small\verb%li%}'s are related by the equation:
{\par\samepage\setseps\small
\begin{verbatim}
   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}
\end{verbatim}
}
\noindent The loop analysis allows the term to be unwound as much as possible
without the risk of looping. The user is left to deal with the recursive
equations.

\FAILURE
The function may fail if the argument theorem is not of the specified form. It
also fails if there is more than one equation for any line variable.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#EXPAND_AUTO_RIGHT_RULE
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# (ASSUME
#   "!(in:num->bool) out.
#     DEV(in,out) =
#      ?l1 l2.
#       INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");;
.. |- !in out. DEV(in,out) = (!t. out t = ~~(in t \/ out(t - 1)))
\end{verbatim}
}
\SEEALSO
EXPAND_ALL_BUT_RIGHT_RULE, EXPAND_AUTO_CONV, EXPAND_ALL_BUT_CONV,
UNFOLD_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE, PRUNE_SOME_RIGHT_RULE.

\ENDDOC
\DOC{FLATTEN\_CONJ\_CONV}

\TYPE {\small\verb%FLATTEN_CONJ_CONV : conv%}\egroup

\SYNOPSIS
Flattens a `tree' of conjunctions.

\DESCRIBE
{\small\verb%FLATTEN_CONJ_CONV "t1 /\ ... /\ tn"%} returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- t1 /\ ... /\ tn = u1 /\ ... /\ un
\end{verbatim}
}
\noindent where the right-hand side of the equation is a flattened version of
the left-hand side.

\FAILURE
Never fails.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#FLATTEN_CONJ_CONV "(a /\ (b /\ c)) /\ ((d /\ e) /\ f)";;
|- (a /\ b /\ c) /\ (d /\ e) /\ f = a /\ b /\ c /\ d /\ e /\ f
\end{verbatim}
}
\SEEALSO
CONJUNCTS_CONV.

\ENDDOC
\DOC{FORALL\_CONJ\_CONV}

\TYPE {\small\verb%FORALL_CONJ_CONV : conv%}\egroup

\SYNOPSIS
Moves universal quantifiers down through a tree of conjunctions.

\DESCRIBE
{\small\verb%FORALL_CONJ_CONV "!x1 ... xm. t1 /\ ... /\ tn"%} returns the theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   |- !x1 ... xm. t1 /\ ... /\ tn =
      (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)
\end{verbatim}
}
\noindent where the original term can be an arbitrary tree of conjunctions. The
structure of the tree is retained in both sides of the equation.

\FAILURE
Never fails.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). (a /\ b) /\ c";;
|- (!x y z. (a /\ b) /\ c) = ((!x y z. a) /\ (!x y z. b)) /\ (!x y z. c)

#FORALL_CONJ_CONV "T";;
|- T = T

#FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). T";;
|- (!x y z. T) = (!x y z. T)
\end{verbatim}
}
\SEEALSO
CONJ_FORALL_CONV, FORALL_CONJ_ONCE_CONV, CONJ_FORALL_ONCE_CONV,
FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_RIGHT_RULE.

\ENDDOC
\DOC{FORALL\_CONJ\_ONCE\_CONV}

\TYPE {\small\verb%FORALL_CONJ_ONCE_CONV : conv%}\egroup

\SYNOPSIS
Moves a single universal quantifier down through a tree of conjunctions.

\DESCRIBE
{\small\verb%FORALL_CONJ_ONCE_CONV "!x. t1 /\ ... /\ tn"%} returns the theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   |- !x. t1 /\ ... /\ tn = (!x. t1) /\ ... /\ (!x. tn)
\end{verbatim}
}
\noindent where the original term can be an arbitrary tree of conjunctions. The
structure of the tree is retained in both sides of the equation.

\FAILURE
Fails if the argument term is not of the required form. The body of the term
need not be a conjunction.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#FORALL_CONJ_ONCE_CONV "!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c)";;
|- (!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c)) =
   ((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c)

#FORALL_CONJ_ONCE_CONV "!x. x \/ a";;
|- (!x. x \/ a) = (!x. x \/ a)

#FORALL_CONJ_ONCE_CONV "!x. ((x \/ a) /\ (y \/ b)) /\ (x \/ c)";;
|- (!x. ((x \/ a) /\ (y \/ b)) /\ (x \/ c)) =
   ((!x. x \/ a) /\ (!x. y \/ b)) /\ (!x. x \/ c)
\end{verbatim}
}
\SEEALSO
CONJ_FORALL_ONCE_CONV, FORALL_CONJ_CONV, CONJ_FORALL_CONV,
FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_RIGHT_RULE.

\ENDDOC
\DOC{FORALL\_CONJ\_RIGHT\_RULE}

\TYPE {\small\verb%FORALL_CONJ_RIGHT_RULE : (thm -> thm)%}\egroup

\SYNOPSIS
Moves universal quantifiers down through a tree of conjunctions.

\DESCRIBE
{\par\samepage\setseps\small
\begin{verbatim}
      A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn
   -------------------------------------------------------------------
    A |- !z1 ... zr.
          t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)
\end{verbatim}
}

\FAILURE
Fails if the argument theorem is not of the required form, though either or
both of {\small\verb%r%} and {\small\verb%p%} may be zero.

\SEEALSO
CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_CONV, CONJ_FORALL_CONV,
FORALL_CONJ_ONCE_CONV, CONJ_FORALL_ONCE_CONV.

\ENDDOC
\DOC{line\_name}

\TYPE {\small\verb%line_name : (term -> string)%}\egroup

\SYNOPSIS
Computes the line name of an equation.

\DESCRIBE
{\small\verb%line_name "!y1 ... ym. f x1 ... xn = t"%} returns the string {\small\verb%`f`%}.

\FAILURE
Fails if the argument term is not of the specified form.

\SEEALSO
line_var.

\ENDDOC
\DOC{line\_var}

\TYPE {\small\verb%line_var : (term -> term)%}\egroup

\SYNOPSIS
Computes the line variable of an equation.

\DESCRIBE
{\small\verb%line_var "!y1 ... ym. f x1 ... xn = t"%} returns the variable {\small\verb%"f"%}.

\FAILURE
Fails if the argument term is not of the specified form.

\SEEALSO
line_name.

\ENDDOC
\DOC{PRUNE\_CONV}

\TYPE {\small\verb%PRUNE_CONV : conv%}\egroup

\SYNOPSIS
Prunes all hidden variables.

\DESCRIBE
{\small\verb%PRUNE_CONV "?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp"%}
returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp) =
      (t1 /\ ... /\ tp)
\end{verbatim}
}
\noindent where each {\small\verb%eqni%} has the form {\small\verb%"!y1 ... ym. li x1 ... xn = b"%} and
{\small\verb%li%} does not appear free in any of the other conjuncts or in {\small\verb%b%}. The
conversion works if one or more of the {\small\verb%eqni%}'s are not present, that is if
{\small\verb%li%} is not free in any of the conjuncts, but does not work if {\small\verb%li%} appears
free in more than one of the conjuncts. {\small\verb%p%} may be zero, that is, all the
conjuncts may be {\small\verb%eqni%}'s. In this case the result will be simply {\small\verb%T%} (true).
Also, for each {\small\verb%eqni%}, {\small\verb%m%} and {\small\verb%n%} may be zero.

\FAILURE
Fails if the argument term is not of the specified form or if any of the
{\small\verb%li%}'s are free in more than one of the conjuncts or if the equation for any
{\small\verb%li%} is recursive.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PRUNE_CONV
# "?l2 l1.
#   (!(x:num). l1 x = F) /\ (!x. l2 x = ~(out x)) /\ (!(x:num). out x = T)";;
|- (?l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~out x) /\ (!x. out x = T)) =
   (!x. out x = T)
\end{verbatim}
}
\SEEALSO
PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

\ENDDOC
\DOC{PRUNE\_ONCE\_CONV}

\TYPE {\small\verb%PRUNE_ONCE_CONV : conv%}\egroup

\SYNOPSIS
Prunes one hidden variable.

\DESCRIBE
{\small\verb%PRUNE_ONCE_CONV "?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp"%} returns a
theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) =
      (t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp)
\end{verbatim}
}
\noindent where {\small\verb%eq%} has the form {\small\verb%"!y1 ... ym. l x1 ... xn = b"%} and {\small\verb%l%} does
not appear free in the {\small\verb%ti%}'s or in {\small\verb%b%}. The conversion works if {\small\verb%eq%} is not
present, that is if {\small\verb%l%} is not free in any of the conjuncts, but does not work
if {\small\verb%l%} appears free in more than one of the conjuncts. Each of {\small\verb%m%}, {\small\verb%n%} and {\small\verb%p%}
may be zero.

\FAILURE
Fails if the argument term is not of the specified form or if {\small\verb%l%} is free in
more than one of the conjuncts or if the equation for {\small\verb%l%} is recursive.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PRUNE_ONCE_CONV "?l2. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";; 
|- (?l2. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (!x. l1 x = F)
\end{verbatim}
}
\SEEALSO
PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

\ENDDOC
\DOC{PRUNE\_ONE\_CONV}

\TYPE {\small\verb%PRUNE_ONE_CONV : (string -> conv)%}\egroup

\SYNOPSIS
Prunes a specified hidden variable.

\DESCRIBE
{\small\verb%PRUNE_ONE_CONV `lj`%} when applied to the term:
{\par\samepage\setseps\small
\begin{verbatim}
   "?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp"
\end{verbatim}
}
\noindent returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) =
      (?l1 ... l(j-1) l(j+1) ... lr. t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp)
\end{verbatim}
}
\noindent where {\small\verb%eq%} has the form {\small\verb%"!y1 ... ym. lj x1 ... xn = b"%} and {\small\verb%lj%}
does not appear free in the {\small\verb%ti%}'s or in {\small\verb%b%}. The conversion works if {\small\verb%eq%} is
not present, that is if {\small\verb%lj%} is not free in any of the conjuncts, but does not
work if {\small\verb%lj%} appears free in more than one of the conjuncts. Each of {\small\verb%m%}, {\small\verb%n%}
and {\small\verb%p%} may be zero.

If there is more than one line with the specified name (but with different
types), the one that appears outermost in the existential quantifications is
pruned.

\FAILURE
Fails if the argument term is not of the specified form or if {\small\verb%lj%} is free in
more than one of the conjuncts or if the equation for {\small\verb%lj%} is recursive. The
function also fails if the specified line is not one of the existentially
quantified lines.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PRUNE_ONE_CONV `l2` "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
|- (?l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (?l1. !x. l1 x = F)

#PRUNE_ONE_CONV `l1` "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";; 
evaluation failed     PRUNE_ONE_CONV
\end{verbatim}
}
\SEEALSO
PRUNE_ONCE_CONV, PRUNE_SOME_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

\ENDDOC
\DOC{PRUNE\_RIGHT\_RULE}

\TYPE {\small\verb%PRUNE_RIGHT_RULE : (thm -> thm)%}\egroup

\SYNOPSIS
Prunes all hidden variables.

\DESCRIBE
{\small\verb%PRUNE_RIGHT_RULE%} behaves as follows:
{\par\samepage\setseps\small
\begin{verbatim}
    A |- !z1 ... zr.
          t = ?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp
   ---------------------------------------------------------------------
                   A |- !z1 ... zr. t = t1 /\ ... /\ tp
\end{verbatim}
}
\noindent where each {\small\verb%eqni%} has the form {\small\verb%"!y1 ... ym. li x1 ... xn = b"%} and
{\small\verb%li%} does not appear free in any of the other conjuncts or in {\small\verb%b%}. The rule
works if one or more of the {\small\verb%eqni%}'s are not present, that is if {\small\verb%li%} is not
free in any of the conjuncts, but does not work if {\small\verb%li%} appears free in more
than one of the conjuncts. {\small\verb%p%} may be zero, that is, all the conjuncts may be
{\small\verb%eqni%}'s. In this case the result will be simply {\small\verb%T%} (true). Also, for each
{\small\verb%eqni%}, {\small\verb%m%} and {\small\verb%n%} may be zero.

\FAILURE
Fails if the argument theorem is not of the specified form or if any of the
{\small\verb%li%}'s are free in more than one of the conjuncts or if the equation for any
{\small\verb%li%} is recursive.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PRUNE_RIGHT_RULE
# (ASSUME
#   "!(in:num->bool) (out:num->bool).
#     DEV (in,out) =
#      ?(l1:num->bool) l2.
#       (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");;
. |- !in out. DEV(in,out) = (!x. out x = ~in x)
\end{verbatim}
}
\SEEALSO
PRUNE_SOME_RIGHT_RULE, PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV,
PRUNE_CONV.

\ENDDOC
\DOC{PRUNE\_SOME\_CONV}

\TYPE {\small\verb%PRUNE_SOME_CONV : (string list -> conv)%}\egroup

\SYNOPSIS
Prunes several hidden variables.

\DESCRIBE
{\small\verb%PRUNE_SOME_CONV [`li1`;...;`lik`]%} when applied to the term:
{\par\samepage\setseps\small
\begin{verbatim}
   "?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp"
\end{verbatim}
}
\noindent returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp) =
      (?li(k+1) ... lir. t1 /\ ... /\ tp)
\end{verbatim}
}
\noindent where for {\small\verb%1 <= j <= k%}, each {\small\verb%eqnij%} has the form:
{\par\samepage\setseps\small
\begin{verbatim}
   "!y1 ... ym. lij x1 ... xn = b"
\end{verbatim}
}
\noindent and {\small\verb%lij%} does not appear free in any of the other conjuncts or in
{\small\verb%b%}. The {\small\verb%li%}'s are related by the equation:
{\par\samepage\setseps\small
\begin{verbatim}
   {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr}
\end{verbatim}
}
\noindent The conversion works if one or more of the {\small\verb%eqnij%}'s are not present,
that is if {\small\verb%lij%} is not free in any of the conjuncts, but does not work if
{\small\verb%lij%} appears free in more than one of the conjuncts. {\small\verb%p%} may be zero, that is,
all the conjuncts may be {\small\verb%eqnij%}'s. In this case the body of the result will be
{\small\verb%T%} (true). Also, for each {\small\verb%eqnij%}, {\small\verb%m%} and {\small\verb%n%} may be zero.

If there is more than one line with a specified name (but with different
types), the one that appears outermost in the existential quantifications is
pruned. If such a line name is mentioned twice in the list, the two outermost
occurrences of lines with that name will be pruned, and so on.

\FAILURE
Fails if the argument term is not of the specified form or if any of the
{\small\verb%lij%}'s are free in more than one of the conjuncts or if the equation for any
{\small\verb%lij%} is recursive. The function also fails if any of the specified lines are
not one of the existentially quantified lines.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PRUNE_SOME_CONV [`l1`;`l2`]
# "?l3 l2 l1.
#   (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l3 x)) /\ (!(x:num). l3 x = T)";;
|- (?l3 l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~l3 x) /\ (!x. l3 x = T)) =
   (?l3. !x. l3 x = T)
\end{verbatim}
}
\SEEALSO
PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

\ENDDOC
\DOC{PRUNE\_SOME\_RIGHT\_RULE}

\TYPE {\small\verb%PRUNE_SOME_RIGHT_RULE : (string list -> thm -> thm)%}\egroup

\SYNOPSIS
Prunes several hidden variables.

\DESCRIBE
{\small\verb%PRUNE_SOME_RIGHT_RULE [`li1`;...;`lik`]%} behaves as follows:
{\par\samepage\setseps\small
\begin{verbatim}
    A |- !z1 ... zr.
          t = ?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp
   -----------------------------------------------------------------------
           A |- !z1 ... zr. t = ?li(k+1) ... lir. t1 /\ ... /\ tp
\end{verbatim}
}
\noindent where for {\small\verb%1 <= j <= k%}, each {\small\verb%eqnij%} has the form:
{\par\samepage\setseps\small
\begin{verbatim}
   "!y1 ... ym. lij x1 ... xn = b"
\end{verbatim}
}
\noindent and {\small\verb%lij%} does not appear free in any of the other conjuncts or in
{\small\verb%b%}. The {\small\verb%li%}'s are related by the equation:
{\par\samepage\setseps\small
\begin{verbatim}
   {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr}
\end{verbatim}
}
\noindent The rule works if one or more of the {\small\verb%eqnij%}'s are not present, that
is if {\small\verb%lij%} is not free in any of the conjuncts, but does not work if {\small\verb%lij%}
appears free in more than one of the conjuncts. {\small\verb%p%} may be zero, that is, all
the conjuncts may be {\small\verb%eqnij%}'s. In this case the conjunction will be
transformed to {\small\verb%T%} (true). Also, for each {\small\verb%eqnij%}, {\small\verb%m%} and {\small\verb%n%} may be zero.

If there is more than one line with a specified name (but with different
types), the one that appears outermost in the existential quantifications is
pruned. If such a line name is mentioned twice in the list, the two outermost
occurrences of lines with that name will be pruned, and so on.

\FAILURE
Fails if the argument theorem is not of the specified form or if any of the
{\small\verb%lij%}'s are free in more than one of the conjuncts or if the equation for any
{\small\verb%lij%} is recursive. The function also fails if any of the specified lines are
not one of the existentially quantified lines.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PRUNE_SOME_RIGHT_RULE [`l1`;`l2`]
# (ASSUME
#   "!(in:num->bool) (out:num->bool).
#     DEV (in,out) =
#      ?(l1:num->bool) l2.
#       (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");;
. |- !in out. DEV(in,out) = (!x. out x = ~in x)
\end{verbatim}
}
\SEEALSO
PRUNE_RIGHT_RULE, PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV.

\ENDDOC
\DOC{UNFOLD\_CONV}

\TYPE {\small\verb%UNFOLD_CONV : (thm list -> conv)%}\egroup

\SYNOPSIS
Expands sub-components of a hardware description using their definitions.

\DESCRIBE
{\small\verb%UNFOLD_CONV thl "t1 /\ ... /\ tn"%} returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   B |- t1 /\ ... /\ tn = t1' /\ ... /\ tn'
\end{verbatim}
}
\noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in
{\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions
of the theorems used for rewriting. If none of the rewrites are applicable to
a {\small\verb%ti%}, it is unchanged.

\FAILURE
Never fails.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#UNFOLD_CONV [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# "INV (l1,l2) /\ INV (l2,l3) /\ (!(t:num). l1 t = l2 (t-1) \/ l3 (t-1))";;
. |- INV(l1,l2) /\ INV(l2,l3) /\ (!t. l1 t = l2(t - 1) \/ l3(t - 1)) =
     (!t. l2 t = ~l1 t) /\
     (!t. l3 t = ~l2 t) /\
     (!t. l1 t = l2(t - 1) \/ l3(t - 1))
\end{verbatim}
}
\SEEALSO
UNFOLD_RIGHT_RULE.

\ENDDOC
\DOC{UNFOLD\_RIGHT\_RULE}

\TYPE {\small\verb%UNFOLD_RIGHT_RULE : (thm list -> thm -> thm)%}\egroup

\SYNOPSIS
Expands sub-components of a hardware description using their definitions.

\DESCRIBE
{\small\verb%UNFOLD_RIGHT_RULE thl%} behaves as follows:
{\par\samepage\setseps\small
\begin{verbatim}
       A |- !z1 ... zr. t = ?y1 ... yp. t1 /\ ... /\ tn
   --------------------------------------------------------
    B u A |- !z1 ... zr. t = ?y1 ... yp. t1' /\ ... /\ tn'
\end{verbatim}
}
\noindent where each {\small\verb%ti'%} is the result of rewriting {\small\verb%ti%} with the theorems in
{\small\verb%thl%}. The set of assumptions {\small\verb%B%} is the union of the instantiated assumptions
of the theorems used for rewriting. If none of the rewrites are applicable to
a {\small\verb%ti%}, it is unchanged.

\FAILURE
Fails if the second argument is not of the required form, though either or
both of {\small\verb%r%} and {\small\verb%p%} may be zero.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#UNFOLD_RIGHT_RULE [ASSUME "!in out. INV(in,out) = !(t:num). out t = ~(in t)"]
# (ASSUME "!(in:num->bool) out. BUF(in,out) = ?l. INV(in,l) /\ INV(l,out)");;
.. |- !in out.
       BUF(in,out) = (?l. (!t. l t = ~in t) /\ (!t. out t = ~l t))
\end{verbatim}
}
\SEEALSO
UNFOLD_CONV.

\ENDDOC
\DOC{UNWIND\_ALL\_BUT\_CONV}

\TYPE {\small\verb%UNWIND_ALL_BUT_CONV : (string list -> conv)%}\egroup

\SYNOPSIS
Unwinds all lines of a device (except those in the argument list) as much as
possible.

\DESCRIBE
{\small\verb%UNWIND_ALL_BUT_CONV l%} when applied to the following term:
{\par\samepage\setseps\small
\begin{verbatim}
   "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn"
\end{verbatim}
}
\noindent returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- t1  /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn =
      t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn'
\end{verbatim}
}
\noindent where {\small\verb%ti'%} (for {\small\verb%1 <= i <= n%}) is {\small\verb%ti%} rewritten with the equations
{\small\verb%eqni%} ({\small\verb%1 <= i <= m%}). These equations are those conjuncts with line name not
in {\small\verb%l%} (and which are equations).

\FAILURE
Never fails but may loop indefinitely.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#UNWIND_ALL_BUT_CONV [`l2`]
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\
   (!x. l2 x = 7)
\end{verbatim}
}
\SEEALSO
UNWIND_ONCE_CONV, UNWIND_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE,
UNWIND_AUTO_RIGHT_RULE.

\ENDDOC
\DOC{UNWIND\_ALL\_BUT\_RIGHT\_RULE}

\TYPE {\small\verb%UNWIND_ALL_BUT_RIGHT_RULE : (string list -> thm -> thm)%}\egroup

\SYNOPSIS
Unwinds all lines of a device (except those in the argument list) as much as
possible.

\DESCRIBE
{\small\verb%UNWIND_ALL_BUT_RIGHT_RULE l%} behaves as follows:
{\par\samepage\setseps\small
\begin{verbatim}
    A |- !z1 ... zr.
          t =
          (?l1 ... lp. t1  /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn)
   ---------------------------------------------------------------------
    A |- !z1 ... zr.
          t =
          (?l1 ... lp. t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn')
\end{verbatim}
}
\noindent where {\small\verb%ti'%} (for {\small\verb%1 <= i <= n%}) is {\small\verb%ti%} rewritten with the equations
{\small\verb%eqni%} ({\small\verb%1 <= i <= m%}). These equations are those conjuncts with line name not
in {\small\verb%l%} (and which are equations).

\FAILURE
Fails if the argument theorem is not of the required form, though either or
both of {\small\verb%p%} and {\small\verb%r%} may be zero. May loop indefinitely.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#UNWIND_ALL_BUT_RIGHT_RULE [`l2`]
# (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 = (l2 x) - 1) /\
        (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\
        (!x. l2 x = 7))
\end{verbatim}
}
\SEEALSO
UNWIND_AUTO_RIGHT_RULE, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV,
UNWIND_ONCE_CONV, UNWIND_CONV.

\ENDDOC
\DOC{UNWIND\_AUTO\_CONV}

\TYPE {\small\verb%UNWIND_AUTO_CONV : conv%}\egroup

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

\DESCRIBE
{\small\verb%UNWIND_AUTO_CONV "?l1 ... lm. t1 /\ ... /\ tn"%} returns a theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- (?l1 ... lm. t1 /\ ... /\ tn) = (?l1 ... lm. t1' /\ ... /\ tn')
\end{verbatim}
}
\noindent where {\small\verb%tj'%} is {\small\verb%tj%} rewritten with equations selected from the
{\small\verb%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.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#UNWIND_AUTO_CONV
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7)
\end{verbatim}
}
\SEEALSO
UNWIND_ONCE_CONV, UNWIND_CONV, UNWIND_ALL_BUT_CONV, UNWIND_ALL_BUT_RIGHT_RULE,
UNWIND_AUTO_RIGHT_RULE.

\ENDDOC
\DOC{UNWIND\_AUTO\_RIGHT\_RULE}

\TYPE {\small\verb%UNWIND_AUTO_RIGHT_RULE : (thm -> thm)%}\egroup

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

\DESCRIBE
{\small\verb%UNWIND_AUTO_RIGHT_RULE%} behaves as follows:
{\par\samepage\setseps\small
\begin{verbatim}
    A |- !z1 ... zr. t = ?l1 ... lm. t1  /\ ... /\ tn
   ----------------------------------------------------
    A |- !z1 ... zr. t = ?l1 ... lm. t1' /\ ... /\ tn'
\end{verbatim}
}
\noindent where {\small\verb%tj'%} is {\small\verb%tj%} rewritten with equations selected from the
{\small\verb%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 {\small\verb%m%} and
{\small\verb%r%} may be zero.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#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))
\end{verbatim}
}
\SEEALSO
UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_CONV,
UNWIND_ONCE_CONV, UNWIND_CONV.

\ENDDOC
\DOC{UNWIND\_CONV}

\TYPE {\small\verb%UNWIND_CONV : ((term -> bool) -> conv)%}\egroup

\SYNOPSIS
Unwinds device behaviour using selected line equations until no change.

\DESCRIBE
{\small\verb%UNWIND_CONV p "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn"%} returns a
theorem of the form:
{\par\samepage\setseps\small
\begin{verbatim}
   |- t1  /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn =
      t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn'
\end{verbatim}
}
\noindent where {\small\verb%ti'%} (for {\small\verb%1 <= i <= n%}) is {\small\verb%ti%} rewritten with the equations
{\small\verb%eqni%} ({\small\verb%1 <= i <= m%}). These equations are the conjuncts for which the
predicate {\small\verb%p%} is true. The {\small\verb%ti%} terms are the conjuncts for which {\small\verb%p%} is false.
The rewriting is repeated until no changes take place.

\FAILURE
Never fails but may loop indefinitely.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#UNWIND_CONV (\tm. mem (line_name tm) [`l1`;`l2`])
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = (l2 x) - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7)
\end{verbatim}
}
\SEEALSO
UNWIND_ONCE_CONV, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV,
UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE.

\ENDDOC
\DOC{UNWIND\_ONCE\_CONV}

\TYPE {\small\verb%UNWIND_ONCE_CONV : ((term -> bool) -> conv)%}\egroup

\SYNOPSIS
Basic conversion for parallel unwinding of equations defining wire values in a
standard device specification.

\DESCRIBE
{\small\verb%UNWIND_ONCE_CONV p tm%} unwinds the conjunction {\small\verb%tm%} using the equations
selected by the predicate {\small\verb%p%}. {\small\verb%tm%} should be a conjunction, equivalent under
associative-commutative reordering to:
{\par\samepage\setseps\small
\begin{verbatim}
   t1 /\ t2 /\ ... /\ tn
\end{verbatim}
}
\noindent {\small\verb%p%} is used to partition the terms {\small\verb%ti%} for {\small\verb%1 <= i <= n%} into two
disjoint sets:
{\par\samepage\setseps\small
\begin{verbatim}
   REW = {ti | p ti}
   OBJ = {ti | ~p ti}
\end{verbatim}
}
\noindent The terms {\small\verb%ti%} for which {\small\verb%p%} is true are then used as a set of
rewrite rules (thus they should be equations) to do a single top-down parallel
rewrite of the remaining terms. The rewritten terms take the place of the
original terms in the input conjunction. For example, if {\small\verb%tm%} is:
{\par\samepage\setseps\small
\begin{verbatim}
   t1 /\ t2 /\ t3 /\ t4
\end{verbatim}
}
\noindent and {\small\verb%REW = {t1,t3}%} then the result is:
{\par\samepage\setseps\small
\begin{verbatim}
   |- t1 /\ t2 /\ t3 /\ t4 = t1 /\ t2' /\ t3 /\ t4'
\end{verbatim}
}
\noindent where {\small\verb%ti'%} is {\small\verb%ti%} rewritten with the equations {\small\verb%REW%}.

\FAILURE
Never fails.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#UNWIND_ONCE_CONV (\tm. mem (line_name tm) [`l1`;`l2`])
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = 7 + ((l2(x + 2)) - 1)) /\
   (!x. l2 x = 7)
\end{verbatim}
}
\SEEALSO
UNWIND_CONV, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE,
UNWIND_AUTO_RIGHT_RULE.

\ENDDOC