---

Step * 1 of Lemma priority-select-inr


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))))
BY
{ xxx(Unfold `l_all` 0
      THEN Auto
      THEN Try (((InstHyp [⌜as[i]⌝] (-2))⋅ THEN Auto THEN BLemma `select_member` THEN Auto))
      THEN (D (-1))
      THEN ExRepD
      THEN (HypSubst (-1) 0)
      THEN Auto
      THEN (InstHyp [⌜i⌝] (-5))⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  f  :  T  {}\mrightarrow{}  \mBbbB{}
4.  g  :  T  {}\mrightarrow{}  \mBbbB{}
5.  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]))))
6.  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]))))
7.  priority-select(f;g;as)  =  (inr  \mcdot{}  )  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}||as||.  ((\mneg{}\muparrow{}(f  as[i]))  \mwedge{}  (\mneg{}\muparrow{}(g  as[i])))
\mvdash{}  uiff(\mforall{}i:\mBbbN{}||as||.  ((\mneg{}\muparrow{}(f  as[i]))  \mwedge{}  (\mneg{}\muparrow{}(g  as[i])));(\mforall{}a\mmember{}as.(\mneg{}\muparrow{}(f  a))  \mwedge{}  (\mneg{}\muparrow{}(g  a))))


By

---

Latex:
xxx(Unfold  `l\_all`  0
        THEN  Auto
        THEN  Try  (((InstHyp  [\mkleeneopen{}as[i]\mkleeneclose{}]  (-2))\mcdot{}  THEN  Auto  THEN  BLemma  `select\_member`  THEN  Auto))
        THEN  (D  (-1))
        THEN  ExRepD
        THEN  (HypSubst  (-1)  0)
        THEN  Auto
        THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-5))\mcdot{}
        THEN  Auto)xxx

---

Home Index