### Nuprl Lemma : round-robin-equal

`∀[L:Top List]. ∀[b:ℕ]. (round-robin(L) (b + ||L||) ~ round-robin(L) b) 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]` top: `Top` apply: `f a` add: `n + m` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` round-robin: `round-robin(L)` squash: `↓T` prop: `ℙ` nat: `ℕ` ge: `i ≥ j ` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` and: `P ∧ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` top: `Top` nat_plus: `ℕ+` nequal: `a ≠ b ∈ T ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_type: `SQType(T)`
Lemmas referenced :  subtype_base_sq int_subtype_base equal_wf squash_wf true_wf rem_rec_case length_wf top_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf less_than_wf intformeq_wf int_formula_prop_eq_lemma equal-wf-T-base iff_weakening_equal add-subtract-cancel nat_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis applyEquality lambdaEquality imageElimination hypothesisEquality equalityTransitivity equalitySymmetry universeEquality dependent_set_memberEquality addEquality setElimination rename dependent_functionElimination natural_numberEquality unionElimination productElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll because_Cache remainderEquality lambdaFormation baseClosed imageMemberEquality independent_functionElimination sqequalAxiom

Latex:
\mforall{}[L:Top  List].  \mforall{}[b:\mBbbN{}].  (round-robin(L)  (b  +  ||L||)  \msim{}  round-robin(L)  b)  supposing  0  <  ||L||

Date html generated: 2017_04_17-AM-09_15_26
Last ObjectModification: 2017_02_27-PM-05_21_08

Theory : decidable!equality

Home Index