cv_termination_tac

cv_transLib.cv_termination_tac : tactic

A tactic for simplifying goals concerning cv_depth_sum.

This tactic is used by cv_transLib.cv_trans (and siblings) when attempting to prove termination goals of translated :cv functions.

See also

cv_transLib.cv_trans, cv_transLib.cv_trans_pre, cv_transLib.cv_trans_pre_rec, cv_transLib.cv_trans_rec, cv_transLib.cv_auto_trans, cv_transLib.cv_auto_trans_pre, cv_transLib.cv_auto_trans_pre_rec, cv_transLib.cv_auto_trans_rec, cv_transLib.cv_eval