---

Step * of Lemma priority-select-tt

∀[T:Type]
  ∀as:T List. ∀f,g:T ⟶ 𝔹.
    (priority-select(f;g;as) = (inl tt) ∈ (𝔹?)
       ⇐⇒ (∃a∈as. (↑(f a)) ∧ (∀b:T. ((b ∈ as) ⇒ ¬↑(g b) supposing b < a)))) supposing 
       (no_repeats(T;as) and 
       sorted(as) and 
       (T ⊆r ℤ))
BY
{ ((((UnivCD THENA Auto) THEN (InstLemma `priority-select-property` [⌜T⌝; ⌜as⌝; ⌜f⌝; ⌜g⌝])⋅) THENA Auto)
   THEN ExRepD
   THEN (Thin (-1))
   THEN (Thin (-1))
   THEN ((RW (SweepDnC (HypC (-1))) 0) THENA (Auto THEN DVar `a' THEN Auto))
   THEN Auto
   THEN ExRepD
   THEN Try ((DoSubsume THEN Complete (Auto)))
   THEN (All (Unfolds ``sorted``))) }

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. ∀j:ℕi. (¬↑(g as[j]))
⊢ (∃a∈as. (↑(f a)) ∧ (∀b:T. ((b ∈ as) ⇒ ¬↑(g b) supposing b < a)))

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. (∃a∈as. (↑(f a)) ∧ (∀b:T. ((b ∈ as) ⇒ ¬↑(g b) supposing b < a)))
⊢ ∃i:ℕ||as||. ((↑(f as[i])) ∧ (∀j:ℕi. (¬↑(g as[j]))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}as:T  List.  \mforall{}f,g:T  {}\mrightarrow{}  \mBbbB{}.
        (priority-select(f;g;as)  =  (inl  tt)
              \mLeftarrow{}{}\mRightarrow{}  (\mexists{}a\mmember{}as.  (\muparrow{}(f  a))  \mwedge{}  (\mforall{}b:T.  ((b  \mmember{}  as)  {}\mRightarrow{}  \mneg{}\muparrow{}(g  b)  supposing  b  <  a))))  supposing 
              (no\_repeats(T;as)  and 
              sorted(as)  and 
              (T  \msubseteq{}r  \mBbbZ{}))


By

---

Latex:
((((UnivCD  THENA  Auto)  THEN  (InstLemma  `priority-select-property`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}as\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}g\mkleeneclose{}])\mcdot{})
    THENA  Auto
    )
  THEN  ExRepD
  THEN  (Thin  (-1))
  THEN  (Thin  (-1))
  THEN  ((RW  (SweepDnC  (HypC  (-1)))  0)  THENA  (Auto  THEN  DVar  `a'  THEN  Auto))
  THEN  Auto
  THEN  ExRepD
  THEN  Try  ((DoSubsume  THEN  Complete  (Auto)))
  THEN  (All  (Unfolds  ``sorted``)))

---

Home Index