Nuprl Lemma : select_cons_tl

[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ].  ([a as][i] as[i 1] ∈ T) supposing ((i ≤ ||as||) and 0 < i)


Definitions occuring in Statement :  select: L[n] length: ||as|| cons: [a b] list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B subtract: m natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a top: Top le: A ≤ B and: P ∧ Q all: x:A. B[x] decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q implies:  Q false: False prop: uiff: uiff(P;Q) subtract: m subtype_rel: A ⊆B less_than': less_than'(a;b) true: True
Lemmas referenced :  select-cons-tl select_wf subtract_wf decidable__le false_wf not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__lt not-lt-2 length_wf le-add-cancel-alt le_wf less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesisEquality independent_isectElimination hypothesis cumulativity natural_numberEquality productElimination dependent_functionElimination unionElimination independent_pairFormation lambdaFormation independent_functionElimination addEquality applyEquality lambdaEquality because_Cache minusEquality axiomEquality equalityTransitivity equalitySymmetry intEquality

\mforall{}[T:Type].  \mforall{}[a:T].  \mforall{}[as:T  List].  \mforall{}[i:\mBbbZ{}].
    ([a  /  as][i]  =  as[i  -  1])  supposing  ((i  \mleq{}  ||as||)  and  0  <  i)

Date html generated: 2016_05_14-AM-06_36_30
Last ObjectModification: 2015_12_26-PM-00_34_03

Theory : list_0

Home Index