---

Step * 1 of Lemma fps-mul-ucont


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. g : PowerSeries(X;r)
6. b : bag(X)
7. f : PowerSeries(X;r)
8. p : bag(X) × bag(X)
9. p ↓∈ bag-partitions(eq;b)
⊢ (* (f (fst(p))) (g (snd(p)))) = (* if deq-sub-bag(eq;fst(p);b) then f (fst(p)) else 0 fi  (g (snd(p)))) ∈ |r|
BY
{ xxx(AutoSplit THEN D (-2) THEN DVar `p' THEN Reduce 0 THEN BagMemberD (-1) THEN With ⌜p2⌝ (D 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  g  :  PowerSeries(X;r)
6.  b  :  bag(X)
7.  f  :  PowerSeries(X;r)
8.  p  :  bag(X)  \mtimes{}  bag(X)
9.  p  \mdownarrow{}\mmember{}  bag-partitions(eq;b)
\mvdash{}  (*  (f  (fst(p)))  (g  (snd(p))))
=  (*  if  deq-sub-bag(eq;fst(p);b)  then  f  (fst(p))  else  0  fi    (g  (snd(p))))


By

---

Latex:
xxx(AutoSplit
        THEN  D  (-2)
        THEN  DVar  `p'
        THEN  Reduce  0
        THEN  BagMemberD  (-1)
        THEN  With  \mkleeneopen{}p2\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto)xxx

---

Home Index