Nuprl Lemma : mem_bsublist

s:DSet. ∀as:DisList{s}. ∀bs:|s| List.  (↑bsublist(s;as;bs) ⇐⇒ ∀c:|s|. ((↑(c ∈b as))  (↑(c ∈b bs))))


Proof




Definitions occuring in Statement :  bsublist: bsublist(s;as;bs) dislist: DisList{s} mem: a ∈b as list: List assert: b all: x:A. B[x] iff: ⇐⇒ Q implies:  Q dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T uall: [x:A]. B[x] dislist: DisList{s} prop: dset: DSet rev_implies:  Q gt: i > j decidable: Dec(P) or: P ∨ Q ge: i ≥  false: False le: A ≤ B uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top guard: {T} less_than: a < b squash: T
Lemmas referenced :  assert_wf mem_wf set_car_wf bsublist_wf list_wf dislist_wf dset_wf mem_bsublist_imp mem_iff_count_nzero gt_wf count_wf count_bsublist_a decidable__equal_int non_neg_length count_bounds decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermVar_wf itermConstant_wf intformeq_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_wf dislist_properties decidable__lt intformless_wf int_formula_prop_less_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt independent_pairFormation universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality setElimination rename hypothesis sqequalRule functionIsType because_Cache independent_functionElimination productElimination natural_numberEquality unionElimination equalityTransitivity equalitySymmetry independent_isectElimination approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination imageElimination

Latex:
\mforall{}s:DSet.  \mforall{}as:DisList\{s\}.  \mforall{}bs:|s|  List.
    (\muparrow{}bsublist(s;as;bs)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}c:|s|.  ((\muparrow{}(c  \mmember{}\msubb{}  as))  {}\mRightarrow{}  (\muparrow{}(c  \mmember{}\msubb{}  bs))))



Date html generated: 2019_10_16-PM-01_05_12
Last ObjectModification: 2018_10_08-AM-10_33_27

Theory : list_2


Home Index