---

Step * 1 of Lemma gen_log_aux_wf

.....assertion..... 
∀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))} ))
BY
{ (CompleteInductionOnNat THEN Auto THEN RecUnfold `gen_log_aux` 0 THEN (BoolCase ⌜M ≤z c * p⌝⋅ THENA Auto)) }

1
1. d : ℕ
2. ∀d:ℕ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))} ))
3. p : ℕ+
4. c : ℕ+
5. x : {2...}
6. i : ℕ
7. n : ℕ
8. M : ℤ
9. M ≤ (d + (c * p))
10. M ≤ (c * p)
⊢ n ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} 

2
1. d : ℕ
2. ∀d:ℕ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))} ))
3. p : ℕ+
4. c : ℕ+
5. x : {2...}
6. i : ℕ
7. n : ℕ
8. M : ℤ
9. ¬(M ≤ (c * p))
10. M ≤ (d + (c * p))
⊢ eval p' = x * p in
  eval c' = c + i in
  eval n' = n + 1 in
    gen_log_aux(p';c';x;i;n';M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} 

---

Latex:

---

Latex:
.....assertion..... 
\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))\}  ))


By

---

Latex:
(CompleteInductionOnNat
  THEN  Auto
  THEN  RecUnfold  `gen\_log\_aux`  0
  THEN  (BoolCase  \mkleeneopen{}M  \mleq{}z  c  *  p\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index