### Nuprl Lemma : round-robin_wf

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

Proof

Definitions occuring in Statement :  round-robin: `round-robin(L)` length: `||as||` list: `T List` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` round-robin: `round-robin(L)` nat: `ℕ` nequal: `a ≠ b ∈ T ` ge: `i ≥ j ` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` nat_plus: `ℕ+`
Lemmas referenced :  list_wf nat_wf less_than_wf rem_bounds_1 equal_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformand_wf satisfiable-full-omega-tt nat_properties length_wf select_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality remainderEquality setElimination rename hypothesis because_Cache lambdaFormation equalityTransitivity equalitySymmetry natural_numberEquality independent_isectElimination dependent_pairFormation int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll dependent_set_memberEquality productElimination axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    round-robin(L)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  T  supposing  0  <  ||L||

Date html generated: 2016_05_14-PM-03_30_48
Last ObjectModification: 2016_01_14-PM-11_20_54

Theory : decidable!equality

Home Index