### Nuprl Lemma : decidable__all-list

`∀[T:Type]`
`  ((∀x,y:T.  Dec(x = y ∈ T))`
`  `` (∀L:T List. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ]. ((∀x:{x:T| (x ∈ L)} . Dec(P[x])) `` Dec(∀x:{x:T| (x ∈ L)} . P[x]))))`

Proof

Definitions occuring in Statement :  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` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` sq_stable: `SqStable(P)` squash: `↓T` subtype_rel: `A ⊆r B` guard: `{T}`
Lemmas referenced :  decidable__l_all decidable_functionality iff_wf l_all_wf l_all_iff set_wf sq_stable__l_member equal_wf list_wf decidable_wf l_member_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality functionEquality cumulativity universeEquality independent_pairFormation dependent_functionElimination setElimination rename independent_functionElimination because_Cache introduction imageMemberEquality baseClosed imageElimination dependent_set_memberEquality addLevel productElimination impliesFunctionality

Latex:
\mforall{}[T:Type]
((\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}L:T  List
\mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  Dec(P[x]))  {}\mRightarrow{}  Dec(\mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  P[x])\000C)))

Date html generated: 2016_05_14-PM-03_31_48
Last ObjectModification: 2016_01_14-PM-11_20_26

Theory : decidable!equality

Home Index