Nuprl Lemma : from-upto-split

[n,m,k:ℤ].  ([n, m) [n, k) [k, m)) supposing ((k ≤ m) and (n ≤ k))


Definitions occuring in Statement :  from-upto: [n, m) append: as bs uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B int: sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T 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: decidable: Dec(P) or: P ∨ Q uiff: uiff(P;Q) append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] from-upto: [n, m) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b has-value: (a)↓
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 le_wf subtract_wf decidable__le intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma nat_wf from-upto-is-nil list_ind_nil_lemma lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot list_ind_cons_lemma value-type-has-value int-value-type itermAdd_wf int_term_value_add_lemma int_subtype_base decidable__equal_int intformeq_wf int_formula_prop_eq_lemma
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation introduction extract_by_obid sqequalHypSubstitution isectElimination thin 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 comment unionElimination because_Cache productElimination equalityElimination equalityTransitivity equalitySymmetry promote_hyp instantiate cumulativity addEquality callbyvalueReduce isect_memberFormation dependent_set_memberEquality

\mforall{}[n,m,k:\mBbbZ{}].    ([n,  m)  \msim{}  [n,  k)  @  [k,  m))  supposing  ((k  \mleq{}  m)  and  (n  \mleq{}  k))

Date html generated: 2017_04_17-AM-07_53_55
Last ObjectModification: 2017_02_27-PM-04_27_18

Theory : list_1

Home Index