---

Step * of Lemma pigeon-hole-implies-ext

∀n:ℕ. ∀[m:ℕ]. ∀f:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕi [((f i) = (f j) ∈ ℤ)]) supposing m < n
BY
{ Extract of Obid: pigeon-hole-implies
  normalizes to:
  
  λn,f. eval j' = n in
        case letrec G(x)=if (x) < (j')
                            then eval x1 = x in
                                 case letrec G(x@0)=if (x@0) < (x1)
                                                       then if f x=f x@0 then inl <x@0, Ax> else (G (x@0 + 1))
                                                       else (inr (λx.Ax) ) in
                                       G(0)
                                  of inl(z) =>
                                  inl <x, z>
                                  | inr(z) =>
                                  G (x + 1)
                            else (inr (λx.Ax) ) in
              G(0)
         of inl(%2) =>
         let i,%2 = %2 
         in <i, fst(%2)>
         | inr(%2) =>
         let i,%2 = Ax 
         in <i, fst(%2)>
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}[m:\mBbbN{}].  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m.  \mexists{}i:\mBbbN{}n.  (\mexists{}j:\mBbbN{}i  [((f  i)  =  (f  j))])  supposing  m  <  n


By

---

Latex:
Extract  of  Obid:  pigeon-hole-implies
normalizes  to:

\mlambda{}n,f.  eval  j'  =  n  in
            case  letrec  G(x)=if  (x)  <  (j')
                                                    then  eval  x1  =  x  in
                                                              case  letrec  G(x@0)=if  (x@0)  <  (x1)
                                                                                                          then  if  f  x=f  x@0
                                                                                                                    then  inl  <x@0,  Ax>
                                                                                                                    else  (G  (x@0  +  1))
                                                                                                          else  (inr  (\mlambda{}x.Ax)  )  in
                                                                          G(0)
                                                                of  inl(z)  =>
                                                                inl  <x,  z>
                                                                |  inr(z)  =>
                                                                G  (x  +  1)
                                                    else  (inr  (\mlambda{}x.Ax)  )  in
                        G(0)
              of  inl(\%2)  =>
              let  i,\%2  =  \%2 
              in  <i,  fst(\%2)>
              |  inr(\%2)  =>
              let  i,\%2  =  Ax 
              in  <i,  fst(\%2)>
finishing  with  Auto

---

Home Index