### Nuprl Lemma : can-apply-p-first

`∀[A,B:Type].  ∀L:(A ⟶ (B + Top)) List. ∀x:A.  (↑can-apply(p-first(L);x) `⇐⇒` (∃f∈L. ↑can-apply(f;x)))`

Proof

Definitions occuring in Statement :  p-first: `p-first(L)` can-apply: `can-apply(f;x)` l_exists: `(∃x∈L. P[x])` list: `T List` assert: `↑b` uall: `∀[x:A]. B[x]` top: `Top` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` so_apply: `x[s]` top: `Top` prop: `ℙ` implies: `P `` Q` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` and: `P ∧ Q` false: `False` rev_implies: `P `` Q` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` or: `P ∨ Q` squash: `↓T` true: `True` guard: `{T}` uiff: `uiff(P;Q)`
Lemmas referenced :  p-first-singleton p-first-append true_wf squash_wf append_wf l_exists_append l_exists_cons p-conditional-to-p-first assert_functionality_wrt_uiff or_wf p-conditional_wf nil_wf cons_wf p-conditional-domain list_ind_nil_lemma list_ind_cons_lemma l_exists_wf_nil l_exists_nil false_wf p_first_nil_lemma list_wf l_member_wf l_exists_wf subtype_rel_union subtype_rel_dep_function subtype_rel_list p-first_wf can-apply_wf assert_wf iff_wf all_wf top_wf list_induction
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin lemma_by_obid sqequalHypSubstitution isectElimination functionEquality hypothesisEquality unionEquality hypothesis sqequalRule lambdaEquality cumulativity because_Cache applyEquality independent_isectElimination isect_memberEquality voidElimination voidEquality setElimination rename setEquality independent_functionElimination dependent_functionElimination universeEquality introduction independent_pairFormation productElimination independent_pairEquality addLevel allFunctionality impliesFunctionality imageElimination equalitySymmetry natural_numberEquality imageMemberEquality baseClosed orFunctionality equalityTransitivity unionElimination inlFormation inrFormation

Latex:
\mforall{}[A,B:Type].
\mforall{}L:(A  {}\mrightarrow{}  (B  +  Top))  List.  \mforall{}x:A.    (\muparrow{}can-apply(p-first(L);x)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}f\mmember{}L.  \muparrow{}can-apply(f;x)))

Date html generated: 2016_05_15-PM-03_45_17
Last ObjectModification: 2016_01_16-AM-10_56_40

Theory : general

Home Index