### Nuprl Lemma : decidable__l_exists

`∀[A:Type]. ∀[F:A ⟶ ℙ].  ∀L:A List. ((∀k:A. Dec(F[k])) `` Dec((∃k∈L. F[k])))`

Proof

Definitions occuring in Statement :  l_exists: `(∃x∈L. P[x])` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` int_seg_decide: `int_seg_decide(d;i;j)` it: `⋅` genrec-ap: genrec-ap l-exists-decider: `l-exists-decider()` decidable__l_exists-proof decidable__exists_int_seg
Lemmas referenced :  decidable__l_exists-proof decidable__exists_int_seg
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

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

Date html generated: 2018_05_21-PM-00_35_50
Last ObjectModification: 2018_05_19-AM-06_43_13

Theory : list_1

Home Index