Step
*
1
2
of Lemma
rng_prod_plus
.....subterm..... T:t
3:n
1. r : CRng
2. n : ℤ
3. 0 < n
4. F : ℕn ⟶ |r|
5. G : ℕn ⟶ |r|
6. ∀[f:(ℕn ⟶ ℕ2) ⟶ |r|]. ∀[as:(ℕn ⟶ ℕ2) List].
(Σ{r} x ∈ as. f[x]
= (Σ{r} x ∈ filter(λ2p.(p (n - 1) =z 0);as). f[x] +r Σ{r} x ∈ filter(λa.(¬b(a (n - 1) =z 0));as). f[x])
∈ |r|)
⊢ (Σ{r} p ∈ functions-list(n - 1;2). (Π(r) 0 ≤ i < n - 1. if (p i =z 0) then F[i] else G[i] fi ) * G[n - 1])
= Σ{r} p ∈ filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)). ((Π(r) 0
≤ i
< n - 1
if (p i =z 0) then F[i] else G[i] fi )
*
if (p (n - 1) =z 0) then F[n - 1] else G[n - 1] fi )
∈ |r|
BY
{ Assert ⌜(Σ{r} p ∈ functions-list(n - 1;2). (Π(r) 0 ≤ i < n - 1. if (p i =z 0) then F[i] else G[i] fi ) * G[n - 1])
= Σ{r} p ∈ filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)). ((Π(r) 0
≤ i
< n - 1
if (p i =z 0) then F[i] else G[i] fi )
*
G[n - 1])
∈ |r|⌝⋅ }
1
.....assertion.....
1. r : CRng
2. n : ℤ
3. 0 < n
4. F : ℕn ⟶ |r|
5. G : ℕn ⟶ |r|
6. ∀[f:(ℕn ⟶ ℕ2) ⟶ |r|]. ∀[as:(ℕn ⟶ ℕ2) List].
(Σ{r} x ∈ as. f[x]
= (Σ{r} x ∈ filter(λ2p.(p (n - 1) =z 0);as). f[x] +r Σ{r} x ∈ filter(λa.(¬b(a (n - 1) =z 0));as). f[x])
∈ |r|)
⊢ (Σ{r} p ∈ functions-list(n - 1;2). (Π(r) 0 ≤ i < n - 1. if (p i =z 0) then F[i] else G[i] fi ) * G[n - 1])
= Σ{r} p ∈ filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)). ((Π(r) 0
≤ i
< n - 1
if (p i =z 0) then F[i] else G[i] fi )
*
G[n - 1])
∈ |r|
2
1. r : CRng
2. n : ℤ
3. 0 < n
4. F : ℕn ⟶ |r|
5. G : ℕn ⟶ |r|
6. ∀[f:(ℕn ⟶ ℕ2) ⟶ |r|]. ∀[as:(ℕn ⟶ ℕ2) List].
(Σ{r} x ∈ as. f[x]
= (Σ{r} x ∈ filter(λ2p.(p (n - 1) =z 0);as). f[x] +r Σ{r} x ∈ filter(λa.(¬b(a (n - 1) =z 0));as). f[x])
∈ |r|)
7. (Σ{r} p ∈ functions-list(n - 1;2). (Π(r) 0 ≤ i < n - 1. if (p i =z 0) then F[i] else G[i] fi ) * G[n - 1])
= Σ{r} p ∈ filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)). ((Π(r) 0
≤ i
< n - 1
if (p i =z 0) then F[i] else G[i] fi )
*
G[n - 1])
∈ |r|
⊢ (Σ{r} p ∈ functions-list(n - 1;2). (Π(r) 0 ≤ i < n - 1. if (p i =z 0) then F[i] else G[i] fi ) * G[n - 1])
= Σ{r} p ∈ filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)). ((Π(r) 0
≤ i
< n - 1
if (p i =z 0) then F[i] else G[i] fi )
*
if (p (n - 1) =z 0) then F[n - 1] else G[n - 1] fi )
∈ |r|
Latex:
Latex:
.....subterm..... T:t
3:n
1. r : CRng
2. n : \mBbbZ{}
3. 0 < n
4. F : \mBbbN{}n {}\mrightarrow{} |r|
5. G : \mBbbN{}n {}\mrightarrow{} |r|
6. \mforall{}[f:(\mBbbN{}n {}\mrightarrow{} \mBbbN{}2) {}\mrightarrow{} |r|]. \mforall{}[as:(\mBbbN{}n {}\mrightarrow{} \mBbbN{}2) List].
(\mSigma{}\{r\} x \mmember{} as. f[x]
= (\mSigma{}\{r\} x \mmember{} filter(\mlambda{}\msubtwo{}p.(p (n - 1) =\msubz{} 0);as). f[x]
+r
\mSigma{}\{r\} x \mmember{} filter(\mlambda{}a.(\mneg{}\msubb{}(a (n - 1) =\msubz{} 0));as). f[x]))
\mvdash{} (\mSigma{}\{r\} p \mmember{} functions-list(n - 1;2). (\mPi{}(r) 0
\mleq{} i
< n - 1
if (p i =\msubz{} 0) then F[i] else G[i] fi )
*
G[n - 1])
= \mSigma{}\{r\} p \mmember{} filter(\mlambda{}a.(\mneg{}\msubb{}(a (n - 1) =\msubz{} 0));functions-list(n;2)). ((\mPi{}(r) 0
\mleq{} i
< n - 1
if (p i =\msubz{} 0)
then F[i]
else G[i]
fi )
*
if (p (n - 1) =\msubz{} 0)
then F[n - 1]
else G[n - 1]
fi )
By
Latex:
Assert \mkleeneopen{}(\mSigma{}\{r\} p \mmember{} functions-list(n - 1;2). (\mPi{}(r) 0
\mleq{} i
< n - 1
if (p i =\msubz{} 0) then F[i] else G[i] fi )
*
G[n - 1])
= \mSigma{}\{r\} p \mmember{} filter(\mlambda{}a.(\mneg{}\msubb{}(a (n - 1) =\msubz{} 0));functions-list(n;2)). ((\mPi{}(r) 0
\mleq{} i
< n - 1
if (p i =\msubz{} 0)
then F[i]
else G[i]
fi )
*
G[n - 1])\mkleeneclose{}\mcdot{}
Home
Index