---

Step * of Lemma fps-compose-single-general

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[b:bag(X)]. ∀[f:PowerSeries(X;r)].
    (<b>(x:=f) = (<(b|¬x)>*((f-(f[{}])*1))^(#((b|x)))) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ xxx(Auto THEN (InstLemma `bag-restrict-split` [⌜X⌝;⌜eq⌝;⌜x⌝;⌜b⌝]⋅ THENA Auto))xxx }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. b : bag(X)
7. f : PowerSeries(X;r)
8. b = ((b|x) + (b|¬x)) ∈ bag(X)
⊢ <b>(x:=f) = (<(b|¬x)>*((f-(f[{}])*1))^(#((b|x)))) ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].  \mforall{}[b:bag(X)].  \mforall{}[f:PowerSeries(X;r)].
        (<b>(x:=f)  =  (<(b|\mneg{}x)>*((f-(f[\{\}])*1))\^{}(\#((b|x))))) 
    supposing  valueall-type(X)


By

---

Latex:
xxx(Auto  THEN  (InstLemma  `bag-restrict-split`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto))xxx

---

Home Index