Nuprl Lemma : length-eq-lists-diff-elts

`∀[T:Type]`
`  ∀eq:∀x,y:T.  Dec(x = y ∈ T). ∀L1,L2:T List.`
`    (no_repeats(T;L1) `` (||L1|| ≥ ||L2|| ) `` (∃x:T. ((x ∈ L2) ∧ (¬(x ∈ L1)))) `` (∃x:T. ((x ∈ L1) ∧ (¬(x ∈ L2)))))`

Proof

Definitions occuring in Statement :  no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` length: `||as||` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` ge: `i ≥ j ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Lemmas :  decidable__l_exists not_wf l_member_wf decidable__not decidable__l_member l_exists_iff not-l_exists l_all_iff deq-exists select_wf sq_stable__le select_member filter_wf5 bnot_wf lelt_wf length_wf equal_wf member_filter int_seg_subtype-nat false_wf less_than_wf iff_transitivity assert_wf eqof_wf iff_weakening_uiff assert_of_bnot safe-assert-deq int_seg_wf exists_wf ge_wf no_repeats_wf list_wf all_wf decidable_wf zero-le-nat non_neg_length length_wf_nat decidable__equal_int_seg le_wf nat_wf iff_weakening_equal squash_wf pigeon-hole length-filter-decreases less_than_transitivity1 less_than_irreflexivity set_wf l_exists_wf l_exists_functionality

Latex:
\mforall{}[T:Type]
\mforall{}eq:\mforall{}x,y:T.    Dec(x  =  y).  \mforall{}L1,L2:T  List.
(no\_repeats(T;L1)
{}\mRightarrow{}  (||L1||  \mgeq{}  ||L2||  )
{}\mRightarrow{}  (\mexists{}x:T.  ((x  \mmember{}  L2)  \mwedge{}  (\mneg{}(x  \mmember{}  L1))))
{}\mRightarrow{}  (\mexists{}x:T.  ((x  \mmember{}  L1)  \mwedge{}  (\mneg{}(x  \mmember{}  L2)))))

Date html generated: 2015_07_22-PM-00_17_23
Last ObjectModification: 2015_02_04-PM-04_39_28

Home Index