---

Step * 1 of Lemma oarcast-deliver-output_wf


1. M : Type
2. num : ℤ
3. s : bag(Id) × ((M × ℕ) List)
⊢ oarcast-deliver-output(num;s) ∈ M?
BY
{ (Unfold `oarcast-deliver-output` 0 THEN D -1 THEN Reduce 0 THEN Unfold `mapfilter` 0) }

1
1. M : Type
2. num : ℤ
3. s1 : bag(Id)
4. s2 : (M × ℕ) List
⊢ eval L = eval_list(map(λp.(fst(p));filter(λp.num ≤z snd(p);s2))) in
  if null(L) then inr ⋅  else let xx,_ = L in inl xx fi  ∈ M?

---

Latex:

---

Latex:

1.  M  :  Type
2.  num  :  \mBbbZ{}
3.  s  :  bag(Id)  \mtimes{}  ((M  \mtimes{}  \mBbbN{})  List)
\mvdash{}  oarcast-deliver-output(num;s)  \mmember{}  M?


By

---

Latex:
(Unfold  `oarcast-deliver-output`  0  THEN  D  -1  THEN  Reduce  0  THEN  Unfold  `mapfilter`  0)

---

Home Index