---

Step * 2 of Lemma free-from-atom2-nat

.....upcase..... 
1. a : Atom2
2. n : ℤ
3. 0 < n
4. a#n - 1:ℕ
⊢ a#n:ℕ
BY
{ TACTIC:(Subst' n ~ (λx.(x + 1)) (n - 1) 0 THEN Try (Complete ((Reduce 0 THEN Auto)))) }

1
1. a : Atom2
2. n : ℤ
3. 0 < n
4. a#n - 1:ℕ
⊢ a#(λx.(x + 1)) (n - 1):ℕ

---

Latex:

---

Latex:
.....upcase..... 
1.  a  :  Atom2
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  a\#n  -  1:\mBbbN{}
\mvdash{}  a\#n:\mBbbN{}


By

---

Latex:
TACTIC:(Subst'  n  \msim{}  (\mlambda{}x.(x  +  1))  (n  -  1)  0  THEN  Try  (Complete  ((Reduce  0  THEN  Auto))))

---

Home Index