---

Step * 1 of Lemma list-max-map

.....assertion..... 
1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. L : A List
6. 0 < ||L||
⊢ list-max(x.f[x];map(g;L)) = ((λp.<fst(p), g (snd(p))>) list-max(x.f[g x];L)) ∈ (i:ℤ × T)
BY
{ (Unfold `list-max` 0
   THEN Unfold `list-max-aux` 0
   THEN (RWO "list_accum-map" 0 THENA Auto)
   THEN DVar `L'
   THEN Reduce (-1)
   THEN Try (Complete (Auto))
   THEN Thin (-1)
   THEN Reduce 0
   THEN (CallByValueReduceOn ⌜f[g u]⌝ 0⋅ THENA Auto)
   THEN (Subst' inl <f[g u], g u> ~ (λp.(inl <fst(outl(p)), g (snd(outl(p)))>)) (inl <f[g u], u>) 0⋅ THENA (Reduce 0 THE\000CN Trivial))
   THEN (GenConcl ⌜(inl <f[g u], u>) = Z ∈ {x:ℤ × A + Top| ↑isl(x)} ⌝⋅ THENA Auto)⋅
   THEN (Thin (-1) THEN MoveToConcl (-1) THEN ListInd (-1) THEN Reduce 0 THEN Auto)⋅) }

1
1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. u : A
6. u1 : A
7. v : A List
8. ∀Z:{x:ℤ × A + Top| ↑isl(x)} 
     (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)))>)) Z))
     = <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:
                  Z)))
       , g 
         (snd(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:
                    Z))))
       >
     ∈ (i:ℤ × T))
9. Z : {x:ℤ × A + Top| ↑isl(x)} @i
⊢ 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(Z)) <z n then inl <n, g u1> else inl <fst(outl(Z)), g (snd(outl(Z)))> fi ))
= <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 Z of inl(p) => if fst(p) <z n then inl <n, u1> else Z fi  | inr(q) => inl <n, u1>)))
  , g 
    (snd(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 Z of inl(p) => if fst(p) <z n then inl <n, u1> else Z fi  | inr(q) => inl <n, u1>))))
  >
∈ (i:ℤ × T)

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  A  :  Type
3.  g  :  A  {}\mrightarrow{}  T
4.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
5.  L  :  A  List
6.  0  <  ||L||
\mvdash{}  list-max(x.f[x];map(g;L))  =  ((\mlambda{}p.<fst(p),  g  (snd(p))>)  list-max(x.f[g  x];L))


By

---

Latex:
(Unfold  `list-max`  0
  THEN  Unfold  `list-max-aux`  0
  THEN  (RWO  "list\_accum-map"  0  THENA  Auto)
  THEN  DVar  `L'
  THEN  Reduce  (-1)
  THEN  Try  (Complete  (Auto))
  THEN  Thin  (-1)
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}f[g  u]\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  inl  <f[g  u],  g  u>  \msim{}  (\mlambda{}p.(inl  <fst(outl(p)),  g  (snd(outl(p)))>))  (inl  <f[g  u],  u>)  0\mcdot{}  T\000CHENA  (Reduce  0  THEN  Trivial))
  THEN  (GenConcl  \mkleeneopen{}(inl  <f[g  u],  u>)  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (Thin  (-1)  THEN  MoveToConcl  (-1)  THEN  ListInd  (-1)  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index