Nuprl Lemma : round-robin-member

∀[T:Type]. ∀L:T List. ∀n:ℕ. (round-robin(L) n ∈ L) supposing 0 < ||L||

Proof

Definitions occuring in Statement : round-robin: round-robin(L), l_member: (x ∈ l), length: ||as||, list: T List, nat: ℕ, less_than: a < b, uimplies: b supposing a, uall: ∀[x:A]. B[x], all: ∀x:A. B[x], apply: f a, natural_number: $n, universe: Type
Definitions unfolded in proof : round-robin: round-robin(L), uall: ∀[x:A]. B[x], all: ∀x:A. B[x], uimplies: b supposing a, member: t ∈ T, int_seg: {i..j^-}, int_nzero: ℤ^-^o, nequal: a ≠ b ∈ T , nat: ℕ, ge: i ≥ j , not: ¬A, implies: P ⇒ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, top: Top, and: P ∧ Q, prop: ℙ, subtype_rel: A ⊆r B, so_lambda: λ₂x.t[x], so_apply: x[s], lelt: i ≤ j < k, nat_plus: ℕ⁺, decidable: Dec(P), or: P ∨ Q, less_than: a < b, squash: ↓T
Lemmas referenced : member-less_than, length_wf, select_member, remainder_wfa, nat_properties, full-omega-unsat, intformand_wf, intformeq_wf, itermVar_wf, itermConstant_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_eq_lemma, int_term_value_var_lemma, int_term_value_constant_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, length_wf_nat, set_subtype_base, le_wf, int_subtype_base, nequal_wf, rem_bounds_1, decidable__lt, intformnot_wf, int_formula_prop_not_lemma, istype-less_than, istype-le, istype-nat, list_wf, istype-universe
Rules used in proof : sqequalSubstitution, sqequalRule, sqequalReflexivity, sqequalTransitivity, computationStep, Error :isect_memberFormation_alt, Error :lambdaFormation_alt, cut, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, natural_numberEquality, hypothesisEquality, hypothesis, independent_isectElimination, rename, dependent_functionElimination, Error :dependent_set_memberEquality_alt, because_Cache, setElimination, equalityTransitivity, equalitySymmetry, approximateComputation, independent_functionElimination, Error :dependent_pairFormation_alt, Error :lambdaEquality_alt, int_eqEquality, Error :isect_memberEquality_alt, voidElimination, independent_pairFormation, Error :universeIsType, Error :equalityIstype, Error :inhabitedIsType, applyEquality, intEquality, baseClosed, sqequalBase, unionElimination, imageElimination, productElimination, Error :productIsType, instantiate

Latex:
\mforall{}[T:Type]. \mforall{}L:T List. \mforall{}n:\mBbbN{}. (round-robin(L) n \mmember{} L) supposing 0 < ||L|| Date html generated: 2019_06_20-PM-01_56_44 Last ObjectModification: 2019_03_06-AM-10_52_15 Theory : decidable!equality Home Index