---

Step * 1 1 2 1 of Lemma fps-Pascal-iff


1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. b : bag(Atom)
7. (+r (-r case bag-diff(AtomDeq;({x} + {y}) + b;{x}) of inl(d) => f d | inr(z) => 0) 
    (+r (-r case bag-diff(AtomDeq;({x} + {y}) + b;{y}) of inl(d) => f d | inr(z) => 0) (f (({x} + {y}) + b))))
= (+r (-r 0) 
   (+r 0 
    (+r 0 
     (+r 
      (-r 
       case bag-diff(AtomDeq;({x} + {y}) + b;{y})
        of inl(d) =>
        if bag-deq-member(AtomDeq;x;d) then 0 else f d fi 
        | inr(z) =>
        0) 
      (-r 
       case bag-diff(AtomDeq;({x} + {y}) + b;{x})
        of inl(d) =>
        if bag-deq-member(AtomDeq;y;d) then 0 else f d fi 
        | inr(z) =>
        0)))))
∈ |r|
⊢ (f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|
BY
{ (Subst' bag-diff(AtomDeq;({x} + {y}) + b;{x}) = (inl ({y} + b)) ∈ (bag(Atom)?) -1 THEN Reduce (-1) THEN Auto) }

1
.....equality..... 
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. b : bag(Atom)
7. (+r (-r case bag-diff(AtomDeq;({x} + {y}) + b;{x}) of inl(d) => f d | inr(z) => 0) 
    (+r (-r case bag-diff(AtomDeq;({x} + {y}) + b;{y}) of inl(d) => f d | inr(z) => 0) (f (({x} + {y}) + b))))
= (+r (-r 0) 
   (+r 0 
    (+r 0 
     (+r 
      (-r 
       case bag-diff(AtomDeq;({x} + {y}) + b;{y})
        of inl(d) =>
        if bag-deq-member(AtomDeq;x;d) then 0 else f d fi 
        | inr(z) =>
        0) 
      (-r 
       case bag-diff(AtomDeq;({x} + {y}) + b;{x})
        of inl(d) =>
        if bag-deq-member(AtomDeq;y;d) then 0 else f d fi 
        | inr(z) =>
        0)))))
∈ |r|
⊢ bag-diff(AtomDeq;({x} + {y}) + b;{x}) = (inl ({y} + b)) ∈ (bag(Atom)?)

2
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. b : bag(Atom)
7. (+r (-r (f ({y} + b))) 
    (+r (-r case bag-diff(AtomDeq;({x} + {y}) + b;{y}) of inl(d) => f d | inr(z) => 0) (f (({x} + {y}) + b))))
= (+r (-r 0) 
   (+r 0 
    (+r 0 
     (+r 
      (-r 
       case bag-diff(AtomDeq;({x} + {y}) + b;{y})
        of inl(d) =>
        if bag-deq-member(AtomDeq;x;d) then 0 else f d fi 
        | inr(z) =>
        0) 
      (-r if bag-deq-member(AtomDeq;y;{y} + b) then 0 else f ({y} + b) fi )))))
∈ |r|
⊢ (f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  f  :  PowerSeries(r)
5.  \mneg{}(x  =  y)
6.  b  :  bag(Atom)
7.  (+r  (-r  case  bag-diff(AtomDeq;(\{x\}  +  \{y\})  +  b;\{x\})  of  inl(d)  =>  f  d  |  inr(z)  =>  0) 
        (+r  (-r  case  bag-diff(AtomDeq;(\{x\}  +  \{y\})  +  b;\{y\})  of  inl(d)  =>  f  d  |  inr(z)  =>  0) 
          (f  ((\{x\}  +  \{y\})  +  b))))
=  (+r  (-r  0) 
      (+r  0 
        (+r  0 
          (+r 
            (-r 
              case  bag-diff(AtomDeq;(\{x\}  +  \{y\})  +  b;\{y\})
                of  inl(d)  =>
                if  bag-deq-member(AtomDeq;x;d)  then  0  else  f  d  fi 
                |  inr(z)  =>
                0) 
            (-r 
              case  bag-diff(AtomDeq;(\{x\}  +  \{y\})  +  b;\{x\})
                of  inl(d)  =>
                if  bag-deq-member(AtomDeq;y;d)  then  0  else  f  d  fi 
                |  inr(z)  =>
                0)))))
\mvdash{}  (f  ((\{x\}  +  \{y\})  +  b))  =  ((f  (\{x\}  +  b))  +r  (f  (\{y\}  +  b)))


By

---

Latex:
(Subst'  bag-diff(AtomDeq;(\{x\}  +  \{y\})  +  b;\{x\})  =  (inl  (\{y\}  +  b))  -1  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index