Step
*
1
1
1
of Lemma
KozenSilva-lemma
.....antecedent.....
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : ℕ
6. m : ℕ
7. n ≤ m
8. ¬(x = y ∈ Atom)
⊢ fps-ucont(Atom;AtomDeq;r;f.([f]_n(y:=1)*Δ(x,y)))
BY
{ xxx(InstLemma `fps-ucont-composition` [⌜Atom⌝;⌜AtomDeq⌝;⌜r⌝;⌜λ2f.(f*Δ(x,y))⌝;⌜λ2f.[f]_n(y:=1)⌝]⋅
THEN Auto
THEN (Try ((BLemma `fps-mul-ucont` THEN Auto)) THEN Try ((BLemma `fps-set-to-one-ucont` THEN Auto)))
THEN RepUR ``compose so_apply so_lambda`` (-1)
THEN Auto)⋅xxx }
Latex:
Latex:
.....antecedent.....
1. r : CRng
2. x : Atom
3. y : Atom
4. h : PowerSeries(r)
5. n : \mBbbN{}
6. m : \mBbbN{}
7. n \mleq{} m
8. \mneg{}(x = y)
\mvdash{} fps-ucont(Atom;AtomDeq;r;f.([f]\_n(y:=1)*\mDelta{}(x,y)))
By
Latex:
xxx(InstLemma `fps-ucont-composition` [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.(f*\mDelta{}(x,y))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.[f]\_n(y:=1)\mkleeneclose{}]\mcdot{}
THEN Auto
THEN (Try ((BLemma `fps-mul-ucont` THEN Auto))
THEN Try ((BLemma `fps-set-to-one-ucont` THEN Auto))
)
THEN RepUR ``compose so\_apply so\_lambda`` (-1)
THEN Auto)\mcdot{}xxx
Home
Index