---

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

.....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 ~ [/]
BY
{ (DVar `l' THEN All Reduce THEN Try (Complete (Auto'))) }

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

---

Latex:

---

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


By

---

Latex:
(DVar  `l'  THEN  All  Reduce  THEN  Try  (Complete  (Auto')))

---

Home Index