---

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

.....subterm..... T:t
2:n
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
⊢ 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, g x> else a fi  | inr(q) => inl <n, g x>
       over list:
         v
       with starting value:
        eval n = f[g u1] in
        if fst(outl(inl x)) <z n then inl <n, g u1> else inl <fst(outl(inl x)), g (snd(outl(inl x)))> fi ))
= 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, g x> else a fi  | inr(q) => inl <n, g x>
       over list:
         v
       with starting value:
        (λp.(inl <fst(outl(p)), g (snd(outl(p)))>)) 
        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>))
∈ (i:ℤ × T)
BY
{ ((RW (AddrC [2;1;2] CallByValueC) 0 THENA Auto)
   THEN (RW (AddrC [3;1;2;2] CallByValueC) 0 THENA Auto)⋅
   THEN Reduce 0
   THEN AutoSplit
   THEN Fold `member` 0
   THEN ((GenConclAtAddrType  ⌜{x:ℤ × T + Top| ↑isl(x)} ⌝ [2;1]⋅
          THENA (Auto
                 THEN Auto
                 THEN (CallByValueReduce 0 THEN Auto)
                 THEN D -2
                 THEN D -3
                 THEN Reduce 0
                 THEN Auto
                 THEN AutoSplit)
          )
         THEN D (-2)
         THEN D -3
         THEN All Reduce 
         THEN Auto)⋅) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{}  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,  g  x>  else  a  fi    |  inr(q)  =>  inl  <n,  g  x>
              over  list:
                  v
              with  starting  value:
                eval  n  =  f[g  u1]  in
                if  fst(outl(inl  x))  <z  n  then  inl  <n,  g  u1>  else  inl  <fst(outl(inl  x)),  g  (snd(outl(inl  x)))\000C>  fi  ))
=  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,  g  x>  else  a  fi    |  inr(q)  =>  inl  <n,  g  x>
              over  list:
                  v
              with  starting  value:
                (\mlambda{}p.(inl  <fst(outl(p)),  g  (snd(outl(p)))>)) 
                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,  u\000C1>))


By

---

Latex:
((RW  (AddrC  [2;1;2]  CallByValueC)  0  THENA  Auto)
  THEN  (RW  (AddrC  [3;1;2;2]  CallByValueC)  0  THENA  Auto)\mcdot{}
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Fold  `member`  0
  THEN  ((GenConclAtAddrType    \mkleeneopen{}\{x:\mBbbZ{}  \mtimes{}  T  +  Top|  \muparrow{}isl(x)\}  \mkleeneclose{}  [2;1]\mcdot{}
                THENA  (Auto
                              THEN  Auto
                              THEN  (CallByValueReduce  0  THEN  Auto)
                              THEN  D  -2
                              THEN  D  -3
                              THEN  Reduce  0
                              THEN  Auto
                              THEN  AutoSplit)
                )
              THEN  D  (-2)
              THEN  D  -3
              THEN  All  Reduce 
              THEN  Auto)\mcdot{})

---

Home Index