---

Step * 1 2 5 1 1 1 1 1 of Lemma fps-rng_wf


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
9. Comm(|r|;+r)
10. x : PowerSeries(X;r)
11. x1 : bag(X)
⊢ (Σ(p∈[x∈bag-partitions(eq;x1)|bag-null(snd(x))]). if bag-null(snd(p)) then x (fst(p)) else 0 fi  
   +r 
   Σ(p∈[x∈bag-partitions(eq;x1)|¬bbag-null(snd(x))]). if bag-null(snd(p)) then x (fst(p)) else 0 fi )
= (x x1)
∈ |r|
BY
{ TACTIC:(Subst ⌜[x∈bag-partitions(eq;x1)|bag-null(snd(x))] = {<x1, {}>} ∈ bag(bag(X) × bag(X))⌝ 0⋅ THEN Auto) }

1
.....equality..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
9. Comm(|r|;+r)
10. x : PowerSeries(X;r)
11. x1 : bag(X)
⊢ [x∈bag-partitions(eq;x1)|bag-null(snd(x))] = {<x1, {}>} ∈ bag(bag(X) × bag(X))

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. IsMonoid(|r|;+r;0)
6. Inverse(|r|;+r;0;-r)
7. IsMonoid(|r|;*;1)
8. BiLinear(|r|;+r;*)
9. Comm(|r|;+r)
10. x : PowerSeries(X;r)
11. x1 : bag(X)
⊢ (Σ(p∈{<x1, {}>}). if bag-null(snd(p)) then x (fst(p)) else 0 fi  
   +r 
   Σ(p∈[x∈bag-partitions(eq;x1)|¬bbag-null(snd(x))]). if bag-null(snd(p)) then x (fst(p)) else 0 fi )
= (x x1)
∈ |r|

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  IsMonoid(|r|;+r;0)
6.  Inverse(|r|;+r;0;-r)
7.  IsMonoid(|r|;*;1)
8.  BiLinear(|r|;+r;*)
9.  Comm(|r|;+r)
10.  x  :  PowerSeries(X;r)
11.  x1  :  bag(X)
\mvdash{}  (\mSigma{}(p\mmember{}[x\mmember{}bag-partitions(eq;x1)|bag-null(snd(x))]).  if  bag-null(snd(p))  then  x  (fst(p))  else  0  fi   
      +r 
      \mSigma{}(p\mmember{}[x\mmember{}bag-partitions(eq;x1)|\mneg{}\msubb{}bag-null(snd(x))]).  if  bag-null(snd(p))
        then  x  (fst(p))
        else  0
        fi  )
=  (x  x1)


By

---

Latex:
TACTIC:(Subst  \mkleeneopen{}[x\mmember{}bag-partitions(eq;x1)|bag-null(snd(x))]  =  \{<x1,  \{\}>\}\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index