---

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


1. [T] : Type
2. f : T ⟶ ℤ
3. n : ℕ
4. u : T
5. u1 : T
6. v : T List
7. ∀L1:T List
     (||L1|| < (||v|| + 1) + 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||)
8. 0 < (||v|| + 1) + 1
9. [u; [u1 / v]] ~ firstn(((||v|| + 1) + 1) - 1;[u; [u1 / v]]) @ [last([u; [u1 / v]])]
10. ¬False
11. ¬1 < (||v|| + 1) + 1
⊢ let n,x = outl(case list-max-aux(x.f[x];firstn(((||v|| + 1) + 1) - 1;[u; [u1 / v]]))
   of inl(p) =>
   if fst(p) <z f[last([u; [u1 / v]])]
   then inl <f[last([u; [u1 / v]])], last([u; [u1 / v]])>
   else list-max-aux(x.f[x];firstn(((||v|| + 1) + 1) - 1;[u; [u1 / v]]))
   fi 
   | inr(q) =>
   inl <f[last([u; [u1 / v]])], last([u; [u1 / v]])>) 
  in (x ∈ firstn(((||v|| + 1) + 1) - 1;[u; [u1 / v]]) @ [last([u; [u1 / v]])])
     ∧ (f[x] = n ∈ ℤ)
     ∧ (∀y∈firstn(((||v|| + 1) + 1) - 1;[u; [u1 / v]]) @ [last([u; [u1 / v]])].f[y] ≤ n)
BY
{ (D (-1) THEN Auto') }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}
4.  u  :  T
5.  u1  :  T
6.  v  :  T  List
7.  \mforall{}L1:T  List
          (||L1||  <  (||v||  +  1)  +  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||)
8.  0  <  (||v||  +  1)  +  1
9.  [u;  [u1  /  v]]  \msim{}  firstn(((||v||  +  1)  +  1)  -  1;[u;  [u1  /  v]])  @  [last([u;  [u1  /  v]])]
10.  \mneg{}False
11.  \mneg{}1  <  (||v||  +  1)  +  1
\mvdash{}  let  n,x  =  outl(case  list-max-aux(x.f[x];firstn(((||v||  +  1)  +  1)  -  1;[u;  [u1  /  v]]))
      of  inl(p)  =>
      if  fst(p)  <z  f[last([u;  [u1  /  v]])]
      then  inl  <f[last([u;  [u1  /  v]])],  last([u;  [u1  /  v]])>
      else  list-max-aux(x.f[x];firstn(((||v||  +  1)  +  1)  -  1;[u;  [u1  /  v]]))
      fi 
      |  inr(q)  =>
      inl  <f[last([u;  [u1  /  v]])],  last([u;  [u1  /  v]])>) 
    in  (x  \mmember{}  firstn(((||v||  +  1)  +  1)  -  1;[u;  [u1  /  v]])  @  [last([u;  [u1  /  v]])])
          \mwedge{}  (f[x]  =  n)
          \mwedge{}  (\mforall{}y\mmember{}firstn(((||v||  +  1)  +  1)  -  1;[u;  [u1  /  v]])  @  [last([u;  [u1  /  v]])].f[y]  \mleq{}  n)


By

---

Latex:
(D  (-1)  THEN  Auto')

---

Home Index