Step
*
1
2
1
1
1
of Lemma
rng_prod_plus
.....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|)
∈ ℙ
BY
{ (EqCDA
THENL [((Assert map(λf,i. if (i =z n - 1) then 1 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List BY
Auto)
THEN (BLemma `rng_lsum_functionality_wrt_permutation` THENA Auto)
THEN ThinVar `r')
; (RepeatFor 3 (EqCDA) THEN AutoSplit)]
) }
1
1. n : ℤ
2. 0 < n
3. filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
4. map(λf,i. if (i =z n - 1) then 1 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List
⊢ permutation(ℕn ⟶ ℕ2;filter(λa.(¬b(a (n - 1) =z 0));functions-list(n;2));
map(λf,i. if (i =z n - 1) then 1 else f i fi ;functions-list(n - 1;2)))
Latex:
Latex:
.....assertion.....
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
8. \mSigma{}\{r\} x \mmember{} map(\mlambda{}f,i. if (i =\msubz{} n - 1) then 1 else f i fi ;functions-list(n - 1;2)). ((\mPi{}(r) 0
\mleq{} i
< n - 1
if (x i =\msubz{} 0)
then F[i]
else G[i]
fi )
*
G[n - 1])
= \mSigma{}\{r\} x \mmember{} functions-list(n - 1;2). ((\mPi{}(r) 0
\mleq{} i
< n - 1
if (if (i =\msubz{} n - 1) then 1 else x i fi =\msubz{} 0)
then F[i]
else G[i]
fi )
*
G[n - 1])
\mvdash{} (\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])
= \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\} x \mmember{} map(\mlambda{}f,i. if (i =\msubz{} n - 1) then 1 else f i fi ;functions-list(n - 1;2)). ((\mPi{}(r) 0
\mleq{} i
< n - 1
if (x i =\msubz{} 0)
then F[i]
else G[i]
fi )
*
G[n - 1])
= \mSigma{}\{r\} x \mmember{} functions-list(n - 1;2). ((\mPi{}(r) 0
\mleq{} i
< n - 1
if (if (i =\msubz{} n - 1) then 1 else x i fi =\msubz{} 0)
then F[i]
else G[i]
fi )
*
G[n - 1]))
By
Latex:
(EqCDA
THENL [((Assert map(\mlambda{}f,i. if (i =\msubz{} n - 1) then 1 else f i fi ;functions-list(n - 1;2)) \mmember{} (\mBbbN{}n
{}\mrightarrow{} \mBbbN{}2) List BY
Auto)
THEN (BLemma `rng\_lsum\_functionality\_wrt\_permutation` THENA Auto)
THEN ThinVar `r')
; (RepeatFor 3 (EqCDA) THEN AutoSplit)]
)
Home
Index