---

Step * 2 2 1 of Lemma list-max-aux-property


1. [T] : Type
2. f : T ⟶ ℤ
3. n : ℕ
4. u : T
5. ∀L1:T List
     (||L1|| < 1
     ⇒ (↑isl(list-max-aux(x.f[x];L1)))
        ∧ let n,x = outl(list-max-aux(x.f[x];L1)) 
          in (x ∈ L1) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L1.f[y] ≤ n) 
        supposing 0 < ||L1||)
6. 0 < 1
7. [u] ~ firstn(0;[u]) @ [last([u])]
8. ¬False
9. ¬1 < 1
⊢ (last([u]) ∈ firstn(0;[u]) @ [last([u])])
∧ (f[last([u])] = f[last([u])] ∈ ℤ)
∧ (∀y∈firstn(0;[u]) @ [last([u])].f[y] ≤ f[last([u])])
BY
{ (Reduce 0⋅ THEN (RWO "first0" 0 THENA Auto) THEN Reduce 0) }

1
1. [T] : Type
2. f : T ⟶ ℤ
3. n : ℕ
4. u : T
5. ∀L1:T List
     (||L1|| < 1
     ⇒ (↑isl(list-max-aux(x.f[x];L1)))
        ∧ let n,x = outl(list-max-aux(x.f[x];L1)) 
          in (x ∈ L1) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L1.f[y] ≤ n) 
        supposing 0 < ||L1||)
6. 0 < 1
7. [u] ~ firstn(0;[u]) @ [last([u])]
8. ¬False
9. ¬1 < 1
⊢ (last([u]) ∈ [last([u])]) ∧ (f[last([u])] = f[last([u])] ∈ ℤ) ∧ (∀y∈[last([u])].f[y] ≤ f[last([u])])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  u  :  T
5.  \mforall{}L1:T  List
          (||L1||  <  1
          {}\mRightarrow{}  (\muparrow{}isl(list-max-aux(x.f[x];L1)))
                \mwedge{}  let  n,x  =  outl(list-max-aux(x.f[x];L1)) 
                    in  (x  \mmember{}  L1)  \mwedge{}  (f[x]  =  n)  \mwedge{}  (\mforall{}y\mmember{}L1.f[y]  \mleq{}  n) 
                supposing  0  <  ||L1||)
6.  0  <  1
7.  [u]  \msim{}  firstn(0;[u])  @  [last([u])]
8.  \mneg{}False
9.  \mneg{}1  <  1
\mvdash{}  (last([u])  \mmember{}  firstn(0;[u])  @  [last([u])])
\mwedge{}  (f[last([u])]  =  f[last([u])])
\mwedge{}  (\mforall{}y\mmember{}firstn(0;[u])  @  [last([u])].f[y]  \mleq{}  f[last([u])])


By

---

Latex:
(Reduce  0\mcdot{}  THEN  (RWO  "first0"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index