Nuprl Lemma : imax-list-eq-implies

`∀L:ℤ List. ∀a:ℤ.  ((a ∈ L)) supposing ((imax-list(L) = a ∈ ℤ) and 0 < ||L||)`

Proof

Definitions occuring in Statement :  imax-list: `imax-list(L)` l_member: `(x ∈ l)` length: `||as||` list: `T List` less_than: `a < b` uimplies: `b supposing a` all: `∀x:A. B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}` prop: `ℙ`
Lemmas referenced :  member-less_than length_wf subtype_base_sq int_subtype_base imax-list-member equal_wf imax-list_wf less_than_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality intEquality hypothesisEquality hypothesis independent_isectElimination rename axiomEquality instantiate cumulativity dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination

Latex:
\mforall{}L:\mBbbZ{}  List.  \mforall{}a:\mBbbZ{}.    ((a  \mmember{}  L))  supposing  ((imax-list(L)  =  a)  and  0  <  ||L||)

Date html generated: 2016_05_14-PM-01_42_21
Last ObjectModification: 2015_12_26-PM-05_30_36

Theory : list_1

Home Index