Nuprl Lemma : member-insert-combine

T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x,z:T. ∀v:T List.
  ((z ∈ insert-combine(cmp;f;x;v))  ((z ∈ v) ∨ (z x ∈ T) ∨ (∃y∈v. ((cmp y) 0 ∈ ℤ) ∧ (z (f y) ∈ T))))


Proof




Definitions occuring in Statement :  insert-combine: insert-combine(cmp;f;x;l) comparison: comparison(T) l_exists: (∃x∈L. P[x]) l_member: (x ∈ l) list: List all: x:A. B[x] implies:  Q or: P ∨ Q and: P ∧ Q apply: a function: x:A ⟶ B[x] natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: and: P ∧ Q comparison: comparison(T) so_apply: x[s] or: P ∨ Q insert-combine: insert-combine(cmp;f;x;l) so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3] guard: {T} subtype_rel: A ⊆B iff: ⇐⇒ Q has-value: (a)↓ uimplies: supposing a bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  rev_implies:  Q bfalse: ff exists: x:A. B[x] sq_type: SQType(T) bnot: ¬bb assert: b false: False not: ¬A l_exists: (∃x∈L. P[x]) int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) nat_plus: + less_than: a < b squash: T true: True decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) cand: c∧ B nequal: a ≠ b ∈  subtract: m ge: i ≥ 
Lemmas referenced :  list_induction l_member_wf insert-combine_wf or_wf equal_wf l_exists_wf equal-wf-T-base list_wf list_ind_nil_lemma list_ind_cons_lemma comparison_wf l_exists_wf_nil and_wf nil_wf member_singleton cons_wf value-type-has-value int-value-type eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int cons_member eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int lt_int_wf assert_of_lt_int less_than_wf length_of_cons_lemma false_wf add_nat_plus length_wf_nat nat_plus_wf nat_plus_properties decidable__lt add-is-int-iff satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf lelt_wf length_wf select-cons-hd select_wf int_seg_properties decidable__le intformle_wf int_formula_prop_le_lemma add-member-int_seg2 subtract_wf itermSubtract_wf int_term_value_subtract_lemma non_neg_length select-cons-tl add-subtract-cancel
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination because_Cache sqequalRule lambdaEquality functionEquality cumulativity hypothesisEquality dependent_functionElimination functionExtensionality applyEquality hypothesis setElimination rename productEquality intEquality baseClosed setEquality independent_functionElimination isect_memberEquality voidElimination voidEquality universeEquality inrFormation inlFormation addLevel impliesFunctionality productElimination callbyvalueReduce independent_isectElimination natural_numberEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp instantiate hyp_replacement applyLambdaEquality dependent_set_memberEquality independent_pairFormation imageMemberEquality pointwiseFunctionality baseApply closedConclusion int_eqEquality computeAll addEquality imageElimination

Latex:
\mforall{}T:Type.  \mforall{}cmp:comparison(T).  \mforall{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T.  \mforall{}x,z:T.  \mforall{}v:T  List.
    ((z  \mmember{}  insert-combine(cmp;f;x;v))  {}\mRightarrow{}  ((z  \mmember{}  v)  \mvee{}  (z  =  x)  \mvee{}  (\mexists{}y\mmember{}v.  ((cmp  x  y)  =  0)  \mwedge{}  (z  =  (f  x  y)))))



Date html generated: 2017_04_17-AM-08_29_04
Last ObjectModification: 2017_02_27-PM-04_50_55

Theory : list_1


Home Index