Nuprl Lemma : from-upto-member-nat

n,m,k:ℕ.  uiff((k ∈ [n, m));(n ≤ k) ∧ k < m)


Proof




Definitions occuring in Statement :  from-upto: [n, m) l_member: (x ∈ l) nat: less_than: a < b uiff: uiff(P;Q) le: A ≤ B all: x:A. B[x] and: P ∧ Q
Definitions unfolded in proof :  all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T le: A ≤ B not: ¬A implies:  Q false: False uall: [x:A]. B[x] nat: prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top l_member: (x ∈ l) sq_type: SQType(T) guard: {T} ifthenelse: if then else fi  btrue: tt iff: ⇐⇒ Q rev_implies:  Q bfalse: ff int_seg: {i..j-} lelt: i ≤ j < k bool: 𝔹 unit: Unit it: bnot: ¬bb assert: b squash: T sq_stable: SqStable(P)
Lemmas referenced :  less_than'_wf member-less_than l_member_wf nat_wf from-upto_wf subtype_rel_list le_wf less_than_wf subtype_rel_sets nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf length-from-upto lt_int_wf assert_wf bnot_wf not_wf bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert_of_lt_int eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot select-from-upto lelt_wf subtract_wf intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma decidable__lt intformless_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_subtract_lemma equal_wf bool_cases_sqequal assert-bnot decidable__equal_int length_wf select_wf sq_stable__and sq_stable__le sq_stable__less_than squash_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality voidElimination extract_by_obid isectElimination setElimination rename hypothesis axiomEquality equalityTransitivity equalitySymmetry independent_isectElimination applyEquality setEquality intEquality productEquality because_Cache natural_numberEquality unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidEquality computeAll instantiate cumulativity independent_functionElimination impliesFunctionality dependent_set_memberEquality applyLambdaEquality equalityElimination promote_hyp addEquality imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}n,m,k:\mBbbN{}.    uiff((k  \mmember{}  [n,  m));(n  \mleq{}  k)  \mwedge{}  k  <  m)



Date html generated: 2017_04_17-AM-07_55_39
Last ObjectModification: 2017_02_27-PM-04_28_41

Theory : list_1


Home Index