Step
*
2
1
2
1
1
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)
⊢ ([h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))(y:=(atom(x)+atom(y)))*(Π(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))))
= ([h]_d 0(y:=((k ⋅r 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅r 1)*atom(x)+atom(y)))^(d (i + 1)))
∈ PowerSeries(r)
BY
{ TACTIC:(EqCD THEN Auto) }
1
.....subterm..... T:t
3: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)
⊢ [h]_d 0(y:=(((k - 1) ⋅r 1)*atom(x)+atom(y)))(y:=(atom(x)+atom(y)))
= [h]_d 0(y:=((k ⋅r 1)*atom(x)+atom(y)))
∈ PowerSeries(r)
2
.....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)
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{} ([h]\_d 0(y:=(((k - 1) \mcdot{}r 1)*atom(x)+atom(y)))(y:=(atom(x)+atom(y)))*(\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))))
= ([h]\_d 0(y:=((k \mcdot{}r 1)*atom(x)+atom(y)))*\mPi{}(i\mmember{}upto(k)).((((k - i) \mcdot{}r 1)*atom(x)+atom(y)))\^{}(d
(i + 1)))
By
Latex:
TACTIC:(EqCD THEN Auto)
Home
Index