Step
*
2
of Lemma
priority-select-ff
1. [T] : Type
2. as : T List
3. f : T ⟶ 𝔹
4. g : T ⟶ 𝔹
5. T ⊆r ℤ
6. ∀i:ℕ||as||. ∀j:ℕi.  (as[j] ≤ as[i])
7. (priority-select(f;g;as) = (inl ff) ∈ (𝔹?)) 
⇒ (∃i:ℕ||as||. ((↑(g as[i])) ∧ (∀j:ℕi + 1. (¬↑(f as[j])))))
8. (priority-select(f;g;as) = (inl ff) ∈ (𝔹?)) 
⇐ ∃i:ℕ||as||. ((↑(g as[i])) ∧ (∀j:ℕi + 1. (¬↑(f as[j]))))
9. (∃a∈as. (↑(g a)) ∧ (∀b:T. ((b ∈ as) 
⇒ ¬↑(f b) supposing b ≤ a)))
⊢ ∃i:ℕ||as||. ((↑(g as[i])) ∧ (∀j:ℕi + 1. (¬↑(f as[j]))))
BY
{ (D (-1) THEN With ⌜i⌝ (D 0)⋅ THEN Auto THEN (BHyp (-3)) THEN Auto) }
1
1. T : Type
2. as : T List
3. f : T ⟶ 𝔹
4. g : T ⟶ 𝔹
5. T ⊆r ℤ
6. ∀i:ℕ||as||. ∀j:ℕi.  (as[j] ≤ as[i])
7. (priority-select(f;g;as) = (inl ff) ∈ (𝔹?)) 
⇒ (∃i:ℕ||as||. ((↑(g as[i])) ∧ (∀j:ℕi + 1. (¬↑(f as[j])))))
8. (priority-select(f;g;as) = (inl ff) ∈ (𝔹?)) 
⇐ ∃i:ℕ||as||. ((↑(g as[i])) ∧ (∀j:ℕi + 1. (¬↑(f as[j]))))
9. i : ℕ||as||
10. ↑(g as[i])
11. ∀b:T. ((b ∈ as) 
⇒ ¬↑(f b) supposing b ≤ as[i])
12. ↑(g as[i])
13. j : ℕi + 1
⊢ as[j] ≤ as[i]
Latex:
Latex:
1.  [T]  :  Type
2.  as  :  T  List
3.  f  :  T  {}\mrightarrow{}  \mBbbB{}
4.  g  :  T  {}\mrightarrow{}  \mBbbB{}
5.  T  \msubseteq{}r  \mBbbZ{}
6.  \mforall{}i:\mBbbN{}||as||.  \mforall{}j:\mBbbN{}i.    (as[j]  \mleq{}  as[i])
7.  (priority-select(f;g;as)  =  (inl  ff))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(g  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j])))))
8.  (priority-select(f;g;as)  =  (inl  ff))  \mLeftarrow{}{}  \mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(g  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j]))))
9.  (\mexists{}a\mmember{}as.  (\muparrow{}(g  a))  \mwedge{}  (\mforall{}b:T.  ((b  \mmember{}  as)  {}\mRightarrow{}  \mneg{}\muparrow{}(f  b)  supposing  b  \mleq{}  a)))
\mvdash{}  \mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(g  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j]))))
By
Latex:
(D  (-1)  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  (BHyp  (-3))  THEN  Auto)
Home
Index