terminates_bind — Mathlib

English

If s terminates and f(get s) terminates, then bind s f terminates.

Русский

Если s завершается и f(get s) завершается, то bind s f завершается.

LaTeX

$$$$ \text{If } \operatorname{Terminates}(s) \text{ and } \operatorname{Terminates}(f(\operatorname{get} s)) \Rightarrow \operatorname{Terminates}(\operatorname{bind} s f). $$$$

Lean4

instance terminates_bind (s : Computation α) (f : α → Computation β) [Terminates s] [Terminates (f (get s))] :
    Terminates (bind s f) :=
  terminates_of_mem (mem_bind (get_mem s) (get_mem (f (get s))))

Похожие утверждения