Nuprl Lemma : no_repeats_l_index

[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[i:ℕ||L||].  index(L;L[i]) supposing no_repeats(T;L)


Proof




Definitions occuring in Statement :  l_index: index(L;x) no_repeats: no_repeats(T;l) select: L[n] length: ||as|| list: List deq: EqDecider(T) int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] natural_number: $n universe: Type sqequal: t
Definitions unfolded in proof :  l_index: index(L;x) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sq_type: SQType(T) all: x:A. B[x] implies:  Q guard: {T} prop:
Lemmas referenced :  no_repeats_mu_index subtype_base_sq int_subtype_base no_repeats_wf int_seg_wf length_wf list_wf deq_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis instantiate cumulativity intEquality dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination because_Cache natural_numberEquality universeEquality isect_memberFormation introduction sqequalAxiom sqequalRule isect_memberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[i:\mBbbN{}||L||].
    index(L;L[i])  \msim{}  i  supposing  no\_repeats(T;L)



Date html generated: 2016_05_14-PM-03_32_18
Last ObjectModification: 2015_12_26-PM-06_01_19

Theory : decidable!equality


Home Index