---

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


1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. (λb.(+r (-r case bag-diff(AtomDeq;b;{x}) of inl(d) => f d | inr(z) => 0) 
        (+r (-r case bag-diff(AtomDeq;b;{y}) of inl(d) => f d | inr(z) => 0) (f b))))
= (λb.(+r (-r if bag-deq-member(AtomDeq;y;b) then 0 if bag-deq-member(AtomDeq;x;b) then 0 else f b fi ) 
       ...))
∈ (bag(Atom) ⟶ |r|)
7. b : bag(Atom)
⊢ (f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|
BY
{ (((ApFunToHypEquands `Z' ⌜Z (({x} + {y}) + b)⌝ ⌜|r|⌝ (-2)⋅ THEN Auto) THEN Reduce(-1) THEN Thin (-3))
   THEN Subst' bag-deq-member(AtomDeq;y;({x} + {y}) + b) ~ tt -1
   THEN Try (Complete ((RepUR ``bag-deq-member bag-append deq-member single-bag eqof atom-deq`` 0
                        THEN AutoBoolCase ⌜x =a y⌝⋅
                        THEN AutoBoolCase ⌜y =a y⌝⋅)))
   THEN Reduce (-1)
   THEN Subst' bag-deq-member(AtomDeq;x;({x} + {y}) + b) ~ tt -1
   THEN Try (Complete ((RepUR ``bag-deq-member bag-append deq-member single-bag eqof atom-deq`` 0
                        THEN AutoBoolCase ⌜x =a x⌝⋅
                        )))
   THEN Reduce (-1)) }

1
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|

---

Latex:

---

Latex:

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


By

---

Latex:
(((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  ((\{x\}  +  \{y\})  +  b)\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto)
    THEN  Reduce(-1)
    THEN  Thin  (-3))
  THEN  Subst'  bag-deq-member(AtomDeq;y;(\{x\}  +  \{y\})  +  b)  \msim{}  tt  -1
  THEN  Try  (Complete  ((RepUR  ``bag-deq-member  bag-append  deq-member  single-bag  eqof  atom-deq``  0
                                            THEN  AutoBoolCase  \mkleeneopen{}x  =a  y\mkleeneclose{}\mcdot{}
                                            THEN  AutoBoolCase  \mkleeneopen{}y  =a  y\mkleeneclose{}\mcdot{})))
  THEN  Reduce  (-1)
  THEN  Subst'  bag-deq-member(AtomDeq;x;(\{x\}  +  \{y\})  +  b)  \msim{}  tt  -1
  THEN  Try  (Complete  ((RepUR  ``bag-deq-member  bag-append  deq-member  single-bag  eqof  atom-deq``  0
                                            THEN  AutoBoolCase  \mkleeneopen{}x  =a  x\mkleeneclose{}\mcdot{}
                                            )))
  THEN  Reduce  (-1))

---

Home Index