---

Step * 1 1 1 1 1 of Lemma int_enumerability_nat


1. T : Type@i'
2. f :   T@i
3. b:T. a:. ((f a) = b)@i
4. b : T@i
5. a : 
6. (f a) = b
7. a = (((a  2) * 2) + (a rem 2))
 a:. (if a <z 0 then f (((-2) * a) - 1) else f (2 * a) fi  = b)
BY
{ GenHypAtAddr (-1) [3;2] }

1
1. T : Type@i'
2. f :   T@i
3. b:T. a:. ((f a) = b)@i
4. b : T@i
5. a : 
6. (f a) = b
7. v : 
8. (a rem 2) = v
9. a = (((a  2) * 2) + v)
 a:. (if a <z 0 then f (((-2) * a) - 1) else f (2 * a) fi  = b)



1.  T  :  Type@i'
2.  f  :  \mBbbN{}  {}\mrightarrow{}  T@i
3.  \mforall{}b:T.  \mexists{}a:\mBbbN{}.  ((f  a)  =  b)@i
4.  b  :  T@i
5.  a  :  \mBbbN{}
6.  (f  a)  =  b
7.  a  =  (((a  \mdiv{}  2)  *  2)  +  (a  rem  2))
\mvdash{}  \mexists{}a:\mBbbZ{}.  (if  a  <z  0  then  f  (((-2)  *  a)  -  1)  else  f  (2  *  a)  fi    =  b)


By

GenHypAtAddr  (-1)  [3;2]



Home Index