### Nuprl Lemma : length-list-diff

`∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List.  ((||as-bs|| ≤ ||as||) ∧ ||as-bs|| < ||as|| supposing (∃a∈as. (a ∈ bs)))`

Proof

Definitions occuring in Statement :  list-diff: `as-bs` l_exists: `(∃x∈L. P[x])` l_member: `(x ∈ l)` length: `||as||` list: `T List` deq: `EqDecider(T)` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  list-diff: `as-bs` uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` le: `A ≤ B` not: `¬A` implies: `P `` Q` false: `False` iff: `P `⇐⇒` Q` exists: `∃x:A. B[x]` l_member: `(x ∈ l)` l_exists: `(∃x∈L. P[x])` nat: `ℕ` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` less_than: `a < b` squash: `↓T` rev_implies: `P `` Q`
Lemmas referenced :  length-filter bnot_wf deq-member_wf l_exists_wf l_member_wf list_wf deq_wf less_than'_wf length_wf filter_wf5 member-less_than length-filter-decreases l_exists_iff lelt_wf not_wf assert_wf select_wf int_seg_properties 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 decidable__lt intformless_wf int_formula_prop_less_lemma false_wf iff_transitivity iff_weakening_uiff assert_of_bnot assert-deq-member
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality cumulativity hypothesis independent_pairFormation setElimination rename setEquality dependent_functionElimination productElimination independent_pairEquality voidElimination because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality independent_isectElimination universeEquality independent_functionElimination dependent_pairFormation dependent_set_memberEquality hyp_replacement Error :applyLambdaEquality,  natural_numberEquality unionElimination int_eqEquality intEquality voidEquality computeAll imageElimination functionEquality addLevel impliesFunctionality

Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.
((||as-bs||  \mleq{}  ||as||)  \mwedge{}  ||as-bs||  <  ||as||  supposing  (\mexists{}a\mmember{}as.  (a  \mmember{}  bs)))

Date html generated: 2016_10_21-AM-10_42_47
Last ObjectModification: 2016_07_12-AM-05_50_28

Theory : decidable!equality

Home Index