---

Step * 2 of Lemma next_wf_bound

.....upcase..... 
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])
⊢ ∀[k:ℤ]. ∀[p:{i:ℤ| k < i}  ⟶ 𝔹].
    (next i > k s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + b))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}  
    supposing ∃n:{i:ℤ| k < i ∧ (i ≤ (k + b))} . (↑p[n])
BY
{ ((UnivCD THENA Auto)⋅
   THEN RecUnfold `next` 0
   THEN RW (AddrC [2] CallByValueC) 0
   THEN Try ((Refine `callbyvalueInt` [] THEN Auto))
   THEN Try ((SplitOnConclITE THENA Auto⋅))) }

1
.....aux..... 
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])
⊢ (k + 1)↓

2
.....truecase..... 
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]
⊢ k + 1 ∈ {i:ℤ| (k < i ∧ (i ≤ (k + b))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))} 

3
.....falsecase..... 
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]
⊢ (next i > k + 1 s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + b))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))} 

---

Latex:

---

Latex:
.....upcase..... 
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])
\mvdash{}  \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)))  \mwedge{}  (\muparrow{}p[i])  \mwedge{}  (\mforall{}j:\{k  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))\}  \000C 
        supposing  \mexists{}n:\{i:\mBbbZ{}|  k  <  i  \mwedge{}  (i  \mleq{}  (k  +  b))\}  .  (\muparrow{}p[n])


By

---

Latex:
((UnivCD  THENA  Auto)\mcdot{}
  THEN  RecUnfold  `next`  0
  THEN  RW  (AddrC  [2]  CallByValueC)  0
  THEN  Try  ((Refine  `callbyvalueInt`  []  THEN  Auto))
  THEN  Try  ((SplitOnConclITE  THENA  Auto\mcdot{})))

---

Home Index