### Nuprl Lemma : comparison-max_wf

[T:Type]. ∀[cmp:comparison(T)].  ∀L:T List+(comparison-max(cmp;L) ∈ {mx:T| (mx ∈ L) ∧ (∀x∈L.0 ≤ (cmp mx))} suppos\000Cing valueall-type(T)

Proof

Definitions occuring in Statement :  comparison-max: comparison-max(cmp;L) comparison: comparison(T) l_all: (∀x∈L.P[x]) l_member: (x ∈ l) listp: List+ valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] and: P ∧ Q member: t ∈ T set: {x:A| B[x]}  apply: a natural_number: \$n universe: Type
Definitions unfolded in proof :  connex: Connex(T;x,y.R[x; y]) sq_stable: SqStable(P) rev_implies:  Q iff: ⇐⇒ Q has-valueall: has-valueall(a) has-value: (a)↓ callbyvalueall: callbyvalueall assert: b bnot: ¬bb bfalse: ff ifthenelse: if then else fi  uiff: uiff(P;Q) btrue: tt unit: Unit bool: 𝔹 refl: Refl(T;x,y.E[x; y]) comparison: comparison(T) cand: c∧ B squash: T less_than: a < b sq_type: SQType(T) so_apply: x[s] so_lambda: λ2x.t[x] it: nil: [] decidable: Dec(P) so_apply: x[s1;s2] so_lambda: λ2y.t[x; y] colength: colength(L) so_apply: x[s1;s2;s3] so_lambda: so_lambda(x,y,z.t[x; y; z]) eager-accum: eager-accum(x,a.f[x; a];y;l) guard: {T} prop: exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) nat: subtype_rel: A ⊆B top: Top comparison-max: comparison-max(cmp;L) false: False implies:  Q not: ¬A true: True less_than': less_than'(a;b) and: P ∧ Q le: A ≤ B ge: i ≥  cons: [a b] or: P ∨ Q listp: List+ all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  comparison-connex sq_stable__le assert_of_bnot iff_weakening_uiff iff_transitivity bool_cases l_all_cons cons_member not_wf bnot_wf assert_wf cons_wf l_all_wf ifthenelse_wf evalall-reduce assert-bnot bool_subtype_base bool_cases_sqequal eqff_to_assert valueall-type-has-valueall assert_of_le_int eqtt_to_assert bool_wf le_int_wf l_all_wf_nil or_wf l_all_nil nil_wf l_member_wf comparison-refl list_ind_cons_lemma decidable__equal_int int_subtype_base set_subtype_base subtype_base_sq int_term_value_subtract_lemma itermSubtract_wf subtract_wf equal_wf le_wf int_formula_prop_not_lemma intformnot_wf decidable__le int_term_value_add_lemma int_formula_prop_eq_lemma itermAdd_wf intformeq_wf spread_cons_lemma list_ind_nil_lemma list_wf less_than_irreflexivity less_than_transitivity1 colength_wf_list nat_wf equal-wf-T-base less_than_wf ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf satisfiable-full-omega-tt nat_properties reduce_tl_cons_lemma reduce_hd_cons_lemma length_of_nil_lemma comparison_wf valueall-type_wf listp_wf product_subtype_list list-cases listp_properties
Rules used in proof :  imageMemberEquality impliesFunctionality inrFormation setEquality callbyvalueReduce equalityElimination functionExtensionality productEquality inlFormation imageElimination instantiate baseClosed addEquality dependent_set_memberEquality applyLambdaEquality computeAll independent_pairFormation intEquality int_eqEquality dependent_pairFormation independent_isectElimination intWeakElimination applyEquality voidEquality voidElimination natural_numberEquality independent_functionElimination universeEquality isect_memberEquality because_Cache equalitySymmetry equalityTransitivity axiomEquality lambdaEquality cumulativity sqequalRule productElimination hypothesis_subsumption promote_hyp unionElimination dependent_functionElimination rename setElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[cmp:comparison(T)].
\mforall{}L:T  List\msupplus{}.  (comparison-max(cmp;L)  \mmember{}  \{mx:T|  (mx  \mmember{}  L)  \mwedge{}  (\mforall{}x\mmember{}L.0  \mleq{}  (cmp  x  mx))\}  )  supposing  valueall\000C-type(T)

Date html generated: 2017_04_17-AM-08_31_42
Last ObjectModification: 2017_03_30-PM-03_44_51

Theory : list_1

Home Index