### Nuprl Lemma : no_repeats-update-alist

`∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[a:A]. ∀[f:A ⟶ A]. ∀[L:(T × A) List].`
`  no_repeats(T;map(λp.(fst(p));update-alist(eq;L;x;a;n.f[n]))) supposing no_repeats(T;map(λp.(fst(p));L))`

Proof

Definitions occuring in Statement :  no_repeats: `no_repeats(T;l)` update-alist: `update-alist(eq;L;x;z;v.f[v])` map: `map(f;as)` list: `T List` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` pi1: `fst(t)` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  deq: `EqDecider(T)` subtype_rel: `A ⊆r B` decidable: `Dec(P)` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` squash: `↓T` less_than: `a < b` sq_type: `SQType(T)` it: `⋅` nil: `[]` colength: `colength(L)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` less_than': `less_than'(a;b)` le: `A ≤ B` cons: `[a / b]` pi1: `fst(t)` so_apply: `x[s1;s2;s3]` so_lambda: so_lambda3 update-alist: `update-alist(eq;L;x;z;v.f[v])` or: `P ∨ Q` guard: `{T}` prop: `ℙ` and: `P ∧ Q` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` ge: `i ≥ j ` false: `False` implies: `P `` Q` nat: `ℕ` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` cand: `A c∧ B` bool: `𝔹` unit: `Unit` btrue: `tt` eqof: `eqof(d)` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` true: `True`
Lemmas referenced :  istype-universe deq_wf istype-nat list_wf ifthenelse_wf list_ind_cons_lemma le_wf decidable__le int_term_value_add_lemma int_term_value_subtract_lemma int_formula_prop_not_lemma itermAdd_wf itermSubtract_wf intformnot_wf subtract_wf decidable__equal_int spread_cons_lemma int_subtype_base set_subtype_base subtype_base_sq subtract-1-ge-0 update-alist_wf pi1_wf map_wf istype-le istype-void colength_wf_list colength-cons-not-zero product_subtype_list no_repeats_wf nil_wf cons_wf no_repeats_singleton map_cons_lemma list_ind_nil_lemma map_nil_lemma list-cases int_formula_prop_eq_lemma intformeq_wf no_repeats_witness istype-less_than ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma istype-int intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat nat_properties equal-wf-T-base bool_wf assert_wf equal_wf no_repeats_cons l_member_wf bnot_wf not_wf eqof_wf istype-assert uiff_transitivity eqtt_to_assert safe-assert-deq iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot squash_wf true_wf member-update-alist1
Rules used in proof :  universeEquality functionIsType independent_pairEquality spreadEquality sqequalBase intEquality baseClosed closedConclusion baseApply imageElimination instantiate applyEquality productIsType dependent_set_memberEquality_alt because_Cache equalityIstype productElimination hypothesis_subsumption promote_hyp unionElimination productEquality functionIsTypeImplies inhabitedIsType isectIsTypeImplies applyLambdaEquality equalitySymmetry equalityTransitivity isect_memberEquality_alt voidElimination universeIsType independent_pairFormation sqequalRule Error :memTop,  dependent_functionElimination int_eqEquality lambdaEquality_alt dependent_pairFormation_alt independent_functionElimination approximateComputation independent_isectElimination natural_numberEquality intWeakElimination rename setElimination hypothesis hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid lambdaFormation_alt thin cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution equalityElimination hyp_replacement imageMemberEquality unionIsType

Latex:
\mforall{}[A,T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[a:A].  \mforall{}[f:A  {}\mrightarrow{}  A].  \mforall{}[L:(T  \mtimes{}  A)  List].
no\_repeats(T;map(\mlambda{}p.(fst(p));update-alist(eq;L;x;a;n.f[n])))
supposing  no\_repeats(T;map(\mlambda{}p.(fst(p));L))

Date html generated: 2020_05_19-PM-09_52_17
Last ObjectModification: 2019_12_26-AM-11_47_52

Theory : decidable!equality

Home Index