Step
*
2
1
2
1
1
1
2
1
of Lemma
KozenSilva-theorem
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)
BY
{ TACTIC:((GenConcl ⌜upto(k - 1) = ks ∈ bag(ℕk - 1)⌝⋅ THENA Auto)
THEN RWO "fps-compose-fps-product" 0⋅
THEN Try (Complete (Auto'))) }
1
.....wf.....
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)
16. ks : bag(ℕk - 1)
17. upto(k - 1) = ks ∈ bag(ℕk - 1)
⊢ Π(i∈ks + {k - 1}).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))
= Π(i∈ks + {k - 1}).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))
∈ PowerSeries(r)
2
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)
16. ks : bag(ℕk - 1)
17. upto(k - 1) = ks ∈ bag(ℕk - 1)
⊢ (Π(i∈ks).((((k - 1 - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))(y:=(atom(x)+atom(y)))*((atom(x)+atom(y)))^(d k))
= Π(i∈ks + {k - 1}).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1))
∈ PowerSeries(r)
Latex:
Latex:
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)))\^{}(d k))
= \mPi{}(i\mmember{}upto(k - 1) + \{k - 1\}).((((k - i) \mcdot{}r 1)*atom(x)+atom(y)))\^{}(d (i + 1))
By
Latex:
TACTIC:((GenConcl \mkleeneopen{}upto(k - 1) = ks\mkleeneclose{}\mcdot{} THENA Auto)
THEN RWO "fps-compose-fps-product" 0\mcdot{}
THEN Try (Complete (Auto')))
Home
Index