Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
TOP_SWEEP_SQCONV : strategy

SYNOPSIS
Applies simplification top-down at all levels, but after descending to subterms, does not return to higher ones.

DESCRIPTION
HOL Light's simplification functions (e.g. SIMP_TAC) have their traversal algorithm controlled by a ``strategy''. TOP_SWEEP_SQCONV is a strategy corresponding to TOP_SWEEP_CONV for ordinary conversions: simplification is applied top-down at all levels, but after descending to subterms, does not return to higher ones.

FAILURE CONDITIONS
Not applicable.

SEE ALSO
DEPTH_SQCONV, ONCE_DEPTH_SQCONV, REDEPTH_SQCONV, TOP_DEPTH_SQCONV, TOP_SWEEP_CONV.