Step * of Lemma free-from-atom-int

[a:Atom1]. ∀[n:ℤ].  a#n:ℤ
BY
(Auto THEN (Decide n < THENA Auto)) }

1
1. Atom1
2. : ℤ
3. n < 0
⊢ a#n:ℤ

2
1. Atom1
2. : ℤ
3. ¬n < 0
⊢ a#n:ℤ


Latex:


Latex:
\mforall{}[a:Atom1].  \mforall{}[n:\mBbbZ{}].    a\#n:\mBbbZ{}


By


Latex:
(Auto  THEN  (Decide  n  <  0  THENA  Auto))




Home Index