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

`∀[A,V:Type]. ∀[eq:EqDecider(A)]. ∀[L:(A × V) List].`
`  uiff(values-for-distinct(eq;L) = [] ∈ (V List);L = [] ∈ ((A × V) List))`

Proof

Definitions occuring in Statement :  values-for-distinct: `values-for-distinct(eq;L)` nil: `[]` list: `T List` deq: `EqDecider(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` and: `P ∧ Q` uiff: `uiff(P;Q)` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` top: `Top` pi1: `fst(t)` deq: `EqDecider(T)` ge: `i ≥ j ` le: `A ≤ B` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` values-for-distinct: `values-for-distinct(eq;L)`
Lemmas referenced :  values-for-distinct-property equal-wf-T-base list_wf values-for-distinct_wf length_wf_nat equal_wf nat_wf length_wf remove-repeats_wf map_wf pi1_wf length_of_nil_lemma list_induction equal-wf-base-T map_nil_lemma remove_repeats_nil_lemma nil_wf equal-wf-base map_cons_lemma remove_repeats_cons_lemma length_of_cons_lemma non_neg_length filter_wf5 l_member_wf bnot_wf satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_formula_prop_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination productElimination independent_pairFormation cumulativity baseClosed productEquality because_Cache sqequalRule independent_pairEquality isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality dependent_set_memberEquality hyp_replacement Error :applyLambdaEquality,  intEquality setElimination rename lambdaEquality functionEquality independent_functionElimination voidElimination voidEquality lambdaFormation applyEquality setEquality natural_numberEquality independent_isectElimination dependent_pairFormation int_eqEquality computeAll addEquality

Latex:
\mforall{}[A,V:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[L:(A  \mtimes{}  V)  List].    uiff(values-for-distinct(eq;L)  =  [];L  =  [])

Date html generated: 2016_10_21-AM-10_39_41
Last ObjectModification: 2016_07_12-AM-05_49_54

Theory : decidable!equality

Home Index