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

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

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


Latex:


Latex:
.....upcase..... 
1.  a  :  Atom1
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