---

Step * of Lemma list-max-aux-property

∀[T:Type]
  ∀f:T ⟶ ℤ. ∀L:T List.
    (↑isl(list-max-aux(x.f[x];L)))
    ∧ let n,x = outl(list-max-aux(x.f[x];L)) 
      in (x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n) 
    supposing 0 < ||L||
BY
{ (InductionOnLength
   THEN (D 0⋅ THENA Auto)
   THEN (InstLemma `last-lemma-sq` [⌜T⌝;⌜L⌝]⋅ THENA (Auto THEN DVar `L' THEN All Reduce THEN Auto))
   THEN ExRepD
   THEN HypSubst' (-1) 0
   THEN (Assert ¬↑null(L) BY
               (DVar `L' THEN All Reduce THEN Auto))
   THEN (Unfold `list-max-aux` 0
         THEN Reduce 0
         THEN ((RWO "list_accum_append" 0 THENA Auto)
               THEN (Fold `list-max-aux` 0 THEN Reduce 0 THEN (CallByValueReduce 0 THENA Auto) THEN D 0)⋅
               )⋅)⋅) }

1
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)>)

2
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)
⊢ let n,x = outl(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)>) 
  in (x ∈ firstn(||L|| - 1;L) @ [last(L)]) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈firstn(||L|| - 1;L) @ [last(L)].f[y] ≤ n)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:T  List.
        (\muparrow{}isl(list-max-aux(x.f[x];L)))
        \mwedge{}  let  n,x  =  outl(list-max-aux(x.f[x];L)) 
            in  (x  \mmember{}  L)  \mwedge{}  (f[x]  =  n)  \mwedge{}  (\mforall{}y\mmember{}L.f[y]  \mleq{}  n) 
        supposing  0  <  ||L||


By

---

Latex:
(InductionOnLength
  THEN  (D  0\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `last-lemma-sq`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  DVar  `L'  THEN  All  Reduce  THEN  Auto))
  THEN  ExRepD
  THEN  HypSubst'  (-1)  0
  THEN  (Assert  \mneg{}\muparrow{}null(L)  BY
                          (DVar  `L'  THEN  All  Reduce  THEN  Auto))
  THEN  (Unfold  `list-max-aux`  0
              THEN  Reduce  0
              THEN  ((RWO  "list\_accum\_append"  0  THENA  Auto)
                          THEN  (Fold  `list-max-aux`  0
                                      THEN  Reduce  0
                                      THEN  (CallByValueReduce  0  THENA  Auto)
                                      THEN  D  0)\mcdot{}
                          )\mcdot{})\mcdot{})

---

Home Index