---

Step * of Lemma equipollent-nat-subset-ext

∀[T:Type]. ∀P:T ⟶ ℙ. ((∀x:T. Dec(P[x])) ⇒ (∀L:T List. ∃x:T. (P[x] ∧ (¬(x ∈ L)))) ⇒ ℕ ~ T ⇒ ℕ ~ {x:T| P[x]} )
BY
{ Extract of Obid: equipollent-nat-subset
  not unfolding  mu primrec
  finishing with Auto
  normalizes to:
  
  λP,d,_,e. let f,bij = e 
            in <λx.(f 
                    primrec(x;mu(λn.if d (f n) then inl Ax else inr Ax  fi );λi,r. eval r' = r + 1 in
                                                                                   r'
                                                                                   + mu(λk.if d (f (r' + k))
                                                                                           then inl Ax
                                                                                           else inr Ax 
                                                                                           fi )))
               , λa1,a2,_. Ax
               , λb.let inj,sur = bij 
                    in let a,_ = sur b 
                       in if d (f a) then <primrec(a;0;λn,m. if d (f n) then 1 + m else 0 + m fi ), Ax> else ⊥ fi > }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}
        ((\mforall{}x:T.  Dec(P[x]))  {}\mRightarrow{}  (\mforall{}L:T  List.  \mexists{}x:T.  (P[x]  \mwedge{}  (\mneg{}(x  \mmember{}  L))))  {}\mRightarrow{}  \mBbbN{}  \msim{}  T  {}\mRightarrow{}  \mBbbN{}  \msim{}  \{x:T|  P[x]\}  )


By

---

Latex:
Extract  of  Obid:  equipollent-nat-subset
not  unfolding    mu  primrec
finishing  with  Auto
normalizes  to:

\mlambda{}P,d,$_{}$,e.  let  f,bij  =  e 
                  in  <\mlambda{}x.(f 
                                  primrec(x;mu(\mlambda{}n.if  d  (f  n)  then  inl  Ax  else  inr  Ax    fi  );\mlambda{}i,r.  eval  r'  =  r  +  1  in
                                                                                                                                                                r'
                                                                                                                                                                +  mu(\mlambda{}k.if  d 
                                                                                                                                                                                      (f 
                                                                                                                                                                                        (r'
                                                                                                                                                                                        +  k))
                                                                                                                                                                                then  inl  Ax
                                                                                                                                                                                else  inr  Ax 
                                                                                                                                                                                fi  )))
                        ,  \mlambda{}a1,a2,$_{}$.  Ax
                        ,  \mlambda{}b.let  inj,sur  =  bij 
                                  in  let  a,$_{}$  =  sur  b 
                                        in  if  d  (f  a)
                                              then  <primrec(a;0;\mlambda{}n,m.  if  d  (f  n)  then  1  +  m  else  0  +  m  fi  ),  Ax>
                                              else  \mbot{}
                                              fi  >

---

Home Index