---

Step * 1 1 3 of Lemma fset-max_wf


1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. f : T ⟶ ℕ
4. s : Base
5. s1 : Base
6. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
7. s ∈ T List
8. s1 ∈ T List
9. set-equal(T;s;s1)
10. eq : EqDecider(T)
11. accumulate (with value a and list item z):
     imax(a;f[z])
    over list:
      s
    with starting value:
     0)
= accumulate (with value a and list item z):
   imax(a;f[z])
  over list:
    s1
  with starting value:
   0)
∈ ℕ
⊢ accumulate (with value x and list item y):
   imax(x;y)
  over list:
    map(f;s)
  with starting value:
   0)
= accumulate (with value x and list item y):
   imax(x;y)
  over list:
    map(f;s1)
  with starting value:
   0)
∈ ℕ
BY
{ (NthHypSq (-1)
   THEN (EqCD THEN Auto)
   THEN ((GenConcl ⌜0 = n ∈ ℤ⌝⋅ THENA Auto) THEN RepUR ``so_apply`` 0)
   THEN GenConclTerms Auto [⌜s⌝;⌜s1⌝]⋅
   THEN PromoteHyp (-2) 2
   THEN PromoteHyp (-3) 2
   THEN Lemmaize []
   THEN InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  f  :  T  {}\mrightarrow{}  \mBbbN{}
4.  s  :  Base
5.  s1  :  Base
6.  s  =  s1
7.  s  \mmember{}  T  List
8.  s1  \mmember{}  T  List
9.  set-equal(T;s;s1)
10.  eq  :  EqDecider(T)
11.  accumulate  (with  value  a  and  list  item  z):
          imax(a;f[z])
        over  list:
            s
        with  starting  value:
          0)
=  accumulate  (with  value  a  and  list  item  z):
      imax(a;f[z])
    over  list:
        s1
    with  starting  value:
      0)
\mvdash{}  accumulate  (with  value  x  and  list  item  y):
      imax(x;y)
    over  list:
        map(f;s)
    with  starting  value:
      0)
=  accumulate  (with  value  x  and  list  item  y):
      imax(x;y)
    over  list:
        map(f;s1)
    with  starting  value:
      0)


By

---

Latex:
(NthHypSq  (-1)
  THEN  (EqCD  THEN  Auto)
  THEN  ((GenConcl  \mkleeneopen{}0  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  RepUR  ``so\_apply``  0)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{}]\mcdot{}
  THEN  PromoteHyp  (-2)  2
  THEN  PromoteHyp  (-3)  2
  THEN  Lemmaize  []
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp)\mcdot{}

---

Home Index