---

Step * 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)
⊢ 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
{ ((Assert EqDecider(T) BY (RenameVar `p' 2 THEN UseWitness ⌜mk_deq(p)⌝⋅ THEN Auto)) THEN RenameVar `eq' (-1)) }

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

---

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)
\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:
((Assert  EqDecider(T)  BY
                (RenameVar  `p'  2  THEN  UseWitness  \mkleeneopen{}mk\_deq(p)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  RenameVar  `eq'  (-1)
  )

---

Home Index