---

Step * 2 of Lemma priority-select-property


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])))))
⊢ ∀f,g:T ⟶ 𝔹.
    ((priority-select(f;g;[u / v]) = (inl tt) ∈ (𝔹?)
     ⇐⇒ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j])))))
    ∧ (priority-select(f;g;[u / v]) = (inl ff) ∈ (𝔹?)
      ⇐⇒ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j])))))
    ∧ (priority-select(f;g;[u / v]) = (inr ⋅ ) ∈ (𝔹?) ⇐⇒ ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i])))))
BY
{ (((UnivCD THENA Auto) THEN Unfold `priority-select` 0 THEN Reduce 0 THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
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)
   ∈ (𝔹?)
  ⇐⇒ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j])))))
∧ (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 ff)
   ∈ (𝔹?)
  ⇐⇒ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j])))))
∧ (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)
   = (inr ⋅ )
   ∈ (𝔹?)
  ⇐⇒ ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i]))))

2
.....falsecase..... 
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:
    if g u then inl ff else inr ⋅  fi )
   = (inl tt)
   ∈ (𝔹?)
  ⇐⇒ ∃i:ℕ||v|| + 1. ((↑(f [u / v][i])) ∧ (∀j:ℕi. (¬↑(g [u / v][j])))))
∧ (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:
    if g u then inl ff else inr ⋅  fi )
   = (inl ff)
   ∈ (𝔹?)
  ⇐⇒ ∃i:ℕ||v|| + 1. ((↑(g [u / v][i])) ∧ (∀j:ℕi + 1. (¬↑(f [u / v][j])))))
∧ (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:
    if g u then inl ff else inr ⋅  fi )
   = (inr ⋅ )
   ∈ (𝔹?)
  ⇐⇒ ∀i:ℕ||v|| + 1. ((¬↑(f [u / v][i])) ∧ (¬↑(g [u / v][i]))))

---

Latex:

---

Latex:

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])))))
\mvdash{}  \mforall{}f,g:T  {}\mrightarrow{}  \mBbbB{}.
        ((priority-select(f;g;[u  /  v])  =  (inl  tt)
          \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||  +  1.  ((\muparrow{}(f  [u  /  v][i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  [u  /  v][j])))))
        \mwedge{}  (priority-select(f;g;[u  /  v])  =  (inl  ff)
            \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||  +  1.  ((\muparrow{}(g  [u  /  v][i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  [u  /  v][j])))))
        \mwedge{}  (priority-select(f;g;[u  /  v])  =  (inr  \mcdot{}  )
            \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}||v||  +  1.  ((\mneg{}\muparrow{}(f  [u  /  v][i]))  \mwedge{}  (\mneg{}\muparrow{}(g  [u  /  v][i])))))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `priority-select`  0  THEN  Reduce  0  THEN  SplitOnConclITE)
  THENA  Auto
  )

---

Home Index