---

Step * 1 1 1 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|)
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. a1 : bag(Atom)
13. x1 = ({x} + a1) ∈ bag(Atom)
14. as : bag(Atom)
15. x2 = ({y} + as) ∈ bag(Atom)
16. ({y} + {x} + a1) = ({x} + {y} + as) ∈ bag(Atom)
⊢ as = a1 ∈ bag(Atom)
BY
{ ((RWO "bag-append-assoc<" (-1) THEN Auto) THEN Subst ⌜({y} + {x}) = ({x} + {y}) ∈ bag(Atom)⌝ (-1)⋅ 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. a1 : bag(Atom)
13. x1 = ({x} + a1) ∈ bag(Atom)
14. as : bag(Atom)
15. x2 = ({y} + as) ∈ bag(Atom)
16. (({x} + {y}) + a1) = (({x} + {y}) + as) ∈ bag(Atom)
⊢ as = a1 ∈ bag(Atom)

---

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.  x1  :  bag(Atom)
9.  x2  :  bag(Atom)
10.  b  =  (\{x\}  +  x2)
11.  b  =  (\{y\}  +  x1)
12.  a1  :  bag(Atom)
13.  x1  =  (\{x\}  +  a1)
14.  as  :  bag(Atom)
15.  x2  =  (\{y\}  +  as)
16.  (\{y\}  +  \{x\}  +  a1)  =  (\{x\}  +  \{y\}  +  as)
\mvdash{}  as  =  a1


By

---

Latex:
((RWO  "bag-append-assoc<"  (-1)  THEN  Auto)  THEN  Subst  \mkleeneopen{}(\{y\}  +  \{x\})  =  (\{x\}  +  \{y\})\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index