---

Step * 1 1 1 1 of Lemma equipollent-nat-list-as-product


1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. h : ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
⊢ InvFuns(ℕ;k:ℕ × (ℕ^k);λn.if (n =z 0)
                           then <0, ⋅>
                           else let n1,n2 = coded-pair(n - 1) 
                                in <n1 + 1, f n1 n2>
                           fi ;λp.let p1,p2 = p 
                                  in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi )
BY
{ ((Assert λn.if (n =z 0) then <0, ⋅> else let n1,n2 = coded-pair(n - 1) in <n1 + 1, f n1 n2> fi  ∈ ℕ
           ⟶ (k:ℕ × (ℕ^k)) BY
          Auto)
   THEN (Assert λp.let p1,p2 = p 
                   in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi  ∈ (k:ℕ × (ℕ^k)) ⟶ ℕ BY
               Auto)
   THEN D 0
   THEN RepUR ``tidentity identity`` 0
   THEN xxx((BetterExt THEN Auto) THEN Reduce 0 THEN AutoSplit)xxx) }

1
1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. h : ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
3. λn.if (n =z 0) then <0, ⋅> else let n1,n2 = coded-pair(n - 1) in <n1 + 1, f n1 n2> fi  ∈ ℕ ⟶ (k:ℕ × (ℕ^k))
4. λp.let p1,p2 = p 
      in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi  ∈ (k:ℕ × (ℕ^k)) ⟶ ℕ
5. x : {1...}
⊢ let p1,p2 = let n1,n2 = coded-pair(x - 1) 
              in <n1 + 1, f n1 n2> 
  in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi 
= x
∈ ℕ

2
1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. h : ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
3. λn.if (n =z 0) then <0, ⋅> else let n1,n2 = coded-pair(n - 1) in <n1 + 1, f n1 n2> fi  ∈ ℕ ⟶ (k:ℕ × (ℕ^k))
4. λp.let p1,p2 = p 
      in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi  ∈ (k:ℕ × (ℕ^k)) ⟶ ℕ
5. x : k:ℕ × (ℕ^k)
6. let p1,p2 = x in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi  = 0 ∈ ℤ
⊢ <0, ⋅> = x ∈ (k:ℕ × (ℕ^k))

3
1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. h : ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
3. λn.if (n =z 0) then <0, ⋅> else let n1,n2 = coded-pair(n - 1) in <n1 + 1, f n1 n2> fi  ∈ ℕ ⟶ (k:ℕ × (ℕ^k))
4. λp.let p1,p2 = p 
      in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi  ∈ (k:ℕ × (ℕ^k)) ⟶ ℕ
5. x : k:ℕ × (ℕ^k)
6. let p1,p2 = x 
   in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi  ≠ 0
⊢ let n1,n2 = coded-pair(let p1,p2 = x 
                         in if (p1 =z 0) then 0 else code-pair(p1 - 1;(fst((h (p1 - 1)))) p2) + 1 fi  - 1) 
  in <n1 + 1, f n1 n2>
= x
∈ (k:ℕ × (ℕ^k))

---

Latex:

---

Latex:

1.  f  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1)
2.  h  :  \mforall{}n:\mBbbN{}.  \mexists{}g:(\mBbbN{}\^{}n  +  1)  {}\mrightarrow{}  \mBbbN{}.  InvFuns(\mBbbN{};(\mBbbN{}\^{}n  +  1);f  n;g)
\mvdash{}  InvFuns(\mBbbN{};k:\mBbbN{}  \mtimes{}  (\mBbbN{}\^{}k);\mlambda{}n.if  (n  =\msubz{}  0)
                                                      then  ɘ,  \mcdot{}>
                                                      else  let  n1,n2  =  coded-pair(n  -  1) 
                                                                in  <n1  +  1,  f  n1  n2>
                                                      fi  ;\mlambda{}p.let  p1,p2  =  p 
                                                                    in  if  (p1  =\msubz{}  0)
                                                                          then  0
                                                                          else  code-pair(p1  -  1;(fst((h  (p1  -  1))))  p2)  +  1
                                                                          fi  )


By

---

Latex:
((Assert  \mlambda{}n.if  (n  =\msubz{}  0)  then  ɘ,  \mcdot{}>  else  let  n1,n2  =  coded-pair(n  -  1)  in  <n1  +  1,  f  n1  n2>  fi    \mmember{}  \mBbbN{}
                  {}\mrightarrow{}  (k:\mBbbN{}  \mtimes{}  (\mBbbN{}\^{}k))  BY
                Auto)
  THEN  (Assert  \mlambda{}p.let  p1,p2  =  p 
                                  in  if  (p1  =\msubz{}  0)  then  0  else  code-pair(p1  -  1;(fst((h  (p1  -  1))))  p2)  +  1  fi    \mmember{}  (k:\mBbbN{}
                            \mtimes{}  (\mBbbN{}\^{}k))  {}\mrightarrow{}  \mBbbN{}  BY
                          Auto)
  THEN  D  0
  THEN  RepUR  ``tidentity  identity``  0
  THEN  xxx((BetterExt  THEN  Auto)  THEN  Reduce  0  THEN  AutoSplit)xxx)

---

Home Index