---

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


1. n : ℕ
2. m : ℕ
3. l : Atom List
4. 0 < ||l||
5. (nat-to-str(n) @ [/]) = (nat-to-str(m) @ [/]) ∈ (Atom List)
6. l ≤ [/]
7. nat-to-str(n) = nat-to-str(m) ∈ (Atom List)
⊢ n = m ∈ ℤ
BY
{ (((InstLemma `str-to-nat-to-str` [⌜n⌝]⋅ THENM RevHypSubst' (-1) 0) THENA Auto)
   THEN ((InstLemma `str-to-nat-to-str` [⌜m⌝]⋅ THENM RevHypSubst' (-1) 0) THENA Auto)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(((InstLemma  `str-to-nat-to-str`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENM  RevHypSubst'  (-1)  0)  THENA  Auto)
  THEN  ((InstLemma  `str-to-nat-to-str`  [\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENM  RevHypSubst'  (-1)  0)  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index