### Nuprl Lemma : finite-double-negation-shift-extract

`∀[A:ℙ]. ∀[B:ℕ ⟶ ℙ].  ∀n:ℕ. ((∀i:ℕn. (((B i) `` A) `` A)) `` ((∀i:ℕn. (B i)) `` A) `` A)`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  member: `t ∈ T` finite-double-negation-shift natrec: natrec genrec: genrec so_apply: `x[s1;s2]` decidable__equal_int decidable__int_equal 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.t[x]` top: `Top` so_apply: `x[s]` uimplies: `b supposing a` strict4: `strict4(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` guard: `{T}` or: `P ∨ Q` squash: `↓T` any: `any x` subtract: `n - m` so_lambda: `λ2x y.t[x; y]` iff_weakening_equal genrec-ap: genrec-ap
Lemmas referenced :  finite-double-negation-shift lifting-strict-int_eq top_wf equal_wf has-value_wf_base base_wf is-exception_wf lifting-strict-spread decidable__equal_int decidable__int_equal iff_weakening_equal
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution isectElimination baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueDecide hypothesisEquality equalityTransitivity equalitySymmetry unionEquality unionElimination sqleReflexivity dependent_functionElimination independent_functionElimination baseApply closedConclusion decideExceptionCases inrFormation because_Cache imageMemberEquality imageElimination exceptionSqequal inlFormation callbyvalueApply applyExceptionCases

Latex:
\mforall{}[A:\mBbbP{}].  \mforall{}[B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].    \mforall{}n:\mBbbN{}.  ((\mforall{}i:\mBbbN{}n.  (((B  i)  {}\mRightarrow{}  A)  {}\mRightarrow{}  A))  {}\mRightarrow{}  ((\mforall{}i:\mBbbN{}n.  (B  i))  {}\mRightarrow{}  A)  {}\mRightarrow{}  A)

Date html generated: 2017_10_01-AM-09_10_26
Last ObjectModification: 2017_07_26-PM-04_46_57

Theory : general

Home Index