---

Step * of Lemma priority-select-property

No Annotations
∀[T:Type]
  ∀as:T List. ∀f,g:T ⟶ 𝔹.
    ((priority-select(f;g;as) = (inl tt) ∈ (𝔹?) ⇐⇒ ∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j])))))
    ∧ (priority-select(f;g;as) = (inl ff) ∈ (𝔹?) ⇐⇒ ∃i:ℕ||as||. ((↑(g as[i])) ∧ (∀j:ℕi + 1. (¬↑(f as[j])))))
    ∧ (priority-select(f;g;as) = (inr ⋅ ) ∈ (𝔹?) ⇐⇒ ∀i:ℕ||as||. ((¬↑(f as[i])) ∧ (¬↑(g as[i])))))
BY
{ (InductionOnList THEN Reduce 0) }

1
1. [T] : Type
⊢ ∀f,g:T ⟶ 𝔹.
    ((priority-select(f;g;[]) = (inl tt) ∈ (𝔹?) ⇐⇒ ∃i:ℕ0. ((↑(f ⊥)) ∧ (∀j:ℕi. (¬↑(g ⊥)))))
    ∧ (priority-select(f;g;[]) = (inl ff) ∈ (𝔹?) ⇐⇒ ∃i:ℕ0. ((↑(g ⊥)) ∧ (∀j:ℕi + 1. (¬↑(f ⊥)))))
    ∧ (priority-select(f;g;[]) = (inr ⋅ ) ∈ (𝔹?) ⇐⇒ ∀i:ℕ0. ((¬↑(f ⊥)) ∧ (¬↑(g ⊥)))))

2
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])))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}as:T  List.  \mforall{}f,g:T  {}\mrightarrow{}  \mBbbB{}.
        ((priority-select(f;g;as)  =  (inl  tt)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(f  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  as[j])))))
        \mwedge{}  (priority-select(f;g;as)  =  (inl  ff)
            \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(g  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j])))))
        \mwedge{}  (priority-select(f;g;as)  =  (inr  \mcdot{}  )  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}||as||.  ((\mneg{}\muparrow{}(f  as[i]))  \mwedge{}  (\mneg{}\muparrow{}(g  as[i])))))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index