---

Step * 1 2 1 of Lemma gen_log_aux_wf


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))
⊢ gen_log_aux(x * p;c + i;x;i;n + 1;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} 
BY
{ (InstHyp [⌜d - 1⌝;⌜x * p⌝;⌜c + i⌝;⌜x⌝;⌜i⌝;⌜n + 1⌝;⌜M⌝] 2⋅ THENA Auto) }

1
.....antecedent..... 
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))
⊢ M ≤ ((d - 1) + ((c + i) * x * p))

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))
11. gen_log_aux(x * p;c + i;x;i;n + 1;M) ∈ {k:{n + 1...}| 
                                            M ≤ (((c + i) + ((k - n + 1) * i)) * (x * p) * x^(k - n + 1))} 
⊢ gen_log_aux(x * p;c + i;x;i;n + 1;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} 

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  \mforall{}d:\mBbbN{}d
          \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))\}  ))
3.  p  :  \mBbbN{}\msupplus{}
4.  c  :  \mBbbN{}\msupplus{}
5.  x  :  \{2...\}
6.  i  :  \mBbbN{}
7.  n  :  \mBbbN{}
8.  M  :  \mBbbZ{}
9.  \mneg{}(M  \mleq{}  (c  *  p))
10.  M  \mleq{}  (d  +  (c  *  p))
\mvdash{}  gen\_log\_aux(x  *  p;c  +  i;x;i;n  +  1;M)  \mmember{}  \{k:\{n...\}|  M  \mleq{}  ((c  +  ((k  -  n)  *  i))  *  p  *  x\^{}(k  -  n))\} 


By

---

Latex:
(InstHyp  [\mkleeneopen{}d  -  1\mkleeneclose{};\mkleeneopen{}x  *  p\mkleeneclose{};\mkleeneopen{}c  +  i\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]  2\mcdot{}  THENA  Auto)

---

Home Index