---

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


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. m ≤ x
11. x < n
12. ↑(d x)
13. m ≤ y
14. y < n
15. ↑(d y)
⊢ x = y ∈ ℕ
BY
{ ((Decide ⌜x < y⌝⋅ THENA Auto)
   THENL [(InstHyp [⌜y⌝] 5⋅ THEN Auto); (Decide ⌜y < x⌝⋅ THEN Auto THEN InstHyp [⌜x⌝] 5⋅ THEN Auto)]
) }

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  m  <  n
5.  \mforall{}j:\mBbbN{}.  (m  <  j  {}\mRightarrow{}  (\muparrow{}(d  j))  {}\mRightarrow{}  (n  \mleq{}  j))
6.  \muparrow{}(d  m)
7.  (\mforall{}[x,y:\mBbbN{}].    (x  =  y)  supposing  ((y  \mmember{}  filter(d;[m,  n)))  and  (x  \mmember{}  filter(d;[m,  n)))))
      \mwedge{}  no\_repeats(\mBbbN{};filter(d;[m,  n)))
      \mwedge{}  0  <  ||filter(d;[m,  n))|| 
      supposing  ||filter(d;[m,  n))||  =  1
8.  x  :  \mBbbN{}
9.  y  :  \mBbbN{}
10.  m  \mleq{}  x
11.  x  <  n
12.  \muparrow{}(d  x)
13.  m  \mleq{}  y
14.  y  <  n
15.  \muparrow{}(d  y)
\mvdash{}  x  =  y


By

---

Latex:
((Decide  \mkleeneopen{}x  <  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [(InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  5\mcdot{}  THEN  Auto);  (Decide  \mkleeneopen{}y  <  x\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  5\mcdot{}  THEN  Auto)]
)

---

Home Index