### 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 x y) = 0 ∈ ℤ) ∧ (z = (f x 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: `T List` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = 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: `P `` 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 ⊆r B` iff: `P `⇐⇒` Q` has-value: `(a)↓` uimplies: `b supposing a` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` rev_implies: `P `` 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: `A c∧ B` nequal: `a ≠ b ∈ T ` subtract: `n - m` ge: `i ≥ j `
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