### Nuprl Lemma : alist-domain-first

`∀[A:Type]`
`  ∀d:A List. ∀f1:a:{a:A| (a ∈ d)}  ⟶ Top. ∀x:A. ∀eq:EqDecider(A).`
`    ((x ∈ d)`
`    `` (∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))))`

Proof

Definitions occuring in Statement :  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]` top: `Top` pi1: `fst(t)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` pair: `<a, b>` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` exists: `∃x:A. B[x]` prop: `ℙ` and: `P ∧ Q` int_seg: `{i..j-}` top: `Top` subtype_rel: `A ⊆r B` uimplies: `b supposing a` lelt: `i ≤ j < k` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` pi1: `fst(t)`
Lemmas referenced :  l_member-first l_member_wf deq_wf istype-top list_wf istype-universe int_seg_wf select-map istype-void subtype_rel_list top_wf int_seg_properties length_wf decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_wf istype-le istype-less_than pi1_wf_top select_wf map_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma map-length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_functionElimination hypothesis productElimination dependent_pairFormation_alt universeIsType functionIsType setIsType instantiate universeEquality independent_pairFormation promote_hyp natural_numberEquality setElimination rename sqequalRule isect_memberEquality_alt voidElimination applyEquality independent_isectElimination lambdaEquality_alt inhabitedIsType equalityTransitivity equalitySymmetry dependent_set_memberEquality_alt unionElimination imageElimination approximateComputation int_eqEquality productIsType because_Cache equalityIstype productEquality independent_pairEquality

Latex:
\mforall{}[A:Type]
\mforall{}d:A  List.  \mforall{}f1:a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  Top.  \mforall{}x:A.  \mforall{}eq:EqDecider(A).
((x  \mmember{}  d)
{}\mRightarrow{}  (\mexists{}i:\mBbbN{}||d||
((\mforall{}j:\mBbbN{}i.  (\mneg{}((fst(map(\mlambda{}x.<x,  f1  x>d)[j]))  =  x)))  \mwedge{}  ((fst(map(\mlambda{}x.<x,  f1  x>d)[i]))  =  x))))

Date html generated: 2019_10_16-AM-11_25_15
Last ObjectModification: 2018_11_30-AM-10_16_56

Theory : finite!partial!functions

Home Index