---

Step * 1 2 1 1 2 of Lemma fps-compose-mul


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. g : PowerSeries(X;r)
7. f : PowerSeries(X;r)
8. h : PowerSeries(X;r)
9. ∀L:bag(X) List+. (||L|| ≥ 1 )
10. Assoc(|r|;+r)
11. IsMonoid(|r|;+r;0)
12. Comm(|r|;+r)
13. Comm(|r|;*)
14. Assoc(|r|;*)
15. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
16. b : bag(X)
⊢ ∀x@0:{L:bag(X) List+| ¬x ↓∈ hd(L)}  × {L:bag(X) List+| ¬x ↓∈ hd(L)} 
    (x@0
    = let L,b1,b2 = <[hd(fst(x@0)) + hd(snd(x@0)) / (tl(fst(x@0)) @ tl(snd(x@0)))]
                    , hd(fst(x@0)) + bag-rep(||tl(fst(x@0))||;x)
                    , hd(snd(x@0)) + bag-rep(||tl(snd(x@0))||;x)> in 
      <[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>
    ∈ ({L:bag(X) List+| ¬x ↓∈ hd(L)}  × {L:bag(X) List+| ¬x ↓∈ hd(L)} ))
BY
{ TACTIC:(Auto THEN D (-1) THEN (RenameVar `L1' (-2)⋅ THEN D -2) THEN RenameVar `L2' (-1)⋅ THEN D -1 THEN Reduce 0) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. g : PowerSeries(X;r)
7. f : PowerSeries(X;r)
8. h : PowerSeries(X;r)
9. ∀L:bag(X) List+. (||L|| ≥ 1 )
10. Assoc(|r|;+r)
11. IsMonoid(|r|;+r;0)
12. Comm(|r|;+r)
13. Comm(|r|;*)
14. Assoc(|r|;*)
15. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
16. b : bag(X)
17. L1 : bag(X) List+
18. ¬x ↓∈ hd(L1)
19. L2 : bag(X) List+
20. ¬x ↓∈ hd(L2)
⊢ <L1, L2>
= <[(hd(L1) + bag-rep(||tl(L1)||;x)|¬x) / firstn(#((hd(L1) + bag-rep(||tl(L1)||;x)|x));tl(L1) @ tl(L2))]
  , [(hd(L2) + bag-rep(||tl(L2)||;x)|¬x) / nth_tl(#((hd(L1) + bag-rep(||tl(L1)||;x)|x));tl(L1) @ tl(L2))]
  >
∈ ({L:bag(X) List+| ¬x ↓∈ hd(L)}  × {L:bag(X) List+| ¬x ↓∈ hd(L)} )

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  x  :  X
6.  g  :  PowerSeries(X;r)
7.  f  :  PowerSeries(X;r)
8.  h  :  PowerSeries(X;r)
9.  \mforall{}L:bag(X)  List\msupplus{}.  (||L||  \mgeq{}  1  )
10.  Assoc(|r|;+r)
11.  IsMonoid(|r|;+r;0)
12.  Comm(|r|;+r)
13.  Comm(|r|;*)
14.  Assoc(|r|;*)
15.  \mforall{}L:bag(X)  List\msupplus{}.  (\mPi{}a  \mmember{}  tl(L).  f  a  \mmember{}  |r|)
16.  b  :  bag(X)
\mvdash{}  \mforall{}x@0:\{L:bag(X)  List\msupplus{}|  \mneg{}x  \mdownarrow{}\mmember{}  hd(L)\}    \mtimes{}  \{L:bag(X)  List\msupplus{}|  \mneg{}x  \mdownarrow{}\mmember{}  hd(L)\} 
        (x@0
        =  let  L,b1,b2  =  <[hd(fst(x@0))  +  hd(snd(x@0))  /  (tl(fst(x@0))  @  tl(snd(x@0)))]
                                        ,  hd(fst(x@0))  +  bag-rep(||tl(fst(x@0))||;x)
                                        ,  hd(snd(x@0))  +  bag-rep(||tl(snd(x@0))||;x)>  in 
            <[(b1|\mneg{}x)  /  firstn(\#((b1|x));tl(L))],  [(b2|\mneg{}x)  /  nth\_tl(\#((b1|x));tl(L))]>)


By

---

Latex:
TACTIC:(Auto
                THEN  D  (-1)
                THEN  (RenameVar  `L1'  (-2)\mcdot{}  THEN  D  -2)
                THEN  RenameVar  `L2'  (-1)\mcdot{}
                THEN  D  -1
                THEN  Reduce  0)

---

Home Index