---

Step * of Lemma tuple-sum-wf-partial

∀[P:Type]. ∀[G:P ⟶ Type]. ∀[f:i:P ⟶ (G i) ⟶ partial(ℕ)]. ∀[as:P List]. ∀[x:tuple-type(map(G;as))].
  (tuple-sum(f;as;x) ∈ partial(ℕ))
BY
{ (InductionOnList
   THEN Unfold `tuple-sum` 0
   THEN Reduce 0
   THEN ((RWO "null-map" 0 THENA Auto) ORELSE Auto)
   THEN (SimpleBoolCase ⌜null(v)⌝⋅ THENA Auto)) }

1
1. P : Type
2. G : P ⟶ Type
3. f : i:P ⟶ (G i) ⟶ partial(ℕ)
4. u : P
5. v : P List
6. ∀[x:tuple-type(map(G;v))]. (tuple-sum(f;v;x) ∈ partial(ℕ))
7. null(v) = tt
⊢ ∀[x@0:G u]. (f u x@0 ∈ partial(ℕ))

2
1. P : Type
2. G : P ⟶ Type
3. f : i:P ⟶ (G i) ⟶ partial(ℕ)
4. u : P
5. v : P List
6. ∀[x:tuple-type(map(G;v))]. (tuple-sum(f;v;x) ∈ partial(ℕ))
7. null(v) = ff
⊢ ∀[x:G u × tuple-type(map(G;v))]. (let u@0,v@0 = x in (f u u@0) + tuple-sum(f;v;v@0) ∈ partial(ℕ))

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[G:P  {}\mrightarrow{}  Type].  \mforall{}[f:i:P  {}\mrightarrow{}  (G  i)  {}\mrightarrow{}  partial(\mBbbN{})].  \mforall{}[as:P  List].
\mforall{}[x:tuple-type(map(G;as))].
    (tuple-sum(f;as;x)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `tuple-sum`  0
  THEN  Reduce  0
  THEN  ((RWO  "null-map"  0  THENA  Auto)  ORELSE  Auto)
  THEN  (SimpleBoolCase  \mkleeneopen{}null(v)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index