---

Step * 1 1 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)
⊢ 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
{ (InstLemma `list_accum-set-equal-idemp`  [⌜T⌝;⌜eq⌝;⌜ℕ⌝;⌜f⌝;⌜λ2x y.imax(x;y)⌝;⌜s⌝;⌜s1⌝;⌜0⌝]⋅ THENA Auto) }

1
.....antecedent..... 
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)
⊢ Comm(ℕ;λx,y. imax(x;y))

2
.....antecedent..... 
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)
⊢ Assoc(ℕ;λx,y. imax(x;y))

3
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)
∈ ℕ

---

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)
\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:
(InstLemma  `list\_accum-set-equal-idemp` 
  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.imax(x;y)\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index