Step
*
of Lemma
strong-continuity2-half-squash-surject-biject-ext
∀[T,S,U:Type].
((U ⊆r ℕ)
⇒ (∃r:ℕ ⟶ U. ∀x:U. ((r x) = x ∈ U))
⇒ (∃g:ℕ ⟶ T. Surj(ℕ;T;g))
⇒ (∃h:S ⟶ U. Bij(S;U;h))
⇒ (∀F:(ℕ ⟶ T) ⟶ S
⇃(∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f))))))
BY
{ Extract of Obid: strong-continuity2-half-squash-surject-biject
not unfolding ucont primrec mu Kleene-M int? is_int
finishing with (RepUR ``let`` 0 THEN Auto)
normalizes to:
λ%,%1,%2,%3,F.
let h,%4 = %3
in let g,%5 = %2
in let M = λf,i. (Kleene-M(λf.(h (F (λx.(g (f x)))))) i (λx.(fst((%5 (f x)))))) in
let r,%6 = %1
in <λn,f. case primrec(n;eval v = M f n in
if v is an integer then inl v
else inr Ax ;λi,r. eval v = M f i in
if v is an integer then inr Ax
else r)
of inl(m) =>
inl let x,y = %4
in fst((y (r m)))
| inr(x) =>
inr x
, λf.<<if primrec(mu(λn.is_int(M f n));eval v = M f mu(λn.is_int(M f n)) in
if v is an integer then inl v
else inr Ax ;λi,r. eval v = M f i in
if v is an integer then inr Ax
else r)
then mu(λn.is_int(M f n))
else let m,_,_ = primrec(mu(λn.is_int(M f n));λf,b,%,%1. Ax;
λi,x,f,b,%2,%3.
if i + 1=0
then Ax
else eval x1 = Kleene-M(λf.(h
(F
(λx.(g
(f
x))))))
((i + 1) - 1)
f in
if x1 is an integer
if primrec((i + 1) - 1;inl x1;
λi,r. eval v = ...
i
f in
if v is an integer
inr Ax
else r)
then <(i + 1) - 1, Ax, Ax>
else let m,_,%37 = x f (inl x1) Ax
Ax in
<m, Ax, %37>
fi
else let m,_,%34 = x f b %2 %3 in
<m, Ax, %34>)
(λx.(fst((%5 (f x)))))
eval v = M f mu(λn.is_int(M f n)) in
if v is an integer then inl v
else inr Ax
Ax
Ax in
m
fi
, Ax
>
, λn.Ax
>
> }
Latex:
Latex:
\mforall{}[T,S,U:Type].
((U \msubseteq{}r \mBbbN{})
{}\mRightarrow{} (\mexists{}r:\mBbbN{} {}\mrightarrow{} U. \mforall{}x:U. ((r x) = x))
{}\mRightarrow{} (\mexists{}g:\mBbbN{} {}\mrightarrow{} T. Surj(\mBbbN{};T;g))
{}\mRightarrow{} (\mexists{}h:S {}\mrightarrow{} U. Bij(S;U;h))
{}\mRightarrow{} (\mforall{}F:(\mBbbN{} {}\mrightarrow{} T) {}\mrightarrow{} S
\00D9(\mexists{}M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (S?)
\mforall{}f:\mBbbN{} {}\mrightarrow{} T
((\mexists{}n:\mBbbN{}. ((M n f) = (inl (F f))))
\mwedge{} (\mforall{}n:\mBbbN{}. (M n f) = (inl (F f)) supposing \muparrow{}isl(M n f))))))
By
Latex:
Extract of Obid: strong-continuity2-half-squash-surject-biject
not unfolding ucont primrec mu Kleene-M int? is\_int
finishing with (RepUR ``let`` 0 THEN Auto)
normalizes to:
\mlambda{}\%,\%1,\%2,\%3,F.
let h,\%4 = \%3
in let g,\%5 = \%2
in let M = \mlambda{}f,i. (Kleene-M(\mlambda{}f.(h (F (\mlambda{}x.(g (f x)))))) i (\mlambda{}x.(fst((\%5 (f x)))))) in
let r,\%6 = \%1
in <\mlambda{}n,f. case primrec(n;eval v = M f n in
if v is an integer then inl v
else inr Ax ;\mlambda{}i,r. eval v = M f i in
if v is an integer then inr Ax
else r)
of inl(m) =>
inl let x,y = \%4
in fst((y (r m)))
| inr(x) =>
inr x
, \mlambda{}f.<<if primrec(mu(\mlambda{}n.is\_int(M f n));
eval v = M f mu(\mlambda{}n.is\_int(M f n)) in
if v is an integer then inl v
else inr Ax ;\mlambda{}i,r. eval v = M f i in
if v is an integer then inr Ax
else r)
then mu(\mlambda{}n.is\_int(M f n))
else let m,$_{}$,$_{}$ = p\000Crimrec(mu(\mlambda{}n.is\_int(M f n));\mlambda{}f,b,\%,\%1. Ax;
\mlambda{}i,x,f,b,\%2,\%3.
if i + 1=0
then Ax
else eval x1 = ...
((i + 1)
- 1)
f in
if x1 is an integer
if primrec((i + 1) - 1;
inl x1;
\mlambda{}i,r. ...)
then <(i + 1) - 1
, Ax
, Ax>
else ...
fi
else ...)
(\mlambda{}x.(fst((\%5 (f x)))))
eval v = M f mu(\mlambda{}n.is\_int(M f n)) in
if v is an integer then inl v
else inr Ax
Ax
Ax in
m
fi
, Ax
>
, \mlambda{}n.Ax
>
>
Home
Index