---

Step * 1 1 1 6 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|)
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|
BY
{ TACTIC:((Assert y ↓∈ b BY
                 ((SubstFor ⌜b⌝ 0⋅ THEN Auto) THEN BagMemberD 0 THEN Auto))
          THEN (RWO "bag-member-iff" (-1) THEN Auto)
          THEN SquashExRepD
          THEN OnMaybeHyp 10 (\h. (InstHyp [⌜as⌝] h⋅ THEN Complete (Auto)))) }

---

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))))
7.  b  :  bag(Atom)
8.  y1  :  Unit
9.  x1  :  bag(Atom)
10.  b  =  (\{x\}  +  x1)
11.  \mforall{}cs:bag(Atom).  (\mneg{}(b  =  (\{y\}  +  cs)))
12.  y  \mdownarrow{}\mmember{}  x1
\mvdash{}  ((f  b)  +r  (-r  (f  x1)))  =  (f  b)


By

---

Latex:
TACTIC:((Assert  y  \mdownarrow{}\mmember{}  b  BY
                              ((SubstFor  \mkleeneopen{}b\mkleeneclose{}  0\mcdot{}  THEN  Auto)  THEN  BagMemberD  0  THEN  Auto))
                THEN  (RWO  "bag-member-iff"  (-1)  THEN  Auto)
                THEN  SquashExRepD
                THEN  OnMaybeHyp  10  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}as\mkleeneclose{}]  h\mcdot{}  THEN  Complete  (Auto))))

---

Home Index