---

Step * 2 of Lemma gen_log_aux_wf


1. ∀d:ℕ
     ∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
       ((M ≤ (d + (c * p))) ⇒ (gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} ))
⊢ ∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
    (gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} )
BY
{ (Auto THEN (D 1 With ⌜|M|⌝  THENA Auto) THEN BHyp -1 THEN Auto) }

1
1. p : ℕ+
2. c : ℕ+
3. x : {2...}
4. i : ℕ
5. n : ℕ
6. M : ℤ
7. ∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M@0:ℤ].
     ((M@0 ≤ (|M| + (c * p))) ⇒ (gen_log_aux(p;c;x;i;n;M@0) ∈ {k:{n...}| M@0 ≤ ((c + ((k - n) * i)) * p * x^(k - n))} )\000C)
⊢ M ≤ (|M| + (c * p))

---

Latex:

---

Latex:

1.  \mforall{}d:\mBbbN{}
          \mforall{}[p,c:\mBbbN{}\msupplus{}].  \mforall{}[x:\{2...\}].  \mforall{}[i,n:\mBbbN{}].  \mforall{}[M:\mBbbZ{}].
              ((M  \mleq{}  (d  +  (c  *  p)))
              {}\mRightarrow{}  (gen\_log\_aux(p;c;x;i;n;M)  \mmember{}  \{k:\{n...\}|  M  \mleq{}  ((c  +  ((k  -  n)  *  i))  *  p  *  x\^{}(k  -  n))\}  ))
\mvdash{}  \mforall{}[p,c:\mBbbN{}\msupplus{}].  \mforall{}[x:\{2...\}].  \mforall{}[i,n:\mBbbN{}].  \mforall{}[M:\mBbbZ{}].
        (gen\_log\_aux(p;c;x;i;n;M)  \mmember{}  \{k:\{n...\}|  M  \mleq{}  ((c  +  ((k  -  n)  *  i))  *  p  *  x\^{}(k  -  n))\}  )


By

---

Latex:
(Auto  THEN  (D  1  With  \mkleeneopen{}|M|\mkleeneclose{}    THENA  Auto)  THEN  BHyp  -1  THEN  Auto)

---

Home Index