Step
*
2
3
2
1
of Lemma
next_wf_bound
.....subterm..... T:t
1:n
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 : {i:ℤ| (k + 1 < i ∧ (i ≤ ((k + 1) + (b - 1)))) ∧ (↑p[i]) ∧ (∀j:{(k + 1) + 1..i-}. (¬↑p[j]))}
⊢ x ∈ {i:ℤ| (k < i ∧ (i ≤ (k + b))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}
BY
{ xxx(D -1 THEN MemTypeCD)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))} . (↑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]))
⊢ x ∈ ℤ
2
.....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]))
3
.....wf.....
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]))
12. i : ℤ
⊢ (k < i ∧ (i ≤ (k + b))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j])) ∈ Type
Latex:
Latex:
.....subterm..... T:t
1:n
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 : \{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]))\}
\mvdash{} x \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]))\}
By
Latex:
xxx(D -1 THEN MemTypeCD)xxx
Home
Index