### Nuprl Lemma : do-apply-p-first-disjoint

`∀[A,B:Type]. ∀[L:(A ⟶ (B + Top)) List]. ∀[x:A].`
`  ∀[f:A ⟶ (B + Top)]. (do-apply(p-first(L);x) = do-apply(f;x) ∈ B) supposing ((↑can-apply(f;x)) and (f ∈ L)) `
`  supposing (∀f,g∈L.  p-disjoint(A;f;g))`

Proof

Definitions occuring in Statement :  p-disjoint: `p-disjoint(A;f;g)` p-first: `p-first(L)` do-apply: `do-apply(f;x)` can-apply: `can-apply(f;x)` pairwise: `(∀x,y∈L.  P[x; y])` l_member: `(x ∈ l)` list: `T List` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` top: `Top` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` l_exists: `(∃x∈L. P[x])` nat: `ℕ` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` cand: `A c∧ B` sq_type: `SQType(T)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` less_than: `a < b` cons: `[a / b]` colength: `colength(L)` nil: `[]` it: `⋅` less_than': `less_than'(a;b)` pairwise: `(∀x,y∈L.  P[x; y])` select: `L[n]` bool: `𝔹` unit: `Unit` uiff: `uiff(P;Q)` bfalse: `ff` p-disjoint: `p-disjoint(A;f;g)`
Lemmas referenced :  equal_wf squash_wf true_wf do-apply-p-first do-apply_wf iff_weakening_equal assert_wf can-apply_wf subtype_rel_union top_wf l_member_wf pairwise_wf2 subtype_rel_list subtype_rel_dep_function p-disjoint_wf list_wf can-apply-p-first lelt_wf length_wf and_wf assert_elim subtype_base_sq bool_wf bool_subtype_base select_wf int_seg_properties nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma ge_wf less_than_wf less_than_transitivity1 less_than_irreflexivity equal-wf-T-base nat_wf colength_wf_list list-cases product_subtype_list spread_cons_lemma intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma le_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma set_subtype_base int_subtype_base decidable__equal_int length_of_nil_lemma stuck-spread base_wf filter_nil_lemma null_nil_lemma btrue_wf member-implies-null-eq-bfalse nil_wf btrue_neq_bfalse all_wf int_seg_wf cons_wf filter_cons_lemma bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot reduce_hd_cons_lemma false_wf length_of_cons_lemma pairwise-cons cons_member not_assert_elim
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache independent_isectElimination cumulativity functionExtensionality natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality productElimination independent_functionElimination isect_memberEquality voidElimination voidEquality axiomEquality functionEquality unionEquality instantiate lambdaFormation dependent_functionElimination dependent_pairFormation setElimination rename dependent_set_memberEquality independent_pairFormation applyLambdaEquality unionElimination int_eqEquality intEquality computeAll intWeakElimination promote_hyp hypothesis_subsumption addEquality equalityElimination hyp_replacement addLevel levelHypothesis

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:(A  {}\mrightarrow{}  (B  +  Top))  List].  \mforall{}[x:A].
\mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)]
(do-apply(p-first(L);x)  =  do-apply(f;x))  supposing  ((\muparrow{}can-apply(f;x))  and  (f  \mmember{}  L))
supposing  (\mforall{}f,g\mmember{}L.    p-disjoint(A;f;g))

Date html generated: 2018_05_21-PM-06_50_10
Last ObjectModification: 2017_07_26-PM-04_57_18

Theory : general

Home Index