---

Step * of Lemma not-isl-priority-select

∀[T:Type]. ∀[as:T List]. ∀[f,g:T ⟶ 𝔹].  uiff(¬↑isl(priority-select(f;g;as));(∀a∈as.(¬↑(f a)) ∧ (¬↑(g a))))
BY
{ xxx((((((UnivCD THENA Auto) THEN RWO "priority-select-inr<" 0) THENA Auto) THEN (GenConclAtAddr [1; 1; 1; 1]))
       THENA Auto
       )
      THEN (Thin (-1))
      THEN Auto)xxx }

1
1. T : Type
2. as : T List
3. f : T ⟶ 𝔹
4. g : T ⟶ 𝔹
5. v : 𝔹?
6. ¬↑isl(v)
⊢ v = (inr ⋅ ) ∈ (𝔹?)

---

Latex:

---

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


By

---

Latex:
xxx((((((UnivCD  THENA  Auto)  THEN  RWO  "priority-select-inr<"  0)  THENA  Auto)
            THEN  (GenConclAtAddr  [1;  1;  1;  1])
            )
          THENA  Auto
          )
        THEN  (Thin  (-1))
        THEN  Auto)xxx

---

Home Index