---

Step * of Lemma fps-div-coeff_wf

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:|r|]. ∀[b:bag(X)].  (fps-div-coeff(eq;r;f;g;x;b) ∈ |r|) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN Assert ⌜∀n:ℕ. ∀b:bag(X).  ((#(b) ≤ n) ⇒ (fps-div-coeff(eq;r;f;g;x;b) ∈ |r|))⌝⋅
   THEN Try ((InstHyp [⌜#(b)⌝;⌜b⌝] (-1)⋅ THEN Auto))
   THEN CompleteInductionOnNat
   THEN Auto
   THEN RecUnfold `fps-div-coeff` 0
   THEN RepeatFor 3 ((MemCD THEN Try (Complete (Auto))))
   THEN GenConclAtAddrType ⌜bag({p:bag(X) × bag(X)| #(snd(p)) < #(b1)} )⌝ [2;3]⋅
   THEN Try (Complete (((Assert Assoc(|r|;+r) BY
                               RepeatFor 2 ((DVar `r' THEN Auto)))
                        THEN Auto
                        THEN InstHyp [⌜n - 1⌝;⌜snd(p)⌝] (-9)⋅
                        THEN Auto')))) }

1
.....wf..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. x : |r|
8. b : bag(X)
9. n : ℕ
10. ∀n:ℕn. ∀b:bag(X).  ((#(b) ≤ n) ⇒ (fps-div-coeff(eq;r;f;g;x;b) ∈ |r|))
11. b1 : bag(X)
12. #(b1) ≤ n
⊢ [p∈bag-partitions(eq;b1)|¬bbag-null(fst(p))] ∈ bag({p:bag(X) × bag(X)| #(snd(p)) < #(b1)} )

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(X;r)].  \mforall{}[x:|r|].  \mforall{}[b:bag(X)].
        (fps-div-coeff(eq;r;f;g;x;b)  \mmember{}  |r|) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}b:bag(X).    ((\#(b)  \mleq{}  n)  {}\mRightarrow{}  (fps-div-coeff(eq;r;f;g;x;b)  \mmember{}  |r|))\mkleeneclose{}\mcdot{}
  THEN  Try  ((InstHyp  [\mkleeneopen{}\#(b)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))
  THEN  CompleteInductionOnNat
  THEN  Auto
  THEN  RecUnfold  `fps-div-coeff`  0
  THEN  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  GenConclAtAddrType  \mkleeneopen{}bag(\{p:bag(X)  \mtimes{}  bag(X)|  \#(snd(p))  <  \#(b1)\}  )\mkleeneclose{}  [2;3]\mcdot{}
  THEN  Try  (Complete  (((Assert  Assoc(|r|;+r)  BY
                                                          RepeatFor  2  ((DVar  `r'  THEN  Auto)))
                                            THEN  Auto
                                            THEN  InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}snd(p)\mkleeneclose{}]  (-9)\mcdot{}
                                            THEN  Auto'))))

---

Home Index