Step
*
1
2
1
1
of Lemma
rng_prod_plus
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. filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
⊢ Σ{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|
BY
{ ((InstLemma `rng_lsum_map` [⌜r⌝;⌜ℕn - 1 ⟶ ℕ2⌝;⌜ℕn ⟶ ℕ2⌝;⌜λf,i. if (i =z n - 1) then 1 else f i fi ⌝;⌜λ2p.(Π(r) 0
≤ i
< n - 1
if (p i =z 0)
then F[i]
else G[i]
fi )
*
G[n - 1]⌝;
⌜functions-list(n - 1;2)⌝]⋅
THENA Auto
)
THEN Reduce -1
THEN Symmetry
THEN NthHypEq (-1)) }
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|)
7. filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
8. Σ{r} x ∈ map(λf,i. if (i =z n - 1) then 1 else f i fi ;functions-list(n - 1;2)). ((Π(r) 0
≤ i
< n - 1
if (x i =z 0)
then F[i]
else G[i]
fi )
*
G[n - 1])
= Σ{r} x ∈ functions-list(n - 1;2). ((Π(r) 0
≤ i
< n - 1
if (if (i =z n - 1) then 1 else x i fi =z 0) then F[i] else G[i] fi )
*
G[n - 1])
∈ |r|
⊢ (Σ{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} 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|)
= (Σ{r} x ∈ map(λf,i. if (i =z n - 1) then 1 else f i fi ;functions-list(n - 1;2)). ((Π(r) 0
≤ i
< n - 1
if (x i =z 0)
then F[i]
else G[i]
fi )
*
G[n - 1])
= Σ{r} x ∈ functions-list(n - 1;2). ((Π(r) 0
≤ i
< n - 1
if (if (i =z n - 1) then 1 else x i fi =z 0) then F[i] else G[i] fi )
*
G[n - 1])
∈ |r|)
∈ ℙ
Latex:
Latex:
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]))
7. filter(\mlambda{}a.(\mneg{}\msubb{}(a (n - 1) =\msubz{} 0));functions-list(n;2)) \mmember{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}2) List
\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 )
*
G[n - 1])
By
Latex:
((InstLemma `rng\_lsum\_map` [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mBbbN{}n - 1 {}\mrightarrow{} \mBbbN{}2\mkleeneclose{};\mkleeneopen{}\mBbbN{}n {}\mrightarrow{} \mBbbN{}2\mkleeneclose{};\mkleeneopen{}\mlambda{}f,i. if (i =\msubz{} n - 1) then 1 else f i fi \000C\mkleeneclose{};
\mkleeneopen{}\mlambda{}\msubtwo{}p.(\mPi{}(r) 0 \mleq{} i < n - 1. if (p i =\msubz{} 0) then F[i] else G[i] fi ) * G[n - 1]\mkleeneclose{};
\mkleeneopen{}functions-list(n - 1;2)\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN Reduce -1
THEN Symmetry
THEN NthHypEq (-1))
Home
Index