EXISTS_EQN_CONV : conv
STRUCTURE
unwindLib
SYNOPSIS
Proves the existence of a line that has a non-recursive equation.
LIBRARY
unwind
DESCRIPTION
EXISTS_EQN_CONV "?l. !y1 ... ym. l x1 ... xn = t"
returns the theorem:
|- (?l. !y1 ... ym. l x1 ... xn = t) = T
provided
l
is not free in
t
. Both
m
and
n
may be zero.
FAILURE
Fails if the argument term is not of the specified form or if
l
appears free in
t
.
SEEALSO
PRUNE_ONCE_CONV
HOL
Kananaskis-14