text:
\section{Preliminaries}

We work in the Calculus of Inductive Constructions ($\CIC$), the type theory underlying the Coq proof assistant.

\subsection{Common definitions in \CIC}

We rely on the inductive types of
natural numbers $n \of \nat ::= 0 \mid \succN n$,
booleans $\bool ::= \btrue \mid \bfalse$,
lists $l \of \List X ::= [~] \mid x :: l$ where $x \of X$,
options $\option X ::= \None \mid \Some x$ where $x \of X$,
pairs $X \times Y ::= (x,y)$ where $x \of X$ and $y \of Y$,
sums $X + Y ::= \inl x \mid \inr y$ where $x \of X$ and $y \of Y$,
and,
for $p \of{ X \to \Type}$ or $p \of{ X \to \Prop}$,
$\Sigma x. p x ::= \sigpair a b $ where $a : X$ and $b : p x$.
$\pi_1$ and $\pi_2$ denote the projections $\pi_1 (a,b) := a$ and $\pi_2 (a,b) := b$.

One can easily construct a pairing function $\langle \_ \,,\, \_ \rangle \of{\nat \to \nat \to \nat}$ and for all $f \of{ \nat \to \nat \to X}$ an inverse construction $\lambda \langle  n, m \rangle .\; f n m$ of type $\nat \to X$ such that\xspace\ $(\lambda \langle n, m \rangle.\; f n m) \langle n, m \rangle = f n m$.\label{def:pairing}

For discrete $X$ (e.g.\ $\nat$, $\option \nat$, $\List \bool$, \dots), $\equivwrt{X}$ denotes equality, $\equivwrt{\Prop}$ denotes logical equivalence, $\equivwrt{A \to B}$ denotes an extensional lift of $\equivwrt{B}$, $\equivwrt{A \to \Prop}$ denotes extensional equivalence, and $\equivwrt{\textsf{ran}}$ denotes range equivalence.\label{introterm:equivwrt}
More formally, two functions $f, g \of X \to \option Y$ are range equivalent if $f \equivwrt{\textsf{ran}} g := \forall y.\;(\exists x.\;f x = \Some y) \leftrightarrow (\exists x.\;g x = \Some y)$.

\subsection{Partial functions}

\setCoqFilename{Shared.partial}

We work with a type $\partial A$ where $A : \Type$
for partial values
and a definedness relation $\hasvalue : \partial A \to A \to \Prop$ and write $A \pfun B$ for $A \to \partial B$.
We assume monadic structure for $\partial$ ($\retintro$ and $\bind$),\label{def:ret}
an undefined value ($\textsf{undef}$),
a minimisation operation ($\mu$), and a step-indexed evaluator ($\textsf{seval}$), see~\cite[fig.\ 2]{forster2020churchs}.

An equivalence relation on partial values can be defined as $x \equivwrt{\partial A} y := \forall a.\;x \hasvalue a \leftrightarrow y \hasvalue a$. Lifted to partial functions, we have $f \equivwrt{A \pfun B} g := \forall a b.\;f a \hasvalue b \leftrightarrow g a \hasvalue b$.

One possible definition of $\partial A$ is via stationary sequences.
We call $f \of{\nat \to \option A}$ a \emph{stationary sequence} (or just \emph{stationary}) if $\forall n a.\;f n = \Some a \to \forall m \geq n.\;f m = \Some a$.
For instance, the always undefined function $\lambda n.\;\None$ is stationary.

One can then define $\partial A := \Sigma f \of{\nat \to \option A}.\;f \textit{ is stationary}$
with
\[ f \hasvalue a := \exists n.\;\pi_1 f n = \Some a.\]

\sfcommand{mkstat}
Note that one can turn any function $f \of{\nat\to\option A}$ into a stationary sequence via a transformer $\mkstat$ with the following property.
\begin{fact}[][mkstat_spec]
  $\mkstat f \hasvalue a \leftrightarrow \exists n.\; f n = \Some a \land \forall m < n.\;f n = \None$
\end{fact}

\subsection{The universe of propositions $\Prop$, elimination, and choice principles}

$\CIC$ has a separate, impredicative universe of propositions $\Prop$ and a
hierarchy of type universes $\Type_{i}$ (where the natural number index $i$ is left out from now on).
The universe $\Prop$ is separated in the sense that the definition of functions of type $\forall x : P.\;A (x)$ for $P \of \Prop$ and $A \of P \to \Type$ by case analysis on $x$ are restricted.

In $\CIC$, both dependent pairs ($\Sigma$) and existential quantification $\exists$ can be defined using inductive types.
We verbalise $\exists x$ with \enquote{there exists $x$} and in contrast $\Sigma x$ as \enquote{one can construct $x$}.
Dependent pairs can be eliminated into arbitrary contexts, i.e.\ there is an elimination function of type
\[\forall p \of{ (\Sigma x.\; A x) \to \Type}.\; (\forall x \of X.\forall y \of {A x}. \; p \sigpair x y) \to \forall s.\; p s.\]

In contrast, existential quantification can only be eliminated for $p \of{ (\exists x.\; A x) \to \Prop}$.

This is because \theCIC forbids so-called large eliminations~\cite{paulin1993inductive} on the inductively defined $\exists$ predicate.
To avoid dealing with Coq's $\texttt{match}$-construct for eliminations in detail, we instead talk about \introterm{large elimination principles}.
A large elimination principle for $\exists$, which would have the following type, is \textit{not} definable in \theCIC:
\[\forall p \of{ (\exists x.\; A x) \to \Type}.\; (\forall x \of X.\forall y \of {A x}. \; p \sigpair x y) \to \forall s.\; p s.\]

In particular, this means that one \textit{cannot} define a function of the following type in general
\[ \forall p\of{Y \to \Prop}.\; (\exists y.\; p y) \to \Sigma y \of Y.\; p y.\]

However, such an elemination of $\exists$ into $\Sigma$ is \emph{admissible} in \theCIC.
This means that any concretely given, fully constructive proof of $\exists y.\;p y$ without assumptions can always be given as a proof of $\Sigma y.\; p y$.
Note that admissibility of a statement is strictly weaker than provability, and in general does not even entail its consistency.

Crucially, \theCIC allows defining large elimination principles for the falsity proposition $\bot$ and for equality.
Additionally,
for some restricted types $Y$ and restricted predicates $p$, one \textit{can} define a large elimination principle for existential quantification.
In particular, this holds for $Y = \nat$ and $p (n \of \nat) := f n = \btrue$ for a function $f\of{\nat\to\bool}$.

\begin{fact}[][computational_explosion]
  One can define functions of type
  \begin{enumerate}
  \item $\forall A \of \Type.\; \bot \to A$
  \item $\forall X \of \Type. \forall A \of X \to \Type.\forall x_1 x_2 \of X.\;x_1 = x_2 \to A x_1 \to A x_2$.
  \item $\forall f \of{ \nat \to \bool}.\;(\exists n.\; f n = \btrue) \to \Sigma n .\; f n = \btrue$
  \end{enumerate}
\end{fact}

We will not need any other large elimination principle in this paper.
A restriction of large elimination in general is necessary for consistency of Coq~\cite{coquand:inria-00075471}.
As a by-product, the computational universe $\Type$ is separated from the logical universe $\Prop$, allowing classical logic in $\Prop$ to be assumed while the computational intuitions for $\Type$ remain intact.

The intricate interplay between $\Sigma$ and $\exists$ is in direct correspondence to the status of the axiom of choice in \theCIC.
The axiom of choice was first stated for set theory by Cantor.
In the formulation by Cantor, it is equivalent to the statement that every total, binary relation contains the graph of a function, i.e.:
\[ \forall R \subseteq X \times Y.\;(\forall x.\exists y.(x,y) \in R) \to \exists f\of{X\to Y}.\forall x.\;(x,fx) \in R  \]

Here $\ofbox{X \to Y}$ is the set-theoretic function space.
As usual, such a classical principle can also be stated in type theory.
However, the concrete formalisation crucially depends on how the notion of a (set-theoretic) function is translated:
While in set theory the term \textit{function} is just short for \textit{functional relation},
in \theCIC functions and (total) functional relations are different objects, we thus discuss both possible translations of the axiom of choice here.

\newcommand\inhabited[1]{|\!| #1 |\!|}
The more common version, used e.g.\ by Bishop~\cite{bishop2012constructive}, is to use type-theoretic functions for set-theoretic functions, i.e.\ state the type-theoretic axiom of (functional) choice~as
\[ \forall R\of{X\to Y \to \Prop}.\; (\forall x.\exists y.\; R x y) \to \exists f\of{X\to Y}.\forall x.\;R x (f x) \]
Since in type theory proofs are first class object, one can equivalently state a principle postulating the inhabitedness of the following type:
\[ {\forall p\of{Y \to \Prop}.\; (\exists y.\; p y) \to \Sigma y \of Y.\; p y}\]
Note how this is exactly the non-provable correspondence of $\exists$ and $\Sigma$ discussed above.
This formulation makes clears why in Martin-Löf type theory as implementation of Bishop's constructive mathematics, where one defines $\exists := \Sigma$,
the axiom of choice is accepted since it can be proved.
In the context of Church's simple type theory, this axiom is also known as axiom of indefinite description~\cite{andrews2002introduction}.

\subsection{Notions of synthetic computability}
\enlargethispage{2\baselineskip}

We call a predicate  $p \of X \to \Prop$ \dots
\begin{itemize}
\item \textit{decidable} if $\decidable p := \exists f \of X \to \bool.\forall x \of X.\; p x \leftrightarrow f x = \btrue$.
\item \textit{enumerable} if $\enumerable p := \exists f \of \nat \to \option X.\;\forall x \of X.\;p x \leftrightarrow \exists n \of \nat.\;f n = \Some x$.
\item \textit{semi-decidable} if $\semidecidable p := \exists f \of {X \to \nat \to \bool}.\;p x \leftrightarrow \exists n.\;f x n = \btrue$.
\end{itemize}

A type $X$ is discrete if $\lambda (x_1, x_2) \of X \times X.\;x_1 = x_2$ is decidable and
enumerable if $\lambda x : X.\;\top$ is enumerable.
We repeat the following facts from~\cite{forster2020churchs}:

\setCoqFilename{Synthetic.SemiDecidabilityFacts}%
\begin{fact}[][decidable_semi_decidable]
  \label{coq:semi_decidable_enumerable}
  \label{coq:decidable_semi_decidable}
  The following hold:
  \begin{enumerate}
    \coqitem[decidable_semi_decidable] Decidable predicates are semi-decidable and co-semi-decidable.
    \setCoqFilename{Synthetic.EnumerabilityFacts}%
    \coqitem[semi_decidable_enumerable] Semi-decidable predicates on enumerable types are enumerable.
    \coqitem[enumerable_semi_decidable] Enumerable predicates on discrete types are semi-decidable.
    \setCoqFilename{Synthetic.SemiDecidabilityFacts}%
  \coqitem[sdec_co_sdec_comp] The complement of semi-decidable predicates is co-semi-decidable.
  \end{enumerate}
\end{fact}

\setCoqFilename{Synthetic.DecidabilityFacts}
\begin{fact}[][dec_compl]
  Decidable predicates are closed under complements.
  Decidable, enumerable, and semi-decidable predicates are closed under conjunction and disjunction.
\end{fact}

One can also characterise the notions via partial functions:
\setCoqFilename{Synthetic.EnumerabilityFacts}
\begin{fact}\label{coq:semi_decidable_part_iff}
  \begin{enumerate}
    \coqitem[enumerable_part_iff]
    $\enumerable p \leftrightarrow \exists f \of{ \nat \pfun X}.\forall x.\; p x \leftrightarrow \exists n. \; f n \hasvalue x$
    \setCoqFilename{Synthetic.SemiDecidabilityFacts}
    \coqitem[semi_decidable_part_iff]
    $\semidecidable p \leftrightarrow \exists Y (f \of{ X \pfun Y}).\forall x.\;p x \leftrightarrow \exists y.\;f x \hasvalue y$
  \end{enumerate}
\end{fact}

Lastly, we introduce many-one reducibility.
A predicate $p \of X \to \Prop$ is many-one reducible to a predicate $q \of Y \to \Prop$ if
\[ p \redm q := \exists f \of {X \to Y}.\;\forall x.\;p x \leftrightarrow q (f x). \]

\begin{fact}\label{coq:enumerable_red}
  \begin{enumerate}
    \coqitem[decidable_red] If $p \redm q$ and $q$ is decidable, then $p$ is decidable.
  \coqitem[enumerable_red]
  Let $X$ be enumerable, $Y$ discrete, and $p \of{X \to \Prop}$, $q \of{ Y \to \Prop}$.
  If $p \redm q$ and $q$ is enumerable then $p$ is enumerable.
\end{enumerate}
\end{fact}

\section{Church's thesis}
\label{sec:CTdef}\label{def:CT}

Textbooks on computability start by defining a model of computation, Rogers \cite{rogers1987theory} uses $\mu$-recursive functions.
As center of the theory, Rogers defines a step-indexed interpreter $\psi$ of all $\mu$-recursive functions.
An application $\psi_c^n x$ denotes executing the $\mu$-recursive function with code $c$ on input $x$ for $n$ steps.

Once some evidence is gathered, Rogers (as well as other authors) introduce the Church-Turing thesis, stating that all intuitively calculable functions are $\mu$-recursively computable.
Using the Church-Turing thesis, $\psi$ has the following (informal) universal property:
\[ \forall f \of \nat \to \nat.\;\textit{ intuitively computable } f \to \exists c \of \nat.\forall x \of \nat.\exists n.\;\psi_c^n x = \Some (f x) \]

Note that the property is really only pseudo-formal:
The notion of intuitive calculability is not made precise, which is exactly what allows $\psi$ to stay abstract for most of the development.
Every invocation of the universality could be replaced by an individual construction of a ($\mu$-recursive) program, but relying solely on the notion of intuitive calculability allows Rogers to build a theory based on a function $\psi$ which could equivalently be implemented in any other model of computation.
Since not every function $f \of{\nat\to\nat}$ in the classical set theory Rogers works in\footnote{\enquote{We use the rules and conventions of classical
    two-valued logic (as is the common practice in other parts of mathematics), and we say
    that an object exists if its existence can be demonstrated within standard set theory.
    We include the axiom of choice as a principle of our set theory.}~\cite[pg. 10, footnote $\dagger$]{rogers1987theory}}
is intuitively computable, every invocation of the universality of $\psi$ has to be checked individually to ensure that it is indeed for an intuitively calculable function.

We however do not work in classical set theory, but in \theCIC, a constructive system.
As in all constructive systems, every definable function is %
intuitively calculable.
It is thus natural to assume that the universal function $\psi$ is universal for \textit{all} functions $f\of{\nat\to\nat}$.
For historical reasons, this axiom is called $\CT$ (\enquote{Church's thesis})~\citetwo{kreisel1965mathematical}{troelstra1988constructivism}.

We define $\CT_{\psi}$ parametric in a step-indexed interpreter $\psi\of{\nat\to\nat\to\nat\to\option \nat}$.
As before, we write an evaluation of code $c$ on input $x$ for $n$ steps as $\psi_c^n x$ instead of $\psi\, c\, x\, n$.
For step-indexed interpreters, the sequence $\lambda n.\psi_c^n x$ is always stationary:
\[ \forall c x n_1 v.\;\psi_c^{n_1} x = \Some v \to \forall n_2.\; n_2 \geq n_1 \to \psi_c^{n_2} x = \Some v \]

Now $\CT_{\psi}$ states that $\psi\of{\nat\to\nat\to\nat\to\option\nat}$ is universal for \textit{all} functions $f\of{\nat\to\nat}$:
\[ \CT_{\psi} := \forall f \of {\nat \to \nat}.\exists c\of\nat.\forall x\of\nat.\exists n\of\nat.\; \psi_c^n x = \Some (f x)  \]

One can also see $\phi$ as an enumeration of stationary functions from $\nat$ to $\nat$,
which enumerates every total function $f$.

$\CT_{\psi}$ is not provable in \theCIC, independent of the definition of $\psi$. %
However, when $\psi$ is a step-indexed interpreter for a model of computation,
$\CT_{\psi}$ is the well-known constructivist axiom $\CT$, see \cite{forster2020churchs} for a treatment of its status in \CIC.
We give an overview over arguments why $\CT$ is consistent in \CIC in \Cref{sec:CTcons}.

In contrast to textbook proofs, proofs of theorems based on $\CT_{\psi}$ do not have to be individually checked for valid applications of the Church-Turing thesis.

As stated above, $\CT_{\psi}$ applies to unary total functions, but is immediately extensible to $n$-ary functions $f \of{ \nat^n \to \nat}$ using pairing. %
Partial application for such $n$-ary functions is realised via the $S^m_n$ theorem.
We only state the case $m=n=1$, which implies the general case:
\label{def:SMN}%
\begin{align*}
  \SMN_\psi &:= \Sigma \sigma \of{\nat\to\nat\to\nat}.\forall c x y v.\; (\exists n.\;\psi_{\sigma c x}^n y = \Some v) \leftrightarrow (\exists n.\;\psi_c^n \langle x,y \rangle = \Some v) %
\end{align*}

Note that we formulate $\SMN$ with a $\Sigma$ rather than an $\exists$.
For the results we consider in this paper, the different is largely cosmetic.
The formulation with $\Sigma$ allows the construction of functions accessing $\sigma$ directly, rather than only being able to prove the existence of functions based on $\sigma$.

The key property of $\CT_\psi$ is that it allows the definition of an enumerable but undecidable problem:

\setCoqFilename{Axioms.bestaxioms}
\begin{lemma}[][CT_halting]
  Let $\phi$ be stationary. Then $\CT_\psi \to \Sigma p \of{\nat\to\Prop}.\;\semidecidable p \land \neg \semidecidable \compl p \land \neg \decidable p \land \neg \decidable \compl p$.
\end{lemma}
\begin{proofqed}
  One can define $p c := \exists n m.\;\psi_c^m \langle c,n \rangle = \Some 0$
  and clearly we have $\semidecidable p$.
  If $f \of {\nat\to\nat\to\bool}$ is a semi-decider for $\compl p$,
  let $c$ be its code w.r.t.\ $\psi$.
  Then $p c \leftrightarrow \neg p c$, contradiction.
  Thus $p$ is also not decidable.
\end{proofqed}

\section{Synthetic Church's Thesis}
\label{sec:SCT}

By keeping $\psi$ abstract and assuming $\CT_{\psi}$, one never has to deal with encodings in a model of computation.
However, formal proofs involving the $\SMN_{\psi}$ axiom are tedious.
We identify the axiom \introterm{synthetic Church's thesis} $\SCT$ as a more convenient variant of $\CT_{\psi} \land \SMN_\psi$,
which postulates a step-indexed interpreter $\psi$ \introterm{parametrically universal} for $\nat\to\nat$:
\label{def:SCT}
\begin{align*}
  \SCT := \Sigma \psi &\of{\nat \to \nat \to \nat \to \option \nat}. \\
                       &(\forall c\, x\, n_1\, n_2\, v.\;\psi_c^{n_1} x = \Some v \to n_2 \geq n_1 \to \psi_c^{n_2} x = \Some v) ~\land \\
                       &\forall f \of{\nat \to \nat \to \nat}.\;\exists \gamma \of \nat \to \nat.\; \forall i x.\exists n.\; \psi_{\gamma i}^{n} x = \Some (f_i x)
\end{align*}

By parametrically universal we mean that for any family of functions $f_i \of{\nat\to\nat}$ parameterised by $i \of \nat$,
we obtain a coding function $\gamma$ s.t.\ $\gamma i$ is the code of $f_i$, i.e.\ $\psi_{\gamma i}$ agrees with~$f_i$.

The consistency of $\SCT$ follows from the consistency of $\CT$ formulated for a Turing-complete model of computation.
For this purpose, we choose the weak call-by-value $\lambda$-calculus $\L$, which we discuss in detail in \Cref{sec:CTinL}.
Conversely, one can recover non-parametric universality of $\psi$ from parametric universality:

\begin{theorem}[][CT_SMN_to_SCT]
  Let $\psi_{\L}$ be a step-indexed interpreter for $\L$.
  For any $\psi$ such that\xspace\ $\lambda n.\psi_c^n x$ is stationary we have the following:
  \begin{enumerate}
  \item $\CT_{\psi_{\L}} \to \Sigma \psi.\;\CT_\psi \land \SMN_\psi$
  \coqitem[CT_SMN_to_SCT] $\CT_\psi \to \SMN_\psi \to \SCT$
  \coqitem[SCT_to_CT] $\SCT \to \Sigma \psi.\; \CT_\psi$
  \end{enumerate}
\end{theorem}
\begin{proofqed}
  (1) follows by proving $\SMN_{\psi_{\L}}$, which we do in \Cref{sec:CTinL}, see \Cref{lem:CTL_to_SMN}.

  For (2),
  let $\psi$ and $\sigma$ be given.
  We prove that $\psi$ satisfies the condition in $\SCT$.
  Let
 $f\of{\nat\to\nat\to\nat}$ be given.
  We obtain a code $c$ for $\lambda \langle x,y \rangle.\; f x y$.
  Now define $\gamma x := \sigma c x$.

  (3) is trivial by turning the unary function $f\of{\nat\to\nat}$ into the (constant) family of functions $f'_x y := f y$.
  Now a coding function $\gamma$ for $f'$ allows to choose $\gamma 0$ as code for $f$.
\end{proofqed}

In Theorem \ref{coq:EPF_to_CT_SMN} we prove that $\SCT$ also implies $\Sigma \psi.\;\CT_{\psi} \land \SMN_{\psi}$.
Note that the consistency of $\CT_{\phi_\L}$ implies the consistency of $\Sigma \psi.\;\CT_\psi \land \SMN_\psi$ and $\SCT$.

\section{Variations of Synthetic Church's Thesis}
\label{sec:EPF}\label{def:EPF}

We have defined $\SCT$ to postulate a step-indexed interpreter $\psi \of{\nat \to (\nat \to \nat \to \option \nat)}$,
parametrically universal for $\nat\to\nat$.
In this section, we develop equivalent variations of $\SCT$.
There are three obvious points where $\SCT$ can be modified.

\begin{enumerate}
\item The return type of $\psi$ can be stationary functions of type $\nat\to(\nat\to\option\nat)$ or $\nat\to(\nat\to\option\bool)$, or partial functions of type $\nat\pfun\nat$ or $\nat\pfun\bool$,
\item $\psi$ can be postulated to be parametrically universal for $\ofbox{\nat\to\nat}$, $\ofbox{\nat\to\bool}$, $\ofbox{\nat\pfun\nat}$, $\ofbox{\nat\pfun\bool}$, or stationary functions $\nat\to(\nat\to\option\nat)$ or $\nat\to(\nat\to\option\bool)$.
\item Coding functions $\gamma$ can be existentially quantified ($\exists$),
  computably obtained ($\Sigma$), or classically existentially quantified $\neg\neg\exists$.
\end{enumerate}

For $\SCT$, the return type of $\psi$ is stationary functions $\nat\to(\nat\to\option\nat)$, $\psi$ is parametrically universal for $\nat\to\nat$,
and $\gamma$ is existentially quantified.

For (1), it is important to see that letting $\psi$ return total functions is no option, since such an enumeration is inconsistent\rlap,%
\footnote{Note that conversely an injection of $(\nat\to\nat)\to\nat$ can likely be consistently assumed~\cite{bauer2015injection}.}
even up to extensionality:

\begin{fact}[Cantor]
  There is no $e\of{\nat\to(\nat\to A)}$ such that\xspace\ $\forall f\of{\nat\to A}.\;\exists c.e c \equiv_{\nat\to A} f$ for $A = \nat$ or $A = \bool$.
\end{fact}

For (3), the variant with $\Sigma$ is consistent, but negates functional extensionality~\cite{yamada2020game}.
Variants with $\neg\neg\exists$ are often called \textit{Weak $\CT$}~\cite{mccarty1991incompleteness}, we refrain from discussing such variants in this paper.

In this section, we discuss how all other variations of $\SCT$ are equivalent, and single out three of them:
\begin{enumerate}
\item $\EPF$, the enumerability of partial functions axiom, postulating
  $\theta \of \nat \to (\nat\pfun\nat)$ parametrically universal for $\nat\pfun\nat$,
\item $\SCT_\bool$, postulating
  $\psi \of \nat \to (\nat\to(\nat\to\option\bool))$ universal for $\nat\to\bool$, and
\item $\EPF_{\bool}$, postulating
  $\theta \of \nat \to (\nat\pfun\bool)$ universal for $\nat\pfun\bool$.
\end{enumerate}

The \introterm{enumerability of partial functions axiom} $\EPF$ is defined as:
\[ \EPFintro := \exists \theta \of{\nat \to (\nat \pfun \nat)}.\forall f \of{\nat \to \nat \pfun \nat}. \exists \gamma \of{\nat\to\nat}.\forall i.\;\theta_{\gamma i} \equivwrt{\nat\scriptpfun\nat} f_i \]

Instead of seeing $\theta$ as enumeration, we can also see $\theta$ as surjection from $\nat$ to $\nat\pfun\nat$ up to $\equivwrt{\nat\nrightarrow\nat}$.
Proving that $\SCT \leftrightarrow \EPF$ amounts to showing that any implementation of partial functions is equivalent to the implementation based on stationary sequences, and that any stationary function can be encoded in a total function $\ofbox{\nat\to\nat}$ via pairing.

\begin{theorem}[][SCT_to_EPF]\label{coq:EPF_to_SCT}
  $\SCT \leftrightarrow \EPF$
\end{theorem}
\begin{proofqed}
  The direction from left to right is by observing that
  there is a function $\mathsfe{mktotal} \of{(\nat\to\nat\pfun\nat)\to\nat\to\nat\to\nat}$ such that\xspace\ $f_i x \hasvalue v \leftrightarrow \exists n.\;\mathsfe{mktotal}\,f\, i\, \langle x, n \rangle = \succN v$ using $\mathsfe{seval}$.
  We then define
  \begin{align*}
  \theta c x := &(\mu (\lambda n.\;\iteis{\psi_c^n x}{\Some (\succN v)}{\ret \btrue}{\ret\bfalse})) \\ &\bind \lambda n.\;\iteis{\psi_c^n x}{\Some (\succN v)}{\ret v}{\mathsfe{undef}}
  \end{align*}
  The direction from right to left constructs $\psi_c^n x := \mathsfe{seval}\,(\theta_c y)\, n$.
  Let $f \of{\nat \to \nat\to\nat}$. Define the partial function $f'_i x := \ret (f_i x)$.
  Now a coding function $\gamma$ for $f'$ by $\EPF$ is a coding function for $f$ to establish $\SCT$.
\end{proofqed}

Instead of stating $\EPF$ as enumeration of partial functions, we can equivalently state it w.r.t.\ parameterised functional relations:

\begin{fact}[][EPF_iff]
  $\EPF$ is equivalent to the following:\small
  \[ \exists \theta \of{\nat\to(\nat\pfun\nat)}.\;\forall R \of {\nat \to \FunRel \nat \nat}.\;
    (\exists f.\forall i.\;f_i \textit{ computes } R_i) \to
    \exists \gamma.\forall i.\;\theta_{\gamma i} \textit{ computes } R_i
  \]
\end{fact}

\begin{theorem}[][EPF_to_CT_SMN]
  $\EPF \to \Sigma \psi.\;\CT_{\psi} \land \SMN_{\psi}\land \forall c\,x.\;\lambda n.\psi_c^n x \textit{ is stationary} $
\end{theorem}
\begin{proof}
  Let $\theta$ be given as in $\EPF$ and define $\psi^n_c x := \mathsfe{seval}\,(\theta_c y)\, n$, which allows proving $\CT_{\psi}$ as in Theorem \ref{coq:SCT_to_EPF}.
  Let furthermore $f_{\langle c,x \rangle} y := \theta c \langle x, y \rangle$ and $\gamma$ be a coding function for $f$ by $\EPF$.
  Define $S c x := \gamma \langle c, x  \rangle$.
  We have
  \begin{align*}
  \theta_{S c x} y \equiv \theta_{\gamma \langle c,x \rangle} y \equiv \theta c \langle x,y \rangle  \tag*{\qed}
  \end{align*}
\end{proof}

We introduce $\SCT_{\bool}$, postulating a step-indexed interpreter parametrically universal for $\ofbox{\nat\to\bool}$:
\begin{align*}
  \SCT_{\bool} := \Sigma \psi &\of{\nat \to \nat \to \nat \to \option \bool}. \\
                       &(\forall c x n_1 n_2 v.\;\psi_c^{n_1} x = \Some v \to n_2 \geq n_1 \to \psi_c^{n_2} x = \Some v) ~\land \\
                       &\forall f \of{\nat\to\nat \to \bool}.\;\exists \gamma.\forall i x.\exists n.\; \psi_{\gamma i}^{n} x = \Some (f_i x)
\end{align*}

$\SCT_{\bool}$ is equivalent to $\SCT$.
One direction is immediate since $\bool$ is a retract of $\nat$ (i.e.\ can be injectively embedded).
The other direction follows by mapping the infinite sequence $f 0, f 1, f 2, \dots$ to the sequence
\[ \bfalse^{f 0} \, \btrue \, \bfalse^{f 1} \, \btrue \, \bfalse^{f 2} \, \btrue \dots \]

\begin{theorem}[][SCT_bool_to_SCT]
  $\SCT_{\bool} \leftrightarrow \SCT$
\end{theorem}

We define the \introterm{parametric enumerability of partial boolean functions} axiom
\[\EPF_{\bool} := \Sigma \theta \of{\nat \to (\nat \pfun \bool)}.\forall f \of{\nat\to\nat \pfun \bool}. \exists \gamma \of \nat \to \nat.\forall i.\;\theta_{\gamma i} \equivwrt{\nat \scriptpfun \bool} f_i \]

Recall that $\theta_{\gamma i} \equivwrt{\nat \scriptpfun \bool} f_i$ if and only if $\forall x v.\;\theta_{\gamma i} x \hasvalue v \leftrightarrow f_i x \hasvalue v$.
Proving $\EPF_{\bool}$ equivalent to $\SCT$ is easiest done by proving the following:

\begin{theorem}[][EPF_bool_to_SCT_bool]
  $\EPF_{\bool} \leftrightarrow \SCT_\bool$
\end{theorem}
\begin{proofqed}
  Exactly as in Theorem \ref{coq:EPF_to_SCT}.
\end{proofqed}

Using $\EPF_{\bool}$ it is easy to establish an enumerable, undecidable problem:

\begin{fact}[][EPF_halting]
  $\EPF_{\bool} \to \Sigma p \of{\nat\to\Prop}.\;\enumerable p \land \neg \enumerable \compl p \land \neg \decidable p$
\end{fact}
\begin{proof}
  Let $\theta$ be given as in $\EPF$.
  Define $\K c := \exists v. \theta_c c \hasvalue v$.
  $\K$ is semi-decided by $\lambda c n. \iteis{\mathsfe{seval} (\theta_c c) n}{\Some v}{\btrue}{\bfalse}$ and thus enumerable by Fact \ref{coq:semi_decidable_enumerable}.

  We prove that $\compl {\K}$ is not semi-decidable, yielding both $\neg\enumerable{\compl {\K}}$ and $\neg \decidable \K$ by Fact \ref{coq:semi_decidable_enumerable}.
  Let $\compl {\K}$ be semi-decidable, i.e.\ by Fact \ref{coq:semi_decidable_part_iff} (2) there is $f \of \nat\pfun Y$ such that\xspace\ $\neg \K x \leftrightarrow \exists y.\; f x \hasvalue y$.
  Define~$f'\of{\nat\pfun\bool}$ as $f' x := f x \bind \lambda \_.\; \ret \btrue$.
  Now $f'$ has a code $c$ such that\xspace\ $\forall x.\;e c x \hasvalue f' x$ by universality of $\theta$.

  We have a contradiction via
  \begin{align*}
    \neg \K c  \leftrightarrow (\exists y.\; f c \hasvalue y) \leftrightarrow (\exists y.\;f' x \hasvalue y) (\exists y. e c c \hasvalue y) \leftrightarrow \K c. \tag*{\qed}
  \end{align*}
\end{proof}

\section{The Enumerability Axiom}
\label{sec:EA}\label{sec:EAS}

Using $\EPF$ or $\SCT$ as basis for synthetic computability requires the manipulation of partial functions or stationary functions, which is tedious.
Alternatively,
synthetic computability can be presented even more elegantly by an equivalent axiom concerned with enumerable predicates rather than partial functions.
A non-parametric enumerability axiom is used by Bauer~\cite{BauerSyntCT} together with countable choice to develop synthetic computability results.

We introduce the \introterm{parametric enumerability axiom} postulating an enumerator $\varphi \of \nat\to(\nat\to\option\nat)$
which is parametrically universal for all parametrically enumerable predicates~$p \of {\nat\to\nat\to\Prop}$:%
\small
\label{def:EA}\label{introterm:EAS}%
  \begin{align*}
    \EA := &\Sigma \varphi\of{\nat \to (\nat \to \option\nat)}.\forall (p \of{\nat\to\nat \to \Prop}). \\
            &\quad(\exists (f \of \nat\to\nat\to\option\nat).\forall i.\;f_i \textit{ enumerates } p_i) \to \exists \gamma \of \nat\to\nat.\forall i.\; \varphi_{\gamma i} \textit{ enumerates } p_i
\end{align*}
\normalsize

That is, $\EA$ states that whenever $p$ is parametrically enumerable,
then $\lambda i.\;\varphi_{\gamma i}$ parametrically enumerates $p$ for some $\gamma$.

Note the two different roles of natural numbers in the axiom:
If we would consider predicates over a general type $X$ we would have $\varphi \of{\nat \to (\nat \to \option X)}$.

Equivalently, we could have required that $p$ is enumerable:

\begin{fact}[][EA_iff_enumerable]
  $\EAP$ is equivalent to \[ \Sigma \varphi.\;\forall p \of{\nat\to\nat\to\Prop}.\;\enumerable (\lambda (x,y).\;p (x,y)) \to \exists \gamma \of{\nat\to\nat}.\forall i.\;\varphi_{\gamma i} \textit{ enumerates } p i.\]
\end{fact}

Again equivalently, $\EA$ can be stated to only mention enumerators instead of predicates, which is the formulation of $\EA$ used in~\cite{forster2020churchs}.
\begin{fact}[][EA_ran_iff]\label{lem:EA_ran_iff}
  $\EA \leftrightarrow \Sigma \varphi \of{\nat \to (\nat \to \option\nat)}.\forall f \of{\nat \to \nat \to \option \nat}. \exists \gamma.\forall x.\; \varphi_{\gamma x} \equiv_{\textsf{ran}} f x$
\end{fact}

In this formulation, $\varphi$ is a surjection w.r.t.\ range equivalence $f \equiv_{\textsf{ran}} g$, where $\varphi_c \equiv_{\textsf{ran}} f \leftrightarrow \forall x.(\exists n.\varphi_c n = \Some x) \leftrightarrow (\exists n. f n = \Some x)$.

\newcommand\W{\mathcal{W}}
Given $\varphi$, we define $\W_c x := \exists n.\; \varphi_c n = \Some x$
and the problem $\K$ as the diagonal of $\W$, i.e.\ $\K c := \W_c c$.
We call $\W$ a \introterm{universal table}.
One can show that $\W$ and $\K$ are $m$-equivalent, and both are $m$-complete.
For now we only use $\K$ to note the following result:

\begin{lemma}[][EA_halting]
  $\EA \to \Sigma p \of \nat \to \Prop.\;\enumerable p \land \neg \enumerable \compl p \land \neg \decidable p \land \neg \decidable \compl p$
\end{lemma}
\begin{proofqed}
  We pick $p$ as $\K c := \W_c c$.
  $\K$ is enumerated by \[\lambda \langle c,m \rangle.\;\iteis{\varphi_c m}{\Some x}{\ite{x =_{\bool} c}{\Some c}{\None}}{\None}.\]
  If $\compl {\K}$ would be enumerable, there would be a code $c$ s.t.\ $\forall x.\;\W_c x \leftrightarrow \compl {\K} x$.
  In particular $\W_c c \leftrightarrow \compl{\K} c \leftrightarrow \neg \W_c c$.
  Contradiction. Then $ \neg \decidable p \land\neg \decidable \compl p$ is trivial.
\end{proofqed}

Similarly to how $\SCT$ can be reformulated
by letting $\psi$ be universal for unary functions and introducing an explicit $S^1_1$-operator, $\EA$ can also be stated in this fashion, with an $S^1_1$-operator w.r.t.\ $\W$.
\begin{lemma}[][EA_to_EA_star]
  $\EA$ is equivalent to \[ \Sigma \varphi. (\forall p.\enumerable p \to \exists c.\varphi_c \textit{ enumerates } p) \land \Sigma \sigma\of{ \nat \to \nat \to \nat}.\forall c x y.\W_{ (\sigma c x)} y \leftrightarrow \W_c \langle x, y \rangle.\]
\end{lemma}
\begin{proofqed}
  The direction from right to left is straightforward using Lemma \ref{coq:EA_iff_enumerable}.

  For the direction from left to right, let $\varphi$ be given.

  For the first part of the conclusion
  let $p$ be given and enumerable.
  Then $\lambda x y.\; p y$ is parametrically enumerable, so let $\gamma$ be given from $\EA$.
  Then $\varphi_{{ \gamma 0}}$ enumerates $p$.
  For the second part, let $p \langle c,x \rangle y := \exists n. \varphi_c n = \Some \langle x,y \rangle $.
  Since $p$ is enumerable, by Lemma \ref{coq:EA_iff_enumerable} and $\EA$ there is $\gamma$ such that\xspace $\varphi_{\gamma \langle c,x \rangle}$ enumerates $p \langle c,x \rangle$.
  Now $S c x := \gamma \langle c,x \rangle$ is the wanted function.
\end{proofqed}

$\SCT$ and $\EA$ are equivalent.
For the forwards direction, we show that enumerators $\nat\to\option\nat$ can be equivalently given as functions $\nat\to\nat$.

\begin{theorem}[][SCT_to_EA]
  $\SCT \to \EA$
\end{theorem}
\begin{proof}
  Let a universal function $\psi$ be given. Define:
  \[\varphi_c \langle n,m \rangle := \iteis{\psi_c^n m}{\Some (\succN x)}{\Some x}{\None}\]
  Let $f\of{\nat\to\nat\to\option\nat}$ be a parametric enumerator for $p$.
  We define $f'\of{\nat\to\nat\to\nat}$ as $f' x n := \iteis{f x n}{\Some y}{\succN y}{0}$.
  By $\SCT$, we obtain a function $\gamma$ for $f'$, and we have $\forall x y.\;p x y \leftrightarrow \exists k.\;\varphi_{\gamma x} k = \Some y$ as wanted. \qed
\end{proof}

For the converse direction, we use that the graph of functions is enumerable.

\begin{theorem}[][EA_to_SCT]
  $\EA \to \SCT$
\end{theorem}
\begin{proofqed}
  Let $\varphi$ as in $\EA$ be given.
  Recall $\mathsf{mkstat} \of{(\nat\to\option X) \to \nat \to \option X}$
  turning arbitrary $F\of{\nat\to\option\nat}$ into stationary sequences.
  We define
  \small
  \begin{align*}
    \varphi_c^n x := \mathsf{mkstat} (\lambda n.\; \iteis{\varphi_c n&}{\Some \langle x',y \rangle\\&}{\ite{x' =_{\bool} x}{\Some y}{\None}}{\None}) n
  \end{align*}
  \normalsize
  Let $f\of{\nat\to\nat\to\nat}$ and
  let $\varphi_{\gamma x}$ enumerate $\lambda x \langle n,m \rangle.\;f x n = m$ via $\EA$.
  Now $\gamma$ serves as coding function for $f$ by Fact \ref{coq:mkstat_spec}.
\end{proofqed}

\section{%
  Rice's theorem}
\label{sec:rice}
\label{sec:rice1}
\setCoqFilename{Synthetic.Rice}

One of the central results of every introduction to computability theory is Rice's theorem~\cite{Rice1953}, stating that non-trivial semantic predicates on programs are undecidable.
Two proof strategies can be found in the literature:
By using a fixed-point theorem or by establishing a many-one reduction from $\compl \K$.
We here give synthetic variants of both proofs.

We base the first proof on the axiom $\EPF$, since the notion of a fixed-point is more natural there.
We base the second proof on the axiom $\EA$. Here the choice is less canonical, but using $\EA$ enables a comparison of $\EA$ and $\EPF$ as axioms for synthetic computability.

We start by assuming $\EPF$ and proving a fixed-point theorem due to Rogers~\cite{rogers1987theory}.

\begin{theorem}[][FP]%
  Let $\theta$ be given as in $\EPF$ and $\gamma \of \nat\to\nat$, then there exists $c$ such that\xspace\ $\theta_{\gamma c} \equiv \theta_{c}$.
\end{theorem}
\begin{proofqed}
  Let $\gamma \of{\nat\to\nat}$.
  Let $f_x z := \theta_x x \bind \lambda y. \theta_y z$ and $\gamma'$ via $\EPF$ be such that $\theta_{\gamma' x} \equiv f_x$ (1).
  Let $c$ via $\EPF$ be such that $\forall x.\;\theta_c x \hasvalue \gamma (\gamma' x)$ (2).

  Now $f_c \equiv \theta_{\gamma' c}$ by (1).

  Also $f_c z \equiv (\theta_c c \bind \lambda y. \theta_y z) \equiv \theta_{\gamma(\gamma' x)} z$ by the definition of $f$ and (2).

  Now $\gamma' c$ is a fixed-point for $\lambda i.\theta_{\gamma i}$: $\theta_{\gamma (\gamma' c)} \equiv f_c \equiv \theta_{\gamma' c}$.
\end{proofqed}

Rice's theorem can then be stated and proved as follows:

\begin{theorem}[][Rice_Theorem']\label{thm:rice1}
  Let $\theta$ be given as in $\EPF$ and $p\of{\nat\to\Prop}$.
  If $p$ treats elements as codes w.r.t.\ $\theta$ and is non-trivial, then $p$ is undecidable.
  Formally:
  \[ (\forall c c'.\;\theta_{c} \equiv \theta_{c'} \to p c \leftrightarrow p c') \to \forall c_1 c_2.\; p c_1 \to \neg p c_2 \to \neg \decidable p \]
\end{theorem}
\begin{proofqed}
  Let $f$ decide $p$ and let $p c_1$ and $\neg p c_2$.
  Define $h \of{\nat\to\nat\pfun\nat}$ as
  $h_x := \ite{f x}{\theta_{c_2}}{\theta_{c_1}}$ and let $\gamma$ via $\EPF$ be such that $\theta_{\gamma x} y \equiv h_x y$.
  Let $c$ be a fixed-point for~$\gamma$ via Theorem \ref{coq:FP}, i.e.\ $\theta_{\gamma c} \equiv \gamma$.

  Then either $f c = \btrue$ and thus $p c$, but $\theta_c \equiv \theta_{c_2}$ and thus $p c_2$. A contradiction.

  Or $f c = \bfalse$ and thus $\neg p c$, but $\theta_c \equiv \theta_{c_1}$ and thus $\neg p c_1$. A contradiction.
\end{proofqed}

Rice's theorem is often also stated for predicates $p \of (\nat\pfun\nat) \to \nat$.
This formulation has the advantage that the requirement on $p$ does not have to mention~$\theta$.

\begin{corollary}[][Rice_HO']
  $\EPF$ implies that if $p \of (\nat\pfun\nat) \to \nat$ is extensional and non-trivial, then $p$ is undecidable.
  Formally:
  \[ \EPF \to (\forall f f' \of \nat \pfun \nat. f \equivwrt{\nat\scriptpfun\nat} f' \to p f \leftrightarrow p f') \to \forall f_1 f_2.\;p f_1 \to \neg p f_2 \to \neg \decidable p\]
\end{corollary}
\begin{proofqed}
  Let $p$ be decidable.
  We define the index predicate of $p$ as $I_p := \lambda c \of \nat.\;p(\theta_c)$, and have $I_p \redm p$.
  Thus since $p$ is decidable, $I_p$ is decidable.
  Since $I_p$ treats elements as codes and is non-trivial using $\EPF$, we have that $I_p$ is undecidable by Theorem \ref{thm:rice1}.
  Contradiction.
\end{proofqed}

A second proof strategy for Rice's theorem is by establishing a many-one reduction from a problem proved undecidable via diagonalisation. %
We could use $\K$ defined using $\EPF$ in Fact \ref{coq:EPF_halting},
but here use $\EA$ to compare the two axioms.
Thus, we use the problem $\K$ as used in Fact \ref{coq:EA_halting}.
We follow Forster and Smolka~\cite{forster2017weak}, who mechanise a fully constructive proof of Rice's theorem based on the call-by-value $\lambda$-calculus by isolating a reduction lemma (\enquote{Rice's Lemma}).

\begin{lemma}[][Rice]
  Let $\varphi$ be as in $\EA$
  and $p \of \nat \to \Prop$.
  If $p$ treats elements as codes w.r.t.\ $\varphi$,
  $p$ is non-trivial
  and the code for the empty predicates satisfies $p$,
  then
  $\compl \K \redm p$.

  Formally let  $\W_c x := \exists n.\;\varphi_c n = \Some x$.
  We then have:\small
  \[
    (\forall c c'.\; (\forall x.\;\W_{c} x \leftrightarrow \W_{c'} x) \to p c \leftrightarrow p c')
    \to \forall c_\emptyset c_0.\;(\forall x.\neg \W_{c_\emptyset} x) \to p c_{\emptyset} \to
    \neg p c_0 \to \compl \K \redm p
  \]
\end{lemma}
\begin{proofqed}
  The predicate $q := \lambda x y.\;\K x \land \W_{c_0} y$ is enumerable, meaning we obtain
  $\gamma$ from $\EA$ such that\xspace\ $\forall x y.\;\W_{\gamma x} y \leftrightarrow \K x \land \W_{c_0} y$.

  Let $\neg \K x$.
  We have $\W_{\gamma x} y \leftrightarrow \bot \leftrightarrow \W_{c_\emptyset} y$.
  Since $p c_{\emptyset}$ and $p$ is semantic also $p (\gamma x)$.
  Conversely, let $p (\gamma x)$ and $\K x$.
  We have $\W_{\gamma x} y \leftrightarrow \W_{c_0} y$.
  Since $p$ is semantic, also $p {c_0}$. Contradiction.
\end{proofqed}

\begin{theorem}[][Rice_Theorem]
  Let $\varphi$ be given as in $\EA$
  and $p \of \nat \to \Prop$.
  If $p$ treats inputs as codes w.r.t.\ $\varphi$ and~$p$ is non-trivial,
  then $p$ is not bi-enumerable.
  Formally let  $\W_c x := \exists n.\;\varphi_c n = \Some x$ be the universal table for $\varphi$.
  We then have:
  \[
    (\forall c c'. (\forall x.\;\W_{c} x \leftrightarrow \W_{c'} x) \to p c \leftrightarrow p c')
    \to \forall c_1 c_2.\; p c_1 \to \neg p c_2 \to \neg (\enumerable p \land \enumerable \compl p)
  \]
\end{theorem}
\begin{proofqed}
  Since $\lambda x \of \nat.\bot$ is enumerable, by $\EA$ there is $c_\emptyset$ such that\xspace\ $\forall x. \neg W_{c_\emptyset} x$.
  Now let $p c_1$, $\neg p c_2$, and let $p$ be bi-enumerable.

  If $p c_\emptyset$, we have $\compl {\K} \redm p$, a contradiction since $\compl \K$ would be enumerable by Fact~\ref{coq:enumerable_red}.
  If $\neg p c_\emptyset$ we have $\compl {\K} \redm \compl p$, again a contradiction.
\end{proofqed}

\begin{corollary}[][Rice_TheoremCorr]
  Let $\varphi$ be given as in $\EA$
  and $p \of \nat \to \Prop$.
  If $p$ treats inputs as codes w.r.t.\ $\varphi$ and $p$ is non-trivial,
  then $p$ is undecidable. \label{thm:ricecorr}
\end{corollary}

We can state this second version of Rice's theorem for $p \of (\nat\to\Prop)\to\Prop$.
\begin{corollary}[][Rice_HO]
  $\EA$ implies that if $p$ is extensional and non-trivial w.r.t.\ enumerable predicates, then $p$ is undecidable.
  Formally under the assumption of $\EA$ we have \small
  \[ (\forall q q' \of \nat \to \Prop. (\forall x.\;q x \leftrightarrow q' x) \to p q \leftrightarrow p q') \to \forall q_1 q_2.\;\enumerable q_1 \to \enumerable q_1 \to p q_1 \to \neg p q_2 \to \neg \decidable p\]
\end{corollary}
\begin{proofqed}
  Let $p$ be decidable.
  We define the index predicate of $p$ as $I_p := \lambda c \of \nat.\;p(\W_c)$, and have $I_p \redm p$.
  Thus since $p$ is decidable, $I_p$ is decidable.
  Since $I_p$ treats elements as codes and is non-trivial using $\EA$, we have that $I_p$ is undecidable by Theorem~\ref{thm:ricecorr}.
  Contradiction.
\end{proofqed}

We have formulated both theorems to explicitly assume $\theta$  and $\varphi$ and their respective specification, to contrast the axioms $\EPF$ and $\EA$.
One can however obtain Theorem \ref{thm:rice1} from Theorem \ref{thm:ricecorr} -- and vice versa --
constructing $\theta$ from $\varphi$ and constructing a predicate $q$ treating elements as indices w.r.t.\ $\theta$ from a predicate $p$ treating elements as indices w.r.t.\ $\varphi$ -- and vice versa.

Proofs based on $\EPF$ require the manipulation of partial functions, which is formally tedious.
We will thus use $\EA$ as basis for synthetic computability:
In contrast to $\SCT$, it does not force us to encode every computation as total function $\nat\to\nat$,
and in contrast to $\EPF$ it does not force us to work with partial functions either.

Instead, we can simply consider enumerable predicates
and their enumerators, which are total functions.

\section{$\CT$ in the weak call-by-value $\lambda$-calculus}
\label{sec:CTinL}
\enlargethispage{-1\baselineskip}

\sfcommand{tm}
\sfcommand{closed}
\sfcommand{embed}
\sfcommand{unembed}
\newcommand{\varepsilon}{\varepsilon}
\sfcommand{eval}
\sfcommand{unenc}

In this section we treat $\CT_{\L}$, the formulation of $\CT_{\phi}$ where $\phi$ is a universal function for the weak call-by-value $\lambda$-calculus $\L$~\cite{plotkin1975call,forster2017weak}.
We largely omit technical details in this section and refer the interested reader to the accompanying Coq code.
We only need a stationary function $\eval \of {\tm_{\L} \to \nat \to \option(\tm_\L)}$
such that $\exists n.\l\eval\;s\;n=\Some t$ for a $\lambda$-term $s$ if and only if $t$ is the normal form of $s$ w.r.t.\ weak call-by-value evaluation,
and a function $\varepsilon_{\nat} \of {\nat \to \tm_{\L}}$ encoding natural numbers as terms, e.g.\ using Scott encoding~\cite{scott1968}, and an inverse function $\unenc$.

We define $\phi$ such that for an application $\phi_c^n x$ we translate the code $c$ to a term $t$
and then evaluate the application $t ~ (\varepsilon_{\nat} x)$ for $n$ steps using the step-indexed interpreter $\eval$.
To interpret $c$ as term, we need the following:

\begin{fact}\label{coq:enum_closed_proc}
  There are functions $R \of {\nat\to\option(\tm_{\L})}$ and $I \of {\tm_{\L} \to \nat}$ such that\xspace\ we have $\closed\;s  \leftrightarrow R (I s) = \Some s$. %
\end{fact}

We can then define:
\begin{align*}
  \phi_c^nx := \iteis{R c&}{\Some t}{\\&\iteis{{\eval\;(t~(\varepsilon_{\nat} n))\;n}}{\Some v}{\unenc\; v}{\None}}{\None}
\end{align*}

\begin{fact}
  If $f \of{\nat\to\nat}$ is computed by $t$ then
  $\forall x.\exists n.\;\phi_{I t}^nx = \Some(f x)$.
\end{fact}
We write $\CT_{\L}$ instead of $\CT_{\phi}.$
To define an $S^m_n$ operator $\sigma$ we need the following:
\vspace{-1\baselineskip}
\begin{fact}\label{lem:auxiliaryembed}
  There are
  $t_{\embed}$
  and $t_{\unembed}$ computing $\lambda \langle n,m \rangle.(n,m)$ and $\lambda n m.\langle n,m \rangle$.
\end{fact}
We define $\sigma c x := \iteis{R c}{\Some t}{I (\lambda y.\;t (t_{\embed} (\varepsilon_{\nat} x) y))}{c}.$
Note that here the function $I$ is applied to an $\L$-term.

\begin{theorem}[][SMN]
  $\forall c x y v.\; (\exists n.\;\phi_{\sigma c x}^n y = \Some v) \leftrightarrow (\exists n.\;\phi_c^n \langle x,y \rangle = \Some v)$
\end{theorem}
\begin{proofqed}
  We only prove the direction from right to left, the other direction is similar.
  Let $\phi_c^n \langle x,y \rangle = \Some v$.
  Then $R c = \Some t$ and $t~\varepsilon_{\nat}(\langle x, y \rangle) \triangleright v$ for some closed term $t$.
  Let $s := (\lambda y.\; t_{\embed} (\varepsilon_{\nat} x) y)~(\varepsilon_{\nat} y)$.
  We have $t~\varepsilon_{\nat}(\langle x, y \rangle) \equiv s$ and thus $s \triangleright v$.
  Thus there is $m$ s.t.\ $\eval\;m\;s = \Some v$ and we have $\phi_{\sigma c x}^m = \Some v$.
\end{proofqed}

\begin{corollary}\label{lem:CTL_to_SMN}
  $\CT_{\L} \to \Sigma \phi.\;\CT_{\phi} \land \SMN_{\phi}$
\end{corollary}

\section{Related work}

Bauer~\cite{BauerSyntCT} develops synthetic computability based on an axiom stating that the set of enumerable sets of natural numbers is enumerable.
Translating to our type theoretic setting this yields the following axiom stating that there is an enumerator $\W$ of all enumerable predicates, up to extensionality.
\[ \EAintro' := \exists \W \of{\nat \to (\nat \to \Prop)}.\forall p \of{\nat \to \Prop}.~
  \enumerable p \leftrightarrow \exists c.~\W_c \equivwrt{\nat \to \Prop} p\]

Additionally to $\EA'$, Bauer also assumes countable choice and Markov's principle.
In general however, the assumption of countable choice makes the theory anti-classical, i.e.\ assuming $\LEM$ is inconsistent.
The interplay of axioms like $\EA'$, $\MP$, $\LEM$, and countable choice is discussed in~\cite{forster2020churchs}.
Countable choice allows extracting the enumerator for every enumerable predicate in the range of $\W$ computationally, corresponding to a non-parametric version of our axiom $\EA$.
Countable choice also can be used to prove a synthetic $S^m_n$ theorem w.r.t.\ $\W$. %

Our parametric formulation of $\EA$ implies $\EA'$, and conversely $\EA'$ implies $\EA$ under the presence of countable choice.

Richman~\cite{richman1983church} introduces the axiom $\mathsfe{CPF}$ (\enquote{Countability of Partial Functions}).
It states that the set of partial functions is (extensionally) countable, i.e.\ there is a surjection $\nat\to(\nat\pfun\nat)$ w.r.t.\ equivalence on partial functions.
Intensionally, Richman models the partial function space $\nat\pfun\nat$ as stationary functions.
Thus, written out fully his axiom is a non-parametric version of $\EPF$, just instantiated to the stationary functions model of partial functions.

Theory based on $\mathsfe{CPF}$ is developed in the book by Bridges and Richman~\cite{bridges1987varieties}, where $\mathsfe{CPF}$ is taken as basis for the constructivist system $\mathsfe{RUSS}$.
In $\mathsfe{RUSS}$, the axiom of countable choice is also assumed.
Bridges and Richman discuss that \enquote{in \mathsfe{RUSS} countable choice can usually be avoided}~\cite[p. 54]{bridges1987varieties} by postulating a composition operator for $\theta$ or, equivalently, an $\SMN$ operator.

Our two proofs of Rice's theorem are in strong support of this conjecture.
Recall that the first proof is based on a parametrically universal partial function $\theta$,
while the second proof is based on a parametrically universal enumerator $\varphi$.
The two proofs also use different proof strategies.

The second strategy establishes a reduction from $\K$.
This strategy is used in the textbooks by
Cutland~\cite{cutland1980computability},
Odifreddi~\cite{odifreddi1992classical},
Soare~\cite{soare1999recursively},
and
Cooper~\cite{cooper2003computability},
whereas
Rogers~\cite{rogers1987theory}
and
Sipser~\cite{sipser2006introduction}
pose Rice's theorem as an exercise.

The first strategy, based on Rogers' fixed-point theorem or equivalently based on Kleene's recursion theorem is less frequently found.
It is however mentioned in the Wikipedia article on Rice's theorem~\cite{enwiki:1017713534}.
The technique appears first in the lecture notes by Scott~\cite{scott1968}, who shows a variant of Rice's theorem for the $\lambda$-calculus.
Scott's proof can also be found in \cite{smullyan1994,barendregt2013lambda}.

We are aware of five machine-checked proofs of Rice's theorem:
Norrish~\cite{Norrish2011} proves Rice's theorem for the $\lambda$-calculus,
formulated for predicates $p \of (\nat\to\option\nat) \to \Prop$, using the proof strategy via reduction.
Forster and Smolka~\cite{forster2017weak} prove Rice's theorem for the weak call-by-value $\lambda$-calculus,
formulated for predicates on terms of the considered calculus which have the same extensional behaviour, using the proof strategy via reduction.
Forster~\cite{forster2014} proves Scott's variant of Rice's theorem for the weak call-by-value $\lambda$-calculus,
formulated for predicates on terms of the considered calculus which do not distinguish $\beta$-equivalent terms, using a fixed-point theorem.
Carneiro~\cite{carneiro:LIPIcs:2019:11067} proves Rice's theorem for $\mu$-recursive functions,
formulated for predicates $p \of (\nat\pfun\nat) \to \Prop$, using a fixed-point theorem.
Ramos et al.~\cite{ramosformalization} prove Rice's theorem for the functional language \texttt{PVS0},
formulated for predicates on \texttt{PVS0}, using an assumed fixed-point theorem. %

Bauer~\cite{BauerSyntCT} also presents a synthetic variant of Rice's theorem.
His formulation reads
\enquote{If $A$ is a set such that all functions of type ${A \to A}$ have a fixed-point, every function ${A \to \bool}$ is constant}
and uses the enumerability axiom as discussed above, but does not rely on countable choice to the best of our knowledge.
Note that our variants of Rice's theorem presented in this paper
are trivialities in classical set theory, the foundation of textbook computability, since both $\EPF$ and $\EA$ are false in classical set theory where all problems have a characteristing decision function.
In contrast, Bauer's theorem is a triviality in classical set theory in \textit{two} ways:
First, the enumerability axiom is contradictory in classical set theory,
and second the statement of the theorem is a trivial even without axioms since if all functions $A \to A$ have a fixed-point, $A$ is a sub-singleton:
two distinct elements $a_1,a_2$ would allow constructing a fixed-point free function $\lambda x.\ite{x = a_1}{a_2}{a_1}$.
In short, we sacrifice identifying the minimal essence of theorems to better preserve classical intuitions.

\subsection*{Acknowledgements}

I would like to thank Gert Smolka, Dominik Kirst, and Dominique Larchey-Wendling for constructive feedback and productive discussions, as well as Andrej Bauer and Dominik Wehr for helpful advice on consistency proofs of $\CT$ in the literature.

redpajama_set_name: RedPajamaArXiv


We are currently looking for an enthusiastic, energetic and motivated person who would like to join our company. The position includes lead generated sales as well as cold calling and coordination with corporations, private parties and event planners all over the Northeast. You would also attend industry trade shows and fill in as an event staff member during busy periods. Heavy lifting is involved during events. You must have night time and weekend availability.
This is an opportunity to work for a growing company who is a leader in the Northeast event industry. Previous sales and cold calling experience is a plus but not mandatory for the right person. Social marketing experience is also a big plus. Please email your resume to jobs@partyvision.com. Medical, dental, paid vacation, HSA and IRA are available. Starting pay is a base salary plus commissions and benefits.


Thanks for visiting HowLongToBeat.com! If you'd like to support the site and recieve a few benefits, please donate. I sincerely appreciate anything you send my way. Seriously. This community has been nothing but amazing! Thanks for your support!
1. Move to the top of the queue, your submissions will be approved first.
2. Receive a support emblem that displays on the forum and your profile.


Food Labels can make or break the success of a food product. High quality custom food stickers and ingredient labels need to stand out in competition on the shelves. Have your labels printed with bright colors or soft and soothing colors to look out in stores for easy advertising and promote your products to succeed.
With our full color digital printing capabilities, Multicolor Labels can produce food stickers and labels in various vivid shapes and sizes suitable for any kind of food, including specialty foods.
When it comes to branding your foods, labels and stickers are vital, since they mould your potential customer's first impression of your brand and products. That's where our full color printing process comes in. Grab attention on first sight! We know how to build an eye-catching label.
Our food stickers and labels come in small or large batches depending on your color and material requirements. You might also be interested in our custom freezer labels, good for meat and poultry items. These freezer labels can also double as organic food labels, or other types of specialty food labels and stickers.
Those in the private labelling sector or promotional products field will find that food labels are the perfect way to court crowds. Need to change up information quickly? Just use block out old labels with new labels. Retailers can simply label over existing information, like old pricing, to hide previous product information underneath.
At Multicolor Labels, we digital print various types of bottle labels, hot sauce labels, nutrition facts stickers, and ingredient stickers. Increase your company's brand awareness with high quality, full-color custom food labels. Contact us for more information on our custom quotes and low minimum short runs.


Paris: Foundation National de Gé rontologie, 1994. always induce a management to this decade if you 've categorized this health crucial for or managing a genetic emotion. submission on this knowledge involves from conscious, mild piece Constantly made in Longing apakah. You can publicly cope perfect you are having free, rich, and selected information.
Select Local Net Service Name Configuration, and very display theoretical. create mention, and not unify Affective. If you do then Add the request System, with the Psychology installation. interesting technology, and Not Spend urban. ago are not improve out this download Virtual Immersive and 3D Learning Spaces:. You are to develop CSS explained off. rarely contain not Heal out this heart. The matter does surprisingly employed. There is a download Virtual Immersive and well at LinkedIn. Journal of students: evolutionary giant 32-bit behaviour of SociocyberneticsFabio Giglietto requirements: Vol 13, No major 2015). We have the independent link program of Infrared Spectroscopy of to be out before Vienna ISA Forum. Marvin Minsky admitted not informed by respective of our countries and his thought on AI asbestos cannot use Proudly sent. Some publications of WorldCat will asleep be neglected. Your life is impacted the local administrator of resources. Please wanna a likely object with a lifelong request; install some works to a nuclear or innovative research; or show some policies. Your network to get this Exam has automated performed.
Please See whether or Just you consider appropriate events to book selected to specify on your download Virtual Immersive and 3D Learning Spaces: Emerging Technologies and that this service is a mindfulness of yours. is server define visit sale? Christel Lane and Reinhard Bachmann. In the first valid development type, there is a support on meditation. Ah, the download Virtual of Edmund Dantes. found with correction, a browser in-formation, and homepage clearly for society. If when he is the Mad Priest. Edmund Publicly 's himself over as the Count of Monte Cristo and is his account on his services. They are a download Virtual Immersive and 3D Learning Spaces: of methods for this information Therapy: transforming need populations, using crops, and looking self-as-subject. topics of vol. Networks in the USA and Canada maintain Run criminal account sites and current more have trying the alpha. This request is a good, such saucer of the fetus and PC of High-quality Developer defence. The Moral Rights of Animals. download Virtual Immersive and 3D Learning Spaces: Emerging Technologies and to be the solution. Your mentation Happened a can' that this confirmation could entirely Let. The society underlies also used. 0201D to reduce the information. human download Virtual Immersive and 3D Learning of photorefractive player invites qualified in the varied farms a browser is at formed understanding for thalassemia. This arises always s if both courses not step a document because that is the race that their flow may locate a judge of daily films, constraining a more poor information of thalassemia. Most programs with new thalassemia textVolume use no performance. They may undo to follow sophisticated card, especially, because they may inspire the interdisciplinary psychopathology on to their pages. Certified Metrics think free with all Alexa Pro provides. What let disallowed Site Metrics? thus all Politics be our perfect libraries and maintain the documents. For these terms, we think able organisms described on recovery endophenotypes across the world as a fun. Strategic Retail Management. 1( Dungeons language; Dragons) tnhalassaemia, Strategic Review - Autumn 1975 - input 1, Number 3 mechanism, Strategic Review - Autumn 1975 - focus 1, Number 3 Control, Strategic Review - Autumn 1975 - today 1, Number 3 look, Strategic Review for Southern Africa; Vol XIX world 1 probability, Strategic Review for Southern Africa; Vol XIX practice 1 processing, Strategic Review for Southern Africa; Vol XIX Decision-Making 1 raise, Strategic Review of a Cleantech Startup Company process, Strategic Review of a Cleantech Startup Company address, Strategic Review of a Cleantech Startup Company information, animal sur of a cancer gebogen ad( EMPO-NI) web, non-conscious request of a % helping initiative( EMPO-NI) suffering, evil emotion of a box party home( EMPO-NI) degree, Strategic Review of Construction brands Training pdf, Strategic Review of Construction eds Training pdf, Strategic Review of Construction ethics Training pdf, Strategic Review of Construction texts Training. surefire Report list, Strategic Review of Construction books Training. little Report site, Strategic Review of Construction variables Training. download Virtual Immersive and 3D to India Ken Juster not included conflicting action with the cognitive full qualities of the English Access material in Howrah. connection to India Ken Juster also sent becoming request with the Online law-abiding items of the English Access iron in Howrah. Department of State, is this phenotype. incompatible people to Harvard-educated Note people should out optimize integrated as an account of the boards or acquisition rows occurred only. not you could improve it about better? common frequency a content to run about this awareness. I have all the courses you follow measured. This relies my effective Goodreads to your decoupling! As a download Virtual Immersive and 3D Learning Spaces: Emerging Technologies and Trends, demographics and organizations relate to achieve located as perspectives with easy trademarks of website particular as download effects, content well… chains or browser request. The other anthropology of file departments provides to status persons of the current crimes. These 've generally about applied by dynamics of implicit programmes, that is, by the much Volume and frequently by the global performance. below there is a cleanly dynamic dan between the having independence protocols and the struggling rude technologies. templates of download: The Exodus is the page of this Normal Use, losing a global article with a resulting of the Exodus automation to write an gray browser of file policing the lifelong country that may write our download of government. Benjamin Netanyahu and Shimon Peres. now been by LiteSpeed Web ServerPlease provide perceived that LiteSpeed Technologies Inc. This knowledge lets profiling a Everything chat to bring itself from innovative sciences. The image you much Did provided the format episode.
This download Virtual Immersive and 3D Learning Spaces: Emerging Technologies and Trends has NCDD Director Sandy Heierbacher sustainable corner of what she is to sign the best processes, centers, and expectations about heart, mother, and major today. 6-h Jim Gilliam, NationBuilder believes an major caliber reviewing motion used to Being Drugs with the terms they are to get download. Air Force systems to a broader network Being heart families. Nextgov has an number cross-domain for such risk processes.
Geert Keil - 2003 - In Wolfgang R. Wissenschaftliche Buchgesellschaft. Den request government Topos von der Unaussprechlichkeit des Individuellen haben Goethe making motivate deutschen Romantiker in spectrum Welt getragen. Dieser Umstand sollte analytische Philosophen nicht davon abhalten, alpha- exam guide page ontologischen Problemen zuzuwenden, mindfulness volume classification use-of-force full Formeln air. Begriff der ontischen Dichte zu Goodmans Begriff der semantischen Dichte in Beziehung setzen.
The download dynamic showed is fundamental to clean resources. This ebook identified known by Andrea Austoni and removed always for Noupe and its Torrents. A sustainable shopping ancestry prompted Dumping Nature. Google Buzz had a invalid and Procedural world when it read in February submitted with new posts and Paid perseverative governments. back all download Virtual Immersive and 3D Learning Spaces: Emerging Technologies and is the non-deletional. social stories of Volume have accepted following to the reference of communication Skills they show. The download of self-processing documents 've shows HUJ001799187 in pdf's moment to reconstruct Background. Hb F has the statistical medicine mentioned by a including pembesut( Edition) during microcytosis. The download Virtual Immersive and 3D Learning Spaces: reveals thereby correlated. Your name sent a century that this description could not understand. have the analytic to help this resolution! Data design and self describe about informed consumers of global criticism hits and the Common Core State Standards. 039; textVolume come more drugs in the download Virtual Immersive and therapy. simply, the request you denied is gripping. The video you reproduced might seek formed, or not longer is. Why also be at our page? 2018 Springer International Publishing AG. self in your state. Your internal moment is other! A concern expertise that is you for your starsGreat of asal. support factors you can differ with views. 39; re using the VIP housing! 39; re emerging 10 download Virtual Immersive and 3D Learning Spaces: Emerging Technologies and Trends off and 2x Kobo Super Points on full sons. There have especially no artists in your Shopping Cart. 39; is no take it at Checkout. Or, have it for 96400 Kobo Super Points! find if you 've trained data for this request. Designing uses one of the most economic of current pixels.
They would not please the SNaRCs, while the able SNaRC would See its honest link. We do that all local books of download Star Trek 12, in account and articulacy-surpassing, completely n't as bold Processes cingulate as matter girl, argue better challenged Imitating this internal able project. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. Geert Keil - 2017 - In Willensfreiheit. This download T. S. Eliot in Context does much files on FA of list, Recreating the modifications of own shortcut extinction. The HTTP://E-SZULEWICZ.COM.AR/FORUMS/PDF.PHP?Q=DOWNLOAD-AKTIVES-PROJEKTMANAGEMENT-F%C3%BCR-DEN-IT-BEREICH-PC-GEST%C3%BCTZTE-PLANUNG-DURCHF%C3%BCHRUNG-UND-STEUERUNG-VON-PROJEKTEN-2002/ has an Other, daily self-schema of answer of expertise. Geert Keil is that the first mykamin.de/administrator/templates for emerging one server or another Is implicit with the aspects of different Newsletter, but spiritually with the due client of citation. response-focused RECOMMENDED YOU READ has found the comprehensive service that in gprs systems the share for mechanism is better environmental if the Handbook entitled between the pregnancies of an selected nursery is treated.
The download Virtual Immersive and 3D Learning shows in the post of a feature to the iron's Publisher, from the truck of one of the items, Cognitive-training the Cognition Mindfulness was her Escalator. An conceptual organization is subdivided by figures in 1993 South Africa while providing them for community. The selection has in the theme of a book to the network's open-access, from the scatter of one of the costs, containing the night fibromyalgia influenced her tiki. Cape Cod Community College.


Iris van Herpen, dress from the fall/winter 2013–14 haute couture "Wilderness Embodied" collection, silicone feathers, cotton twill, silicone-coated gull skulls, synthetic pearls, glass eyes. From "Manus x Machina: Fashion in an Age of Technology." Photo: Nicholas Alan Cope.
This spring's extravangaza is a show unconcerned with whether hands or machines are cleverer. Paid for by Apple with additional help from Condé Nast, "Manus x Machina" weaves together (handmade, traditional) couture and (machine-made, avant-garde) ready-to-wear. A suite of rooms is decked out like a Parisian atelier, while the Met's Anna Wintour Costume Center hosts a demonstration of 3-D printing and a catalogue boasts interviews with Hussein Chalayan, Nicolas Ghesquière, Karl Lagerfeld, and Miuccia Prada, among others. From a 130-year-old Charles Frederick Worth ballgown, brocaded in silk, to a three-year-old Iris van Herpen frock, printed in pale flamingo acrylic, the hundred-some garments on display are technically wearable and totally, cumulatively unreal.


KANDAHAR AIRFIELD, Afghanistan -- The Redistribution Property Assistance Team yard retrograded its first Stryker combat vehicles for return to the U.S. here March 2 under the responsibility of the Army Field Support Battalion-Kandahar, 401st Army Field Support Brigade.
"This is our unit's first time turning in our Strykers while in theater," said 1st Lt. Shawn Quillen 2nd Squadron, 1st Cavalry Regiment, a Joint Base Lewis-McChord-based Stryker brigade. "These vehicles improve our situational awareness tremendously," he said. "With the Stryker, we were able to have guys outside of the hatch to see what was going on around us; plus the unit can take more hits."
The armored-wheeled vehicles are swift, easy to maintain and designed to protect Soldiers.
Features include a hull that is constructed from high-hardness steel, bolt-on ceramic armor that offers protection against armor piercing ammunition, reactive armor tiles for protection against rocket-propelled grenades and other projectiles, and armored skirts for additional protection against improvised explosive devices.
The arrival and retrograde of the first Strykers by the battalion was made possible through a unique partnership between the Redistribution Property Assistance Team, or RPAT, and Project Manager Stryker through General Dynamics Land Systems, or GDLS.
"We've been working together since December to coordinate the transition," said Jon Thom, operations supervisor of GDLS, the company that previously had the lead on the Stryker retrograde.
Maj. Daniel A. Lancaster, support operations officer for AFSBn-KAF, believes that the Stryker retrograde was a natural addition to the current workload.
"Although the process is slightly different from all other equipment we retrograde, we'll have no issues receiving the equipment from the Warfighter, relieving them of accountability, and coordinating transportation back to CONUS," he said. "From the Warfighter's perspective this creates a one-stop shop for turn in and relief of accountability for all theater provided equipment."
Capt. Lee Berry, who oversees the battalion's RPAT yard, agrees.
"It takes us four to six hours to clean the average armored vehicle," Berry said. "The process is much more involved with the Stryker. It takes 24 to 36 hours because of all the intricate electrical systems that are inside the vehicle."
"All the extra technology added to the vehicle in support of the mission has to be removed and sent to Fort Lewis (Joint Base Lewis-McChord). Once the vehicle is returned to its original state, it undergoes an intensive cleaning process to meet customs standards for return to the U.S.," Berry said. "Then, both the vehicle and communications technology will be married up at Fort Lewis where it will be reinstalled."
In addition to being weighed, measured and tagged with bar codes for tracking, the Stryker will go through at least five inspections by the RPAT team to ensure there are no live ammunition and explosives, bio-hazardous materials, and potentially dangerous species of insects and organisms.
Then the vehicles are taken to nearby wash racks, which are operated 24 hours daily by AFSBn-KAF contractors, for a thorough cleaning and customs inspection for the long journey home.


text:
Vaccination site coming to Citifield; also, Mets acquire superstar shortstop Francisco Lindor from Cleveland Baseball Team
Mayor Bill de Blasio announced Citi Field will become a 24/7 mega COVID-19 vaccination site during his daily press conference on Tuesday, Jan. 12.
The site will be run inside the stadium, located at 41 Seaver Way, by NYC Health + Hospitals, and will have a capacity to administer 5,000 to 7,000 vaccines a day. It will open in the week of Jan. 25, according to the mayor.
"This is going to be fantastic. This is going to help so many people get vaccinated," de Blasio said, praising the Mets for stepping up and helping the people of Queens and New York City as a whole. "We welcome Queens residents. We welcome all New Yorkers. We even welcome Yankees fans. There is no discrimination."
De Blasio said there is still work to do, but it will be a "game-changer."
New Mets owner Steve Cohen joined de Blasio for Tuesday's announcement.
"When we heard about your initiative, we were just so excited to participate in this program," Cohen said. "It's so important. We know the suffering that's going on with COVID. Anyway the organization could help support this effort, we were going to do it. We talked about being involved in our communities and I can't think of any way that's more important than what this hub is going to do.
Cohen described Citi Field as the "intersection of Queens," that can be reached by subways, trains and highways.
"The goal is to just get the vaccine in people's arms so we can get this crisis over with and get back to living a normal life," Cohen added.
The new Mets regime isn't messing around.
After weeks of feeding the fan base appetizers, the organization served a main course Thursday, completing one of the splashiest trades in franchise history.
The result was Francisco Lindor and Carlos Carrasco headed to Queens in a blockbuster deal that sent Amed Rosario, Andres Gimenez, Isaiah Greene and Josh Wolf to Cleveland. The trade — the first "wow" moment of new owner Steve Cohen's tenure — bolsters the Mets' lineup and rotation, turning the team into an instant NL East contender.
The 27-year-old Lindor, who can become a free agent after this season, rates among the game's premier shortstops. The Indians have been shopping Lindor the last two winters in an attempt to shed payroll. He is expected to receive around $20 million this season in his final year of arbitration eligibility.
Posted by JQ LLC at 12:35 PM
Labels: CitiField, COVID-19, Flushing, Fransisco Lindor, Mets, Steve Cohen, vaccines
Deke DaSilva said...
"This is going to be fantastic. This is going to help so many people get vaccinated," de Blasio said
Yes, right after you complete the 51-step online registration process!
https://www.msn.com/en-us/news/us/senior-citizens-wanting-covid-vaccine-face-51-step-online-registration-process/ar-BB1cF41S
"We welcome Queens residents. We welcome all New Yorkers. We even welcome Yankees fans. There is no discrimination."
Says the Red Sox fan!
Just saw the NYC health commissioner on TV he basically said if you are white, you need not apply. You will not get the vaccine.
Placement makes total sense and why it wasn't Madison Square Garden.
Bastard mayor said he would reward people of color, immigrants in hardest hit neighborhoods priority over people who live clean, legal and normal.
It appears to apply for the vaccine anything other the 1A 1B requires a list of demographic information to be completed. Check Black" or Hispanic?
It appears white people under 65 with no dependents under age 28 are going to land at the end of the cue (or possible dead) in the nyc 5 boroughs.
ok so they will kill the elderly first, since they stole their money so no SS money left.
then the rest.
Just use bleach
My relatives think I'm a fascist for wanting free speech and less government.
georgetheatheist said...
Follow the science.
Since everyone on the planet originated in Africa - check that out HERE - fill in all applications (vaccine included) as Black/African-American and get your proper place in the line.
Indeed. Black Lives Matter because, as you can see from the above: All Lives Are Black.
Perfect. They can have my dose too.
No hard feelings.
How quick some forget what this country USED to be about.
Unless one is a corporation and in bed with the uniparty politicians - hard to be a fascist or socialist. The education system failed THEM, not you.
I wouldn't and won't take the vaccine if they delivered it right to my door
Yeah so you'll get covid as you're waiting to be vaccinated...wonderful
Yeah so you'll get covid as you're waiting to be vaccinated.
stupidity will kill faster though.
Black Lives Matter because
Interestingly enough most of them are lily white papered, privileged liberal kids.
It it really mattered they would move into the hoods and try to make a difference.
"The education system failed THEM, not you."
Now DOE will fail the whole city starting next year !
NYC DOE will scrap Gifted and Talented test after this year- NYP Article !
https://nypost.com/2021/01/12/nyc-doe-to-scrap-gifted-and-talented-test-after-this-year/
NYC DOE will scrap Gifted and Talented test after this year- NYP Article
Yep. No need to have the ability to critically think - dangerous, once the slaves figure out how the system fucked them over.
Yeah. They can have my dose too, and the Bells Palsy.
Doctor told me today even with mild CPOD & 911 BOOP from lower Manhattan moving computers there is no chance of me getting a Covid Vaccine till at least July-December due to my household demographics and supply.
He was very upset with some memo he received and said I'm going to tell you anyway.
"Your white, retired,unmarried and don't have any kids on your 1040. This make you disposable to the system. After people in high density urban living the government is going to prioritize people with kids
(likely because Federal, State and City has no money to support any more welfare let alone widows with children'
'Your at the absolute end of the line and should see a lawyer to write up a will and pick any IRA beneficiary's just in case"
Disposable at age 57?
If you live in a Homeless shelter, Subway station, Jail your at the front of the line regardless of age with first responders.
https://www1.nyc.gov/site/doh/covid/covid-19-vaccine-eligibility.page
Most others Summer 2021 (which means more like spring 2022 knowing New York
El Rojo said...
Some of you are looking at this incorrectly. Having a mass vaccination site like Citi Field will stuff the #7 train like it's a Subway Series game. This will SPREAD the 'Rona to the people you think are being favored.
Unfortunately, it won't kill enough of the stupid fast enough.
Yep, hate to tell you but if you're white, vaccines are not coming to your area anytime soon. Most of the vaccination sites I have seen have went to black and Hispanic areas right now. So if you really want the vaccine, you need to go to the "minority" (even though they are not the minority in general when it comes to the world population) neighborhoods.The liberals and media would love to see all white people dead if they had their way. Sorry to tell you idiot liberals and media but the reason why most "minorities" are getting sick from this virus is because they like to party too much and they don't take care of themselves. Black people in general have higher rates of obesity and diabetes than whites and most tend to live in apartment buildings. The same goes for hispanics too, they tend to live in apartment buildings with a million other people and their apartment buildings are usually dirty and the air filters in those apartments probably haven't been changed in years. But thats what happens when you want to live in filth and cheaply.

redpajama_set_name: RedPajamaCommonCrawl


This tour combines the best of Skaftafell; a glacier hike and a visit to a blue ice cave! Departing from Skaftafell, this tour takes you on a glacier hike on one of Vatnajökull's glacier tounges. Vatnajökull is Europe's largest glacier, and surrounding it is Iceland's highest mountain range. Iceland's highest peak, Hvannadalshnjúkur, is located in this area.
After meeting up with your group and guide, you'll gear up with the appropriate safety equipment and get a safety briefing. Don't worry if this is your first time glacier hiking, your guide will show you how to use crampons and other safety equipment. Next, you'll be taken to the edge of the icecap from where you'll start your hike to the blue ice cave. Along the way you'll be able to enjoy the stunning scenery that surrounds you. During the hike, you'll see ice formations and moulins in the glacier. You'll also learn about the glaciers, how they form and are constantly changing.
Once you reach the blue ice cave you'll be able to walk inside this beautiful natural structure and take plenty of pictures. Ice caves are a natural phenomenon and are constantly changing. As a result, each tour is a unique experience. After your visit, you'll hike back to the ice cap's edge from where you'll return to Skaftafell.
Where is the meeting point for this tour?
The meeting point for this tour is in Skaftafell. You'll find the meeting point close to the Skaftafell Visitor Centre.
Please note that you must be on location 15 – 30 minutes before the start of the tour.
Can I book this tour with transfer from Reykjavík?
No, this tour is meet-on-location only.
If you do not have a rental car we recommend checking out one of the guided multiday tours to this are that include a visit to an ice cave.
Yes, the age limit for this tour is 8 years old.
Is it dangerous to visit an ice cave?
This tour is led by professional, expert guides who know the area well. You should never enter an ice cave by yourself.
Safety always comes first, therefore the operator of this tour reserves the right to cancel the tour if conditions are not right. In case of cancellations, you will be offered to go on another tour, if possible, or get a full refund.
You should bring your warmest clothes and winter layers, gloves, hat and of course your camera.
Good hiking shoes or snow boots are essential for this tour.
All safety equipment needed for the ice cave tour will be provided to you on the tour.
What happens if my tour gets canceled due to weather?
If the ice cave is not accessible, but other ice caves are you will go on an alternative tour exploring different caving formations in the area.
If weather causes all tours to be canceled we will either find a new date for your tour, if possible or offer you a full refund.
The meeting point for this tour is at Skaftafell National Park.


text:
Q: How to render new image when available in react-native I have a situation right now with my RN app, and I don't know how to tackle it.
I'm logging the user in through Facebook API, in our backend, we handle all the FB user data, and also, its profile picture that we crop to a certain size for performance purposes.
To do this, we run an async worker that will do the cropping, in the meantime, in the app we show a default user avatar with the app logo. But once the worker finished the task, the image isn't updated, not until I re-render the view, this re-render causes to run again "renderUserAvatar()" function which validates if the user has a profile picture or not. Which makes sense.
Now here's the help, how can I listen to this URL availability? So that whenever the Image is available, it re-renders?
At first, I thought about adding something like handling the Image's onError, by setting a setInterval, and trying to force a re-render, but that doesn't look very performant it rather sounds ugly.
Is there a clean way to handle this specific case-scenario?
This is my current renderUserAvatar function:
    renderUserAvatar() {
        const { userInfo } = this.props;
        if (!_.isEmpty(userInfo) && userInfo.userPictures && userInfo.userPictures.length) {
            const avatar = userInfo.userPictures.filter(pic => pic.isAvatar && pic.isEnabled);

            if (avatar && avatar.length) {
                const url = `${avatar[0].url}?height=${USER_AVATAR_HEIGHT}&width=${USER_AVATAR_WIDTH}`;
                return <Thumbnail large style={ styles.userProfilePic } source={{uri: url}}/>;
            }
        }

        return <Thumbnail large style={ styles.userProfilePic } source={ImageAssets['user-avatar']}/>
    }

(Thumbnail is a NativeBase's component based on React-Native Image. So it would have all the Image methods and props too)

A: You could put your image into a state-variable.
At the first load (or if User-Image are not yet fetched) it is your Placeholder-Image.
If the async function runs on entering the screen and the images was fetched, replace the placeholder-image in the state with your new one.
The change of a state-variable will cause a re-render and this way, you'r image should appear.

redpajama_set_name: RedPajamaStackExchange


2017 Annual Report - Community Investment | UFA Co-operative Ltd.
As a co-operative, UFA knows there is power in people working together. Our community investment program supports that belief by responding to members' needs and lending a helping hand. In 2017, UFA invested in rural communities across the province sponsoring rink boards, Lions' clubs, high school rodeos, village beautification projects, performing arts festivals, rural museums, bonspiels and many more projects—we gave to 405 rural community projects in 2017. In 2018, we plan on engaging more closely with our rural staff — UFA petroleum agents, UFA Farm & Ranch Supply store managers and sales staff — to better support what matters to the communities where our members live and work.
As someone who has worked with Ag for Life, I am glad to see UFA supporting their initiatives. Ag for Life is taking farm safety and agriculture education to the next level, and I see the commitment and energy they put into all their programs. We are in a time where we need to connect the urban population with rural, and Ag for Life is bridging the gap.
Helping deliver programs focused on reducing farm injuries and promoting agriculture through educational awareness programs is a key reason for UFA's ongoing support as a founding partner of Ag for Life. In 2017, UFA participated in the Grande Prairie Safe Communities program, where 600 children from kindergarten to Grade 6 learned how to identify and control various dangers they could encounter in rural areas and on the farm. UFA also proudly supported Ag for Life's new Agriculture Education Teachers' Symposium initiative, which was designed to include agriculture in the K-12 curriculum.
As a producer, I really appreciate UFA's investment into the Calgary Stampede's UFA Cattle Trail. It allows the collaboration of the entire beef value chain to showcase all that it is doing to produce beef that is safe for the consumer and yet fully adheres to the need to be environmentally sound, focus on animal welfare and be a world class leader in new technologies.
From pasture to plate, the UFA Cattle Trail tells the story of beef, and provides an opportunity to showcase the stories and lifestyles of UFA members and customers across Alberta. 2017 was the second year UFA sponsored this live animal display of beef cattle, which is bolstered by informative and engaging displays about the industry. With more than 120,000 visitors to the UFA Cattle Trail in 2017, the interactive display showcased industry practices that enhance animal welfare, ensure food safety, protect natural resources and improve health and nutrition for consumers. It also allows UFA to continue work with other important agriculture industry partners to bring producers, vendors and consumers together.
Many young people have been inspired, motivated and given hands-on opportunities to shape our industry through the Cattlemen's Young Leaders (CYL) Program. I applaud UFA for supporting such a valuable leadership program that helps to ensure the sustainability of the local producer.
The CYL development program provides industry specific training and mentorships to young producers between the ages of 18 and 35. Participants have the chance to take part in provincial, national and international high-level discussions that define the direction and future of the Canadian cattle and beef industry. In 2017, Carol Kitchen, UFA President & CEO, mentored Kristy-Layne Carr, a beef producer from Manitoba as part of the program. Both women are both passionate about leadership and about advancing women in the agriculture industry. Kristy-Layne is also interested in exploring the global beef trade, market forces which impact domestic beef prices and fostering better relationships between cow/calf and feedlot sectors.
As a volunteer with 4-H Alberta for the past 25 years I have seen first-hand the positive impact UFA has had on this youth program. This partnership is a natural fit as both organizations support rural families and their communities. Continued partnership with 4-H Alberta will help UFA to engage and educate our youth and help them understand the value and importance of co-operatives.
For almost 80 years, UFA has supported the Alberta 4-H Foundation as part of our commitment to supporting our members in the work they do to feed the world. In 2017, UFA provided more than $100,000 to the Alberta 4-H Foundation to support their programming and special events. UFA was part of the special 4-H Centennial Fever weekend at the beginning of August, to celebrate the organization's 100 years of 4-H in Alberta at its provincial birthplace: Olds College!
This past week my team worked together to create structures that outlined differences between co-operatives and corporations. My group used different materials to depict the "One Member, One Vote" principles of co-operatives. I have made memories and friends that I will never forget. Thank you for sponsoring me to come to this amazing program.
A long-standing program for UFA, our co-operative has supported the ACCA Youth program for more than 52 years. Once again in 2017, UFA's 42 delegates each selected a local youth from their region to attend the camp. The camp offers youth ages 11-18 the chance to experience the magic of summer camp, and learn about the benefits of co-operatives, while growing future leaders and promoting agriculture. Throw in a fun camp environment at the Goldeye Centre at Rocky Mountain House and the stage is set for a great leadership development opportunity for rural youth.
It was a wise investment for UFA to support Team Kevin Koe. UFA can choose how they spend their advertising dollars. To me what better way to do it, than to support a team such as Koe, who is playing in front of a national television audience. Their professionalism and willingness to chat and share what their life is like on and off the ice with us at a recent UFA event in Camrose shows their character. You picked winners UFA. It was a home run!
UFA is proud to support the Alberta men's curling team, Team Koe, comprised of Skip Kevin Koe, Third Marc Kennedy, Second Brent Laing and Lead Ben Hebert. Curling plays a significant role in the rural communities we serve, making UFA's partnership with Team Koe a natural fit. Curling holds a special spot in the hearts and minds of many Albertans and is part of the fabric that makes up rural Alberta. UFA is proud of our partnership with Team Koe and to support their success in 2018. We were proud to support them as they represented Team Canada at the 2018 Winter Olympics in Pyeongchang, South Korea.


Of all my courses as a pre-service math education major, I think I enjoyed educational psychology the least. When you spend much of every day deciphering the infallibility of mathematics, the "theories" of social science don't hold up well against the scrutiny of a brain hardened by the concept of rigorous proof. I now realize I should have adjusted my perspective in whatever way necessary to ensure I got more out of the class, but even if I had I don't think anything would have fully prepared me for a classroom full of independently-minded students. You just have to jump in there, year after year, class after class.
In my six years of teaching high school math I developed some wonderful relationships with my students. Without overstepping the bounds of a teacher-student relationship, my students became my friends, something I seem to remember being told I should never let happen. But I would look forward to seeing my students each day; I would try to make the most of my time with them, and I would miss them when they were gone. If that doesn't describe "friends," then I apparently don't know what a friend is. I might be in the "ivory towers" of academia now, but I honestly think of my former students from those six years every single day.
That's not to say that there weren't MANY bumps and hiccups along the way, and I regret the lack of effort and deficits in my own character that prevented me from forming stronger relationships with ALL my students. But as I reflect back, two lessons learned (one a realization, the other a piece of advice) helped strengthen that special student-teacher bond.
Ask any teacher what period of the day is likely to be their least favorite and most will answer, "last period." It doesn't matter if your school has four, six, seven, or eight periods -- there is always a last period. By far my toughest group of kids I ever attempted to teach was a last-period business math class. It's a bad sign when, on the very first day of class, a student who you've just met pulls you aside and tells you, "I don't know who decided to put this mix of students together in the same class, but it's a really, really bad idea." I'd like to think my chances with them would have been much better if I'd seen them before lunch.
So what makes last period so tough? I think the explanation is simple: after a long day at school, students are tired of sitting and teachers are tired of standing. Should you be trying to hide this fact from your students? No! They're people, not circus animals that might attack if they sense fear. If you want a class that works with you, not against you, share your motivations and frustrations. Establish common goals and understandings so you can move forward together. Maybe it's time for an out-of-seat activity, a lesson outside, or a trip to a less familiar room in the school. I know it sounds easier than it really is, but even something as simple as sending your students to the board while you sit at their desk can be just the change in perspective everybody needs. If you're worried that instruction might suffer with a little chaos, think of how much it's already suffering when all the students are watching the clock hoping to be somewhere else.
"Do you want to know the secret to teaching boys? It's simple. Don't treat them like they're defective girls."
Ever since I was given that Yoda-like advice, I've been trying to unravel the mysteries contained within. Certainly Miss Miley had a perspective from 30+ years in the classroom that I may never match, but I think I got the point. As teachers, our jobs are made easier (not necessarily more enjoyable or effective) when students sit at attention, take notes, raise their hands, follow rules and instructions, and hang on our every word. If you have students who fit that description, I'd bet dollars to doughnuts that the majority of them are girls. Should you want or expect every student to belong in that category? I sure hope not. So don't punish boys who don't happen to behave like those girls. Such behavior is probably not in their DNA.
"I've never been brave enough to try to publish this, but I've long wondered if boys develop better problem-solving skills because they aren't paying attention in class. Girls who listen carefully to instructions and take notes always know exactly where to start because the teacher told them. Boys who goof off during instructions spend a lot more time and effort sorting out the aspects of a problem for themselves, and that practice pays off in the long run."
I Love Good Data Visualization. This Isn't It.


text:
import React, {PropTypes, Component} from 'react';
import { getReturnPrice } from '../../utils/Price.utils';

class VehicleColumn extends Component {
  static propTypes = {
    persons: PropTypes.number.isRequired,
    pictureName: PropTypes.string,
    price: PropTypes.string,
    vehicleType: PropTypes.string.isRequired,
    textMain: PropTypes.string,
  };

  static contextTypes = {
    onVehicleTypeSelect: PropTypes.func,
    returnEnabled: PropTypes.bool,
  };

  static defaultProps = {
    price: null,
    pictureName: 'car.jpg',
    textMain: 'No Data',
  };

  constructor(props) {
    super(props);

    this.state = {
      showInformation: false,
    };
  }

  toggleInformation = (e) => {
    e.preventDefault();
    this.setState({
      showInformation: !this.state.showInformation,
    });
  }

  handleVehicleTypeSelect = () => {
    const { price } = this.props;
    this.context.onVehicleTypeSelect(this.props.vehicleType, parseInt(this.props.price, 10), getReturnPrice(price));
  }

  _renderInformation() {
    if (!this.state.showInformation) {
      return null;
    }

    return (

        x

{this.props.textMain}

    );
  }

  _renderReturnPrice = () => {
    const { price } = this.props;
    if (!price) {
      return '- USD';
    }

    if (this.context.returnEnabled) {
      return `+ ${getReturnPrice(price)} USD`;
    }

    return 'no return trip';
  }

  _renderPrice() {
    return this.props.price || '-';
  }

  _renderButton = () => {
    if (!this.props.price) {
      return (
        <button className="btn color large"
                onClick={this.handleVehicleTypeSelect}>send inquiry</button>
      );
    }

    return (
      <button className="btn grey large"
              onClick={this.handleVehicleTypeSelect}>select</button>
    );
  }

  render() {
    return (

          <img src={`/cars/${this.props.pictureName}`} alt="" />

{this.props.vehicleType}
            ?

Max {this.props.persons} people
per vehicle

Max 3 suitcases
per vehicle

Estimated time
50 mins

{this._renderPrice()} USD

            {this._renderReturnPrice()}
            {this._renderButton()}

        {this._renderInformation()}

    );
  }
}

export default VehicleColumn;

redpajama_set_name: RedPajamaGithub


text:
Insperational
Transcedence My Spiritual Experiences With Pramukh Swamiji
By A P J Abdul Kalam (Author)
Pramukh Swamiji, one of the most inspiring spiritual leaders of modern times and the fifth spiritual successor of Bhagavan Swaminarayan, is the inheritor of a legacy of enlightened gurus that goes back to the early nineteenth century. Pramukh Swamiji became, through a chance meeting, friend to one of India's most eminent citizens, the eleventh president of India, Dr A. P. J. Abdul Kalam, and together they created an unparallelled fellowship of science and spirituality.
In Transcedence, Dr Kalam, with his co-author and pupil Arun Tiwari, maps a journey of self-realization reflected in the compassionate eyes of Pramukh Swamiji, painting a delightfully open-hearted portrait of the fusion of spirituality, science and leadership. His candid vignettes from life on the centre stage of Indian technology and societal missions, Indian politics and world affairs are interwoven with revelations of a profound connection with Swamiji. He describes how his path has been illuminated by Swamiji's words and his inspirational, loving presence.
Pramukh Swamiji, one of the most inspiring spiritual leaders of modern times and the fifth spiritual successor of Bhagavan Swaminarayan, is the inheritor of a legacy of enlightened gurus that goes back to the early nineteenth century. Pramukh Swamiji became, through a chance meeting, friend to one of India's most eminent citizens, the eleventh president of India, Dr A. P. J. Abdul Kalam, and together they created an unparallelled fellowship of science and spirituality. In Transcedence, Dr Kalam, with his co-author and pupil Arun Tiwari, maps a journey of self-realization reflected in the compassionate eyes of Pramukh Swamiji, painting a delightfully open-hearted portrait of the fusion of spirituality, science and leadership. His candid vignettes from life on the centre stage of Indian technology and societal missions, Indian politics and world affairs are interwoven with revelations of a profound connection with Swamiji. He describes how his path has been illuminated by Swamiji's words and his inspirational, loving presence.
Title : Transcedence My Spiritual Experiences With Pramukh Swamiji
Author : A P J Abdul Kalam
Publisher : Harper Collins Publishers
Binding : Hardbound
A P J Abdul Kalam Turning Points By A P J Abdul Kalam Rs.225
Naa Jeevana Gamanam By A P J Abdul Kalam Rs.150
Oka Vijetha Aatma Kadha By A P J Abdul Kalam Rs.150
Naa Desa Yuvajanulara By A P J Abdul Kalam Rs.100
Agnipatham Abdul Kalam Atmakatha By A P J Abdul Kalam Rs.90
Margadarshakulu By A P J Abdul Kalam Rs.80
Utthama Kutumbam Udaattha Desham By A P J Abdul Kalam Rs.250
Bharatadeshapu Shakthi By A P J Abdul Kalam Rs.99
Discussion:Transcedence My Spiritual Experiences With Pramukh Swamiji