Nuprl Lemma : sbcode-mul

[m,n,k:ℕ+].  (sbcode(k m;k n) sbcode(m;n))


Proof




Definitions occuring in Statement :  sbcode: sbcode(m;n) nat_plus: + uall: [x:A]. B[x] multiply: m sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A top: Top and: P ∧ Q prop: guard: {T} int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) so_lambda: λ2x.t[x] so_apply: x[s] sbcode: sbcode(m;n) sq_type: SQType(T) less_than: a < b nat_plus: + bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) true: True squash: T bfalse: ff bnot: ¬bb ifthenelse: if then else fi  assert: b
Lemmas referenced :  nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf 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 less_than_wf nat_plus_wf nat_wf int_seg_wf int_seg_properties decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma decidable__equal_int int_seg_subtype false_wf intformeq_wf int_formula_prop_eq_lemma le_wf subtype_base_sq list_wf list_subtype_base set_subtype_base lelt_wf int_subtype_base decidable__lt itermAdd_wf int_term_value_add_lemma nat_plus_subtype_nat nat_plus_properties sbcode_wf lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot cons_wf squash_wf true_wf itermMultiply_wf int_term_value_mul_lemma mul_preserves_le mul_preserves_lt nil_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction thin lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll independent_functionElimination sqequalAxiom because_Cache productElimination unionElimination applyEquality equalityTransitivity equalitySymmetry applyLambdaEquality hypothesis_subsumption dependent_set_memberEquality instantiate cumulativity addEquality multiplyEquality equalityElimination lessCases imageMemberEquality baseClosed imageElimination promote_hyp universeEquality

Latex:
\mforall{}[m,n,k:\mBbbN{}\msupplus{}].    (sbcode(k  *  m;k  *  n)  \msim{}  sbcode(m;n))



Date html generated: 2018_05_21-PM-11_39_50
Last ObjectModification: 2017_07_26-PM-06_42_48

Theory : rationals


Home Index