---

Step * 2 1 1 of Lemma priority-select-tt


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. no_repeats(T;as)
8. (priority-select(f;g;as) = (inl tt) ∈ (𝔹?)) ⇒ (∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j])))))
9. (priority-select(f;g;as) = (inl tt) ∈ (𝔹?)) ⇐ ∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j]))))
10. i : ℕ||as||
11. ↑(f as[i])
12. ∀b:T. ((b ∈ as) ⇒ ¬↑(g b) supposing b < as[i])
13. ↑(f as[i])
14. j : ℕi
⊢ as[j] < as[i]
BY
{ (Decide ⌜i = j ∈ ℤ⌝⋅ 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. no_repeats(T;as)
8. (priority-select(f;g;as) = (inl tt) ∈ (𝔹?)) ⇒ (∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j])))))
9. (priority-select(f;g;as) = (inl tt) ∈ (𝔹?)) ⇐ ∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j]))))
10. i : ℕ||as||
11. ↑(f as[i])
12. ∀b:T. ((b ∈ as) ⇒ ¬↑(g b) supposing b < as[i])
13. ↑(f as[i])
14. j : ℕi
15. i = j ∈ ℤ
⊢ as[j] < as[i]

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. no_repeats(T;as)
8. (priority-select(f;g;as) = (inl tt) ∈ (𝔹?)) ⇒ (∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j])))))
9. (priority-select(f;g;as) = (inl tt) ∈ (𝔹?)) ⇐ ∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j]))))
10. i : ℕ||as||
11. ↑(f as[i])
12. ∀b:T. ((b ∈ as) ⇒ ¬↑(g b) supposing b < as[i])
13. ↑(f as[i])
14. j : ℕi
15. ¬(i = j ∈ ℤ)
⊢ 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.  no\_repeats(T;as)
8.  (priority-select(f;g;as)  =  (inl  tt))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(f  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  as[j])))))
9.  (priority-select(f;g;as)  =  (inl  tt))  \mLeftarrow{}{}  \mexists{}i:\mBbbN{}||as||.  ((\muparrow{}(f  as[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(g  as[j]))))
10.  i  :  \mBbbN{}||as||
11.  \muparrow{}(f  as[i])
12.  \mforall{}b:T.  ((b  \mmember{}  as)  {}\mRightarrow{}  \mneg{}\muparrow{}(g  b)  supposing  b  <  as[i])
13.  \muparrow{}(f  as[i])
14.  j  :  \mBbbN{}i
\mvdash{}  as[j]  <  as[i]


By

---

Latex:
(Decide  \mkleeneopen{}i  =  j\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index