### Nuprl Lemma : l_disjoint_from-upto

`∀[L:ℤ List]. ∀n1:ℤ. ∀[n2:ℤ]. uiff(∀x:ℤ. ((x ∈ L) `` (x < n1 ∨ (x ≥ n2 )));l_disjoint(ℤ;L;[n1, n2)))`

Proof

Definitions occuring in Statement :  from-upto: `[n, m)` l_disjoint: `l_disjoint(T;l1;l2)` l_member: `(x ∈ l)` list: `T List` less_than: `a < b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` ge: `i ≥ j ` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` l_disjoint: `l_disjoint(T;l1;l2)` not: `¬A` implies: `P `` Q` false: `False` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` or: `P ∨ Q` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` decidable: `Dec(P)` iff: `P `⇐⇒` Q` rev_uimplies: `rev_uimplies(P;Q)` guard: `{T}` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  sq_stable__le int_formula_prop_not_lemma intformnot_wf decidable__lt decidable__le not_wf not_over_and int_formula_prop_wf int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf itermVar_wf intformless_wf intformand_wf satisfiable-full-omega-tt from-upto-member list_wf l_disjoint_wf ge_wf or_wf all_wf less_than_wf le_wf subtype_rel_list from-upto_wf l_member_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation introduction cut sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination lemma_by_obid isectElimination intEquality hypothesis applyEquality setEquality because_Cache independent_isectElimination setElimination rename functionEquality productElimination independent_functionElimination unionElimination natural_numberEquality dependent_pairFormation int_eqEquality isect_memberEquality voidEquality computeAll inlFormation inrFormation imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}n1:\mBbbZ{}.  \mforall{}[n2:\mBbbZ{}].  uiff(\mforall{}x:\mBbbZ{}.  ((x  \mmember{}  L)  {}\mRightarrow{}  (x  <  n1  \mvee{}  (x  \mgeq{}  n2  )));l\_disjoint(\mBbbZ{};L;[n1,  n2)))

Date html generated: 2016_05_14-PM-02_01_50
Last ObjectModification: 2016_01_15-AM-08_08_55

Theory : list_1

Home Index