Step
*
2
1
2
1
1
1
2
of Lemma
KozenSilva-theorem
.....subterm..... T:t
4:n
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. h : PowerSeries(r)
6. d : ℕ ⟶ ℕ
7. k : ℤ
8. k ∈ ℕ
9. k ≠ 0
10. 0 < k
11. [Moessner-aux(r;x;y;h;d;k - 1)]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
12. Σ(d i | i < k) ∈ ℕ
13. Σ(d i | i < k + 1) ∈ ℕ
14. [([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)
+atom(y)))^(d (i + 1)))]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
15. Σ(d i | i < k) ≤ Σ(d i | i < k + 1)
⊢ (Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))(y:=(atom(x)+atom(y)))*((atom(x)
+atom(y)))^(Σ(d i | i < k
+ 1) - Σ(d i | i < k)))
= Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))
∈ PowerSeries(r)
BY
{ TACTIC:((Subst' ⌜(Σ(d i | i < k + 1) - Σ(d i | i < k)) = (d k) ∈ ℤ⌝ 0⋅
THENA (RW (AddrC [2;1] (LemmaC `sum_split1`)) 0 THEN Auto')⋅
)
THEN (Subst ⌜upto(k) ~ upto(k - 1) + {k - 1}⌝ 0⋅
THENA ((RepUR ``bag-append single-bag`` 0 THEN BLemma `upto_decomp1`) THEN Auto)
)
) }
1
1. r : CRng
2. x : Atom
3. y : Atom
4. ¬(x = y ∈ Atom)
5. h : PowerSeries(r)
6. d : ℕ ⟶ ℕ
7. k : ℤ
8. k ∈ ℕ
9. k ≠ 0
10. 0 < k
11. [Moessner-aux(r;x;y;h;d;k - 1)]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
12. Σ(d i | i < k) ∈ ℕ
13. Σ(d i | i < k + 1) ∈ ℕ
14. [([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)
+atom(y)))^(d (i + 1)))]_Σ(d i | i < k)
= ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
15. Σ(d i | i < k) ≤ Σ(d i | i < k + 1)
⊢ (Π(i∈upto(k - 1)).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(d k))
= Π(i∈upto(k - 1) + {k - 1}).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))
∈ PowerSeries(r)
Latex:
Latex:
.....subterm..... T:t
4:n
1. r : CRng
2. x : Atom
3. y : Atom
4. \mneg{}(x = y)
5. h : PowerSeries(r)
6. d : \mBbbN{} {}\mrightarrow{} \mBbbN{}
7. k : \mBbbZ{}
8. k \mmember{} \mBbbN{}
9. k \mneq{} 0
10. 0 < k
11. [Moessner-aux(r;x;y;h;d;k - 1)]\_\mSigma{}(d i | i < k)
= ([h]\_d 0(y:=(((k - 1) \mcdot{}r 1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k
- 1)).((((k - 1 - i) \mcdot{}r 1)*atom(x)+atom(y)))\^{}(d (i + 1)))
12. \mSigma{}(d i | i < k) \mmember{} \mBbbN{}
13. \mSigma{}(d i | i < k + 1) \mmember{} \mBbbN{}
14. [([h]\_d 0(y:=(((k - 1) \mcdot{}r 1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k
- 1)).((((k - 1 - i) \mcdot{}r 1)*atom(x)+atom(y)))\^{}(d (i + 1)))]\_\mSigma{}(d i | i < k)
= ([h]\_d 0(y:=(((k - 1) \mcdot{}r 1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k
- 1)).((((k - 1 - i) \mcdot{}r 1)*atom(x)+atom(y)))\^{}(d (i + 1)))
15. \mSigma{}(d i | i < k) \mleq{} \mSigma{}(d i | i < k + 1)
\mvdash{} (\mPi{}(i\mmember{}upto(k - 1)).((((k - 1 - i) \mcdot{}r 1)*atom(x)
+atom(y)))\^{}(d (i + 1))(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))\^{}(\mSigma{}(d
i | i < k
+ 1) - \mSigma{}(d i | i < k)))
= \mPi{}(i\mmember{}upto(k)).((((k - i) \mcdot{}r 1)*atom(x)+atom(y)))\^{}(d (i + 1))
By
Latex:
TACTIC:((Subst' \mkleeneopen{}(\mSigma{}(d i | i < k + 1) - \mSigma{}(d i | i < k)) = (d k)\mkleeneclose{} 0\mcdot{}
THENA (RW (AddrC [2;1] (LemmaC `sum\_split1`)) 0 THEN Auto')\mcdot{}
)
THEN (Subst \mkleeneopen{}upto(k) \msim{} upto(k - 1) + \{k - 1\}\mkleeneclose{} 0\mcdot{}
THENA ((RepUR ``bag-append single-bag`` 0 THEN BLemma `upto\_decomp1`) THEN Auto)
)
)
Home
Index