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

REDEPTH_SQCONV : strategy

SYNOPSIS: Applies simplification bottom-up to all subterms, retraversing changed ones.
DESCRIPTION: HOL Light's simplification functions (e.g. SIMP_TAC) have their traversal algorithm controlled by a ``strategy''. REDEPTH_SQCONV is a strategy corresponding to REDEPTH_CONV for ordinary conversions: simplification is applied bottom-up to all subterms, retraversing changed ones.
FAILURE CONDITIONS: Not applicable.
SEE ALSO: DEPTH_SQCONV, ONCE_DEPTH_SQCONV, REDEPTH_CONV, TOP_DEPTH_SQCONV, TOP_SWEEP_SQCONV.