---

Step * of Lemma oarcast-deliver-output_wf

∀[M:Type]. ∀[num:ℤ]. ∀[s:bag(Id) × ((M × ℕ) List)].  (oarcast-deliver-output(num;s) ∈ M?)
BY
{ Auto }

1
1. M : Type
2. num : ℤ
3. s : bag(Id) × ((M × ℕ) List)
⊢ oarcast-deliver-output(num;s) ∈ M?

---

Latex:

---

Latex:
\mforall{}[M:Type].  \mforall{}[num:\mBbbZ{}].  \mforall{}[s:bag(Id)  \mtimes{}  ((M  \mtimes{}  \mBbbN{})  List)].    (oarcast-deliver-output(num;s)  \mmember{}  M?)


By

---

Latex:
Auto

---

Home Index