---

Step * of Lemma priority-select-inr

∀[T:Type]. ∀[as:T List]. ∀[f,g:T ⟶ 𝔹].  uiff(priority-select(f;g;as) = (inr ⋅ ) ∈ (𝔹?);(∀a∈as.(¬↑(f a)) ∧ (¬↑(g a))))
BY
{ xxx(((InstLemma `priority-select-property` [])
       THEN RepeatFor 4 (ParallelLast)
       THEN ExRepD
       THEN (RW (SweepDnC (HypC (-1))) 0))
      THENA Auto
      )xxx }

1
1. T : Type
2. as : T List
3. f : T ⟶ 𝔹
4. g : T ⟶ 𝔹
5. priority-select(f;g;as) = (inl tt) ∈ (𝔹?) ⇐⇒ ∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j]))))
6. priority-select(f;g;as) = (inl ff) ∈ (𝔹?) ⇐⇒ ∃i:ℕ||as||. ((↑(g as[i])) ∧ (∀j:ℕi + 1. (¬↑(f as[j]))))
7. priority-select(f;g;as) = (inr ⋅ ) ∈ (𝔹?) ⇐⇒ ∀i:ℕ||as||. ((¬↑(f as[i])) ∧ (¬↑(g as[i])))
⊢ uiff(∀i:ℕ||as||. ((¬↑(f as[i])) ∧ (¬↑(g as[i])));(∀a∈as.(¬↑(f a)) ∧ (¬↑(g a))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[f,g:T  {}\mrightarrow{}  \mBbbB{}].
    uiff(priority-select(f;g;as)  =  (inr  \mcdot{}  );(\mforall{}a\mmember{}as.(\mneg{}\muparrow{}(f  a))  \mwedge{}  (\mneg{}\muparrow{}(g  a))))


By

---

Latex:
xxx(((InstLemma  `priority-select-property`  [])
          THEN  RepeatFor  4  (ParallelLast)
          THEN  ExRepD
          THEN  (RW  (SweepDnC  (HypC  (-1)))  0))
        THENA  Auto
        )xxx

---

Home Index