---

Step * 2 1 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)
9. 1 < ||L||
10. (↑isl(list-max-aux(x.f[x];firstn(||L|| - 1;L))))
∧ let n,x = outl(list-max-aux(x.f[x];firstn(||L|| - 1;L))) 
  in (x ∈ firstn(||L|| - 1;L)) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈firstn(||L|| - 1;L).f[y] ≤ n)
⊢ 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)
BY
{ (MoveToConcl (-1)
   THEN GenConclAtAddr [1;1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN Try ((TACTIC:(At ⌜Type⌝ (D 0)⋅ THENM (D (-1) THEN Trivial)) THENA Auto)⋅)
   THEN D (-2)
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto
   THEN skip{(RWW "l_all_append member_append" 0⋅
              THEN Auto
              THEN Try ((RepeatFor 3 (ParallelLast) THEN Complete (Auto)))
              THEN OrRight
              THEN Auto)}) }

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)
9. 1 < ||L||
10. i : ℤ
11. x1 : {x:T| f[x] = i ∈ ℤ} 
12. list-max-aux(x.f[x];firstn(||L|| - 1;L)) = (inl <i, x1>) ∈ (i:ℤ × {x:T| f[x] = i ∈ ℤ}  + Top)
13. i < f[last(L)]
14. True
15. (x1 ∈ firstn(||L|| - 1;L))
16. f[x1] = i ∈ ℤ
17. (∀y∈firstn(||L|| - 1;L).f[y] ≤ i)
18. (last(L) ∈ firstn(||L|| - 1;L) @ [last(L)])
19. f[last(L)] = f[last(L)] ∈ ℤ
⊢ (∀y∈firstn(||L|| - 1;L) @ [last(L)].f[y] ≤ f[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)
9. 1 < ||L||
10. i : ℤ
11. ¬i < f[last(L)]
12. x1 : {x:T| f[x] = i ∈ ℤ} 
13. list-max-aux(x.f[x];firstn(||L|| - 1;L)) = (inl <i, x1>) ∈ (i:ℤ × {x:T| f[x] = i ∈ ℤ}  + Top)
14. True
15. (x1 ∈ firstn(||L|| - 1;L))
16. f[x1] = i ∈ ℤ
17. (∀y∈firstn(||L|| - 1;L).f[y] ≤ i)
18. (x1 ∈ firstn(||L|| - 1;L) @ [last(L)])
19. f[x1] = i ∈ ℤ
⊢ (∀y∈firstn(||L|| - 1;L) @ [last(L)].f[y] ≤ i)

---

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)
9.  1  <  ||L||
10.  (\muparrow{}isl(list-max-aux(x.f[x];firstn(||L||  -  1;L))))
\mwedge{}  let  n,x  =  outl(list-max-aux(x.f[x];firstn(||L||  -  1;L))) 
    in  (x  \mmember{}  firstn(||L||  -  1;L))  \mwedge{}  (f[x]  =  n)  \mwedge{}  (\mforall{}y\mmember{}firstn(||L||  -  1;L).f[y]  \mleq{}  n)
\mvdash{}  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  \mmember{}  firstn(||L||  -  1;L)  @  [last(L)])
          \mwedge{}  (f[x]  =  n)
          \mwedge{}  (\mforall{}y\mmember{}firstn(||L||  -  1;L)  @  [last(L)].f[y]  \mleq{}  n)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Try  ((TACTIC:(At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENM  (D  (-1)  THEN  Trivial))  THENA  Auto)\mcdot{})
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto
  THEN  skip\{(RWW  "l\_all\_append  member\_append"  0\mcdot{}
                        THEN  Auto
                        THEN  Try  ((RepeatFor  3  (ParallelLast)  THEN  Complete  (Auto)))
                        THEN  OrRight
                        THEN  Auto)\})

---

Home Index