---

Step * 1 1 of Lemma oarcast-deliver-output_wf


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?
BY
{ ((GenConclAtAddrType ⌜(M × ℕ) List⌝ [2;1;1;2]⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜M List⌝ [2;1]⋅ THENA Auto)
   THEN D -2
   THEN RepUR ``it null`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type
2.  num  :  \mBbbZ{}
3.  s1  :  bag(Id)
4.  s2  :  (M  \mtimes{}  \mBbbN{})  List
\mvdash{}  eval  L  =  eval\_list(map(\mlambda{}p.(fst(p));filter(\mlambda{}p.num  \mleq{}z  snd(p);s2)))  in
    if  null(L)  then  inr  \mcdot{}    else  let  xx,$_{}$  =  L  in  inl  xx  fi    \mmember{}  M?


By

---

Latex:
((GenConclAtAddrType  \mkleeneopen{}(M  \mtimes{}  \mBbbN{})  List\mkleeneclose{}  [2;1;1;2]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}M  List\mkleeneclose{}  [2;1]\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  RepUR  ``it  null``  0
  THEN  Auto)

---

Home Index