---

Step * 2 1 of Lemma fps-deriv-commutes

.....subterm..... T:t
2:n
1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. f : PowerSeries(X;r)
5. g : PowerSeries(X;r)
6. x : X
7. y : X
8. b : bag(X)
⊢ x.y.b = y.x.b ∈ bag(X)
BY
{ ((Subst' x.y.b ~ {x} + {y} + b 0 THENA Auto) THEN (Subst' y.x.b ~ {y} + {x} + b 0 THENA Auto)) }

1
1. X : Type
2. eq : EqDecider(X)
3. r : CRng
4. f : PowerSeries(X;r)
5. g : PowerSeries(X;r)
6. x : X
7. y : X
8. b : bag(X)
⊢ ({x} + {y} + b) = ({y} + {x} + b) ∈ bag(X)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  Type
2.  eq  :  EqDecider(X)
3.  r  :  CRng
4.  f  :  PowerSeries(X;r)
5.  g  :  PowerSeries(X;r)
6.  x  :  X
7.  y  :  X
8.  b  :  bag(X)
\mvdash{}  x.y.b  =  y.x.b


By

---

Latex:
((Subst'  x.y.b  \msim{}  \{x\}  +  \{y\}  +  b  0  THENA  Auto)  THEN  (Subst'  y.x.b  \msim{}  \{y\}  +  \{x\}  +  b  0  THENA  Auto))

---

Home Index