---

Step * 2 of Lemma nat-to-incomparable-property


1. n : ℕ
2. m : ℕ
3. ¬(n = m ∈ ℤ)
4. ∃l:Atom List. (0 < ||l|| ∧ ((nat-to-str(n) @ [/]) = (nat-to-str(m) @ l) ∈ (Atom List)) ∧ l ≤ [/])
⊢ False
BY
{ (D 3 THEN ExRepD THEN Subst' l ~ [/] -2) }

1
.....equality..... 
1. n : ℕ
2. m : ℕ
3. l : Atom List
4. 0 < ||l||
5. (nat-to-str(n) @ [/]) = (nat-to-str(m) @ l) ∈ (Atom List)
6. l ≤ [/]
⊢ l ~ [/]

2
1. n : ℕ
2. m : ℕ
3. l : Atom List
4. 0 < ||l||
5. (nat-to-str(n) @ [/]) = (nat-to-str(m) @ [/]) ∈ (Atom List)
6. l ≤ [/]
⊢ n = m ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  \mneg{}(n  =  m)
4.  \mexists{}l:Atom  List.  (0  <  ||l||  \mwedge{}  ((nat-to-str(n)  @  [/])  =  (nat-to-str(m)  @  l))  \mwedge{}  l  \mleq{}  [/])
\mvdash{}  False


By

---

Latex:
(D  3  THEN  ExRepD  THEN  Subst'  l  \msim{}  [/]  -2)

---

Home Index