Nuprl Lemma : decidable-cantor-to-int-ext

`∀[R:ℤ ⟶ ℤ ⟶ ℙ]. ((∀x,y:ℤ.  Dec(R[x;y])) `` (∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. Dec(∃f,g:ℕ ⟶ 𝔹. R[F f;F g])))`

Proof

Definitions occuring in Statement :  nat: `ℕ` bool: `𝔹` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  member: `t ∈ T` bfalse: `ff` it: `⋅` btrue: `tt` subtract: `n - m` ifthenelse: `if b then t else f fi ` let: let lt_int: `i <z j` so_lambda: `λ2x.t[x]` spreadn: spread3 decidable-cantor-to-int cantor-to-int-uniform-continuity decidable-finite-cantor-to-int uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` uimplies: `b supposing a` so_apply: `x[s]`
Lemmas referenced :  decidable-cantor-to-int lifting-strict-spread istype-void strict4-spread lifting-strict-callbyvalue lifting-strict-less strict4-decide cantor-to-int-uniform-continuity decidable-finite-cantor-to-int
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination

Latex:
\mforall{}[R:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x,y:\mBbbZ{}.    Dec(R[x;y]))  {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbZ{}.  Dec(\mexists{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  R[F  f;F  g])))

Date html generated: 2019_10_15-AM-10_26_38
Last ObjectModification: 2019_08_05-PM-02_14_27

Theory : continuity

Home Index