---

Step * of Lemma fset-max_wf

∀[T:Type]. ∀[f:T ⟶ ℕ]. ∀[s:fset(T)].  (fset-max(f;s) ∈ ℕ) supposing ∀x,y:T.  Dec(x = y ∈ T)
BY
{ ((UnivCD THENA Auto) THEN (D -1 THENA Auto) THEN RepUR ``fset-max imax-list combine-list`` 0) }

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)
⊢ 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:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[s:fset(T)].    (fset-max(f;s)  \mmember{}  \mBbbN{})  supposing  \mforall{}x,y:T.    Dec(x  =  y)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (D  -1  THENA  Auto)  THEN  RepUR  ``fset-max  imax-list  combine-list``  0)

---

Home Index