---

Step * 1 of Lemma int_enumerability_nat


1. T : Type@i'
2. f:  T. Surj(;T;f)@i
 g:  T. Surj(;T;g)
BY
{ (D (-1) THEN InstConcl [z.if z <z 0 then f (((-2) * z) - 1) else f (2 * z) fi ] THEN MaAuto) }

1
1. T : Type@i'
2. f :   T@i
3. Surj(;T;f)@i
 Surj(;T;z.if z <z 0 then f (((-2) * z) - 1) else f (2 * z) fi )



1.  T  :  Type@i'
2.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  Surj(\mBbbN{};T;f)@i
\mvdash{}  \mexists{}g:\mBbbZ{}  {}\mrightarrow{}  T.  Surj(\mBbbZ{};T;g)


By

(D  (-1)  THEN  InstConcl  [\mkleeneopen{}\mlambda{}z.if  z  <z  0  then  f  (((-2)  *  z)  -  1)  else  f  (2  *  z)  fi  \mkleeneclose{}]\mcdot{}  THEN  MaAuto)



Home Index