### Nuprl Lemma : decidable__l_all

`∀[A:Type]. ∀L:A List. ∀[F:{a:A| (a ∈ L)}  ⟶ ℙ]. ((∀k:{a:A| (a ∈ L)} . Dec(F[k])) `` Dec((∀k∈L.F[k])))`

Proof

Definitions occuring in Statement :  l_all: `(∀x∈L.P[x])` l_member: `(x ∈ l)` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  l-all-decider: `l-all-decider()` ifthenelse: `if b then t else f fi ` genrec-ap: genrec-ap it: `⋅` any: `any x` decidable__false decidable__implies decidable__not int_seg_decide: `int_seg_decide(d;i;j)` squash: `↓T` or: `P ∨ Q` guard: `{T}` prop: `ℙ` has-value: `(a)↓` implies: `P `` Q` all: `∀x:A. B[x]` and: `P ∧ Q` strict4: `strict4(F)` uimplies: `b supposing a` so_apply: `x[s]` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2;s3;s4]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` uall: `∀[x:A]. B[x]` decidable__exists_int_seg decidable__all_int_seg decidable__l_all-proof member: `t ∈ T`
Lemmas referenced :  lifting-strict-decide is-exception_wf base_wf has-value_wf_base equal_wf top_wf lifting-strict-callbyvalue decidable__l_all-proof decidable__false decidable__implies decidable__not decidable__exists_int_seg decidable__all_int_seg
Rules used in proof :  inlFormation exceptionSqequal imageElimination imageMemberEquality because_Cache inrFormation decideExceptionCases closedConclusion baseApply independent_functionElimination dependent_functionElimination sqleReflexivity unionElimination unionEquality equalitySymmetry equalityTransitivity hypothesisEquality callbyvalueDecide lambdaFormation independent_pairFormation independent_isectElimination voidEquality voidElimination isect_memberEquality baseClosed isectElimination sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

Latex:
\mforall{}[A:Type].  \mforall{}L:A  List.  \mforall{}[F:\{a:A|  (a  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}k:\{a:A|  (a  \mmember{}  L)\}  .  Dec(F[k]))  {}\mRightarrow{}  Dec((\mforall{}k\mmember{}L.F[k])\000C))

Date html generated: 2018_05_21-PM-00_35_36
Last ObjectModification: 2018_05_18-PM-04_17_57

Theory : list_1

Home Index