Step * 1 of Lemma free-from-atom-int


1. Atom1
2. : ℤ
3. n < 0
⊢ a#n:ℤ
BY
Subst' x.(-x)) (-n) }

1
.....equality..... 
1. Atom1
2. : ℤ
3. n < 0
⊢ x.(-x)) (-n)

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


Latex:


Latex:

1.  a  :  Atom1
2.  n  :  \mBbbZ{}
3.  n  <  0
\mvdash{}  a\#n:\mBbbZ{}


By


Latex:
Subst'  n  \msim{}  (\mlambda{}x.(-x))  (-n)  0




Home Index