Nuprl Lemma : member-count-repeats1

[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀L:T List.  ((x ∈ map(λp.(fst(p));count-repeats(L,eq))) ⇐⇒ (x ∈ L))


Proof




Definitions occuring in Statement :  count-repeats: count-repeats(L,eq) l_member: (x ∈ l) map: map(f;as) list: List deq: EqDecider(T) uall: [x:A]. B[x] pi1: fst(t) all: x:A. B[x] iff: ⇐⇒ Q lambda: λx.A[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q not: ¬A false: False or: P ∨ Q uimplies: supposing a sq_type: SQType(T) guard: {T} uiff: uiff(P;Q) ifthenelse: if then else fi  btrue: tt bfalse: ff isl: isl(x) assert: b true: True
Lemmas referenced :  apply-alist-count-repeats list_wf deq_wf deq-member_wf l_member_wf map_wf nat_plus_wf pi1_wf count-repeats_wf assert_wf bnot_wf not_wf bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert-deq-member eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot isl-apply-alist and_wf equal_wf unit_wf2 isl_wf btrue_wf assert_elim apply-alist_wf bfalse_wf btrue_neq_bfalse
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation universeEquality equalityTransitivity equalitySymmetry independent_pairFormation productEquality lambdaEquality sqequalRule independent_functionElimination voidElimination dependent_functionElimination unionElimination instantiate cumulativity independent_isectElimination productElimination impliesFunctionality dependent_set_memberEquality unionEquality applyEquality setElimination rename setEquality natural_numberEquality

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:T  List.    ((x  \mmember{}  map(\mlambda{}p.(fst(p));count-repeats(L,eq)))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))



Date html generated: 2016_05_14-PM-03_23_04
Last ObjectModification: 2015_12_26-PM-06_21_15

Theory : decidable!equality


Home Index