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))


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: List assert: b uimplies: supposing a uall: [x:A]. B[x] top: Top function: x:A ⟶ B[x] union: left right universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a squash: T prop: true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q top: Top so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] so_lambda: λ2y.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: c∧ B sq_type: SQType(T) assert: b ifthenelse: if then else fi  btrue: tt ge: i ≥  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

\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