---

Step * 2 of Lemma sum-has-value


1. n : Base
2. f : Base
3. (Σ(f[x] | x < n))↓
4. n ∈ ℤ
⊢ f ∈ ℕn ⟶ ℤ
BY
{ TACTIC:(Unfold `sum` -2
          THEN Assert ⌜∀d,n,m:ℕ.  (((n - m) ≤ d) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))⌝⋅
          ) }

1
.....assertion..... 
1. n : Base
2. f : Base
3. (sum_aux(n;0;0;x.f[x]))↓
4. n ∈ ℤ
⊢ ∀d,n,m:ℕ.  (((n - m) ≤ d) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))

2
1. n : Base
2. f : Base
3. (sum_aux(n;0;0;x.f[x]))↓
4. n ∈ ℤ
5. ∀d,n,m:ℕ.  (((n - m) ≤ d) ⇒ (∀v:ℤ. ((sum_aux(n;v;m;x.f[x]))↓ ⇒ (f ∈ {m..n-} ⟶ ℤ))))
⊢ f ∈ ℕn ⟶ ℤ

---

Latex:

---

Latex:

1.  n  :  Base
2.  f  :  Base
3.  (\mSigma{}(f[x]  |  x  <  n))\mdownarrow{}
4.  n  \mmember{}  \mBbbZ{}
\mvdash{}  f  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}


By

---

Latex:
TACTIC:(Unfold  `sum`  -2
                THEN  Assert  \mkleeneopen{}\mforall{}d,n,m:\mBbbN{}.
                                              (((n  -  m)  \mleq{}  d)  {}\mRightarrow{}  (\mforall{}v:\mBbbZ{}.  ((sum\_aux(n;v;m;x.f[x]))\mdownarrow{}  {}\mRightarrow{}  (f  \mmember{}  \{m..n\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}))))\mkleeneclose{}\mcdot{}
                )

---

Home Index