---

Step * 1 1 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). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
⊢ (λ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|)
BY
{ TACTIC:((EqCD THEN Auto)⋅
          THEN ((RW (AddrC [3;1] (SweepUpC (LemmaC `bag-deq-member-bag-diff`))) 0 THENA Auto)
                THEN (RW (AddrC [3;2;1] (SweepUpC (LemmaC `bag-deq-member-bag-diff`))) 0 THENA Auto)
                THEN (RW (AddrC [3;2;2;1] (SweepUpC (LemmaC `bag-deq-member-bag-diff`))) 0 THENA Auto))
          THEN ((InstLemma `bag-diff-property` [⌜Atom⌝;⌜AtomDeq⌝;⌜{y}⌝;⌜b⌝]⋅ THENA Auto)
                THEN MoveToConcl (-1)
                THEN GenConclAtAddr [1;1]
                THEN Thin (-1)
                THEN D -1
                THEN Reduce 0
                THEN (InstLemma `bag-diff-property` [⌜Atom⌝;⌜AtomDeq⌝;⌜{x}⌝;⌜b⌝]⋅ THENA Auto)
                THEN MoveToConcl (-1)
                THEN GenConclAtAddr [1;1]
                THEN Thin (-1)
                THEN D -1
                THEN Reduce 0
                THEN Auto
                THEN RW RngNormC 0
                THEN Auto
                THEN Repeat (AutoSplit⋅)
                THEN RW RngNormC 0
                THEN Auto)⋅) }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. ∀b:bag(Atom). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
7. b : bag(Atom)
8. x1 : bag(Atom)
9. x2 : bag(Atom)
10. b = ({x} + x2) ∈ bag(Atom)
11. b = ({y} + x1) ∈ bag(Atom)
12. x ↓∈ x1
13. y ↓∈ x2
⊢ ((f b) +r ((-r (f x1)) +r (-r (f x2)))) = 0 ∈ |r|

2
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. ∀b:bag(Atom). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
7. b : bag(Atom)
8. x1 : bag(Atom)
9. x2 : bag(Atom)
10. ¬y ↓∈ x2
11. b = ({x} + x2) ∈ bag(Atom)
12. b = ({y} + x1) ∈ bag(Atom)
13. x ↓∈ x1
⊢ ((f b) +r ((-r (f x1)) +r (-r (f x2)))) = (-r (f x2)) ∈ |r|

3
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. ∀b:bag(Atom). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
7. b : bag(Atom)
8. x1 : bag(Atom)
9. ¬x ↓∈ x1
10. x2 : bag(Atom)
11. b = ({x} + x2) ∈ bag(Atom)
12. b = ({y} + x1) ∈ bag(Atom)
13. y ↓∈ x2
⊢ ((f b) +r ((-r (f x1)) +r (-r (f x2)))) = (-r (f x1)) ∈ |r|

4
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. ∀b:bag(Atom). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
7. b : bag(Atom)
8. x1 : bag(Atom)
9. ¬x ↓∈ x1
10. x2 : bag(Atom)
11. ¬y ↓∈ x2
12. b = ({x} + x2) ∈ bag(Atom)
13. b = ({y} + x1) ∈ bag(Atom)
⊢ ((f b) +r ((-r (f x1)) +r (-r (f x2)))) = ((-r (f x1)) +r (-r (f x2))) ∈ |r|

5
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. ∀b:bag(Atom). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
7. b : bag(Atom)
8. x1 : bag(Atom)
9. y1 : Unit
10. ∀cs:bag(Atom). (¬(b = ({x} + cs) ∈ bag(Atom)))
11. b = ({y} + x1) ∈ bag(Atom)
12. x ↓∈ x1
⊢ ((f b) +r (-r (f x1))) = (f b) ∈ |r|

6
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. ∀b:bag(Atom). ((f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|)
7. b : bag(Atom)
8. y1 : Unit
9. x1 : bag(Atom)
10. b = ({x} + x1) ∈ bag(Atom)
11. ∀cs:bag(Atom). (¬(b = ({y} + cs) ∈ bag(Atom)))
12. y ↓∈ x1
⊢ ((f b) +r (-r (f x1))) = (f b) ∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  f  :  PowerSeries(r)
5.  \mneg{}(x  =  y)
6.  \mforall{}b:bag(Atom).  ((f  ((\{x\}  +  \{y\})  +  b))  =  ((f  (\{x\}  +  b))  +r  (f  (\{y\}  +  b))))
\mvdash{}  (\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))))))


By

---

Latex:
TACTIC:((EqCD  THEN  Auto)\mcdot{}
                THEN  ((RW  (AddrC  [3;1]  (SweepUpC  (LemmaC  `bag-deq-member-bag-diff`)))  0  THENA  Auto)
                            THEN  (RW  (AddrC  [3;2;1]  (SweepUpC  (LemmaC  `bag-deq-member-bag-diff`)))  0  THENA  Auto)
                            THEN  (RW  (AddrC  [3;2;2;1]  (SweepUpC  (LemmaC  `bag-deq-member-bag-diff`)))  0
                                        THENA  Auto
                                        ))
                THEN  ((InstLemma  `bag-diff-property`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}\{y\}\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  MoveToConcl  (-1)
                            THEN  GenConclAtAddr  [1;1]
                            THEN  Thin  (-1)
                            THEN  D  -1
                            THEN  Reduce  0
                            THEN  (InstLemma  `bag-diff-property`  [\mkleeneopen{}Atom\mkleeneclose{};\mkleeneopen{}AtomDeq\mkleeneclose{};\mkleeneopen{}\{x\}\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  MoveToConcl  (-1)
                            THEN  GenConclAtAddr  [1;1]
                            THEN  Thin  (-1)
                            THEN  D  -1
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  RW  RngNormC  0
                            THEN  Auto
                            THEN  Repeat  (AutoSplit\mcdot{})
                            THEN  RW  RngNormC  0
                            THEN  Auto)\mcdot{})

---

Home Index