### Nuprl Lemma : seq-tl_wf

`∀[T:Type]. ∀[s:sequence(T)].  seq-tl(s) ∈ sequence(T) supposing 0 < ||s||`

Proof

Definitions occuring in Statement :  seq-tl: `seq-tl(s)` seq-len: `||s||` sequence: `sequence(T)` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  lelt: `i ≤ j < k` int_seg: `{i..j-}` true: `True` less_than': `less_than'(a;b)` le: `A ≤ B` top: `Top` subtype_rel: `A ⊆r B` subtract: `n - m` uiff: `uiff(P;Q)` prop: `ℙ` false: `False` implies: `P `` Q` rev_implies: `P `` Q` not: `¬A` and: `P ∧ Q` iff: `P `⇐⇒` Q` or: `P ∨ Q` decidable: `Dec(P)` all: `∀x:A. B[x]` nat: `ℕ` pi1: `fst(t)` seq-len: `||s||` sequence: `sequence(T)` seq-tl: `seq-tl(s)` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Rules used in proof :  universeEquality equalitySymmetry equalityTransitivity axiomEquality functionEquality functionExtensionality intEquality minusEquality voidEquality isect_memberEquality lambdaEquality applyEquality addEquality independent_isectElimination independent_functionElimination voidElimination lambdaFormation independent_pairFormation unionElimination hypothesisEquality dependent_functionElimination natural_numberEquality hypothesis because_Cache rename setElimination isectElimination extract_by_obid dependent_set_memberEquality dependent_pairEquality thin productElimination sqequalHypSubstitution sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].    seq-tl(s)  \mmember{}  sequence(T)  supposing  0  <  ||s||

Date html generated: 2018_07_25-PM-01_29_11
Last ObjectModification: 2018_06_15-PM-01_08_13

Theory : arithmetic

Home Index