---

Step * 2 3 2 1 2 of Lemma next_wf_bound

.....set predicate..... 
1. b : ℤ
2. 0 < b
3. ∀[k:ℤ]. ∀[p:{i:ℤ| k < i}  ⟶ 𝔹].
     (next i > k s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}  
     supposing ∃n:{i:ℤ| k < i ∧ (i ≤ (k + (b - 1)))} . (↑p[n])
4. k : ℤ
5. p : {i:ℤ| k < i}  ⟶ 𝔹
6. ∃n:{i:ℤ| k < i ∧ (i ≤ (k + b))} . (↑p[n])
7. ¬↑p[k + 1]
8. (next i > k + 1 s.t. ↑p[i]) ∈ {i:ℤ| 
                                  (k + 1 < i ∧ (i ≤ ((k + 1) + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{(k + 1) + 1..i-}. (¬↑p[j]))} 
9. (next i > k + 1 s.t. ↑p[i])
= (next i > k + 1 s.t. ↑p[i])
∈ {i:ℤ| (k + 1 < i ∧ (i ≤ ((k + 1) + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{(k + 1) + 1..i-}. (¬↑p[j]))} 
10. x : ℤ
11. (k + 1 < x ∧ (x ≤ ((k + 1) + (b - 1)))) ∧ (↑p[x]) ∧ (∀j:{(k + 1) + 1..x-}. (¬↑p[j]))
⊢ (k < x ∧ (x ≤ (k + b))) ∧ (↑p[x]) ∧ (∀j:{k + 1..x-}. (¬↑p[j]))
BY
{ xxx(ExRepD THEN D 0)xxx }

1
1. b : ℤ
2. 0 < b
3. ∀[k:ℤ]. ∀[p:{i:ℤ| k < i}  ⟶ 𝔹].
     (next i > k s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}  
     supposing ∃n:{i:ℤ| k < i ∧ (i ≤ (k + (b - 1)))} . (↑p[n])
4. k : ℤ
5. p : {i:ℤ| k < i}  ⟶ 𝔹
6. n : {i:ℤ| k < i ∧ (i ≤ (k + b))} 
7. ↑p[n]
8. ¬↑p[k + 1]
9. (next i > k + 1 s.t. ↑p[i]) ∈ {i:ℤ| 
                                  (k + 1 < i ∧ (i ≤ ((k + 1) + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{(k + 1) + 1..i-}. (¬↑p[j]))} 
10. (next i > k + 1 s.t. ↑p[i])
= (next i > k + 1 s.t. ↑p[i])
∈ {i:ℤ| (k + 1 < i ∧ (i ≤ ((k + 1) + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{(k + 1) + 1..i-}. (¬↑p[j]))} 
11. x : ℤ
12. k + 1 < x
13. x ≤ ((k + 1) + (b - 1))
14. ↑p[x]
15. ∀j:{(k + 1) + 1..x-}. (¬↑p[j])
⊢ k < x ∧ (x ≤ (k + b))

2
1. b : ℤ
2. 0 < b
3. ∀[k:ℤ]. ∀[p:{i:ℤ| k < i}  ⟶ 𝔹].
     (next i > k s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}  
     supposing ∃n:{i:ℤ| k < i ∧ (i ≤ (k + (b - 1)))} . (↑p[n])
4. k : ℤ
5. p : {i:ℤ| k < i}  ⟶ 𝔹
6. n : {i:ℤ| k < i ∧ (i ≤ (k + b))} 
7. ↑p[n]
8. ¬↑p[k + 1]
9. (next i > k + 1 s.t. ↑p[i]) ∈ {i:ℤ| 
                                  (k + 1 < i ∧ (i ≤ ((k + 1) + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{(k + 1) + 1..i-}. (¬↑p[j]))} 
10. (next i > k + 1 s.t. ↑p[i])
= (next i > k + 1 s.t. ↑p[i])
∈ {i:ℤ| (k + 1 < i ∧ (i ≤ ((k + 1) + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{(k + 1) + 1..i-}. (¬↑p[j]))} 
11. x : ℤ
12. k + 1 < x
13. x ≤ ((k + 1) + (b - 1))
14. ↑p[x]
15. ∀j:{(k + 1) + 1..x-}. (¬↑p[j])
⊢ (↑p[x]) ∧ (∀j:{k + 1..x-}. (¬↑p[j]))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  b  :  \mBbbZ{}
2.  0  <  b
3.  \mforall{}[k:\mBbbZ{}].  \mforall{}[p:\{i:\mBbbZ{}|  k  <  i\}    {}\mrightarrow{}  \mBbbB{}].
          (next  i  >  k  s.t.  \muparrow{}p[i])  \mmember{}  \{i:\mBbbZ{}| 
                                                                (k  <  i  \mwedge{}  (i  \mleq{}  (k  +  (b  -  1))))
                                                                \mwedge{}  (\muparrow{}p[i])
                                                                \mwedge{}  (\mforall{}j:\{k  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))\}   
          supposing  \mexists{}n:\{i:\mBbbZ{}|  k  <  i  \mwedge{}  (i  \mleq{}  (k  +  (b  -  1)))\}  .  (\muparrow{}p[n])
4.  k  :  \mBbbZ{}
5.  p  :  \{i:\mBbbZ{}|  k  <  i\}    {}\mrightarrow{}  \mBbbB{}
6.  \mexists{}n:\{i:\mBbbZ{}|  k  <  i  \mwedge{}  (i  \mleq{}  (k  +  b))\}  .  (\muparrow{}p[n])
7.  \mneg{}\muparrow{}p[k  +  1]
8.  (next  i  >  k  +  1  s.t.  \muparrow{}p[i])  \mmember{}  \{i:\mBbbZ{}| 
                                                                    (k  +  1  <  i  \mwedge{}  (i  \mleq{}  ((k  +  1)  +  (b  -  1))))
                                                                    \mwedge{}  (\muparrow{}p[i])
                                                                    \mwedge{}  (\mforall{}j:\{(k  +  1)  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))\} 
9.  (next  i  >  k  +  1  s.t.  \muparrow{}p[i])  =  (next  i  >  k  +  1  s.t.  \muparrow{}p[i])
10.  x  :  \mBbbZ{}
11.  (k  +  1  <  x  \mwedge{}  (x  \mleq{}  ((k  +  1)  +  (b  -  1))))  \mwedge{}  (\muparrow{}p[x])  \mwedge{}  (\mforall{}j:\{(k  +  1)  +  1..x\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))
\mvdash{}  (k  <  x  \mwedge{}  (x  \mleq{}  (k  +  b)))  \mwedge{}  (\muparrow{}p[x])  \mwedge{}  (\mforall{}j:\{k  +  1..x\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))


By

---

Latex:
xxx(ExRepD  THEN  D  0)xxx

---

Home Index