### Nuprl Lemma : l_before_select

`∀[T:Type]. ∀L:T List. ∀i,j:ℕ||L||.  L[j] before L[i] ∈ L supposing j < i`

Proof

Definitions occuring in Statement :  l_before: `x before y ∈ l` select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  l_before: `x before y ∈ l` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` prop: `ℙ` int_seg: `{i..j-}`
Lemmas referenced :  member-less_than sublist_pair less_than_wf int_seg_wf length_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache independent_isectElimination hypothesis rename hypothesisEquality dependent_functionElimination setElimination natural_numberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}i,j:\mBbbN{}||L||.    L[j]  before  L[i]  \mmember{}  L  supposing  j  <  i

Date html generated: 2016_05_14-AM-07_45_39
Last ObjectModification: 2015_12_26-PM-02_53_32

Theory : list_1

Home Index