---

Step * 2 1 1 of Lemma priority-select-property

.....equality..... 
1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
     ((priority-select(f;g;v) = (inl tt) ∈ (𝔹?) ⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
     ∧ (priority-select(f;g;v) = (inl ff) ∈ (𝔹?) ⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
     ∧ (priority-select(f;g;v) = (inr ⋅ ) ∈ (𝔹?) ⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ↑(f u)
⊢ accumulate (with value x and list item m):
   if isl(x) then x
   if f m then inl tt
   if g m then inl ff
   else x
   fi 
  over list:
    v
  with starting value:
   inl tt) ~ inl tt
BY
{ ((Thin (-4)) THEN (ListInd (-4)) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}f,g:T  {}\mrightarrow{}  \mBbbB{}.
          ((priority-select(f;g;v)  =  (inl  tt)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(f  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  v[j])))))
          \mwedge{}  (priority-select(f;g;v)  =  (inl  ff)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(g  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  v[j])))))
          \mwedge{}  (priority-select(f;g;v)  =  (inr  \mcdot{}  )  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}||v||.  ((\mneg{}\muparrow{}(f  v[i]))  \mwedge{}  (\mneg{}\muparrow{}(g  v[i])))))
5.  f  :  T  {}\mrightarrow{}  \mBbbB{}
6.  g  :  T  {}\mrightarrow{}  \mBbbB{}
7.  \muparrow{}(f  u)
\mvdash{}  accumulate  (with  value  x  and  list  item  m):
      if  isl(x)  then  x
      if  f  m  then  inl  tt
      if  g  m  then  inl  ff
      else  x
      fi 
    over  list:
        v
    with  starting  value:
      inl  tt)  \msim{}  inl  tt


By

---

Latex:
((Thin  (-4))  THEN  (ListInd  (-4))  THEN  Reduce  0  THEN  Auto)

---

Home Index