---

Step * 1 1 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. v : 
8. (a rem 2) = v
9. a = (((a  2) * 2) + v)
 if if (v = 0) then a  2 else (-(a  2)) - 1 fi  <z 0
then f (((-2) * if (v = 0) then a  2 else (-(a  2)) - 1 fi ) - 1)
else f (2 * if (v = 0) then a  2 else (-(a  2)) - 1 fi )
fi 
= b
BY
{ ((AutoSplit THEN AutoSplit) THEN MaAuto) }

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)
10. v = 0
11. 0  (a  2)
 (f (2 * (a  2))) = b

2
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)
10. (v = 0)
11. ((-(a  2)) - 1) < 0
 (f (((-2) * ((-(a  2)) - 1)) - 1)) = b

3
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)
10. (v = 0)
11. 0  ((-(a  2)) - 1)
 (f (2 * ((-(a  2)) - 1))) = 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.  v  :  \mBbbZ{}
8.  (a  rem  2)  =  v
9.  a  =  (((a  \mdiv{}  2)  *  2)  +  v)
\mvdash{}  if  if  (v  =\msubz{}  0)  then  a  \mdiv{}  2  else  (-(a  \mdiv{}  2))  -  1  fi    <z  0
then  f  (((-2)  *  if  (v  =\msubz{}  0)  then  a  \mdiv{}  2  else  (-(a  \mdiv{}  2))  -  1  fi  )  -  1)
else  f  (2  *  if  (v  =\msubz{}  0)  then  a  \mdiv{}  2  else  (-(a  \mdiv{}  2))  -  1  fi  )
fi 
=  b


By

((AutoSplit\mcdot{}  THEN  AutoSplit)  THEN  MaAuto)



Home Index