---

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


1. [T] : Type
2. f : T ⟶ ℤ
3. n : ℕ
4. L : T List
5. ∀L1:T List
     (||L1|| < ||L||
     ⇒ (↑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 < ||L||
7. L ~ firstn(||L|| - 1;L) @ [last(L)]
8. ¬↑null(L)
⊢ ↑isl(case list-max-aux(x.f[x];firstn(||L|| - 1;L))
 of inl(p) =>
 if fst(p) <z f[last(L)] then inl <f[last(L)], last(L)> else list-max-aux(x.f[x];firstn(||L|| - 1;L)) fi 
 | inr(q) =>
 inl <f[last(L)], last(L)>)
BY
{ (GenConclAtAddr [1;1;1] THEN D -2 THEN Reduce 0 THEN Auto THEN AutoSplit)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  L  :  T  List
5.  \mforall{}L1:T  List
          (||L1||  <  ||L||
          {}\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  <  ||L||
7.  L  \msim{}  firstn(||L||  -  1;L)  @  [last(L)]
8.  \mneg{}\muparrow{}null(L)
\mvdash{}  \muparrow{}isl(case  list-max-aux(x.f[x];firstn(||L||  -  1;L))
  of  inl(p)  =>
  if  fst(p)  <z  f[last(L)]
  then  inl  <f[last(L)],  last(L)>
  else  list-max-aux(x.f[x];firstn(||L||  -  1;L))
  fi 
  |  inr(q)  =>
  inl  <f[last(L)],  last(L)>)


By

---

Latex:
(GenConclAtAddr  [1;1;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto  THEN  AutoSplit)\mcdot{}

---

Home Index