### Nuprl Lemma : values-for-distinct-property

`∀[A,V:Type].`
`  ∀eq:EqDecider(A). ∀L:(A × V) List.`
`    ((||values-for-distinct(eq;L)|| = ||remove-repeats(eq;map(λp.(fst(p));L))|| ∈ ℤ)`
`    ∧ (∀i:ℕ||remove-repeats(eq;map(λp.(fst(p));L))||`
`         (<remove-repeats(eq;map(λp.(fst(p));L))[i], values-for-distinct(eq;L)[i]> ∈ L)))`

Proof

Definitions occuring in Statement :  values-for-distinct: `values-for-distinct(eq;L)` remove-repeats: `remove-repeats(eq;L)` l_member: `(x ∈ l)` select: `L[n]` length: `||as||` map: `map(f;as)` list: `T List` deq: `EqDecider(T)` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` pi1: `fst(t)` all: `∀x:A. B[x]` and: `P ∧ Q` lambda: `λx.A[x]` pair: `<a, b>` product: `x:A × B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s]` so_lambda: `λ2x.t[x]` member: `t ∈ T` cand: `A c∧ B` and: `P ∧ Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` top: `Top` values-for-distinct: `values-for-distinct(eq;L)` iff: `P `⇐⇒` Q` prop: `ℙ` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` implies: `P `` Q` not: `¬A` or: `P ∨ Q` decidable: `Dec(P)` le: `A ≤ B` lelt: `i ≤ j < k` uimplies: `b supposing a` int_seg: `{i..j-}` pi1: `fst(t)` rev_implies: `P `` Q` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` outl: `outl(x)` isl: `isl(x)`
Lemmas referenced :  deq_wf list_wf pi1_wf map_wf remove-repeats_wf length_wf int_seg_wf istype-void length-map select_member int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma istype-int itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le int_seg_properties select_wf member-remove-repeats isl-apply-alist l_member_wf squash_wf true_wf istype-universe select-map subtype_rel_list top_wf apply-alist_wf assert_elim btrue_wf bfalse_wf btrue_neq_bfalse
Rules used in proof :  because_Cache inhabitedIsType productIsType sqequalRule lambdaEquality_alt productEquality hypothesisEquality natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction universeIsType hypothesis independent_pairFormation cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution voidElimination isect_memberEquality_alt dependent_functionElimination int_eqEquality dependent_pairFormation_alt independent_functionElimination approximateComputation unionElimination equalitySymmetry equalityTransitivity independent_isectElimination rename setElimination productElimination hyp_replacement applyEquality imageElimination instantiate universeEquality independent_pairEquality imageMemberEquality baseClosed equalityIstype dependent_set_memberEquality_alt applyLambdaEquality

Latex:
\mforall{}[A,V:Type].
\mforall{}eq:EqDecider(A).  \mforall{}L:(A  \mtimes{}  V)  List.
((||values-for-distinct(eq;L)||  =  ||remove-repeats(eq;map(\mlambda{}p.(fst(p));L))||)
\mwedge{}  (\mforall{}i:\mBbbN{}||remove-repeats(eq;map(\mlambda{}p.(fst(p));L))||
(<remove-repeats(eq;map(\mlambda{}p.(fst(p));L))[i],  values-for-distinct(eq;L)[i]>  \mmember{}  L)))

Date html generated: 2019_10_15-AM-10_24_16
Last ObjectModification: 2019_08_05-PM-02_03_49

Theory : decidable!equality

Home Index