---

Step * of Lemma threshold_accum_wf

∀[S,A,B:Type]. ∀[test:S ─→ A ─→ 𝔹]. ∀[nxt:(S × A) ─→ S]. ∀[step:S ─→ A ─→ S]. ∀[g:(S × A) ─→ (B?)].
  (threshold_accum(test;
   nxt;
   step;
   g) ∈ (S × (B?)) ─→ A ─→ (S × (B?)))
BY
{ (ProveWfLemma THEN Auto) }

---

Latex:


\mforall{}[S,A,B:Type].  \mforall{}[test:S  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[nxt:(S  \mtimes{}  A)  {}\mrightarrow{}  S].  \mforall{}[step:S  {}\mrightarrow{}  A  {}\mrightarrow{}  S].  \mforall{}[g:(S  \mtimes{}  A)  {}\mrightarrow{}  (B?)].
    (threshold\_accum(test;
      nxt;
      step;
      g)  \mmember{}  (S  \mtimes{}  (B?))  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  (B?)))


By

(ProveWfLemma  THEN  Auto)

---

Home Index