---

Step * 1 2 2 1 1 1 of Lemma unbounded-decidable-nset-infinite

.....equality..... 
1. K : Type
2. K ⊆r ℕ
3. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
4. ∀B:ℕ. ∃k:K. B < k
5. d : ℕ ⟶ 𝔹
6. ∀l:ℕ. (l ∈ K ⇐⇒ ↑(d l))
7. λk.||filter(d;upto(k))|| ∈ K ⟶ ℕ
8. b : ℤ
9. 0 < b
10. a : K
11. ||filter(d;upto(a))|| = (b - 1) ∈ ℕ
12. k : K
13. a < k ∧ (∀j:ℕ. (a < j ⇒ (j ∈ K) ⇒ (k ≤ j)))
14. upto(k) ~ upto(a) @ [a, k)
⊢ ||filter(d;[a, k))|| ~ 1
BY
{ ((Assert ↑(d a) BY
          (RWO "6<" 0 THEN Auto))
   THEN MoveToConcl (-1)
   THEN (RWO "6" (-2) THENA Auto)
   THEN MoveToConcl (-2)
   THEN (GenConcl ⌜k = n ∈ ℕ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜a = m ∈ ℕ⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto
   THEN (InstLemma `length-one-iff` [⌜ℕ⌝;⌜filter(d;[m, n))⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN Auto) }

1
1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. m : ℕ
4. m < n
5. ∀j:ℕ. (m < j ⇒ (↑(d j)) ⇒ (n ≤ j))
6. ↑(d m)
7. (∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n)))))
   ∧ no_repeats(ℕ;filter(d;[m, n)))
   ∧ 0 < ||filter(d;[m, n))|| 
   supposing ||filter(d;[m, n))|| = 1 ∈ ℤ
8. x : ℕ
9. y : ℕ
10. (x ∈ filter(d;[m, n)))
11. (y ∈ filter(d;[m, n)))
⊢ x = y ∈ ℕ

2
1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. m : ℕ
4. m < n
5. ∀j:ℕ. (m < j ⇒ (↑(d j)) ⇒ (n ≤ j))
6. ↑(d m)
7. (∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n)))))
   ∧ no_repeats(ℕ;filter(d;[m, n)))
   ∧ 0 < ||filter(d;[m, n))|| 
   supposing ||filter(d;[m, n))|| = 1 ∈ ℤ
8. ∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n))))
⊢ no_repeats(ℕ;filter(d;[m, n)))

3
1. d : ℕ ⟶ 𝔹
2. n : ℕ
3. m : ℕ
4. m < n
5. ∀j:ℕ. (m < j ⇒ (↑(d j)) ⇒ (n ≤ j))
6. ↑(d m)
7. (∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n)))))
   ∧ no_repeats(ℕ;filter(d;[m, n)))
   ∧ 0 < ||filter(d;[m, n))|| 
   supposing ||filter(d;[m, n))|| = 1 ∈ ℤ
8. ∀[x,y:ℕ].  (x = y ∈ ℕ) supposing ((y ∈ filter(d;[m, n))) and (x ∈ filter(d;[m, n))))
9. no_repeats(ℕ;filter(d;[m, n)))
⊢ 0 < ||filter(d;[m, n))||

---

Latex:

---

Latex:
.....equality..... 
1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  \mforall{}l:\mBbbN{}.  ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K)))
4.  \mforall{}B:\mBbbN{}.  \mexists{}k:K.  B  <  k
5.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
6.  \mforall{}l:\mBbbN{}.  (l  \mmember{}  K  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(d  l))
7.  \mlambda{}k.||filter(d;upto(k))||  \mmember{}  K  {}\mrightarrow{}  \mBbbN{}
8.  b  :  \mBbbZ{}
9.  0  <  b
10.  a  :  K
11.  ||filter(d;upto(a))||  =  (b  -  1)
12.  k  :  K
13.  a  <  k  \mwedge{}  (\mforall{}j:\mBbbN{}.  (a  <  j  {}\mRightarrow{}  (j  \mmember{}  K)  {}\mRightarrow{}  (k  \mleq{}  j)))
14.  upto(k)  \msim{}  upto(a)  @  [a,  k)
\mvdash{}  ||filter(d;[a,  k))||  \msim{}  1


By

---

Latex:
((Assert  \muparrow{}(d  a)  BY
                (RWO  "6<"  0  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (RWO  "6"  (-2)  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}k  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}a  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  (InstLemma  `length-one-iff`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}filter(d;[m,  n))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  Auto)

---

Home Index