### Nuprl Lemma : round-robin-onto

`∀[T:Type]. ∀L:T List. (∀x∈L.∃b:ℕ. (x = (round-robin(L) b) ∈ T))`

Proof

Definitions occuring in Statement :  round-robin: `round-robin(L)` l_all: `(∀x∈L.P[x])` list: `T List` nat: `ℕ` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` l_all: `(∀x∈L.P[x])` member: `t ∈ T` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` round-robin: `round-robin(L)` squash: `↓T` prop: `ℙ` int_seg: `{i..j-}` nat_plus: `ℕ+` lelt: `i ≤ j < k` less_than: `a < b` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cand: `A c∧ B` nat: `ℕ` ge: `i ≥ j `
Lemmas referenced :  int_seg_wf length_wf list_wf istype-universe int_seg_subtype_nat istype-false select_wf squash_wf le_wf less_than_wf istype-int equal_wf true_wf rem_base_case int_seg_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformle_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-less_than subtype_rel_self iff_weakening_equal decidable__le nat_properties round-robin_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesisEquality hypothesis instantiate universeEquality Error :dependent_pairFormation_alt,  applyEquality independent_isectElimination sqequalRule independent_pairFormation Error :lambdaEquality_alt,  imageElimination productElimination equalityTransitivity equalitySymmetry productEquality Error :inhabitedIsType,  because_Cache intEquality setElimination rename Error :dependent_set_memberEquality_alt,  dependent_functionElimination unionElimination approximateComputation independent_functionElimination int_eqEquality Error :isect_memberEquality_alt,  voidElimination imageMemberEquality baseClosed Error :equalityIstype

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  (\mforall{}x\mmember{}L.\mexists{}b:\mBbbN{}.  (x  =  (round-robin(L)  b)))

Date html generated: 2019_06_20-PM-01_56_49
Last ObjectModification: 2019_03_06-AM-10_52_42

Theory : decidable!equality

Home Index