---

Step * 1 1 1 2 of Lemma list-max-map


1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. u : A
6. u1 : A
7. v : A List
8. x : ℤ × A@i
9. True
⊢ fst(outl(accumulate (with value a and list item x):
            eval n = f[g x] in
            case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi  | inr(q) => inl <n, x>
           over list:
             v
           with starting value:
            eval n = f[g u1] in
            case inl x of inl(p) => if fst(p) <z n then inl <n, u1> else inl x fi  | inr(q) => inl <n, u1>))) ∈ ℤ
BY
{ TACTIC:((GenConclAtAddrType  ⌜{x:ℤ × A + Top| ↑isl(x)} ⌝ [2;1;1]⋅ THENA Auto)
THENM (D (-2) THEN D -3 THEN All Reduce  THEN Auto)
) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  g  :  A  {}\mrightarrow{}  T
4.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
5.  u  :  A
6.  u1  :  A
7.  v  :  A  List
8.  x  :  \mBbbZ{}  \mtimes{}  A@i
9.  True
\mvdash{}  fst(outl(accumulate  (with  value  a  and  list  item  x):
                        eval  n  =  f[g  x]  in
                        case  a  of  inl(p)  =>  if  fst(p)  <z  n  then  inl  <n,  x>  else  a  fi    |  inr(q)  =>  inl  <n,  x>
                      over  list:
                          v
                      with  starting  value:
                        eval  n  =  f[g  u1]  in
                        case  inl  x
                          of  inl(p)  =>
                          if  fst(p)  <z  n  then  inl  <n,  u1>  else  inl  x  fi 
                          |  inr(q)  =>
                          inl  <n,  u1>)))  \mmember{}  \mBbbZ{}


By

---

Latex:
TACTIC:((GenConclAtAddrType    \mkleeneopen{}\{x:\mBbbZ{}  \mtimes{}  A  +  Top|  \muparrow{}isl(x)\}  \mkleeneclose{}  [2;1;1]\mcdot{}  THENA  Auto)
THENM  (D  (-2)  THEN  D  -3  THEN  All  Reduce    THEN  Auto)
)

---

Home Index