---

Step * 1 of Lemma next_wf


1. k : ℤ
2. p : {i:ℤ| k < i}  ⟶ 𝔹
3. n : {i:ℤ| k < i} 
4. ↑p[n]
⊢ (next i > k s.t. ↑p[i]) ∈ {i:ℤ| k < i ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))} 
BY
{ (D -2 THEN (InstLemma `next_wf_bound` [⌜n - k⌝;⌜k⌝;⌜p⌝]⋅ THENA Auto')) }

1
1. k : ℤ
2. p : {i:ℤ| k < i}  ⟶ 𝔹
3. n : ℤ
4. k < n
5. ↑p[n]
6. (next i > k s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + (n - k)))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))} 
⊢ (next i > k s.t. ↑p[i]) ∈ {i:ℤ| k < i ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))} 

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  p  :  \{i:\mBbbZ{}|  k  <  i\}    {}\mrightarrow{}  \mBbbB{}
3.  n  :  \{i:\mBbbZ{}|  k  <  i\} 
4.  \muparrow{}p[n]
\mvdash{}  (next  i  >  k  s.t.  \muparrow{}p[i])  \mmember{}  \{i:\mBbbZ{}|  k  <  i  \mwedge{}  (\muparrow{}p[i])  \mwedge{}  (\mforall{}j:\{k  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))\} 


By

---

Latex:
(D  -2  THEN  (InstLemma  `next\_wf\_bound`  [\mkleeneopen{}n  -  k\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto'))

---

Home Index