---

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


1. T : Type
2. u : T
3. v : T List
4. ∀f,g:T ⟶ 𝔹.
     ((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:
        inr ⋅ )
       = (inl tt)
       ∈ (𝔹?)
      ⇐⇒ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g 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:
         inr ⋅ )
        = (inl ff)
        ∈ (𝔹?)
       ⇐⇒ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f 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:
         inr ⋅ )
        = (inr ⋅ )
        ∈ (𝔹?)
       ⇐⇒ ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))))
5. f : T ⟶ 𝔹
6. g : T ⟶ 𝔹
7. ¬↑(f u)
8. ¬↑(g u)
9. (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:
     inr ⋅ )
= (inl tt)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j])))))
10. (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:
      inr ⋅ )
= (inl tt)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(f v[i])) ∧ (∀j:ℕi. (¬↑(g v[j]))))
11. (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:
      inr ⋅ )
= (inl ff)
∈ (𝔹?))
⇒ (∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j])))))
12. (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:
      inr ⋅ )
= (inl ff)
∈ (𝔹?)) ⇐ ∃i:ℕ||v||. ((↑(g v[i])) ∧ (∀j:ℕi + 1. (¬↑(f v[j]))))
13. 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:
     inr ⋅ )
= (inr ⋅ )
∈ (𝔹?)
14. ∀i:ℕ||v||. ((¬↑(f v[i])) ∧ (¬↑(g v[i])))
15. i : ℕ||v|| + 1
16. ¬↑(f [u / v][i])
⊢ ¬↑(g [u / v][i])
BY
{ (CaseNat 0 `i' THEN Reduce 0 THEN Auto THEN RWO "select_cons_tl" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}f,g:T  {}\mrightarrow{}  \mBbbB{}.
          ((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:
                inr  \mcdot{}  )
              =  (inl  tt)
            \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(f  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  v[j])))))
          \mwedge{}  (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:
                  inr  \mcdot{}  )
                =  (inl  ff)
              \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(g  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  v[j])))))
          \mwedge{}  (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:
                  inr  \mcdot{}  )
                =  (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.  \mneg{}\muparrow{}(f  u)
8.  \mneg{}\muparrow{}(g  u)
9.  (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:
          inr  \mcdot{}  )
=  (inl  tt))
{}\mRightarrow{}  (\mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(f  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  v[j])))))
10.  (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:
            inr  \mcdot{}  )
=  (inl  tt))  \mLeftarrow{}{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(f  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  v[j]))))
11.  (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:
            inr  \mcdot{}  )
=  (inl  ff))
{}\mRightarrow{}  (\mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(g  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  v[j])))))
12.  (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:
            inr  \mcdot{}  )
=  (inl  ff))  \mLeftarrow{}{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(g  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  v[j]))))
13.  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:
          inr  \mcdot{}  )
=  (inr  \mcdot{}  )
14.  \mforall{}i:\mBbbN{}||v||.  ((\mneg{}\muparrow{}(f  v[i]))  \mwedge{}  (\mneg{}\muparrow{}(g  v[i])))
15.  i  :  \mBbbN{}||v||  +  1
16.  \mneg{}\muparrow{}(f  [u  /  v][i])
\mvdash{}  \mneg{}\muparrow{}(g  [u  /  v][i])


By

---

Latex:
(CaseNat  0  `i'  THEN  Reduce  0  THEN  Auto  THEN  RWO  "select\_cons\_tl"  0  THEN  Auto)

---

Home Index