### Nuprl Lemma : strict-majority-or-max_wf

`∀[L:ℤ List]. (strict-majority-or-max(L) ∈ ℤ)`

Proof

Definitions occuring in Statement :  strict-majority-or-max: `strict-majority-or-max(L)` list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` strict-majority-or-max: `strict-majority-or-max(L)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` subtype_rel: `A ⊆r B` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` prop: `ℙ` bfalse: `ff` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` or: `P ∨ Q` cons: `[a / b]` top: `Top` guard: `{T}` nat: `ℕ` le: `A ≤ B` decidable: `Dec(P)` subtract: `n - m` less_than': `less_than'(a;b)` true: `True`
Lemmas referenced :  null_wf bool_wf uiff_transitivity equal-wf-base list_subtype_base int_subtype_base assert_wf list_wf eqtt_to_assert assert_of_null strict-majority_wf int-deq_wf unit_wf2 equal_wf iff_transitivity bnot_wf not_wf iff_weakening_uiff eqff_to_assert assert_of_bnot imax-list_wf list-cases length_of_nil_lemma nil_wf product_subtype_list length_of_cons_lemma length_wf_nat nat_wf decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination baseApply closedConclusion baseClosed applyEquality independent_isectElimination independent_functionElimination because_Cache productElimination unionEquality equalityTransitivity equalitySymmetry natural_numberEquality dependent_functionElimination independent_pairFormation impliesFunctionality voidElimination promote_hyp hypothesis_subsumption isect_memberEquality voidEquality setElimination rename addEquality lambdaEquality minusEquality axiomEquality

Latex:
\mforall{}[L:\mBbbZ{}  List].  (strict-majority-or-max(L)  \mmember{}  \mBbbZ{})

Date html generated: 2019_06_20-PM-01_55_00
Last ObjectModification: 2018_08_21-PM-01_55_26

Theory : decidable!equality

Home Index