---

Step * 1 1 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. i : ℕ||as||
10. ↑(g as[i])
11. ∀j:ℕi + 1. (¬↑(f as[j]))
12. ↑(g as[i])
13. b : T
14. (b ∈ as)
15. b ≤ as[i]
⊢ ¬↑(f b)
BY
{ (((((D (-2)) THEN ExRepD THEN (HypSubst (-2) 0)) THENA Auto) THEN Decide ⌜i1 ≤ i⌝⋅) THENA 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. ∀j:ℕi + 1. (¬↑(f as[j]))
12. ↑(g as[i])
13. b : T
14. i1 : ℕ
15. i1 < ||as||
16. b = as[i1] ∈ T
17. b ≤ as[i]
18. i1 ≤ i
⊢ ¬↑(f as[i1])

2
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. ∀j:ℕi + 1. (¬↑(f as[j]))
12. ↑(g as[i])
13. b : T
14. i1 : ℕ
15. i1 < ||as||
16. b = as[i1] ∈ T
17. b ≤ as[i]
18. ¬(i1 ≤ i)
⊢ ¬↑(f as[i1])

---

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.  i  :  \mBbbN{}||as||
10.  \muparrow{}(g  as[i])
11.  \mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(f  as[j]))
12.  \muparrow{}(g  as[i])
13.  b  :  T
14.  (b  \mmember{}  as)
15.  b  \mleq{}  as[i]
\mvdash{}  \mneg{}\muparrow{}(f  b)


By

---

Latex:
(((((D  (-2))  THEN  ExRepD  THEN  (HypSubst  (-2)  0))  THENA  Auto)  THEN  Decide  \mkleeneopen{}i1  \mleq{}  i\mkleeneclose{}\mcdot{})  THENA  Auto)

---

Home Index