### Nuprl Lemma : combinations_aux_rem_property

[k:ℕ+]. ∀[n,b,m:ℕ].  (combinations_aux_rem(b rem k;n;m;k) (combinations_aux(b;n;m) rem k) ∈ ℤ)

Proof

Definitions occuring in Statement :  combinations_aux_rem: combinations_aux_rem(b;n;m;k) combinations_aux: combinations_aux(b;n;m) nat_plus: + nat: uall: [x:A]. B[x] remainder: rem m int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] all: x:A. B[x] and: P ∧ Q prop: combinations_aux_rem: combinations_aux_rem(b;n;m;k) combinations_aux: combinations_aux(b;n;m) eq_int: (i =z j) subtract: m ifthenelse: if then else fi  btrue: tt subtype_rel: A ⊆B nat_plus: + has-value: (a)↓ bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) bfalse: ff iff: ⇐⇒ Q rev_implies:  Q decidable: Dec(P) or: P ∨ Q sq_type: SQType(T) guard: {T} nequal: a ≠ b ∈  top: Top int_nzero: -o so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B true: True squash: T
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than remainder_wfa nat_plus_inc_int_nzero subtract-1-ge-0 istype-nat nat_plus_wf eq_int_wf equal-wf-base bool_wf int_subtype_base assert_wf nat_plus_properties intformeq_wf int_formula_prop_eq_lemma bnot_wf not_wf istype-assert istype-void value-type-has-value int-value-type subtract_wf uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot decidable__equal_int subtype_base_sq mul-zero satisfiable-full-omega-tt zero-rem subtype_rel_sets less_than_wf nequal_wf add-commutes zero-mul iff_weakening_equal subtype_rel_self rem-zero istype-universe true_wf squash_wf equal_wf decidable__le intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma le_wf rem_mul2 mul_bounds_1a combinations_aux_wf_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation_alt natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination Error :memTop,  sqequalRule independent_pairFormation universeIsType voidElimination isect_memberEquality_alt axiomEquality isectIsTypeImplies inhabitedIsType functionIsTypeImplies callbyvalueReduce sqleReflexivity applyEquality because_Cache equalityTransitivity equalitySymmetry baseApply closedConclusion baseClosed equalityIstype sqequalBase functionIsType multiplyEquality unionElimination equalityElimination productElimination instantiate cumulativity intEquality remainderEquality lambdaFormation dependent_pairFormation lambdaEquality isect_memberEquality voidEquality computeAll setEquality applyLambdaEquality independent_pairEquality imageMemberEquality universeEquality imageElimination dependent_set_memberEquality

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[n,b,m:\mBbbN{}].    (combinations\_aux\_rem(b  rem  k;n;m;k)  =  (combinations\_aux(b;n;m)  rem  k))

Date html generated: 2020_05_20-AM-08_13_05
Last ObjectModification: 2020_02_28-PM-02_51_06

Theory : general

Home Index